From 9714dfdb3f2c98c665f403e45c5875b4739e68c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Jan 2020 20:39:13 +0100
Subject: [PATCH] Add some basic tests for the `siProp` proofmode.

---
 tests/proofmode_siprop.ref |  0
 tests/proofmode_siprop.v   | 22 ++++++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 tests/proofmode_siprop.ref
 create mode 100644 tests/proofmode_siprop.v

diff --git a/tests/proofmode_siprop.ref b/tests/proofmode_siprop.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
new file mode 100644
index 000000000..d9dc2c4e8
--- /dev/null
+++ b/tests/proofmode_siprop.v
@@ -0,0 +1,22 @@
+From iris.proofmode Require Import tactics .
+From iris.si_logic Require Import bi.
+Set Ltac Backtrace.
+
+Section si_logic_tests.
+  Implicit Types P Q R : siProp.
+
+  Lemma test_everything_persistent P : P -∗ P.
+  Proof. by iIntros "#HP". Qed.
+
+  Lemma test_everything_affine P : P -∗ True.
+  Proof. by iIntros "_". Qed.
+
+  Lemma test_iIntro_impl P Q R : (P → Q ∧ R → P ∧ R)%I.
+  Proof. iIntros "#HP #[HQ HR]". auto. Qed.
+
+  Lemma test_iApply_impl_1 P Q R : (P → (P → Q) → Q)%I.
+  Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
+
+  Lemma test_iApply_impl_2 P Q R : (P → (P → Q) → Q)%I.
+  Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
+End si_logic_tests.
-- 
GitLab