]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/decidable_kit/streicher.ma
demodulate takes an extra argument 'all', if present it attempts to solve
[helm.git] / helm / software / matita / library / decidable_kit / streicher.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 "logic/equality.ma".
17
18 definition step ≝ λT:Type.λa,b,c:T.λH1:a=b.λH2:a=c. eq_ind T ? (λx.b = x) H1 ? H2.
19
20 lemma stepH : ∀T:Type.∀a:T.∀H:a=a. step ? ? ? ? H H = refl_eq T a.
21 intros (T a H); cases H; reflexivity.
22 qed.
23
24 definition decT ≝ λT:Type.∀x,y:T. decidable (x=y).
25
26 lemma nu : ∀T:Type.∀a,b:T. decT T → ∀E:a=b. a=b.
27 intros (T a b decT E); cases (decT a b) (Ecanonical Abs); [ exact Ecanonical | cases (Abs E) ]
28 qed.
29
30 lemma nu_k : ∀T:Type.∀a,b:T.∀E1,E2:a=b. ∀d : decT T. nu ? ? ? d E1 = nu ? ? ? d E2.
31 intros (T a b E1 E2 decT); unfold nu; 
32 cases (decT a b); simplify; [ reflexivity | cases (H E1) ]
33 qed.
34
35 definition nu_inv ≝ λT:Type.λa,b:T. λd: decT T.λE:a=b. 
36   step ? ? ? ? (nu ? ? ? d (refl_eq ? a)) E. 
37
38 definition cancel ≝ λT:Type.λA,B:Type.λf.λg:A→B.∀x:A.f (g x) = x.
39
40 (* non inferisce Prop?!??! *)
41 lemma cancel_nu_nu_inv : ∀T:Type.∀a,b:T.∀d: decT T. 
42   cancel Prop (a=b) (a=b) (nu_inv ? a b d) (nu ? a b d).
43 intros (T a b); unfold cancel; intros (E); cases E;
44 unfold nu_inv; rewrite > stepH; reflexivity.
45 qed.
46
47 theorem pirrel :  ∀T:Type.∀a,b:T.∀E1,E2:a=b.∀d: decT T. E1 = E2.
48 intros (T a b E1 E2 decT);
49 rewrite < (cancel_nu_nu_inv ? ? ? decT); 
50 rewrite < (cancel_nu_nu_inv ? ? ? decT) in ⊢ (? ? ? %);
51 rewrite > (nu_k ? ? ? E1 E2 decT).
52 reflexivity.
53 qed.
54