(** * Higher Order Logic and its relation to Inductive Types *)


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

(** Now prove reflexivity, transitivity and symmetry *)
Lemma LRefl : forall x : A, Lq x x.
Proof.
Admitted.

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

Lemma LSymm : forall x y : A, Lq x y -> Lq y x.
Proof.
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.
Proof.
Admitted.

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

End Leib.


Section Rels.
(** Basics about relations *)
Variable D : Set.
Variable R : D -> D -> Prop.
Variable Q : D -> D -> Prop.
Definition Transitive := forall x y z : D, R x y -> R y z -> R x z. 
Definition Symmetric := forall x y : D, R x y -> R y x. 
Definition Subrel := forall x y : D, R x y -> Q x y.
(** Please type [Check Trans.] *)
End Rels.

(** Please type again [Check Trans.] #<br>#
    By closing the Section [Rels], Rocq has abstracted over 
    the relevant variables that were declared at the start of 
    the Section. *)

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

(** We define the transitive closure of R using higher order logic *)
Definition Trclos (x y : D) :=
  forall Q : D -> D -> Prop, Transitive _ Q -> Subrel _ R Q -> Q x y.
(** Note the use of [_] which is a place holder, a "hole", for an argument 
   to be inferred by the type checker. Note that the type checker can infer 
   from the type of [Q] that [D] should be filled in here *)

(** You can also introduce notation to avoid having to write the [_] *) 
Notation Trans := (Transitive _).
Notation Symm := (Symmetric _) .
Notation Subr := (Subrel _).

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

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

(** Prove that the transitive closure is the smallest set that is transitive and contains [R] *)
Lemma transclos_smallest : forall Q : D -> D -> Prop, Trans Q -> Subr R Q -> Subr Trclos Q.
Proof.
Admitted.

(** We define the transitive closure of [R] inductively *)

Inductive TrclosInd : D -> D -> Prop :=
  sub : forall x y : D, R x y -> TrclosInd x y 
  | tra : forall x y z : D, TrclosInd x y -> TrclosInd y z -> TrclosInd x z. 

(** Prove that [TrclosInd] and [Trclos] are the same *)

Lemma trclos1 : forall x y : D, Trclos x y -> TrclosInd x y.
Proof.
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.
Proof.
Admitted.

Lemma help2 : Subr R TrclosInd.
Proof.
Admitted.

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

(** Now also do the following: #<br>#
- Define the symmetric reflexive closure of [R], [TrSymclos] #<br>#
- Prove that [TrSymclos] is symmetric #<br>#
- Prove that [TrSymclos] is reflexive #<br>#
*)

End TrClos.


Section Existential.
(** The higher order definition of the existential quantifier *)
Definition exi (D:Set)(P:D->Prop) := forall B:Prop, (forall x:D, P x -> B) -> B.

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

(* Prove that the introduction and elimination rules for the existential hold for [exi A P] *)
Lemma exi_intro : forall a:D, P a -> exi D P.
Proof.
Admitted.

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

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

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

End Existential.

(** Some definitions relating to sets and subsets *)
Section Subsets.
Variable D:Set.
Variable A B : D -> Prop.
Definition Subset := forall x y : D, A x -> B x.
End Subsets.
Notation Subs := (Subset _).

(** Unions and intersections of subsets *)
Section caps_and_cups.
Variable D:Set.

(** Intersection *)
Definition cap (A B: D -> Prop) := 
fun x: D => forall P : D -> Prop, (forall y : D, A y -> B y -> P y) -> P x.

(** Union *)
Definition cup (A B: D -> Prop) := 
fun x: D => forall P : D -> Prop, Subs A P -> Subs B P -> P x.

(** Higher order definition of disjunction *)
Definition OR (X Y :Prop) := forall Z :Prop, (X -> Z)  -> (Y -> Z) -> Z.

Lemma subcup (A B : D-> Prop) : Subs A (cup A B).
Proof.
Admitted. 

Lemma capsub (A B : D-> Prop) : Subs (cap A B) A.
Proof.
Admitted. 

Lemma subcap (A B : D-> Prop) : forall x :D, A x -> B x -> cap A B x.
Proof.
Admitted. 

Lemma cupsub (A B : D-> Prop) : forall x :D, cup A B x -> OR (A x) (B x).
Proof.
Admitted. 

End caps_and_cups.