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

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?

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.

@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.