The Coq mailing list

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

Thank you very much, Daniel and Auger. Your comments were very helpful.

Regards,

Marcus.

2013/11/7 AUGER Cédric <sedrikov AT gmail.com>

Le Thu, 7 Nov 2013 16:01:54 -0200,

Marcus Ramos <marcus.ramos AT univasf.edu.br> a écrit :

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

Daniel answered using inversion. If you want to see the low level way
to do it, try:

revert H0; revert H; revert H1.
change (re_matches (re_cat r' r'') s ->
  match re_cat r' r'' with
  | re_cat r' r'' => re_fa_equiv r' a'0 -> re_fa_equiv r'' a''0 ->

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

  | _ => True end).
generalize (re_cat r' r'').
intros re Hre.

And now, the magic part:

destruct Hre. (* case Hre. should also work *)

You should get 7 goals, with 6 of them solvable with "split.", and the
last one being what you want. It is not exactly what inversion does
(inversion is not that efficient, but the result is more or less the
same), still it can be helpfull to understand what kind of tricks one
can rely on in Coq.