1
아래에 정의 된 문자열 정렬 함수가 있으며 아래 보조제 sort_str_list_same을 증명하려고합니다. 나는 전문가가 아니기 때문에 유도를 사용하여 그것을 풀려고했지만 그것을 풀 수는 없었다. 제발 도와주세요. 감사합니다.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.