(* Coq answers to exercises 10 *)

Section Leib.
Variable A:Set.
Definition Lq (x y :A)  := forall P :A -> Prop, P x -> P y.

Lemma LRefl : forall x :A, Lq x x.
intro x.
unfold Lq.
intros P H.
exact H.
Qed.

Print LRefl.

Lemma LTrans : forall x y z:A, Lq x y -> Lq y z -> Lq x z.
intros x y z.
intros H0 H1.
apply H1.
exact H0.
Qed.

Print LTrans.

Lemma LSymm : forall x y :A, Lq x y -> Lq y x.
intros x y.
unfold Lq.
intros H0 P.
apply H0.
intro H; exact H.
Qed.

Print LSymm.

(* Can you create proof scripts that generate
   the other two terms in the answers to exercises10 ? *)


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 Subs := forall x y : A, R x y -> Q x y.
End Rels.

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

Definition Trclos (x y : A) :=
  forall Q : A -> A -> Prop, Trans _ Q -> Subs _ 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.
unfold Trans.
intros x y z Hxy Hyz.
unfold Trclos.
intros Q H1 H2.
unfold Trans in H1.
apply H1 with y.
(* Note that apply H1 doesn't work, because Coq can't infer the
   "missing argument" y; In case there are many choices, Coq will
   never "just choose one" but hand the choice back to the author *)
unfold Trclos in Hxy.
apply Hxy.
unfold Trans.
intros p q r Hpq Hqr.
apply (H1 p q r). 
(* Note that this another way to provide the "missing argument", which
   is q this time: just instantiate H1 with its arguments explicitly *)
assumption. 
assumption.
unfold Subs.
intros a b Hab.
apply H2.
(* Note that I don't _have_ to unfold Subs first; apply H2 does it for me *) 
assumption.
(* the next proof of Q y z is the same as the proof we have done for 
   Q x y before; one caould copy-paste-edit part of the previous script,
   but we will not do that, as we want to show some other tactics  *) 
apply Hyz.
unfold Trans; intros. 
eapply H1.
(* eapply can be used in case you don't want to give the "missing
   argument"; this leaves you with a ? argument *) 
apply H.
(* this instantiates -- via unification -- the ? to y0 
   note: assumption will not do this; there is no such assumption *) 
assumption.
unfold Subs; intros; apply H2; assumption.
Qed.


(* Prove that the transitive closure contains R *)
Lemma Subs_rel_transclos : Subs _ R Trclos. 
unfold Subs; intros.
unfold Trclos; intros.
apply H1.
assumption.
Qed.


(* Prove that the transitive closure is the smallest relation
   that is transitive and contains R: it is contained in every other
   relation that is transitive and contains R *)
Lemma smallest_transclos : forall Q : A -> A -> Prop, Trans _ Q -> Subs _ R Q -> Subs _ Trclos Q. 
Proof.
intros.
unfold Subs.
intros.
unfold Trclos in H1.
apply (H1 Q). (* apply H also works, but then you have to do more work *)
exact H.
exact H0.
Qed.


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.
Variable C:Prop.

Lemma ex_intro : forall a:A, P a -> exi A P.
intros a H.
unfold exi.
intros B H1.
apply H1 with a; assumption.
Qed.

Lemma ex_elim : exi A P -> (forall x:A, P x -> C) -> C.
intros H H1.
(* problem: I would like to do apply H1, but with which element of type A ? *)
unfold exi in H.
apply H.
assumption.
Qed.

End Existential.