bedrock.prelude.compare

(*
 * Copyright (C) BedRock Systems Inc. 2024
 *
 * This software is distributed under the terms of the BedRock Open-Source License.
 * See the LICENSE-BedRock file in the repository root for details.
 *)

Require Import bedrock.prelude.base.
Require Import bedrock.prelude.numbers.

Generic comparison

Inspired by:
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP 2023.
Section compare.
  #[local] Open Scope positive.
  Import EqNotations.

Compare constructors represented as tags and data.
  Definition compare_ctor {A : Type}
      
constructor numbers (#[only(tag)] derive)
      (tag : A -> positive)
      
constructor data (#[only(fields)] derive)
      (car : positive -> Type) (data : ∀ a, car (tag a))
      (compare : ∀ p, car p -> car p -> comparison)
data comparison
      (t : positive) (d : unit -> car t) (* deconstructed inhabitant of <<A>> *)
      (a : A) : comparison :=
    let ta := tag a in
    let c := Pos.compare ta t in
    match c as c' return c = c' -> comparison with
    | Eq => fun EQ => compare t (d ()) $ rew (Pos.compare_eq _ _ EQ) in data a
    | Lt => fun _ => Gt
    | Gt => fun _ => Lt
    end eq_refl.

Compare tags (for trivial constructors)
  Definition compare_tag {A : Type}
      (tag : A -> positive)
      (t : positive)
      (a : A) : comparison :=
    Pos.compare t (tag a).

End compare.

Definition compare_lex (a : comparison) (b : unit -> comparison) : comparison :=
  match a with
  | Eq => b ()
  | Lt | Gt => a
  end.