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