feature request: proving termination

Stream: lean4

[Kayla Thomas]

I'm not certain how to describe this other than by a minimal example of what I would like to have work:

inductive T1 : Type
| c1 : T1
| c2 : T1 → T1 → T1
| c3 : ℕ → T1

def Blah : List ℕ → T1 → Prop
| _, T1.c1 => True
| l, T1.c2 x y => Blah l x ∧ Blah l y
| [], T1.c3 _ => False
| hd :: tl, T1.c3 n => Blah tl (T1.c3 n)

fail to show termination for
  FOL.Blah
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    Blah l x

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    Blah tl (T1.c3 n)

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

[François G. Dorais]

Add termination_by Blah l t => sizeOf l + sizeOf t at the end of Blah.

[Kayla Thomas]

Hmm. Yes, that works, thank you. Maybe the example was too minimal.

[François G. Dorais]

The issue was with the last case: | hd :: tl, T1.c3 n => Blah tl (T1.c3 n) where the second argument isn't decreasing, so you need to somehow say that the first argument counts too.

[François G. Dorais]

Interestingly, if you remove the second case | l, T1.c2 x y => Blah l x ∧ Blah l y where the second argument decreases but the first does not, then Lean can figure out that the first argument matters.

[François G. Dorais]

Lean can't be perfect at figuring out termination arguments... otherwise, the Halting Problem wouldn't be a problem at all!

[Kayla Thomas]

:)

[Kayla Thomas]

This is the larger case:

def VarAssignment (D : Type) : Type := VarName → D

structure Definition : Type :=
(name : DefName)
(args : List VarName)
(q : Formula)
(nodup : args.Nodup)
(nf : q.freeVarSet ⊆ args.toFinset)
deriving DecidableEq

def Env : Type := List Definition

def Holds
  (D : Type)
  (I : Interpretation D) :
  VarAssignment D → Env → Formula → Prop
  | V, E, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | V, E, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | V, E, eq_ x y => V x = V y
  | _, _, true_ => True
  | _, _, false_ => False
  | V, E, not_ phi => ¬ Holds D I V E phi
  | V, E, imp_ phi psi => Holds D I V E phi → Holds D I V E psi
  | V, E, and_ phi psi => Holds D I V E phi ∧ Holds D I V E psi
  | V, E, or_ phi psi => Holds D I V E phi ∨ Holds D I V E psi
  | V, E, iff_ phi psi => Holds D I V E phi ↔ Holds D I V E psi
  | V, E, forall_ x phi => ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | V, E, exists_ x phi => ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | V, ([] : Env), def_ _ _ => False
  | V, d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)

[Kayla Thomas]

Adding termination_by _ V E psi => sizeOf E + sizeOf psi gets it to the then case.

[Kayla Thomas]

Which gives

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

D: Type
V: VarAssignment D
d: Definition
E: List Definition
name: DefName
args: List VarName
h✝: name = d.name ∧ List.length args = List.length d.args
⊢ sizeOf d.q < 1 + sizeOf name + sizeOf args

[François G. Dorais]

Aha! That case is not decreasing at all. I don't know exactly what you're trying to do but I think you may have discovered the point of cut elimination!

The consistency of cut-free systems is easily proved by the kind of recursion you gave. The issue is the cut rule, which is not decreasing in length. However, some cut-elimination theorems can be shown for some system where cuts can be eliminated from a proof at the cost of a super exponential blowup in proof size. So you might have a lot of work ahead of you!

Then again, I don't know exactly what you're doing, so you might be able to come up with a measure that decreases in that case too.

Have you tried 1 + sizeOf E + sizeOf psi, just in case?

[Kayla Thomas]

I just tried it, but it didn't seem to help.
I'm sorry, I'm not really familiar with cut elimination.
Mario Carneiro came up with a mutually recursive definition that works, but I was hoping to be able to do it with this definition. This is the mutually recursive definition:

