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/classes/SMT_classes.v | 151 ++++++++++++++++++++++++++++++---------------- 1 file changed, 100 insertions(+), 51 deletions(-) (limited to 'src/classes/SMT_classes.v') 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. -- cgit