From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 test-suite/typeclasses/NewSetoid.v | 74 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 test-suite/typeclasses/NewSetoid.v

(limited to 'test-suite/typeclasses/NewSetoid.v')

diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
new file mode 100644
index 00000000..8ad03880
--- /dev/null
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certified Haskell Prelude.
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Import Coq.Classes.SetoidTactics.
+
+Goal not True == not (not False) -> ((not True -> True)) \/ True.
+  intros.
+  clrewrite H.
+  clrewrite <- H.
+  right ; auto.
+Defined.
+
+Definition reduced_thm := Eval compute in Unnamed_thm.
+
+(* Print reduced_thm. *)
+
+Lemma foo [ Setoid a R ] : True. (* forall x y, R x y -> x -> y. *)
+Proof.
+  intros.
+  Print respect2.
+  pose setoid_morphism.
+  pose (respect2 (b0:=b)).
+  simpl in b0.
+  unfold binary_respectful in b0.
+  pose (arrow_morphism R).
+  pose (respect2 (b0:=b1)).
+  unfold binary_respectful in b2.
+
+  pose (eq_morphism (A:=a)).
+  pose (respect2 (b0:=b3)).
+  unfold binary_respectful in b4.
+  exact I.
+Qed.
+
+Goal forall A B C (H : A <-> B) (H' : B <-> C), A /\ B <-> B /\ C.
+  intros.
+  Set Printing All.
+  Print iff_morphism.
+  clrewrite H.
+  clrewrite H'.
+  reflexivity.
+Defined.
+
+Goal forall A B C (H : A <-> B) (H' : B <-> C), A /\ B <-> B /\ C.
+  intros.
+  rewrite H.
+  rewrite H'.
+  reflexivity.
+Defined.
+
+Require Import Setoid_tac.
+Require Import Setoid_Prop.
+
+(* Print Unnamed_thm0. *)
+(* Print Unnamed_thm1. *)
+
+
-- 
cgit v1.2.3