Commit fbf07f03 authored by Ralf Jung's avatar Ralf Jung

program_logic: improve 'proof using' hint to be more minimal, more future-proof

parent 599c70e1
Pipeline #3603 passed with stage
in 10 minutes and 25 seconds
...@@ -3,7 +3,7 @@ From iris.algebra Require Import gmap auth agree gset coPset. ...@@ -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 Require Import big_op soundness.
From iris.base_logic.lib Require Import wsat. From iris.base_logic.lib Require Import wsat.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
(* Global functor setup *) (* Global functor setup *)
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
that this gives rise to a "language" in the Iris sense. *) that this gives rise to a "language" in the Iris sense. *)
From iris.algebra Require Export base. From iris.algebra Require Export base.
From iris.program_logic Require Import language. 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 (* We need to make thos arguments indices that we want canonical structure
inference to use a keys. *) inference to use a keys. *)
......
(** Some derived lemmas for ectx-based languages *) (** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting. From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
(* FIXME: This file needs a 'Proof Using' hint, but the default we use Set Default Proof Using "Type".
everywhere makes for lots of extra ssumptions. *)
Section wp. Section wp.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}. 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 P : iProp Σ.
Implicit Types Φ : val iProp Σ. Implicit Types Φ : val iProp Σ.
Implicit Types v : val. Implicit Types v : val.
...@@ -37,7 +36,7 @@ Lemma wp_lift_pure_head_step E Φ e1 : ...@@ -37,7 +36,7 @@ Lemma wp_lift_pure_head_step E Φ e1 :
( e2 efs σ, head_step e1 σ e2 σ efs ( e2 efs σ, head_step e1 σ e2 σ efs
WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }}) WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof using Hinh.
iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext. iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
iIntros (????). iApply "H". eauto. iIntros (????). iApply "H". eauto.
Qed. Qed.
...@@ -77,7 +76,7 @@ Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs : ...@@ -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') head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' efs = efs')
(WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }}) (WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. 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 : Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
to_val e1 = None to_val e1 = None
...@@ -85,7 +84,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 : ...@@ -85,7 +84,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
( σ1 e2' σ2 efs', ( σ1 e2' σ2 efs',
head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs') head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}. 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. intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
Qed. Qed.
End wp. End wp.
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
a proof that these are instances of general ectx-based languages. *) a proof that these are instances of general ectx-based languages. *)
From iris.algebra Require Export base. From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language. 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 (* We need to make thos arguments indices that we want canonical structure
inference to use a keys. *) inference to use a keys. *)
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export viewshifts. From iris.base_logic.lib Require Export viewshifts.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ) Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ iProp Σ) : iProp Σ := (e : expr Λ) (Φ : val Λ iProp Σ) : iProp Σ :=
......
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Structure language := Language { Structure language := Language {
expr : Type; expr : Type;
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Section lifting. Section lifting.
Context `{irisG Λ Σ}. Context `{irisG Λ Σ}.
......
...@@ -3,7 +3,7 @@ From iris.program_logic Require Import lifting adequacy. ...@@ -3,7 +3,7 @@ From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language. From iris.program_logic Require ectx_language.
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG { Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ; ownP_invG : invG Σ;
...@@ -158,7 +158,7 @@ End lifting. ...@@ -158,7 +158,7 @@ End lifting.
Section ectx_lifting. Section ectx_lifting.
Import ectx_language. Import ectx_language.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}. 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 Φ : val iProp Σ.
Implicit Types e : expr. Implicit Types e : expr.
Hint Resolve head_prim_reducible head_reducible_prim_step. Hint Resolve head_prim_reducible head_reducible_prim_step.
...@@ -181,7 +181,7 @@ Section ectx_lifting. ...@@ -181,7 +181,7 @@ Section ectx_lifting.
( e2 efs σ, head_step e1 σ e2 σ efs ( e2 efs σ, head_step e1 σ e2 σ efs
WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }}) WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof using Hinh.
iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext. iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
iIntros (????). iApply "H". eauto. iIntros (????). iApply "H". eauto.
Qed. Qed.
...@@ -220,14 +220,14 @@ Section ectx_lifting. ...@@ -220,14 +220,14 @@ Section ectx_lifting.
( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' efs = efs') ( σ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 e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. 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 : Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
to_val e1 = None to_val e1 = None
( σ1, head_reducible e1 σ1) ( σ1, head_reducible e1 σ1)
( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs') ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}. 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. intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
Qed. Qed.
End ectx_lifting. End ectx_lifting.
...@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates. ...@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language. From iris.program_logic Require Export language.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG { Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment