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.

The way of sharing the post is amazing. I really like it. Doing a paper can sometimes feel overwhelming, especially when you are juggling so many responsibilities. It is like trying to find a needle in a haystack with all the information out there. What I appreciate about services like do my paper is that they can help lighten the load when things get too hectic. Visit here domypaper.com it is not about taking the easy way out, it is about getting support when you need it most. Everyone has their strengths, and sometimes we just need a little extra help to get our thoughts organized and on paper.