helm/software/matita/nlibrary/basics/eq.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/relations.ma".
  16
  17 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
  18
  19 ntheorem reflexive_eq : ∀A:Type. reflexive A (eq A).
  20 //; nqed.
  21
  22 ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
  23 //; nqed.
  24
  25 ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
  26 #A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
  27
  28 (*
  29 ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
  30 /3/; nqed.
  31 *)
  32
  33 ntheorem symmetric_not_eq: ∀A:Type. ∀x,y:A. x ≠ y → y ≠ x.
  34 /3/; nqed.
  35
  36 (*
  37 #A; #x; #y; #H; #K; napply H; napply symmetric_eq; //; nqed.
  38 *)
  39
  40 ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y.
  41 #A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.
  42
  43 (*
  44 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
  45 \forall x,y:A. x=y \to f y = f x.
  46 intros.elim H.apply refl_eq.
  47 qed. *)
  48
  49 ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
  50 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
  51 #A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
  52 nqed.