Created
July 23, 2017 01:00
-
-
Save palmskog/0477cbf8c8c90d0fa2b92e0358fbc4da to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Ascii. | |
Require Import String. | |
Open Scope string_scope. | |
Inductive regexp := | |
| regexp_zero : regexp | |
| regexp_unit : regexp | |
| regexp_char (c:ascii) | |
| regexp_plus (r:regexp) (r':regexp) | |
| regexp_times (r:regexp) (r':regexp) | |
| regexp_star (r:regexp). | |
Inductive s_in_regexp_lang : string -> regexp -> Prop := | |
| s_in_regexp_lang_unit : | |
s_in_regexp_lang "" regexp_unit | |
| s_in_regexp_lang_char : forall (a5:ascii), | |
s_in_regexp_lang (String a5 "") (regexp_char a5) | |
| s_in_regexp_lang_plus_1 : forall (s5:string) (r1 r2:regexp), | |
s_in_regexp_lang s5 r1 -> | |
s_in_regexp_lang s5 (regexp_plus r1 r2) | |
| s_in_regexp_lang_plus_2 : forall (s5:string) (r1 r2:regexp), | |
s_in_regexp_lang s5 r2 -> | |
s_in_regexp_lang s5 (regexp_plus r1 r2) | |
| s_in_regexp_lang_times : forall (s5 s':string) (r1 r2:regexp), | |
s_in_regexp_lang s5 r1 -> | |
s_in_regexp_lang s' r2 -> | |
s_in_regexp_lang ( s5 ++ s' ) (regexp_times r1 r2) | |
| s_in_regexp_lang_star_1 : forall (r:regexp), | |
s_in_regexp_lang "" (regexp_star r) | |
| s_in_regexp_lang_star_2 : forall (s5 s':string) (r:regexp), | |
s_in_regexp_lang s5 r -> | |
s_in_regexp_lang s' (regexp_star r) -> | |
s_in_regexp_lang ( s5 ++ s' ) (regexp_star r). | |
Lemma regexp_star_c_split : forall r' s' c, | |
s_in_regexp_lang (String c s') (regexp_star r') -> | |
exists s1 s2, s' = s1 ++ s2 /\ s_in_regexp_lang (String c s1) r' /\ s_in_regexp_lang s2 (regexp_star r'). | |
Proof. | |
Admitted. |
wilcoxjay
commented
Jul 23, 2017
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment