# Unable to understand the 'total\_relation' question

**URL:** <https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [July 2, 2024, 2:11pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363 "2024-07-02T14:11:04Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![EmilyPriyadarshini](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/emilypriyadarshini/32/988_2.png) [@EmilyPriyadarshini](https://discourse.rocq-prover.org/u/EmilyPriyadarshini)\
**Post date:** [July 2, 2024, 2:11pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/1 "2024-07-02T14:11:04Z")

</div>

Hi there!

I am currently solving the following question in the IndProp chapter in Logical Foundations:

```auto
Define an inductive binary relation total_relation that holds between every pair of natural numbers.
Inductive total_relation : nat → nat → Prop :=
  (* FILL IN HERE *)
.

```

I don’t understand what we have to do. Do we have to define a specific total relation? And so, there would be multiple answers to this, won’t there?

I’d really appreciate any insight. Thanks!

---

<div class="post-metadata">

**Author:** ![JoJoDeveloping](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jojodeveloping/32/886_2.png) [@JoJoDeveloping](https://discourse.rocq-prover.org/u/JoJoDeveloping)\
**Post date:** [July 2, 2024, 2:22pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/2 "2024-07-02T14:22:21Z")

</div>

How would two total relations be different?

---

<div class="post-metadata">

**Author:** ![EmilyPriyadarshini](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/emilypriyadarshini/32/988_2.png) [@EmilyPriyadarshini](https://discourse.rocq-prover.org/u/EmilyPriyadarshini)\
**Post date:** [July 2, 2024, 2:33pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/3 "2024-07-02T14:33:31Z")

</div>

What I was thinking was that ‘total relations’ are those that hold between every pair of natural numbers. So, if we have `n m : nat`, then one way I could define `total_relation` would be that either `n=m or n<m or n>m`. I don’t know if I am grasping the concept correctly, and how I would define what I am talking about.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [July 2, 2024, 7:48pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/5 "2024-07-02T19:48:21Z")

</div>

If “total” means “true for any pair of arguments” then `<`, “=” and ‘\<’ have easy counter-examples: (1,0), (1,0) and (0,1). Try again 🙂

---

<div class="post-metadata">

**Author:** ![EmilyPriyadarshini](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/emilypriyadarshini/32/988_2.png) [@EmilyPriyadarshini](https://discourse.rocq-prover.org/u/EmilyPriyadarshini)\
**Post date:** [July 2, 2024, 8:02pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/6 "2024-07-02T20:02:39Z")

</div>

Sorry, I couldn’t get you. What I was thinking was if we have for example (0,1), then we have that 0\<1. So, for any (n,m), either n\<m, n=m, or n\>m.

I think I am misunderstanding what is meant by total relations.

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [July 3, 2024, 6:31am UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/7 "2024-07-03T06:31:44Z")

</div>

@EmilyPriyadarshini You’re right, that is a valid definition of a total relation. `total_relation := fun n m => n < m \/ n = m \/ n > m`.

There are multiple valid solutions to that exercise, but they are all logically equivalent: `forall n m. total_relation_1 n m <-> total_relation_2 n m` would be a theorem.

---

<div class="post-metadata">

**Author:** ![EmilyPriyadarshini](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/emilypriyadarshini/32/988_2.png) [@EmilyPriyadarshini](https://discourse.rocq-prover.org/u/EmilyPriyadarshini)\
**Post date:** [July 3, 2024, 12:04pm UTC](https://discourse.rocq-prover.org/t/unable-to-understand-the-total-relation-question/2363/8 "2024-07-03T12:04:18Z")

</div>

@Lyxia Thank you so much for your reply! It’s much clearer to me now!