# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223405535 14400
# Node ID 4a57a4922af5a072813dbae0cc3c6d495f2c7af1
# Parent  9b0d118abbc9e3add395fcbd7bb988744514d52e
Add star to regexp matcher; need to automate a bit more

diff -r 9b0d118abbc9 -r 4a57a4922af5 src/MoreDep.v
--- a/src/MoreDep.v	Tue Oct 07 10:50:36 2008 -0400
+++ b/src/MoreDep.v	Tue Oct 07 14:52:15 2008 -0400
@@ -349,13 +349,26 @@
 Require Import Ascii String.
 Open Scope string_scope.
 
+Section star.
+  Variable P : string -> Prop.
+
+  Inductive star : string -> Prop :=
+  | Empty : star ""
+  | Iter : forall s1 s2,
+    P s1
+    -> star s2
+    -> star (s1 ++ s2).
+End star.
+
 Inductive regexp : (string -> Prop) -> Type :=
 | Char : forall ch : ascii,
   regexp (fun s => s = String ch "")
 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
   regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
-  regexp (fun s => P1 s \/ P2 s).
+  regexp (fun s => P1 s \/ P2 s)
+| Star : forall P (r : regexp P),
+  regexp (star P).
 
 Open Scope specif_scope.
 
@@ -416,12 +429,12 @@
   induction s1; crush.
 Qed.
 
-Hint Rewrite substring_app_fst substring_app_snd using assumption : cpdt.
+Hint Rewrite substring_app_fst substring_app_snd using (trivial; fail) : cpdt.
 
 Section split.
   Variables P1 P2 : string -> Prop.
-  Variable P1_dec : forall s, {P1 s} + {~P1 s}.
-  Variable P2_dec : forall s, {P2 s} + {~P2 s}.
+  Variable P1_dec : forall s, {P1 s} + { ~P1 s}.
+  Variable P2_dec : forall s, {P2 s} + { ~P2 s}.
 
   Variable s : string.
 
@@ -453,6 +466,231 @@
 
 Implicit Arguments split [P1 P2].
 
