1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/test/".
17 include "logic/connectives.ma".
18 include "logic/equality.ma".
22 definition step ≝ λa,b,c:T.λH1:a=b.λH2:a=c. eq_ind T ? (λx.b = x) H1 ? H2.
24 lemma stepH : ∀a:T.∀H:a=a. step ? ? ? H H = refl_eq T a.
25 intros (a H); cases H; reflexivity.
28 axiom decT : ∀a,b:T. a = b ∨ a ≠ b.
30 lemma nu : ∀a,b:T. ∀E:a=b. a=b.
31 intros (a b E); cases (decT a b) (Ecanonical Abs); [ exact H | cases (H E) ]
34 lemma nu_k : ∀a,b:T. ∀E1,E2:a=b. nu ? ? E1 = nu ? ? E2.
35 intros (a b E1 E2); unfold nu;
36 cases (decT a b); simplify; [ reflexivity | cases (H E1) ]
39 definition nu_inv ≝ λa,b:T. λE:a=b. step ? ? ? (nu ? ? (refl_eq ? a)) E.
41 definition cancel ≝ λA,B:Type.λf.λg:A→B.∀x:A.f (g x) = x.
43 lemma cancel_nu_nu_inv : ∀a,b:T. cancel (a=b) (a=b) (nu_inv a b) (nu a b).
44 intros (a b); unfold cancel; intros (E); cases E;
45 unfold nu_inv; rewrite > stepH; reflexivity.
48 lemma pirrel : ∀a,b:T.∀E1,E2:a=b. E1 = E2.
50 rewrite < cancel_nu_nu_inv;
51 rewrite < cancel_nu_nu_inv in ⊢ (? ? ? %);
52 rewrite > (nu_k ? ? E1 E2).
57 inductive eq4 (A : Type) (x : A) (y : A) : A → A → Prop ≝
58 eq_refl4 : eq4 A x y x y.
60 lemma step4 : ∀a,b:T.∀H:eq4 T a b a b.
61 eq4_ind T a b (λx,y.eq4 T x y a b) H a b H = eq_refl4 T a b.
62 intros (a b H). cases H. reflexivity.