From fbf07f03f25dcad4d6bd97824e200a67f1531e45 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Jan 2017 18:13:28 +0100
Subject: [PATCH] program_logic: improve 'proof using' hint to be more minimal,
 more future-proof

---
 theories/program_logic/adequacy.v       |  2 +-
 theories/program_logic/ectx_language.v  |  2 +-
 theories/program_logic/ectx_lifting.v   | 11 +++++------
 theories/program_logic/ectxi_language.v |  2 +-
 theories/program_logic/hoare.v          |  2 +-
 theories/program_logic/language.v       |  2 +-
 theories/program_logic/lifting.v        |  2 +-
 theories/program_logic/ownp.v           | 10 +++++-----
 theories/program_logic/weakestpre.v     |  2 +-
 9 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 9951b8e47..fd31d79ba 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (* Global functor setup *)
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 76b2b167b..646ebbdca 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -2,7 +2,7 @@
     that this gives rise to a "language" in the Iris sense. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index df02d3969..e0c0f468b 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,12 +1,11 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+Set Default Proof Using "Type".
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ} `{Inhabited state}.
+Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
@@ -37,7 +36,7 @@ Lemma wp_lift_pure_head_step E Φ e1 :
   (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof.
+Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
   iIntros (????). iApply "H". eauto.
 Qed.
@@ -77,7 +76,7 @@ Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_pure_det_step. Qed.
+Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   to_val e1 = None →
@@ -85,7 +84,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-Proof.
+Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
 Qed.
 End wp.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 74da06afc..ee9851867 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -2,7 +2,7 @@
     a proof that these are instances of general ectx-based languages. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Import language ectx_language.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index b5ca5a347..0cb4f409c 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 3227a06e1..21fc2e3a1 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Structure language := Language {
   expr : Type;
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index b56edc556..82706be47 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index e57910e9f..0a9862986 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
 From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
@@ -158,7 +158,7 @@ End lifting.
 Section ectx_lifting.
   Import ectx_language.
   Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-  Context `{ownPG (ectx_lang expr) Σ} `{Inhabited state}.
+  Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
   Implicit Types Φ : val → iProp Σ.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
@@ -181,7 +181,7 @@ Section ectx_lifting.
     (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
       WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
     ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
+  Proof using Hinh.
     iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
     iIntros (????). iApply "H". eauto.
   Qed.
@@ -220,14 +220,14 @@ Section ectx_lifting.
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
     ⊢ WP e1 @ E {{ Φ }}.
-  Proof. eauto using wp_lift_pure_det_step. Qed.
+  Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
   Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
+  Proof using Hinh.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index b75cb874b..98a08018f 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
-- 
GitLab