Software Foundations: More Basic Tactics

Tactics.v

Require Import List.
Require Import Nat.

Require Import Coq.Arith.Mult.

Theorem S_injective : forall n m : nat,
  S n = S m -> n = m.
Proof.
  intros. injection H.
  intros. apply H0.
Qed.

Theorem injection_ex : forall m n o : nat,
  (n, m) = (o, o) -> n = m.
Proof.
  intros. injection H.
  intros. rewrite H0. apply H1.
Qed.

Theorem S_inj : forall (n m : nat) (b : bool),
  S n =? S m = b -> n =? m = b.
Proof.
  intros. simpl in H. apply H.
Qed.

Theorem f_equal : forall (A B : Type) (f : A -> B) (x y : A),
  x = y -> f x = f y.
Proof.
  intros. rewrite H. reflexivity.
Qed.

Fixpoint double (n : nat) : nat :=
  match n with
  | O => O
  | S n => S (S (double n))
  end.

Theorem double_injective : forall n m : nat,
  double n = double m -> n = m.
Proof.
  intros n. induction n.
  - intros [].
    + reflexivity.
    + discriminate.
  - intros [] eq.
    + discriminate.
    + apply f_equal.
      apply IHn.
      injection eq as goal.
      apply goal.
Qed.

Definition square n := n * n.

Lemma square_mult : forall n m,
  square (n * m) = square n * square m.
Proof.
  intros.
  unfold square.
  rewrite mult_assoc.
  assert (H : n * m * n = n * n * m).
    { rewrite mult_comm. apply mult_assoc. }
  rewrite H.
  rewrite mult_assoc.
  reflexivity.
Qed.

Theorem eqb_true : forall (n m : nat),
  n =? m = true -> n = m.
Proof.
  intros n. induction n.
  - intros [] eq. reflexivity. discriminate.
  - intros [] eq.
    + discriminate.
    + apply f_equal. apply IHn. apply eq.
Qed.

Theorem nth_error_after_last : forall (A : Type) (l : list A) (n : nat),
  length l = n -> nth_error l n = None.
Proof.
  intros A l. induction l.
  - intros [] eq. reflexivity. discriminate.
  - intros [] eq.
    + discriminate.
    + injection eq as goal. apply IHl. apply goal.
Qed.

Lemma split_nil : forall {A B : Type} (a : A * B) (l : list (A * B)),
  split (a :: l) <> (nil, nil).
Proof.
  intros A B a.
  destruct a.
  simpl.
  intros.
  destruct (split l).
  discriminate.
Qed.

Theorem combine_split : forall (A B : Type) (l : list (A * B)) l1 l2,
  split l = (l1, l2) -> combine l1 l2 = l.
Proof.
  intros A B l.
  induction l.
  - intros. injection H.
    intros. rewrite <- H0. rewrite <- H1. reflexivity.
  - destruct a.
    simpl.
    destruct (split l) as [la lb].
    intros.
    injection H as H1 H2.
    rewrite <- H1, <- H2.
    simpl.
    assert (eq : combine la lb = l).
      { rewrite IHl. reflexivity. reflexivity. }
    apply f_equal.
    apply eq.
Qed.

Theorem bool_fn_applied_thrice : forall (f : bool -> bool) (b : bool),
  f (f (f b)) = f b.
Proof.
  intros f b.
  destruct (f b) eqn:Hb.
  - destruct b.
    + rewrite Hb, Hb. reflexivity.
    + destruct (f true) eqn:Htrue.
      * apply Htrue.
      * apply Hb.
  - destruct b.
    + destruct (f false) eqn:Hfalse.
      * apply Hb.
      * apply Hfalse.
    + rewrite Hb, Hb. reflexivity.
Qed.

Theorem eqb_sym : forall (n m : nat),
  (n =? m) = (m =? n).
Proof.
  induction n.
  - destruct m. reflexivity. reflexivity.
  - destruct m. reflexivity. apply IHn.
Qed.

Theorem eqb_trans : forall (n m p : nat),
  n =? m = true -> m =? p = true -> n =? p = true.
Proof.
  induction n.
  - destruct m, p. reflexivity. discriminate. discriminate. discriminate.
  - destruct m, p.
    + discriminate.
    + discriminate.
    + discriminate.
    + simpl. apply IHn.
Qed.

Theorem split_combine : forall (A B : Type) (l : list (A * B)) l1 l2,
  length l1 = length l2 -> combine l1 l2 = l -> split l = (l1, l2).
Proof.
  induction l.
  - intros [] []. reflexivity. discriminate. discriminate. discriminate.
  - intros [] [].
    + discriminate.
    + discriminate.
    + discriminate.
    + intros.
      injection H as H.
      injection H0 as H0.
      simpl.
      destruct a.
      rewrite (IHl l0 l1 H H1).
      injection H0 as Ha Hb.
      rewrite Ha, Hb.
      reflexivity.
Qed.

Theorem filter_exercise : forall {A : Type} (test : A -> bool) (a : A) (l lf : list A),
  filter test l = a :: lf -> test a = true.
Proof.
  induction l.
  - discriminate.
  - destruct (test a0) eqn:H.
    + intros lf eq.
      simpl in eq.
      rewrite H in eq.
      injection eq as eq _.
      rewrite eq in H.
      apply H.
    + intros lf eq.
      simpl in eq.
      rewrite H in eq.
      apply (IHl lf).
      apply eq.
Qed.

Fixpoint forallb {A : Type} (test : A -> bool) (l : list A) : bool :=
  match l with
  | nil => true
  | a :: l => test a && forallb test l
  end.

Fixpoint existsb {A : Type} (test : A -> bool) (l : list A) : bool :=
  match l with
  | nil => false
  | a :: l => test a || existsb test l
  end.

Definition existsb' {A : Type} (test : A -> bool) (l : list A) : bool :=
  negb (forallb (fun (a : A) => negb (test a)) l).

Theorem existsb_existsb' : forall (A : Type) (test : A -> bool) (l : list A),
  existsb test l = existsb' test l.
Proof.
  induction l.
  - reflexivity.
  - unfold existsb'.
    unfold forallb.
    simpl.
    destruct (test a).
    + reflexivity.
    + apply IHl.
Qed.