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