Deduplicate size constraints

[ionathanch]

A lot of size constraints are duplicated because they're no longer stored in a set. For instance, the following program:

Inductive Eq (A : Type) (x : A) : A -> Type :=
| eq_refl : Eq A x x.

Inductive N : Type :=
| O : N
| S : forall (n : N) (n_eq_n : Eq N n n), N.

Definition sr_c_ex : N :=
  match (S O (eq_refl N O)) return N with
  | O          => O
  | S n n_eq_n => ((fun (_ : _) (n : N) => n)
                    (eq_refl (Eq N n n)
                             n_eq_n)
                    O)
  end.

produces for the body of sr_c_ex the following constraints:

{s8⊑s19, s19⊑s8, ∞⊑s10, s9⊑s19, s19⊑s9, s18⊑s6, s7+1⊑s6, s5⊑s19+1, s4⊑s19,
s14+1⊑s18, s13+1⊑s17, s12⊑s16, s16⊑s12, s11⊑s15, s15⊑s11, s10⊑s16, s9⊑s15,
s15⊑s9, s10⊑s16, s9⊑s15, s15⊑s9, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s10⊑s12, s9⊑s11, s11⊑s9, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4,
s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s11, s8⊑s11,
s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s10⊑s12, s9⊑s11, s11⊑s9,
s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s11, s8⊑s11, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s8⊑s15, s8⊑s15, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s10⊑s12, s9⊑s11, s11⊑s9,
s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s11, s8⊑s11, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s10⊑s12, s9⊑s11, s11⊑s9, s8⊑s9, s8⊑s9, s1⊑s4,
s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s8⊑s11, s8⊑s11, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9,
s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s10⊑s12, s9⊑s11, s11⊑s9, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1, s8⊑s11, s8⊑s11, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4,
s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4,
s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s8⊑s9, s8⊑s9, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1,
s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4, s2+1⊑s1, s1⊑s4, s4⊑s1, s0+1⊑s4,
s2+1⊑s1}

but when sorted and deduplicated, there are only the following constraints left:

{s0+1⊑s4, "∞"⊑s10, s10⊑s12, s10⊑s16, s11⊑s15, s11⊑s9, s12⊑s16, s13+1⊑s17, s14+1⊑s18,
s15⊑s11, s15⊑s9, s16⊑s12, s18⊑s6, s19⊑s8, s19⊑s9, s1⊑s4, s2+1⊑s1, s4⊑s1, s4⊑s19,
s5⊑s19+1, s7+1⊑s6, s8⊑s11, s8⊑s15, s8⊑s19, s8⊑s9, s9⊑s11, s9⊑s15, s9⊑s19}

There should be some way to find a good tradeoff between time usage (set operations) and space usage (duplicated constraints).