--- Data and Functions

inductive Day : Type :=
  | 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

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 :=
  | B₁
  | B₀

inductive Nybble :=
  | 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