Hi there!
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?
I’d really appreciate any insight. Thanks!
How would two total relations be different?
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.
If “total” means “true for any pair of arguments” then <, “=” and ‘<’ have easy counter-examples: (1,0), (1,0) and (0,1). Try again 
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.
@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.
@Lyxia Thank you so much for your reply! It’s much clearer to me now!