From c827acdbf2814bc13495ab1599af9dfe85e32fbb Mon Sep 17 00:00:00 2001 From: ckeller Date: Tue, 25 May 2021 17:18:15 +0200 Subject: CompDec clean-up (#93) Clean-up the definition of CompDec, leaving the required minimum (in particular for functional arrays) --- src/QInst.v | 9 +- src/SMT_terms.v | 132 ++++++------- src/array/Array_checker.v | 83 +++++++- src/array/FArray.v | 372 ++++++++++++++---------------------- src/bva/Bva_checker.v | 248 ++++++++++++------------ src/classes/SMT_classes.v | 151 ++++++++++----- src/classes/SMT_classes_instances.v | 368 ++++++++++++++--------------------- 7 files changed, 648 insertions(+), 715 deletions(-) (limited to 'src') diff --git a/src/QInst.v b/src/QInst.v index 2684dea..01d8f01 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -88,14 +88,7 @@ Qed. (* An auxiliary lemma to rewrite an eqb_of_compdec into its the symmetrical version *) Lemma eqb_of_compdec_sym (A:Type) (HA:CompDec A) (a b:A) : eqb_of_compdec HA b a = eqb_of_compdec HA a b. -Proof. - destruct (@eq_dec _ (@Decidable _ HA) a b) as [H|H]. - - now rewrite H. - - case_eq (eqb_of_compdec HA a b). - + now rewrite <- !(@compdec_eq_eqb _ HA). - + intros _. case_eq (eqb_of_compdec HA b a); auto. - intro H1. elim H. symmetry. now rewrite compdec_eq_eqb. -Qed. +Proof. apply eqb_sym2. Qed. (* First strategy: change the order of all equalities in the goal or the hypotheses diff --git a/src/SMT_terms.v b/src/SMT_terms.v index bbb122a..1490acc 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -274,13 +274,13 @@ Module Typ. match t with | TFArray ti te => existT (fun ty : Type => CompDec ty) - (@farray (type_compdec (projT2 (interp_compdec_aux ti))) - (type_compdec (projT2 (interp_compdec_aux te))) + (@farray (projT1 (interp_compdec_aux ti)) + (projT1 (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)))) + (projT1 (interp_compdec_aux ti)) + (projT1 (interp_compdec_aux te))) | Tindex i => existT (fun ty : Type => CompDec ty) (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i])) @@ -293,7 +293,7 @@ Module Typ. Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) := projT2 (interp_compdec_aux t). - Definition interp (t:type) : Type := type_compdec (interp_compdec t). + Definition interp (t:type) : Type := projT1 (interp_compdec_aux t). Definition interp_ftype (t:ftype) := @@ -302,23 +302,26 @@ Module Typ. Definition dec_interp (t:type) : DecType (interp t). - destruct (interp_compdec t). - subst ty. - apply Decidable. - Defined. - - Instance comp_interp (t:type) : Comparable (interp t). - destruct (interp_compdec t). - subst ty. - apply Comp. + Proof. + unfold interp. + destruct (interp_compdec_aux t) as [x c]. simpl. + apply EqbToDecType. Defined. Instance ord_interp (t:type) : OrdType (interp t). - destruct (interp_compdec t). - subst ty. + Proof. + unfold interp. + destruct (interp_compdec_aux t) as [x c]. simpl. apply Ordered. Defined. + Instance comp_interp (t:type) : Comparable (interp t). + Proof. + unfold interp, ord_interp. + destruct (interp_compdec_aux t) as [x c]. simpl. + apply Comp. + Defined. + Definition inh_interp (t:type) : Inhabited (interp t). unfold interp. @@ -326,7 +329,7 @@ Module Typ. apply Inh. Defined. - Definition inhabitant_interp (t:type) : interp t := default_value. + Definition inhabitant_interp (t:type) : interp t := @default_value _ (inh_interp _). Hint Resolve @@ -344,28 +347,18 @@ Module Typ. Lemma eqb_compdec_spec {t} (c : CompDec t) : forall x y, eqb_of_compdec c x y = true <-> x = y. - intros. - destruct c. - destruct Eqb. - simpl. - auto. + Proof. + intros x y. + destruct c as [[E HE] O C I]. + unfold eqb_of_compdec. + simpl. now rewrite HE. Qed. Lemma eqb_compdec_spec_false {t} (c : CompDec t) : forall x y, eqb_of_compdec c x y = false <-> x <> y. - intros. - destruct c. - destruct Eqb. - simpl. - split. intros. - unfold not. intros. - apply eqb_spec in H0. - rewrite H in H0. now contradict H0. - intros. unfold not in H. - rewrite <- not_true_iff_false. - unfold not. intros. - apply eqb_spec in H0. - apply H in H0. now contradict H0. + Proof. + intros x y. + apply eqb_spec_false. Qed. Lemma i_eqb_spec : forall t x y, i_eqb t x y <-> x = y. @@ -384,12 +377,9 @@ Module Typ. Lemma reflect_eqb_compdec {t} (c : CompDec t) : forall x y, reflect (x = y) (eqb_of_compdec c x y). - intros. - destruct c. - destruct Eqb. - simpl in *. - apply iff_reflect. - symmetry; auto. + Proof. + intros x y. + apply reflect_eqb. Qed. @@ -401,15 +391,8 @@ Module Typ. Qed. Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x. - Proof. - intros t x y; case_eq (i_eqb t x y); intro H1; symmetry; - [ | rewrite neg_eq_true_eq_false in *; intro H2; apply H1]; - rewrite is_true_iff in *; now rewrite i_eqb_spec in *. - Qed. - + Proof. intros. apply eqb_sym2. Qed. - (* Lemma i_eqb_compdec_tbv (c: CompDec): forall x y, TBV x y = BITVECTOR_LIST_FIXED.bv_eq x y. *) - (* Proof. *) Definition i_eqb_eqb (t:type) : interp t -> interp t -> bool := match t with @@ -424,11 +407,9 @@ Module Typ. Lemma eqb_compdec_refl {t} (c : CompDec t) : forall x, eqb_of_compdec c x x = true. - intros. - destruct c. - destruct Eqb. - simpl. - apply eqb_spec. auto. + Proof. + intro x. + apply eqb_refl. Qed. Lemma i_eqb_refl : forall t x, i_eqb t x x. @@ -442,15 +423,10 @@ Module Typ. Lemma eqb_compdec_trans {t} (c : CompDec t) : forall x y z, eqb_of_compdec c x y = true -> eqb_of_compdec c y z = true -> - eqb_of_compdec c x z = true . - intros. - destruct c. - destruct Eqb. - simpl in *. - apply eqb_spec. - apply eqb_spec in H. - apply eqb_spec in H0. - subst; auto. + eqb_of_compdec c x z = true. + Proof. + intros x y z. + apply eqb_trans. Qed. Lemma i_eqb_trans : forall t x y z, i_eqb t x y -> i_eqb t y z -> i_eqb t x z. @@ -1547,13 +1523,13 @@ 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 + 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)) 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 + 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)) end. Fixpoint compute_interp ty acc l := @@ -1987,7 +1963,11 @@ Qed. rewrite H2, H3, H1. rewrite !Typ.cast_refl. intros. - exists (FArray.diff x1 x2); auto. + 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.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto. (* Ternary operatores *) destruct op as [ti te]; intros [ ti' te' | | | | | ]; @@ -2008,7 +1988,11 @@ Qed. intros. rewrite !Typ.cast_refl. intros. - exists (FArray.store x1 x2 x3); auto. + 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. (* N-ary operators *) destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha). @@ -2483,7 +2467,12 @@ 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 (k1 interp_t x) (k2 interp_t y)); auto. + 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. (* Ternary operators *) intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3]; @@ -2496,7 +2485,12 @@ Qed. simpl; try (exists true; auto); intro k2; case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ]; simpl; try (exists true; reflexivity). - exists (FArray.store (k1 interp_t x) (k2 interp_t y) (k3 interp_t z)); auto. + 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) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y) + (k3 (Typ.interp t_i) z)); auto. (* N-ary operators *) intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl. diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index da0f6f2..5bf0eaa 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -380,8 +380,11 @@ Section certif. rewrite H6d1, H6d2, H14. intros. - specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) - (store v_val2 v_val3 v_val4) (v_val0)). + specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) + (@store _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0))) + _ _ _ (Typ.comp_interp t_i t) _ + v_val2 v_val3 v_val4) v_val0). intros. specialize (H18 H6). rewrite <- H18. @@ -397,7 +400,8 @@ Section certif. intros. specialize (H20 Htia2). rewrite <- H20. apply Typ.i_eqb_spec. - apply (read_over_write (elt_dec:=(EqbToDecType _ (@Eqb _ _)))). + apply (read_over_write (elt_dec:=(@EqbToDecType _ (@Eqb _ + (projT2 (Typ.interp_compdec_aux t_i _)))))). Qed. @@ -677,9 +681,12 @@ Section certif. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) - (store v_vale1 v_vale2 v_vale3) (v_vald1')). + (@store _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1))) + _ _ _ (Typ.comp_interp t_i t2) _ + v_vale1 v_vale2 v_vale3) (v_vald1')). intro H25. specialize (H25 Htid1'). - + unfold Atom.interp_form_hatom, interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Heq6. simpl. @@ -725,7 +732,7 @@ Section certif. subst; intros; rewrite Htid2 in Htic2; - rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite Htie2 in Htia1. rewrite Htia2 in Htic2''. @@ -831,7 +838,10 @@ Section certif. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) - (store v_vale1 v_vale2 v_vale3) (v_valc1')). + (@store _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1))) + _ _ _ (Typ.comp_interp t_i t2) _ + v_vale1 v_vale2 v_vale3) (v_valc1')). intro H25. specialize (H25 Htic1'). unfold Atom.interp_form_hatom, interp_hatom. @@ -878,7 +888,7 @@ Section certif. subst; intros; rewrite Htid2 in Htic2; - rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite Htie2 in Htia1. rewrite Htia2 in Htic2''. @@ -1169,7 +1179,10 @@ Section certif. unfold Bval. rewrite <- H25. rewrite !Typ.cast_refl. intros. - specialize (Atom.Bval_inj2 t_i t0 (diff v_valf1 v_valf2) (v_vald2')). + specialize (Atom.Bval_inj2 t_i t0 (@diff _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec 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'). (* semantics *) @@ -1212,7 +1225,57 @@ Section certif. apply negb_true_iff. apply Typ.i_eqb_spec_false. subst. - specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (diff v_valf1 v_valf2)). + specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1') + (@EqbToDecType + _ + (@eqbtype_of_compdec + _ + (Typ.interp_compdec t_i v_typed2'))) + _ + (@comp_of_compdec (Typ.interp t_i v_typed2') + (projT2 + ((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 + (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) + (@projT1 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 + (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) + (@projT1 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.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'''). rewrite <- H5. specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)). diff --git a/src/array/FArray.v b/src/array/FArray.v index 68ee19d..f094927 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -54,10 +54,7 @@ Module Raw. Definition ltk (a b : (key * elt)) := lt (fst a) (fst b). - (* Definition ltke (a b : (key * elt)) := *) - (* lt (fst a) (fst b) \/ ( (fst a) = (fst b) /\ lt (snd a) (snd b)). *) - - Hint Unfold ltk (* ltke *) eqk eqke. + Hint Unfold ltk eqk eqke. Hint Extern 2 (eqke ?a ?b) => split. Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop). @@ -69,8 +66,6 @@ Module Raw. Global Instance ke_dec : DecType (key * elt). Proof. split; auto. - intros; destruct x, y, z. - inversion H. inversion H0. trivial. intros; destruct x, y. destruct (eq_dec k k0). destruct (eq_dec e e0). @@ -107,45 +102,6 @@ Module Raw. Hint Unfold MapsTo In. - (* Instance ke_ord: OrdType (key * elt). *) - (* Proof. *) - (* exists ltke. *) - (* unfold ltke. intros. *) - (* destruct H, H0. *) - (* left; apply (lt_trans _ (fst y)); auto. *) - (* destruct H0. left. rewrite <- H0. assumption. *) - (* destruct H. left. rewrite H. assumption. *) - (* destruct H, H0. *) - (* right. split. *) - (* apply (eq_trans _ (fst y)); trivial. *) - (* apply (lt_trans _ (snd y)); trivial. *) - (* unfold ltke. intros. *) - (* destruct x, y. simpl in H. *) - (* destruct H. *) - (* apply lt_not_eq in H. *) - (* unfold not in *. intro. inversion H0. apply H. trivial. *) - (* destruct H. apply lt_not_eq in H0. unfold not in *. intro. *) - (* inversion H1. apply H0; trivial. *) - (* intros. *) - (* unfold ltke. *) - (* destruct (compare (fst x) (fst y)). *) - (* apply LT. left; assumption. *) - (* destruct (compare (snd x) (snd y)). *) - (* apply LT. right; split; assumption. *) - (* apply EQ. destruct x, y. simpl in *. rewrite e, e0; trivial. *) - (* apply GT. right; symmetry in e; split; assumption. *) - (* apply GT. left; assumption. *) - (* Qed. *) - - (* Hint Immediate ke_ord. *) - (* Let ke_ord := ke_ord. *) - - (* Instance keyelt_ord: OrdType (key * elt). *) - - - (* Variable keyelt_ord : OrdType (key * elt). *) - (* eqke is stricter than eqk *) - Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. Proof. unfold eqk, eqke; intuition. @@ -166,15 +122,15 @@ Module Raw. Proof. unfold eqke; intuition. Qed. Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. - Proof. eauto. Qed. + Proof. unfold eqk; now intros e1 e2 e3 ->. Qed. Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. Proof. - unfold eqke; intuition; [ eauto | congruence ]. + unfold eqke; intros [k1 e1] [k2 e2] [k3 e3]; simpl; now intros [-> ->]. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. unfold ltk; eauto. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto. Qed. @@ -203,25 +159,12 @@ Module Raw. unfold Transitive. intros x y z. apply lt_trans. Qed. - (* Instance ltke_strorder : StrictOrder ltke. *) - (* Proof. *) - (* split. *) - (* unfold Irreflexive, Reflexive, complement. *) - (* intros. apply lt_not_eq in H; auto. *) - (* unfold Transitive. apply lt_trans. *) - (* Qed. *) - Global Instance eq_equiv : @Equivalence (key * elt) eq. Proof. split; auto. unfold Transitive. apply eq_trans. Qed. - (* Instance ltke_compat : Proper (eq ==> eq ==> iff) ltke. *) - (* Proof. *) - (* split; rewrite H, H0; trivial. *) - (* Qed. *) - Global Instance ltk_compat : Proper (eq ==> eq ==> iff) ltk. Proof. split; rewrite H, H0; trivial. @@ -276,27 +219,6 @@ Module Raw. Hint Resolve InA_eqke_eqk. - (* Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. *) - (* Proof. *) - (* intros; apply InA_eqA with p; auto with *. *) - (* Qed. *) - - (* Lemma In_eq : forall l x y, eq x y -> InA eqke x l -> InA eqke y l. *) - (* Proof. intros. rewrite <- H; auto. Qed. *) - - (* Lemma ListIn_In : forall l x, List.In x l -> InA eqk x l. *) - (* Proof. apply In_InA. split; auto. unfold Transitive. *) - (* unfold eqk; intros. rewrite H, <- H0. auto. *) - (* Qed. *) - - (* Lemma Inf_lt : forall l x y, ltk x y -> Inf y l -> Inf x l. *) - (* Proof. exact (InfA_ltA ltk_strorder). Qed. *) - - (* Lemma Inf_eq : forall l x y, x = y -> Inf y l -> Inf x l. *) - (* Proof. exact (InfA_eqA eq_equiv ltk_compat). Qed. *) - - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. firstorder. @@ -666,10 +588,6 @@ Module Raw. clear e0. inversion Hm. subst. apply Sort_Inf_NotIn with x0; auto. - (* clear e0;inversion_clear Hm. *) - (* apply Sort_Inf_NotIn with x0; auto. *) - (* apply Inf_eq with (k',x0);auto; compute; apply eq_trans with x; auto. *) - clear e0;inversion_clear Hm. assert (notin:~ In y (remove y l)) by auto. intros (x1,abs). @@ -755,7 +673,6 @@ Module Raw. | _ => idtac end. intros. - (* rewrite In_alt in *. *) destruct H0 as (e, H0). exists e. apply InA_cons_tl. auto. @@ -764,7 +681,6 @@ Module Raw. inversion_clear Hm. apply In_inv in H0. destruct H0. - (* destruct (eq_dec k' y). *) exists _x. apply InA_cons_hd. split; simpl; auto. specialize (IHb H1 H H0). @@ -1030,16 +946,11 @@ Section FArray. Qed. (** Boolean comparison over elements *) - Definition cmp (e e':elt) := - match compare e e' with EQ _ => true | _ => false end. - + Definition cmp := @compare2eqb _ _ elt_comp. Lemma cmp_refl : forall e, cmp e e = true. - unfold cmp. - intros. - destruct (compare e e); auto; - apply lt_not_eq in l; now contradict l. - Qed. + Proof. intro e. unfold cmp. now rewrite compare2eqb_spec. Qed. + Lemma remove_nodefault : forall l (Hd:NoDefault l) (Hs:Sorted (Raw.ltk key_ord) l) x , NoDefault (Raw.remove key_comp x l). @@ -1072,29 +983,26 @@ Section FArray. Lemma add_nodefault : forall l (Hd:NoDefault l) (Hs:Sorted (Raw.ltk key_ord) l) x e, NoDefault (raw_add_nodefault x e l). Proof. - intros. + intros l Hd Hs x e. unfold raw_add_nodefault. - case_eq (cmp e default_value); intro; auto. - case_eq (Raw.mem key_comp x l); intro; auto. - apply remove_nodefault; auto. - unfold NoDefault; intros. - assert (e <> default_value). - unfold cmp in H. - case (compare e default_value) in H; try now contradict H. - apply lt_not_eq in l0; auto. - apply lt_not_eq in l0; now auto. - destruct (eq_dec k x). - - symmetry in e0. - apply (Raw.add_1 key_dec key_comp l e) in e0. - unfold not; intro. - specialize (Raw.add_sorted key_dec key_comp Hs x e). - intro Hsadd. - specialize (Raw.MapsTo_inj key_dec Hsadd e0 H1). - intro. contradiction. - - unfold not; intro. - assert (x <> k). unfold not in *. intro. apply n. symmetry; auto. - specialize (Raw.add_3 key_dec key_comp l e H2 H1). - intro. now apply Hd in H3. + case_eq (cmp e default_value); intro H; auto. + - case_eq (Raw.mem key_comp x l); intro H0; auto. + apply remove_nodefault; auto. + - unfold NoDefault; intros k. + assert (H0: e <> default_value). + { intro H1. subst e. rewrite cmp_refl in H. discriminate. } + destruct (eq_dec k x) as [e0|n]. + + symmetry in e0. + apply (Raw.add_1 key_comp l e) in e0. + unfold not; intro. + specialize (Raw.add_sorted key_comp Hs x e). + intro Hsadd. + specialize (Raw.MapsTo_inj Hsadd e0 H1). + intro. contradiction. + + unfold not; intro. + assert (x <> k). unfold not in *. intro. apply n. symmetry; auto. + specialize (Raw.add_3 key_comp l e H2 H1). + intro. now apply Hd in H3. Qed. Definition empty : farray := @@ -1133,8 +1041,7 @@ Section FArray. Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.ltk key elt key_ord. Lemma MapsTo_1 : forall m x y e, eq x y -> MapsTo x e m -> MapsTo y e m. - Proof. intros m. - apply (Raw.MapsTo_eq key_dec elt_dec). Qed. + Proof. intros m. apply Raw.MapsTo_eq. Qed. Lemma mem_1 : forall m x, In x m -> mem x m = true. Proof. intros m; apply (Raw.mem_1); auto. apply m.(sorted). Qed. @@ -1150,12 +1057,13 @@ Section FArray. Proof. intros m; apply Raw.is_empty_2. Qed. Lemma add_1 : forall m x y e, e <> default_value -> eq x y -> MapsTo y e (add x e m). - Proof. intros. + Proof. + intros m x y e H H0. unfold add, raw_add_nodefault. unfold MapsTo. simpl. - case_eq (cmp e default_value); intro; auto. - unfold cmp in H1. destruct (compare e default_value); try now contradict H1. - apply Raw.add_1; auto. + case_eq (cmp e default_value); intro H1; auto. + - elim H. unfold cmp in H1. now rewrite compare2eqb_spec in H1. + - apply Raw.add_1; auto. Qed. Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). @@ -1203,7 +1111,7 @@ Section FArray. Proof. intros m; apply Raw.elements_3; auto. apply m.(sorted). Qed. Lemma elements_3w : forall m, NoDupA eq_key (elements m). - Proof. intros m; apply (Raw.elements_3w key_dec m.(sorted)). Qed. + Proof. intros m; apply (Raw.elements_3w m.(sorted)). Qed. Lemma cardinal_1 : forall m, cardinal m = length (elements m). Proof. intros; reflexivity. Qed. @@ -1236,62 +1144,64 @@ Section FArray. apply (H k). unfold Raw.MapsTo. apply InA_cons_tl. apply H0. Qed. - Lemma raw_equal_eq : forall a (Ha: Sorted (Raw.ltk key_ord) a) b (Hb: Sorted (Raw.ltk key_ord) b), + Lemma raw_equal_eq : + forall a (Ha: Sorted (Raw.ltk key_ord) a) b (Hb: Sorted (Raw.ltk key_ord) b), Raw.equal key_comp cmp a b = true -> a = b. Proof. - induction a; intros. - simpl in H. - case b in *; auto. - now contradict H. - destruct a as (xa, ea). - simpl in H. - case b in *. - now contradict H. - destruct p as (xb, eb). - destruct (compare xa xb); auto; try (now contradict H). - rewrite andb_true_iff in H. destruct H. - unfold cmp in H. - destruct (compare ea eb); auto; try (now contradict H). - subst. apply f_equal. - apply IHa; auto. - now inversion Ha. - now inversion Hb. + induction a as [ |a a0 IHa]; intros Ha b Hb H. + - simpl in H. + case b in *; auto. + now contradict H. + - destruct a as (xa, ea). + simpl in H. + case b in *. + + now contradict H. + + destruct p as (xb, eb). + destruct (compare xa xb); auto; try (now contradict H). + rewrite andb_true_iff in H. destruct H as [H H0]. + unfold cmp in H. rewrite compare2eqb_spec in H. + subst. apply f_equal. + apply IHa; auto. + * now inversion Ha. + * now inversion Hb. Qed. Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true. Proof. - intros (l,Hl,Hd); induction l. - intros (l',Hl',Hd'); unfold eq; simpl. - destruct l'; unfold equal; simpl; intuition. - intros (l',Hl',Hd'); unfold eq. - destruct l'. - destruct a; unfold equal; simpl; intuition. - destruct a as (x,e). - destruct p as (x',e'). - unfold equal; simpl. - destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; intuition. - unfold cmp at 1. - case (compare e e'); - subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); - clear HH; simpl. - inversion_clear Hl. - inversion_clear Hl'. - apply nodefault_tail in Hd. - apply nodefault_tail in Hd'. - destruct (IHl H Hd (Build_farray H2 Hd')). - unfold equal, eq in H5; simpl in H5; auto. - destruct (andb_prop _ _ H); clear H. - generalize H0; unfold cmp. - case (compare e e'); - subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); - auto; intro; discriminate. - destruct (andb_prop _ _ H); clear H. - inversion_clear Hl. - inversion_clear Hl'. - apply nodefault_tail in Hd. - apply nodefault_tail in Hd'. - destruct (IHl H Hd (Build_farray H3 Hd')). - unfold equal, eq in H6; simpl in H6; auto. + intros (l,Hl,Hd); induction l as [ |a l IHl]. + - intros (l',Hl',Hd'); unfold eq; simpl. + destruct l'; unfold equal; simpl; intuition. + - intros (l',Hl',Hd'); unfold eq. + destruct l' as [ |p l']. + + destruct a; unfold equal; simpl; intuition. + + destruct a as (x,e). + destruct p as (x',e'). + unfold equal; simpl. + destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; [intuition| |intuition]. + split. + * intros [H0 H1]. + unfold cmp, compare2eqb at 1. + case (compare e e'); + subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); + clear HH; simpl. + inversion_clear Hl. + inversion_clear Hl'. + apply nodefault_tail in Hd. + apply nodefault_tail in Hd'. + destruct (IHl H Hd (Build_farray H2 Hd')). + unfold equal, eq in H5; simpl in H5; auto. + * { intro H. destruct (andb_prop _ _ H) as [H0 H1]; clear H. split. + - generalize H0; unfold cmp, compare2eqb. + case (compare e e'); + subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); + auto; intro; discriminate. + - inversion_clear Hl. + inversion_clear Hl'. + apply nodefault_tail in Hd. + apply nodefault_tail in Hd'. + destruct (IHl H Hd (Build_farray H3 Hd')). + unfold equal, eq in H6; simpl in H6; auto. + } Qed. Lemma eq_1 : forall m m', Equivb m m' -> eq m m'. @@ -1509,37 +1419,40 @@ Section FArray. Lemma raw_add_d_rem : forall m (Hm: Sorted (Raw.ltk key_ord) m) x, raw_add_nodefault x default_value m = Raw.remove key_comp x m. - intros. + Proof. + intros m Hm x. unfold raw_add_nodefault. rewrite cmp_refl. - case_eq (Raw.mem key_comp x m); intro. - auto. + case_eq (Raw.mem key_comp x m); intro H; auto. apply Raw.mem_3 in H; auto. apply raw_equal_eq; auto. - apply Raw.remove_sorted; auto. - apply Raw.equal_1; auto. - apply Raw.remove_sorted; auto. - unfold Raw.Equivb. - split. - intros. - destruct (eq_dec x k). subst. - split. intro. contradiction. - intro. contradict H0. - apply Raw.remove_1; auto. - apply Raw.remove_4; auto. - - intros. - destruct (eq_dec x k). - assert (exists e, InA (Raw.eqk (elt:=elt)) (k, e) (Raw.remove key_comp x m)). - exists e'. apply Raw.InA_eqke_eqk; auto. - rewrite <- Raw.In_alt in H2; auto. - contradict H2. - apply Raw.remove_1; auto. - apply key_comp. - apply (Raw.remove_2 key_comp Hm n) in H0. - specialize (Raw.remove_sorted key_comp Hm x). intros. - specialize (Raw.MapsTo_inj key_dec H2 H0 H1). - intro. subst. apply cmp_refl. + - apply Raw.remove_sorted; auto. + - apply Raw.equal_1; auto. + + apply Raw.remove_sorted; auto. + + unfold Raw.Equivb. + split. + * { intros k. + destruct (eq_dec x k) as [e|n]. + - subst. + split. + + intro. contradiction. + + intro. contradict H0. + apply Raw.remove_1; auto. + - apply Raw.remove_4; auto. + } + * { intros k e e' H0 H1. + destruct (eq_dec x k) as [e0|n]. + - assert (H2:exists e, InA (Raw.eqk (elt:=elt)) (k, e) (Raw.remove key_comp x m)). + { exists e'. apply Raw.InA_eqke_eqk; auto. } + rewrite <- Raw.In_alt in H2; auto. + + contradict H2. + apply Raw.remove_1; auto. + + apply key_comp. + - apply (Raw.remove_2 key_comp Hm n) in H0. + specialize (Raw.remove_sorted key_comp Hm x). intros H2. + specialize (Raw.MapsTo_inj H2 H0 H1). + intro H3. subst. apply cmp_refl. + } Qed. Lemma add_d_rem : forall m x, add x default_value m = remove x m. @@ -1559,19 +1472,18 @@ Section FArray. Lemma add_eq_d : forall m x y, x = y -> find y (add x default_value m) = None. Proof. - intros. - simpl. + intros m x y h. rewrite add_d_rem. case_eq (find y (remove x m)); auto. - intros. + intros e H0. apply find_2 in H0. unfold MapsTo, Raw.MapsTo in H0. - assert (exists e, InA (Raw.eqk (elt:=elt)) (y, e) (remove x m).(this)). - exists e. apply Raw.InA_eqke_eqk in H0. auto. + assert (H1:exists e, InA (Raw.eqk (elt:=elt)) (y, e) (remove x m).(this)). + { exists e. apply Raw.InA_eqke_eqk in H0. auto. } rewrite <- Raw.In_alt in H1; auto. - contradict H1. - apply remove_1; auto. - apply key_comp. + - contradict H1. + apply remove_1; auto. + - apply key_comp. Qed. Lemma add_neq_o : forall m x y e, @@ -1626,8 +1538,8 @@ Section FArray. Lemma Equiv_Equivb : forall m m', Equiv m m' <-> Equivb m m'. Proof. unfold Equiv, Equivb, Raw.Equivb, cmp; intuition; specialize (H1 k e e' H H2). - destruct (compare e e'); auto; apply lt_not_eq in l; auto. - destruct (compare e e'); auto; now contradict H1. + - unfold compare2eqb; destruct (compare e e'); auto; apply lt_not_eq in l; auto. + - unfold compare2eqb in *; destruct (compare e e'); auto; inversion H1. Qed. (** Composition of the two last results: relation between [Equal] @@ -1653,17 +1565,17 @@ Section FArray. Proof. intros a i j v Heq. unfold select, store. - case_eq (cmp v default_value); intro; auto. - unfold cmp in H. - case (compare v default_value) in H; auto; try now contradict H. - rewrite e. - rewrite add_eq_d; auto. - assert (v <> default_value). - unfold cmp in H. - case (compare v default_value) in H; auto; try now contradict H. - apply lt_not_eq in l. auto. - apply lt_not_eq in l. auto. - rewrite (add_eq_o a Heq H0). auto. + case_eq (cmp v default_value); intro H; auto. + - unfold cmp, compare2eqb in H. + case (compare v default_value) as [ | |e] in H; auto; try now contradict H. + rewrite e. + rewrite add_eq_d; auto. + - assert (H0: v <> default_value). + { unfold cmp, compare2eqb in H. + case (compare v default_value) as [l|e|l] in H; auto; try now contradict H. + - apply lt_not_eq in l. auto. + - apply lt_not_eq in l. auto. } + rewrite (add_eq_o a Heq H0). auto. Qed. Lemma read_over_write : forall a i v, select (store a i v) i = v. @@ -1904,10 +1816,10 @@ Section FArray. Qed. Definition diff (a b: farray) : key. - case_eq (equal a b); intro. + Proof. + case_eq (equal a b); intro H. - apply default_value. - apply (diff_index (notequal_neq H)). - (* destruct (diff_index_p H). apply x. *) Defined. Lemma select_at_diff: forall a b, a <> b -> @@ -1934,12 +1846,12 @@ Arguments store {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. Arguments diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _. Arguments equal {_} {_} {_} {_} {_} {_} {_} _ _. Arguments equal_iff_eq {_} {_} {_} {_} {_} {_} {_} _ _. -Arguments read_over_same_write {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _ _ _. -Arguments read_over_write {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. -Arguments read_over_other_write {_} {_} {_} {_} {_} {_} {_} {_} _ _ _ _ _. -Arguments extensionality {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. +Arguments read_over_same_write {_} {_} {_} {_} {_} {_} {_} _ _ _ _ _. +Arguments read_over_write {_} {_} {_} {_} {_} {_} {_} _ _ _. +Arguments read_over_other_write {_} {_} {_} {_} {_} {_} _ _ _ _ _. +Arguments extensionality {_} {_} {_} {_} {_} {_} {_} _ _ _. Arguments extensionality2 {_} {_} {_} {_} {_} {_} {_} {_} {_} _. -Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. +Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. Notation "a '[' i ']'" := (select a i) (at level 1, format "a [ i ]") : farray_scope. diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 24cf620..a2fd213 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -1179,132 +1179,132 @@ Proof. intro la. Qed. Lemma valid_check_bbDiseq lres : C.valid rho (check_bbDiseq lres). -Proof. - unfold check_bbDiseq. - case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true. - case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). - intros f Heq2. - case_eq (t_atom .[ f]); try (intros; now apply C.interp_true). - - intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ]; - try (intros; now apply C.interp_true). intros a b Heq3. - case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros c Heq4. - case_eq c; try (intros; now apply C.interp_true). - intros la n1 Heq5. - case_eq (t_atom .[ b]); try (intros; now apply C.interp_true). - intros c0 Heq6. - case_eq c0; try (intros; now apply C.interp_true). - intros lb n2 Heq7. - case_eq (List_diseqb la lb && (N.of_nat (Datatypes.length la) =? n)%N - && (N.of_nat (Datatypes.length lb) =? n)%N - && (n1 =? n)%N && (n2 =? n)%N); - try (intros; now apply C.interp_true). intros Heq8. +Proof. + unfold check_bbDiseq. + case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true. + case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). + intros f Heq2. + case_eq (t_atom .[ f]); try (intros; now apply C.interp_true). - unfold C.valid. simpl. rewrite orb_false_r. - unfold Lit.interp. rewrite Heq. - unfold Var.interp. - rewrite wf_interp_form; trivial. rewrite Heq2. simpl. - unfold Atom.interp_form_hatom, interp_hatom. - rewrite Atom.t_interp_wf; trivial. - rewrite Heq3. simpl. - rewrite !Atom.t_interp_wf; trivial. - rewrite Heq4, Heq6. simpl. - rewrite Heq5, Heq7. simpl. + intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ]; + try (intros; now apply C.interp_true). intros a b Heq3. + case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). + intros c Heq4. + case_eq c; try (intros; now apply C.interp_true). + intros la n1 Heq5. + case_eq (t_atom .[ b]); try (intros; now apply C.interp_true). + intros c0 Heq6. + case_eq c0; try (intros; now apply C.interp_true). + intros lb n2 Heq7. + case_eq (List_diseqb la lb && (N.of_nat (Datatypes.length la) =? n)%N + && (N.of_nat (Datatypes.length lb) =? n)%N + && (n1 =? n)%N && (n2 =? n)%N); + try (intros; now apply C.interp_true). intros Heq8. - rewrite !andb_true_iff in Heq8. - destruct Heq8 as (((Heq8, Ha), Hb), Hc). - destruct Heq8 as (Heq8, Hd). - rewrite N.eqb_eq in Hb, Hc. - rewrite Hb, Hc. - rewrite Typ.N_cast_refl. simpl. + unfold C.valid. simpl. rewrite orb_false_r. + unfold Lit.interp. rewrite Heq. + unfold Var.interp. + rewrite wf_interp_form; trivial. rewrite Heq2. simpl. + unfold Atom.interp_form_hatom, interp_hatom. + rewrite Atom.t_interp_wf; trivial. + rewrite Heq3. simpl. + rewrite !Atom.t_interp_wf; trivial. + rewrite Heq4, Heq6. simpl. + rewrite Heq5, Heq7. simpl. + + rewrite !andb_true_iff in Heq8. + destruct Heq8 as (((Heq8, Ha), Hb), Hc). + destruct Heq8 as (Heq8, Hd). + rewrite N.eqb_eq in Hb, Hc. + rewrite Hb, Hc. + rewrite Typ.N_cast_refl. simpl. - generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + generalize wt_t_atom. unfold Atom.wt. unfold is_true. + rewrite PArray.forallbi_spec;intros. - (* a *) - pose proof (H a). - assert (a < PArray.length t_atom). - { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4, Heq5. easy. } - specialize (@H0 H1). rewrite Heq4 in H0. simpl in H0. - unfold get_type' in H0. unfold v_type in H0. - case_eq (t_interp .[ a]). - intros v_typea v_vala Htia. rewrite Htia in H0. - rewrite Atom.t_interp_wf in Htia; trivial. - rewrite Heq4, Heq5 in Htia. simpl in Htia. - rewrite Hb in Htia. - unfold Bval in Htia. - rewrite Heq5 in H0. simpl in H0. - inversion Htia. - - generalize dependent v_vala. - rewrite <- H3. intros. - - (* b *) - pose proof (H b). - assert (b < PArray.length t_atom). - { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6, Heq7. easy. } - specialize (@H2 H4). rewrite Heq6 in H2. simpl in H2. - unfold get_type' in H2. unfold v_type in H2. - case_eq (t_interp .[ b]). - intros v_typeb v_valb Htib. rewrite Htib in H2. - rewrite Atom.t_interp_wf in Htib; trivial. - rewrite Heq6, Heq7 in Htib. simpl in Htib. - rewrite Hc in Htib. - unfold Bval in Htib. - rewrite Heq7 in H2. simpl in H2. - inversion Htib. - - generalize dependent v_valb. - rewrite <- H6. intros. - - (* f *) - pose proof (H f). - assert (f < PArray.length t_atom). - { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. } - specialize (@H5 H7). rewrite Heq3 in H5. simpl in H5. - unfold get_type' in H5. unfold v_type in H5. - case_eq (t_interp .[ f]). - intros v_typef v_valf Htif. rewrite Htif in H5. - rewrite Atom.t_interp_wf in Htif; trivial. - rewrite Heq3 in Htif. simpl in Htif. - rewrite !Atom.t_interp_wf in Htif; trivial. - rewrite Heq4, Heq6 in Htif. - rewrite Heq5, Heq7 in Htif. - simpl in Htif. - rewrite Hb, Hc in Htif. - rewrite Typ.N_cast_refl in Htif. - unfold Bval in Htif. - rewrite !andb_true_iff in H5. - destruct H5. destruct H5. - - inversion Htif. - - generalize dependent v_valf. - rewrite <- H11. intros. - - unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits. - rewrite N.eqb_eq in Ha, Hd. - - generalize (BITVECTOR_LIST._of_bits_size la n). - - unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits. - - rewrite Hd. - - generalize (BITVECTOR_LIST._of_bits_size lb n). - unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits. - rewrite Ha. - intros. + (* a *) + pose proof (H a). + assert (H1: a < PArray.length t_atom). + { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4, Heq5. easy. } + specialize (@H0 H1). rewrite Heq4 in H0. simpl in H0. + unfold get_type' in H0. unfold v_type in H0. + case_eq (t_interp .[ a]). + intros v_typea v_vala Htia. rewrite Htia in H0. + rewrite Atom.t_interp_wf in Htia; trivial. + rewrite Heq4, Heq5 in Htia. simpl in Htia. + rewrite Hb in Htia. + unfold Bval in Htia. + rewrite Heq5 in H0. simpl in H0. + inversion Htia. + + generalize dependent v_vala. + rewrite <- H3. intros. + + (* b *) + pose proof (H b). + assert (H4: b < PArray.length t_atom). + { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6, Heq7. easy. } + specialize (@H2 H4). rewrite Heq6 in H2. simpl in H2. + unfold get_type' in H2. unfold v_type in H2. + case_eq (t_interp .[ b]). + intros v_typeb v_valb Htib. rewrite Htib in H2. + rewrite Atom.t_interp_wf in Htib; trivial. + rewrite Heq6, Heq7 in Htib. simpl in Htib. + rewrite Hc in Htib. + unfold Bval in Htib. + rewrite Heq7 in H2. simpl in H2. + inversion Htib. + + generalize dependent v_valb. + rewrite <- H6. intros. + + (* f *) + pose proof (H f). + assert (H7: f < PArray.length t_atom). + { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. } + specialize (@H5 H7). rewrite Heq3 in H5. simpl in H5. + unfold get_type' in H5. unfold v_type in H5. + case_eq (t_interp .[ f]). + intros v_typef v_valf Htif. rewrite Htif in H5. + rewrite Atom.t_interp_wf in Htif; trivial. + rewrite Heq3 in Htif. simpl in Htif. + rewrite !Atom.t_interp_wf in Htif; trivial. + rewrite Heq4, Heq6 in Htif. + rewrite Heq5, Heq7 in Htif. + simpl in Htif. + rewrite Hb, Hc in Htif. + rewrite Typ.N_cast_refl in Htif. + unfold Bval in Htif. + rewrite !andb_true_iff in H5. + destruct H5. destruct H5. + + inversion Htif. + + generalize dependent v_valf. + rewrite <- H11. intros. + + unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits. + rewrite N.eqb_eq in Ha, Hd. + + generalize (BITVECTOR_LIST._of_bits_size la n). + + unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits. + + rewrite Hd. + + generalize (BITVECTOR_LIST._of_bits_size lb n). + unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits. + rewrite Ha. + intros. - unfold Typ.i_eqb. simpl. - unfold BITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.bv_eq. - simpl. - rewrite e, e0. - rewrite N.eqb_refl. - unfold RAWBITVECTOR_LIST.bits. + change (Typ.i_eqb t_i (Typ.TBV n)) with (@BITVECTOR_LIST.bv_eq n). + unfold BITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.bv_eq. + simpl. + rewrite e, e0. + rewrite N.eqb_refl. + unfold RAWBITVECTOR_LIST.bits. - apply diseq_neg_eq. easy. + apply diseq_neg_eq. easy. Qed. Lemma prop_checkbb: forall (a: int) (bs: list _lit) (i n: nat), @@ -4718,8 +4718,8 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). (** case symmetry **) - (* interp_form_hatom_bv a1' = - interp_bv t_i (interp_atom (t_atom .[a1'])) *) + (* interp_form_hatom_bv a1' = *) +(* interp_bv t_i (interp_atom (t_atom .[a1'])) *) assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { @@ -4737,8 +4737,8 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). rewrite Htia1 in HSp2. unfold interp_bv in HSp2. - (* interp_form_hatom_bv a2' = - interp_bv t_i (interp_atom (t_atom .[a2'])) *) + (* interp_form_hatom_bv a2' = *) +(* interp_bv t_i (interp_atom (t_atom .[a2'])) *) assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index 5f79faf..f8d5b50 100644 --- a/src/classes/SMT_classes.v +++ b/src/classes/SMT_classes.v @@ -28,7 +28,7 @@ Definition eqb_to_eq_dec : Defined. -(** Types with a Boolean equality that reflects in Leibniz equality *) +(** Types with a Boolean equality that reflects Leibniz equality *) Class EqbType T := { eqb : T -> T -> bool; eqb_spec : forall x y, eqb x y = true <-> x = y @@ -37,32 +37,65 @@ Class EqbType T := { (** Types with a decidable equality *) Class DecType T := { - eq_refl : forall x : T, x = x; - eq_sym : forall x y : T, x = y -> y = x; - eq_trans : forall x y z : T, x = y -> y = z -> x = z; eq_dec : forall x y : T, { x = y } + { x <> y } }. -Hint Immediate eq_sym. -Hint Resolve eq_refl eq_trans. - (** Types equipped with Boolean equality are decidable *) -Instance EqbToDecType T `(EqbType T) : DecType T. -Proof. - destruct H. - split; auto. - intros; subst; auto. - apply (eqb_to_eq_dec _ eqb0); auto. -Defined. +Section EqbToDecType. + Generalizable Variable T. + Context `{ET : EqbType T}. + + Instance EqbToDecType : DecType T. + Proof. + destruct ET as [eqb0 Heqb0]. split. + apply (eqb_to_eq_dec _ eqb0); auto. + Defined. +End EqbToDecType. + + +(** Basic properties on types with Boolean equality *) +Section EqbTypeProp. + Generalizable Variable T. + Context `{ET : EqbType T}. + + Lemma eqb_refl x : eqb x x = true. + Proof. now rewrite eqb_spec. Qed. + + Lemma eqb_sym x y : eqb x y = true -> eqb y x = true. + Proof. rewrite !eqb_spec. now intros ->. Qed. + + Lemma eqb_trans x y z : eqb x y = true -> eqb y z = true -> eqb x z = true. + Proof. rewrite !eqb_spec. now intros ->. Qed. + + Lemma eqb_spec_false x y : eqb x y = false <-> x <> y. + Proof. + split. + - intros H1 H2. subst y. rewrite eqb_refl in H1. inversion H1. + - intro H. case_eq (eqb x y); auto. intro H1. elim H. now rewrite <- eqb_spec. + Qed. + + Lemma reflect_eqb x y : reflect (x = y) (eqb x y). + Proof. + case_eq (eqb x y); intro H; constructor. + - now rewrite eqb_spec in H. + - now rewrite eqb_spec_false in H. + Qed. + + Lemma eqb_sym2 x y : eqb x y = eqb y x. + Proof. + case_eq (eqb y x); intro H. + - now apply eqb_sym. + - rewrite eqb_spec_false in *. auto. + Qed. +End EqbTypeProp. (** Class of types with a partial order *) Class OrdType T := { lt: T -> T -> Prop; lt_trans : forall x y z : T, lt x y -> lt y z -> lt x z; - lt_not_eq : forall x y : T, lt x y -> ~ eq x y - (* compare : forall x y : T, Compare lt eq x y *) + lt_not_eq : forall x y : T, lt x y -> x <> y }. Hint Resolve lt_not_eq lt_trans. @@ -84,6 +117,29 @@ Class Comparable T {ot:OrdType T} := { }. +(* A Comparable type is also an EqbType *) +Section Comparable2EqbType. + Generalizable Variable T. + Context `{OTT : OrdType T}. + Context `{CT : Comparable T}. + + Definition compare2eqb (x y:T) : bool := + match compare x y with + | EQ _ => true + | _ => false + end. + + Lemma compare2eqb_spec x y : compare2eqb x y = true <-> x = y. + Proof. + unfold compare2eqb. + case_eq (compare x y); simpl; intros e He; split; try discriminate; + try (intros ->; elim (lt_not_eq _ _ e (eq_refl _))); auto. + Qed. + + Instance Comparable2EqbType : EqbType T := Build_EqbType _ _ compare2eqb_spec. +End Comparable2EqbType. + + (** Class of inhabited types *) Class Inhabited T := { default_value : T @@ -92,53 +148,44 @@ Class Inhabited T := { (** * CompDec: Merging all previous classes *) Class CompDec T := { - ty := T; - Eqb :> EqbType ty; - Decidable := EqbToDecType ty Eqb; - Ordered :> OrdType ty; - Comp :> @Comparable ty Ordered; - Inh :> Inhabited ty + Eqb :> EqbType T; (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *) + Ordered :> OrdType T; + Comp :> @Comparable T Ordered; + Inh :> Inhabited T }. -Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) := - let (_, _, _, ord, _, _) := c in ord. +Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) := + let (eqb, _, _, _) := c in eqb. -Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) := - let (_, _, _, _, _, inh) := c in inh. +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) := + let (_, _, _, inh) := c in inh. Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t). -destruct c; trivial. + destruct c; trivial. Defined. -Instance eqbtype_of_compdec t `{c: CompDec t} : EqbType t := - let (_, eqbtype, _, _, _, inh) := c in eqbtype. - -Instance dec_of_compdec t `{c: CompDec t} : DecType t := - let (_, _, dec, _, _, inh) := c in dec. - - -Definition type_compdec {ty:Type} (cd : CompDec ty) := ty. Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool := - match c with - | {| ty := ty; Eqb := {| eqb := eqb |} |} => eqb + match eqbtype_of_compdec t with + | {| eqb := eqb |} => eqb end. Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T, x = y <-> eqb_of_compdec c x y = true. Proof. - destruct c. destruct Eqb0. - simpl. intros. rewrite eqb_spec0. reflexivity. + intros x y. destruct c as [[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 - dec_of_compdec : typeclass_instances. + eqbtype_of_compdec : typeclass_instances. Record typ_compdec : Type := Typ_compdec { @@ -146,28 +193,30 @@ Record typ_compdec : Type := Typ_compdec { te_compdec : CompDec te_carrier }. + Section CompDec_from. Variable T : Type. + Variable eqb' : T -> T -> bool. + Variable eqb'_spec : forall x y, eqb' x y = true <-> x = y. + Variable lt' : T -> T -> Prop. - Variable d : T. + Hypothesis lt'_trans : forall x y z : T, lt' x y -> lt' y z -> lt' x z. + Hypothesis lt'_neq : forall x y : T, lt' x y -> x <> y. - Hypothesis eqb_spec' : forall x y : T, eqb' x y = true <-> x = y. - Hypothesis lt_trans': forall x y z : T, lt' x y -> lt' y z -> lt' x z. - Hypothesis lt_neq': forall x y : T, lt' x y -> x <> y. - Variable compare': forall x y : T, Compare lt' eq x y. - + + Variable d : T. + Program Instance CompDec_from : (CompDec T) := {| - Eqb := {| eqb := eqb' |}; - Ordered := {| lt := lt'; lt_trans := lt_trans' |}; + Eqb := {| eqb := eqb'; eqb_spec := eqb'_spec |}; + Ordered := {| lt := lt'; lt_trans := lt'_trans |}; Comp := {| compare := compare' |}; Inh := {| default_value := d |} |}. - Definition typ_compdec_from : typ_compdec := Typ_compdec T CompDec_from. - + End CompDec_from. diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index 71318df..339d710 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -18,45 +18,37 @@ Require Export SMT_classes. Section Unit. - Let eqb : unit -> unit -> bool := fun _ _ => true. Let lt : unit -> unit -> Prop := fun _ _ => False. - - Instance unit_ord : OrdType unit. + + Global Instance unit_ord : OrdType unit. Proof. exists lt; unfold lt; trivial. intros; contradict H; trivial. Defined. - Instance unit_eqbtype : EqbType unit. + Global Instance unit_eqbtype : EqbType unit. Proof. exists eqb. intros. destruct x, y. unfold eqb. split; trivial. Defined. - Instance unit_comp : @Comparable unit unit_ord. + Global Instance unit_comp : @Comparable unit unit_ord. Proof. split. intros. destruct x, y. apply OrderedType.EQ; trivial. Defined. - Instance unit_inh : Inhabited unit := {| default_value := tt |}. - - Instance unit_compdec : CompDec unit := {| + Global Instance unit_inh : Inhabited unit := {| default_value := tt |}. + + Global Instance unit_compdec : CompDec unit := {| Eqb := unit_eqbtype; Ordered := unit_ord; Comp := unit_comp; Inh := unit_inh |}. - - Definition unit_typ_compdec := Typ_compdec unit unit_compdec. - - Lemma eqb_eq_unit : forall x y, eqb x y <-> x = y. - Proof. intros. split; case x; case y; unfold eqb; intros; now auto. - Qed. - End Unit. @@ -65,23 +57,17 @@ Section Bool. Definition ltb_bool x y := negb x && y. Definition lt_bool x y := ltb_bool x y = true. - - Instance bool_ord : OrdType bool. + + Global Instance bool_ord : OrdType bool. Proof. exists lt_bool. intros x y z. - case x; case y; case z; intros; simpl; subst; auto. + case x; case y; case z; intros; simpl; subst; auto. intros x y. - case x; case y; intros; simpl in H; easy. + case x; case y; intros; simpl in H; easy. Defined. - Instance bool_eqbtype : EqbType bool := - {| eqb := Bool.eqb; eqb_spec := eqb_true_iff |}. - - Instance bool_dec : DecType bool := - EqbToDecType _ bool_eqbtype. - - Instance bool_comp: Comparable bool. + Global Instance bool_comp: Comparable bool. Proof. constructor. intros x y. @@ -99,11 +85,16 @@ Section Bool. case x in *; case y in *; auto. Defined. - Instance bool_inh : Inhabited bool := {| default_value := false|}. + Global Instance bool_eqbtype : EqbType bool := + {| eqb := Bool.eqb; eqb_spec := eqb_true_iff |}. + + Global Instance bool_dec : DecType bool := EqbToDecType. + + Global Instance bool_inh : Inhabited bool := {| default_value := false|}. - Instance bool_compdec : CompDec bool := {| - Eqb := bool_eqbtype; - Ordered := bool_ord; + Global Instance bool_compdec : CompDec bool := {| + Eqb := bool_eqbtype; + Ordered := bool_ord; Comp := bool_comp; Inh := bool_inh |}. @@ -119,36 +110,32 @@ End Bool. Section Z. - Instance Z_ord : OrdType Z. + Global Instance Z_ord : OrdType Z. Proof. exists Z_as_OT.lt. exact Z_as_OT.lt_trans. exact Z_as_OT.lt_not_eq. Defined. - Instance Z_eqbtype : EqbType Z := - {| eqb := Z.eqb; eqb_spec := Z.eqb_eq |}. - - (* Instance Z_eqbtype : EqbType Z := *) - (* {| eqb := Zeq_bool; eqb_spec := fun x y => symmetry (Zeq_is_eq_bool x y) |}. *) - - Instance Z_dec : DecType Z := - EqbToDecType _ Z_eqbtype. - - Instance Z_comp: Comparable Z. + Global Instance Z_comp: Comparable Z. Proof. constructor. apply Z_as_OT.compare. Defined. + Global Instance Z_eqbtype : EqbType Z := + {| eqb := Z.eqb; eqb_spec := Z.eqb_eq |}. + + Global Instance Z_dec : DecType Z := @EqbToDecType _ Z_eqbtype. + + + Global Instance Z_inh : Inhabited Z := {| default_value := 0%Z |}. - Instance Z_inh : Inhabited Z := {| default_value := 0%Z |}. - - Instance Z_compdec : CompDec Z := {| - Eqb := Z_eqbtype; - Ordered := Z_ord; + Global Instance Z_compdec : CompDec Z := {| + Eqb := Z_eqbtype; + Ordered := Z_ord; Comp := Z_comp; Inh := Z_inh |}. @@ -202,7 +189,7 @@ Section Z. Lemma lt_Z_B2P': forall x y, ltP_Z x y <-> Z.lt x y. Proof. intros x y; split; intro H. - unfold ltP_Z in H. + unfold ltP_Z in H. case_eq ((x Z.le x y. Proof. intros x y; split; intro H. - unfold leP_Z in H. + unfold leP_Z in H. case_eq ((x <=? y)%Z ); intros; rewrite H0 in H; try easy. now apply Z.leb_le in H0. apply le_Z_B2P. @@ -220,7 +207,7 @@ Section Z. Lemma gt_Z_B2P': forall x y, gtP_Z x y <-> Z.gt x y. Proof. intros x y; split; intro H. - unfold gtP_Z in H. + unfold gtP_Z in H. case_eq ((x >? y)%Z ); intros; rewrite H0 in H; try easy. now apply Zgt_is_gt_bool in H0. apply gt_Z_B2P. @@ -229,7 +216,7 @@ Section Z. Lemma ge_Z_B2P': forall x y, geP_Z x y <-> Z.ge x y. Proof. intros x y; split; intro H. - unfold geP_Z in H. + unfold geP_Z in H. case_eq ((x >=? y)%Z ); intros; rewrite H0 in H; try easy. rewrite Z.geb_leb in H0. rewrite le_Z_B2P in H0. apply le_Z_B2P' in H0. now apply Z.ge_le_iff. @@ -250,34 +237,33 @@ End Z. Section Nat. - Instance Nat_ord : OrdType nat. + Global Instance Nat_ord : OrdType nat. Proof. - + exists Nat_as_OT.lt. exact Nat_as_OT.lt_trans. exact Nat_as_OT.lt_not_eq. Defined. - Instance Nat_eqbtype : EqbType nat := - {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}. - - Instance Nat_dec : DecType nat := - EqbToDecType _ Nat_eqbtype. - - Instance Nat_comp: Comparable nat. + Global Instance Nat_comp: Comparable nat. Proof. constructor. apply Nat_as_OT.compare. Defined. + Global Instance Nat_eqbtype : EqbType nat := + {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}. + + Global Instance Nat_dec : DecType nat := EqbToDecType. + - Instance Nat_inh : Inhabited nat := {| default_value := O%nat |}. + Global Instance Nat_inh : Inhabited nat := {| default_value := O%nat |}. - - Instance Nat_compdec : CompDec nat := {| - Eqb := Nat_eqbtype; - Ordered := Nat_ord; + + Global Instance Nat_compdec : CompDec nat := {| + Eqb := Nat_eqbtype; + Ordered := Nat_ord; Comp := Nat_comp; Inh := Nat_inh |}. @@ -287,30 +273,29 @@ End Nat. Section Positive. - Instance Positive_ord : OrdType positive. + Global Instance Positive_ord : OrdType positive. Proof. exists Positive_as_OT.lt. exact Positive_as_OT.lt_trans. exact Positive_as_OT.lt_not_eq. Defined. - Instance Positive_eqbtype : EqbType positive := - {| eqb := Pos.eqb; eqb_spec := Pos.eqb_eq |}. - - Instance Positive_dec : DecType positive := - EqbToDecType _ Positive_eqbtype. - - Instance Positive_comp: Comparable positive. + Global Instance Positive_comp: Comparable positive. Proof. constructor. apply Positive_as_OT.compare. Defined. - Instance Positive_inh : Inhabited positive := {| default_value := 1%positive |}. + Global Instance Positive_eqbtype : EqbType positive := + {| eqb := Pos.eqb; eqb_spec := Pos.eqb_eq |}. + + Global Instance Positive_dec : DecType positive := EqbToDecType. - Instance Positive_compdec : CompDec positive := {| - Eqb := Positive_eqbtype; - Ordered := Positive_ord; + Global Instance Positive_inh : Inhabited positive := {| default_value := 1%positive |}. + + Global Instance Positive_compdec : CompDec positive := {| + Eqb := Positive_eqbtype; + Ordered := Positive_ord; Comp := Positive_comp; Inh := Positive_inh |}. @@ -323,8 +308,8 @@ Section BV. Import BITVECTOR_LIST. - - Instance BV_ord n : OrdType (bitvector n). + + Global Instance BV_ord n : OrdType (bitvector n). Proof. exists (fun a b => (bv_ult a b)). unfold bv_ult, RAWBITVECTOR_LIST.bv_ult. @@ -342,15 +327,8 @@ Section BV. apply H. easy. Defined. - Instance BV_eqbtype n : EqbType (bitvector n) := - {| eqb := @bv_eq n; - eqb_spec := @bv_eq_reflect n |}. - Instance BV_dec n : DecType (bitvector n) := - EqbToDecType _ (BV_eqbtype n). - - - Instance BV_comp n: Comparable (bitvector n). + Global Instance BV_comp n: Comparable (bitvector n). Proof. constructor. intros x y. @@ -388,13 +366,19 @@ Section BV. now apply RAWBITVECTOR_LIST.rev_neq in H. Defined. - Instance BV_inh n : Inhabited (bitvector n) := + Global Instance BV_eqbtype n : EqbType (bitvector n) := + {| eqb := @bv_eq n; + eqb_spec := @bv_eq_reflect n |}. + + Global Instance BV_dec n : DecType (bitvector n) := EqbToDecType. + + Global Instance BV_inh n : Inhabited (bitvector n) := {| default_value := zeros n |}. - Instance BV_compdec n: CompDec (bitvector n) := {| - Eqb := BV_eqbtype n; - Ordered := BV_ord n; + Global Instance BV_compdec n: CompDec (bitvector n) := {| + Eqb := BV_eqbtype n; + Ordered := BV_ord n; Comp := BV_comp n; Inh := BV_inh n |}. @@ -405,10 +389,9 @@ End BV. Section FArray. - Instance FArray_ord key elt + Global Instance FArray_ord key elt `{key_ord: OrdType key} `{elt_ord: OrdType elt} - `{elt_dec: DecType elt} `{elt_inh: Inhabited elt} `{key_comp: @Comparable key key_ord} : OrdType (farray key elt). Proof. @@ -419,10 +402,30 @@ Section FArray. apply lt_farray_not_eq in H. apply H. rewrite H0. - apply eqfarray_refl. auto. + apply eqfarray_refl. Defined. - Instance FArray_eqbtype key elt + + Global Instance FArray_comp key elt + `{key_ord: OrdType key} + `{elt_ord: OrdType elt} + `{key_comp: @Comparable key key_ord} + `{elt_inh: Inhabited elt} + `{elt_comp: @Comparable elt elt_ord} : Comparable (farray key elt). + Proof. + constructor. + intros. + destruct (compare_farray key_comp elt_comp x y). + - apply OrderedType.LT. auto. + - apply OrderedType.EQ. + specialize (@eq_equal key elt key_ord key_comp elt_ord elt_comp elt_inh x y). + intros. + apply H in e. + now apply equal_eq in e. + - apply OrderedType.GT. auto. + Defined. + + Global Instance FArray_eqbtype key elt `{key_ord: OrdType key} `{elt_ord: OrdType elt} `{elt_eqbtype: EqbType elt} @@ -436,88 +439,48 @@ Section FArray. split. apply FArray.equal_eq. intros. subst. apply eq_equal. apply eqfarray_refl. - apply EqbToDecType. auto. Defined. - - Instance FArray_dec key elt + Global Instance FArray_dec key elt `{key_ord: OrdType key} `{elt_ord: OrdType elt} `{elt_eqbtype: EqbType elt} `{key_comp: @Comparable key key_ord} `{elt_comp: @Comparable elt elt_ord} `{elt_inh: Inhabited elt} - : DecType (farray key elt) := - EqbToDecType _ (FArray_eqbtype key elt). + : DecType (farray key elt) := EqbToDecType. - - Instance FArray_comp key elt - `{key_ord: OrdType key} - `{elt_ord: OrdType elt} - `{elt_eqbtype: EqbType elt} - `{key_comp: @Comparable key key_ord} - `{elt_inh: Inhabited elt} - `{elt_comp: @Comparable elt elt_ord} : Comparable (farray key elt). - Proof. - constructor. - intros. - destruct (compare_farray key_comp (EqbToDecType _ elt_eqbtype) elt_comp x y). - - apply OrderedType.LT. auto. - - apply OrderedType.EQ. - specialize (@eq_equal key elt key_ord key_comp elt_ord elt_comp elt_inh x y). - intros. - apply H in e. - now apply equal_eq in e. - - apply OrderedType.GT. auto. - Defined. - - Instance FArray_inh key elt + Global Instance FArray_inh key elt `{key_ord: OrdType key} `{elt_inh: Inhabited elt} : Inhabited (farray key elt) := {| default_value := FArray.empty key_ord elt_inh |}. - Program Instance FArray_compdec key elt + Global Instance FArray_compdec key elt `{key_compdec: CompDec key} `{elt_compdec: CompDec elt} : CompDec (farray key elt) := {| Eqb := FArray_eqbtype key elt; Ordered := FArray_ord key elt; - (* Comp := FArray_comp key elt ; *) + Comp := FArray_comp key elt ; Inh := FArray_inh key elt |}. - - Next Obligation. - constructor. - destruct key_compdec, elt_compdec. - simpl in *. - unfold lt_farray. - intros. simpl. - unfold EqbToDecType. simpl. - case_eq (compare x y); intros. - apply OrderedType.LT. - destruct (compare x y); try discriminate H; auto. - apply OrderedType.EQ. - destruct (compare x y); try discriminate H; auto. - apply OrderedType.GT. - destruct (compare y x); try discriminate H; auto; clear H. - Defined. End FArray. Section Int63. - + Local Open Scope int63_scope. Let int_lt x y := if Int63Native.ltb x y then True else False. - - Instance int63_ord : OrdType int. + + Global Instance int63_ord : OrdType int. Proof. exists int_lt; unfold int_lt. - - intros x y z. + - intros x y z. case_eq (x < y); intro; case_eq (y < z); intro; case_eq (x < z); intro; @@ -533,15 +496,9 @@ Section Int63. rewrite <- Int63Properties.to_Z_eq. exact (Z.lt_neq _ _ H). Defined. - - Instance int63_eqbtype : EqbType int := - {| eqb := Int63Native.eqb; eqb_spec := Int63Properties.eqb_spec |}. - Instance int63_dec : DecType int := - EqbToDecType _ int63_eqbtype. - - Instance int63_comp: Comparable int. + Global Instance int63_comp: Comparable int. Proof. constructor. intros x y. @@ -566,16 +523,20 @@ Section Int63. rewrite H0. auto. Defined. + Global Instance int63_eqbtype : EqbType int := + {| eqb := Int63Native.eqb; eqb_spec := Int63Properties.eqb_spec |}. + + Global Instance int63_dec : DecType int := EqbToDecType. + - Instance int63_inh : Inhabited int := {| default_value := 0 |}. - - Instance int63_compdec : CompDec int := {| - Eqb := int63_eqbtype; - Ordered := int63_ord; + Global Instance int63_inh : Inhabited int := {| default_value := 0 |}. + + Global Instance int63_compdec : CompDec int := {| + Eqb := int63_eqbtype; + Ordered := int63_ord; Comp := int63_comp; Inh := int63_inh |}. - End Int63. @@ -586,25 +547,6 @@ Section option. Context `{HA : CompDec A}. - Definition option_eqb (x y : option A) : bool := - match x, y with - | Some a, Some b => eqb a b - | None, None => true - | _, _ => false - end. - - - Lemma option_eqb_spec : forall (x y : option A), option_eqb x y = true <-> x = y. - Proof. - intros [a| ] [b| ]; simpl; split; try discriminate; auto. - - intro H. rewrite eqb_spec in H. now subst b. - - intros H. inversion H as [H1]. now rewrite eqb_spec. - Qed. - - - Instance option_eqbtype : EqbType (option A) := Build_EqbType _ _ option_eqb_spec. - - Definition option_lt (x y : option A) : Prop := match x, y with | Some a, Some b => lt a b @@ -631,7 +573,7 @@ Section option. Qed. - Instance option_ord : OrdType (option A) := + Global Instance option_ord : OrdType (option A) := Build_OrdType _ _ option_lt_trans option_lt_not_eq. @@ -647,15 +589,15 @@ Section option. - now apply EQ. Defined. + Global Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare. - Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare. + Global Instance option_eqbtype : EqbType (option A) := Comparable2EqbType. - Instance option_inh : Inhabited (option A) := Build_Inhabited _ None. + Global Instance option_inh : Inhabited (option A) := Build_Inhabited _ None. - Instance option_compdec : CompDec (option A) := {| - Eqb := option_eqbtype; + Global Instance option_compdec : CompDec (option A) := {| Ordered := option_ord; Comp := option_comp; Inh := option_inh @@ -670,27 +612,6 @@ Section list. Context `{HA : CompDec A}. - Fixpoint list_eqb (xs ys : list A) : bool := - match xs, ys with - | nil, nil => true - | x::xs, y::ys => eqb x y && list_eqb xs ys - | _, _ => false - end. - - - Lemma list_eqb_spec : forall (x y : list A), list_eqb x y = true <-> x = y. - Proof. - induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; split; try discriminate; auto. - - rewrite andb_true_iff. intros [H1 H2]. rewrite eqb_spec in H1. rewrite IHxs in H2. now subst. - - intros H. inversion H as [H1]. rewrite andb_true_iff; split. - + now rewrite eqb_spec. - + subst ys. now rewrite IHxs. - Qed. - - - Instance list_eqbtype : EqbType (list A) := Build_EqbType _ _ list_eqb_spec. - - Fixpoint list_lt (xs ys : list A) : Prop := match xs, ys with | nil, nil => False @@ -700,6 +621,22 @@ Section list. end. + Definition list_compare : forall (x y : list A), Compare list_lt Logic.eq x y. + Proof. + induction x as [ |x xs IHxs]; intros [ |y ys]; simpl. + - now apply EQ. + - now apply LT. + - now apply GT. + - case_eq (compare x y); intros l H. + + apply LT. simpl. now left. + + case_eq (IHxs ys); intros l1 H1. + * apply LT. simpl. right. split; auto. now apply eqb_spec. + * apply EQ. now rewrite l, l1. + * apply GT. simpl. right. split; auto. now apply eqb_spec. + + apply GT. simpl. now left. + Defined. + + Lemma list_lt_trans : forall (x y z : list A), list_lt x y -> list_lt y z -> list_lt x z. Proof. @@ -720,39 +657,24 @@ Section list. induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; auto. - discriminate. - intros [H1|[H1 H2]]; intros H; inversion H; subst. - + eapply lt_not_eq; eauto. - + eapply IHxs; eauto. + + now apply (lt_not_eq _ _ H1). + + now apply (IHxs _ H2). Qed. - Instance list_ord : OrdType (list A) := + Global Instance list_ord : OrdType (list A) := Build_OrdType _ _ list_lt_trans list_lt_not_eq. - Definition list_compare : forall (x y : list A), Compare list_lt Logic.eq x y. - Proof. - induction x as [ |x xs IHxs]; intros [ |y ys]; simpl. - - now apply EQ. - - now apply LT. - - now apply GT. - - case_eq (compare x y); intros l H. - + apply LT. simpl. now left. - + case_eq (IHxs ys); intros l1 H1. - * apply LT. simpl. right. split; auto. now apply eqb_spec. - * apply EQ. now rewrite l, l1. - * apply GT. simpl. right. split; auto. now apply eqb_spec. - + apply GT. simpl. now left. - Defined. - + Global Instance list_comp : Comparable (list A) := Build_Comparable _ _ list_compare. - Instance list_comp : Comparable (list A) := Build_Comparable _ _ list_compare. + Global Instance list_eqbtype : EqbType (list A) := Comparable2EqbType. - Instance list_inh : Inhabited (list A) := Build_Inhabited _ nil. + Global Instance list_inh : Inhabited (list A) := Build_Inhabited _ nil. - Instance list_compdec : CompDec (list A) := {| - Eqb := list_eqbtype; + Global Instance list_compdec : CompDec (list A) := {| Ordered := list_ord; Comp := list_comp; Inh := list_inh -- cgit