The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

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