Skip to content

Instantly share code, notes, and snippets.

@yuga

yuga/Logic_five_not_even.v

Last active Aug 29, 2015
Embed
What would you like to do?
Definition five_not_even' : ~ ev 5 :=
fun (Hev5 : ev 5) =>
(fun (P : nat -> Prop) (* evの帰納法の原理*)
(f : P 0)
(f0 : forall n : nat, ev n -> P n -> P (S (S n))) =>
fix F (n : nat) (e : ev n) {struct e} : P n := (* eについて減少 *)
match e in (ev n0) return (P n0) with
| ev_0 => f
| ev_SS n1 ev1 => f0 n1 ev1 (F n1 ev1)
end)
(fun n : nat => ev (S n) -> False)
(fun ev1 : ev 1 => (* 基底 *)
(fun H : 1 = 1 -> False => H eq_refl)
match ev1 in (ev n0) return (n0 = 1 -> False) with
| ev_0 =>
fun H1 : 0 = 1 =>
eq_ind 0 (fun n1 : nat => match n1 with
| 0 => True
| S _ => False
end) I 1 H1
| ev_SS n2 Hev2 =>
fun H2 : S (S n2) = 1 =>
eq_ind (S (S n2)) (fun n3 : nat => match n3 with
| 0 => False
| 1 => False
| S (S _) => True
end) I 1 H2
end
)
(fun (n : nat) (e : ev n) (IHev : ev (S n) -> False) => (* 帰納 *)
fun evn : ev (S (S (S n))) =>
(fun H : S (S (S n)) = S (S (S n)) -> False => H eq_refl)
match evn in (ev n0) return (n0 = S (S (S n)) -> False) with
| ev_0 =>
fun H1 : 0 = S (S (S n)) =>
eq_ind 0 (fun n1 : nat => match n1 with
| 0 => True
| S _ => False
end) I (S (S (S n))) H1
| ev_SS n2 Hev2 =>
fun H2 : S (S n2) = S (S (S n)) =>
(fun H3 : n2 = S n => (* 帰納法の仮定と一致のためコンストラクタを削る *)
eq_ind
(S n) (* x : A *)
(fun n3 : nat => ev n3 -> False) (* P : A -> Prop *)
(fun H4 : ev (S n) => IHev H4) (* f : P x *)
n2 (* y : A *)
(eq_sym H3) (* H3とはx, yの順が逆だから*) (* e : x = y *)
)
(f_equal (fun e : nat => match e : nat with
| 0 => n2
| 1 => n2
| S (S n4) => n4
end) H2) (* コンストラクタ削るのに使う *)
Hev2
end
)
4 (ev_SS 2 (ev_SS 0 ev_0)) Hev5.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment