(*** Introduction to Computational Logic, Coq part of Assignment 12 ***)
(*** Solutions ***)
(***
Use Coq to complete the file below.  
If you have any questions, please use the discussion board.
http://www.ps.uni-saarland.de/courses/cl-ss12/forum/
***)

Set Implicit Arguments. Unset Strict Implicit.
Require Import Bool List Omega Setoid Recdef.
Notation "[ a , .. , b ]" := (a :: .. (b :: nil) ..).
Coercion bool2Prop (x : bool) : Prop := if x then True else False.

(** Boolean Reflection *)

Lemma negb_ref (x : bool) :
negb x <-> ~x.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma andb_ref x y :
x && y <-> x /\ y.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma orb_ref x y :
x || y <-> x \/ y.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma implb_ref x y :
implb x y <-> x -> y.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma bcontra (x : bool) :
~ (negb x) -> x.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma implb_orb x y :
implb x y = negb x || y.

Proof. destruct x ; reflexivity. Qed.

Definition inb (x : nat) (xs : list nat) : bool :=
if in_dec eq_nat_dec x xs then true else false.

Lemma inb_ref x A :
inb x A <-> In x A.

Proof. unfold inb. destruct (in_dec eq_nat_dec x A) ; simpl ; tauto. Qed.

Lemma forallb_ref X f A :
forallb f A <-> forall x : X, In x A -> f x.

Proof. induction A ; simpl. now firstorder.
rewrite andb_ref, IHA. split.
intros [B C] x [D|D]. congruence. now auto.
firstorder. Qed.

Lemma existsb_ref X f A :
existsb f A <-> exists x : X, In x A /\ f x.

Proof. induction A ; simpl. now firstorder.
rewrite orb_ref, IHA. split.
intros [B|B]. exists a. tauto.
destruct B as [x B]. exists x. tauto.
intros [x [[B|B] C]]. subst. tauto. 
right. exists x. auto. Qed.

Definition negbfun (X : Type) (f : X -> bool) (x : X) : bool := negb (f x).

Lemma negb_forallb X (f : X -> bool) A :
negb (forallb f A) = existsb (negbfun f) A.

Proof. induction A ; simpl. reflexivity.
rewrite negb_andb, IHA. reflexivity. Qed.

(** List inclusion and equivalence *)

Lemma cons_incl_elim X (x : X) A B :
incl (x :: A) B <-> In x B /\ incl A B.

Proof. split.
unfold incl ; simpl ; now auto.
intros [C D]. apply incl_cons ; assumption. Qed.

Lemma cons_incl X (x : X) A B :
incl A B -> incl (x::A) (x::B).

Proof. firstorder. Qed.

Definition equi X (A B : list X) :=
incl A B /\ incl B A.

Lemma equi_refl X (A : list X) :  equi A A.
Proof. firstorder. Qed.

Lemma equi_sym X (A B : list X) : equi A B -> equi B A.
Proof. firstorder. Qed.

Lemma equi_tran X (A B C : list X) : equi A B -> equi B C -> equi A C.
Proof. firstorder. Qed.

Add Parametric Relation X : (list X) (@equi X)
reflexivity proved by (@equi_refl X)
symmetry proved by (@equi_sym X)
transitivity proved by (@equi_tran X)
as equi_rel.

Add Parametric Morphism X : (@cons X) with 
signature eq ==> (@equi X) ==> (@equi X) as equi_cons_comp.

Proof. firstorder. Qed.

Add Parametric Morphism X : (@app X) with 
signature (@equi X) ==> (@equi X) ==> (@equi X) as equi_app_comp.

Proof. intros A B [C D] E F [G H] ; split
; auto using incl_app, incl_appl, incl_appr. Qed.

Lemma swap_cons X (x y : X) A :
equi (x :: y :: A) (y :: x :: A).

Proof. split ; intros z ; simpl ; tauto. Qed.

Lemma shift_cons X (x : X) A B :
equi (x :: A ++ B) (A ++ x :: B).

Proof. induction A ; simpl. reflexivity.
rewrite <- IHA, swap_cons. reflexivity. Qed.

Lemma rotate X (x : X) A :
equi (x :: A) (A ++ [x]).

Proof. induction A ; simpl. reflexivity.
rewrite <- IHA. rewrite swap_cons. reflexivity. Qed.

Lemma push_member X (x : X) A :
In x A -> equi A (x :: A).

Proof. induction A ; simpl. tauto.
intros [B|B]. now subst ; firstorder.
rewrite swap_cons, <- IHA. reflexivity. exact B. Qed.

(** Formulas *)

Definition var := nat.

Inductive form : Type :=
| Var : var -> form
| Imp : form -> form -> form
| Fal : form.

Definition Not (s : form) : form :=
Imp s Fal.

Definition FDN (s : form) : form := Imp (Not (Not s)) s.

(** Boolean Satisfiability *)

Definition assignment := list var.

Fixpoint eval (a : assignment) (s : form) : bool :=
match s with
| Var x => inb x a
| Imp s t => implb (eval a s) (eval a t)
| Fal => false
end.

Definition eva (a : assignment) (G : list form) : bool :=
forallb (eval a) G.

Definition sat (G : list form) : Prop := 
exists a, eva a G.

Lemma eva_incl G G' a :
incl G G' -> eva a G' -> eva a G.

Proof. unfold eva, incl. rewrite forallb_ref, forallb_ref. firstorder. Qed.

Lemma sat_incl G G':
incl G G' -> sat G' -> sat G.

Proof. intros A [a B]. exists a. exact (eva_incl A B). Qed.

Add Morphism sat with 
signature (@equi form) --> iff as sat_mor.

Proof. intros A B [C D] ; split ; intros E ; eauto using sat_incl. Qed.

Lemma eval_not a s :
~eval a (Not s) <-> eval a s.

Proof. split ; simpl ; destruct (eval a s) ; simpl ; auto. Qed.

Definition valid (s : form) : Prop := 
forall a, eval a s.

Lemma valid_unsat s :
valid s <-> ~sat [Not s].

Proof. unfold sat, valid ; simpl ; split.
intros A [a B]. specialize (A a). now destruct (eval a s) ; auto.
intros A a. apply bcontra ; intros B.
apply A. exists a. destruct (eval a s) ; auto. Qed.

Goal forall G s,
(forall a, eva a G -> eval a s) <-> ~sat (Not s :: G).

Proof. split.
intros A [a B]. specialize (A a). revert B. simpl.
destruct (eval a s) ; tauto.
intros A a B. apply bcontra ; intros C.
apply A. exists a. simpl. destruct (eval a s) ; tauto. Qed.

(** ND Systems *)

Inductive nd : list form -> form -> Prop :=
| ndA G s :
  nd (s::G) s
| ndW G s t :
  nd G s -> nd (t::G) s
| ndII G s t :
  nd (s::G) t -> nd G (Imp s t)
| ndIE G s t :
  nd G (Imp s t) -> nd G s -> nd G t
| ndE G s :
  nd G Fal -> nd G s.

Lemma ndM s G :
In s G -> nd G s.

Proof. induction G ; simpl. tauto.
intros [A|A]. subst. now apply ndA. apply ndW ; auto. Qed.

Lemma nd_incl G G' s :
incl G G'-> nd G s -> nd G' s.

Proof. intros A B. revert G' A ; induction B ; intros G' A.
(* ndA *) apply ndM, A ; simpl. tauto.
(* ndW *) apply IHB. apply cons_incl_elim in A. destruct A ; assumption.
(* ndII *) apply ndII, IHB. now apply cons_incl, A.
(* ndIE *) apply ndIE with (s:=s) ; now auto.
(* ndE *) apply ndE, IHB, A. Qed.

Add Morphism nd with 
signature (@equi form) ==> eq ==> iff as nd_mor.

