Certified Programming with Dependent Types: src/MoreDep.v comparison

comparison src/MoreDep.v @ 91:4a57a4922af5

Add star to regexp matcher; need to automate a bit more

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 07 Oct 2008 14:52:15 -0400
parents	939add5a7db9
children	41392e5acbf5

comparison

equal deleted inserted replaced

-:9b0d118abbc9
+:4a57a4922af5
 (** * A Certified Regular Expression Matcher *)
 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.
 Lemma length_emp : length "" <= 0.
 crush.
 Hint Rewrite <- minus_n_O : cpdt.
 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 P1_dec : forall s, {P1 s} + { ~P1 s}.
-Variable P2_dec : forall s, {P2 s} + {~P2 s}.
+Variable P2_dec : forall s, {P2 s} + { ~P2 s}.
 Variable s : string.
 Definition split' (n : nat) : n <= length s
 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
 Defined.
 End split.
 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
 -> x1 ++ y1 = x2 ++ y2.
 congruence.
 Qed.
 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 _))
 end;
 tauto.
 Example a_b := Or (Char "a"%char) (Char "b"%char).
 Eval simpl in matches a_b "".
 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".

Mercurial > cpdt > repo

comparison src/MoreDep.v @ 91:4a57a4922af5