Skip to content
Snippets Groups Projects
Commit 75e1dcfb authored by François Clément's avatar François Clément
Browse files

Add LocallySorted_cons2.

parent 609fdbc5
No related branches found
No related tags found
No related merge requests found
......@@ -119,15 +119,15 @@ inversion H1.
now simpl.
Qed.
(* Useful?
Lemma LocallySorted_0_1_nil :
forall P l (a0 : A),
l <> nil -> LocallySorted P l -> LocallySorted P (a0 :: l) ->
P a0 (nth 0 l a0).
Proof.
intros P; induction l;intros.
now contradict H.
inversion H1;now simpl.
intros; now apply LocallySorted_0_1.
Qed.
*)
Lemma LocallySorted_cons :
forall P (a : A) l,
......@@ -295,6 +295,18 @@ apply Sorted_extends; try assumption.
now apply Sorted_LocallySorted_iff.
Qed.
Lemma LocallySorted_cons2 :
forall (a b : A) l,
(forall x y z, ord x y -> ord y z -> ord x z) ->
LocallySorted ord (a :: b :: l) -> LocallySorted ord (a :: l).
Proof.
intros a b l Ho Hl.
inversion Hl; inversion H1.
apply LSorted_cons1.
apply LSorted_consn; try easy.
now apply Ho with b.
Qed.
Lemma LocallySorted_select :
forall P l,
(forall x y z, ord x y -> ord y z -> ord x z) ->
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment