Remove the use of the phantom type

finmap.v

@@ -147,10 +147,10 @@
 Reserved Notation "A `=P` B" (at level 70, no associativity).
 
 Reserved Notation "f @`[ key ] A" (at level 24, key at level 0).
 Reserved Notation "f @2`[ key ] ( A , B )"
   (at level 24, format "f  @2`[ key ]  ( A ,  B )").
 Reserved Notation "f @` A" (at level 24).
 Reserved Notation "f @2` ( A , B )" (at level 24, format "f  @2`  ( A ,  B )").
 
 (* unary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A ]" (at level 0, E, x at level 99).
@@ -168,9 +168,9 @@
 Reserved Notation "[ 'fset' x 'in' A | P & Q ]" (at level 0, x at level 99).
 
 (* binary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 
 (* keyed parse only *)
@@ -183,11 +183,11 @@
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A & P ]"
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y : B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y 'in' B ]"
   (at level 0, E, x, y at level 99).
@@ -233,7 +233,7 @@
 Reserved Notation "[ 'f' 'set' x 'in' A | P & Q ]"
   (at level 0, x at level 99, format "[ 'f' 'set'  x  'in'  A  |  P  &  Q ]").
 (* binary printing only *)
 Reserved Notation "[ 'f' 'set' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99,
    format "[ '[hv' 'f' 'set'  E '/ '  |  x  'in'  A , '/' y  'in'  B ] ']'").
 
@@ -338,8 +338,11 @@
 Reserved Notation "[ 'f' 'setval' x : A | P & Q ]"
   (at level 0, x at level 99, format "[ 'f' 'setval'  x  :  A  |  P  &  Q ]").
 
-Reserved Notation "{fmap T }" (at level 0, format "{fmap  T }").
+Reserved Notation "{ 'fmap' K -> T }"
+  (at level 0, K at level 98, T at level 99, format "{ 'fmap'  K  ->  T }").
+Reserved Notation "[ 'fmap' 'of' K -> T ]"
+  (at level 0, K at level 98, T at level 99, format "[ 'fmap' 'of'  K  -> T ]").
 Reserved Notation "x .[ k <- v ]"
   (left associativity, format "x .[ k  <-  v ]").
 Reserved Notation "x .[~ k ]" (format "x .[~  k ]").
 Reserved Notation "x .[& k ]" (format "x .[&  k ]").
@@ -476,12 +479,14 @@
   _ : canonical_keys enum_fset
 }.
 
+#[deprecated(note="Use finSet instead")]
 Definition finset_of (_ : phant K) := finSet.
 
 End Def.
 
+#[warning="-deprecated-reference"]
 Identity Coercion type_of_finset : finset_of >-> finSet.
-Notation "{fset T }" := (@finset_of _ (Phant T)) : type_scope.
+Notation "{fset T }" := (finSet T) : type_scope.
 
 Definition pred_of_finset (K : choiceType)
   (f : finSet K) : pred K := fun k => k \in (enum_fset f).
@@ -547,6 +552,7 @@
 
 End FinTypeSet.
 
+#[warning="-deprecated-reference"]
 Identity Coercion finSet_sub_type : finset_of >-> finSet.
 Coercion fset_sub_type : finSet >-> predArgType.
 #[global] Hint Resolve fsvalP fset_uniq mem_fset_sub_enum : core.
@@ -593,7 +599,7 @@
 
 #[global] Hint Resolve keys_canonical sort_keys_uniq : core.
 
 HB.instance Definition _ K := [isSub for (@enum_fset K)].
 HB.instance Definition _ (K : choiceType) := [Choice of {fset K} by <:].
 
 Section FinPredStruct.
@@ -673,7 +679,7 @@
                             (enum_finpred_uniq p) (enum_finpredE p)).
 
 Definition finpred_of (T : eqType) (pT : predType T) (p : pT)
