Library HOL_Indtypes

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.
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:
  • 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.
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.