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 "logic/pts.ma".
17 ninductive eq (A:Type[3]) (x:A) : A → Prop ≝
20 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
23 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl_eq A a) → P x p.
24 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
28 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
29 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
34 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
35 #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
36 ncases p0; #Heq; nassumption.
40 ntheorem rewrite_l: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
41 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
44 ntheorem sym_eq: ∀A:Type[3].∀x,y:A. x = y → y = x.
45 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
46 ##[ @; ##| nassumption; ##]
49 ntheorem rewrite_r: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
50 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
53 ntheorem eq_coerc: ∀A,B:Type[2].A→(A=B)→B.
54 #A; #B; #Ha; #Heq;nelim Heq; nassumption.