--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "Coq.ma".
+
+(*#**********************************************************************)
+
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+
+(* \VV/ *************************************************************)
+
+(* // * This file is distributed under the terms of the *)
+
+(* * GNU Lesser General Public License Version 2.1 *)
+
+(*#**********************************************************************)
+
+(*i $Id: Logic.v,v 1.29 2004/03/29 09:40:49 herbelin Exp $ i*)
+
+(* UNEXPORTED
+Set Implicit Arguments.
+*)
+
+include "Init/Notations.ma".
+
+(*#* * Propositional connectives *)
+
+(*#* [True] is the always true proposition *)
+
+inline procedural "cic:/Coq/Init/Logic/True.ind".
+
+(*#* [False] is the always false proposition *)
+
+inline procedural "cic:/Coq/Init/Logic/False.ind".
+
+(*#* [not A], written [~A], is the negation of [A] *)
+
+inline procedural "cic:/Coq/Init/Logic/not.con" as definition.
+
+(* NOTATION
+Notation "~ x" := (not x) : type_scope.
+*)
+
+(* UNEXPORTED
+Hint Unfold not: core.
+*)
+
+inline procedural "cic:/Coq/Init/Logic/and.ind".
+
+(* UNEXPORTED
+Section Conjunction
+*)
+
+(*#* [and A B], written [A /\ B], is the conjunction of [A] and [B]
+
+ [conj p q] is a proof of [A /\ B] as soon as
+ [p] is a proof of [A] and [q] a proof of [B]
+
+ [proj1] and [proj2] are first and second projections of a conjunction *)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Conjunction/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Conjunction/B.var
+*)
+
+inline procedural "cic:/Coq/Init/Logic/proj1.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/proj2.con" as theorem.
+
+(* UNEXPORTED
+End Conjunction
+*)
+
+(*#* [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
+
+inline procedural "cic:/Coq/Init/Logic/or.ind".
+
+(*#* [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
+
+inline procedural "cic:/Coq/Init/Logic/iff.con" as definition.
+
+(* NOTATION
+Notation "A <-> B" := (iff A B) : type_scope.
+*)
+
+(* UNEXPORTED
+Section Equivalence
+*)
+
+inline procedural "cic:/Coq/Init/Logic/iff_refl.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/iff_trans.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/iff_sym.con" as theorem.
+
+(* UNEXPORTED
+End Equivalence
+*)
+
+(*#* [(IF_then_else P Q R)], written [IF P then Q else R] denotes
+ either [P] and [Q], or [~P] and [Q] *)
+
+inline procedural "cic:/Coq/Init/Logic/IF_then_else.con" as definition.
+
+(* NOTATION
+Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
+ (at level 200) : type_scope.
+*)
+
+(*#* * First-order quantifiers
+ - [ex A P], or simply [exists x, P x], expresses the existence of an
+ [x] of type [A] which satisfies the predicate [P] ([A] is of type
+ [Set]). This is existential quantification.
+ - [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the
+ existence of an [x] of type [A] which satisfies both the predicates
+ [P] and [Q].
+ - Universal quantification (especially first-order one) is normally
+ written [forall x:A, P x]. For duality with existential quantification,
+ the construction [all P] is provided too.
+*)
+
+inline procedural "cic:/Coq/Init/Logic/ex.ind".
+
+inline procedural "cic:/Coq/Init/Logic/ex2.ind".
+
+inline procedural "cic:/Coq/Init/Logic/all.con" as definition.
+
+(* Rule order is important to give printing priority to fully typed exists *)
+
+(* NOTATION
+Notation "'exists' x , p" := (ex (fun x => p))
+ (at level 200, x ident) : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists' x : t , p" := (ex (fun x:t => p))
+ (at level 200, x ident, format "'exists' '/ ' x : t , '/ ' p")
+ : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
+ (at level 200, x ident, p at level 200) : type_scope.
+*)
+
+(* NOTATION
+Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
+ (at level 200, x ident, t at level 200, p at level 200,
+ format "'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']'")
+ : type_scope.
+*)
+
+(*#* Derived rules for universal quantification *)
+
+(* UNEXPORTED
+Section universal_quantification
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/universal_quantification/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/universal_quantification/P.var
+*)
+
+inline procedural "cic:/Coq/Init/Logic/inst.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/gen.con" as theorem.
+
+(* UNEXPORTED
+End universal_quantification
+*)
+
+(*#* * Equality *)
+
+(*#* [eq x y], or simply [x=y], expresses the (Leibniz') equality
+ of [x] and [y]. Both [x] and [y] must belong to the same type [A].
+ The definition is inductive and states the reflexivity of the equality.
+ The others properties (symmetry, transitivity, replacement of
+ equals) are proved below. The type of [x] and [y] can be made explicit
+ using the notation [x = y :> A] *)
+
+inline procedural "cic:/Coq/Init/Logic/eq.ind".
+
+(* NOTATION
+Notation "x = y" := (x = y :>_) : type_scope.
+*)
+
+(* NOTATION
+Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
+*)
+
+(* NOTATION
+Notation "x <> y" := (x <> y :>_) : type_scope.
+*)
+
+(* UNEXPORTED
+Implicit Arguments eq_ind [A].
+*)
+
+(* UNEXPORTED
+Implicit Arguments eq_rec [A].
+*)
+
+(* UNEXPORTED
+Implicit Arguments eq_rect [A].
+*)
+
+(* UNEXPORTED
+Hint Resolve I conj or_introl or_intror refl_equal: core v62.
+*)
+
+(* UNEXPORTED
+Hint Resolve ex_intro ex_intro2: core v62.
+*)
+
+(* UNEXPORTED
+Section Logic_lemmas
+*)
+
+inline procedural "cic:/Coq/Init/Logic/absurd.con" as theorem.
+
+(* UNEXPORTED
+Section equality
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var
+*)
+
+inline procedural "cic:/Coq/Init/Logic/sym_eq.con" as theorem.
+
+(* UNEXPORTED
+Opaque sym_eq.
+*)
+
+inline procedural "cic:/Coq/Init/Logic/trans_eq.con" as theorem.
+
+(* UNEXPORTED
+Opaque trans_eq.
+*)
+
+inline procedural "cic:/Coq/Init/Logic/f_equal.con" as theorem.
+
+(* UNEXPORTED
+Opaque f_equal.
+*)
+
+inline procedural "cic:/Coq/Init/Logic/sym_not_eq.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/sym_equal.con" as definition.
+
+inline procedural "cic:/Coq/Init/Logic/sym_not_equal.con" as definition.
+
+inline procedural "cic:/Coq/Init/Logic/trans_equal.con" as definition.
+
+(* UNEXPORTED
+End equality
+*)
+
+(* Is now a primitive principle
+ Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
+ Proof.
+ Intros.
+ Cut (identity A x y).
+ NewDestruct 1; Auto.
+ NewDestruct H; Auto.
+ Qed.
+*)
+
+inline procedural "cic:/Coq/Init/Logic/eq_ind_r.con" as definition.
+
+inline procedural "cic:/Coq/Init/Logic/eq_rec_r.con" as definition.
+
+inline procedural "cic:/Coq/Init/Logic/eq_rect_r.con" as definition.
+
+(* UNEXPORTED
+End Logic_lemmas
+*)
+
+inline procedural "cic:/Coq/Init/Logic/f_equal2.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/f_equal3.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/f_equal4.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Logic/f_equal5.con" as theorem.
+
+(* UNEXPORTED
+Hint Immediate sym_eq sym_not_eq: core v62.
+*)
+
projects / helm.git / blobdiff