proposition: Lemma poly_add_compat : forall pl pr var, eval var (poly_add pl pr) = xorb (eval var pl) (eval var pr).
proof: Proof. intros pl; induction pl; intros pr var; simpl. - induction pr; simpl; auto; solve [try_rewrite; ring]. - induction pr; simpl; auto; try solve [try_rewrite; simpl; ring]. destruct (Pos.compare_spec p p0); repeat case_decide; simpl; first [try_rewrite; ring|idtac]. + try_rewrite; ring_simplify; repeat rewrite xorb_assoc. match goal with [ |- context [xorb (andb ?b1 ?b2) (andb ?b1 ?b3)] ] => replace (xorb (andb b1 b2) (andb b1 b3)) with (andb b1 (xorb b2 b3)) by ring end. rewrite <- IHpl2. match goal with [ H : null ?p |- _ ] => rewrite (eval_null_zero _ _ H) end; ring. + simpl; rewrite IHpl1; simpl; ring. Qed.
imports: Bool PArith DecidableClass Ring Lia