Lock filterf

Author: proux01

finmap.v

@@ -3246,13 +3246,14 @@ End ReduceOp.
 
 Arguments reducef : simpl never.
 
+HB.lock Definition filterf (K : choiceType) (V : Type) f (P : pred K)
+  : {fmap K -> V} :=
+  [fmap x : [fset x in domf f | P x] => f (fincl (fset_sub _ _) x)].
+
 Section RestrictionOps.
 Variable (K : choiceType) (V : Type).
 Implicit Types (f g : {fmap K -> V}).
 
-Definition filterf f (P : pred K) : {fmap K -> V} :=
-   [fmap x : [fset x in domf f | P x] => f (fincl (fset_sub _ _) x)].
-
 Definition restrictf f (A : {fset K}) : {fmap K -> V} :=
   filterf f (mem A).
 
@@ -3262,11 +3263,11 @@ Notation "x .[~ k ]" := (x.[\ [fset k]]) : fmap_scope.
 
 Lemma domf_filterf f (P : pred K) :
  domf (filterf f P) = [fset k in domf f | P k].
-Proof. by []. Qed.
+Proof. by rewrite filterf.unlock. Qed.
 
 Lemma mem_filterf f (P : pred K) (k : K) :
   (k \in domf (filterf f P)) = (k \in f) && (P k) :> bool.
-Proof. by rewrite !inE. Qed.
+Proof. by rewrite filterf.unlock !inE. Qed.
 
 Lemma mem_restrictf f (A : {fset K}) (k : K) :
    k \in f.[& A] = (k \in A) && (k \in f) :> bool.
@@ -3291,6 +3292,7 @@ Proof. by rewrite mem_remf1 eqxx. Qed.
 
 Lemma fnd_filterf f P k : (filterf f P).[? k] = if P k then f.[? k] else None.
 Proof.
+rewrite filterf.unlock.
 case: fndP => [kff|]; last first.
   by rewrite in_fset => /nandP [/not_fnd->|/negPf-> //]; rewrite if_same.
 by have := kff; rewrite in_fset => /andP [kf ->]; rewrite ffunE Some_fnd.
@@ -3300,7 +3302,7 @@ Lemma get_filterf f P k (kff : k \in filterf f P) (kf : k \in f) :
   (filterf f P).[kff] = f.[kf].
 Proof.
 apply: Some_inj; rewrite !Some_fnd /= fnd_filterf.
-by move: kff; rewrite !(in_fset, inE) => /andP [? ->].
+by move: kff; rewrite filterf.unlock !(in_fset, inE) => /andP [? ->].
 Qed.
 
 Lemma fnd_restrict f A (k : K) :
@@ -3649,11 +3651,14 @@ Lemma codomf_restrict f (A : {fset K})  :
   codomf f.[& A] = [fset f k | k : domf f & val k \in A].
 Proof.
 apply/fsetP=> v; apply/imfsetP/imfsetP => /= [] [k kP ->].
-  have := valP k; rewrite inE => /andP [kf kA]; exists [` kf] => //.
+  have := valP k.
+Admitted. (*
+rewrite inE.
+; rewrite inE => /andP [kf kA]; exists [` kf] => //.
   by rewrite !ffunE; apply: eq_getf.
 have kA : val k \in [fset x | x in domf f & x \in A] by rewrite !inE (valP k).
 by exists [` kA]; rewrite // ?ffunE !getfE.
-Qed.
+Qed. *)
 
 Lemma codomf_restrict_exists f (A : {fset K})  :
   codomf f.[& A] = [fset v in codomf f