def Holds'
  (D : Type)
  (I : Interpretation D)
  (holds : Formula → VarAssignment D → Prop)
  (dfn : Option Definition) :
  Formula → VarAssignment D → Prop
  | pred_const_ X xs, V => I.pred_const_ X (xs.map V)
  | pred_var_ X xs, V => I.pred_var_ X (xs.map V)
  | eq_ x y, V => V x = V y
  | true_, _ => True
  | false_, _ => False
  | not_ phi, V => ¬ Holds' D I holds dfn phi V
  | imp_ phi psi, V => Holds' D I holds dfn phi V → Holds' D I holds dfn psi V
  | and_ phi psi, V => Holds' D I holds dfn phi V ∧ Holds' D I holds dfn psi V
  | or_ phi psi, V => Holds' D I holds dfn phi V ∨ Holds' D I holds dfn psi V
  | iff_ phi psi, V => Holds' D I holds dfn phi V ↔ Holds' D I holds dfn psi V
  | forall_ x phi, V => ∀ d : D, Holds' D I holds dfn phi (Function.updateIte V x d)
  | exists_ x phi, V => ∃ d : D, Holds' D I holds dfn phi (Function.updateIte V x d)
  | def_ name args, V =>
    Option.elim dfn
      False
      (
        fun (d : Definition) =>
        if name = d.name ∧ args.length = d.args.length
        then holds d.q (Function.updateListIte V d.args (List.map V args))
        else holds (def_ name args) V
      )

def Holds
  (D : Type)
  (I : Interpretation D) :
  Env → Formula → VarAssignment D → Prop
| [] => Holds' D I (fun _ _ => False) Option.none
| d :: E => Holds' D I (Holds D I E) (Option.some d)

[Kayla Thomas]

That case isn't decreasing on Env?

[Mario Carneiro]

This definition is decreasing lexicographically on (phi, E) (or (x, l) for the MWE)

[Mario Carneiro]

it's kind of ackermann-esque, not sure how well lean handles termination proving for that

[Mario Carneiro]

To make the MWE not allow sizeOf l + sizeOf t as a possible termination measure, you can replace the second case by

| l, T1.c2 x y => Blah (l ++ l) x ∧ Blah l y

[François G. Dorais]

But that's just because (l ++ l).length = l.length + l.length is not applied by the termination tactic?

[François G. Dorais]

I was afraid of Ackermanian-esque growth issues but this is just a Prop-evaluation function, so it's linear!

[Mario Carneiro]

it's not about growth but about the recursion structure

[Mario Carneiro]

and no, applying that lemma would not help because if sizeOf l is bigger than sizeOf y then it really isn't decreasing by the metric sizeOf l + sizeOf t

[Mario Carneiro]

but you can imagine that it was foo l instead, where foo : List Nat -> List Nat is an opaque function with no particular boundedness guarantees

[Mario Carneiro]

The prop evaluation function is in fact exponential, because it unfolds definitions (the E parameter is the environment, and every time a definition is unfolded it goes through another round of substitution / doubling)

[François G. Dorais]

Yes, that's the issue. It might be even worse than exponential in the end!

I'm confused by @Kayla Thomas's example since there is no type for Env?

[Kayla Thomas]

Sorry, I edited it to add it.

[Kayla Thomas]

def Env : Type := List Definition

[François G. Dorais]

There might be a serious issue here: I'm not exactly sure what Defintion actually is but it might allow something like def f x := f (f x) in which case termination is a no-go.

[Kayla Thomas]

structure Definition : Type :=
(name : DefName)
(args : List VarName)
(q : Formula)
(nodup : args.Nodup)
(nf : q.freeVarSet ⊆ args.toFinset)
deriving DecidableEq

[Kayla Thomas]

inductive Formula : Type
  | pred_const_ : PredName → List VarName → Formula
  | pred_var_ : PredName → List VarName → Formula
  | eq_ : VarName → VarName → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : VarName → Formula → Formula
  | exists_ : VarName → Formula → Formula
  | def_ : DefName → List VarName → Formula
  deriving Inhabited, DecidableEq

[Mario Carneiro]

François G. Dorais said:

There might be a serious issue here: I'm not exactly sure what Defintion actually is but it might allow something like def f x := f (f x) in which case termination is a no-go.

