Library HOL_Indtypes_answers

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.
intros x y H.
unfold Lq in H.
apply H.
apply LRefl.
Qed.
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. Note that, given x, y : A, H : Lq x y Rocq has taken P := fun y0 : A => Lq y0 x for the predicate so H P yields the proof of Lq y x in a few simple steps

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.
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.
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 : 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.
intros.
unfold Subr.
intros.
unfold Trclos in H1.
apply (H1 Q).
apply H1 also works
* exact H.
* exact H0.
Qed.

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 help1 : Trans TrclosInd.
Proof.
unfold Trans.
You can also do exact tra. right away; don't need to unfold
NB apply tra. doesn't work as the unification attempts to match the whole goal with the end of the type of tra. You would have to do intros. apply tra.
exact tra.
Qed.

Lemma help2 : Subr R TrclosInd.
Proof.
unfold Trans.
exact sub.
Qed.

Lemma trclos1 : forall x y : D, Trclos x y -> TrclosInd x y.
Proof.
intros x y H.
apply transclos_smallest.
- exact help1.
- exact help2.
- auto.
Qed.

Lemma trclos2 : forall x y : D, TrclosInd x y -> Trclos x y.
Proof.
intros x y H.
induction H.
- unfold Trclos.
  intuition.
Combines R x y and Subr R Q to get Q x y automatically
- eapply trans_transclos.
NB apply trans_transclos with y. will also work this is to show you that Rocq 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.
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.

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.
intros.
apply H.
exact H0.
Qed.

Prove the equivalence with the inductive exists
Lemma ex_implies_exi : (exists x:D, P x) -> exi D P.
Proof.
intro H.
elim H.
exact exi_intro.
Qed.

Lemma exi_implies_ex : exi D P -> exists x:D, P x.
Proof.
intro H.
apply H.
intros.
exists x.
auto.
Qed.

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.
intros x H.
unfold cup in H.
apply (H (fun x : D => OR (A x) (B x))).
- unfold Subs.
  intros x0 d Hx0.
  unfold OR.
  intros Z H1 H2. apply H1; auto.
- unfold Subs.
  intros x0 d Hx0.
  unfold OR.
  intros Z H1 H2. apply H2; auto.
Qed.
End caps_and_cups.