Stream: Coq users

Topic: ✔ rewriting in the presence of universal quantifiers


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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