From 5787f17138df2cf1ebffb3be8a49a0a8b43899ee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Apr 2018 10:04:03 -0700 Subject: [PATCH] chore(library/init): merge sigma/lex.lean with wf.lean --- library/init/data/default.lean | 2 +- library/init/data/sigma/default.lean | 7 - library/init/data/sigma/lex.lean | 128 ---------- library/init/meta/well_founded_tactics.lean | 2 +- library/init/wf.lean | 254 ++++++++++++++------ 5 files changed, 189 insertions(+), 204 deletions(-) delete mode 100644 library/init/data/sigma/default.lean delete mode 100644 library/init/data/sigma/lex.lean diff --git a/library/init/data/default.lean b/library/init/data/default.lean index 83305d7bc4..687559cfed 100644 --- a/library/init/data/default.lean +++ b/library/init/data/default.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string +import init.data.basic init.data.nat init.data.char init.data.string import init.data.list init.data.int init.data.array import init.data.bool init.data.fin init.data.uint init.data.ordering import init.data.rbtree init.data.rbmap init.data.option.basic init.data.option.instances diff --git a/library/init/data/sigma/default.lean b/library/init/data/sigma/default.lean deleted file mode 100644 index 1d25537078..0000000000 --- a/library/init/data/sigma/default.lean +++ /dev/null @@ -1,7 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -prelude -import init.data.sigma.lex diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean deleted file mode 100644 index e7fac27e21..0000000000 --- a/library/init/data/sigma/lex.lean +++ /dev/null @@ -1,128 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura --/ -prelude -import init.wf -universes u v - -namespace psigma -section -variables {α : Sort u} {β : α → Sort v} -variable (r : α → α → Prop) -variable (s : ∀ a, β a → β a → Prop) - --- Lexicographical order based on r and s -inductive lex : psigma β → psigma β → Prop -| left : ∀ {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ -| right : ∀ (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → lex ⟨a, b₁⟩ ⟨a, b₂⟩ -end - -section -parameters {α : Sort u} {β : α → Sort v} -parameters {r : α → α → Prop} {s : Π a : α, β a → β a → Prop} -local infix `≺`:50 := lex r s - -def lex_accessible {a} (aca : acc r a) (acb : ∀ a, well_founded (s a)) - : ∀ (b : β a), acc (lex r s) ⟨a, b⟩ := -acc.rec_on aca - (λ xa aca (iha : ∀ y, r y xa → ∀ b : β y, acc (lex r s) ⟨y, b⟩), - λ b : β xa, acc.rec_on (well_founded.apply (acb xa) b) - (λ xb acb - (ihb : ∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩), - acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), - have aux : xa = xa → xb == xb → acc (lex r s) p, from - @psigma.lex.rec_on α β r s (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁) - p ⟨xa, xb⟩ lt - (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb), - have aux : (∀ (y : α), r y xa → ∀ (b : β y), acc (lex r s) ⟨y, b⟩) → - r a₁ a₂ → ∀ (b₁ : β a₁), acc (lex r s) ⟨a₁, b₁⟩, - from eq.subst eq₂ (λ iha h b₁, iha a₁ h b₁), - aux iha h b₁) - (λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb), - have aux : ∀ (xb : β xa), (∀ (y : β xa), s xa y xb → acc (s xa) y) → - (∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩) → - lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ == xb → acc (lex r s) ⟨a, b₁⟩, - from eq.subst eq₂ (λ xb acb ihb lt b₁ h eq₃, - have new_eq₃ : b₂ = xb, from eq_of_heq eq₃, - have aux : (∀ (y : β a), s a y xb → acc (lex r s) ⟨a, y⟩) → - ∀ (b₁ : β a), s a b₁ b₂ → acc (lex r s) ⟨a, b₁⟩, - from eq.subst new_eq₃ (λ ihb b₁ h, ihb b₁ h), - aux ihb b₁ h), - aux xb acb ihb lt b₁ h eq₃), - aux rfl (heq.refl xb)))) - --- The lexicographical order of well founded relations is well-founded -def lex_wf (ha : well_founded r) (hb : ∀ x, well_founded (s x)) : well_founded (lex r s) := -well_founded.intro $ λ ⟨a, b⟩, lex_accessible (well_founded.apply ha a) hb b -end - -section -parameters {α : Sort u} {β : Sort v} - -def lex_ndep (r : α → α → Prop) (s : β → β → Prop) := -lex r (λ a : α, s) - -def lex_ndep_wf {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) - : well_founded (lex_ndep r s) := -well_founded.intro $ λ ⟨a, b⟩, lex_accessible (well_founded.apply ha a) (λ x, hb) b -end - -section -variables {α : Sort u} {β : Sort v} -variable (r : α → α → Prop) -variable (s : β → β → Prop) - --- Reverse lexicographical order based on r and s -inductive rev_lex : @psigma α (λ a, β) → @psigma α (λ a, β) → Prop -| left : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → rev_lex ⟨a₁, b⟩ ⟨a₂, b⟩ -| right : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → rev_lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ -end - -section -open well_founded -parameters {α : Sort u} {β : Sort v} -parameters {r : α → α → Prop} {s : β → β → Prop} -local infix `≺`:50 := rev_lex r s - -def rev_lex_accessible {b} (acb : acc s b) (aca : ∀ a, acc r a): ∀ a, acc (rev_lex r s) ⟨a, b⟩ := -acc.rec_on acb - (λ xb acb (ihb : ∀ y, s y xb → ∀ a, acc (rev_lex r s) ⟨a, y⟩), - λ a, acc.rec_on (aca a) - (λ xa aca (iha : ∀ y, r y xa → acc (rev_lex r s) (mk y xb)), - acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), - have aux : xa = xa → xb = xb → acc (rev_lex r s) p, from - @rev_lex.rec_on α β r s (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁) - p ⟨xa, xb⟩ lt - (λ a₁ a₂ b (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb), - show acc (rev_lex r s) ⟨a₁, b⟩, from - have r₁ : r a₁ xa, from eq.rec_on eq₂ h, - have aux : acc (rev_lex r s) ⟨a₁, xb⟩, from iha a₁ r₁, - eq.rec_on (eq.symm eq₃) aux) - (λ a₁ b₁ a₂ b₂ (h : s b₁ b₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), - show acc (rev_lex r s) (mk a₁ b₁), from - have s₁ : s b₁ xb, from eq.rec_on eq₃ h, - ihb b₁ s₁ a₁), - aux rfl rfl))) - -def rev_lex_wf (ha : well_founded r) (hb : well_founded s) : well_founded (rev_lex r s) := -well_founded.intro $ λ ⟨a, b⟩, rev_lex_accessible (apply hb b) (well_founded.apply ha) a -end - -section - def skip_left (α : Type u) {β : Type v} (s : β → β → Prop) : @psigma α (λ a, β) → @psigma α (λ a, β) → Prop := - rev_lex empty_relation s - - def skip_left_wf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : well_founded s) : well_founded (skip_left α s) := - rev_lex_wf empty_wf hb - - def mk_skip_left {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} - (a₁ a₂ : α) (h : s b₁ b₂) : skip_left α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ := - rev_lex.right _ _ _ h -end - -instance has_well_founded {α : Type u} {β : α → Type v} [s₁ : has_well_founded α] [s₂ : ∀ a, has_well_founded (β a)] : has_well_founded (psigma β) := -{r := lex s₁.r (λ a, (s₂ a).r), wf := lex_wf s₁.wf (λ a, (s₂ a).wf)} - -end psigma diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean index 68c02ef5f9..3bf098eacf 100644 --- a/library/init/meta/well_founded_tactics.lean +++ b/library/init/meta/well_founded_tactics.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.meta init.data.sigma.lex +import init.meta /-- Argument for using_well_founded diff --git a/library/init/wf.lean b/library/init/wf.lean index 682ff313dd..7e7c53a200 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -35,10 +35,10 @@ local infix `≺`:50 := r parameter hwf : well_founded r -lemma recursion {C : α → Sort v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := +theorem recursion {C : α → Sort v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih) -lemma induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := +theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := recursion a h variable {C : α → Sort v} @@ -47,7 +47,7 @@ variable F : Π x, (Π y, y ≺ x → C y) → C x def fix_F (x : α) (a : acc r x) : C x := acc.rec_on a (λ x₁ ac₁ ih, F x₁ ih) -lemma fix_F_eq (x : α) (acx : acc r x) : +theorem fix_F_eq (x : α) (acx : acc r x) : fix_F F x acx = F x (λ (y : α) (p : y ≺ x), fix_F F y (acc.inv acx p)) := acc.drec (λ x r ih, rfl) acx end @@ -59,7 +59,7 @@ def fix (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : α fix_F F x (apply hwf x) -- Well-founded fixpoint satisfies fixpoint equation -lemma fix_eq (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : α) : +theorem fix_eq (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : α) : fix hwf F x = F x (λ y h, fix hwf F y) := fix_F_eq F x (apply hwf x) end well_founded @@ -74,54 +74,54 @@ well_founded.intro (λ (a : α), -- Subrelation of a well-founded relation is well-founded namespace subrelation section - parameters {α : Sort u} {r Q : α → α → Prop} - parameters (h₁ : subrelation Q r) - parameters (h₂ : well_founded r) +parameters {α : Sort u} {r Q : α → α → Prop} +parameters (h₁ : subrelation Q r) +parameters (h₂ : well_founded r) - def accessible {a : α} (ac : acc r a) : acc Q a := - acc.rec_on ac (λ x ax ih, - acc.intro x (λ (y : α) (lt : Q y x), ih y (h₁ lt))) +def accessible {a : α} (ac : acc r a) : acc Q a := +acc.rec_on ac (λ x ax ih, + acc.intro x (λ (y : α) (lt : Q y x), ih y (h₁ lt))) - def wf : well_founded Q := - ⟨λ a, accessible (apply h₂ a)⟩ +def wf : well_founded Q := +⟨λ a, accessible (apply h₂ a)⟩ end end subrelation -- The inverse image of a well-founded relation is well-founded namespace inv_image section - parameters {α : Sort u} {β : Sort v} {r : β → β → Prop} - parameters (f : α → β) - parameters (h : well_founded r) +parameters {α : Sort u} {β : Sort v} {r : β → β → Prop} +parameters (f : α → β) +parameters (h : well_founded r) - private def acc_aux {b : β} (ac : acc r b) : ∀ (x : α), f x = b → acc (inv_image r f) x := - acc.rec_on ac (λ x acx ih z e, - acc.intro z (λ y lt, eq.rec_on e (λ acx ih, ih (f y) lt y rfl) acx ih)) +private def acc_aux {b : β} (ac : acc r b) : ∀ (x : α), f x = b → acc (inv_image r f) x := +acc.rec_on ac (λ x acx ih z e, + acc.intro z (λ y lt, eq.rec_on e (λ acx ih, ih (f y) lt y rfl) acx ih)) - def accessible {a : α} (ac : acc r (f a)) : acc (inv_image r f) a := - acc_aux ac a rfl +def accessible {a : α} (ac : acc r (f a)) : acc (inv_image r f) a := +acc_aux ac a rfl - def wf : well_founded (inv_image r f) := - ⟨λ a, accessible (apply h (f a))⟩ +def wf : well_founded (inv_image r f) := +⟨λ a, accessible (apply h (f a))⟩ end end inv_image -- The transitive closure of a well-founded relation is well-founded namespace tc section - parameters {α : Sort u} {r : α → α → Prop} - local notation `r⁺` := tc r +parameters {α : Sort u} {r : α → α → Prop} +local notation `r⁺` := tc r - def accessible {z : α} (ac : acc r z) : acc (tc r) z := - acc.rec_on ac (λ x acx ih, - acc.intro x (λ y rel, - tc.rec_on rel - (λ a b rab acx ih, ih a rab) - (λ a b c rab rbc ih₁ ih₂ acx ih, acc.inv (ih₂ acx ih) rab) - acx ih)) +def accessible {z : α} (ac : acc r z) : acc (tc r) z := +acc.rec_on ac (λ x acx ih, + acc.intro x (λ y rel, + tc.rec_on rel + (λ a b rab acx ih, ih a rab) + (λ a b c rab rbc ih₁ ih₂ acx ih, acc.inv (ih₂ acx ih) rab) + acx ih)) - def wf (h : well_founded r) : well_founded r⁺ := - ⟨λ a, accessible (apply h a)⟩ +def wf (h : well_founded r) : well_founded r⁺ := +⟨λ a, accessible (apply h a)⟩ end end tc @@ -152,50 +152,170 @@ namespace prod open well_founded section - variables {α : Type u} {β : Type v} - variable (ra : α → α → Prop) - variable (rb : β → β → Prop) +variables {α : Type u} {β : Type v} +variable (ra : α → α → Prop) +variable (rb : β → β → Prop) - -- Lexicographical order based on ra and rb - inductive lex : α × β → α × β → Prop - | left {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : lex (a₁, b₁) (a₂, b₂) - | right (a) {b₁ b₂} (h : rb b₁ b₂) : lex (a, b₁) (a, b₂) +-- Lexicographical order based on ra and rb +inductive lex : α × β → α × β → Prop +| left {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : lex (a₁, b₁) (a₂, b₂) +| right (a) {b₁ b₂} (h : rb b₁ b₂) : lex (a, b₁) (a, b₂) - -- relational product based on ra and rb - inductive rprod : α × β → α × β → Prop - | intro {a₁ b₁ a₂ b₂} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : rprod (a₁, b₁) (a₂, b₂) - end +-- relational product based on ra and rb +inductive rprod : α × β → α × β → Prop +| intro {a₁ b₁ a₂ b₂} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : rprod (a₁, b₁) (a₂, b₂) +end - section - parameters {α : Type u} {β : Type v} - parameters {ra : α → α → Prop} {rb : β → β → Prop} - local infix `≺`:50 := lex ra rb +section +parameters {α : Type u} {β : Type v} +parameters {ra : α → α → Prop} {rb : β → β → Prop} +local infix `≺`:50 := lex ra rb - def 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 b, - acc.rec_on (acb b) (λ xb acb ihb, - acc.intro (xa, xb) (λ p lt, - have aux : xa = xa → xb = xb → acc (lex ra rb) p, from - @prod.lex.rec_on α β ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁) - p (xa, xb) lt - (λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁) - (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂.symm (ihb b₁ (eq.rec_on eq₃ h))), - aux rfl rfl))) +def 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 b, + acc.rec_on (acb b) (λ xb acb ihb, + acc.intro (xa, xb) (λ p lt, + have aux : xa = xa → xb = xb → acc (lex ra rb) p, from + @prod.lex.rec_on α β ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁) + p (xa, xb) lt + (λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁) + (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂.symm (ihb b₁ (eq.rec_on eq₃ h))), + aux rfl rfl))) - -- The lexicographical order of well founded relations is well-founded - def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := - ⟨λ p, cases_on p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩ +-- The lexicographical order of well founded relations is well-founded +def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := +⟨λ p, cases_on p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩ - -- relational product is a subrelation of the lex - def 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 b₁ b₂ h₁) +-- relational product is a subrelation of the lex +def 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 b₁ b₂ h₁) - -- The relational product of well founded relations is well-founded - def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) := - subrelation.wf (rprod_sub_lex) (lex_wf ha hb) +-- The relational product of well founded relations is well-founded +def 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 instance has_well_founded {α : Type u} {β : Type v} [s₁ : has_well_founded α] [s₂ : has_well_founded β] : has_well_founded (α × β) := {r := lex s₁.r s₂.r, wf := lex_wf s₁.wf s₂.wf} end prod + +namespace psigma +section +variables {α : Sort u} {β : α → Sort v} +variable (r : α → α → Prop) +variable (s : ∀ a, β a → β a → Prop) + +-- Lexicographical order based on r and s +inductive lex : psigma β → psigma β → Prop +| left : ∀ {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ +| right : ∀ (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → lex ⟨a, b₁⟩ ⟨a, b₂⟩ +end + +section +parameters {α : Sort u} {β : α → Sort v} +parameters {r : α → α → Prop} {s : Π a : α, β a → β a → Prop} +local infix `≺`:50 := lex r s + +def lex_accessible {a} (aca : acc r a) (acb : ∀ a, well_founded (s a)) + : ∀ (b : β a), acc (lex r s) ⟨a, b⟩ := +acc.rec_on aca + (λ xa aca (iha : ∀ y, r y xa → ∀ b : β y, acc (lex r s) ⟨y, b⟩), + λ b : β xa, acc.rec_on (well_founded.apply (acb xa) b) + (λ xb acb + (ihb : ∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩), + acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), + have aux : xa = xa → xb == xb → acc (lex r s) p, from + @psigma.lex.rec_on α β r s (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁) + p ⟨xa, xb⟩ lt + (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb), + have aux : (∀ (y : α), r y xa → ∀ (b : β y), acc (lex r s) ⟨y, b⟩) → + r a₁ a₂ → ∀ (b₁ : β a₁), acc (lex r s) ⟨a₁, b₁⟩, + from eq.subst eq₂ (λ iha h b₁, iha a₁ h b₁), + aux iha h b₁) + (λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb), + have aux : ∀ (xb : β xa), (∀ (y : β xa), s xa y xb → acc (s xa) y) → + (∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩) → + lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ == xb → acc (lex r s) ⟨a, b₁⟩, + from eq.subst eq₂ (λ xb acb ihb lt b₁ h eq₃, + have new_eq₃ : b₂ = xb, from eq_of_heq eq₃, + have aux : (∀ (y : β a), s a y xb → acc (lex r s) ⟨a, y⟩) → + ∀ (b₁ : β a), s a b₁ b₂ → acc (lex r s) ⟨a, b₁⟩, + from eq.subst new_eq₃ (λ ihb b₁ h, ihb b₁ h), + aux ihb b₁ h), + aux xb acb ihb lt b₁ h eq₃), + aux rfl (heq.refl xb)))) + +-- The lexicographical order of well founded relations is well-founded +def lex_wf (ha : well_founded r) (hb : ∀ x, well_founded (s x)) : well_founded (lex r s) := +well_founded.intro $ λ ⟨a, b⟩, lex_accessible (well_founded.apply ha a) hb b +end + +section +parameters {α : Sort u} {β : Sort v} + +def lex_ndep (r : α → α → Prop) (s : β → β → Prop) := +lex r (λ a : α, s) + +def lex_ndep_wf {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) + : well_founded (lex_ndep r s) := +well_founded.intro $ λ ⟨a, b⟩, lex_accessible (well_founded.apply ha a) (λ x, hb) b +end + +section +variables {α : Sort u} {β : Sort v} +variable (r : α → α → Prop) +variable (s : β → β → Prop) + +-- Reverse lexicographical order based on r and s +inductive rev_lex : @psigma α (λ a, β) → @psigma α (λ a, β) → Prop +| left : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → rev_lex ⟨a₁, b⟩ ⟨a₂, b⟩ +| right : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → rev_lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ +end + +section +open well_founded +parameters {α : Sort u} {β : Sort v} +parameters {r : α → α → Prop} {s : β → β → Prop} +local infix `≺`:50 := rev_lex r s + +def rev_lex_accessible {b} (acb : acc s b) (aca : ∀ a, acc r a): ∀ a, acc (rev_lex r s) ⟨a, b⟩ := +acc.rec_on acb + (λ xb acb (ihb : ∀ y, s y xb → ∀ a, acc (rev_lex r s) ⟨a, y⟩), + λ a, acc.rec_on (aca a) + (λ xa aca (iha : ∀ y, r y xa → acc (rev_lex r s) (mk y xb)), + acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), + have aux : xa = xa → xb = xb → acc (rev_lex r s) p, from + @rev_lex.rec_on α β r s (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁) + p ⟨xa, xb⟩ lt + (λ a₁ a₂ b (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb), + show acc (rev_lex r s) ⟨a₁, b⟩, from + have r₁ : r a₁ xa, from eq.rec_on eq₂ h, + have aux : acc (rev_lex r s) ⟨a₁, xb⟩, from iha a₁ r₁, + eq.rec_on (eq.symm eq₃) aux) + (λ a₁ b₁ a₂ b₂ (h : s b₁ b₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), + show acc (rev_lex r s) (mk a₁ b₁), from + have s₁ : s b₁ xb, from eq.rec_on eq₃ h, + ihb b₁ s₁ a₁), + aux rfl rfl))) + +def rev_lex_wf (ha : well_founded r) (hb : well_founded s) : well_founded (rev_lex r s) := +well_founded.intro $ λ ⟨a, b⟩, rev_lex_accessible (apply hb b) (well_founded.apply ha) a +end + +section +def skip_left (α : Type u) {β : Type v} (s : β → β → Prop) : @psigma α (λ a, β) → @psigma α (λ a, β) → Prop := +rev_lex empty_relation s + +def skip_left_wf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : well_founded s) : well_founded (skip_left α s) := +rev_lex_wf empty_wf hb + +def mk_skip_left {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} + (a₁ a₂ : α) (h : s b₁ b₂) : skip_left α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ := +rev_lex.right _ _ _ h +end + +instance has_well_founded {α : Type u} {β : α → Type v} [s₁ : has_well_founded α] [s₂ : ∀ a, has_well_founded (β a)] : has_well_founded (psigma β) := +{r := lex s₁.r (λ a, (s₂ a).r), wf := lex_wf s₁.wf (λ a, (s₂ a).wf)} + +end psigma