# Zulip Chat Archive

## Stream: lean4

### Topic: tactic to equate inductive indices

#### Jakob von Raumer (Feb 04 2021 at 11:17):

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 (Feb 04 2021 at 13:18):

Note that if you start with `apply a`

, you don't need to worry about elimination into `Prop`

any more

#### Eric Wieser (Feb 04 2021 at 13:19):

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

#### Eric Wieser (Feb 04 2021 at 13:19):

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 (Feb 04 2021 at 13:20):

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 (Feb 04 2021 at 13:21):

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

#### Jakob von Raumer (Feb 04 2021 at 13:31):

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 (Feb 04 2021 at 17:07):

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 (Feb 04 2021 at 20:57):

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

#### Jakob von Raumer (Feb 04 2021 at 20:58):

I could call it `clarifyIndices`

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

#### Jakob von Raumer (Feb 07 2021 at 13:11):

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 (Feb 11 2021 at 11:31):

... 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 (Feb 11 2021 at 11:42):

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 (Feb 11 2021 at 14:41):

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.

Last updated: May 18 2021 at 22:15 UTC