Make Expr comparable

[awalterschulze]

Here are some starting points

Fixpoint compare_info (x y: Info) {struct x} :=
  match x with
  | mkInfo xname xparams _ xhash =>
    match y with
    | mkInfo yname yparams _ yhash =>
      match Nat.compare xhash yhash with
      | Lt => Lt
      | Gt => Gt
      | Eq =>
        match Nat.compare xname yname with
        | Lt => Lt
        | Gt => Gt
        | Eq => ((fix compare_params (xs ys: list Info) {struct xs} :=
        (match xs with
         | [] =>
           match ys with
           | [] => Eq
           | _ => Lt
           end
         | (x'::xs') =>
           match ys with
           | [] => Gt
           | (y'::ys') =>
             match compare_info x' y' with
             | Lt => Lt
             | Gt => Gt
             | Eq => compare_params xs' ys'
             end
           end
         end)) xparams yparams)
        end
      end
    end
  end
.

Definition compare_rexpr {A: Set} {B: Set} (x y: RExpr B): comparison :=
  compare_info (@get_info A B x) (@get_info A B y).

Fixpoint compare_info (x y: Info) {struct x}: comparison :=
  match x with
  | mkInfo xname xparams _ xhash =>
    match y with
    | mkInfo yname yparams _ yhash =>
      match compare xhash yhash with
      | Lt => Lt
      | Gt => Gt
      | Eq =>
        match compare xname yname with
        | Lt => Lt
        | Gt => Gt
        | Eq => ((fix compare_params (xs ys: list Info) {struct xs} :=
        (match xs with
         | [] =>
           match ys with
           | [] => Eq
           | _ => Lt
           end
         | (x'::xs') =>
           match ys with
           | [] => Gt
           | (y'::ys') =>
             match compare_info x' y' with
             | Lt => Lt
             | Gt => Gt
             | Eq => compare_params xs' ys'
             end
           end
         end)) xparams yparams)
        end
      end
    end
  end
.

Definition compare_smart_info (xsmart ysmart: SmartInfo): comparison :=
  match xsmart with
  | mkSmart xinfo x_is_smart =>
    match ysmart with
    | mkSmart yinfo y_is_smart =>
      compare_info xinfo yinfo
    end
  end.

[awalterschulze]

Started by adding Cmp instances for Func and SmartFunc, still have proofs left, see TODOs in https://github.com/katydid/proofs/pull/24

[awalterschulze]

Next you will probably need https://github.com/katydid/proofs/issues/25 to complete the proofs

[awalterschulze]

These proofs are no longer in Coq, so this issue is not relevant anymore.