michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/logic/wf): add well_founded class, and cleanup file

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-07 10:18:24 -08:00
parent f16f215c2a
commit 92b0a538c5
1 changed files with 33 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
library/logic/wf.lean
View file

@ -6,27 +6,31 @@ import logic.eq
inductive acc {A : Type} (R : A → A → Prop) : A → Prop := inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
intro : ∀x, (∀ y, R y x → acc R y) → acc R x intro : ∀x, (∀ y, R y x → acc R y) → acc R x
definition well_founded {A : Type} (R : A → A → Prop) := namespace acc
∀a, acc R a variables {A : Type} {R : A → A → Prop}
definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y :=
acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂
end acc
inductive well_founded [class] {A : Type} (R : A → A → Prop) : Prop :=
intro : (∀ a, acc R a) → well_founded R
namespace well_founded namespace well_founded
definition apply [coercion] {A : Type} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
take a, well_founded.rec_on wf (λp, p) a
context context
parameters {A : Type} {R : A → A → Prop} parameters {A : Type} {R : A → A → Prop}
infix `≺`:50 := R infix `≺`:50 := R
definition acc_inv {x y : A} (H₁ : acc R x) (H₂ : y ≺ x) : acc R y := hypothesis [Hwf : well_founded R]
have gen : y ≺ x → acc R y, from
acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂),
gen H₂
hypothesis Hwf : well_founded R theorem recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
theorem well_founded_rec {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
acc.rec_on (Hwf a) (λ x₁ ac₁ iH, H x₁ iH) acc.rec_on (Hwf a) (λ x₁ ac₁ iH, H x₁ iH)
theorem well_founded_ind {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a := theorem indunction {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a :=
well_founded_rec a H recursion a H
variable {C : A → Type} variable {C : A → Type}
variable F : Πx, (Πy, y ≺ x → C y) → C x variable F : Πx, (Πy, y ≺ x → C y) → C x
@ -35,29 +39,30 @@ context
acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH) acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH)
theorem fix_F_eq (x : A) (r : acc R x) : theorem fix_F_eq (x : A) (r : acc R x) :
fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc_inv r p)) := fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
have gen : Π r : acc R x, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc_inv r p)), from have gen : Π r : acc R x, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)), from
acc.rec_on r acc.rec_on r
(λ x₁ ac iH (r₁ : acc R x₁), (λ x₁ ac iH (r₁ : acc R x₁),
-- The proof is straightforward after we replace r₁ with acc.intro (to "unblock" evaluation). -- The proof is straightforward after we replace r₁ with acc.intro (to "unblock" evaluation).
calc fix_F F x₁ r₁ calc fix_F F x₁ r₁
= fix_F F x₁ (acc.intro x₁ ac) : proof_irrel r₁ = fix_F F x₁ (acc.intro x₁ ac) : proof_irrel r₁
... = F x₁ (λ y ay, fix_F F y (acc_inv r₁ ay)) : rfl), ... = F x₁ (λ y ay, fix_F F y (acc.inv r₁ ay)) : rfl),
gen r gen r
end end
variables {A : Type} {C : A → Type} {R : A → A → Prop} variables {A : Type} {C : A → Type} {R : A → A → Prop}
-- Well-founded fixpoint -- Well-founded fixpoint
definition fix (Hwf : well_founded R) (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x := definition fix [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x :=
fix_F F x (Hwf x) fix_F F x (Hwf x)
-- Well-founded fixpoint satisfies fixpoint equation -- Well-founded fixpoint satisfies fixpoint equation
theorem fix_eq (Hwf : well_founded R) (F : Πx, (Πy, R y x → C y) → C x) (x : A) : theorem fix_eq [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
fix Hwf F x = F x (λy h, fix Hwf F y) := fix F x = F x (λy h, fix F y) :=
calc calc
-- The proof is straightforward, it just uses fix_F_eq and proof irrelevance -- The proof is straightforward, it just uses fix_F_eq and proof irrelevance
fix Hwf F x fix F x
= F x (λy h, fix_F F y (acc_inv (Hwf x) h)) : fix_F_eq F x (Hwf x) = F x (λy h, fix_F F y (acc.inv (Hwf x) h)) : fix_F_eq F x (Hwf x)
... = F x (λy h, fix Hwf F y) : rfl -- proof irrelevance is used here ... = F x (λy h, fix F y) : rfl -- proof irrelevance is used here
end well_founded end well_founded