diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 497a17979..2587f6abf 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura -/ prelude -import init.wf init.tactic init.num init.types init.path +import init.tactic init.num init.types init.path open eq eq.ops decidable open algebra sum set_option class.force_new true @@ -185,25 +185,6 @@ namespace nat protected theorem le_of_eq_sum_lt {a b : ℕ} (H : a = b ⊎ a < b) : a ≤ b := sum.rec_on H !nat.le_of_eq !nat.le_of_lt - -- less-than is well-founded - definition lt.wf [instance] : well_founded (lt : ℕ → ℕ → Type₀) := - begin - constructor, intro n, induction n with n IH, - { constructor, intros n H, exfalso, exact !not_lt_zero H}, - { constructor, intros m H, - assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, - { intros n₁ hlt, induction hlt, - { intro p, injection p with q, exact q ▸ IH}, - { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}}, - apply aux H rfl}, - end - - definition measure {A : Type} : (A → ℕ) → A → A → Type₀ := - inv_image lt - - definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := - inv_image.wf f lt.wf - theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b := succ_le_succ diff --git a/hott/init/types.hlean b/hott/init/types.hlean index f01da8acf..bac36fc19 100644 --- a/hott/init/types.hlean +++ b/hott/init/types.hlean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer -/ prelude -import init.num init.wf +import init.num init.relation open iff -- Empty type @@ -92,61 +92,4 @@ namespace prod definition flip [unfold 3] {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a) - open well_founded - - section - variables {A B : Type} - variable (Ra : A → A → Type) - variable (Rb : B → B → Type) - - -- Lexicographical order based on Ra and Rb - inductive lex : A × B → A × B → Type := - | left : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂) - | right : ∀a {b₁ b₂}, Rb b₁ b₂ → lex (a, b₁) (a, b₂) - - -- Relational product based on Ra and Rb - inductive rprod : A × B → A × B → Type := - intro : ∀{a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂) - end - - section - parameters {A B : Type} - parameters {Ra : A → A → Type} {Rb : B → B → Type} - local infix `≺`:50 := lex Ra Rb - - definition lex.accessible {a} (aca : acc Ra a) (acb : ∀b, acc Rb b): ∀b, acc (lex Ra Rb) (a, b) := - acc.rec_on aca - (λxa aca (iHa : ∀y, Ra y xa → ∀b, acc (lex Ra Rb) (y, b)), - λb, acc.rec_on (acb b) - (λxb acb - (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)), - acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)), - have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from - @prod.lex.rec_on A B Ra Rb (λp₁ p₂ h, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) - p (xa, xb) lt - (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), - show acc (lex Ra Rb) (a₁, b₁), from - have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, - iHa a₁ Ra₁ b₁) - (λa b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb), - show acc (lex Ra Rb) (a, b₁), from - have Rb₁ : Rb b₁ xb, from eq.rec_on eq₃ H, - have eq₂' : xa = a, from eq.rec_on eq₂ rfl, - eq.rec_on eq₂' (iHb b₁ Rb₁)), - aux rfl rfl))) - - -- The lexicographical order of well founded relations is well-founded - definition lex.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) := - well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) (well_founded.apply Hb) b)) - - -- Relational product is a subrelation of the lex - definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := - λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) - - -- The relational product of well founded relations is well-founded - definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := - subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb) - - end - end prod diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean index b5fc9cc71..00346cd30 100644 --- a/hott/init/wf.hlean +++ b/hott/init/wf.hlean @@ -3,9 +3,10 @@ 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 +import init.relation init.tactic init.funext + +open eq 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 @@ -13,15 +14,38 @@ intro : ∀x, (∀ y, R y x → acc R y) → acc R x namespace acc variables {A : Type} {R : A → A → Type} + definition acc_eq {a : A} (H₁ H₂ : acc R a) : H₁ = H₂ := + begin + induction H₁ with a K₁ IH₁, + induction H₂ with a K₂ IH₂, + apply eq.ap (intro a), + apply eq_of_homotopy, intro a, + apply eq_of_homotopy, intro r, + apply IH₁ + end + 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₂ + + -- dependent elimination for acc + protected definition drec [recursor] + {C : Π (a : A), acc R a → Type} + (h₁ : Π (x : A) (acx : Π (y : A), R y x → acc R y), + (Π (y : A) (ryx : R y x), C y (acx y ryx)) → C x (acc.intro x acx)) + {a : A} (h₂ : acc R a) : C a h₂ := + begin + refine acc.rec _ h₂ h₂, + intro x acx ih h₂, + exact transport (C x) !acc_eq (h₁ x acx (λ y ryx, ih y ryx (acx y ryx))) + end + end acc inductive well_founded [class] {A : Type} (R : A → A → Type) : Type := -intro : (∀ a, acc R a) → well_founded R +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 := + 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 section @@ -30,60 +54,42 @@ namespace well_founded hypothesis [Hwf : well_founded R] - definition recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a := + 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) - definition induction {C : A → Type} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a := + 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 + variable {C : A → Type} + variable 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) - definition 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) + 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)) := + begin + induction r using acc.drec, + reflexivity -- proof is star due to proof irrelevance + end + end - -- 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₁) + variables {A : Type} {C : A → Type} {R : A → A → Type} -- Well-founded fixpoint - definition fix (x : A) : C x := - fix_F x (Hwf 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) -- Well-founded fixpoint satisfies fixpoint equation - definition 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 - + theorem fix_eq [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) : + fix F x = F x (λy h, fix F y) := + begin + refine fix_F_eq F x (Hwf x) ⬝ _, + apply ap (F x), + apply eq_of_homotopy, intro a, + apply eq_of_homotopy, intro r, + apply ap (fix_F F a), + apply acc.acc_eq end end well_founded @@ -97,17 +103,20 @@ well_founded.intro (λ (a : A), -- Subrelation of a well-founded relation is well-founded namespace subrelation section + universe variable u 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))) + using H₁, + begin + induction ac with x ax ih, constructor, + exact λ (y : A) (lt : Q y x), ih y (H₁ lt) + end definition wf : well_founded Q := - well_founded.intro (λ a, accessible (H₂ a)) + well_founded.intro (λ a, accessible proof (@apply A R H₂ a) qed) end end subrelation @@ -118,14 +127,16 @@ section parameters (f : A → B) parameters (H : well_founded R) + private definition acc_aux {b : B} (ac : acc R b) : Π x, f x = b → acc (inv_image R f) x := + begin + induction ac with x acx ih, + intro z e, constructor, + intro y lt, subst x, + exact ih (f y) lt y rfl + end + 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 + acc_aux ac a rfl definition wf : well_founded (inv_image R f) := well_founded.intro (λ a, accessible (H (f a))) @@ -139,22 +150,99 @@ section local 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)) + begin + induction ac with x acx ih, + constructor, intro y rel, + induction rel with a b rab a b c rab rbc ih₁ ih₂, + {exact ih a rab}, + {exact acc.inv (ih₂ acx ih) rab} + end definition wf (H : well_founded R) : well_founded R⁺ := well_founded.intro (λ a, accessible (H a)) - end end tc + +namespace nat + + -- less-than is well-founded + definition lt.wf [instance] : well_founded (lt : ℕ → ℕ → Type₀) := + begin + constructor, intro n, induction n with n IH, + { constructor, intros n H, exfalso, exact !not_lt_zero H}, + { constructor, intros m H, + assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, + { intros n₁ hlt, induction hlt, + { intro p, injection p with q, exact q ▸ IH}, + { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}}, + apply aux H rfl}, + end + + definition measure {A : Type} : (A → ℕ) → A → A → Type₀ := + inv_image lt + + definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := + inv_image.wf f lt.wf + +end nat + +namespace prod + + open well_founded prod.ops + + section + variables {A B : Type} + variable (Ra : A → A → Type) + variable (Rb : B → B → Type) + + -- Lexicographical order based on Ra and Rb + inductive lex : A × B → A × B → Type := + | left : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂) + | right : ∀a {b₁ b₂}, Rb b₁ b₂ → lex (a, b₁) (a, b₂) + + -- Relational product based on Ra and Rb + inductive rprod : A × B → A × B → Type := + intro : ∀{a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂) + end + + section + parameters {A B : Type} + parameters {Ra : A → A → Type} {Rb : B → B → Type} + local infix `≺`:50 := lex Ra Rb + + definition lex.accessible {a} (aca : acc Ra a) (acb : ∀b, acc Rb b): ∀b, acc (lex Ra Rb) (a, b) := + acc.rec_on aca + (λxa aca (iHa : ∀y, Ra y xa → ∀b, acc (lex Ra Rb) (y, b)), + λb, acc.rec_on (acb b) + (λxb acb + (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)), + acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)), + have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from + @prod.lex.rec_on A B Ra Rb (λp₁ p₂ h, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) + p (xa, xb) lt + (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), + show acc (lex Ra Rb) (a₁, b₁), from + have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, + iHa a₁ Ra₁ b₁) + (λa b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb), + show acc (lex Ra Rb) (a, b₁), from + have Rb₁ : Rb b₁ xb, from eq.rec_on eq₃ H, + have eq₂' : xa = a, from eq.rec_on eq₂ rfl, + eq.rec_on eq₂' (iHb b₁ Rb₁)), + aux rfl rfl))) + + -- The lexicographical order of well founded relations is well-founded + definition lex.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) := + well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) (well_founded.apply Hb) b)) + + -- Relational product is a subrelation of the lex + definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := + λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) + + -- The relational product of well founded relations is well-founded + definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := + subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb) + + end + +end prod diff --git a/library/init/nat.lean b/library/init/nat.lean index 3488756eb..f11181388 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura -/ prelude -import init.wf init.tactic init.num +import init.relation init.tactic init.num open eq.ops decidable or notation `ℕ` := nat @@ -189,20 +189,6 @@ namespace nat protected theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := or.elim H !nat.le_of_eq !nat.le_of_lt - -- less-than is well-founded - definition lt.wf [instance] : well_founded lt := - well_founded.intro (nat.rec - (!acc.intro (λn H, absurd H (not_lt_zero n))) - (λn IH, !acc.intro (λm H, - or.elim (nat.eq_or_lt_of_le (le_of_succ_le_succ H)) - (λe, eq.substr e IH) (acc.inv IH)))) - - definition measure {A : Type} : (A → ℕ) → A → A → Prop := - inv_image lt - - definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := - inv_image.wf f lt.wf - theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b := succ_le_succ diff --git a/library/init/prod.lean b/library/init/prod.lean index 6085c43c7..f4a8027cf 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura, Jeremy Avigad -/ prelude -import init.num init.wf +import init.num init.relation definition pair [constructor] := @prod.mk notation A × B := prod A B @@ -30,60 +30,4 @@ namespace prod | (a, b) := rfl end - open well_founded - - section - variables {A B : Type} - variable (Ra : A → A → Prop) - variable (Rb : B → B → Prop) - - -- Lexicographical order based on Ra and Rb - inductive lex : A × B → A × B → Prop := - | left : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂) - | right : ∀a {b₁ b₂}, Rb b₁ b₂ → lex (a, b₁) (a, b₂) - - -- Relational product based on Ra and Rb - inductive rprod : A × B → A × B → Prop := - intro : ∀{a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂) - end - - section - parameters {A B : Type} - parameters {Ra : A → A → Prop} {Rb : B → B → Prop} - local infix `≺`:50 := lex Ra Rb - - definition lex.accessible {a} (aca : acc Ra a) (acb : ∀b, acc Rb b): ∀b, acc (lex Ra Rb) (a, b) := - acc.rec_on aca - (λxa aca (iHa : ∀y, Ra y xa → ∀b, acc (lex Ra Rb) (y, b)), - λb, acc.rec_on (acb b) - (λxb acb - (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)), - acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)), - have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from - @prod.lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) - p (xa, xb) lt - (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), - show acc (lex Ra Rb) (a₁, b₁), from - have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, - iHa a₁ Ra₁ b₁) - (λa b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb), - show acc (lex Ra Rb) (a, b₁), from - have Rb₁ : Rb b₁ xb, from eq.rec_on eq₃ H, - have eq₂' : xa = a, from eq.rec_on eq₂ rfl, - eq.rec_on eq₂' (iHb b₁ Rb₁)), - aux rfl rfl))) - - -- The lexicographical order of well founded relations is well-founded - definition lex.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) := - well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) (well_founded.apply Hb) b)) - - -- Relational product is a subrelation of the lex - definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := - λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) - - -- The relational product of well founded relations is well-founded - definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := - subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb) - - end end prod diff --git a/library/init/wf.lean b/library/init/wf.lean index 979e586e8..a8fd38fba 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import init.relation init.tactic +import init.relation init.tactic init.nat init.prod inductive acc {A : Type} (R : A → A → Prop) : A → Prop := intro : ∀x, (∀ y, R y x → acc R y) → acc R x @@ -141,3 +141,81 @@ section well_founded.intro (λ a, accessible (H a)) end end tc + +namespace nat + + -- less-than is well-founded + definition lt.wf [instance] : well_founded lt := + well_founded.intro (nat.rec + (!acc.intro (λn H, absurd H (not_lt_zero n))) + (λn IH, !acc.intro (λm H, + or.elim (nat.eq_or_lt_of_le (le_of_succ_le_succ H)) + (λe, eq.substr e IH) (acc.inv IH)))) + + definition measure {A : Type} : (A → ℕ) → A → A → Prop := + inv_image lt + + definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := + inv_image.wf f lt.wf + +end nat + +namespace prod + open well_founded + + section + variables {A B : Type} + variable (Ra : A → A → Prop) + variable (Rb : B → B → Prop) + + -- Lexicographical order based on Ra and Rb + inductive lex : A × B → A × B → Prop := + | left : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂) + | right : ∀a {b₁ b₂}, Rb b₁ b₂ → lex (a, b₁) (a, b₂) + + -- Relational product based on Ra and Rb + inductive rprod : A × B → A × B → Prop := + intro : ∀{a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂) + end + + section + parameters {A B : Type} + parameters {Ra : A → A → Prop} {Rb : B → B → Prop} + local infix `≺`:50 := lex Ra Rb + + definition lex.accessible {a} (aca : acc Ra a) (acb : ∀b, acc Rb b): ∀b, acc (lex Ra Rb) (a, b) := + acc.rec_on aca + (λxa aca (iHa : ∀y, Ra y xa → ∀b, acc (lex Ra Rb) (y, b)), + λb, acc.rec_on (acb b) + (λxb acb + (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)), + acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)), + have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from + @prod.lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) + p (xa, xb) lt + (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), + show acc (lex Ra Rb) (a₁, b₁), from + have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, + iHa a₁ Ra₁ b₁) + (λa b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb), + show acc (lex Ra Rb) (a, b₁), from + have Rb₁ : Rb b₁ xb, from eq.rec_on eq₃ H, + have eq₂' : xa = a, from eq.rec_on eq₂ rfl, + eq.rec_on eq₂' (iHb b₁ Rb₁)), + aux rfl rfl))) + + -- The lexicographical order of well founded relations is well-founded + definition lex.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) := + well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) (well_founded.apply Hb) b)) + + -- Relational product is a subrelation of the lex + definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := + λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) + + -- The relational product of well founded relations is well-founded + definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := + subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb) + + end + +end prod diff --git a/library/init/wf_k.lean b/library/init/wf_k.lean index 03dde4d75..159e596ca 100644 --- a/library/init/wf_k.lean +++ b/library/init/wf_k.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura prelude -import init.nat +import init.wf namespace well_founded -- This is an auxiliary definition that useful for generating a new "proof" for (well_founded R)