Module BooleanSemanticTable

Require Import Coqlib.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import BooleanDecomposition.
Require Import BinRec.
Opaque Z.mul.

Definitions

Definition T (xb yb: bool) (f: Z -> Z -> Z) : Z -> Z -> Z :=
  fun (x y: Z) => f (2*x + Z.b2z xb) (2*y + Z.b2z yb) - 2 * (f x y).

Definition isConstant (f: Z -> Z -> Z) : Prop :=
  forall (x y: Z), f x y = f 0 0.

Definition isLocal (f: Z -> Z -> Z) : Prop :=
  forall (b1 b2: bool), isConstant (T b1 b2 f).

Definition BST (T: Type) := bool -> bool -> T.
Definition TT := BST bool.

Definition BST_of_local (f: Z -> Z -> Z) : BST Z :=
  fun xb yb => (T xb yb f 0 0).

Definition BST_binop {A B C: Type} (op: A -> B -> C)
           (bst1: BST A) (bst2: BST B) : BST C :=
  fun xb yb => op (bst1 xb yb) (bst2 xb yb).

Definition BST_unop {A B: Type} (op: A -> B) (bst: BST A) :=
  fun xb yb => op (bst xb yb).

Definition BST_add := BST_binop Z.add.
Definition BST_mul (k: Z) := BST_unop (fun x => k * x).

Definition TT_and := BST_binop andb.
Definition TT_or := BST_binop orb.
Definition TT_xor := BST_binop xorb.
Definition TT_not := BST_unop negb.

Examples

Example example_constant: isConstant (fun (x y: Z) => 4).

Proof.

  unfold isConstant.
  intros.
  auto.
Qed.

Example example_local: isLocal Z.land.

Proof.

  unfold isLocal.
  unfold isConstant.
  unfold T.
  destruct b1; destruct b2;
    intros; bool_decomp;
      omega.
Qed.

Example example_same_BST:
BST_of_local Z.add = BST_of_local (fun x y => Z.add (Z.lxor x y) (2 * Z.land x y)).

Proof.

  apply functional_extensionality.
  intros x.
  apply functional_extensionality.
  intros y.
  destruct x; destruct y; reflexivity.
Qed.

T is linear:

Lemma T_additivity : forall (xb yb: bool) (f g: Z -> Z -> Z) (x y: Z),
T xb yb (fun x' y' => f x' y' + g x' y') x y = T xb yb f x y + T xb yb g x y.

Proof.

  intros.
  unfold T.
  omega.
Qed.

Lemma T_homogeneity : forall (xb yb: bool) (f: Z -> Z -> Z) (k: Z) (x y: Z),
T xb yb (fun x' y' => k * (f x' y')) x y = k * T xb yb f x y.

Proof.

  intros.
  unfold T.
  rewrite Z.mul_shuffle3.
  rewrite <- Z.mul_sub_distr_l.
  omega.
Qed.

BST_of_local is linear:

Theorem BST_of_local_additivity : forall (f g: Z -> Z -> Z),
BST_of_local (fun x y => f x y + g x y) =
BST_add (BST_of_local f) (BST_of_local g).

Proof.

  intros.
  unfold BST_of_local.
  unfold BST_add.
  unfold BST_binop.
  apply functional_extensionality.
  intros x.
  apply functional_extensionality.
  intros y.
  rewrite !T_additivity.
  reflexivity.
Qed.

Theorem BST_of_local_homogeneity : forall (f g: Z -> Z -> Z) (k: Z),
BST_of_local (fun x y => k * (f x y)) =
BST_mul k (BST_of_local f).

Proof.

  intros.
  unfold BST_of_local.
  unfold BST_mul.
  unfold BST_unop.
  apply functional_extensionality.
  intros x.
  apply functional_extensionality.
  intros y.
  rewrite !T_homogeneity.
  reflexivity.
Qed.

BST_of_local is injective

Theorem BST_of_local_injective : forall (f g: Z -> Z -> Z),
    isLocal f -> isLocal g ->
    BST_of_local f = BST_of_local g ->
    f = g.

Proof.

  intros f g.
  intros HLf HLg.
  intros HBST.
  assert(HBST': forall xb yb, BST_of_local f xb yb = BST_of_local g xb yb).
  { intros.
    rewrite HBST.
    reflexivity.
  }
  unfold isLocal in HLf, HLg.
  unfold isConstant in HLf, HLg.
  unfold BST_of_local in HBST'.
  unfold T in *.
  rewrite Z.mul_0_r in *.
  simpl in *.

  apply functional_extensionality.
  intros x.
  apply functional_extensionality.
  generalize dependent x.
  apply binrecZZ_short.
  - intros xb yb.
    specialize (HBST' xb yb).
    specialize (HLf xb yb (-Z.b2z xb) (-Z.b2z yb)).
    specialize (HLg xb yb (-Z.b2z xb) (-Z.b2z yb)).
    destruct xb; destruct yb; simpl in *;
    replace (2 * -1 + 1) with (-1) in * by omega;
    replace (2 * 0 + 0) with (0) in * by omega;
    omega.
  - intros xb yb x y H.
    specialize (HBST' xb yb).
    specialize (HLf xb yb x y).
    specialize (HLg xb yb x y).
    destruct xb; destruct yb; simpl in *;
    omega.
Qed.