The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Hi Wilayat,
I think it's a good idea to use more expressive functions.

For an example, consider ble_nat.
A better way to write ble_nat is (as in the standard library http://coq.inria.fr/stdlib/Coq.Arith.Compare_dec.html#le_lt_dec ) le_lt_dec:

Definition le_lt_dec n m : {n <= m} + {m < n}.

That way you don't get "true" or "false", which are quite meaningless, but you get "n <= m" or "m < n".

For another,
Definition ascii_eqb (a a': ascii) : {a = a'} + {a <> a'}.
decide equality. Defined.

The way you currently do things you lose any kind of meaning of, e.g., ascii_eqb a a' = true. How do you conclude from such a statement that a = a'?

Next, I suggest proving this on a more general level; i.e., instead of defining sorting for lists of strings, you could define sorting for any type and decidable ordering on that type.

Finally, the theorem you're trying to prove is

aux a (aux b l) = aux b (aux a l)

I believe the reason why you're stuck is that you do not have any meaning of "str_le_gt_dec".
Therefore you can not tell, e.g., that "str_le_gt_dec a x = true" and "str_le_gt_dec b x = false" implies "str_le_gt_dec a b = true".
I think your problem is along these lines, even though I'm not sure of the exact statements that you'd need.
If you make the changes as I suggest, I believe the statement will be provable.

Regards, Jonas


Am 19.05.2013 13:30, schrieb Wilayat Khan:

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.