Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* 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].
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment