helm/software/matita/nlibrary/logic/equality.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/connectives.ma".
  16 include "properties/relations.ma".
  17
  18 ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  19  refl: eq A a a.
  20
  21 nlemma eq_rect_CProp0_r':
  22  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
  23  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
  24 nqed.
  25
  26 nlemma eq_rect_CProp0_r:
  27  ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  28  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
  29 nqed.
  30
  31 nlemma eq_ind_r :
  32  ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  33  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
  34 nqed.
  35
  36 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  37
  38 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
  39
  40 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
  41  #A; napply mk_equivalence_relation
  42   [ napply eq
  43   | napply refl
  44   | #x; #y; #H; nrewrite < H; napply refl
  45   | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
  46 nqed.