Dependent definition of interval?

Using Coq
1

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

2

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

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

Brilliant, thanks!

Best wishes,
Nicolás

4

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