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 (* this is refl
  20 ntheorem reflexive_eq : ∀A:Type. reflexive A (eq A).
  21 //; nqed. *)
  22
  23 (* this is sym_eq
  24 ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
  25 //; nqed. *)
  26
  27 ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
  28 #A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
  29
  30 (*
  31 ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
  32 /3/; nqed.
  33 *)
  34
  35 ntheorem symmetric_not_eq: ∀A:Type. ∀x,y:A. x ≠ y → y ≠ x.
  36 /3/; nqed.
  37
  38 (*
  39 #A; #x; #y; #H; #K; napply H; napply symmetric_eq; //; nqed.
  40 *)
  41
  42 ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y.
  43 #A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.
  44
  45 (*
  46 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
  47 \forall x,y:A. x=y \to f y = f x.
  48 intros.elim H.apply refl_eq.
  49 qed. *)
  50
  51 (* deleterio per auto*)
  52 ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
  53 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
  54 #A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
  55 nqed.