이자벨에서 유도 적으로 정의 된 관계의 비 반사성을 어떻게 증명할 수 있습니까?

Question

이자벨에서 예를 들어 자연수의 불평등의 다음과 같은 정의를 생각해

inductive unequal :: "nat ⇒ nat ⇒ bool" where 
    zero_suc: "unequal 0 (Suc _)" | 
    suc_zero: "unequal (Suc _) 0" | 
    suc_suc: "unequal n m ⟹ unequal (Suc n) (Suc m)" 

내가 unequal의 irreflexivity을 증명하려는, 즉, ¬ unequal n n입니다. 설명을 위해이 날 처음 고안 보조 정리를 ¬ unequal (n + m) (n + m)을 증명하지 말라 : 처음 두 경우

lemma "¬ unequal (n + m) (n + m)" 
proof 
    assume "unequal (n + m) (n + m)" 
    then show False 
    proof (induction "n + m" "n + m" arbitrary: n m) 
    case zero_suc 
    then show False by simp 
    next 
    case suc_zero 
    then show False by simp 
    next 
    case suc_suc 
    then show False by presburger 
    qed 
qed 

을 False는 사소한 가정 0 = n + m 및 Suc _ = n + m에서 추론 할 수 있어야합니다.

나는 다음과 같은 패턴에 따라, 즉, ¬ unequal n n의 증거가 유사한 방법으로 수행 할 수 있다는 기대 : 특히

lemma "¬ unequal n n" 
proof 
    assume "unequal n n" 
    then show False 
    proof (induction n n arbitrary: n) 
    case zero_suc 
    then show False sorry 
    next 
    case suc_zero 
    then show False sorry 
    next 
    case suc_suc 
    then show False sorry 
    qed 
qed 

를, 내가 기대하는 처음 두 경우에, I 가정은 0 = n 및 Suc _ = n입니다. 그러나 나는 아무런 가정도 얻지 못한다. 즉, 아무것도 얻지 못하도록 False을 증명하도록 요청 받았다. 왜 그런가, 그리고 어떻게하면 불평등의 증거를 수행 할 수 있을까?

Answer 1

induction 방법은 다른 변수 인스턴스화 및 비 변수 인스턴스화를 처리합니다 (CVC4 포함) 슬레지 해머는 다음과 같이 증거를 완료하기 위해 우리를 권장합니다. 변수가 아닌 인스턴스화 t은 x ≡ t의 축약어로 x은 새로운 변수입니다. 결과적으로 유도는 x에서 수행되고 컨텍스트에는 정의 x ≡ t이 추가로 포함됩니다.

그러므로 첫 번째 증명에서 (induction "n + m" "n + m" arbitrary: n m)은 위에 설명한 효과를 갖는 (induction k ≡ "n + m" l ≡ "n + m" arbitrary: n m)과 같습니다. 두 번째 증명을 위해이 효과를 얻으려면 (induction n n arbitrary: n)을 (induction k ≡ n l ≡ n arbitrary: n)으로 대체해야합니다. 가정은 실제로 매우 간단 해 induction 메서드로 실행되는 사전 단순화 기가 False을 파생시킬 수 있습니다. 결과적으로 증명할만한 사례는 없을 것이며 proof - qed 블록을 by (induction k ≡ n l ≡ n arbitrary: n)으로 바꿀 수 있습니다.

Answer 2

귀하는 unequal을 (를) 이용할 수 있습니다. 대신 다음과 같이 n을 통해 입회해야합니다

lemma "¬ (unequal n n)" 
proof (induct n) 
    case 0 
    then show ?case sorry 
next 
    case (Suc n) 
    then show ?case sorry 
qed 

그런 다음 우리는 sorry로 표시된 하위 목표의 각 슬레지 해머를 사용할 수 있습니다.

lemma "¬ (unequal n n)" 
proof (induct n) 
    case 0 
    then show ?case using unequal.cases by blast 
next 
    case (Suc n) 
    then show ?case using unequal.cases by blast 
qed