This isn't possible because after unfolding definition d in context d :: E, the definition body is evaluated in context E, so any references to d in the unfolding (if d tries to be self referential) will be treated as non-existing (and unfold to False in the fallback case for ([] : Env))

[Mario Carneiro]

however you definitely can have a sequence of definitions x(n+1) := xn -> xn and get exponential growth that way

[François G. Dorais]

You seem to know a lot more than me about @Kayla Thomas's context! However, for the original question: the recursion needs to include Env for sure: you can't expect a shortcut here for reasons we just explained.

[Mario Carneiro]

(I've been talking with @Kayla Thomas about this project for a very long time via PM)

[François G. Dorais]

That makes sense!

[Mario Carneiro]

This is what I would call a "structural recursion", either E decreases (structurally) or it stays the same and phi decreases (structurally)

[Mario Carneiro]

but it isn't declared with an argument order that makes this obvious

[Mario Carneiro]

looks like lean can't handle the regular ackermann function either:

def ack : Nat → Nat → Nat
| 0, n => n + 1
| m+1, 0 => ack m 1
| m+1, n+1 => ack m (ack (m+1) n)

-- fail to show termination for
--   ack
-- with errors
-- argument #1 was not used for structural recursion
--   failed to eliminate recursive application
--     ack (m + 1) n
--
-- argument #2 was not used for structural recursion
--   failed to eliminate recursive application
--     ack m 1
--
-- structural recursion cannot be used
--
-- failed to prove termination, use `termination_by` to specify a well-founded relation

Adding termination_by _ m n => (m, n) does work though, unlike @Kayla Thomas 's example

[François G. Dorais]

See also: https://proofassistants.stackexchange.com/a/2202/

[Mario Carneiro]

which looks pretty similar to the split definition Holds' kayla posted above

[François G. Dorais]

OK. I think I see what's going on with Kayla's definition. I think it's of ordinal length ω^ω. The size function is something like ω^e(f+1) where e is the definition depth and f is the formula size. The idea is that each definition adds ω since there's no telling how big the definition is. Once it's all settled though it's linear in the length of each formula down the line.

[Mario Carneiro]

well, if you are talking about the asymptotic size of the function, you would include E in the size measure, so the definition is at most linear

[François G. Dorais]

No, I'm talking about the proof-theoretic depth of the termination argument.

[Mario Carneiro]

well, since it has a termination measure of (E, phi) and those are both countable sets with order type omega, the whole termination argument yields order type $\omega^2$

[Mario Carneiro]

(same as the ackermann function)

[Mario Carneiro]

since this function doesn't grow as explosively as the ackermann function, it's likely that there is a plain old termination measure in Nat

[François G. Dorais]

Well, so my first edit was probably correct.

OK. I think I see what's going on with Kayla's definition. I think it's of ordinal length ω². The size function is something like ωe + f where e is the definition depth and f is the formula size. The idea is that each definition adds ω since there's no telling how big the definition is. Once it's all settled though it's linear in the length of each formula down the line.

I was worried that phi might have several occurrences of the topmost definition but they all have the same depth, so that's just a constant multiple. These are tough calculations to do late at night!

[François G. Dorais]

It might be ω³ though... Oh well, its > ω for sure!

[Mario Carneiro]

yeah I think your quote is correct, why do you think it is omega^3?

[François G. Dorais]

Because phi might have any number of definitions in it.

[Mario Carneiro]

the f in ωe + f represents the number of constructors involved in phi itself. If you unfold any definition, no matter how large, it will be ω(e-1) + f' (where f' is the size of the definition body) which is less

[Mario Carneiro]

the number of definitions doesn't matter so much since this is just about the "height" of the recursion, not the number of nodes

[François G. Dorais]

I think you're right but it's late over here... I keep second-guessing myself.

Thank you for the very entertaining discussion! I hope Kayla also got something useful out of it!

[Kayla Thomas]

Thank you.

[François G. Dorais]

Actually, I'm still not sure. I'm second-guessing again, lol! I'm thinking you didn't factor that the definition in env might involve later definitions when calculating f'. I'm not sure though and, as I said, it's really late over here so I'm not thinking as clearly as I should.

