restricted induction

Stream: lean4

[Palalansoukî]

I'm considering using a special form of induction, but the induction tactic doesn't behave as expected, and I'm seeking advice. Since my current situation is complex (using more technical terms, I'm attempting to perform induction on a structure that is a model of restricted induction axioms like $I_\mathrm{open}$ and $I\Sigma_0$), to illustrate the issue, I provide a simpler example with a type N that has restricted induction:

import Init

axiom N : Type

axiom zero : N

axiom succ : N → N

axiom add : N → N → N

axiom add_zero : ∀ n : N, add n zero = n

axiom add_succ : ∀ n m : N, add n (succ m) = succ (add n m)

axiom succ_ne_zero : ∀ n : N, succ n ≠ zero

axiom Restriction : (N → Prop) → Prop

axiom restricted_induction {motive : N → Prop} (h : Restriction motive)
  (zero : motive zero) (succ : ∀ n, motive n → motive (succ n)) : ∀ n, motive n

Now, I want to prove n ≠ zero → add m n ≠ zero, but it results in an error.

example (n m : N) (h : n ≠ zero) : add m n ≠ zero := by
  /-
  tactic 'introN' failed, insufficient number of binders

  nm: N
  ⊢ Restriction fun n => n ≠ zero → add m n ≠ zero
  -/
  induction n using restricted_induction

Supplementing an term as an argument resolves this error, but I cannot establish the proof for the case when n = zero.

example (n m : N) (h : n ≠ zero) : add m n ≠ zero := by
  induction n, _ using restricted_induction
  · sorry
  · /-
      case zero
      n m : N
      h : n ≠ zero
      x✝ : ?m.190
      ⊢ add m zero ≠ zero
    -/
    -- we cannot prove this since there is no proof of zero ≠ zero
    sorry
  · sorry

While using revert h eliminates the error and allows the proof, doing this every time feels cumbersome, especially when there are many assumptions.

example (n m : N) (h : n ≠ zero) : add m n ≠ zero := by
  revert h
  induction n using restricted_induction
  · sorry
  · intro h; contradiction
  · intro h; rw [add_succ]; exact succ_ne_zero _

What would be the recommended approach in this situation? Should induction not be used in such cases?

[Kyle Miller]

It's cumbersome in a different way, but you could use refine, assuming your induction principle is tagged @[elab_as_elim] to get the elaborator to solve for the motive argument.

@[elab_as_elim]
axiom restricted_induction {motive : N → Prop} (h : Restriction motive)
  (zero : motive zero) (succ : ∀ n, motive n → motive (succ n)) : ∀ n, motive n

example (n m : N) (h : n ≠ zero) : add m n ≠ zero := by
  refine restricted_induction ?res ?zero ?succ n
  -- has three goals, `res`, `zero` and `succ`

[Palalansoukî]

It seems that this is not working well. In the generated zero goal, the n appearing in the assumption h should be rewritten to zero, but it is not, so it cannot be proven.

[Kyle Miller]

Ah, ok, you need to do the same revert/intro trick with refine too to get that to happen, so this is no better than what you have.

[Joachim Breitner]

One could argue that this is a bug in the induction tactic; it should only intro in cases where the motive is the conclusion of that case.

Maybe open an issue and we can see how often this comes up and whether induction should handle it, or whether these are too corner case and users just have to apply the lemma manually (revert + refine)

[Joachim Breitner]

Looking at the code a bit, I one possible fix would be to extend docs#Lean.Meta.Match.Alt with a field indicating whether this “alternative” as the motive as the result type, and then use that field in docs#Lean.Elab.Tactic.ElimApp.evalAlts to run

          (_, altMVarId) ← altMVarId'.introNP numGeneralized

only if it is set. Probably worth fixing.

[Palalansoukî]

Thanks. I opened the issue https://github.com/leanprover/lean4/issues/3212