关于连接列表排序的引理
Lemma about Sortedness of concatenated lists
我对列表的排序有以下归纳定义:
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'
:
Lemma lem_lstle_lelst {A} {dto: DecTotalOrder A} : forall h l l',
LstLe h l -> LeLst h l' -> Sorted l -> Sorted l' -> Sorted (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.
我对列表的排序有以下归纳定义:
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'
:
Lemma lem_lstle_lelst {A} {dto: DecTotalOrder A} : forall h l l', LstLe h l -> LeLst h l' -> Sorted l -> Sorted l' -> Sorted (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.