more exercise on grade

basics/main.lean

@@ -1,6 +1,6 @@
 --- Data and Functions
 
-inductive Day : Type :=
+inductive Day : Type where
   | Monday
   | Tuesday
   | Wednesday
@@ -138,11 +138,11 @@ def foo : Bool := true
 --- Tuples
 namespace TuplePlayground
 
-inductive Bit : Type :=
+inductive Bit : Type where
   | B₁
   | B₀
 
-inductive Nybble :=
+inductive Nybble where
   | bits (b₀ b₁ b₂ b₃ : Bit)
 
 #print Nybble
@@ -387,3 +387,124 @@ 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