tactic to equate inductive indices

Stream: lean4

[Jakob von Raumer]

I kind of need a tactic that automates the following: Suppose I have some inductive predicate with more than one constructor. Then, the predicate only eliminates into Prop. But oftentimes, because one or more of the indices already determine the constructor, I can pin down the remaning indices as well, like in the following example:

inductive Foo : (n : Nat) → Fin n → Prop
| mk1 : Foo 5 0
| mk2 : Foo 8 3

example (x : Fin 5) (p : Foo 5 x) (A : Type) (a : x ≤ 2 → A) : A := by
  have e : 0 = x := by { cases p; rfl }
  induction e
  exact a rfl

Does anyone know a tactic (maybe also in Lean 3, so I could port it) that takes p as input and automates the first two lines of this proof? I think the equalities needed are actually generated in Lean.Meta.Tactic.Cases...
(I think I asked a similar question to @Jannis Limperg before...)

[Eric Wieser]

Note that if you start with apply a, you don't need to worry about elimination into Prop any more

[Eric Wieser]

You also get a definition that's way easier to write proofs about

[Eric Wieser]

Lean3, but:

inductive Foo : Π (n : nat), fin n → Prop
| mk1 : Foo 5 0
| mk2 : Foo 8 3

def foo1 (x : fin 5) (p : Foo 5 x) (A : Type) (a : x ≤ 2 → A) : A := by {
  have e : 0 = x := by { cases p, refl },
  subst e,
  exact a (nat.zero_le _),
}

def foo2 (x : fin 5) (p : Foo 5 x) (A : Type) (a : x ≤ 2 → A) : A := by {
  apply a,
  cases p,
  exact nat.zero_le _,
}

Compare #print foo1 with #print foo2

[Jakob von Raumer]

Eric Wieser said:

Note that if you start with apply a, you don't need to worry about elimination into Prop any more

Well yea, the situation above is just a minimal example I came up with.

[Jakob von Raumer]

(I'm also not needing this to write a manual proof but to base other tactics on it)

[Jakob von Raumer]

This might be an example where the equality proof a bit more necessary:

example (x : Fin 5) (p : Foo 5 x) (B : ∀ n, Fin n → Type) (b : B 5 x)
  (A : Type) (a : B 5 0 → A) : A := by
  have e : 0 = x := by { cases p; rfl }
  induction e
  apply a b

[Jannis Limperg]

I'm not aware of a tactic that would do this for you, though as you say, cases does something similar. Afaict, the tactic you want wouldn't be super hard to write in principle, but it would be a fair amount of busywork.

[Jakob von Raumer]

I guess I'll tackle it tomorrow, going off the def of generalizeIndices

[Jakob von Raumer]

I could call it clarifyIndices or something, I think there might be quite some situations where it's useful

[Jakob von Raumer]

For future reference, I've implemented this now. The tactic "clarifies" free variable in the indices of instances of inductive propositions if there is exactly one matching constructor, or proves the target via False if there is no matching case https://github.com/javra/iit/blob/main/IIT/ClarifyIndices.lean

[Jakob von Raumer]

... and, in a similar fashion, here's an inversion tactic which, for a free variable of an inductive proposition, introduces the Prop sorted constructor fields, if there's a unique match: https://github.com/javra/iit/blob/main/IIT/PropInversion.lean. Example:

inductive Foo : Nat → Nat → Prop
| mk1 : Foo 5 3
| mk2 : Foo 3 3 → Foo 9 8 → (n : Nat) → Foo 1 2

def bar (n : Nat) (x : Foo 1 n) (A : Type) (p : Foo 9 8 → A) : A := by
  inversion x
  apply p
  assumption

[Eric Wieser]

Can you come up with a more compelling example? Again, cases works fine there in lean 3:

inductive Foo : nat → nat → Prop
| mk1 : Foo 5 3
| mk2 : Foo 3 3 → Foo 9 8 → nat → Foo 1 2

def bar (n : nat) (x : Foo 1 n) (A : Type) (p : Foo 9 8 → A) : A := by {
  apply p,
  cases x,
  assumption, }

[Jakob von Raumer]

Ah, right, it's more useful in examples where you use the premise multiple times in the subsequent proof, and you want to avoid needing cases x later multiple times. The resulting proof term should be beta-equivalent to yours in the end.