From ad435a84b5cf45dab2844f9135cc742d895bc771 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Sep 2020 15:00:11 +0200
Subject: [PATCH] Tests for `clProp` proof mode.
---
tests/proofmode_clprop.ref | 0
tests/proofmode_clprop.v | 33 +++++++++++++++++++++++++++++++++
2 files changed, 33 insertions(+)
create mode 100644 tests/proofmode_clprop.ref
create mode 100644 tests/proofmode_clprop.v
diff --git a/tests/proofmode_clprop.ref b/tests/proofmode_clprop.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/proofmode_clprop.v b/tests/proofmode_clprop.v
new file mode 100644
index 000000000..3fab654f3
--- /dev/null
+++ b/tests/proofmode_clprop.v
@@ -0,0 +1,33 @@
+From iris.proofmode Require Import tactics.
+From iris.cl_logic Require Import bi.
+
+Section si_logic_tests.
+ Implicit Types P Q R : clProp.
+
+ 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.
+ Proof. iIntros "#HP #[HQ HR]". auto. Qed.
+
+ Lemma test_iApply_impl_1 P Q R : ⊢ P → (P → Q) → Q.
+ Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
+
+ Lemma test_iApply_impl_2 P Q R : ⊢ P → (P → Q) → Q.
+ Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
+
+ Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P.
+ Proof.
+ iApply clProp.dn; iIntros "#H". iApply "H".
+ iRight. iIntros "HP". iApply "H". auto.
+ Qed.
+
+ Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P.
+ Proof.
+ iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP".
+ iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %[].
+ Qed.
+End si_logic_tests.
--
GitLab