(* Exercises on Higher Order Logic in Coq and its relation to Inductive Types *)


Section Leib.
(* Define the Leibniz equality on A *)
Variable A : Set.
Definition Lq (x y : A) := forall P : A -> Prop, P x -> P y.

Lemma LRefl : forall x : A, Lq x x.
Admitted.

Lemma LTrans : forall x y z : A, Lq x y -> Lq y z -> Lq x z. 
Admitted.

Lemma LSymm : forall x y : A, Lq x y -> Lq y x.
Admitted.
(* There is a surprisingly simple tactic script that proves this.
   Please also inspect and try to understand the generated proof term by typing
   Print LSymm.
*)

Lemma Leib_implies_eq : forall x y : A, Lq x y -> x = y.
Admitted.

Lemma eq_implies_Leib : forall x y : A,  x = y -> Lq x y.
Admitted.

End Leib.


Section Rels.
(* Basics about relations *)
Variable A : Set.
Variable R : A -> A -> Prop.
Variable Q : A -> A -> Prop.
Definition Trans := forall x y z : A, R x y -> R y z -> R x z. 
Definition Sym := forall x y : A, R x y -> R y x. 
Definition Subset := forall x y : A, R x y -> Q x y.
End Rels.

Section TrClos.
Variable A : Set.
Variable R : A -> A -> Prop.

(* We define the transitive closure of R using higher order logic *)
Definition Trclos (x y : A) :=
  forall Q : A -> A -> Prop, Trans  _ Q -> Subset _ R Q -> Q x y.
(* Note the use of _ which is a place holder for an argument 
   to be inferred by the type checker *)

(* Prove that the transitive closure is transitive *)
Lemma trans_transclos : Trans _ Trclos.
Admitted.

(* Prove that the transitive closure contains R *)
Lemma subset_transclos : Subset _ R Trclos. 
Admitted.

(* Prove that the transitive closure is the _smallest_set_ that is transitive and contains R *)
Lemma transclos_smallest : forall Q : A -> A -> Prop, Trans _ Q -> Subset _ R Q -> Subset _ Trclos Q.
Admitted.

(* We define the transitive closure of R inductively *)
Inductive TrclosInd : A -> A -> Prop :=
  sub : forall x y : A, R x y -> TrclosInd x y 
  | trans : forall x y z : A, TrclosInd x y -> TrclosInd y z -> TrclosInd x z. 

(* Prove that TrclosInd ans Trclos are the same *)

Lemma trclos1 : forall x y : A, Trclos x y -> TrclosInd x y.
Admitted.
(* It is convenient to first prove that TrclosInd is transitive and R is a subset of it 
   and then use transclos_smallest !! *)

Lemma help1 : Trans _ TrclosInd.
Admitted.
Lemma help2 : Subset _ R TrclosInd.
Admitted.

Lemma trclos2 : forall x y : A, TrclosInd x y -> Trclos x y.
Admitted.

(* Now also do the following:
- Define the symmetric reflexive closure of R, TrSymclos
- Prove that TrSymclos is symmetric
- Prove that TrSymclos is reflexive
*)

End TrClos.


Section Existential.

Definition exi (A:Set)(P:A->Prop) := forall B:Prop, (forall x:A, P x -> B) -> B.

Variable A:Set.
Variable P: A -> Prop.

(* Prove that the intro and elim rules for the existential hold for exi A P *)
Lemma exi_intro : forall a:A, P a -> exi A P.
Admitted.

Lemma exi_elim : exi A P -> forall C : Prop, (forall x:A, P x -> C) -> C.
Admitted.

(* Prove the equivalence with the inductive exists *)
Lemma ex_implies_exi : (exists x:A, P x) -> exi A P.
Admitted.

Lemma exi_implies_ex : exi A P -> exists x:A, P x.
Admitted.

End Existential.