make_diff.v

(* https://stackoverflow.com/questions/44612214/how-to-deal-with-really-large-terms-generated-by-program-fixpoint-in-coq *)

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Relations.Relations.
Require Import Coq.Program.Program.

Definition is_decidable (A : Type) (R : relation A) := forall x y, {R x y} + {~(R x y)}.
Definition eq_decidable (A : Type) := forall (x y : A), { x = y } + { ~ (x = y) }.

Inductive diff (X: Type) : Type :=
  | add : X -> diff X
  | remove : X -> diff X 
  | update : X -> X -> diff X.

Section make_diff.

Variable A : Type.
Variable R : relation A.
Variable dec : is_decidable A R.
Variable eq_dec : eq_decidable A.
Variable trans : transitive A R.
Variable lt_neq : forall x y, R x y -> x <> y.
  
Fixpoint make_diff (l1 : list A) : list A -> list (diff A) :=
  match l1 with
  | nil =>
    fix make_diff2 l2 :=
      match l2 with
      | nil => nil
      | new_h::new_t => (add A new_h) :: make_diff2 new_t
      end
  | old_h::old_t =>
    fix make_diff2 l2 :=
      match l2 with
      | nil => (remove A old_h) :: make_diff old_t nil
      | new_h::new_t =>
        if dec old_h new_h 
        then (remove A old_h) :: make_diff old_t l2
        else if eq_dec old_h new_h 
             then (update A old_h new_h) :: make_diff old_t new_t
             else (add A new_h) :: make_diff2 new_t
      end
  end.
End make_diff.

Arguments make_diff [A R] _ _ _ _.

Require Import Coq.Arith.Arith.
Compute make_diff lt_dec Nat.eq_dec [1;2;3] [4;5;6].