# Inductive relations

**URL:** <https://discourse.rocq-prover.org/t/inductive-relations/514>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [December 3, 2019, 8:00am UTC](https://discourse.rocq-prover.org/t/inductive-relations/514 "2019-12-03T08:00:26Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [December 3, 2019, 8:00am UTC](https://discourse.rocq-prover.org/t/inductive-relations/514/1 "2019-12-03T08:00:26Z")

</div>

Hello,  
I am reading the book: Volume 1: Logical Foundations  
([https://softwarefoundations.cis.upenn.edu/lf-current/index.html](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](https://us1.discourse-cdn.com/flex001/uploads/coq/original/1X/3bc14bf960c7d428e3c721407fce2e43f4fba470.png)

---

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [December 3, 2019, 9:23am UTC](https://discourse.rocq-prover.org/t/inductive-relations/514/2 "2019-12-03T09:23:19Z")

</div>

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?

```coq
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.

```

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [December 3, 2019, 12:49pm UTC](https://discourse.rocq-prover.org/t/inductive-relations/514/3 "2019-12-03T12:49:28Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [December 4, 2019, 6:44am UTC](https://discourse.rocq-prover.org/t/inductive-relations/514/4 "2019-12-04T06:44:47Z")

</div>

Thank you.

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

```coq
 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…

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [December 6, 2019, 2:06pm UTC](https://discourse.rocq-prover.org/t/inductive-relations/514/5 "2019-12-06T14:06:27Z")

</div>

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.