1
我有一個字符串排序函數定義如下，並想在下面證明一個引理 sort_str_list_same。我不是Coq專家，我試圖用歸納解決它，但無法解決它。請幫我解決它。謝謝，Coq字符串排序引理
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.