optimized peano.pg a bit
This commit is contained in:
parent
832af2271f
commit
7f9d029ff9
2 changed files with 100 additions and 118 deletions
|
|
@ -185,15 +185,13 @@ def rec_rel_cond2 : cond2 rec_rel :=
|
|||
h2 n y (h Q h1 h2);
|
||||
|
||||
def rec_rel_total : total nat A rec_rel :=
|
||||
let (R := rec_rel)
|
||||
(P (x : nat) := exists A (R x))
|
||||
in
|
||||
let (P (x : nat) := exists A (rec_rel x)) in
|
||||
nat_ind P
|
||||
(exists_intro A (R zero) z rec_rel_cond1)
|
||||
(exists_intro A (rec_rel zero) z rec_rel_cond1)
|
||||
(fun (n : nat) (IH : P n) =>
|
||||
exists_elim A (P (suc n)) (R n) IH
|
||||
(fun (y0 : A) (hy : R n y0) =>
|
||||
exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 n y0 hy)))
|
||||
exists_elim A (P (suc n)) (rec_rel n) IH
|
||||
(fun (y0 : A) (hy : rec_rel n y0) =>
|
||||
exists_intro A (rec_rel (suc n)) (fS n y0) (rec_rel_cond2 n y0 hy)))
|
||||
end;
|
||||
|
||||
-- }}}
|
||||
|
|
@ -217,43 +215,42 @@ def rec_rel_alt (x : nat) (y : A) := or (alt_cond1 x y) (alt_cond2 x y);
|
|||
-- {{{ R = R2
|
||||
|
||||
-- {{{ R2 ⊆ R
|
||||
def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y -> rec_rel x y :=
|
||||
let (R := rec_rel)
|
||||
(R2 := rec_rel_alt)
|
||||
(ac1 := alt_cond1 x y)
|
||||
(ac2 := alt_cond2 x y)
|
||||
in
|
||||
fun (h : R2 x y) =>
|
||||
or_elim ac1 ac2 (R x y) h
|
||||
(fun (case1 : ac1) =>
|
||||
let
|
||||
(x0 := and_elim_l (eq nat x zero) (eq A y z) case1)
|
||||
def R2_sub_R_case1 (x : nat) (y : A) : alt_cond1 x y -> rec_rel x y :=
|
||||
fun (case1 : alt_cond1 x y) =>
|
||||
let (x0 := and_elim_l (eq nat x zero) (eq A y z) case1)
|
||||
(yz := and_elim_r (eq nat x zero) (eq A y z) case1)
|
||||
(a1 := (eq_sym A y z yz) (R zero) rec_rel_cond1)
|
||||
(a1 := (eq_sym A y z yz) (rec_rel zero) rec_rel_cond1)
|
||||
in
|
||||
(eq_sym nat x zero x0) (fun (n : nat) => R n y) a1
|
||||
end)
|
||||
(fun (case2 : ac2) =>
|
||||
(eq_sym nat x zero x0) (fun (n : nat) => rec_rel n y) a1
|
||||
end;
|
||||
|
||||
def R2_sub_R_case2 (x : nat) (y : A) : alt_cond2 x y -> rec_rel x y :=
|
||||
fun (case2 : alt_cond2 x y) =>
|
||||
let (h1 := cond_x2 x y)
|
||||
(h2 := cond_y2 x y)
|
||||
in
|
||||
exists_elim nat (R x y) h1 case2
|
||||
exists_elim nat (rec_rel x y) h1 case2
|
||||
(fun (x2 : nat) (hx2 : h1 x2) =>
|
||||
let (hpred := and_elim_l (pred x x2) (exists A (h2 x2)) hx2)
|
||||
(hex := and_elim_r (pred x x2) (exists A (h2 x2)) hx2)
|
||||
in
|
||||
exists_elim A (R x y) (h2 x2) hex
|
||||
exists_elim A (rec_rel x y) (h2 x2) hex
|
||||
(fun (y2 : A) (hy2 : h2 x2 y2) =>
|
||||
let (hpreim := and_elim_l (eq A y (fS x2 y2)) (R x2 y2) hy2)
|
||||
(hR := and_elim_r (eq A y (fS x2 y2)) (R x2 y2) hy2)
|
||||
let (hpreim := and_elim_l (eq A y (fS x2 y2)) (rec_rel x2 y2) hy2)
|
||||
(hR := and_elim_r (eq A y (fS x2 y2)) (rec_rel x2 y2) hy2)
|
||||
(a1 := rec_rel_cond2 x2 y2 hR)
|
||||
(a2 := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1)
|
||||
(a2 := (eq_sym A y (fS x2 y2) hpreim) (rec_rel (suc x2)) a1)
|
||||
in
|
||||
(eq_sym nat x (suc x2) hpred) (fun (n : nat) => R n y) a2
|
||||
end)
|
||||
(eq_sym nat x (suc x2) hpred) (fun (n : nat) => rec_rel n y) a2
|
||||
end)
|
||||
end)
|
||||
end;
|
||||
|
||||
def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y -> rec_rel x y :=
|
||||
fun (h : rec_rel_alt x y) =>
|
||||
or_elim (alt_cond1 x y) (alt_cond2 x y) (rec_rel x y) h
|
||||
(R2_sub_R_case1 x y)
|
||||
(R2_sub_R_case2 x y);
|
||||
-- }}}
|
||||
|
||||
-- {{{ R ⊆ R2
|
||||
|
|
@ -264,10 +261,7 @@ def R2_cond1 : cond1 rec_rel_alt :=
|
|||
(eq_refl A z));
|
||||
|
||||
def R2_cond2 : cond2 rec_rel_alt :=
|
||||
let (R := rec_rel)
|
||||
(R2 := rec_rel_alt)
|
||||
in
|
||||
fun (x2 : nat) (y2 : A) (h : R2 x2 y2) =>
|
||||
fun (x2 : nat) (y2 : A) (h : rec_rel_alt x2 y2) =>
|
||||
let (x := suc x2)
|
||||
(y := fS x2 y2)
|
||||
(cx2 := cond_x2 x y)
|
||||
|
|
@ -278,10 +272,9 @@ def R2_cond2 : cond2 rec_rel_alt :=
|
|||
(and_intro (pred x x2) (exists A cy2)
|
||||
(eq_refl nat x)
|
||||
(exists_intro A cy2 y2
|
||||
(and_intro (eq A y y) (R x2 y2)
|
||||
(and_intro (eq A y y) (rec_rel x2 y2)
|
||||
(eq_refl A y)
|
||||
(R2_sub_R x2 y2 h)))))
|
||||
end
|
||||
end;
|
||||
|
||||
|
||||
|
|
@ -299,15 +292,12 @@ def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
|
|||
def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
|
||||
|
||||
def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
|
||||
let (R2 := rec_rel_alt)
|
||||
(ac1 := alt_cond1 zero y)
|
||||
(ac2 := alt_cond2 zero y)
|
||||
(cx2 := cond_x2 zero y)
|
||||
let (cx2 := cond_x2 zero y)
|
||||
(cy2 := cond_y2 zero y)
|
||||
in fun (h : R2 zero y) =>
|
||||
or_elim ac1 ac2 (eq A y z) h
|
||||
(fun (case1 : ac1) => and_elim_r (eq nat zero zero) (eq A y z) case1)
|
||||
(fun (case2 : ac2) =>
|
||||
in fun (h : rec_rel_alt zero y) =>
|
||||
or_elim (alt_cond1 zero y) (alt_cond2 zero y) (eq A y z) h
|
||||
(fun (case1 : alt_cond1 zero y) => and_elim_r (eq nat zero zero) (eq A y z) case1)
|
||||
(fun (case2 : alt_cond2 zero y) =>
|
||||
exists_elim nat (eq A y z) cx2 case2
|
||||
(fun (x2 : nat) (h2 : cx2 x2) =>
|
||||
suc_nonzero x2
|
||||
|
|
@ -316,18 +306,15 @@ def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
|
|||
end;
|
||||
|
||||
def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc x2) y x2) :=
|
||||
let (R2 := rec_rel_alt)
|
||||
(x := suc x2)
|
||||
(ac1 := alt_cond1 x y)
|
||||
(ac2 := alt_cond2 x y)
|
||||
let (x := suc x2)
|
||||
(cx2 := cond_x2 x y)
|
||||
(cy2 := cond_y2 x y)
|
||||
(goal := exists A (cy2 x2))
|
||||
in
|
||||
fun (h : R2 x y) =>
|
||||
or_elim ac1 ac2 goal h
|
||||
(fun (case1 : ac1) => suc_nonzero x2 (and_elim_l (eq nat x zero) (eq A y z) case1) goal)
|
||||
(fun (case2 : ac2) =>
|
||||
fun (h : rec_rel_alt x y) =>
|
||||
or_elim (alt_cond1 x y) (alt_cond2 x y) goal h
|
||||
(fun (case1 : alt_cond1 x y) => suc_nonzero x2 (and_elim_l (eq nat x zero) (eq A y z) case1) goal)
|
||||
(fun (case2 : alt_cond2 x y) =>
|
||||
exists_elim nat goal cx2 case2
|
||||
(fun (x22 : nat) (hx22 : cx2 x22) =>
|
||||
let (hpred := and_elim_l (pred x x22) (exists A (cy2 x22)) hx22)
|
||||
|
|
@ -340,16 +327,14 @@ def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc
|
|||
end))
|
||||
end;
|
||||
|
||||
def R2_functional : fl nat A rec_rel_alt :=
|
||||
let (R := rec_rel)
|
||||
(R2 := rec_rel_alt)
|
||||
(f_in := fl_in nat A R2)
|
||||
in nat_ind f_in
|
||||
(fun (y1 y2 : A) (h1 : R2 zero y1) (h2 : R2 zero y2) =>
|
||||
def R2_functional_base_case : fl_in nat A rec_rel_alt zero :=
|
||||
fun (y1 y2 : A) (h1 : rec_rel_alt zero y1) (h2 : rec_rel_alt zero y2) =>
|
||||
eq_trans A y1 z y2
|
||||
(R2_zero y1 h1)
|
||||
(eq_sym A y2 z (R2_zero y2 h2)))
|
||||
(fun (x2 : nat) (IH : f_in x2) (y1 y2 : A) (h1 : R2 (suc x2) y1) (h2 : R2 (suc x2) y2) =>
|
||||
(eq_sym A y2 z (R2_zero y2 h2));
|
||||
|
||||
def R2_functional_inductive_step (x2 : nat) (IH : fl_in nat A rec_rel_alt x2) : fl_in nat A rec_rel_alt (suc x2) :=
|
||||
fun (y1 y2 : A) (h1 : rec_rel_alt (suc x2) y1) (h2 : rec_rel_alt (suc x2) y2) =>
|
||||
let (x := suc x2)
|
||||
(cy1 := cond_y2 x y1 x2)
|
||||
(cy2 := cond_y2 x y2 x2)
|
||||
|
|
@ -359,10 +344,10 @@ def R2_functional : fl nat A rec_rel_alt :=
|
|||
(fun (y12 : A) (h12 : cy1 y12) =>
|
||||
exists_elim A goal cy2 (R2_suc x2 y2 h2)
|
||||
(fun (y22 : A) (h22 : cy2 y22) =>
|
||||
let (y1_preim := and_elim_l (eq A y1 (fS x2 y12)) (R x2 y12) h12)
|
||||
(y2_preim := and_elim_l (eq A y2 (fS x2 y22)) (R x2 y22) h22)
|
||||
(R_x2_y12 := and_elim_r (eq A y1 (fS x2 y12)) (R x2 y12) h12)
|
||||
(R_x2_y22 := and_elim_r (eq A y2 (fS x2 y22)) (R x2 y22) h22)
|
||||
let (y1_preim := and_elim_l (eq A y1 (fS x2 y12)) (rec_rel x2 y12) h12)
|
||||
(y2_preim := and_elim_l (eq A y2 (fS x2 y22)) (rec_rel x2 y22) h22)
|
||||
(R_x2_y12 := and_elim_r (eq A y1 (fS x2 y12)) (rec_rel x2 y12) h12)
|
||||
(R_x2_y22 := and_elim_r (eq A y2 (fS x2 y22)) (rec_rel x2 y22) h22)
|
||||
(R2_x2_y12 := R_sub_R2 x2 y12 R_x2_y12)
|
||||
(R2_x2_y22 := R_sub_R2 x2 y22 R_x2_y22)
|
||||
(y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22)
|
||||
|
|
@ -373,9 +358,11 @@ def R2_functional : fl nat A rec_rel_alt :=
|
|||
(eq_cong A A y12 y22 (fun (y : A) => fS x2 y) y12_y22)
|
||||
(eq_sym A y2 (fS x2 y22) y2_preim))
|
||||
end))
|
||||
end)
|
||||
end;
|
||||
|
||||
def R2_functional : fl nat A rec_rel_alt :=
|
||||
nat_ind (fl_in nat A rec_rel_alt) R2_functional_base_case R2_functional_inductive_step;
|
||||
|
||||
def R_functional : fl nat A rec_rel :=
|
||||
fun (n : nat) (y1 y2 : A) (h1 : rec_rel n y1) (h2 : rec_rel n y2) =>
|
||||
R2_functional n y1 y2 (R_sub_R2 n y1 h1) (R_sub_R2 n y2 h2);
|
||||
|
|
@ -414,13 +401,8 @@ def eq2 (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
|
|||
def rec_def_sat_zero : eq1 rec_def := R_functional zero (rec_def zero) z (rec_def_sat zero) rec_rel_cond1;
|
||||
|
||||
-- f n = y -> f (suc n) = fS n y
|
||||
def rec_def_sat_suc : eq2 rec_def :=
|
||||
fun (n : nat) =>
|
||||
let (y := rec_def n)
|
||||
(RSnfy := rec_rel_cond2 n y (rec_def_sat n))
|
||||
in
|
||||
R_functional (suc n) (rec_def (suc n)) (fS n y) (rec_def_sat (suc n)) RSnfy
|
||||
end;
|
||||
def rec_def_sat_suc : eq2 rec_def := fun (n : nat) =>
|
||||
R_functional (suc n) (rec_def (suc n)) (fS n (rec_def n)) (rec_def_sat (suc n)) (rec_rel_cond2 n (rec_def n) (rec_def_sat n));
|
||||
|
||||
-- }}}
|
||||
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ category: Math
|
|||
build-type: Simple
|
||||
|
||||
extra-doc-files: CHANGELOG.md
|
||||
, README.org
|
||||
, README.md
|
||||
|
||||
common warnings
|
||||
ghc-options: -Wall
|
||||
|
|
|
|||
Loading…
Reference in a new issue