The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

I did the following.

I do not know if it is or is not worth to be added in the standard
library or the contribs. I have not documented it, although it is
rather straightforward.

I did use only very low-level tactics. The proofs can be shortened by
using more complex tactics.

Implementing directly a module for Strings would also have been
shorter. I did this to check my statement that a "Serializable" module
would be a good idea. And it seems rather good (at least for strings).

==================================================================
Require Import Utf8.
Require Import Ascii.
Require Import String.
Require Import FMapAVL.

Set Implicit Arguments.

Inductive data : Set := Node : data → data → data | Leaf.

Definition is_leaf (d : data) : Prop :=
  match d with Leaf => True | _ => False end.
Definition is_node (d : data) : Prop :=
  match d with Leaf => False | _ => True end.

Definition is_leaf_unicity d : ∀ (il1 il2 : is_leaf d), il1 = il2 :=
  match d with
  | Leaf => λ (il1 il2 : is_leaf Leaf),
            match il1, il2 with I, I => eq_refl I end
  | Node x y => λ (il1 : is_leaf (Node x y)), match il1 with end
  end.

Definition is_node_unicity d : ∀ (il1 il2 : is_node d), il1 = il2 :=
  match d with
  | Node x y => λ (il1 il2 : is_node (Node x y)),
                match il1, il2 with I, I => eq_refl I end
  | Leaf => λ (il1 : is_node Leaf), match il1 with end
  end.

Definition dleft d : is_node d → data :=
  match d with
  | Leaf => λ H, match H with end
  | Node l _ => λ _, l
  end.
Definition dright d : is_node d → data :=
  match d with
  | Leaf => λ H, match H with end
  | Node _ r => λ _, r
  end.

Inductive data_lt (a b : data) : Prop :=
  | LtLeaf : is_leaf a → is_node b → data_lt a b
  | LtLeft : ∀ Na Nb, data_lt (dleft a Na) (dleft b Nb) → data_lt a b
  | LtRight : ∀ Na Nb, dleft a Na = dleft b Nb →
              data_lt (dright a Na) (dright b Nb) → data_lt a b.

Definition right_node a b (H : data_lt a b) : is_node b :=
  match H with
  | LtLeaf _ H => H
  | LtLeft _ H _ => H
  | LtRight _ H _ _ => H
  end.

Fixpoint data_lt_trans x y z (H : data_lt x y) : data_lt y z → data_lt
x z. Proof.
  destruct H.
  (* case LtLeaf *)
    intros K; constructor 1; auto; destruct K; auto.
  (* case LtLeft *)
    intros K; apply (LtLeft x z Na (right_node K)); destruct K; simpl
in *. exfalso; destruct y; simpl in *; auto.
      eapply data_lt_trans; eauto; case (is_node_unicity y Na0 Nb);
auto. case e; case (is_node_unicity y Nb Na0); auto.
  (* case LtRight *)
  intros K; destruct K.
      exfalso; destruct y; simpl in *; auto.
    apply (LtLeft x z Na Nb0); rewrite H; case (is_node_unicity y Na0
Nb); auto. apply (LtRight x z Na Nb0); case H1; case (is_node_unicity y
Nb Na0); auto. eapply data_lt_trans; eauto; case (is_node_unicity y Na0
Nb); auto. Qed.

Lemma data_lt_not_eq x y : data_lt x y → x ≠ y.
Proof.
  intros H K; revert H; case K; clear.
  revert x; fix 2; intros x [lx nx | nx1 nx2 Hlt | nx1 nx2 Heq Hlt];
  destruct x; simpl in *; eauto.
Qed.

Fixpoint data_compare x y : OrderedType.Compare data_lt (@eq data) x y.
refine (
  match x with
  | Leaf => match y with
            | Leaf => OrderedType.EQ _
            | Node c d => OrderedType.LT _
            end
  | Node a b => match y with
                | Leaf => OrderedType.GT _
                | Node c d => match data_compare a c with
                              | OrderedType.LT H => OrderedType.LT _
                              | OrderedType.EQ K =>
                                match data_compare b d with
                                | OrderedType.LT H => OrderedType.LT _
                                | OrderedType.EQ H => OrderedType.EQ _
                                | OrderedType.GT H => OrderedType.GT _
                                end
                              | OrderedType.GT H => OrderedType.GT _
                              end
                end
  end
).
Proof. exact (LtLeft (Node a b) (Node c d) I I H).
Proof. exact (LtRight (Node a b) (Node c d) I I K H).
Proof. exact (match K with eq_refl => match H with eq_refl=>eq_refl _
end end). Proof. exact (LtRight (Node c d) (Node a b) I I (eq_sym K) H).
Proof. exact (LtLeft (Node c d) (Node a b) I I H).
Proof. exact (LtLeaf Leaf (Node a b) I I).
Proof. exact (LtLeaf Leaf (Node c d) I I).
Proof. exact (eq_refl Leaf).
Defined.

