The Coq mailing list

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

Hi,

I advanced the demonstration a little bit, but I am stuck again. In the previous situation, I used "inversion H1" to split "s" into "s1+s2" in the goal. Now I have the same situation, but can´t use "inversion" anymore (I guess):

1 subgoals

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 : fa_belongs_p s (fa_cat a'0 a''0)

______________________________________(1/1)

re_matches (re_cat r' r'') s

Any ideas on how to fix it? In other words, how can I apply the "re_matches_cat" constructor below to the current goal?

Thanks a lot,

Marcus.

2013/11/7 Marcus Ramos <marcus.ramos AT univasf.edu.br>

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.