proposition: Lemma reduce_aux_eval_compat : forall k p var, valid (Pos.succ k) p -> (list_nth k var false && eval var (reduce_aux k p) = list_nth k var false && eval var p).
proof: Proof. intros k p var; revert k; induction p; intros k Hv; simpl; auto. inversion Hv; case_decide; subst. + rewrite poly_add_compat; ring_simplify. specialize (IHp1 k); specialize (IHp2 k). destruct (list_nth k var false); ring_simplify; [|now auto]. rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p3)). rewrite <- IHp2; auto; rewrite <- IHp1; [ring|]. apply (valid_le_compat k); [now auto|lia]. + remember (list_nth k var false) as b; destruct b; ring_simplify; [|now auto]. case_decide; simpl. - rewrite <- (IHp2 p2); [inversion H|now auto]; simpl. replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k). { rewrite <- Heqb; ring. } { apply (valid_le_compat p2); [auto|lia]. } - rewrite (IHp2 p2); [|now auto]. replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring). rewrite <- (IHp1 k); [rewrite <- Heqb; ring|]. apply (valid_le_compat p2); [auto|lia]. Qed.
imports: Bool PArith DecidableClass Ring Lia