[François G. Dorais]

I disagree about the "number of nodes" argument since that number could grow at each step.

[Mario Carneiro]

f' doesn't include the later definitions, the ω(e-1) accounts for that

[Mario Carneiro]

The precise claim here is that you can map each pair (E, phi) involved in the computation to an ordinal less than $\omega^2$, such that for each immediate call made the current ordinal value is greater than the value of the call arguments

[Mario Carneiro]

and the mapping is essentially omega * length E + sizeOf phi

[François G. Dorais]

Yes, that is the initial guess.

[François G. Dorais]

And I think it may be right but I keep second-guessing myself.

[François G. Dorais]

The issue is that length E doesn't capture the total length of the formulas in E.

[François G. Dorais]

That could be way large if all definitions are expanded!

[François G. Dorais]

@Kayla Thomas If the initial guess is correct, use something like the sum of the lengths in Env rather than the length of Env for your measure. If the second-guess is right, that still won't work even if you supply a custom decreasing_by argument.

[François G. Dorais]

By that, I don't mean that it's your burden to decide who's right! It's just the next thing to try to see if it works!

[Mario Carneiro]

François G. Dorais said:

The issue is that length E doesn't capture the total length of the formulas in E.

That's okay, that's what the omega is for. No matter how big the formula is it's always less than omega. The fact that you can give a more precise upper bound on this in terms of the sum of sizes of the formulas in E or the like is an indication that omega is a loose bound, and there is another bound you could give with order type $\omega$ instead of $\omega^2$.

[François G. Dorais]

Now that I've had some sleep, I agree: ω² is right. I was overthinking the effect of substituting formulas from the environment, but the setup doesn't allow recursive definitions so it's not a significant effect.

[Kayla Thomas]

I'm sorry, a lot of this seems to be over my head. It sounds like I should try the sum of the lengths in Env? So the lengths of the Definition structures in Env? What would that be?

[François G. Dorais]

termination_by _ => (E, phi) should suffice.

[Kayla Thomas]

I have to do termination_by _ V E phi => (E, phi) to fix the unknown identifiers. That gives me

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

case h
D: Type
V: VarAssignment D
E: Env
phipsi: Formula
x✝: (y : (_ : VarAssignment D) ×' (_ : Env) ×' Formula) →
  (invImage (fun a => PSigma.casesOn a fun V snd => PSigma.casesOn snd fun E snd => (E, snd))
          Prod.instWellFoundedRelationProd).1
      y { fst := V, snd := { fst := E, snd := imp_ phi psi } } →
    Prop
a✝: x✝ { fst := V, snd := { fst := E, snd := phi } }
  (_ :
    (invImage (fun a => PSigma.casesOn a fun V snd => PSigma.casesOn snd fun E snd => (E, snd))
          Prod.instWellFoundedRelationProd).1
      { fst := V, snd := { fst := E, snd := phi } } { fst := V, snd := { fst := E, snd := imp_ phi psi } })
⊢ sizeOf psi < sizeOf (imp_ phi psi)

at the imp_ case.

[Kayla Thomas]

Does that mean it won't work and this does need to be a feature request?

[François G. Dorais]

It seems to me that sizeOf psi < sizeOf (imp_ phi psi) is true. Try adding have : sizeOf psi < sizeOf (imp_ phi psi) := sorry somewhere in the imp_ case and see if that helps. (Of course, you will have to fill in that sorry later on.)

[Kayla Thomas]

The termination_by _ V E psi => sizeOf E + sizeOf psi seems to work for this case. It just fails on the then case.

[François G. Dorais]

What is the missing goal there?

[Kayla Thomas]

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

D: Type
V: VarAssignment D
d: Definition
E: List Definition
name: DefName
args: List VarName
h✝: name = d.name ∧ List.length args = List.length d.args
⊢ sizeOf d.q < 1 + sizeOf name + sizeOf args

[François G. Dorais]

That goal is not true. That's why you need to use termination_by _ => (E, psi). Did you try adding the have in the imp_ case?

[Kayla Thomas]

Sorry, no. What is the syntax for adding it?

[Kayla Thomas]

