Add homework 1's problem 1 formalization

This commit is contained in:
Danila Fedorin 2022-01-06 21:42:42 -08:00
commit 1ec72b59b9
1 changed files with 98 additions and 0 deletions

98
hw1.v Normal file
View File

@ -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.