COQ :

다음과 같은 부분적인 증거 고려 목표의 양쪽에서 생성자를 제거 :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. 이 작업을 수행하는 전술이 있습니까?

출처

2017-05-12 Carl Patenaude Poulin

현재 질문은 [이] (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

f_equal 전술을 찾고 있습니다.

출처

2017-05-12 15:50:47 Vinz

답변

관련 문제