From 9ee62a197ea094911907341848d624ba33789f24 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Sat, 28 Feb 2015 15:22:37 +0100 Subject: Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or r15439 as we were talking at that time) --- CHANGES | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/CHANGES b/CHANGES index 712a8a7e92..e44fd5de0c 100644 --- a/CHANGES +++ b/CHANGES @@ -83,10 +83,13 @@ Specification Language - Added a syntax $(...)$ that allows putting tactics in terms (may break user notations using "$(", fixable by inserting a space or rewriting the notation). -- Constants in pattern-matching branches now respect the same rules regarding - implicit arguments than in applicative position. The old behavior can be - recovered by the command "Set Asymmetric Patterns". (possible source of - incompatibilities) +- Constructors in pattern-matching patterns now respect the same rules + regarding implicit arguments than in applicative position. The old + behavior can be recovered by the command "Set Asymmetric + Patterns". As a side effect, Much more notations can be used in + patterns. Considering that the pattern language is rich enough like + that, definitions are now always forbidden in patterns. (source of + incompatibilities for definitions that delta-reduce to a constructor) - Type inference algorithm now granting opacity of constants. This might also affect behavior of tactics (source of incompatibilities, solvable by re-declaring transparent constants which were set opaque). -- cgit v1.2.3 From dedd99c3e8c455514a2cffa9e4015d395572ab34 Mon Sep 17 00:00:00 2001 From: mlasson Date: Fri, 27 Feb 2015 14:54:35 +0100 Subject: Fixing the rule for ml4 depencies in coq_makefile --- tools/coq_makefile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 85206b8232..568c909edb 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -366,7 +366,7 @@ let implicit () = print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; -- cgit v1.2.3 From 73f04b525ef4283dfa999fbf2b00860b35be5a92 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Sat, 28 Feb 2015 15:36:51 +0100 Subject: Coq_makefile clean target erases .coq-native dirs in . if they are empty --- tools/coq_makefile.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 568c909edb..7491c1f9af 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -330,6 +330,7 @@ let clean sds sps = if !some_vfile then begin print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; + print "\tfind . -name .coq-native -type d -empty -delete\n"; print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" end; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; -- cgit v1.2.3 From 7bad2a2caeeafdc05ec0d768b17bd6d7a7e3acd0 Mon Sep 17 00:00:00 2001 From: Bruno Barras Date: Mon, 2 Mar 2015 11:45:06 +0100 Subject: Now accepting unit props in mutual definitions --- checker/indtypes.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 2ce9f038a0..050c33e603 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -230,7 +230,6 @@ let compute_elim_sorts env_ar params mib arity lc = let infos = Array.map (sorts_of_constr_args env_params) lc in let (small,unit) = small_unit infos in (* We accept recursive unit types... *) - let unit = unit && mib.mind_ntypes = 1 in (* compute the max of the sorts of the products of the constructor type *) let level = max_inductive_sort (Array.concat (Array.to_list (Array.map Array.of_list infos))) in -- cgit v1.2.3 From 022ec07048962ccd33ffdbcdc06adcb7fb09924f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 2 Mar 2015 13:08:59 +0100 Subject: Fix bug #4097. --- pretyping/evarsolve.ml | 15 +++++----- test-suite/bugs/closed/4097.v | 64 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 72 insertions(+), 7 deletions(-) create mode 100644 test-suite/bugs/closed/4097.v diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f355d9a725..db7f6f6772 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -179,23 +179,24 @@ let restrict_instance evd evk filter argsv = let noccur_evar env evd evk c = let cache = ref Int.Set.empty (* cache for let-ins *) in - let rec occur_rec k c = + let rec occur_rec (k, env as acc) c = match kind_of_term c with | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec k c + | Some c -> occur_rec acc c | None -> if Evar.equal evk evk' then raise Occur - else Array.iter (occur_rec k) args') + else Array.iter (occur_rec acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then (match pi2 (Environ.lookup_rel (i-k) env) with | None -> () - | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b)) - | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c []) - | _ -> iter_constr_with_binders succ occur_rec k c + | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) + | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) + | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) + occur_rec acc c in - try occur_rec 0 c; true with Occur -> false + try occur_rec (0,env) c; true with Occur -> false (***************************************) (* Managing chains of local definitons *) diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v new file mode 100644 index 0000000000..2109a4cd92 --- /dev/null +++ b/test-suite/bugs/closed/4097.v @@ -0,0 +1,64 @@ +(* File reduced by coq-bug-finder from original input, then from 6082 lines to 81 lines, then from 436 lines to 93 lines *) +(* coqc version 8.5beta1 (February 2015) compiled on Feb 27 2015 15:10:37 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (fc1b3ef9d7270938cd83c524aae0383093b7a4b5) *) +Global Set Primitive Projections. +Record sigT {A} (P : A -> Type) := exist { projT1 : A ; projT2 : P projT1 }. +Arguments projT1 {A P} _ / . +Arguments projT2 {A P} _ / . +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope path_scope. +Open Scope fibration_scope. +Notation "( x ; y )" := (exist _ _ x y) : fibration_scope. +Notation pr1 := projT1. +Notation pr2 := projT2. +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): + p # (f x) = f y + := + match p with idpath => idpath end. +Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B) + (p : x = y) (z : P (f x)) + : transport (fun x => P (f x)) p z = transport P (ap f p) z. +admit. +Defined. +Generalizable Variables X A B C f g n. +Definition pr1_path `{P : A -> Type} {u v : sigT P} (p : u = v) +: u.1 = v.1 + := ap pr1 p. +Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope. +Definition pr2_path `{P : A -> Type} {u v : sigT P} (p : u = v) +: p..1 # u.2 = v.2 + := (transport_compose P pr1 p u.2)^ + @ (@apD {x:A & P x} _ pr2 _ _ p). +Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope. +Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (p q : u = v) + (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2}) +: p = q. +admit. +Defined. +Set Debug Unification. +Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sigT P) + (p q : u = v) + (r : p..1 = q..1) + (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2) +: p = q + := path_path_sigma_uncurried P u v p q (r; s). \ No newline at end of file -- cgit v1.2.3 From e77f178e60918f14eacd1ec0364a491d4cfd0f3f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 00:48:34 +0100 Subject: Fix bug introduced by my last commit, forgetting to adjust de Bruijn index lookup. --- pretyping/evarsolve.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index db7f6f6772..99d83a0e88 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -189,7 +189,7 @@ let noccur_evar env evd evk c = else Array.iter (occur_rec acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then - (match pi2 (Environ.lookup_rel (i-k) env) with + (match pi2 (Environ.lookup_rel i env) with | None -> () | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) -- cgit v1.2.3 From ac62cda8a4f488b94033b108c37556877232137a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 09:41:51 +0100 Subject: Fix bug #4101, noccur_evar's expand_projection can legitimately fail when called from w_unify, so we protect it. --- pretyping/evarsolve.ml | 8 +++++++- test-suite/bugs/closed/4101.v | 19 +++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4101.v diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 99d83a0e88..bfd19c6c7d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -192,7 +192,13 @@ let noccur_evar env evd evk c = (match pi2 (Environ.lookup_rel i env) with | None -> () | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) - | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) + | Proj (p,c) -> + let c = + try Retyping.expand_projection env evd p c [] + with Retyping.RetypeError _ -> + (* Can happen when called from w_unify which doesn't assign evars/metas + eagerly enough *) c + in occur_rec acc c | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) occur_rec acc c in diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v new file mode 100644 index 0000000000..a38b050966 --- /dev/null +++ b/test-suite/bugs/closed/4101.v @@ -0,0 +1,19 @@ +(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *) + +Global Set Primitive Projections. +Set Implicit Arguments. +Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. +Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x), + (forall x, f x = g x) -> f = g. +Lemma sigT_obj_eq +: forall (T : Type) (T0 : T -> Type) + (s s0 : forall s : sigT T0, + sigT (fun _ : T0 (projT1 s) => unit) -> + sigT (fun _ : T0 (projT1 s) => unit)), + s0 = s. +Proof. + intros. + Set Debug Tactic Unification. + apply path_forall. \ No newline at end of file -- cgit v1.2.3 From 51b4d0cdad77f2874bd481dabd32e0772563dc3f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 15:47:24 +0100 Subject: Fix bug #4103: forgot to allow unfolding projections of cofixpoints like cases, in some cases. --- kernel/closure.ml | 2 +- pretyping/reductionops.ml | 4 ++-- test-suite/bugs/closed/4103.v | 12 ++++++++++++ 3 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/4103.v diff --git a/kernel/closure.ml b/kernel/closure.ml index 6824c399e6..ea9b2755f2 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -924,7 +924,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _)::_) as stk')) -> + (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 09eb38bd12..21f13a51f1 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -994,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, ((Stack.Case _ |Stack.Proj _)::s') -> reduce_and_refold_cofix whrec env cst_l cofix stack |_ -> fold () else fold () @@ -1073,7 +1073,7 @@ let local_whd_state_gen flags sigma = | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') -> + |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) |_ -> s else s diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v new file mode 100644 index 0000000000..92cc0279ac --- /dev/null +++ b/test-suite/bugs/closed/4103.v @@ -0,0 +1,12 @@ +Set Primitive Projections. + +CoInductive stream A := { hd : A; tl : stream A }. + +CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}. + +Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _). +Proof. + eexists. + (* Set Debug Tactic Unification. *) + (* Set Debug RAKAM. *) + reflexivity. -- cgit v1.2.3 From 9256b2eae87f342473dccc05308ffe4758780795 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 26 Feb 2015 14:33:20 +0100 Subject: Typos in doc modules. --- doc/refman/RefMan-mod.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 0e7b39c751..f48cf6abf5 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -74,9 +74,9 @@ This command is used to start an interactive module named {\ident}. \item {\tt Include {\module}} Includes the content of {\module} in the current interactive - module. Here {\module} can be a module expresssion or a module type + module. Here {\module} can be a module expression or a module type expression. If {\module} is a high-order module or module type - expression then the system tries to instanciate {\module} + expression then the system tries to instantiate {\module} by the current interactive module. \item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} -- cgit v1.2.3 From dc9e41d116854e35bf9c1765d9c6e3bc475383a1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 3 Mar 2015 12:15:56 +0100 Subject: Reinstalling search of camlpX in camldir, when given, for compatibility with pre-1b7d4a033af heuristic in searching camlpX (continuation of a joint patch with Maxime). Typo basename -> dirname. --- configure.ml | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/configure.ml b/configure.ml index f169e71000..2a4ef50e4b 100644 --- a/configure.ml +++ b/configure.ml @@ -534,6 +534,16 @@ let camltag = match caml_version_list with (** * CamlpX configuration *) +(* Convention: we use camldir as a prioritary location for camlpX, if given *) + +let which_camlpX base = + match !Prefs.camldir with + | Some dir -> + let file = Filename.concat dir base in + if is_executable file then file else which base + | None -> + which base + (* TODO: camlp5dir should rather be the *binary* location, just as camldir *) (* TODO: remove the late attempts at finding gramlib.cma *) @@ -569,7 +579,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with let check_camlp5_version () = try - let camlp5o = which "camlp5o" in + let camlp5o = which_camlpX "camlp5o" in let version_line, _ = run ~err:StdOut camlp5o ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in match string_split '.' version with @@ -586,7 +596,7 @@ let config_camlpX () = let camlp5mod = "gramlib" in let camlp5libdir = check_camlp5 (camlp5mod^".cma") in let camlp5o = check_camlp5_version () in - "camlp5", camlp5o, Filename.basename camlp5o, camlp5libdir, camlp5mod + "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod with NoCamlp5 -> (* We now try to use Camlp4, either by explicit choice or by lack of proper Camlp5 installation *) @@ -595,9 +605,9 @@ let config_camlpX () = if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then die "No Camlp4 installation found.\n"; try - let camlp4orf = which "camlp4orf" in + let camlp4orf = which_camlpX "camlp4orf" in ignore (run camlp4orf []); - "camlp4", camlp4orf, Filename.basename camlp4orf, camlp4libdir, camlp4mod + "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod with _ -> die "No Camlp4 installation found.\n" let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod = config_camlpX () -- cgit v1.2.3 From 2f8a153dafb144b3fbf984680b4da7bc06c357c2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 3 Mar 2015 12:31:01 +0100 Subject: Improving display of camlp4/camlp5 versions, library and binary locations. --- configure.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/configure.ml b/configure.ml index 2a4ef50e4b..45912615e2 100644 --- a/configure.ml +++ b/configure.ml @@ -584,7 +584,7 @@ let check_camlp5_version () = let version = List.nth (string_split ' ' version_line) 2 in match string_split '.' version with | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) -> - printf "You have Camlp5 %s. Good!\n" version; camlp5o + printf "You have Camlp5 %s. Good!\n" version; camlp5o, version | _ -> failwith "bad version" with | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" @@ -595,8 +595,8 @@ let config_camlpX () = if not !Prefs.usecamlp5 then raise NoCamlp5; let camlp5mod = "gramlib" in let camlp5libdir = check_camlp5 (camlp5mod^".cma") in - let camlp5o = check_camlp5_version () in - "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod + let camlp5o, camlp5_version = check_camlp5_version () in + "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version with NoCamlp5 -> (* We now try to use Camlp4, either by explicit choice or by lack of proper Camlp5 installation *) @@ -606,11 +606,12 @@ let config_camlpX () = die "No Camlp4 installation found.\n"; try let camlp4orf = which_camlpX "camlp4orf" in - ignore (run camlp4orf []); - "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod + let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in + let camlp4_version = List.nth (string_split ' ' version_line) 2 in + "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version with _ -> die "No Camlp4 installation found.\n" -let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod = config_camlpX () +let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX () let shorten_camllib s = if starts_with s (camllib^"/") then @@ -967,9 +968,11 @@ let print_summary () = pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags); pr " Other bytecode link flags : %s\n" custom_flag; pr " OS dependent libraries : %s\n" osdeplibs; - pr " OCaml/Camlp4 version : %s\n" caml_version; - pr " OCaml/Camlp4 binaries in : %s\n" camlbin; + pr " OCaml version : %s\n" caml_version; + pr " OCaml binaries in : %s\n" camlbin; pr " OCaml library in : %s\n" camllib; + pr " %s version : %s\n" (String.capitalize camlpX) camlpX_version; + pr " %s binaries in : %s\n" (String.capitalize camlpX) camlpXbindir; pr " %s library in : %s\n" (String.capitalize camlpX) camlpXlibdir; if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; -- cgit v1.2.3 From 2d3916766d3f145643a994aa83174c98394d5baa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 21:45:42 +0100 Subject: Fix bug #3590, keeping evars that are not turned into named metas by pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches. --- plugins/quote/quote.ml | 4 ++-- pretyping/patternops.ml | 49 +++++++++++++++++++++++++++++------------------- pretyping/patternops.mli | 3 ++- tactics/hints.ml | 6 +++--- tactics/tacinterp.ml | 10 +++++----- 5 files changed, 42 insertions(+), 30 deletions(-) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 637e0e28d5..2a2ef30fb1 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) + PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) + | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) in aux bodyi diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c49bec9aec..009b7323e4 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with let pattern_of_constr env sigma t = let ctx = ref [] in + let keep = ref Evar.Set.empty in + let remove = ref Evar.Set.empty in let rec pattern_of_constr env t = match kind_of_term t with | Rel n -> PRel n @@ -141,28 +143,35 @@ let pattern_of_constr env sigma t = | App (f,a) -> (match match kind_of_term f with - Evar (evk,args as ev) -> - (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - Some id - | _ -> None) - | _ -> None - with - | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) - | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) + | Evar (evk,args as ev) -> + (match snd (Evd.evar_source evk sigma) with + Evar_kinds.MatchingVar (true,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + keep := Evar.Set.union (evars_of_term ty) !keep; + remove := Evar.Set.add evk !remove; + Some id + | _ -> None) + | _ -> None + with + | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) + | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> pattern_of_constr env (Retyping.expand_projection env sigma p c []) | Evar (evk,ctxt as ev) -> - (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) - | _ -> PMeta None) + remove := Evar.Set.add evk !remove; + (match snd (Evd.evar_source evk sigma) with + | Evar_kinds.MatchingVar (b,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + keep := Evar.Set.union (evars_of_term ty) !keep; + assert (not b); PMeta (Some id) + | Evar_kinds.GoalEvar -> + PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; @@ -178,9 +187,11 @@ let pattern_of_constr env sigma t = | Fix f -> PFix f | CoFix f -> PCoFix f in let p = pattern_of_constr env t in + let remove = Evar.Set.diff !remove !keep in + let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in (* side-effect *) (* Warning: the order of dependencies in ctx is not ensured *) - (!ctx,p) + (sigma,!ctx,p) (* To process patterns, we need a translation without typing at all. *) @@ -220,7 +231,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - snd (pattern_of_constr env sigma c) + pi3 (pattern_of_constr env sigma c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in @@ -245,7 +256,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - snd (pattern_of_constr (Global.env()) Evd.empty t) + pi3 (pattern_of_constr (Global.env()) Evd.empty t) | PVar _ | PEvar _ | PRel _ -> pat diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index cf02421c24..9e72280fe2 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) -val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern +val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> + Evd.evar_map * named_context * constr_pattern (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they diff --git a/tactics/hints.ml b/tactics/hints.ml index 5621c365aa..101223b570 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -609,7 +609,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = snd (Patternops.pattern_of_constr env sigma cty) in + let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -628,7 +628,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = snd (Patternops.pattern_of_constr env ce.evd c') in + let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -726,7 +726,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); + pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t,ctx) }) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8826875a38..1429211f19 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -681,7 +681,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let p = match a with | Inl b -> Inl (interp_evaluable ist env sigma b) - | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in + | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in interp_occurrences ist occs, p let interp_constr_with_occurrences_and_name_as_list = @@ -1030,7 +1030,7 @@ let use_types = false let eval_pattern lfun ist env sigma (_,pat as c) = if use_types then - snd (interp_typed_pattern ist env sigma c) + pi3 (interp_typed_pattern ist env sigma c) else instantiate_pattern env sigma lfun pat @@ -2138,7 +2138,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in Proofview.V82.tactic begin fun gl -> - let sign,op = interp_typed_pattern ist env sigma op in + let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let env' = Environ.push_named_context sign env in let c_interp sigma = @@ -2146,8 +2146,8 @@ and interp_atomic ist tac : unit Proofview.tactic = with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in - (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) - gl + (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) + { gl with sigma = sigma } end end end -- cgit v1.2.3 From c135410086c256fcc74f579459687a83718148b9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 22:20:30 +0100 Subject: Fix test-suite file, this is currently a wontfix, but keep the test-suite file for when we move to a better implementation. --- test-suite/bugs/closed/3690.v | 52 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 test-suite/bugs/closed/3690.v diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v new file mode 100644 index 0000000000..4069e38075 --- /dev/null +++ b/test-suite/bugs/closed/3690.v @@ -0,0 +1,52 @@ +Set Printing Universes. +Set Universe Polymorphism. +Definition foo (a := Type) (b := Type) (c := Type) := Type. +Print foo. +(* foo = +let a := Type@{Top.1} in +let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4} + : Type@{Top.4+1} +(* Top.1 + Top.2 + Top.3 + Top.4 |= *) *) +Check @foo. (* foo@{Top.5 Top.6 Top.7 +Top.8} + : Type@{Top.8+1} +(* Top.5 + Top.6 + Top.7 + Top.8 |= *) *) +Definition bar := $(let t := eval compute in foo in exact t)$. +Check @bar. (* bar@{Top.13 Top.14 Top.15 +Top.16} + : Type@{Top.16+1} +(* Top.13 + Top.14 + Top.15 + Top.16 |= *) *) +(* The following should fail, since [bar] should only need one universe. *) +Check @bar@{i j}. +Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c. +Definition qux := Eval compute in baz. +Check @qux. (* qux@{Top.24 Top.25 +Top.26} + : Type@{max(Top.24+1, Top.26+1)} +(* Top.24 + Top.25 + Top.26 |= Top.25 < Top.24 + Top.26 < Top.25 + *) *) +Print qux. (* qux = +Type@{Top.21} -> Type@{Top.23} + : Type@{max(Top.21+1, Top.23+1)} +(* Top.21 + Top.22 + Top.23 |= Top.22 < Top.21 + Top.23 < Top.22 + *) *) +Fail Check @qux@{Set Set}. +Fail Check @qux@{Set Set Set}. +(* [qux] should only need two universes *) +Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *) +Fail Check @qux@{i j}. -- cgit v1.2.3 From f51efdd18b01c7f3fce026c32c0cd21ff4f6ca02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 22:28:09 +0100 Subject: Add a test-suite file ensuring coinductives with primitive projections do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching. --- test-suite/success/coindprim.v | 52 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 test-suite/success/coindprim.v diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v new file mode 100644 index 0000000000..4e0b7bf5c6 --- /dev/null +++ b/test-suite/success/coindprim.v @@ -0,0 +1,52 @@ +Set Primitive Projections. + +CoInductive stream A := { hd : A; tl : stream A }. + +CoFixpoint ticks : stream unit := + {| hd := tt; tl := ticks |}. + +Arguments hd [ A ] s. +Arguments tl [ A ] s. + +CoInductive bisim {A} : stream A -> stream A -> Prop := + | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'. + +Lemma bisim_refl {A} (s : stream A) : bisim s s. +Proof. + revert s. + cofix aux. intros. constructor. reflexivity. apply aux. +Defined. + +Lemma constr : forall (A : Type) (s : stream A), + bisim s (Build_stream _ s.(hd) s.(tl)). +Proof. + intros. constructor. reflexivity. simpl. apply bisim_refl. +Defined. + +Lemma constr' : forall (A : Type) (s : stream A), + s = Build_stream _ s.(hd) s.(tl). +Proof. + intros. + Fail destruct s. +Abort. + +Eval compute in constr _ ticks. + +Notation convertible x y := (eq_refl x : x = y). + +Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}. + +CoInductive U := inU + { outU : U }. + +CoFixpoint u : U := + inU u. + +CoFixpoint force (u : U) : U := + inU (outU u). + +Lemma eq (x : U) : x = force x. +Proof. + Fail destruct x. +Abort. + (* Impossible *) \ No newline at end of file -- cgit v1.2.3 From c1a330b28cd1417099183a1cb0a86b6a606b7ae9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 22:32:02 +0100 Subject: Add missing test-suite files and update gitignore. --- .gitignore | 3 +++ test-suite/bugs/closed/3590.v | 14 ++++++++++++++ test-suite/bugs/closed/4046.v | 6 ++++++ test-suite/bugs/opened/3794.v | 7 +++++++ 4 files changed, 30 insertions(+) create mode 100644 test-suite/bugs/closed/3590.v create mode 100644 test-suite/bugs/closed/4046.v create mode 100644 test-suite/bugs/opened/3794.v diff --git a/.gitignore b/.gitignore index 54b9d10b5d..c0bae6c665 100644 --- a/.gitignore +++ b/.gitignore @@ -160,3 +160,6 @@ dev/myinclude # coqide generated files (when testing) *.crashcoqide +/doc/refman/Reference-Manual.hoptind +/doc/refman/Reference-Manual.optidx +/doc/refman/Reference-Manual.optind diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v new file mode 100644 index 0000000000..51d6744c5c --- /dev/null +++ b/test-suite/bugs/closed/3590.v @@ -0,0 +1,14 @@ +(* Set Primitive Projections. *) +Set Implicit Arguments. +Record prod A B := pair { fst : A ; snd : B }. +Definition idS := Set. +Goal forall x y : prod Set Set, fst x = fst y. + intros. + change (@fst _ _ ?z) with (@fst Set idS z) at 2. + Unshelve. + admit. +Qed. + +(* Toplevel input, characters 20-58: +Error: Failed to get enough information from the left-hand side to type the +right-hand side. *) \ No newline at end of file diff --git a/test-suite/bugs/closed/4046.v b/test-suite/bugs/closed/4046.v new file mode 100644 index 0000000000..8f8779b7b2 --- /dev/null +++ b/test-suite/bugs/closed/4046.v @@ -0,0 +1,6 @@ +Module Import Foo. + Class Foo := { foo : Type }. +End Foo. + +Instance f : Foo := { foo := nat }. (* works fine *) +Instance f' : Foo.Foo := { Foo.foo := nat }. diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v new file mode 100644 index 0000000000..511a92b2af --- /dev/null +++ b/test-suite/bugs/opened/3794.v @@ -0,0 +1,7 @@ +Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate. +Hint Unfold not : core. + +Goal true<>false. +Set Typeclasses Debug. +typeclasses eauto with core. +Qed. \ No newline at end of file -- cgit v1.2.3 From 1b7e788a2bc6c7beb5d2e6971574e3349fd2a1cf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 23:20:53 +0100 Subject: Fix bug #3732: firstorder was using detyping to build existential instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms. --- plugins/firstorder/instances.ml | 32 +++++-------- test-suite/bugs/closed/3513.v | 75 +++++++++++++++++++++++++++++ test-suite/bugs/closed/3732.v | 104 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 192 insertions(+), 19 deletions(-) create mode 100644 test-suite/bugs/closed/3513.v create mode 100644 test-suite/bugs/closed/3732.v diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a88778c739..5912f0a0c3 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -113,24 +113,14 @@ let mk_open_instance id idc gl m t= Name id -> id | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in - let rec aux n avoid= - if Int.equal n 0 then [] else + let rec aux n avoid env evmap decls = + if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in - (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in - let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype false [] env evmap nt in - let rec raux n t= - if Int.equal n 0 then t else - match t with - GLambda(loc,name,k,_,t0)-> - let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1) - | _-> anomaly (Pp.str "can't happen") in - let ntt=try - fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*) - with e when Errors.noncritical e -> - error "Untypable instance, maybe higher-order non-prenex quantification" in - decompose_lam_n_assum m ntt + let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + let decl = (Name nid,None,c) in + aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in + let evmap, decls = aux m [] env evmap [] in + evmap, decls, revt (* tactics *) @@ -159,11 +149,15 @@ let left_instance_tac (inst,id) continue seq= if m>0 then pf_constr_of_global id (fun idc -> fun gl-> - let (rc,ot) = mk_open_instance id idc gl m t in + let evmap,rc,ot = mk_open_instance id idc gl m t in let gt= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in - generalize [gt] gl) + let evmap, _ = + try Typing.e_type_of (pf_env gl) evmap gt + with e when Errors.noncritical e -> + error "Untypable instance, maybe higher-order non-prenex quantification" in + tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) else pf_constr_of_global id (fun idc -> generalize [mkApp(idc,[|t|])]) diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v new file mode 100644 index 0000000000..80695f382c --- /dev/null +++ b/test-suite/bugs/closed/3513.v @@ -0,0 +1,75 @@ +(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *) +Require Coq.Setoids.Setoid. +Import Coq.Setoids.Setoid. +Generalizable All Variables. +Axiom admit : forall {T}, T. +Class Equiv (A : Type) := equiv : relation A. +Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv. +Class ILogicOps Frm := { lentails: relation Frm; + ltrue: Frm; + land: Frm -> Frm -> Frm; + lor: Frm -> Frm -> Frm }. +Infix "|--" := lentails (at level 79, no associativity). +Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. +Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. +Infix "-|-" := lequiv (at level 85, no associativity). +Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. +Section ILogic_Fun. + Context (T: Type) `{TType: type T}. + Context `{IL: ILogic Frm}. + Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. + Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. +End ILogic_Fun. +Implicit Arguments ILFunFrm [[ILOps] [e]]. +Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; + ltrue := True; + land P Q := P /\ Q; + lor P Q := P \/ Q |}. +Axiom Action : Set. +Definition Actions := list Action. +Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }. +Definition OPred := ILFunFrm Actions Prop. +Local Existing Instance ILFun_Ops. +Local Existing Instance ILFun_ILogic. +Definition catOP (P Q: OPred) : OPred := admit. +Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. +admit. +Defined. +Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. +Class IsPointed (T : Type) := point : T. +Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)). +Record PointedOPred := mkPointedOPred { + OPred_pred :> OPred; + OPred_inhabited: IsPointed_OPred OPred_pred + }. +Existing Instance OPred_inhabited. +Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred + := {| OPred_pred := O ; OPred_inhabited := _ |}. +Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit. +Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) + (tr : T -> T) (O2 : PointedOPred) (x : T) + (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0), + exists e1 e2, + catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2. + intros; do 2 esplit. + rewrite <- catOPA. + lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred) + (@Morphisms.respectful OPred (OPred -> OPred) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop)) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==> + @lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP + catOP_entails_m_Proper a a' H b b' H') in + pose P; + refine (P _ _) + end; unfold Basics.flip. + 2: solve [ apply reflexivity ]. + Undo. + 2: reflexivity. (* Toplevel input, characters 18-29: +Error: +Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *) \ No newline at end of file diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v new file mode 100644 index 0000000000..6e5952a527 --- /dev/null +++ b/test-suite/bugs/closed/3732.v @@ -0,0 +1,104 @@ +(* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *) +(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) +Require Coq.Lists.List. + +Import Coq.Lists.List. + +Set Implicit Arguments. +Global Set Asymmetric Patterns. + +Section machine. + Variables pc state : Type. + + Inductive propX (i := pc) (j := state) : list Type -> Type := + | Inj : forall G, Prop -> propX G + | ExistsX : forall G A, propX (A :: G) -> propX G. + + Implicit Arguments Inj [G]. + + Definition PropX := propX nil. + Fixpoint last (G : list Type) : Type. + exact (match G with + | nil => unit + | T :: nil => T + | _ :: G' => last G' + end). + Defined. + Fixpoint eatLast (G : list Type) : list Type. + exact (match G with + | nil => nil + | _ :: nil => nil + | x :: G' => x :: eatLast G' + end). + Defined. + + Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) := + match p with + | Inj _ P => fun _ => Inj P + | ExistsX G A p1 => fun p' => + match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with + | nil => fun p1 _ => ExistsX p1 + | _ :: _ => fun _ rc => ExistsX rc + end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with + | nil => fun _ _ => Inj True + | _ => fun p' => p' + end p')) + end. + + Definition spec := state -> PropX. + Definition codeSpec := pc -> option spec. + + Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P. + Definition interp specs := valid specs nil. +End machine. +Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope. +Bind Scope PropX_scope with PropX propX. +Variables pc state : Type. + +Inductive subs : list Type -> Type := +| SNil : subs nil +| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts). + +Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) := + match s in subs G return subs (T :: G) with + | SNil => SCons _ nil f SNil + | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f) + end. + +Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state := + match s in subs G return propX pc state G -> PropX pc state with + | SNil => fun p => p + | SCons _ _ f s' => fun p => Substs s' (subst p f) + end. +Variable specs : codeSpec pc state. + +Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)), + interp specs (Substs s (ExX : A, p)) + -> exists a, interp specs (Substs (SPush s a) p). +admit. +Defined. + +Goal forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G)) + (s : subs G) + (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p))) + (P : forall _ : subs (@cons Type A G), Prop) + (_ : forall (s0 : subs (@cons Type A G)) + (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)), + P s0), + @ex (forall _ : A, PropX pc state) + (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)). + intros ? ? ? ? H ? H'. + apply simplify_fwd_ExistsX in H. + firstorder. +Qed. + (* Toplevel input, characters 15-19: +Error: Illegal application: +The term "cons" of type "forall A : Type, A -> list A -> list A" +cannot be applied to the terms + "Type" : "Type" + "T" : "Type" + "G0" : "list Type" +The 2nd term has type "Type@{Top.53}" which should be coercible to + "Type@{Top.12}". + *) \ No newline at end of file -- cgit v1.2.3 From c35c97e7c904f2109110c64f2ba9e45e945de381 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 23:32:44 +0100 Subject: Fix test-suite file, this is open. --- test-suite/bugs/opened/3794.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v index 511a92b2af..99ca6cb39d 100644 --- a/test-suite/bugs/opened/3794.v +++ b/test-suite/bugs/opened/3794.v @@ -3,5 +3,5 @@ Hint Unfold not : core. Goal true<>false. Set Typeclasses Debug. -typeclasses eauto with core. -Qed. \ No newline at end of file +Fail typeclasses eauto with core. +Abort. \ No newline at end of file -- cgit v1.2.3 From 85fc5f90c52a755d1b64640f4f0b3421979c0fe8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 4 Mar 2015 00:32:58 +0100 Subject: Fix bug #3532, providing universe inconsistency information when a unification fails due to that, during a conversion step. --- pretyping/evarconv.ml | 23 +++++++++++++++-------- pretyping/reductionops.ml | 5 +++-- pretyping/reductionops.mli | 6 ++++-- 3 files changed, 22 insertions(+), 12 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 616ceeabdc..f388f90057 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( - let evd, b = - try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 - with Univ.UniverseInconsistency _ -> evd, false + let evd, e = + try + let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) + env evd term1 term2 + in + if b then evd, None + else evd, Some (ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e) in - if b then Some (evd, true) - else if is_ground_env evd env then Some (evd, false) - else None) + match e with + | None -> Some (evd, e) + | Some e -> + if is_ground_env evd env then Some (evd, Some e) + else None) else None in match ground_test with - | Some (evd, true) -> Success evd - | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2)) + | Some (evd, None) -> Success evd + | Some (evd, Some e) -> UnifFailure (evd,e) | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 21f13a51f1..dd671f111e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1293,7 +1293,8 @@ let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances } -let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = +let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) + env sigma x y = try let b, sigma = let b, cstrs = @@ -1315,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y sigma', true with | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ -> sigma, false + | Univ.UniverseInconsistency _ when catch_incon -> sigma, false | e when is_anomaly e -> error "Conversion test raised an anomaly" (********************************************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d4f061c5be..1df2a73b2e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_fconv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. + @raises UniverseInconsistency iff catch_incon is set to false, + otherwise returns false in that case. *) -val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> - evar_map * bool +val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> + env -> evar_map -> constr -> constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) -- cgit v1.2.3 From 00018101cf81f69d23587985a16fe3c8eefb8eaf Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 4 Mar 2015 15:12:46 +0100 Subject: Introducing MMaps, a modernized FMaps. NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty". --- Makefile.common | 3 +- theories/Lists/SetoidList.v | 11 +- theories/Lists/SetoidPermutation.v | 74 +- theories/MMaps/MMapFacts.v | 2434 +++++++++++++++++++++++++++++++++ theories/MMaps/MMapInterface.v | 292 ++++ theories/MMaps/MMapWeakList.v | 687 ++++++++++ theories/MMaps/MMaps.v | 18 + theories/MMaps/vo.itarget | 4 + theories/Structures/EqualitiesFacts.v | 214 +-- theories/Structures/OrdersLists.v | 211 +-- theories/theories.itarget | 1 + 11 files changed, 3697 insertions(+), 252 deletions(-) create mode 100644 theories/MMaps/MMapFacts.v create mode 100644 theories/MMaps/MMapInterface.v create mode 100644 theories/MMaps/MMapWeakList.v create mode 100644 theories/MMaps/MMaps.v create mode 100644 theories/MMaps/vo.itarget diff --git a/Makefile.common b/Makefile.common index e548619610..07df8bb157 100644 --- a/Makefile.common +++ b/Makefile.common @@ -288,6 +288,7 @@ STRINGSVO:=$(call cat_vo_itarget, theories/Strings) SETSVO:=$(call cat_vo_itarget, theories/Sets) FSETSVO:=$(call cat_vo_itarget, theories/FSets) MSETSVO:=$(call cat_vo_itarget, theories/MSets) +MMAPSVO:=$(call cat_vo_itarget, theories/MMaps) RELATIONSVO:=$(call cat_vo_itarget, theories/Relations) WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded) REALSVO:=$(call cat_vo_itarget, theories/Reals) @@ -303,7 +304,7 @@ THEORIESVO:=\ $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \ $(LISTSVO) $(STRINGSVO) \ $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ - $(SETSVO) $(FSETSVO) $(MSETSVO) \ + $(SETSVO) $(FSETSVO) $(MSETSVO) $(MMAPSVO) \ $(REALSVO) $(SORTINGVO) $(QARITHVO) \ $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index b57c3f046b..c95fb4d5c4 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -613,18 +613,18 @@ induction s1; simpl; auto; intros. Qed. Lemma fold_right_equivlistA_restr2 : - forall s s' (i j:B) (heqij: eqB i j), + forall s s' i j, NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> - eqB i j -> - equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). + equivlistA s s' -> eqB i j -> + eqB (fold_right f i s) (fold_right f j s'). Proof. simple induction s. destruct s'; simpl. intros. assumption. unfold equivlistA; intros. - destruct (H3 a). + destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' i j heqij N N' F eqij E; simpl in *. + intros x l Hrec s' i j N N' F E eqij; simpl in *. assert (InA x s') by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. @@ -649,7 +649,6 @@ Proof. red; intros; rewrite E; auto. Qed. - Lemma fold_right_add_restr2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index afc7c25bd8..cea3e839f6 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Import SetoidList. +Require Import Permutation SetoidList. (* Set Universe Polymorphism. *) Set Implicit Arguments. @@ -123,4 +123,76 @@ Proof. apply equivlistA_NoDupA_split with x y; intuition. Qed. +Lemma Permutation_eqlistA_commute l₁ l₂ l₃ : + eqlistA eqA l₁ l₂ -> Permutation l₂ l₃ -> + exists l₂', Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃. +Proof. + intros E P. revert l₁ E. + induction P; intros. + - inversion_clear E. now exists nil. + - inversion_clear E. + destruct (IHP l0) as (l0',(P',E')); trivial. clear IHP. + exists (x0::l0'). split; auto. + - inversion_clear E. inversion_clear H0. + exists (x1::x0::l1). now repeat constructor. + - clear P1 P2. + destruct (IHP1 _ E) as (l₁',(P₁,E₁)). + destruct (IHP2 _ E₁) as (l₂',(P₂,E₂)). + exists l₂'. split; trivial. econstructor; eauto. +Qed. + +Lemma PermutationA_decompose l₁ l₂ : + PermutationA l₁ l₂ -> + exists l, Permutation l₁ l /\ eqlistA eqA l l₂. +Proof. + induction 1. + - now exists nil. + - destruct IHPermutationA as (l,(P,E)). exists (x₁::l); auto. + - exists (x::y::l). split. constructor. reflexivity. + - destruct IHPermutationA1 as (l₁',(P,E)). + destruct IHPermutationA2 as (l₂',(P',E')). + destruct (@Permutation_eqlistA_commute l₁' l₂ l₂') as (l₁'',(P'',E'')); + trivial. + exists l₁''. split. now transitivity l₁'. now transitivity l₂'. +Qed. + +Lemma Permutation_PermutationA l₁ l₂ : + Permutation l₁ l₂ -> PermutationA l₁ l₂. +Proof. + induction 1. + - constructor. + - now constructor. + - apply permA_swap. + - econstructor; eauto. +Qed. + +Lemma eqlistA_PermutationA l₁ l₂ : + eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂. +Proof. + induction 1; now constructor. +Qed. + +Lemma NoDupA_equivlistA_decompose l1 l2 : + NoDupA eqA l1 -> NoDupA eqA l2 -> equivlistA eqA l1 l2 -> + exists l, Permutation l1 l /\ eqlistA eqA l l2. +Proof. + intros. apply PermutationA_decompose. + now apply NoDupA_equivlistA_PermutationA. +Qed. + +Lemma PermutationA_preserves_NoDupA l₁ l₂ : + PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂. +Proof. + induction 1; trivial. + - inversion_clear 1; constructor; auto. + apply PermutationA_equivlistA in H0. contradict H2. + now rewrite H, H0. + - inversion_clear 1. inversion_clear H1. constructor. + + contradict H. inversion_clear H; trivial. + elim H0. now constructor. + + constructor; trivial. + contradict H0. now apply InA_cons_tl. + - eauto. +Qed. + End Permutation. diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v new file mode 100644 index 0000000000..69066a7b6d --- /dev/null +++ b/theories/MMaps/MMapFacts.v @@ -0,0 +1,2434 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (b=true <-> b'=true). +Proof. + destruct b, b'; intuition. +Qed. + +Lemma eq_option_alt {elt}(o o':option elt) : + o=o' <-> (forall e, o=Some e <-> o'=Some e). +Proof. +split; intros. +- now subst. +- destruct o, o'; rewrite ?H; auto. + symmetry; now apply H. +Qed. + +Lemma option_map_some {A B}(f:A->B) o : + option_map f o <> None <-> o <> None. +Proof. + destruct o; simpl. now split. split; now destruct 1. +Qed. + +(** * Properties about weak maps *) + +Module WProperties_fun (E:DecidableType)(Import M:WSfun E). + +Definition Empty {elt}(m : t elt) := forall x e, ~MapsTo x e m. + +(** A few things about E.eq *) + +Lemma eq_refl x : E.eq x x. Proof. apply E.eq_equiv. Qed. +Lemma eq_sym x y : E.eq x y -> E.eq y x. Proof. apply E.eq_equiv. Qed. +Lemma eq_trans x y z : E.eq x y -> E.eq y z -> E.eq x z. +Proof. apply E.eq_equiv. Qed. +Hint Immediate eq_refl eq_sym : map. +Hint Resolve eq_trans eq_equivalence E.eq_equiv : map. + +Definition eqb x y := if E.eq_dec x y then true else false. + +Lemma eqb_eq x y : eqb x y = true <-> E.eq x y. +Proof. + unfold eqb; case E.eq_dec; now intuition. +Qed. + +Lemma eqb_sym x y : eqb x y = eqb y x. +Proof. + apply eq_bool_alt. rewrite !eqb_eq. split; apply E.eq_equiv. +Qed. + +(** Initial results about MapsTo and In *) + +Lemma mapsto_fun {elt} m x (e e':elt) : + MapsTo x e m -> MapsTo x e' m -> e=e'. +Proof. +rewrite <- !find_spec. congruence. +Qed. + +Lemma in_find {elt} (m : t elt) x : In x m <-> find x m <> None. +Proof. + unfold In. split. + - intros (e,H). rewrite <-find_spec in H. congruence. + - destruct (find x m) as [e|] eqn:H. + + exists e. now apply find_spec. + + now destruct 1. +Qed. + +Lemma not_in_find {elt} (m : t elt) x : ~In x m <-> find x m = None. +Proof. + rewrite in_find. split; auto. + intros; destruct (find x m); trivial. now destruct H. +Qed. + +Notation in_find_iff := in_find (only parsing). +Notation not_find_in_iff := not_in_find (only parsing). + +(** * [Equal] is a setoid equality. *) + +Infix "==" := Equal (at level 30). + +Lemma Equal_refl {elt} (m : t elt) : m == m. +Proof. red; reflexivity. Qed. + +Lemma Equal_sym {elt} (m m' : t elt) : m == m' -> m' == m. +Proof. unfold Equal; auto. Qed. + +Lemma Equal_trans {elt} (m m' m'' : t elt) : + m == m' -> m' == m'' -> m == m''. +Proof. unfold Equal; congruence. Qed. + +Instance Equal_equiv {elt} : Equivalence (@Equal elt). +Proof. +constructor; [exact Equal_refl | exact Equal_sym | exact Equal_trans]. +Qed. + +Arguments Equal {elt} m m'. + +Instance MapsTo_m {elt} : + Proper (E.eq==>Logic.eq==>Equal==>iff) (@MapsTo elt). +Proof. +intros k k' Hk e e' <- m m' Hm. rewrite <- Hk. +now rewrite <- !find_spec, Hm. +Qed. + +Instance In_m {elt} : + Proper (E.eq==>Equal==>iff) (@In elt). +Proof. +intros k k' Hk m m' Hm. unfold In. +split; intros (e,H); exists e; revert H; + now rewrite Hk, <- !find_spec, Hm. +Qed. + +Instance find_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@find elt). +Proof. +intros k k' Hk m m' <-. +rewrite eq_option_alt. intros. now rewrite !find_spec, Hk. +Qed. + +Instance mem_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@mem elt). +Proof. +intros k k' Hk m m' Hm. now rewrite eq_bool_alt, !mem_spec, Hk, Hm. +Qed. + +Instance Empty_m {elt} : Proper (Equal==>iff) (@Empty elt). +Proof. +intros m m' Hm. unfold Empty. now setoid_rewrite Hm. +Qed. + +Instance is_empty_m {elt} : Proper (Equal ==> Logic.eq) (@is_empty elt). +Proof. +intros m m' Hm. rewrite eq_bool_alt, !is_empty_spec. + now setoid_rewrite Hm. +Qed. + +Instance add_m {elt} : Proper (E.eq==>Logic.eq==>Equal==>Equal) (@add elt). +Proof. +intros k k' Hk e e' <- m m' Hm y. +destruct (E.eq_dec k y) as [H|H]. +- rewrite <-H, add_spec1. now rewrite Hk, add_spec1. +- rewrite !add_spec2; trivial. now rewrite <- Hk. +Qed. + +Instance remove_m {elt} : Proper (E.eq==>Equal==>Equal) (@remove elt). +Proof. +intros k k' Hk m m' Hm y. +destruct (E.eq_dec k y) as [H|H]. +- rewrite <-H, remove_spec1. now rewrite Hk, remove_spec1. +- rewrite !remove_spec2; trivial. now rewrite <- Hk. +Qed. + +Instance map_m {elt elt'} : + Proper ((Logic.eq==>Logic.eq)==>Equal==>Equal) (@map elt elt'). +Proof. +intros f f' Hf m m' Hm y. rewrite !map_spec, Hm. +destruct (find y m'); simpl; trivial. f_equal. now apply Hf. +Qed. + +Instance mapi_m {elt elt'} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@mapi elt elt'). +Proof. +intros f f' Hf m m' Hm y. +destruct (mapi_spec f m y) as (x,(Hx,->)). +destruct (mapi_spec f' m' y) as (x',(Hx',->)). +rewrite <- Hm. destruct (find y m); trivial. simpl. +f_equal. apply Hf; trivial. now rewrite Hx, Hx'. +Qed. + +Instance merge_m {elt elt' elt''} : + Proper ((E.eq==>Logic.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal==>Equal) + (@merge elt elt' elt''). +Proof. +intros f f' Hf m1 m1' Hm1 m2 m2' Hm2 y. +destruct (find y m1) as [e1|] eqn:H1. +- apply find_spec in H1. + assert (H : In y m1 \/ In y m2) by (left; now exists e1). + destruct (merge_spec1 f H) as (y1,(Hy1,->)). + rewrite Hm1,Hm2 in H. + destruct (merge_spec1 f' H) as (y2,(Hy2,->)). + rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y. +- destruct (find y m2) as [e2|] eqn:H2. + + apply find_spec in H2. + assert (H : In y m1 \/ In y m2) by (right; now exists e2). + destruct (merge_spec1 f H) as (y1,(Hy1,->)). + rewrite Hm1,Hm2 in H. + destruct (merge_spec1 f' H) as (y2,(Hy2,->)). + rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y. + + apply not_in_find in H1. apply not_in_find in H2. + assert (H : ~In y (merge f m1 m2)). + { intro H. apply merge_spec2 in H. intuition. } + apply not_in_find in H. rewrite H. + symmetry. apply not_in_find. intro H'. + apply merge_spec2 in H'. rewrite <- Hm1, <- Hm2 in H'. + intuition. +Qed. + +(* Later: compatibility for cardinal, fold, ... *) + +(** ** Earlier specifications (cf. FMaps) *) + +Section OldSpecs. +Variable elt: Type. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma MapsTo_1 m x y e : E.eq x y -> MapsTo x e m -> MapsTo y e m. +Proof. + now intros ->. +Qed. + +Lemma find_1 m x e : MapsTo x e m -> find x m = Some e. +Proof. apply find_spec. Qed. + +Lemma find_2 m x e : find x m = Some e -> MapsTo x e m. +Proof. apply find_spec. Qed. + +Lemma mem_1 m x : In x m -> mem x m = true. +Proof. apply mem_spec. Qed. + +Lemma mem_2 m x : mem x m = true -> In x m. +Proof. apply mem_spec. Qed. + +Lemma empty_1 : Empty (@empty elt). +Proof. + intros x e. now rewrite <- find_spec, empty_spec. +Qed. + +Lemma is_empty_1 m : Empty m -> is_empty m = true. +Proof. + unfold Empty; rewrite is_empty_spec. setoid_rewrite <- find_spec. + intros H x. specialize (H x). + destruct (find x m) as [e|]; trivial. + now destruct (H e). +Qed. + +Lemma is_empty_2 m : is_empty m = true -> Empty m. +Proof. + rewrite is_empty_spec. intros H x e. now rewrite <- find_spec, H. +Qed. + +Lemma add_1 m x y e : E.eq x y -> MapsTo y e (add x e m). +Proof. + intros <-. rewrite <-find_spec. apply add_spec1. +Qed. + +Lemma add_2 m x y e e' : + ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). +Proof. + intro. now rewrite <- !find_spec, add_spec2. +Qed. + +Lemma add_3 m x y e e' : + ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. +Proof. + intro. rewrite <- !find_spec, add_spec2; trivial. +Qed. + +Lemma remove_1 m x y : E.eq x y -> ~ In y (remove x m). +Proof. + intros <-. apply not_in_find. apply remove_spec1. +Qed. + +Lemma remove_2 m x y e : + ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). +Proof. + intro. now rewrite <- !find_spec, remove_spec2. +Qed. + +Lemma remove_3bis m x y e : + find y (remove x m) = Some e -> find y m = Some e. +Proof. + destruct (E.eq_dec x y) as [<-|H]. + - now rewrite remove_spec1. + - now rewrite remove_spec2. +Qed. + +Lemma remove_3 m x y e : MapsTo y e (remove x m) -> MapsTo y e m. +Proof. + rewrite <-!find_spec. apply remove_3bis. +Qed. + +Lemma bindings_1 m x e : + MapsTo x e m -> InA eq_key_elt (x,e) (bindings m). +Proof. apply bindings_spec1. Qed. + +Lemma bindings_2 m x e : + InA eq_key_elt (x,e) (bindings m) -> MapsTo x e m. +Proof. apply bindings_spec1. Qed. + +Lemma bindings_3w m : NoDupA eq_key (bindings m). +Proof. apply bindings_spec2w. Qed. + +Lemma cardinal_1 m : cardinal m = length (bindings m). +Proof. apply cardinal_spec. Qed. + +Lemma fold_1 m (A : Type) (i : A) (f : key -> elt -> A -> A) : + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. +Proof. apply fold_spec. Qed. + +Lemma equal_1 m m' cmp : Equivb cmp m m' -> equal cmp m m' = true. +Proof. apply equal_spec. Qed. + +Lemma equal_2 m m' cmp : equal cmp m m' = true -> Equivb cmp m m'. +Proof. apply equal_spec. Qed. + +End OldSpecs. + +Lemma map_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:elt->elt') : + MapsTo x e m -> MapsTo x (f e) (map f m). +Proof. + rewrite <- !find_spec, map_spec. now intros ->. +Qed. + +Lemma map_2 {elt elt'}(m: t elt)(x:key)(f:elt->elt') : + In x (map f m) -> In x m. +Proof. + rewrite !in_find, map_spec. apply option_map_some. +Qed. + +Lemma mapi_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:key->elt->elt') : + MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). +Proof. + destruct (mapi_spec f m x) as (y,(Hy,Eq)). + intro H. exists y; split; trivial. + rewrite <-find_spec in *. now rewrite Eq, H. +Qed. + +Lemma mapi_2 {elt elt'}(m: t elt)(x:key)(f:key->elt->elt') : + In x (mapi f m) -> In x m. +Proof. + destruct (mapi_spec f m x) as (y,(Hy,Eq)). + rewrite !in_find. intro H; contradict H. now rewrite Eq, H. +Qed. + +(** The ancestor [map2] of the current [merge] was dealing with functions + on datas only, not on keys. *) + +Definition map2 {elt elt' elt''} (f:option elt->option elt'->option elt'') + := merge (fun _ => f). + +Lemma map2_1 {elt elt' elt''}(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt'') : + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). +Proof. + intros. unfold map2. + now destruct (merge_spec1 (fun _ => f) H) as (y,(_,->)). +Qed. + +Lemma map2_2 {elt elt' elt''}(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt'') : + In x (map2 f m m') -> In x m \/ In x m'. +Proof. apply merge_spec2. Qed. + +Hint Immediate MapsTo_1 mem_2 is_empty_2 + map_2 mapi_2 add_3 remove_3 find_2 : map. +Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 + remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 : map. + +(** ** Specifications written using equivalences *) + +Section IffSpec. +Variable elt: Type. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma in_iff m x y : E.eq x y -> (In x m <-> In y m). +Proof. now intros ->. Qed. + +Lemma mapsto_iff m x y e : E.eq x y -> (MapsTo x e m <-> MapsTo y e m). +Proof. now intros ->. Qed. + +Lemma mem_in_iff m x : In x m <-> mem x m = true. +Proof. symmetry. apply mem_spec. Qed. + +Lemma not_mem_in_iff m x : ~In x m <-> mem x m = false. +Proof. +rewrite mem_in_iff; destruct (mem x m); intuition. +Qed. + +Lemma mem_find m x : mem x m = true <-> find x m <> None. +Proof. + rewrite <- mem_in_iff. apply in_find. +Qed. + +Lemma not_mem_find m x : mem x m = false <-> find x m = None. +Proof. + rewrite <- not_mem_in_iff. apply not_in_find. +Qed. + +Lemma In_dec m x : { In x m } + { ~ In x m }. +Proof. + generalize (mem_in_iff m x). + destruct (mem x m); [left|right]; intuition. +Qed. + +Lemma find_mapsto_iff m x e : MapsTo x e m <-> find x m = Some e. +Proof. symmetry. apply find_spec. Qed. + +Lemma equal_iff m m' cmp : Equivb cmp m m' <-> equal cmp m m' = true. +Proof. symmetry. apply equal_spec. Qed. + +Lemma empty_mapsto_iff x e : MapsTo x e empty <-> False. +Proof. +rewrite <- find_spec, empty_spec. now split. +Qed. + +Lemma not_in_empty x : ~In x (@empty elt). +Proof. +intros (e,H). revert H. apply empty_mapsto_iff. +Qed. + +Lemma empty_in_iff x : In x (@empty elt) <-> False. +Proof. +split; [ apply not_in_empty | destruct 1 ]. +Qed. + +Lemma is_empty_iff m : Empty m <-> is_empty m = true. +Proof. split; [apply is_empty_1 | apply is_empty_2 ]. Qed. + +Lemma add_mapsto_iff m x y e e' : + MapsTo y e' (add x e m) <-> + (E.eq x y /\ e=e') \/ + (~E.eq x y /\ MapsTo y e' m). +Proof. +split. +- intros H. destruct (E.eq_dec x y); [left|right]; split; trivial. + + symmetry. apply (mapsto_fun H); auto with map. + + now apply add_3 with x e. +- destruct 1 as [(H,H')|(H,H')]; subst; auto with map. +Qed. + +Lemma add_mapsto_new m x y e e' : ~In x m -> + MapsTo y e' (add x e m) <-> (E.eq x y /\ e=e') \/ MapsTo y e' m. +Proof. + intros. + rewrite add_mapsto_iff. intuition. + right; split; trivial. contradict H. exists e'. now rewrite H. +Qed. + +Lemma in_add m x y e : In y m -> In y (add x e m). +Proof. + destruct (E.eq_dec x y) as [<-|H']. + - now rewrite !in_find, add_spec1. + - now rewrite !in_find, add_spec2. +Qed. + +Lemma add_in_iff m x y e : In y (add x e m) <-> E.eq x y \/ In y m. +Proof. +split. +- intros H. destruct (E.eq_dec x y); [now left|right]. + rewrite in_find, add_spec2 in H; trivial. now apply in_find. +- intros [<-|H]. + + exists e. now apply add_1. + + now apply in_add. +Qed. + +Lemma add_neq_mapsto_iff m x y e e' : + ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). +Proof. +split; [apply add_3|apply add_2]; auto. +Qed. + +Lemma add_neq_in_iff m x y e : + ~ E.eq x y -> (In y (add x e m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +- now apply add_3 with x e. +- now apply add_2. +Qed. + +Lemma remove_mapsto_iff m x y e : + MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m. +Proof. +split; [split|destruct 1]. +- intro E. revert H. now rewrite <-E, <- find_spec, remove_spec1. +- now apply remove_3 with x. +- now apply remove_2. +Qed. + +Lemma remove_in_iff m x y : In y (remove x m) <-> ~E.eq x y /\ In y m. +Proof. +unfold In; split; [ intros (e,H) | intros (E,(e,H)) ]. +- apply remove_mapsto_iff in H. destruct H; split; trivial. + now exists e. +- exists e. now apply remove_2. +Qed. + +Lemma remove_neq_mapsto_iff : forall m x y e, + ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m). +Proof. +split; [apply remove_3|apply remove_2]; auto. +Qed. + +Lemma remove_neq_in_iff : forall m x y, + ~ E.eq x y -> (In y (remove x m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +- now apply remove_3 with x. +- now apply remove_2. +Qed. + +Lemma bindings_mapsto_iff m x e : + MapsTo x e m <-> InA eq_key_elt (x,e) (bindings m). +Proof. symmetry. apply bindings_spec1. Qed. + +Lemma bindings_in_iff m x : + In x m <-> exists e, InA eq_key_elt (x,e) (bindings m). +Proof. +unfold In; split; intros (e,H); exists e; now apply bindings_spec1. +Qed. + +End IffSpec. + +Lemma map_mapsto_iff {elt elt'} m x b (f : elt -> elt') : + MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m. +Proof. +rewrite <-find_spec, map_spec. setoid_rewrite <- find_spec. +destruct (find x m); simpl; split. +- injection 1. now exists e. +- intros (a,(->,H)). now injection H as ->. +- discriminate. +- intros (a,(_,H)); discriminate. +Qed. + +Lemma map_in_iff {elt elt'} m x (f : elt -> elt') : + In x (map f m) <-> In x m. +Proof. +rewrite !in_find, map_spec. apply option_map_some. +Qed. + +Lemma mapi_in_iff {elt elt'} m x (f:key->elt->elt') : + In x (mapi f m) <-> In x m. +Proof. +rewrite !in_find. destruct (mapi_spec f m x) as (y,(_,->)). +apply option_map_some. +Qed. + +(** Unfortunately, we don't have simple equivalences for [mapi] + and [MapsTo]. The only correct one needs compatibility of [f]. *) + +Lemma mapi_inv {elt elt'} m x b (f : key -> elt -> elt') : + MapsTo x b (mapi f m) -> + exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m. +Proof. +rewrite <- find_spec. setoid_rewrite <- find_spec. +destruct (mapi_spec f m x) as (y,(E,->)). +destruct (find x m); simpl. +- injection 1 as <-. now exists e, y. +- discriminate. +Qed. + +Lemma mapi_spec' {elt elt'} (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + forall m x, + find x (mapi f m) = option_map (f x) (find x m). +Proof. + intros. destruct (mapi_spec f m x) as (y,(Hy,->)). + destruct (find x m); simpl; trivial. + now rewrite Hy. +Qed. + +Lemma mapi_1bis {elt elt'} m x e (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + MapsTo x e m -> MapsTo x (f x e) (mapi f m). +Proof. +intros. destruct (mapi_1 f H0) as (y,(->,H2)). trivial. +Qed. + +Lemma mapi_mapsto_iff {elt elt'} m x b (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m). +Proof. +rewrite <-find_spec. setoid_rewrite <-find_spec. +intros Pr. rewrite mapi_spec' by trivial. +destruct (find x m); simpl; split. +- injection 1 as <-. now exists e. +- intros (a,(->,H)). now injection H as <-. +- discriminate. +- intros (a,(_,H)). discriminate. +Qed. + +(** Things are even worse for [merge] : we don't try to state any + equivalence, see instead boolean results below. *) + +(** Useful tactic for simplifying expressions like + [In y (add x e (remove z m))] *) + +Ltac map_iff := + repeat (progress ( + rewrite add_mapsto_iff || rewrite add_in_iff || + rewrite remove_mapsto_iff || rewrite remove_in_iff || + rewrite empty_mapsto_iff || rewrite empty_in_iff || + rewrite map_mapsto_iff || rewrite map_in_iff || + rewrite mapi_in_iff)). + +(** ** Specifications written using boolean predicates *) + +Section BoolSpec. + +Lemma mem_find_b {elt}(m:t elt)(x:key) : + mem x m = if find x m then true else false. +Proof. +apply eq_bool_alt. rewrite mem_find. destruct (find x m). +- now split. +- split; (discriminate || now destruct 1). +Qed. + +Variable elt elt' elt'' : Type. +Implicit Types m : t elt. +Implicit Types x y z : key. +Implicit Types e : elt. + +Lemma mem_b m x y : E.eq x y -> mem x m = mem y m. +Proof. now intros ->. Qed. + +Lemma find_o m x y : E.eq x y -> find x m = find y m. +Proof. now intros ->. Qed. + +Lemma empty_o x : find x (@empty elt) = None. +Proof. apply empty_spec. Qed. + +Lemma empty_a x : mem x (@empty elt) = false. +Proof. apply not_mem_find. apply empty_spec. Qed. + +Lemma add_eq_o m x y e : + E.eq x y -> find y (add x e m) = Some e. +Proof. + intros <-. apply add_spec1. +Qed. + +Lemma add_neq_o m x y e : + ~ E.eq x y -> find y (add x e m) = find y m. +Proof. apply add_spec2. Qed. +Hint Resolve add_neq_o : map. + +Lemma add_o m x y e : + find y (add x e m) = if E.eq_dec x y then Some e else find y m. +Proof. +destruct (E.eq_dec x y); auto with map. +Qed. + +Lemma add_eq_b m x y e : + E.eq x y -> mem y (add x e m) = true. +Proof. +intros <-. apply mem_spec, add_in_iff. now left. +Qed. + +Lemma add_neq_b m x y e : + ~E.eq x y -> mem y (add x e m) = mem y m. +Proof. +intros. now rewrite !mem_find_b, add_neq_o. +Qed. + +Lemma add_b m x y e : + mem y (add x e m) = eqb x y || mem y m. +Proof. +rewrite !mem_find_b, add_o. unfold eqb. +now destruct (E.eq_dec x y). +Qed. + +Lemma remove_eq_o m x y : + E.eq x y -> find y (remove x m) = None. +Proof. intros ->. apply remove_spec1. Qed. + +Lemma remove_neq_o m x y : + ~ E.eq x y -> find y (remove x m) = find y m. +Proof. apply remove_spec2. Qed. + +Hint Resolve remove_eq_o remove_neq_o : map. + +Lemma remove_o m x y : + find y (remove x m) = if E.eq_dec x y then None else find y m. +Proof. +destruct (E.eq_dec x y); auto with map. +Qed. + +Lemma remove_eq_b m x y : + E.eq x y -> mem y (remove x m) = false. +Proof. +intros <-. now rewrite mem_find_b, remove_eq_o. +Qed. + +Lemma remove_neq_b m x y : + ~ E.eq x y -> mem y (remove x m) = mem y m. +Proof. +intros. now rewrite !mem_find_b, remove_neq_o. +Qed. + +Lemma remove_b m x y : + mem y (remove x m) = negb (eqb x y) && mem y m. +Proof. +rewrite !mem_find_b, remove_o; unfold eqb. +now destruct (E.eq_dec x y). +Qed. + +Lemma map_o m x (f:elt->elt') : + find x (map f m) = option_map f (find x m). +Proof. apply map_spec. Qed. + +Lemma map_b m x (f:elt->elt') : + mem x (map f m) = mem x m. +Proof. +rewrite !mem_find_b, map_o. now destruct (find x m). +Qed. + +Lemma mapi_b m x (f:key->elt->elt') : + mem x (mapi f m) = mem x m. +Proof. +apply eq_bool_alt; rewrite !mem_spec. apply mapi_in_iff. +Qed. + +Lemma mapi_o m x (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + find x (mapi f m) = option_map (f x) (find x m). +Proof. intros; now apply mapi_spec'. Qed. + +Lemma merge_spec1' (f:key->option elt->option elt'->option elt'') : + Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> + forall (m:t elt)(m':t elt') x, + In x m \/ In x m' -> + find x (merge f m m') = f x (find x m) (find x m'). +Proof. + intros Hf m m' x H. + now destruct (merge_spec1 f H) as (y,(->,->)). +Qed. + +Lemma merge_spec1_none (f:key->option elt->option elt'->option elt'') : + (forall x, f x None None = None) -> + forall (m: t elt)(m': t elt') x, + exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m'). +Proof. +intros Hf m m' x. +destruct (find x m) as [e|] eqn:Hm. +- assert (H : In x m \/ In x m') by (left; exists e; now apply find_spec). + destruct (merge_spec1 f H) as (y,(Hy,->)). + exists y; split; trivial. now rewrite Hm. +- destruct (find x m') as [e|] eqn:Hm'. + + assert (H : In x m \/ In x m') by (right; exists e; now apply find_spec). + destruct (merge_spec1 f H) as (y,(Hy,->)). + exists y; split; trivial. now rewrite Hm, Hm'. + + exists x. split. reflexivity. rewrite Hf. + apply not_in_find. intro H. + apply merge_spec2 in H. apply not_in_find in Hm. apply not_in_find in Hm'. + intuition. +Qed. + +Lemma merge_spec1'_none (f:key->option elt->option elt'->option elt'') : + Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> + (forall x, f x None None = None) -> + forall (m: t elt)(m': t elt') x, + find x (merge f m m') = f x (find x m) (find x m'). +Proof. + intros Hf Hf' m m' x. + now destruct (merge_spec1_none Hf' m m' x) as (y,(->,->)). +Qed. + +Lemma bindings_o : forall m x, + find x m = findA (eqb x) (bindings m). +Proof. +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, bindings_mapsto_iff. +unfold eqb. +rewrite <- findA_NoDupA; dintuition; try apply bindings_3w; eauto. +Qed. + +Lemma bindings_b : forall m x, + mem x m = existsb (fun p => eqb x (fst p)) (bindings m). +Proof. +intros. +apply eq_bool_alt. +rewrite mem_spec, bindings_in_iff, existsb_exists. +split. +- intros (e,H). + rewrite InA_alt in H. + destruct H as ((k,e'),((H1,H2),H')); simpl in *; subst e'. + exists (k, e); split; trivial. simpl. now apply eqb_eq. +- intros ((k,e),(H,H')); simpl in *. apply eqb_eq in H'. + exists e. rewrite InA_alt. exists (k,e). now repeat split. +Qed. + +End BoolSpec. + +Section Equalities. +Variable elt:Type. + +(** A few basic equalities *) + +Lemma eq_empty (m: t elt) : m == empty <-> is_empty m = true. +Proof. + unfold Equal. rewrite is_empty_spec. now setoid_rewrite empty_spec. +Qed. + +Lemma add_id (m: t elt) x e : add x e m == m <-> find x m = Some e. +Proof. + split. + - intros H. rewrite <- (H x). apply add_spec1. + - intros H y. rewrite !add_o. now destruct E.eq_dec as [<-|E]. +Qed. + +Lemma add_add_1 (m: t elt) x e : + add x e (add x e m) == add x e m. +Proof. + intros y. rewrite !add_o. destruct E.eq_dec; auto. +Qed. + +Lemma add_add_2 (m: t elt) x x' e e' : + ~E.eq x x' -> add x e (add x' e' m) == add x' e' (add x e m). +Proof. + intros H y. rewrite !add_o. + do 2 destruct E.eq_dec; auto. + elim H. now transitivity y. +Qed. + +Lemma remove_id (m: t elt) x : remove x m == m <-> ~In x m. +Proof. + rewrite not_in_find. split. + - intros H. rewrite <- (H x). apply remove_spec1. + - intros H y. rewrite !remove_o. now destruct E.eq_dec as [<-|E]. +Qed. + +Lemma remove_remove_1 (m: t elt) x : + remove x (remove x m) == remove x m. +Proof. + intros y. rewrite !remove_o. destruct E.eq_dec; auto. +Qed. + +Lemma remove_remove_2 (m: t elt) x x' : + remove x (remove x' m) == remove x' (remove x m). +Proof. + intros y. rewrite !remove_o. do 2 destruct E.eq_dec; auto. +Qed. + +Lemma remove_add_1 (m: t elt) x e : + remove x (add x e m) == remove x m. +Proof. + intro y. rewrite !remove_o, !add_o. now destruct E.eq_dec. +Qed. + +Lemma remove_add_2 (m: t elt) x x' e : + ~E.eq x x' -> remove x' (add x e m) == add x e (remove x' m). +Proof. + intros H y. rewrite !remove_o, !add_o. + do 2 destruct E.eq_dec; auto. + - elim H; now transitivity y. + - symmetry. now apply remove_eq_o. + - symmetry. now apply remove_neq_o. +Qed. + +Lemma add_remove_1 (m: t elt) x e : + add x e (remove x m) == add x e m. +Proof. + intro y. rewrite !add_o, !remove_o. now destruct E.eq_dec. +Qed. + +(** Another characterisation of [Equal] *) + +Lemma Equal_mapsto_iff : forall m1 m2 : t elt, + m1 == m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2). +Proof. +intros m1 m2. split; [intros Heq k e|intros Hiff]. +rewrite 2 find_mapsto_iff, Heq. split; auto. +intro k. rewrite eq_option_alt. intro e. +rewrite <- 2 find_mapsto_iff; auto. +Qed. + +(** * Relations between [Equal], [Equiv] and [Equivb]. *) + +(** First, [Equal] is [Equiv] with Leibniz on elements. *) + +Lemma Equal_Equiv : forall (m m' : t elt), + m == m' <-> Equiv Logic.eq m m'. +Proof. +intros. rewrite Equal_mapsto_iff. split; intros. +- split. + + split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto. + + intros; apply mapsto_fun with m k; auto; rewrite H; auto. +- split; intros H'. + + destruct H. + assert (Hin : In k m') by (rewrite <- H; exists e; auto). + destruct Hin as (e',He'). + rewrite (H0 k e e'); auto. + + destruct H. + assert (Hin : In k m) by (rewrite H; exists e; auto). + destruct Hin as (e',He'). + rewrite <- (H0 k e' e); auto. +Qed. + +(** [Equivb] and [Equiv] and equivalent when [eq_elt] and [cmp] + are related. *) + +Section Cmp. +Variable eq_elt : elt->elt->Prop. +Variable cmp : elt->elt->bool. + +Definition compat_cmp := + forall e e', cmp e e' = true <-> eq_elt e e'. + +Lemma Equiv_Equivb : compat_cmp -> + forall m m', Equiv eq_elt m m' <-> Equivb cmp m m'. +Proof. + unfold Equivb, Equiv, Cmp; intuition. + red in H; rewrite H; eauto. + red in H; rewrite <-H; eauto. +Qed. +End Cmp. + +(** Composition of the two last results: relation between [Equal] + and [Equivb]. *) + +Lemma Equal_Equivb : forall cmp, + (forall e e', cmp e e' = true <-> e = e') -> + forall (m m':t elt), m == m' <-> Equivb cmp m m'. +Proof. + intros; rewrite Equal_Equiv. + apply Equiv_Equivb; auto. +Qed. + +Lemma Equal_Equivb_eqdec : + forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }), + let cmp := fun e e' => if eq_elt_dec e e' then true else false in + forall (m m':t elt), m == m' <-> Equivb cmp m m'. +Proof. +intros; apply Equal_Equivb. +unfold cmp; clear cmp; intros. +destruct eq_elt_dec; now intuition. +Qed. + +End Equalities. + +(** * Results about [fold], [bindings], induction principles... *) + +Section Elt. + Variable elt:Type. + + Definition Add x (e:elt) m m' := m' == (add x e m). + + Notation eqke := (@eq_key_elt elt). + Notation eqk := (@eq_key elt). + + Instance eqk_equiv : Equivalence eqk. + Proof. unfold eq_key. destruct E.eq_equiv. constructor; eauto. Qed. + + Instance eqke_equiv : Equivalence eqke. + Proof. + unfold eq_key_elt; split; repeat red; intuition; simpl in *; + etransitivity; eauto. + Qed. + + (** Complements about InA, NoDupA and findA *) + + Lemma InA_eqke_eqk k k' e e' l : + E.eq k k' -> InA eqke (k,e) l -> InA eqk (k',e') l. + Proof. + intros Hk. rewrite 2 InA_alt. + intros ((k'',e'') & (Hk'',He'') & H); simpl in *; subst e''. + exists (k'',e); split; auto. red; simpl. now transitivity k. + Qed. + + Lemma NoDupA_incl {A} (R R':relation A) : + (forall x y, R x y -> R' x y) -> + forall l, NoDupA R' l -> NoDupA R l. + Proof. + intros Incl. + induction 1 as [ | a l E _ IH ]; constructor; auto. + contradict E. revert E. rewrite 2 InA_alt. firstorder. + Qed. + + Lemma NoDupA_eqk_eqke l : NoDupA eqk l -> NoDupA eqke l. + Proof. + apply NoDupA_incl. now destruct 1. + Qed. + + Lemma findA_rev l k : NoDupA eqk l -> + findA (eqb k) l = findA (eqb k) (rev l). + Proof. + intros H. apply eq_option_alt. intros e. unfold eqb. + rewrite <- !findA_NoDupA, InA_rev; eauto with map. reflexivity. + change (NoDupA eqk (rev l)). apply NoDupA_rev; auto using eqk_equiv. + Qed. + + (** * Bindings *) + + Lemma bindings_Empty (m:t elt) : Empty m <-> bindings m = nil. + Proof. + unfold Empty. split; intros H. + - assert (H' : forall a, ~ List.In a (bindings m)). + { intros (k,e) H'. apply (H k e). + rewrite bindings_mapsto_iff, InA_alt. + exists (k,e); repeat split; auto with map. } + destruct (bindings m) as [|p l]; trivial. + destruct (H' p); simpl; auto. + - intros x e. rewrite bindings_mapsto_iff, InA_alt. + rewrite H. now intros (y,(E,H')). + Qed. + + Lemma bindings_empty : bindings (@empty elt) = nil. + Proof. + rewrite <-bindings_Empty; apply empty_1. + Qed. + + (** * Conversions between maps and association lists. *) + + Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W := + fun p => f (fst p) (snd p). + + Definition of_list := + List.fold_right (uncurry (@add _)) (@empty elt). + + Definition to_list := bindings. + + Lemma of_list_1 : forall l k e, + NoDupA eqk l -> + (MapsTo k e (of_list l) <-> InA eqke (k,e) l). + Proof. + induction l as [|(k',e') l IH]; simpl; intros k e Hnodup. + - rewrite empty_mapsto_iff, InA_nil; intuition. + - unfold uncurry; simpl. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k e Hnodup'); clear Hnodup'. + rewrite add_mapsto_iff, InA_cons, <- IH. + unfold eq_key_elt at 1; simpl. + split; destruct 1 as [H|H]; try (intuition;fail). + destruct (E.eq_dec k k'); [left|right]; split; auto with map. + contradict Hnotin. + apply InA_eqke_eqk with k e; intuition. + Qed. + + Lemma of_list_1b : forall l k, + NoDupA eqk l -> + find k (of_list l) = findA (eqb k) l. + Proof. + induction l as [|(k',e') l IH]; simpl; intros k Hnodup. + apply empty_o. + unfold uncurry; simpl. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k Hnodup'); clear Hnodup'. + rewrite add_o, IH, eqb_sym. unfold eqb; now destruct E.eq_dec. + Qed. + + Lemma of_list_2 : forall l, NoDupA eqk l -> + equivlistA eqke l (to_list (of_list l)). + Proof. + intros l Hnodup (k,e). + rewrite <- bindings_mapsto_iff, of_list_1; intuition. + Qed. + + Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s. + Proof. + intros s k. + rewrite of_list_1b, bindings_o; auto. + apply bindings_3w. + Qed. + + (** * Fold *) + + (** Alternative specification via [fold_right] *) + + Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) : + fold f m i = List.fold_right (uncurry f) i (rev (bindings m)). + Proof. + rewrite fold_1. symmetry. apply fold_left_rev_right. + Qed. + + (** ** Induction principles about fold contributed by S. Lescuyer *) + + (** In the following lemma, the step hypothesis is deliberately restricted + to the precise map m we are considering. *) + + Lemma fold_rec : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), + forall (i:A)(m:t elt), + (forall m, Empty m -> P m i) -> + (forall k e a m' m'', MapsTo k e m -> ~In k m' -> + Add k e m' m'' -> P m' a -> P m'' (f k e a)) -> + P m (fold f m i). + Proof. + intros A P f i m Hempty Hstep. + rewrite fold_spec_right. + set (F:=uncurry f). + set (l:=rev (bindings m)). + assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' -> + Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)). + { + intros k e a m' m'' H ? ? ?; eapply Hstep; eauto. + revert H; unfold l; rewrite InA_rev, bindings_mapsto_iff; auto with *. } + assert (Hdup : NoDupA eqk l). + { unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *. + apply bindings_3w. } + assert (Hsame : forall k, find k m = findA (eqb k) l). + { intros k. unfold l. rewrite bindings_o, findA_rev; auto. + apply bindings_3w. } + clearbody l. clearbody F. clear Hstep f. revert m Hsame. induction l. + - (* empty *) + intros m Hsame; simpl. + apply Hempty. intros k e. + rewrite find_mapsto_iff, Hsame; simpl; discriminate. + - (* step *) + intros m Hsame; destruct a as (k,e); simpl. + apply Hstep' with (of_list l); auto. + + rewrite InA_cons; left; red; auto with map. + + inversion_clear Hdup. contradict H. destruct H as (e',He'). + apply InA_eqke_eqk with k e'; auto with map. + rewrite <- of_list_1; auto. + + intro k'. rewrite Hsame, add_o, of_list_1b. simpl. + rewrite eqb_sym. unfold eqb. now destruct E.eq_dec. + inversion_clear Hdup; auto with map. + + apply IHl. + * intros; eapply Hstep'; eauto. + * inversion_clear Hdup; auto. + * intros; apply of_list_1b. inversion_clear Hdup; auto. + Qed. + + (** Same, with [empty] and [add] instead of [Empty] and [Add]. In this + case, [P] must be compatible with equality of sets *) + + Theorem fold_rec_bis : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), + forall (i:A)(m:t elt), + (forall m m' a, Equal m m' -> P m a -> P m' a) -> + (P empty i) -> + (forall k e a m', MapsTo k e m -> ~In k m' -> + P m' a -> P (add k e m') (f k e a)) -> + P m (fold f m i). + Proof. + intros A P f i m Pmorphism Pempty Pstep. + apply fold_rec; intros. + apply Pmorphism with empty; auto. intro k. rewrite empty_o. + case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff. + intro H'; elim (H k e'); auto. + apply Pmorphism with (add k e m'); try intro; auto. + Qed. + + Lemma fold_rec_nodep : + forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt), + P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) -> + P (fold f m i). + Proof. + intros; apply fold_rec_bis with (P:=fun _ => P); auto. + Qed. + + (** [fold_rec_weak] is a weaker principle than [fold_rec_bis] : + the step hypothesis must here be applicable anywhere. + At the same time, it looks more like an induction principle, + and hence can be easier to use. *) + + Lemma fold_rec_weak : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A), + (forall m m' a, Equal m m' -> P m a -> P m' a) -> + P empty i -> + (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) -> + forall m, P m (fold f m i). + Proof. + intros; apply fold_rec_bis; auto. + Qed. + + Lemma fold_rel : + forall (A B:Type)(R : A -> B -> Type) + (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B) + (m : t elt), + R i j -> + (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) -> + R (fold f m i) (fold g m j). + Proof. + intros A B R f g i j m Rempty Rstep. + rewrite 2 fold_spec_right. set (l:=rev (bindings m)). + assert (Rstep' : forall k e a b, InA eqke (k,e) l -> + R a b -> R (f k e a) (g k e b)). + { intros; apply Rstep; auto. + rewrite bindings_mapsto_iff, <- InA_rev; auto with map. } + clearbody l; clear Rstep m. + induction l; simpl; auto. + apply Rstep'; auto. + destruct a; simpl; rewrite InA_cons; left; red; auto with map. + Qed. + + (** From the induction principle on [fold], we can deduce some general + induction principles on maps. *) + + Lemma map_induction : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. + Qed. + + Lemma map_induction_bis : + forall P : t elt -> Type, + (forall m m', Equal m m' -> P m -> P m') -> + P empty -> + (forall x e m, ~In x m -> P m -> P (add x e m)) -> + forall m, P m. + Proof. + intros. + apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. + Qed. + + (** [fold] can be used to reconstruct the same initial set. *) + + Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m empty) m. + Proof. + intros. + apply fold_rec with (P:=fun m acc => Equal acc m); auto with map. + intros m' Heq k'. + rewrite empty_o. + case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff. + intro; elim (Heq k' e'); auto. + intros k e a m' m'' _ _ Hadd Heq k'. + red in Heq. rewrite Hadd, 2 add_o, Heq; auto. + Qed. + + Section Fold_More. + + (** ** Additional properties of fold *) + + (** When a function [f] is compatible and allows transpositions, we can + compute [fold f] in any order. *) + + Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA). + + Lemma fold_Empty (f:key->elt->A->A) : + forall m i, Empty m -> eqA (fold f m i) i. + Proof. + intros. apply fold_rec_nodep with (P:=fun a => eqA a i). + reflexivity. + intros. elim (H k e); auto. + Qed. + + Lemma fold_init (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i'). + Proof. + intros Hf m i i' Hi. apply fold_rel with (R:=eqA); auto. + intros. now apply Hf. + Qed. + + (** Transpositions of f (a.k.a diamond property). + Could we swap two sequential calls to f, i.e. do we have: + + f k e (f k' e' a) == f k' e' (f k e a) + + First, we do no need this equation for all keys, but only + when k and k' aren't equal, as suggested by Pierre Castéran. + Think for instance of [f] being [M.add] : in general, we don't have + [M.add k e (M.add k e' m) == M.add k e' (M.add k e m)]. + Fortunately, we will never encounter this situation during a real + [fold], since the keys received by this [fold] are unique. + NB: without this condition, this condition would be + [SetoidList.transpose2]. + + Secondly, instead of the equation above, we now use a statement + with more basic equalities, allowing to prove [fold_commutes] even + when [f] isn't a morphism. + NB: When [f] is a morphism, [Diamond f] gives back the equation above. +*) + + Definition Diamond (f:key->elt->A->A) := + forall k k' e e' a b b', ~E.eq k k' -> + eqA (f k e a) b -> eqA (f k' e' a) b' -> eqA (f k e b') (f k' e' b). + + Lemma fold_commutes (f:key->elt->A->A) : + Diamond f -> + forall i m k e, ~In k m -> + eqA (fold f m (f k e i)) (f k e (fold f m i)). + Proof. + intros Hf i m k e H. + apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto. + - reflexivity. + - intros k' e' b a Hm E. + apply Hf with a; try easy. + contradict H; rewrite <- H. now exists e'. + Qed. + + Hint Resolve NoDupA_eqk_eqke NoDupA_rev bindings_3w : map. + + Lemma fold_Proper (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + Proper (Equal==>eqA==>eqA) (fold f). + Proof. + intros Hf Hf' m1 m2 Hm i j Hi. + rewrite 2 fold_spec_right. + assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). + assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). + apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke) + ; auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *. now apply Hf. + - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto with map. + - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. + rewrite h'. eapply Hf'; now eauto. + - rewrite <- NoDupA_altdef; auto. + - intros (k,e). + rewrite 2 InA_rev, <- 2 bindings_mapsto_iff, 2 find_mapsto_iff, Hm; + auto with *. + Qed. + + Lemma fold_Equal (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m1 m2 i, + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + intros. now apply fold_Proper. + Qed. + + Lemma fold_Add (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 -> + eqA (fold f m2 i) (f k e (fold f m1 i)). + Proof. + intros Hf Hf' m1 m2 k e i Hm1 Hm2. + rewrite 2 fold_spec_right. + set (f':=uncurry f). + change (f k e (fold_right f' i (rev (bindings m1)))) + with (f' (k,e) (fold_right f' i (rev (bindings m1)))). + assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). + assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). + apply fold_right_add_restr with + (R:=complement eqk)(eqA:=eqke); auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. now apply Hf. + - unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto with map. + - intros (k1,e1) (k2,e2) z1 z2; unfold eq_key, f', uncurry; simpl. + eapply Hf'; now eauto. + - rewrite <- NoDupA_altdef; auto. + - rewrite InA_rev, <- bindings_mapsto_iff by (auto with * ). firstorder. + - intros (a,b). + rewrite InA_cons, 2 InA_rev, <- 2 bindings_mapsto_iff, + 2 find_mapsto_iff by (auto with * ). + unfold eq_key_elt; simpl. + rewrite Hm2, !find_spec, add_mapsto_new; intuition. + Qed. + + Lemma fold_add (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m k e i, ~In k m -> + eqA (fold f (add k e m) i) (f k e (fold f m i)). + Proof. + intros. now apply fold_Add. + Qed. + + End Fold_More. + + (** * Cardinal *) + + Lemma cardinal_fold (m : t elt) : + cardinal m = fold (fun _ _ => S) m 0. + Proof. + rewrite cardinal_1, fold_1. + symmetry; apply fold_left_length; auto. + Qed. + + Lemma cardinal_Empty : forall m : t elt, + Empty m <-> cardinal m = 0. + Proof. + intros. + rewrite cardinal_1, bindings_Empty. + destruct (bindings m); intuition; discriminate. + Qed. + + Lemma Equal_cardinal (m m' : t elt) : + Equal m m' -> cardinal m = cardinal m'. + Proof. + intro. rewrite 2 cardinal_fold. + apply fold_Equal with (eqA:=eq); try congruence; auto with map. + Qed. + + Lemma cardinal_0 (m : t elt) : Empty m -> cardinal m = 0. + Proof. + intros; rewrite <- cardinal_Empty; auto. + Qed. + + Lemma cardinal_S m m' x e : + ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m). + Proof. + intros. rewrite 2 cardinal_fold. + change S with ((fun _ _ => S) x e). + apply fold_Add with (eqA:=eq); try congruence; auto with map. + Qed. + + Lemma cardinal_inv_1 : forall m : t elt, + cardinal m = 0 -> Empty m. + Proof. + intros; rewrite cardinal_Empty; auto. + Qed. + Hint Resolve cardinal_inv_1 : map. + + Lemma cardinal_inv_2 : + forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros; rewrite M.cardinal_spec in *. + generalize (bindings_mapsto_iff m). + destruct (bindings m); try discriminate. + exists p; auto. + rewrite H0; destruct p; simpl; auto. + constructor; red; auto with map. + Qed. + + Lemma cardinal_inv_2b : + forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros. + generalize (@cardinal_inv_2 m); destruct cardinal. + elim H;auto. + eauto. + Qed. + + Lemma not_empty_mapsto (m : t elt) : + ~Empty m -> exists k e, MapsTo k e m. + Proof. + intro. + destruct (@cardinal_inv_2b m) as ((k,e),H'). + contradict H. now apply cardinal_inv_1. + exists k; now exists e. + Qed. + + Lemma not_empty_in (m:t elt) : + ~Empty m -> exists k, In k m. + Proof. + intro. destruct (not_empty_mapsto H) as (k,Hk). + now exists k. + Qed. + + (** * Additional notions over maps *) + + Definition Disjoint (m m' : t elt) := + forall k, ~(In k m /\ In k m'). + + Definition Partition (m m1 m2 : t elt) := + Disjoint m1 m2 /\ + (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2). + + (** * Emulation of some functions lacking in the interface *) + + Definition filter (f : key -> elt -> bool)(m : t elt) := + fold (fun k e m => if f k e then add k e m else m) m empty. + + Definition for_all (f : key -> elt -> bool)(m : t elt) := + fold (fun k e b => if f k e then b else false) m true. + + Definition exists_ (f : key -> elt -> bool)(m : t elt) := + fold (fun k e b => if f k e then true else b) m false. + + Definition partition (f : key -> elt -> bool)(m : t elt) := + (filter f m, filter (fun k e => negb (f k e)) m). + + (** [update] adds to [m1] all the bindings of [m2]. It can be seen as + an [union] operator which gives priority to its 2nd argument + in case of binding conflit. *) + + Definition update (m1 m2 : t elt) := fold (@add _) m2 m1. + + (** [restrict] keeps from [m1] only the bindings whose key is in [m2]. + It can be seen as an [inter] operator, with priority to its 1st argument + in case of binding conflit. *) + + Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1. + + (** [diff] erases from [m1] all bindings whose key is in [m2]. *) + + Definition diff (m1 m2 : t elt) := filter (fun k _ => negb (mem k m2)) m1. + + (** Properties of these abbreviations *) + + Lemma filter_iff (f : key -> elt -> bool) : + Proper (E.eq==>eq==>eq) f -> + forall m k e, + MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true. + Proof. + unfold filter. + set (f':=fun k e m => if f k e then add k e m else m). + intros Hf m. pattern m, (fold f' m empty). apply fold_rec. + + - intros m' Hm' k e. rewrite empty_mapsto_iff. intuition. + elim (Hm' k e); auto. + + - intros k e acc m1 m2 Hke Hn Hadd IH k' e'. + change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd. + unfold f'; simpl. + rewrite add_mapsto_new by trivial. + case_eq (f k e); intros Hfke; simpl; + rewrite ?add_mapsto_iff, IH; clear IH; intuition. + + rewrite <- Hfke; apply Hf; auto with map. + + right. repeat split; trivial. contradict Hn. rewrite Hn. now exists e'. + + assert (f k e = f k' e') by (apply Hf; auto). congruence. + Qed. + + Lemma for_all_filter f m : + for_all f m = is_empty (filter (fun k e => negb (f k e)) m). + Proof. + unfold for_all, filter. + eapply fold_rel with (R:=fun x y => x = is_empty y). + - symmetry. apply is_empty_iff. apply empty_1. + - intros; subst. destruct (f k e); simpl; trivial. + symmetry. apply not_true_is_false. rewrite is_empty_spec. + intros H'. specialize (H' k). now rewrite add_spec1 in H'. + Qed. + + Lemma exists_filter f m : + exists_ f m = negb (is_empty (filter f m)). + Proof. + unfold for_all, filter. + eapply fold_rel with (R:=fun x y => x = negb (is_empty y)). + - symmetry. rewrite negb_false_iff. apply is_empty_iff. apply empty_1. + - intros; subst. destruct (f k e); simpl; trivial. + symmetry. rewrite negb_true_iff. apply not_true_is_false. + rewrite is_empty_spec. + intros H'. specialize (H' k). now rewrite add_spec1 in H'. + Qed. + + Lemma for_all_iff f m : + Proper (E.eq==>eq==>eq) f -> + (for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true)). + Proof. + intros Hf. + rewrite for_all_filter. + rewrite <- is_empty_iff. unfold Empty. + split; intros H k e; specialize (H k e); + rewrite filter_iff in * by solve_proper; intuition. + - destruct (f k e); auto. + - now rewrite H0 in H2. + Qed. + + Lemma exists_iff f m : + Proper (E.eq==>eq==>eq) f -> + (exists_ f m = true <-> + (exists k e, MapsTo k e m /\ f k e = true)). + Proof. + intros Hf. + rewrite exists_filter. rewrite negb_true_iff. + rewrite <- not_true_iff_false, <- is_empty_iff. + split. + - intros H. apply not_empty_mapsto in H. now setoid_rewrite filter_iff in H. + - unfold Empty. setoid_rewrite filter_iff; trivial. firstorder. + Qed. + + Lemma Disjoint_alt : forall m m', + Disjoint m m' <-> + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False). + Proof. + unfold Disjoint; split. + intros H k v v' H1 H2. + apply H with k; split. + exists v; trivial. + exists v'; trivial. + intros H k ((v,Hv),(v',Hv')). + eapply H; eauto. + Qed. + + Section Partition. + Variable f : key -> elt -> bool. + Hypothesis Hf : Proper (E.eq==>eq==>eq) f. + + Lemma partition_iff_1 : forall m m1 k e, + m1 = fst (partition f m) -> + (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true). + Proof. + unfold partition; simpl; intros. subst m1. + apply filter_iff; auto. + Qed. + + Lemma partition_iff_2 : forall m m2 k e, + m2 = snd (partition f m) -> + (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false). + Proof. + unfold partition; simpl; intros. subst m2. + rewrite filter_iff. + split; intros (H,H'); split; auto. + destruct (f k e); simpl in *; auto. + rewrite H'; auto. + repeat red; intros. f_equal. apply Hf; auto. + Qed. + + Lemma partition_Partition : forall m m1 m2, + partition f m = (m1,m2) -> Partition m m1 m2. + Proof. + intros. split. + rewrite Disjoint_alt. intros k e e'. + rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) + by (rewrite H; auto). + intros (U,V) (W,Z). rewrite <- (mapsto_fun U W) in Z; congruence. + intros k e. + rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) + by (rewrite H; auto). + destruct (f k e); intuition. + Qed. + + End Partition. + + Lemma Partition_In : forall m m1 m2 k, + Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}. + Proof. + intros m m1 m2 k Hm Hk. + destruct (In_dec m1 k) as [H|H]; [left|right]; auto. + destruct Hm as (Hm,Hm'). + destruct Hk as (e,He); rewrite Hm' in He; destruct He. + elim H; exists e; auto. + exists e; auto. + Defined. + + Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1. + Proof. + intros m1 m2 H k (H1,H2). elim (H k); auto. + Qed. + + Lemma Partition_sym : forall m m1 m2, + Partition m m1 m2 -> Partition m m2 m1. + Proof. + intros m m1 m2 (H,H'); split. + apply Disjoint_sym; auto. + intros; rewrite H'; intuition. + Qed. + + Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 -> + (Empty m <-> (Empty m1 /\ Empty m2)). + Proof. + intros m m1 m2 (Hdisj,Heq). split. + intro He. + split; intros k e Hke; elim (He k e); rewrite Heq; auto. + intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke. + elim (He1 k e); auto. + elim (He2 k e); auto. + Qed. + + Lemma Partition_Add : + forall m m' x e , ~In x m -> Add x e m m' -> + forall m1 m2, Partition m' m1 m2 -> + exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/ + Add x e m3 m2 /\ Partition m m1 m3). + Proof. + unfold Partition. intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor). + assert (Heq : Equal m (remove x m')). + { change (Equal m' (add x e m)) in Hadd. rewrite Hadd. + intro k. rewrite remove_o, add_o. + destruct E.eq_dec as [He|Hne]; auto. + rewrite <- He, <- not_find_in_iff; auto. } + assert (H : MapsTo x e m'). + { change (Equal m' (add x e m)) in Hadd; rewrite Hadd. + apply add_1; auto with map. } + rewrite Hor in H; destruct H. + + - (* first case : x in m1 *) + exists (remove x m1); left. split; [|split]. + + (* add *) + change (Equal m1 (add x e (remove x m1))). + intro k. + rewrite add_o, remove_o. + destruct E.eq_dec as [He|Hne]; auto. + rewrite <- He; apply find_1; auto. + + (* disjoint *) + intros k (H1,H2). elim (Hdisj k). split; auto. + rewrite remove_in_iff in H1; destruct H1; auto. + + (* mapsto *) + intros k' e'. + rewrite Heq, 2 remove_mapsto_iff, Hor. + intuition. + elim (Hdisj x); split; [exists e|exists e']; auto. + apply MapsTo_1 with k'; auto with map. + + - (* second case : x in m2 *) + exists (remove x m2); right. split; [|split]. + + (* add *) + change (Equal m2 (add x e (remove x m2))). + intro k. + rewrite add_o, remove_o. + destruct E.eq_dec as [He|Hne]; auto. + rewrite <- He; apply find_1; auto. + + (* disjoint *) + intros k (H1,H2). elim (Hdisj k). split; auto. + rewrite remove_in_iff in H2; destruct H2; auto. + + (* mapsto *) + intros k' e'. + rewrite Heq, 2 remove_mapsto_iff, Hor. + intuition. + elim (Hdisj x); split; [exists e'|exists e]; auto. + apply MapsTo_1 with k'; auto with map. + Qed. + + Lemma Partition_fold : + forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond eqA f -> + forall m m1 m2 i, + Partition m m1 m2 -> + eqA (fold f m i) (fold f m1 (fold f m2 i)). + Proof. + intros A eqA st f Comp Tra. + induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction. + + - intros m1 m2 i Hp. rewrite (fold_Empty (eqA:=eqA)); auto. + rewrite (Partition_Empty Hp) in Hm. destruct Hm. + rewrite 2 (fold_Empty (eqA:=eqA)); auto. reflexivity. + + - intros m1 m2 i Hp. + destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]). + + (* fst case: m3 is (k,e)::m1 *) + assert (~In k m3). + { contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } + transitivity (f k e (fold f m i)). + apply fold_Add with (eqA:=eqA); auto. + symmetry. + transitivity (f k e (fold f m3 (fold f m2 i))). + apply fold_Add with (eqA:=eqA); auto. + apply Comp; auto with map. + symmetry; apply IH; auto. + + (* snd case: m3 is (k,e)::m2 *) + assert (~In k m3). + { contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } + assert (~In k m1). + { contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } + transitivity (f k e (fold f m i)). + apply fold_Add with (eqA:=eqA); auto. + transitivity (f k e (fold f m1 (fold f m3 i))). + apply Comp; auto using IH with map. + transitivity (fold f m1 (f k e (fold f m3 i))). + symmetry. + apply fold_commutes with (eqA:=eqA); auto. + apply fold_init with (eqA:=eqA); auto. + symmetry. + apply fold_Add with (eqA:=eqA); auto. + Qed. + + Lemma Partition_cardinal : forall m m1 m2, Partition m m1 m2 -> + cardinal m = cardinal m1 + cardinal m2. + Proof. + intros. + rewrite (cardinal_fold m), (cardinal_fold m1). + set (f:=fun (_:key)(_:elt)=>S). + setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)). + rewrite <- cardinal_fold. + apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto. + apply Partition_fold with (eqA:=eq); compute; auto with map. congruence. + Qed. + + Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 -> + let f := fun k (_:elt) => mem k m1 in + Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)). + Proof. + intros m m1 m2 Hm f. + assert (Hf : Proper (E.eq==>eq==>eq) f). + intros k k' Hk e e' _; unfold f; rewrite Hk; auto. + set (m1':= fst (partition f m)). + set (m2':= snd (partition f m)). + split; rewrite Equal_mapsto_iff; intros k e. + rewrite (@partition_iff_1 f Hf m m1') by auto. + unfold f. + rewrite <- mem_in_iff. + destruct Hm as (Hm,Hm'). + rewrite Hm'. + intuition. + exists e; auto. + elim (Hm k); split; auto; exists e; auto. + rewrite (@partition_iff_2 f Hf m m2') by auto. + unfold f. + rewrite <- not_mem_in_iff. + destruct Hm as (Hm,Hm'). + rewrite Hm'. + intuition. + elim (Hm k); split; auto; exists e; auto. + elim H1; exists e; auto. + Qed. + + Lemma update_mapsto_iff : forall m m' k e, + MapsTo k e (update m m') <-> + (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')). + Proof. + unfold update. + intros m m'. + pattern m', (fold (@add _) m' m). apply fold_rec. + + - intros m0 Hm0 k e. + assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto). + intuition. + elim (Hm0 k e); auto. + + - intros k e m0 m1 m2 _ Hn Hadd IH k' e'. + change (Equal m2 (add k e m1)) in Hadd. + rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff. clear IH. intuition. + Qed. + + Lemma update_dec : forall m m' k e, MapsTo k e (update m m') -> + { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}. + Proof. + intros m m' k e H. rewrite update_mapsto_iff in H. + destruct (In_dec m' k) as [H'|H']; [left|right]; intuition. + elim H'; exists e; auto. + Defined. + + Lemma update_in_iff : forall m m' k, + In k (update m m') <-> In k m \/ In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite update_mapsto_iff in H. + destruct H; [right|left]; exists e; intuition. + destruct (In_dec m' k) as [H|H]. + destruct H as (e,H). intros _; exists e. + rewrite update_mapsto_iff; left; auto. + destruct 1 as [H'|H']; [|elim H; auto]. + destruct H' as (e,H'). exists e. + rewrite update_mapsto_iff; right; auto. + Qed. + + Lemma diff_mapsto_iff : forall m m' k e, + MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'. + Proof. + intros m m' k e. + unfold diff. + rewrite filter_iff. + intuition. + rewrite mem_1 in *; auto; discriminate. + intros ? ? Hk _ _ _; rewrite Hk; auto. + Qed. + + Lemma diff_in_iff : forall m m' k, + In k (diff m m') <-> In k m /\ ~In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite diff_mapsto_iff in H. + destruct H; split; auto. exists e; auto. + intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto. + Qed. + + Lemma restrict_mapsto_iff : forall m m' k e, + MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'. + Proof. + intros m m' k e. + unfold restrict. + rewrite filter_iff. + intuition. + intros ? ? Hk _ _ _; rewrite Hk; auto. + Qed. + + Lemma restrict_in_iff : forall m m' k, + In k (restrict m m') <-> In k m /\ In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite restrict_mapsto_iff in H. + destruct H; split; auto. exists e; auto. + intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto. + Qed. + + (** specialized versions analyzing only keys (resp. bindings) *) + + Definition filter_dom (f : key -> bool) := filter (fun k _ => f k). + Definition filter_range (f : elt -> bool) := filter (fun _ => f). + Definition for_all_dom (f : key -> bool) := for_all (fun k _ => f k). + Definition for_all_range (f : elt -> bool) := for_all (fun _ => f). + Definition exists_dom (f : key -> bool) := exists_ (fun k _ => f k). + Definition exists_range (f : elt -> bool) := exists_ (fun _ => f). + Definition partition_dom (f : key -> bool) := partition (fun k _ => f k). + Definition partition_range (f : elt -> bool) := partition (fun _ => f). + + End Elt. + + Instance cardinal_m {elt} : Proper (Equal ==> Logic.eq) (@cardinal elt). + Proof. intros m m'. apply Equal_cardinal. Qed. + + Instance Disjoint_m {elt} : Proper (Equal ==> Equal ==> iff) (@Disjoint elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros. + rewrite <- Hm1, <- Hm2; auto. + rewrite Hm1, Hm2; auto. + Qed. + + Instance Partition_m {elt} : + Proper (Equal ==> Equal ==> Equal ==> iff) (@Partition elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3. unfold Partition. + rewrite <- Hm2, <- Hm3. + split; intros (H,H'); split; auto; intros. + rewrite <- Hm1, <- Hm2, <- Hm3; auto. + rewrite Hm1, Hm2, Hm3; auto. + Qed. + +(* + Instance filter_m0 {elt} (f:key->elt->bool) : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + Proper (Equal==>Equal) (filter f). + Proof. + intros Hf m m' Hm. apply Equal_mapsto_iff. intros. + now rewrite !filter_iff, Hm. + Qed. +*) + + Instance filter_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@filter elt). + Proof. + intros f f' Hf m m' Hm. unfold filter. + rewrite 2 fold_spec_right. + set (l := rev (bindings m)). + set (l' := rev (bindings m')). + set (op := fun (f:key->elt->bool) => + uncurry (fun k e acc => if f k e then add k e acc else acc)). + change (Equal (fold_right (op f) empty l) (fold_right (op f') empty l')). + assert (Hl : NoDupA eq_key l). + { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. } + assert (Hl' : NoDupA eq_key l'). + { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. } + assert (H : PermutationA eq_key_elt l l'). + { apply NoDupA_equivlistA_PermutationA. + - apply eqke_equiv. + - now apply NoDupA_eqk_eqke. + - now apply NoDupA_eqk_eqke. + - intros (k,e); unfold l, l'. rewrite 2 InA_rev, 2 bindings_spec1. + rewrite Equal_mapsto_iff in Hm. apply Hm. } + destruct (PermutationA_decompose (eqke_equiv _) H) as (l0,(P,E)). + transitivity (fold_right (op f) empty l0). + - apply fold_right_equivlistA_restr2 + with (eqA:=Logic.eq)(R:=complement eq_key); auto with *. + + intros p p' <- acc acc' Hacc. + destruct p as (k,e); unfold op, uncurry; simpl. + destruct (f k e); now rewrite Hacc. + + intros (k,e) (k',e') z z'. + unfold op, complement, uncurry, eq_key; simpl. + intros Hk Hz. + destruct (f k e), (f k' e'); rewrite <- Hz; try reflexivity. + now apply add_add_2. + + apply NoDupA_incl with eq_key; trivial. intros; subst; now red. + + apply PermutationA_preserves_NoDupA with l; auto with *. + apply Permutation_PermutationA; auto with *. + apply NoDupA_incl with eq_key; trivial. intros; subst; now red. + + apply NoDupA_altdef. apply NoDupA_rev. apply eqk_equiv. + apply bindings_spec2w. + + apply PermutationA_equivlistA; auto with *. + apply Permutation_PermutationA; auto with *. + - clearbody l'. clear l Hl Hl' H P m m' Hm. + induction E. + + reflexivity. + + simpl. destruct x as (k,e), x' as (k',e'). + unfold op, uncurry at 1 3; simpl. + destruct H; simpl in *. rewrite <- (Hf _ _ H _ _ H0). + destruct (f k e); trivial. now f_equiv. + Qed. + + Instance for_all_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@for_all elt). + Proof. + intros f f' Hf m m' Hm. rewrite 2 for_all_filter. + (* Strange: we cannot rewrite Hm here... *) + f_equiv. f_equiv; trivial. + intros k k' Hk e e' He. f_equal. now apply Hf. + Qed. + + Instance exists_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@exists_ elt). + Proof. + intros f f' Hf m m' Hm. rewrite 2 exists_filter. + f_equal. now apply is_empty_m, filter_m. + Qed. + + Fact diamond_add {elt} : Diamond Equal (@add elt). + Proof. + intros k k' e e' a b b' Hk <- <-. now apply add_add_2. + Qed. + + Instance update_m {elt} : Proper (Equal ==> Equal ==> Equal) (@update elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. + unfold update. + apply fold_Proper; auto using diamond_add with *. + Qed. + + Instance restrict_m {elt} : Proper (Equal==>Equal==>Equal) (@restrict elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 y. + unfold restrict. + apply eq_option_alt. intros e. + rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity. + clear. intros x x' Hx e e' He. now rewrite Hx. + clear. intros x x' Hx e e' He. now rewrite Hx. + Qed. + + Instance diff_m {elt} : Proper (Equal==>Equal==>Equal) (@diff elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 y. + unfold diff. + apply eq_option_alt. intros e. + rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity. + clear. intros x x' Hx e e' He. now rewrite Hx. + clear. intros x x' Hx e e' He. now rewrite Hx. + Qed. + +End WProperties_fun. + +(** * Same Properties for self-contained weak maps and for full maps *) + +Module WProperties (M:WS) := WProperties_fun M.E M. +Module Properties := WProperties. + +(** * Properties specific to maps with ordered keys *) + +Module OrdProperties (M:S). + Module Import ME := OrderedTypeFacts M.E. + Module Import O:=KeyOrderedType M.E. + Module Import P:=Properties M. + Import M. + + Section Elt. + Variable elt:Type. + + Definition Above x (m:t elt) := forall y, In y m -> E.lt y x. + Definition Below x (m:t elt) := forall y, In y m -> E.lt x y. + + Section Bindings. + + Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), + sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'. + Proof. + apply SortA_equivlistA_eqlistA; eauto with *. + Qed. + + Ltac klean := unfold O.eqke, O.ltk, RelCompFun in *; simpl in *. + Ltac keauto := klean; intuition; eauto. + + Definition gtb (p p':key*elt) := + match E.compare (fst p) (fst p') with Gt => true | _ => false end. + Definition leb p := fun p' => negb (gtb p p'). + + Definition bindings_lt p m := List.filter (gtb p) (bindings m). + Definition bindings_ge p m := List.filter (leb p) (bindings m). + + Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p. + Proof. + intros (x,e) (y,e'); unfold gtb; klean. + case E.compare_spec; intuition; try discriminate; ME.order. + Qed. + + Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p. + Proof. + intros (x,e) (y,e'); unfold leb, gtb; klean. + case E.compare_spec; intuition; try discriminate; ME.order. + Qed. + + Instance gtb_compat : forall p, Proper (eqke==>eq) (gtb p). + Proof. + red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H. + generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e'')); + destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); klean; auto. + - intros. symmetry; rewrite H2. rewrite <-H, <-H1; auto. + - intros. rewrite H1. rewrite H, <- H2; auto. + Qed. + + Instance leb_compat : forall p, Proper (eqke==>eq) (leb p). + Proof. + intros x a b H. unfold leb; f_equal; apply gtb_compat; auto. + Qed. + + Hint Resolve gtb_compat leb_compat bindings_spec2 : map. + + Lemma bindings_split : forall p m, + bindings m = bindings_lt p m ++ bindings_ge p m. + Proof. + unfold bindings_lt, bindings_ge, leb; intros. + apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *. + intros; destruct x; destruct y; destruct p. + rewrite gtb_1 in H; klean. + apply not_true_iff_false in H0. rewrite gtb_1 in H0. klean. ME.order. + Qed. + + Lemma bindings_Add : forall m m' x e, ~In x m -> Add x e m m' -> + eqlistA eqke (bindings m') + (bindings_lt (x,e) m ++ (x,e):: bindings_ge (x,e) m). + Proof. + intros; unfold bindings_lt, bindings_ge. + apply sort_equivlistA_eqlistA; auto with *. + - apply (@SortA_app _ eqke); auto with *. + + apply (@filter_sort _ eqke); auto with *; keauto. + + constructor; auto with map. + * apply (@filter_sort _ eqke); auto with *; keauto. + * rewrite (@InfA_alt _ eqke); auto with *; try (keauto; fail). + { intros. + rewrite filter_InA in H1; auto with *; destruct H1. + rewrite leb_1 in H2. + destruct y; klean. + rewrite <- bindings_mapsto_iff in H1. + assert (~E.eq x t0). + { contradict H. + exists e0; apply MapsTo_1 with t0; auto. + ME.order. } + ME.order. } + { apply (@filter_sort _ eqke); auto with *; keauto. } + + intros. + rewrite filter_InA in H1; auto with *; destruct H1. + rewrite gtb_1 in H3. + destruct y; destruct x0; klean. + inversion_clear H2. + * red in H4; klean; destruct H4; simpl in *. ME.order. + * rewrite filter_InA in H4; auto with *; destruct H4. + rewrite leb_1 in H4. klean; ME.order. + - intros (k,e'). + rewrite InA_app_iff, InA_cons, 2 filter_InA, + <-2 bindings_mapsto_iff, leb_1, gtb_1, + find_mapsto_iff, (H0 k), <- find_mapsto_iff, + add_mapsto_iff by (auto with * ). + change (eqke (k,e') (x,e)) with (E.eq k x /\ e' = e). + klean. + split. + + intros [(->,->)|(Hk,Hm)]. + * right; now left. + * destruct (lt_dec k x); intuition. + + intros [(Hm,LT)|[(->,->)|(Hm,EQ)]]. + * right; split; trivial; ME.order. + * now left. + * destruct (eq_dec x k) as [Hk|Hk]. + elim H. exists e'. now rewrite Hk. + right; auto. + Qed. + + Lemma bindings_Add_Above : forall m m' x e, + Above x m -> Add x e m m' -> + eqlistA eqke (bindings m') (bindings m ++ (x,e)::nil). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + apply (@SortA_app _ eqke); auto with *. + intros. + inversion_clear H2. + destruct x0; destruct y. + rewrite <- bindings_mapsto_iff in H1. + destruct H3; klean. + rewrite H2. + apply H; firstorder. + inversion H3. + red; intros a; destruct a. + rewrite InA_app_iff, InA_cons, InA_nil, <- 2 bindings_mapsto_iff, + find_mapsto_iff, (H0 t0), <- find_mapsto_iff, + add_mapsto_iff by (auto with *). + change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e). + intuition. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. + exfalso. + assert (In t0 m) by (exists e0; auto). + generalize (H t0 H1). + ME.order. + Qed. + + Lemma bindings_Add_Below : forall m m' x e, + Below x m -> Add x e m m' -> + eqlistA eqke (bindings m') ((x,e)::bindings m). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + change (sort ltk (((x,e)::nil) ++ bindings m)). + apply (@SortA_app _ eqke); auto with *. + intros. + inversion_clear H1. + destruct y; destruct x0. + rewrite <- bindings_mapsto_iff in H2. + destruct H3; klean. + rewrite H1. + apply H; firstorder. + inversion H3. + red; intros a; destruct a. + rewrite InA_cons, <- 2 bindings_mapsto_iff, + find_mapsto_iff, (H0 t0), <- find_mapsto_iff, + add_mapsto_iff by (auto with * ). + change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e). + intuition. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. + exfalso. + assert (In t0 m) by (exists e0; auto). + generalize (H t0 H1). + ME.order. + Qed. + + Lemma bindings_Equal_eqlistA : forall (m m': t elt), + Equal m m' -> eqlistA eqke (bindings m) (bindings m'). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + red; intros. + destruct x; do 2 rewrite <- bindings_mapsto_iff. + do 2 rewrite find_mapsto_iff; rewrite H; split; auto. + Qed. + + End Bindings. + + Section Min_Max_Elt. + + (** We emulate two [max_elt] and [min_elt] functions. *) + + Fixpoint max_elt_aux (l:list (key*elt)) := match l with + | nil => None + | (x,e)::nil => Some (x,e) + | (x,e)::l => max_elt_aux l + end. + Definition max_elt m := max_elt_aux (bindings m). + + Lemma max_elt_Above : + forall m x e, max_elt m = Some (x,e) -> Above x (remove x m). + Proof. + red; intros. + rewrite remove_in_iff in H0. + destruct H0. + rewrite bindings_in_iff in H1. + destruct H1. + unfold max_elt in *. + generalize (bindings_spec2 m). + revert x e H y x0 H0 H1. + induction (bindings m). + simpl; intros; try discriminate. + intros. + destruct a; destruct l; simpl in *. + injection H; clear H; intros; subst. + inversion_clear H1. + red in H; simpl in *; intuition. + now elim H0. + inversion H. + change (max_elt_aux (p::l) = Some (x,e)) in H. + generalize (IHl x e H); clear IHl; intros IHl. + inversion_clear H1; [ | inversion_clear H2; eauto ]. + red in H3; simpl in H3; destruct H3. + destruct p as (p1,p2). + destruct (E.eq_dec p1 x) as [Heq|Hneq]. + rewrite <- Heq; auto. + inversion_clear H2. + inversion_clear H5. + red in H2; simpl in H2; ME.order. + transitivity p1; auto. + inversion_clear H2. + inversion_clear H5. + red in H2; simpl in H2; ME.order. + eapply IHl; eauto with *. + econstructor; eauto. + red; eauto with *. + inversion H2; auto. + Qed. + + Lemma max_elt_MapsTo : + forall m x e, max_elt m = Some (x,e) -> MapsTo x e m. + Proof. + intros. + unfold max_elt in *. + rewrite bindings_mapsto_iff. + induction (bindings m). + simpl; try discriminate. + destruct a; destruct l; simpl in *. + injection H; intros; subst; constructor; red; auto with *. + constructor 2; auto. + Qed. + + Lemma max_elt_Empty : + forall m, max_elt m = None -> Empty m. + Proof. + intros. + unfold max_elt in *. + rewrite bindings_Empty. + induction (bindings m); auto. + destruct a; destruct l; simpl in *; try discriminate. + assert (H':=IHl H); discriminate. + Qed. + + Definition min_elt m : option (key*elt) := match bindings m with + | nil => None + | (x,e)::_ => Some (x,e) + end. + + Lemma min_elt_Below : + forall m x e, min_elt m = Some (x,e) -> Below x (remove x m). + Proof. + unfold min_elt, Below; intros. + rewrite remove_in_iff in H0; destruct H0. + rewrite bindings_in_iff in H1. + destruct H1. + generalize (bindings_spec2 m). + destruct (bindings m). + try discriminate. + destruct p; injection H; intros; subst. + inversion_clear H1. + red in H2; destruct H2; simpl in *; ME.order. + inversion_clear H4. + rewrite (@InfA_alt _ eqke) in H3; eauto with *. + apply (H3 (y,x0)); auto. + Qed. + + Lemma min_elt_MapsTo : + forall m x e, min_elt m = Some (x,e) -> MapsTo x e m. + Proof. + intros. + unfold min_elt in *. + rewrite bindings_mapsto_iff. + destruct (bindings m). + simpl; try discriminate. + destruct p; simpl in *. + injection H; intros; subst; constructor; red; auto with *. + Qed. + + Lemma min_elt_Empty : + forall m, min_elt m = None -> Empty m. + Proof. + intros. + unfold min_elt in *. + rewrite bindings_Empty. + destruct (bindings m); auto. + destruct p; simpl in *; discriminate. + Qed. + + End Min_Max_Elt. + + Section Induction_Principles. + + Lemma map_induction_max : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, Above x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. + apply X; apply cardinal_inv_1; auto. + + case_eq (max_elt m); intros. + destruct p. + assert (Add k e (remove k m) m). + { apply max_elt_MapsTo, find_spec, add_id in H. + unfold Add. symmetry. now rewrite add_remove_1. } + apply X0 with (remove k m) k e; auto with map. + apply IHn. + assert (S n = S (cardinal (remove k m))). + { rewrite Heqn. + eapply cardinal_S; eauto with map. } + inversion H1; auto. + eapply max_elt_Above; eauto. + + apply X; apply max_elt_Empty; auto. + Qed. + + Lemma map_induction_min : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, Below x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. + apply X; apply cardinal_inv_1; auto. + + case_eq (min_elt m); intros. + destruct p. + assert (Add k e (remove k m) m). + { apply min_elt_MapsTo, find_spec, add_id in H. + unfold Add. symmetry. now rewrite add_remove_1. } + apply X0 with (remove k m) k e; auto. + apply IHn. + assert (S n = S (cardinal (remove k m))). + { rewrite Heqn. + eapply cardinal_S; eauto with map. } + inversion H1; auto. + eapply min_elt_Below; eauto. + + apply X; apply min_elt_Empty; auto. + Qed. + + End Induction_Principles. + + Section Fold_properties. + + (** The following lemma has already been proved on Weak Maps, + but with one additionnal hypothesis (some [transpose] fact). *) + + Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A), + Proper (E.eq==>eq==>eqA==>eqA) f -> + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + intros m1 m2 A eqA st f i Hf Heq. + rewrite 2 fold_spec_right. + apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. + intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto. + apply eqlistA_rev. apply bindings_Equal_eqlistA. auto. + Qed. + + Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f), + Above x m1 -> Add x e m1 m2 -> + eqA (fold f m2 i) (f x e (fold f m1 i)). + Proof. + intros. rewrite 2 fold_spec_right. set (f':=uncurry f). + transitivity (fold_right f' i (rev (bindings m1 ++ (x,e)::nil))). + apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. + intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto. + apply eqlistA_rev. + apply bindings_Add_Above; auto. + rewrite distr_rev; simpl. + reflexivity. + Qed. + + Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f), + Below x m1 -> Add x e m1 m2 -> + eqA (fold f m2 i) (fold f m1 (f x e i)). + Proof. + intros. rewrite 2 fold_spec_right. set (f':=uncurry f). + transitivity (fold_right f' i (rev (((x,e)::nil)++bindings m1))). + apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. + intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto. + apply eqlistA_rev. + simpl; apply bindings_Add_Below; auto. + rewrite distr_rev; simpl. + rewrite fold_right_app. + reflexivity. + Qed. + + End Fold_properties. + + End Elt. + +End OrdProperties. diff --git a/theories/MMaps/MMapInterface.v b/theories/MMaps/MMapInterface.v new file mode 100644 index 0000000000..05c5e5d8fb --- /dev/null +++ b/theories/MMaps/MMapInterface.v @@ -0,0 +1,292 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* elt->bool) e1 e2 := cmp e1 e2 = true. + +(** ** Weak signature for maps + + No requirements for an ordering on keys nor elements, only decidability + of equality on keys. First, a functorial signature: *) + +Module Type WSfun (E : DecidableType). + + Definition key := E.t. + Hint Transparent key. + + Definition eq_key {elt} (p p':key*elt) := E.eq (fst p) (fst p'). + + Definition eq_key_elt {elt} (p p':key*elt) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Parameter t : Type -> Type. + (** the abstract type of maps *) + + Section Ops. + + Parameter empty : forall {elt}, t elt. + (** The empty map. *) + + Variable elt:Type. + + Parameter is_empty : t elt -> bool. + (** Test whether a map is empty or not. *) + + Parameter add : key -> elt -> t elt -> t elt. + (** [add x y m] returns a map containing the same bindings as [m], + plus a binding of [x] to [y]. If [x] was already bound in [m], + its previous binding disappears. *) + + Parameter find : key -> t elt -> option elt. + (** [find x m] returns the current binding of [x] in [m], + or [None] if no such binding exists. *) + + Parameter remove : key -> t elt -> t elt. + (** [remove x m] returns a map containing the same bindings as [m], + except for [x] which is unbound in the returned map. *) + + Parameter mem : key -> t elt -> bool. + (** [mem x m] returns [true] if [m] contains a binding for [x], + and [false] otherwise. *) + + Parameter bindings : t elt -> list (key*elt). + (** [bindings m] returns an assoc list corresponding to the bindings + of [m], in any order. *) + + Parameter cardinal : t elt -> nat. + (** [cardinal m] returns the number of bindings in [m]. *) + + Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A. + (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], + where [k1] ... [kN] are the keys of all bindings in [m] + (in any order), and [d1] ... [dN] are the associated data. *) + + Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool. + (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal, + that is, contain equal keys and associate them with equal data. + [cmp] is the equality predicate used to compare the data associated + with the keys. *) + + Variable elt' elt'' : Type. + + Parameter map : (elt -> elt') -> t elt -> t elt'. + (** [map f m] returns a map with same domain as [m], where the associated + value a of all bindings of [m] has been replaced by the result of the + application of [f] to [a]. Since Coq is purely functional, the order + in which the bindings are passed to [f] is irrelevant. *) + + Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'. + (** Same as [map], but the function receives as arguments both the + key and the associated value for each binding of the map. *) + + Parameter merge : (key -> option elt -> option elt' -> option elt'') -> + t elt -> t elt' -> t elt''. + (** [merge f m m'] creates a new map whose bindings belong to the ones + of either [m] or [m']. The presence and value for a key [k] is + determined by [f k e e'] where [e] and [e'] are the (optional) + bindings of [k] in [m] and [m']. *) + + End Ops. + Section Specs. + + Variable elt:Type. + + Parameter MapsTo : key -> elt -> t elt -> Prop. + + Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m. + + Global Declare Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + + Variable m m' : t elt. + Variable x y : key. + Variable e : elt. + + Parameter find_spec : find x m = Some e <-> MapsTo x e m. + Parameter mem_spec : mem x m = true <-> In x m. + Parameter empty_spec : find x (@empty elt) = None. + Parameter is_empty_spec : is_empty m = true <-> forall x, find x m = None. + Parameter add_spec1 : find x (add x e m) = Some e. + Parameter add_spec2 : ~E.eq x y -> find y (add x e m) = find y m. + Parameter remove_spec1 : find x (remove x m) = None. + Parameter remove_spec2 : ~E.eq x y -> find y (remove x m) = find y m. + + (** Specification of [bindings] *) + Parameter bindings_spec1 : + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + (** When compared with ordered maps, here comes the only + property that is really weaker: *) + Parameter bindings_spec2w : NoDupA eq_key (bindings m). + + (** Specification of [cardinal] *) + Parameter cardinal_spec : cardinal m = length (bindings m). + + (** Specification of [fold] *) + Parameter fold_spec : + forall {A} (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + + (** Equality of maps *) + + (** Caveat: there are at least three distinct equality predicates on maps. + - The simpliest (and maybe most natural) way is to consider keys up to + their equivalence [E.eq], but elements up to Leibniz equality, in + the spirit of [eq_key_elt] above. This leads to predicate [Equal]. + - Unfortunately, this [Equal] predicate can't be used to describe + the [equal] function, since this function (for compatibility with + ocaml) expects a boolean comparison [cmp] that may identify more + elements than Leibniz. So logical specification of [equal] is done + via another predicate [Equivb] + - This predicate [Equivb] is quite ad-hoc with its boolean [cmp], + it can be generalized in a [Equiv] expecting a more general + (possibly non-decidable) equality predicate on elements *) + + Definition Equal (m m':t elt) := forall y, find y m = find y m'. + Definition Equiv (eq_elt:elt->elt->Prop) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). + Definition Equivb (cmp: elt->elt->bool) := Equiv (Cmp cmp). + + (** Specification of [equal] *) + Parameter equal_spec : forall cmp : elt -> elt -> bool, + equal cmp m m' = true <-> Equivb cmp m m'. + + End Specs. + Section SpecMaps. + + Variables elt elt' elt'' : Type. + + Parameter map_spec : forall (f:elt->elt') m x, + find x (map f m) = option_map f (find x m). + + Parameter mapi_spec : forall (f:key->elt->elt') m x, + exists y:key, E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + + Parameter merge_spec1 : + forall (f:key->option elt->option elt'->option elt'') m m' x, + In x m \/ In x m' -> + exists y:key, E.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). + + Parameter merge_spec2 : + forall (f:key -> option elt->option elt'->option elt'') m m' x, + In x (merge f m m') -> In x m \/ In x m'. + + End SpecMaps. +End WSfun. + +(** ** Static signature for Weak Maps + + Similar to [WSfun] but expressed in a self-contained way. *) + +Module Type WS. + Declare Module E : DecidableType. + Include WSfun E. +End WS. + + + +(** ** Maps on ordered keys, functorial signature *) + +Module Type Sfun (E : OrderedType). + Include WSfun E. + + Definition lt_key {elt} (p p':key*elt) := E.lt (fst p) (fst p'). + + (** Additional specification of [bindings] *) + + Parameter bindings_spec2 : forall {elt}(m : t elt), sort lt_key (bindings m). + + (** Remark: since [fold] is specified via [bindings], this stronger + specification of [bindings] has an indirect impact on [fold], + which can now be proved to receive bindings in increasing order. *) + +End Sfun. + + +(** ** Maps on ordered keys, self-contained signature *) + +Module Type S. + Declare Module E : OrderedType. + Include Sfun E. +End S. + + + +(** ** Maps with ordering both on keys and datas *) + +Module Type Sord. + + Declare Module Data : OrderedType. + Declare Module MapS : S. + Import MapS. + + Definition t := MapS.t Data.t. + + Include HasEq <+ HasLt <+ IsEq <+ IsStrOrder. + + Definition cmp e e' := + match Data.compare e e' with Eq => true | _ => false end. + + Parameter eq_spec : forall m m', eq m m' <-> Equivb cmp m m'. + + Parameter compare : t -> t -> comparison. + + Parameter compare_spec : forall m1 m2, CompSpec eq lt m1 m2 (compare m1 m2). + +End Sord. + + +(* TODO: provides filter + partition *) + +(* TODO: provide split + Parameter split : key -> t elt -> t elt * option elt * t elt. + + Parameter split_spec k m : + split k m = (filter (fun x -> E.compare x k) m, find k m, filter ...) + + min_binding, max_binding, choose ? +*) diff --git a/theories/MMaps/MMapWeakList.v b/theories/MMaps/MMapWeakList.v new file mode 100644 index 0000000000..656c61e112 --- /dev/null +++ b/theories/MMaps/MMapWeakList.v @@ -0,0 +1,687 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* a = a'. +Proof. split; congruence. Qed. + +Module Raw (X:DecidableType). + +Module Import PX := KeyDecidableType X. + +Definition key := X.t. +Definition t (elt:Type) := list (X.t * elt). + +Ltac dec := match goal with + | |- context [ X.eq_dec ?x ?x ] => + let E := fresh "E" in destruct (X.eq_dec x x) as [E|E]; [ | now elim E] + | H : X.eq ?x ?y |- context [ X.eq_dec ?x ?y ] => + let E := fresh "E" in destruct (X.eq_dec x y) as [_|E]; [ | now elim E] + | H : ~X.eq ?x ?y |- context [ X.eq_dec ?x ?y ] => + let E := fresh "E" in destruct (X.eq_dec x y) as [E|_]; [ now elim H | ] + | |- context [ X.eq_dec ?x ?y ] => + let E := fresh "E" in destruct (X.eq_dec x y) as [E|E] +end. + +Section Elt. + +Variable elt : Type. +Notation NoDupA := (@NoDupA _ eqk). + +(** * [find] *) + +Fixpoint find (k:key) (s: t elt) : option elt := + match s with + | nil => None + | (k',x)::s' => if X.eq_dec k k' then Some x else find k s' + end. + +Lemma find_spec : forall m (Hm:NoDupA m) x e, + find x m = Some e <-> MapsTo x e m. +Proof. + unfold PX.MapsTo. + induction m as [ | (k,e) m IH]; simpl. + - split; inversion 1. + - intros Hm k' e'. rewrite InA_cons. + change (eqke (k',e') (k,e)) with (X.eq k' k /\ e' = e). + inversion_clear Hm. dec. + + rewrite Some_iff; intuition. + elim H. apply InA_eqk with (k',e'); auto. + + rewrite IH; intuition. +Qed. + +(** * [mem] *) + +Fixpoint mem (k : key) (s : t elt) : bool := + match s with + | nil => false + | (k',_) :: l => if X.eq_dec k k' then true else mem k l + end. + +Lemma mem_spec : forall m (Hm:NoDupA m) x, mem x m = true <-> In x m. +Proof. + induction m as [ | (k,e) m IH]; simpl; intros Hm x. + - split. discriminate. inversion_clear 1. inversion H0. + - inversion_clear Hm. rewrite PX.In_cons; simpl. + rewrite <- IH by trivial. + dec; intuition. +Qed. + +(** * [empty] *) + +Definition empty : t elt := nil. + +Lemma empty_spec x : find x empty = None. +Proof. + reflexivity. +Qed. + +Lemma empty_NoDup : NoDupA empty. +Proof. + unfold empty; auto. +Qed. + +(** * [is_empty] *) + +Definition is_empty (l : t elt) : bool := if l then true else false. + +Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. +Proof. + destruct m; simpl; intuition; try discriminate. + specialize (H a). + revert H. now dec. +Qed. + +(* Not part of the exported specifications, used later for [merge]. *) + +Lemma find_eq : forall m (Hm:NoDupA m) x x', + X.eq x x' -> find x m = find x' m. +Proof. + induction m; simpl; auto; destruct a; intros. + inversion_clear Hm. + rewrite (IHm H1 x x'); auto. + dec; dec; trivial. + elim E0. now transitivity x. + elim E. now transitivity x'. +Qed. + +(** * [add] *) + +Fixpoint add (k : key) (x : elt) (s : t elt) : t elt := + match s with + | nil => (k,x) :: nil + | (k',y) :: l => if X.eq_dec k k' then (k,x)::l else (k',y)::add k x l + end. + +Lemma add_spec1 m x e : find x (add x e m) = Some e. +Proof. + induction m as [ | (k,e') m IH]; simpl. + - now dec. + - dec; simpl; now dec. +Qed. + +Lemma add_spec2 m x y e : ~X.eq x y -> find y (add x e m) = find y m. +Proof. + intros N. + assert (N' : ~X.eq y x) by now contradict N. + induction m as [ | (k,e') m IH]; simpl. + - dec; trivial. + - repeat (dec; simpl); trivial. elim N. now transitivity k. +Qed. + +Lemma add_InA : forall m x y e e', + ~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m. +Proof. + induction m as [ | (k,e') m IH]; simpl; intros. + - inversion_clear H0. elim H. symmetry; apply H1. inversion_clear H1. + - revert H0; dec; rewrite !InA_cons. + + rewrite E. intuition. + + intuition. right; eapply IH; eauto. +Qed. + +Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m). +Proof. + induction m as [ | (k,e') m IH]; simpl; intros Hm x e. + - constructor; auto. now inversion 1. + - inversion_clear Hm. dec; constructor; auto. + + contradict H. apply InA_eqk with (x,e); auto. + + contradict H; apply add_InA with x e; auto. +Qed. + +(** * [remove] *) + +Fixpoint remove (k : key) (s : t elt) : t elt := + match s with + | nil => nil + | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l + end. + +Lemma remove_spec1 m (Hm: NoDupA m) x : find x (remove x m) = None. +Proof. + induction m as [ | (k,e') m IH]; simpl; trivial. + inversion_clear Hm. + repeat (dec; simpl); auto. + destruct (find x m) eqn:F; trivial. + apply find_spec in F; trivial. + elim H. apply InA_eqk with (x,e); auto. +Qed. + +Lemma remove_spec2 m (Hm: NoDupA m) x y : ~X.eq x y -> + find y (remove x m) = find y m. +Proof. + induction m as [ | (k,e') m IH]; simpl; trivial; intros E. + inversion_clear Hm. + repeat (dec; simpl); auto. + elim E. now transitivity k. +Qed. + +Lemma remove_InA : forall m (Hm:NoDupA m) x y e, + InA eqk (y,e) (remove x m) -> InA eqk (y,e) m. +Proof. + induction m as [ | (k,e') m IH]; simpl; trivial; intros. + inversion_clear Hm. + revert H; dec; rewrite !InA_cons; intuition. + right; eapply H; eauto. +Qed. + +Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m). +Proof. + induction m. + simpl; intuition. + intros. + inversion_clear Hm. + destruct a as (x',e'). + simpl; case (X.eq_dec x x'); auto. + constructor; auto. + contradict H; apply remove_InA with x; auto. +Qed. + +(** * [bindings] *) + +Definition bindings (m: t elt) := m. + +Lemma bindings_spec1 m x e : InA eqke (x,e) (bindings m) <-> MapsTo x e m. +Proof. + reflexivity. +Qed. + +Lemma bindings_spec2w m (Hm:NoDupA m) : NoDupA (bindings m). +Proof. + trivial. +Qed. + +(** * [fold] *) + +Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc : A) : A := + match m with + | nil => acc + | (k,e)::m' => fold f m' (f k e acc) + end. + +Lemma fold_spec : forall m (A:Type)(i:A)(f:key->elt->A->A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. +Proof. + induction m as [ | (k,e) m IH]; simpl; auto. +Qed. + +(** * [equal] *) + +Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) := + match find k m' with + | None => false + | Some e' => cmp e e' + end. + +Definition submap (cmp : elt -> elt -> bool)(m m' : t elt) : bool := + fold (fun k e b => andb (check cmp k e m') b) m true. + +Definition equal (cmp : elt -> elt -> bool)(m m' : t elt) : bool := + andb (submap cmp m m') (submap (fun e' e => cmp e e') m' m). + +Definition Submap (cmp:elt->elt->bool) m m' := + (forall k, In k m -> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Definition Equivb (cmp:elt->elt->bool) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + Submap cmp m m' -> submap cmp m m' = true. +Proof. + unfold Submap, submap. + induction m. + simpl; auto. + destruct a; simpl; intros. + destruct H. + inversion_clear Hm. + assert (H3 : In t0 m'). + { apply H; exists e; auto with *. } + destruct H3 as (e', H3). + assert (H4 : find t0 m' = Some e') by now apply find_spec. + unfold check at 2. rewrite H4. + rewrite (H0 t0); simpl; auto with *. + eapply IHm; auto. + split; intuition. + apply H. + destruct H6 as (e'',H6); exists e''; auto. + apply H0 with k; auto. +Qed. + +Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + submap cmp m m' = true -> Submap cmp m m'. +Proof. + unfold Submap, submap. + induction m. + simpl; auto. + intuition. + destruct H0; inversion H0. + inversion H0. + + destruct a; simpl; intros. + inversion_clear Hm. + rewrite andb_b_true in H. + assert (check cmp t0 e m' = true). + clear H1 H0 Hm' IHm. + set (b:=check cmp t0 e m') in *. + generalize H; clear H; generalize b; clear b. + induction m; simpl; auto; intros. + destruct a; simpl in *. + destruct (andb_prop _ _ (IHm _ H)); auto. + rewrite H2 in H. + destruct (IHm H1 m' Hm' cmp H); auto. + unfold check in H2. + case_eq (find t0 m'); [intros e' H5 | intros H5]; + rewrite H5 in H2; try discriminate. + split; intros. + destruct H6 as (e0,H6); inversion_clear H6. + compute in H7; destruct H7; subst. + exists e'. + apply PX.MapsTo_eq with t0; auto with *. + apply find_spec; auto. + apply H3. + exists e0; auto. + inversion_clear H6. + compute in H8; destruct H8; subst. + assert (H8 : MapsTo t0 e'0 m'). { eapply PX.MapsTo_eq; eauto. } + apply find_spec in H8; trivial. congruence. + apply H4 with k; auto. +Qed. + +(** Specification of [equal] *) + +Lemma equal_spec : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, + equal cmp m m' = true <-> Equivb cmp m m'. +Proof. + unfold Equivb, equal. + split. + - intros. + destruct (andb_prop _ _ H); clear H. + generalize (submap_2 Hm Hm' H0). + generalize (submap_2 Hm' Hm H1). + firstorder. + - intuition. + apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder. +Qed. +End Elt. +Section Elt2. +Variable elt elt' : Type. + +(** * [map] and [mapi] *) + +Fixpoint map (f:elt -> elt') (m:t elt) : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f e) :: map f m' + end. + +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := + match m with + | nil => nil + | (k,e)::m' => (k,f k e) :: mapi f m' + end. + +(** Specification of [map] *) + +Lemma map_spec (f:elt->elt')(m:t elt)(x:key) : + find x (map f m) = option_map f (find x m). +Proof. + induction m as [ | (k,e) m IH]; simpl; trivial. + dec; simpl; trivial. +Qed. + +Lemma map_NoDup m (Hm : NoDupA (@eqk elt) m)(f:elt->elt') : + NoDupA (@eqk elt') (map f m). +Proof. + induction m; simpl; auto. + intros. + destruct a as (x',e'). + inversion_clear Hm. + constructor; auto. + contradict H. + clear IHm H0. + induction m; simpl in *; auto. + inversion H. + destruct a; inversion H; auto. +Qed. + +(** Specification of [mapi] *) + +Lemma mapi_spec (f:key->elt->elt')(m:t elt)(x:key) : + exists y, X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). +Proof. + induction m as [ | (k,e) m IH]; simpl; trivial. + - now exists x. + - dec; simpl. + + now exists k. + + destruct IH as (y,(Hy,H)). now exists y. +Qed. + +Lemma mapi_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f: key->elt->elt'), + NoDupA (@eqk elt') (mapi f m). +Proof. + induction m; simpl; auto. + intros. + destruct a as (x',e'). + inversion_clear Hm; auto. + constructor; auto. + contradict H. + clear IHm H0. + induction m; simpl in *; auto. + inversion_clear H. + destruct a; inversion_clear H; auto. +Qed. + +End Elt2. + +Lemma mapfst_InA {elt}(m:t elt) x : + InA X.eq x (List.map fst m) <-> In x m. +Proof. + induction m as [| (k,e) m IH]; simpl; auto. + - split; inversion 1. inversion H0. + - rewrite InA_cons, In_cons. simpl. now rewrite IH. +Qed. + +Lemma mapfst_NoDup {elt}(m:t elt) : + NoDupA X.eq (List.map fst m) <-> NoDupA eqk m. +Proof. + induction m as [| (k,e) m IH]; simpl. + - split; constructor. + - split; inversion_clear 1; constructor; try apply IH; trivial. + + contradict H0. rewrite mapfst_InA. eapply In_alt'; eauto. + + rewrite mapfst_InA. contradict H0. now apply In_alt'. +Qed. + +Lemma filter_NoDup f (m:list key) : + NoDupA X.eq m -> NoDupA X.eq (List.filter f m). +Proof. + induction 1; simpl. + - constructor. + - destruct (f x); trivial. constructor; trivial. + contradict H. rewrite InA_alt in *. destruct H as (y,(Hy,H)). + exists y; split; trivial. now rewrite filter_In in H. +Qed. + +Lemma NoDupA_unique_repr (l:list key) x y : + NoDupA X.eq l -> X.eq x y -> List.In x l -> List.In y l -> x = y. +Proof. + intros H E Hx Hy. + induction H; simpl in *. + - inversion Hx. + - intuition; subst; trivial. + elim H. apply InA_alt. now exists y. + elim H. apply InA_alt. now exists x. +Qed. + +Section Elt3. + +Variable elt elt' elt'' : Type. + +Definition restrict (m:t elt)(k:key) := + match find k m with + | None => true + | Some _ => false + end. + +Definition domains (m:t elt)(m':t elt') := + List.map fst m ++ List.filter (restrict m) (List.map fst m'). + +Lemma domains_InA m m' (Hm : NoDupA eqk m) x : + InA X.eq x (domains m m') <-> In x m \/ In x m'. +Proof. + unfold domains. + assert (Proper (X.eq==>eq) (restrict m)). + { intros k k' Hk. unfold restrict. now rewrite (find_eq Hm Hk). } + rewrite InA_app_iff, filter_InA, !mapfst_InA; intuition. + unfold restrict. + destruct (find x m) eqn:F. + - left. apply find_spec in F; trivial. now exists e. + - now right. +Qed. + +Lemma domains_NoDup m m' : NoDupA eqk m -> NoDupA eqk m' -> + NoDupA X.eq (domains m m'). +Proof. + intros Hm Hm'. unfold domains. + apply NoDupA_app; auto with *. + - now apply mapfst_NoDup. + - now apply filter_NoDup, mapfst_NoDup. + - intros x. + rewrite mapfst_InA. intros (e,H). + apply find_spec in H; trivial. + rewrite InA_alt. intros (y,(Hy,H')). + rewrite (find_eq Hm Hy) in H. + rewrite filter_In in H'. destruct H' as (_,H'). + unfold restrict in H'. now rewrite H in H'. +Qed. + +Fixpoint fold_keys (f:key->option elt'') l := + match l with + | nil => nil + | k::l => + match f k with + | Some e => (k,e)::fold_keys f l + | None => fold_keys f l + end + end. + +Lemma fold_keys_In f l x e : + List.In (x,e) (fold_keys f l) <-> List.In x l /\ f x = Some e. +Proof. + induction l as [|k l IH]; simpl. + - intuition. + - destruct (f k) eqn:F; simpl; rewrite IH; clear IH; intuition; + try left; congruence. +Qed. + +Lemma fold_keys_NoDup f l : + NoDupA X.eq l -> NoDupA eqk (fold_keys f l). +Proof. + induction 1; simpl. + - constructor. + - destruct (f x); trivial. + constructor; trivial. contradict H. + apply InA_alt in H. destruct H as ((k,e'),(E,H)). + rewrite fold_keys_In in H. + apply InA_alt. exists k. now split. +Qed. + +Variable f : key -> option elt -> option elt' -> option elt''. + +Definition merge m m' : t elt'' := + fold_keys (fun k => f k (find k m) (find k m')) (domains m m'). + +Lemma merge_NoDup m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m') : + NoDupA (@eqk elt'') (merge m m'). +Proof. + now apply fold_keys_NoDup, domains_NoDup. +Qed. + +Lemma merge_spec1 m (Hm:NoDupA eqk m) m' (Hm':NoDupA eqk m') x : + In x m \/ In x m' -> + exists y:key, X.eq y x /\ + find x (merge m m') = f y (find x m) (find x m'). +Proof. + assert (Hmm' : NoDupA eqk (merge m m')) by now apply merge_NoDup. + rewrite <- domains_InA; trivial. + rewrite InA_alt. intros (y,(Hy,H)). + exists y; split; [easy|]. + rewrite (find_eq Hm Hy), (find_eq Hm' Hy). + destruct (f y (find y m) (find y m')) eqn:F. + - apply find_spec; trivial. + red. apply InA_alt. exists (y,e). split. now split. + unfold merge. apply fold_keys_In. now split. + - destruct (find x (merge m m')) eqn:F'; trivial. + rewrite <- F; clear F. symmetry. + apply find_spec in F'; trivial. + red in F'. rewrite InA_alt in F'. + destruct F' as ((y',e'),(E,F')). + unfold merge in F'; rewrite fold_keys_In in F'. + destruct F' as (H',F'). + compute in E; destruct E as (Hy',<-). + replace y with y'; trivial. + apply (@NoDupA_unique_repr (domains m m')); auto. + now apply domains_NoDup. + now transitivity x. +Qed. + +Lemma merge_spec2 m (Hm:NoDupA eqk m) m' (Hm':NoDupA eqk m') x : + In x (merge m m') -> In x m \/ In x m'. +Proof. + rewrite <- domains_InA; trivial. + intros (e,H). red in H. rewrite InA_alt in H. destruct H as ((k,e'),(E,H)). + unfold merge in H; rewrite fold_keys_In in H. destruct H as (H,_). + apply InA_alt. exists k. split; trivial. now destruct E. +Qed. + +End Elt3. +End Raw. + + +Module Make (X: DecidableType) <: WS with Module E:=X. + Module Raw := Raw X. + + Module E := X. + Definition key := E.t. + Definition eq_key {elt} := @Raw.PX.eqk elt. + Definition eq_key_elt {elt} := @Raw.PX.eqke elt. + + Record t_ (elt:Type) := Mk + {this :> Raw.t elt; + nodup : NoDupA Raw.PX.eqk this}. + Definition t := t_. + + Definition empty {elt} : t elt := Mk (Raw.empty_NoDup elt). + +Section Elt. + Variable elt elt' elt'':Type. + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition find x m : option elt := Raw.find x m.(this). + Definition mem x m : bool := Raw.mem x m.(this). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Mk (Raw.add_NoDup m.(nodup) x e). + Definition remove x m : t elt := Mk (Raw.remove_NoDup m.(nodup) x). + Definition map f m : t elt' := Mk (Raw.map_NoDup m.(nodup) f). + Definition mapi (f:key->elt->elt') m : t elt' := + Mk (Raw.mapi_NoDup m.(nodup) f). + Definition merge f m (m':t elt') : t elt'' := + Mk (Raw.merge_NoDup f m.(nodup) m'.(nodup)). + Definition bindings m : list (key*elt) := Raw.bindings m.(this). + Definition cardinal m := length m.(this). + Definition fold {A}(f:key->elt->A->A) m (i:A) : A := Raw.fold f m.(this) i. + Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this). + Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this). + Definition In x m : Prop := Raw.PX.In x m.(this). + + Definition Equal m m' := forall y, find y m = find y m'. + Definition Equiv (eq_elt:elt->elt->Prop) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). + Definition Equivb cmp m m' : Prop := Raw.Equivb cmp m.(this) m'.(this). + + Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros x x' Hx e e' <- m m' <-. unfold MapsTo. now rewrite Hx. + Qed. + + Lemma find_spec m : forall x e, find x m = Some e <-> MapsTo x e m. + Proof. exact (Raw.find_spec m.(nodup)). Qed. + + Lemma mem_spec m : forall x, mem x m = true <-> In x m. + Proof. exact (Raw.mem_spec m.(nodup)). Qed. + + Lemma empty_spec : forall x, find x empty = None. + Proof. exact (Raw.empty_spec _). Qed. + + Lemma is_empty_spec m : is_empty m = true <-> (forall x, find x m = None). + Proof. exact (Raw.is_empty_spec m.(this)). Qed. + + Lemma add_spec1 m : forall x e, find x (add x e m) = Some e. + Proof. exact (Raw.add_spec1 m.(this)). Qed. + Lemma add_spec2 m : forall x y e, ~E.eq x y -> find y (add x e m) = find y m. + Proof. exact (Raw.add_spec2 m.(this)). Qed. + + Lemma remove_spec1 m : forall x, find x (remove x m) = None. + Proof. exact (Raw.remove_spec1 m.(nodup)). Qed. + Lemma remove_spec2 m : forall x y, ~E.eq x y -> find y (remove x m) = find y m. + Proof. exact (Raw.remove_spec2 m.(nodup)). Qed. + + Lemma bindings_spec1 m : forall x e, + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + Proof. exact (Raw.bindings_spec1 m.(this)). Qed. + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. exact (Raw.bindings_spec2w m.(nodup)). Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. reflexivity. Qed. + + Lemma fold_spec m : forall (A : Type) (i : A) (f : key -> elt -> A -> A), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + Proof. exact (Raw.fold_spec m.(this)). Qed. + + Lemma equal_spec m m' : forall cmp, equal cmp m m' = true <-> Equivb cmp m m'. + Proof. exact (Raw.equal_spec m.(nodup) m'.(nodup)). Qed. + +End Elt. + + Lemma map_spec {elt elt'} (f:elt->elt') m : + forall x, find x (map f m) = option_map f (find x m). + Proof. exact (Raw.map_spec f m.(this)). Qed. + + Lemma mapi_spec {elt elt'} (f:key->elt->elt') m : + forall x, exists y, + E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + Proof. exact (Raw.mapi_spec f m.(this)). Qed. + + Lemma merge_spec1 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' : + forall x, + In x m \/ In x m' -> + exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m'). + Proof. exact (Raw.merge_spec1 f m.(nodup) m'.(nodup)). Qed. + + Lemma merge_spec2 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' : + forall x, + In x (merge f m m') -> In x m \/ In x m'. + Proof. exact (Raw.merge_spec2 m.(nodup) m'.(nodup)). Qed. + +End Make. diff --git a/theories/MMaps/MMaps.v b/theories/MMaps/MMaps.v new file mode 100644 index 0000000000..93d1178175 --- /dev/null +++ b/theories/MMaps/MMaps.v @@ -0,0 +1,18 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* InA eqk x m. - Proof. - unfold eqke, RelProd; induction 1; firstorder. - Qed. - Hint Resolve InA_eqke_eqk. + Lemma eqke_def {elt} k k' (e e':elt) : + eqke (k,e) (k',e') = (D.eq k k' /\ e = e'). + Proof. reflexivity. Defined. - Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. - Proof. - intros. rewrite <- H; auto. - Qed. + Lemma eqke_def' {elt} (p q:key*elt) : + eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q). + Proof. reflexivity. Defined. - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. + Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'. + Proof. now destruct 1. Qed. - Hint Unfold MapsTo In. + Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'. + Proof. now destruct 1. Qed. - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) + Lemma eqk_def {elt} k k' (e e':elt) : eqk (k,e) (k',e') = D.eq k k'. + Proof. reflexivity. Defined. - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. - firstorder. - exists x; auto. - induction H. - destruct y; compute in H. - exists e; left; auto. - destruct IHInA as [e H0]. - exists e; auto. - Qed. - - Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l. - Proof. + Lemma eqk_def' {elt} (p q:key*elt) : eqk p q = D.eq (fst p) (fst q). + Proof. reflexivity. Qed. + + Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'. + Proof. trivial. Qed. + + Hint Resolve eqke_1 eqke_2 eqk_1. + + (* Additionnal facts *) + + Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) : + InA eqke p m -> InA eqk p m. + Proof. + induction 1; firstorder. + Qed. + Hint Resolve InA_eqke_eqk. + + Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : + InA eqk p m -> exists q, eqk p q /\ InA eqke q m. + Proof. + induction 1; firstorder. + Qed. + + Lemma InA_eqk {elt} p q (m:list (key*elt)) : + eqk p q -> InA eqk p m -> InA eqk q m. + Proof. + now intros <-. + Qed. + + Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e). + Definition In {elt} k m := exists e:elt, MapsTo k e m. + + Hint Unfold MapsTo In. + + (* Alternative formulations for [In k l] *) + + Lemma In_alt {elt} k (l:list (key*elt)) : + In k l <-> exists e, InA eqk (k,e) l. + Proof. + unfold In, MapsTo. + split; intros (e,H). + - exists e; auto. + - apply InA_eqk_eqke in H. destruct H as ((k',e'),(E,H)). + compute in E. exists e'. now rewrite E. + Qed. + + Lemma In_alt' {elt} (l:list (key*elt)) k e : + In k l <-> InA eqk (k,e) l. + Proof. + rewrite In_alt. firstorder. eapply InA_eqk; eauto. now compute. + Qed. + + Lemma In_alt2 {elt} k (l:list (key*elt)) : + In k l <-> Exists (fun p => D.eq k (fst p)) l. + Proof. unfold In, MapsTo. setoid_rewrite Exists_exists; setoid_rewrite InA_alt. firstorder. exists (snd x), x; auto. - Qed. - - Lemma In_nil : forall k, In k nil <-> False. - Proof. - intros; rewrite In_alt2; apply Exists_nil. - Qed. - - Lemma In_cons : forall k p l, - In k (p::l) <-> eq k (fst p) \/ In k l. - Proof. - intros; rewrite !In_alt2, Exists_cons; intuition. - Qed. - - Global Instance MapsTo_compat : - Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo. - Proof. + Qed. + + Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False. + Proof. + rewrite In_alt2; apply Exists_nil. + Qed. + + Lemma In_cons {elt} k p (l:list (key*elt)) : + In k (p::l) <-> D.eq k (fst p) \/ In k l. + Proof. + rewrite !In_alt2, Exists_cons; intuition. + Qed. + + Instance MapsTo_compat {elt} : + Proper (D.eq==>Logic.eq==>equivlistA eqke==>iff) (@MapsTo elt). + Proof. intros x x' Hx e e' He l l' Hl. unfold MapsTo. rewrite Hx, He, Hl; intuition. - Qed. + Qed. - Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. - Proof. + Instance In_compat {elt} : Proper (D.eq==>equivlistA eqk==>iff) (@In elt). + Proof. intros x x' Hx l l' Hl. rewrite !In_alt. setoid_rewrite Hl. setoid_rewrite Hx. intuition. - Qed. - - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. - Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed. + Qed. - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. - Proof. intros l x y EQ. rewrite <- EQ; auto. Qed. + Lemma MapsTo_eq {elt} (l:list (key*elt)) x y e : + D.eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. now intros <-. Qed. - Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. - Proof. - intros; invlist In; invlist MapsTo. compute in * |- ; intuition. - right; exists x; auto. - Qed. + Lemma In_eq {elt} (l:list (key*elt)) x y : + D.eq x y -> In x l -> In y l. + Proof. now intros <-. Qed. - Lemma In_inv_2 : forall k k' e e' l, - InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. - Proof. - intros; invlist InA; intuition. - Qed. + Lemma In_inv {elt} k k' e (l:list (key*elt)) : + In k ((k',e) :: l) -> D.eq k k' \/ In k l. + Proof. + intros (e',H). red in H. rewrite InA_cons, eqke_def in H. + intuition. right. now exists e'. + Qed. - Lemma In_inv_3 : forall x x' l, - InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. - Proof. - intros; invlist InA; compute in * |- ; intuition. - Qed. + Lemma In_inv_2 {elt} k k' e e' (l:list (key*elt)) : + InA eqk (k, e) ((k', e') :: l) -> ~ D.eq k k' -> InA eqk (k, e) l. + Proof. + rewrite InA_cons, eqk_def. intuition. + Qed. - End Elt. + Lemma In_inv_3 {elt} x x' (l:list (key*elt)) : + InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. + Proof. + rewrite InA_cons. destruct 1 as [H|H]; trivial. destruct 1. + eauto with *. + Qed. - Hint Unfold eqk eqke. Hint Extern 2 (eqke ?a ?b) => split. Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. Hint Resolve In_inv_2 In_inv_3. End KeyDecidableType. -(** * PairDecidableType - +(** * PairDecidableType + From two decidable types, we can build a new DecidableType over their cartesian product. *) diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 059992f5b0..4d49ac84ed 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -6,51 +6,47 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Export RelationPairs SetoidList Orders. +Require Export RelationPairs SetoidList Orders EqualitiesFacts. Set Implicit Arguments. Unset Strict Implicit. (** * Specialization of results about lists modulo. *) -Module OrderedTypeLists (Import O:OrderedType). +Module OrderedTypeLists (O:OrderedType). -Section ForNotations. - -Notation In:=(InA eq). -Notation Inf:=(lelistA lt). -Notation Sort:=(sort lt). -Notation NoDup:=(NoDupA eq). +Local Notation In:=(InA O.eq). +Local Notation Inf:=(lelistA O.lt). +Local Notation Sort:=(sort O.lt). +Local Notation NoDup:=(NoDupA O.eq). Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. Proof. intros. rewrite <- H; auto. Qed. Lemma ListIn_In : forall l x, List.In x l -> In x l. -Proof. exact (In_InA eq_equiv). Qed. +Proof. exact (In_InA O.eq_equiv). Qed. -Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. -Proof. exact (InfA_ltA lt_strorder). Qed. +Lemma Inf_lt : forall l x y, O.lt x y -> Inf y l -> Inf x l. +Proof. exact (InfA_ltA O.lt_strorder). Qed. -Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_compat). Qed. +Lemma Inf_eq : forall l x y, O.eq x y -> Inf y l -> Inf x l. +Proof. exact (InfA_eqA O.eq_equiv O.lt_compat). Qed. -Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. -Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. +Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> O.lt a x. +Proof. exact (SortA_InfA_InA O.eq_equiv O.lt_strorder O.lt_compat). Qed. -Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l. -Proof. exact (@In_InfA t lt). Qed. +Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> O.lt x y) -> Inf x l. +Proof. exact (@In_InfA O.t O.lt). Qed. -Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l. -Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed. +Lemma In_Inf : forall l x, (forall y, In y l -> O.lt x y) -> Inf x l. +Proof. exact (InA_InfA O.eq_equiv (ltA:=O.lt)). Qed. Lemma Inf_alt : - forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)). -Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed. + forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> O.lt x y)). +Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed. Lemma Sort_NoDup : forall l, Sort l -> NoDup l. -Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed. - -End ForNotations. +Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed. Hint Resolve ListIn_In Sort_NoDup Inf_lt. Hint Immediate In_eq Inf_lt. @@ -58,140 +54,66 @@ Hint Immediate In_eq Inf_lt. End OrderedTypeLists. +(** * Results about keys and data as manipulated in MMaps. *) +Module KeyOrderedType(O:OrderedType). + Include KeyDecidableType(O). (* provides eqk, eqke *) + Local Notation key:=O.t. + Local Open Scope signature_scope. -(** * Results about keys and data as manipulated in FMaps. *) - - -Module KeyOrderedType(Import O:OrderedType). - Module Import MO:=OrderedTypeLists(O). - - Section Elt. - Variable elt : Type. - Notation key:=t. - - Local Open Scope signature_scope. - - Definition eqk : relation (key*elt) := eq @@1. - Definition eqke : relation (key*elt) := eq * Logic.eq. - Definition ltk : relation (key*elt) := lt @@1. - - Hint Unfold eqk eqke ltk. + Definition ltk {elt} : relation (key*elt) := O.lt @@1. - (* eqke is stricter than eqk *) + Hint Unfold ltk. - Global Instance eqke_eqk : subrelation eqke eqk. - Proof. firstorder. Qed. + (* ltk is a strict order *) - (* eqk, eqke are equalities, ltk is a strict order *) + Instance ltk_strorder {elt} : StrictOrder (@ltk elt) := _. - Global Instance eqk_equiv : Equivalence eqk := _. + Instance ltk_compat {elt} : Proper (eqk==>eqk==>iff) (@ltk elt). + Proof. unfold eqk, ltk; auto with *. Qed. - Global Instance eqke_equiv : Equivalence eqke := _. + Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt). + Proof. eapply subrelation_proper; eauto with *. Qed. - Global Instance ltk_strorder : StrictOrder ltk := _. + (* Additionnal facts *) - Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. - Proof. unfold eqk, ltk; auto with *. Qed. + Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt). + Proof. apply pair_compat. Qed. - (* Additionnal facts *) - - Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt). - Proof. apply pair_compat. Qed. + Section Elt. + Variable elt : Type. + Implicit Type p q : key*elt. + Implicit Type l m : list (key*elt). - Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. + Lemma ltk_not_eqk p q : ltk p q -> ~ eqk p q. Proof. - intros e e' LT EQ; rewrite EQ in LT. + intros LT EQ; rewrite EQ in LT. elim (StrictOrder_Irreflexive _ LT). Qed. - Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. + Lemma ltk_not_eqke p q : ltk p q -> ~eqke p q. Proof. - intros e e' LT EQ; rewrite EQ in LT. + intros LT EQ; rewrite EQ in LT. elim (StrictOrder_Irreflexive _ LT). Qed. - Lemma InA_eqke_eqk : - forall x m, InA eqke x m -> InA eqk x m. - Proof. - unfold eqke, RelProd; induction 1; firstorder. - Qed. - Hint Resolve InA_eqke_eqk. - - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). - Hint Unfold MapsTo In. - - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) - - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. - firstorder. - exists x; auto. - induction H. - destruct y; compute in H. - exists e; left; auto. - destruct IHInA as [e H0]. - exists e; auto. - Qed. + Lemma Inf_eq l x x' : eqk x x' -> Inf x' l -> Inf x l. + Proof. now intros <-. Qed. - Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l. - Proof. - unfold In, MapsTo. - setoid_rewrite Exists_exists; setoid_rewrite InA_alt. - firstorder. - exists (snd x), x; auto. - Qed. - - Lemma In_nil : forall k, In k nil <-> False. - Proof. - intros; rewrite In_alt2; apply Exists_nil. - Qed. - - Lemma In_cons : forall k p l, - In k (p::l) <-> eq k (fst p) \/ In k l. - Proof. - intros; rewrite !In_alt2, Exists_cons; intuition. - Qed. - - Global Instance MapsTo_compat : - Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo. - Proof. - intros x x' Hx e e' He l l' Hl. unfold MapsTo. - rewrite Hx, He, Hl; intuition. - Qed. - - Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. - Proof. - intros x x' Hx l l' Hl. rewrite !In_alt. - setoid_rewrite Hl. setoid_rewrite Hx. intuition. - Qed. - - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. - Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed. - - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. - Proof. intros l x y EQ. rewrite <- EQ; auto. Qed. - - Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. intros l x x' H. rewrite H; auto. Qed. - - Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. + Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l. Proof. apply InfA_ltA; auto with *. Qed. Hint Immediate Inf_eq. Hint Resolve Inf_lt. - Lemma Sort_Inf_In : - forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. + Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p. Proof. apply SortA_InfA_InA; auto with *. Qed. - Lemma Sort_Inf_NotIn : - forall l k e, Sort l -> Inf (k,e) l -> ~In k l. + Lemma Sort_Inf_NotIn l k e : Sort l -> Inf (k,e) l -> ~In k l. Proof. intros; red; intros. destruct H1 as [e' H2]. @@ -200,57 +122,34 @@ Module KeyOrderedType(Import O:OrderedType). repeat red; reflexivity. Qed. - Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. + Lemma Sort_NoDupA l : Sort l -> NoDupA eqk l. Proof. apply SortA_NoDupA; auto with *. Qed. - Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. + Lemma Sort_In_cons_1 l p q : Sort (p::l) -> InA eqk q l -> ltk p q. Proof. intros; invlist sort; eapply Sort_Inf_In; eauto. Qed. - Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> - ltk e e' \/ eqk e e'. + Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) -> + ltk p q \/ eqk p q. Proof. intros; invlist InA; auto with relations. left; apply Sort_In_cons_1 with l; auto with relations. Qed. - Lemma Sort_In_cons_3 : - forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. + Lemma Sort_In_cons_3 x l k e : + Sort ((k,e)::l) -> In x l -> ~O.eq x k. Proof. intros; invlist sort; red; intros. eapply Sort_Inf_NotIn; eauto using In_eq. Qed. - Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. - Proof. - intros; invlist In; invlist MapsTo. compute in * |- ; intuition. - right; exists x; auto. - Qed. - - Lemma In_inv_2 : forall k k' e e' l, - InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. - Proof. - intros; invlist InA; intuition. - Qed. - - Lemma In_inv_3 : forall x x' l, - InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. - Proof. - intros; invlist InA; compute in * |- ; intuition. - Qed. - End Elt. - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. Hint Resolve ltk_not_eqk ltk_not_eqke. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. Hint Immediate Inf_eq. Hint Resolve Inf_lt. Hint Resolve Sort_Inf_NotIn. - Hint Resolve In_inv_2 In_inv_3. End KeyOrderedType. diff --git a/theories/theories.itarget b/theories/theories.itarget index 3a87d8cf14..4519070e45 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -3,6 +3,7 @@ Bool/vo.otarget Classes/vo.otarget FSets/vo.otarget MSets/vo.otarget +MMaps/vo.otarget Structures/vo.otarget Init/vo.otarget Lists/vo.otarget -- cgit v1.2.3