Commit d52fc276 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Add some tests.

parent a1f630a6
......@@ -97,6 +97,7 @@ theories/tests/heap_lang.v
theories/tests/one_shot.v
theories/tests/proofmode.v
theories/tests/proofmode_iris.v
theories/tests/proofmode_monPred.v
theories/tests/list_reverse.v
theories/tests/tree_sum.v
theories/tests/ipm_paper.v
......
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic lib.invariants.
Section tests.
Context {I : bi_index} {PROP : sbi}.
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 i j : I.
Lemma test0 P : P - P.
Proof. iIntros "$". Qed.
Lemma test_iStartProof_1 P : P - P.
Proof. iStartProof. iStartProof. iIntros "$". Qed.
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.
Lemma test_iStartProof_4 P : P - P.
Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
Lemma test_iStartProof_5 P : P - P.
Proof. iStartProof PROP. iIntros (i) "$". Qed.
Lemma test_iStartProof_6 P : P P.
Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
Lemma test_iStartProof_7 P : ((P P)%I : monPredI).
Proof. iStartProof PROP. done. Qed.
End tests.
\ No newline at end of file
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