Merge PR #12044: proposed fix for the issue #12015 (String_as_OT)

Reviewed-by: JasonGross

1 files changed, 175 insertions, 25 deletions

diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 288aa0c789..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,32 +454,106 @@ Module String_as_OT <: UsualOrderedType.
         apply Nat.lt_irrefl in H2; auto.
   Qed.
 
-  Definition compare x y : Compare lt eq x y.
+  Fixpoint cmp (a b : string) : comparison :=
+    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 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.
+    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.
+    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.
+    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.
+    }
+    {
+      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.
+    }
+  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.