-
Notifications
You must be signed in to change notification settings - Fork 350
/
casesRec.lean
51 lines (42 loc) · 1 KB
/
casesRec.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
namespace Ex1
def f (x : Nat) : Nat := by
cases x with
| zero => exact 1
| succ x' =>
apply Nat.mul 2
exact f x'
#eval f 10
example : f x.succ = 2 * f x := rfl
end Ex1
namespace Ex2
inductive Foo where
| mk : List Foo → Foo
mutual
def g (x : Foo) : Nat := by
cases x with
| mk xs => exact gs xs
def gs (xs : List Foo) : Nat := by
cases xs with
| nil => exact 1
| cons x xs =>
apply Nat.add
exact g x
exact gs xs
end
end Ex2
namespace Ex3
inductive Foo where
| a | b | c
| pair: Foo × Foo → Foo
def Foo.deq (a b : Foo) : Decidable (a = b) := by
cases a <;> cases b
any_goals apply isFalse Foo.noConfusion
any_goals apply isTrue rfl
case pair a b =>
let (a₁, a₂) := a
let (b₁, b₂) := b
exact match deq a₁ b₁, deq a₂ b₂ with
| isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂])
| isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl))
| _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))
end Ex3