Mercurial > cpdt > repo
comparison src/MoreDep.v @ 92:41392e5acbf5
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 "") |