basics/main.lean

@@ -1,6 +1,6 @@
 --- Data and Functions
 
-inductive Day : Type where
+inductive Day : Type :=
   | Monday
   | Tuesday
   | Wednesday
@@ -138,11 +138,11 @@ def foo : Bool := true
 --- Tuples
 namespace TuplePlayground
 
-inductive Bit : Type where
+inductive Bit : Type :=
   | B₁
   | B₀
 
-inductive Nybble where
+inductive Nybble :=
   | bits (b₀ b₁ b₂ b₃ : Bit)
 
 #print Nybble
@@ -387,124 +387,3 @@ theorem andb_eq_orb :
   case false => exact h
 
 end Exercise
-
-namespace LateDays
-
-inductive Letters where
-  | A | B | C | D | F
-deriving Repr
-
-inductive Modifiers where
-  | Plus | Natural | Minus
-deriving Repr
-
-structure Grade where
-  l : Letters
-  m : Modifiers
-deriving Repr
-
-#print Ordering
-#eval Grade.mk .A .Plus
-
-def letter_comparison (l₁ l₂ : Letters) : Ordering :=
-  open Letters Ordering in
-  match l₁, l₂ with
-  | A, A => eq
-  | A, _ => gt
-  | B, A => lt
-  | B, B => eq
-  | B, _ => gt
-  | C, A | C, B => lt
-  | C, C => eq
-  | C, _ => gt
-  | D, A | D, B | D, C => lt
-  | D, D => eq
-  | D, _ => gt
-  | F, A | F, B | F, C | F, D => lt
-  | F, F => eq
-
-#eval letter_comparison Letters.B Letters.A
-#eval letter_comparison .D .D
-#eval letter_comparison .B .F
-
-theorem letter_comparison_eq :
-  ∀ l: Letters, letter_comparison l l = .eq
-:= by
-  intros l
-  cases l
-  . rfl
-  . rfl
-  . rfl
-  . rfl
-  . rfl
-
-def modifier_comparison (m₁ m₂ : Modifiers) : Ordering :=
-  match m₁, m₂ with
-  | .Plus, .Plus => .eq
-  | .Plus, _ => .gt
-  | .Natural, .Plus => .lt
-  | .Natural, .Natural => .eq
-  | .Natural, _ => .gt
-  | .Minus, .Plus | .Minus, .Natural => .lt
-  | .Minus, .Minus => .eq
-
-#eval modifier_comparison .Natural .Minus
-
-def grade_comparison (g₁ g₂ : Grade) : Ordering :=
-  match g₁, g₂ with
-  | ⟨.A, m₁⟩, ⟨.A, m₂⟩ => modifier_comparison m₁ m₂
-  | ⟨.A, _⟩, _ => .gt
-  | ⟨.B, _⟩, ⟨.A, _⟩ => .lt
-  | ⟨.B, m₁⟩, ⟨.B, m₂⟩ => modifier_comparison m₁ m₂
-  | ⟨.B, _⟩, _ => .gt
-  | ⟨.C, _⟩, ⟨.A, _⟩ | ⟨.C, _⟩, ⟨.B, _⟩ => .lt
-  | ⟨.C, m₁⟩, ⟨.C, m₂⟩ => modifier_comparison m₁ m₂
-  | ⟨.C, _⟩, _ => .gt
-  | ⟨.D, _⟩, ⟨.A, _⟩ | ⟨.D, _⟩, ⟨.B, _⟩ | ⟨.D, _⟩, ⟨.C, _⟩ => .lt
-  | ⟨.D, m₁⟩, ⟨.D, m₂⟩ => modifier_comparison m₁ m₂
-  | ⟨.D, _⟩, _ => .gt
-  | ⟨.F, _⟩, ⟨.A, _⟩ | ⟨.F, _⟩, ⟨.B, _⟩ | ⟨.F, _⟩, ⟨.C, _⟩ | ⟨.F, _⟩, ⟨.D, _⟩ => .lt
-  | ⟨.F, m₁⟩, ⟨.F, m₂⟩ => modifier_comparison m₁ m₂
-
-example : grade_comparison ⟨.A, .Minus⟩ ⟨.B, .Plus⟩ = .gt := by
-  rfl
-
-example : grade_comparison ⟨.A, .Minus⟩ ⟨.A, .Plus⟩ = .lt := by
-  rfl
-
-example : grade_comparison (Grade.mk .F .Plus) (Grade.mk Letters.F Modifiers.Plus) = Ordering.eq := by
-  rfl
-
-example : grade_comparison { l := .B, m := .Minus } { l := .C, m := .Plus } = .gt := by
-  rfl
-
-def lower_letter (l : Letters) : Letters :=
-  open Letters in
-  match l with
-  | A => B
-  | B => C
-  | C => D
-  | D => F
-  | F => F
-
-#eval lower_letter .F
-
-theorem lower_letter_F_is_F :
-    lower_letter .F = .F
-:= by rfl
-
-theorem lower_letter_lowers:
-    ∀ (l : Letters),
-      letter_comparison .F l = .lt →
-      letter_comparison (lower_letter l) l = .lt
-  := by
-    intro l hl
-    cases l
-    . exact hl
-    . exact hl
-    . exact hl
-    . exact hl
-    . exact hl
-
-
-end LateDays