171 lines
6.1 KiB
Text
171 lines
6.1 KiB
Text
open tactic
|
||
|
||
/- User spec
|
||
|
||
f 0 0 = some 1
|
||
f 0 m = f m 0
|
||
f (n+1) m = match f n m with
|
||
| some a := some (a+1)
|
||
| none := none
|
||
end
|
||
-/
|
||
|
||
/- Define f_aux using well-founded recursion -/
|
||
constant R : (nat × nat) → (nat × nat) → Prop
|
||
axioms R_wf : well_founded R
|
||
|
||
axiom Dec (p₂ p₁ : nat × nat) : R p₂ p₁
|
||
|
||
definition f_aux : Π (p₁ : nat × nat), (Π (p₂ : nat × nat), R p₂ p₁ → option nat) → option nat
|
||
| (0, 0) F := some 1
|
||
| (0, m) F := F (m, 0) (Dec (m, 0) (0, m))
|
||
| (n+1, m) F := match F (n, m) (Dec (n,m) (n+1, m)) with
|
||
| some a := some (a+1)
|
||
| none := none
|
||
end
|
||
|
||
lemma f_aux.eq_1 (F : Π (p₂ : nat × nat), R p₂ (0,0) → option nat) : f_aux (0, 0) F = some 1 :=
|
||
rfl
|
||
|
||
lemma f_aux.eq_2 (m : nat) (F : Π (p₂ : nat × nat), R p₂ (0, m+1) → option nat) :
|
||
f_aux (0, m+1) F = F (m+1, 0) (Dec (m+1, 0) (0, m+1)) :=
|
||
rfl
|
||
|
||
/- The procedure is bottom-up, and will define the auxiliary function match_1 for the nexted match -/
|
||
|
||
definition match_1 : option nat → option nat
|
||
| (some a) := some (a+1)
|
||
| none := none
|
||
|
||
lemma match_1.eq_1 (a : nat) : match_1 (some a) = some (a+1) :=
|
||
rfl
|
||
|
||
lemma match_1.eq_2 : match_1 none = none :=
|
||
rfl
|
||
|
||
lemma f_aux.eq_3 (n m : nat) (F : Π (p₂ : nat × nat), R p₂ (n+1, m) → option nat) :
|
||
f_aux (n+1, m) F = match_1 (F (n, m) (Dec (n,m) (n+1, m))) :=
|
||
rfl
|
||
|
||
/- "Expand" match_1 at f_aux.eq_3 -/
|
||
|
||
meta_definition rewrite_H (H : expr) : tactic unit :=
|
||
rewrite_core semireducible tt occurrences.all ff H
|
||
|
||
lemma f_aux.eq_3_a
|
||
(n m : nat)
|
||
(a : nat)
|
||
(F : Π (p₂ : nat × nat), R p₂ (n+1, m) → option nat)
|
||
(H : F (n, m) (Dec (n, m) (n+1, m)) = some a) :
|
||
f_aux (n+1, m) F = some (a+1) :=
|
||
by do rewrite `f_aux.eq_3, get_local `H >>= rewrite_H, rewrite `match_1.eq_1
|
||
|
||
lemma f_aux.eq_3_b
|
||
(n m : nat)
|
||
(F : Π (p₂ : nat × nat), R p₂ (n+1, m) → option nat)
|
||
(H : F (n, m) (Dec (n, m) (n+1, m)) = none) :
|
||
f_aux (n+1, m) F = none :=
|
||
by do rewrite `f_aux.eq_3, get_local `H >>= rewrite_H, rewrite `match_1.eq_2
|
||
|
||
/- Define f using fix -/
|
||
|
||
definition f (n m : nat) : option nat :=
|
||
well_founded.fix R_wf f_aux (n, m)
|
||
|
||
/- Prove lemmas about 'f' using well_founded.fix_eq -/
|
||
|
||
lemma f.eq_1 : f 0 0 = some 1 :=
|
||
well_founded.fix_eq R_wf f_aux (0, 0)
|
||
|
||
lemma f.eq_2 (m : nat) : f 0 (m+1) = f (m+1) 0 :=
|
||
well_founded.fix_eq R_wf f_aux (0, m+1)
|
||
|
||
lemma f.eq_3_a (n m a : nat) (H : f n m = some a) : f (n+1) m = some (a+1) :=
|
||
eq.trans (well_founded.fix_eq R_wf f_aux (n+1, m))
|
||
(f_aux.eq_3_a n m a (λ y h, well_founded.fix R_wf f_aux y) H)
|
||
|
||
lemma f.eq_3_b (n m : nat) (H : f n m = none) : f (n+1) m = none :=
|
||
eq.trans (well_founded.fix_eq R_wf f_aux (n+1, m))
|
||
(f_aux.eq_3_b n m (λ y h, well_founded.fix R_wf f_aux y) H)
|
||
|
||
/- Create f_aux.ind based on the structure of f_aux and generated equations -/
|
||
|
||
lemma f_aux.ind
|
||
(C : nat → nat → Type)
|
||
(m₁ : C 0 0)
|
||
(m₂ : ∀ m, C 0 m)
|
||
(m₃ : ∀ n m a, f n m = some a → C n m → C (n+1) m)
|
||
(m₄ : ∀ n m, f n m = none → C n m → C (n+1) m) :
|
||
Π (p₁ : nat × nat), (Π (p₂ : nat × nat), R p₂ p₁ → C (pr₁ p₂) (pr₂ p₂)) → C (pr₁ p₁) (pr₂ p₁)
|
||
| (0, 0) F := m₁
|
||
| (0, m) F := m₂ m
|
||
| (n+1, m) F :=
|
||
have C n m, from F (n, m) (Dec (n, m) (n+1, m)),
|
||
match f n m, rfl : ∀ x, f n m = x → _ with
|
||
| some a, H₁ := m₃ n m a H₁ this
|
||
| none, H₂ := m₄ n m H₂ this
|
||
end
|
||
|
||
lemma f.ind
|
||
(C : nat → nat → Type)
|
||
(m₁ : C 0 0)
|
||
(m₂ : ∀ m, C 0 m)
|
||
(m₃ : ∀ n m a, f n m = some a → C n m → C (n+1) m)
|
||
(m₄ : ∀ n m, f n m = none → C n m → C (n+1) m)
|
||
(n m : nat) : C n m :=
|
||
well_founded.fix R_wf (f_aux.ind C m₁ m₂ m₃ m₄) (n, m)
|
||
|
||
constant unpair : nat → nat × nat
|
||
constant decode (A : Type) : nat → option A
|
||
constant decode_list (A : Type) : nat → nat → option (list A)
|
||
/-
|
||
User spec
|
||
definition decode_list_core : nat → nat → option (list A)
|
||
| 0 v := some []
|
||
| (succ n) v :=
|
||
match unpair v with
|
||
| (v₁, v₂) :=
|
||
match decode A v₁ with
|
||
| some a :=
|
||
match decode_list_core n v₂ with
|
||
| some l := some (a::l)
|
||
| none := none
|
||
end
|
||
| none := none
|
||
end
|
||
end
|
||
-/
|
||
|
||
lemma decode_list_aux.ind
|
||
(A : Type)
|
||
(C : nat → nat → Type)
|
||
(m₁ : ∀ v, C 0 v)
|
||
(m₂ : ∀ n v v₁ v₂ a ls, unpair v = (v₁, v₂) → decode A v₁ = some a → decode_list A n v₂ = some ls → C n v₂ → C (n+1) v)
|
||
(m₃ : ∀ n v v₁ v₂ a, unpair v = (v₁, v₂) → decode A v₁ = some a → decode_list A n v₂ = none → C n v₂ → C (n+1) v)
|
||
(m₄ : ∀ n v v₁ v₂, unpair v = (v₁, v₂) → decode A v₁ = none → C (n+1) v) :
|
||
Π (p₁ : nat × nat), (Π (p₂ : nat × nat), R p₂ p₁ → C (pr₁ p₂) (pr₂ p₂)) → C (pr₁ p₁) (pr₂ p₁)
|
||
| (0, v) F := m₁ v
|
||
| (n+1, v) F :=
|
||
match unpair v, rfl : ∀ x, unpair v = x → _ with
|
||
| (v₁, v₂), Heq₁ :=
|
||
match decode A v₁, rfl : ∀ x, decode A v₁ = x → _ with
|
||
| some a, Heq₂ :=
|
||
have aux : R (n, v₂) (n+1, v) → C n v₂, from F (n, v₂),
|
||
have C n v₂, from aux (Dec (n, v₂) (n+1, v)),
|
||
match decode_list A n v₂, rfl : ∀ x, decode_list A n v₂ = x → _ with
|
||
| some ls, He₃ := m₂ n v v₁ v₂ a ls Heq₁ Heq₂ He₃ this
|
||
| none, He₃ := m₃ n v v₁ v₂ a Heq₁ Heq₂ He₃ this
|
||
end
|
||
| none, Heq₂ := m₄ n v v₁ v₂ Heq₁ Heq₂
|
||
end
|
||
end
|
||
|
||
lemma decode_list.ind
|
||
(A : Type)
|
||
(C : nat → nat → Type)
|
||
(m₁ : ∀ v, C 0 v)
|
||
(m₂ : ∀ n v v₁ v₂ a ls, unpair v = (v₁, v₂) → decode A v₁ = some a → decode_list A n v₂ = some ls → C n v₂ → C (n+1) v)
|
||
(m₃ : ∀ n v v₁ v₂ a, unpair v = (v₁, v₂) → decode A v₁ = some a → decode_list A n v₂ = none → C n v₂ → C (n+1) v)
|
||
(m₄ : ∀ n v v₁ v₂, unpair v = (v₁, v₂) → decode A v₁ = none → C (n+1) v)
|
||
(n m : nat) : C n m :=
|
||
well_founded.fix R_wf (decode_list_aux.ind A C m₁ m₂ m₃ m₄) (n, m)
|