From aee4c67e43c082c60e759a95d9311be1b49e06ef Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 1 Dec 2020 19:44:47 -0800
Subject: [PATCH] Add day 1 part 1 formalized in Coq.

---
 day1.v | 156 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 156 insertions(+)
 create mode 100644 day1.v

diff --git a/day1.v b/day1.v
new file mode 100644
index 0000000..b027722
--- /dev/null
+++ b/day1.v
@@ -0,0 +1,156 @@
+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.
+