 # Dependent definition of interval?

Hello,

I am trying to define a datatype for intervals of natural numbers: either a “proper” interval or the empty interval: something like

``````Inductive t :=
| Range: forall d1 d2, d1 <= d2 -> t
| Empty: t.
``````

Then I define the “merge” function (the smallest interval containing two intervals) by:

``````Definition merge (a1 a2 : t) :=
match a1, a2 with
| Empty, _ -> a2
| _, Empty -> a1
| Range l1 r1 H1, Range l2 r2 H2 -> Range (min l1 l2) (max r1 r2) _
end
``````

and the `In` predicate:

``````Definition In (d : nat) (a : t) : Prop :=
match a with
| Empty => False
| Range l r _ => l <= d /\ d <= r
end.
``````

However the fact that the proof of the inequality is carried around makes Leibniz equality for `t` pretty much useless. Is there a way to make the proof in the `Range` constructor somehow irrelevant so that Leibniz equality can be used (ideally without assuming any extra axioms)? Or maybe there a reformulation of the definition without this problem?

Otherwise, how “bad” would it be if I were to add the following axiom to my development:

``````Axiom t_eq: forall l r H1 H2, Range l r H1 = Range l r H2.
``````

?

Thanks! All suggestions welcome!

Best wishes,
Nicolás

This is actually provable. A consequence of `le_unique` which is proved in the standard library:

``````Require Import Arith.
(* le_unique : forall (m n : nat) (le_mn1 le_mn2 : m <= n), le_mn1 = le_mn2 *)
``````
1 Like

Brilliant, thanks!

Best wishes,
Nicolás

When it is possible, I would indeed recommend to use a definition which “encapsulates” properties rather than stating them:

``````Inductive t :=
| Range: nat -> nat -> t
| Empty: t.
``````

where `Range d w` is meant to represent the interval [d, d+w].

1 Like