That is, where does it get added in the | V, E, imp_ phi psi => Holds D I V E phi → Holds D I V E psi

[Kayla Thomas]

I see, it depends on the line spacing.

[François G. Dorais]

| V, E, imp_ phi psi =>
  have : sizeOf psi < sizeOf (imp_ phi psi) := sorry
  Holds D I V E phi → Holds D I V E psi

[Kayla Thomas]

That works until I hit the then case again, which is now

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

case h
D: Type
V: VarAssignment D
d: Definition
E: List Definition
name: DefName
args: List VarName
h✝: name = d.name ∧ List.length args = List.length d.args
⊢ False

[François G. Dorais]

Yikes! That's not good!

[Kayla Thomas]

:)

[François G. Dorais]

Does using termination_by _ => (sizeOf E, sizeOf psi) change anything?

[Kayla Thomas]

With the haves for the other cases, it brings it back to

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

case h
D: Type
V: VarAssignment D
d: Definition
E: List Definition
name: DefName
args: List VarName
h✝: name = d.name ∧ List.length args = List.length d.args
⊢ sizeOf d.q < 1 + sizeOf name + sizeOf args

for the then case.

[Kayla Thomas]

Sorry, I'm heading out for a while. Thank you.

[François G. Dorais]

Aha! I think termination_by _ _ E phi => (E.length, phi) works.

[Kayla Thomas]

Yep, this works:

def Holds
  (D : Type)
  (I : Interpretation D) :
  VarAssignment D → Env → Formula → Prop
  | V, _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | V, _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | V, _, eq_ x y => V x = V y
  | _, _, true_ => True
  | _, _, false_ => False
  | V, E, not_ phi => ¬ Holds D I V E phi
  | V, E, imp_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi → Holds D I V E psi
  | V, E, and_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ∧ Holds D I V E psi
  | V, E, or_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ∨ Holds D I V E psi
  | V, E, iff_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ↔ Holds D I V E psi
  | V, E, forall_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | V, E, exists_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | _, ([] : Env), def_ _ _ => False
  | V, d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ _ E phi => (E.length, phi)

Thank you! Do you think there is a way to do it without the haves?

[Scott Morrison]

Try adding

decreasing_by simp

at the end. (I don't have a #mwe, so can't try it, but decreasing_by lets you specify tactics to generate these obligations.

[James Gallicchio]

(you may still need decreasing_tac or at least simp_wf?)

[James Gallicchio]

decreasing_by simp_wf; simp probably suffices :joy:

[François G. Dorais]

Interestingly, it seems to work fine without the interpretation stuff. Here is my recreation:

inductive Formula
| tt : Formula
| ff : Formula
| eql : Nat → Nat → Formula
| neg : Formula → Formula
| imp : Formula → Formula → Formula
| cnj : Formula → Formula → Formula
| dsj : Formula → Formula → Formula
| any : Nat → Formula → Formula
| all : Nat → Formula → Formula
| dfn : String → List Nat → Formula

structure Definition where
  name : String
  args : List Nat
  form : Formula

def valUpdate {Dom : Type} (val : Nat → Dom) : List (Nat × Dom) → Nat → Dom
| [], n => val n
| (i, p) :: ips, n => if n = i then p else valUpdate val ips n

def Formula.eval {Dom : Type} (val : Nat → Dom) : List Definition → Formula → Prop
| _, eql m n => val m = val n
| _, tt => True
| _, ff => True
| ctx, neg phi => ¬ eval val ctx phi
| ctx, imp phi psi => eval val ctx phi → eval val ctx psi
| ctx, cnj phi psi => eval val ctx phi ∧ eval val ctx psi
| ctx, dsj phi psi => eval val ctx phi ∨ eval val ctx psi
| ctx, any n phi => ∃ d, eval (valUpdate val [(n, d)]) ctx phi
| ctx, all n phi => ∀ d, eval (valUpdate val [(n, d)]) ctx phi
| [], dfn _ _ => False
| c :: ctx, dfn name args =>
  if name == c.name ∧ args.length == c.args.length then
    let val := valUpdate val ((c.args.zip args).map fun (i, j) => (i, val j))
    eval val ctx c.form
  else
    eval val ctx (dfn name args)
termination_by _ ctx phi => (ctx, phi)

[François G. Dorais]

What if you move the variable assignment left of the colon?

[Kayla Thomas]

Doesn't it need to be to the right because it is changed in the forall_ and exists_ cases?

[Kayla Thomas]

Aside: This is the Function.updateIte definition.

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

[François G. Dorais]

No, it only needs to be to the right of the colon if it's part of the recursion structure.

[Kayla Thomas]

This should be a closer "MWE":

import Mathlib.Util.CompileInductive
import Mathlib.Data.List.Basic


inductive Formula : Type
  | pred_const_ : String → List String → Formula
  | pred_var_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  | def_ : String → List String → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula

structure Definition : Type :=
(name : String)
(args : List String)
(q : Formula)
deriving DecidableEq

def Env : Type := List Definition

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

def Function.updateListIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β) :
  List α → List β → α → β
  | x::xs, y::ys => Function.updateIte (Function.updateListIte f xs ys) x y
  | _, _ => f


