(* begin hide *) Require Import List. Require Import Arith. Require Import Recdef. Require Import Lia. (* end hide *) (** * Introdução *) (** comentários da introdução *) (** ** Subseção *) Definition len (p: list nat * list nat) := length (fst p) + length (snd p). Function merge (p: list nat * list nat) {measure len p} := match p with | (nil, l2) => l2 | (l1, nil) => l1 | ((hd1 :: tl1) as l1, (hd2 :: tl2) as l2) => if hd1 <=? hd2 then hd1 :: merge (tl1, l2) else hd2 :: merge (l1, tl2) end. Proof. - intros. unfold len. simpl. lia. - intros. unfold len. simpl. lia. Defined. Inductive sorted : list nat -> Prop := | sorted_nil: sorted nil | sorted_one: forall x, sorted (x :: nil) | sorted_all: forall x y l, x <= y -> sorted (y :: l) -> sorted (x :: y :: l). (** O teorema a seguir mostra que a função [merge_sorted] retorna uma lista ordenada quando as listas que formam o par estão ordenadas. *) Theorem merge_sorted: forall p:(list nat * list nat), sorted (fst p) -> sorted (snd p) -> sorted (merge p). Proof. intro p. functional induction (merge p). - intros H1 H2. unfold snd in H2. assumption. - intros H1 H2. unfold fst in H1. assumption. - intros H1 H2. unfold fst in *. unfold snd in *. generalize dependent tl1. intro tl1. case tl1. + intros IH H1. rewrite merge_equation. apply sorted_all. * apply leb_complete. assumption. * assumption. + intros n l IH H1. rewrite merge_equation in *. destruct (n <=? hd2) eqn:H. * apply sorted_all. ** inversion H1; subst. assumption. ** apply IH. *** inversion H1; subst; assumption. *** assumption. * apply sorted_all. ** apply leb_complete; assumption. ** apply IH. *** inversion H1; subst; assumption. *** assumption. - intros H1 H2. unfold fst in *. unfold snd in *. generalize dependent tl2. intro tl2. case tl2. + intros IH H2. rewrite merge_equation. apply sorted_all. * apply leb_complete_conv in e0. apply Nat.lt_le_incl in e0. assumption. * assumption. + intros n l IH H2. rewrite merge_equation in *. destruct (hd1 <=? n) eqn:H. * apply sorted_all. ** apply leb_complete_conv in e0. apply Nat.lt_le_incl in e0. assumption. ** apply IH. *** assumption. *** inversion H2; subst; assumption. * apply sorted_all. ** inversion H2; subst; assumption. ** apply IH. *** assumption. *** inversion H2; subst; assumption. Qed. (* Theorem merge_sorted: forall l1 l2, sorted l1 -> sorted l2 -> sorted (merge(l1,l2)). Proof. intros l1 l2. remember (l1,l2) as p. functional induction (merge(p)). - inversion Heqp; subst. intros H1 H2; assumption. - inversion Heqp; subst. intros H1 H2; assumption. - Admitted. *) Function mergesort (l: list nat) {measure length l} := match l with | nil => nil | hd :: nil => l | hd :: tail => let n := length(l) / 2 in let l1 := firstn n l in let l2 := skipn n l in let sorted_l1 := mergesort(l1) in let sorted_l2 := mergesort(l2) in merge (sorted_l1, sorted_l2) end. Proof. Admitted.