Блог

У меня есть следующее индуктивное определение сортировки списка:

 
Class DecTotalOrder (A : Type) := {
  leb : A -> A -> bool;
  leb_total_dec : forall x y, {leb x y} {leb y x};
  leb_antisym : forall x y, leb x y -> leb y x -> x = y;
  leb_trans : forall x y z, leb x y -> leb y z -> leb x z }.

Inductive Sorted {A} {dto : DecTotalOrder A} : list A -> Prop :=
| Sorted_0 : Sorted []
| Sorted_1 : forall x, Sorted [x]
| Sorted_2 : forall x y, leb x y ->
                         forall l, Sorted (y :: l) ->
                                   Sorted (x :: y :: l).
  

И следующие два определения, чтобы объявить, что элемент x меньше или равен каждому элементу списка (LeLst) и больше или равен каждому элементу списка (LstLe) :

 Definition LeLst {A} {dto : DecTotalOrder A} (x : A) (l : list A) :=
  List.Forall (leb x) l.

Definition LstLe {A} {dto : DecTotalOrder A} (x : A) (l : list A) := 
   List.Forall (fun y => leb y x) l.

  

Я пытаюсь доказать следующую лемму о сортировке, которая в основном гласит, что если мы знаем, что h больше или равно каждому элементу в l, а h меньше или равно каждому элементу в l ‘, мы можем поместить его между двумя:

 Lemma lem_lstle_lelst {A} {dto: DecTotalOrder A} : forall h l l',
LstLe h l -> LeLst h l' -> Sorted (l    h :: l').
  

Это кажется очень интуитивным, но я каждый раз застреваю в доказательстве. Это моя текущая попытка:

 Lemma lem_lstle_lelst {A} {dto: DecTotalOrder A} : forall h l l',
LstLe h l -> LeLst h l' -> Sorted (l    h :: l').
Proof.
intros h l l' H_LstLe.
induction H_LstLe.
- intros. simpl. Search (Sorted (_ :: _)).
  unfold LeLst in H. Search (List.Forall _ _).
  induction l'.
    constructor.
    Search (List.Forall _ _). 
    constructor. 
      { hauto use: List.Forall_inv. }
      { generalize (List.Forall_inv_tail H).
        intros.
        generalize (List.Forall_inv H).
        intros. 
        generalize (IHl' H0).
        intros.
        generalize (lem_sorted_tail H2).
        intros.
  

Однако я застрял здесь, потому что гипотезы просто не кажутся достаточно сильными:

 1 subgoal
A : Type
dto : DecTotalOrder A
h, a : A
l' : list A
H : List.Forall (fun x : A => leb h x) (a :: l')
IHl' : List.Forall (fun x : A => leb h x) l' -> Sorted (h :: l')
H0 : List.Forall (fun x : A => leb h x) l'
H1 : leb h a
H2 : Sorted (h :: l')
H3 : Sorted l'
______________________________________(1/1)
Sorted (a :: l')

  

Я был бы очень рад, если бы кто-нибудь мог дать мне подсказку, может быть, что-то не так с моими определениями, и именно поэтому я не могу продолжить доказательство? Или я просто упускаю какую-то тактику, которую я мог бы использовать?

Вот список уже доказанных лемм о сортировке:

 Lemma lem_sorted_tail {A} {dto : DecTotalOrder A}{l x} :
  Sorted (x :: l) -> Sorted l.

Lemma lem_sorted_prepend {A} {dto: DecTotalOrder A} : forall x l l',
  Sorted((x :: l)    l') -> Sorted(l    l').

Lemma lem_sort_conc_mid {A} {dto: DecTotalOrder A} : forall x y l, 
  Sorted (x :: y :: l) -> Sorted (x :: l).

  

Как указано в комментарии, лемма не доказуема. Вместо этого его определение должно быть расширено путем добавления свойств о сортировке l и l' :

Лемма lem_lstle_lelst {A} {dto: итоговый порядок A} : для всех h l l', 
Сначала h l -> Отсортированное l -> Отсортированное l' -> Отсортированное (l    h :: l').

Это можно доказать с помощью следующего:

 Proof.
intros h l l' H_Lstle_h_l.
induction H_Lstle_h_l.
- intros H_Lelst_h_l' H_Sort_1 H_Sort_2.
  simpl;inversion H_Lelst_h_l';sauto.
- intros H_Lelst_h_l' H_Sort_1 H_Sort_2.
  generalize (lem_sorted_tail H_Sort_1).
  intros H_Sort_l.
  generalize (IHH_Lstle_h_l H_Lelst_h_l' H_Sort_l H_Sort_2).
  intros H_Sort_l_h_l'.
  generalize (lem_sorted_lelst x l H_Sort_1).
  intros H_Lelst_x_l.
  hauto use: lem_Sorted_prepend_inv.
Qed. 

  

представляем новые вспомогательные леммы:

 Lemma lem_Sorted_prepend_inv {A} {dto: DecTotalOrder A} : 
  forall x h l l', leb x h ->  Sorted(l    h :: l') -> LeLst x l -> Sorted(x::l   h::l').

Lemma lem_sorted_lelst {A} {dto: DecTotalOrder A} :
  forall x l, Sorted(x :: l) -> LeLst x l.