Stream: Coq users

Topic: Help with syntax

Mycroft92 (Jan 30 2023 at 12:48):

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.

Ali Caglayan (Jan 30 2023 at 12:53):

That means apply the eliminator to only PRE and the goal. A , B |- C is meant to reference the hypotheses and goal.

Mycroft92 (Jan 30 2023 at 12:57):

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

Ali Caglayan (Jan 30 2023 at 12:58):

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.

Mycroft92 (Jan 30 2023 at 13:01):

I was confused because in this proof, the in PRE |-* clause has no effect and can safely be elided. Thanks again for the help.

Meven Lennon-Bertrand (Jan 30 2023 at 13:29):

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.

Meven Lennon-Bertrand (Jan 30 2023 at 13:31):

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.

Meven Lennon-Bertrand (Jan 30 2023 at 13:31):

Probably in your case generalizing over PRE is actually useless

Mycroft92 (Jan 30 2023 at 15:55):

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: Apr 16 2024 at 14:02 UTC