SECTIONS WORKING!!!

examples/algebra.pg

@@ -131,14 +131,6 @@ def inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i)
 def inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) :=
     and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);
 
-section Groups
-    variable G : *;
-    variable op : binop G;
-    hypothesis Hgroup : group G op e i;
-
-    def left_inv_unique 
-end Groups
-
 def left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) :=
     -- b = b * e
     --   = b * (a * a^-1)

examples/logic.pg

@@ -115,101 +115,107 @@ def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :
 
 -- Some logic theorems
 
--- ~(A ∨ B) => ~A ∧ ~B
+section Theorems
-def de_morgan1 (A B : *) (h : not (or A B)) : and (not A) (not B) :=
-    and_intro (not A) (not B)
-        (fun (a : A) => h (or_intro_l A B a))
-        (fun (b : B) => h (or_intro_r A B b));
 
--- ~A ∧ ~B => ~(A ∨ B)
+    variable (A B C : *);
-def de_morgan2 (A B : *) (h : and (not A) (not B)) : not (or A B) :=
-    fun (contra : or A B) => 
-        or_elim A B false contra
-            (and_elim_l (not A) (not B) h)
-            (and_elim_r (not A) (not B) h);
 
--- ~A ∨ ~B => ~(A ∧ B)
+    -- ~(A ∨ B) => ~A ∧ ~B
-def de_morgan3 (A B : *) (h : or (not A) (not B)) : not (and A B) :=
+    def de_morgan1 (h : not (or A B)) : and (not A) (not B) :=
-    fun (contra : and A B) =>
+        and_intro (not A) (not B)
-        or_elim (not A) (not B) false h
+            (fun (a : A) => h (or_intro_l A B a))
-            (fun (na : not A) => na (and_elim_l A B contra))
+            (fun (b : B) => h (or_intro_r A B b));
-            (fun (nb : not B) => nb (and_elim_r A B contra));
 
--- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
+    -- ~A ∧ ~B => ~(A ∨ B)
+    def de_morgan2 (h : and (not A) (not B)) : not (or A B) :=
+        fun (contra : or A B) => 
+            or_elim A B false contra
+                (and_elim_l (not A) (not B) h)
+                (and_elim_r (not A) (not B) h);
 
--- A ∧ B => B ∧ A
+    -- ~A ∨ ~B => ~(A ∧ B)
-def and_comm (A B : *) (h : and A B) : and B A :=
+    def de_morgan3 (h : or (not A) (not B)) : not (and A B) :=
-    and_intro B A
+        fun (contra : and A B) =>
-        (and_elim_r A B h)
+            or_elim (not A) (not B) false h
-        (and_elim_l A B h);
+                (fun (na : not A) => na (and_elim_l A B contra))
+                (fun (nb : not B) => nb (and_elim_r A B contra));
 
--- A ∨ B => B ∨ A
+    -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
-def or_comm (A B : *) (h : or A B) : or B A :=
-    or_elim A B (or B A) h
-        (fun (a : A) => or_intro_r B A a)
-        (fun (b : B) => or_intro_l B A b);
 
--- A ∧ (B ∧ C) => (A ∧ B) ∧ C
+    -- A ∧ B => B ∧ A
-def and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
+    def and_comm (h : and A B) : and B A :=
-    let (a := (and_elim_l A (and B C) h))
+        and_intro B A
-        (bc := (and_elim_r A (and B C) h))
+            (and_elim_r A B h)
-        (b := (and_elim_l B C bc))
+            (and_elim_l A B h);
-        (c := (and_elim_r B C bc))
-    in
-        and_intro (and A B) C (and_intro A B a b) c
-    end;
 
--- (A ∧ B) ∧ C => A ∧ (B ∧ C)
+    -- A ∨ B => B ∨ A
-def and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
+    def or_comm (h : or A B) : or B A :=
-    let (ab := and_elim_l (and A B) C h)
+        or_elim A B (or B A) h
-        (a := and_elim_l A B ab)
+            (fun (a : A) => or_intro_r B A a)
-        (b := and_elim_r A B ab)
+            (fun (b : B) => or_intro_l B A b);
-        (c := and_elim_r (and A B) C h)
-    in
-        and_intro A (and B C) a (and_intro B C b c)
-    end;
 
