proposition: Lemma check_flatten_aux_correct : forall l lf, check_flatten_aux l lf = true -> interp_lit l = interp_lit lf.
proof: Proof. unfold check_flatten_aux. apply foldi_ind. apply leb_0. discriminate. intros i cont _ Hle Hrec l lf;unfold check_flatten_body. rewrite <- (remove_not_correct l), <- (remove_not_correct lf). generalize (remove_not l) (remove_not lf);clear l lf;intros l lf. destruct (reflect_eqb l lf);[ intros;subst;trivial | ]. destruct (reflect_eqb (1 land (l lxor lf)) 0). unfold Lit.interp. assert (Lit.is_pos l = Lit.is_pos lf). unfold Lit.is_pos. rewrite <- eqb_spec, landC in e. change (is_true (is_even (l lxor lf))) in e. rewrite is_even_xor in e. destruct (is_even l);destruct (is_even lf);trivial;discriminate. rewrite H;match goal with |- ?P -> _ => assert (W:P -> Var.interp interp_var (Lit.blit l) = Var.interp interp_var (Lit.blit lf)); [ | intros;rewrite W;trivial] end. unfold Var.interp;rewrite !wf_interp_form;trivial. clear e n H. destruct (get_form (Lit.blit l)); destruct (get_form (Lit.blit lf));intros;try discriminate;simpl;trivial. apply check_atom_correct;trivial. rewrite <- !flatten_and_correct. revert H;generalize (flatten_and a) (flatten_and a0);clear a a0. induction l0;intros l1;destruct l1;simpl;trivial;try discriminate. rewrite andb_true_iff;intros (H1, H2). rewrite (Hrec _ _ H1), (IHl0 _ H2);trivial. rewrite <- !flatten_or_correct. revert H;generalize (flatten_or a) (flatten_or a0);clear a a0. induction l0;intros l1;destruct l1;simpl;trivial;try discriminate. rewrite andb_true_iff;intros (H1, H2). rewrite (Hrec _ _ H1), (IHl0 _ H2);trivial. revert H;destruct (reflect_eqb (length a) (length a0));[intros|discriminate]. apply afold_right_eq;rewrite !length_amap;trivial. intros;rewrite !get_amap by congruence;rewrite aforallbi_spec in H;auto. unfold is_true in H;rewrite andb_true_iff in H;destruct H as [H H0]. rewrite (Hrec _ _ H), (Hrec _ _ H0);trivial. unfold is_true in H;rewrite andb_true_iff in H;destruct H as [H H0]. rewrite (Hrec _ _ H), (Hrec _ _ H0);trivial. unfold is_true in H;rewrite !andb_true_iff in H;destruct H as [[H H0] H1]. rewrite (Hrec _ _ H), (Hrec _ _ H0), (Hrec _ _ H1);trivial. assert (Lit.is_pos l = negb (Lit.is_pos lf)). unfold Lit.is_pos. rewrite <- eqb_spec, landC in n0. change (~is_true (is_even (l lxor lf))) in n0. rewrite is_even_xor in n0. destruct (is_even l);destruct (is_even lf);trivial;elim n0;reflexivity. unfold Lit.interp;rewrite H. match goal with |- ?P -> _ => assert (W:P -> Var.interp interp_var (Lit.blit l) = negb (Var.interp interp_var (Lit.blit lf))); [ | intros;rewrite W;trivial] end. unfold Var.interp;rewrite !wf_interp_form;trivial. destruct (get_form (Lit.blit l));try discriminate. destruct (get_form (Lit.blit lf));try discriminate. apply check_neg_atom_correct. rewrite negb_involutive;destruct (Lit.is_pos lf);trivial. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList