Reference no: EM133170102

Assignment: Properties and logic

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: *)

(** Locate sumbool. =>

Inductive Coq.Init.Specif.sumbool

Print sumbool. =>

Inductive sumbool (A B : Prop) : Set := left : A -> {A} + {B} | right : B -> {A} + {B} you can find more about sumbool in ProSeSu22.v (in the course material folder) *)

Definition deceq (X: Type) := forall (x y : X), {x = y} + {x <> y}.

(** Now let us generalize what we did for lists natural numbers. Recall that [sumbool]s can be treated as "fancy bools"... *)

Fixpoint inb {X:Type} (d: deceq X) (a: X) (l : list X) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(** The [sumboolP] view can prove quite useful below. *) Print sumboolP.

Theorem inbP {X:Type} (d: deceq X) n l : reflect (In n l) (inb d n l).
Proof. (* FILL IN HERE *) Admitted.

(** Let us now return to [nat]s, but in a somewhat roundabout way. *)

(** Here is yet another way of stating that a type has decidable equality. *)

Inductive booleq {X : Type} (d: X -> X -> bool) :=
Beq : (forall x : X, d x x = true) ->
(forall x y : X, d x y = true -> x = y) -> booleq d.

Theorem refbool {X: Type} {d: X -> X -> bool} (be: booleq d) : deceq X.
Proof. (* FILL IN HERE *) Admitted.

(** Now you might search a bit for theorems about [eqb], or prove the following fact directly. *)

Theorem eqb_wrap : booleq eqb.
Proof. (* FILL IN HERE *) Admitted.

Corollary innatP {X:Type} n l : reflect (In n l) (inb (refbool eqb_wrap) n l).
Proof. (* FILL IN HERE *) Admitted.

(** The last result should be just an application of [inbP]. *)

(** Of course, there is a still quicker route to show inhabitation of [deceq nat]: standard library... *)

Check eq_dec.

Definition exact_deceq : (deceq nat). exact (eq_dec). Defined.

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.
(* FILL IN HERE *) Admitted.

Exercise 3: constructive quantification

(** 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 ... *)

(** [] *)

Attachment:- Assignment3_exercises.rar