--- A ∨ (B ∨ C) => (A ∨ B) ∨ C
+    -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
-def or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
+    def and_assoc_l (h : and A (and B C)) : and (and A B) C :=
-    or_elim A (or B C) (or (or A B) C) h
+        let (a := (and_elim_l A (and B C) h))
-        (fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
+            (bc := (and_elim_r A (and B C) h))
-        (fun (g : or B C) =>
+            (b := (and_elim_l B C bc))
-            or_elim B C (or (or A B) C) g
+            (c := (and_elim_r B C bc))
-                (fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
+        in
-                (fun (c : C) => or_intro_r (or A B) C c));
+            and_intro (and A B) C (and_intro A B a b) c
+        end;
 
--- (A ∨ B) ∨ C => A ∨ (B ∨ C)
+    -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
-def or_assoc_r (A B C : *) (h : or (or A B) C) : or A (or B C) :=
+    def and_assoc_r (h : and (and A B) C) : and A (and B C) :=
-    or_elim (or A B) C (or A (or B C)) h
+        let (ab := and_elim_l (and A B) C h)
-        (fun (g : or A B) => 
+            (a := and_elim_l A B ab)
-            or_elim A B (or A (or B C)) g
+            (b := and_elim_r A B ab)
-                (fun (a : A) => or_intro_l A (or B C) a)
+            (c := and_elim_r (and A B) C h)
-                (fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
+        in
-        (fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
+            and_intro A (and B C) a (and_intro B C b c)
+        end;
 
--- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
+    -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
-def and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (and A B) (and A C) :=
+    def or_assoc_l (h : or A (or B C)) : or (or A B) C :=
-    or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
+        or_elim A (or B C) (or (or A B) C) h
-        (fun (b : B) => or_intro_l (and A B) (and A C)
+            (fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
-            (and_intro A B (and_elim_l A (or B C) h) b))
+            (fun (g : or B C) =>
-        (fun (c : C) => or_intro_r (and A B) (and A C)
+                or_elim B C (or (or A B) C) g
-            (and_intro A C (and_elim_l A (or B C) h) c));
+                    (fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
+                    (fun (c : C) => or_intro_r (or A B) C c));
 
--- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
+    -- (A ∨ B) ∨ C => A ∨ (B ∨ C)
-def and_factor_l_or (A B C : *) (h : or (and A B) (and A C)) : and A (or B C) :=
+    def or_assoc_r (h : or (or A B) C) : or A (or B C) :=
-    or_elim (and A B) (and A C) (and A (or B C)) h
+        or_elim (or A B) C (or A (or B C)) h
-        (fun (ab : and A B) => and_intro A (or B C)
+            (fun (g : or A B) => 
-            (and_elim_l A B ab)
+                or_elim A B (or A (or B C)) g
-            (or_intro_l B C (and_elim_r A B ab)))
+                    (fun (a : A) => or_intro_l A (or B C) a)
-        (fun (ac : and A C) => and_intro A (or B C)
+                    (fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
-            (and_elim_l A C ac)
+            (fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
-            (or_intro_r B C (and_elim_r A C ac)));
 
--- Thanks Quinn!
+    -- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
--- A ∨ B => ~B => A
+    def and_distrib_l_or (h : and A (or B C)) : or (and A B) (and A C) :=
-def disj_syllog (A B : *) (nb : not B) (hor : or A B) : A :=
+        or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
-    or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
+            (fun (b : B) => or_intro_l (and A B) (and A C)
+                (and_intro A B (and_elim_l A (or B C) h) b))
+            (fun (c : C) => or_intro_r (and A B) (and A C)
+                (and_intro A C (and_elim_l A (or B C) h) c));
 
--- (A => B) => ~B => ~A
+    -- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
-def contrapositive (A B : *) (f : A -> B) (nb : not B) : not A :=
+    def and_factor_l_or (h : or (and A B) (and A C)) : and A (or B C) :=
-    fun (a : A) => nb (f a);
+        or_elim (and A B) (and A C) (and A (or B C)) h
+            (fun (ab : and A B) => and_intro A (or B C)
+                (and_elim_l A B ab)
+                (or_intro_l B C (and_elim_r A B ab)))
+            (fun (ac : and A C) => and_intro A (or B C)
+                (and_elim_l A C ac)
+                (or_intro_r B C (and_elim_r A C ac)));
+
+    -- Thanks Quinn!
+    -- A ∨ B => ~B => A
+    def disj_syllog (nb : not B) (hor : or A B) : A :=
+        or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
+
+    -- (A => B) => ~B => ~A
+    def contrapositive (f : A -> B) (nb : not B) : not A :=
+        fun (a : A) => nb (f a);
+
+end Theorems

examples/peano.pg

@@ -155,73 +155,72 @@ def suc_or_zero : forall (n : nat), szc n :=
 -- 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.
 
+section RecursiveDefs
+
+variable (A : *) (z : A) (fS : nat -> A -> A);
+
 -- {{{ Defining R
 -- Here is condition 1 formally expressed in perga.
-def cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+def cond1 (Q : nat -> A -> *) := Q zero z;
-    Q zero z;
 
 -- Likewise for condition 2.
-def cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
+def cond2 (Q : nat -> A -> *) :=
     forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
 
 -- From here we can define R.
-def rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def rec_rel (x : nat) (y : A) :=
-    forall (Q : nat -> A -> *), cond1 A z fS Q -> cond2 A z fS Q -> Q x y;
+    forall (Q : nat -> A -> *), cond1 Q -> cond2 Q -> Q x y;
 -- }}}
 
 -- {{{ R is total
 def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
 
-def rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
+def rec_rel_cond1 : cond1 rec_rel :=
-    fun (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) => h1;
+    fun (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
 
-def rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
+def rec_rel_cond2 : cond2 rec_rel :=
-    fun (n : nat) (y : A) (h : rec_rel A z fS n y)
+    fun (n : nat) (y : A) (h : rec_rel n y)
-        (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) =>
+        (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) =>
         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) :=
+def rec_rel_total : total nat A rec_rel :=
-    let (R           := rec_rel A z fS)
+    let (R           := rec_rel)
         (P (x : nat) := exists A (R x))
-        (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))
+    (exists_intro A (R 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 A z fS n y0 hy)))
+            exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 n y0 hy)))
     end;
+
 -- }}}
 
 -- {{{ Defining R2
-def alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
+def alt_cond1 (x : nat) (y : A) :=
     and (eq nat x zero) (eq A y z);
 
-def cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
+def cond_y2 (x : nat) (y : A)
     (x2 : nat) (y2 : A) :=
-        and (eq A y (fS x2 y2)) (rec_rel A z fS x2 y2);
+        and (eq A y (fS x2 y2)) (rec_rel x2 y2);
 
-def cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
+def cond_x2 (x : nat) (y : A) (x2 : nat) :=
-    and (pred x x2) (exists A (cond_y2 A z fS x y x2));
+    and (pred x x2) (exists A (cond_y2 x y x2));
 
-def alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def alt_cond2 (x : nat) (y : A) := exists nat (cond_x2 x y);
-    exists nat (cond_x2 A z fS x y);
 
-def rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
+def rec_rel_alt (x : nat) (y : A) := or (alt_cond1 x y) (alt_cond2 x y);
-    or (alt_cond1 A z x y) (alt_cond2 A z fS x y);
 -- }}}
 
 -- {{{ R = R2
 
 -- {{{ R2 ⊆ R
-def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
+def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y -> rec_rel x y :=
-    rec_rel_alt A z fS x y -> rec_rel A z fS x y :=
+    let (R   := rec_rel)
-    let (R   := rec_rel A z fS)
+        (R2  := rec_rel_alt)
-        (R2  := rec_rel_alt A z fS)
+        (ac1 := alt_cond1 x y)
-        (ac1 := alt_cond1 A z x y)
+        (ac2 := alt_cond2 x y)
-        (ac2 := alt_cond2 A z fS x y)
     in
         fun (h : R2 x y) =>
             or_elim ac1 ac2 (R x y) h
@@ -229,13 +228,13 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
                 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 A z fS))
+                    (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 A z fS x y)
+                let (h1 := cond_x2 x y)
-                    (h2 := cond_y2 A z fS x y)
+                    (h2 := cond_y2 x y)
                 in
                 exists_elim nat (R x y) h1 case2
                 (fun (x2 : nat) (hx2 : h1 x2) =>
@@ -246,7 +245,7 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
                     (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)
+                            (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
@@ -257,41 +256,36 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
 -- }}}
 
 -- {{{ R ⊆ R2
-def R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
+def R2_cond1 : cond1 rec_rel_alt :=
-    or_intro_l (alt_cond1 A z zero z) (alt_cond2 A z fS zero z)
+    or_intro_l (alt_cond1 zero z) (alt_cond2 zero z)
     (and_intro (eq nat zero zero) (eq A z z)
         (eq_refl nat zero)
         (eq_refl A z));
 
-def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
+def R2_cond2 : cond2 rec_rel_alt :=
-    let (R  := rec_rel A z fS)
+    let (R  := rec_rel)
-        (R2 := rec_rel_alt A z fS)
+        (R2 := rec_rel_alt)
     in
         fun (x2 : nat) (y2 : A) (h : R2 x2 y2) =>
         let (x   := suc x2)
             (y   := fS x2 y2)
-            (cx2 := cond_x2 A z fS x y)
+            (cx2 := cond_x2 x y)
-            (cy2 := cond_y2 A z fS x y x2)
+            (cy2 := cond_y2 x y x2)
         in
-            or_intro_r (alt_cond1 A z x y) (alt_cond2 A z fS x y)
+            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 A z fS x2 y2 h)))))
+                            (R2_sub_R x2 y2 h)))))
         end
     end;
 
-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 :=
+def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
-    let (R  := rec_rel A z fS)
+    fun (h : rec_rel x y) => h rec_rel_alt R2_cond1 R2_cond2;
-        (R2 := rec_rel_alt A z fS)
-    in
-        fun (h : R x y) =>
-            h R2 (R2_cond1 A z fS) (R2_cond2 A z fS)
-    end;
 -- }}}
 
 -- }}}
