Require Import Coq.Sorting.Mergesort. Require Import Coq.Lists.List. Require Import Coq.Program.Wf. Require Import Coq.Arith.PeanoNat. Require Import Omega. Require Import ExtrHaskellBasic. Definition has_pair (t : nat) (is : list nat) : Prop := exists n1 n2 : nat, n1 <> n2 /\ In n1 is /\ In n2 is /\ n1 + n2 = t. Fixpoint find_matching (is : list nat) (total : nat) (x : nat) : option nat := match is with | nil => None | cons y ys => if Nat.eqb (x + y) total then Some y else find_matching ys total x end. Fixpoint find_sum (is : list nat) (total : nat) : option (nat * nat) := match is with | nil => None | cons x xs => match find_matching xs total x with | None => find_sum xs total (* Was buggy! *) | Some y => Some (x, y) end end. Lemma find_matching_correct : forall is k x y, find_matching is k x = Some y -> x + y = k. Proof. intros is. induction is; intros k x y Hev. - simpl in Hev. inversion Hev. - simpl in Hev. destruct (Nat.eqb (x+a) k) eqn:Heq. + injection Hev as H; subst. apply EqNat.beq_nat_eq. auto. + apply IHis. assumption. Qed. Lemma find_matching_skip : forall k x y i is, find_matching is k x = Some y -> find_matching (cons i is) k x = Some y. Proof. intros k x y i is Hsmall. simpl. destruct (Nat.eqb (x+i) k) eqn:Heq. - apply find_matching_correct in Hsmall. symmetry in Heq. apply EqNat.beq_nat_eq in Heq. assert (i = y). { omega. } rewrite H. reflexivity. - assumption. Qed. Lemma find_matching_works : forall is k x y, In y is /\ x + y = k -> find_matching is k x = Some y. Proof. intros is. induction is; intros k x y [Hin Heq]. - inversion Hin. - inversion Hin. + subst a. simpl. Search Nat.eqb. destruct (Nat.eqb_spec (x+y) k). * reflexivity. * exfalso. apply n. assumption. + apply find_matching_skip. apply IHis. split; assumption. Qed. Theorem find_sum_works : forall k is, has_pair k is -> exists x y, (find_sum is k = Some (x, y) /\ x + y = k). Proof. intros k is. generalize dependent k. induction is; intros k [x' [y' [Hneq [Hinx [Hiny Hsum]]]]]. - (* is is empty. But x is in is! *) inversion Hinx. - (* is is not empty. *) inversion Hinx. + (* x is the first element. *) subst a. inversion Hiny. * (* y is also the first element; but this is impossible! *) exfalso. apply Hneq. apply H. * (* y is somewhere in the rest of the list. We've proven that we will find it! *) exists x'. simpl. erewrite find_matching_works. { exists y'. split. reflexivity. assumption. } { split; assumption. } + (* x is not the first element. *) inversion Hiny. * (* y is the first element, so x is somewhere in the rest of the list. Again, we've proven that we can find it. *) subst a. exists y'. simpl. erewrite find_matching_works. { exists x'. split. reflexivity. rewrite plus_comm. assumption. } { split. assumption. rewrite plus_comm. assumption. } * (* y is not the first element, either. Of course, there could be another matching pair starting with a. Otherwise, the inductive hypothesis applies. *) simpl. destruct (find_matching is k a) eqn:Hf. { exists a. exists n. split. reflexivity. apply find_matching_correct with is. assumption. } { apply IHis. unfold has_pair. exists x'. exists y'. repeat split; assumption. } Qed. Extraction Language Haskell. Extraction "test.hs" find_sum. Check find_sum_works. (* WIP stuff for 2-pointer solution. *) Inductive non_empty {X : Type} : list X -> Prop := | non_empty_cons : forall x xs, non_empty (cons x xs). Lemma nil_empty {X: Type} : ~ @non_empty X nil. Proof. intros H. inversion H. Qed. Program Fixpoint last (is : list nat) (H : non_empty is) {measure (length is)} : nat := match is with | nil => _ | cons x nil => x | cons x (cons y xs) => last (cons y xs) _ end. Obligation 1. exfalso. apply (nil_empty H). Qed. Obligation 2. apply non_empty_cons. Qed. Program Fixpoint drop_last (is : list nat) (H : non_empty is) {measure (length is)} : list nat := match is with | nil => _ | cons x nil => nil | cons x (cons y xs) => cons x (drop_last (cons y xs) _) end. Obligation 1. exfalso. apply (nil_empty H). Qed. Obligation 2. apply non_empty_cons. Qed. Program Fixpoint find_pair (is : list nat) (t : nat) : option (nat * nat) := match is with | nil => None | cons x nil => None | cons x (cons y xs) => Some (x, last (cons y xs) _) end. Obligation 1. apply non_empty_cons. Qed.