+Lemma app_empty_end : forall s, s ++ "" = s.
+  induction s; crush.
+Qed.
+
+Hint Rewrite app_empty_end : cpdt.
+
+Lemma substring_self : forall s n,
+  n <= 0
+  -> substring n (length s - n) s = s.
+  induction s; substring.
+Qed.
+
+Lemma substring_empty : forall s n m,
+  m <= 0
+  -> substring n m s = "".
+  induction s; substring.
+Qed.
+
+Hint Rewrite substring_self substring_empty using omega : cpdt.
+
+Lemma substring_split' : forall s n m,
+  substring n m s ++ substring (n + m) (length s - (n + m)) s
+  = substring n (length s - n) s.
+  Hint Rewrite substring_split : cpdt.
+
+  induction s; substring.
+Qed.
+
+Lemma substring_stack : forall s n2 m1 m2,
+  m1 <= m2
+  -> substring 0 m1 (substring n2 m2 s)
+  = substring n2 m1 s.
+  induction s; substring.
+Qed.
+
+Ltac substring' :=
+  crush;
+  repeat match goal with
+           | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
+         end.
+
+Lemma substring_stack' : forall s n1 n2 m1 m2,
+  n1 + m1 <= m2
+  -> substring n1 m1 (substring n2 m2 s)
+  = substring (n1 + n2) m1 s.
+  induction s; substring';
+    match goal with
+      | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
+        replace N1 with N2; crush
+    end.
+Qed.
+
+Lemma substring_suffix : forall s n,
+  n <= length s
+  -> length (substring n (length s - n) s) = length s - n.
+  induction s; substring.
+Qed.
+
+Lemma substring_suffix_emp' : forall s n m,
+  substring n (S m) s = ""
+  -> n >= length s.
+  induction s; crush;
+    match goal with
+      | [ |- ?N >= _ ] => destruct N; crush
+    end;
+    match goal with
+      [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
+    end.
+Qed.
+
+Lemma substring_suffix_emp : forall s n m,
+  m > 0
+  -> substring n m s = ""
+  -> n >= length s.
+  destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
+Qed.
+
+Hint Rewrite substring_stack substring_stack' substring_suffix
+  using omega : cpdt.
+
+Lemma minus_minus : forall n m1 m2,
+  m1 + m2 <= n
+  -> n - m1 - m2 = n - (m1 + m2).
+  intros; omega.
+Qed.
+
+Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
+  intros; omega.
+Qed.
+
+Hint Rewrite minus_minus using omega : cpdt.
+
+Section dec_star.
+  Variable P : string -> Prop.
+  Variable P_dec : forall s, {P s} + { ~P s}.
+
+  Hint Constructors star.
+
+  Lemma star_empty : forall s,
+    length s = 0
+    -> star P s.
+    destruct s; crush.
+  Qed.
+
+  Lemma star_singleton : forall s, P s -> star P s.
+    intros; rewrite <- (app_empty_end s); auto.
+  Qed.
+
+  Lemma star_app : forall s n m,
+    P (substring n m s)
+    -> star P (substring (n + m) (length s - (n + m)) s)
+    -> star P (substring n (length s - n) s).
+    induction n; substring;
+      match goal with
+        | [ H : P (substring ?N ?M ?S) |- _ ] =>
+          solve [ rewrite <- (substring_split S M); auto
+            | rewrite <- (substring_split' S N M); auto ]
+      end.
+  Qed.
+
+  Hint Resolve star_empty star_singleton star_app.
+
+  Variable s : string.
+
+  Lemma star_inv : forall s,
+    star P s
+    -> s = ""
+    \/ exists i, i < length s
+      /\ P (substring 0 (S i) s)
+      /\ star P (substring (S i) (length s - S i) s).
+    Hint Extern 1 (exists i : nat, _) =>
+      match goal with
+        | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
+      end.
+
+    induction 1; [
+      crush
+      | match goal with
+          | [ _ : P ?S |- _ ] => destruct S; crush
+        end
+    ].
+  Qed.    
+
+  Lemma star_substring_inv : forall n,
+    n <= length s
+    -> star P (substring n (length s - n) s)
+    -> substring n (length s - n) s = ""
+    \/ exists l, l < length s - n
+      /\ P (substring n (S l) s)
+      /\ star P (substring (n + S l) (length s - (n + S l)) s).
+    Hint Rewrite plus_n_Sm' : cpdt.
+
+    intros;
+      match goal with
+        | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
+      end.
+  Qed.
+
+  Section dec_star''.
+    Variable n : nat.
+
+    Variable P' : string -> Prop.
+    Variable P'_dec : forall n' : nat, n' > n
+      -> {P' (substring n' (length s - n') s)}
+      + { ~P' (substring n' (length s - n') s)}.
+
+    Definition dec_star'' (l : nat)
+      : {exists l', S l' <= l
+        /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
+      + {forall l', S l' <= l
+        -> ~P (substring n (S l') s) \/ ~P' (substring (n + S l') (length s - (n + S l')) s)}.
+      refine (fix F (l : nat) : {exists l', S l' <= l
+        /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
+      + {forall l', S l' <= l
+        -> ~P (substring n (S l') s) \/ ~P' (substring (n + S l') (length s - (n + S l')) s)} :=
+      match l return {exists l', S l' <= l
+        /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
+      + {forall l', S l' <= l ->
+        ~P (substring n (S l') s) \/ ~P' (substring (n + S l') (length s - (n + S l')) s)} with
+        | O => _
+        | S l' =>
+          (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
+          || F l'
+      end); clear F; crush; eauto 7;
+      match goal with
+        | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
+      end.
+    Defined.
+  End dec_star''.
+
+  Definition dec_star' (n n' : nat) : length s - n' <= n
+    -> {star P (substring n' (length s - n') s)}
+    + {~star P (substring n' (length s - n') s)}.
+    About dec_star''.
+
+    refine (fix F (n n' : nat) {struct n} : length s - n' <= n
+      -> {star P (substring n' (length s - n') s)}
+      + {~star P (substring n' (length s - n') s)} :=
+      match n return length s - n' <= n
+        -> {star P (substring n' (length s - n') s)}
+        + {~star P (substring n' (length s - n') s)} with
+        | O => fun _ => Yes
+        | S n'' => fun _ =>
+          le_gt_dec (length s) n'
+          || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
+      end); clear F; crush; eauto.
+
+    apply star_substring_inv in H; crush; eauto.
+
+    assert (n' >= length s); [ | omega].
+    apply substring_suffix_emp with (length s - n'); crush.
+
+    assert (S x <= length s - n'); [ omega | ].
+    apply _1 in H1.
+    tauto.
+  Defined.
+
+  Definition dec_star : {star P s} + { ~star P s}.
+    refine (match s with
+              | "" => Reduce (dec_star' (n := length s) 0 _)
+              | _ => Reduce (dec_star' (n := length s) 0 _)
+            end); crush.
+  Defined.
+End dec_star.
+
 Lemma app_cong : forall x1 y1 x2 y2,
   x1 = x2
   -> y1 = y2
@@ -462,12 +700,15 @@
 
 Hint Resolve app_cong.
 
+
+
 Definition matches P (r : regexp P) s : {P s} + { ~P s}.
   refine (fix F P (r : regexp P) s : {P s} + { ~P s} :=
     match r with
       | Char ch => string_dec s (String ch "")
       | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
       | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
+      | Star _ r => dec_star _ _ _
     end); crush;
   match goal with
     | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
@@ -484,3 +725,9 @@
 Eval simpl in matches a_b "a".
 Eval simpl in matches a_b "aa".
 Eval simpl in matches a_b "b".
+
+Example a_star := Star (Char "a"%char).
+Eval simpl in matches a_star "".
+Eval simpl in matches a_star "a".
+Eval simpl in matches a_star "b".
+Eval simpl in matches a_star "aa".