@[implemented_by _private.Init.WFExtrinsicFix.0.WellFounded.opaqueFix]

def WellFounded.extrinsicFix {α : Sort u_1} {C : α → Sort u_2} [∀ (a : α), Nonempty (C a)] (R : α → α → Prop) (F : (a : α) → ((a' : α) → R a' a → C a') → C a) (a : α) : C a

A fixpoint combinator that allows for deferred proofs of termination.

extrinsicFix R F is function implemented as the loop extrinsicFix R F a = F a (fun a _ => extrinsicFix R F a).

If the loop can be shown to be well-founded, extrinsicFix_eq_apply proves that it satisfies the fixpoint equation. Otherwise, extrinsicFix R F is opaque, i.e., it is impossible to prove nontrivial properties about it.

Equations

• WellFounded.extrinsicFix R F a = if h : WellFounded R then h.fix F a else WellFounded.opaqueFix✝ R F a

theorem WellFounded.extrinsicFix_eq_fix {α : Sort u_2} {C : α → Sort u_1} [∀ (a : α), Nonempty (C a)] {R : α → α → Prop} {F : (a : α) → ((a' : α) → R a' a → C a') → C a} (wf : WellFounded R) {a : α} : extrinsicFix R F a = wf.fix F a

theorem WellFounded.extrinsicFix_eq_apply {α : Sort u_2} {C : α → Sort u_1} [∀ (a : α), Nonempty (C a)] {R : α → α → Prop} {F : (a : α) → ((a' : α) → R a' a → C a') → C a} (h : WellFounded R) {a : α} : extrinsicFix R F a = F a fun (a_1 : α) (x : R a_1 a) => extrinsicFix R F a_1

@[implemented_by _private.Init.WFExtrinsicFix.0.WellFounded.opaqueFix₂]

def WellFounded.extrinsicFix₂ {α : Sort u_1} {β : α → Sort u_2} {C₂ : (a : α) → β a → Sort u_3} [∀ (a : α) (b : β a), Nonempty (C₂ a b)] (R : (a : α) ×' β a → (a : α) ×' β a → Prop) (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) (a : α) (b : β a) : C₂ a b

A fixpoint combinator that allows for deferred proofs of termination.

extrinsicFix₂ R F is function implemented as the loop extrinsicFix₂ R F a b = F a b (fun a' b' _ => extrinsicFix₂ R F a' b').

If the loop can be shown to be well-founded, extrinsicFix₂_eq_apply proves that it satisfies the fixpoint equation. Otherwise, extrinsicFix₂ R F is opaque, i.e., it is impossible to prove nontrivial properties about it.

Equations

• One or more equations did not get rendered due to their size.

theorem WellFounded.extrinsicFix₂_eq_fix {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [∀ (a : α) (b : β a), Nonempty (C₂ a b)] {R : (a : α) ×' β a → (a : α) ×' β a → Prop} {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} (wf : WellFounded R) {a : α} {b : β a} : extrinsicFix₂ R F a b = wf.fix (fun (x : (a : α) ×' β a) (G : (y : (a : α) ×' β a) → R y x → C₂ y.fst y.snd) => F x.fst x.snd fun (a : α) (b : β a) (h : R ⟨a, b⟩ ⟨x.fst, x.snd⟩) => G ⟨a, b⟩ h) ⟨a, b⟩

theorem WellFounded.extrinsicFix₂_eq_apply {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [∀ (a : α) (b : β a), Nonempty (C₂ a b)] {R : (a : α) ×' β a → (a : α) ×' β a → Prop} {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} (wf : WellFounded R) {a : α} {b : β a} : extrinsicFix₂ R F a b = F a b fun (a' : α) (b' : β a') (x : R ⟨a', b'⟩ ⟨a, b⟩) => extrinsicFix₂ R F a' b'

@[specialize #[]]

partial def WellFounded.opaqueFix₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4} [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop) (F : (a : α) → (b : β a) → (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c) (a : α) (b : β a) (c : γ a b) : C₃ a b c

The function implemented as the loop opaqueFix₃ R F a b c = F a b c (fun a' b' c' _ => opaqueFix₃ R F a' b' c'). opaqueFix₃ R F is the fixpoint of the functional F, as long as the loop is well-founded.

The loop might run forever depending on F. It is opaque, i.e., it is impossible to prove nontrivial properties about it.

@[implemented_by WellFounded.opaqueFix₃]

def WellFounded.extrinsicFix₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4} [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop) (F : (a : α) → (b : β a) → (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c) (a : α) (b : β a) (c : γ a b) : C₃ a b c

A fixpoint combinator that allows for deferred proofs of termination.

extrinsicFix₃ R F is function implemented as the loop extrinsicFix₃ R F a b c = F a b c (fun a b c _ => extrinsicFix₃ R F a b c).

If the loop can be shown to be well-founded, extrinsicFix₃_eq_apply proves that it satisfies the fixpoint equation. Otherwise, extrinsicFix₃ R F is opaque, i.e., it is impossible to prove nontrivial properties about it.

Equations

• One or more equations did not get rendered due to their size.

theorem WellFounded.extrinsicFix₃_eq_fix {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1} [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop} {F : (a : α) → (b : β a) → (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c} (wf : WellFounded R) {a : α} {b : β a} {c : γ a b} : extrinsicFix₃ R F a b c = wf.fix (fun (x : (a : α) ×' (b : β a) ×' γ a b) (G : (y : (a : α) ×' (b : β a) ×' γ a b) → R y x → C₃ y.fst y.snd.fst y.snd.snd) => F x.fst x.snd.fst x.snd.snd fun (a : α) (b : β a) (c : γ a b) (h : R ⟨a, ⟨b, c⟩⟩ ⟨x.fst, ⟨x.snd.fst, x.snd.snd⟩⟩) => G ⟨a, ⟨b, c⟩⟩ h) ⟨a, ⟨b, c⟩⟩

theorem WellFounded.extrinsicFix₃_eq_apply {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1} [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop} {F : (a : α) → (b : β a) → (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c} (wf : WellFounded R) {a : α} {b : β a} {c : γ a b} : extrinsicFix₃ R F a b c = F a b c fun (a_1 : α) (b_1 : β a_1) (c_1 : γ a_1 b_1) (x : R ⟨a_1, ⟨b_1, c_1⟩⟩ ⟨a, ⟨b, c⟩⟩) => extrinsicFix₃ R F a_1 b_1 c_1