-
Notifications
You must be signed in to change notification settings - Fork 346
/
inductive_pred.lean
117 lines (91 loc) · 3.85 KB
/
inductive_pred.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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
import Lean
open Lean
namespace Ex
inductive LE : Nat → Nat → Prop
| refl : LE n n
| succ : LE n m → LE n m.succ
def typeOf {α : Sort u} (a : α) := α
theorem LE.trans' : LE m n → LE n o → LE m o
| h1, refl => h1
| h1, succ h2 => succ (trans' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
inductive Even : Nat → Prop
| zero : Even 0
| ss : Even n → Even n.succ.succ
theorem Even_brecOn : typeOf @Even.brecOn = ∀ {motive : (a : Nat) → Even a → Prop} {a : Nat} (x : Even a),
(∀ (a : Nat) (x : Even a), @Even.below motive a x → motive a x) → motive a x := rfl
theorem Even.add : Even n → Even m → Even (n+m) := by
intro h1 h2
induction h2 with
| zero => exact h1
| ss h2 ih => exact ss ih
theorem Even.add' : Even n → Even m → Even (n+m)
| h1, zero => h1
| h1, ss h2 => ss (add' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
inductive Power2 : Nat → Prop
| base : Power2 1
| ind : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a),
(∀ (a : Nat) (x : Power2 a), @Power2.below motive a x → motive a x) → motive a x := rfl
theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
intro h1 h2
induction h2 with
| base => simp_all
| ind h2 ih => exact mul_left_comm .. ▸ ind ih
/- The following example fails because the structural recursion cannot be performed on the `Nat`s and
the `brecOn` construction doesn't work for inductive predicates -/
set_option trace.Elab.definition.structural true in
set_option trace.Meta.IndPredBelow.match true in
set_option pp.explicit true in
theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
| h1, base => by simp_all
| h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
inductive tm : Type :=
| C : Nat → tm
| P : tm → tm → tm
open tm
set_option hygiene false in
infixl:40 " ==> " => step
inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) ==> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 ==> t1' →
P t1 t2 ==> P t1' t2
| ST_Plus2 : ∀ n1 t2 t2',
t2 ==> t2' →
P (C n1) t2 ==> P (C n1) t2'
def deterministic {X : Type} (R : X → X → Prop) :=
∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2
theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ =>
@step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ =>
match hy₁, hy₂ with
| step.below.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
| step.below.ST_Plus1 _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw [←ih t₁']; assumption
| step.below.ST_Plus1 _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
| step.below.ST_Plus2 _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw [←ih t₂]; assumption
| step.below.ST_Plus2 _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
) y₂ hy₂
section NestedRecursion
axiom f : Nat → Nat
inductive is_nat : Nat -> Prop
| Z : is_nat 0
| S {n} : is_nat n → is_nat (f n)
axiom P : Nat → Prop
axiom F0 : P 0
axiom F1 : P (f 0)
axiom FS {n : Nat} : P n → P (f (f n))
-- we would like to write this
theorem foo : ∀ {n}, is_nat n → P n
| _, is_nat.Z => F0
| _, is_nat.S is_nat.Z => F1
| _, is_nat.S (is_nat.S h) => FS (foo h)
theorem foo' : ∀ {n}, is_nat n → P n := fun h =>
@is_nat.brecOn (fun n hn => P n) _ h fun n h ih =>
match ih with
| is_nat.below.Z => F0
| is_nat.below.S is_nat.below.Z _ => F1
| is_nat.below.S (is_nat.below.S b hx) h₂ => FS hx
end NestedRecursion
end Ex