Inductive predicate_polynomial : Set :=
  | Pred : (nat -> bool) -> predicate_polynomial
  | PredVar : nat -> predicate_polynomial
  | PredInter : predicate_polynomial -> predicate_polynomial -> predicate_polynomial
  | PredSymdiff : predicate_polynomial -> predicate_polynomial -> predicate_polynomial
  | PredBot : predicate_polynomial
  | PredTop : predicate_polynomial
.

Inductive pred_poly_eq : predicate_polynomial -> predicate_polynomial -> Prop :=
  | pred_poly_refl : forall (p : predicate_polynomial), pred_poly_eq p p
  | pred_poly_sym : forall p q, pred_poly_eq p q -> pred_poly_eq q p
  | pred_poly_trans : forall p q r, pred_poly_eq p q -> pred_poly_eq q r -> pred_poly_eq p r

  | pred_poly_inter_morph : forall p p', pred_poly_eq p p' ->
    forall q q', pred_poly_eq q q' -> pred_poly_eq (PredInter p q) (PredInter p' q')
  | pred_poly_sym_morph : forall p p', pred_poly_eq p p' ->
    forall q q', pred_poly_eq q q' -> pred_poly_eq (PredSymdiff p q) (PredSymdiff p' q')

  | pred_poly_inter_comm : forall p q, pred_poly_eq (PredInter p q) (PredInter q p)
  | pred_poly_inter_assoc : forall p q r,
    pred_poly_eq (PredInter p (PredInter q r)) (PredInter (PredInter p q) r)
  | pred_poly_inter_unit : forall p, pred_poly_eq (PredInter PredTop p) p
  | pred_poly_iter_idem : forall p, pred_poly_eq (PredInter p p) p

  | pred_poly_sym_comm : forall p q, pred_poly_eq (PredSymdiff p q) (PredSymdiff q p)
  | pred_poly_sym_assoc : forall p q r,
    pred_poly_eq (PredSymdiff p (PredSymdiff q r)) (PredSymdiff (PredSymdiff p q) r)
  | pred_poly_sym_unit : forall p, pred_poly_eq (PredSymdiff PredBot p) p
  | pred_poly_sym_nil : forall p, pred_poly_eq (PredSymdiff p p) PredBot

  | pred_poly_left_distr : forall p q r,
    pred_poly_eq (PredInter (PredSymdiff p q) r) (PredSymdiff (PredInter p r) (PredInter q r))
.

Fixpoint interp (p : predicate_polynomial) (x : nat) : bool :=
  match p with
  | Pred f => f x
  | PredVar _ => false (* todo variable substitution *)
  | PredInter p1 p2 => (interp p1 x) && (interp p2 x)
  | PredSymdiff p1 p2 => xorb (interp p1 x) (interp p2 x)
  | PredBot => false
  | PredTop => true
  end.

Theorem interp_respects : forall p1 p2 x, pred_poly_eq p1 p2 -> interp p1 x = interp p2 x.
Proof.
  intros p1 p2 x H.
  induction H; cbn [interp].
  - eauto.
  - eauto.
  - transitivity (interp q x); eauto.
  - rewrite IHpred_poly_eq1, IHpred_poly_eq2; eauto.
  - rewrite IHpred_poly_eq1, IHpred_poly_eq2; eauto.
  - destruct (interp p x), (interp q x); eauto.
  - destruct (interp p x), (interp q x); eauto.
  - destruct (interp p x); eauto.
  - destruct (interp p x); eauto.
  - destruct (interp p x), (interp q x); eauto.
  - destruct (interp p x), (interp q x), (interp r x); eauto.
  - destruct (interp p x); eauto.
  - destruct (interp p x); eauto.
  - destruct (interp p x), (interp q x), (interp r x); eauto.
Qed.

Lemma silly : (forall a, Nat.eqb a a = true).
Proof.
  intros a; induction a; cbn [Nat.eqb]; eauto.
Qed.

Theorem thm1: forall x,
  pred_poly_eq (Pred (Nat.eqb x)) PredBot -> False.
Proof.
  intros.
  assert (interp (Pred (Nat.eqb x)) x = interp PredBot x) as H0.
  - apply interp_respects; eauto.
  - cbv [interp] in H0.
    assert (Nat.eqb x x = true) by apply silly.
    congruence.
Qed.