File 1

Propositional Logic, Equality, and Rewriting

Due	2019-9-19 11:45AM
Reading	Programs and Proofs: Chapter 3, Chapter 4.1-4.2, Mathematical Components: Chapter 2
Link	https://github.ccs.neu.edu/verifcomp/19/asgn/1.v

This assignment will get you started with proofs in Coq. You'll figure out how they are similar, and how they are different, from programming.

Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

Exercise 1. Prove the following lemmas. Use only the basic tactics introduced thus far.

Lemma id_P (P : Prop) : P -> P.
Admitted.

Lemma id_PP (P : Prop) : (P -> P) -> (P -> P).
Admitted.

Lemma imp_trans (P Q R : Prop) : (P -> Q) -> (Q -> R) -> P -> R.
Admitted.

Lemma imp_perm (P Q R : Prop) : (P -> Q -> R) -> (Q -> P -> R).
Admitted.

Lemma ignore_Q (P Q R : Prop) : (P -> R) -> P -> Q -> R.
Admitted.

Lemma delta_imp (P Q : Prop) : (P -> P -> Q) -> P -> Q.
Admitted.

Lemma delta_impR (P Q : Prop) : (P -> Q) -> (P -> P -> Q).
Admitted.

Lemma diamond (P Q R T : Prop) : (P -> Q) -> (P -> R) -> (Q -> R -> T) -> P -> T.
Admitted.

Lemma weak_peirce (P Q : Prop) : ((((P -> Q) -> P) -> P) -> Q) -> Q.
Admitted.

Exercise 2. (MASTERS CREDIT ONLY)

Lemma propEx (P Q R T : Prop) : (P -> Q) -> (Q -> R) -> ((P -> R) -> T -> Q) -> ((P -> R) -> T) -> Q.
Admitted.

Exercise 3. Experiments with falsehood.

Goal ~False.
Admitted.

Goal forall (P : Prop), ~ ~ ~P -> ~P.
Admitted.

Goal forall (P Q : Prop), ~ ~ ~P -> P -> Q.
Admitted.

Goal forall (P Q : Prop), (P -> Q) -> ~Q -> ~P.
Admitted.

Goal forall (P Q R : Prop), (P -> Q) -> (P -> ~Q) -> P -> R.
Admitted.

Goal (forall (P Q : Prop), (P -> Q) -> (Q -> P)) -> False.
Admitted.

Goal (forall (P Q : Prop), (P -> Q) -> (~P -> ~Q)) -> False.
Admitted.

Exercise 4. Experiments with existential types.

Section Ex4.
  Hypothesis A : Set.
  Hypothesis P Q : A -> Prop.

  Goal (exists x : A, P x \/ Q x) -> (ex P)\/(ex Q).
  Admitted.

  Goal (ex P)\/(ex Q) -> exists x : A, P x \/ Q x.
  Admitted.

  Goal (exists x : A, (forall R : A -> Prop, R x)) -> 2 = 3.
  Admitted.

  Goal (forall x : A, P x) -> ~(exists y : A, ~ P y).
  Admitted.
End Ex4.

Exercise 5. More classical equivalences.

Definition peirce := forall P Q : Prop,
  ((P->Q)->P)->P.
Definition classic := forall P : Prop,
  ~ ~P -> P.
Definition excluded_middle := forall P : Prop,
  P \/ not P.
Definition de_morgan_not_and_not := forall P Q : Prop,
  ~(~P /\ not Q) -> P \/ Q.
Definition implies_to_or := forall P Q : Prop,
    (P -> Q) -> (not P \/ Q).

Goal excluded_middle -> de_morgan_not_and_not.
Admitted.

Goal de_morgan_not_and_not -> implies_to_or.
Admitted.

Goal implies_to_or -> peirce.
Admitted.

Exercise 6. Some misc proofs about lists.

Fixpoint split {X Y : Type} (l : seq (X*Y))
  : (seq X) * (seq Y) :=
  match l with
  | [::] => ([::], [::])
  | (x, y) :: t =>
      match split t with
      | (lx, ly) => (x :: lx, y :: ly)
      end
  end.

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  zip l1 l2 = l.
Proof.
Admitted.

Theorem filter_exercise : forall (X : Type) (test : X -> bool)
                             (x : X) (l lf : list X),
     filter test l = x :: lf ->
     test x = true.
Proof.
Admitted.

Exercise 7: Equality!

Section Equality.
  Inductive eq {X:Type} : X -> X -> Prop :=
  | eq_refl : forall x, eq x x.

  Notation "x =~= y" := (eq x y)
                          (at level 70, no associativity)
                        : type_scope.

  Lemma equality_leibniz_equality : forall(X : Type) (x y : X),
      x =~= y -> forall P : X -> Prop, P x -> P y.
  Proof.
  Admitted.

  Lemma leibniz_equality_equality : forall(X : Type) (x y : X),
      (forall P : X -> Prop, P x -> P y) -> x =~= y.
  Proof.
  Admitted.
End Equality.