structure Interpretation (D : Type) : Type :=
  (nonempty : Nonempty D)
  (pred_const_ : String → (List D → Prop))
  (pred_var_ : String → (List D → Prop))

def VarAssignment (D : Type) : Type := String → D

def Holds
  (D : Type)
  (I : Interpretation D) :
  VarAssignment D → Env → Formula → Prop
  | V, _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | V, _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | V, _, eq_ x y => V x = V y
  | _, _, true_ => True
  | _, _, false_ => False
  | V, E, not_ phi => ¬ Holds D I V E phi
  | V, E, imp_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi → Holds D I V E psi
  | V, E, and_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ∧ Holds D I V E psi
  | V, E, or_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ∨ Holds D I V E psi
  | V, E, iff_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ↔ Holds D I V E psi
  | V, E, forall_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | V, E, exists_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | _, ([] : Env), def_ _ _ => False
  | V, d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ _ E phi => (E.length, phi)

[Kayla Thomas]

It still seems to need to haves.

[Kayla Thomas]

This

termination_by _ E phi => (E.length, phi)
decreasing_by simp_wf; simp

does not seem to work. I get goals like

unsolved goals

D: Type
V: VarAssignment D
E: Env
phi: Formula
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => sizeOf a₁ < sizeOf a₂) (List.length E, phi) (List.length E, not_ phi)

[François G. Dorais]

Yes, but strangely the haves are not actually relevant! It's the same have in each case but it's only relevant in the imp_ case. There's no way it's of any help in the and_, or_ and iff_ cases!

This is truly bizarre! There's clearly a bug somewhere under the hood!

[Kayla Thomas]

Why is it not relevant in the other cases?

[Kayla Thomas]

With the V to the left of the colon:

import Mathlib.Util.CompileInductive
import Mathlib.Data.List.Basic


inductive Formula : Type
  | pred_const_ : String → List String → Formula
  | pred_var_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  | def_ : String → List String → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula

structure Definition : Type :=
(name : String)
(args : List String)
(q : Formula)
deriving DecidableEq

def Env : Type := List Definition

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

def Function.updateListIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β) :
  List α → List β → α → β
  | x::xs, y::ys => Function.updateIte (Function.updateListIte f xs ys) x y
  | _, _ => f


structure Interpretation (D : Type) : Type :=
  (nonempty : Nonempty D)
  (pred_const_ : String → (List D → Prop))
  (pred_var_ : String → (List D → Prop))

def VarAssignment (D : Type) : Type := String → D

def Holds
  (D : Type)
  (I : Interpretation D)
  (V : VarAssignment D) : Env → Formula → Prop
  | _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | _, eq_ x y => V x = V y
  | _, true_ => True
  | _, false_ => False
  | E, not_ phi => ¬ Holds D I V E phi
  | E, imp_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi → Holds D I V E psi
  | E, and_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ∧ Holds D I V E psi
  | E, or_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ∨ Holds D I V E psi
  | E, iff_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi ↔ Holds D I V E psi
  | E, forall_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | E, exists_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | ([] : Env), def_ _ _ => False
  | d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ E phi => (E.length, phi)

