237 lines
3.9 KiB
Text
237 lines
3.9 KiB
Text
--- 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
|
||
|