Require Import List.
Import ListNotations.

Definition poly : Set := list nat.

Inductive polyc : Set :=
  | polyc_one : nat -> polyc
  | polyc_sum : nat -> nat -> nat -> polyc
  | polyc_prod : nat -> nat -> polyc.

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).

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.

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.

Definition LPolyNC_SAT (l : list polyc) := exists φ, forall c, In c l -> polyc_sem φ c.