@@ -303,13 +297,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 (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
+def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
-    rec_rel_alt A z fS zero y -> eq A y z :=
+    let (R2  := rec_rel_alt)
-    let (R2  := rec_rel_alt A z fS)
+        (ac1 := alt_cond1 zero y)
-        (ac1 := alt_cond1 A z zero y)
+        (ac2 := alt_cond2 zero y)
-        (ac2 := alt_cond2 A z fS zero y)
+        (cx2 := cond_x2 zero y)
-        (cx2 := cond_x2 A z fS zero y)
+        (cy2 := cond_y2 zero y)
-        (cy2 := cond_y2 A z fS 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)
@@ -321,14 +314,13 @@ def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
                 (eq A y z)))
     end;
 
-def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
+def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc x2) y x2) :=
-    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)
-    let (R2   := rec_rel_alt A z fS)
         (x    := suc x2)
-        (ac1  := alt_cond1 A z x y)
+        (ac1  := alt_cond1 x y)
-        (ac2  := alt_cond2 A z fS x y)
+        (ac2  := alt_cond2 x y)
-        (cx2  := cond_x2 A z fS x y)
+        (cx2  := cond_x2 x y)
-        (cy2  := cond_y2 A z fS x y)
+        (cy2  := cond_y2 x y)
         (goal := exists A (cy2 x2))
     in
         fun (h : R2 x y) =>
