Add examples for destruct and using destruct to do split or constructor in a hypothesis #21021
Conversation
constructor in a hypothesis
coqbot-app
bot
added
the
needs: full CI
| which can result in more than one success (e.g. for `\\/`) when using | ||
| backtracking tactics such as `constructor; ...`. See :tacn:`ltac-seq`. | ||
|
|
||
| To use :n:`constructor` on a hypothesis :n:`H`, use :tacn:`destruct` :n:`H`. |
There was a problem hiding this comment.
This makes no sense, to "use a constructor on a hypothesis", you use apply c in H and this has no connection to destruct. I assume this was written to mirror split, but this doesn't feel needed and would feel more confusing than anything.
There was a problem hiding this comment.
This makes no sense, to "use a constructor on a hypothesis", you use apply c in H and this has no connection to destruct
You added "a", which changes the meaning. I am referring to the 'constructor' tactic. 'constructor'' doesn't require specifying 'c', which may be useful if you're using 'auto''.
There was a problem hiding this comment.
I should have said "to use constructor on a hypothesis", but the rest of the sentence still holds.
You can't use constructor on a hypothesis, its reasonable semantics is apply c in H which is the best way to do it (and barely makes sense since "applying constructor to a hypothesis" barely makes sense by itself), and most importantly none of this has anything to do with using destruct.
| typically used to split conjunctions in the conclusion such as `A /\\ B` into | ||
| two new goals `A` and `B`. | ||
|
|
||
| To :n:`split` a hypothesis :n:`H`, use :tacn:`destruct` :n:`H`. |
There was a problem hiding this comment.
It is too confusing to tell newcomers that we "split" hypotheses; I could see such a sentence if it said
To split a conjunction in a hypothesis :n:`H` instead of the conclusion, use :tacn:`destruct` :n:`H`.
| .. example:: Using :tacn:`destruct` on the conclusion | ||
|
|
||
| Creates a subgoal for each constructor, substituting the constructor | ||
| into the conclusion. | ||
|
|
||
| .. rocqtop:: reset none | ||
|
|
||
| Goal forall m n: nat, m + n = n + m. | ||
|
|
||
| .. rocqtop:: out | ||
|
|
||
| intros. | ||
|
|
||
| .. rocqtop:: all | ||
|
|
||
| destruct n. (* n is an inductive *) | ||
| .. _example_split_hypothesis: | ||
|
|
||
| .. example:: Using :tacn:`destruct` on a hypothesis | ||
|
|
||
| This gives the effect of a :tacn:`split` or :tacn:`constructor` on the | ||
| hypothesis. Creates hypotheses for each constructor of the head constant. | ||
|
|
||
| .. rocqtop:: reset none | ||
|
|
||
| Goal forall A B: Prop, A /\ B -> True. | ||
|
|
||
| .. rocqtop:: out | ||
|
|
||
| intros. | ||
|
|
||
| .. rocqtop:: all | ||
|
|
||
| destruct H. (* H is a hypothesis *) |
There was a problem hiding this comment.
There is no practical difference between "destruct on the conclusion" and "destruct on a hypothesis" since the former is really impossible, you need to destruct a hypothesis or a term constructed from hypotheses.
Here, the difference is really between using destruct on a dependent premise (example 1) or a non-dependent premise (example 2).
As said above, I can't see any way in which this resembles constructor, and it can resemble "a split" (not split) if the hypothesis is a conjunction, but it's way more general.
|
Hi @yannl35133, I think this revised version will be more to your liking. Let me know what you think. |
No description provided.