Hello,

I am reading the book: Volume 1: Logical Foundations

(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!