(* CS3234, Martin Henz and Aquinas Hobor *)
(* Homework on induction in Coq *)
(* Some useful tactics *)
Tactic Notation "spec" hyp(H) :=
match type of H with ?a -> _ =>
let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end.
Tactic Notation "spec" hyp(H) constr(a) :=
(generalize (H a); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) :=
(generalize (H a b); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) :=
(generalize (H a b c); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
(generalize (H a b c d); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) :=
(generalize (H a b c d e); clear H; intro H).
Ltac remembertac2 x a :=
let x := fresh x in
let H := fresh "Heq" x in
(set (x:=a) in *; assert (H: a=x) by reflexivity; clearbody x).
Tactic Notation "cases" constr(a) :=
let x := fresh in (remembertac2 x a; destruct x).
Require ClassicalFacts. (* no axioms in this line *)
Require Export Coq.Logic.ClassicalChoice.
(* Axioms dependent_unique_choice, relational_choice *)
Tactic Notation "LEM" constr(a) :=
destruct (classic a).
Axiom dep_extensionality:
forall (A: Type) (B: A -> Type) (f g : forall x: A, B x), (forall x, f x = g x) -> f = g.
Implicit Arguments dep_extensionality.
Axiom prop_ext: ClassicalFacts.prop_extensionality.
Implicit Arguments prop_ext.
(* You may want to look at the notes on induction for help understanding
this file. *)
(* Total, 70 points of proof script, + 5 points for an explanation in the
last problem, + 25 points extra credit. *)
(* These were defined in class and/or in the notes *)
Inductive Tree : Type :=
| Leaf : Tree
| Node : Tree -> Tree -> Tree.
Fixpoint size(t : Tree) : nat :=
match t with
| Leaf => 1
| Node t1 t2 => 1 + size t1 + size t2
end.
Inductive List (A : Type) : Type :=
| Nil : List A
| Cons : A -> List A -> List A.
Implicit Arguments Nil [A].
Implicit Arguments Cons [A].
Fixpoint map (A B : Type) (f : A -> B) (L : List A) : List B :=
match L with
| Nil => Nil
| Cons a L' => Cons (f a) (map A B f L')
end.
Implicit Arguments map [A B].
CoInductive CoNatStream : Type :=
CNS : nat -> CoNatStream -> CoNatStream.
Inductive InNatStream : Type :=
INS : nat -> InNatStream -> InNatStream.
(* The following material is new *)
Fixpoint deep_swap (t : Tree) : Tree :=
match t with
| Leaf => Leaf
| Node t1 t2 => Node (deep_swap t2) (deep_swap t1)
end.
Require Import Omega.
(* 10 points *)
Lemma swap_size: forall t,
size t = size(deep_swap t).
Proof.
induction t; simpl.
trivial.
omega.
Qed.
Fixpoint concat (A : Type) (L1 L2 : List A) : List A :=
match L1 with
| Nil => L2
| Cons a L1' => Cons a (concat A L1' L2)
end.
Implicit Arguments concat.
Fixpoint length (A : Type) (L : List A) : nat :=
match L with
| Nil => 0
| Cons _ L' => 1 + length A L'
end.
Implicit Arguments length.
(* 10 points *)
Lemma concat_length: forall A (L1 L2 : List A),
length (concat L1 L2) = length L1 + length L2.
Proof.
induction L1; simpl.
trivial.
intro.
rewrite IHL1.
omega.
Qed.
Definition headStream (cns : CoNatStream) : nat :=
match cns with
| CNS n cns' => n
end.
Definition tailStream (cns : CoNatStream) : CoNatStream :=
match cns with
| CNS n cns' => cns'
end.
CoFixpoint increasingStream (n : nat) : CoNatStream :=
CNS n (increasingStream (S n)).
(* 5 points *)
Lemma increasingStream_increases: forall n,
headStream (increasingStream n) <
headStream (tailStream (increasingStream n)).
Proof.
intros.
simpl.
omega.
Qed.
(* 10 points *)
Lemma no_InNatStream:
~ exists ins : InNatStream, True.
Proof.
intro.
destruct H.
induction x.
trivial.
Qed.
Inductive Option (A : Type) : Type :=
| NO : Option A
| YES : A -> Option A.
Implicit Arguments NO [A].
Implicit Arguments YES [A].
Fixpoint get_nth (A : Type) (L : List A) (n : nat) : Option A :=
match (L,n) with
| (Nil,_) => NO
| (Cons a _,0) => YES a
| (Cons _ L',S n') => get_nth A L' n'
end.
Implicit Arguments get_nth [A].
Definition double (n : nat) : nat :=
n + n.
(* Recall that if you get a hypothesis like NO = YES x, then you can
use the "inversion" or "discriminate" tactics to expose the
contradiction. "inversion" can also be useful if you have a
hypothesis like YES x = YES y, since it will give you x=y. *)
(* 15 points *)
Lemma map_double: forall n L o,
get_nth (map double L) n = YES o ->
exists o',
get_nth L n = YES o' /\ o = double o'.
Proof.
induction n; destruct L; simpl; intros.
inversion H.
inversion H.
exists n.
split; trivial.
inversion H.
apply IHn.
trivial.
Qed.
Inductive Pair (A B : Type) : Type :=
mkPair : A -> B -> Pair A B.
Implicit Arguments mkPair [A B].
Definition first (A B : Type) (p : Pair A B) :=
match p with
mkPair a b => a
end.
Implicit Arguments first [A B].
Definition second (A B : Type) (p : Pair A B) :=
match p with
mkPair a b => b
end.
Implicit Arguments second [A B].
(* As the name might imply, this one is not so easy. You will need
to strengthen the induction hypothesis to make it work out. *)
(* The @ is to help with the implicit arguments; see the notes if you like.
It won't show up in the interactive mode when you're doing the proof. *)
(* 20 points *)
Lemma MasterOfInduction: forall B (L : List (Pair nat B)) n x,
get_nth L n = YES (mkPair n x) ->
get_nth (map (@second nat B) L) n = YES x.
Proof.
(* Here there are several ways to go. We will go the longer way so that
you can see the individual steps better. *)
intro.
(* We will strengthen the induction hypothesis as follows *)
assert (forall L n n' x, get_nth L n = YES (mkPair n' x) -> get_nth (map (@second nat B) L) n = YES x).
induction L; simpl; intros.
inversion H.
destruct n.
inversion H.
simpl.
trivial.
apply IHL with n'.
trivial.
(* Now things are easy *)
intros.
spec H L n n x.
apply H.
trivial.
Qed.
Fixpoint left_skewed (t : Tree) : Prop :=
match t with
| Leaf => True
| Node (Node t11 t12) t2 =>
left_skewed t11 /\ left_skewed t12 /\ left_skewed t2
| _ => False
end.
Fixpoint right_skewed (t : Tree) : Prop :=
match t with
| Leaf => True
| Node t1 (Node t21 t22) =>
right_skewed t1 /\ right_skewed t21 /\ right_skewed t22
| _ => False
end.
(* It's not really fair of me to ask you to do this, since it is quite
tricky. For 5 points, explain why it is tricky right here:
The obvious induction hypothesis is only useful if our children
are left-skewed. The right child is, but the left child is not
(it's two children are). We need a more general induction
hypothesis or the ability to apply the induction hypothesis to our
grandchildren (i.e., strong structural induction).
For 25 points of extra credit, solve it. Do everything else first.
You might find a way forward by cleverly strengthening the induction
hypothesis; alternatively you can investigate the "fix" tactic (look it
up in Coq reference manual). Note that "fix" can be very tricky to
use; make sure that you do a "Qed" before celebrating since it is
an "unsafe" tactic---you can get to "Proof completed." only to have
the "Qed" fail.
Good luck!
*)
(* I will provide two solutions for your study and comparison *)
(* Solution 1: using a more general induction hypothesis *)
Lemma swap_skew:
forall t, left_skewed t -> right_skewed (deep_swap t).
Proof.
assert (forall t, (left_skewed t -> right_skewed (deep_swap t)) /\
(forall t1 t2, t = Node t1 t2 ->
(left_skewed t1 -> right_skewed (deep_swap t1)) /\
(left_skewed t2 -> right_skewed (deep_swap t2)))).
induction t.
simpl.
split; trivial.
intros.
discriminate.
(* induction case *)
split.
intros.
destruct t1.
simpl in H.
contradiction.
simpl in H.
simpl.
destruct IHt1.
spec H1 t1_1 t1_2.
spec H1.
trivial.
destruct H1.
destruct IHt2.
destruct H.
destruct H5.
split.
apply H3.
trivial.
split.
apply H2.
trivial.
apply H1.
trivial.
(* other case *)
intros.
inversion H.
subst t0 t3.
split; intro.
destruct IHt1.
apply H1.
trivial.
destruct IHt2.
apply H1.
trivial.
(* Finally *)
intro.
spec H t.
destruct H.
trivial.
Qed.
(* Solution 2: using strong structual induction with fix *)
Lemma swap_skew2:
forall t, left_skewed t -> right_skewed (deep_swap t).
Proof.
fix 1.
destruct t; intros.
clear swap_skew2.
simpl.
trivial.
destruct t1.
simpl in H. contradiction.
simpl in H.
destruct H.
destruct H0.
apply swap_skew2 in H.
apply swap_skew2 in H0.
apply swap_skew2 in H1.
clear swap_skew2.
simpl.
split; trivial.
split; trivial.
Qed.