Я рад, что вы переформулировали свой вопрос @laibanaz. Ваша лемма теперь является просто более сильной версией предыдущей леммы, которую вы предложили в своей последней записи .
Например, зная, что все значения равны / меньше максимального значения в списке и, следовательно, любое значение n-го хвоста некоторого списка также:
Fixpoint taill {A} (x : nat) (ls : list A) : list A :=
match x with
|S n => match ls with
|k :: u => taill n u
|[] => []
end
|0 => ls
end.
Theorem maxValue_tail : forall ls y (H : [] <> ls) n, In n (taill y ls) -> n <= maxvalue H.
Вы должны быть в состоянии получить:
(* your lemma probably will need a way of checking the index boundaries, so I put this additional checking*)
Theorem sorting_leb_order : forall (l : list nat) k k',
descending l -> k' < length l -> k < length l -> k <= k ->
index_value k' l <= index_value k l.
Просто полагаясь на тот факт, что любой (нисходящий) отсортированный список, заголовок является максимальным значением и получение индекса некоторого списка, просто заголовок n-го списка.
(* the j second index is really necessary? *)
Fixpoint index_value (i: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h t =>
match (Nat.eqb i 0) with
| true => h
| false => index_value (i - 1) t
end
end.
Definition hd A (ls : list A) : [] <> ls -> A :=
match ls return [] <> ls -> A with
|x :: xs => fun H => x
|[] => fun H => match (H eq_refl) with end
end.
Theorem maxl_prop : forall (l : list nat) (H : [] <> l),
descending l -> maxvalue H = hd H.
(* the index of some value is the head of nth tail *)
Theorem index_taill : forall (ls : list nat) k (H : [] <> (taill k ls)),
index_value k ls = hd H.
(* We'll need a way of getting a In preposition of some index value *)
Theorem index_InBound : forall k k' l, k' < length l -> k <= k' ->
In (index_value k' l) (taill k l).
Theorem inToIndex : forall (ls : list nat) k, k < length ls -> In (index_value k ls) ls
Теперь нам нужно доказать, что sorting_leb_order переписывает лемму с помощью приведенных выше теорем (другие теоремы доступны в вашем последнем посте ):
Theorem sorting_leb_order : forall (l : list nat) k k',
descending l -> k' < length l -> k < length l -> k <= k' ->
index_value k' l <= index_value k l.
intros.
destruct (destruct_list (taill k l)).
do 2! destruct s.
have : ~ [] = taill k l. rewrite e; done.
move => H'.
(*rewrite the definitions*)
pose (inToIndex H0).
rewrite (index_taill H'); rewrite <- maxl_prop.
by apply : maxValue; apply : index_InBound.
clear i e x0 H0 H1.
move : H.
(* cut a sorted listed produces a cutted list sorted *)
unfold descending.
elim/@taill_scheme : (taill k l).
intros; assumption.
intros; assumption.
intros; apply : H; simpl in H0.
destruct u.
exact I.
(*bound checking *)
by case : H0.
have : False.
elim/@taill_scheme : (taill k l) H1 e.
intros; subst.
inversion H1.
intros; inversion H1.
intros; apply : H1.
auto with arith.
trivial.
move => //=.
Qed.
Я предложил определение предлога сортировки, но вы можете без проблем доказать соответствие вашего предлога. Лемма не обязательно сложная, но может расти очень быстро, это зависит от того, какие определения вы используете. В этом случае, если вы предпочитаете работать с несвязанной версией индекса (лучше работать с Fin ), лемма становится немного более сложной, во-первых, из-за крайних случаев, а во-вторых, потому что выполнение индукции с использованием индексов требует более уточненные схемы. К сожалению ... лемма становится немного больше, поэтому я не смог опубликовать полное доказательство здесь, но вы можете получить здесь ).