--- Data and Functions

inductive Day : Type where
  | Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday
deriving Repr

def next_weekday (d : Day) : Day :=
  match d with
  | .Monday => .Tuesday
  | .Tuesday => .Wednesday
  | .Wednesday => .Thursday
  | .Thursday => .Friday
  | .Friday | .Saturday | .Sunday => .Monday

#eval next_weekday Day.Friday
#eval next_weekday (next_weekday .Saturday)

theorem test_next_weekday : next_weekday (next_weekday .Saturday) = .Tuesday := by
  rfl

--- Booleans
#print bool
#eval not true
#print not
#print and
#print or

def andb (b₁ : Bool) (b₂ : Bool) : Bool :=
  match b₁ with
  | true => b₂
  | false => false

def orb (b₁ : Bool) (b₂ : Bool) : Bool :=
  match b₁ with
  | true => true
  | false => b₂

example : or true false = true := by rfl
example : or false false = false := by rfl
example : or false true = true := by rfl
example : or true true = true := by rfl

#eval true ∨ false
example : true ∨ false = true := by
  simp
example : false ∨ false ∨ true = true := by
  simp

def negb' (b : Bool) : Bool :=
  if b then false
  else true

#eval negb' true
example : negb' true = ¬ true := by
  simp
  rfl

--- Exercise 1
namespace Exercise1

def nandb (b₁ : Bool) (b₂ : Bool) : Bool :=
  match (b₁, b₂) with
  | (true, true) => false
  | _            => true

example : (nandb true false) = true := by
  rfl

example : (nandb false false) = true := by
  rfl

example : (nandb false true) = true := by
  rfl
example : (nandb true true) = false := by
  rfl

def andb3
  | true, true, true => true
  | _, _, _          => false

example : andb3 true true true = true := by rfl
example : andb3 false true true = false := by rfl
example : andb3 true false true = false := by rfl
example : andb3 true true false = false := by rfl

end Exercise1

--- Types

#check true
#check Bool.not
#check true.not
#check not

--- New Types from Old

inductive Rgb : Type :=
  | red
  | green
  | blue

inductive Color : Type :=
  | black
  | white
  | primary (p : Rgb)

#check Color.primary

def monochrome (c : Color) : Bool :=
  match c with
  | .black => true
  | .white => true
  | .primary _p => false

def isred (c : Color) : Bool :=
  match c with
  | .primary .red => true
  | _ => false

--- Modules
namespace Playground

def foo : Rgb := .blue

end Playground

def foo : Bool := true

#check Playground.foo
#check foo

--- Tuples
namespace TuplePlayground

inductive Bit : Type where
  | B₁
  | B₀

inductive Nybble where
  | bits (b₀ b₁ b₂ b₃ : Bit)

#print Nybble

#check Nybble.bits .B₁ .B₀ .B₁ .B₀

def all_zero (nb : Nybble) : Bool :=
  match nb with
  | .bits .B₀ .B₀ .B₀ .B₀ => true
  | .bits _ _ _ _ => false

#eval all_zero (.bits .B₁ .B₁ .B₁ .B₁)
#eval all_zero (.bits .B₀ .B₀ .B₀ .B₀)

end TuplePlayground

--- Numbers
namespace NatPlayground

#eval Nat.zero
#eval Nat.zero.succ
#eval Nat.zero.succ.succ
example : Nat.zero.succ.succ = 2 := by rfl

end NatPlayground

open Nat in
#check succ (succ (succ 0))

def minustwo (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | .succ .zero => 0
  | .succ (.succ n') => n'

#eval minustwo 4

def even (n : Nat) : Bool :=
  match n with
  | .zero => true
  | .succ .zero => false
  | .succ (.succ n') => even n'

example : even 4 = true := by
  rfl
example : even 51 = false := by
  rfl

namespace NatPlayground2

def plus (n : Nat) (m : Nat) : Nat :=
  match n with
  | .zero => m
  | .succ n' => .succ (plus n' m)

#eval plus 3 4

def mult (n m : Nat) : Nat :=
  match n with
  | .zero => .zero
  | .succ n' => plus m (mult n' m)

end NatPlayground2

namespace Exercise1

def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | .succ n' => (n' + 1) * factorial n'

#eval factorial 3

example : factorial 3 = 6 := by
  rfl

