more peano, fixed bug in checking ascriptions of definitions
This commit is contained in:
parent
84e44b0e33
commit
c0e0c37689
3 changed files with 281 additions and 236 deletions
|
|
@ -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)))));
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue