hoisting a proof of termination to a separate definition

Stream: lean4

[Jonathan Protzenko]

consider the following definition (please ignore the terrible proof):

def fact (x: Nat) :=
  if x <= 1 then
    1
  else
    x * fact (x - 1)
termination_by fact x => x
decreasing_by
  simp_wf
  simp_arith
  have sub_eq x y: Nat.sub x y = x - y := rfl
  rewrite [ sub_eq ]
  rewrite [ Nat.sub_add_cancel ]
  simp_arith
  have h: ¬ (x <= 1) := by assumption
  have h: x > 1 := Nat.gt_of_not_le h
  have h: 1 < x := by assumption
  apply Nat.le_of_lt
  assumption

I would like to hoist both the termination measure (termination_by) and the proof of termination for that measure (decreasing_by) to separate top-level definitions

for the termination measure, it's easy:

@[simp]
def fact_termination_measure (x: Nat) := x

def fact (x: Nat) :=
  if x <= 1 then
    1
  else
    x * fact (x - 1)
termination_by fact x => fact_termination_measure x
decreasing_by ...

but for the proof itself, I don't know how to "lift" it to its own tactic definition

syntax "fact_termination_proof" term : tactic

macro_rules | `(tactic| fact_termination_proof x) => `(tactic| (
  ... same contents as before ...

def fact
  ... as above ...
decreasing_by fact_termination_proof

doesn't seem to work -- is there a way to write this termination proof in its own separate definition?

context: I am writing a Lean backend for my Rust verification tool, and now I'm adding support for termination proofs... the tool translates a Rust definition to a Lean definition that contains "open variables" for the proof of termination, found in another module, and the user is expected to fill them out... in my case, fact_termination_proof would be a stub in UserProvidedProofs.lean, and then the user would replace a sorry with an actual proof of termination

[Jonathan Protzenko]

expanding on the "doesn't seem to work": I get a whole lot of errors along the lines of unknown identifier 'x✝' so I'm probably not doing my binding right

[Mario Carneiro]

Note that it is unusual to provide a complicated proof of termination directly in decreasing_by unless it is a general purpose tactic, because it runs on all termination goals. If you want to provide a specific termination argument, you should use decreasing_by assumption (which is also the default, more or less) and then put have : x - 1 < x := by ... before the call to fact (x - 1)

[Jonathan Protzenko]

ok, yes, good usability question: do I want the user to solve all termination goals at once, or have them fill out separate proofs for each recursive call... worth pondering (I was basing myself on the example here: https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html for ack which solves both goals at once)

[Mario Carneiro]

I would (and lean does) use a general purpose tactic which can prove most termination goals, and then have a fallback of manual proof which is for specific termination goals. Users can't easily write termination proofs that prove multiple goals at once

[Mario Carneiro]

normally there will only be one nontrivial termination goal in a given function, though

[Jonathan Protzenko]

thanks, two sub-questions then:

• in this particular case, decreasing_tactic does not work -- what would be the recommended style for this specific example?
• back to my original use-case, the function body is auto-generated by a tool, but the termination proofs are hand-written, so I need to modularly de-couple the two -- there are no annotations on the source program, so I really want to separate the function definition (auto-generated, may be overwritten at some point in the future) and the proof of termination (maintained by the user in a separate file that does not get overwritten when the code is re-generated)

[James Gallicchio]

RE: the first point, the idea is that decreasing_tactic gets called on each of the termination goals. it includes (as one of the things it tries) assumption, which just looks for a proof of the goal in context. so if you provide a goal with have : the_termination_goal := the_proof right before making a recursive call, the default decreasing_by tactic will find and use that proof.

[Jonathan Protzenko]

ah I see what you mean... bearing in mind that the definition is auto-generated, this means that I would have to generate the have : clause before the recursive call, refer to the proof that the user has written somewhere else (possibly via their own tactic), and maybe even pick a particular kind of ordering?

[Mario Carneiro]

In this specific example I think you could do something like this:

import Std.Data.Nat.Lemmas

theorem termination_proof (h : ¬x ≤ 1) : x - 1 < x :=
  Nat.sub_lt (Nat.lt_trans (by decide) (Nat.not_le.1 h)) (by decide)

def fact (x: Nat) :=
  if h : x <= 1 then
    1
  else
    x * have := termination_proof h; fact (x - 1)

[Mario Carneiro]

the proof is not as automatic as I would like (it gets better if you can use mathlib linarith)

[James Gallicchio]

out of curiosity, what's the use case? this seems like an interesting project

[Jonathan Protzenko]

thanks, no worries about the proof quality

[Jonathan Protzenko]

this is the tool: https://arxiv.org/abs/2206.07185, presented at ICFP of last year, see also https://github.com/AeneasVerif/aeneas: we generate a pure translation of Rust programs (currently, we have Coq + F* backends, with Isabelle/HOL and Lean4 in the works)

[Jonathan Protzenko]

then the user provides the proofs on top of the generated code

[Jonathan Protzenko]

here's where it gets complicated for me: because our tool auto-generates the definition fact, right now, I don't know that h is an important hypothesis that needs to be inserted in the output of the translation (the fact) function, so I would be at a loss as to how to "infer" the have clause to be inserted at the site of the recursive call

[Jonathan Protzenko]

here's an example using the F* backend: this is what the tool generates, notice how the decreases clause is "generic" https://github.com/AeneasVerif/aeneas/blob/main/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst#L14-L34

then, the definition for this decreases clause is written by the user here: https://github.com/AeneasVerif/aeneas/blob/main/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst#L10-L12 (possibly with something custom is the recursion is non-trivial)

[Jonathan Protzenko]

by the way, Aeneas is @Son Ho's PhD project (just realized he's on this Zulip, too)

[James Gallicchio]

F* has much more automation in its proof checker than Lean (where the automation is done during elaboration, not during typechecking). You can probably get something very close to the F* backend if you always use the proof-term-having control flow structures (like if h : whatever then .. else .. and match h : object with | ... => ...) and allow users to add hypotheses to the termination proofs, which you can then fill in at the call site with by assumption or similar.

[Mario Carneiro]

Jonathan Protzenko said:

here's where it gets complicated for me: because our tool auto-generates the definition fact, right now, I don't know that h is an important hypothesis that needs to be inserted in the output of the translation (the fact) function, so I would be at a loss as to how to "infer" the have clause to be inserted at the site of the recursive call

You can just put everything in the context in there

[James Gallicchio]

^only thing is re-generating the def might change the available context. not sure what the best approach would be there

[Jonathan Protzenko]

yes, but that's a problem for other backends too if you e.g. add arguments to the function

[Jonathan Protzenko]

so it's not perfect, but at least it's an improvement

[Jonathan Protzenko]

so that could work, provided I know all of the hypotheses... for instance, what happens if the if-condition is negated? will the hypothesis still be name-able in the else branch?

[Mario Carneiro]

yes, in fact that is the case in this example

[Jonathan Protzenko]

indeed!

[Mario Carneiro]

it will be a double negative if you say if h : not (x > 1) but I assume that isn't a major issue

[Jonathan Protzenko]

and do control-flow dependent hypotheses arise from anything other than if and match?

[Mario Carneiro]

well function calls can have complicated conditions on them but maybe you are fine with having the user supply the condition

[Mario Carneiro]

the lean compiler is basically just if, match and recursive functions, control-flow-wise

[Mario Carneiro]

so I think you are covered

[Jonathan Protzenko]

great -- thanks to both of you for the discussion, that was very helpful

[Jonathan Protzenko]

I'm still curious as to why I was getting these unknown identifier 'x✝' errors in the first place, but I guess that's irrelevant... maybe I was violating hygiene or something

[Mario Carneiro]

do you have an MWE for that?

[Jonathan Protzenko]

@[simp]
def fact_termination_measure (x: Nat) := x

syntax "fact_termination_proof" term : tactic

macro_rules | `(tactic| fact_termination_proof x) => `(tactic| (
  simp_wf
  simp_arith
  have sub_eq x y: Nat.sub x y = x - y := rfl
  rewrite [ sub_eq ]
  rewrite [ Nat.sub_add_cancel ]
  simp_arith
  have h: ¬ (x <= 1) := by assumption
  have h: x > 1 := Nat.gt_of_not_le h
  have h: 1 < x := by assumption
  apply Nat.le_of_lt
  assumption))

def fact (x: Nat) :=
  if x <= 1 then
    1
  else
    x * fact (x - 1)
termination_by fact x => fact_termination_measure x
decreasing_by
  fact_termination_proof x

[Jonathan Protzenko]

I don't have a precise mental model for how the elaborator works and how binding resolution is done, so maybe this isn't supposed to work to begin with

[Mario Carneiro]

you are pattern matching a literal x in your macro definition. The macro model is somewhat similar to rust hygienic macros

[Mario Carneiro]

this works:

macro_rules | `(tactic| fact_termination_proof $x) => `(tactic| (
  simp_wf
  simp_arith
  have sub_eq x y: Nat.sub x y = x - y := rfl
  rewrite [ sub_eq ]
  rewrite [ Nat.sub_add_cancel ]
  simp_arith
  have h: ¬ ($x <= 1) := by assumption
  have h: $x > 1 := Nat.gt_of_not_le h
  have h: 1 < $x := by assumption
  apply Nat.le_of_lt
  assumption))

[Jonathan Protzenko]

ah yes of course... thanks!