Termination of head induction on `ReflTransGen`

Stream: new members

[rami3l]

Hi! It's me (again)!

This time I'm trying to recursively prove a property on a Relation.ReflTransGen and I'm stuck with showing termination with head induction (instead of the default tail induction).

In the following #mwe I'll use GE.ge as the relation in question to show the basic structure of my proof, so the example might look a bit dumb. Anyway, I believe this problem is not specific to one relation.

import Mathlib.Tactic

abbrev GEs : ℕ → ℕ → Prop := Relation.ReflTransGen GE.ge

theorem test {m n'} (mn' : GEs m n') : GEs (m - n') 0
:= open Relation.ReflTransGen in by
  cases mn' using head_induction_on with
  | refl => simp; rfl
  | head mm' m'n' =>
    rename_i m' f
    refine head ?_ (test m'n')
    exact Nat.sub_le_sub_right mm' n'

This gives

fail to show termination for
  test
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    test m'n'

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    test m'n'

structural recursion cannot be used

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

• I'm not sure if cases mn' using head_induction_on with is the right way to tell lean that I want to use head induction on this one, but it seems to typecheck anyway.
• My intuition is that in the head mm' m'n' case, m'n' is "smaller than" mn' (the former is then passed to test), so we should be able to prove termination... But how?

Thanks a lot!

[rami3l]

Every time I encountered such problems, I always resorted to using Types instead of Props, and the termination check "just worked".
However this does make me feel bad because I miss all the niceties in mathlib... Am I doing something wrong?

[rami3l]

Okay, it looks like induction _ generalizing _ with can be used instead of match/cases when there's no mutual recursion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20How.20to.20show.20termination.20here.3F/near/366288337

[Kyle Miller]

@rami3l Yeah, induction is the way to go here:

open Relation.ReflTransGen in
theorem test {m n'} (mn' : GEs m n') : GEs (m - n') 0 := by
  induction mn' using head_induction_on with
  | refl => simp; rfl
  | head mm' _ ih =>
    rename_i m' f
    refine head ?_ ih
    exact Nat.sub_le_sub_right mm' n'

[rami3l]

@Kyle Miller Thanks a lot!

I think I can close this thread now (but it seems that I have no permission to do so)...

[Kevin Buzzard]

Please don't close threads. It breaks things like linkifiers and serves no useful purpose.

[rami3l]

@Kyle Miller Now that we are here, would you mind having a look at how to show termination in another pretty self-contained example? :pray:

import Mathlib.Tactic

namespace Denotational

-- https://plfa.github.io/Denotational/#values
inductive Value : Type where
/-- No information is provided about the computation. -/
| bot : Value
/-- A single input-output mapping, from the first term to the second. -/
| fn : Value → Value → Value
/-- A function that maps inputs to outputs according to both terms. -/
| conj : Value → Value → Value

instance : Bot Value where bot := .bot
instance : Sup Value where sup := .conj
infixr:70 " ⇾ " => Value.fn

/-- `Sub` adapts the familiar notion of subset to the `Value` type. -/
inductive Sub : Value → Value → Prop where
| bot : Sub ⊥ v
| conjL : Sub v u → Sub w u → Sub (v ⊔ w) u
| conjR₁ : Sub u v → Sub u (v ⊔ w)
| conjR₂ : Sub u w → Sub u (v ⊔ w)
| trans : Sub u v → Sub v w → Sub u w
| fn : Sub v' v → Sub w w' → Sub (v ⇾ w) (v' ⇾ w')
| dist : Sub (v ⇾ (w ⊔ w')) ((v ⇾ w) ⊔ (v ⇾ w'))

infix:40 " ⊑ " => Sub
instance : Trans Sub Sub Sub where trans := .trans

def conj_sub₁ : u ⊔ v ⊑ w → u ⊑ w := by intro
| .conjL h _ => exact h
| .conjR₁ h => refine .conjR₁ ?_; exact conj_sub₁ h
| .conjR₂ h => refine .conjR₂ ?_; exact conj_sub₁ h
| .trans h h' => refine .trans ?_ h'; exact conj_sub₁ h
/-
fail to show termination for
  Denotational.conj_sub₁
with errors
argument #3 was not used for structural recursion
  failed to eliminate recursive application
    conj_sub₁ h

structural recursion cannot be used

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

Again, changing Prop to Type just works, but I doubt if there is a more idiomatic way of doing this :thinking:

[Kyle Miller]

@rami3l The answer again is to use induction, though this one needs another trick because the induction tactic doesn't want to apply to h directly due to the indices to Sub not being variables. You can use the generalize tactic to replace u ⊔ v with a fresh variable and to generate an equality for it, and then induction carries through. There's also some syntax in induction where you can give a tactic that should run in all cases first.

theorem conj_sub₁ (h : u ⊔ v ⊑ w) : u ⊑ w := by
  generalize hx : u ⊔ v = x at *
  induction h with subst_vars
  | bot => cases hx
  | conjL h1 => cases hx; exact h1
  | conjR₁ h ih => exact .conjR₁ (ih rfl)
  | conjR₂ h ih => exact .conjR₂ (ih rfl)
  | trans h h' ih => exact .trans (ih rfl) h'
  | fn => cases hx
  | dist => cases hx

[Kyle Miller]

Oh, I guess you can put try cases hx into that too to eliminate some cases, and then it's looking a lot like your recursive version:

theorem conj_sub₁ (h : u ⊔ v ⊑ w) : u ⊑ w := by
  generalize hx : u ⊔ v = x at *
  induction h with (subst_vars; try cases hx)
  | conjL h1 => exact h1
  | conjR₁ h ih => exact .conjR₁ (ih rfl)
  | conjR₂ h ih => exact .conjR₂ (ih rfl)
  | trans h h' ih => exact .trans (ih rfl) h'

[rami3l]

@Kyle Miller Thanks a lot! You made my day! :congratulations:

[Daniel Fabian]

on this one, I wonder if anything was refactored on the structural recursion or if it's another case where backwards-chaining is not sufficient to solve the goal.

Do we happen to have traces for this case?