@@ -347,31 +339,31 @@ def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
                 end))
     end;
 
-def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
+def R2_functional : fl nat A rec_rel_alt :=
-    let (R    := rec_rel A z fS)
+    let (R    := rec_rel)
-        (R2   := rec_rel_alt A z fS)
+        (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 A z fS y1 h1)
+            (R2_zero y1 h1)
-            (eq_sym A y2 z (R2_zero A z fS y2 h2)))
+            (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 A z fS x y1 x2)
+                (cy1  := cond_y2 x y1 x2)
-                (cy2  := cond_y2 A z fS x y2 x2)
+                (cy2  := cond_y2 x y2 x2)
                 (goal := eq A y1 y2)
             in
-                exists_elim A goal cy1 (R2_suc A z fS x2 y1 h1)
+                exists_elim A goal cy1 (R2_suc x2 y1 h1)
                 (fun (y12 : A) (h12 : cy1 y12) =>
-                    exists_elim A goal cy2 (R2_suc A z fS x2 y2 h2)
+                    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 A z fS x2 y12 R_x2_y12)
+                            (R2_x2_y12 := R_sub_R2 x2 y12 R_x2_y12)
-                            (R2_x2_y22 := R_sub_R2 A z fS x2 y22 R_x2_y22)
+                            (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
@@ -383,21 +375,16 @@ 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) :=
+def R_functional : fl nat A rec_rel :=
-    let (R   := rec_rel A z fS)
+    fun (n : nat) (y1 y2 : A) (h1 : rec_rel n y1) (h2 : rec_rel n y2) =>
-        (sub := R_sub_R2 A z fS)
+        R2_functional n y1 y2 (R_sub_R2 n y1 h1) (R_sub_R2 n y2 h2);
-    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 :=
+def rec_def (x : nat) : A :=
-    exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x)
+    exists_elim A A (rec_rel x) (rec_rel_total x) (fun (y : A) (_ : rec_rel x y) => y);
-        (fun (y : A) (_ : rec_rel A z fS x y) => y);
 
 -- }}}
 
