string - Coq 字符串排序引理

Question

我有一个定义如下的字符串排序函数，并想在下面证明一个引理 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. 

Answer 1

你的引理相当于forall z1 z2 zm, aux z1 (aux z2 zm) = aux z2 (aux z1 zm). 对于具有顺序关系的任意类型，您可以通过以下方法证明类似的定理。要在您的案例中使用它，您只需证明给定的假设。请注意，Coq 标准库定义了一些排序函数并证明了有关它们的引理，因此您可以解决您的问题而无需证明太多东西。

Require Import Coq.Lists.List.

Section sort.

Variable A : Type.

Variable comp : A -> A -> bool.

Hypothesis comp_trans :
  forall a b c, comp a b = true ->
                comp b c = true ->
                comp a c = true.

Hypothesis comp_antisym :
  forall a b, comp a b = true ->
              comp b a = true ->
              a = b.

Hypothesis comp_total :
  forall a b, comp a b = true \/ comp b a = true.

Fixpoint insert (a : A) (l : list A) : list A :=
  match l with
    | nil => a :: nil
    | a' :: l' => if comp a a' then a :: a' :: l'
                  else a' :: insert a l'
  end.

Lemma l1 : forall a1 a2 l, insert a1 (insert a2 l) = insert a2 (insert a1 l).
Proof.
  intros a1 a2 l.
  induction l as [|a l IH]; simpl.
  - destruct (comp a1 a2) eqn:E1.
    + destruct (comp a2 a1) eqn:E2; trivial.
      rewrite (comp_antisym _ _ E1 E2). trivial.
    + destruct (comp a2 a1) eqn:E2; trivial.
      destruct (comp_total a1 a2); congruence.
  - destruct (comp a2 a) eqn:E1; simpl;
    destruct (comp a1 a) eqn:E2; simpl;
    destruct (comp a1 a2) eqn:E3; simpl;
    destruct (comp a2 a1) eqn:E4; simpl;
    try rewrite E1; trivial;
    try solve [rewrite (comp_antisym _ _ E3 E4) in *; congruence];
    try solve [destruct (comp_total a1 a2); congruence].
    + assert (H := comp_trans _ _ _ E3 E1). congruence.
    + assert (H := comp_trans _ _ _ E4 E2). congruence.
Qed.

Section sort.