MikeMKH

(* exercise 5.1 from Coq Art *)

Lemma id_P :
  forall P : Prop, P -> P.
Proof.
  intros P H.
  assumption.
Qed.

Lemma id_PP :

MikeMKH

(* exercise 4.3 from Coq Art *)

Lemma all_perm :
  forall (A : Type) (P : A -> A -> Prop),
    (forall x y : A, P x y) ->
      forall x y : A, P y x.
Proof.
  intros A P H x y.
  apply H.
Qed.

MikeMKH

Definition ninc (n : nat) : nat := n + 1.
Definition ntwice (f : nat -> nat) (n : nat) : nat := f (f n).

Eval cbv in (ntwice ninc 0).
(* = 2 *)

Eval cbv delta [ninc ntwice] in (ntwice ninc 0).
(* = (fun (f : nat -> nat) (n : nat) => f (f n)) (fun n : nat => n + 1) 1 *)

Eval cbv delta [ninc] in (ntwice ninc 0).

MikeMKH

(* exercise 3.5 from Coq Art *)

Section section_for_cut_example.
  Variables P Q R T : Prop.

  Hypotheses (H  : P -> Q)
             (H0 : Q -> R)
             (H1 : (P -> R) -> T -> Q)
             (H2 : (P -> R) -> T).

MikeMKH

(* exercise 3.2 from Coq Art *)

Variables P Q R T : Prop.

Lemma id_P : P -> P.
Proof.
  intro H.
  assumption.
Qed.

MikeMKH

(* taken from More Exercies - exercie 3 of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Inductive bin : Type :=
| Zero : bin
| Twice : bin -> bin
| More : bin -> bin.

Function bin_incr (n : bin) : bin :=
  match n with
  | Zero => More Zero

MikeMKH

(* taken from More Exercises sections in https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
    (forall (x : bool), f x = x)
      -> forall (b : bool), f (f b) = b.
Proof.
  intros f H b.
  rewrite -> H.
  rewrite -> H.

MikeMKH

(* taken from By Case Analysis section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Fixpoint beq_nat (n m : nat) : bool :=
  match n, m with
  | O, O       => true
  | O, _       => false
  | S _, O     => false
  | S n', S m' => beq_nat n' m'
  end.

MikeMKH

(* taken from the Proof by Rewriting section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Theorem plus_id : forall n m : nat,
  n = m -> n + n = m + m.
Proof.
  intros.
  rewrite <- H.
  reflexivity.
Qed.

MikeMKH

(* taken from https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Theorem plus_0_l : forall n : nat, 0 + n = n.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Theorem plus_1_l : forall n : nat, 1 + n = S n.