Library SSProve.Crypt.package.fmap_extra
From Coq Require Import Utf8.
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect eqtype choice seq ssrfun ssrbool.
Set Warnings "notation-overridden".
From Equations Require Import Equations.
Require Equations.Prop.DepElim.
Set Equations With UIP.
From extructures Require Import ord fset fmap.
#[local] Open Scope fset.
(******************************************************************************)
(* Extra definitions and lemmas about fmap from extructures. *)
(* This file also provides fmap_solve, which automates proofs of the defs. *)
(* below using auto based on the hint database fmap_solve_db. fmap_solve has *)
(* some support for symbolic terms, but generally does not deconstruct *)
(* assumptions in the context. More hints may be added to extend the solver. *)
(* Definitions: *)
(* fhas m kv == the key-value pair kv is present in m *)
(* fsubmap m m' == m is a submap of m' i.e. when m has value v at *)
(* key k, then m' has value v at key k. *)
(* fcompat m m' == if both maps define a key it has the same value *)
(* fseparate m m' == maps m and m' define a disjoint set of keys. *)
(* Separation of maps implies compatability. *)
(******************************************************************************)
Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.
(* Note that fsubmap is defined into Prop unlike other extructures operators.
A bool definition would require S to be an eqType, which would make it
hard to have maps into e.g. Type or choiceType. *)
Definition fsubmap {T : ordType} {S} (m m' : {fmap T → S}) : Prop
:= unionm m m' = m'.
Definition fhas {T : ordType} {S} (m : {fmap T → S}) kv
:= let '(k, v) := kv in (m k = Some v).
Lemma fhas_fsubmap {T : ordType} {S} (m m' : {fmap T → S})
: (∀ kv, fhas m kv → fhas m' kv) ↔ fsubmap m m'.
Proof.
split.
- intros H.
apply eq_fmap ⇒ t.
rewrite unionmE.
destruct (m t) eqn:E ⇒ //.
specialize (H (t, s) E).
rewrite H //.
- intros H [t s] H'.
rewrite -H //=.
rewrite unionmE H' //=.
Qed.
Lemma fsubmap_fhas {T : ordType} {S} (m m' : {fmap T → S}) kv
: fsubmap m m' → fhas m kv → fhas m' kv.
Proof. rewrite -fhas_fsubmap. auto. Qed.
Definition fcompat {T : ordType} {S} (m m' : {fmap T → S}) :=
unionm m m' = unionm m' m.
Lemma fsubmapUl {T : ordType} {S} (m m' : {fmap T → S}) :
fsubmap m (unionm m m').
Proof.
apply eq_fmap ⇒ t.
rewrite 2!unionmE.
destruct (m t), (m' t) ⇒ //.
Qed.
Lemma fsubmapUr {T : ordType} {S} (m m' : {fmap T → S}) :
fcompat m m' → fsubmap m' (unionm m m').
Proof.
move⇒ →.
apply eq_fmap ⇒ t.
rewrite 2!unionmE.
destruct (m t), (m' t) ⇒ //.
Qed.
Lemma fsubmap_trans {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m m' → fsubmap m' m'' → fsubmap m m''.
Proof.
intros H H'.
apply eq_fmap ⇒ t.
rewrite -{2}H' -H -unionmA H' //.
Qed.
Lemma fsubmapUl_trans {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m m' → fsubmap m (unionm m' m'').
Proof.
intros H. eapply fsubmap_trans;
[ apply H | apply fsubmapUl ].
Qed.
Lemma fsubmapUr_trans {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fcompat m' m'' → fsubmap m m'' → fsubmap m (unionm m' m'').
Proof.
intros H H'. eapply fsubmap_trans;
[ apply H' | apply fsubmapUr, H ].
Qed.
Lemma fsubUmap {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m m'' → fsubmap m' m'' → fsubmap (unionm m m') m''.
Proof.
intros H H'.
rewrite /fsubmap -unionmA H' H //.
Qed.
Lemma fsub0map {T : ordType} {S} (m : {fmap T → S}) : fsubmap emptym m.
Proof. rewrite /fsubmap union0m //. Qed.
Lemma fsubmap_fcompat {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m' m → fsubmap m'' m → fcompat m' m''.
Proof.
intros H H'.
apply eq_fmap in H, H'.
apply eq_fmap ⇒ t.
specialize (H t).
rewrite unionmE in H.
specialize (H' t).
rewrite unionmE in H'.
rewrite 2!unionmE.
destruct (m' t), (m'' t) ⇒ //.
rewrite H H' //.
Qed.
Lemma fhas_in {T : ordType} {S} (m : {fmap T → S}) ts
: fhas m ts → ts.1 \in domm m.
Proof.
move: ts ⇒ [t s] H.
apply /dommP.
by ∃ s.
Qed.
Lemma fhas_empty {T : ordType} {S} k : ¬ fhas (@emptym T S) k.
Proof. by destruct k. Qed.
Lemma fhas_set {T : ordType} {S} k v (m : {fmap T → S}) :
fhas (setm m k v) (k, v).
Proof. rewrite //= setmE eq_refl //. Qed.
Lemma fhas_set_next {T : ordType} {S} (m : {fmap T → S}) k k' v v' :
k ≠ k' → fhas m (k, v) → fhas (setm m k' v') (k, v).
Proof.
move⇒ /eqP H H'.
rewrite //= setmE.
destruct (k == k') ⇒ //.
Qed.
Lemma fsubmapxx {T : ordType} {S} (m : {fmap T → S}) : fsubmap m m.
Proof. rewrite /fsubmap unionmI //. Qed.
Lemma fsubmap_eq {T : ordType} {S} (m m' : {fmap T → S}) :
fsubmap m m' → fsubmap m' m → m = m'.
Proof.
unfold fsubmap.
intros H H'.
rewrite -H -{1}H'.
eapply fsubmap_fcompat.
1: apply H'.
apply fsubmapxx.
Qed.
Lemma fhas_set_case {T : ordType} {S} x y (m : {fmap T → S}) :
fhas (setm m x.1 x.2) y → (x = y) ∨ fhas m y.
Proof.
move: x y ⇒ [k v] [k' v'] H.
rewrite /fhas //= setmE in H.
destruct (k' == k) eqn:E.
- left.
move: E ⇒ /eqP → {k'}.
by noconf H.
- by right.
Qed.
Lemma fhas_union {S : ordType} {T} m m' (k : S) (v : T)
: fhas (unionm m m') (k, v)
→ fhas m (k, v) ∨ (k \notin domm m ∧ fhas m' (k, v)).
Proof.
rewrite /fhas unionmE.
destruct (m k) eqn:E ⇒ //=; auto.
intros H; right; split; try done.
by apply /dommPn.
Qed.
Lemma fhas_union_l {S : ordType} {T} m m' (k : S) (v : T)
: fhas m (k, v) → fhas (unionm m m') (k, v).
Proof.
rewrite /fhas unionmE.
destruct (m k) ⇒ //=; auto.
Qed.
Lemma fhas_union_r {S : ordType} {T} m m' (k : S) (v : T)
: k \notin domm m → fhas m' (k, v) → fhas (unionm m m') (k, v).
Proof.
move⇒ /dommPn H1 H2.
rewrite /fhas unionmE H1 //.
Qed.
(* Tactics *)
Ltac fmap_invert H :=
(by apply fhas_empty in H) ||
( let x := fresh "x" in
apply fhas_set_case in H ;
destruct H as [x|H]; [ noconf x | fmap_invert H ]
).
Create HintDb fmap_solve_db.
#[export] Hint Extern 2 (fhas ?m ?k) ⇒
apply fhas_set
: fmap_solve_db.
#[export] Hint Extern 3 (fhas ?m ?k) ⇒
apply fhas_set_next; [ done |]
: fmap_solve_db.
#[export] Hint Resolve fsubmapUl_trans fsubmapUr_trans
: fmap_solve_db.
#[export] Hint Extern 1 (fcompat ?m ?m') ⇒
reflexivity
: fmap_solve_db.
Hint Extern 1 (fsubmap ?m ?m') ⇒
apply fsubmapxx
: fmap_solve_db.
Ltac fmap_solve :=
typeclasses eauto with fmap_solve_db.
Definition fcompat11 {T : ordType} {S} (x x' : T × S)
:= x.1 ≠ x'.1 ∨ x.2 = x'.2.
Lemma fcompat0m {T : ordType} {S} (m : {fmap T → S})
: fcompat emptym m.
Proof. rewrite /fcompat unionm0 //. Qed.
Lemma fcompatm0 {T : ordType} {S} (m : {fmap T → S})
: fcompat m emptym.
Proof. rewrite /fcompat unionm0 //. Qed.
Lemma fcompat11_swap {T : ordType} {S} (x y : T × S) m
: fcompat11 x y
→ setm (setm m y.1 y.2) x.1 x.2 = setm (setm m x.1 x.2) y.1 y.2.
Proof.
intros [H|H].
- rewrite setmC //.
rewrite eq_sym; by apply /eqP.
- destruct (y.1 == x.1) eqn:E.
+ move: E H ⇒ /eqP.
destruct x, y ⇒ //= H H'.
subst. rewrite setmI // setmE eq_refl //.
+ rewrite setmC // E //.
Qed.
Lemma fcompat_cons1 {T : ordType} {S} (x : T × S) y ys
: fcompat11 x y
→ fcompat [fmap x] (mkfmap ys)
→ fcompat [fmap x] (mkfmap (y :: ys)).
Proof.
intros H H'.
rewrite /fcompat //= -setm_union union0m.
rewrite -setm_union -H'.
rewrite (fcompat11_swap _ _ _ H) //.
Qed.
Lemma fcompat_cons {T : ordType} {S} (x x' : T × S) xs ys
: fcompat [fmap x] (mkfmap ys)
→ fcompat (mkfmap (x' :: xs)) (mkfmap ys)
→ fcompat (mkfmap (x :: x' :: xs)) (mkfmap ys).
Proof.
intros H H'.
rewrite /fcompat //= -setm_union H'.
rewrite /fcompat -setm_union union0m in H.
rewrite setm_union H -unionmA //.
Qed.
Hint Extern 1 (fcompat11 ?m ?m') ⇒
(by left) || (by right)
: fmap_solve_db.
Hint Resolve fcompat_cons1 fcompat_cons fcompatm0 fcompat0m : fmap_solve_db.
Lemma union_fcompat {T : ordType} {S} (m m' m'' : {fmap T → S})
: fcompat m m''
→ fcompat m' m''
→ fcompat (unionm m m') m''.
Proof.
intros H H'.
rewrite /fcompat unionmA -H -unionmA H' unionmA //.
Qed.
Lemma fcompat_union {T : ordType} {S} (m m' m'' : {fmap T → S})
: fcompat m m'
→ fcompat m m''
→ fcompat m (unionm m' m'').
Proof.
intros H H'.
rewrite /fcompat unionmA H -unionmA H' unionmA //.
Qed.
Hint Resolve union_fcompat fcompat_union : fmap_solve_db.
Lemma fsubmap_set {T : ordType} {S} (k : T) (v : S) m m'
: fhas m' (k, v)
→ fsubmap m m'
→ fsubmap (setm m k v) m'.
Proof.
intros H H'.
rewrite /fsubmap -setm_union H' setmI //.
Qed.
Hint Resolve fsub0map fsubUmap fsubmap_set : fmap_solve_db.
Inductive fseparate {T : ordType} {S S' : Type}
(m : {fmap T → S}) (m' : {fmap T → S'}) :=
| fsep : domm m :#: domm m' → fseparate m m'.
Lemma fseparateUl {T : ordType} {S S' : Type}
(m m' : {fmap T → S}) (m'' : {fmap T → S'})
: fseparate m m'' → fseparate m' m'' → fseparate (unionm m m') m''.
Proof.
intros [H] [H'].
apply fsep.
rewrite domm_union fdisjointUl H H' //.
Qed.
Lemma fseparateUr {T : ordType} {S S'}
(m : {fmap T → S}) (m' m'' : {fmap T → S'})
: fseparate m m' → fseparate m m'' → fseparate m (unionm m' m'').
Proof.
intros [H] [H'].
apply fsep.
rewrite domm_union fdisjointUr H H' //.
Qed.
Lemma fseparate_set {T : ordType} {S S'} (k k' : T) (v v' : S)
(m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate (setm emptym k v) m'
→ fseparate (setm m k' v') m'
→ fseparate (setm (setm m k' v') k v) m'.
Proof.
intros [H] [H'].
apply fsep.
rewrite domm_set domm0 fsetU0 in H.
rewrite domm_set fdisjointUl H' H //.
Qed.
Lemma fseparate_set1 {T : ordType} {S S'} (k k' : T)
(v : S) (v' : S') (m' : {fmap T → S'})
: k ≠ k'
→ fseparate (setm emptym k v) m'
→ fseparate (setm emptym k v) (setm m' k' v').
Proof.
intros H [H'].
apply fsep.
rewrite domm_set domm0 fsetU0 in H'.
rewrite 2!domm_set domm0 fsetU0 fdisjointUr H'.
apply /andP; split ⇒ //.
apply /fdisjointP ⇒ x /fset1P → {x}.
apply /negP ⇒ /fset1P //.
Qed.
Lemma fseparate0m {T : ordType} {S S'} (m : {fmap T → S'})
: fseparate (@emptym T S) m.
Proof. apply fsep. rewrite domm0 fdisjoint0s //. Qed.
Lemma fseparatem0 {T : ordType} {S S'} (m : {fmap T → S})
: fseparate m (@emptym T S').
Proof. apply fsep. rewrite domm0 fdisjoints0 //. Qed.
Lemma fseparateE {T : ordType} {S S'} (m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → domm m :#: domm m'.
Proof. by intros [?]. Qed.
Lemma fseparateMl {T : ordType} {S S' S'' : Type}
(f : S → S') (m : {fmap T → S}) (m' : {fmap T → S''})
: fseparate m m' → fseparate (mapm f m) m'.
Proof. intros [H]. apply fsep. rewrite domm_map //. Qed.
Lemma fseparateMil {T : ordType} {S S' S'' : Type}
(f : T → S → S') (m : {fmap T → S}) (m' : {fmap T → S''})
: fseparate m m' → fseparate (mapim f m) m'.
Proof. intros [H]. apply fsep. rewrite domm_mapi //. Qed.
Lemma fseparateMr {T : ordType} {S S' S'' : Type}
(f : S' → S'') (m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → fseparate m (mapm f m').
Proof. intros [H]. apply fsep. rewrite domm_map //. Qed.
Lemma fseparateMir {T : ordType} {S S' S'' : Type}
(f : T → S' → S'') (m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → fseparate m (mapim f m').
Proof. intros [H]. apply fsep. rewrite domm_mapi //. Qed.
Lemma notin_fseparate {T : ordType} {S S'} (x : T × S) (m : {fmap T → S'})
: fseparate [fmap x] m → x.1 \notin domm m.
Proof.
move⇒ [] /fdisjointP H.
apply H.
rewrite domm_set in_fsetU1 eq_refl //.
Qed.
Hint Extern 2 (?x ≠ ?y) ⇒
done : fmap_solve_db.
Hint Resolve fseparateE fseparate0m fseparatem0 : fmap_solve_db.
Hint Resolve fseparateUl fseparateUr : fmap_solve_db.
Hint Resolve fseparateMl fseparateMr : fmap_solve_db.
Hint Resolve fseparateMil fseparateMir : fmap_solve_db.
Hint Resolve notin_fseparate fseparate_set fseparate_set1 : fmap_solve_db.
(* case over booleans *)
Lemma fsubmap_case_l {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fsubmap m m'' → fsubmap m' m'' → fsubmap (if b then m else m') m''.
Proof. by move: b ⇒ []. Qed.
Lemma fsubmap_case_r {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fsubmap m m' → fsubmap m m'' → fsubmap m (if b then m' else m'').
Proof. by move: b ⇒ []. Qed.
Hint Resolve fsubmap_case_l fsubmap_case_r : fmap_solve_db.
Lemma fcompat_case_l {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fcompat m m'' → fcompat m' m'' → fcompat (if b then m else m') m''.
Proof. by move: b ⇒ []. Qed.
Lemma fcompat_case_r {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fcompat m m' → fcompat m m'' → fcompat m (if b then m' else m'').
Proof. by move: b ⇒ []. Qed.
Hint Resolve fcompat_case_l fcompat_case_r : fmap_solve_db.
Lemma fseparate_case_l {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fseparate m m'' → fseparate m' m'' → fseparate (if b then m else m') m''.
Proof. by move: b ⇒ []. Qed.
Lemma fseparate_case_r {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fseparate m m' → fseparate m m'' → fseparate m (if b then m' else m'').
Proof. by move: b ⇒ []. Qed.
Hint Resolve fseparate_case_l fseparate_case_r : fmap_solve_db.
Lemma fseparate_compat {T : ordType} {S : Type} (m m' : {fmap T → S})
: fseparate m m' → fcompat m m'.
Proof. intros [H]. rewrite /fcompat unionmC //. Qed.
(* danger of two solution paths? (more expensive search) *)
Hint Resolve fseparate_compat : fmap_solve_db.
Lemma fcompatC {T : ordType} {S : Type} (m m' : {fmap T → S})
: fcompat m m' → fcompat m' m.
Proof. done. Qed.
Lemma fseparateC {T : ordType} {S S' : Type}
(m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → fseparate m' m.
Proof. intros [H]. apply fsep. rewrite fdisjointC //. Qed.
Lemma fseparate_trans_l {T : ordType} {S S' : Type}
(m m'' : {fmap T → S}) (m' : {fmap T → S'})
: fsubmap m m'' → fseparate m'' m' → fseparate m m'.
Proof.
unfold fsubmap.
intros H [H'].
apply fsep.
eapply (fdisjointSl _ H').
Unshelve.
rewrite -H domm_union fsubsetUl //.
Qed.
Lemma fseparate_trans_r {T : ordType} {S S' : Type}
(m : {fmap T → S}) (m' m'' : {fmap T → S'})
: fsubmap m' m'' → fseparate m m'' → fseparate m m'.
Proof.
unfold fsubmap.
intros H [H'].
apply fsep.
rewrite fdisjointC in H'.
rewrite fdisjointC.
eapply (fdisjointSl _ H').
Unshelve.
rewrite -H domm_union fsubsetUl //.
Qed.
Hint Extern 4 (fcompat _ _) ⇒
apply fcompatC; done : fmap_solve_db.
Hint Extern 4 (fseparate _ _) ⇒
apply fseparateC; done : fmap_solve_db.
Lemma notin_has_separate {T : ordType} {S : Type} (m m' : {fmap T → S}) (l : T × S)
: fhas m l → fseparate m m' → l.1 \notin domm m'.
Proof.
move⇒ H [H'].
apply fhas_in in H.
apply /fdisjointP; eassumption.
Qed.
Hint Extern 4 (is_true (_ \notin _)) ⇒
eapply notin_has_separate; [ eassumption | ] : fmap_solve_db.
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect eqtype choice seq ssrfun ssrbool.
Set Warnings "notation-overridden".
From Equations Require Import Equations.
Require Equations.Prop.DepElim.
Set Equations With UIP.
From extructures Require Import ord fset fmap.
#[local] Open Scope fset.
(******************************************************************************)
(* Extra definitions and lemmas about fmap from extructures. *)
(* This file also provides fmap_solve, which automates proofs of the defs. *)
(* below using auto based on the hint database fmap_solve_db. fmap_solve has *)
(* some support for symbolic terms, but generally does not deconstruct *)
(* assumptions in the context. More hints may be added to extend the solver. *)
(* Definitions: *)
(* fhas m kv == the key-value pair kv is present in m *)
(* fsubmap m m' == m is a submap of m' i.e. when m has value v at *)
(* key k, then m' has value v at key k. *)
(* fcompat m m' == if both maps define a key it has the same value *)
(* fseparate m m' == maps m and m' define a disjoint set of keys. *)
(* Separation of maps implies compatability. *)
(******************************************************************************)
Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.
(* Note that fsubmap is defined into Prop unlike other extructures operators.
A bool definition would require S to be an eqType, which would make it
hard to have maps into e.g. Type or choiceType. *)
Definition fsubmap {T : ordType} {S} (m m' : {fmap T → S}) : Prop
:= unionm m m' = m'.
Definition fhas {T : ordType} {S} (m : {fmap T → S}) kv
:= let '(k, v) := kv in (m k = Some v).
Lemma fhas_fsubmap {T : ordType} {S} (m m' : {fmap T → S})
: (∀ kv, fhas m kv → fhas m' kv) ↔ fsubmap m m'.
Proof.
split.
- intros H.
apply eq_fmap ⇒ t.
rewrite unionmE.
destruct (m t) eqn:E ⇒ //.
specialize (H (t, s) E).
rewrite H //.
- intros H [t s] H'.
rewrite -H //=.
rewrite unionmE H' //=.
Qed.
Lemma fsubmap_fhas {T : ordType} {S} (m m' : {fmap T → S}) kv
: fsubmap m m' → fhas m kv → fhas m' kv.
Proof. rewrite -fhas_fsubmap. auto. Qed.
Definition fcompat {T : ordType} {S} (m m' : {fmap T → S}) :=
unionm m m' = unionm m' m.
Lemma fsubmapUl {T : ordType} {S} (m m' : {fmap T → S}) :
fsubmap m (unionm m m').
Proof.
apply eq_fmap ⇒ t.
rewrite 2!unionmE.
destruct (m t), (m' t) ⇒ //.
Qed.
Lemma fsubmapUr {T : ordType} {S} (m m' : {fmap T → S}) :
fcompat m m' → fsubmap m' (unionm m m').
Proof.
move⇒ →.
apply eq_fmap ⇒ t.
rewrite 2!unionmE.
destruct (m t), (m' t) ⇒ //.
Qed.
Lemma fsubmap_trans {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m m' → fsubmap m' m'' → fsubmap m m''.
Proof.
intros H H'.
apply eq_fmap ⇒ t.
rewrite -{2}H' -H -unionmA H' //.
Qed.
Lemma fsubmapUl_trans {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m m' → fsubmap m (unionm m' m'').
Proof.
intros H. eapply fsubmap_trans;
[ apply H | apply fsubmapUl ].
Qed.
Lemma fsubmapUr_trans {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fcompat m' m'' → fsubmap m m'' → fsubmap m (unionm m' m'').
Proof.
intros H H'. eapply fsubmap_trans;
[ apply H' | apply fsubmapUr, H ].
Qed.
Lemma fsubUmap {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m m'' → fsubmap m' m'' → fsubmap (unionm m m') m''.
Proof.
intros H H'.
rewrite /fsubmap -unionmA H' H //.
Qed.
Lemma fsub0map {T : ordType} {S} (m : {fmap T → S}) : fsubmap emptym m.
Proof. rewrite /fsubmap union0m //. Qed.
Lemma fsubmap_fcompat {T : ordType} {S} (m m' m'' : {fmap T → S}) :
fsubmap m' m → fsubmap m'' m → fcompat m' m''.
Proof.
intros H H'.
apply eq_fmap in H, H'.
apply eq_fmap ⇒ t.
specialize (H t).
rewrite unionmE in H.
specialize (H' t).
rewrite unionmE in H'.
rewrite 2!unionmE.
destruct (m' t), (m'' t) ⇒ //.
rewrite H H' //.
Qed.
Lemma fhas_in {T : ordType} {S} (m : {fmap T → S}) ts
: fhas m ts → ts.1 \in domm m.
Proof.
move: ts ⇒ [t s] H.
apply /dommP.
by ∃ s.
Qed.
Lemma fhas_empty {T : ordType} {S} k : ¬ fhas (@emptym T S) k.
Proof. by destruct k. Qed.
Lemma fhas_set {T : ordType} {S} k v (m : {fmap T → S}) :
fhas (setm m k v) (k, v).
Proof. rewrite //= setmE eq_refl //. Qed.
Lemma fhas_set_next {T : ordType} {S} (m : {fmap T → S}) k k' v v' :
k ≠ k' → fhas m (k, v) → fhas (setm m k' v') (k, v).
Proof.
move⇒ /eqP H H'.
rewrite //= setmE.
destruct (k == k') ⇒ //.
Qed.
Lemma fsubmapxx {T : ordType} {S} (m : {fmap T → S}) : fsubmap m m.
Proof. rewrite /fsubmap unionmI //. Qed.
Lemma fsubmap_eq {T : ordType} {S} (m m' : {fmap T → S}) :
fsubmap m m' → fsubmap m' m → m = m'.
Proof.
unfold fsubmap.
intros H H'.
rewrite -H -{1}H'.
eapply fsubmap_fcompat.
1: apply H'.
apply fsubmapxx.
Qed.
Lemma fhas_set_case {T : ordType} {S} x y (m : {fmap T → S}) :
fhas (setm m x.1 x.2) y → (x = y) ∨ fhas m y.
Proof.
move: x y ⇒ [k v] [k' v'] H.
rewrite /fhas //= setmE in H.
destruct (k' == k) eqn:E.
- left.
move: E ⇒ /eqP → {k'}.
by noconf H.
- by right.
Qed.
Lemma fhas_union {S : ordType} {T} m m' (k : S) (v : T)
: fhas (unionm m m') (k, v)
→ fhas m (k, v) ∨ (k \notin domm m ∧ fhas m' (k, v)).
Proof.
rewrite /fhas unionmE.
destruct (m k) eqn:E ⇒ //=; auto.
intros H; right; split; try done.
by apply /dommPn.
Qed.
Lemma fhas_union_l {S : ordType} {T} m m' (k : S) (v : T)
: fhas m (k, v) → fhas (unionm m m') (k, v).
Proof.
rewrite /fhas unionmE.
destruct (m k) ⇒ //=; auto.
Qed.
Lemma fhas_union_r {S : ordType} {T} m m' (k : S) (v : T)
: k \notin domm m → fhas m' (k, v) → fhas (unionm m m') (k, v).
Proof.
move⇒ /dommPn H1 H2.
rewrite /fhas unionmE H1 //.
Qed.
(* Tactics *)
Ltac fmap_invert H :=
(by apply fhas_empty in H) ||
( let x := fresh "x" in
apply fhas_set_case in H ;
destruct H as [x|H]; [ noconf x | fmap_invert H ]
).
Create HintDb fmap_solve_db.
#[export] Hint Extern 2 (fhas ?m ?k) ⇒
apply fhas_set
: fmap_solve_db.
#[export] Hint Extern 3 (fhas ?m ?k) ⇒
apply fhas_set_next; [ done |]
: fmap_solve_db.
#[export] Hint Resolve fsubmapUl_trans fsubmapUr_trans
: fmap_solve_db.
#[export] Hint Extern 1 (fcompat ?m ?m') ⇒
reflexivity
: fmap_solve_db.
Hint Extern 1 (fsubmap ?m ?m') ⇒
apply fsubmapxx
: fmap_solve_db.
Ltac fmap_solve :=
typeclasses eauto with fmap_solve_db.
Definition fcompat11 {T : ordType} {S} (x x' : T × S)
:= x.1 ≠ x'.1 ∨ x.2 = x'.2.
Lemma fcompat0m {T : ordType} {S} (m : {fmap T → S})
: fcompat emptym m.
Proof. rewrite /fcompat unionm0 //. Qed.
Lemma fcompatm0 {T : ordType} {S} (m : {fmap T → S})
: fcompat m emptym.
Proof. rewrite /fcompat unionm0 //. Qed.
Lemma fcompat11_swap {T : ordType} {S} (x y : T × S) m
: fcompat11 x y
→ setm (setm m y.1 y.2) x.1 x.2 = setm (setm m x.1 x.2) y.1 y.2.
Proof.
intros [H|H].
- rewrite setmC //.
rewrite eq_sym; by apply /eqP.
- destruct (y.1 == x.1) eqn:E.
+ move: E H ⇒ /eqP.
destruct x, y ⇒ //= H H'.
subst. rewrite setmI // setmE eq_refl //.
+ rewrite setmC // E //.
Qed.
Lemma fcompat_cons1 {T : ordType} {S} (x : T × S) y ys
: fcompat11 x y
→ fcompat [fmap x] (mkfmap ys)
→ fcompat [fmap x] (mkfmap (y :: ys)).
Proof.
intros H H'.
rewrite /fcompat //= -setm_union union0m.
rewrite -setm_union -H'.
rewrite (fcompat11_swap _ _ _ H) //.
Qed.
Lemma fcompat_cons {T : ordType} {S} (x x' : T × S) xs ys
: fcompat [fmap x] (mkfmap ys)
→ fcompat (mkfmap (x' :: xs)) (mkfmap ys)
→ fcompat (mkfmap (x :: x' :: xs)) (mkfmap ys).
Proof.
intros H H'.
rewrite /fcompat //= -setm_union H'.
rewrite /fcompat -setm_union union0m in H.
rewrite setm_union H -unionmA //.
Qed.
Hint Extern 1 (fcompat11 ?m ?m') ⇒
(by left) || (by right)
: fmap_solve_db.
Hint Resolve fcompat_cons1 fcompat_cons fcompatm0 fcompat0m : fmap_solve_db.
Lemma union_fcompat {T : ordType} {S} (m m' m'' : {fmap T → S})
: fcompat m m''
→ fcompat m' m''
→ fcompat (unionm m m') m''.
Proof.
intros H H'.
rewrite /fcompat unionmA -H -unionmA H' unionmA //.
Qed.
Lemma fcompat_union {T : ordType} {S} (m m' m'' : {fmap T → S})
: fcompat m m'
→ fcompat m m''
→ fcompat m (unionm m' m'').
Proof.
intros H H'.
rewrite /fcompat unionmA H -unionmA H' unionmA //.
Qed.
Hint Resolve union_fcompat fcompat_union : fmap_solve_db.
Lemma fsubmap_set {T : ordType} {S} (k : T) (v : S) m m'
: fhas m' (k, v)
→ fsubmap m m'
→ fsubmap (setm m k v) m'.
Proof.
intros H H'.
rewrite /fsubmap -setm_union H' setmI //.
Qed.
Hint Resolve fsub0map fsubUmap fsubmap_set : fmap_solve_db.
Inductive fseparate {T : ordType} {S S' : Type}
(m : {fmap T → S}) (m' : {fmap T → S'}) :=
| fsep : domm m :#: domm m' → fseparate m m'.
Lemma fseparateUl {T : ordType} {S S' : Type}
(m m' : {fmap T → S}) (m'' : {fmap T → S'})
: fseparate m m'' → fseparate m' m'' → fseparate (unionm m m') m''.
Proof.
intros [H] [H'].
apply fsep.
rewrite domm_union fdisjointUl H H' //.
Qed.
Lemma fseparateUr {T : ordType} {S S'}
(m : {fmap T → S}) (m' m'' : {fmap T → S'})
: fseparate m m' → fseparate m m'' → fseparate m (unionm m' m'').
Proof.
intros [H] [H'].
apply fsep.
rewrite domm_union fdisjointUr H H' //.
Qed.
Lemma fseparate_set {T : ordType} {S S'} (k k' : T) (v v' : S)
(m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate (setm emptym k v) m'
→ fseparate (setm m k' v') m'
→ fseparate (setm (setm m k' v') k v) m'.
Proof.
intros [H] [H'].
apply fsep.
rewrite domm_set domm0 fsetU0 in H.
rewrite domm_set fdisjointUl H' H //.
Qed.
Lemma fseparate_set1 {T : ordType} {S S'} (k k' : T)
(v : S) (v' : S') (m' : {fmap T → S'})
: k ≠ k'
→ fseparate (setm emptym k v) m'
→ fseparate (setm emptym k v) (setm m' k' v').
Proof.
intros H [H'].
apply fsep.
rewrite domm_set domm0 fsetU0 in H'.
rewrite 2!domm_set domm0 fsetU0 fdisjointUr H'.
apply /andP; split ⇒ //.
apply /fdisjointP ⇒ x /fset1P → {x}.
apply /negP ⇒ /fset1P //.
Qed.
Lemma fseparate0m {T : ordType} {S S'} (m : {fmap T → S'})
: fseparate (@emptym T S) m.
Proof. apply fsep. rewrite domm0 fdisjoint0s //. Qed.
Lemma fseparatem0 {T : ordType} {S S'} (m : {fmap T → S})
: fseparate m (@emptym T S').
Proof. apply fsep. rewrite domm0 fdisjoints0 //. Qed.
Lemma fseparateE {T : ordType} {S S'} (m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → domm m :#: domm m'.
Proof. by intros [?]. Qed.
Lemma fseparateMl {T : ordType} {S S' S'' : Type}
(f : S → S') (m : {fmap T → S}) (m' : {fmap T → S''})
: fseparate m m' → fseparate (mapm f m) m'.
Proof. intros [H]. apply fsep. rewrite domm_map //. Qed.
Lemma fseparateMil {T : ordType} {S S' S'' : Type}
(f : T → S → S') (m : {fmap T → S}) (m' : {fmap T → S''})
: fseparate m m' → fseparate (mapim f m) m'.
Proof. intros [H]. apply fsep. rewrite domm_mapi //. Qed.
Lemma fseparateMr {T : ordType} {S S' S'' : Type}
(f : S' → S'') (m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → fseparate m (mapm f m').
Proof. intros [H]. apply fsep. rewrite domm_map //. Qed.
Lemma fseparateMir {T : ordType} {S S' S'' : Type}
(f : T → S' → S'') (m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → fseparate m (mapim f m').
Proof. intros [H]. apply fsep. rewrite domm_mapi //. Qed.
Lemma notin_fseparate {T : ordType} {S S'} (x : T × S) (m : {fmap T → S'})
: fseparate [fmap x] m → x.1 \notin domm m.
Proof.
move⇒ [] /fdisjointP H.
apply H.
rewrite domm_set in_fsetU1 eq_refl //.
Qed.
Hint Extern 2 (?x ≠ ?y) ⇒
done : fmap_solve_db.
Hint Resolve fseparateE fseparate0m fseparatem0 : fmap_solve_db.
Hint Resolve fseparateUl fseparateUr : fmap_solve_db.
Hint Resolve fseparateMl fseparateMr : fmap_solve_db.
Hint Resolve fseparateMil fseparateMir : fmap_solve_db.
Hint Resolve notin_fseparate fseparate_set fseparate_set1 : fmap_solve_db.
(* case over booleans *)
Lemma fsubmap_case_l {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fsubmap m m'' → fsubmap m' m'' → fsubmap (if b then m else m') m''.
Proof. by move: b ⇒ []. Qed.
Lemma fsubmap_case_r {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fsubmap m m' → fsubmap m m'' → fsubmap m (if b then m' else m'').
Proof. by move: b ⇒ []. Qed.
Hint Resolve fsubmap_case_l fsubmap_case_r : fmap_solve_db.
Lemma fcompat_case_l {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fcompat m m'' → fcompat m' m'' → fcompat (if b then m else m') m''.
Proof. by move: b ⇒ []. Qed.
Lemma fcompat_case_r {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fcompat m m' → fcompat m m'' → fcompat m (if b then m' else m'').
Proof. by move: b ⇒ []. Qed.
Hint Resolve fcompat_case_l fcompat_case_r : fmap_solve_db.
Lemma fseparate_case_l {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fseparate m m'' → fseparate m' m'' → fseparate (if b then m else m') m''.
Proof. by move: b ⇒ []. Qed.
Lemma fseparate_case_r {T : ordType} {S : Type} {b : bool} {m m' m'' : {fmap T → S}}
: fseparate m m' → fseparate m m'' → fseparate m (if b then m' else m'').
Proof. by move: b ⇒ []. Qed.
Hint Resolve fseparate_case_l fseparate_case_r : fmap_solve_db.
Lemma fseparate_compat {T : ordType} {S : Type} (m m' : {fmap T → S})
: fseparate m m' → fcompat m m'.
Proof. intros [H]. rewrite /fcompat unionmC //. Qed.
(* danger of two solution paths? (more expensive search) *)
Hint Resolve fseparate_compat : fmap_solve_db.
Lemma fcompatC {T : ordType} {S : Type} (m m' : {fmap T → S})
: fcompat m m' → fcompat m' m.
Proof. done. Qed.
Lemma fseparateC {T : ordType} {S S' : Type}
(m : {fmap T → S}) (m' : {fmap T → S'})
: fseparate m m' → fseparate m' m.
Proof. intros [H]. apply fsep. rewrite fdisjointC //. Qed.
Lemma fseparate_trans_l {T : ordType} {S S' : Type}
(m m'' : {fmap T → S}) (m' : {fmap T → S'})
: fsubmap m m'' → fseparate m'' m' → fseparate m m'.
Proof.
unfold fsubmap.
intros H [H'].
apply fsep.
eapply (fdisjointSl _ H').
Unshelve.
rewrite -H domm_union fsubsetUl //.
Qed.
Lemma fseparate_trans_r {T : ordType} {S S' : Type}
(m : {fmap T → S}) (m' m'' : {fmap T → S'})
: fsubmap m' m'' → fseparate m m'' → fseparate m m'.
Proof.
unfold fsubmap.
intros H [H'].
apply fsep.
rewrite fdisjointC in H'.
rewrite fdisjointC.
eapply (fdisjointSl _ H').
Unshelve.
rewrite -H domm_union fsubsetUl //.
Qed.
Hint Extern 4 (fcompat _ _) ⇒
apply fcompatC; done : fmap_solve_db.
Hint Extern 4 (fseparate _ _) ⇒
apply fseparateC; done : fmap_solve_db.
Lemma notin_has_separate {T : ordType} {S : Type} (m m' : {fmap T → S}) (l : T × S)
: fhas m l → fseparate m m' → l.1 \notin domm m'.
Proof.
move⇒ H [H'].
apply fhas_in in H.
apply /fdisjointP; eassumption.
Qed.
Hint Extern 4 (is_true (_ \notin _)) ⇒
eapply notin_has_separate; [ eassumption | ] : fmap_solve_db.