Proof. firstorder using nd_incl. Qed.

Inductive ndc : list form -> form -> Prop :=
| ndcA G s :
  ndc (s::G) s
| ndcW G s t :
  ndc G s -> ndc (t::G) s
| ndcII G s t :
  ndc (s::G) t -> ndc G (Imp s t)
| ndcIE G s t :
  ndc G (Imp s t) -> ndc G s -> ndc G t
| ndcC G s :
  ndc (Not s :: G) Fal -> ndc G s.

Lemma ndc_refut G s :
ndc G s <-> ndc (Not s :: G) Fal.

Proof. split ; intros A. 
apply ndcIE with (s:=s). now apply ndcA. now apply ndcW, A.
apply ndcC, A. Qed.

Lemma nd_ndc G s :
nd G s -> ndc G s.

Proof. intros A ; induction A.
(* ndA *) now apply ndcA.
(* ndW *) now apply ndcW, IHA.
(* ndII *) now apply ndcII, IHA.
(* ndIE *) apply ndcIE with (s:=s). exact IHA1. exact IHA2.
(* ndC *) apply ndcC, ndcW, IHA. Qed.

(** Soundness *)

Lemma ndc_sound G s a :
ndc G s -> eva a G -> eval a s.

Proof. intros A B ; induction A ; simpl in *|-*.
(* ndcA *) now destruct (eval a s) ; simpl ; auto. 
(* ndcW *) now destruct (eval a t) ; simpl in B ; auto.
(* ndcII *) now destruct (eval a s) ; simpl in *|- ; auto.
(* ndcIE *) now destruct (eval a s) ; simpl in *|- ; auto.
(* ndcC *) now destruct (eval a s) ; simpl in *|- ; auto. Qed.

Lemma nd_sat G :
nd G Fal -> ~sat G.

Proof. intros A [a B]. apply nd_ndc in A. 
exact (ndc_sound A B). Qed.

Goal ~ndc nil Fal.

Proof. intros A. apply ndc_sound with (a:=nil) in A.
contradiction A. exact I. Qed.

Goal forall x, ~ndc nil (Var x).

Proof. intros x A. 
apply ndc_sound with (a:=nil) in A.
contradiction A. exact I. Qed.

Goal forall x, ~ndc nil (Not (Var x)).

Proof. intros x A. 
apply ndc_sound with (a:=[x]) in A.
simpl in A. rewrite implb_ref, inb_ref in A. now firstorder.
exact I. Qed.

(* Main Results *)

Definition csc (G : list form) (s : form) : Prop :=
forall a, eva a G -> eval a s.

Goal forall G s,  ndc G s -> csc G s.

Proof. intros G s A a. exact (ndc_sound A). Qed.

Section Main_Results.

Variable sat_nd : forall G, {sat G} + {nd G Fal}.

Goal forall G s, ndc G s <-> csc G s.

Proof. split.
intros A a. exact (ndc_sound A).
intros A. apply ndcC, nd_ndc. 
destruct (sat_nd (Not s :: G)) as [[a B]|B].
exfalso. specialize (A a). simpl in B. destruct (eval a s) ; tauto. 
exact B. Qed.

Definition ndc_dec G s : {ndc G s} + {~ndc G s}.

destruct (sat_nd (Not s :: G)) as [A|A].
right. intros B. destruct A as [a A]. simpl in A. 
apply andb_ref in A. destruct A as [A C]. apply (ndc_sound B) in C.
destruct (eval a s) ; tauto.
left. apply ndcC, nd_ndc, A. Defined.

Goal forall G, nd G Fal <-> ndc G Fal.

Proof. split. now apply nd_ndc.
intros A ; destruct (sat_nd G) as [B|B].
destruct B as [a B]. contradiction (ndc_sound A B).
exact B. Qed.

(*** Exercise 12.1 ***)
Goal forall G, nd G Fal <-> ~sat G.

(*** Give Proof ***)

Goal forall s, ndc nil s <-> valid s.

(*** Give Proof ***)

(*** Exercise 12.2 ***)
Definition sat_dec G : {sat G} + {~sat G}.

(*** Give Definition as a Script ***)

Definition nd_dec G : {nd G Fal} + {~nd G Fal}.

(*** Give Definition as a Script ***)

End Main_Results.

Check ndc_dec.

(** Tableau System *)

Inductive tab : list form -> Prop :=
| tabF C : tab (Fal :: C)
| tabC s C : tab (Not s :: s :: C)
| tabIP s t C : tab (Not s :: C) -> tab (t :: C) -> tab (Imp s t :: C)
| tabIN s t C : tab (s :: Not t :: C) -> tab (Not (Imp s t) :: C)
| tabS C C' : equi C C' -> tab C -> tab C'.

Goal tab [Not (FDN (Var 0))].

Proof. apply tabIN. apply tabC. Qed.

Definition x := Var 0.
Definition y := Var 1.
Definition Peirce := Imp (Imp (Imp x y) x) x.

Goal tab [Not Peirce].

Proof. apply tabIN. apply tabIP.
apply tabIN. 
apply tabS with (C := [Not x, x, Not y]). now firstorder.
now apply tabC.
apply tabS with (C := [Not x, x]). now firstorder.
now apply tabC. Qed.

Add Morphism tab with 
signature (@equi form) --> iff as tab_equi_comp.

Proof. firstorder using tabS. Qed.

Goal tab [Not Peirce].

Proof. apply tabIN. apply tabIP.
apply tabIN. rewrite rotate ; simpl. rewrite rotate ; simpl. 
now apply tabC.
rewrite swap_cons. apply tabC. Qed.

Lemma tab_nd C :
tab C -> nd C Fal.

Proof. intros A ; induction A.
(* tabF *) now apply ndA.
(* tabC *) apply ndIE with (s:=s). now apply ndA. now apply ndW, ndA.
(* tabIP *) apply ndIE with (s:= Not s). now apply ndW, ndII, IHA1.
apply ndII. apply ndIE with (s:=t). now apply ndW, ndW, ndII, IHA2.
apply ndIE with (s:=s). now apply ndW, ndA. apply ndA.
(* tabIN *) apply ndIE with (s:= Imp s t). now apply ndA.
apply ndII, ndE.
apply ndIE with (s:= Not t). 
apply ndIE with (s:= s). 
apply ndW, ndW, ndII, ndII. rewrite swap_cons. exact IHA.
now apply ndA.
apply ndII. 
apply ndIE with (s:= Imp s t). now apply ndW, ndW, ndA.
apply ndII, ndW, ndA.
(* tabS *) rewrite <- H. exact IHA. Qed.

Lemma tabW C s :
tab C -> tab (s :: C).

Proof. intros A ; induction A.
(* tabF *) rewrite rotate ; simpl. now apply tabF.
(* tabC *) rewrite rotate ; simpl. now apply tabC.
(* tabIP *) rewrite rotate ; rewrite rotate in IHA1, IHA2 ; simpl in *|-*.
apply tabIP ; assumption.
(* tabIN *) rewrite rotate ; rewrite rotate in IHA ; simpl in *|-*.
apply tabIN ; assumption.
(* tabS *) rewrite <- H. exact IHA. Qed.

Lemma tabClash C s :
In (Not s) C -> In s C -> tab C.

Proof. intros A B. rewrite (push_member A), (push_member B). apply tabC. Qed.

(** Co-Tableau *)

Definition nvar (x : var) : form := Not (Var x).

Definition solved (C : list form) : Prop :=
exists P : list var, exists N : list var,
C = map Var P ++ map nvar N /\ eva P (map nvar N).

