The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Amin,

thanks, this works! I thought I tried this, but looks like I had some typo in 
it.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Amin Timany
Sent: Tuesday, July 15, 2014 10:17 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] assert in a ltac match

Hi Michael,

One way to do this is by using "assert by", as you mentioned. But what 
follows the "by" must be a complete proof. Furthermore, note that the ";" 
operator has a higher precedence in parsing than "by" in "assert by" clause. 
As a result, you have to use parentheses to override the precedence. 
Therefore, the following ltac should work:

match goal with
   H1: (?a->?b) /\ (_->_), H2: ?a |- _ =>  assert(b) by (apply H1; exact H2)  
end.

Regards,
Amin

On 15 Jul 2014, at 10:03, 
michael.soegtrop AT intel.com
 wrote:

> Dear Coq users,
> 
> I want to do an assert as result of a ltac match and immediaetly 
> resolve it with hypothesis I found in the match, but somehow I can't 
> find the right syntax. Please have a look at the example below:
> 
> Parameter A B C D E: Prop.
> 
> Lemma Test1: A -> (A->B) /\ (C->D) -> E.
> Proof.
>  intros.
>  match goal with
>    H1: (?a->?b) /\ (_->_), H2: ?a |- _ =>  assert(b)  end.
> 
> I want to resolve the assert by applying H1 and H2, but chaining with 
> ; doesn't work for assert, because the chained tactics still apply to 
> the goal before the assert was issued and not the goal created by the 
> assert. assert seems to require . but this doesn't work in a match.
> 
> Also I can't get this to work with variations of assert by H1;H2.
> 
> I frequently do somethign like assert(AH:=H1 H2), but this doesn't 
> work cause of the conjunction in this case. Is there a way to get e.g. 
> the left part of
> H1 on the fly (without doing an inversion).
> 
> What does work is doing an inversion on H1, match HL with the left 
> part of H1 and use assert(AH:=HL H2), but this is way complicated. 
> Also in the actual case there are quantifiers in the hypothesis, so that 
> inversion doesn't work.
> 
> What is the best way of doing this?
> 
> Thanks & best regards,
> 
> Michael