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 ++++++++++----- src/classes/SMT_classes_instances.v | 368 ++++++++++++++---------------------- 2 files changed, 245 insertions(+), 274 deletions(-) (limited to 'src/classes') 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