Mercurial > cpdt > repo

comparison src/MoreDep.v @ 87:a0b8b550e265

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add 'Or' to regexp matcher
author Adam Chlipala <adamc@hcoop.net>
date Mon, 06 Oct 2008 14:41:13 -0400
parents fd505bcb5632
children 939add5a7db9
comparison
equal deleted inserted replaced
86:fd505bcb5632 87:a0b8b550e265
351 351
352 Inductive regexp : (string -> Prop) -> Set := 352 Inductive regexp : (string -> Prop) -> Set :=
353 | Char : forall ch : ascii, 353 | Char : forall ch : ascii,
354 regexp (fun s => s = String ch "") 354 regexp (fun s => s = String ch "")
355 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2), 355 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
356 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2). 356 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
357 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
358 regexp (fun s => P1 s \/ P2 s).
357 359
358 Open Scope specif_scope. 360 Open Scope specif_scope.
359 361
360 Lemma length_emp : length "" <= 0. 362 Lemma length_emp : length "" <= 0.
361 crush. 363 crush.
463 Definition matches P (r : regexp P) s : {P s} + { ~P s}. 465 Definition matches P (r : regexp P) s : {P s} + { ~P s}.
464 refine (fix F P (r : regexp P) s : {P s} + { ~P s} := 466 refine (fix F P (r : regexp P) s : {P s} + { ~P s} :=
465 match r with 467 match r with
466 | Char ch => string_dec s (String ch "") 468 | Char ch => string_dec s (String ch "")
467 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s) 469 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
470 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
468 end); crush; 471 end); crush;
469 match goal with 472 match goal with
470 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _)) 473 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
471 end; 474 end;
472 tauto. 475 tauto.
473 Defined. 476 Defined.
474 477
475 Example hi := Concat (Char "h"%char) (Char "i"%char). 478 Example hi := Concat (Char "h"%char) (Char "i"%char).
476 Eval simpl in matches hi "hi". 479 Eval simpl in matches hi "hi".
477 Eval simpl in matches hi "bye". 480 Eval simpl in matches hi "bye".
481
482 Example a_b := Or (Char "a"%char) (Char "b"%char).
483 Eval simpl in matches a_b "".
484 Eval simpl in matches a_b "a".
485 Eval simpl in matches a_b "aa".
486 Eval simpl in matches a_b "b".