mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
feat: enable partial termination proofs about WellFounded.extrinsicFix (#12430)
This PR provides `WellFounded.partialExtrinsicFix`, which makes it possible to implement and verify partially terminating functions, safely building on top of the seemingly less general `extrinsicFix` (which is now called `totalExtrinsicFix`). A proof of termination is only necessary in order to formally verify the behavior of `partialExtrinsicFix`.
This commit is contained in:
Paul Reichert
@@ -30,6 +30,7 @@ variable {α : Sort _} {β : α → Sort _} {γ : (a : α) → β a → Sort _}
|
||||
set_option doc.verso true
|
||||
|
||||
namespace WellFounded
|
||||
open Relation
|
||||
|
||||
/--
|
||||
The function implemented as the loop {lean}`opaqueFix R F a = F a (fun a _ => opaqueFix R F a)`.
|
||||
@@ -85,6 +86,23 @@ public theorem extrinsicFix_eq_apply [∀ a, Nonempty (C a)] {R : α → α →
|
||||
simp only [extrinsicFix, dif_pos h]
|
||||
rw [WellFounded.fix_eq]
|
||||
|
||||
public theorem extrinsicFix_invImage {α' : Sort _} [∀ 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, F (f a) r = F' a fun a' hR => r (f a') hR) (a : α') (h : WellFounded R) :
|
||||
extrinsicFix (C := (C <| f ·)) (InvImage R f) F' a = extrinsicFix (C := C) R F (f a) := by
|
||||
have h' := h
|
||||
rcases h with ⟨h⟩
|
||||
specialize h (f a)
|
||||
have : Acc (InvImage R f) a := InvImage.accessible _ h
|
||||
clear h
|
||||
induction this
|
||||
rename_i ih
|
||||
rw [extrinsicFix_eq_apply, extrinsicFix_eq_apply, h]
|
||||
· congr; ext a x
|
||||
rw [ih _ x]
|
||||
· assumption
|
||||
· exact InvImage.wf _ ‹_›
|
||||
|
||||
/--
|
||||
A fixpoint combinator that allows for deferred proofs of termination.
|
||||
|
||||
@@ -242,4 +260,273 @@ nontrivial properties about it.
|
||||
-/
|
||||
add_decl_doc extrinsicFix₃
|
||||
|
||||
/--
|
||||
A fixpoint combinator that can be used to construct recursive functions with an
|
||||
*extrinsic, partial* proof of termination.
|
||||
|
||||
Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
|
||||
to {name}`R`, {lean}`partialExtrinsicFix R F` is the recursive function obtained by having {name}`F` call
|
||||
itself recursively.
|
||||
|
||||
For each input {given}`a`, {lean}`partialExtrinsicFix R F a` can be verified given a *partial* termination
|
||||
proof. The precise semantics are as follows.
|
||||
|
||||
If {lean}`Acc R a` does not hold, {lean}`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 {lean}`Acc R a` _does_ hold, {lean}`partialExtrinsicFix R F a` is equivalent to
|
||||
{lean}`F a (fun a' _ => partialExtrinsicFix R F a')`, both logically and regarding its termination behavior.
|
||||
|
||||
In particular, if {name}`R` is well-founded, {lean}`partialExtrinsicFix R F a` is equivalent to
|
||||
{lean}`WellFounded.fix _ F`.
|
||||
-/
|
||||
@[inline]
|
||||
public def partialExtrinsicFix [∀ a, Nonempty (C a)] (R : α → α → Prop)
|
||||
(F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a :=
|
||||
extrinsicFix (α := { a' : α // a' = a ∨ TransGen R a' a }) (C := (C ·.1))
|
||||
(fun p q => R p.1 q.1)
|
||||
(fun a recur => F a.1 fun a' hR => recur ⟨a', by
|
||||
rcases a.property with ha | ha
|
||||
· exact Or.inr (TransGen.single (ha ▸ hR))
|
||||
· apply Or.inr
|
||||
apply TransGen.trans ?_ ‹_›
|
||||
apply TransGen.single
|
||||
assumption⟩ ‹_›) ⟨a, Or.inl rfl⟩
|
||||
|
||||
public theorem partialExtrinsicFix_eq_apply_of_acc [∀ 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' _ => partialExtrinsicFix R F a') := by
|
||||
simp only [partialExtrinsicFix]
|
||||
rw [extrinsicFix_eq_apply]
|
||||
congr; ext a' hR
|
||||
let f (x : { x : α // x = a' ∨ TransGen R x a' }) : { x : α // x = a ∨ TransGen R x a } :=
|
||||
⟨x.val, by
|
||||
cases x.property
|
||||
· rename_i h
|
||||
rw [h]
|
||||
exact Or.inr (.single hR)
|
||||
· rename_i h
|
||||
apply Or.inr
|
||||
refine TransGen.trans h ?_
|
||||
exact .single hR⟩
|
||||
have := extrinsicFix_invImage (C := (C ·.val)) (R := (R ·.1 ·.1)) (f := f)
|
||||
(F := fun a r => F a.1 fun a' hR => r ⟨a', Or.inr (by rcases a.2 with ha | ha; exact .single (ha ▸ hR); exact .trans (.single hR) ‹_›)⟩ hR)
|
||||
(F' := fun a r => F a.1 fun a' hR => r ⟨a', by rcases a.2 with ha | ha; exact .inr (.single (ha ▸ hR)); exact .inr (.trans (.single hR) ‹_›)⟩ hR)
|
||||
unfold InvImage at this
|
||||
rw [this]
|
||||
· simp +zetaDelta
|
||||
· constructor
|
||||
intro x
|
||||
refine InvImage.accessible _ ?_
|
||||
cases x.2 <;> rename_i hx
|
||||
· rwa [hx]
|
||||
· exact h.inv_of_transGen hx
|
||||
· constructor
|
||||
intro x
|
||||
refine InvImage.accessible _ ?_
|
||||
cases x.2 <;> rename_i hx
|
||||
· rwa [hx]
|
||||
· exact h.inv_of_transGen hx
|
||||
|
||||
public theorem partialExtrinsicFix_eq_apply [∀ 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' _ => partialExtrinsicFix R F a') :=
|
||||
partialExtrinsicFix_eq_apply_of_acc (wf.apply _)
|
||||
|
||||
public theorem partialExtrinsicFix_eq_fix [∀ 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 := by
|
||||
have h := wf.apply a
|
||||
induction h with | intro a' h ih
|
||||
rw [partialExtrinsicFix_eq_apply_of_acc (Acc.intro _ h), WellFounded.fix_eq]
|
||||
congr 1; ext a'' hR
|
||||
exact ih _ hR
|
||||
|
||||
/--
|
||||
A 2-ary fixpoint combinator that can be used to construct recursive functions with an
|
||||
*extrinsic, partial* proof of termination.
|
||||
|
||||
Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
|
||||
to {name}`R`, {lean}`partialExtrinsicFix₂ R F` is the recursive function obtained by having {name}`F` call
|
||||
itself recursively.
|
||||
|
||||
For each pair of inputs {given}`a` and {given}`b`, {lean}`partialExtrinsicFix₂ R F a b` can be verified
|
||||
given a *partial* termination proof. The precise semantics are as follows.
|
||||
|
||||
If {lean}`Acc R ⟨a, b⟩ ` does not hold, {lean}`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 {lean}`Acc R ⟨a, b⟩` _does_ hold, {lean}`partialExtrinsicFix₂ R F a b` is equivalent to
|
||||
{lean}`F a b (fun a' b' _ => partialExtrinsicFix₂ R F a' b')`, both logically and regarding its
|
||||
termination behavior.
|
||||
|
||||
In particular, if {name}`R` is well-founded, {lean}`partialExtrinsicFix₂ R F a b` is equivalent to
|
||||
a well-foundesd fixpoint.
|
||||
-/
|
||||
@[inline]
|
||||
public def partialExtrinsicFix₂ [∀ a b, 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 :=
|
||||
extrinsicFix₂ (α := α) (β := fun a' => { b' : β a' // (PSigma.mk a' b') = (PSigma.mk a b) ∨ TransGen R ⟨a', b'⟩ ⟨a, b⟩ })
|
||||
(C₂ := (C₂ · ·.1))
|
||||
(fun p q => R ⟨p.1, p.2.1⟩ ⟨q.1, q.2.1⟩)
|
||||
(fun a b recur => F a b.1 fun a' b' hR => recur a' ⟨b', Or.inr (by
|
||||
rcases b.property with hb | hb
|
||||
· exact .single (hb ▸ hR)
|
||||
· apply TransGen.trans ?_ ‹_›
|
||||
apply TransGen.single
|
||||
assumption)⟩ ‹_›) a ⟨b, Or.inl rfl⟩
|
||||
|
||||
public theorem partialExtrinsicFix₂_eq_partialExtrinsicFix [∀ a b, 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 (α := PSigma β) (C := fun a => C₂ a.1 a.2) R (fun p r => F p.1 p.2 fun a' b' hR => r ⟨a', b'⟩ hR) ⟨a, b⟩ := by
|
||||
simp only [partialExtrinsicFix, partialExtrinsicFix₂, extrinsicFix₂]
|
||||
let f (x : ((a' : α) ×' { b' // PSigma.mk a' b' = ⟨a, b⟩ ∨ TransGen R ⟨a', b'⟩ ⟨a, b⟩ })) : { a' // a' = ⟨a, b⟩ ∨ TransGen R a' ⟨a, b⟩ } :=
|
||||
⟨⟨x.1, x.2.1⟩, x.2.2⟩
|
||||
have := extrinsicFix_invImage (C := fun a => C₂ a.1.1 a.1.2) (f := f) (R := (R ·.1 ·.1))
|
||||
(F := fun a r => F a.1.1 a.1.2 fun a' b' hR => r ⟨⟨a', b'⟩, ?refine_a⟩ hR)
|
||||
(F' := fun a r => F a.1 a.2.1 fun a' b' hR => r ⟨a', b', ?refine_b⟩ hR)
|
||||
(a := ⟨a, b, ?refine_c⟩); rotate_left
|
||||
· cases a.2 <;> rename_i heq
|
||||
· rw [heq] at hR
|
||||
exact .inr (.single hR)
|
||||
· exact .inr (.trans (.single hR) heq)
|
||||
· cases a.2.2 <;> rename_i heq
|
||||
· rw [heq] at hR
|
||||
exact .inr (.single hR)
|
||||
· exact .inr (.trans (.single hR) heq)
|
||||
· exact .inl rfl
|
||||
unfold InvImage f at this
|
||||
simp at this
|
||||
rw [this]
|
||||
constructor
|
||||
intro x
|
||||
apply InvImage.accessible
|
||||
cases x.2 <;> rename_i heq
|
||||
· rwa [heq]
|
||||
· exact h.inv_of_transGen heq
|
||||
|
||||
public theorem partialExtrinsicFix₂_eq_apply_of_acc [∀ a b, 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' _ => partialExtrinsicFix₂ R F a' b') := by
|
||||
rw [partialExtrinsicFix₂_eq_partialExtrinsicFix wf, partialExtrinsicFix_eq_apply_of_acc wf]
|
||||
congr 1; ext a' b' hR
|
||||
rw [partialExtrinsicFix₂_eq_partialExtrinsicFix (wf.inv hR)]
|
||||
|
||||
public theorem partialExtrinsicFix₂_eq_apply [∀ a b, 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' _ => partialExtrinsicFix₂ R F a' b') :=
|
||||
partialExtrinsicFix₂_eq_apply_of_acc (wf.apply _)
|
||||
|
||||
public theorem partialExtrinsicFix₂_eq_fix [∀ a b, Nonempty (C₂ a b)]
|
||||
{R : (a : α) ×' β a → (a : α) ×' β a → Prop}
|
||||
{F : ∀ a b, (∀ a' b', R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
|
||||
(wf : WellFounded R) {a b} :
|
||||
partialExtrinsicFix₂ R F a b = wf.fix (fun x G => F x.1 x.2 (fun a b h => G ⟨a, b⟩ h)) ⟨a, b⟩ := by
|
||||
rw [partialExtrinsicFix₂_eq_partialExtrinsicFix (wf.apply _), partialExtrinsicFix_eq_fix wf]
|
||||
|
||||
|
||||
/--
|
||||
A 3-ary fixpoint combinator that can be used to construct recursive functions with an
|
||||
*extrinsic, partial* proof of termination.
|
||||
|
||||
Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
|
||||
to {name}`R`, {lean}`partialExtrinsicFix₃ R F` is the recursive function obtained by having {name}`F` call
|
||||
itself recursively.
|
||||
|
||||
For each pair of inputs {given}`a`, {given}`b` and {given}`c`, {lean}`partialExtrinsicFix₃ R F a b` can be
|
||||
verified given a *partial* termination proof. The precise semantics are as follows.
|
||||
|
||||
If {lean}`Acc R ⟨a, b, c⟩ ` does not hold, {lean}`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 {lean}`Acc R ⟨a, b, c⟩` _does_ hold, {lean}`partialExtrinsicFix₃ R F a b` is equivalent to
|
||||
{lean}`F a b c (fun a' b' c' _ => partialExtrinsicFix₃ R F a' b' c')`, both logically and regarding its
|
||||
termination behavior.
|
||||
|
||||
In particular, if {name}`R` is well-founded, {lean}`partialExtrinsicFix₃ R F a b c` is equivalent to
|
||||
a well-foundesd fixpoint.
|
||||
-/
|
||||
@[inline]
|
||||
public def partialExtrinsicFix₃ [∀ a b c, 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 :=
|
||||
extrinsicFix₃ (α := α) (β := β) (γ := fun a' b' => { c' : γ a' b' // (⟨a', b', c'⟩ : (a : α) ×' (b : β a) ×' γ a b) = ⟨a, b, c⟩ ∨ TransGen R ⟨a', b', c'⟩ ⟨a, b, c⟩ })
|
||||
(C₃ := (C₃ · · ·.1))
|
||||
(fun p q => R ⟨p.1, p.2.1, p.2.2.1⟩ ⟨q.1, q.2.1, q.2.2.1⟩)
|
||||
(fun a b c recur => F a b c.1 fun a' b' c' hR => recur a' b' ⟨c', Or.inr (by
|
||||
rcases c.property with hb | hb
|
||||
· exact .single (hb ▸ hR)
|
||||
· apply TransGen.trans ?_ ‹_›
|
||||
apply TransGen.single
|
||||
assumption)⟩ ‹_›) a b ⟨c, Or.inl rfl⟩
|
||||
|
||||
public theorem partialExtrinsicFix₃_eq_partialExtrinsicFix [∀ a b c, 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 (α := (a : α) ×' (b : β a) ×' γ a b) (C := fun a => C₃ a.1 a.2.1 a.2.2) R (fun p r => F p.1 p.2.1 p.2.2 fun a' b' c' hR => r ⟨a', b', c'⟩ hR) ⟨a, b, c⟩ := by
|
||||
simp only [partialExtrinsicFix, partialExtrinsicFix₃, extrinsicFix₃]
|
||||
let f (x : ((a' : α) ×' (b' : β a') ×' { c' // (⟨a', b', c'⟩ : (a : α) ×' (b : β a) ×' γ a b) = ⟨a, b, c⟩ ∨ TransGen R ⟨a', b', c'⟩ ⟨a, b, c⟩ })) : { a' // a' = ⟨a, b, c⟩ ∨ TransGen R a' ⟨a, b, c⟩ } :=
|
||||
⟨⟨x.1, x.2.1, x.2.2.1⟩, x.2.2.2⟩
|
||||
have := extrinsicFix_invImage (C := fun a => C₃ a.1.1 a.1.2.1 a.1.2.2) (f := f) (R := (R ·.1 ·.1))
|
||||
(F := fun a r => F a.1.1 a.1.2.1 a.1.2.2 fun a' b' c' hR => r ⟨⟨a', b', c'⟩, ?refine_a⟩ hR)
|
||||
(F' := fun a r => F a.1 a.2.1 a.2.2.1 fun a' b' c' hR => r ⟨a', b', c', ?refine_b⟩ hR)
|
||||
(a := ⟨a, b, c, ?refine_c⟩); rotate_left
|
||||
· cases a.2 <;> rename_i heq
|
||||
· rw [heq] at hR
|
||||
exact .inr (.single hR)
|
||||
· exact .inr (.trans (.single hR) heq)
|
||||
· cases a.2.2.2 <;> rename_i heq
|
||||
· rw [heq] at hR
|
||||
exact .inr (.single hR)
|
||||
· exact .inr (.trans (.single hR) heq)
|
||||
· exact .inl rfl
|
||||
unfold InvImage f at this
|
||||
simp at this
|
||||
rw [this]
|
||||
constructor
|
||||
intro x
|
||||
apply InvImage.accessible
|
||||
cases x.2 <;> rename_i heq
|
||||
· rwa [heq]
|
||||
· exact h.inv_of_transGen heq
|
||||
|
||||
public theorem partialExtrinsicFix₃_eq_apply_of_acc [∀ a b c, Nonempty (C₃ a b c)]
|
||||
{R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
|
||||
{F : ∀ (a b c), (∀ (a' b' c'), 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 b c _ => partialExtrinsicFix₃ R F a b c) := by
|
||||
rw [partialExtrinsicFix₃_eq_partialExtrinsicFix wf, partialExtrinsicFix_eq_apply_of_acc wf]
|
||||
congr 1; ext a' b' c' hR
|
||||
rw [partialExtrinsicFix₃_eq_partialExtrinsicFix (wf.inv hR)]
|
||||
|
||||
public theorem partialExtrinsicFix₃_eq_apply [∀ a b c, Nonempty (C₃ a b c)]
|
||||
{R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
|
||||
{F : ∀ (a b c), (∀ (a' b' c'), 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 b c _ => partialExtrinsicFix₃ R F a b c) :=
|
||||
partialExtrinsicFix₃_eq_apply_of_acc (wf.apply _)
|
||||
|
||||
public theorem partialExtrinsicFix₃_eq_fix [∀ a b c, Nonempty (C₃ a b c)]
|
||||
{R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
|
||||
{F : ∀ a b c, (∀ a' b' c', R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
|
||||
(wf : WellFounded R) {a b c} :
|
||||
partialExtrinsicFix₃ R F a b c = wf.fix (fun x G => F x.1 x.2.1 x.2.2 (fun a b c h => G ⟨a, b, c⟩ h)) ⟨a, b, c⟩ := by
|
||||
rw [partialExtrinsicFix₃_eq_partialExtrinsicFix (wf.apply _), partialExtrinsicFix_eq_fix wf]
|
||||
|
||||
end WellFounded
|
||||
|
||||
Reference in New Issue
Block a user