在Coq的

Question

證明無限電感值的不存在

假設我有一個很簡單的感應型：

Inductive ind : Set := 
    | ind0 : ind 
    | ind1 : ind -> ind. 

，我想證明某些值可以不存在。具體來說，不可能有非正當的價值觀：~exists i, i = ind1 i。

 

我環顧四周互聯網上的位，並與一無所獲。我能寫：

Fixpoint depth (i : ind) : nat := 
    match i with 
    | ind0 => 0 
    | ind1 i2 => 1 + depth i2 
    end. 

Goal ~exists i, i = ind1 i. 
Proof. 
    intro. inversion_clear H. 
    remember (depth x) as d. 
    induction d. 
     rewrite H0 in Heqd; simpl in Heqd. discriminate. 
     rewrite H0 in Heqd; simpl in Heqd. injection Heqd. assumption. 
Qed. 

其工作原理，但似乎真的醜陋和非一般。

Answer 1

我不認爲有一個通用的方法來證明這樣的目標。根據我的經驗，這看起來並不是什麼問題。對你來說，還有一個更簡單的證明，使用congruence戰術：

Inductive ind : Type := 
| ind0 : ind 
| ind1 : ind -> ind. 

Goal ~exists i, i = ind1 i. 
Proof. 
    intros [x Hx]. induction x; congruence. 
Qed. 

Answer 2

我會證明forall n1, n1 = Succ n1 <-> False代替，並把它放在一個autorewrite數據庫。

Require Import Coq.Setoids.Setoid. 

Lemma L1 : forall P1, (P1 <-> P1) <-> True. 
Proof. tauto. Qed. 

Hint Rewrite L1 : LogHints. 

Lemma L2 : forall (S1 : Set) (e1 : S1), e1 = e1 <-> True. 
Proof. tauto. Qed. 

Hint Rewrite L2 : LogHints. 

Lemma L3 : forall n1, O = S n1 <-> False. 
Proof. 
intros. split. 
    intros H1. inversion H1. 
    tauto. 
Qed. 

Lemma L4 : forall n1, S n1 = O <-> False. 
Proof. 
intros. split. 
    intros H1. inversion H1. 
    tauto. 
Qed. 

Lemma L5 : forall n1 n2, S n1 = S n2 <-> n1 = n2. 
Proof. 
intros. split. 
    intros H1. inversion H1 as [H2]. tauto. 
    intros H1. rewrite H1. tauto. 
Qed. 

Hint Rewrite L3 L4 L5 : NatHints. 

Lemma L6 : forall n1, n1 = S n1 <-> False. 
Proof. 
induction n1 as [| n1 H1]; 
    autorewrite with LogHints NatHints; 
    tauto. 
Qed. 

Lemma L7 : forall n1, S n1 = n1 <-> False. 
Proof. 
induction n1 as [| n1 H1]; 
    autorewrite with LogHints NatHints; 
    tauto. 
Qed. 

Hint Rewrite L6 L7 : NatHints. 

Answer 3

另外，你可以編程你的證明。

Definition IsO (n1 : nat) : Prop := 
    match n1 with 
    | O => True 
    | S _ => False 
    end. 

Definition eq_O {n1 : nat} (H1 : O = n1) : IsO n1 := 
    match H1 with 
    | eq_refl => I 
    end. 

Definition O_S_impl {n1 : nat} (H1 : O = S n1) : False := eq_O H1. 

Definition S_S_impl {n1 n2 : nat} (H1 : S n1 = S n2) : n1 = n2 := 
    match H1 with 
    | eq_refl => eq_refl 
    end. 

Fixpoint nat_inf'' {n1 : nat} : n1 = S n1 -> False := 
    match n1 with 
    | O => fun H1 => O_S_impl H1 
    | S _ => fun H1 => nat_inf'' (S_S_impl H1) 
    end. 

Definition nat_inf' (H1 : exists n1, n1 = S n1) : False := 
    match H1 with 
    | ex_intro _ H2 => nat_inf'' H2 
    end. 

Definition nat_inf : ~ exists n1, n1 = S n1 := nat_inf'.