(**************************************************************************) (* ___ *) (* ||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 *) (* 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. *)