I am having a huge elim that looks like this:

```
Tactic Notation "SynTypeElim" ident(Γ) ident(t) ident(T):=
elim => {Γ t T} =>
[ Γ idx T Hdget HWfΓ
| Γ lvl HWfΓ
| Γ A B i j HtypeA IHA HtypeB IHB
| Γ A B t l HtypeA IHA Htypet IHt
| Γ A B m n Htypem IHm Htypen IHn
| Γ A B i j HtypeA IHA HtypeB IHB
| Γ m n A B i j HtypeA IHA HtypeB IHB Htypem IHm Htypen IHn
| Γ m A B Htypem IHm
| Γ m A B Htypem IHm
| Γ T T' t HtypeT IHT HconvTT'
].
```

What I want to do is something like this (except for I want it to work):

```
Tactic Notation "SynTypeElim" ident(Γ) ident(t) ident(T):=
elim => {Γ t T};
rewrite ?substE /=; (* note this line*)
move =>
[ Γ idx T Hdget HWfΓ
| Γ lvl HWfΓ
| Γ A B i j HtypeA IHA HtypeB IHB
| Γ A B t l HtypeA IHA Htypet IHt
| Γ A B m n Htypem IHm Htypen IHn
| Γ A B i j HtypeA IHA HtypeB IHB
| Γ m n A B i j HtypeA IHA HtypeB IHB Htypem IHm Htypen IHn
| Γ m A B Htypem IHm
| Γ m A B Htypem IHm
| Γ T T' t HtypeT IHT HconvTT'
].
```

I am not sure where to even look for that in the man pages.

https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Rewrite.20in.20existential has an example

See the !inE part. Note it needs mathcomp not just ssreflect, IIRC

Hmm, /[!inE] I guess, or /[!substE]. (I'd have to try to be sure)

wow what are the chances, it literally the last question

it is more pain to work with than I thought, now I have to rewrite under binders. because this is generalized induction principle.

rewrites never would have worked

Ah, you'd have to introduce the binders first

FWIW, ssreflect IMHO isn't quite focused at "inductive proofs on large inductives", but then it's reasonable to supplement it with ltac automation, such as `rewrite -> substE in *`

, hoping that works

At least it gained block introductions, `elim => [^ prefix]`

(IIRC)

I am not even sure if `rewrite`

works the problem is induction hypothesis comes in form of `forall X Y ..., subst(x, y ...)`

So what I would need is setoid rewrite which I won't use here because it will make things very very slow.

rewrite can work, and there's a rule.

Say you want to rewrite foo to bar. Does foo mention X Y, or not? If not, you're fine. If yes, then you need something extra.

(either setoid_rewrite, or ssreflect over/under).

To check this rule, make sure to specialize your "foo" and "bar" to your goal first.

Here's where I should show an example, but I don't have one now.

no worries, I just went on with manual rewrites after specialization when needed! that should do for now

Last updated: Jul 15 2024 at 20:02 UTC