Inductive cotab : list form -> Prop :=
| cotabV C : solved C -> cotab C
| cotabIPF C : cotab C -> cotab (Not Fal :: C)
| cotabIPL C s t : cotab (Not s :: C) -> cotab (Imp s t :: C)
| cotabIPR C s t : cotab (t :: C) -> cotab (Imp s t :: C)
| cotabIN C s t : cotab (s :: Not t :: C) -> cotab (Not (Imp s t) :: C)
| cotabS C C' : equi C C' -> cotab C -> cotab C'.

Add Morphism cotab with 
signature (@equi form) --> iff as cotab_equi_comp.

Proof. firstorder using cotabS. Qed.

Lemma eva_map_var A Q :
eva A (map Var Q) <-> incl Q A.

Proof. induction Q ; simpl. now firstorder.
rewrite andb_ref, inb_ref, IHQ ; clear IHQ.
symmetry. apply cons_incl_elim. Qed.

Lemma solved_sat C :
solved C -> sat C.

Proof. intros A. destruct A as [P [N [A B]]]. subst C. exists P.
unfold eva. rewrite forallb_app, andb_ref ; split.
change (eva P (map Var P)). rewrite eva_map_var. now apply incl_refl.
exact B. Qed.

Lemma cotab_sat C :
cotab C -> sat C.

Proof. intros A. induction A.
(* cotabV *) now apply solved_sat, H.
(* cotabF *) destruct IHA as [a B]. exists a ; simpl. exact B.
(* cotabIPL *) destruct IHA as [a B]. exists a ; revert B ; simpl.
destruct (eval a s) ; simpl ; tauto.
(* cotabIPR *) destruct IHA as [a B]. exists a ; revert B ; simpl.
destruct (eval a s), (eval a t) ; simpl ; tauto.
(* cotabIN *) destruct IHA as [a B]. exists a ; revert B ; simpl.
destruct (eval a s) ; simpl ; tauto.
(* cotabS *) rewrite <-H. exact IHA. Qed.

(** Decision Procedure *)

Inductive clause : Type :=
| CL : list form -> list form -> list var -> list var -> clause.

Coercion clause2list (C : clause) : list form :=
match C with CL P N Q R =>
  P ++ map Not N ++ map Var Q ++ map nvar R
end.

Definition cl C := CL C nil nil nil.

Lemma ecl C :
equi C (cl C).

Proof. simpl. rewrite app_nil_r. reflexivity. Qed.

Fixpoint size_form (s : form) : nat :=
match s with
| Var _ => 1
| Imp s t => S (size_form s + size_form t)
| Fal => 1
end.

Definition size_list := fold_right (fun s a => size_form s + a) 0.

Definition size_clause (C : clause) : nat :=
match C with CL P N _ _ => size_list P + size_list N end.

Function dec (C : clause)  {measure size_clause C} : bool :=
match C with CL P N Q R => 
match P with
  | Fal :: _  => false
  | Var x :: P' => dec (CL P' N (x :: Q) R)
  | Imp s t :: P'  => dec (CL P' (s :: N) Q R) || dec (CL (t :: P') N Q R)
  | nil => match N with
             | Fal :: N' => dec (CL nil N' Q R)
             | Var x :: N' => dec (CL nil N' Q (x :: R))
             | Imp s t :: N'  => dec (CL [s] (t :: N') Q R)
             | nil => eva Q (map nvar R)
           end
end end.

intros ; simpl ; omega.
intros ; simpl ; omega.
intros ; simpl ; omega.
intros ; simpl ; omega.
intros ; simpl ; omega.
intros ; simpl ; omega. 
Defined.

Compute dec (cl [FDN (Var 0)]).
Compute dec (cl [Not (FDN (Var 0))]).
Compute dec (cl [Var 0]).
Compute dec (cl [Not (Var 0)]).

(* Correctness *)

Lemma dec_cotab C :
dec C -> cotab C.

