# Dependent definition of interval?

**URL:** <https://discourse.rocq-prover.org/t/dependent-definition-of-interval/844>\
**Category:** Using Rocq\
**Created:** [May 18, 2020, 12:35pm UTC](https://discourse.rocq-prover.org/t/dependent-definition-of-interval/844 "2020-05-18T12:35:10Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [May 18, 2020, 12:35pm UTC](https://discourse.rocq-prover.org/t/dependent-definition-of-interval/844/1 "2020-05-18T12:35:10Z")

</div>

Hello,

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

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

```

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

```auto
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:

```auto
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:

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

```

?

Thanks! All suggestions welcome!

Best wishes,  
Nicolás

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [May 18, 2020, 1:08pm UTC](https://discourse.rocq-prover.org/t/dependent-definition-of-interval/844/2 "2020-05-18T13:08:05Z")

</div>

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

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

```

---

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [May 18, 2020, 1:39pm UTC](https://discourse.rocq-prover.org/t/dependent-definition-of-interval/844/3 "2020-05-18T13:39:02Z")

</div>

Brilliant, thanks!

Best wishes,  
Nicolás

---

<div class="post-metadata">

**Author:** ![olaure01](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/olaure01/32/733_2.png) [@olaure01](https://discourse.rocq-prover.org/u/olaure01)\
**Post date:** [May 19, 2020, 10:01am UTC](https://discourse.rocq-prover.org/t/dependent-definition-of-interval/844/4 "2020-05-19T10:01:48Z")

</div>

> [@nojb](#):
>
> Or maybe there a reformulation of the definition without this problem?

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

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

```

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