Commit 62be0a86 authored by Robbert's avatar Robbert

Merge branch 'explicit-vdash' into 'master'

Explicit vdash

See merge request iris/iris!358
parents ad82d138 31bb46c5
......@@ -26,7 +26,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
P : val → iProp Σ
============================
<<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
<<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -58,7 +58,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
<<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -89,7 +89,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
<<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -121,7 +121,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
<<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -154,7 +154,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -173,9 +175,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -194,10 +196,10 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
<<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -218,9 +220,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ x, RET #() >>>
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -240,9 +242,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -263,9 +265,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ #(), RET #() >>>
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -286,9 +288,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy, RET #() >>>
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy, RET #() >>>
1 subgoal
Σ : gFunctors
......@@ -309,10 +311,10 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
......
......@@ -41,28 +41,28 @@ Section printing.
Definition code : expr := #().
Lemma print_both_quant (P : val iProp Σ) :
<<< x, P x >>> code @ <<< y, P y, RET #() >>>.
<<< x, P x >>> code @ <<< y, P y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_first_quant l :
<<< x, l x >>> code @ <<< l x, RET #() >>>.
<<< x, l x >>> code @ <<< l x, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_second_quant l :
<<< l #() >>> code @ <<< y, l y, RET #() >>>.
<<< l #() >>> code @ <<< y, l y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_no_quant l :
<<< l #() >>> code @ <<< l #(), RET #() >>>.
<<< l #() >>> code @ <<< l #(), RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
......@@ -71,49 +71,49 @@ Section printing.
Check "Now come the long pre/post tests".
Lemma print_both_quant_long l :
<<< x, l x l x >>> code @ <<< y, l y, RET #() >>>.
<<< x, l x l x >>> code @ <<< y, l y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpre l :
<<< x, l x l x l x l x l x l x >>> code @ <<< y, l y, RET #() >>>.
<<< x, l x l x l x l x l x l x >>> code @ <<< y, l y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpost l :
<<< xx, l xx l xx l xx >>> code @ <<< yyyy, l yyyy l xx l xx l xx l xx l xx, RET #() >>>.
<<< xx, l xx l xx l xx >>> code @ <<< yyyy, l yyyy l xx l xx l xx l xx l xx, RET #() >>>.
Proof.
Show. iIntros (Φ) "?". Show.
Abort.
Lemma print_first_quant_long l :
<<< x, l x l x l x l x >>> code @ <<< l x, RET #() >>>.
<<< x, l x l x l x l x >>> code @ <<< l x, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_second_quant_long l x :
<<< l x l x l x l x l x l x >>> code @ <<< y, l y, RET #() >>>.
<<< l x l x l x l x l x l x >>> code @ <<< y, l y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_long l x :
<<< l x l x l x l x l x l x >>> code @ <<< l #(), RET #() >>>.
<<< l x l x l x l x l x l x >>> code @ <<< l #(), RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpre l xx yyyy :
<<< l xx l xx l xx l xx l xx l xx l xx >>> code @ <<< l yyyy, RET #() >>>.
<<< l xx l xx l xx l xx l xx l xx l xx >>> code @ <<< l yyyy, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpost l xx yyyy :
<<< l xx l xx l xx >>> code @ <<< l yyyy l xx l xx l xx l xx l xx l xx, RET #() >>>.
<<< l xx l xx l xx >>> code @ <<< l yyyy l xx l xx l xx l xx l xx l xx, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
......@@ -121,7 +121,7 @@ Section printing.
Check "Prettification".
Lemma iMod_prettify (P : val iProp Σ) :
<<< x, P x >>> !#0 @ <<< y, P y, RET #() >>>.
<<< x, P x >>> !#0 @ <<< y, P y, RET #() >>>.
Proof.
iIntros (Φ) "AU". iMod "AU". Show.
Abort.
......
......@@ -24,7 +24,7 @@ Section tests.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}.
Proof.
iIntros "". rewrite /heap_e. Show.
wp_alloc l as "?". wp_load. Show.
......@@ -36,7 +36,7 @@ Section tests.
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }].
Proof.
iIntros "". rewrite /heap_e2.
wp_alloc l as "Hl". Show. wp_alloc l'.
......@@ -48,7 +48,7 @@ Section tests.
let: "f" := λ: "z", "z" + #1 in
if: "x" then "f" #0 else "f" #1.
Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, v = #1 }]%I.
Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, v = #1 }].
Proof.
iIntros "". rewrite /heap_e3.
by repeat (wp_pure _).
......@@ -58,7 +58,7 @@ Section tests.
let: "x" := (let: "y" := ref (ref #1) in ref "y") in
! ! !"x".
Lemma heap_e4_spec : WP heap_e4 [{ v, v = #1 }]%I.
Lemma heap_e4_spec : WP heap_e4 [{ v, v = #1 }].
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'.
wp_alloc l''. by repeat wp_load.
......@@ -67,7 +67,7 @@ Section tests.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }].
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'.
wp_load. wp_faa. do 2 wp_load. by wp_pures.
......@@ -76,7 +76,7 @@ Section tests.
Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) :
val_is_unboxed v (WP heap_e6 v {{ w, w = #true }})%I.
val_is_unboxed v WP heap_e6 v {{ w, w = #true }}.
Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
......@@ -117,7 +117,7 @@ Section tests.
Qed.
Lemma Pred_user E :
WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }].
Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
Lemma wp_apply_evar e P :
......@@ -132,22 +132,22 @@ Section tests.
Qed.
Lemma wp_alloc_split :
WP Alloc #0 {{ _, True }}%I.
WP Alloc #0 {{ _, True }}.
Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
Lemma wp_alloc_drop :
WP Alloc #0 {{ _, True }}%I.
WP Alloc #0 {{ _, True }}.
Proof. wp_alloc l as "_". Show. done. Qed.
Check "wp_nonclosed_value".
Lemma wp_nonclosed_value :
WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
Lemma wp_alloc_array n : 0 < n
{{{ True }}}
AllocN #n #0
{{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}%I.
{{{ True }}}
AllocN #n #0
{{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}.
Proof.
iIntros (? Φ) "!> _ HΦ".
wp_alloc l as "?"; first done.
......@@ -155,9 +155,9 @@ Section tests.
Qed.
Lemma twp_alloc_array n : 0 < n
[[{ True }]]
AllocN #n #0
[[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]]%I.
[[{ True }]]
AllocN #n #0
[[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]].
Proof.
iIntros (? Φ) "!> _ HΦ".
wp_alloc l as "?"; first done. Show.
......@@ -258,7 +258,7 @@ Section error_tests.
Check "not_cmpxchg".
Lemma not_cmpxchg :
(WP #() #() {{ _, True }})%I.
WP #() #() {{ _, True }}.
Proof.
Fail wp_cmpxchg_suc.
Abort.
......
......@@ -75,7 +75,7 @@ Section list_reverse.
end.
Lemma rev_acc_ht hd acc xs ys :
{{ is_list hd xs is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
{{ is_list hd xs is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
Proof.
iIntros "!> [Hxs Hys]".
iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
......@@ -89,7 +89,7 @@ Section list_reverse.
Qed.
Lemma rev_ht hd xs :
{{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
{{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
Proof.
iIntros "!> Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
......@@ -202,7 +202,7 @@ Section counter_proof.
Proof. apply _. Qed.
Lemma newcounter_spec :
{{ True }} newcounter #() {{ v, l, v = #l C l 0 }}.
{{ True }} newcounter #() {{ v, l, v = #l C l 0 }}.
Proof.
iIntros "!> _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
......@@ -214,7 +214,7 @@ Section counter_proof.
Qed.
Lemma incr_spec l n :
{{ C l n }} incr #l {{ v, v = #() C l (S n) }}.
{{ C l n }} incr #l {{ v, v = #() C l (S n) }}.
Proof.
iIntros "!> Hl /=". iLöb as "IH". wp_rec.
iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
......@@ -239,7 +239,7 @@ Section counter_proof.
Check "read_spec".
Lemma read_spec l n :
{{ C l n }} read #l {{ v, m : nat, v = #m n m C l m }}.
{{ C l n }} read #l {{ v, m : nat, v = #m n m C l m }}.
Proof.
iIntros "!> Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
......
......@@ -88,7 +88,7 @@ Proof.
Qed.
Lemma ht_one_shot (Φ : val iProp Σ) :
{{ True }} one_shot_example #()
{{ True }} one_shot_example #()
{{ ff,
( n : Z, {{ True }} Fst ff #n {{ w, w = #true w = #false }})
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
......@@ -108,7 +108,7 @@ Definition client : expr :=
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
Lemma client_safe : WP client {{ _, True }}.
Proof using Type*.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
wp_let. wp_apply wp_par.
......
......@@ -105,7 +105,7 @@ Proof.
Qed.
Lemma ht_one_shot (Φ : val iProp Σ) :
{{ True }} one_shot_example #()
{{ True }} one_shot_example #()
{{ ff, T, T
( n : Z, {{ T }} Fst ff #n {{ _, True }})
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
......@@ -126,7 +126,7 @@ Definition client : expr :=
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
Lemma client_safe : WP client {{ _, True }}.
Proof using Type*.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
wp_let. wp_apply (wp_par with "[HT]").
......
......@@ -8,10 +8,10 @@ Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp P - P.
Proof. eauto 6. Qed.
Lemma test_eauto_isplit_biwand P : (P - P)%I.
Lemma test_eauto_isplit_biwand P : P - P.
Proof. eauto. Qed.
Fixpoint test_fixpoint (n : nat) {struct n} : True emp @{PROP} (n + 0)%nat = n %I.
Fixpoint test_fixpoint (n : nat) {struct n} : True emp @{PROP} (n + 0)%nat = n .
Proof.
case: n => [|n] /=; first (iIntros (_) "_ !%"; reflexivity).
iIntros (_) "_".
......@@ -53,7 +53,7 @@ Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
Lemma test_unfold_constants : bar.
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
Check "test_iStopProof".
......@@ -74,7 +74,7 @@ Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
P emp - emp Q - <affine> (P Q).
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P Q P Q)%I.
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P Q P Q).
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
......@@ -104,15 +104,15 @@ Qed.
Lemma test_iDestruct_spatial_noop Q : Q - Q.
Proof. iIntros "-#HQ". done. Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ ( φ P φ ψ P)%I.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ φ P φ ψ P.
Proof. iIntros (??) "H". auto. Qed.
Lemma test_iIntros_pure_not : ( ¬False : PROP)%I.
Lemma test_iIntros_pure_not : @{PROP} ¬False .
Proof. by iIntros (?). Qed.
Lemma test_fast_iIntros P Q :
( x y z : nat,
x = plus 0 x y = 0 z = 0 P Q foo (x x))%I.
x y z : nat,
x = plus 0 x y = 0 z = 0 P Q foo (x x).
Proof.
iIntros (a) "*".
iIntros "#Hfoo **".
......@@ -120,11 +120,11 @@ Proof.
Qed.
Lemma test_very_fast_iIntros P :
x y : nat, ( x = y P - P)%I.
x y : nat, x = y P - P.
Proof. by iIntros. Qed.
Definition tc_opaque_test : PROP := tc_opaque ( x : nat, x = x )%I.
Lemma test_iIntros_tc_opaque : tc_opaque_test.
Lemma test_iIntros_tc_opaque : tc_opaque_test.
Proof. by iIntros (x). Qed.
(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
......@@ -163,12 +163,12 @@ Lemma test_iSpecialize_auto_frame P Q R :
(P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
Lemma test_iSpecialize_pure (φ : Prop) Q R:
φ (⌜φ⌝ - Q) Q.
Lemma test_iSpecialize_pure (φ : Prop) Q R :
φ (⌜φ⌝ - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_Coq_entailment P Q R :
P (P - Q) Q.
( P) (P - Q) ( Q).
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_intuitionistic P Q R :
......@@ -271,7 +271,7 @@ Qed.
Lemma test_iExist_coercion (P : Z PROP) : ( x, P x) - x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
Lemma test_iExist_tc `{Set_ A C} P : ( x1 x2 : gset positive, P - P)%I.
Lemma test_iExist_tc `{Set_ A C} P : x1 x2 : gset positive, P - P.
Proof. iExists {[ 1%positive ]}, . auto. Qed.
Lemma test_iSpecialize_tc P : ( x y z : gset positive, P) - P.
......@@ -384,7 +384,7 @@ Proof.
iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.
Lemma test_iLöb P : ( n, ^n P)%I.
Lemma test_iLöb P : n, ^n P.
Proof.
iLöb as "IH". iDestruct "IH" as (n) "IH".
by iExists (S n).
......@@ -408,7 +408,7 @@ Proof.
Qed.
Lemma test_iIntros_start_proof :
(True : PROP)%I.
@{PROP} True.
Proof.
(* Make sure iIntros actually makes progress and enters the proofmode. *)
progress iIntros. done.
......@@ -437,7 +437,7 @@ Proof.
Qed.
Lemma test_iIntros_modalities `(!Absorbing P) :
(<pers> ( x : nat, x = 0 x = 0 - False - P - P))%I.
<pers> ( x : nat, x = 0 x = 0 - False - P - P).
Proof.
iIntros (x ??).
iIntros "* **". (* Test that fast intros do not work under modalities *)
......@@ -613,11 +613,11 @@ Check "test_iSimpl_in4".
Lemma test_iSimpl_in4 x y : (3 + x)%nat = y - S (S (S x)) = y : PROP.
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
Lemma test_iIntros_pure_neg : ( ¬False : PROP)%I.
Lemma test_iIntros_pure_neg : @{PROP} ¬False .
Proof. by iIntros (?). Qed.
Lemma test_iPureIntro_absorbing (φ : Prop) :
φ sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
φ @{PROP} <absorb> ⌜φ⌝.
Proof. intros ?. iPureIntro. done. Qed.