@@ -415,39 +402,30 @@ 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) :=
+def rec_def_sat (x : nat) : rec_rel x (rec_def x) :=
-    definite_description A (rec_rel A z fS x) (rec_rel_total A z fS x);
+    definite_description A (rec_rel x) (rec_rel_total x);
 
-def eq1 (A : *) (z : A) (f : nat -> A) := eq A (f zero) z;
+def eq1 (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));
+def eq2 (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) :=
+def rec_def_sat_zero : eq1 rec_def := R_functional zero (rec_def zero) z (rec_def_sat zero) rec_rel_cond1;
-    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) :=
+def rec_def_sat_suc : eq2 rec_def :=
     fun (n : nat) =>
-        let (R     := rec_rel A z fS)
+        let (y     := rec_def n)
-            (f     := rec_def A z fS)
+            (RSnfy := rec_rel_cond2 n y (rec_def_sat n))
-            (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 
+            R_functional (suc n) (rec_def (suc n)) (fS n y) (rec_def_sat (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)
+def rec_def_unique (fS : nat -> A -> A) (f g : nat -> A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
-    (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
@@ -470,6 +448,8 @@ def rec_def_unique (A : *) (z : A) (fS : nat -> A -> A) (f g : nat -> A)
 
 -- }}}
 
+end RecursiveDefs
+
 -- }}}
 
 -- Now we can safely define addition.

lib/Elaborator.hs

@@ -2,29 +2,25 @@
 
 module Elaborator where
 
-import Control.Monad.Except
 import Data.List (elemIndex, lookup)
-import Data.List.NonEmpty ((<|))
+import qualified Data.Set as S
-import Errors (Error (..), Result)
 import Expr (Expr)
 import qualified Expr as E
-import IR (IRDef (..), IRExpr, IRProgram)
+import IR (IRDef (..), IRExpr, IRProgram, IRSectionDef (..))
 import qualified IR as I
 import Relude.Extra.Lens
 
 type Binders = [Text]
 
 data SectionContext = SectionContext
