The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

You are right. I used to converse lemma and managed to complete the proof. Thanks a lot.

Marcus.

2013/11/12 Laurent Théry <Laurent.Thery AT inria.fr>

On 11/12/2013 03:07 PM, Marcus Ramos wrote:

Hi,

In the proof state below:

1 subgoals

r' : re

r'' : re

a' : f_automata

a'' : f_automata

H : re_fa_equiv_concept r' a' /\ re_fa_equiv_concept r'' a''

s : string

H0 : fa_belongs_p s (fa_uni a' a'')

______________________________________(1/1)

re_matches r' (Some s) \/ re_matches r'' (Some s)

where:

Lemma fa_uni_str: 

      forall s: string, 

      forall a1 a2: f_automata, 

      (fa_belongs_p s a1) \/ (fa_belongs_p s a2) -> (fa_belongs_p s (fa_uni a1 a2)).

I want to add to the context the new hypothesis H1: (fa_belongs_p s a') \/ (fa_belongs_p s a'') (assumptions of the lemma above).

However, Coq does not accept the tactic "apply (fa_uni_str s a' a'') in H0" ("Unable to unify"). What is wrong? How can this be done?

Apply in an assumption works the other way around if you have H0 : A and H1 : A -> B

apply H1 in H0 gives you H0 : B.

--
Laurent

Thank you.

Marcus.