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/decidable_kit/eqtype/".
17 include "decidable_kit/decidable.ma".
18 include "datatypes/constructors.ma".
20 (* ### types with a decidable AND rewrite (leibniz) compatible ### *)
22 definition eq_compatible ≝ λT:Type.λa,b:T. reflect (a = b).
24 record eqType : Type ≝ {
26 cmp : sort → sort → bool ;
27 eqP : ∀x,y:sort. eq_compatible sort x y (cmp x y)
30 lemma cmp_refl : ∀d:eqType.∀x. cmp d x x = true.
31 intros (d x); generalize in match (eqP d x x); intros (H);
32 unfold in H; (* inversion non fa whd!!! *)
33 inversion H; [ intros; reflexivity | intros (ABS); cases (ABS (refl_eq ? ?)) ]
36 (* to use streicher *)
37 lemma eqType_decidable : ∀d:eqType. decT d.
38 intros (d); unfold decT; intros (x y); unfold decidable;
39 generalize in match (eqP d x y); intros (H);
40 cases H; [left | right] assumption;
43 lemma eqbP : ∀x,y:nat. eq_compatible nat x y (eqb x y).
45 generalize in match (refl_eq ? (eqb x y));
46 generalize in match (eqb x y) in ⊢ (? ? ? % → %); intros 1 (b);
47 cases b; intros (H); [ apply reflect_true | apply reflect_false ];
48 [ apply (eqb_true_to_eq ? ? H) | apply (eqb_false_to_not_eq ? ? H) ]
51 definition nat_eqType : eqType ≝ mk_eqType ? ? eqbP.
52 (* XXX le coercion nel cast non vengono inserite *)
53 definition nat_canonical_eqType : nat → nat_eqType :=
54 λn : nat.(n : sort nat_eqType).
55 coercion cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con.
57 definition bcmp ≝ λx,y:bool. match x with [ true ⇒ y | false => notb y ].
59 lemma bcmpP : ∀x,y:bool. eq_compatible bool x y (bcmp x y).
61 generalize in match (refl_eq ? (bcmp x y));
62 generalize in match (bcmp x y) in ⊢ (? ? ? % → %); intros 1 (b);
63 cases b; intros (H); [ apply reflect_true | apply reflect_false ];
64 generalize in match H; clear H;
65 cases x; cases y; simplify; intros (H); [1,4: reflexivity];
66 (* non va: try destruct H; *)
67 [1,2,3,6: destruct H | *: unfold Not; intros (H1); destruct H1]
70 definition bool_eqType : eqType ≝ mk_eqType ? ? bcmpP.
71 definition bool_canonical_eqType : bool → bool_eqType :=
72 λb : bool.(b : sort bool_eqType).
73 coercion cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con.
75 (* ### subtype of an eqType ### *)
77 record sigma (d : eqType) (p : d -> bool) : Type ≝ {
83 right associative with precedence 80
86 interpretation "sub_eqType" 'sig x h =
87 (cic:/matita/decidable_kit/eqtype/sigma.ind#xpointer(1/1/1) _ _ x h).
89 (* restricting an eqType gives an eqType *)
90 lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p.
91 eq_compatible ? x y (cmp ? (sval ? ? x) (sval ? ?y)).
93 generalize in match (refl_eq ? (cmp d (sval d p x) (sval d p y)));
94 generalize in match (cmp d (sval d p x) (sval d p y)) in ⊢ (? ? ? % → %); intros 1 (b);
95 cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp);
97 generalize in match (eqP d s t); intros (Est);
98 cases Est (H); clear Est;
99 [ generalize in match ps;
100 rewrite > H; intros (pt');
101 rewrite < (pirrel bool (p t) true pt pt' (eqType_decidable bool_eqType));
103 | cases (H (b2pT ? ? (eqP d s t) Hcmp))
105 | constructor 2; unfold Not; intros (H);
106 (* XXX destruct H; *)
107 change in Hcmp with (cmp d (match {?,ps} with [(mk_sigma s _)⇒s]) t = false);
108 rewrite > H in Hcmp; simplify in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;
112 definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
114 inductive in_sub (d : eqType) (p : d → bool) (x : d) : option (sigma d p) → Type ≝
115 | in_sig : ∀s : sigma d p. sval ? ? s = x → in_sub d p x (Some ? s)
116 | out_sig : p x = false → in_sub d p x (None ?).
118 definition if_p ≝ λd:eqType.λp:d→bool.λx:d.
119 match (eqP bool_eqType (p x) true) with
120 [ (reflect_true H) ⇒ Some ? {?,H}
121 | (reflect_false _) ⇒ None ?].
123 lemma in_sub_eq : ∀d,p,x. in_sub d p x (if_p d p x).
124 intros (d p x); unfold if_p;
125 cases (eqP bool_eqType (p x) true); simplify;
126 [ apply in_sig; reflexivity; | apply out_sig; apply (p2bF ? ? (idP ?) H)]
129 definition ocmp : ∀d:eqType.∀a,b:option d.bool ≝
130 λd:eqType.λa,b:option d.
132 [ None ⇒ match b with [ None ⇒ true | (Some _) ⇒ false]
133 | (Some x) ⇒ match b with [ None ⇒ false | (Some y) ⇒ cmp d x y]].
135 lemma ocmpP : ∀d:eqType.∀a,b:option d.eq_compatible ? a b (ocmp d a b).
137 generalize in match (refl_eq ? (ocmp ? a b));
138 generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c);
139 cases c; intros (H); [ apply reflect_true | apply reflect_false ];
140 generalize in match H; clear H;
142 [1: intros; reflexivity;
143 |2,3: intros (H); destruct H;
144 |4: intros (H); simplify in H; rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity;
145 (* se faccio la rewrite diretta non tipa *)
146 |5: intros (H H1); destruct H
147 |6,7: unfold Not; intros (H H1); destruct H1
148 |8: unfold Not; simplify; intros (H H1);
149 (* ancora injection non va *)
150 cut (s = s1); [ rewrite > Hcut in H; rewrite > cmp_refl in H; destruct H;].
151 change with (match (Some d s) with
152 [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1;
153 simplify; reflexivity;
156 definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
157 definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝
158 λd:eqType.λx:d.(Some ? x : sort (option_eqType d)).
159 coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con.
161 (* belle le coercions! *)
162 definition test_canonical_option_eqType ≝
163 (eq (option_eqType nat_eqType) O (S O)).
166 lemma eqbC : ∀x,y:nat. eqb x y = eqb y x.
167 intros (x y); apply bool_to_eq; split; intros (H);
168 rewrite > (b2pT ? ? (eqbP ? ?) H); rewrite > (cmp_refl nat_eqType);