The Coq mailing list

[<michael.soegtrop AT intel.com>]

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