-    { sectionDefs :: [(Text, [Text])] -- name and list of variables it depends on
+    { sectionDefs :: [(Text, [(Text, IRExpr)])] -- name and list of variables and their types it depends on
     , sectionVars :: [(Text, IRExpr)] -- variables and their types
     }
 
 type ElabMonad = State SectionContext
 
 lookupDefInCtxt :: Text -> SectionContext -> Maybe [(Text, IRExpr)]
-lookupDefInCtxt def (SectionContext defs vars) = mapMaybe helper <$> lookup def defs
+lookupDefInCtxt def (SectionContext defs _) = lookup def defs
-  where
-    helper dep = (dep,) <$> dep `lookup` vars
 
 -- looks up a definition in the context and gives a list of the variables and
 -- their types that it depends on
@@ -38,7 +34,7 @@ lookupVarInCtxt var = lookup var . sectionVars
 lookupVar :: Text -> ElabMonad (Maybe IRExpr)
 lookupVar var = lookupVarInCtxt var <$> get
 
-sectionDefsL :: Lens' SectionContext [(Text, [Text])]
+sectionDefsL :: Lens' SectionContext [(Text, [(Text, IRExpr)])]
 sectionDefsL = lens sectionDefs setter
   where
     setter ctxt newDefs = ctxt{sectionDefs = newDefs}
@@ -51,56 +47,83 @@ sectionVarsL = lens sectionVars setter
 saveState :: ElabMonad a -> ElabMonad a
 saveState action = get >>= (action <*) . put
 
-elabSection :: Text -> [IRDef] -> ElabMonad [IRDef]
+debugIRExpr :: IRExpr -> String
+debugIRExpr = E.prettyS . elaborate
+
+debugIRDef :: IRDef -> String
+debugIRDef (Def name (Just ty) body) = "def " ++ toString name ++ " : " ++ debugIRExpr ty ++ " := " ++ debugIRExpr body ++ ";"
+debugIRDef (Def name Nothing body) = "def " ++ toString name ++ " := " ++ debugIRExpr body ++ ";"
+debugIRDef (Axiom name typ) = "axiom " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";"
+
+debugIRSectionDef :: IRSectionDef -> String
+debugIRSectionDef (Variable name typ) = "variable " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";"
+debugIRSectionDef (Section name _) = "section " ++ toString name ++ ";"
+debugIRSectionDef (IRDef def) = debugIRDef def
+
+elabSection :: Text -> [IRSectionDef] -> ElabMonad [IRDef]
 elabSection _name contents = saveState $ concat <$> forM contents elabDef
 
-elabProgram :: IRProgram -> IRProgram
+elabProgram :: IRProgram -> [IRDef]
 elabProgram prog = evalState (elabSection "" prog) (SectionContext [] [])
 
 pushVariable :: Text -> IRExpr -> SectionContext -> SectionContext
 pushVariable name ty (SectionContext defs vars) = SectionContext defs ((name, ty) : vars)
 
-pushDefinition :: Text -> [Text] -> SectionContext -> SectionContext
+pushDefinition :: Text -> [(Text, IRExpr)] -> SectionContext -> SectionContext
 pushDefinition name defVars (SectionContext defs vars) = SectionContext ((name, defVars) : defs) vars
 
 removeName :: Text -> ElabMonad ()
-removeName name = do
+removeName name = do 
     modify $ over sectionDefsL (filter ((/= name) . fst))
     modify $ over sectionVarsL (filter ((/= name) . fst))
 
+extendVars :: Set (Text, IRExpr) -> ElabMonad (Set (Text, IRExpr))
+extendVars vars = do
+    vars' <- foldr S.union S.empty <$> traverse (usedVars . snd) (S.toList vars)
+    if vars' `S.isSubsetOf` vars
+        then pure vars
+        else extendVars (vars `S.union` vars')
+
+organize :: Set (Text, IRExpr) -> ElabMonad [(Text, IRExpr)]
+organize found = do
+    vars <- gets sectionVars
+    pure $ reverse [var | var <- vars, var `S.member` found]
+
 -- find all the section variables used in an expression
-usedVars :: IRExpr -> ElabMonad [(Text, IRExpr)]
+usedVars :: IRExpr -> ElabMonad (Set (Text, IRExpr))
-usedVars (I.Var name) = maybe [] (pure . (name,)) <$> lookupVar name
+usedVars (I.Var name) = do
-usedVars I.Star = pure []
+    varDeps <- maybe S.empty (S.singleton . (name,)) <$> lookupVar name
-usedVars (I.Level _) = pure []
+    defDeps <- maybe S.empty S.fromList <$> lookupDef name
-usedVars (I.App m n) = (++) <$> usedVars m <*> usedVars n
+    pure $ varDeps `S.union` defDeps
+usedVars I.Star = pure S.empty
+usedVars (I.Level _) = pure S.empty
+usedVars (I.App m n) = S.union <$> usedVars m <*> usedVars n
 usedVars (I.Abs name ty ascr body) = saveState $ do
     ty' <- usedVars ty
     ascr' <- traverse usedVars ascr
     removeName name
-    ((ty' ++ (ascr' ?: [])) ++) <$> usedVars body
+    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
 usedVars (I.Pi name ty ascr body) = saveState $ do
     ty' <- usedVars ty
     ascr' <- traverse usedVars ascr
     removeName name
-    ((ty' ++ (ascr' ?: [])) ++) <$> usedVars body
+    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
 usedVars (I.Let name ascr value body) = saveState $ do
     ty' <- usedVars value
     ascr' <- traverse usedVars ascr
     removeName name
-    ((ty' ++ (ascr' ?: [])) ++) <$> usedVars body
+    S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
 
 -- traverse the body of a definition, adding the necessary section arguments to
 -- any definitions made within the section
 traverseBody :: IRExpr -> ElabMonad IRExpr
 traverseBody (I.Var name) = do
-    deps <- lookupDef name
+    mdeps <- lookupDef name
-    case deps of
+    case mdeps of
         Nothing -> pure $ I.Var name
-        Just [] -> pure $ I.Var name
+        Just deps -> pure $ foldl' (\acc newVar -> I.App acc (I.Var $ fst newVar)) (I.Var name) deps
-        Just ((top, _) : rest) -> pure $ foldr (I.App . I.Var . fst) (I.Var top) rest
 traverseBody I.Star = pure I.Star
-traverseBody e@(I.Level _) = pure e
+traverseBody (I.Level k) = pure $ I.Level k
 traverseBody (I.App m n) = I.App <$> traverseBody m <*> traverseBody n
 traverseBody (I.Abs name ty ascr body) = saveState $ do
     ty' <- traverseBody ty
@@ -113,8 +136,8 @@ traverseBody (I.Pi name ty ascr body) = saveState $ do
     removeName name
     I.Pi name ty' ascr' <$> traverseBody body
 traverseBody (I.Let name ascr value body) = saveState $ do
