From cf7dd60442eb2400d5db0de4160ca526324ab426 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Dec 2014 21:36:34 -0800 Subject: [PATCH] feat(hott/init): add well-founded recursion to HoTT library --- hott/init/wf.hlean | 159 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 hott/init/wf.hlean diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean new file mode 100644 index 0000000000..6c5eaf6469 --- /dev/null +++ b/hott/init/wf.hlean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura +-/ +prelude +import init.relation init.tactic + +inductive acc.{l₁ l₂} {A : Type.{l₁}} (R : A → A → Type.{l₂}) : A → Type.{max l₁ l₂} := +intro : ∀x, (∀ y, R y x → acc R y) → acc R x + +namespace acc + variables {A : Type} {R : A → A → Type} + + definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y := + rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂ +end acc + +inductive well_founded [class] {A : Type} (R : A → A → Type) : Type := +intro : (∀ a, acc R a) → well_founded R + +namespace well_founded + definition apply [coercion] {A : Type} {R : A → A → Type} (wf : well_founded R) : ∀a, acc R a := + take a, well_founded.rec_on wf (λp, p) a + + context + parameters {A : Type} {R : A → A → Type} + infix `≺`:50 := R + + hypothesis [Hwf : well_founded R] + + theorem recursion {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) + + theorem induction {C : A → Type} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a := + recursion a H + + parameter {C : A → Type} + parameter F : Πx, (Πy, y ≺ x → C y) → C x + + definition fix_F (x : A) (a : acc R x) : C x := + acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH) + + theorem fix_F_eq (x : A) (r : acc R x) : + fix_F x r = F x (λ (y : A) (p : y ≺ x), fix_F y (acc.inv r p)) := + acc.rec_on r (λ x H ih, rfl) + + -- Remark: after we prove function extensionality from univalence, we can drop this hypothesis + hypothesis F_ext : Π (x : A) (f g : Π y, y ≺ x → C y), + (Π (y : A) (p : y ≺ x), f y p = g y p) → F x f = F x g + + lemma fix_F_inv (x : A) (r : acc R x) : Π (s : acc R x), fix_F x r = fix_F x s := + acc.rec_on r (λ + (x₁ : A) + (h₁ : Π y, y ≺ x₁ → acc R y) + (ih₁ : Π y (hlt : y ≺ x₁) (s : acc R y), fix_F y (h₁ y hlt) = fix_F y s) + (s : acc R x₁), + have aux₁ : Π (s : acc R x₁) (h₁ : Π y, y ≺ x₁ → acc R y) (ih₁ : Π y (hlt : y ≺ x₁) (s : acc R y), + fix_F y (h₁ y hlt) = fix_F y s), fix_F x₁ (acc.intro x₁ h₁) = fix_F x₁ s, from + λ s, acc.rec_on s (λ + (x₂ : A) + (h₂ : Π y, y ≺ x₂ → acc R y) + (ih₂ : _) + (h₁ : Π y, y ≺ x₂ → acc R y) + (ih₁ : Π y (hlt : y ≺ x₂) (s : acc R y), fix_F y (h₁ y hlt) = fix_F y s), + calc fix_F x₂ (acc.intro x₂ h₁) + = F x₂ (λ (y : A) (p : y ≺ x₂), fix_F y (h₁ y p)) : rfl + ... = F x₂ (λ (y : A) (p : y ≺ x₂), fix_F y (h₂ y p)) : F_ext x₂ _ _ (λ (y : A) (p : y ≺ x₂), ih₁ y p (h₂ y p)) + ... = fix_F x₂ (acc.intro x₂ h₂) : rfl), + show fix_F x₁ (acc.intro x₁ h₁) = fix_F x₁ s, from + aux₁ s h₁ ih₁) + + -- Well-founded fixpoint + definition fix (x : A) : C x := + fix_F x (Hwf x) + + -- Well-founded fixpoint satisfies fixpoint equation + theorem fix_eq (x : A) : fix x = F x (λy h, fix y) := + calc + fix x + = fix_F x (Hwf x) : rfl + ... = F x (λy h, fix_F y (acc.inv (Hwf x) h)) : fix_F_eq x (Hwf x) + ... = F x (λy h, fix_F y (Hwf y)) : F_ext x _ _ (λ y h, fix_F_inv y _ _) + ... = F x (λy h, fix y) : rfl + + end +end well_founded + +open well_founded + +-- Empty relation is well-founded +definition empty.wf {A : Type} : well_founded empty_relation := +well_founded.intro (λ (a : A), + acc.intro a (λ (b : A) (lt : empty), empty.rec _ lt)) + +-- Subrelation of a well-founded relation is well-founded +namespace subrelation +context + parameters {A : Type} {R Q : A → A → Type} + parameters (H₁ : subrelation Q R) + parameters (H₂ : well_founded R) + + definition accessible {a : A} (ac : acc R a) : acc Q a := + acc.rec_on ac + (λ (x : A) (ax : _) (iH : ∀ (y : A), R y x → acc Q y), + acc.intro x (λ (y : A) (lt : Q y x), iH y (H₁ lt))) + + definition wf : well_founded Q := + well_founded.intro (λ a, accessible (H₂ a)) +end +end subrelation + +-- The inverse image of a well-founded relation is well-founded +namespace inv_image +context + parameters {A B : Type} {R : B → B → Type} + parameters (f : A → B) + parameters (H : well_founded R) + + definition accessible {a : A} (ac : acc R (f a)) : acc (inv_image R f) a := + have gen : ∀x, f x = f a → acc (inv_image R f) x, from + acc.rec_on ac + (λx acx (iH : ∀y, R y x → (∀z, f z = y → acc (inv_image R f) z)) + (z : A) (eq₁ : f z = x), + acc.intro z (λ (y : A) (lt : R (f y) (f z)), + iH (f y) (eq.rec_on eq₁ lt) y rfl)), + gen a rfl + + definition wf : well_founded (inv_image R f) := + well_founded.intro (λ a, accessible (H (f a))) +end +end inv_image + +-- The transitive closure of a well-founded relation is well-founded +namespace tc +context + parameters {A : Type} {R : A → A → Type} + notation `R⁺` := tc R + + definition accessible {z} (ac: acc R z) : acc R⁺ z := + acc.rec_on ac + (λ x acx (iH : ∀y, R y x → acc R⁺ y), + acc.intro x (λ (y : A) (lt : R⁺ y x), + have gen : x = x → acc R⁺ y, from + tc.rec_on lt + (λa b (H : R a b) (Heq : b = x), + iH a (eq.rec_on Heq H)) + (λa b c (H₁ : R⁺ a b) (H₂ : R⁺ b c) + (iH₁ : b = x → acc R⁺ a) + (iH₂ : c = x → acc R⁺ b) + (Heq : c = x), + acc.inv (iH₂ Heq) H₁), + gen rfl)) + + definition wf (H : well_founded R) : well_founded R⁺ := + well_founded.intro (λ a, accessible (H a)) + +end +end tc