From c0e0c376896cdca645f8ad1dbf0fc9754375b81c Mon Sep 17 00:00:00 2001 From: William Ball Date: Thu, 5 Dec 2024 18:56:41 -0800 Subject: [PATCH] more peano, fixed bug in checking ascriptions of definitions --- examples/peano.pg | 512 +++++++++++++++++++++++++--------------------- lib/Errors.hs | 4 +- lib/Program.hs | 1 + 3 files changed, 281 insertions(+), 236 deletions(-) diff --git a/examples/peano.pg b/examples/peano.pg index 5b26ec8..201ae76 100644 --- a/examples/peano.pg +++ b/examples/peano.pg @@ -151,7 +151,7 @@ def suc_or_zero : forall (n : nat), szc n := -- 1) Q 0 z and -- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y), -- Q x y. --- In more math lingo, we take R to be the intersection of every relation +-- In more mathy lingo, we take R to be the intersection of every relation -- satisfying 1 and 2. From there we will, with much effort, prove that R is -- actually a function satisfying the equations we want it to. @@ -181,10 +181,10 @@ def rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A h2 n y (h Q h1 h2); def rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) := - let (R := rec_rel A z fS) + let (R := rec_rel A z fS) (P (x : nat) := exists A (R x)) - (c1 := cond1 A z fS) - (c2 := cond2 A z fS) + (c1 := cond1 A z fS) + (c2 := cond2 A z fS) in nat_ind P (exists_intro A (R zero) z (rec_rel_cond1 A z fS)) @@ -218,8 +218,8 @@ def rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) := -- {{{ R2 ⊆ R def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) : rec_rel_alt A z fS x y -> rec_rel A z fS x y := - let (R := rec_rel A z fS) - (R2 := rec_rel_alt A z fS) + let (R := rec_rel A z fS) + (R2 := rec_rel_alt A z fS) (ac1 := alt_cond1 A z x y) (ac2 := alt_cond2 A z fS x y) in @@ -240,14 +240,14 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) : 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) + (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 A z fS x2 y2 hR) - (a2 := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1) + (hR := and_elim_r (eq A y (fS x2 y2)) (R x2 y2) hy2) + (a1 := rec_rel_cond2 A z fS 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) @@ -264,12 +264,12 @@ def R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A (eq_refl A z)); def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) := - let (R := rec_rel A z fS) + let (R := rec_rel A z fS) (R2 := rec_rel_alt A z fS) in fun (x2 : nat) (y2 : A) (h : R2 x2 y2) => - let (x := suc x2) - (y := fS x2 y2) + let (x := suc x2) + (y := fS x2 y2) (cx2 := cond_x2 A z fS x y) (cy2 := cond_y2 A z fS x y x2) in @@ -286,7 +286,7 @@ def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A def R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) : rec_rel A z fS x y -> rec_rel_alt A z fS x y := - let (R := rec_rel A z fS) + let (R := rec_rel A z fS) (R2 := rec_rel_alt A z fS) in fun (h : R x y) => @@ -305,7 +305,7 @@ def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x; def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) : rec_rel_alt A z fS zero y -> eq A y z := - let (R2 := rec_rel_alt A z fS) + let (R2 := rec_rel_alt A z fS) (ac1 := alt_cond1 A z zero y) (ac2 := alt_cond2 A z fS zero y) (cx2 := cond_x2 A z fS zero y) @@ -323,12 +323,12 @@ def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) : def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) : rec_rel_alt A z fS (suc x2) y -> exists A (cond_y2 A z fS (suc x2) y x2) := - let (R2 := rec_rel_alt A z fS) - (x := suc x2) - (ac1 := alt_cond1 A z x y) - (ac2 := alt_cond2 A z fS x y) - (cx2 := cond_x2 A z fS x y) - (cy2 := cond_y2 A z fS x y) + let (R2 := rec_rel_alt A z fS) + (x := suc x2) + (ac1 := alt_cond1 A z x y) + (ac2 := alt_cond2 A z fS x y) + (cx2 := cond_x2 A z fS x y) + (cy2 := cond_y2 A z fS x y) (goal := exists A (cy2 x2)) in fun (h : R2 x y) => @@ -337,8 +337,8 @@ def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) : (fun (case2 : ac2) => 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) - (hgoal := and_elim_r (pred x x22) (exists A (cy2 x22)) hx22) + let (hpred := and_elim_l (pred x x22) (exists A (cy2 x22)) hx22) + (hgoal := and_elim_r (pred x x22) (exists A (cy2 x22)) hx22) (x2_x22 := suc_inj x2 x22 hpred) in (eq_sym nat x2 x22 x2_x22) @@ -348,8 +348,8 @@ def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) : end; def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) := - let (R := rec_rel A z fS) - (R2 := rec_rel_alt A z fS) + let (R := rec_rel A z fS) + (R2 := rec_rel_alt A z fS) (f_in := fl_in nat A R2) in nat_ind f_in (fun (y1 y2 : A) (h1 : R2 zero y1) (h2 : R2 zero y2) => @@ -357,22 +357,22 @@ def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A (R2_zero A z fS y1 h1) (eq_sym A y2 z (R2_zero A z fS 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 A z fS x y1 x2) - (cy2 := cond_y2 A z fS x y2 x2) + let (x := suc x2) + (cy1 := cond_y2 A z fS x y1 x2) + (cy2 := cond_y2 A z fS x y2 x2) (goal := eq A y1 y2) in exists_elim A goal cy1 (R2_suc A z fS x2 y1 h1) (fun (y12 : A) (h12 : cy1 y12) => exists_elim A goal cy2 (R2_suc A z fS 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)) (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 A z fS x2 y12 R_x2_y12) (R2_x2_y22 := R_sub_R2 A z fS x2 y22 R_x2_y22) - (y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22) + (y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22) in eq_trans A y1 (fS x2 y12) y2 y1_preim @@ -383,213 +383,259 @@ def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A end) end; +def R_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel A z fS) := + let (R := rec_rel A z fS) + (sub := R_sub_R2 A z fS) + in + fun (n : nat) (y1 y2 : A) (h1 : R n y1) (h2 : R n y2) => + R2_functional A z fS n y1 y2 (sub n y1 h1) (sub n y2 h2) + end; + -- }}} +-- {{{ Actually defining the function + def rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A := exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x) (fun (y : A) (_ : rec_rel A z fS x y) => y); -- }}} --- -- For any such equations, there exists a function. --- rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom; --- --- -- Here's equation one. --- rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) := --- eq A (f zero) fzero; --- --- -- And equation two. --- rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) := --- forall (n : nat) (y : A), --- eq A (f n) y -> eq A (f (suc n)) (fsuc n y); --- --- -- Said function satisfies the equations. --- -- It satisfies equation one. --- rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) : --- rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom; --- --- -- And two. --- rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) : --- rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom; --- --- -- And, finally, this function is unique in the sense that if any other function --- -- also satisfies the equations, it takes the same values as rec_def. --- rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) : --- rec_cond_zero A fzero fsuc f -> --- rec_cond_suc A fzero fsuc f -> --- rec_cond_zero A fzero fsuc g -> --- rec_cond_suc A fzero fsuc g -> --- forall (x : nat), eq A (f x) (g x) := axiom; --- --- -- Now we can safely define addition. --- --- -- First, here's the RHS of equation 2 as a function, since it will show up --- -- multiple times. --- psuc (_ r : nat) := suc r; --- --- -- And here's plus! --- plus (n : nat) : nat -> nat := rec_def nat n psuc; --- --- -- The first equation manifests itself as the familiar --- -- n + 0 = 0. --- plus_0_r (n : nat) : eq nat (plus n zero) n := --- rec_def_sat_zero nat n psuc; --- --- -- The second equation, after a bit of massaging, manifests itself as the --- -- likewise familiar --- -- n + suc m = suc (n + m). --- plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) := --- rec_def_sat_suc nat n psuc m (plus n m) (eq_refl nat (plus n m)); --- +-- {{{ It satisfies the properties we want it to + +-- Kind of stupidly, we still need one more axiom. Due to how existentials are +-- defined, even though rec_def n is defined to be the y such that R n y, we +-- can't actually conclude that R n (rec_def n). + +-- We need to assert that, even if you "forget" that a value came from an +-- existential, it still satisfies the property it definitionally is supposed +-- to satisfy. This annoying problem would be subverted with proper Σ-types, +-- provided they had η-equality. +axiom definite_description (A : *) (P : A -> *) (h : exists A P) : + P (exists_elim A A P h (fun (x : A) (_ : P x) => x)); + +-- Now we can use this axiom to prove that R n (rec_def n). +def rec_def_sat (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : rec_rel A z fS x (rec_def A z fS x) := + definite_description A (rec_rel A z fS x) (rec_rel_total A z fS x); + +def eq1 (A : *) (z : A) (f : nat -> A) := eq A (f zero) z; + +def eq2 (A : *) (z : A) (fS : nat -> A -> A) (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n)); + +-- f zero = z +def rec_def_sat_zero (A : *) (z : A) (fS : nat -> A -> A) : eq1 A z (rec_def A z fS) := + let (f := rec_def A z fS) in + R_functional A z fS zero (f zero) z + (rec_def_sat A z fS zero) + (rec_rel_cond1 A z fS) + end; + +-- f n = y -> f (suc n) = fS n y +def rec_def_sat_suc (A : *) (z : A) (fS : nat -> A -> A) : eq2 A z fS (rec_def A z fS) := + fun (n : nat) => + let (R := rec_rel A z fS) + (f := rec_def A z fS) + (y := f n) + (Rf := rec_def_sat A z fS) + (RSnfy := rec_rel_cond2 A z fS n y (Rf n)) + in + R_functional A z fS (suc n) (f (suc n)) (fS n y) (Rf (suc n)) RSnfy + end; + +-- }}} + +-- {{{ The function satisfying these equations is unique + +def rec_def_unique (A : *) (z : A) (fS : nat -> A -> A) (f g : nat -> A) + (h1f : eq1 A z f) (h2f : eq2 A z fS f) (h1g : eq1 A z g) (h2g : eq2 A z fS g) + : forall (n : nat), eq A (f n) (g n) := + nat_ind (fun (n : nat) => eq A (f n) (g n)) + -- base case: f 0 = g 0 + (eq_trans A (f zero) z (g zero) h1f (eq_sym A (g zero) z h1g)) + + -- Inductive step + (fun (n : nat) (IH : eq A (f n) (g n)) => + -- f (suc n) = fS n (f n) + -- = fS n (g n) + -- = g (suc n) + eq_trans A (f (suc n)) (fS n (f n)) (g (suc n)) + -- f (suc n) = fS n (f n) + (h2f n) + -- fS n (f n) = g (suc n) + (eq_trans A (fS n (f n)) (fS n (g n)) (g (suc n)) + -- fS n (f n) = fS n (g n) + (eq_cong A A (f n) (g n) (fS n) IH) + -- fS n (g n) = g (suc n) + (eq_sym A (g (suc n)) (fS n (g n)) (h2g n)))); + +-- }}} + +-- }}} + +-- Now we can safely define addition. + +-- First, here's the RHS of equation 2 as a function, since it will show up +-- multiple times. +def psuc (_ r : nat) := suc r; + +-- And here's plus! +def plus (n : nat) : nat -> nat := rec_def nat n psuc; + +-- The first equation manifests itself as the familiar +-- n + 0 = 0. +def plus_0_r (n : nat) : eq nat (plus n zero) n := + rec_def_sat_zero nat n psuc; + +-- The second equation, after a bit of massaging, manifests itself as the +-- likewise familiar +-- n + suc m = suc (n + m). +def plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) := + rec_def_sat_suc nat n psuc m; + -- -- We can now prove 1 + 1 = 2! --- one_plus_one_two : eq nat (plus one one) two := --- -- 1 + (suc zero) = suc (1 + zero) = suc one --- eq_trans nat (plus one one) (suc (plus one zero)) two +def one_plus_one_two : eq nat (plus one one) two := + -- 1 + (suc zero) = suc (1 + zero) = suc one + eq_trans nat (plus one one) (suc (plus one zero)) two + + -- 1 + (suc zero) = suc (1 + zero) + (plus_s_r one zero) + + -- suc (1 + zero) = suc one + (eq_cong nat nat (plus one zero) one suc (plus_0_r one)); + +-- We have successfully defined addition! Note that evaluating 1 + 1 to 2 +-- requires a proof, unfortunately, since this computation isn't visible to +-- perga. -- --- -- 1 + (suc zero) = suc (1 + zero) --- (plus_s_r one zero) --- --- -- suc (1 + zero) = suc one --- (eq_cong nat nat (plus one zero) one suc (plus_0_r one)); --- --- -- --- -- We have successfully defined addition! Note that evaluating 1 + 1 to 2 --- -- requires a proof, unfortunately, since this computation isn't visible to --- -- perga. --- -- --- -- We will now prove a couple standard properties of addition. --- -- --- --- -- First, associativity, namely that n + (m + p) = (n + m) + p. --- plus_assoc : assoc nat plus := --- -- We prove this via induction on p. --- nat_ind --- (fun (p : nat) => --- forall (n m : nat), --- eq nat (plus n (plus m p)) (plus (plus n m) p)) --- --- -- Base case: p = 0 --- -- WTS n + (m + 0) = (n + m) + 0 --- (fun (n m : nat) => --- -- n + (m + 0) = n + m = (n + m) + 0 --- (eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero) --- -- n + (m + 0) = n + m --- (eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m)) --- --- -- n + m = (n + m) + 0 --- (eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m))))) --- --- -- Inductive step: IH = n + (m + p) = (n + m) + p --- (fun (p : nat) (IH : forall (n m : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)) (n m : nat) => --- -- WTS n + (m + suc p) = (n + m) + suc p --- -- n + (m + suc p) = n + suc (m + p) --- -- = suc (n + (m + p)) --- -- = suc ((n + m) + p) --- -- = (n + m) + suc p --- eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p)) --- --- -- n + (m + suc p) = n + suc (m + p) --- (eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p)) --- --- -- n + suc (m + p) = (n + m) + suc p --- (eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p)) --- -- n + suc (m + p) = suc (n + (m + p)) --- (plus_s_r n (plus m p)) --- --- -- suc (n + (m + p)) = (n + m) + suc p --- (eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p)) --- -- suc (n + (m + p)) = suc ((n + m) + p) --- (eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc (IH n m)) --- --- -- suc ((n + m) + p) = (n + m) + suc p --- (eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p)) --- (plus_s_r (plus n m) p))))); --- --- -- Up next is commutativity, but we will need a couple lemmas first. --- --- -- First, we will show that 0 + n = n. --- plus_0_l : forall (n : nat), eq nat (plus zero n) n := --- -- We prove this by induction on n. --- nat_ind (fun (n : nat) => eq nat (plus zero n) n) --- -- base case: WTS 0 + 0 = 0 --- -- This is just plus_0_r 0 --- (plus_0_r zero) --- --- -- inductive case --- (fun (n : nat) (IH : eq nat (plus zero n) n) => --- -- WTS 0 + (suc n) = suc n --- -- 0 + (suc n) = suc (0 + n) = suc n --- eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n) --- -- 0 + (suc n) = suc (0 + n) --- (plus_s_r zero n) --- --- -- suc (0 + n) = suc n --- (eq_cong nat nat (plus zero n) n suc IH)); --- --- -- Next, we will show that (suc n) + m = suc (n + m). --- plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) := --- -- We proceed by induction on m. --- nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m))) --- -- base case: (suc n) + 0 = suc (n + 0) --- -- (suc n) + 0 = suc n = suc (n + 0) --- (eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero)) --- -- (suc n) + 0 = suc n --- (plus_0_r (suc n)) --- --- -- suc n = suc (n + 0) --- (eq_cong nat nat n (plus n zero) suc --- -- n = n + 0 --- (eq_sym nat (plus n zero) n (plus_0_r n)))) --- --- -- inductive case --- -- IH = suc n + m = suc (n + m) --- (fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) => --- -- WTS suc n + suc m = suc (n + suc m) --- -- suc n + suc m = suc (suc n + m) --- -- = suc (suc (n + m)) --- -- = suc (n + suc m) --- (eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m))) --- -- suc n + suc m = suc (suc n + m) --- (plus_s_r (suc n) m) --- --- -- suc (suc n + m) = suc (n + suc m) --- (eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m))) --- -- suc (suc n + m) = suc (suc (n + m)) --- (eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH) --- --- -- suc (suc (n + m)) = suc (n + suc m) --- (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc --- -- suc (n + m) = n + suc m --- (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m)))))); --- --- -- Finally, we can prove commutativity. --- plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) := --- -- As usual, we proceed by induction. --- nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n)) --- --- -- Base case: WTS n + 0 = 0 + n --- -- n + 0 = n = 0 + n --- (eq_trans nat (plus n zero) n (plus zero n) --- -- n + 0 = n --- (plus_0_r n) --- --- -- n = 0 + n --- (eq_sym nat (plus zero n) n (plus_0_l n))) --- --- -- Inductive step: --- (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) => --- -- WTS n + suc m = suc m + n --- -- n + suc m = suc (n + m) --- -- = suc (m + n) --- -- = suc m + n --- (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n) --- -- n + suc m = suc (n + m) --- (plus_s_r n m) --- --- -- suc (n + m) = suc m + n --- (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n) --- -- suc (n + m) = suc (m + n) --- (eq_cong nat nat (plus n m) (plus m n) suc IH) --- --- -- suc (m + n) = suc m + n --- (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n))))); +-- We will now prove a couple standard properties of addition. + +-- First, associativity, namely that n + (m + p) = (n + m) + p. +def plus_assoc : assoc nat plus := fun (n m : nat) => + -- We prove this via induction on p for any fixed n and m. + nat_ind + (fun (p : nat) => eq nat (plus n (plus m p)) (plus (plus n m) p)) + + -- Base case: p = 0 + -- WTS n + (m + 0) = (n + m) + 0 + -- n + (m + 0) = n + m = (n + m) + 0 + (eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero) + -- n + (m + 0) = n + m + (eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m)) + + -- n + m = (n + m) + 0 + (eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m)))) + + -- Inductive step: IH = n + (m + p) = (n + m) + p + (fun (p : nat) (IH : eq nat (plus n (plus m p)) (plus (plus n m) p)) => + -- WTS n + (m + suc p) = (n + m) + suc p + -- n + (m + suc p) = n + suc (m + p) + -- = suc (n + (m + p)) + -- = suc ((n + m) + p) + -- = (n + m) + suc p + eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p)) + + -- n + (m + suc p) = n + suc (m + p) + (eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p)) + + -- n + suc (m + p) = (n + m) + suc p + (eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p)) + -- n + suc (m + p) = suc (n + (m + p)) + (plus_s_r n (plus m p)) + + -- suc (n + (m + p)) = (n + m) + suc p + (eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p)) + -- suc (n + (m + p)) = suc ((n + m) + p) + (eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc IH) + + -- suc ((n + m) + p) = (n + m) + suc p + (eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p)) + (plus_s_r (plus n m) p))))); + +-- Up next is commutativity, but we will need a couple lemmas first. + +-- First, we will show that 0 + n = n. +def plus_0_l : forall (n : nat), eq nat (plus zero n) n := + -- We prove this by induction on n. + nat_ind (fun (n : nat) => eq nat (plus zero n) n) + -- base case: WTS 0 + 0 = 0 + -- This is just plus_0_r 0 + (plus_0_r zero) + + -- inductive case + (fun (n : nat) (IH : eq nat (plus zero n) n) => + -- WTS 0 + (suc n) = suc n + -- 0 + (suc n) = suc (0 + n) = suc n + eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n) + -- 0 + (suc n) = suc (0 + n) + (plus_s_r zero n) + + -- suc (0 + n) = suc n + (eq_cong nat nat (plus zero n) n suc IH)); + +-- Next, we will show that (suc n) + m = suc (n + m). +def plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) := + -- We proceed by induction on m. + nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m))) + -- base case: (suc n) + 0 = suc (n + 0) + -- (suc n) + 0 = suc n = suc (n + 0) + (eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero)) + -- (suc n) + 0 = suc n + (plus_0_r (suc n)) + + -- suc n = suc (n + 0) + (eq_cong nat nat n (plus n zero) suc + -- n = n + 0 + (eq_sym nat (plus n zero) n (plus_0_r n)))) + + -- inductive case + -- IH = suc n + m = suc (n + m) + (fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) => + -- WTS suc n + suc m = suc (n + suc m) + -- suc n + suc m = suc (suc n + m) + -- = suc (suc (n + m)) + -- = suc (n + suc m) + (eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m))) + -- suc n + suc m = suc (suc n + m) + (plus_s_r (suc n) m) + + -- suc (suc n + m) = suc (n + suc m) + (eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m))) + -- suc (suc n + m) = suc (suc (n + m)) + (eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH) + + -- suc (suc (n + m)) = suc (n + suc m) + (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc + -- suc (n + m) = n + suc m + (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m)))))); + +-- Finally, we can prove commutativity. +def plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) := + -- As usual, we proceed by induction. + nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n)) + + -- Base case: WTS n + 0 = 0 + n + -- n + 0 = n = 0 + n + (eq_trans nat (plus n zero) n (plus zero n) + -- n + 0 = n + (plus_0_r n) + + -- n = 0 + n + (eq_sym nat (plus zero n) n (plus_0_l n))) + + -- Inductive step: + (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) => + -- WTS n + suc m = suc m + n + -- n + suc m = suc (n + m) + -- = suc (m + n) + -- = suc m + n + (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n) + -- n + suc m = suc (n + m) + (plus_s_r n m) + + -- suc (n + m) = suc m + n + (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n) + -- suc (n + m) = suc (m + n) + (eq_cong nat nat (plus n m) (plus m n) suc IH) + + -- suc (m + n) = suc m + n + (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n))))); diff --git a/lib/Errors.hs b/lib/Errors.hs index 3df35d3..5e2dda5 100644 --- a/lib/Errors.hs +++ b/lib/Errors.hs @@ -3,8 +3,7 @@ module Errors where import Expr data Error - = SquareUntyped - | UnboundVariable Text + = UnboundVariable Text | NotASort Expr Expr | ExpectedPiType Expr Expr | NotEquivalent Expr Expr Expr @@ -13,7 +12,6 @@ data Error deriving (Eq, Ord) instance ToText Error where - toText SquareUntyped = "□ does not have a type" toText (UnboundVariable x) = "Unbound variable: '" <> x <> "'" toText (NotASort x t) = "Expected '" <> pretty x <> "' to have type * or □, instead found '" <> pretty t <> "'" toText (ExpectedPiType x t) = "'" <> pretty x <> "' : '" <> pretty t <> "' is not a function" diff --git a/lib/Program.hs b/lib/Program.hs index 7439ae3..3e6f974 100644 --- a/lib/Program.hs +++ b/lib/Program.hs @@ -30,6 +30,7 @@ handleDef (Def name Nothing irBody) = do handleDef (Def name (Just irTy) irBody) = do env <- get ty' <- liftEither $ checkType env body + _ <- liftEither $ checkType env ty liftEither $ checkBeta env ty ty' body modify $ insertDef name ty' body where