Tricky lexicographic termination issue

Stream: general

[Joachim Breitner]

I am trying to improve Lean’s support for guessing lexicographic orderings, and following an approach that's used by Isabelle. This guessing uses Lean’s default decreasing_tactic, or the user-specified one (but if they user specifies a tactic, then they probably have specified the termination order first anyways, and guessing isn’t really required).

Here is a mutual function definition that goes through in Isabelle automatically:

mutual
def prod (x y z : Nat) : Nat :=
  if y % 2 = 0 then eprod x y z else oprod x y z
def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
end

The order that it infers is this one, which we can of course give explicitly:

termination_by
  prod x y z => (y, 2)
  oprod x y z => (y, 1)
  eprod x y z => (y,

However, it seems our default deceasing_tactic is far from handling that automatically. This is what I had to write to make it go through:

macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.le_refl)
macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.succ_lt_succ; decreasing_trivial)
macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.sub_le)
macro_rules | `(tactic| decreasing_trivial) =>
              `(tactic| apply Nat.div_le_self)

mutual
def prod (x y z : Nat) : Nat :=
  if y % 2 = 0 then eprod x y z else oprod x y z
def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
end
termination_by
  prod x y z => (y, 2)
  oprod x y z => (y, 1)
  eprod x y z => (y, 0)
decreasing_by
  simp_wf
  solve
    | apply Prod.Lex.right'
      · solve | decreasing_trivial
      · solve | decreasing_trivial
    | apply Prod.Lex.left
      · solve | decreasing_trivial
              | apply Nat.bitwise_rec_lemma; assumption

For comparison, this is the default setup:

/-- Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using `ts` to solve the base case. If it fails,
it prints a message to help the user diagnose an ill-founded recursive definition. -/
macro "decreasing_with " ts:tacticSeq : tactic =>
 `(tactic|
   (simp_wf
    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
    first
    | done
    | $ts
    | fail "failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal"))

macro "decreasing_tactic" : tactic =>
  `(tactic| decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial)

Notable points:

• The default setup uses docs#Prod.Lex.right, which requires the left component on the pair to be defEq. This doesn’t work in the second recursive call, where the we need y - 1 ≤ y. There is a suitable lemma (docs#Prod.Lex.right'), but now we need backtracking, which the default repeat doesn't do, it seems.
• Not surprisingly, decreasing_trivial misses a lot of lemmas about ≤
• Instead of docs#Nat.bitwise_rec_lemma, it would be more natural to use Nat.div_lt_self, but which tactic will reliably get 0 < y from y ≠ 0.

It seems for the last two issues, it makes sense to wait for omega and start using that in decreasing_trivial, when maybe all these problems will dispappear, right. @Scott Morrison ? :-)

For the first issue – the more general lexicographic ordering lemma which will need backtracking, I am not sure what the best way forward will be. Or will omega be able to deal with goals of the form x1 < x2 \/ (x1 ≤ x2 /\ y1 < y2) natively?

(Or maybe such function definitions are simply out of scope for us.)

[Joachim Breitner]

Furthermore, I found it hard to develop these termination tactics, partly because the tactic passed to decreasing_by is applied at every call.

Wouldn’t it be much nicer if the goal after termination_by was a conjunction of all the proof obligations, and you could focus each goal with . individually there? (Maybe starting with all_goals simp_wf… to get a more sensible goal). It might be doable; a downside might be that if you first collect all the proof obligations in one place, it’s harder to put the squiggly line under the right function call.

[Bhavik Mehta]

I've also found filling in decreasing_by arguments hard for the same reason, so I'm in favour of your change.

[Joachim Breitner]

Great! I’ll ask you to :thumbs_up: the corresponding issue once I get around to it :-)

[Shreyas Srinivas]

+1

[Joachim Breitner]

I had a brief look, currently stuck passing more than MVar to TacticM.run: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Lean.2EElab.2ETactic.2Erun.20but.20with.20multiple.20goals

[Joachim Breitner]

I cast this idea into an RFC so that it has an issue number and a place to record more thoughts: https://github.com/leanprover/lean4/issues/2921