Init.WF

inductive Acc {α : Sort u} (r : α → α → Prop) :

α → Prop

intro: ∀ {α : Sort u} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x

@[inline]

abbrev Acc.ndrec {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a) :

C a

Equations

Acc.ndrec m n = Acc.rec m n

source

@[inline]

abbrev Acc.ndrecOn {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) :

C a

Equations

Acc.ndrecOn n m = Acc.rec m n

source

noncomputable def Acc.inv {α : Sort u} {r : α → α → Prop} {x : α} {y : α} (h₁ : Acc r x) (h₂ : r y x) :

Acc r y

Equations

@Acc.inv = @Acc.inv.proof_1

source

inductive WellFounded {α : Sort u} (r : α → α → Prop) :

Prop

intro: ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r

source

class WellFoundedRelation (α : Sort u) :

Sort (max 1 u)

rel : α → α → Prop
wf : WellFounded rel

Instances

source

noncomputable def WellFounded.apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) :

Acc r a

Equations

@WellFounded.apply = @WellFounded.apply.proof_1

source

theorem WellFounded.recursion {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (a : α) (h : (x : α) → ((y : α) → r y x → C y) → C x) :

C a

source

theorem WellFounded.induction {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Prop} (a : α) (h : (x : α) → ((y : α) → r y x → C y) → C x) :

C a

source

noncomputable def WellFounded.fixF {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x) :

C x

Equations

WellFounded.fixF F x a = Acc.rec (fun x₁ h ih => F x₁ ih) a

source

noncomputable def WellFounded.fixFEq {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (acx : Acc r x) :

WellFounded.fixF F x acx = F x fun y p => WellFounded.fixF F y (_ : Acc (fun y x => r y x) y)

Equations

@WellFounded.fixFEq = @WellFounded.fixFEq.proof_1

source

noncomputable def WellFounded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) :

C x

Equations

WellFounded.fix hwf F x = WellFounded.fixF F x (_ : Acc r x)

source

theorem WellFounded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) :

WellFounded.fix hwf F x = F x fun y x => WellFounded.fix hwf F y

source

def emptyWf {α : Sort u} :

WellFoundedRelation α

Equations

emptyWf = { rel := emptyRelation, wf := (_ : WellFounded emptyRelation) }

source

noncomputable def Subrelation.accessible {α : Sort u} {r : α → α → Prop} {q : α → α → Prop} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :

Acc q a

Equations

@Subrelation.accessible = @Subrelation.accessible.proof_1

source

noncomputable def Subrelation.wf {α : Sort u} {r : α → α → Prop} {q : α → α → Prop} (h₁ : Subrelation q r) (h₂ : WellFounded r) :

WellFounded q

Equations

@Subrelation.wf = @Subrelation.wf.proof_1

source

noncomputable def InvImage.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} {a : α} (f : α → β) (ac : Acc r (f a)) :

Acc (InvImage r f) a

Equations

@InvImage.accessible = @InvImage.accessible.proof_1

source

noncomputable def InvImage.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) (h : WellFounded r) :

WellFounded (InvImage r f)

Equations

@InvImage.wf = @InvImage.wf.proof_1

source

def invImage {α : Sort u_1} {β : Sort u_2} (f : α → β) (h : WellFoundedRelation β) :

WellFoundedRelation α

Equations

invImage f h = { rel := InvImage WellFoundedRelation.rel f, wf := (_ : WellFounded (InvImage WellFoundedRelation.rel f)) }

source

noncomputable def TC.accessible {α : Sort u} {r : α → α → Prop} {z : α} (ac : Acc r z) :

Acc (TC r) z

Equations

@TC.accessible = @TC.accessible.proof_1

source

noncomputable def TC.wf {α : Sort u} {r : α → α → Prop} (h : WellFounded r) :

WellFounded (TC r)

Equations

@TC.wf = @TC.wf.proof_1

source

def Nat.lt_wfRel :

WellFoundedRelation Nat

Equations

Nat.lt_wfRel = { rel := Nat.lt, wf := Nat.lt_wfRel.proof_1 }

source

theorem Nat.strongInductionOn {motive : Nat → Sort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) :

motive n

source

theorem Nat.caseStrongInductionOn {motive : Nat → Sort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m ≤ n → motive m) → motive (Nat.succ n)) :

motive a

source

noncomputable def Measure {α : Sort u} :

(α → Nat) → α → α → Prop

Equations

Measure = InvImage fun a b => a < b

source

@[inline]

abbrev measure {α : Sort u} (f : α → Nat) :

WellFoundedRelation α

Equations

measure f = invImage f Nat.lt_wfRel

source

noncomputable def SizeOfRef (α : Sort u) [inst : SizeOf α] :

α → α → Prop

Equations

SizeOfRef α = Measure sizeOf

source

@[inline]

abbrev sizeOfWFRel {α : Sort u} [inst : SizeOf α] :

WellFoundedRelation α

Equations

sizeOfWFRel = measure sizeOf

source

instance instWellFoundedRelation {α : Sort u_1} [inst : SizeOf α] :