-    value' <- traverseBody value
     ascr' <- traverse traverseBody ascr
+    value' <- traverseBody value
     removeName name
     I.Let name ascr' value' <$> traverseBody body
 
@@ -130,53 +153,55 @@ generalizeType = foldr mkPi
 generalizeVal :: IRExpr -> [(Text, IRExpr)] -> IRExpr
 generalizeVal = foldr mkAbs
 
-elabDef :: IRDef -> ElabMonad [IRDef]
+elabDef :: IRSectionDef -> ElabMonad [IRDef]
-elabDef (Def name ty body) = do
+elabDef (IRDef (Def name ty body)) = do
-    tyVars <- fromMaybe [] <$> traverse usedVars ty
+    tyVars <- fromMaybe S.empty <$> traverse usedVars ty
     bodyVars <- usedVars body
-    let totalVars = tyVars ++ bodyVars
+    totalVars <- extendVars (tyVars `S.union` bodyVars) >>= organize
-    modify $ pushDefinition name (map fst totalVars)
+    newBody <- traverseBody body
-    pure [Def name (flip generalizeType totalVars <$> ty) (generalizeVal body totalVars)]
+    newType <- traverse traverseBody ty
-elabDef (Axiom name ty) = do
+    modify $ pushDefinition name totalVars
-    vars <- usedVars ty
+    pure [Def name (flip generalizeType totalVars <$> newType) (generalizeVal newBody totalVars)]
-    modify $ pushDefinition name (map fst vars)
+elabDef (IRDef (Axiom name ty)) = do
+    vars <- usedVars ty >>= extendVars >>= organize
+    modify $ pushDefinition name vars
     pure [Axiom name (generalizeType ty vars)]
 elabDef (Section name contents) = saveState $ elabSection name contents
 elabDef (Variable name ty) = [] <$ modify' (pushVariable name ty)
 