Proof. functional induction (dec C) ; simpl ; intros A.
(* Fal+ *) contradiction A.
(* Var+ *) rewrite shift_cons, shift_cons. exact (IHb A).
(* Imp+ *) rewrite orb_ref in A ; destruct A as [A|A].
apply cotabIPL. rewrite shift_cons. exact (IHb A).
apply cotabIPR. exact (IHb0 A).
(* Fal- *) apply cotabIPF. exact (IHb A).
(* Var- *) rewrite shift_cons, shift_cons. exact (IHb A).
(* Imp- *) apply cotabIN. exact (IHb A).
(* Done *) apply cotabV. exists Q, R. auto. Qed.

Lemma eva_map_nvar Q R :
eva Q (map nvar R) = forallb (fun x => negb (inb x Q)) R.

Proof. induction R ; simpl. reflexivity.
rewrite IHR. destruct (inb a Q) ; reflexivity. Qed.

Lemma clash P N :
negb (eva P (map nvar N)) -> tab (map Var P ++ map nvar N).

Proof. rewrite eva_map_nvar, negb_forallb, existsb_ref. intros [x [A B]]. unfold negbfun in B. rewrite negb_involutive, inb_ref in B.
apply tabClash with (s:= Var x).
apply in_or_app ; right. exact (in_map _ _ _ A).
apply in_or_app ; left. exact (in_map _ _ _ B). Qed.

Lemma dec_tab C :
negb (dec C) -> tab C.

Proof. intros A ; functional induction (dec C) ; simpl in *|-*.
(* Fal+ *) now apply tabF.
(* Var+ *) rewrite shift_cons, shift_cons. exact (IHb A).
(* Imp+ *) rewrite negb_orb, andb_ref in A. destruct A as [A1 A2].
apply tabIP. rewrite shift_cons. exact (IHb A1). exact (IHb0 A2).
(* Fal- *) apply tabW. exact (IHb A).
(* Var- *) rewrite shift_cons, shift_cons. exact (IHb A).
(* Imp- *) apply tabIN. exact (IHb A).
(* Done *) exact (clash A). Qed.

Definition IBC (x : bool) : {x} + {negb x}.

destruct x. left. exact I. right. exact I. Defined.

Definition tableau C : {cotab C} + {tab C}.

destruct (IBC (dec (cl C))) as [A|A].
left. rewrite ecl. exact (dec_cotab A).
right. rewrite ecl. exact (dec_tab A). Defined.

Definition sat_nd C : {sat C} + {nd C Fal}.

destruct (tableau C) as [A|A]. 
left. now apply cotab_sat, A.
right. now apply tab_nd, A. Defined.

(** Exercise 12.5 **)

Lemma cotab_sat_equiv : forall C, cotab C <-> sat C.

(*** Give Proof ***)

Lemma tab_unsat_equiv : forall C, tab C <-> ~sat C.

(*** Give Proof ***)

(** Exercise 12.6 **)

Definition tab_dec C : {tab C} + {~tab C}.

(*** Give Definition as a Script ***)

Definition cotab_dec C : {cotab C} + {~cotab C}.

(*** Give Definition as a Script ***)

(*** Exercise 12.7 ***)
Lemma cotabW C s : cotab (s::C) -> cotab C.

(*** Give Proof ***)

(*** Sigma Types and Proof Irrelevance ***)
(*** Exercise 12.9 ***)
Print sig.

