510 lines
9.7 KiB
Text
Executable file
510 lines
9.7 KiB
Text
Executable file
--- 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
|