Inductive relations

Using Coq
1

Hello,
I am reading the book: Volume 1: Logical Foundations
(https://softwarefoundations.cis.upenn.edu/lf-current/index.html)
Chapter IndProp
Inductively Defined Propositions

I am not able to understand how to solve next 2 tasks:

Exercise: 2 stars, standard, optional (total_relation) :
Define an inductive binary relation total_relation
that holds between every pair of natural numbers.

Exercise: 2 stars, standard, optional (empty_relation)
Define an inductive binary relation empty_relation (on numbers) that never holds.

I don’t understand the logic. I tried to solve somehow… please see the bottom of attached screenshot.

Please give me a hint if you can.

Is that correct that “total relation” is “less than” relation?
There are a lot of total relations on natural numbers, right? For example “more than” is also a total relation, right?
Is one constructor enough?
I destruct m. Is it enough? Or n should be considered too?

Is that correct that empty_relation can throw away parameters in constructor and return just couple of arbitrary numbers? Or maybe constructor here should not have parameters at all?

Thank you!

Exercises_at_the_bottom_of_the_page
Exercises_at_the_bottom_of_the_page1920Ă—1080 282 KB

2

I found this solution in internet. Is it correct? It tells nothing about parameters… what is the point ?
How can it be used on practice?

Inductive total_relation : nat -> nat -> Prop :=
  tot_rel : forall (n m:nat), total_relation n m.

Inductive empty_relation : nat -> nat -> Prop :=
  empt_rel : empty_relation 0 0.
3

The point is just to make you consider extreme case of binary relations. In practice, you will virtually never use the total and empty binary relation.

The total binary relation is a relation that holds between any two natural number, so yes, the solution you found is correct.

On the other hand, the empty binary relation is a relation that never holds between any two natural number, so no, the solution you found for this is not correct. Indeed, this relation holds between 0 and 0.

Hint: think about how the empty proposition False is defined.

1 Like
4

Thank you.

Empty binary relation between any two natural numbers
(there is no constructor, because there is no instance …):

 Inductive empty_relation : nat -> nat -> Prop := .

Similarly contradictory proposition False is defined in the standard library.

Shall I delete this topic? It contains answer to the exercise from the book, and they asked not to post answers…

5

I’d rather avoid deleting topics unless it is spam or it exposes private information. If you want, you can edit your own messages to remove the solutions. I tried to answer you in a way that gives the requested hint without blatantly giving the solution.

1 Like