WellFoundedRelation α

Equations

instWellFoundedRelation = sizeOfWFRel

source

inductive Prod.Lex {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) :

α × β → α × β → Prop

left: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β), ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
right: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β}, rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)

source

noncomputable def Prod.Lex.right' {β : Type v} (rb : β → β → Prop) {a₂ : Nat} {b₂ : β} {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) :

Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)

Equations

@Prod.Lex.right' = @Prod.Lex.right'.proof_1

source

inductive Prod.RProd {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) :

α × β → α × β → Prop

intro: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, ra a₁ a₂ → rb b₁ b₂ → Prod.RProd ra rb (a₁, b₁) (a₂, b₂)

source

noncomputable def Prod.lexAccessible {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (aca : ∀ (a : α), Acc ra a) (acb : ∀ (b : β), Acc rb b) (a : α) (b : β) :

Acc (Prod.Lex ra rb) (a, b)

Equations

@Prod.lexAccessible = @Prod.lexAccessible.proof_1

source

def Prod.lex {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :

WellFoundedRelation (α × β)

Equations

Prod.lex ha hb = { rel := Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel, wf := (_ : WellFounded (Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel)) }

source

instance Prod.instWellFoundedRelationProd {α : Type u} {β : Type v} [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] :

WellFoundedRelation (α × β)

Equations

Prod.instWellFoundedRelationProd = Prod.lex ha hb

source

noncomputable def Prod.RProdSubLex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α × β) (b : α × β) (h : Prod.RProd ra rb a b) :

Prod.Lex ra rb a b

Equations

@Prod.RProdSubLex = @Prod.RProdSubLex.proof_1

source

def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :

WellFoundedRelation (α × β)

Equations

Prod.rprod ha hb = { rel := Prod.RProd WellFoundedRelation.rel WellFoundedRelation.rel, wf := (_ : WellFounded (Prod.RProd WellFoundedRelation.rel WellFoundedRelation.rel)) }

source

inductive PSigma.Lex {α : Sort u} {β : α → Sort v} (r : α → α → Prop) (s : (a : α) → β a → β a → Prop) :

PSigma β → PSigma β → Prop

left: ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → PSigma.Lex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
right: ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → PSigma.Lex r s { fst := a, snd := b₁ } { fst := a, snd := b₂ }

source

noncomputable def PSigma.lexAccessible {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) :

Acc (PSigma.Lex r s) { fst := a, snd := b }

Equations

@PSigma.lexAccessible = @PSigma.lexAccessible.proof_1

source

def PSigma.lex {α : Sort u} {β : α → Sort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) :

WellFoundedRelation (PSigma β)

Equations

PSigma.lex ha hb = { rel := PSigma.Lex WellFoundedRelation.rel fun a => WellFoundedRelation.rel, wf := (_ : WellFounded (PSigma.Lex WellFoundedRelation.rel fun a => WellFoundedRelation.rel)) }

source

instance PSigma.instWellFoundedRelationPSigma {α : Sort u} {β : α → Sort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] :

WellFoundedRelation (PSigma β)

Equations

PSigma.instWellFoundedRelationPSigma = PSigma.lex ha hb

source

noncomputable def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :

(_ : α) ×' β → (_ : α) ×' β → Prop

Equations

PSigma.lexNdep r s = PSigma.Lex r fun x => s

source

noncomputable def PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :

WellFounded (PSigma.lexNdep r s)

Equations

@PSigma.lexNdepWf = @PSigma.lexNdepWf.proof_1

source

inductive PSigma.RevLex {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :

(_ : α) ×' β → (_ : α) ×' β → Prop

left: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β), r a₁ a₂ → PSigma.RevLex r s { fst := a₁, snd := b } { fst := a₂, snd := b }
right: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → PSigma.RevLex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }

source

noncomputable def PSigma.revLexAccessible {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {b : β} (acb : Acc s b) (aca : ∀ (a : α), Acc r a) (a : α) :

Acc (PSigma.RevLex r s) { fst := a, snd := b }

Equations

@PSigma.revLexAccessible = @PSigma.revLexAccessible.proof_1

source

noncomputable def PSigma.revLex {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :

WellFounded (PSigma.RevLex r s)

Equations

@PSigma.revLex = @PSigma.revLex.proof_1

source

noncomputable def PSigma.SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) :

(_ : α) ×' β → (_ : α) ×' β → Prop

Equations

PSigma.SkipLeft α s = PSigma.RevLex emptyRelation s

source

def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) :

WellFoundedRelation ((_ : α) ×' β)

Equations

PSigma.skipLeft α hb = { rel := PSigma.SkipLeft α WellFoundedRelation.rel, wf := (_ : WellFounded (PSigma.RevLex emptyRelation WellFoundedRelation.rel)) }

source

noncomputable def PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {s : β → β → Prop} (a₁ : α) (a₂ : α) (h : s b₁ b₂) :

PSigma.SkipLeft α s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }

Equations

@PSigma.mkSkipLeft = @PSigma.mkSkipLeft.proof_1