From 6699a08a64470c8145324e6ff392fcb3453ade38 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 21 Oct 2021 15:50:04 +0200 Subject: Better use of the typeclass mechanism --- src/PropToBool.v | 6 +- src/SMT_terms.v | 104 +++++++-------- src/array/Array_checker.v | 211 ++++++++++++------------------- src/classes/SMT_classes.v | 16 +-- src/classes/SMT_classes_instances.v | 2 - src/versions/standard/Tactics_standard.v | 4 +- 6 files changed, 133 insertions(+), 210 deletions(-) diff --git a/src/PropToBool.v b/src/PropToBool.v index cad6dae..cab5b50 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -59,7 +59,7 @@ Ltac prop2bool := | _ => let p := fresh "p" in assert (p:CompDec t); - [ auto with typeclass_instances + [ try (exact _) (* Use the typeclass machinery *) | rewrite (@compdec_eq_eqb _ p) ] end @@ -172,7 +172,7 @@ Ltac prop2bool_hyp H := | _ => let Hcompdec := fresh "Hcompdec" in assert (Hcompdec: CompDec A); - [ auto with typeclass_instances | ] + [ try (exact _) | ] end | false => idtac end; @@ -223,7 +223,7 @@ Ltac remove_compdec_hyp H := | _ => let c := fresh "c" in assert (c : CompDec A); - [ auto with typeclass_instances + [ try (exact _) | let H1 := fresh in assert (H1 := H c); clear H; assert (H := H1); clear H1; remove_compdec_hyp H ] diff --git a/src/SMT_terms.v b/src/SMT_terms.v index dc5063f..eb33298 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -273,14 +273,18 @@ Module Typ. Fixpoint interp_compdec_aux (t:type) : {ty: Type & CompDec ty} := match t with | TFArray ti te => + let iti := interp_compdec_aux ti in + let ite := interp_compdec_aux te in + let cti := projT2 iti in + let cte := projT2 ite in + let tti := type_compdec cti in + let tte := type_compdec cte in existT (fun ty : Type => CompDec ty) - (@farray (type_compdec (projT2 (interp_compdec_aux ti))) - (type_compdec (projT2 (interp_compdec_aux te))) - (@ord_of_compdec _ (projT2 (interp_compdec_aux ti))) - (@inh_of_compdec _ (projT2 (interp_compdec_aux te)))) - (FArray_compdec - (type_compdec (projT2 (interp_compdec_aux ti))) - (type_compdec (projT2 (interp_compdec_aux te)))) + (@farray tti + tte + (@ord_of_compdec tti cti) + (@inh_of_compdec tte cte)) + (FArray_compdec tti tte) | Tindex i => existT (fun ty : Type => CompDec ty) (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i])) @@ -290,10 +294,10 @@ Module Typ. | TBV n => existT (fun ty : Type => CompDec ty) (BITVECTOR_LIST.bitvector n) (BV_compdec n) end. - Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) := - projT2 (interp_compdec_aux t). + Definition interp (t:type) : Type := type_compdec (projT2 (interp_compdec_aux t)). - Definition interp (t:type) : Type := type_compdec (interp_compdec t). + Definition interp_compdec (t:type) : CompDec (interp t) := + projT2 (interp_compdec_aux t). Definition interp_ftype (t:ftype) := @@ -301,40 +305,17 @@ Module Typ. (interp (snd t)) (fst t). - Definition dec_interp (t:type) : DecType (interp t). - Proof. - unfold interp. - destruct (interp_compdec t) as [x c]. simpl. - apply EqbToDecType. - Defined. - - Instance ord_interp (t:type) : OrdType (interp t). - Proof. - unfold interp. - destruct (interp_compdec t) as [x c]. simpl. - apply Ordered. - Defined. - - Instance comp_interp (t:type) : Comparable (interp t). - Proof. - unfold interp, ord_interp. - destruct (interp_compdec t) as [x c]. simpl. - apply Comp. - Defined. - - - Definition inh_interp (t:type) : Inhabited (interp t). - unfold interp. - destruct (interp_compdec t). - apply Inh. - Defined. + Global Instance dec_interp (t:type) : DecType (interp t) := + (@EqbToDecType _ (@eqbtype_of_compdec (interp t) (interp_compdec t))). - Definition inhabitant_interp (t:type) : interp t := @default_value _ (inh_interp _). + Global Instance ord_interp (t:type) : OrdType (interp t) := + @ord_of_compdec (interp t) (interp_compdec t). + Global Instance comp_interp (t:type) : Comparable (interp t) := + @comp_of_compdec (interp t) (interp_compdec t). - Hint Resolve - dec_interp comp_interp ord_interp - inh_interp interp_compdec : typeclass_instances. + Global Instance inh_interp (t:type) : Inhabited (interp t) := + @inh_of_compdec (interp t) (interp_compdec t). (* Boolean equality over interpretation of a btype *) @@ -1523,13 +1504,25 @@ Qed. apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shr s) | BO_select ti te => apply_binop (Typ.TFArray ti te) ti te FArray.select | BO_diffarray ti te => - apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te)) + let iti := Typ.interp_compdec_aux t_i ti in + let ite := Typ.interp_compdec_aux t_i te in + let cti := projT2 iti in + let cte := projT2 ite in + let tti := type_compdec cti in + let tte := type_compdec cte in + apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@EqbToDecType _ (@eqbtype_of_compdec tte cte)) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tti cti) (@inh_of_compdec tte cte)) end. Definition interp_top o := match o with | TO_store ti te => - apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te)) + let iti := Typ.interp_compdec_aux t_i ti in + let ite := Typ.interp_compdec_aux t_i te in + let cti := projT2 iti in + let cte := projT2 ite in + let tti := type_compdec cti in + let tte := type_compdec cte in + apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tte cte)) end. Fixpoint compute_interp ty acc l := @@ -1964,9 +1957,9 @@ Qed. rewrite !Typ.cast_refl. intros. exists ((@FArray.diff (Typ.interp t_i t') (Typ.interp t_i te) - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t'))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) + (Typ.dec_interp t_i t') + (Typ.ord_interp t_i t') + (Typ.comp_interp t_i t') (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto. (* Ternary operatores *) @@ -1988,11 +1981,7 @@ Qed. intros. rewrite !Typ.cast_refl. intros. - exists ((@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti'))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') - (Typ.inh_interp t_i te') x1 x2 x3)); auto. + exists (@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') (Typ.dec_interp t_i ti') (Typ.ord_interp t_i ti') (Typ.comp_interp t_i ti') (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') (Typ.inh_interp t_i te') x1 x2 x3); auto. (* N-ary operators *) destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha). @@ -2467,12 +2456,7 @@ Qed. simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TFArray ti te)) as [k2| ]; simpl; try (exists true; reflexivity). - exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) - (@EqbToDecType _ (@eqbtype_of_compdec _(Typ.interp_compdec t_i ti))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) - (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te) - (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto. + exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (Typ.dec_interp t_i ti) (Typ.ord_interp t_i ti) (Typ.comp_interp t_i ti) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto. (* Ternary operators *) intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3]; @@ -2486,9 +2470,9 @@ Qed. case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ]; simpl; try (exists true; reflexivity). exists (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) - (ord_of_compdec _) - (comp_of_compdec _) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) + (Typ.dec_interp t_i ti) + (Typ.ord_interp t_i ti) + (Typ.comp_interp t_i ti) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y) (k3 (Typ.interp t_i) z)); auto. diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index de20723..b6d7ef4 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -382,7 +382,7 @@ Section certif. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) (@store _ _ - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0))) + (Typ.dec_interp t_i t0) _ _ _ (Typ.comp_interp t_i t) _ v_val2 v_val3 v_val4) v_val0). intros. specialize (H18 H6). @@ -682,7 +682,7 @@ Section certif. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (@store _ _ - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1))) + (Typ.dec_interp t_i t1) _ _ _ (Typ.comp_interp t_i t2) _ v_vale1 v_vale2 v_vale3) (v_vald1')). intro H25. specialize (H25 Htid1'). @@ -839,7 +839,7 @@ Section certif. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (@store _ _ - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1))) + (Typ.dec_interp t_i t1) _ _ _ (Typ.comp_interp t_i t2) _ v_vale1 v_vale2 v_vale3) (v_valc1')). intro H25. specialize (H25 Htic1'). @@ -1180,7 +1180,7 @@ Section certif. rewrite !Typ.cast_refl. intros. specialize (Atom.Bval_inj2 t_i t0 (@diff _ _ - (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0))) + (Typ.dec_interp t_i t0) _ _ (Typ.dec_interp t_i v_typec2') _ (Typ.comp_interp t_i v_typec2') (Typ.inh_interp t_i t0) _ v_valf1 v_valf2) (v_vald2')). intros. specialize (H29 Htid2'). @@ -1225,140 +1225,87 @@ Section certif. apply negb_true_iff. apply Typ.i_eqb_spec_false. subst. - specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1') + + specialize (Atom.Bval_inj2 t_i v_typed2' v_vald2 (@diff + _ + _ (@EqbToDecType - (@projT1 Type (fun ty : Type => CompDec ty) - (Typ.interp_compdec_aux t_i v_typed2')) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) (@eqbtype_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')))) + (@ord_of_compdec + (@type_compdec (@projT1 Type (fun ty : Type => CompDec ty) (Typ.interp_compdec_aux t_i v_typed2')) - (Typ.interp_compdec t_i v_typed2'))) - (@ord_of_compdec (Typ.interp t_i v_typed2') + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) (@projT2 Type (fun ty : Type => CompDec ty) - ((fix interp_compdec_aux (t : Typ.type) : - @sigT Type (fun ty : Type => CompDec ty) := - match t return (@sigT Type (fun ty : Type => CompDec ty)) with - | Typ.TFArray ti te => - @existT Type (fun ty : Type => CompDec ty) - (@farray - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti))) - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te))) - (@ord_of_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti))) - (@inh_of_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)))) - (@SMT_classes_instances.FArray_compdec - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti))) - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te))) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te))) - | Typ.Tindex i => - @existT Type (fun ty : Type => CompDec ty) - (te_carrier (@get typ_compdec t_i i)) - (te_compdec (@get typ_compdec t_i i)) - | Typ.TZ => - @existT Type (fun ty : Type => CompDec ty) BinNums.Z - SMT_classes_instances.Z_compdec - | Typ.Tbool => - @existT Type (fun ty : Type => CompDec ty) bool - SMT_classes_instances.bool_compdec - | Typ.Tpositive => - @existT Type (fun ty : Type => CompDec ty) - BinNums.positive SMT_classes_instances.Positive_compdec - | Typ.TBV n => - @existT Type (fun ty : Type => CompDec ty) - (BVList.BITVECTOR_LIST.bitvector n) - (SMT_classes_instances.BV_compdec n) - end) v_typed2'))) - (@comp_of_compdec (Typ.interp t_i v_typed2') + (Typ.interp_compdec_aux t_i v_typed2'))) + (@comp_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) + (@EqbToDecType + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) + (@eqbtype_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1')))) + (@ord_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) + (@comp_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) + (@inh_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2'))) + (@inh_of_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1')) + (@projT2 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typec1'))) (@projT2 Type (fun ty : Type => CompDec ty) - ((fix interp_compdec_aux (t : Typ.type) : - @sigT Type (fun ty : Type => CompDec ty) := - match t return (@sigT Type (fun ty : Type => CompDec ty)) with - | Typ.TFArray ti te => - @existT Type (fun ty : Type => CompDec ty) - (@farray - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti))) - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te))) - (@ord_of_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti))) - (@inh_of_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)))) - (@SMT_classes_instances.FArray_compdec - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti))) - (@type_compdec - (@projT1 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te))) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) - (interp_compdec_aux te))) - | Typ.Tindex i => - @existT Type (fun ty : Type => CompDec ty) - (te_carrier (@get typ_compdec t_i i)) - (te_compdec (@get typ_compdec t_i i)) - | Typ.TZ => - @existT Type (fun ty : Type => CompDec ty) BinNums.Z - SMT_classes_instances.Z_compdec - | Typ.Tbool => - @existT Type (fun ty : Type => CompDec ty) bool - SMT_classes_instances.bool_compdec - | Typ.Tpositive => - @existT Type (fun ty : Type => CompDec ty) - BinNums.positive SMT_classes_instances.Positive_compdec - | Typ.TBV n => - @existT Type (fun ty : Type => CompDec ty) - (BVList.BITVECTOR_LIST.bitvector n) - (SMT_classes_instances.BV_compdec n) - end) v_typed2'))) (Typ.dec_interp t_i v_typec1') - (Typ.ord_interp t_i v_typec1') (Typ.comp_interp t_i v_typec1') - (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1 - v_valf2)). - intros. specialize (H5 Htid2'''). + (Typ.interp_compdec_aux t_i v_typec1'))) v_valf1 v_valf2)). + intros H5. specialize (H5 Htid2'''). rewrite <- H5. specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)). intros. diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index 53d5dcc..9ee394b 100644 --- a/src/classes/SMT_classes.v +++ b/src/classes/SMT_classes.v @@ -156,16 +156,16 @@ Class CompDec T := { }. -Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) := +Global Instance eqbtype_of_compdec {t} `{c: CompDec t} : (EqbType t) := let (_, eqb, _, _, _) := c in eqb. -Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) := +Global Instance ord_of_compdec {t} `{c: CompDec t} : (OrdType t) := let (_, _, ord, _, _) := c in ord. -Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) := +Global Instance inh_of_compdec {t} `{c: CompDec t} : (Inhabited t) := let (_, _, _, _, inh) := c in inh. -Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t). +Global Instance comp_of_compdec {t} `{c: CompDec t} : @Comparable t (ord_of_compdec (t:=t)). destruct c; trivial. Defined. @@ -173,7 +173,7 @@ Defined. Definition type_compdec {ty:Type} (cd : CompDec ty) := ty. Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool := - match eqbtype_of_compdec t with + match eqbtype_of_compdec (t:=t) with | {| eqb := eqb |} => eqb end. @@ -184,12 +184,6 @@ Proof. intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. Qed. -Hint Resolve - ord_of_compdec - inh_of_compdec - comp_of_compdec - eqbtype_of_compdec : typeclass_instances. - Record typ_compdec : Type := Typ_compdec { te_carrier : Type; diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index 6e7bc3d..178a546 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -748,5 +748,3 @@ Section prod. |}. End prod. - -Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec prod_compdec : typeclass_instances. diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v index edf2f19..5be62cc 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/versions/standard/Tactics_standard.v @@ -69,8 +69,8 @@ Ltac get_hyps := (** Tactics in bool *) -Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; auto with typeclass_instances. -Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; auto with typeclass_instances. +Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; try (exact _). +Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; try (exact _). Tactic Notation "verit_bool" constr(h) := let Hs := get_hyps in -- cgit