Lemma bPI (x:bool) : forall (H H':x), H = H'.

(*** Give Proof ***)

Lemma sig_bPI (X:Type) (p:X -> bool) (x y : X) (H : p x) (H' : p y) : x = y
 -> exist (fun z => p z) x H = exist (fun z => p z) y H'.

(*** Give Proof ***)

(*** Quotients ***)
Fixpoint evenb (x : nat) : bool :=
match x with
| O => true
| S x' => negb (evenb x')
end.

(*** An Equivalence relation is a type X with a relation E which is reflexive, symmetric and transitive.
 We define a corresponding "Module Type" EQUIVRELN in Coq. ***)
Module Type EQUIVRELN.
 Parameter X:Type.
 Parameter E:X -> X -> Prop.
 Axiom Eref : forall x, E x x.
 Axiom Esym : forall x y, E x y -> E y x.
 Axiom Etra : forall x y z, E x y -> E y z -> E x z.
End EQUIVRELN.

(*** Now to implement an equivalence relation, we give a Module of Module Type EQUIVRELN.
     Here is an example: nat with the full equivalence relation. ***)
Module NATMODALL <: EQUIVRELN.
Definition X := nat.
Definition E := fun n m:nat => True.
Lemma Eref : forall x, E x x.
Proof. firstorder. Qed.
Lemma Esym : forall x y, E x y -> E y x.
Proof. firstorder. Qed.
Lemma Etra : forall x y z, E x y -> E y z -> E x z.
Proof. firstorder. Qed.
End NATMODALL.

(*** Given an equivalence relation (a Module of Module Type EQUIVRELN) E',
a Quotient consists of a type Q and two functions A and C satisfying the two properties below. ***)
Module Type QUOT (E':EQUIVRELN).
  Import E'.
  Parameter Q:Type.
  Parameter A:X -> Q.
  Parameter C:Q -> X.
  Axiom C_inj : forall a b, E (C a) (C b) -> a = b.
  Axiom CA_id : forall x, E (C (A x)) x.
End QUOT.

(*** To implement a quotient for E', we give a Module of Module Type QUOT E'. ***)
Module NATMODALLQUOT <: QUOT NATMODALL.
Import NATMODALL.
Definition Q := unit.
Definition A := fun n:nat => tt.
Definition C := fun _:unit => 0.
Lemma C_inj : forall a b, E (C a) (C b) -> a = b.
Proof. intros [] [] H. reflexivity. Qed.
Lemma CA_id : forall x, E (C (A x)) x.
Proof. intros x. unfold E. tauto. Qed.
End NATMODALLQUOT.

(*** Exercise 12.10 ***)
Module NATMOD2 <: EQUIVRELN.
Definition X := nat.
Definition E := fun x y => evenb x = evenb y.
Lemma Eref : forall x, E x x.
Proof. firstorder. Qed.
Lemma Esym : forall x y, E x y -> E y x.
Proof. firstorder. Qed.
Lemma Etra : forall x y z, E x y -> E y z -> E x z.
Proof. unfold E. intros x y z H1 H2. rewrite H1. exact H2. Qed.
End NATMOD2.

Module NATMOD2QUOT <: QUOT NATMOD2.
Import NATMOD2.
(*** Give Implemenation of Module (Define Q,A,C and prove C_inj and CA_id) ***)
End NATMOD2QUOT.

Module LISTLEN <: EQUIVRELN.
Definition X := list nat.
Definition E := fun l l':list nat => length l = length l'.
Lemma Eref : forall x, E x x.
Proof. firstorder. Qed.
Lemma Esym : forall x y, E x y -> E y x.
Proof. firstorder. Qed.
Lemma Etra : forall x y z, E x y -> E y z -> E x z.
Proof. unfold E. now firstorder. Qed.
End LISTLEN.

Module LISTLENQUOT <: QUOT LISTLEN.
Import LISTLEN.
(*** Give Implemenation of Module (Define Q,A,C and prove C_inj and CA_id) ***)
End LISTLENQUOT.

Module BOOLFUN <: EQUIVRELN.
Definition X := bool -> bool.
Definition E := fun f g:bool -> bool => forall b, f b = g b.
Lemma Eref : forall x, E x x.
Proof. firstorder. Qed.
Lemma Esym : forall x y, E x y -> E y x.
Proof. firstorder. Qed.
Lemma Etra : forall x y z, E x y -> E y z -> E x z.
Proof. unfold E. intros x y z H1 H2 b. rewrite H1. now apply H2. Qed.
End BOOLFUN.

Module BOOLFUNQUOT : QUOT BOOLFUN.
Import BOOLFUN.
(*** Give Implemenation of Module (Define Q,A,C and prove C_inj and CA_id) ***)
End BOOLFUNQUOT.