Can someone help me understand this syntax? I can't find it on reference manual.

` induction a as [ x ] in PRE |- * using Acc_inv_dep. `

specificaly the `|-`

part.

That means apply the eliminator to only PRE and the goal. `A , B |- C`

is meant to reference the hypotheses and goal.

Thanks Ali, essentially the plain induction is just `induction ident in * |- *.`

right?

I think it is a bit more complicated than that. For example, sometimes you have to revert goals to get a more general ind hyp. So I don't think it is just that.

I was confused because in this proof, the `in PRE |-*`

clause has no effect and can safely be elided. Thanks again for the help.

I think plain induction is rather `induction ident in |- *`

, while adding hypothesis before the turnstile lets you generalize your induction hypothesis with respect to those. For instance, say you want to prove `forall x y : nat, R x y -> R' x y`

, and you start by `intros x y H.`

. If you use `induction x`

(or `induction x as [| n IH] in |- *`

), then your induction hypothesis will be of type `R' n y`

. If instead you use `induction x as [|n IH] in y, H |- *`

, then your induction hypothesis will instead be of type `forall y, R n y -> R' n y`

.

Basically, this is a shortcut for the very common pattern of reverting/generalizing some hypothesis, using induction, and then introducing the things you reverted again.

Probably in your case generalizing over `PRE`

is actually useless

Meven Lennon-Bertrand said:

I think plain induction is rather

`induction ident in |- *`

, while adding hypothesis before the turnstile lets you generalize your induction hypothesis with respect to those. For instance, say you want to prove`forall x y : nat, R x y -> R' x y`

, and you start by`intros x y H.`

. If you use`induction x`

(or`induction x as [| n IH] in |- *`

), then your induction hypothesis will be of type`R' n y`

. If instead you use`induction x as [|n IH] in y, H |- *`

, then your induction hypothesis will instead be of type`forall y, R n y -> R' n y`

.

Thanks that explanation was really helpful.

Last updated: Jun 16 2024 at 02:41 UTC