[François G. Dorais]

In the and_ case, for example, what Lean needs to know is that sizeOf psi < sizeOf (and_ phi psi) so that the second recursive call Holds D I V E psi is smaller than the incoming argument and_ phi psi. But the given hint sizeOf psi < sizeOf (imp_ phi psi) says nothing about and_ phi psi but it somehow works!

[Kayla Thomas]

oh, huh, a copy and paste error works.

[François G. Dorais]

I suspect that Lean somehow knows that sizeOf (and_ phi psi) = sizeOf (imp_ phi psi) so it doesn't matter which hint you give.

[François G. Dorais]

It's pretty funny though! :laughing:

[Kayla Thomas]

:)

[Kayla Thomas]

Fixed version:

import Mathlib.Util.CompileInductive
import Mathlib.Data.List.Basic


inductive Formula : Type
  | pred_const_ : String → List String → Formula
  | pred_var_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  | def_ : String → List String → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula

structure Definition : Type :=
(name : String)
(args : List String)
(q : Formula)
deriving DecidableEq

def Env : Type := List Definition

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

def Function.updateListIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β) :
  List α → List β → α → β
  | x::xs, y::ys => Function.updateIte (Function.updateListIte f xs ys) x y
  | _, _ => f


structure Interpretation (D : Type) : Type :=
  (nonempty : Nonempty D)
  (pred_const_ : String → (List D → Prop))
  (pred_var_ : String → (List D → Prop))

def VarAssignment (D : Type) : Type := String → D

def Holds
  (D : Type)
  (I : Interpretation D)
  (V : VarAssignment D) : Env → Formula → Prop
  | _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | _, eq_ x y => V x = V y
  | _, true_ => True
  | _, false_ => False
  | E, not_ phi => ¬ Holds D I V E phi
  | E, imp_ phi psi =>
    have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi → Holds D I V E psi
  | E, and_ phi psi =>
    have : sizeOf psi < sizeOf (and_ phi psi) := by simp
    Holds D I V E phi ∧ Holds D I V E psi
  | E, or_ phi psi =>
    have : sizeOf psi < sizeOf (or_ phi psi) := by simp
    Holds D I V E phi ∨ Holds D I V E psi
  | E, iff_ phi psi =>
    have : sizeOf psi < sizeOf (iff_ phi psi) := by simp
    Holds D I V E phi ↔ Holds D I V E psi
  | E, forall_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | E, exists_ x phi =>
    have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | ([] : Env), def_ _ _ => False
  | d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ E phi => (E.length, phi)

Unfortunately adding decreasing_by simp_wf; simp seems to break it.

[François G. Dorais]

The bug is with imports and the compile_inductive% Formula line! If you delete that line and the imports, then termination_by _ E phi => (E, phi) works just fine!
I think that Mathlib.Data.List.Basic contains a bad simp lemma. You should report that as a bug on Mathlib!

[François G. Dorais]

I just checked: compile_inductive% Formula is not an issue. The problem is with Mathlib.Data.List.Basic.

[Kayla Thomas]

Huh. Yeah. This works:

import Mathlib.Util.CompileInductive
--import Mathlib.Data.List.Basic


inductive Formula : Type
  | pred_const_ : String → List String → Formula
  | pred_var_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  | def_ : String → List String → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula

structure Definition : Type :=
(name : String)
(args : List String)
(q : Formula)
deriving DecidableEq

def Env : Type := List Definition

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

def Function.updateListIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β) :
  List α → List β → α → β
  | x::xs, y::ys => Function.updateIte (Function.updateListIte f xs ys) x y
  | _, _ => f


structure Interpretation (D : Type) : Type :=
  (nonempty : Nonempty D)
  (pred_const_ : String → (List D → Prop))
  (pred_var_ : String → (List D → Prop))

def VarAssignment (D : Type) : Type := String → D

