lang implicits.

core_lang.v

@@ -42,7 +42,7 @@ Module Type CORE_LANG.
   Axiom fill_noinv: forall K1 K2, (* positivity *)
                        K1 ∘ K2 = ε -> K1 = ε /\ K2 = ε.
   Axiom fill_value : forall K e,
-                       is_value (fill K e ) ->
+                       is_value (fill K e) ->
                        K = ε.
   Axiom fill_fork  : forall K e e',
                        fork e' = fill K e ->

iris_ht_rules.v

@@ -33,9 +33,9 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       rewrite unfold_wp; intros w'; intros; split; [| split; [| split] ]; intros.
       - exists w' r'; split; [reflexivity | split; [| assumption] ].
         simpl; reflexivity.
-      - contradiction (values_stuck _ HV _ _ HDec).
+      - contradiction (values_stuck HV HDec).
         repeat eexists; eassumption.
-      - subst e; assert (HT := fill_value _ _ HV); subst K.
+      - subst e; assert (HT := fill_value HV); subst K.
         revert HV; rewrite fill_empty; intros.
         contradiction (fork_not_value _ HV).
       - unfold safeExpr. auto.
@@ -75,7 +75,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         do 30 red in HK; unfold proj1_sig in HK.
         apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
       - intros w'; intros; edestruct He as [_ [HS [HF HS'] ] ]; try eassumption; [].
