(* 
  Autor(s):
    Andrej Dudenhefner (1) 
  Affiliation(s):
    (1) Saarland University, Saarbrücken, Germany
*)

(* 
  Problem:
    Linear Polynomial (over N) Constraint Solvability (LPolyNC_SAT)

  A linear polynomial constraint has one of the following shapes
    x ≐ 1
    x ≐ y + z
    x ≐ X * y (where X is the polynomial indeterminate)

  A polynomial is mechanized by a list of its coefficients.

  LPolyNC_SAT:
    Given a list of constraints,
    is there a valuation φ : nat -> list nat such that
    for each constraint c we have
      if c is x ≐ 1, then φ(x) ≃ 1
      if c is x ≐ y + z, then φ(x) ≃ poly_add (φ(y)) (φ(z))
      if c is x ≐ X * y, then φ(x) ≃ poly_mult 0; 1 (φ(y))
    where ≃ is equality up to trailing zeroes?
*)

Require Import List.
Import ListNotations.

Definition poly : Set := list nat.

(* constraint representation *)
Inductive polyc : Set :=
  | polyc_one : nat -> polyc
  | polyc_sum : nat -> nat -> nat -> polyc
  | polyc_prod : nat -> nat -> polyc.

(* test whether all coefficients are equal, default to 0 *)
Definition poly_eq (p q: poly) : Prop :=
  forall i, nth i p 0 = nth i q 0.

Local Notation "p ≃ q" := (poly_eq p q) (at level 65).

(* polynomial addition *)
Fixpoint poly_add (p q: poly) : poly :=
  match p, q with
  | [], q => q
  | p, [] => p
  | (c :: p), (d :: q) => (c + d) :: poly_add p q
  end.

(* polynomial multiplication *)
Fixpoint poly_mult (p q: poly) : poly :=
  match p with
  | [] => []
  | (c :: p) => poly_add (map (fun a => c * a) q) (0 :: (poly_mult p q))
  end.

Definition polyc_sem (φ: nat -> poly) (c: polyc) :=
  match c with
    | polyc_one x => φ x ≃ [1]
    | polyc_sum x y z => φ x ≃ poly_add (φ y) (φ z)
    | polyc_prod x y => φ x ≃ poly_mult [0; 1] (φ y)
  end.

(* given a list l of constraints, 
  is there a valuation φ satisfying each constraint? *)
Definition LPolyNC_SAT (l : list polyc) := exists φ, forall c, In c l -> polyc_sem φ c.