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):

I made things complicated, sorry.
This induction n as [| n' IHn']; intros m. performs intros m on all generated subgoals.
To make things clearer please, consider instead:

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: Oct 13 2024 at 01:02 UTC