-        split; [intros HVal; contradiction HNVal; assert (HT := fill_value _ _ HVal);
+        split; [intros HVal; contradiction HNVal; assert (HT := fill_value HVal);
                 subst K; rewrite fill_empty in HVal; assumption | split; [| split]; intros].
         + clear He HF HE; edestruct step_by_value as [K' EQK];
           [eassumption | repeat eexists; eassumption | eassumption |].
@@ -170,11 +170,11 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         edestruct HS as [w [r'' [HSw [He' HE] ] ] ]; try eassumption; clear He HS HE'.
         destruct k as [| k]; [exists w' r'; split; [reflexivity | split; [apply wpO | exact I] ] |].
         assert (HNV : ~ is_value ei)
-          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
-        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
+          by (intros HV; eapply (values_stuck HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
+        subst e; assert (HT := atomic_fill HAt HNV); subst K; clear HNV.
         rewrite ->fill_empty in *; rename ei into e.
         setoid_rewrite HSw'; setoid_rewrite HSw.
-        assert (HVal := atomic_step _ _ _ _ HAt HStep).
+        assert (HVal := atomic_step HAt HStep).
         rewrite ->HSw', HSw in HQ; clear - HE He' HQ HSub HVal HD.
         rewrite ->unfold_wp in He'; edestruct He' as [HV _];
         [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
@@ -192,7 +192,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
           unfold lt in HLt; rewrite ->HLt, <- HSw.
           eapply Q, HQ; [| apply le_n]; simpl; reflexivity.
         + eapply values_stuck; [.. | repeat eexists]; eassumption.
-        + clear - HDec HVal; subst; assert (HT := fill_value _ _ HVal); subst.
+        + clear - HDec HVal; subst; assert (HT := fill_value HVal); subst.
           rewrite ->fill_empty in HVal; now apply fork_not_value in HVal.
         + intros; left; assumption.
       - clear HQ; intros; rewrite <- HLe, HSw in He; clear HLe HSw.
@@ -285,11 +285,11 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         exists w'' (r1' · r2).
         split; [eassumption | split; [| eassumption] ].
         assert (HNV : ~ is_value ei)
-          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
-        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
+          by (intros HV; eapply (values_stuck HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
+        subst e; assert (HT := atomic_fill HAt HNV); subst K; clear HNV.
         rewrite ->fill_empty in *.
         unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; simpl in HLR.
-        assert (HVal := atomic_step _ _ _ _ HAt HStep).
+        assert (HVal := atomic_step HAt HStep).
         clear - He' HVal HLR; rename w'' into w; rewrite ->unfold_wp; intros w'; intros.
         split; [intros HV; clear HVal | split; intros; [exfalso| split; intros; [exfalso |] ] ].
         + rewrite ->unfold_wp in He'. rewrite <-assoc in HE.
@@ -302,7 +302,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
           unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
         + eapply values_stuck; [.. | repeat eexists]; eassumption.
         + subst; clear -HVal.
-          assert (HT := fill_value _ _ HVal); subst K; rewrite ->fill_empty in HVal.
+          assert (HT := fill_value HVal); subst K; rewrite ->fill_empty in HVal.
           contradiction (fork_not_value e').
         + unfold safeExpr. now auto.
       - subst; eapply fork_not_atomic; eassumption.
@@ -321,9 +321,9 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       clear rz n HLe; rewrite ->unfold_wp.
       clear w HSw HP; rename n' into n; rename w' into w; intros w'; intros.
       split; [intros; contradiction (fork_not_value e) | split; intros; [exfalso | split; intros ] ].
-      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec; subst.
+      - assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec; subst.
         eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
-      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec.
+      - assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec.
         apply fork_inj in HDec; subst e'; rewrite <- EQr in HE.
         unfold lt in HLt; rewrite <- (le_S_n _ _ HLt), HSw in He.
         simpl in HLR; rewrite <- Le.le_n_Sn in HE.
@@ -336,7 +336,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
           simpl; reflexivity.
         + eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
         + assert (HV := fork_ret_is_value); rewrite ->HDec in HV; clear HDec.
-          assert (HT := fill_value _ _ HV);subst K; rewrite ->fill_empty in HV.
+          assert (HT := fill_value HV);subst K; rewrite ->fill_empty in HV.
           eapply fork_not_value; eassumption.
         + left; apply fork_ret_is_value.
       - right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.

iris_meta.v

@@ -133,7 +133,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       exists w' rs' φs',
         wptp safe m w' (S k') tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'.
     Proof.
-      destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
+      destruct (steps_stepn HSN) as [n HSN']. clear HSN.
       pose (r := (ex_own σ, 1) : res).
       edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=r) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS]]]]]; clear HT HSN'.
       - exists 1; now rewrite ->ra_op_unit by apply _.
@@ -306,7 +306,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       { exists w'' r'. by split; [done | split; [exact: wpO | done]]. }
       have HLt': k' < S k' by done.
       move/(_ _ _ _ _ _ (prefl w'') HLt' HD HW'): Hei' => [Hv _] {HLt' HD HW'}.
-      move: (atomic_step _ _ _ _ HA HStep) => HV {HA HStep}.
+      move: (atomic_step HA HStep) => HV {HA HStep}.
       move/(_ HV): Hv => [w''' [rei' [HSw'' [Hei' HW]]]].
       move: HW; rewrite assoc => HW.
       set Hw'Sw''' := ptrans HSw' HSw''.
@@ -383,7 +383,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       have HK: K = ε.
       { move: HDec; rewrite eq_sym_iff -(fill_empty e) => HDec.
         have HRed1: reducible ei by exists σ (e',σ').
-        by apply: (step_same_ctx _ _ _ _ HDec HRed1 RED). }
+        by apply: (step_same_ctx HDec HRed1 RED). }
       move: HDec HStep; rewrite HK 2!fill_empty; move=><- HStep {ei K HK RED}.
 
       (* have φ(e',σ'), so we can apply the triple… *)

lang.v

@@ -12,6 +12,16 @@ Module Lang (C : CORE_LANG).
 
   Export C.
 
+  Arguments fork_inj {_ _} _.
+  Arguments fill_inj1 {_ _} _ _.
+  Arguments fill_inj2 _ {_ _} _.
+  Arguments fill_noinv {_ _} _.
+  Arguments fill_value {_ _} _.
+  Arguments fill_fork {_ _ _} _.
+  Arguments values_stuck {_} _ {_ _} _ _.
+  Arguments atomic_reducible {_} _.
+  Arguments atomic_step {_ _ _ _} _ _.
+
   Local Open Scope lang_scope.
 
   (** Thread pools **)
@@ -34,28 +44,28 @@ Module Lang (C : CORE_LANG).
       step ρ ρ'.
 
   (* Some derived facts about contexts *)
-  Lemma comp_ctx_assoc K0 K1 K2 :
+  Lemma comp_ctx_assoc {K0 K1 K2} :
     (K0 ∘ K1) ∘ K2 = K0 ∘ (K1 ∘ K2).
   Proof.
-    apply (fill_inj1 _ _ fork_ret).
+    apply (fill_inj1 fork_ret).
     now rewrite <- !fill_comp.
   Qed.
 
-  Lemma comp_ctx_emp_l K :
+  Lemma comp_ctx_emp_l {K} :
     ε ∘ K = K.
   Proof.
-    apply (fill_inj1 _ _ fork_ret).
+    apply (fill_inj1 fork_ret).
     now rewrite <- fill_comp, fill_empty.
   Qed.
 
-  Lemma comp_ctx_emp_r K :
+  Lemma comp_ctx_emp_r {K} :
     K ∘ ε = K.
   Proof.
-    apply (fill_inj1 _ _ fork_ret).
+    apply (fill_inj1 fork_ret).
     now rewrite <- fill_comp,  fill_empty.
   Qed.
 
-  Lemma comp_ctx_inj1 K1 K2 K :
+  Lemma comp_ctx_inj1 {K1 K2 K} :
     K1 ∘ K = K2 ∘ K ->
     K1 = K2.
   Proof.
@@ -64,7 +74,7 @@ Module Lang (C : CORE_LANG).
     now rewrite -> !fill_comp, HEq.
   Qed.
 
-  Lemma comp_ctx_inj2  K K1 K2 :
+  Lemma comp_ctx_inj2  {K K1 K2} :
     K ∘ K1 = K ∘ K2 ->
     K1 = K2.
   Proof.
@@ -73,26 +83,26 @@ Module Lang (C : CORE_LANG).
     now rewrite -> !fill_comp, HEq.
   Qed.
 
-  Lemma comp_ctx_neut_emp_r K K' :
+  Lemma comp_ctx_neut_emp_r {K K'} :
     K = K ∘ K' ->
     K' = ε.
   Proof.
     intros HEq.
     rewrite <- comp_ctx_emp_r in HEq at 1.
-    apply comp_ctx_inj2 in HEq; congruence.
+    apply comp_ctx_inj2 in HEq; now symmetry.
   Qed.
 
-  Lemma comp_ctx_neut_emp_l K K' :
+  Lemma comp_ctx_neut_emp_l {K K'} :
     K = K' ∘ K ->
     K' = ε.
   Proof.
     intros HEq.
     rewrite <- comp_ctx_emp_l in HEq at 1.
-    apply comp_ctx_inj1 in HEq; congruence.
+    apply comp_ctx_inj1 in HEq; now symmetry.
   Qed.
 
   (* Lemmas about expressions *)
-  Lemma reducible_not_value e:
+  Lemma reducible_not_value {e} :
     reducible e -> ~is_value e.
   Proof.
     intros H_red H_val.
@@ -108,13 +118,13 @@ Module Lang (C : CORE_LANG).
     exact: (HStuck _ _ eq_refl).
   Qed.
 
-  Lemma step_same_ctx: forall K K' e e',
+  Lemma step_same_ctx {K K' e e'} :
                          fill K e = fill K' e' ->
                          reducible e  ->
                          reducible e' ->
                          K = K'.
   Proof.
-    intros K K' e e' H_fill H_red H_red'.
+    intros H_fill H_red H_red'.
     edestruct (step_by_value K K' e e') as [K'' H_K''].
     - assumption.
     - assumption.
@@ -125,14 +135,14 @@ Module Lang (C : CORE_LANG).
       + now apply reducible_not_value.
       + subst K.
         rewrite comp_ctx_assoc in H_K''.
-        assert (H_emp := comp_ctx_neut_emp_r _ _ H_K'').
+        assert (H_emp := comp_ctx_neut_emp_r H_K'').
         apply fill_noinv in H_emp.
         destruct H_emp as[H_K'''_emp H_K''_emp].
         subst K'' K'''.
         now rewrite comp_ctx_emp_r.
   Qed.
 
-  Lemma atomic_not_stuck e:
+  Lemma atomic_not_stuck {e} :
     atomic e -> ~stuck e.
   Proof.
     intros H_atomic H_stuck.
@@ -157,7 +167,7 @@ Module Lang (C : CORE_LANG).
     tauto.
   Qed.
 
-  Lemma atomic_fill e K
+  Lemma atomic_fill {e K}
         (HAt : atomic (fill K e))
         (HNV : ~ is_value e) :
     K = empty_ctx.
@@ -182,7 +192,7 @@ Module Lang (C : CORE_LANG).
             (HSN : stepn n ρ2 ρ3) :
       stepn (S n) ρ1 ρ3.
 
-  Lemma steps_stepn ρ1 ρ2:
+  Lemma steps_stepn {ρ1 ρ2} :
     steps ρ1 ρ2 -> exists n, stepn n ρ1 ρ2.
   Proof.
     induction 1.
@@ -190,7 +200,7 @@ Module Lang (C : CORE_LANG).
     - destruct IHsteps as [n IH]. eexists. eauto using stepn.
   Qed.
 
-  Lemma stepn_steps n ρ1 ρ2:
+  Lemma stepn_steps {n ρ1 ρ2}:
     stepn n ρ1 ρ2 -> steps ρ1 ρ2.
   Proof.
     induction 1; now eauto using steps.