proposition: Lemma Forall_append : forall A (P : A → Prop) xs ys, List.Forall P xs /\ List.Forall P ys <-> List.Forall P (xs ++ ys).
proof: Proof. Admitted. Lemma StronglySorted_inv_app : forall a R (l1 l2 : list a), StronglySorted R (l1 ++ l2) → StronglySorted R l1 /\ StronglySorted R l2. Proof. Admitted. Lemma StronglySorted_cat {A : Type} {xs ys : list A} {R : A → A → Prop} `{Transitive _ R} : StronglySorted R xs → StronglySorted R ys → (match olast xs, ys with | Just x, y :: _ => R x y | _, _ => True end) → StronglySorted R (xs ++ ys)%list. Proof. Admitted. Lemma StronglySorted_cons_cons : forall a (R : a → a → Prop) x xs y ys, StronglySorted R (x :: xs ++ y :: ys) → R x y. Proof. Admitted. Lemma Forall_ordered : forall a (R : a → a → Prop) `{Transitive _ R} x y xs, R x y → List.Forall (R y) xs → List.Forall (R x) xs. Proof. Admitted. Lemma StronglySorted_impl : forall (A : Type) (P Q : A → A → Prop), (forall a b : A, P a b → Q a b) -> forall l : list A, StronglySorted P l → StronglySorted Q l. Proof. intros. induction l; simpl. - constructor. - constructor. + apply IHl. inversion H0; assumption. + inversion H0; subst. apply Forall_impl with (P:=P a). * apply H. * assumption. Qed.
imports: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe