The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I won’t try to give an answer, simply tell that "assert (H0: A); let H1:=fresh in let H2:=fresh in destruct H as [H1 H2]; exact H1" cannot do what you wanted:

assert (H0:A)

creates a new branch (…⊢A) and extend the old one with "H0:A", then ';' tells to run the remaining of the script on both branches.
So, unless your initial goal was "A", "exact H1" will succeed with the new branch, but fail on the old one, resulting in a failure of the tactic.

"assert (H0: A); [let H1:=fresh in let H2:=fresh in destruct H as [H1 H2]; exact H1|]" would have been a better attempt.
This can be improved by removing declaration of the unrequired H2:
"assert (H0: A); [let H1:=fresh in destruct H as [H1 _]; exact H1|]".

Eventually, I would even rewrite this part as
"assert(H0 := (let (H1,_) := H in H1) : A)." (yes, in this case, the "let H1 := fresh in" is not required anymore)
or
"assert(H0 := (fst H) : A)."

For the rest of the syntax, see Théry’s answer.

2013/10/30 Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>

Hi!

I'm new to Ltac and I'm trying to define a tactic that will take a hypothesis name as an argument, match the formula/type of this hypothesis and then do something with the parts that have been matched.

Here is a concrete minimal (and kind-of dumb-looking) example of the kind of tactic I would like to write:

Ltac my_and_elimination H H0 := match goal with
     | [ H: ?A /\ ?B |- _ ] => assert (H0: A); let H1:=fresh in let H2:=fresh in destruct H as [H1 H2]; exact H1
end.






I know this is wrong (it doesn't behave as expected in my proof scripts). The question is: how could I do it correctly?

Best regards,

Bruno

--
.../Sedrikov\...