Commit 1c1ae879 authored by Ralf Jung's avatar Ralf Jung

proofmode tests: use a section

parent 1edf71ef
......@@ -2,7 +2,9 @@ From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import invariants.
Set Default Proof Using "Type".
Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
Section tests.
Context {M : ucmraT}.
Lemma demo_0 (P Q : uPred M) :
(P Q) - ( x, x = 0 x = 1) (Q P).
Proof.
iIntros "#H #H2".
......@@ -12,7 +14,7 @@ Proof.
iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.
Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat uPred M) :
Lemma demo_1 (P1 P2 P3 : nat uPred M) :
( (x y : nat) a b,
x y
(uPred_ownM (a b) -
......@@ -37,7 +39,7 @@ Proof.
- done.
Qed.
Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat uPredC M):
Lemma demo_2 (P1 P2 P3 P4 Q : uPred M) (P5 : nat uPredC M):
P2 (P3 Q) True P1 P2 (P4 ( x:nat, P5 x P3)) True -
P1 - (True True) -
(((P2 False P2 0 = 0) P3) Q P1 True)
......@@ -55,17 +57,17 @@ Proof.
* iSplitL "HQ". iAssumption. by iSplitL "H1".
Qed.
Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
Lemma demo_3 (P1 P2 P3 : uPred M) :
P1 P2 P3 - P1 (P2 x, (P3 x = 0) P3).
Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
Definition foo {M} (P : uPred M) := (P P)%I.
Definition bar {M} : uPred M := ( P, foo P)%I.
Definition foo (P : uPred M) := (P P)%I.
Definition bar : uPred M := ( P, foo P)%I.
Lemma demo_4 (M : ucmraT) : True - @bar M.
Lemma demo_4 : True - bar.
Proof. iIntros. iIntros (P) "HP //". Qed.
Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
Lemma demo_5 (x y : M) (P : uPred M) :
( z, P z y) - (P - (x,x) (y,x)).
Proof.
iIntros "H1 H2".
......@@ -74,7 +76,7 @@ Proof.
done.
Qed.
Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
Lemma demo_6 (P Q : uPred M) :
( x y z : nat,
x = plus 0 x y = 0 z = 0 P Q foo (x x))%I.
Proof.
......@@ -83,7 +85,7 @@ Proof.
iIntros "# _ //".
Qed.
Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P (Q1 Q2) - P Q1.
Lemma demo_7 (P Q1 Q2 : uPred M) : P (Q1 Q2) - P Q1.
Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
Section iris.
......@@ -101,11 +103,11 @@ Section iris.
Qed.
End iris.
Lemma demo_9 (M : ucmraT) (x y z : M) :
Lemma demo_9 (x y z : M) :
x y z - ( x x y z : uPred M).
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
Lemma demo_10 (M : ucmraT) (P Q : uPred M) : P - Q - True.
Lemma demo_10 (P Q : uPred M) : P - Q - True.
Proof.
iIntros "HP HQ".
iAssert True%I as "#_". { by iClear "HP HQ". }
......@@ -115,44 +117,44 @@ Proof.
done.
Qed.
Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
Lemma demo_11 (P Q R : uPred M) :
(P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
(* Check coercions *)
Lemma demo_12 (M : ucmraT) (P : Z uPred M) : ( x, P x) - x, P x.
Lemma demo_12 (P : Z uPred M) : ( x, P x) - x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) - |==> P.
Lemma demo_13 (P : uPred M) : (|==> False) - |==> P.
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
Lemma demo_14 (M : ucmraT) (P : uPred M) : False - P.
Lemma demo_14 (P : uPred M) : False - P.
Proof. iIntros "H". done. Qed.
(* Check instantiation and dependent types *)
Lemma demo_15 (M : ucmraT) (P : n, vec nat n uPred M) :
Lemma demo_15 (P : n, vec nat n uPred M) :
( n v, P n v) - n v, P n v.
Proof.
iIntros "H". iExists _, [#10].
iSpecialize ("H" $! _ [#10]). done.
Qed.
Lemma demo_16 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
Lemma demo_16 (P Q R : uPred M) `{!PersistentP R} :
P - Q - R - R Q P R False.
Proof. eauto with iFrame. Qed.
Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
Lemma demo_17 (P Q R : uPred M) `{!PersistentP R} :
P - Q - R - R Q P R False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
Lemma test_iNext_evar (M : ucmraT) (P : uPred M) :
Lemma test_iNext_evar (P : uPred M) :
P - True.
Proof.
iIntros "HP". iAssert ( _ - P)%I as "?"; last done.
iIntros "?". iNext. iAssumption.
Qed.
Lemma test_iNext_sep1 (M : ucmraT) (P Q : uPred M)
Lemma test_iNext_sep1 (P Q : uPred M)
(R1 := (P Q)%I) (R2 := ( P Q)%I) :
( P Q) R1 R2 - (P Q) R1 R2.
Proof.
......@@ -160,16 +162,18 @@ Proof.
rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
Lemma test_iNext_sep2 (M : ucmraT) (P Q : uPred M) :
Lemma test_iNext_sep2 (P Q : uPred M) :
P Q - (P Q).
Proof.
iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
Lemma test_frame_persistent (M : ucmraT) (P Q : uPred M) :
Lemma test_frame_persistent (P Q : uPred M) :
P - Q - (P P) (P Q Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
Lemma test_split_box (M : ucmraT) (P Q : uPred M) :
Lemma test_split_box (P Q : uPred M) :
P - (P P).
Proof. iIntros "#?". by iSplit. Qed.
End tests.
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