From e6b5e0c964fd9a5018ff8c1f258c09e47e9657a7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Feb 2018 17:42:08 +0100
Subject: [PATCH] Add non backtracking `TCIf` type class.

---
 theories/base.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 4dcc5852..12e6afd7 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -62,6 +62,20 @@ of this type class. *)
 Class NoBackTrack (P : Prop) := { no_backtrack : P }.
 Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
 
+(* 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.
+
 (** * Typeclass opaque definitions *)
 (** The constant [tc_opaque] is used to make definitions opaque for just type
 class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
-- 
GitLab