move all instance declarations of setoids and metrics together in one place

iris_core.v

@@ -27,25 +27,30 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
 
   Instance Props_BI : ComplBI Props | 0 := _.
   Instance Props_Later : Later Props | 0 := _.
- 
-  
-  (* Benchmark: How large is this type? *)
-  (*Section Benchmark.
-    Local Open Scope mask_scope.
-    Local Open Scope pcm_scope.
-    Local Open Scope bi_scope.
-    Local Open Scope lang_scope.
 
-    Local Instance _bench_expr_type : Setoid expr := discreteType.
-    Local Instance _bench_expr_metr : metric expr := discreteMetric.
-    Local Instance _bench_cmetr : cmetric expr := discreteCMetric.
+  (** Instances for a bunch of types *)
+  Instance state_type : Setoid state := discreteType.
+  Instance state_metr : metric state := discreteMetric.
+  Instance state_cmetr : cmetric state := discreteCMetric.
+
+  (* The equivalence for this is a paremeter *)
+  Instance logR_metr : metric RL.res := discreteMetric.
+  Instance logR_cmetr : cmetric RL.res := discreteCMetric.
+
+  Instance nat_type : Setoid nat := discreteType.
+  Instance nat_metr : metric nat := discreteMetric.
+  Instance nat_cmetr : cmetric nat := discreteCMetric.
 
-    Set Printing All.
-    Check (expr -n> (value -n> Props) -n> Props).
-    Check ((expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props).
-    Unset Printing All.
-  End Benchmark.*)
+  Instance expr_type : Setoid expr := discreteType.
+  Instance expr_metr : metric expr := discreteMetric.
+  Instance expr_cmetr : cmetric expr := discreteCMetric.
 
+  (* We use this type quite a bit, so give it and its instances names *)
+  Definition vPred := value -n> Props.
+  Instance vPred_type  : Setoid vPred  := _.
+  Instance vPred_metr  : metric vPred  := _.
+  Instance vPred_cmetr : cmetric vPred := _.
+  
   (** And now we're ready to build the IRIS-specific connectives! *)
 
   Section Necessitation.
@@ -169,10 +174,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
     ownR (pcm_unit _, r).
 
   (** Proper physical state: ownership of the machine state **)
-  Instance state_type : Setoid state := discreteType.
-  Instance state_metr : metric state := discreteMetric.
-  Instance state_cmetr : cmetric state := discreteCMetric.
-
   Program Definition ownS : state -n> Props :=
     n[(fun s => ownRP (ex_own _ s))].
   Next Obligation.
@@ -187,9 +188,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
     simpl in HEq; subst; reflexivity.
   Qed.
 
-  Instance logR_metr : metric RL.res := discreteMetric.
-  Instance logR_cmetr : cmetric RL.res := discreteCMetric.
-
   Program Definition ownL : (option RL.res) -n> Props :=
     n[(fun r => match r with
                   | Some r => ownRL r
@@ -212,7 +210,7 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
   Proof.
     intros w n r Hp; simpl in Hp.
     eapply uni_pred, Hp; [reflexivity |].
-    exists r; now erewrite comm, pcm_op_unit by apply _.
+    now eapply unit_min.
   Qed.
 
   Lemma box_top : ⊤ == □ ⊤.

iris_vs.v

@@ -158,7 +158,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
           rewrite HSub in HP; specialize (HSub i); rewrite HLu in HSub.
           destruct (w' i) as [π' |]; [| contradiction].
           split; [intuition now eauto | intros].
-          simpl in HLw, HLrs, HSub; subst ri0; rewrite <- HLw, <- HSub.
+          simpl in HLw, HLrs, HSub. subst ri0. rewrite <- HLw, <- HSub.
           apply HInv; [now auto with arith |].
           eapply uni_pred, HP; [now auto with arith |].
           assert (HT : Some ri · Some r1 · Some r2 == Some rri)
@@ -301,10 +301,6 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     (* The above proof is rather ugly in the way it handles the monoid elements,
        but it works *)
 
-    Global Instance nat_type : Setoid nat := discreteType.
-    Global Instance nat_metr : metric nat := discreteMetric.
-    Global Instance nat_cmetr : cmetric nat := discreteCMetric.
-
     Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
       n[(fun p => n[(fun n => inv n p)])].
     Next Obligation.

iris_wp.v

@@ -16,20 +16,11 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Local Open Scope bi_scope.
     Local Open Scope lang_scope.
 
-    Global Instance expr_type : Setoid expr := discreteType.
-    Global Instance expr_metr : metric expr := discreteMetric.
-    Global Instance expr_cmetr : cmetric expr := discreteCMetric.
     Instance LP_isval : LimitPreserving is_value.
     Proof.
       intros σ σc HC; apply HC.
     Qed.
 
-    (* We use this type quite a bit, so give it and its instances names *)
-    Definition vPred := value -n> Props.
-    Global Instance vPred_type  : Setoid vPred  := _.
-    Global Instance vPred_metr  : metric vPred  := _.
-    Global Instance vPred_cmetr : cmetric vPred := _.
-
     Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : vPred) (r : res).
 
     Local Obligation Tactic := intros; eauto with typeclass_instances.
@@ -331,10 +322,10 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
           rewrite <-assoc, (comm (Some rret)), comm. reflexivity.
     Qed.
 
-    Lemma adequacy_ht {safe m e p φ n k tp' σ σ' w r}
-            (HT  : valid (ht safe m p e φ))
+    Lemma adequacy_ht {safe m e P φ n k tp' σ σ' w r}
+            (HT  : valid (ht safe m P e φ))
             (HSN : stepn n ([e], σ) (tp', σ'))
-            (HP  : p w (n + S k) r)
+            (HP  : P w (n + S k) r)
             (HE  : wsat σ m (Some r) w @ n + S k) :
       exists w' rs' φs',
         w ⊑ w' /\ wptp safe m w' (S k) tp' rs' (φ :: φs') /\ wsat σ' m (comp_list rs') w' @ S k.
@@ -363,8 +354,8 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
           intros _ _ [].
       - do 3 eexists. split; [eassumption|]. assumption.
     Qed.
-      
-    Program Definition cons_pred (φ : value -=> Prop): vPred :=
+
+    Program Definition lift_pred (φ : value -=> Prop): vPred :=
       n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
     Next Obligation.
       firstorder.
@@ -375,9 +366,10 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
     Qed.
 
+      
     (* Adequacy as stated in the paper: for observations of the return value, after termination *)
     Theorem adequacy_obs safe m e (φ : value -=> Prop) e' tp' σ σ'
-            (HT  : valid (ht safe m (ownS σ) e (cons_pred φ)))
+            (HT  : valid (ht safe m (ownS σ) e (lift_pred φ)))
             (HSN : steps ([e], σ) (e' :: tp', σ'))
             (HV : is_value e') :
         φ (exist _ e' HV).
@@ -417,6 +409,14 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
 
   End Adequacy.
 
+(*  Section Lifting.
+
+    Theorem lift_pure_step e (e's : expr -=> Prop) P Q mask
+            (RED  : reducible e)
+            (STEP : forall σ e' σ', prim_step (e, σ) (e', σ') -> 
+
+  End Lifting. *)
+  
   Section HoareTripleProperties.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
@@ -472,8 +472,8 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
 
     Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
 
-    Lemma htBind P φ φ' K e safe m :
-      ht safe m P e φ ∧ all (plugV safe m φ φ' K) ⊑ ht safe m P (K [[ e ]]) φ'.
+    Lemma htBind P φ ψ K e safe m :
+      ht safe m P e φ ∧ all (plugV safe m φ ψ K) ⊑ ht safe m P (K [[ e ]]) ψ.
     Proof.
       intros wz nz rz [He HK] w HSw n r HLe _ HP.
       specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
@@ -485,7 +485,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ HE] ] ] ].
         (* Fold the goal back into a wp *)
         setoid_rewrite HSw'.
-        assert (HT : wp safe m (K [[ e ]]) φ' w'' (S k) r');
+        assert (HT : wp safe m (K [[ e ]]) ψ w'' (S k) r');
           [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
         clear HE; specialize (HK (exist _ e HVal)).
         do 30 red in HK; unfold proj1_sig in HK.

lib/ModuRes/MetricCore.v

@@ -145,7 +145,7 @@ Class cmetric M `{mM : metric M} {cM : Completion M} :=
 Record cmtyp :=
   { cmm  :> Mtyp;
     iscm :  cmetric cmm}.
-Instance cmtyp_cmetric {M : cmtyp} : cmetric M := iscm M.
+Instance cmtyp_cmetric {M : cmtyp} : cmetric M | 0 := iscm M.
 Definition cmfromType (T : Type) `{cT : cmetric T} := Build_cmtyp (mfromType T) _.
 
 Section ChainCompl.

lib/ModuRes/PCM.v

@@ -31,6 +31,7 @@ Notation "p · q" := (pcm_op _ p q) (at level 40, left associativity) : pcm_scop
 
 Delimit Scope pcm_scope with pcm.
 
+(* FIXME having this with highest priority is really not a good idea. but necessary. *)
 Instance pcm_eq T `{pcmT : PCM T} : Setoid T | 0 := eqT _.
 
 (* PCMs with cartesian products of carriers. *)
@@ -96,7 +97,7 @@ Section Order.
   Context T `{pcmT : PCM T}.
   Local Open Scope pcm_scope.
 
-  Global Instance pcm_op_equiv : Proper (equiv ==> equiv ==> equiv) (pcm_op _).
+  Global Instance pcm_op_equiv : Proper (equiv ==> equiv ==> equiv) (pcm_op T).
   Proof.
     intros [s1 |] [s2 |] EQs; try contradiction; [|];
     [intros [t1 |] [t2 |] EQt; try contradiction; [| rewrite (comm (Some s1)), (comm (Some s2)) ] | intros t1 t2 _];

world_prop.v

@@ -2,8 +2,7 @@
     domain equations to build a higher-order separation logic *)
 Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
 Require Import ModuRes.Finmap ModuRes.Constr.
-Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
-
+Require Import ModuRes.PCM ModuRes.UPred.
 
 (* This interface keeps some of the details of the solution opaque *)
 Module Type WORLD_PROP (Res : PCM_T).
@@ -17,7 +16,7 @@ Module Type WORLD_PROP (Res : PCM_T).
   Definition Wld       := nat -f> PreProp.
   Definition Props     := Wld -m> UPred Res.res.
 
-  (* Define all the things on Props, so they have names - this shortens the terms later *)
+  (* Define all the things on Props, so they have names - this shortens the terms later. *)
   Instance Props_ty   : Setoid Props  | 1 := _.
   Instance Props_m    : metric Props  | 1 := _.
   Instance Props_cm   : cmetric Props | 1 := _.