Module DataOrder.
  Definition t := data.
  Definition eq := @eq t.
  Definition lt := data_lt.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.
  Definition lt_trans := data_lt_trans.
  Definition lt_not_eq := data_lt_not_eq.
  Definition compare := data_compare.
  Definition eq_dec : ∀ x y : t, {eq x y} + {¬eq x y} :=
    λ x y, match compare x y with
           | OrderedType.GT H => right (λ K, lt_not_eq H (eq_sym K))
           | OrderedType.EQ H => left H
           | OrderedType.LT H => right (lt_not_eq H)
           end.
End DataOrder.

Module Type Serializable.
  Parameter t : Type.
  Parameter serialize : t → data.
  Parameter unserialize : data → t.
  Hypothesis SerializeSection : ∀ t, unserialize (serialize t) = t.
End Serializable.

Module SerializeOrder (S : Serializable).
  Definition t := S.t.
  Definition eq := @eq t.
  Definition lt := λ x y, DataOrder.lt (S.serialize x) (S.serialize y).
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.
  Definition lt_trans x y z (H : lt x y) (K : lt y z) :=
DataOrder.lt_trans H K. Lemma lt_not_eq x y (H : lt x y) (Heq : x =
y) : False. Proof. unfold lt in *. apply (DataOrder.lt_not_eq H). case
Heq. split. Qed. Definition compare x y : OrderedType.Compare lt eq x y.
  refine (match DataOrder.compare (S.serialize x) (S.serialize y) with
          | OrderedType.GT H => OrderedType.GT _
          | OrderedType.EQ H => OrderedType.EQ _
          | OrderedType.LT H => OrderedType.LT _
          end);
  auto.
  case (S.SerializeSection x); rewrite H; apply S.SerializeSection.
  Defined.
  Definition eq_dec : ∀ x y : t, {eq x y} + {¬eq x y} :=
    λ x y, match compare x y with
           | OrderedType.GT H => right (λ K, lt_not_eq H (eq_sym K))
           | OrderedType.EQ H => left H
           | OrderedType.LT H => right (lt_not_eq H)
           end.
End SerializeOrder.

(********** Example with ASCII ************)
Module SBool.
  Definition t := bool.
  Definition serialize (b : bool) := if b then Node Leaf Leaf else Leaf.
  Definition unserialize (d : data) := if d then true else false.
  Lemma SerializeSection : ∀ b, unserialize (serialize b) = b.
    intros []; split.
  Qed.
End SBool.

Module SAscii.
  Definition t := ascii.
  Definition serialize a :=
    match a with
    | Ascii a b c d e f g h => Node (Node (Node (SBool.serialize a)
                                                (SBool.serialize b))
                                          (Node (SBool.serialize c)
                                                (SBool.serialize d)))
                                    (Node (Node (SBool.serialize e)
                                                (SBool.serialize f))
                                          (Node (SBool.serialize g)
                                                (SBool.serialize h)))
    end.
  Definition unserialize a :=
    match a with
    | Node (Node (Node a b) (Node c d)) (Node (Node e f) (Node g h)) =>
      Ascii (SBool.unserialize a)
            (SBool.unserialize b)
            (SBool.unserialize c)
            (SBool.unserialize d)
            (SBool.unserialize e)
            (SBool.unserialize f)
            (SBool.unserialize g)
            (SBool.unserialize h)
    | _ => Ascii false false false false false false false false
    end.
  Lemma SerializeSection : ∀ b, unserialize (serialize b) = b.
    intros [a b c d e f g h]; simpl; repeat rewrite
SBool.SerializeSection. split.
  Qed.
End SAscii.

Module SString.
  Definition t := string.
  Fixpoint serialize s :=
    match s with
    | EmptyString => Leaf
    | String a s => Node (SAscii.serialize a) (serialize s)
    end.
  Fixpoint unserialize d :=
    match d with
    | Leaf => EmptyString
    | Node l r => String (SAscii.unserialize l) (unserialize r)
    end.
  Lemma SerializeSection : ∀ b, unserialize (serialize b) = b.
    intros b; induction b; simpl; auto.
    rewrite SAscii.SerializeSection.
    rewrite IHb.
    split.
  Qed.
End SString.

Module StringOrder := SerializeOrder SString.
Module StringMap := Make StringOrder.