- (fp : finpred pT) & phantom pT fp : finpred pT := fp.
+  (fp : finpred pT) : finpred pT := fp.
 
 Structure finmempred (T : eqType) := FinMemPred {
   pred_of_finmempred :> mem_pred T;
@@ -692,7 +698,7 @@
 Proof. by case: p => ?[]. Qed.
 
 Definition finmempred_of (T : eqType) (P : pred T)
- (mP : finmempred T) & phantom (mem_pred T) mP : finmempred T := mP.
+ (mP : finmempred T) : finmempred T := mP.
 
 Canonical mem_fin (T : eqType) (pT : predType T) (p : finpred pT) :=
   @FinMemPred  _ (mem p)
@@ -735,22 +741,19 @@
 
 Local Notation imfset_def key :=
   (fun (T K : choiceType) (f : T -> K) (p : finmempred T)
-       of phantom (mem_pred T) p => seq_fset key [seq f x | x <- enum_finmem p]).
+       => seq_fset key [seq f x | x <- enum_finmem p]).
 Local Notation imfset2_def key :=
   (fun (K T1 : choiceType) (T2 : T1 -> choiceType)
        (f : forall x : T1, T2 x -> K)
-       (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x))
-   of phantom (mem_pred T1) p1 & phantom (forall x, mem_pred (T2 x)) p2 =>
+       (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x)) =>
   seq_fset key [seq f x y | x <- enum_finmem p1, y <- enum_finmem (p2 x)]).
 
 Module Type ImfsetSig.
 Parameter imfset : forall (key : unit) (T K : choiceType)
-       (f : T -> K) (p : finmempred T),
-  phantom (mem_pred T) p ->  {fset K}.
+       (f : T -> K) (p : finmempred T), {fset K}.
 Parameter imfset2 : forall (key : unit) (K T1 : choiceType)
        (T2 : T1 -> choiceType)(f : forall x : T1, T2 x -> K)
-       (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x)),
-  phantom (mem_pred T1) p1 -> phantom (forall x, mem_pred (T2 x)) p2 -> {fset K}.
+       (p1 : finmempred T1) (p2 : forall x : T1, finmempred (T2 x)), {fset K}.
 Axiom imfsetE : forall key, imfset key = imfset_def key.
 Axiom imfset2E : forall key, imfset2 key = imfset2_def key.
 End ImfsetSig.
@@ -762,11 +765,8 @@
 Lemma imfset2E key : imfset2 key = imfset2_def key. Proof. by []. Qed.
 End Imfset.
 
-Notation imfset key f p :=
-   (Imfset.imfset key f (Phantom _ (pred_of_finmempred p))).
-Notation imfset2 key f p q :=
-   (Imfset.imfset2 key f (Phantom _ (pred_of_finmempred p))
-                   (Phantom _ (fun x => (pred_of_finmempred (q x))))).
+Notation imfset := Imfset.imfset.
+Notation imfset2 := Imfset.imfset2.
 Canonical imfset_unlock k := Unlockable (Imfset.imfsetE k).
 Canonical imfset2_unlock k := Unlockable (Imfset.imfset2E k).
 
@@ -776,11 +776,9 @@
 Notation "A `!=` B" := (A != B :> {fset _}) (only parsing) : fset_scope.
 Notation "A `=P` B" := (A =P B :> {fset _}) (only parsing) : fset_scope.
 
-Notation "f @`[ key ] A" :=
-  (Imfset.imfset key f (Phantom _ (mem A))) : fset_scope.
+Notation "f @`[ key ] A" := (Imfset.imfset key f (mem A)) : fset_scope.
 Notation "f @2`[ key ] ( A , B )" :=
-   (Imfset.imfset2 key f (Phantom _ (mem A)) (Phantom _ (fun x => (mem (B x)))))
-  : fset_scope.
+  (Imfset.imfset2 key f (mem A) (fun x => (mem (B x)))) : fset_scope.
 
 Fact imfset_key : unit. Proof. exact: tt. Qed.
 
@@ -2984,14 +2982,15 @@
   ffun_of_fmap :> {ffun domf -> V}
 }.
 
+#[deprecated(note="Use finMap instead.")]
 Definition finmap_of (_ : phant (K -> V)) := finMap.
 
 Let T_ (domf : {fset K}) :=  {ffun domf -> V}.
 Local Notation finMap' := {domf : _ & T_ domf}.
 
 End DefMap.
 
-Notation "{fmap T }" := (@finmap_of _ _ (Phant T)) : type_scope.
+Notation "{ 'fmap' K -> T }" := (finMap K T) : type_scope.
 
 Definition pred_of_finmap (K : choiceType) (V : Type)
   (f : {fmap K -> V}) : pred K := mem (domf f).
@@ -3045,7 +3044,8 @@
 Arguments setf : simpl never.
 Arguments fnd : simpl never.
 
-Notation "[ 'fmap' 'of' T ]" := (fmap0 : {fmap T}) (only parsing) : fmap_scope.
+Notation "[ 'fmap' 'of' K -> T ]" :=
+  (fmap0 : {fmap K -> T}) (only parsing) : fmap_scope.
 Notation "[fmap]" := fmap0 : fmap_scope.
 Notation "x .[ k <- v ]" := (setf x k v) : fmap_scope.
 Notation "f .[? k ]" := (fnd f k) : fmap_scope.