Proving FFs extensionally equal

FF.v

Require Import ZArith.

Local Open Scope Z_scope.

Section FF.

Parameter A : Type.
Parameter (a b c d : A).

Definition FF := Z -> Z -> A.

Definition empty : FF := fun _ _ => a.

Definition i (x y : Z) (v : A) (f : FF) : FF :=
  fun x' y' =>
    if andb (x =? x') (y =? y')
    then v
    else f x' y'.


Definition foo := i 0 0 b (i 0 (-42) c (i 56 1 d empty)).
Definition foo' := i 0 (-42) c (i 56 1 d (i 0 0 b empty)).

Require Import Coq.Logic.FunctionalExtensionality.

Ltac inspect_eq y x :=
  let p := fresh "p" in
  let q := fresh "q" in
  let H := fresh "H" in
  assert (p := proj1 (Z.eqb_eq x y));
  assert (q := proj1 (Z.eqb_neq x y));
  destruct (Z.eqb x y) eqn: H;
  [apply (fun p => p eq_refl) in p; clear q|
   apply (fun p => p eq_refl) in q; clear p].

Ltac fire_i x y := match goal with
  | [ |- context[i ?x' ?y' _ _] ] =>
    unfold i at 1; inspect_eq x x'; inspect_eq y y'; (omega || simpl)
end.

Ltac eqFF :=
  let x := fresh "x" in
  let y := fresh "y" in
  intros;
  apply functional_extensionality; intro x;
  apply functional_extensionality; intro y;
  repeat fire_i x y; reflexivity.

Lemma foo_eq : foo = foo'.
Proof.
unfold foo, foo'; eqFF.
Qed.