The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I would use "inversion H1", which should determine that re_matches_cat is the only applicable constructor, and add

s1 : string

s2 : string

H2 : re_matches r' s1

H3 : re_matches r'' s2

to the context, along with probably some equality hypotheses.  (The exact names it creates might be different.)
--

Daniel Schepler

On Thu, Nov 7, 2013 at 10:01 AM, Marcus Ramos <marcus.ramos AT univasf.edu.br> wrote:

Hi,

Thanks to previous suggestions, I am now using the inductive proposition below:

Inductive re_matches: re ->  string ->  Prop:=

   | re_matches_eps: re_matches re_eps ""

   | re_matches_sym: forall c: ascii, re_matches (re_sym c) (chr_to_str c)

   | re_matches_cat: forall r1 r2: re, forall s1 s2: string, re_matches r1 s1 -> re_matches r2 s2 -> re_matches (re_cat r1 r2) (s1++s2)

   | re_matches_uni_l: forall r1 r2: re, forall s: string, re_matches r1 s -> re_matches (re_uni r1 r2) s

   | re_matches_uni_r: forall r1 r2: re, forall s: string, re_matches r2 s -> re_matches (re_uni r1 r2) s

   | re_matches_clo_n: forall r: re, re_matches (re_clo r) ""

   | re_matches_clo_c: forall r: re, forall s1 s2: string, re_matches r s1 -> re_matches (re_clo r) s2 -> re_matches (re_clo r) (s1++s2).

and now I have the following situation in my demonstration of "re_fa_equiv":

2 subgoal

r' : re

r'' : re

a'0 : f_automata

a''0 : f_automata

H : re_fa_equiv r' a'0

H0 : re_fa_equiv r'' a''0

s : string

H1 : re_matches (re_cat r' r'') s

______________________________________(1/2)

fa_belongs s (fa_cat a'0 a''0) = true

______________________________________(2/2)

fa_belongs s (fa_cat a'0 a''0) = true -> re_matches (re_cat r' r'') s

Does anybody have an idea of how I can split "s" into "s1++s2" in hypothesis H1, so that I can then apply the constructor "re_matches_cat" to it?

Thanks in advance,

Marcus.