(** Comparison functions. *)
Require Import Coq.Lists.List.
Require Import Coq.Strings.Ascii.
Require Char.
Require Import LString.

Import ListNotations.
Import LString.

(** Total order on strings. *)
Fixpoint compare (x y : t) : comparison :=
  match x, y with
  | [], [] => Eq
  | [], _ => Lt
  | _, [] => Gt
  | x :: xs, y :: ys =>
    match Char.compare x y with
    | Eq => compare xs ys
    | c => c
    end
  end.

Lemma compare_implies_eq : forall (x y : t), compare x y = Eq -> x = y.
(* Goal: forall (x y : t) (_ : @eq comparison (compare x y) Eq), @eq t x y *)
  induction x as [|a x HI]; destruct y as [|b y]; simpl; try congruence.
(* Goal: forall _ : @eq comparison match Char.compare a b with | Eq => compare x y | Lt => Lt | Gt => Gt end Eq, @eq t (@cons ascii a x) (@cons ascii b y) *)
  case_eq (Char.compare a b); simpl; try congruence.
(* Goal: forall (_ : @eq comparison (Char.compare a b) Eq) (_ : @eq comparison (compare x y) Eq), @eq t (@cons ascii a x) (@cons ascii b y) *)
  now intros Hab Hxy; rewrite (Char.compare_implies_eq _ _ Hab); rewrite (HI _ Hxy).
Qed.

Lemma compare_same_is_eq : forall (x : t), compare x x = Eq.
(* Goal: forall x : t, @eq comparison (compare x x) Eq *)
  intro x; induction x; simpl; trivial.
(* Goal: @eq comparison match Char.compare a a with | Eq => compare x x | Lt => Lt | Gt => Gt end Eq *)
  now rewrite Char.compare_same_is_eq; rewrite IHx.
Qed.

(** Test if two strings are equal. *)
Definition eqb (x y : t) : bool :=
  match compare x y with
  | Eq => true
  | _ => false
  end.

Lemma eqb_implies_eq : forall (x y : t), eqb x y = true -> x = y.
(* Goal: forall (x y : t) (_ : @eq bool (eqb x y) true), @eq t x y *)
  intros x y; unfold eqb; case_eq (compare x y); try congruence.
(* Goal: forall (_ : @eq comparison (compare x y) Eq) (_ : @eq bool true true), @eq t x y *)
  now intros; apply compare_implies_eq.
Qed.

Lemma eqb_same_is_eq : forall (x : t), eqb x x = true.
(* Goal: forall x : t, @eq bool (eqb x x) true *)
  now intros; unfold eqb; rewrite compare_same_is_eq.
Qed.

(** Decide the equality of two strings. *)
Definition eq_dec (x y : t) : {x = y} + {x <> y}.
(* Goal: sumbool (@eq t x y) (not (@eq t x y)) *)
  case_eq (eqb x y); intro Heqb; [left | right].
  - now apply eqb_implies_eq.
  - intro Heq; rewrite Heq in Heqb.
(* Goal: False *)
    rewrite eqb_same_is_eq in Heqb; congruence.
Defined.
