The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, November 09, 2013 03:27:54 PM Marcus Ramos wrote:
> Hi Daniel,
> 
> Thanks a lot for the hints, I was indeed planning to do something like that
> when it comes to prove the Lemma below. I still didn´t really know how to
> do that in Coq, but now you gave me good ideas for it:
> 
> Lemma fa_cat_str:
>       forall s1 s2: string,
>       forall a1 a2: f_automata,
>       (fa_belongs_p s1 a1) -> (fa_belongs_p s2 a2) -> (fa_belongs_p
> (s1++s2) (fa_cat a1 a2)).
> 
> However, my current plan is to transform "re_matches (re_cat r' r'') s"
> into "re_matches (re_cat r' r'') (s1++s2)", so that I could apply
> "re_matches_cat" and then get the subgoals "re_matches r' s1" and
> "re_matches r'' s2" which, with the help of the hypothesis and some other
> Lemmas, including the one above, I guess would enable me to finish the
> proof.
> 
> Thus, is there a way to introduce "s1++s2" in place of "s" in "re_matches
> (re_cat r' r'') s"? After this, I´ll turn into the demonstration of the
> Lemma abouve with your suggestions. Thanks again.
> 
> Marcus.

What I was describing was a step leading to more of a converse of your 
fa_cat_str as a special case:

Lemma fa_cat_str_conv:
  forall (s:string) (a1 a2:f_automata),
  fa_belongs_p s (fa_cat a1 a2) ->
  exists (s1 s2:string), s = s1 ++ s2 /\
    fa_belongs_p s1 a1 /\ fa_belongs_p s2 a2.

Then in the original goal

> > > 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

I would do something like

destruct (fa_cat_str_conv _ _ _ H1) as
  [s1 [s2 [? [? ?]]]].

which should transform the goal into something like

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)
s1 : string
s2 : string
H2 : s = s1 ++ s2
H3 : fa_belongs_p s1 a'0
H4 : fa_belongs_p s2 a''0
__________________________(1/1)
re_matches (re_cat r' r'') s

(Or actually, lately I've been leaning more towards defining a custom Prop 
equivalent to the "exists ..." conclusion of the above:

Inductive is_cat_of_belonging_strs (a1 a2:f_automata) : string -> Prop :=
| is_cat_of_belonging_strs_def : forall (s1 s2:string),
  fa_belongs_p s1 a1 -> fa_belongs_p s2 a2 ->
  is_cat_of_belonging_strs a1 a2 (s1 ++ s2).

That would have the slight advantage that if you make the conclusion of 
fa_cat_str_conv into "is_cat_of_belonging_strs a1 a2 s" then you will be able 
to just do
destruct (fa_cat_str_conv _ _ _ H1) as [s1 s2 ? ?].
and get directly:
...
s1 : string
s2 : string
H2 : fa_belongs_p s1 a'0
H3 : fa_belongs_p s2 a''0
___________________________(1/1)
re_matches (re_cat r' r'') (s1 ++ s2)

On the other hand, it's maybe a bit less clear to somebody new to Coq what 
is_cat_of_belonging_strs actually means...  But I do see this approach 
definitely being useful when it comes time to do the case of the Kleine star.)
-- 
Daniel Schepler