From 7f9d029ff90d9f80fc63a151168cec615b9f99ac Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 6 Dec 2024 21:23:35 -0800 Subject: [PATCH] optimized peano.pg a bit --- examples/peano.pg | 216 +++++++++++++++++++++------------------------- perga.cabal | 2 +- 2 files changed, 100 insertions(+), 118 deletions(-) diff --git a/examples/peano.pg b/examples/peano.pg index e194897..f1561e1 100644 --- a/examples/peano.pg +++ b/examples/peano.pg @@ -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_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) (rec_rel zero) rec_rel_cond1) + in + (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 (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 (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)) (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) (rec_rel (suc x2)) a1) + in + (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 := - 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) - (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) - in - (eq_sym nat x zero x0) (fun (n : nat) => R n y) a1 - end) - (fun (case2 : ac2) => - let (h1 := cond_x2 x y) - (h2 := cond_y2 x y) - in - exists_elim nat (R 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 - (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) - (a1 := rec_rel_cond2 x2 y2 hR) - (a2 := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1) - in - (eq_sym nat x (suc x2) hpred) (fun (n : nat) => R n y) a2 - end) - end) - end) - end; + 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,24 +261,20 @@ 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) + fun (x2 : nat) (y2 : A) (h : rec_rel_alt x2 y2) => + let (x := suc x2) + (y := fS x2 y2) + (cx2 := cond_x2 x y) + (cy2 := cond_y2 x y x2) in - fun (x2 : nat) (y2 : A) (h : R2 x2 y2) => - let (x := suc x2) - (y := fS x2 y2) - (cx2 := cond_x2 x y) - (cy2 := cond_y2 x y x2) - in - or_intro_r (alt_cond1 x y) (alt_cond2 x y) - (exists_intro nat cx2 x2 - (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) - (eq_refl A y) - (R2_sub_R x2 y2 h))))) - end + or_intro_r (alt_cond1 x y) (alt_cond2 x y) + (exists_intro nat cx2 x2 + (and_intro (pred x x2) (exists A cy2) + (eq_refl nat x) + (exists_intro A cy2 y2 + (and_intro (eq A y y) (rec_rel x2 y2) + (eq_refl A y) + (R2_sub_R x2 y2 h))))) 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,41 +327,41 @@ def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc end)) end; +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)); + +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) + (goal := eq A y1 y2) + in + exists_elim A goal cy1 (R2_suc x2 y1 h1) + (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)) (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) + in + eq_trans A y1 (fS x2 y12) y2 + y1_preim + (eq_trans A (fS x2 y12) (fS x2 y22) y2 + (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; + 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) => - 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) => - let (x := suc x2) - (cy1 := cond_y2 x y1 x2) - (cy2 := cond_y2 x y2 x2) - (goal := eq A y1 y2) - in - exists_elim A goal cy1 (R2_suc x2 y1 h1) - (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) - (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) - in - eq_trans A y1 (fS x2 y12) y2 - y1_preim - (eq_trans A (fS x2 y12) (fS x2 y22) y2 - (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; + 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) => @@ -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)); -- }}} diff --git a/perga.cabal b/perga.cabal index ae11988..7e806a4 100644 --- a/perga.cabal +++ b/perga.cabal @@ -18,7 +18,7 @@ category: Math build-type: Simple extra-doc-files: CHANGELOG.md - , README.org + , README.md common warnings ghc-options: -Wall