Reference no: EM133168869

Assignment: Properties and logic

- Please never change names or statements of Theorems,
Lemmas, Definitions, Examples or anything else provided here.
- [Abort] only additional lemmas that you did not manage to prove.
For theorems provided here, either use [Qed]/[Defined] or keep [Admitted].
- Please do not change the file name.
- Do not post your solution in any publically available location.
- Please submit on time, late solutions not accepted.
- Before submission, please check from command line if your script compiles.
In other words, do run [coqc] to make sure it accepts your file.
If it doesn't, no points can be awarded.
- Please submit _only_ the source file of the solution, i.e., [*.v]!
- Compiled output [*.vo] is useless for submission.

Exercise 1: Membership with decidable equality

(** Recall the type [sumbool] from ProSeSu22.v*)
(** An alternate way to characterize decision procedures, widely used in Coq, is via the inductive type [sumbool].

Suppose [Q] is a proposition, that is, [Q: Prop].
- We say [Q] is _decidable_ if there is an algorithm for
computing a proof of [Q] or [~Q].
- More generally, when [P] is a predicate
(a function from some type [T] to [Prop]),
we say [P] is decidable when [forall x:T, decidable(P)].

We represent this concept in Coq by an inductive datatype: *)

Exercise 2: Reflection for predicates on lists

** The standard library offers an inductive predicate for comparing lists wrt to a given binary relation *)

Print Forall2.

(**

Inductive Forall2 (A B : Type) (R : A -> B -> Prop) : list A -> list B -> Prop :=
Forall2_nil : Forall2 R [] []
| Forall2_cons : forall (x : A) (y : B) (l : list A) (l' : list B),
R x y -> Forall2 R l l' -> Forall2 R (x :: l) (y :: l')
*)

(** First, let us recall what it means for a relation to be reflected by a binary function. *)

Definition Rreflected {A B : Type} (R : A -> B -> Prop) (f: A -> B -> bool) :=
forall a b, reflect (R a b) (f a b).

(** Define its boolean counterpart. It might be a good idea to do pattern matching on two arguments at the same time. *)

Fixpoint forall2 {A B : Type} (R : A -> B -> Prop) (f: A -> B -> bool) (P: Rreflected R f) (la: list A) (lb : list B) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(** In the following proof, you might:
- want to think whether you do induction first, or rather
apply some trivial reflection view first to split the goal
- recall you can handle boolean conjunctions with [move => /andP ...]
- realize that (instantiated) premises can be also used as reflection views.
*)

Theorem forall2P {A B : Type} (R : A -> B -> Prop) (f: A -> B -> bool) : forall (P: Rreflected R f), Rreflected (Forall2 R) (forall2 R f P).
Proof.

Exercise 3: constructive quantification *)

(** **** Exercise: 3 stars, standard (quantifiers) *)

(** Many of familiar laws for quantifiers still hold for constructive logic.
Here and everywhere below you can actually provide a normal tactic proof if writing down proof term provides too difficult. *)

Definition notexists_forallnot : forall (X:Type) (P : X -> Prop),
~ (exists x : X, P x) -> (forall x : X, ~ P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Definition forallnot_notexists : forall (X:Type) (P : X -> Prop),
(forall x, ~ P x) -> ~ (exists x, P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Definition forallnot_equiv_notexists : forall (X:Type) (P : X -> Prop),
(forall x, ~ P x) <-> ~ (exists x, P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Definition forallnotnot_equiv_notexistsnot : forall (X:Type) (P : X -> Prop),
(forall x, ~ ~ P x) <-> ~ (exists x, ~ P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Lemma CEpqENpNq : forall P Q, (P <-> Q) -> (~P <-> ~Q).
Proof.
(* FILL IN HERE *) Admitted.

Definition notforallnot_equiv_notnotexists : forall (X:Type) (P : X -> Prop),
~(forall x, ~ P x) <-> ~ ~ (exists x, P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Definition existsnot_notforall : forall (X:Type) (P : X -> Prop),
(exists x, ~ P x) -> ~ (forall x, P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Definition forall_notexistsnot : forall (X:Type) (P : X -> Prop),
(forall x, P x) -> ~ (exists x, ~ P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(** How about the converse of the last one? As it turns out, it requires
classical logic, see below ... *)

Exercise 4, elective: classical axioms

(** **** Exercise: 4 stars, advanced, optional (classical_axioms) *)

(** Let us have a closer look at classical propositions in Coq. *)

(** Here are several "classical" properties and axioms. When universally quantified over all propositions, all of them imply each other. Sometimes, it makes sense to state them for individual propositions too, especially in the context of reflection with boolean functions. *)

(** Recall again: here and everywhere below you can actually provide a normal tactic proof if writing down proof term provides too difficult. *)

Definition em_for_P (P : Prop) := P \/ ~P.
(** The above is sometimes called _decidability_ for [P], but one should be slightly careful about this name. *)
Definition peirce_for_P (P:Prop) := forall Q: Prop,
((P->Q)->P)->P.
Definition dn_elimination_for_P (P : Prop) :=
~ ~P -> P.
Definition de_morgan_not_and_not_forPQ (P Q:Prop) :=
~(~P /\ ~Q) -> P\/Q.
Definition implies_to_or_forPQ (P Q:Prop) :=
(P->Q) -> (~P\/Q).

Definition excluded_middle := forall P, em_for_P P.
Definition peirce := forall P, peirce_for_P P.
Definition double_negation_elimination := forall P:Prop, dn_elimination_for_P P.
Definition de_morgan_not_and_not := forall P Q:Prop,
de_morgan_not_and_not_forPQ P Q.
Definition implies_to_or := forall P Q:Prop, implies_to_or_forPQ P Q.

Exercise 5: Kuroda and some classical aspects of negation

(** Warning: in this exercise you might find yourself in need of some theorems from the previous elective one. In such a case, go back and prove what's needed (thus earning more points). *)

(** Just like in the propositional case, there are many propositions which cannot be proved in the intuitionistic logic, but are not as strong as classical axioms either. Here is a famous example: *)

Definition kuroda (X:Type) (P : X -> Prop) :=
(forall x, ~ ~ P x) -> ~ ~(forall x, P x).

(** This law of course trivially holds in classical logic. *)

(** Here and everywhere below you can actually provide
a normal tactic proof
if writing down proof term provides too difficult. *)

Definition decprop {X: Type} P := forall (x : X), P x \/ ~ P x.

Definition classic_kuroda : forall X P, decprop P -> kuroda X P
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(** Here is an example of a law governing the interaction of negation and quantification, which only requires the Kuroda axiom: *)

Definition notforall_notnotexistsnot :
forall (X:Type) (P : X -> Prop), kuroda X P ->
~ (forall x, P x) -> ~ ~ (exists x, ~ P x)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(** However, there are laws which require more of classical logic. Some not all that much: *)

Theorem notexistsnot_forall : forall (X:Type) (P : X -> Prop),
(decprop P) ->
~ (exists x, ~ P x) -> (forall x, P x).
Proof.
(* FILL IN HERE *) Admitted.

(** [] *)

Attachment:- Properties and logic.rar