From 1ec72b59b91fbc6e136aa0e68bb60fae46989c87 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 6 Jan 2022 21:42:42 -0800
Subject: [PATCH] Add homework 1's problem 1 formalization

---
 hw1.v | 98 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)
 create mode 100644 hw1.v

diff --git a/hw1.v b/hw1.v
new file mode 100644
index 0000000..67120c5
--- /dev/null
+++ b/hw1.v
@@ -0,0 +1,98 @@
+Require Import Coq.Arith.PeanoNat.
+Require Import Coq.Logic.EqdepFacts.
+
+Inductive OrderedNums : nat -> list nat -> Prop :=
+  | FoundAll : forall (l : list nat), OrderedNums 0 (cons 0 l)
+  | FoundNext : forall (n : nat) (l : list nat),
+      OrderedNums n l -> OrderedNums (S n) (cons (S n) l)
+  | Skip : forall (n x : nat) (l : list nat),
+      OrderedNums n l -> OrderedNums n (cons x l).
+
+Fact orderedThree : OrderedNums 3 (cons 3 (cons 2 (cons 2 (cons 1 (cons 0 nil))))).
+Proof. 
+  apply FoundNext.
+  apply FoundNext.
+  apply Skip.
+  apply FoundNext.
+  apply FoundAll.
+Qed.
+
+Fixpoint check_numbers (k : nat) (v : list nat) : bool :=
+  match v with
+  | nil => false
+  | cons n v =>
+      if Nat.eq_dec k n
+      then
+        match k with
+        | 0 => true
+        | (S k') => check_numbers k' v
+        end
+      else check_numbers k v
+  end.
+
+Theorem check_numbers_one : forall (k : nat) (l : list nat),
+  check_numbers k l = true -> OrderedNums k l.
+Proof.
+  intros k l Heq.
+  generalize dependent k.
+  (* Go by induction on l. *)
+  induction l; intros k Heq; simpl in Heq.
+  - (* List is empty, algorithm couldn't have returned true. *)
+    discriminate Heq.
+  - (* List is not empty; what we do next depends on whether k is equal or not. *)
+    destruct (Nat.eq_dec k a) eqn:Heqk.
+    + (* k is equal, so we either recurse (if it' not zero), or we're done (if it's zero). *)
+      destruct k; subst.
+      * (* k is zero, so we've found all the numbers *)
+        apply FoundAll.
+      * (* k is not zero, we go on looking, which is correct by the induction hypothesis. *)
+        apply FoundNext. auto.
+    + (* k didn't match. We go on looking, and it's correct by the induction hypothesis. *)
+      apply Skip. auto.
+Qed.
+
+Require Import Coq.Program.Equality.
+
+Lemma check_numbers_suc : forall (k : nat) (v : list nat),
+  OrderedNums (S k) v -> OrderedNums k v.
+Proof.
+  intros k v Hsk.
+  dependent induction Hsk.
+  - apply Skip. auto.
+  - apply Skip. apply IHHsk. auto.
+Qed.
+
+Lemma check_numbers_suc_p : forall (k : nat) (v : list nat),
+  ~ OrderedNums k v -> ~ OrderedNums (S k) v.
+Proof.
+  intros k v Hk HSk.
+  apply Hk. apply check_numbers_suc. auto.
+Qed.
+
+Theorem check_numbers_two : forall (k : nat) (l : list nat),
+  check_numbers k l = false -> ~ OrderedNums k l.
+Proof.
+  intros k l.
+  generalize dependent k.
+  (* Go by induction on the list. *)
+  induction l; intros k Heq Hk.
+  - (* The list is empty, so we can't have ordered numbers. *)
+    inversion Hk.
+  - (* The evaluation depends on whether or not k is equal to the given number. *)
+    simpl in Heq. destruct (Nat.eq_dec k a) eqn:Heqk.
+    + (* k is equal to the number; what we do next depends on k. *)
+      destruct k; subst.
+      * (* k is zero, so we return true. Contradictory assumption. *)
+        inversion Heq.
+      * (* k is not zero, we make a recurisve call. *)
+        (* k = S k'. So the recursive call returns false, and we know that
+           there aren't k' numbers in a row. *)
+        inversion Hk; subst;
+        (* We know that if there are no k' numbers, there also can't be k numbers. *)
+        specialize (check_numbers_suc k l) as Hsuc;
+        (* We know there are no k' numbers by induction. *)
+        specialize (IHl k Heq);
+        auto.
+    + (* k is not equal to the number. We just go by induction. *)
+      specialize (IHl k Heq). inversion Hk; subst; auto.
+Qed.