(* 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.
Proof.
intros.
unfold Lq in H.
apply H.
apply LRefl.
Qed.
Print LSymm.
(* Note that, given x, y : A, H : Lq x y Coq has taken
P := fun y0 : A => Lq y0 x for the predicate
so H P yields the proof of Lq y x in soem simple steps *)
(* 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.
Proof.
unfold Trans; intros.
unfold Trclos.
intros.
unfold Trclos in H.
unfold Trclos in H0.
unfold Trans in H1.
apply (H1 x y z).
(* or: apply H1 with y. *)
apply H; try assumption.
apply H0; try assumption.
Qed.
(* 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.
Proof.
intros.
unfold Subset.
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.
(* 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 *)
(* First the suggested helper lemma's *)
Lemma help1 : Trans _ TrclosInd.
Proof.
unfold Trans.
(* NB you can do exact right away; don't need to unfold
NB apply trans. doesn't work as the unification attempts to
match the whole goal with the _end_ of the type of trans
The you would have to do intros. apply trans. *)
exact trans.
Qed.
Lemma help2 : Subset _ R TrclosInd.
Proof.
unfold Trans.
exact sub.
Qed.
Lemma trclos1 : forall x y : A, Trclos x y -> TrclosInd x y.
Proof.
intros x y H.
apply transclos_smallest.
- exact help1.
- exact help2.
- auto.
Qed.
(* It is convenient to first prove that TrclosInd is transitive and R is a subset of it
and then use transclos_smallest !! *)
Lemma trclos2 : forall x y : A, TrclosInd x y -> Trclos x y.
Proof.
intros x y H.
induction H.
- unfold Trclos.
intuition.
- eapply trans_transclos.
(* NB apply trans_transclos with y. will also work
this is to show you that Coq can also work with "existential variables",
variables of some domain that are left open and can be filled in later,
for example when we know better what to chooes *)
+ apply IHTrclosInd1.
+ auto.
Qed.
(* 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.
Proof.
intros.
apply H.
exact H0.
Qed.
(* Prove the equivalence with the inductive exists *)
Lemma ex_implies_exi : (exists x:A, P x) -> exi A P.
Proof.
intro H.
elim H.
exact exi_intro.
Qed.
Lemma exi_implies_ex : exi A P -> exists x:A, P x.
Proof.
intro H.
apply H.
intros.
exists x.
auto.
Qed.
End Existential.