Termination failure on FPIL Sect. 9 exercise

Stream: new members

[mars0i]

One of FPIL section 9's exercise says to "Prove plusR_succ_left using the induction ... with tactic." I am confused about whether I've successfully done the exercise. I think I haven't, but I don't understand what the problem is. Here's the relevant code:

def Nat.plusR : Nat → Nat → Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

set_option trace.Meta.Tactic.simp.rewrite true

def plusR_succ_left (n : Nat) : (k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1 :=  by
induction n with
  | zero => simp [plusR_succ_left] -- works for induction on n (not k)
  | succ n ih => simp [plusR_succ_left]

This produces the following error on the first line of the definition of plusR_succ_left:

▶ 363:5-363:20: error:
fail to show termination for
  plusR_succ_left
with errors
failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    plusR_succ_left 0 k


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
n✝ : Nat
a✝ : ∀ (y : Nat),
  (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y n✝ → ∀ (k : Nat), Nat.plusR (y + 1) k = Nat.plusR y k + 1
n : Nat
⊢ n < n✝

However, I get goals accomplished 🎉 after each of the simp lines, and according to my (perhaps incorrect) understanding of the trace output, it shows that each of the cases is proven:

case zero
⊢ ∀ (k : Nat), Nat.plusR (0 + 1) k = Nat.plusR 0 k + 1

▶ 364:13-364:35: information:
[Meta.Tactic.simp.rewrite] Nat.zero_add:1000, 0 + 1 ==> 1

[Meta.Tactic.simp.rewrite] plusR_succ_left:1000, Nat.plusR 1 k ==> Nat.plusR 0 k + 1

[Meta.Tactic.simp.rewrite] eq_self:1000, Nat.plusR 0 k + 1 = Nat.plusR 0 k + 1 ==> True

[Meta.Tactic.simp.rewrite] implies_true:1000, Nat → True ==> True

And:

case succ
n : Nat
ih : ∀ (k : Nat), Nat.plusR (n + 1) k = Nat.plusR n k + 1
⊢ ∀ (k : Nat), Nat.plusR (n + 1 + 1) k = Nat.plusR (n + 1) k + 1

▶ 365:18-365:40: information:
[Meta.Tactic.simp.rewrite] plusR_succ_left:1000, Nat.plusR (n + 1 + 1) k ==> Nat.plusR (n + 1) k + 1

[Meta.Tactic.simp.rewrite] plusR_succ_left:1000, Nat.plusR (n + 1) k ==> Nat.plusR n k + 1

[Meta.Tactic.simp.rewrite] eq_self:1000, Nat.plusR n k + 1 + 1 = Nat.plusR n k + 1 + 1 ==> True

[Meta.Tactic.simp.rewrite] implies_true:1000, Nat → True ==> True

I understand the idea of failure of termination, but I'm confused about what the error message is telling me. "Cannot use parameter n" in what sense? What is wrong with the recursion?

[Ruben Van de Velde]

What this seems to be saying is "yes, you've proved each case, but only by assuming your conclusion in the first place". It also seems like you're not using your induction hypothesis ih, which also indicates something has gone wrong

[mars0i]

Thanks @Ruben Van de Velde. That makes sense. That seems like the tip I needed. Obvious now that you say it, but it wasn't before, for me.