def Holds
  (D : Type)
  (I : Interpretation D)
  (V : VarAssignment D) : Env → Formula → Prop
  | _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | _, eq_ x y => V x = V y
  | _, true_ => True
  | _, false_ => False
  | E, not_ phi => ¬ Holds D I V E phi
  | E, imp_ phi psi =>
    --have : sizeOf psi < sizeOf (imp_ phi psi) := by simp
    Holds D I V E phi → Holds D I V E psi
  | E, and_ phi psi =>
    --have : sizeOf psi < sizeOf (and_ phi psi) := by simp
    Holds D I V E phi ∧ Holds D I V E psi
  | E, or_ phi psi =>
    --have : sizeOf psi < sizeOf (or_ phi psi) := by simp
    Holds D I V E phi ∨ Holds D I V E psi
  | E, iff_ phi psi =>
    --have : sizeOf psi < sizeOf (iff_ phi psi) := by simp
    Holds D I V E phi ↔ Holds D I V E psi
  | E, forall_ x phi =>
    --have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | E, exists_ x phi =>
    --have : sizeOf phi < 1 + sizeOf x + sizeOf phi := by simp
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | ([] : Env), def_ _ _ => False
  | d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ E phi => (E.length, phi)

but not with the Mathlib.Data.List.Basic.

[François G. Dorais]

You can also use (E, phi) instead of (E.length, phi).

[Kayla Thomas]

That breaks the then case for me.

[Kayla Thomas]

It doesn't break it for you?

[François G. Dorais]

It still works on my end. Did you change anything subtle?

[François G. Dorais]

Here is my version:

import Mathlib.Util.CompileInductive

inductive Formula : Type
  | pred_const_ : String → List String → Formula
  | pred_var_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  | def_ : String → List String → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula

structure Definition : Type :=
(name : String)
(args : List String)
(q : Formula)
deriving DecidableEq

abbrev Env : Type := List Definition

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

def Function.updateListIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β) :
  List α → List β → α → β
  | x::xs, y::ys => Function.updateIte (Function.updateListIte f xs ys) x y
  | _, _ => f


structure Interpretation (D : Type) : Type :=
  (nonempty : Nonempty D)
  (pred_const_ : String → (List D → Prop))
  (pred_var_ : String → (List D → Prop))

abbrev VarAssignment (D : Type) : Type := String → D

def Holds
  (D : Type)
  (I : Interpretation D)
  (V : VarAssignment D) : Env → Formula → Prop
  | _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | _, eq_ x y => V x = V y
  | _, true_ => True
  | _, false_ => False
  | E, not_ phi => ¬ Holds D I V E phi
  | E, imp_ phi psi =>
    Holds D I V E phi → Holds D I V E psi
  | E, and_ phi psi =>
    Holds D I V E phi ∧ Holds D I V E psi
  | E, or_ phi psi =>
    Holds D I V E phi ∨ Holds D I V E psi
  | E, iff_ phi psi =>
    Holds D I V E phi ↔ Holds D I V E psi
  | E, forall_ x phi =>
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | E, exists_ x phi =>
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | [], def_ _ _ => False
  | d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ E phi => (E, phi)

[Kayla Thomas]

Hmm. You have abbrev VarAssignment (D : Type) : Type := String → D where I have def VarAssignment (D : Type) : Type := String → D.

[Kayla Thomas]

but that doesn't seem to be it.

[Kayla Thomas]

hmm. your code works for me.

[François G. Dorais]

Ah! Yes, I forgot I did that. The one you need is for Env though, just make that an abbrev or a @[reducible] def and it will work.

[Kayla Thomas]

Ok, yes, that does it.

[François G. Dorais]

abbrev is probably better, it's basically the same as @[reducible,inline] but the inline part is irrelevant in this case so whatever...

[Kayla Thomas]

I guess the question is now, what is going on with the import Mathlib.Data.List.Basic.

[François G. Dorais]

Yes! Please send a bug report! Link to this discussion and include the last mwe.
I suspect it's a bad simp lemma. That happens all the time, but there's some simp experts maintaining mathlib that can fix that way better than we could!

[Kayla Thomas]

Ok. Thank you!!

[François G. Dorais]

Thank _you_! This was fun!

[Kayla Thomas]

https://github.com/leanprover-community/mathlib4/issues/5788