The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

Hello 

I have defined a sort function on string list. Now I want to prove a lemma [sort_str_list_same] that if the lists

are equivalent, then sorted lists are equal. I tried induction, but get stuck in the loop.

Please if you help me solving the lemma. 

Thanks, 

Wilayat

CODE:

Require Import Ascii.

Require Import String.

Notation "x :: l" := (cons x l) (at level 60, right associativity).

Notation "[ ]" := nil.

Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Fixpoint ble_nat (n m : nat) : bool :=

  match n with

  | O => true

  | S n' =>

      match m with

      | O => false

      | S m' => ble_nat n' m'

      end

  end.

Definition ascii_eqb (a a': ascii) : bool :=

if ascii_dec a a' then true else false. 

(** true if s1 <= s2; s1 is before/same as s2 in alphabetical order *)

Fixpoint str_le_gt_dec (s1 s2 : String.string) 

 : bool :=

 match s1, s2 with 

 | EmptyString, EmptyString => true

 | String a b, String a' b' => 

        if ascii_eqb a a' then str_le_gt_dec b b'

        else if ble_nat (nat_of_ascii a) (nat_of_ascii a')

         then true else false

 | String a b, _ => false

 | _, String a' b' => true

 end.

Fixpoint aux (s: String.string) (ls: list String.string) 

 : list String.string :=

 match ls with 

 | nil => s :: nil

 | a :: l' => if str_le_gt_dec s a 

              then s :: 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. 

Notation "s1 +s+ s2" := (String.append s1 s2) (at level 60, right associativity) : string_scope.

Lemma sort_str_list_same: forall z1 z2 zm, 

 sort (z1 :: z2 :: zm) =

 sort (z2 :: z1 :: zm).

Proof with o.

 Admitted.