example : factorial 5 = .mul 10 12 := by
  rfl

end Exercise1

#check LT.lt 1 2
#check LT Nat
#check (LT Nat)
#check Nat.lt 1 2

namespace Exercise1

def ltb (n m : Nat) : Bool :=
  match n, m with
  | 0, _ => true
  | _, 0 => false
  | .succ n', .succ m' => ltb n' m'

#eval ltb 1 2
#eval ltb 10242 1055090
example : (ltb 1 2) = true := by rfl

end Exercise1

--- Proof by Simplification

theorem plus_0_n : ∀ n : Nat, 0 + n = n := by
  intros n
  simp

#check ∀ n : Nat, 0 + n = n

example : ∀ n : Nat, 1 + n = .succ n := by
  intros m
  simp
  apply Nat.add_comm 1 m

example : ∀ n : Nat, 0 * n = 0 := by
  intros n
  exact Nat.zero_mul n

--- Proof by Rewriting
example : ∀ n m : Nat, n = m → n + n = m + m := by
  intros n m h
  rw [h]

namespace Exercise1

theorem plus_id_exercise : ∀ n m o : Nat, n = m → m = o → n + m = m + o := by
  intros n m o h₁ h₂
  rw [h₁]
  rw [h₂]

#check plus_0_n

theorem mult_n_1 : ∀ p : Nat, p * 1 = p := by
  intros p
  cases p
  . rw [Nat.mul_one]
  . rw [Nat.mul_one]

example : ∀ p : Nat, p * 1 = p := by
  intros p
  rw [Nat.mul_one]

#check Nat.mul_zero
#check Nat.mul_succ
example : ∀ p : Nat, p * 1 = p := by
  intros
  rw [Nat.mul_succ]
  rw [Nat.mul_zero]
  simp

end Exercise1

#eval (1).succ.succ.succ
#eval [1, 2, 3, 4].foldl (· + ·) 0
#print Array.foldl
#print optParam

--- Proof by Case Analysis
example : ∀ n : Nat, ((n + 1) = 0) = False := by
  intros n
  cases n
  case zero => simp only [Nat.zero_add, Nat.add_one_ne_zero]
  case succ => simp only [Nat.add_one_ne_zero]

example : ∀ b : Bool, ¬ (¬ b) = b := by
  intros b
  cases b
  . simp
  . rw [Lean.Grind.not_eq_prop]

example : ∀ b c : Bool, (b ∧ c) = (c ∧ b) := by
  intros b c
  cases b
  . cases c
    . simp only [Bool.false_eq_true, and_self]
    . rw [@and_comm]
  . rw [@and_comm]

#eval true ∧ true
#eval (true ∧ true) = (true ∧ true)
#eval true ∧ false = false ∧ true
#eval false ∧ false = false ∧ false
#eval (false ∧ false) = (false ∧ false)
#eval Bool.and true true
#eval Bool.true ∧ Bool.true
#eval true && false = false && true
#print and_comm

namespace Exercise

example : ∀ b c : Bool, (Bool.and b c = true) → (c = true) := by
  intros b c
  cases c
  case true => exact fun _a => rfl
  case false =>
    cases b
    case true =>
      intros h
      exact h
    case false =>
      intros h
      exact h

#print id
#check Function.const

example : ∀ n : Nat, (0 == (n + 1)) = false := by
  intros n
  cases n
  . simp only [Nat.zero_add, Nat.reduceBEq]
  . simp only [Nat.reduceBeqDiff]

end Exercise

--- More on Notation
-- skipping

--- More Exercises
namespace Exercise

theorem identity_fn_applied_twice : ∀ (f : Bool → Bool), (∀ (x : Bool), f x = x) → ∀ (b : Bool), f (f b) = b := by
  intro f
  intro h₁
  intro b
  rw [h₁]
  rw [h₁]

theorem negation_fn_applied_twice : ∀ (f : Bool → Bool), (∀ (x : Bool), f x = not x) → ∀ (b : Bool), f (f b) = b := by
  intros f h b
  rw [h]
  rw [h]
  rw [@Bool.not_eq_eq_eq_not]

theorem andb_eq_orb :
  ∀ (b c : Bool),
  (andb b c = orb b c) →
  b = c
:= by
  intros b c
  intro h
  cases b
  case true => exact id (Eq.symm h)
  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
