proposition: Lemma merge_rect: forall P: list A -> list A -> list A -> Type, (forall l:list A, P nil l l) -> (forall l: list A, P l nil l) -> (forall a1 l1 a2 l2, a1 <= a2 -> P l1 (a2::l2) (merge (fun x y => bool_decide (x <= y)) l1 (a2::l2)) -> P (a1::l1) (a2::l2) (a1::(merge (fun x y => bool_decide (x <= y))l1 (a2::l2)))) -> (forall a1 l1 a2 l2, ~ le a1 a2 -> P (a1::l1) l2 (merge (fun x y => bool_decide (x <= y))(a1::l1) l2) -> P (a1::l1) (a2::l2) (a2::(merge (fun x y => bool_decide (x <= y)) (a1::l1) l2))) -> forall l1 l2, P l1 l2 (merge (fun x y => bool_decide (x <= y)) l1 l2).
proof: Proof. Proof with auto. induction l1. - intros; simpl; destruct l2; apply X. - induction l2. + apply X0. + simpl; unfold bool_decide. destruct (decide_rel le a a0). * apply X1; [assumption|apply IHl1]. * apply X2; assumption. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)