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