The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, November 09, 2013 01:18:05 PM Marcus Ramos wrote:
> 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.

I guess it would depend on the definition of fa_cat.  Let's suppose, for 
simplicity, that you were first compiling a regex to a nondeterministic 
finite 
automaton with a single accepting state, with the possibility of edges which 
can be traversed without consuming a symbol.  (With the intention of 
subsequently feeding that into the algorithm to transform into a 
deterministic 
finite automaton.)  In that context, fa_cat would be the operation of taking 
the disjoint union of the two nd automata and adding a nonconsuming edge from 
the accepting state of the first to the initial state of the second, setting 
the initial state of the result to the initial state of the first and the 
accepting state of the result to the accepting state of the second.

Then you'd need to prove, by induction on the path (or by induction on an 
inductive reachability predicate), that if a state n is reachable from the 
initial state with s consumed, then:
if n is in the first automaton, then n is reachable within the first 
automaton 
with s consumed;
if n is in the second automaton, then s can be split into s' and s'' where 
the 
first automaton accepts s', and n is reachable within the second automaton 
with 
s'' consumed.
So in Coq terms, that would look something like:
forall (n : fa_states (fa_cat a1 a2)) (s : string), 
fa_state_reachable_consuming (fa_cat a1 a2) n s ->
match n with
| inl n1 => fa_state_reachable_consuming a1 n1 s
| inr n2 => exists (s' s'':string), s = s' ++ s'' /\
    fa_belongs_p s' a1 /\
    fa_state_reachable_consuming a2 n2 s''
end.
This should be fairly easy to prove by induction on the 
fa_state_reachable_consuming hypothesis, with the most "interesting" case 
being traversing the added edge to move from the inl case to the inr case.
-- 
Daniel Schepler