Mercurial > cpdt > repo

comparison src/MoreDep.v @ 92:41392e5acbf5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish automating regexp
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 16:08:58 -0400
parents 4a57a4922af5
children a08e82c646a5
comparison
equal deleted inserted replaced
91:4a57a4922af5 92:41392e5acbf5
535 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ] 535 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
536 end. 536 end.
537 Qed. 537 Qed.
538 538
539 Lemma substring_suffix_emp : forall s n m, 539 Lemma substring_suffix_emp : forall s n m,
540 m > 0 540 substring n m s = ""
541 -> substring n m s = "" 541 -> m > 0
542 -> n >= length s. 542 -> n >= length s.
543 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption]. 543 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
544 Qed. 544 Qed.
545 545
546 Hint Rewrite substring_stack substring_stack' substring_suffix 546 Hint Rewrite substring_stack substring_stack' substring_suffix
654 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush 654 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
655 end. 655 end.
656 Defined. 656 Defined.
657 End dec_star''. 657 End dec_star''.
658 658
659 Lemma star_length_contra : forall n,
660 length s > n
661 -> n >= length s
662 -> False.
663 crush.
664 Qed.
665
666 Lemma star_length_flip : forall n n',
667 length s - n <= S n'
668 -> length s > n
669 -> length s - n > 0.
670 crush.
671 Qed.
672
673 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
674
659 Definition dec_star' (n n' : nat) : length s - n' <= n 675 Definition dec_star' (n n' : nat) : length s - n' <= n
660 -> {star P (substring n' (length s - n') s)} 676 -> {star P (substring n' (length s - n') s)}
661 + {~star P (substring n' (length s - n') s)}. 677 + {~star P (substring n' (length s - n') s)}.
662 About dec_star''.
663
664 refine (fix F (n n' : nat) {struct n} : length s - n' <= n 678 refine (fix F (n n' : nat) {struct n} : length s - n' <= n
665 -> {star P (substring n' (length s - n') s)} 679 -> {star P (substring n' (length s - n') s)}
666 + {~star P (substring n' (length s - n') s)} := 680 + {~star P (substring n' (length s - n') s)} :=
667 match n return length s - n' <= n 681 match n return length s - n' <= n
668 -> {star P (substring n' (length s - n') s)} 682 -> {star P (substring n' (length s - n') s)}
669 + {~star P (substring n' (length s - n') s)} with 683 + {~star P (substring n' (length s - n') s)} with
670 | O => fun _ => Yes 684 | O => fun _ => Yes
671 | S n'' => fun _ => 685 | S n'' => fun _ =>
672 le_gt_dec (length s) n' 686 le_gt_dec (length s) n'
673 || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n') 687 || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
674 end); clear F; crush; eauto. 688 end); clear F; crush; eauto;
675 689 match goal with
676 apply star_substring_inv in H; crush; eauto. 690 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
677 691 end;
678 assert (n' >= length s); [ | omega]. 692 match goal with
679 apply substring_suffix_emp with (length s - n'); crush. 693 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
680 694 generalize (H2 _ (lt_le_S _ _ H1)); tauto
681 assert (S x <= length s - n'); [ omega | ]. 695 end.
682 apply _1 in H1.
683 tauto.
684 Defined. 696 Defined.
685 697
686 Definition dec_star : {star P s} + { ~star P s}. 698 Definition dec_star : {star P s} + { ~star P s}.
687 refine (match s with 699 refine (match s with
688 | "" => Reduce (dec_star' (n := length s) 0 _) 700 | "" => Reduce (dec_star' (n := length s) 0 _)
697 -> x1 ++ y1 = x2 ++ y2. 709 -> x1 ++ y1 = x2 ++ y2.
698 congruence. 710 congruence.
699 Qed. 711 Qed.
700 712
701 Hint Resolve app_cong. 713 Hint Resolve app_cong.
702
703
704 714
705 Definition matches P (r : regexp P) s : {P s} + { ~P s}. 715 Definition matches P (r : regexp P) s : {P s} + { ~P s}.
706 refine (fix F P (r : regexp P) s : {P s} + { ~P s} := 716 refine (fix F P (r : regexp P) s : {P s} + { ~P s} :=
707 match r with 717 match r with
708 | Char ch => string_dec s (String ch "") 718 | Char ch => string_dec s (String ch "")