From ea64fd148b56e1c38c08c2954e76bfa2e75b4db9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Feb 2017 19:11:27 +0100
Subject: [PATCH] Let iAssumption succeed when there is H : False.
---
theories/proofmode/class_instances.v | 2 ++
theories/tests/proofmode.v | 3 +++
2 files changed, 5 insertions(+)
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b623f0d48..7694c59b6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -10,6 +10,8 @@ Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
(* FromAssumption *)
+Global Instance from_assumption_False p P : FromAssumption p False P.
+Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
Global Instance from_assumption_exact p P : FromAssumption p P P.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
Global Instance from_assumption_always_l p P Q :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 8a884b3d7..63b55ce51 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -127,3 +127,6 @@ Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) -∗ |==> P.
Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
+
+Lemma demo_14 (M : ucmraT) (P : uPred M) : False -∗ P.
+Proof. iIntros "H". done. Qed.
--
GitLab