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