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 include "projdat/basic_type.ma".
18 theorem base_iff: ∀b,y:bool. if b then y else y = y.
21 theorem base_iff2: ∀b. if b then true else false = b.
24 theorem hp_tesi: ∀D:DeqSet. ∀x,y:D. ∀b:bool. if (x==y) then b else false=true→b=true.
25 #D #x #y #b elim b #Hp // normalize in Hp; > base_iff in Hp; // qed.
27 theorem hp_tesi2: ∀D:DeqSet. ∀x,y:D. ∀b:bool. if (x==y) then b else false=true→(x==y)=true.
28 #D #x #y #b #Hp lapply (hp_tesi … Hp) #Hp2
29 destruct >base_iff2 in Hp; // qed.
31 (******************************************************************************)
32 (* Coercizione per i dati lista *)
33 (******************************************************************************)
35 let rec eqb_lD (T:DeqSet) (x,y:list T) on x : bool ≝
44 | cons c d ⇒ (eqb T a c)∧(eqb_lD T b d)]].
46 lemma eqb_same_D: ∀D:DeqSet. ∀x:D. (eqb D x x)=true.
47 #D #same @(proj2 … (eqb_true D ? ? ) …) // qed.
51 ∀R:list D→ list D → Prop.
54 → (∀n,m,r,u. R n m → R (r::n) (u::m))
57 #R #ROn #RSO #RSS #n (elim n) // #n0 #lN0 #Rn0m #m (cases m) /2/ qed.
59 lemma list_destr_l: ∀D:DeqSet. ∀a,b:D.∀r,s:list D. (a=b)∧(r=s)→(a::r)=(b::s).
61 lapply (proj1 (x=y) (r=s) Hp)
62 lapply (proj2 (x=y) (r=s) Hp)
65 lemma list_destr_r: ∀D:DeqSet. ∀a,b:D.∀r,s:list D. (a::r)=(b::s)→(a=b)∧(r=s).
75 | #d #lD #s #hp destruct % @refl] qed.
77 lemma obv_eqb: ∀D:DeqSet.∀x:D. (x==x)=true.
78 #D #l @(proj2 … (eqb_true ???) ) // qed.
80 lemma obv_eb_l: ∀D. ∀e,l. (eqb_lD D (e::l) (e::l)=true).
81 #D #x#y normalize elim y normalize >obv_eqb //
82 #X #lX normalize #Hp >obv_eqb normalize @Hp qed.
84 lemma liD_right: ∀D:DeqSet. ∀x,y:list D. (x=y)→(eqb_lD D x y)=true.
89 | #l1 #l2 #e1 #e2 #Hp #eI lapply(list_destr_r D e1 e2 l1 l2 eI)
90 #HpE lapply (proj1 ? ? HpE) lapply (proj2 ? ? HpE) -HpE
91 #ls lapply (Hp ls) -Hp
94 normalize >obv_eqb normalize @eqv] qed.
96 lemma lid_left_1: ∀D:DeqSet. ∀x,y:D. ∀l1,l2:list D. ((x==y)=true)∧(l1=l2)→(x::l1=y::l2).
97 #D #x #y #L #M * #Hp lapply (proj1 … (eqb_true D ? ? ) Hp) -Hp #Hp #LH destruct // qed.
99 lemma tesi3: ∀D:DeqSet. ∀x,y:D. ∀M. (x=y)→(x::M=y::M).
100 #T#a #b #L #hp destruct // qed.
102 lemma liD_left: ∀D:DeqSet. ∀x,y:list D. (eqb_lD D x y)=true→(x=y).
104 [ * normalize // #hp #HHp #abs destruct
105 | #L #el normalize #abs destruct
106 | #L #M #x #y #Hp normalize #N lapply (hp_tesi2… N) #Hp2
107 lapply(hp_tesi D … N) -N #N lapply(Hp N)
108 -Hp -N #HP destruct @tesi3 @(proj1 … (eqb_true D ? ? )) //] qed.
110 lemma biimplication_lD: ∀D:DeqSet. ∀x,y:list D. iff ((eqb_lD D x y)=true) (x=y).
112 [ @liD_left | @liD_right ]
116 definition DeqList ≝ λT:DeqSet. mk_DeqSet (list T) (eqb_lD T) (biimplication_lD T).
118 unification hint 0 ≔ C1:DeqSet;
120 (* ---------------------------------------- *) ⊢
123 unification hint 0 ≔ C1:DeqSet,b1:list C1,b2: list C1;
125 (* ---------------------------------------- *) ⊢
126 eqb_lD C1 b1 b2 ≡ eqb X b1 b2.
129 (******************************************************************************)
130 (* Coercizione per i dati Σ *)
131 (******************************************************************************)
133 definition Sig_fst ≝ λA:Type[0].λP:A→Prop.λx:Sig A P.
134 match x with [mk_Sig a h ⇒ a].
136 definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
137 match x return λx.P (Sig_fst A P x) with [mk_Sig a h ⇒ h].
139 definition Sig_eq ≝ λA:DeqSet.λP:A→Prop. λx,y:Sig A P.
140 ((Sig_fst A P x)==(Sig_fst A P y)).
142 lemma biimplication_Sig: ∀A:DeqSet.∀P:A→Prop. ∀x,y:Sig A P.
143 (Sig_eq A P x y)=true↔(x=y).
148 lapply (proj1 … (eqb_true A ? ?) Hp)
151 | #Hp destruct normalize //] qed.
153 definition DeqSig ≝ λT:DeqSet.λP:T→Prop. mk_DeqSet (Sig T P) (Sig_eq T P) (biimplication_Sig T P).
155 unification hint 0 ≔ C1:DeqSet,C2:C1→Prop;
157 (* ---------------------------------------- *) ⊢
158 DeqSig C1 C2 ≡ carr X.
160 unification hint 0 ≔ C1:DeqSet,C2:C1→Prop,b1:Sig C1 C2,b2:Sig C1 C2;
162 (* ---------------------------------------- *) ⊢
163 Sig_eq C1 C2 b1 b2 ≡ eqb X b1 b2.
165 definition mk_DeqSig : ∀T:DeqSet.∀P:T→Prop.∀x:T. (P x)→(DeqSig T P) ≝
166 λT,P,x,p. mk_Sig T P x p.
169 (******************************************************************************)
170 (* Coercizione per i dati Cast *)
171 (******************************************************************************)
173 lemma eqc_b: ∀n1,hs. (eq_c (CBool n1) (CBool hs))=(beqb n1 hs).
174 #n1 #hs normalize // qed.
176 lemma eqc_n: ∀n1,hs. (eq_c (CNat n1) (CNat hs))=(eqb n1 hs).
177 #n1 #hs normalize // qed.
180 theorem dimplication_cast: ∀a,b. eq_c a b=true → a = b.
182 [* normalize #n2 [#Hp @eq_f @eqb_true_to_eq //
184 |* [normalize #n2 #abs @False_ind /2/
185 | #b >eqc_b #hp @eq_f @(\P hp)]
188 theorem eimplication_cast: ∀a,b. a = b →eq_c a b=true.
191 [ normalize @eq_to_eqb_true destruct //
195 | destruct @(proj2 … (beqb_true …) ) //
200 theorem biimplication_cast: ∀a,b. iff (eq_c a b=true) (a = b).
201 #A #B % [ @dimplication_cast | @eimplication_cast ] qed.
203 definition DeqCoer ≝ mk_DeqSet coerc eq_c biimplication_cast.
205 unification hint 0 ≔ ;
207 (* ---------------------------------------- *) ⊢
210 unification hint 0 ≔ b1,b2:coerc;
212 (* ---------------------------------------- *) ⊢
213 eq_c b1 b2 ≡ eqb X b1 b2.
215 (******************************************************************************)
216 (* Coercizione per i dati Type *)
217 (******************************************************************************)
219 theorem biimplication_type: ∀a,b. iff (eqb_type a b=true) (a=b).
221 [ normalize #abs @False_ind /2/
223 | normalize #abs @False_ind /2/
226 definition DeqType ≝ mk_DeqSet type eqb_type biimplication_type.
228 unification hint 0 ≔ ;
230 (* ---------------------------------------- *) ⊢
233 unification hint 0 ≔ b1,b2:type;
235 (* ---------------------------------------- *) ⊢
236 eqb_type b1 b2 ≡ eqb X b1 b2.
238 (******************************************************************************)
239 (* Coercizione per i dati naturali *)
240 (******************************************************************************)
242 definition eqb_nat ≝λx,y:nat. eqb x y.
243 theorem biimplication_nat: ∀a,b. iff (eqb_nat a b=true) (a = b).
244 #A #B % [ @eqb_true_to_eq | @eq_to_eqb_true ] qed.
246 definition DeqNat ≝ mk_DeqSet ℕ eqb_nat biimplication_nat.
248 unification hint 0 ≔ ;
250 (* ---------------------------------------- *) ⊢
253 unification hint 0 ≔ b1,b2:nat;
255 (* ---------------------------------------- *) ⊢
256 eqb_nat b1 b2 ≡ eqb X b1 b2.