1
다음과 같은 부분적인 증거 고려 목표의 양쪽에서 생성자를 제거 :COQ :
1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
S n = S m
내가에서 S들 제거 할 것 :
Theorem test : forall (n m : nat),
n = m -> S n = S m.
Proof.
intros n m H.
이 시점까지 실행하면 다음 나에게 준다 목표는 목표를 달성 n = m. 이 작업을 수행하는 전술이 있습니까?
현재 질문은 [이] (http://stackoverflow.com/q/37490891/2747511) 질문과 [this one] (http://stackoverflow.com/q/13749403/2747511)의 중복으로 보입니다.). –
결국 이것은 본질적으로 단지 'match' 문이지만, Coq의 유형 시스템이'S n = S n' 유형을'cast'로'return '주석을 사용하는 고급 형식이라는 점에 주목하는 것이 흥미로울 것입니다. S n = S m '이다. eq_refl => eq_refl 끝과 함께'apply (_ = n2) return (S _ = S n2)와 일치 시키십시오. ' – larsr