Unable to understand the 'total_relation' question

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 :slight_smile:

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.

1 Like

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