1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Certified Haskell Prelude.
10
* Author: Matthieu Sozeau
11
* Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
12
* 91405 Orsay, France *)
14
(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
16
Require Import Coq.Program.Program.
18
Set Implicit Arguments.
19
Unset Strict Implicit.
21
Require Import Coq.Classes.SetoidTactics.
23
Goal not True == not (not False) -> ((not True -> True)) \/ True.
30
Definition reduced_thm := Eval compute in Unnamed_thm.
32
(* Print reduced_thm. *)
34
Lemma foo [ Setoid a R ] : True. (* forall x y, R x y -> x -> y. *)
39
pose (respect2 (b0:=b)).
41
unfold binary_respectful in b0.
42
pose (arrow_morphism R).
43
pose (respect2 (b0:=b1)).
44
unfold binary_respectful in b2.
46
pose (eq_morphism (A:=a)).
47
pose (respect2 (b0:=b3)).
48
unfold binary_respectful in b4.
52
Goal forall A B C (H : A <-> B) (H' : B <-> C), A /\ B <-> B /\ C.
61
Goal forall A B C (H : A <-> B) (H' : B <-> C), A /\ B <-> B /\ C.
68
Require Import Setoid_tac.
69
Require Import Setoid_Prop.
71
(* Print Unnamed_thm0. *)
72
(* Print Unnamed_thm1. *)