make Coq *much* faster by introducing names for some instances

configure

+#!/bin/sh
+coq_makefile lib/ModuRes -R lib/ModuRes ModuRes *.v -o Makefile

iris.v

@@ -25,7 +25,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   Instance Props_BI : ComplBI Props | 0 := _.
   Instance Props_Later : Later Props | 0 := _.
-
+  
   (* Benchmark: How large is thid type? *)
   Section Benchmark.
     Local Open Scope mask_scope.
@@ -33,11 +33,12 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
     Local Open Scope bi_scope.
     Local Open Scope lang_scope.
 
-    Local Instance expr_type : Setoid expr := discreteType.
-    Local Instance expr_metr : metric expr := discreteMetric.
-    Local Instance expr_cmetr : cmetric expr := discreteCMetric.
+    Local Instance _bench_expr_type : Setoid expr := discreteType.
+    Local Instance _bench_expr_metr : metric expr := discreteMetric.
+    Local Instance _bench_cmetr : cmetric expr := 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).
   End Benchmark.
 
@@ -403,6 +404,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   End Erasure.
 
+  Check erasure.
 
   Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
 
@@ -484,6 +486,8 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   End ViewShifts.
 
+  Check vs.
+
   Section ViewShiftProps.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
@@ -996,6 +1000,8 @@ Qed.
 
   End HoareTriples.
 
+  Check wp.
+
   Section Soundness.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
@@ -1211,6 +1217,8 @@ Qed.
 
   End Soundness.
 
+  Check soundness.
+
   Section HoareTripleProperties.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.

world_prop.v

@@ -80,8 +80,20 @@ Module WorldProp (Res : PCM_T).
   Lemma isoR T : ı (ı' T) == T.
   Proof. apply (UF_id T). Qed.
 
+  Set Printing All.
+  (* PreProp has an equivalence and a complete metric. It also has a preorder that fits to everything else. *)
+  Instance PProp_ty   : Setoid PreProp     := _.
+  Instance PProp_m    : metric PreProp     := _.
+  Instance PProp_cm   : cmetric PreProp    := _.
   Instance PProp_preo : preoType PreProp   := disc_preo PreProp.
   Instance PProp_pcm  : pcmType PreProp    := disc_pcm PreProp.
   Instance PProp_ext  : extensible PreProp := disc_ext PreProp.
 
+  (* Give names to the things for Props, so the terms can get shorter. *)
+  Instance Props_ty   : Setoid Props     := _.
+  Instance Props_m    : metric Props     := _.
+  Instance Props_cm   : cmetric Props    := _.
+  Instance Props_preo : preoType Props   := _.
+  Instance Props_pcm  : pcmType Props    := _.
+
 End WorldProp.