Commit cfac1295 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge sbi canonical structure into the bi canonical structure.

parent 69dfcc71
......@@ -2,7 +2,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
......@@ -13,7 +13,7 @@
1 subgoal
PROP : sbi
PROP : bi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
......@@ -25,7 +25,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
Q : PROP
============================
"H1" : emp
......@@ -36,7 +36,7 @@
1 subgoal
PROP : sbi
PROP : bi
Q : PROP
============================
□ emp ∗ Q -∗ Q
......@@ -44,7 +44,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
......@@ -58,7 +58,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
Q : PROP
============================
"HQ" : <affine> Q
......@@ -69,7 +69,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
Q : PROP
Affine0 : Affine Q
============================
......@@ -81,7 +81,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
Ψ : nat → PROP
a : nat
============================
......@@ -109,7 +109,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
: string
1 subgoal
PROP : sbi
PROP : bi
P, Q : PROP
n, m, k : nat
============================
......@@ -120,7 +120,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
: string
1 subgoal
PROP : sbi
PROP : bi
φ : Prop
P, P2, Q, R1, R2 : PROP
H : φ
......@@ -136,7 +136,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
: string
1 subgoal
PROP : sbi
PROP : bi
x, y : nat
============================
"H" : ⌜S (S (S x)) = y⌝
......@@ -145,7 +145,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
1 subgoal
PROP : sbi
PROP : bi
x, y, z : nat
============================
"H1" : ⌜S (S (S x)) = y⌝
......@@ -155,7 +155,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
1 subgoal
PROP : sbi
PROP : bi
x, y, z : nat
============================
"H1" : ⌜S (S (S x)) = y⌝
......@@ -172,7 +172,7 @@ Tactic failure: iEval: %: unsupported selection pattern.
: string
1 subgoal
PROP : sbi
PROP : bi
P, Q : PROP
============================
--------------------------------------∗
......@@ -182,7 +182,7 @@ Tactic failure: iEval: %: unsupported selection pattern.
: string
1 subgoal
PROP : sbi
PROP : bi
P, Q : PROP
============================
--------------------------------------∗
......@@ -194,7 +194,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiAffine0 : BiAffine PROP
P, Q : PROP
============================
......@@ -207,7 +207,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
x : nat
l : list nat
P : PROP
......@@ -220,7 +220,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
PROP : bi
x : nat
l : list nat
P : PROP
......@@ -235,7 +235,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
x1, x2 : nat
l1, l2 : list nat
P : PROP
......@@ -248,7 +248,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
PROP : bi
x1, x2 : nat
l1, l2 : list nat
P : PROP
......@@ -264,7 +264,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
Φ : nat → nat → PROP
x1, x2 : nat
l1, l2 : list nat
......@@ -278,7 +278,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
============================
"H" : □ True
--------------------------------------∗
......@@ -288,7 +288,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
============================
"H" : emp
--------------------------------------□
......@@ -298,7 +298,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
============================
"H" : emp
--------------------------------------□
......@@ -308,7 +308,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
mP : option PROP
Q, R : PROP
============================
......@@ -320,7 +320,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
PROP : bi
mP : option PROP
Q, R : PROP
============================
......@@ -332,12 +332,11 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
X : Type
E1, E2 : coPset.coPset
α : X → PROP
β : X → PROP
α, β : X → PROP
γ : X → option PROP
============================
"Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
......@@ -348,7 +347,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
......@@ -359,7 +358,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
......@@ -372,7 +371,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
......@@ -383,7 +382,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
......@@ -396,7 +395,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
......@@ -408,7 +407,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
......@@ -421,7 +420,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
......@@ -433,7 +432,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
......@@ -446,7 +445,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
E : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
......@@ -459,7 +458,7 @@ Tactic failure: iFrame: cannot frame Q.
: string
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
......@@ -537,7 +536,7 @@ Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
: string
The command has indeed failed with message:
In environment
PROP : sbi
PROP : bi
P : PROP
The term "true" has type "bool" while it is expected to have type "nat".
"iStartProof_fail"
......@@ -622,15 +621,15 @@ k is used in hypothesis Hk.
: string
The command has indeed failed with message:
Tactic failure: iRevert: k is used in hypothesis "Hk".
"iLöb_no_sbi"
"iLöb_no_bi"
: string
The command has indeed failed with message:
Tactic failure: iLöb: not a step-indexed BI entailment.
Tactic failure: iLöb: Löb induction not supported for this BI.
"test_pure_name"
: string
1 subgoal
PROP : sbi
PROP : bi
P1 : PROP
P2, P3 : Prop
Himpl : P2 → P3
......
......@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics intro_patterns.
Set Default Proof Using "Type".
Section tests.
Context {PROP : sbi}.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp P - P.
......@@ -411,7 +411,7 @@ Proof.
iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.
Lemma test_iLöb P : n, ^n P.
Lemma test_iLöb `{!BiLöb PROP} P : n, ^n P.
Proof.
iLöb as "IH". iDestruct "IH" as (n) "IH".
by iExists (S n).
......@@ -822,7 +822,7 @@ Qed.
End tests.
Section parsing_tests.
Context {PROP : sbi}.
Context {PROP : bi}.
Implicit Types P : PROP.
(** Test notations for (bi)entailment and internal equality. These tests are
......@@ -860,7 +860,7 @@ Lemma test_entails_annot_sections_space_close P :
(P @{PROP} P ) (@{PROP} ) P P (. P ) P.
Proof. naive_solver. Qed.
Lemma test_sbi_internal_eq_annot_sections P :
Lemma test_bi_internal_eq_annot_sections P :
@{PROP}
P @{PROP} P (@{PROP}) P P (P .) P (. P) P
((P @{PROP} P)) ((@{PROP})) P P ((P .)) P ((. P)) P
......@@ -870,7 +870,7 @@ Proof. naive_solver. Qed.
End parsing_tests.
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Context {PROP : bi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
Check "elim_mod_accessor".
......@@ -944,7 +944,7 @@ End printing_tests.
(** Test error messages *)
Section error_tests.
Context {PROP : sbi}.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iStopProof_not_proofmode".
......@@ -1127,13 +1127,13 @@ Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iLöb_no_sbi".
Lemma iLöb_no_sbi P : P.
Check "iLöb_no_bi".
Lemma iLöb_no_bi P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
Section pure_name_tests.
Context {PROP : sbi}.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
(* mock string_to_ident for just these tests *)
Ltac ltac_tactics.string_to_ident_hook ::=
......
......@@ -45,9 +45,9 @@ Section base_logic_tests.
Lemma test_iStartProof_2 P : P -* P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_3 P : P -* P.
Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_4 P : P -* P.
Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
End base_logic_tests.
Section iris_tests.
......@@ -233,7 +233,6 @@ Section monpred_tests.
Context {I : biIndex}.
Local Notation monPred := (monPred I (iPropI Σ)).
Local Notation monPredI := (monPredI I (iPropI Σ)).
Local Notation monPredSI := (monPredSI I (iPropSI Σ)).
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
......@@ -261,7 +260,7 @@ End monpred_tests.
(** Test specifically if certain things parse correctly. *)
Section parsing_tests.
Context {PROP : sbi}.
Context {PROP : bi}.
Implicit Types P : PROP.
Lemma test_bi_emp_valid : |--@{PROP} True.
......
......@@ -43,9 +43,9 @@ Section base_logic_tests.
Lemma test_iStartProof_2 P : P - P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_3 P : P - P.
Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_4 P : P - P.
Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
End base_logic_tests.
Section iris_tests.
......@@ -231,7 +231,6 @@ Section monpred_tests.
Context {I : biIndex}.
Local Notation monPred := (monPred I (iPropI Σ)).
Local Notation monPredI := (monPredI I (iPropI Σ)).
Local Notation monPredSI := (monPredSI I (iPropSI Σ)).
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
......
1 subgoal
I : biIndex
PROP : sbi
P, Q : monpred.monPred I PROP
PROP : bi
P, Q : monPred
i : I
============================
"HW" : (P -∗ Q) i
......@@ -12,8 +12,8 @@
1 subgoal
I : biIndex
PROP : sbi
P, Q : monpred.monPred I PROP
PROP : bi
P, Q : monPred
i, j : I
============================
"HW" : (P -∗ Q) j
......@@ -24,8 +24,8 @@
1 subgoal
I : biIndex
PROP : sbi
P, Q : monpred.monPred I PROP
PROP : bi
P, Q : monPred
Objective0 : Objective Q
𝓟, 𝓠 : PROP
============================
......@@ -38,9 +38,9 @@
1 subgoal
I : biIndex
PROP : sbi
PROP : bi
FU0 : BiFUpd PROP * ()
P, Q : monpred.monPred I PROP
P, Q : monPred
i : I
============================
--------------------------------------∗
......@@ -49,9 +49,9 @@
1 subgoal
I : biIndex
PROP : sbi
PROP : bi
FU0 : BiFUpd PROP * ()
P : monpred.monPred I PROP
P : monPred
i : I
============================
--------------------------------------∗
......
......@@ -3,10 +3,9 @@ From iris.base_logic.lib Require Import invariants.
Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
Section tests.
Context {I : biIndex} {PROP : sbi}.
Context {I : biIndex} {PROP : bi}.
Local Notation monPred := (monPred I PROP).
Local Notation monPredI := (monPredI I PROP).
Local Notation monPredSI := (monPredSI I PROP).
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : PROP.
Implicit Types i j : I.
......@@ -19,9 +18,9 @@ Section tests.
Lemma test_iStartProof_2 P : P - P.
Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
Lemma test_iStartProof_3 P : P - P.
Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
Proof. iStartProof monPredI. iStartProof monPredI. iIntros "$". Qed.
Lemma test_iStartProof_4 P : P - P.
Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
Proof. iStartProof monPredI. iStartProof monPred. iIntros "$". Qed.
Lemma test_iStartProof_5 P : P - P.
Proof. iStartProof PROP. iIntros (i) "$". Qed.
Lemma test_iStartProof_6 P : P P.
......
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
......@@ -15,7 +15,7 @@
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
......@@ -24,7 +24,7 @@
accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
......@@ -37,7 +37,7 @@
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
......@@ -50,7 +50,7 @@
1 subgoal
PROP : sbi
PROP : bi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset
============================
......@@ -62,7 +62,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
......@@ -71,7 +71,7 @@
1 subgoal
PROP : sbi
PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
......@@ -82,7 +82,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
============================
"H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝
--------------------------------------∗
......@@ -90,7 +90,7 @@
1 subgoal
PROP : sbi
PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
......@@ -99,7 +99,7 @@
1 subgoal
PROP : sbi
PROP : bi
x : nat
============================
"H" : ▷ (∃ x0 : nat, <affine> ⌜x = x0⌝)
......@@ -110,7 +110,7 @@
: string
1 subgoal
PROP : sbi
PROP : bi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
......@@ -119,7 +119,7 @@
1 subgoal
PROP : sbi
PROP : bi
x : nat
============================
"H" : ◇ (∃ x0 : nat, <affine> ⌜x = x0⌝)
......
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section basic_tests.