--- saveBinders :: State Binders a -> State Binders a
+saveBinders :: State Binders a -> State Binders a
--- saveBinders action = do
+saveBinders action = do
---     binders <- get
+    binders <- get
---     res <- action
+    res <- action
---     put binders
+    put binders
---     pure res
+    pure res
---
+
--- elaborate :: IRExpr -> Expr
+elaborate :: IRExpr -> Expr
--- elaborate ir = evalState (elaborate' ir) []
+elaborate ir = evalState (elaborate' ir) []
---   where
+  where
---     elaborate' :: IRExpr -> State Binders Expr
+    elaborate' :: IRExpr -> State Binders Expr
---     elaborate' (I.Var n) = do
+    elaborate' (I.Var n) = do
---         binders <- get
+        binders <- get
---         pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+        pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
---     elaborate' I.Star = pure E.Star
+    elaborate' I.Star = pure E.Star
---     elaborate' (I.Level level) = pure $ E.Level level
+    elaborate' (I.Level level) = pure $ E.Level level
---     elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
+    elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
---     elaborate' (I.Abs x t a b) = saveBinders $ do
+    elaborate' (I.Abs x t a b) = saveBinders $ do
---         t' <- elaborate' t
+        t' <- elaborate' t
---         a' <- traverse elaborate' a
+        a' <- traverse elaborate' a
---         modify (x :)
+        modify (x :)
---         E.Abs x t' a' <$> elaborate' b
+        E.Abs x t' a' <$> elaborate' b
---     elaborate' (I.Pi x t a b) = saveBinders $ do
+    elaborate' (I.Pi x t a b) = saveBinders $ do
---         t' <- elaborate' t
+        t' <- elaborate' t
---         a' <- traverse elaborate' a
+        a' <- traverse elaborate' a
---         modify (x :)
+        modify (x :)
---         E.Pi x t' a' <$> elaborate' b
+        E.Pi x t' a' <$> elaborate' b
---     elaborate' (I.Let name Nothing val body) = saveBinders $ do
+    elaborate' (I.Let name Nothing val body) = saveBinders $ do
---         val' <- elaborate' val
+        val' <- elaborate' val
---         modify (name :)
+        modify (name :)
---         E.Let name Nothing val' <$> elaborate' body
+        E.Let name Nothing val' <$> elaborate' body
---     elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
+    elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
---         val' <- elaborate' val
+        val' <- elaborate' val
---         ty' <- elaborate' ty
+        ty' <- elaborate' ty
---         modify (name :)
+        modify (name :)
---         E.Let name (Just ty') val' <$> elaborate' body
+        E.Let name (Just ty') val' <$> elaborate' body

lib/Expr.hs

@@ -143,12 +143,12 @@ helper k e@(Pi{}) = if k > 2 then parenthesize res else res
   where
     (params, body) = collectPis e
     grouped = showParamGroup <$> groupParams params
-    res = "∏ " <> unwords grouped <> " . " <> pretty body
+    res = "∏ " <> unwords grouped <> " , " <> pretty body
 helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
   where
     (params, body) = collectLambdas e
     grouped = showParamGroup <$> groupParams params
-    res = "λ " <> unwords grouped <> " . " <> pretty body
+    res = "λ " <> unwords grouped <> " => " <> pretty body
 helper _ e@(Let{}) = res
   where
     (binds, body) = collectLets e

lib/IR.hs

@@ -30,6 +30,18 @@ data IRExpr
         }
     deriving (Show, Eq, Ord)
 
+data IRSectionDef
+    = Section
+        { sectionName :: Text
+        , sectionContents :: [IRSectionDef]
+        }
+    | Variable
+        { variableName :: Text
+        , variableType :: IRExpr
+        }
+    | IRDef IRDef
+    deriving (Show, Eq, Ord)
+
 data IRDef
     = Def
         { defName :: Text
@@ -40,14 +52,6 @@ data IRDef
         { axiomName :: Text
         , axiomAscription :: IRExpr
         }
-    | Section
-        { sectionName :: Text
-        , sectionContents :: [IRDef]
-        }
-    | Variable
-        { variableName :: Text
-        , variableType :: IRExpr
-        }
     deriving (Show, Eq, Ord)
 
-type IRProgram = [IRDef]
+type IRProgram = [IRSectionDef]

lib/Parser.hs

@@ -176,14 +176,12 @@ pAxiom = lexeme $ label "axiom" $ do
     eat ";"
     pure $ Axiom ident ascription
 
-pVariable :: Parser IRDef
+pVariable :: Parser [IRSectionDef]
 pVariable = lexeme $ label "variable declaration" $ do
     eat "variable" <|> eat "hypothesis"
-    ident <- pIdentifier
+    vars <- pManyParams
-    params <- pManyParams
-    ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
     eat ";"
-    pure $ Variable ident ascription
+    pure $ uncurry Variable <$> vars
 
 pDef :: Parser IRDef
 pDef = lexeme $ label "definition" $ do
@@ -196,20 +194,20 @@ pDef = lexeme $ label "definition" $ do
     eat ";"
     pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
 
-pSection :: Parser IRDef
+pSection :: Parser IRSectionDef
 pSection = lexeme $ label "section" $ do
     eat "section"
     secLabel <- pIdentifier
-    body <- many pIRDef
+    body <- concat <$> many pIRDef
     eat "end"
     void $ lexeme $ chunk secLabel
     pure $ Section secLabel body
 
-pIRDef :: Parser IRDef
+pIRDef :: Parser [IRSectionDef]
-pIRDef = pAxiom <|> pDef <|> pVariable <|> pSection
+pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection)
 
 pIRProgram :: Parser IRProgram
-pIRProgram = skipSpace >> some pIRDef
+pIRProgram = skipSpace >> concat <$> some pIRDef
 
 parserWrapper :: Parser a -> String -> Text -> Either String a
 parserWrapper p filename input = first errorBundlePretty $ runParser p filename input
@@ -218,7 +216,7 @@ parseProgram :: String -> Text -> Either String IRProgram
 parseProgram = parserWrapper pIRProgram
 
 parseDef :: String -> Text -> Either String IRDef
-parseDef = parserWrapper pIRDef
+parseDef = parserWrapper (pAxiom <|> pDef)
 
 parseExpr :: String -> Text -> Either String IRExpr
 parseExpr = parserWrapper pIRExpr

lib/Program.hs

@@ -36,14 +36,12 @@ handleDef (Def name (Just irTy) irBody) = do
   where
     body = elaborate irBody
     ty = elaborate irTy
-handleDef (Variable name ty) = undefined
-handleDef (Section name contents) = undefined
 
 evalDef :: Env -> IRDef -> Result Env
 evalDef = flip (execStateT . handleDef)
 
 handleProgram :: Env -> IRProgram -> Result Env
-handleProgram env = flip execStateT env . mapM_ handleDef
+handleProgram env = flip execStateT env . mapM_ handleDef . elabProgram
 
 handleAndParseProgram :: Env -> String -> Text -> Either String Env
 handleAndParseProgram env filename input = (first toString . handleProgram env) =<< parseProgram filename input