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/SMT_terms.v | 132 +++++++++++++++++++++++++++----------------------------- 1 file changed, 63 insertions(+), 69 deletions(-) (limited to 'src/SMT_terms.v') 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. -- cgit