Mercurial > cpdt > repo

comparison src/MoreDep.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 0ce9829efa3b
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith Bool List Omega. 11 Require Import Arith Bool List Lia.
12 12
13 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif. 13 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
14 14
15 Require Extraction. 15 Require Extraction.
16 16
869 869
870 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial]. 870 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
871 (* end hide *) 871 (* end hide *)
872 872
873 (** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *) 873 (** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *)
874 Hint Extern 1 (_ <= _) => lia.
874 875
875 Section split. 876 Section split.
876 Variables P1 P2 : string -> Prop. 877 Variables P1 P2 : string -> Prop.
877 Variable P1_dec : forall s, {P1 s} + {~ P1 s}. 878 Variable P1_dec : forall s, {P1 s} + {~ P1 s}.
878 Variable P2_dec : forall s, {P2 s} + {~ P2 s}. 879 Variable P2_dec : forall s, {P2 s} + {~ P2 s}.
936 m <= 0 937 m <= 0
937 -> substring n m s = "". 938 -> substring n m s = "".
938 induction s; substring. 939 induction s; substring.
939 Qed. 940 Qed.
940 941
941 Hint Rewrite substring_self substring_empty using omega. 942 Hint Rewrite substring_self substring_empty using lia.
942 943
943 Lemma substring_split' : forall s n m, 944 Lemma substring_split' : forall s n m,
944 substring n m s ++ substring (n + m) (length s - (n + m)) s 945 substring n m s ++ substring (n + m) (length s - (n + m)) s
945 = substring n (length s - n) s. 946 = substring n (length s - n) s.
946 Hint Rewrite substring_split. 947 Hint Rewrite substring_split.
984 induction s; crush; 985 induction s; crush;
985 match goal with 986 match goal with
986 | [ |- ?N >= _ ] => destruct N; crush 987 | [ |- ?N >= _ ] => destruct N; crush
987 end; 988 end;
988 match goal with 989 match goal with
989 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ] 990 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | lia ]
990 end. 991 end.
991 Qed. 992 Qed.
992 993
993 Lemma substring_suffix_emp : forall s n m, 994 Lemma substring_suffix_emp : forall s n m,
994 substring n m s = "" 995 substring n m s = ""
996 -> n >= length s. 997 -> n >= length s.
997 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption]. 998 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
998 Qed. 999 Qed.
999 1000
1000 Hint Rewrite substring_stack substring_stack' substring_suffix 1001 Hint Rewrite substring_stack substring_stack' substring_suffix
1001 using omega. 1002 using lia.
1002 1003
1003 Lemma minus_minus : forall n m1 m2, 1004 Lemma minus_minus : forall n m1 m2,
1004 m1 + m2 <= n 1005 m1 + m2 <= n
1005 -> n - m1 - m2 = n - (m1 + m2). 1006 -> n - m1 - m2 = n - (m1 + m2).
1006 intros; omega. 1007 intros; lia.
1007 Qed. 1008 Qed.
1008 1009
1009 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n. 1010 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
1010 intros; omega. 1011 intros; lia.
1011 Qed. 1012 Qed.
1012 1013
1013 Hint Rewrite minus_minus using omega. 1014 Hint Rewrite minus_minus using lia.
1014 (* end hide *) 1015 (* end hide *)
1015 1016
1016 (** 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. *) 1017 (** 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. *)
1017 1018
1018 Section dec_star. 1019 Section dec_star.
1097 + {~ P' (substring n' (length s - n') s)}. 1098 + {~ P' (substring n' (length s - n') s)}.
1098 1099
1099 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *) 1100 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *)
1100 1101
1101 (** Now we come to [dec_star''] itself. It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split']. The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *) 1102 (** Now we come to [dec_star''] itself. It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split']. The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *)
1102 1103 Hint Extern 2 (_ \/ _) => lia.
1104
1103 Definition dec_star'' : forall l : nat, 1105 Definition dec_star'' : forall l : nat,
1104 {exists l', S l' <= l 1106 {exists l', S l' <= l
1105 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)} 1107 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
1106 + {forall l', S l' <= l 1108 + {forall l', S l' <= l
1107 -> ~ P (substring n (S l') s) 1109 -> ~ P (substring n (S l') s)