Making `termination_by` smarter

Stream: lean4

[Arthur Adjedj]

Hi, is there a way to make the termination tactics used by termination_by smarter in any way ? In the following example, the proof of termination gets stuck trying to prove that sizeOf a < 1 + sizeOf a, despite it being provable by simp_arithwith no issue. Is the system extensible in any way that would allow me to plug in simp_arith without having to write the decreasing_by myself ?
code example:

inductive ComplexInductive (A B C : Type _) (n : Nat) : Type
  | constr : A → B → C → ComplexInductive A B C n
deriving DecidableEq

inductive NestedComplex : Type
  | constr : ComplexInductive Nat NestedComplex Nat 1 → NestedComplex

mutual
private def decEqNestedComplex (x : NestedComplex) (x₁ : NestedComplex) : Decidable (x = x₁) :=
  match x, x₁ with
  | NestedComplex.constr a , NestedComplex.constr b =>
    let inst  := decEqComplexInductiveNestedComplex a b; -- sizeOf a < 1 + sizeOf a
    if h  : a  = b  then by subst h ; exact isTrue rfl
    else isFalse  (by intro n ; injection n ; apply h  _; assumption)

private def decEqComplexInductiveNestedComplex [DecidableEq  A] [DecidableEq  C]
    (x₂ : ComplexInductive A NestedComplex C n₁)
    (x₃ : ComplexInductive A NestedComplex C n₁) : Decidable (x₂ = x₃) :=
  match x₂, x₃ with
  | ComplexInductive.constr a₁ a₂ a₃, ComplexInductive.constr b₁ b₂ b₃ =>
    if h₁ : a₁ = b₁ then by subst h₁; exact(
        let inst₁ := decEqNestedComplex  a₂ b₂;
        if h₂ : a₂ = b₂ then by subst h₂; exact (
            if h₃ : a₃ = b₃ then by subst h₃; exact isTrue rfl
            else isFalse (by intro n₂; injection n₂; apply h₃ _; assumption))
        else isFalse (by intro n₃; injection n₃; apply h₂ _; assumption))
    else isFalse (by intro n₄; injection n₄; apply h₁ _; assumption)
end
termination_by decEqNestedComplex x _ => sizeOf x
               decEqComplexInductiveNestedComplex x _ => sizeOf x

[Arthur Adjedj]

For context, I am trying to make deriving handlers manage nested inductive types, the last problem I'm encountering regards proving termination, and it would make the automation much easier if such "easy" goals could be proven automatically.

[Mario Carneiro]

Yes, the default decreasing_by is decreasing_tactic which is basically decreasing_with decreasing_trivial where decreasing_trivial is an extensible tactic, i.e. you can add lines like

macro_rules | `(tactic| decreasing_trivial) => `(tactic| do_smart_thing)

to make it do some additional logic

[Mario Carneiro]

alternatively you can overload decreasing_tactic instead if you want to do something else for the preprocessor

[Arthur Adjedj]

I'm puzzled as to why this goal doesn't get solved then: in Init.WFTactics, there is clearly

macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })); done)

and this tactic apparently solves the goal in general:

example : a < 1 + a := by simp (config := { arith := true, failIfUnchanged := false })

Yet the goal in my example above doesn't pass.

[Mario Carneiro]

If you inline the tactic definitions you get a better error message:

decreasing_by
  simp_wf
  repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
  repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
  first
  | done
  | subst_vars
    decreasing_trivial

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ComplexInductive._sizeOf_inst Nat NestedComplex Nat 1
inferred
  ComplexInductive._sizeOf_inst Nat NestedComplex Nat 1

[Mario Carneiro]

that last bit is a bit ambiguous though, with pp.all it is

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @ComplexInductive._sizeOf_inst Nat NestedComplex Nat (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) instSizeOfNat
    NestedComplex._sizeOf_inst instSizeOfNat
inferred
  @ComplexInductive._sizeOf_inst Nat NestedComplex Nat (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (instSizeOf.{1} Nat)
    NestedComplex._sizeOf_inst (instSizeOf.{1} Nat)

[Mario Carneiro]

and the difference between instSizeOfNat and instSizeOf.{1} Nat is mathematically meaningful: instSizeOfNat is the identity function and instSizeOf.{1} Nat is fun _ => 0

[Mario Carneiro]

Well, actually that is an error message from the wrong decreasing_trivial branch; but replacing decreasing_trivial with (simp (config := { arith := true, failIfUnchanged := false })); done reveals that it also doesn't prove the goal, for much the same reason: the goal is sizeOf a < 1 + sizeOf a where the two occurrences of sizeOf are using different SizeOf Nat instances

[Mario Carneiro]

If you use Nat instead of A and C in the mutual def it works without modifying the decreasing tactic

[Eric Wieser]

Mario Carneiro said:

Yes, the default decreasing_by is decreasing_tactic which is basically decreasing_with decreasing_trivial where decreasing_trivial is an extensible tactic, i.e. you can add lines like

macro_rules | `(tactic| decreasing_trivial) => `(tactic| do_smart_thing)

to make it do some additional logic

How can I tell by looking at that line that I'm extending the tactic and not replacing it?

[Mario Carneiro]

when a tactic has multiple macro_rules or elab_rules declarations for the same syntax, it will try all of them

[Mario Carneiro]

when you use macro or elab, this creates a new syntax in addition to defining a macro_rules / elab_rules for it, so it will be replacing or overloading any existing syntax of the same shape

[Eric Wieser]

Mario Carneiro said:

when a tactic has multiple macro_rules or elab_rules declarations for the same syntax, it will try all of them

I thought it tried all of them until it finds one that is matching syntax. Are you saying it tries all of them until the tactic succeeds?

[Mario Carneiro]

They are keyed by the syntax. It tries all rules for the syntax that was parsed