Stream: Coq users

Topic: ✔ rewriting in the presence of universal quantifiers

Nicolas Rinaudo (Aug 23 2023 at 07:02):

By "filling the holes", do you mean that Coq tries to find, in our example, all variables `x` and `y` such that there is an instance of `x + y` in the target?

And so, if I specify `add_comm n`, the first hole is already filled, and Coq will try to find all variables `x` such that there is an instance of `n + x` in the target, where `n` is fixed?

Pierre Rousselin (Aug 23 2023 at 07:02):

Nicolas Rinaudo said:

Pierre Rousselin said:

As a side remark, while having the most general induction hypothesis is a good habit, you don't lose anything if you `intros m` after `induction`.

I was not aware you could use `intros` right after `induction`! Thank you so much.

Ah, this is to do with `;`, isn't it? I'm technically not supposed to know about this yet, and will not pretend I understand how it works :)

No, nothing to do with `;`, please ignore it and replace it with `.`, you are right, it's best to learn about it later.
You can always `intros` when the goal has the form `forall ..., blah` or `A -> blah`.

Pierre Rousselin (Aug 23 2023 at 07:02):

Nicolas Rinaudo said:

By "filling the holes", do you mean that Coq tries to find, in our example, all variables `x` and `y` such that there is an instance of `x + y` in the target?

And so, if I specify `add_comm n`, the first hole is already filled, and Coq will try to find all variables `x` such that there is an instance of `n + x` in the target, where `n` is fixed?

exactly, except, it will not find all `x`, just the first one.

Nicolas Rinaudo (Aug 23 2023 at 07:14):

Pierre Rousselin said:

No, nothing to do with `;`, please ignore it and replace it with `.`, you are right, it's best to learn about it later.
You can always `intros` when the goal has the form `forall ..., blah` or `A -> blah`.

Really? After playing with it, I have the impression that `induction n as [| n' IHn']. intros m` will only introduce `m` in the first subgoal, which matches my current intuition for `;`. Am I missing something?

Pierre Rousselin (Aug 23 2023 at 07:23):

This `induction n as [| n' IHn']; intros m.` performs `intros m` on all generated subgoals.

``````Theorem plus_n_Sm :
forall n m : nat, S (n + m) = n + (S m).
Proof.
induction n as [| n' IHn'].
- intros m. reflexivity. (* ok by computation (definition of add) *)
- intros m. simpl. rewrite (IHn' m). (* specifying m make it match only LHS *)
reflexivity.
Qed.
``````

Nicolas Rinaudo (Aug 23 2023 at 07:26):

Thanks, that was a very helpful conversation. I've learned a lot - not necessarily understood everything, it'll take time to percolate, but it's definitely helping to improve my mental model.

Notification Bot (Aug 23 2023 at 07:26):

Nicolas Rinaudo has marked this topic as resolved.

Last updated: Jun 18 2024 at 22:01 UTC