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?

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`

.

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.

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 canalways`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?

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.
```

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.

Nicolas Rinaudo has marked this topic as resolved.

Last updated: Jun 18 2024 at 22:01 UTC