software_foundation/basics/main.lean

--- 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

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