Added type ascriptions, which fixed many bugs.

plfa · Nov 19, 2023 · a4684b2 · a4684b2
1 parent 366c943
commit a4684b2
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 18 deletions.
diff --git a/src/Relations.lean b/src/Relations.lean
@@ -35,7 +35,7 @@ theorem zero_le_n : ∀ {n : Nat}, 0 ≤ n
           exact ih
 
 theorem succ_le_succ : ∀ {m n : Nat}, m ≤ n → succ m ≤ succ n
-  := by 
+  := by
       intros m n m_le_n
       induction m_le_n with
       | refl =>
@@ -44,7 +44,7 @@ theorem succ_le_succ : ∀ {m n : Nat}, m ≤ n → succ m ≤ succ n
          apply le.step
          exact ih
 
-theorem invert : ∀ {m n : Nat}, succ m ≤ succ n → m ≤ n 
+theorem invert : ∀ {m n : Nat}, succ m ≤ succ n → m ≤ n
   := by
       intros m n sm_le_sn
       cases sm_le_sn with
@@ -72,9 +72,9 @@ instance : Trans (.≤. : Nat → Nat → Prop)
 
 example : 2 ≤ 7 :=
   calc
-    2 ≤ 4 := le.step (le.step le.refl)
-    _ ≤ 5 := le.step le.refl 
-    _ ≤ 7 := le.step (le.step le.refl)
+    (2 : Nat) ≤ 4 := le.step (le.step le.refl)
+    _         ≤ 5 := le.step le.refl
+    _         ≤ 7 := le.step (le.step le.refl)
 
 -- Strict inequality
 
@@ -87,14 +87,14 @@ theorem lt_succ : ∀ {n : Nat}, n < succ n
   := by
       intros
       exact le.refl
-  
+
 theorem le_of_lt : ∀ {m n : Nat}, m < n → m ≤ n
   := by
       intros
       apply invert
       apply le.step
       assumption
-      
+
 theorem trans_lt_of_lt_of_le : ∀ {m n p : Nat}, m < n → n ≤ p → m < p
   := by
       intros
@@ -109,7 +109,7 @@ theorem trans_lt_of_le_of_lt : ∀ {m n p : Nat}, m ≤ n → n < p → m < p
       apply succ_le_succ
       assumption
       assumption
-      
+
 theorem trans_lt : ∀ {m n p : Nat}, m < n → n < p → m < p
   := by
       intros
@@ -135,9 +135,9 @@ instance : Trans (.<. : Nat → Nat → Prop)
 
 example : 2 < 7 :=
   calc
-    2 ≤ 4 := le.step (le.step le.refl)
-    _ < 5 := lt_succ  
-    _ ≤ 7 := le.step (le.step le.refl)
+    (2 : Nat) ≤ 4 := le.step (le.step le.refl)
+    _         < 5 := lt_succ
+    _         ≤ 7 := le.step (le.step le.refl)
 
 -- Exercise.
 -- Here is a different definition of ≤.
@@ -163,11 +163,11 @@ theorem antisymm : ∀ {m n : Nat}, le2 m n → le2 n m → m = n
         cases n_le_m with
         | z_le_n =>
             rfl
-      | s_le_s _ ih => 
+      | s_le_s _ ih =>
         cases n_le_m with
         | s_le_s n_le_m =>
             rw [ih n_le_m]
-          
+
 
 theorem antisymm' : ∀ {m n : Nat}, le2 m n → le2 n m → m = n
 | _ , _ , z_le_n , z_le_n => rfl
@@ -193,5 +193,3 @@ inductive lt3 : Nat → Nat → Prop where
 -- Exercise. Prove the following.
 --   m ≤ n iff ∃ p, m + p = n
 --   m < n iff ∃ p, p ≠ 0 ∧ m + p = n
-
-
diff --git a/src/Typesig.lean b/src/Typesig.lean
@@ -95,7 +95,7 @@ instance [OfNat (Γ ∋ B) n] : OfNat (Γ ▷ A ∋ B) (Nat.succ n) where
 example : 2 = (S S Z : ∅ ▷ ℕ ⇒ ℕ ▷ ℕ ▷ ℕ ∋ ℕ ⇒ ℕ) := rfl
 
 def plus : Γ ⊢ ℕ ⇒ ℕ ⇒ ℕ :=
-  μ ƛ ƛ (switch (# 0) (# 1) ((# 3 ⬝ # S S Z ⬝ # Z) +1))
+  μ ƛ ƛ (switch (# Z) (# S Z) ((# S S S Z ⬝ # S S Z ⬝ # Z) +1))
 def two_plus_two : ∅ ⊢ ℕ :=
   plus ⬝ 2 ⬝ 2
 
@@ -106,7 +106,7 @@ def suc_c : Γ ⊢ ℕ ⇒ ℕ :=
   ƛ (# Z +1)
 def Ch (A : Tp) : Tp := (A ⇒ A) ⇒ A ⇒ A
 def two_c : Γ ⊢ Ch A :=
-  ƛ ƛ (# S Z ⬝ (# 1 ⬝ # 0))
+  ƛ ƛ (# S Z ⬝ (# S Z ⬝ # Z))
 -- twoᶜ =  ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z")
 def plus_c : Γ ⊢ Ch A ⇒ Ch A ⇒ Ch A :=
   ƛ ƛ ƛ ƛ (# S S S Z ⬝ # S Z ⬝ (# S S Z ⬝ # S Z ⬝ # Z))
@@ -277,7 +277,7 @@ example : (suc_c ⬝ 1 : ∅ ⊢ ℕ) ~> 2
 
 example : two ~>> 2 :=
   calc
-    two_c ⬝ suc_c ⬝ 0
+    (two_c ⬝ suc_c ⬝ 0 : ∅ ⊢ ℕ)
       ~> (ƛ (suc_c ⬝ (suc_c ⬝ # Z))) ⬝ 0  := xi_app_1 (beta Value.lambda)
     _ ~> (suc_c ⬝ (suc_c ⬝ 0))            := beta Value.zero
     _ ~> suc_c ⬝ 1                       := xi_app_2 Value.lambda (beta Value.zero)