@[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

theorem WellFounded.extrinsicFix_invImage {α : Sort u_3} {C : α → Sort u_2} {α' : Sort u_1} [∀ (a : α), Nonempty (C a)] (R : α → α → Prop) (f : α' → α) (F : (a : α) → ((a' : α) → R a' a → C a') → C a) (F' : (a : α') → ((a' : α') → R (f a') (f a) → C (f a')) → C (f a)) (h : ∀ (a : α') (r : (a' : α) → R a' (f a) → C a'), F (f a) r = F' a fun (a' : α') (hR : R (f a') (f a)) => r (f a') hR) (a : α') : WellFounded R → extrinsicFix (InvImage R f) F' a = extrinsicFix R F (f a)

@[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

@[inline]

def WellFounded.partialExtrinsicFix {α : 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 can be used to construct recursive functions with an extrinsic, partial proof of termination.

Given a relation R and a fixpoint functional F which must be decreasing with respect to R, partialExtrinsicFix R F is the recursive function obtained by having F call itself recursively.

For each input a, partialExtrinsicFix R F a can be verified given a partial termination proof. The precise semantics are as follows.

If Acc R a does not hold, partialExtrinsicFix R F a might run forever. In this case, nothing interesting can be proved about the recursive function; it is opaque and behaves like a recursive function with the partial modifier.

If Acc R a does hold, partialExtrinsicFix R F a is equivalent to F a (fun a' _ => partialExtrinsicFix R F a'), both logically and regarding its termination behavior.

In particular, if R is well-founded, partialExtrinsicFix R F a is equivalent to WellFounded.fix _ F.

Equations

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

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

theorem WellFounded.partialExtrinsicFix_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} {a : α} (wf : WellFounded R) : partialExtrinsicFix R F a = F a fun (a' : α) (x : R a' a) => partialExtrinsicFix R F a'

theorem WellFounded.partialExtrinsicFix_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 : α} : partialExtrinsicFix R F a = wf.fix F a

@[inline]

def WellFounded.partialExtrinsicFix₂ {α : 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 2-ary fixpoint combinator that can be used to construct recursive functions with an extrinsic, partial proof of termination.

Given a relation R and a fixpoint functional F which must be decreasing with respect to R, partialExtrinsicFix₂ R F is the recursive function obtained by having F call itself recursively.

For each pair of inputs a and b, partialExtrinsicFix₂ R F a b can be verified given a partial termination proof. The precise semantics are as follows.

If Acc R ⟨a, b⟩ does not hold, partialExtrinsicFix₂ R F a b might run forever. In this case, nothing interesting can be proved about the recursive function; it is opaque and behaves like a recursive function with the partial modifier.

If Acc R ⟨a, b⟩ does hold, partialExtrinsicFix₂ R F a b is equivalent to F a b (fun a' b' _ => partialExtrinsicFix₂ R F a' b'), both logically and regarding its termination behavior.

In particular, if R is well-founded, partialExtrinsicFix₂ R F a b is equivalent to a well-foundesd fixpoint.

Equations

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

theorem WellFounded.partialExtrinsicFix₂_eq_partialExtrinsicFix {α : 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} {a : α} {b : β a} (h : Acc R ⟨a, b⟩) : partialExtrinsicFix₂ R F a b = partialExtrinsicFix R (fun (p : PSigma β) (r : (a' : PSigma β) → R a' p → (fun (a : PSigma β) => C₂ a.fst a.snd) a') => F p.fst p.snd fun (a' : α) (b' : β a') (hR : R ⟨a', b'⟩ ⟨p.fst, p.snd⟩) => r ⟨a', b'⟩ hR) ⟨a, b⟩

theorem WellFounded.partialExtrinsicFix₂_eq_apply_of_acc {α : 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} {a : α} {b : β a} (wf : Acc R ⟨a, b⟩) : partialExtrinsicFix₂ R F a b = F a b fun (a' : α) (b' : β a') (x : R ⟨a', b'⟩ ⟨a, b⟩) => partialExtrinsicFix₂ R F a' b'

theorem WellFounded.partialExtrinsicFix₂_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} {a : α} {b : β a} (wf : WellFounded R) : partialExtrinsicFix₂ R F a b = F a b fun (a' : α) (b' : β a') (x : R ⟨a', b'⟩ ⟨a, b⟩) => partialExtrinsicFix₂ R F a' b'

theorem WellFounded.partialExtrinsicFix₂_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} : partialExtrinsicFix₂ 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⟩

@[inline]

def WellFounded.partialExtrinsicFix₃ {α : 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 3-ary fixpoint combinator that can be used to construct recursive functions with an extrinsic, partial proof of termination.

Given a relation R and a fixpoint functional F which must be decreasing with respect to R, partialExtrinsicFix₃ R F is the recursive function obtained by having F call itself recursively.

For each pair of inputs a, b and c, partialExtrinsicFix₃ R F a b can be verified given a partial termination proof. The precise semantics are as follows.

If Acc R ⟨a, b, c⟩ does not hold, partialExtrinsicFix₃ R F a b might run forever. In this case, nothing interesting can be proved about the recursive function; it is opaque and behaves like a recursive function with the partial modifier.

If Acc R ⟨a, b, c⟩ does hold, partialExtrinsicFix₃ R F a b is equivalent to F a b c (fun a' b' c' _ => partialExtrinsicFix₃ R F a' b' c'), both logically and regarding its termination behavior.

In particular, if R is well-founded, partialExtrinsicFix₃ R F a b c is equivalent to a well-foundesd fixpoint.

Equations

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

theorem WellFounded.partialExtrinsicFix₃_eq_partialExtrinsicFix {α : 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} {a : α} {b : β a} {c : γ a b} (h : Acc R ⟨a, ⟨b, c⟩⟩) : partialExtrinsicFix₃ R F a b c = partialExtrinsicFix R (fun (p : (a : α) ×' (b : β a) ×' γ a b) (r : (a' : (a : α) ×' (b : β a) ×' γ a b) → R a' p → (fun (a : (a : α) ×' (b : β a) ×' γ a b) => C₃ a.fst a.snd.fst a.snd.snd) a') => F p.fst p.snd.fst p.snd.snd fun (a' : α) (b' : β a') (c' : γ a' b') (hR : R ⟨a', ⟨b', c'⟩⟩ ⟨p.fst, ⟨p.snd.fst, p.snd.snd⟩⟩) => r ⟨a', ⟨b', c'⟩⟩ hR) ⟨a, ⟨b, c⟩⟩

theorem WellFounded.partialExtrinsicFix₃_eq_apply_of_acc {α : 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} {a : α} {b : β a} {c : γ a b} (wf : Acc R ⟨a, ⟨b, c⟩⟩) : partialExtrinsicFix₃ 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⟩⟩) => partialExtrinsicFix₃ R F a_1 b_1 c_1

theorem WellFounded.partialExtrinsicFix₃_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} {a : α} {b : β a} {c : γ a b} (wf : WellFounded R) : partialExtrinsicFix₃ 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⟩⟩) => partialExtrinsicFix₃ R F a_1 b_1 c_1

theorem WellFounded.partialExtrinsicFix₃_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} : partialExtrinsicFix₃ 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⟩⟩