From 509a8e2acb908cdddd693d93a39ed317f30d8ab6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 7 Jun 2018 16:59:23 +0200
Subject: add test for #7595

---
 test-suite/misc/7595.sh     |  5 +++++
 test-suite/misc/7595/FOO.v  | 39 +++++++++++++++++++++++++++++++++++++++
 test-suite/misc/7595/base.v | 28 ++++++++++++++++++++++++++++
 3 files changed, 72 insertions(+)
 create mode 100755 test-suite/misc/7595.sh
 create mode 100644 test-suite/misc/7595/FOO.v
 create mode 100644 test-suite/misc/7595/base.v

(limited to 'test-suite/misc')

diff --git a/test-suite/misc/7595.sh b/test-suite/misc/7595.sh
new file mode 100755
index 000000000..836e354ee
--- /dev/null
+++ b/test-suite/misc/7595.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+set -e
+
+$coqc -R misc/7595 Test misc/7595/base.v
+$coqc -R misc/7595 Test misc/7595/FOO.v
diff --git a/test-suite/misc/7595/FOO.v b/test-suite/misc/7595/FOO.v
new file mode 100644
index 000000000..30c957d3b
--- /dev/null
+++ b/test-suite/misc/7595/FOO.v
@@ -0,0 +1,39 @@
+Require Import Test.base.
+
+Lemma dec_stable `{Decision P} : ¬¬P → P.
+Proof. firstorder. Qed.
+
+(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
+components is double negated, it will try to remove the double negation. *)
+Tactic Notation "destruct_decide" constr(dec) "as" ident(H) :=
+  destruct dec as [H|H];
+  try match type of H with
+  | ¬¬_ => apply dec_stable in H
+  end.
+Tactic Notation "destruct_decide" constr(dec) :=
+  let H := fresh in destruct_decide dec as H.
+
+
+(** * Monadic operations *)
+Instance option_guard: MGuard option := λ P dec A f,
+  match dec with left H => f H | _ => None end.
+
+(** * Tactics *)
+Tactic Notation "case_option_guard" "as" ident(Hx) :=
+  match goal with
+  | H : context C [@mguard option _ ?P ?dec] |- _ =>
+    change (@mguard option _ P dec) with (λ A (f : P → option A),
+      match @decide P dec with left H' => f H' | _ => None end) in *;
+    destruct_decide (@decide P dec) as Hx
+  | |- context C [@mguard option _ ?P ?dec] =>
+    change (@mguard option _ P dec) with (λ A (f : P → option A),
+      match @decide P dec with left H' => f H' | _ => None end) in *;
+    destruct_decide (@decide P dec) as Hx
+  end.
+Tactic Notation "case_option_guard" :=
+  let H := fresh in case_option_guard as H.
+
+(* This proof failed depending on the name of the module. *)
+Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
+  P → (guard P; mx) = mx.
+Proof. intros. case_option_guard. reflexivity. contradiction. Qed.
diff --git a/test-suite/misc/7595/base.v b/test-suite/misc/7595/base.v
new file mode 100644
index 000000000..6a6b7b79d
--- /dev/null
+++ b/test-suite/misc/7595/base.v
@@ -0,0 +1,28 @@
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+Set Default Proof Using "Type".
+Export ListNotations.
+From Coq.Program Require Export Basics Syntax.
+Global Generalizable All Variables.
+
+(** * Type classes *)
+(** ** Decidable propositions *)
+(** This type class by (Spitters/van der Weegen, 2011) collects decidable
+propositions. *)
+Class Decision (P : Prop) := decide : {P} + {¬P}.
+Hint Mode Decision ! : typeclass_instances.
+Arguments decide _ {_} : simpl never, assert.
+
+(** ** Proof irrelevant types *)
+(** This type class collects types that are proof irrelevant. That means, all
+elements of the type are equal. We use this notion only used for propositions,
+but by universe polymorphism we can generalize it. *)
+Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
+Hint Mode ProofIrrel ! : typeclass_instances.
+
+Class MGuard (M : Type → Type) :=
+  mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
+Arguments mguard _ _ _ !_ _ _ / : assert.
+Notation "'guard' P ; z" := (mguard P (λ _, z))
+  (at level 20, z at level 200, only parsing, right associativity) .
+Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
+  (at level 20, z at level 200, only parsing, right associativity) .
-- 
cgit v1.2.3