From a1b9346cb2be60342a8b80b2e8082fcf2023baf8 Mon Sep 17 00:00:00 2001 From: ilya Date: Tue, 7 Apr 2020 19:33:18 +0300 Subject: proposed fix for the issue #12015 (String_as_OT) --- theories/Structures/OrderedTypeEx.v | 167 ++++++++++++++++++++++++++++++------ 1 file changed, 142 insertions(+), 25 deletions(-) diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 288aa0c789..b99de1e3af 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -378,32 +378,149 @@ Module String_as_OT <: UsualOrderedType. apply Nat.lt_irrefl in H2; auto. Qed. - Definition compare x y : Compare lt eq x y. + + Definition ascii_compare (a b : ascii) : comparison := + N.compare (N_of_ascii a) (N_of_ascii b). + + Lemma ascii_compare_eq (a b : ascii): + ascii_compare a b = Eq <-> a = b. Proof. - generalize dependent y. - induction x as [ | a s1]; destruct y as [ | b s2]. - - apply EQ; constructor. - - apply LT; constructor. - - apply GT; constructor. - - destruct ((nat_of_ascii a) ?= (nat_of_ascii b))%nat eqn:ltb. - + assert (a = b). - { - apply Nat.compare_eq in ltb. - assert (ascii_of_nat (nat_of_ascii a) - = ascii_of_nat (nat_of_ascii b)) by auto. - repeat rewrite ascii_nat_embedding in H. - auto. - } - subst. - destruct (IHs1 s2). - * apply LT; constructor; auto. - * apply EQ. unfold eq in e. subst. constructor; auto. - * apply GT; constructor; auto. - + apply nat_compare_lt in ltb. - apply LT; constructor; auto. - + apply nat_compare_gt in ltb. - apply GT; constructor; auto. - Defined. + unfold ascii_compare. + rewrite N.compare_eq_iff. + split. 2:{ intro. now subst. } + intro H. + rewrite<- (ascii_N_embedding a). + rewrite<- (ascii_N_embedding b). + now rewrite H. + Qed. + + Lemma ascii_compare_lt (a b : ascii): + ascii_compare a b = Lt <-> (nat_of_ascii a < nat_of_ascii b)%nat. + Proof. + unfold ascii_compare. unfold nat_of_ascii. + rewrite N2Nat.inj_compare. + rewrite Nat.compare_lt_iff. + reflexivity. + Qed. + + Fixpoint cmp (a b : string) : comparison := + match a with + | EmptyString => + match b with + | EmptyString => Eq + | _ => Lt + end + | String a_head a_tail => + match b with + | EmptyString => Gt + | String b_head b_tail => + match ascii_compare a_head b_head with + | Lt => Lt + | Gt => Gt + | Eq => cmp a_tail b_tail + end + end + end. + + Lemma cmp_eq (a b : string): + cmp a b = Eq <-> a = b. + Proof. + generalize b. clear b. + induction a; intro b. { induction b; easy. } + cbn. + destruct b. { easy. } + remember (ascii_compare _ _) as cmp. symmetry in Heqcmp. + destruct cmp; split; try discriminate; + try rewrite ascii_compare_eq in Heqcmp; try subst; + try rewrite IHa; intro H. + { now subst. } + { now inversion H. } + { inversion H; subst. rewrite<- Heqcmp. now rewrite ascii_compare_eq. } + { inversion H; subst. rewrite<- Heqcmp. now rewrite ascii_compare_eq. } + Qed. + + Lemma ascii_compare_antisym (a b : ascii): + ascii_compare a b = CompOpp (ascii_compare b a). + Proof. + unfold ascii_compare. + apply N.compare_antisym. + Qed. + + Lemma cmp_antisym (a b : string): + cmp a b = CompOpp (cmp b a). + Proof. + generalize b. clear b. + induction a. { destruct b; easy. } + intro b. destruct b. { easy. } + cbn. rewrite IHa. clear IHa. + remember (ascii_compare _ _) as cmp. symmetry in Heqcmp. + destruct cmp; rewrite ascii_compare_antisym in Heqcmp; destruct ascii_compare; cbn in *; easy. + Qed. + + Lemma cmp_lt (a b : string): + cmp a b = Lt <-> lt a b. + Proof. + generalize b. clear b. + induction a as [ | a_head a_tail ]. + { + destruct b. { easy. } + cbn. split; trivial. intro. apply lts_empty. + } + intro b. cbn. destruct b. { easy. } + remember (ascii_compare _ _) as cmp. symmetry in Heqcmp. + destruct cmp; split; intro H; try discriminate; trivial. + { + rewrite ascii_compare_eq in Heqcmp. subst. + apply String_as_OT.lts_tail. + apply IHa_tail. + assumption. + } + { + rewrite ascii_compare_eq in Heqcmp. subst. + inversion H; subst. { rewrite IHa_tail. assumption. } + exfalso. apply (Nat.lt_irrefl (nat_of_ascii a)). assumption. + } + { + apply String_as_OT.lts_head. + rewrite<- ascii_compare_lt. + assumption. + } + { + exfalso. inversion H; subst. + { + assert(X: ascii_compare a a = Eq). { apply ascii_compare_eq. trivial. } + rewrite Heqcmp in X. discriminate. + } + rewrite<- ascii_compare_lt in *. rewrite Heqcmp in *. discriminate. + } + Qed. + + Local Lemma compare_helper_lt {a b : string} (L : cmp a b = Lt): + lt a b. + Proof. + now apply cmp_lt. + Qed. + + Local Lemma compare_helper_gt {a b : string} (G : cmp a b = Gt): + lt b a. + Proof. + rewrite cmp_antisym in G. + rewrite CompOpp_iff in G. + now apply cmp_lt. + Qed. + + Local Lemma compare_helper_eq {a b : string} (E : cmp a b = Eq): + a = b. + Proof. + now apply cmp_eq. + Qed. + + Definition compare (a b : string) : Compare lt eq a b := + match cmp a b as z return _ = z -> _ with + | Lt => fun E => LT (compare_helper_lt E) + | Gt => fun E => GT (compare_helper_gt E) + | Eq => fun E => EQ (compare_helper_eq E) + end Logic.eq_refl. Definition eq_dec (x y : string): {x = y} + { ~ (x = y)} := string_dec x y. End String_as_OT. -- cgit v1.2.3 From 808fe6cdc19949a11171770838612613a3df9cf9 Mon Sep 17 00:00:00 2001 From: ilya Date: Tue, 7 Apr 2020 23:07:14 +0300 Subject: Integrated changes proposed by @JasonGross --- theories/Structures/OrderedTypeEx.v | 227 +++++++++++++++++++++--------------- 1 file changed, 130 insertions(+), 97 deletions(-) diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index b99de1e3af..83c690ab71 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -317,6 +317,82 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. End PositiveOrderedTypeBits. +Module Ascii_as_OT <: UsualOrderedType. + Definition t := ascii. + + Definition eq := @eq ascii. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. + + Definition cmp (a b : ascii) : comparison := + N.compare (N_of_ascii a) (N_of_ascii b). + + Lemma cmp_eq (a b : ascii): + cmp a b = Eq <-> a = b. + Proof. + unfold cmp. + rewrite N.compare_eq_iff. + split. 2:{ intro. now subst. } + intro H. + rewrite<- (ascii_N_embedding a). + rewrite<- (ascii_N_embedding b). + now rewrite H. + Qed. + + Lemma cmp_lt_nat (a b : ascii): + cmp a b = Lt <-> (nat_of_ascii a < nat_of_ascii b)%nat. + Proof. + unfold cmp. unfold nat_of_ascii. + rewrite N2Nat.inj_compare. + rewrite Nat.compare_lt_iff. + reflexivity. + Qed. + + Lemma cmp_antisym (a b : ascii): + cmp a b = CompOpp (cmp b a). + Proof. + unfold cmp. + apply N.compare_antisym. + Qed. + + Definition lt (x y : ascii) := (N_of_ascii x < N_of_ascii y)%N. + + Lemma lt_trans (x y z : ascii): + lt x y -> lt y z -> lt x z. + Proof. + apply N.lt_trans. + Qed. + + Lemma lt_not_eq (x y : ascii): + lt x y -> x <> y. + Proof. + intros L H. subst. + exact (N.lt_irrefl _ L). + Qed. + + Local Lemma compare_helper_eq {a b : ascii} (E : cmp a b = Eq): + a = b. + Proof. + now apply cmp_eq. + Qed. + + Local Lemma compare_helper_gt {a b : ascii} (G : cmp a b = Gt): + lt b a. + Proof. + now apply N.compare_gt_iff. + Qed. + + Definition compare (a b : ascii) : Compare lt eq a b := + match cmp a b as z return _ = z -> _ with + | Lt => fun E => LT E + | Gt => fun E => GT (compare_helper_gt E) + | Eq => fun E => EQ (compare_helper_eq E) + end Logic.eq_refl. + + Definition eq_dec (x y : ascii): {x = y} + { ~ (x = y)} := ascii_dec x y. +End Ascii_as_OT. + (** [String] is an ordered type with respect to the usual lexical order. *) Module String_as_OT <: UsualOrderedType. @@ -378,121 +454,78 @@ Module String_as_OT <: UsualOrderedType. apply Nat.lt_irrefl in H2; auto. Qed. - - Definition ascii_compare (a b : ascii) : comparison := - N.compare (N_of_ascii a) (N_of_ascii b). - - Lemma ascii_compare_eq (a b : ascii): - ascii_compare a b = Eq <-> a = b. - Proof. - unfold ascii_compare. - rewrite N.compare_eq_iff. - split. 2:{ intro. now subst. } - intro H. - rewrite<- (ascii_N_embedding a). - rewrite<- (ascii_N_embedding b). - now rewrite H. - Qed. - - Lemma ascii_compare_lt (a b : ascii): - ascii_compare a b = Lt <-> (nat_of_ascii a < nat_of_ascii b)%nat. - Proof. - unfold ascii_compare. unfold nat_of_ascii. - rewrite N2Nat.inj_compare. - rewrite Nat.compare_lt_iff. - reflexivity. - Qed. - Fixpoint cmp (a b : string) : comparison := - match a with - | EmptyString => - match b with - | EmptyString => Eq - | _ => Lt - end - | String a_head a_tail => - match b with - | EmptyString => Gt - | String b_head b_tail => - match ascii_compare a_head b_head with - | Lt => Lt - | Gt => Gt - | Eq => cmp a_tail b_tail - end - end + match a, b with + | EmptyString, EmptyString => Eq + | EmptyString, _ => Lt + | String _ _, EmptyString => Gt + | String a_head a_tail, String b_head b_tail => + match Ascii_as_OT.cmp a_head b_head with + | Lt => Lt + | Gt => Gt + | Eq => cmp a_tail b_tail + end end. Lemma cmp_eq (a b : string): cmp a b = Eq <-> a = b. Proof. - generalize b. clear b. - induction a; intro b. { induction b; easy. } - cbn. - destruct b. { easy. } - remember (ascii_compare _ _) as cmp. symmetry in Heqcmp. - destruct cmp; split; try discriminate; - try rewrite ascii_compare_eq in Heqcmp; try subst; - try rewrite IHa; intro H. - { now subst. } - { now inversion H. } - { inversion H; subst. rewrite<- Heqcmp. now rewrite ascii_compare_eq. } - { inversion H; subst. rewrite<- Heqcmp. now rewrite ascii_compare_eq. } - Qed. - - Lemma ascii_compare_antisym (a b : ascii): - ascii_compare a b = CompOpp (ascii_compare b a). - Proof. - unfold ascii_compare. - apply N.compare_antisym. + revert b. + induction a, b; try easy. + cbn. + remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc. + destruct c; split; try discriminate; + try rewrite Ascii_as_OT.cmp_eq in Heqc; try subst; + try rewrite IHa; intro H. + { now subst. } + { now inversion H. } + { inversion H; subst. rewrite<- Heqc. now rewrite Ascii_as_OT.cmp_eq. } + { inversion H; subst. rewrite<- Heqc. now rewrite Ascii_as_OT.cmp_eq. } Qed. Lemma cmp_antisym (a b : string): cmp a b = CompOpp (cmp b a). Proof. - generalize b. clear b. - induction a. { destruct b; easy. } - intro b. destruct b. { easy. } - cbn. rewrite IHa. clear IHa. - remember (ascii_compare _ _) as cmp. symmetry in Heqcmp. - destruct cmp; rewrite ascii_compare_antisym in Heqcmp; destruct ascii_compare; cbn in *; easy. + revert b. + induction a, b; try easy. + cbn. rewrite IHa. clear IHa. + remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc. + destruct c; rewrite Ascii_as_OT.cmp_antisym in Heqc; + destruct Ascii_as_OT.cmp; cbn in *; easy. Qed. Lemma cmp_lt (a b : string): cmp a b = Lt <-> lt a b. Proof. - generalize b. clear b. - induction a as [ | a_head a_tail ]. - { - destruct b. { easy. } - cbn. split; trivial. intro. apply lts_empty. - } - intro b. cbn. destruct b. { easy. } - remember (ascii_compare _ _) as cmp. symmetry in Heqcmp. - destruct cmp; split; intro H; try discriminate; trivial. - { - rewrite ascii_compare_eq in Heqcmp. subst. - apply String_as_OT.lts_tail. - apply IHa_tail. - assumption. - } - { - rewrite ascii_compare_eq in Heqcmp. subst. - inversion H; subst. { rewrite IHa_tail. assumption. } - exfalso. apply (Nat.lt_irrefl (nat_of_ascii a)). assumption. - } - { - apply String_as_OT.lts_head. - rewrite<- ascii_compare_lt. - assumption. - } - { - exfalso. inversion H; subst. + revert b. + induction a as [ | a_head a_tail ], b; try easy; cbn. + { split; trivial. intro. apply lts_empty. } + remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc. + destruct c; split; intro H; try discriminate; trivial. + { + rewrite Ascii_as_OT.cmp_eq in Heqc. subst. + apply String_as_OT.lts_tail. + apply IHa_tail. + assumption. + } + { + rewrite Ascii_as_OT.cmp_eq in Heqc. subst. + inversion H; subst. { rewrite IHa_tail. assumption. } + exfalso. apply (Nat.lt_irrefl (nat_of_ascii a)). assumption. + } + { + apply String_as_OT.lts_head. + rewrite<- Ascii_as_OT.cmp_lt_nat. + assumption. + } { - assert(X: ascii_compare a a = Eq). { apply ascii_compare_eq. trivial. } - rewrite Heqcmp in X. discriminate. + exfalso. inversion H; subst. + { + assert(X: Ascii_as_OT.cmp a a = Eq). { apply Ascii_as_OT.cmp_eq. trivial. } + rewrite Heqc in X. discriminate. + } + rewrite<- Ascii_as_OT.cmp_lt_nat in *. rewrite Heqc in *. discriminate. } - rewrite<- ascii_compare_lt in *. rewrite Heqcmp in *. discriminate. - } Qed. Local Lemma compare_helper_lt {a b : string} (L : cmp a b = Lt): -- cgit v1.2.3