Require Import List Arith Recdef. Definition m (p:list nat * list nat) := let (l1,l2) := p in length l1 + length l2. Function merge (p:list nat*list nat) {measure m} : list nat := match p with (a::l1, b::l2) => if le_lt_dec a b then a::merge (l1, b::l2) else b::merge(a::l1, l2) | (nil, l) => l | (l, nil) => l end. intros p l l0 _ a l1 _ b l2 _ ab _; clear l l0 p. simpl; auto. intros p l l0 _ a l1 _ b l2 _ _ _; simpl. rewrite plus_comm. rewrite (plus_comm (length l1)). auto. Qed. Check merge_equation. Check merge_ind. Inductive sorted : list nat -> Prop := s1 : sorted nil | s2 : forall n, sorted (n::nil) | s3 : forall n m l, n <= m -> sorted (m::l) -> sorted (n::m::l). Lemma merge_sorted : forall p, sorted (fst p) -> sorted (snd p) -> sorted (merge p). (* A good example of "induction loading": you need to prove by induction a statement that is stronger, in a non-trivial manner, than the statement you really want to achieve. *) intros p; assert ((sorted (fst p) -> sorted (snd p) -> sorted (merge p)) /\ forall a, sorted (a::(fst p)) -> sorted (a::(snd p)) -> sorted (a::merge p)). functional induction merge p; simpl in IHl |- * || simpl; try destruct IHl as [IH1 IH2]. (* first case. *) split. intros al1 bl2; apply IH2; trivial; apply s3; trivial. intros c cal1 cbl2; inversion cal1; inversion cbl2; apply s3; trivial; apply IH2; trivial;apply s3; trivial. (* second case. *) split. intros al1 bl2; apply IH2; trivial; apply s3; trivial; apply lt_le_weak; trivial. intros c cal1 cbl2; inversion cal1; inversion cbl2; apply s3; trivial; apply IH2; trivial;apply s3; trivial; apply lt_le_weak; trivial. (* third case. *) intuition. (* fourth case. *) intuition. (* The last tactic "unloads the induction". *) intuition. Qed.