From 0505dc66385647feecbacc1d93687b53450eceff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Feb 2018 22:45:29 +0100
Subject: [PATCH] Type-class based conditional `TCIf P Q R` that does not
 backtrack on `P`.

---
 theories/proofmode/class_instances.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 6777c7688..dae05433d 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -5,6 +5,21 @@ From iris.base_logic Require Import big_op tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
+(* FIXME: Move to stdpp *)
+(* A conditional at the type class level. Note that [TCIf P Q R] is not the same
+as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
+establish [R], i.e. does not have the behavior of a conditional. Furthermore,
+note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
+would not be able to proof the negation of [P]. *)
+Inductive TCIf (P Q R : Prop) :=
+  | TCIf_true : P → Q → TCIf P Q R
+  | TCIf_false : R → TCIf P Q R.
+Existing Class TCIf.
+
+Hint Extern 0 (TCIf _ _ _) =>
+  first [apply TCIf_true; [apply _|]
+        |apply TCIf_false] : typeclass_instances.
+
 Section classes.
 Context {M : ucmraT}.
 Implicit Types P Q R : uPred M.
-- 
GitLab