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