Mercurial > cpdt > repo

comparison src/MoreDep.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents f7c2bf7f1324
children 31fa03bc0f18
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
858 Lemma substring_none : forall s n, 858 Lemma substring_none : forall s n,
859 substring n 0 s = "". 859 substring n 0 s = "".
860 induction s; substring. 860 induction s; substring.
861 Qed. 861 Qed.
862 862
863 Hint Rewrite substring_all substring_none : cpdt. 863 Hint Rewrite substring_all substring_none.
864 864
865 Lemma substring_split : forall s m, 865 Lemma substring_split : forall s m,
866 substring 0 m s ++ substring m (length s - m) s = s. 866 substring 0 m s ++ substring m (length s - m) s = s.
867 induction s; substring. 867 induction s; substring.
868 Qed. 868 Qed.
881 Qed. 881 Qed.
882 882
883 Lemma substring_app_snd : forall s2 s1 n, 883 Lemma substring_app_snd : forall s2 s1 n,
884 length s1 = n 884 length s1 = n
885 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2. 885 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
886 Hint Rewrite <- minus_n_O : cpdt. 886 Hint Rewrite <- minus_n_O.
887 887
888 induction s1; crush. 888 induction s1; crush.
889 Qed. 889 Qed.
890 890
891 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial] : cpdt. 891 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
892 (* end hide *) 892 (* end hide *)
893 893
894 (** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *) 894 (** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *)
895 895
896 Section split. 896 Section split.
944 (* begin hide *) 944 (* begin hide *)
945 Lemma app_empty_end : forall s, s ++ "" = s. 945 Lemma app_empty_end : forall s, s ++ "" = s.
946 induction s; crush. 946 induction s; crush.
947 Qed. 947 Qed.
948 948
949 Hint Rewrite app_empty_end : cpdt. 949 Hint Rewrite app_empty_end.
950 950
951 Lemma substring_self : forall s n, 951 Lemma substring_self : forall s n,
952 n <= 0 952 n <= 0
953 -> substring n (length s - n) s = s. 953 -> substring n (length s - n) s = s.
954 induction s; substring. 954 induction s; substring.
958 m <= 0 958 m <= 0
959 -> substring n m s = "". 959 -> substring n m s = "".
960 induction s; substring. 960 induction s; substring.
961 Qed. 961 Qed.
962 962
963 Hint Rewrite substring_self substring_empty using omega : cpdt. 963 Hint Rewrite substring_self substring_empty using omega.
964 964
965 Lemma substring_split' : forall s n m, 965 Lemma substring_split' : forall s n m,
966 substring n m s ++ substring (n + m) (length s - (n + m)) s 966 substring n m s ++ substring (n + m) (length s - (n + m)) s
967 = substring n (length s - n) s. 967 = substring n (length s - n) s.
968 Hint Rewrite substring_split : cpdt. 968 Hint Rewrite substring_split.
969 969
970 induction s; substring. 970 induction s; substring.
971 Qed. 971 Qed.
972 972
973 Lemma substring_stack : forall s n2 m1 m2, 973 Lemma substring_stack : forall s n2 m1 m2,
1018 -> n >= length s. 1018 -> n >= length s.
1019 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption]. 1019 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
1020 Qed. 1020 Qed.
1021 1021
1022 Hint Rewrite substring_stack substring_stack' substring_suffix 1022 Hint Rewrite substring_stack substring_stack' substring_suffix
1023 using omega : cpdt. 1023 using omega.
1024 1024
1025 Lemma minus_minus : forall n m1 m2, 1025 Lemma minus_minus : forall n m1 m2,
1026 m1 + m2 <= n 1026 m1 + m2 <= n
1027 -> n - m1 - m2 = n - (m1 + m2). 1027 -> n - m1 - m2 = n - (m1 + m2).
1028 intros; omega. 1028 intros; omega.
1030 1030
1031 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n. 1031 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
1032 intros; omega. 1032 intros; omega.
1033 Qed. 1033 Qed.
1034 1034
1035 Hint Rewrite minus_minus using omega : cpdt. 1035 Hint Rewrite minus_minus using omega.
1036 (* end hide *) 1036 (* end hide *)
1037 1037
1038 (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *) 1038 (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *)
1039 1039
1040 Section dec_star. 1040 Section dec_star.
1096 -> star P (substring n (length s - n) s) 1096 -> star P (substring n (length s - n) s)
1097 -> substring n (length s - n) s = "" 1097 -> substring n (length s - n) s = ""
1098 \/ exists l, l < length s - n 1098 \/ exists l, l < length s - n
1099 /\ P (substring n (S l) s) 1099 /\ P (substring n (S l) s)
1100 /\ star P (substring (n + S l) (length s - (n + S l)) s). 1100 /\ star P (substring (n + S l) (length s - (n + S l)) s).
1101 Hint Rewrite plus_n_Sm' : cpdt. 1101 Hint Rewrite plus_n_Sm'.
1102 1102
1103 intros; 1103 intros;
1104 match goal with 1104 match goal with
1105 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto 1105 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
1106 end. 1106 end.