diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 07bab45..6f0be78 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,7 +19,7 @@ jobs: image: - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.3.0-coq-8.20' - - 'mathcomp/mathcomp:latest-coq-dev' + - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: - uses: actions/checkout@v4 diff --git a/README.md b/README.md index 54c4882..e2beef1 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ This library relies on propositional and functional extentionality axioms. - License: [Apache-2.0](LICENSE) - Compatible Coq versions: Coq 8.19 to 8.20 - Additional dependencies: - - [MathComp ssreflect 2.2](https://math-comp.github.io) + - [MathComp ssreflect 2.2 or later](https://math-comp.github.io) - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) - [MathComp algebra](https://math-comp.github.io) - Coq namespace: `pcm` diff --git a/_CoqProject b/_CoqProject index 5cf4cc3..6ccbe52 100644 --- a/_CoqProject +++ b/_CoqProject @@ -12,6 +12,7 @@ core/axioms.v core/prelude.v core/pred.v core/auto.v +core/autouniq.v core/seqext.v core/slice.v core/uslice.v diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam index 104d746..2c56077 100644 --- a/coq-fcsl-pcm.opam +++ b/coq-fcsl-pcm.opam @@ -27,7 +27,7 @@ install: [make "install"] depends: [ "coq" { (>= "8.19" & < "8.21~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } - "coq-hierarchy-builder" {>= "1.7.0"} + "coq-hierarchy-builder" { (>= "1.7.0" & < "1.9~") | (= "dev") } "coq-mathcomp-algebra" ] diff --git a/core/autouniq.v b/core/autouniq.v new file mode 100644 index 0000000..a66fa40 --- /dev/null +++ b/core/autouniq.v @@ -0,0 +1,618 @@ +(* +Copyright 2024 IMDEA Software Institute +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + http://www.apache.org/licenses/LICENSE-2.0 +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*) + +From HB Require Import structures. +From Coq Require Import ssreflect ssrbool ssrfun. +From mathcomp Require Import ssrnat seq eqtype. +From pcm Require Import options prelude auto. + +(**********************************************************) +(**********************************************************) +(* Canonical structure lemmas for automating three tasks *) +(* given hypothesis uniq s, of uniqueness of elements of *) +(* sequence s. *) +(* *) +(* 1. Automate inferring uniq s', when s' contains subset *) +(* of elements of s *) +(* *) +(* 2. Automate inferring facts of the form x != y *) +(* when x and y are both in s *) +(* *) +(* 3. Automate inferring facts of the form x \notin s' *) +(* when x::s' contains subset of elements of s *) +(**********************************************************) +(**********************************************************) + + +Section UniqReflectionContexts. +Variable A : eqType. + +Structure ctx := Context {keyx : seq A; varx : seq (seq A)}. +Definition empx := Context [::] [::]. + +(* sub-context *) +Definition sub_ctx (i j : ctx) := + Prefix (keyx i) (keyx j) /\ Prefix (varx i) (varx j). + +Lemma sc_refl i : sub_ctx i i. +Proof. by []. Qed. + +Lemma sc_trans i j k : + sub_ctx i j -> + sub_ctx j k -> + sub_ctx i k. +Proof. +by case=>K1 V1 [K2 V2]; split; [move: K2|move: V2]; apply: Prefix_trans. +Qed. + +End UniqReflectionContexts. + +Section UniqReflection. +Variable A : eqType. +Implicit Type i : ctx A. +Inductive term := Pts of nat | Var of nat. + +Definition eq_term t1 t2 : bool := + match t1, t2 with + | Pts n1, Pts n2 => n1 == n2 + | Var x1, Var x2 => x1 == x2 + | _, _ => false + end. +Lemma eq_termP : Equality.axiom eq_term. +Proof. +case=>n; case=>m /=; try by [constructor]; +by case: eqP=>[->|N]; constructor=>//; case=>/N. +Qed. + +HB.instance Definition _ := hasDecEq.Build term eq_termP. + +(* interpretation for terms *) +Definition interp' i (t : term) : seq A := + match t with + Pts n => if onth (keyx i) n is Some k then [:: k] else [::] + | Var n => if onth (varx i) n is Some f then f else [::] + end. + +(* interpretation for term sequences *) +Definition interp (i : ctx A) (ts : seq term) : seq A := + foldr (fun t s => interp' i t ++ s) [::] ts. + +Lemma interp_cat k ts1 ts2 : + interp k (ts1 ++ ts2) = interp k ts1 ++ interp k ts2. +Proof. by elim: ts1=>[|t ts1 IH] //=; rewrite -catA IH. Qed. + +(* interpretation is invariant under context weakening *) +(* under assumption that the interpreted term is well-formed *) +Definition wf i t := + match t with + | Pts n => n < size (keyx i) + | Var n => n < size (varx i) + end. + +Lemma sc_wf i j ts : + sub_ctx i j -> + all (wf i) ts -> all (wf j) ts. +Proof. +case=>/Prefix_size H1 /Prefix_size H2; elim: ts=>[|t ts IH] //=. +case/andP=>H /IH ->; rewrite andbT. +by case: t H=>n H; apply: leq_trans H _. +Qed. + +Lemma sc_interp i j ts : + sub_ctx i j -> + all (wf i) ts -> + interp i ts = interp j ts. +Proof. +case=>H1 H2; elim: ts=>[|t ts IH] //= /andP [H] /IH ->. +by case: t H=>n /= /Prefix_onth <-. +Qed. + +Definition key n t := if t is Pts m then n == m else false. +Definition var n t := if t is Var m then n == m else false. +Definition kfree n t := rfilter (key n) t. +Definition vfree n t := rfilter (var n) t. + +Lemma kfree_sub ts n : {subset kfree n ts <= ts}. +Proof. +elim: ts=>[|x ts IH] // z; rewrite /kfree/= inE. +case: ifP=>[_ ->|_]; first by rewrite orbT. +by rewrite inE; case: (z =P x)=>//= _ /IH. +Qed. + +Lemma vfree_sub ts n : {subset vfree n ts <= ts}. +Proof. +elim: ts=>[|x ts IH] // z; rewrite /vfree/= inE. +case: ifP=>[_ ->|_]; first by rewrite orbT. +by rewrite inE; case: (z =P x)=>//= _ /IH. +Qed. + +Lemma wf_kfree i n ts : + all (wf i) ts -> + all (wf i) (kfree n ts). +Proof. +rewrite /kfree; elim: ts=>//= -[]t ts IH /=; last first. +- by case/andP=>-> /IH. +by case: (n =P t)=>[_ /andP []|/= _ /andP [->] /IH]. +Qed. + +Lemma wf_vfree i n ts : + all (wf i) ts -> + all (wf i) (vfree n ts). +Proof. +rewrite /vfree; elim: ts=>//= -[]t ts IH /=. +- by case/andP=>-> /IH. +by case: (n =P t)=>[_ /andP []|/= _ /andP [->] /IH]. +Qed. + +Lemma keyN i n ts : + ~~ has (key n) ts -> + perm_eq (interp i (kfree n ts)) (interp i ts). +Proof. +elim: ts=>[|t ts IH] //=; rewrite negb_or; case/andP=>H1. +move/IH=>E; rewrite /kfree /= (negbTE H1) /=. +by rewrite perm_cat2l E. +Qed. + +Lemma varN i n ts : + ~~ has (var n) ts -> + perm_eq (interp i (vfree n ts)) (interp i ts). +Proof. +elim: ts=>[|t ts IH] //=; rewrite negb_or; case/andP=>H1. +move/IH=>E; rewrite /vfree /= (negbTE H1) /=. +by rewrite perm_cat2l E. +Qed. + +Lemma keyP i n k ts : + has (key n) ts -> + onth (keyx i) n = Some k -> + perm_eq (interp i ts) (k :: interp i (kfree n ts)). +Proof. +rewrite /kfree; elim: ts=>[|[]t ts IH] //=. +- case: (n =P t)=>[-> _ ->//|/= _ H /(IH H) {}IH]. + case: (onth _ t)=>[a|] //; rewrite -(cat1s k). + apply: perm_trans (perm_cat _ IH) _=>//. + by rewrite -(cat1s k) !catA perm_cat // perm_catC. +move=>H /(IH H) {}IH. +case: (onth _ t)=>[a|] //=; rewrite -(cat1s k). +apply: perm_trans (perm_cat _ IH) _=>//. +by rewrite -(cat1s k) !catA perm_cat // perm_catC. +Qed. + +Lemma varP i n u ts : + has (var n) ts -> + onth (varx i) n = Some u -> + perm_eq (interp i ts) (u ++ interp i (vfree n ts)). +Proof. +rewrite /vfree; elim: ts=>[|[]t ts IH] //=. +- move=>H /(IH H) {}IH. + case: (onth _ t)=>[a|] //=; rewrite -(cat1s a). + apply: perm_trans (perm_cat _ IH) _=>//. + by rewrite -(cat1s a (interp _ _)) !catA perm_cat // perm_catC. +case: (n =P t)=>[-> _ ->//|/= _ H /(IH H) {}IH]. +case: (onth _ t)=>[a|] //=. +apply: perm_trans (perm_cat _ IH) _=>//. +by rewrite !catA perm_cat // perm_catC. +Qed. + +End UniqReflection. + +(* deciding if ts1 represents a subterm of ts2 *) + +Section Subterm. +Variable A : eqType. +Implicit Types (i : ctx A) (ts : seq term). + +Fixpoint subterm ts1 ts2 := + match ts1 with + | Pts n :: tsx1 => + if has (key n) ts2 then subterm tsx1 (kfree n ts2) else false + | Var n :: tsx1 => + if has (var n) ts2 then subterm tsx1 (vfree n ts2) else false + | [::] => true + end. + +(* the procedure is sound for deciding *) +(* subset and uniqueness properties *) + +Lemma subterm_sound_sub i ts1 ts2 : + all (wf i) ts1 -> + all (wf i) ts2 -> + subterm ts1 ts2 -> + {subset interp i ts1 <= interp i ts2}. +Proof. +elim: ts1 ts2=>[|t ts1 IH] ts2 //= A1 A2. +case/andP: A1; case: t=>t /= /size_onth [k] X A1; rewrite X; +case: ifP=>Y // /(IH _ A1) S z. +- rewrite inE; case/orP=>[/eqP ->|]. + - by rewrite (perm_mem (keyP Y X)) inE eqxx. + move/(S (wf_kfree _ A2)). + by rewrite (perm_mem (keyP Y X)) inE orbC=>->. +rewrite mem_cat (perm_mem (varP Y X)) mem_cat. +case/orP=>[->//|] /(S (wf_vfree _ A2)) ->. +by rewrite orbC. +Qed. + +Lemma subterm_sound_uniq i ts1 ts2 : + all (wf i) ts1 -> + all (wf i) ts2 -> + subterm ts1 ts2 -> + uniq (interp i ts2) -> + uniq (interp i ts1). +Proof. +elim: ts1 ts2=>[|[]t ts1 IH] ts2 //= /andP [] /size_onth [k] /[dup] X -> +A1 A2; case: ifP=>// Y S. +- move: (IH _ A1 (wf_kfree _ A2) S)=>{}IH. + rewrite (perm_uniq (keyP Y X)) /=. + case/andP=>K /IH ->; rewrite andbT (contra _ K) //. + by apply: (subterm_sound_sub A1 (wf_kfree _ A2) S). +move: (IH _ A1 (wf_vfree _ A2) S)=>{}IH. +rewrite (perm_uniq (varP Y X)) /= !cat_uniq. +case/and3P=>-> /= H /IH ->; rewrite andbT (contra _ H) //. +case/hasP=>x /(subterm_sound_sub A1 (wf_vfree _ A2) S) V K. +by apply/hasP; exists x. +Qed. + +End Subterm. + +Module Syntactify. +Section Syntactify. +Variables (A : eqType). +Implicit Types (i : ctx A) (ts : seq term). + +(* a tagging structure to control the flow of computation *) +Structure tagged_map := Tag {untag : seq A}. + +Local Coercion untag : tagged_map >-> seq. + +(* in reversed order; first test for unions, then cons, rcons, empty, and vars *) +Definition var_tag := Tag. +Definition empty_tag := var_tag. +Definition rcons_tag := empty_tag. +Definition cons_tag := rcons_tag. +Canonical Structure union_tag hc := cons_tag hc. + +(* Main structure *) +(* - i : input context *) +(* - j : output context *) +(* - ts : syntactification of sequence using context j *) + +Definition axiom i j ts (pivot : tagged_map) := + [/\ interp j ts = untag pivot, sub_ctx i j & all (wf j) ts]. +Structure form i j ts := Form {pivot : tagged_map; _ : axiom i j ts pivot}. + +Local Coercion pivot : form >-> tagged_map. + +Lemma union_pf i j k ts1 ts2 (f1 : form i j ts1) (f2 : form j k ts2) : + axiom i k (ts1 ++ ts2) (union_tag (untag f1 ++ untag f2)). +Proof. +case: f1 f2=>f1 [E1 S1 W1][f2][E2 S2 W2]; split=>/=. +- by rewrite interp_cat -(sc_interp S2 W1) E1 E2. +- by apply: sc_trans S1 S2. +by rewrite all_cat (sc_wf S2 W1) W2. +Qed. + +Canonical union_form i j k ts1 ts2 f1 f2 := + Form (@union_pf i j k ts1 ts2 f1 f2). + +(* check for cons *) +Lemma cons_pf i keys2 k j ts (f1 : xfind (keyx i) keys2 k) + (f2 : form (Context keys2 (varx i)) j ts) : + axiom i j (Pts k :: ts) (cons_tag (xuntag f1 :: untag f2)). +Proof. +case: f1 f2=>f1 [E1 H1][f2][E2 H2 W2]; split=>/=. +- by rewrite -(Prefix_onth (onth_size E1) (proj1 H2)) E1 /= E2. +- by apply: sc_trans H2. +by rewrite W2 andbT (leq_trans (onth_size E1)) // (Prefix_size (proj1 H2)). +Qed. + +Canonical cons_form i keys2 k j ts f1 f2 := + Form (@cons_pf i keys2 k j ts f1 f2). + +(* check for rcons *) +Lemma rcons_pf i j ts keys2 k (f1 : form i j ts) + (f2 : xfind (keyx j) keys2 k) : + axiom i (Context keys2 (varx j)) + (rcons ts (Pts k)) (rcons_tag (rcons (untag f1) (xuntag f2))). +Proof. +case: f1 f2=>f1 [E1 H1 W1][f2][E2 H2]. +have H3 : sub_ctx j (Context keys2 (varx j)) by []. +split=>/=. +- by rewrite -cats1 interp_cat /= E2 -(sc_interp H3) // cats1 E1. +- by apply: (sc_trans H1 H3). +by rewrite all_rcons /= (onth_size E2) (sc_wf H3 W1). +Qed. + +Canonical rcons_form i j ts keys2 k f1 f2 := + Form (@rcons_pf i j ts keys2 k f1 f2). + +(* check if reached empty *) + +Lemma empty_pf i : axiom i i [::] (empty_tag [::]). +Proof. by split. Qed. + +Canonical empty_form i := Form (@empty_pf i). + +(* check for var (default case) *) +Lemma var_pf i vars2 n (f : xfind (varx i) vars2 n) : + axiom i (Context (keyx i) vars2) + [:: Var n] (var_tag (xuntag f)). +Proof. +case: f=>f [E H]; split=>//=; first by rewrite E cats0. +by rewrite (onth_size E). +Qed. + +Canonical var_form i vars2 n f := Form (@var_pf i vars2 n f). + +End Syntactify. + +Module Exports. +Coercion untag : tagged_map >-> seq. +Coercion pivot : form >-> tagged_map. +Canonical union_tag. +Canonical union_form. +Canonical cons_form. +Canonical rcons_form. +Canonical empty_form. +Canonical var_form. + +End Exports. +End Syntactify. + +Export Syntactify.Exports. + +(*********************************************************************) +(* Overloaded lemma for concluding uniq facts out of uniq hypothesis *) +(*********************************************************************) + +Module UniqX. +Section UniqX. +Variable A : eqType. +Implicit Types (j : ctx A) (ts : seq term). +Notation form := Syntactify.form. +Notation untag := Syntactify.untag. + +Structure packed_map (m : seq A) := Pack {unpack : seq A}. +Canonical equate (m : seq A) := Pack m m. + +Definition raxiom j ts1 m (b : bool) (pivot : packed_map m) := + all (wf j) ts1 -> uniq (interp j ts1) -> b -> uniq (unpack pivot). + +Structure rform j ts1 m b := + RForm {pivot :> packed_map m; _ : raxiom j ts1 b pivot}. + +(* start instance: note how subterm ts2 ts1 is unified with *) +(* the boolean component of rform *) + +Lemma start_pf j k ts1 ts2 (f2 : form j k ts2) : + @raxiom j ts1 (untag f2) (subterm ts2 ts1) (equate f2). +Proof. +case: f2=>f2 [E S A2] A1; rewrite (sc_interp S A1)=>V. +move/(subterm_sound_uniq A2 (sc_wf S A1))=>H /=. +by rewrite -E (H V). +Qed. + +Canonical start j k ts1 ts2 f2 := RForm (@start_pf j k ts1 ts2 f2). + +End UniqX. + +Module Exports. +Canonical equate. +Canonical start. + +Section Exports. +Variable A : eqType. +Implicit Types (j : ctx A) (ts : seq term). +Notation form := Syntactify.form. +Notation untag := Syntactify.untag. + +(* main lemma *) +(* boolean component of rform is set to true *) +(* so that the lemma succeeds only if the subterm checks suceeds *) +Lemma uniqO m j ts1 (f1 : form (empx A) j ts1) (g : rform j ts1 m true) : + uniq (untag f1) -> uniq (unpack (pivot g)). +Proof. +case: g f1; case=>pivot H [f1][<- Sc X] /=. +by move/H; apply. +Qed. + +End Exports. + +Arguments uniqO {A m j ts1 f1 g}. + +End Exports. +End UniqX. + +Export UniqX.Exports. + +(***********************************************************************) +(* Overloaded lemma for concluding _ != _ facts out of uniq hypothesis *) +(***********************************************************************) + +Module NeqX. +Section NeqX. +Variable A : eqType. +Implicit Types (j : ctx A) (ts : seq term). +Notation form := Syntactify.form. +Notation untag := Syntactify.untag. + +Structure packed_elem (x : A) := Pack {unpack : A}. +Canonical equate m := Pack m m. + +Definition raxiom j ts1 (n : nat) m b (pivot : packed_elem m) := + all (wf j) ts1 -> uniq (interp j ts1) -> b -> + interp j [:: Pts n] != [:: unpack pivot]. + +Structure rform j ts1 (n : nat) m b := + RForm {pivot :> packed_elem m; _ : raxiom j ts1 n b pivot}. + +Lemma start_pf j keys2 ts1 n m (f2 : xfind (keyx j) keys2 m) : + @raxiom j ts1 n (xuntag f2) + (subterm [:: Pts n; Pts m] ts1) + (equate (xuntag f2)). +Proof. +case: f2; case=>f2 [O P] Aw U S. +have [Pn Pm] : Pts n \in ts1 /\ Pts m \in ts1. +- move: S=>/=; case: ifP=>//; case: ifP=>//. + case/hasP=>/= -[] xm /kfree_sub Pm //= /eqP ->. + by case/hasP=>/= -[] xn //= Pn /eqP ->. +have Sn : wf j (Pts n) by move/allP: Pn; apply. +have Sm : wf j (Pts m) by move/allP: Pm; apply. +have Ax: all (wf j) [:: Pts n; Pts m] by apply/and3P. +move: (subterm_sound_uniq Ax Aw S U)=>/=. +rewrite (Prefix_onth Sm P) O /= cat_uniq cats0. +case: (onth _ _)=>//= a; rewrite orbF andbT inE. +by apply: contra=>/eqP [->]. +Qed. + +Canonical start j keys2 ts1 n m f2 := RForm (@start_pf j keys2 ts1 n m f2). + +End NeqX. + +Module Exports. +Canonical equate. +Canonical start. + +Section Exports. +Variable A : eqType. +Implicit Types (j : ctx A) (ts : seq term). +Notation form := Syntactify.form. +Notation untag := Syntactify.untag. + +(* main lemma *) +Lemma neqO n m i keys2 ts1 (f : form (empx A) i ts1) + (x : xfind (keyx i) keys2 n) + (y : rform (Context keys2 (varx i)) ts1 n m true) : + uniq (untag f) -> xuntag x != unpack (pivot y). +Proof. +case: f=>f [Ef S Aw]; case: x=>x [O P]; case: y=>y H. +rewrite /raxiom/= -Ef O cats0 in H *. +have {}S : sub_ctx i (Context keys2 (varx i)) by []. +rewrite -(sc_interp S) // (sc_wf S) // in H. +by move/(H erefl)=>/(_ erefl); apply: contra=>/eqP ->. +Qed. + +Lemma test (x y z : A) : + uniq [:: x; y; z] -> + (z != y)*(z != x) * (x != y). +Proof. by move=>U; rewrite !(neqO _ _ U). Abort. + +End Exports. + +Arguments neqO {A n m i keys2 ts1 f x y}. + +End Exports. +End NeqX. + +Export NeqX.Exports. + +(***************************************************************************) +(* Overloaded lemma for concluding _ \notin _ facts out of uniq hypothesis *) +(***************************************************************************) + +Module NotinX. +Section NotinX. +Variable A : eqType. +Implicit Types (j : ctx A) (ts : seq term). +Notation form := Syntactify.form. +Notation untag := Syntactify.untag. + +Structure packed_map (x : seq A) := Pack {unpack : seq A}. +Canonical equate m := Pack m m. + +Definition raxiom j ts1 (n : nat) m b (pivot : packed_map m) := + all (wf j) ts1 -> uniq (interp j ts1) -> b -> + uniq (interp j [:: Pts n] ++ unpack pivot). + +Structure rform j ts1 (n : nat) m b := + RForm {pivot :> packed_map m; _ : raxiom j ts1 n b pivot}. + +Lemma start_pf j k ts1 ts2 n (f2 : form j k ts2) : + @raxiom j ts1 n (untag f2) + (subterm [:: Pts n & ts2] ts1) + (equate f2). +Proof. +case: f2=>f2 [E S A2] A1 U X /=. +have Pn : Pts n \in ts1. +- by move: X=>/=; case: ifP=>// /hasP [][] // xn /[swap] /eqP=>->. +have Sn : wf j (Pts n) by move/allP: Pn; apply. +rewrite (sc_interp S A1) in U; move/(sc_wf S): A1=>A1. +have Ax : all (wf k) (Pts n :: ts2). +- by apply/andP; split=>//; move/allP: Pn; apply. +move: (subterm_sound_uniq Ax A1 X U). +by rewrite (Prefix_onth Sn (proj1 S)) cats0 -E. +Qed. + +Canonical start j k ts1 ts2 n f2 := RForm (@start_pf j k ts1 ts2 n f2). + +End NotinX. + +Module Exports. +Canonical equate. +Canonical start. + +Section Exports. +Variable A : eqType. +Implicit Types (j : ctx A) (ts : seq term). +Notation form := Syntactify.form. +Notation untag := Syntactify.untag. + +(* main lemma *) +Lemma notinO n m i keys2 ts1 (f : form (empx A) i ts1) + (x : xfind (keyx i) keys2 n) + (y : rform (Context keys2 (varx i)) ts1 n m true) : + uniq (untag f) -> xuntag x \notin unpack (pivot y). +Proof. +case: f=>f [Ef S Aw]; case: x=>x [O P]; case: y=>y H. +rewrite /raxiom/= -Ef O cats0 in H *. +have {}S : sub_ctx i (Context keys2 (varx i)) by []. +rewrite -(sc_interp S) // (sc_wf S) // in H. +by move/(H erefl)=>/(_ erefl) /andP []. +Qed. + +Lemma test (x y z : A) : + uniq [:: x; y; z] -> + (x \notin [:: z; y]) * (y \notin [:: x; z]). +Proof. by move=>U; rewrite !(notinO _ _ U). Abort. + +End Exports. + +Arguments notinO {A n m i keys2 ts1 f x y}. + +End Exports. +End NotinX. + +Export NotinX.Exports. + +(* packaging the three automated lemmas into one *) +(* stating them in the form X = false instead of ~~ X *) +(* so that rewrites apply to positive terms as well *) +Lemma uniqX' (A : eqType) i ts1 (f1 : Syntactify.form (empx A) i ts1) : + uniq f1 -> + (forall m (g : UniqX.rform i ts1 m true), + uniq (UniqX.unpack (UniqX.pivot g))) * + (forall n keys2 (x : xfind (keyx i) keys2 n), + ((forall m (y : NeqX.rform (Context keys2 (varx i)) ts1 n m true), + xuntag x == NeqX.unpack (NeqX.pivot y) = false) * + (forall m (y : NotinX.rform (Context keys2 (varx i)) ts1 n m true), + xuntag x \in NotinX.unpack (NotinX.pivot y) = false))). +Proof. +by move=>U; split; [|split]=>*; first by [apply: uniqO U]; +apply/negbTE; [apply: neqO U|apply: notinO U]. +Qed. + +(* adding common goal transformations *) +(* that appear when reasoning about uniq *) +Definition uniqX {A i ts1 f1} U := + (mem_rcons, mem_cat, inE, negb_or, rcons_uniq, cat_uniq, andbT, orbF, + @uniqX' A i ts1 f1 U). + diff --git a/core/finmap.v b/core/finmap.v index 97df883..8b04992 100644 --- a/core/finmap.v +++ b/core/finmap.v @@ -981,7 +981,7 @@ Definition mapf' (m : seq (K * U)) : seq (K * V) := Lemma map_key_mapf (m : seq (K * U)) : map key (mapf' m) = map key m. Proof. by elim: m=>[|[k v] m IH] //=; rewrite IH. Qed. -Lemma sorted_map (m : seq (K * U)) : +Lemma sorted_map_key (m : seq (K * U)) : sorted ord (map key m) -> sorted ord (map key (mapf' m)). Proof. elim: m=>[|[k v] m IH] //= H. @@ -991,7 +991,7 @@ by apply/(order_path_min _ H);apply/trans. Qed. Definition mapf (m : finMap K U) : finMap K V := - let: FinMap _ pf := m in FinMap (sorted_map pf). + let: FinMap _ pf := m in FinMap (sorted_map_key pf). Lemma supp_mapf (s : finMap K U) : supp (mapf s) = supp s. @@ -1134,7 +1134,7 @@ Fixpoint zip' (s1 s2 : seq (K * V)) := | _, _ => None end. -Definition zip_unit' (s : seq (K * V)) := @mapf' K _ _ unit_f s. +Definition zip_unit' (s : seq (K * V)) := @mapf' K V V unit_f s. Lemma zipC' s1 s2 : zip' s1 s2 = zip' s2 s1. Proof. diff --git a/core/ordtype.v b/core/ordtype.v index e685128..affe1c6 100644 --- a/core/ordtype.v +++ b/core/ordtype.v @@ -43,8 +43,8 @@ HB.mixin Record isOrdered T of Equality T := { (* In this file in particular, the canonicals for each instance *) (* must be declared by hand as HB.instance does that *) (* only if Ordered is declared by HB.structure *) - -(* #[log(raw)] +(* +#[log(raw)] #[short(type="ordType")] HB.structure Definition Ordered := {T of Equality T & isOrdered T}. @@ -199,6 +199,7 @@ Global Arguments ordtype_subproof {_}. Notation Ordered X1 := (Ordered.axioms_ X1). (* end of generated and changed code *) + (* Repacking *) Lemma irr {T : ordType} : irreflexive (@ord T). @@ -470,8 +471,7 @@ case: (x =P y)=>[-> H|/eqP/connex //]. by apply: IH; apply: contra H=>/eqP ->. Qed. -HB.instance Definition seq_ord_mix := - isOrdered.Build (seq T) seq_is_ordtype. +HB.instance Definition seq_ord_mix := isOrdered.Build (seq T) seq_is_ordtype. (* manual canonical declaration, as HB fails to declare it *) Canonical seq_ordType : ordType := Ordered.Pack (sort:=seq T) (Ordered.Class seq_ord_mix). diff --git a/core/pred.v b/core/pred.v index b98befc..f94c2f6 100644 --- a/core/pred.v +++ b/core/pred.v @@ -16,7 +16,7 @@ limitations under the License. (******************************************************************************) From Coq Require Import ssreflect ssrbool ssrfun Setoid Basics. -From mathcomp Require Import ssrnat seq eqtype. +From mathcomp Require Import ssrnat seq eqtype bigop. From pcm Require Import options. (* First some basic propositional equalities *) @@ -807,6 +807,14 @@ End ListMembership. Prenex Implicits In_split. +(* for equality types, membership predicates coincide *) +Lemma mem_seqP (A : eqType) x (s : seq A) : reflect (x \In s) (x \in s). +Proof. +elim: s=>[|y s IH]; first by constructor. +rewrite inE; case: eqP=>[<-|H /=]; first by constructor; left. +by apply: equivP IH _; rewrite InE; split; [right | case]. +Qed. + Lemma Mem_map T T' (f : T -> T') x (s : seq T) : x \In s -> f x \In (map f s). Proof. @@ -835,6 +843,10 @@ case=>k /In_cons [->|H E]; first by left. by right; apply/IHs; exists k. Qed. +Lemma mapPP T1 (T2 : eqType) (f : T1 -> T2) (s : seq T1) y : + reflect (exists2 x, x \In s & y = f x) (y \in map f s). +Proof. by apply: (iffP idP)=>[/mem_seqP/MapP|/MapP/mem_seqP]. Qed. + Lemma Mem_filter (T : Type) (a : pred T) (x : T) (s : seq T) : x \In filter a s <-> a x /\ x \In s. Proof. @@ -860,12 +872,13 @@ rewrite IHs // => y s_y; apply: eq_a. by rewrite InE; right. Qed. -(* for equality types, membership predicates coincide *) -Lemma mem_seqP (A : eqType) x (s : seq A) : reflect (x \In s) (x \in s). +Lemma eq_In_map S T (f g : S -> T) (s : seq S) : + (forall x, x \In s -> f x = g x) <-> + map f s = map g s. Proof. -elim: s=>[|y s IH]; first by constructor. -rewrite inE; case: eqP=>[<-|H /=]; first by constructor; left. -by apply: equivP IH _; rewrite InE; split; [right | case]. +elim: s=>[|x s IH] //=; split=>[H|[H1 /IH H2 k]]. +- by congr (_ :: _); [apply: H; left|apply/IH=>k K; apply: H; right]. +by rewrite InE; case=>[->|/H2]. Qed. @@ -989,6 +1002,60 @@ case: andP=>H; constructor. by case=>/mem_seqP H1 /IH H2; elim: H. Qed. +Lemma map_Uniq T1 (T2 : eqType) (f : T1 -> T2) (s : seq T1) : + uniq [seq f i | i <- s] -> Uniq s. +Proof. +elim: s=>//= x s IH /andP [nsfx /IH H]; split=>//. +apply: contraNnot nsfx=>Hx. +by apply/mapPP; exists x. +Qed. + +(* \In and big operators *) + +Lemma Big_rec R (K : R -> Type) (idx : R) (op : R -> R -> R) : + K idx -> + forall I (r : seq I) (P : pred I) (F : I -> R), + (forall (i : I) (x : R), i \In r -> P i -> K x -> K (op (F i) x)) -> + K (\big[op/idx]_(i <- r | P i) F i). +Proof. +rewrite unlock; move=>Kid I r P F; elim: r=>[|x r IH] Kop //=. +case: ifP=>H; last by apply: IH=>i x0 X; apply: Kop; right. +apply: (Kop)=>//; first by left. +by apply: IH=>i x0 X; apply: Kop; right. +Qed. + +Lemma Big_rec2 R1 R2 (K : R1 -> R2 -> Type) (id1 : R1) + (op1 : R1 -> R1 -> R1) (id2 : R2) (op2 : R2 -> R2 -> R2) : + K id1 id2 -> + forall I (r : seq I) (P : pred I) (F1 : I -> R1) (F2 : I -> R2), + (forall (i : I) (y1 : R1) (y2 : R2), + i \In r -> P i -> K y1 y2 -> + K (op1 (F1 i) y1) (op2 (F2 i) y2)) -> + K (\big[op1/id1]_(i <- r | P i) F1 i) + (\big[op2/id2]_(i <- r | P i) F2 i). +Proof. +move=>Kid I r P F1 F2; rewrite unlock. +elim: r=>[|x r IH] //=. +case: ifP=>H K_F; last by apply: IH=>i y1 y2 X; apply: K_F; right. +apply: (K_F)=>//; first by left. +by apply: IH=>i y1 y2 X; apply: K_F; right. +Qed. + +Lemma eq_Bigr R (idx : R) (op : R -> R -> R) I (r : seq I) + (P : pred I) F1 F2 : + (forall i, i \In r -> P i -> F1 i = F2 i) -> + \big[op/idx]_(i <- r | P i) F1 i = \big[op/idx]_(i <- r | P i) F2 i. +Proof. +by move=>eqF12; elim/Big_rec2: _=>// i x y2 X /(eqF12 _ X) ->->. +Qed. + +Lemma eq_bigR R (idx : R) (op : R -> R -> R) (I : eqType) (r : seq I) + (P : pred I) F1 F2 : + (forall i, i \in r -> P i -> F1 i = F2 i) -> + \big[op/idx]_(i <- r | P i) F1 i = \big[op/idx]_(i <- r | P i) F2 i. +Proof. by move=>eqF12; apply: eq_Bigr=>i /mem_seqP/eqF12. Qed. + + (***********************************) (* Image of a collective predicate *) (***********************************) diff --git a/core/prelude.v b/core/prelude.v index 16ba856..d9c2f1b 100644 --- a/core/prelude.v +++ b/core/prelude.v @@ -541,6 +541,12 @@ Proof. by case: a=>//=->. Qed. Lemma iffE (b1 b2 : bool) : b1 = b2 <-> (b1 <-> b2). Proof. by split=>[->|] //; move/iffPb/eqP. Qed. +Lemma orPl (a b : bool) : reflect (a \/ ~~ a /\ b) (a || b). +Proof. by case: a; case: b=>/=; constructor; auto; case=>//; case. Qed. + +Lemma orPr (a b : bool) : reflect (~~ b /\ a \/ b) (a || b). +Proof. by case: a; case: b=>/=; constructor; auto; case=>//; case. Qed. + (* subsets *) Lemma subsetC T (p q : mem_pred T) : diff --git a/core/seqext.v b/core/seqext.v index 7033112..f2c4baa 100644 --- a/core/seqext.v +++ b/core/seqext.v @@ -98,6 +98,9 @@ Section LemmasEq. Variables A : eqType. Implicit Type xs : seq A. +Lemma eqnil xs : xs =i [::] -> xs = [::]. +Proof. by case: xs=>// x xs /(_ x); rewrite inE eqxx. Qed. + (* With A : Type, we have the In_split lemma. *) (* With A : eqType, the lemma can be strenghtened to *) (* not only return the split of xs, but the split of xs *) @@ -256,6 +259,16 @@ case: has_nilP=>X; constructor. by case=>k K; elim: X; apply/hasP; exists k. Qed. +Lemma all_filterPC T (a : pred T) (s : seq T) : + reflect (filter a s = [::]) (all (predC a) s). +Proof. +case: all_filterP=>H; constructor. +- rewrite -H -filter_predI -(filter_pred0 s). + by apply: eq_filter=>z; rewrite inE andbN. +move=>E; apply: H; elim: s E=>[|x s IH] //=. +by case: ifP=>//= E /IH ->. +Qed. + Lemma filter_nilP (p : pred A) xs : reflect (forall x, p x -> x \in xs -> false) ([seq x <- xs | p x] == [::]). @@ -381,6 +394,71 @@ Qed. End LemmasEq. +(* lemmas about prev and next should generally by proved using *) +(* prev_nth and next_nth, but sometimes we can also prove them *) +(* directly by setting up the right induction *) + +Lemma prevE (T : eqType) (s : seq T) (p x : T) : + prev_at p x x s = prev (x :: s) p. +Proof. by []. Qed. + +Lemma nextE (T : eqType) (s : seq T) (p x : T) : + next_at p x x s = next (x :: s) p. +Proof. by []. Qed. + +(* prev starts counting occurrences of p from the second position; *) +(* the first position is counted as last; that's the meaning *) +(* of considering the sequence argument as a cycle *) +Lemma prev_cons (T : eqType) (s : seq T) x y p : + prev (x :: y :: s) p = + if p == y then x else + if p \in s then prev (y :: s) p else + if p == x then last y s else p. +Proof. +rewrite !prev_nth !inE orbC /= (eq_sym y); case: (p =P y)=>//= /eqP Npy. +have [S|/index_sizeE ->/=] := boolP (p \in s). +- by apply: set_nth_default; rewrite ltnW // ltnS index_mem. +by case: (p =P x)=>// <-{x}; rewrite -last_nth. +Qed. + +Lemma next_rcons (T : eqType) (s : seq T) a b c : + next (rcons (rcons s a) b) c = + if c \in s then next (rcons s a) c else + if c == a then b else + if c == b then head a s else c. +Proof. +case: s=>[|y s] //=; rewrite inE. +by elim: s y {2 3 5}y=>[|x s IH] y y' /=; case: (c =P y'). +Qed. + +Lemma prevat_rcons (T : eqType) (s : seq T) a b c : + (* prev (a :: rcons s b) c *) + prev_at c a a (rcons s b) = + if c \in s then prev (a :: s) c + else if c == b then last a s + else if c == a then b else c. +Proof. +rewrite /prev /=; elim: s a {2 4 5}a=>[|x s IH] a a'//=. +by rewrite inE; case: (c =P x). +Qed. + +Lemma nextat_rcons (T : eqType) (s : seq T) a b c : + (* next (rcons (a :: s) b) c = *) + next_at c a a (rcons s b) = + if c == a then head b s + else if c \in s then next (rcons s b) c + else if c == b then a else c. +Proof. +rewrite nextE !next_nth inE /= eq_sym. +case: (a =P c)=>[->|/eqP N] /=; first by rewrite nth0 head_rcons. +rewrite mem_rcons inE orbC index_rcons. +case C: (c \in s)=>//=; last first. +- by case: (c =P b)=>// <-; rewrite nth_default // size_rcons. +case: s C=>//= x s; rewrite inE eq_sym. +case: (x =P c)=>[-> _|/eqP Nc /= C]; first by rewrite !nth0 !head_rcons. +by apply: set_nth_default; rewrite size_rcons ltnS index_mem C. +Qed. + (* decidable sequence disjointness *) Definition disjoint {A : eqType} (s1 s2 : seq A) := @@ -944,6 +1022,11 @@ Qed. Arguments last_in x [k s]. +Lemma last_mem x (s : seq A) a : + a = last x s -> + (a == x) || (a \in s). +Proof. by move=>->; apply: mem_last. Qed. + Lemma last_notin x k (s : seq A) : x \in s -> k \notin s -> @@ -2135,4 +2218,3 @@ Lemma uniq_big_cat_disj (A : finType) (B : eqType) (f : A -> seq B) t1 t2 x : t1 = t2. Proof. by case/uniq_big_cat=>_; apply. Qed. - diff --git a/meta.yml b/meta.yml index ce4edd6..e0ab662 100644 --- a/meta.yml +++ b/meta.yml @@ -48,18 +48,18 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.3.0-coq-8.20' repo: 'mathcomp/mathcomp' -- version: 'latest-coq-dev' - repo: 'mathcomp/mathcomp' +- version: 'coq-dev' + repo: 'mathcomp/mathcomp-dev' dependencies: - opam: name: coq-mathcomp-ssreflect version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }' description: |- - [MathComp ssreflect 2.2](https://math-comp.github.io) + [MathComp ssreflect 2.2 or later](https://math-comp.github.io) - opam: name: coq-hierarchy-builder - version: '{>= "1.7.0"}' + version: '{ (>= "1.7.0" & < "1.9~") | (= "dev") }' description: |- [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) - opam: diff --git a/pcm/automap.v b/pcm/automap.v index 88d8474..a39c577 100644 --- a/pcm/automap.v +++ b/pcm/automap.v @@ -43,7 +43,7 @@ From pcm Require Import pcm unionmap natmap. (* The context of keys is thus seq K. The context of vars is seq U. *) Section ReflectionContexts. -Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Structure ctx := Context {keyx : seq K; varx : seq U}. @@ -74,8 +74,8 @@ End ReflectionContexts. (* now for reflection *) Section Reflection. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). -Implicit Type i : @ctx K _ _ U. +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). +Implicit Type i : ctx (K:=K) U. Inductive term := Pts of nat & T | Var of nat. @@ -200,7 +200,7 @@ End Reflection. (* subterm is purely functional version of validX *) Section Subterm. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (i : ctx U) (ts : seq (term T)). Fixpoint subterm ts1 ts2 := @@ -232,7 +232,7 @@ End Subterm. (* subtract is purely functional version of domeqX *) Section Subtract. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (i : ctx U) (ts : seq (term T)). (* We need a subterm lemma that returns the uncancelled stuff from *) @@ -273,7 +273,7 @@ End Subtract. (* invalid is a purely functional test of invalidX *) Section Invalid. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (i : ctx U) (t : term T) (ts : seq (term T)). Definition undefx i t := @@ -315,7 +315,7 @@ End Invalid. Module Syntactify. Section Syntactify. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (i : ctx U) (ts : seq (term T)). (* a tagging structure to control the flow of computation *) @@ -404,7 +404,7 @@ Export Syntactify.Exports. Module ValidX. Section ValidX. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (j : ctx U) (ts : seq (term T)). Notation form := Syntactify.form. Notation untag := Syntactify.untag. @@ -471,7 +471,7 @@ Canonical equate. Canonical start. Section Exports. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (j : ctx U) (ts : seq (term T)). Notation form := Syntactify.form. Notation untag := Syntactify.untag. @@ -509,7 +509,7 @@ Export ValidX.Exports. Module DomeqX. Section DomeqX. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (j : ctx U) (ts : seq (term T)). Notation form := Syntactify.form. Notation untag := Syntactify.untag. @@ -548,7 +548,7 @@ Canonical equate. Canonical start. Section Exports. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (j : ctx U) (ts : seq (term T)). Notation form := Syntactify.form. Notation untag := Syntactify.untag. @@ -583,7 +583,7 @@ Export DomeqX.Exports. Module InvalidX. Section InvalidX. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (i : ctx U) (ts : seq (term T)). Notation form := Syntactify.form. Notation untag := Syntactify.untag. @@ -614,7 +614,7 @@ Canonical equate. Canonical start. Section Exports. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Implicit Types (i : ctx U) (ts : seq (term T)). Notation form := Syntactify.form. Notation untag := Syntactify.untag. diff --git a/pcm/heap.v b/pcm/heap.v index ea4c3c1..f2955a1 100644 --- a/pcm/heap.v +++ b/pcm/heap.v @@ -324,8 +324,8 @@ Lemma updi_inv x xs1 xs2 : valid (updi x xs1) -> updi x xs1 = updi x xs2 -> xs1 = xs2. Proof. elim: xs1 x xs2 =>[|v1 xs1 IH] x /=; case=>[|v2 xs2] //= D. -- by case/esym/umap0E=>/unitbP; rewrite um_unitbPt. -- by case/umap0E=>/unitbP; rewrite um_unitbPt. +- by case/esym/join0I=>/unitbP; rewrite um_unitbPt. +- by case/join0I=>/unitbP; rewrite um_unitbPt. by case/(hcancelV D)=><- {}D /(IH _ _ D) <-. Qed. diff --git a/pcm/morphism.v b/pcm/morphism.v index 57e193d..79ae583 100644 --- a/pcm/morphism.v +++ b/pcm/morphism.v @@ -13,7 +13,7 @@ limitations under the License. From HB Require Import structures. From Coq Require Import ssreflect ssrbool ssrfun. -From mathcomp Require Import ssrnat eqtype choice fintype finfun. +From mathcomp Require Import ssrnat eqtype fintype finfun. From pcm Require Import options pred axioms prelude. From pcm Require Import pcm. @@ -2369,11 +2369,25 @@ case/fpVI=>/= W1 H1 /fpVI [/= W2 H2]. by rewrite -(pval_psub S _ W1 H1) -(pval_psub S _ W2 H2) E. Qed. +(* unitb *) + +Lemma unitb_psub (x : V) : unitb (psub S x) = unitb x. +Proof. +apply/unitbP/unitbP=>[E|->]; last by rewrite pfunit. +by apply: psub_inj; [rewrite E|rewrite pfunit]. +Qed. + +Lemma unitb_pval (x : U) : unitb (pval S x) = unitb x. +Proof. +apply/unitbP/unitbP=>[E|->]; last by rewrite pfunit. +by apply: pval_inj; rewrite pfunit. +Qed. + End DerivedLemmas. Prenex Implicits valid_sepE valid_pvalE valid_pvalEP valid_pvalS valid_psubS valid_sepUnE valid_pvalUnE valid_pvalUnS valid_sep3E valid_psubUnX valid_psubXUn -psubUnX psubXUn pvalXUn pvalUnX pval_inj psub_inj. +psubUnX psubXUn pvalXUn pvalUnX pval_inj psub_inj unitb_psub unitb_pval. (* properties of V propagate to U *) @@ -2797,6 +2811,21 @@ rewrite /undef/= xsep_undefE valxE /psub/= subxE /=. by case: decP=>//; rewrite (negbTE X) andbF. Qed. +(***************************) +(* xsep preserves conicity *) +(***************************) + +Lemma xsep_is_conic (V : tpcmc) (D : seprel V) : + pcmc_axiom (xsep D). +Proof. +move=>x y; case: (normalP (x \+ y))=>[//|W]. +rewrite /unitb /= xsep_unitbE pfjoinT //=. +by move/join00. +Qed. + +HB.instance Definition _ (V : tpcmc) (D : seprel V) := + isPCMC.Build (xsep D) (@xsep_is_conic V D). + (*****************************************) (* Normalize = mod out trivially by relT *) (*****************************************) diff --git a/pcm/mutex.v b/pcm/mutex.v index ef6c6c2..58c5232 100644 --- a/pcm/mutex.v +++ b/pcm/mutex.v @@ -80,6 +80,14 @@ Lemma mutex_is_normal : normal_tpcm_axiom (mutex T). Proof. by case; [right|rewrite valid_unit; left|move=>t; left]. Qed. HB.instance Definition _ : isNormal_TPCM (mutex T) := isNormal_TPCM.Build (mutex T) mutex_is_normal. + +(* conicity *) +Lemma mutex_is_conical : pcmc_axiom (mutex T). +Proof. by case=>[||x1][||x2]. Qed. + +HB.instance Definition _ := + isPCMC.Build (mutex T) mutex_is_conical. + End GeneralizedMutex. (* if T is eqType, so is mutex T *) diff --git a/pcm/natmap.v b/pcm/natmap.v index 7189964..7faf782 100644 --- a/pcm/natmap.v +++ b/pcm/natmap.v @@ -291,7 +291,7 @@ Lemma lastkeyP A (U : natmap A) (h : U) : (last_val h). Proof. have L (x : U) : valid x -> last_key x \notin dom x -> x = Unit. -- rewrite /last_key !umEX /UM.valid/UM.dom/UM.empty -{4}[x]tfE. +- rewrite /last_key/domx !umEX /UM.valid/UM.dom/UM.empty -{4}[x]tfE. case: (UMC_from x)=>//=; case=>s H H1 _ /seq_last_in. by rewrite eqE UM.umapE /supp fmapE /= {H H1}; elim: s. case: (normalP0 h)=>[->|->|]. @@ -339,7 +339,7 @@ Lemma dom_lastkey h k : k \in dom h -> k <= last_key h. Proof. -rewrite /last_key !umEX /UM.dom; case: (UMC_from h)=>//; case=>s H _ /=. +rewrite /last_key/domx !umEX /UM.dom; case: (UMC_from h)=>//; case=>s H _ /=. rewrite /supp/ord /= (leq_eqVlt k) orbC. by apply: sorted_last_key_maxR otrans (sorted_oleq H). Qed. @@ -561,9 +561,9 @@ Proof. move=>D; have {}D : last_key h \in dom h by case: lastkeyP D. case: (um_eta D)=>v [Ef Eh]. have N : last_key h \notin dom (free h (last_key h)). -- by rewrite domF inE eqxx. +- by rewrite domF eqxx. have: last_key (free h (last_key h)) <= last_key h. -- by apply: lastkey_mono=>x; rewrite domF inE; case: ifP. +- by apply: lastkey_mono=>x; rewrite domF; case/andP. rewrite leq_eqVlt; case/orP=>// /eqP E; rewrite -{1}E in N. have : last_key h > 0 by move/dom_cond: D; case: (last_key h). by case: lastkeyP N. diff --git a/pcm/pcm.v b/pcm/pcm.v index 3e0f949..34dbfd2 100644 --- a/pcm/pcm.v +++ b/pcm/pcm.v @@ -19,7 +19,8 @@ limitations under the License. From HB Require Import structures. From Coq Require Import ssreflect ssrbool ssrfun Setoid. -From mathcomp Require Import ssrnat eqtype seq bigop choice fintype finset finfun. +From mathcomp Require Import ssrnat eqtype seq bigop choice. +From mathcomp Require Import fintype finset finfun. From pcm Require Import options axioms prelude seqperm pred seqext. Declare Scope pcm_scope. @@ -214,6 +215,45 @@ Qed. End CPCMLemmas. +(****************) +(* Conical PCMs *) +(****************) + +(* commutative monoid is conical if *) +(* x+y=0 implies that x=y=0, for any elements x,y *) +(* https://en.wikipedia.org/wiki/Refinement_monoid *) + +Definition pcmc_axiom (U : pcm) := + forall x1 x2 : U, unitb (x1 \+ x2) -> unitb x1 && unitb x2. + +HB.mixin Record isPCMC U of PCM U := { + pcmc_subproof : pcmc_axiom U}. + +#[short(type="pcmc")] +HB.structure Definition PCMC := {U of PCM U & isPCMC U}. + +Section Repack. +Context {U : pcmc}. +Implicit Type x : U. + +Lemma join00 {x1 x2} : unitb (x1 \+ x2) -> unitb x1 && unitb x2. +Proof. by move/pcmc_subproof. Qed. + +Lemma join0L {x1 x2} : unitb (x1 \+ x2) -> unitb x1. +Proof. by case/join00/andP. Qed. + +Lemma join0R {x1 x2} : unitb (x1 \+ x2) -> unitb x2. +Proof. by case/join00/andP. Qed. + +Lemma join0E {x1 x2 : U} : unitb (x1 \+ x2) = unitb x1 && unitb x2. +Proof. +apply/idP/idP; first by apply/join00. +by case/andP=>/unitbP -> /unitbP ->; apply/unitbP; rewrite unitL. +Qed. + +Lemma join0I {x1 x2} : x1 \+ x2 = Unit -> x1 = Unit /\ x2 = Unit. +Proof. by case/unitbP/join00/andP; split; apply/unitbP. Qed. +End Repack. (***************) (* Topped PCMs *) @@ -368,6 +408,58 @@ HB.structure Definition Normal_CTPCM := {U of Normal_TPCM U & CPCM U}. #[short(type="normal_eqctpcm")] HB.structure Definition Normal_EQCTPCM := {U of Normal_TPCM U & EQCPCM U}. +(* adding conical variants *) + +(* conical pcm with decidable equality *) +#[short(type="eqpcmc")] +HB.structure Definition EQPCMC := {U of Equality U & PCMC U}. + +(* conical cancellative pcm *) +#[short(type="cpcmc")] +HB.structure Definition CPCMC := {U of CPCM U & PCMC U}. + +(* conical tpcm *) +#[short(type="tpcmc")] +HB.structure Definition TPCMC := {U of TPCM U & PCMC U}. + +(* conical normal tpcm *) +#[short(type="normal_tpcmc")] +HB.structure Definition Normal_TPCMC := {U of Normal_TPCM U & PCMC U}. + +(* conical with two extra properties *) + +(* conical cancellative pcm with decidable equality *) +#[short(type="eqcpcmc")] +HB.structure Definition EQCPCMC := {U of CPCM U & EQPCMC U}. + +(* conical tpcm with decidable equality *) +#[short(type="eqtpcmc")] +HB.structure Definition EQTPCMC := {U of TPCMC U & EQPCM U}. + +(* conical cancellative tpcm *) +#[short(type="ctpcmc")] +HB.structure Definition CTPCMC := {U of TPCMC U & CTPCM U}. + +(* conical with three extra properties *) + +(* conical normal tpcm with decidable equality *) +#[short(type="normal_eqtpcmc")] +HB.structure Definition Normal_EQTPCMC := {U of Normal_TPCMC U & EQPCM U}. + +(* conical normal cancellative tpcm *) +#[short(type="normal_ctpcmc")] +HB.structure Definition Normal_CTPCMC := {U of Normal_TPCMC U & CTPCM U}. + +(* conical cancellative tpcm with decidable equality *) +#[short(type="eqctpcmc")] +HB.structure Definition EQCTPCMC := {U of EQTPCMC U & CTPCM U}. + +(* conical with four extra properties *) + +(* conical normal cancellative tpcm with decidable equality *) +#[short(type="normal_eqctpcmc")] +HB.structure Definition Normal_EQCTPCMC := {U of Normal_CTPCM U & EQPCMC U}. + (***************************************) (* Support for big operators over PCMs *) @@ -411,32 +503,41 @@ Proof. by split=>//; [apply:addnC|apply:addnA|apply:(@eqP _^~_)]. Qed. HB.instance Definition natPCM : isPCM nat := isPCM.Build nat nat_is_pcm. (* Check (PCM.clone nat _). *) +Lemma nat_is_conical : pcmc_axiom nat. +Proof. +move=>x y /unitbP/eqP; rewrite addn_eq0. +by case/andP=>/eqP -> /eqP ->. +Qed. +HB.instance Definition _ := isPCMC.Build nat nat_is_conical. + (* nats are pcm with multiplication too *) (* but the instance isn't declared canonical as natPCM already is *) Lemma nat_is_mulpcm : pcm_axiom xpredT mult 1 (eq_op^~ 1). Proof. by split=>//; [apply:mulnC|apply:mulnA|apply:mul1n|apply:(@eqP _^~_)]. Qed. -(* HB.instance Definition nat_mulPCM : isPCM nat := - isPCM.Build nat nat_is_mulpcm. *) +HB.instance Definition nat_mulPCM : isPCM nat := isPCM.Build nat nat_is_mulpcm. (* nats with max too *) Lemma nat_is_maxpcm : pcm_axiom xpredT maxn 0 (eq_op^~ 0). Proof. by split=>//; [apply:maxnC|apply:maxnA|apply:max0n|apply:(@eqP _^~_)]. Qed. -(* HB.instance Definition nat_maxPCM : isPCM nat := - isPCM.Build nat nat_is_maxpcm. *) +HB.instance Definition nat_maxPCM : isPCM nat := isPCM.Build nat nat_is_maxpcm. -(* bools with conjunction *) +(* bools with disjunction *) (* eqpcm automatically inferred *) -Lemma bool_is_pcm : pcm_axiom xpredT andb true (eq_op^~ true). -Proof. by split=>//; [apply:andbC|apply:andbA|apply:(@eqP _^~_)]. Qed. -HB.instance Definition boolPCM : isPCM bool := isPCM.Build bool bool_is_pcm. +Lemma bool_is_disjpcm : pcm_axiom xpredT orb false (eq_op^~ false). +Proof. by split=>//; [apply:orbC|apply:orbA|apply:(@eqP _^~_)]. Qed. +HB.instance Definition bool_disjPCM : isPCM bool := + isPCM.Build bool bool_is_disjpcm. (* Check (EQPCM.clone bool _). *) -(* bools with disjunction *) +Lemma bool_is_conical : pcmc_axiom bool. +Proof. by case; case. Qed. +HB.instance Definition _ := isPCMC.Build bool bool_is_conical. + +(* bools with conjunction *) (* but the instance isn't declared canonical as boolPCM alread is *) -Lemma bool_is_disjpcm : pcm_axiom xpredT orb false (eq_op^~ false). -Proof. by split=>//; [apply:orbC|apply:orbA|apply:(@eqP _^~_)]. Qed. -(* HB.instance Definition bool_disjPCM : isPCM bool := - isPCM.Build bool bool_is_disjpcm. *) +Lemma bool_is_pcm : pcm_axiom xpredT andb true (eq_op^~ true). +Proof. by split=>//; [apply:andbC|apply:andbA|apply:(@eqP _^~_)]. Qed. +HB.instance Definition boolPCM : isPCM bool := isPCM.Build bool bool_is_pcm. (* positive nats under max *) Section PosNatMax. @@ -542,6 +643,12 @@ Lemma option_is_normal (U : pcm) : @valid U =1 xpredT -> normal_tpcm_axiom (option U). Proof. by move=>E [x|]; [left; rewrite /valid /= E|right]. Qed. +(* option preserves conicity *) +Lemma option_is_conical (U : pcmc) : pcmc_axiom (option U). +Proof. by case=>[x|][y|] //= /unitbP [/unitbP/join00]. Qed. +HB.instance Definition _ (U : pcmc) := + isPCMC.Build (option U) (@option_is_conical U). + (* case analysis infrastructure *) CoInductive option_pcm_spec (A : pcm) (x y : option A) : option A -> Type := @@ -591,6 +698,16 @@ HB.instance Definition _ (U V : eqpcm) := PCM.copy (U * V)%type _. Arguments unit2 /. +Lemma prod_is_conical (U V : pcmc) : pcmc_axiom (U * V)%type. +Proof. +case=>x1 x2 [y1 y2] /unitbP []. +case/unitbP/join00/andP=>X1 Y1 /unitbP/join00/andP [X2 Y2]. +by rewrite /unitb /= X1 X2 Y1 Y2. +Qed. + +HB.instance Definition _ (U V : pcmc) := + isPCMC.Build (U * V)%type (@prod_is_conical U V). + (* product simplification *) Section Simplification. Variable U V : pcm. @@ -657,6 +774,17 @@ HB.instance Definition _ (U1 U2 U3 : eqpcm) := Arguments unit3 /. +Lemma prod3_is_conical (U1 U2 U3 : pcmc) : pcmc_axiom (Prod3 U1 U2 U3). +Proof. +case=>x1 x2 x3 [y1 y2 y3] /unitbP []. +case/unitbP/join00/andP=>X1 Y1 /unitbP/join00/andP [X2 Y2] +/unitbP/join00/andP [X3 Y3]. +by rewrite /unitb /= X1 X2 X3 Y1 Y2 Y3. +Qed. + +HB.instance Definition _ (U1 U2 U3 : pcmc) := + isPCMC.Build (Prod3 U1 U2 U3) (@prod3_is_conical U1 U2 U3). + Section Prod4PCM. Variables U1 U2 U3 U4 : pcm. Notation tp := (Prod4 U1 U2 U3 U4). @@ -699,6 +827,17 @@ HB.instance Definition _ (U1 U2 U3 U4 : eqpcm) := Arguments unit4 /. +Lemma prod4_is_conical (U1 U2 U3 U4 : pcmc) : pcmc_axiom (Prod4 U1 U2 U3 U4). +Proof. +case=>x1 x2 x3 x4 [y1 y2 y3 y4] /unitbP []. +case/unitbP/join00/andP=>X1 Y1 /unitbP/join00/andP [X2 Y2] +/unitbP/join00/andP [X3 Y3] /unitbP/join00/andP [X4 Y4]. +by rewrite /unitb /= X1 X2 X3 X4 Y1 Y2 Y3 Y4. +Qed. + +HB.instance Definition _ (U1 U2 U3 U4 : pcmc) := + isPCMC.Build (Prod4 U1 U2 U3 U4) (@prod4_is_conical U1 U2 U3 U4). + Section Prod5PCM. Variables U1 U2 U3 U4 U5 : pcm. Notation tp := (Prod5 U1 U2 U3 U4 U5). @@ -745,6 +884,19 @@ HB.instance Definition _ (U1 U2 U3 U4 U5 : eqpcm) := Arguments unit5 /. +Lemma prod5_is_conical (U1 U2 U3 U4 U5 : pcmc) : + pcmc_axiom (Prod5 U1 U2 U3 U4 U5). +Proof. +case=>x1 x2 x3 x4 x5 [y1 y2 y3 y4 y5] /unitbP []. +case/unitbP/join00/andP=>X1 Y1 /unitbP/join00/andP [X2 Y2] +/unitbP/join00/andP [X3 Y3 ]/unitbP/join00/andP [X4 Y4] +/unitbP/join00/andP [X5 Y5]. +by rewrite /unitb /= X1 X2 X3 X4 X5 Y1 Y2 Y3 Y4 Y5. +Qed. + +HB.instance Definition _ (U1 U2 U3 U4 U5 : pcmc) := + isPCMC.Build (Prod5 U1 U2 U3 U4 U5) (@prod5_is_conical U1 U2 U3 U4 U5). + Section Prod6PCM. Variables U1 U2 U3 U4 U5 U6 : pcm. Notation tp := (Prod6 U1 U2 U3 U4 U5 U6). @@ -794,6 +946,19 @@ HB.instance Definition _ (U1 U2 U3 U4 U5 U6 : eqpcm) := Arguments unit6 /. +Lemma prod6_is_conical (U1 U2 U3 U4 U5 U6 : pcmc) : + pcmc_axiom (Prod6 U1 U2 U3 U4 U5 U6). +Proof. +case=>x1 x2 x3 x4 x5 x6 [y1 y2 y3 y4 y5 y6] /unitbP []. +case/unitbP/join00/andP=>X1 Y1 /unitbP/join00/andP [X2 Y2] +/unitbP/join00/andP [X3 Y3 ]/unitbP/join00/andP [X4 Y4] +/unitbP/join00/andP [X5 Y5] /unitbP/join00/andP [X6 Y6]. +by rewrite /unitb /= X1 X2 X3 X4 X5 X6 Y1 Y2 Y3 Y4 Y5 Y6. +Qed. + +HB.instance Definition _ (U1 U2 U3 U4 U5 U6 : pcmc) := + isPCMC.Build (Prod6 U1 U2 U3 U4 U5 U6) (@prod6_is_conical U1 U2 U3 U4 U5 U6). + Section Prod7PCM. Variables U1 U2 U3 U4 U5 U6 U7 : pcm. Notation tp := (Prod7 U1 U2 U3 U4 U5 U6 U7). @@ -846,6 +1011,21 @@ HB.instance Definition _ (U1 U2 U3 U4 U5 U6 U7 : eqpcm) := Arguments unit7 /. +Lemma prod7_is_conical (U1 U2 U3 U4 U5 U6 U7 : pcmc) : + pcmc_axiom (Prod7 U1 U2 U3 U4 U5 U6 U7). +Proof. +case=>x1 x2 x3 x4 x5 x6 x7 [y1 y2 y3 y4 y5 y6 y7] /unitbP []. +case/unitbP/join00/andP=>X1 Y1 /unitbP/join00/andP [X2 Y2] +/unitbP/join00/andP [X3 Y3 ]/unitbP/join00/andP [X4 Y4] +/unitbP/join00/andP [X5 Y5] /unitbP/join00/andP [X6 Y6] +/unitbP/join00/andP [X7 Y7]. +by rewrite /unitb /= X1 X2 X3 X4 X5 X6 X7 Y1 Y2 Y3 Y4 Y5 Y6 Y7. +Qed. + +HB.instance Definition _ (U1 U2 U3 U4 U5 U6 U7 : pcmc) := + isPCMC.Build (Prod7 U1 U2 U3 U4 U5 U6 U7) + (@prod7_is_conical U1 U2 U3 U4 U5 U6 U7). + (* Finite products of PCMs as functions *) Section FunPCM. Variables (T : finType) (Us : T -> pcm). @@ -876,8 +1056,7 @@ End FunPCM. Arguments fun_unit /. (* we won't use fun types for any examples *) -(* so we don't need equality structure on them *) - +(* so we don't need equality or conicity structure on them *) (* Finite products of PCMs as finfuns *) (* We will work with this second structure, though *) @@ -918,6 +1097,16 @@ HB.instance Definition _ (T : finType) (Us : T -> eqpcm) := Arguments fin_unit /. +Lemma dffun_is_conical (T : finType) (Us : T -> pcmc) : + pcmc_axiom {dffun forall t, Us t}. +Proof. +by move=>x y /forallP H; apply/andP; split; apply/forallP=>t; +move: (H t); rewrite /sel !ffunE; [move/join0L|move/join0R]. +Qed. + +HB.instance Definition _ (T : finType) (Us : T -> pcmc) := + isPCMC.Build {dffun forall t, Us t} (@dffun_is_conical T Us). + (* product of TPCMs is a TPCM *) (* With TPCMs we could remove the pairs where *) diff --git a/pcm/unionmap.v b/pcm/unionmap.v index 7262083..e1244c4 100644 --- a/pcm/unionmap.v +++ b/pcm/unionmap.v @@ -104,7 +104,7 @@ From pcm Require Import pcm morphism. (****************************) (* UM.base type is reference implementation of union_maps. *) -(* Type has @union_map K structure if it exhibits isomorphism with UM.base. *) +(* Type has union_map structure if it exhibits isomorphism with UM.base. *) (* Tying to reference implementation is alternative to axiomatizing *) (* union maps, which seems unwieldy. *) (* Thus, the underlying type of all union_maps instances will be *) @@ -277,7 +277,7 @@ End UM. (***********************) (***********************) -(* type T has @union_map K structure is it's cancellative TPCM *) +(* type T has union_map structure is it's cancellative TPCM *) (* with an isomorphism to UM.base *) Definition union_map_axiom (K : ordType) (C : pred K) V T @@ -304,7 +304,7 @@ Definition union_map_axiom (K : ordType) (C : pred K) V T HB.mixin Record isUnionMap_helper (K : ordType) (C : pred K) V T of Normal_CTPCM T := { upd : K -> V -> T -> T; - dom : T -> seq K; + dom_op : T -> seq K; assocs : T -> seq (K * V); free : T -> K -> T; find : K -> T -> option V; @@ -312,26 +312,28 @@ HB.mixin Record isUnionMap_helper (K : ordType) (C : pred K) V T of UMC_from : T -> @UM.base K C V; UMC_to : UM.base C V -> T; union_map_helper_subproof : - union_map_axiom valid Unit undef upd dom assocs + union_map_axiom valid Unit undef upd dom_op assocs free find join unitb undefb pts_op UMC_from UMC_to}. -(* embed cancellative topped PCM structure to enable inheritance *) +(* embed cancellative topped conical PCM structure to enable inheritance *) (* we prove later that this isn't needed *) #[short(type="union_map")] HB.structure Definition UMC K C V := - {T of @isUnionMap_helper K C V T & Normal_TPCM T & CTPCM T}. + {T of @isUnionMap_helper K C V T & Normal_TPCM T & CTPCMC T}. -Lemma ftE K C V (U : @union_map K C V) b : UMC_from (UMC_to b : U) = b. +Arguments union_map : clear implicits. + +Lemma ftE K C V (U : union_map K C V) b : UMC_from (UMC_to b : U) = b. Proof. by rewrite union_map_helper_subproof. Qed. -Lemma tfE K C V (U : @union_map K C V) b : UMC_to (UMC_from b) = b :> U. +Lemma tfE K C V (U : union_map K C V) b : UMC_to (UMC_from b) = b :> U. Proof. by rewrite union_map_helper_subproof. Qed. -Lemma eqE K C V (U : @union_map K C V) (b1 b2 : UM.base C V) : +Lemma eqE K C V (U : union_map K C V) (b1 b2 : UM.base C V) : UMC_to b1 = UMC_to b2 :> U <-> b1 = b2. Proof. by split=>[E|->//]; rewrite -(ftE U b1) -(ftE U b2) E. Qed. -Definition umEX K C V (U : @union_map K C V) := +Definition umEX K C V (U : union_map K C V) := (@union_map_helper_subproof K C V U, eqE, UM.umapE). (* Build CTCPM structure from the rest *) @@ -431,10 +433,28 @@ Qed. HB.instance Definition _ := isNormal_TPCM.Build T union_map_is_normal. HB.instance Definition _ := isUnionMap_helper.Build K C V T union_map_subproof. + +Lemma union_map_is_conical : pcmc_axiom T. +Proof. +move=>/= x y; rewrite /unitb pcmE /= !umEX ftE /UM.empb/UM.union. +case: (um_from x) (um_from y)=>[|fx Fx][|fy Fy] //=; case: ifP=>E //. +case: (supp (fcat fx fy) =P [::])=>// E1 _; case: (supp fx =P [::])=>E2 /=. +- by move/supp_nilE: E2 E1=>-> /eqP; rewrite fcat0s. +have [k H3] : exists k, k \in supp fx. +- case: (supp fx) {E1 E} E2=>[|k s _] //. + by exists k; rewrite inE eqxx. +suff : k \in supp (fcat fx fy) by rewrite E1. +by rewrite supp_fcat inE /= H3. +Qed. + +HB.instance Definition _ := isPCMC.Build T union_map_is_conical. HB.end. -(* Making pts infer @union_map K structure *) -Definition ptsx K C V (U : @union_map K C V) k v of phant U : U := +(* Notation for pts and dom that infers union_map structure. *) +(* Different structures can use different syntax for pts and dom *) + +(* Making pts infer union_map structure *) +Definition ptsx K C V (U : union_map K C V) k v of phant U : U := @pts_op K C V U k v. (* use ptsT to pass map type explicitly *) @@ -445,6 +465,19 @@ Notation "@ 'pts' K C V U k v" := (@ptsx K C V U%type k v (Phant U)) (at level 10, K at level 8, C at level 8, V at level 8, U at level 8, k at level 8, v at level 8, only parsing). +(* Making dom infer union_map structure *) +Definition domx K C V (U : union_map K C V) f of phant U : seq K := + @dom_op K C V U f. + +(* use domT to pass map type explicitly *) +(* use dom when type inferrable or for printing *) +Notation domT U f := (domx f (Phant U)) (only parsing). +Notation dom f := (domT _ f). +Notation "@ 'dom' K C V U f" := (@domx K C V U%type f (Phant U)) + (at level 10, K at level 8, C at level 8, V at level 8, + U at level 8, f at level 8, only parsing). + + (*************************************) (* Union map with decidable equality *) (*************************************) @@ -453,7 +486,7 @@ Notation "@ 'pts' K C V U k v" := (@ptsx K C V U%type k v (Phant U)) Section UnionMapEq. Variables (K : ordType) (C : pred K) (V : eqType). -Variable (U : @union_map K C V). +Variables U : union_map K C V. Definition union_map_eq (f1 f2 : U) := match (UMC_from f1), (UMC_from f2) with @@ -575,29 +608,45 @@ Abort. (* dom *) (*******) -Notation "[ 'dom' f ]" := [mem (dom f)] : fun_scope. +Notation "[ 'dom' f ]" := + [mem (dom f)] (format "[ 'dom' f ]") : fun_scope. Section DomLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f g : U). Lemma dom_undef : dom (undef : U) = [::]. -Proof. by rewrite !umEX. Qed. +Proof. by rewrite /domx !umEX. Qed. Lemma dom0 : dom (Unit : U) = [::]. -Proof. by rewrite !umEX. Qed. +Proof. by rewrite /domx !umEX. Qed. + +Lemma sorted_dom f : sorted (@ord K) (dom f). +Proof. by rewrite /domx !umEX; case: (UMC_from f)=>[|[]]. Qed. + +Lemma sorted_dom_oleq f : sorted (@oleq K) (dom f). +Proof. by apply: sorted_oleq (sorted_dom f). Qed. + +Lemma uniq_dom f : uniq (dom f). +Proof. +apply: sorted_uniq (sorted_dom f); +by [apply: ordtype.trans | apply: ordtype.irr]. +Qed. Lemma dom0E f : valid f -> dom f =i pred0 -> f = Unit. Proof. -rewrite !umEX /UM.valid /UM.dom /UM.empty -{3}[f]tfE !eqE UM.umapE. +rewrite /domx !umEX /UM.valid /UM.dom /UM.empty -{3}[f]tfE !eqE UM.umapE. case: (UMC_from f)=>[|f' S] //= _; rewrite fmapE /= {S}. by case: f'; case=>[|kv s] //= P /= /(_ kv.1); rewrite inE eq_refl. Qed. -Lemma domNE f : reflect (dom f = [::]) (unitb f || undefb f). +Lemma all_dom f : all C (dom f). +Proof. by rewrite /domx !umEX; case: (UMC_from f). Qed. + +Lemma domNE f : reflect (dom f = [::]) (unitb f || undefb f). Proof. case: (normalP0 f)=>[->|->|W N]; constructor; rewrite ?dom0 ?dom_undef //. by move=>M; apply: N; apply: dom0E W _; rewrite M. @@ -614,29 +663,41 @@ Lemma domU k v f : dom (upd k v f) =i [pred x | C k & if x == k then valid f else x \in dom f]. Proof. -rewrite !umEX /UM.dom /UM.upd /UM.valid /=. +rewrite /domx !umEX /UM.dom /UM.upd /UM.valid /=. case: (UMC_from f)=>[|f' H] /= x. - by rewrite !inE andbC; case: ifP. case: decP=>[->|/(introF idP)->//]. by rewrite supp_ins. Qed. -Lemma domF k f : +Lemma domFF k f : dom (free f k) =i [pred x | if k == x then false else x \in dom f]. Proof. -rewrite !umEX; case: (UMC_from f)=>[|f' H] x; rewrite inE /=; +rewrite /domx !umEX; case: (UMC_from f)=>[|f' H] x; rewrite inE /=; by case: ifP=>// E; rewrite supp_rem inE /= eq_sym E. Qed. +Lemma domFE k f : + dom (free f k) = filter (predC1 k) (dom f). +Proof. +apply/ord_sorted_eq; first by apply/sorted_dom. +- by apply/sorted_filter=>//; apply/sorted_dom. +by move=>z; rewrite mem_filter domFF inE /= eq_sym; case: eqP. +Qed. + +Lemma domF k x f : + x \in dom (free f k) = (x != k) && (x \in dom f). +Proof. by rewrite domFE mem_filter. Qed. + Lemma subdomF k f : {subset dom (free f k) <= dom f}. -Proof. by move=>x; rewrite domF inE; case: eqP. Qed. +Proof. by move=>x; rewrite domF=>/andP []. Qed. Lemma domUn f1 f2 : dom (f1 \+ f2) =i [pred x | valid (f1 \+ f2) & (x \in dom f1) || (x \in dom f2)]. Proof. -rewrite !umEX /UM.dom /UM.valid /UM.union. +rewrite /domx !umEX /UM.dom /UM.valid /UM.union. case: (UMC_from f1) (UMC_from f2)=>[|f1' H1] // [|f2' H2] // x. by case: ifP=>E //; rewrite supp_fcat. Qed. @@ -648,10 +709,10 @@ Lemma domUnE f1 f2 x : Proof. by move=>W; rewrite domUn inE W. Qed. Lemma dom_valid k f : k \in dom f -> valid f. -Proof. by rewrite !umEX; case: (UMC_from f). Qed. +Proof. by rewrite /domx !umEX; case: (UMC_from f). Qed. Lemma dom_cond k f : k \in dom f -> C k. -Proof. by rewrite !umEX; case: (UMC_from f)=>[|f' F] // /(allP F). Qed. +Proof. by rewrite /domx !umEX; case: (UMC_from f)=>[|f' F] // /(allP F). Qed. Lemma cond_dom k f : ~~ C k -> k \in dom f = false. Proof. by apply: contraTF=>/dom_cond ->. Qed. @@ -674,7 +735,7 @@ Proof. by move=> D; apply/contra/dom_inIR. Qed. Lemma dom_free k f : k \notin dom f -> free f k = f. Proof. -rewrite -{3}[f]tfE !umEX /UM.dom /UM.free /=. +rewrite /domx -{3}[f]tfE !umEX /UM.dom /UM.free /=. by case: (UMC_from f)=>[|f' H] //; apply: rem_supp. Qed. @@ -685,7 +746,7 @@ Variant dom_find_spec k f : option V -> bool -> Type := Lemma dom_find k f : dom_find_spec k f (find k f) (k \in dom f). Proof. -rewrite !umEX /UM.dom -{1}[f]tfE. +rewrite /domx !umEX /UM.dom -{1}[f]tfE. case: (UMC_from f)=>[|f' H]. - by apply: dom_find_none''; rewrite !umEX. case: suppP (allP H k)=>[v|] /[dup] H1 /= -> I; last first. @@ -710,7 +771,7 @@ Lemma dom_prec f1 f2 g1 g2 : f1 \+ g1 = f2 \+ g2 -> dom f1 =i dom f2 -> f1 = f2. Proof. -rewrite -{4}[f1]tfE -{3}[f2]tfE /= !umEX. +rewrite /domx -{4}[f1]tfE -{3}[f2]tfE /= !umEX. rewrite /UM.valid /UM.union /UM.dom; move=>D E. case: (UMC_from f1) (UMC_from f2) (UMC_from g1) (UMC_from g2) E D=> [|f1' F1][|f2' F2][|g1' G1][|g2' G2] //; @@ -724,21 +785,6 @@ suff L: forall m s, k \in supp m -> disj m s -> by move=>m s S; case: disjP=>//; move/(_ _ S)/negbTE; rewrite fnd_fcat=>->. Qed. -Lemma sorted_dom f : sorted (@ord K) (dom f). -Proof. by rewrite !umEX; case: (UMC_from f)=>[|[]]. Qed. - -Lemma sorted_dom_oleq f : sorted (@oleq K) (dom f). -Proof. by apply: sorted_oleq (sorted_dom f). Qed. - -Lemma uniq_dom f : uniq (dom f). -Proof. -apply: sorted_uniq (sorted_dom f); -by [apply: ordtype.trans | apply: ordtype.irr]. -Qed. - -Lemma all_dom f : all C (dom f). -Proof. by rewrite !umEX; case: (UMC_from f). Qed. - Lemma perm_domUn f1 f2 : valid (f1 \+ f2) -> perm_eq (dom (f1 \+ f2)) (dom f1 ++ dom f2). Proof. @@ -746,7 +792,7 @@ move=>Vh; apply: uniq_perm; last 1 first. - by move=>x; rewrite mem_cat domUn inE Vh. - by apply: uniq_dom. rewrite cat_uniq !uniq_dom /= andbT; apply/hasPn=>x. -rewrite !umEX /UM.valid /UM.union /UM.dom in Vh *. +rewrite /domx !umEX /UM.valid /UM.union /UM.dom in Vh *. case: (UMC_from f1) (UMC_from f2) Vh=>// f1' H1 [//|f2' H2]. by case: disjP=>// H _; apply: contraL (H x). Qed. @@ -759,7 +805,7 @@ Proof. by move/perm_domUn/seq.perm_size; rewrite size_cat. Qed. Lemma size_domF k f : k \in dom f -> size (dom (free f k)) = (size (dom f)).-1. Proof. -rewrite !umEX; case: (UMC_from f)=>[|f'] //=; case: f'=>f' F /= _. +rewrite /domx !umEX; case: (UMC_from f)=>[|f'] //=; case: f'=>f' F /= _. rewrite /supp /= !size_map size_filter=>H. move/(sorted_uniq (@trans K) (@irr K))/count_uniq_mem: F=>/(_ k). rewrite {}H count_map /ssrbool.preim /= => H. @@ -771,7 +817,7 @@ Lemma size_domU k v f : size (dom (upd k v f)) = if k \in dom f then size (dom f) else (size (dom f)).+1. Proof. -rewrite !umEX /UM.valid /UM.upd /UM.dom. +rewrite /domx !umEX /UM.valid /UM.upd /UM.dom. case: (UMC_from f)=>[|f'] //= H; case: decP=>// P _. by case: f' H=>f' F H; rewrite /supp /= !size_map size_ins'. Qed. @@ -787,7 +833,7 @@ Prenex Implicits find_some find_none subdomF. (* lemmas for comparing doms of two differently-typed maps *) Section DomLemmas2. Variables (K : ordType) (C1 C2 : pred K) (V1 V2 : Type). -Variables (U1 : @union_map K C1 V1) (U2 : @union_map K C2 V2). +Variables (U1 : union_map K C1 V1) (U2 : union_map K C2 V2). Lemma domE (f1 : U1) (f2 : U2) : dom f1 =i dom f2 <-> dom f1 = dom f2. Proof. by split=>[|->] //; apply/ord_sorted_eq/sorted_dom/sorted_dom. Qed. @@ -797,7 +843,7 @@ Lemma domKi (f1 g1 : U1) (f2 g2 : U2) : dom (f1 \+ g1) =i dom (f2 \+ g2) -> dom f1 =i dom f2 -> dom g1 =i dom g2. Proof. -rewrite !umEX /UM.valid /UM.union /UM.dom. +rewrite /domx !umEX /UM.valid /UM.union /UM.dom. case: (UMC_from f1) (UMC_from f2) (UMC_from g1) (UMC_from g2)=> [|f1' F1][|f2' F2][|g1' G1][|g2' G2] //. case: disjP=>// D1 _; case: disjP=>// D2 _ E1 E2 x. @@ -846,7 +892,7 @@ End DomLemmas2. (*********) Section ValidLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f g : U). Lemma invalidE f : ~~ valid f <-> f = undef. @@ -879,9 +925,9 @@ case: (UMC_from f1) (UMC_from f2)=>[|f1' F1][|f2' F2] /=. - by apply: valid_false2; rewrite !umEX. case: ifP=>E. - apply: valid_true; try by rewrite !umEX. - by move=>k; rewrite !umEX => H; case: disjP E=>//; move/(_ _ H). + by move=>k; rewrite /domx !umEX => H; case: disjP E=>//; move/(_ _ H). case: disjP E=>// k T1 T2 _. -by apply: (valid_false3 (k:=k)); rewrite !umEX. +by apply: (valid_false3 (k:=k)); rewrite /domx !umEX. Qed. Lemma validUnAE f1 f2 : @@ -918,7 +964,7 @@ Proof. case: validUn=>// V1 V2 H _; case: validUn=>//. - by rewrite validF V1. - by rewrite V2. -by move=>k'; rewrite domF inE; case: eqP=>// _ /H/negbTE ->. +by move=>x; rewrite domF=>/andP [_] /H/negbTE ->. Qed. Lemma validUnF k f1 f2 : @@ -969,7 +1015,7 @@ Proof. by case: (k1 =P k2) =>// <- W H /(dom_inNLX W H). Qed. Lemma dom_inNX k1 k2 f1 f2 : valid (f1 \+ f2) -> - k1 \in dom f1 -> k2 \in dom f2 -> k1 <> k2. + k1 \in dom f1 -> k2 \in dom f2 -> k1 <> k2. Proof. by move=>W K1 K2; apply/eqP; apply: dom_inN K1 K2. Qed. End ValidLemmas. @@ -982,7 +1028,7 @@ End ValidLemmas. (* AKA empb *) Section UnitbLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U). Lemma um_unitbU k v f : unitb (upd k v f) = false. @@ -993,35 +1039,13 @@ suff: k \in supp (ins k v f') by case: (supp _). by rewrite supp_ins inE /= eq_refl. Qed. -Lemma um_unitbUn f1 f2 : unitb (f1 \+ f2) = unitb f1 && unitb f2. -Proof. -rewrite !umEX /UM.empb /UM.union. -case: (UMC_from f1) (UMC_from f2)=>[|f1' F1][|f2' F2] //. -- by rewrite andbF. -case: ifP=>E; case: eqP=>E1; case: eqP=>E2 //; last 2 first. -- by move: E2 E1; move/supp_nilE=>->; rewrite fcat0s; case: eqP. -- by move: E1 E2 E; do 2![move/supp_nilE=>->]; case: disjP. -- by move/supp_nilE: E2 E1=>-> <-; rewrite fcat0s eq_refl. -have [k H3]: exists k, k \in supp f1'. -- case: (supp f1') {E1 E} E2=>[|x s _] //. - by exists x; rewrite inE eq_refl. -suff: k \in supp (fcat f1' f2') by rewrite E1. -by rewrite supp_fcat inE /= H3. -Qed. - (* some transformation lemmas *) -(* AKA conicity *) -Lemma umap0E f1 f2 : f1 \+ f2 = Unit -> f1 = Unit /\ f2 = Unit. -Proof. -by move/unitbP; rewrite um_unitbUn=>/andP [H1 H2]; split; apply/unitbP. -Qed. - Lemma validEb f : reflect (valid f /\ forall k, k \notin dom f) (unitb f). Proof. case: unitbP=>E; constructor; first by rewrite E valid_unit dom0. case=>V' H; apply: E; move: V' H. -rewrite !umEX /UM.valid /UM.dom /UM.empty -{3}[f]tfE. +rewrite /domx !umEX /UM.valid /UM.dom /UM.empty -{3}[f]tfE. case: (UMC_from f)=>[|f' F] // _ H; rewrite !umEX. apply/supp_nilE; case: (supp f') H=>// x s /(_ x). by rewrite inE eq_refl. @@ -1042,7 +1066,7 @@ End UnitbLemmas. (**********) Section UndefbLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U). Lemma undefb_undef : undefb (undef : U). @@ -1075,8 +1099,8 @@ End UndefbLemmas. Section DomEqDef. Variables (K : ordType) (C1 C2 : pred K) (V1 V2 : Type). -Variable U1 : @union_map K C1 V1. -Variable U2 : @union_map K C2 V2. +Variable U1 : union_map K C1 V1. +Variable U2 : union_map K C2 V2. Definition dom_eq (f1 : U1) (f2 : U2) := (valid f1 == valid f2) && (dom f1 == dom f2). @@ -1085,9 +1109,9 @@ End DomEqDef. Section DomEqLemmas. Variables (K : ordType) (C1 C2 C3 : pred K) (V1 V2 V3 : Type). -Variable U1 : @union_map K C1 V1. -Variable U2 : @union_map K C2 V2. -Variable U3 : @union_map K C3 V3. +Variable U1 : union_map K C1 V1. +Variable U2 : union_map K C2 V2. +Variable U3 : union_map K C3 V3. Lemma domeqP (f1 : U1) (f2 : U2) : reflect (valid f1 = valid f2 /\ dom f1 = dom f2) (dom_eq f1 f2). @@ -1129,8 +1153,8 @@ Lemma domeqVUnE (f1 f1' : U1) (f2 f2' : U2) : dom_eq f1 f2 -> dom_eq f1' f2' -> valid (f1 \+ f1') = valid (f2 \+ f2'). Proof. -suff L (C1' C2' : pred K) V1' V2' (U1' : @union_map K C1' V1') - (U2' : @union_map K C2' V2') (g1 g1' : U1') (g2 g2' : U2') : +suff L (C1' C2' : pred K) V1' V2' (U1' : union_map K C1' V1') + (U2' : union_map K C2' V2') (g1 g1' : U1') (g2 g2' : U2') : dom_eq g1 g2 -> dom_eq g1' g2' -> valid (g1 \+ g1') -> valid (g2 \+ g2'). - by move=>D D'; apply/idP/idP; apply: L=>//; apply: domeq_sym. @@ -1180,7 +1204,7 @@ End DomEqLemmas. Hint Resolve domeq_refl : core. Section DomEq1Lemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Lemma domeqfU k v (f : U) : k \in dom f -> dom_eq f (upd k v f). Proof. @@ -1213,7 +1237,7 @@ End DomEq1Lemmas. Section DomEq2Lemmas. Variables (K : ordType) (C1 C2 : pred K) (V1 V2 : Type). -Variables (U1 : @union_map K C1 V1) (U2 : @union_map K C2 V2). +Variables (U1 : union_map K C1 V1) (U2 : union_map K C2 V2). Lemma domeq_symE (f1 : U1) (f2 : U2) : dom_eq f1 f2 = dom_eq f2 f1. Proof. by apply/idP/idP; apply: domeq_sym. Qed. @@ -1226,7 +1250,7 @@ End DomEq2Lemmas. (**********) Section UpdateLemmas. -Variable (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variable (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U). Lemma upd_undef k v : upd k v undef = undef :> U. @@ -1273,7 +1297,7 @@ Lemma updUnL k v f1 f2 : upd k v (f1 \+ f2) = if k \in dom f1 then upd k v f1 \+ f2 else f1 \+ upd k v f2. Proof. -rewrite !umEX /UM.upd /UM.union /UM.dom. +rewrite /domx !umEX /UM.upd /UM.union /UM.dom. case: (UMC_from f1) (UMC_from f2)=>[|f1' F1][|f2' F2] //=. - by case: ifP=>//; case: decP. case: ifP=>// D; case: ifP=>// H1; case: decP=>// H2. @@ -1311,7 +1335,7 @@ End UpdateLemmas. (********) Section FreeLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U). Lemma free0 k : free Unit k = Unit :> U. @@ -1347,7 +1371,7 @@ Lemma freeUn k f1 f2 : if k \in dom (f1 \+ f2) then free f1 k \+ free f2 k else f1 \+ f2. Proof. -rewrite !umEX /UM.free /UM.union /UM.dom. +rewrite /domx !umEX /UM.free /UM.union /UM.dom. case: (UMC_from f1) (UMC_from f2)=>[|f1' F1][|f2' F2] //. case: ifP=>// E1; rewrite supp_fcat inE /=. case: ifP=>E2; last by rewrite !umEX rem_supp // supp_fcat inE E2. @@ -1378,8 +1402,8 @@ suff: ~~ valid (f1 \+ free f2 k) by move/invalidE: V2=>-> /invalidE ->. apply: contra V2; case: validUn=>// H1 H2 H _. case: validUn=>//; first by rewrite H1. - by move: H2; rewrite validF => ->. -move=>x H3; move: (H _ H3); rewrite domF inE /=. -by case: ifP H3 V1=>[|_ _ _]; [move/eqP=><- -> | move/negbTE=>->]. +move=>x H3; move: (H _ H3); rewrite domF negb_and negbK. +by case: (x =P k) H3 V1=>[->|_ _ _ /negbTE] ->. Qed. Lemma freeUnL k f1 f2 : @@ -1412,7 +1436,7 @@ End FreeLemmas. (********) Section FindLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U). Lemma find0E k : find k (Unit : U) = None. @@ -1452,7 +1476,7 @@ Lemma findUnL k f1 f2 : valid (f1 \+ f2) -> find k (f1 \+ f2) = if k \in dom f1 then find k f1 else find k f2. Proof. -rewrite !umEX /UM.valid /UM.find /UM.union /UM.dom. +rewrite /domx !umEX /UM.valid /UM.find /UM.union /UM.dom. case: (UMC_from f1) (UMC_from f2)=>[|f1' F1][|f2' F2] //. case: ifP=>// D _; case: ifP=>E1; last first. - rewrite fnd_fcat; case: ifP=>// E2. @@ -1480,7 +1504,7 @@ End FindLemmas. (* if maps store units, i.e., we keep them just for sets *) (* then we can simplify the find_eta lemma a bit *) -Lemma domeq_eta (K : ordType) (C : pred K) (U : @union_map K C unit) (f1 f2 : U) : +Lemma domeq_eta (K : ordType) (C : pred K) (U : union_map K C unit) (f1 f2 : U) : dom_eq f1 f2 -> f1 = f2. Proof. case/domeqP=>V E; case V1 : (valid f1); last first. @@ -1496,7 +1520,7 @@ Qed. (**********) Section AssocsLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Type f : U. Lemma assocs_valid k f : k \In assocs f -> valid f. @@ -1521,7 +1545,7 @@ by case: ifP=>// D _; apply: seqof_fcat_perm D. Qed. Lemma assocs_dom f : dom f = map fst (assocs f). -Proof. by rewrite !umEX; case: (UMC_from f). Qed. +Proof. by rewrite /domx !umEX; case: (UMC_from f). Qed. Lemma size_assocs f : size (assocs f) = size (dom f). Proof. by rewrite assocs_dom size_map. Qed. @@ -1553,12 +1577,24 @@ move=>H1 H2; case: H2 H1. by move=>H1 H2; apply: IH H2 H1. Qed. +Lemma Uniq_assocs K C V (U : @union_map K C V) (f : U) : + Uniq (assocs f). +Proof. +rewrite !umEX /UM.assocs /=; case: (UMC_from f)=>[|[s H _]] //=. +move/(sorted_uniq (@trans K) (@irr K)): H. +apply: map_Uniq. +Qed. + +Lemma sorted_assocs K C V (U : @union_map K C V) (f : U) : + sorted (relpre fst ord) (assocs f). +Proof. rewrite -sorted_map -assocs_dom; exact: sorted_dom. Qed. + (*********************************) (* Interaction of subset and dom *) (*********************************) Section Interaction. -Variables (K : ordType) (C : pred K) (A : Type) (U : @union_map K C A). +Variables (K : ordType) (C : pred K) (A : Type) (U : union_map K C A). Implicit Types (x y a b : U) (p q : pred K). (* Some equivalent forms for subset with dom *) @@ -1598,7 +1634,7 @@ End Interaction. (****************************) Section PointsToLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U). Lemma ptsU k v : pts k v = upd k v Unit :> U. @@ -1609,7 +1645,7 @@ Proof. by move=>C'; rewrite ptsU upd_condN. Qed. Lemma domPtK k v : dom (pts k v : U) = if C k then [:: k] else [::]. Proof. -rewrite /ptsx !umEX /= /UM.dom /supp /UM.pts /UM.upd /UM.empty /=. +rewrite /domx/ptsx !umEX /= /UM.dom /supp /UM.pts /UM.upd /UM.empty /=. by case D : (decP _)=>[a|a] /=; rewrite ?a ?(introF idP a). Qed. @@ -1689,7 +1725,7 @@ Lemma assocsUnPt f k v : all (ord^~ k) (dom f) -> assocs (f \+ pts k v) = rcons (assocs f) (k, v). Proof. -rewrite /ptsx !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. +rewrite /domx/ptsx !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. case: (UMC_from f)=>//=; case: decP=>//= H1 g H2; case: ifP=>//= _ _. by case: allP=>//; case: g H2=>// s1 H2 H3 H4 _; apply: first_ins' H4. Qed. @@ -1699,7 +1735,7 @@ Lemma assocsPtUn f k v : all (ord k) (dom f) -> assocs (pts k v \+ f) = (k, v) :: (assocs f). Proof. -rewrite /ptsx !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. +rewrite /domx/ptsx !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. case: decP=>// H1; case: (UMC_from f)=>//= g H2. rewrite /disj /= andbT; case: ifP=>//= D _ H3. rewrite (fcat_inss _ (@nil K V) D) fcat0s. @@ -1908,7 +1944,7 @@ case: (normalP f)=>[->|W]; first by rewrite upd_undef free_undef join_undef. case H : (C k); last first. - by move/negbT: H=>H; rewrite (upd_condN v) // pts_condN // undef_join. have W' : valid (pts k v \+ free f k). -- by rewrite validPtUn H validF W domF inE eq_refl. +- by rewrite validPtUn H validF W domF eqxx. apply: find_eta=>//; first by rewrite validU H W. by move=>k'; rewrite findU H W findPtUn2 // findF; case: eqP. Qed. @@ -1921,7 +1957,7 @@ Proof. by move=>D; rewrite upd_eta freeND. Qed. (* um_unitb *) Lemma um_unitbPtUn k v f : unitb (pts k v \+ f) = false. -Proof. by rewrite um_unitbUn um_unitbPt. Qed. +Proof. by rewrite join0E um_unitbPt. Qed. Lemma um_unitbUnPt k v f : unitb (f \+ pts k v) = false. Proof. by rewrite joinC; apply: um_unitbPtUn. Qed. @@ -1948,7 +1984,7 @@ Lemma um_eta k f : k \in dom f -> exists v, find k f = Some v /\ f = pts k v \+ free f k. Proof. case: dom_find=>// v E1 E2 _; exists v; split=>//. -by rewrite {1}E2 -{1}[free f k]unitL updUnR domF inE /= eq_refl ptsU. +by rewrite {1}E2 -{1}[free f k]unitL updUnR domF eqxx ptsU. Qed. Lemma um_eta2 k v f : find k f = Some v -> f = pts k v \+ free f k. @@ -2002,7 +2038,7 @@ Lemma um_indf (P : U -> Prop) : P (pts k v \+ f)) -> forall f, P f. Proof. -rewrite /ptsx !umEX => H1 H2 H3 f; rewrite -[f]tfE. +rewrite /domx/ptsx !umEX => H1 H2 H3 f; rewrite -[f]tfE. apply: (UM.base_indf (P := (fun b => P (UMC_to b))))=>//. move=>k v g H V1; move: (H3 k v _ H); rewrite !umEX. by apply. @@ -2016,7 +2052,7 @@ Lemma um_indb (P : U -> Prop) : P (pts k v \+ f)) -> forall f, P f. Proof. -rewrite /ptsx !umEX => H1 H2 H3 f; rewrite -[f]tfE. +rewrite /domx/ptsx !umEX => H1 H2 H3 f; rewrite -[f]tfE. apply: (UM.base_indb (P := (fun b => P (UMC_to b))))=>//. move=>k v g H V1; move: (H3 k v _ H); rewrite !umEX. by apply. @@ -2048,7 +2084,7 @@ have W : valid (pts k2 w2 \+ (f1 \+ f)). - by rewrite -(validPt _ v) -E -joinA in X. rewrite -[pts k v]unitR -joinA in E. move/(cancel2 W): E; case: ifP. -- by move/eqP=>-> [->] /umap0E [->->]; rewrite unitR; left. +- by move/eqP=>-> [->] /join0I [->->]; rewrite unitR; left. by move=>_ [_ _] /esym/unitbP; rewrite um_unitbPtUn. Qed. @@ -2064,7 +2100,7 @@ Prenex Implicits validPtUnD validUnPtD cancelPt cancelPt2 um_prime. Section DomeqPtLemmas. Variables (K : ordType) (C1 C2 : pred K) (V1 V2 : Type). -Variables (U1 : @union_map K C1 V1) (U2 : @union_map K C2 V2). +Variables (U1 : union_map K C1 V1) (U2 : union_map K C2 V2). Lemma domeqPt (k : K) (v1 : V1) (v2 : V2) : C1 k = C2 k -> @@ -2090,7 +2126,7 @@ Hint Resolve domeqPt domeqPtUn domeqUnPt : core. Section EqPtLemmas. Variables (K : ordType) (C : pred K) (V : eqType). -Variables (U : @union_map K C V). +Variables (U : union_map K C V). Notation Ue := (Equality.pack_ (Equality.Mixin (union_map_eqP (U:=U)))). @@ -2138,7 +2174,7 @@ Lemma um0UndefE : (Unit == undef :> Ue) = false. Proof. by rewrite eq_sym umUndef0E. Qed. Lemma umPtUE (k : K) (v : V) f : (pts k v \+ f == Unit :> Ue) = false. -Proof. by apply/eqP=>/umap0E/proj1/unitbP; rewrite um_unitbPt. Qed. +Proof. by apply/eqP=>/join0I/proj1/unitbP; rewrite um_unitbPt. Qed. Lemma umUPtE (k : K) (v : V) f : (f \+ pts k v == Unit :> Ue) = false. Proof. by rewrite joinC umPtUE. Qed. @@ -2210,7 +2246,7 @@ End EqPtLemmas. (************) Section PreimDefLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (k : K) (v : V) (f : U) (p : pred V). Definition um_preim p f k := oapp p false (find k f). @@ -2265,7 +2301,7 @@ End PreimDefLemmas. (****************************) Section MapMembership. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Type f : U. Definition Mem_UmMap f := @@ -2495,6 +2531,18 @@ have : find x1 (pts x1 v1 \+ z) = Some v1 by rewrite findPtUn // -E. by rewrite -E findF; case: eqP=>//= _ /In_find. Qed. +(* stronger version of InU that removes k from f *) +Lemma InFU x k v f : + x \In upd k v f <-> + valid (upd k v f) /\ + if x.1 == k then x.2 = v else x \In free f k. +Proof. +split; last first. +- by case=>W H; apply/InU; split=>//; case: ifP H=>// _ /InF []. +case/InU=>W; case: ifPn=>// N H; split=>//. +by apply/InF; rewrite validF (In_valid H). +Qed. + Lemma In_eta k v f : (k, v) \In f -> f = pts k v \+ free f k. Proof. by move=>H; case/In_dom/um_eta: (H)=>w [/In_find/(In_fun H) ->]. Qed. @@ -2503,7 +2551,7 @@ End MapMembership. Arguments In_condPt {K C V U k}. Prenex Implicits InPt In_eta InPtUn In_dom InPtUnEL In_findE. -(* Umap and fset are special cases of @union_map K but are *) +(* Umap and fset are special cases of union_map but are *) (* defined before membership structure is declared. *) (* Their membership structures aren't directly inheritted from that *) (* of union_map, but must be declared separately *) @@ -2518,7 +2566,7 @@ Coercion Pred_of_fset K (x : fset K) : {Pred _} := Section MorphMembership. Variables (K : ordType) (C : pred K) (V : Type). -Variables (U1 : pcm) (U2 : @union_map K C V). +Variables (U1 : pcm) (U2 : union_map K C V). Section PlainMorph. Variable f : pcm_morph U1 U2. @@ -2576,7 +2624,7 @@ End MorphMembership. (*********) Section Range. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types f : U. Definition range f := map snd (assocs f). @@ -2672,7 +2720,7 @@ Prenex Implicits In_range_valid In_range In_rangeUn In_rangeF. (* decidable versions, when V is eqtype *) Section DecidableRange. -Variables (K : ordType) (C : pred K) (V : eqType) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : eqType) (U : union_map K C V). Implicit Types f : U. Lemma uniq_rangeP f : @@ -2805,7 +2853,7 @@ End DecidableRange. (********************) Section MapMonotonicity. -Variables (K V : ordType) (C : pred K) (U : @union_map K C V). +Variables (K V : ordType) (C : pred K) (U : union_map K C V). Implicit Types f : U. Definition um_mono f := sorted ord (range f). @@ -2958,7 +3006,7 @@ End MapMonotonicity. (* Induction lemmas over PCMs in the proofs *) Section FoldDefAndLemmas. -Variables (K : ordType) (C : pred K) (V R : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V R : Type) (U : union_map K C V). Implicit Type f : U. Definition um_foldl (a : R -> K -> V -> R) (z0 d : R) f := @@ -3110,12 +3158,12 @@ Qed. End FoldDefAndLemmas. Section PCMFold. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Variables (R : pcm) (a : R -> K -> V -> R). Hypothesis frame : forall x y k v, a (x \+ y) k v = a x k v \+ y. Lemma umfoldl0_frame z0 d (f : U) : - valid f -> @um_foldl K _ _ _ _ a z0 d f = um_foldl a Unit d f \+ z0. + valid f -> um_foldl (K:=K) a z0 d f = um_foldl a Unit d f \+ z0. Proof. move=>W; elim/um_indf: f W d z0 =>[||k v f IH _ /(order_path_min (@trans K)) P] W d z0. @@ -3151,12 +3199,12 @@ End PCMFold. (* Fold when the function produces a map *) Section FoldMap. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Variable (a : U -> K -> V -> U). Hypothesis frame : forall x y k v, a (x \+ y) k v = a x k v \+ y. Lemma In_umfoldlMX (f : U) (k : K) (v : V) : - (k, v) \In @um_foldl K _ _ _ _ a Unit undef f -> + (k, v) \In um_foldl (K:=K) a Unit undef f -> exists k1 (v1 : V), (k, v) \In a Unit k1 v1 /\ (k1, v1) \In f. Proof. elim/um_indf: f. @@ -3185,7 +3233,7 @@ End FoldMap. Section MapPrefix. Variables (K : ordType) (C : pred K) (V : Type). -Variables (U : @union_map K C V). +Variables (U : union_map K C V). Definition um_prefix (h1 h2 : U) := Prefix (assocs h1) (assocs h2). @@ -3254,7 +3302,7 @@ case/(IH _ (validR W1) W')=>h2 Eh' H; exists h2. move=>x y; rewrite domPtUn inE W1 /=; case/orP; last by apply: H. move/eqP=><-{x} Dy. have : y \in dom h' by rewrite Eh' domUn inE -Eh' W' /= Dy orbT. -rewrite domF inE; case: (k =P y)=>// /eqP N. +rewrite domF eq_sym; case: (k =P y)=>// /eqP N. rewrite assocs_dom Eh /= inE eq_sym (negbTE N) /=. case/mem_seqP/MapP; case=>a b X -> /=. have {}P : path ord k (map fst (assocs h1 ++ h2')). @@ -3278,7 +3326,7 @@ End MapPrefix. (* Definition and basic properties *) Section OmapDefs. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Variable f : K * V -> option V'. Definition omap (x : U) : U' := @@ -3362,21 +3410,21 @@ Arguments omap {K C V V' U U'}. (* Structure definition *) Definition omap_fun_axiom (K : ordType) (C : pred K) (V V' : Type) - (U : @union_map K C V) (U' : @union_map K C V') + (U : union_map K C V) (U' : union_map K C V') (f : U -> U') (omf : K * V -> option V') := f =1 omap omf. (* factory to use if full/norm/tpcm morphism property already proved *) (* (omap_fun isn't binormal as it can drop timestamps) *) HB.mixin Record isOmapFun_morph (K : ordType) (C : pred K) (V V' : Type) - (U : @union_map K C V) (U' : @union_map K C V') (f : U -> U') of + (U : union_map K C V) (U' : union_map K C V') (f : U -> U') of @Full_Norm_TPCM_morphism U U' f := { omf_op : K * V -> option V'; omfE_op : omap_fun_axiom f omf_op}. #[short(type=omap_fun)] HB.structure Definition OmapFun (K : ordType) (C : pred K) (V V' : Type) - (U : @union_map K C V) (U' : @union_map K C V') := + (U : union_map K C V) (U' : union_map K C V') := {f of isOmapFun_morph K C V V' U U' f &}. Arguments omfE_op {K C V V' U U'}. @@ -3385,7 +3433,7 @@ Arguments omf_op {K C V V' U U'} _ _ /. (* factory to use when full/norm/tpcm morphism property *) (* hasn't been established *) HB.factory Record isOmapFun (K : ordType) (C : pred K) (V V' : Type) - (U : @union_map K C V) (U' : @union_map K C V') (f : U -> U') := { + (U : union_map K C V) (U' : union_map K C V') (f : U -> U') := { omf : K * V -> option V'; omfE : omap_fun_axiom f omf}. @@ -3424,7 +3472,7 @@ HB.end. (* notation to hide the structure when projecting omf *) Section OmapFunNotation. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Definition omfx (f : omap_fun U U') of phantom (U -> U') f : K * V -> option V' := omf_op f. @@ -3440,7 +3488,7 @@ Notation omf f := (omfx (Phantom (_ -> _) f)). (* omap is omap_fun *) Section OmapOmapFun. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). HB.instance Definition _ f := isOmapFun.Build K C V V' U U' (omap f) (fun => erefl _). @@ -3453,7 +3501,7 @@ End OmapOmapFun. Section OmapFunLemmas. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Implicit Types (f : omap_fun U U') (x : U). (* different name for pfjoin on full morphisms *) @@ -3658,7 +3706,7 @@ Proof. case: ifP=>// D; last by rewrite (upd_condN v x (negbT D)) pfundef. case: (normalP x)=>[->|H]. - by case: (omf _ _)=>[a|]; rewrite ?(upd_undef,free_undef,pfundef). -rewrite upd_eta omfPtUn validPtUn D validF H domF inE eq_refl /=. +rewrite upd_eta omfPtUn validPtUn D validF H domF eqxx /=. case: (omf _ _)=>[xa|]; last by rewrite omfF. by rewrite upd_eta omfF. Qed. @@ -3772,7 +3820,7 @@ Arguments In_odom {K C V V' U U' f x k} . Section OmapFun2. Variables (K : ordType) (C : pred K) (V V1 V2 : Type). -Variables (U : @union_map K C V) (U1 : @union_map K C V1) (U2 : @union_map K C V2). +Variables (U : union_map K C V) (U1 : union_map K C V1) (U2 : union_map K C V2). Variables (f1 : omap_fun U U1) (f2 : omap_fun U U2). (* when one mapped function is included in other *) @@ -3810,7 +3858,7 @@ End OmapFun2. Section OmapFun2Eq. Variables (K : ordType) (C : pred K) (V V1 V2 : Type). -Variables (U : @union_map K C V) (U1 : @union_map K C V1) (U2 : @union_map K C V2). +Variables (U : union_map K C V) (U1 : union_map K C V1) (U2 : union_map K C V2). Variables (f1 : omap_fun U U1) (f2 : omap_fun U U2). Lemma omf_dom_eq (x : U) : @@ -3825,7 +3873,7 @@ End OmapFun2Eq. Section OmapMembershipExtra. Variables (K : ordType) (C : pred K) (V1 V2 : Type). -Variables (U1 : @union_map K C V1) (U2 : @union_map K C V2). +Variables (U1 : union_map K C V1) (U2 : union_map K C V2). Variables f : omap_fun U1 U2. Lemma omfL e (x y : U1) : @@ -3873,7 +3921,7 @@ End OmapMembershipExtra. Section OmapMembershipExtra2. Variables (K : ordType) (C : pred K) (V1 V2 : Type). -Variables (U1 : @union_map K C V1) (U2 : @union_map K C V2). +Variables (U1 : union_map K C V1) (U2 : union_map K C V2). Variables f : omap_fun U1 U2. Lemma omfDL00 k a (x y : U1) : @@ -3917,7 +3965,7 @@ End OmapMembershipExtra2. Section OmapFunId. Variables (K : ordType) (C : pred K) (V : Type). -Variables (U : @union_map K C V). +Variables (U : union_map K C V). Lemma omf_some (f : omap_fun U U) x : (forall kv, kv \In x -> omf f kv = Some kv.2) -> @@ -3950,7 +3998,7 @@ End OmapFunId. Section OmapFunComp. Variables (K : ordType) (C : pred K) (V1 V2 V3 : Type). -Variables (U1 : @union_map K C V1) (U2 : @union_map K C V2) (U3 : @union_map K C V3). +Variables (U1 : union_map K C V1) (U2 : union_map K C V2) (U3 : union_map K C V3). Variables (f1 : omap_fun U1 U2) (f2 : omap_fun U2 U3). Lemma comp_is_omap_fun : @@ -3986,7 +4034,7 @@ Notation omapv f := (omap (f \o snd)). Notation mapv f := (omapv (Some \o f)). Section OmapId. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Lemma omapv_id : omapv Some =1 @id U. Proof. by move=>x; apply: omf_some. Qed. @@ -3998,7 +4046,7 @@ End OmapId. Section OmapComp. Variables (K : ordType) (C : pred K) (V1 V2 V3 : Type). -Variables (U1 : @union_map K C V1) (U2 : @union_map K C V2) (U3 : @union_map K C V3). +Variables (U1 : union_map K C V1) (U2 : union_map K C V2) (U3 : union_map K C V3). Lemma omap_omap f1 f2 (x : U1) : omap f2 (omap f1 x : U2) = @@ -4028,7 +4076,7 @@ End OmapComp. Section OmapMembership. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Lemma In_omapX f k v (x : U) : (k, v) \In (omap f x : U') <-> @@ -4058,7 +4106,7 @@ Arguments In_omapv {K C V V' U U' f k v w}. Section OmapMembership2. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Lemma In_omapV f g k v (x : U) : ocancel f g -> pcancel g f -> @@ -4083,7 +4131,7 @@ End OmapMembership2. Section OmapMembership3. Variables (K : ordType) (C : pred K) (V V' : eqType). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). (* decidable variant of In_rangev *) Lemma mem_rangev f g v (x : U) : @@ -4099,7 +4147,7 @@ End OmapMembership3. (* freeing k representable as omap *) Section OmapFree. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Lemma omap_free k x : free x k = @@ -4119,7 +4167,7 @@ End OmapFree. (* eq_in_omap *) Section EqInOmap. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Lemma eq_in_omap a1 a2 (h : U) : (forall kv, kv \In h -> a1 kv = a2 kv) <-> @@ -4135,7 +4183,7 @@ End EqInOmap. (* filter that works over both domain and range at once *) Section FilterDefLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (f : U) (p q : pred (K * V)). Definition um_filter p f : U := @@ -4196,7 +4244,7 @@ apply: (iffP (In_domX _ _)). by case=>v Hp Hf; exists v; apply/In_umfilt. Qed. -Lemma dom_omf_umfilt V' (U' : @union_map K C V') (f : omap_fun U U') x : +Lemma dom_omf_umfilt V' (U' : union_map K C V') (f : omap_fun U U') x : dom (f x) = dom (um_filter (isSome \o omf f) x). Proof. apply/domE=>k; apply/idP/idP. @@ -4207,7 +4255,7 @@ case E: (omf f (k, w))=>[a|] // _ H. by move/In_dom: (In_omf _ H E). Qed. -Lemma dom_omap_umfilt V' (U' : @union_map K C V') a x : +Lemma dom_omap_umfilt V' (U' : union_map K C V') a x : dom (omap a x : U') = dom (um_filter (isSome \o a) x). Proof. exact: dom_omf_umfilt. Qed. @@ -4256,6 +4304,23 @@ Lemma eq_in_umfiltE p1 p2 f : p1 =1 p2 -> um_filter p1 f = um_filter p2 f. Proof. by move=>S; apply/eq_in_umfilt=>kv _; apply: S. Qed. +(* filters of the same map are equal if their domains are equal *) +Lemma eq_umfiltD p1 p2 f : + dom (um_filter p1 f) =i dom (um_filter p2 f) -> + um_filter p1 f = um_filter p2 f. +Proof. +move=>S; apply/eq_in_umfilt; case=>k v H; apply/idP/idP. +- move/(In_umfilt H)/In_dom; rewrite S. + by case/In_domX=>v2 /In_umfiltX [P2] /(In_fun H) ->. +move/(In_umfilt H)/In_dom; rewrite -S. +by case/In_domX=>v1 /In_umfiltX [P1] /(In_fun H) ->. +Qed. + +Lemma id_umfiltD p f : + dom (um_filter p f) =i dom f -> + um_filter p f = f. +Proof. by rewrite -{2 4}(umfilt_predT f); apply: eq_umfiltD. Qed. + Lemma umfiltC p1 p2 f : um_filter p1 (um_filter p2 f) = um_filter p2 (um_filter p1 f). Proof. @@ -4415,6 +4480,11 @@ move: (In_fun H1 H2)=>E; rewrite -{v2}E in X2 H2 *. by apply/In_dom_umfilt; exists v1=>//; apply/andP. Qed. +Lemma dom_umfiltF p f z x : + z \in dom (um_filter p (free f x)) = + (z != x) && (z \in dom (um_filter p f)). +Proof. by rewrite omfF /= domF eq_sym; case: eqP. Qed. + End FilterDefLemmas. #[export] @@ -4427,7 +4497,7 @@ Notation um_filterv p f := (um_filter (p \o snd) f). Arguments In_umfilt [K C V U] p x f _ _. Section FilterKLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Type f : U. Implicit Type p q : pred K. @@ -4537,14 +4607,14 @@ Qed. (* filters commute with omap_fun *) -Lemma umfiltk_omf V' (U' : @union_map K C V') (f : omap_fun U U') p x : +Lemma umfiltk_omf V' (U' : union_map K C V') (f : omap_fun U U') p x : f (um_filterk p x) = um_filterk p (f x). Proof. rewrite (compE f) [RHS]compE eq_in_omf !omf_comp !omf_omap /=. by rewrite /obind/oapp /=; case=>k v; case: ifP; case: (omf f _). Qed. -Lemma umfiltk_dom_omf V' (U' : @union_map K C V') (f : omap_fun U U') x : +Lemma umfiltk_dom_omf V' (U' : union_map K C V') (f : omap_fun U U') x : um_filterk [dom x] (f x) = f x. Proof. by rewrite -umfiltk_omf umfiltk_dom'. Qed. @@ -4569,12 +4639,27 @@ Qed. Lemma In_umfiltk p x f : x \In f -> p x.1 -> x \In um_filterk p f. Proof. by apply: In_umfilt. Qed. +Lemma umfiltkC1 (f : U) x : + um_filterk (predC1 x) f = free f x. +Proof. +case: (normalP f)=>[->|W]; first by rewrite pfundef free_undef. +rewrite [in RHS](umfilt_predC f (pred1 x \o fst)). +rewrite freeUnL; last first. +- rewrite dom_umfiltE mem_filter. + by case: dom_find=>//= v; rewrite eqxx. +rewrite (_ : free (um_filterk (pred1 x) f) x = + um_filterk (pred1 x) (free f x)); last first. +- by rewrite umfiltkF /= eqxx. +rewrite [in RHS]umfilt_mem0L ?unitL ?validF //. +by move=>k v /InF []. +Qed. + End FilterKLemmas. Arguments In_umfiltk {K C V U} p {x f} _ _. Section FilterVLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Type f : U. Implicit Type p q : pred V. @@ -4597,7 +4682,7 @@ Arguments In_umfiltv {K C V U} p {x f} _ _. Section OmapMembershipLemmas. Variables (K : ordType) (C : pred K) (V V' : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Lemma mapv_omapv f g (x : U) : ocancel f g -> @@ -4606,6 +4691,89 @@ Proof. exact: mapv_omapvE. Qed. End OmapMembershipLemmas. +(* map fun = omap fun which is total *) + +Definition map_fun_axiom (K : ordType) (C : pred K) V V' + (U : @union_map K C V) (U' : @union_map K C V') + (f : omap_fun U U') := + forall x, isSome (omf f x). + +HB.mixin Record isMapFun (K : ordType) (C : pred K) (V V' : Type) + (U : @union_map K C V) (U' : @union_map K C V') (f : U -> U') of + @OmapFun K C V V' U U' f := { + mapfun_subproof : map_fun_axiom f}. + +#[short(type=map_fun)] +HB.structure Definition MapFun (K : ordType) (C : pred K) (V V' : Type) + (U : @union_map K C V) (U' : @union_map K C V') := + {f of isMapFun K C V V' U U' f & + @Binorm_PCM_morphism U U' f & + OmapFun K f}. + +HB.builders Context K C V V' U U' f of isMapFun K C V V' U U' f. +Lemma map_fun_is_binorm_morph : binorm_pcm_morph_axiom f. +Proof. +by move=>x y; rewrite -omfUn_some ?pfVE ?pfT //= => k; rewrite mapfun_subproof. +Qed. +HB.instance Definition _ := + isBinorm_PCM_morphism.Build U U' f map_fun_is_binorm_morph. +HB.end. + +Section MapFunLemmas. +Variables (K : ordType) (C : pred K) (V V' : Type). +Variables (U : @union_map K C V) (U' : @union_map K C V'). +Implicit Types (f : map_fun U U') (x : U). + +Lemma mf_some f (x : K * V) : omf f x. +Proof. by apply: mapfun_subproof. Qed. + +Definition mfx f (x : K * V) := + match omf f x as z return z -> V' with + | Some v => fun => v + | None => False_rect V' \o not_false_is_true + end (mf_some f x). + +Lemma mfE f : omf f =1 some \o mfx f. +Proof. by move=>x; rewrite /mfx /=; case: (omf f x) (mf_some f x). Qed. + +Lemma dom_mf f x : dom (f x) = dom x. +Proof. by rewrite dom_omf_some // => k _; rewrite mf_some. Qed. + +(* mfPt differs from omfPt in eliding validity checks *) +Lemma mfPt f k v : + f (pts k v) = pts k (mfx f (k, v)). +Proof. +case H: (C k); last by rewrite !pts_condN ?H // pfundef. +by rewrite omfPt // /mfx; case: (omf f (k, v)) (mf_some _ _). +Qed. + +(* stronger than morphism property because no validity check *) +Lemma mfUn f x1 x2 : + f (x1 \+ x2) = f x1 \+ f x2. +Proof. by rewrite omfUn_some // => k _; apply/mf_some. Qed. + +(* mfPtUn differs from omfPtUn in eliding validity check *) +Lemma mfPtUn f k v x : + f (pts k v \+ x) = pts k (mfx f (k, v)) \+ f x. +Proof. by rewrite mfUn mfPt. Qed. + +Lemma mfUnPt f k v x : + f (x \+ pts k v) = f x \+ pts k (mfx f (k, v)). +Proof. by rewrite joinC mfPtUn joinC. Qed. + +Lemma mf_unit f x : + unitb (f x) = unitb x. +Proof. +apply/omf_unit/validEb; case=>W H; split=>// k. +- by apply/In_domX; case=>v /H E; move: (mf_some f (k, v)); rewrite E. +by move/In_dom; rewrite (negbTE (H _)). +Qed. + +End MapFunLemmas. + +Arguments mfx {K C V V' U U'} _ _ /. + + (************************) (* PCM-induced ordering *) (************************) @@ -4613,7 +4781,7 @@ End OmapMembershipLemmas. (* Union maps and PCM ordering. *) Section UmpleqLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (x y a b : U) (p : pred K). (* PCM-induced preorder is order in the case of union maps *) @@ -4623,7 +4791,7 @@ Proof. case=>a -> [b]; case W : (valid x); last first. - by move/invalidE: (negbT W)=>->; rewrite undef_join. rewrite -{1 2}[x]unitR -joinA in W *. -by case/(joinxK W)/esym/umap0E=>->; rewrite unitR. +by case/(joinxK W)/esym/join0I=>->; rewrite unitR. Qed. (* lemmas on the PCM ordering and um_filter(k) *) @@ -4699,15 +4867,26 @@ Lemma umpleq_none x1 x2 t : valid x2 -> [pcm x1 <= x2] -> find t x2 = None -> find t x1 = None. Proof. by case E: (find t x1)=>[a|] // W H <-; rewrite (umpleq_some W H E). Qed. +Lemma pleq_free (f : U) k : + [pcm free f k <= f]. +Proof. +case D : (k \in dom f); last by rewrite freeND // D. +by case: (um_eta D)=>x [_ E]; rewrite {2}E. +Qed. + End UmpleqLemmas. +Prenex Implicits pleq_free. + +#[export] +Hint Resolve pleq_free : core. (********************) (* Precision lemmas *) (********************) Section Precision. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (x y : U). Lemma prec_flip x1 x2 y1 y2 : @@ -4752,7 +4931,7 @@ End Precision. (* as list of timestamps which are then read in-order. *) Section OrdEvalDefLemmas. -Variables (K : ordType) (C : pred K) (V R : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V R : Type) (U : union_map K C V). Implicit Type f : U. Implicit Type a : R -> K -> V -> R. Implicit Type p q : pred (K * V). @@ -5013,7 +5192,7 @@ Arguments oev_sub_filter {K C V R U a ks p}. Notation oevalv a ks f z0 := (oeval (fun r _ => a r) ks f z0). Section OrdEvalRelationalInduction1. -Variables (K : ordType) (C : pred K) (V R1 R2 : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V R1 R2 : Type) (U : union_map K C V). Lemma oev_ind2 {P : R1 -> R2 -> Prop} (f : U) ks a1 a2 z1 z2 : P z1 z2 -> @@ -5031,14 +5210,14 @@ Qed. End OrdEvalRelationalInduction1. Section OrdEvalPCM. -Variables (K : ordType) (C : pred K) (V : Type) (R : pcm) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (R : pcm) (U : union_map K C V). Implicit Type f : U. Variable (a : R -> K -> V -> R). Implicit Type p q : pred (K * V). Implicit Type ks : seq K. Hypothesis frame : forall x y k v, a (x \+ y) k v = a x k v \+ y. -Lemma oev1 ks f z0 : @oeval K _ _ _ _ a ks f z0 = oeval a ks f Unit \+ z0. +Lemma oev1 ks f z0 : oeval (K:=K) a ks f z0 = oeval a ks f Unit \+ z0. Proof. apply: (oev_ind2 (P:=fun r1 r2 => r1 = r2 \+ z0)); first by rewrite unitL. by move=>k v z1 z2 H1 H2 ->; apply: frame. @@ -5065,7 +5244,7 @@ End OrdEvalPCM. (* as default for undefined maps. *) Section EvalDefLemmas. -Variables (K : ordType) (C : pred K) (V R : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V R : Type) (U : union_map K C V). Implicit Type f : U. Implicit Type a : R -> K -> V -> R. Implicit Type p q : pred (K * V). @@ -5223,7 +5402,7 @@ End EvalDefLemmas. Section EvalOmapLemmas. Variables (K : ordType) (C : pred K) (V V' R : Type). -Variables (U : @union_map K C V) (U' : @union_map K C V'). +Variables (U : union_map K C V) (U' : union_map K C V'). Lemma eval_omap (b : R -> K -> V' -> R) p a (f : U) z0 : eval b p (omap a f : U') z0 = @@ -5246,7 +5425,7 @@ End EvalOmapLemmas. Section EvalRelationalInduction1. -Variables (K : ordType) (C : pred K) (V R1 R2 : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V R1 R2 : Type) (U : union_map K C V). Lemma eval_ind2 {P : R1 -> R2 -> Prop} (f : U) p0 p1 a0 a1 z0 z1 : P z0 z1 -> @@ -5267,8 +5446,8 @@ End EvalRelationalInduction1. Section EvalRelationalInduction2. Variables (K1 K2 : ordType) (C1 : pred K1) (C2 : pred K2). Variables (V1 V2 R1 R2 : Type). -Variables (U1 : @union_map K1 C1 V1) (U2 : @union_map K2 C2 V2). -Variables (U : @union_map K1 C1 K2) (P : R1 -> R2 -> Prop). +Variables (U1 : union_map K1 C1 V1) (U2 : union_map K2 C2 V2). +Variables (U : union_map K1 C1 K2) (P : R1 -> R2 -> Prop). (* generalization of eval_ind2 to different maps, but related by a bijection *) @@ -5310,7 +5489,7 @@ set phi2 := free phi1 k1. have W2 : valid f2 by move/In_dom/dom_valid: I3. have E2 : f2 = pts k2 v2 \+ free f2 k2 by apply/In_eta: I3. have A2 : all (ord k2) (dom (free f2 k2)). -- apply/allP=>x; rewrite domF inE E2 domPtUn inE -E2 W2 /= domF inE. +- apply/allP=>x; rewrite domF E2 domPtUn inE -E2 W2 /= domF eq_sym. case: eqP=>//= N; rewrite -R =>R'; move/mem_seqP/In_rangeX: (R'). case=>k' H1; apply: M1 (I1) (H1) _; move/allP: A1; apply. move/In_dom: H1 (H1); rewrite D1 inE; case/orP=>//= /eqP ->. @@ -5319,13 +5498,13 @@ rewrite E2 evalPtUn -?E2 //. have M2 : um_mono phi2. - by apply/ummonoP=>???? /InF [_ _ /M1] X /InF [_ _]; apply: X. have D2 : dom phi2 = dom f1. -- apply/domE=>x; rewrite domF inE D1 inE eq_sym. +- apply/domE=>x; rewrite domF D1 inE. by case: eqP=>// ->{x}; rewrite (negbTE (validPtUnD W)). have R2' : range phi2 = dom (free f2 k2). move/In_eta: (I1) (R)=>E1; rewrite E1 rangePtUnK. - by rewrite {1}E2 domPtUnK //; [case | rewrite -E2]. - by rewrite -E1. - apply/allP=>x; rewrite domF inE D1 inE eq_sym. + apply/allP=>x; rewrite domF D1 inE. by case: eqP=>//= _; apply/allP/A1. have {}H x1 w1 x2 w2 t1 t2 : (x1, x2) \In phi2 -> (x1, w1) \In f1 -> (x2, w2) \In free f2 k2 -> P t1 t2 -> @@ -5341,7 +5520,7 @@ End EvalRelationalInduction2. (* Evaluating frameable functions *) Section EvalFrame. -Variables (K : ordType) (C : pred K) (V : Type) (R : pcm) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (R : pcm) (U : union_map K C V). Variables (a : R -> K -> V -> R) (p : pred (K * V)). Hypothesis frame : (forall x y k v, a (x \+ y) k v = a x k v \+ y). @@ -5351,7 +5530,7 @@ Implicit Type f : U. (* so that the result is independent of the order of k *) Lemma evalFPtUn k v z0 f : valid (pts k v \+ f) -> - @eval K _ _ _ _ a p (pts k v \+ f) z0 = + eval (K:=K) a p (pts k v \+ f) z0 = if p (k, v) then a Unit k v \+ eval a p f z0 else eval a p f z0. Proof. move=>W; rewrite /eval umfiltPtUn W. @@ -5391,7 +5570,7 @@ Notation evalv a p f z0 := (eval (fun r _ => a r) p f z0). (************) Section CountDefLemmas. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Type f : U. Implicit Type p : pred (K * V). @@ -5637,8 +5816,8 @@ Hint Extern 0 (ocancel (side_m _) (Tag _)) => Section Side. Variables (K : ordType) (C : pred K) (T : eqType) (Us : T -> Type). -Variables (U : @union_map K C (sigT Us)). -Variables (Ut : forall t, @union_map K C (Us t)). +Variables (U : union_map K C (sigT Us)). +Variables (Ut : forall t, union_map K C (Us t)). Variables t : T. Definition side_map : U -> Ut t := locked (omapv (side_m t)). @@ -5741,8 +5920,8 @@ Arguments In_dom_side {K C T Us U} Ut {t x a h}. Section Side2. Variables (K : ordType) (C : pred K) (T : eqType) (Us : T -> Type). -Variables (U : @union_map K C (sigT Us)). -Variables (Ut : forall t, @union_map K C (Us t)). +Variables (U : union_map K C (sigT Us)). +Variables (Ut : forall t, union_map K C (Us t)). Variables t1 t2 : T. Lemma sideN_all_predC (h : U) : @@ -5806,13 +5985,13 @@ Definition gather_m : sigT (sliceT Us) -> sigT Us := fun '(Tag t (Tag k v)) => Tag (Tag t k) v. Variables (K : ordType) (C : pred K). -Variables (U : @union_map K C (sigT Us)). -Variables (S : @union_map K C (sigT (sliceT Us))). +Variables (U : union_map K C (sigT Us)). +Variables (S : union_map K C (sigT (sliceT Us))). Definition slice : U -> S := mapv slice_m. -HB.instance Definition _ := OmapFun.copy slice slice. +HB.instance Definition _ := OmapFun.on slice. Definition gather : S -> U := mapv gather_m. -HB.instance Definition _ := OmapFun.copy gather gather. +HB.instance Definition _ := OmapFun.on gather. Lemma In_slice x t (k : Ts t) (v : Us (Tag t k)) h : (x, Tag t (Tag k v)) \In slice h <-> @@ -5862,8 +6041,8 @@ Arguments gather {T Ts Us K C U}. Section GraftDef. Variables (K : ordType) (C : pred K) (T : eqType) (Us : T -> Type). -Variables (U : @union_map K C (sigT Us)). -Variables (Ut : forall t, @union_map K C (Us t)). +Variables (U : union_map K C (sigT Us)). +Variables (Ut : forall t, union_map K C (Us t)). Variables (h : U) (t : T). Definition graft (ht : Ut t) : U := @@ -5874,7 +6053,7 @@ Arguments graft {K C T Us U Ut}. Section GraftLemmas. Variables (K : ordType) (C : pred K) (T : eqType) (Us : T -> Type). -Variables (U : @union_map K C (sigT Us)) (Ut : forall t, @union_map K C (Us t)). +Variables (U : union_map K C (sigT Us)) (Ut : forall t, union_map K C (Us t)). Implicit Type h : U. (* ht has disjoint domain with other sides of h *) @@ -5961,7 +6140,7 @@ End GraftLemmas. Section DomMap. Variables (K : ordType) (C : pred K) (V : Type). -Variables (U : @union_map K C V) (U' : @union_map K C unit). +Variables (U : union_map K C V) (U' : union_map K C unit). Definition dom_map (x : U) : U' := omap (fun => Some tt) x. @@ -5996,8 +6175,8 @@ Arguments dom_map [K C V U U'] _. (* composing dom_map *) Section DomMapIdempotent. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). -Variables (U' : @union_map K C unit) (U'' : @union_map K C unit). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). +Variables (U' : union_map K C unit) (U'' : union_map K C unit). Lemma dom_map_idemp (x : U) : dom_map (dom_map x : U') = dom_map x :> U''. Proof. by rewrite /dom_map omap_omap. Qed. @@ -6011,7 +6190,7 @@ End DomMapIdempotent. Section MapInvert. Variables (K V : ordType) (C : pred K) (C' : pred V). -Variables (U : @union_map K C V) (U' : @union_map V C' K). +Variables (U : union_map K C V) (U' : union_map V C' K). (* inverting f = flipping each pts k v in f into pts v k *) Definition invert (f : U) : U' := @@ -6131,7 +6310,7 @@ Arguments invert {K V C C' U U'}. Section InvertLaws. Variables (K V : ordType) (C : pred K) (C' : pred V). -Variables (U : @union_map K C V) (U' : @union_map V C' K). +Variables (U : union_map K C V) (U' : union_map V C' K). Lemma valid_invert_idemp (f : U) : valid (invert (invert f : U') : U) = valid (invert f : U'). @@ -6163,7 +6342,9 @@ Arguments In_invert {K V C C' U U' k v f}. Section MapComposition. Variables (K1 K2 : ordType) (C1 : pred K1) (C2 : pred K2) (V : Type). -Variables (Uf : @union_map K1 C1 K2) (Ug : @union_map K2 C2 V) (U : @union_map K1 C1 V). +Variables Uf : union_map K1 C1 K2. +Variables Ug : union_map K2 C2 V. +Variables U : union_map K1 C1 V. Implicit Types (f : Uf) (g : Ug). Definition um_comp g f : U := @@ -6328,7 +6509,7 @@ End MapComposition. Section AllDefLemmas. Variables (K : ordType) (C : pred K) (V : Type). -Variables (U : @union_map K C V) (P : K -> V -> Prop). +Variables (U : union_map K C V) (P : K -> V -> Prop). Implicit Types (k : K) (v : V) (f : U). Definition um_all f := forall k v, (k, v) \In f -> P k v. @@ -6393,7 +6574,7 @@ Hint Resolve umall_undef umall0 : core. (* decidable um_all *) Section MapAllDecidable. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Implicit Types (f : U) (p : pred (K*V)). Definition um_allb p f := um_count p f == size (dom f). @@ -6405,28 +6586,19 @@ apply/(equivP idP); split=>[/eqP | H]. by apply/eqP; rewrite umcnt_memT=>k v; apply: H. Qed. -Lemma umallb_is_pcm_morph p : pcm_morph_axiom relT (um_allb p). -Proof. -rewrite /um_allb; split=>[|x y W _]; first by rewrite umcnt0 dom0. -split=>//; apply/idP/idP. -- by move/umallbP=>H; apply/andP; split; apply/umallbP=>k X; - apply: H; [apply: InL | apply: InR]. -case/andP=>/umallbP X1 /umallbP X2; apply/umallbP=>k. -by case/InUn; [apply: X1 | apply: X2]. -Qed. - -HB.instance Definition _ p := - isPCM_morphism.Build U bool (um_allb p) (umallb_is_pcm_morph p). -HB.instance Definition _ p := - isFull_PCM_morphism.Build U bool (um_allb p) (fun x y => erefl). - Lemma umallb0 p : um_allb p Unit. -Proof. exact: pfunit. Qed. +Proof. by rewrite /um_allb umcnt0 dom0. Qed. Lemma umallbUn p f1 f2 : valid (f1 \+ f2) -> um_allb p (f1 \+ f2) = um_allb p f1 && um_allb p f2. -Proof. exact: pfjoinT. Qed. +Proof. +move=>W; apply/idP/idP. +- by move/umallbP=>H; apply/andP; split; apply/umallbP=>k X; + apply: H; [apply: InL | apply: InR]. +case/andP=>/umallbP X1 /umallbP X2; apply/umallbP=>k. +by case/InUn; [apply: X1 | apply: X2]. +Qed. (* bool isn't tpcm, so we can't declare umallb tpcm morphism *) (* however, we can prove some properties about under *) @@ -6447,7 +6619,7 @@ Lemma umallbU p k v f : um_allb p (upd k v f) = p (k, v) && um_allb p (free f k). Proof. rewrite validU=>/andP [W1 W2]; rewrite upd_eta // umallbPtUn //. -by rewrite validPtUn W1 validF W2 domF inE eq_refl. +by rewrite validPtUn W1 validF W2 domF eqxx. Qed. Lemma umallbF p k f : um_allb p f -> um_allb p (free f k). @@ -6464,7 +6636,7 @@ End MapAllDecidable. (* values of equal keys in both maps. *) Section BinaryMapAll. -Variables (K : ordType) (C : pred K) (V : Type) (U : @union_map K C V). +Variables (K : ordType) (C : pred K) (V : Type) (U : union_map K C V). Variables (P : V -> V -> Prop). Implicit Types (k : K) (v : V) (f : U). @@ -6697,7 +6869,7 @@ End BinaryMapAll. Section BigOpsUM. Variables (K : ordType) (C : pred K) (T : Type). -Variables (U : @union_map K C T). +Variables (U : union_map K C T). Variables (I : Type) (f : I -> U). Lemma big_domUn (xs : seq I) : @@ -6831,7 +7003,7 @@ Qed. (* if xs is domain of some map *) -Lemma bigD1FE (k : K) (F : K -> U) (g : U) : +Lemma bigD1FE (V: pcm) (k : K) (F : K -> V) (g : U) : \big[join/Unit]_(i <- dom g) F i = if k \in dom g then F k \+ \big[join/Unit]_(i <- dom (free g k)) F i @@ -6841,34 +7013,43 @@ case: ifP=>D; last by rewrite freeND // (negbT D). rewrite (bigD1_seq k) //= -big_filter (_ : filter _ _ = dom (free g k)) //. apply/ord_sorted_eq; first by rewrite sorted_filter. - by rewrite sorted_dom. -by move=>z; rewrite mem_filter domF inE eq_sym; case: (k =P z). +by move=>z; rewrite mem_filter domF. Qed. -Lemma bigPtUnE (x : K) (a : T) (g : U) (F : K -> U) : +Lemma bigPtUnE (V : pcm) (x : K) (a : T) (g : U) (F : K -> V) : \big[join/Unit]_(i <- dom (pts x a \+ g)) F i = if valid (pts x a \+ g) then F x \+ \big[join/Unit]_(i <- dom g) F i else Unit. Proof. rewrite (bigD1FE x) domPtUnE. -case: (normalP (pts x a \+ g))=>[->|V]. +case: (normalP (pts x a \+ g))=>[->|W]. - by rewrite free_undef dom_undef big_nil. by rewrite freePtUn. Qed. -Lemma bigPtUn (x : K) (a : T) (g : U) (F : K -> U) : +Lemma bigPtUn (V : pcm) (x : K) (a : T) (g : U) (F : K -> V) : valid (pts x a \+ g) -> \big[join/Unit]_(i <- dom (pts x a \+ g)) F i = F x \+ \big[join/Unit]_(i <- dom g) F i. -Proof. by move=>V; rewrite bigPtUnE V. Qed. +Proof. by move=>W; rewrite bigPtUnE W. Qed. -Lemma bigDUE (x : K) (a : T) (g : U) (F : K -> U) : +Lemma bigDUE (V : pcm) (x : K) (a : T) (g : U) (F : K -> V) : \big[join/Unit]_(i <- dom (upd x a g)) F i = if C x && valid g then F x \+ \big[join/Unit]_(i <- dom (free g x)) F i else Unit. Proof. -by rewrite (upd_eta x) bigPtUnE validPtUn validF domF inE eqxx andbT. +by rewrite (upd_eta x) bigPtUnE validPtUn validF domF eqxx andbT. +Qed. + +Lemma big_assocs_dom (V : tpcm) (F : K * T -> V) (g : U): + \big[join/Unit]_(x <- assocs g) F x = + \big[join/Unit]_(x <- dom g) + if find x g is Some v then F (x, v) else undef. +Proof. +rewrite assocs_dom big_map. +by apply: eq_Bigr=>-[x v] /In_assocs/In_find ->. Qed. End BigOpsUM. @@ -6880,7 +7061,7 @@ Prenex Implicits big_find_someX big_find_someXP bigIn bigInD bigInX bigInXP. (* big validity lemma *) Section BigOpsUMEq. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Variables (I : eqType) (f : I -> U). Lemma big_validP (xs : seq I) : @@ -6924,7 +7105,7 @@ Qed. End BigOpsUMEq. Section BigCatSeqUM. -Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T). +Variables (K : ordType) (C : pred K) (T : Type) (U : union_map K C T). Variables (I : eqType) (g : I -> U). Lemma big_valid_dom_seq (xs : seq I) : @@ -6961,7 +7142,7 @@ Proof. by move=>x; rewrite big_valid_dom_seq. Qed. End BigCatSeqUM. -Lemma bigPt_valid (K : ordType) (C : pred K) T (U : @union_map K C T) +Lemma bigPt_valid (K : ordType) (C : pred K) T (U : union_map K C T) (g : U) (F : K -> T) : valid (\big[join/Unit]_(i <- dom g) pts i (F i) : U). Proof. @@ -6973,7 +7154,7 @@ Qed. Section OMapBig. Variables (K : ordType) (C : pred K) (T T' : Type). -Variables (U : @union_map K C T) (U' : @union_map K C T'). +Variables (U : union_map K C T) (U' : union_map K C T'). Variables (I : Type) (f : I -> U). Lemma big_omapVUn (a : K * T -> option T') ts :