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

feat(init/wf): port from standard library to HoTT library

Browse source 
After this commit we need some more advanced theorems in init/wf, notably function extenstionality.
For this reason I had to refactor the init folder a little bit.
To keep the init folders in both libraries similar, I did the same refactorization in the standard library, even though that was not required for the standard library
This commit is contained in:
Floris van Doorn 2016-02-08 20:07:44 -05:00 committed by Leonardo de Moura
parent c0abcc7722
commit e14d4a4c0c
7 changed files with 242 additions and 222 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
hott/init/nat.hlean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura Authors: Floris van Doorn, Leonardo de Moura
-/ -/
prelude 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 eq eq.ops decidable
open algebra sum open algebra sum
set_option class.force_new true 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 := 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 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 := theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b :=
succ_le_succ succ_le_succ

59
hott/init/types.hlean
View file

@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
-/ -/
prelude prelude
import init.num init.wf import init.num init.relation
open iff open iff
-- Empty type -- 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) 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 end prod

228
hott/init/wf.hlean
View file

@ -3,9 +3,10 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
-/ -/
prelude 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₂} := 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 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 namespace acc
variables {A : Type} {R : A → A → Type} 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 := 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₂ 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 end acc
inductive well_founded [class] {A : Type} (R : A → A → Type) : Type := 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 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 take a, well_founded.rec_on wf (λp, p) a
section section
@ -30,60 +54,42 @@ namespace well_founded
hypothesis [Hwf : well_founded R] 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) 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 recursion a H
parameter {C : A → Type} variable {C : A → Type}
parameter F : Πx, (Πy, y ≺ x → C y) → C x variable F : Πx, (Πy, y ≺ x → C y) → C x
definition fix_F (x : A) (a : acc R x) : C x := definition fix_F (x : A) (a : acc R x) : C x :=
acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH) acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH)
definition fix_F_eq (x : A) (r : acc R x) : 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)) := fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
acc.rec_on r (λ x H ih, rfl) 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 variables {A : Type} {C : A → Type} {R : A → A → Type}
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 -- Well-founded fixpoint
definition fix (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 x (Hwf x) fix_F F x (Hwf x)
-- Well-founded fixpoint satisfies fixpoint equation -- Well-founded fixpoint satisfies fixpoint equation
definition fix_eq (x : A) : fix x = F x (λy h, fix y) := theorem fix_eq [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
calc fix F x = F x (λy h, fix F y) :=
fix x begin
= fix_F x (Hwf x) : rfl refine fix_F_eq F x (Hwf x) ⬝ _,
... = F x (λy h, fix_F y (acc.inv (Hwf x) h)) : fix_F_eq x (Hwf x) apply ap (F x),
... = F x (λy h, fix_F y (Hwf y)) : F_ext x _ _ (λ y h, fix_F_inv y _ _) apply eq_of_homotopy, intro a,
... = F x (λy h, fix y) : rfl apply eq_of_homotopy, intro r,
apply ap (fix_F F a),
apply acc.acc_eq
end end
end well_founded end well_founded
@ -97,17 +103,20 @@ well_founded.intro (λ (a : A),
-- Subrelation of a well-founded relation is well-founded -- Subrelation of a well-founded relation is well-founded
namespace subrelation namespace subrelation
section section
universe variable u
parameters {A : Type} {R Q : A → A → Type} parameters {A : Type} {R Q : A → A → Type}
parameters (H₁ : subrelation Q R) parameters (H₁ : subrelation Q R)
parameters (H₂ : well_founded R) parameters (H₂ : well_founded R)
definition accessible {a : A} (ac : acc R a) : acc Q a := definition accessible {a : A} (ac : acc R a) : acc Q a :=
acc.rec_on ac using H₁,
(λ (x : A) (ax : _) (iH : ∀ (y : A), R y x → acc Q y), begin
acc.intro x (λ (y : A) (lt : Q y x), iH y (H₁ lt))) induction ac with x ax ih, constructor,
exact λ (y : A) (lt : Q y x), ih y (H₁ lt)
end
definition wf : well_founded Q := 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
end subrelation end subrelation
@ -118,14 +127,16 @@ section
parameters (f : A → B) parameters (f : A → B)
parameters (H : well_founded R) 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 := 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_aux ac a rfl
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) := definition wf : well_founded (inv_image R f) :=
well_founded.intro (λ a, accessible (H (f a))) well_founded.intro (λ a, accessible (H (f a)))
@ -139,22 +150,99 @@ section
local notation `R⁺` := tc R local notation `R⁺` := tc R
definition accessible {z} (ac: acc R z) : acc R⁺ z := definition accessible {z} (ac: acc R z) : acc R⁺ z :=
acc.rec_on ac begin
(λ x acx (iH : ∀y, R y x → acc R⁺ y), induction ac with x acx ih,
acc.intro x (λ (y : A) (lt : R⁺ y x), constructor, intro y rel,
have gen : x = x → acc R⁺ y, from induction rel with a b rab a b c rab rbc ih₁ ih₂,
tc.rec_on lt {exact ih a rab},
(λa b (H : R a b) (Heq : b = x), {exact acc.inv (ih₂ acx ih) rab}
iH a (eq.rec_on Heq H)) end
(λ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⁺ := definition wf (H : well_founded R) : well_founded R⁺ :=
well_founded.intro (λ a, accessible (H a)) well_founded.intro (λ a, accessible (H a))
end end
end tc 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

16
library/init/nat.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura Authors: Floris van Doorn, Leonardo de Moura
-/ -/
prelude prelude
import init.wf init.tactic init.num import init.relation init.tactic init.num
open eq.ops decidable or open eq.ops decidable or
notation `ℕ` := nat notation `ℕ` := nat
@ -189,20 +189,6 @@ namespace nat
protected theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := 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 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 := theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b :=
succ_le_succ succ_le_succ

58
library/init/prod.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Jeremy Avigad Author: Leonardo de Moura, Jeremy Avigad
-/ -/
prelude prelude
import init.num init.wf import init.num init.relation
definition pair [constructor] := @prod.mk definition pair [constructor] := @prod.mk
notation A × B := prod A B notation A × B := prod A B
@ -30,60 +30,4 @@ namespace prod
| (a, b) := rfl | (a, b) := rfl
end 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 end prod

80
library/init/wf.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
-/ -/
prelude 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 := 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
@ -141,3 +141,81 @@ section
well_founded.intro (λ a, accessible (H a)) well_founded.intro (λ a, accessible (H a))
end end
end tc 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

2
library/init/wf_k.lean
View file

@ -2,7 +2,7 @@
-- Released under Apache 2.0 license as described in the file LICENSE. -- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura -- Author: Leonardo de Moura
prelude prelude
import init.nat import init.wf
namespace well_founded namespace well_founded
-- This is an auxiliary definition that useful for generating a new "proof" for (well_founded R) -- This is an auxiliary definition that useful for generating a new "proof" for (well_founded R)