helm/software/matita/library/decidable_kit/eqtype.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 "decidable_kit/decidable.ma".
  16 include "datatypes/constructors.ma".
  17
  18 (* ### types with a decidable AND rewrite (leibniz) compatible ### *)
  19
  20 definition eq_compatible ≝ λT:Type.λa,b:T. reflect (a = b).
  21
  22 record eqType : Type ≝ {
  23   sort :> Type;
  24   cmp : sort → sort → bool ;
  25   eqP : ∀x,y:sort. eq_compatible sort x y (cmp x y)
  26 }.
  27
  28 lemma cmp_refl : ∀d:eqType.∀x. cmp d x x = true.
  29 intros (d x); generalize in match (eqP d x x); intros (H);
  30 unfold in H; (* inversion non fa whd!!! *)
  31 inversion H; [ intros; reflexivity | intros (ABS); cases (ABS (refl_eq ? ?)) ]
  32 qed.
  33
  34 (* to use streicher *)
  35 lemma eqType_decidable : ∀d:eqType. decT d.
  36 intros (d); unfold decT; intros (x y); unfold decidable;
  37 generalize in match (eqP d x y); intros (H);
  38 cases H; [left | right] assumption;
  39 qed.
  40
  41 lemma eqbP : ∀x,y:nat. eq_compatible nat x y (eqb x y).
  42 intros (x y);
  43 generalize in match (refl_eq ? (eqb x y));
  44 generalize in match (eqb x y) in ⊢ (? ? ? % → %); intros 1 (b);
  45 cases b; intros (H); [ apply reflect_true | apply reflect_false ];
  46 [ apply (eqb_true_to_eq ? ? H) | apply (eqb_false_to_not_eq ? ? H) ]
  47 qed.
  48
  49 definition nat_eqType : eqType ≝ mk_eqType ? ? eqbP.
  50 (* XXX le coercion nel cast non vengono inserite *)
  51 definition nat_canonical_eqType : nat → nat_eqType :=
  52   λn : nat.(n : sort nat_eqType).
  53 coercion nat_canonical_eqType.
  54
  55 definition bcmp ≝ λx,y:bool. match x with [ true ⇒ y | false => notb y ].
  56
  57 lemma bcmpP : ∀x,y:bool. eq_compatible bool x y (bcmp x y).
  58 intros (x y);
  59 generalize in match (refl_eq ? (bcmp x y));
  60 generalize in match (bcmp x y) in ⊢ (? ? ? % → %); intros 1 (b);
  61 cases b; intros (H); [ apply reflect_true | apply reflect_false ];
  62 generalize in match H; clear H;
  63 cases x; cases y; simplify; intros (H); [1,4: reflexivity];
  64 (* non va: try destruct H; *)
  65 [1,2,3,6: destruct H | *: unfold Not; intros (H1); destruct H1]
  66 qed.
  67
  68 definition bool_eqType : eqType ≝  mk_eqType ? ? bcmpP.
  69 definition bool_canonical_eqType : bool → bool_eqType :=
  70   λb : bool.(b : sort bool_eqType).
  71 coercion bool_canonical_eqType.
  72
  73 (* ### subtype of an eqType ### *)
  74
  75 record sigma (d : eqType) (p : d -> bool) : Type ≝ {
  76   sval : d;
  77   sprop : p sval = true
  78 }.
  79
  80 notation "{x, h}"
  81   right associative with precedence 80
  82 for @{'sig $x $h}.
  83
  84 interpretation "sub_eqType" 'sig x h =  (mk_sigma ? ? x h).
  85
  86 (* restricting an eqType gives an eqType *)
  87 lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p.
  88   eq_compatible ? x y (cmp ? (sval ? ? x) (sval ? ?y)).
  89 intros (d p x y);
  90 cases (eqP d (sval ? ? x) (sval ? ? y)); generalize in match H; clear H;
  91 cases x (s ps); cases y (t pt); simplify; intros (Est);
  92 [1: constructor 1; generalize in match ps; rewrite > Est; intros (pt');
  93     rewrite < (pirrel ? ? ? pt pt' (eqType_decidable bool_eqType)); reflexivity;
  94 |2: constructor 2; unfold Not; intros (H); destruct H;
  95     cases (Est); reflexivity]
  96 qed.
  97
  98 definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
  99
 100 inductive in_sub (d : eqType) (p : d → bool) (x : d) : option (sigma d p) → Type ≝
 101 | in_sig : ∀s : sigma d p. sval ? ? s = x → in_sub d p x (Some ? s)
 102 | out_sig : p x = false → in_sub d p x (None ?).
 103
 104 definition if_p ≝ λd:eqType.λp:d→bool.λx:d.
 105   match (eqP bool_eqType (p x) true) with
 106   [ (reflect_true H) ⇒ Some ? {?,H}
 107   | (reflect_false _) ⇒ None ?].
 108
 109 lemma in_sub_eq : ∀d,p,x. in_sub d p x (if_p d p x).
 110 intros (d p x); unfold if_p;
 111 cases (eqP bool_eqType (p x) true); simplify;
 112 [ apply in_sig; reflexivity; | apply out_sig; apply (p2bF ? ? (idP ?) H)]
 113 qed.
 114
 115 definition ocmp : ∀d:eqType.∀a,b:option d.bool ≝
 116   λd:eqType.λa,b:option d.
 117   match a with
 118   [ None ⇒ match b with [ None ⇒ true | (Some _) ⇒ false]
 119   | (Some x) ⇒ match b with [ None ⇒ false | (Some y) ⇒ cmp d x y]].
 120
 121 lemma ocmpP : ∀d:eqType.∀a,b:option d.eq_compatible ? a b (ocmp d a b).
 122 intros (d a b);
 123 generalize in match (refl_eq ? (ocmp ? a b));
 124 generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c);
 125 cases c; intros (H); [ apply reflect_true | apply reflect_false ];
 126 generalize in match H; clear H;
 127 cases a; cases b; simplify; intros (H);
 128 [1: reflexivity;
 129 |2,3,5: destruct H;
 130 |4: rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity;
 131 |6,7: unfold Not; intros (H1); destruct H1
 132 |8: unfold Not; intros (H1); destruct H1;rewrite > cmp_refl in H; destruct H;]
 133 qed.
 134
 135 definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
 136 definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝
 137   λd:eqType.λx:d.(Some ? x : sort (option_eqType d)).
 138 coercion option_canonical_eqType.
 139
 140 (* belle le coercions! *)
 141 definition test_canonical_option_eqType ≝
 142   (eq (option_eqType nat_eqType) O (S O)).
 143
 144 lemma cmpP : ∀d:eqType.∀x,y:d.∀P:bool → Prop.
 145   (x=y → P true) → (cmp d x y = false → P false) → P (cmp d x y).
 146 intros; cases (eqP ? x y); [2:apply H1; apply (p2bF ? ? (eqP d ? ?))] autobatch;
 147 qed.
 148
 149 lemma cmpC : ∀d:eqType.∀x,y:d. cmp d x y = cmp d y x.
 150 intros; apply (cmpP ? x y); apply (cmpP ? y x); [1,4: intros; reflexivity]
 151 [intros (H2 H1) | intros (H1 H2)] rewrite > H1 in H2; rewrite > cmp_refl in H2;
 152 destruct H2.
 153 qed.