The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 19.05.2013 21:50, schrieb Wilayat Khan:
> Hello Jonas

Hello Wilayat,

FYI here is the end of the file with the lemmas I mentioned and a proof 
of your property:


(*============*)

Require Import Omega.


Lemma str_lt_antisym s1 s2 : str_lt s1 s2 -> ~ str_lt s2 s1.
induction 1 ; intros B ; inversion B ; auto.
  omega.
  subst. omega.
  subst. omega.
Qed.

Lemma str_lt_antiref s1 s2 : str_lt s1 s2 -> s1 <> s2.

intros H ; induction H ; auto.
  discriminate.

  injection. intros _ e.
  subst. omega.

  injection. auto.
Qed.

Lemma str_lt_trans s1 s2 : str_lt s1 s2 -> forall s3, str_lt s2 s3 -> 
str_lt s1 s3.

induction 1 ; inversion 1 ; auto.
  constructor.

  constructor.

  subst. constructor 2. omega.

  subst. constructor 2. omega.

  subst. constructor 2. omega.

  subst. constructor 3 ; auto.
Qed.

Fixpoint aux (s: String.string) (ls: list String.string)
 : list String.string :=
 match ls with
 | nil => s :: nil
 | a :: l' => if str_lt_ge_dec s a
              then s :: (aux a l')
              else a :: (aux s l')
 end.

Fixpoint sort (ls: list String.string) : list String.string :=
 match ls with
 | nil => nil
 | a :: tl => aux a (sort tl)
 end.

Ltac dec_str_lt s1 s2 :=
  let H1 := fresh in let H2 := fresh in
    destruct str_lt_ge_dec with s1 s2 as [H1|[H1|H1]],
             str_lt_ge_dec with s2 s1 as [H2|[H2|H2]];
    try (exfalso ; now apply str_lt_antisym with s1 s2);
    try (exfalso ; now apply str_lt_antiref with s1 s2);
    try (exfalso ; now apply str_lt_antiref with s2 s1);
    clear H2.


Lemma sort_same : forall z s1 s2,
  aux s1 (aux s2 z) = aux s2 (aux s1 z).

induction z ; intros.
  simpl.
  dec_str_lt s1 s2 ; subst ; auto.

  simpl.
  dec_str_lt s1 a ; dec_str_lt s2 a ; simpl.
    dec_str_lt s1 s2 ; subst ; auto.

    dec_str_lt s1 a ; subst ; auto.
    dec_str_lt s1 a ; subst ; auto.

    rewrite IHz with s2 a, IHz with s1 a.
    dec_str_lt s1 a ; subst ; auto.
    dec_str_lt s1 s2 ; subst ; auto.
    exfalso ; apply str_lt_antisym with s2 s1 ; auto.
    apply str_lt_trans with a ; auto.

    dec_str_lt s2 a ; subst ; auto.
    dec_str_lt s2 a ; subst ; auto.

    dec_str_lt s1 a ; subst ; auto.
    dec_str_lt a a ; subst ; auto.

    dec_str_lt s1 a ; subst ; auto.
    dec_str_lt s2 a ; subst ; auto.
    now rewrite IHz.

    rewrite IHz with s2 a, IHz with s1 a.
    dec_str_lt s2 a ; subst ; auto.
    dec_str_lt s1 s2 ; subst ; auto.
    exfalso ; apply str_lt_antisym with s2 s1 ; auto.
    apply str_lt_trans with a ; auto.

    dec_str_lt s1 a ; subst ; auto.
    dec_str_lt a a ; subst ; auto.
    now rewrite IHz.

    dec_str_lt s1 a ; subst ; auto.
    dec_str_lt s2 a ; subst ; auto.
    now rewrite IHz.
Qed.

(*============*)

Note the usage of an Ltac to do most of the heavy lifting for us. The 
last lemma is not tough to prove - it's just very unhandy. The intuition 
behind the tactic is: if we already know the result, then we can exclude 
some cases of str_lt_ge_dec. There are two cases in the proof where my 
Ltac code is not sophisticated enough to find the contradtion by itself 
and I need to provide it by hand.
I'm not sure if there is a better proof, i.e., one which doesn't have to 
try all cases like this one.

Anyway, I hope this was as helpful for you as it was fun for me - I 
wanted to prove this theorem for quite a while, but I was always too 
lazy to put down the definitions. Now I had a good reason to :)

Have a lot of fun,

Jonas