Phantom decreasing measure and monadic termination

Stream: lean4

[Leni Aniva]

I want to prove that this terminates:

structure State where
  n : Nat

def f : StateM State Nat := do
  match (← get).n with
  | x+1 =>
    set ({n := x} : State)
    f
  | 0 =>
    return 0

I could not use termination_by since the function takes no arguments.

In this case, the variant is the n inside State. Is there a way to add the variant to the arguments of f, without changing its ABI call signature? For example, if I add a Nat, the compiled code would be different.

def f (n : Nat) : StateM State Nat := ...

would compile with an extra argument compared to the f above.

Is there a way to construct a Rust Phantom-like type in Lean that could be used as a variant (so a singleton inductive would not do it), and does not occupy physical memory?

For more complicated monadic algorithms, some termination proofs call for the construction of non-trivial variants. In which case, adding an explicit variant argument would change both the memory signature and runtime of the function.

Ideally the function would look like

def (n : Phantom Nat) : StateM State Nat := ...
  decreasing_by n

This doesn't work either since it needs to generate projections:

structure Decr : Prop where
  n : Nat

[Leni Aniva]

This does not work either:

inductive Flag : Prop where
  | intro (n : Nat)
structure State (flag : Flag) where
  n : Nat
  p : flag = .intro n

def f (flag : Flag) : StateM (State flag) Nat := do
  match (← get).n with
  | x+1 =>
    let flag' := .intro x
    set ({n := x, p := rfl} : State flag')
    f flag'
  | 0 =>
    return 0

which shows

fail to show termination for
  f
with errors
failed to infer structural recursion:
Cannot use parameter flag:
  the type Flag does not have a `.brecOn` recursor


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)

1) 12:4-11
Please use `termination_by` to specify a decreasing measure.

[Aaron Liu]

Well that's because Flag.intro n = Flag.intro m even when n ≠ m

[Leni Aniva]

Aaron Liu said:

Well that's because Flag.intro n = Flag.intro m even when n ≠ m

so is there no way to make a phantom variant

[Aaron Liu]

• You could make it partial
• You could unfold the definition of StateM and expose a function

[Paul Reichert]

The latter might would look like this:

structure State where
  n : Nat

@[inline]
def f : StateM State Nat :=
  let rec f' (state : State) :=
    match _ : state.n with
    | x+1 =>
      f' {n := x}
    | 0 =>
      (0, state)
  termination_by state.n
  f'

Not super nice, but I don't know of a better way in such a case...

[Paul Mure]

structure State where
  n : Nat

def f : StateM State Nat := fun s =>
  match s with
  | ⟨0⟩ => (0, s)
  | ⟨x + 1⟩ => f ⟨x⟩
termination_by s => s.n

Slightly cleaner, but might get annoying to do when the state is non-trivial. Also someone should confirm if the ABI is the same with this definition.

[Paul Mure]

Also you entirely lose the benefit of the do-notation with this.

[Leni Aniva]

Paul Mure said:

structure State where
  n : Nat

def f : StateM State Nat := fun s =>
  match s with
  | ⟨0⟩ => (0, s)
  | ⟨x + 1⟩ => f ⟨x⟩
termination_by s => s.n

Slightly cleaner, but might get annoying to do when the state is non-trivial. Also someone should confirm if the ABI is the same with this definition.

This also wouldn't work with StateRefT

[Aaron Liu]

I don't think you can prove that functions with StateRefT terminate by arguing the state is decreasing

[Henrik Böving]

That's correct

[Leni Aniva]

Aaron Liu said:

I don't think you can prove that functions with StateRefT terminate by arguing the state is decreasing

Would it be possible with additional assumptions about separation logic?

[Henrik Böving]

People have so far not been able to find a sound axiomatization of IO.Ref

[Robin Arnez]

Well, more concretely, the naive axiomatization of IO.Ref is simply inconsistent. You can get something consistent if you add the hypothesis that type inside the reference is "small" for some theorems though, e.g. see my attempt at an EIO axiomatization

[Leni Aniva]

could type erasure annotations be added to Lean to make phantom variants possible?

[Robin Arnez]

If you only care about equation lemmas, then partial_fixpoint might be enough to make it work though there's some stuff needed that currently isn't in the standard library:

open Lean Order

noncomputable instance [Nonempty α] : CCPO (Id α) := inferInstanceAs (CCPO (FlatOrder Classical.ofNonempty))
noncomputable instance [Nonempty ε] : CCPO (EStateM ε σ α) :=
  inferInstanceAs (CCPO ((s : σ) → FlatOrder (.error Classical.ofNonempty (Classical.choice ⟨s⟩))))

noncomputable instance [Nonempty ε] : CCPO (EIO ε α) := inferInstanceAs (CCPO (EStateM _ _ _))

noncomputable instance {m : Type u → Type v} [∀ α, PartialOrder (m α)] : PartialOrder (ReaderT ρ m α) := inferInstanceAs (PartialOrder (_ → _))
noncomputable instance {m : Type u → Type v} [∀ α, PartialOrder (m α)] : PartialOrder (StateT ρ m α) := inferInstanceAs (PartialOrder (_ → _))
noncomputable instance {m : Type → Type} [∀ α, PartialOrder (m α)] : PartialOrder (StateRefT' ω σ m α) := inferInstanceAs (PartialOrder (_ → _))
noncomputable instance {m : Type u → Type v} [∀ α, CCPO (m α)] : CCPO (ReaderT ρ m α) := inferInstanceAs (CCPO (_ → _))
noncomputable instance {m : Type u → Type v} [∀ α, CCPO (m α)] : CCPO (StateT ρ m α) := inferInstanceAs (CCPO (_ → _))
noncomputable instance {m : Type → Type} [∀ α, CCPO (m α)] : CCPO (StateRefT' ω σ m α) := inferInstanceAs (CCPO (_ → _))

instance [Nonempty ε] : MonoBind (EStateM ε σ) where
  bind_mono_left {_ _ a₁ a₂ f} h s := by
    specialize h s
    simp only [bind, EStateM.bind]
    generalize a₁ s = a₁ at h
    generalize a₂ s = a₂ at h
    cases h
    · exact .bot
    · exact .refl
  bind_mono_right {_ _ a f₁ f₂} h s := by
    simp only [bind, EStateM.bind]
    split
    · apply h
    · exact .refl

instance [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] : MonoBind (ReaderT ρ m) where
  bind_mono_left h s := MonoBind.bind_mono_left (h s)
  bind_mono_right h s := MonoBind.bind_mono_right (fun x => h x s)

instance [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] : MonoBind (StateT ρ m) where
  bind_mono_left h s := MonoBind.bind_mono_left (h s)
  bind_mono_right h _ := MonoBind.bind_mono_right (fun x => h x.1 x.2)

instance [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] : MonoBind (StateRefT' ω σ m) :=
  inferInstanceAs (MonoBind (ReaderT _ _))

structure State where
  n : Nat

def f : StateT State Option Nat := do
  match (← get).n with
  | x+1 =>
    set ({n := x} : State)
    f
  | 0 =>
    return 0
partial_fixpoint

[Alex Keizer]

Leni Aniva said:

could type erasure annotations be added to Lean to make phantom variants possible?

I've not read through the entire thread, but is Erased what you're looking for here?