proposition: Lemma build_formula_atom_correct : forall a vm vm' f t, check_atom a t -> build_formula_atom vm a = Some (vm',f) -> wf_vmap vm -> wf_vmap vm' /\ (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ (forall p, (nat_of_P p < nat_of_P (fst vm))%nat -> nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_formula (fst vm') f /\ (interp_bool t_i (interp_atom a) <->Zeval_formula (interp_vmap vm') isProp f).
proof: Proof. intros a vm vm' f t. destruct a;simpl;try discriminate. case_eq (build_op2 b);try discriminate. intros o Heq Ht. assert (Typ.eqb Typ.Tbool t && Typ.eqb (get_type t_i t_func t_atom i) Typ.TZ && Typ.eqb (get_type t_i t_func t_atom i0) Typ.TZ). destruct b;try discriminate;trivial. destruct t0;try discriminate;trivial. unfold is_true in H;rewrite !andb_true_iff in H;decompose [and] H;clear H. case_eq (build_pexpr vm i);intros vm0 pe1 Heq1. case_eq (build_pexpr vm0 i0);intros vm1 pe2 Heq2. intros H Hwf;inversion H;clear H;subst. assert (W1:= build_pexpr_correct _ _ _ _ H3 Heq1 Hwf). decompose [and] W1;clear W1. assert (W1:= build_pexpr_correct _ _ _ _ H1 Heq2 H). decompose [and] W1;clear W1. split;trivial. split;[ apply le_trans with (1:= H4);trivial | ]. split. intros p Hlt;rewrite H0, H8;trivial. apply lt_le_trans with (1:= Hlt);trivial. split. unfold bounded_formula;simpl;rewrite H10, andb_true_r. apply (bounded_pexpr_le (fst vm0));auto with arith. rewrite (interp_pexpr_le _ _ H8 _ H5) in H7. rewrite H7,H12;destruct b;try discriminate;simpl in Heq |- *; inversion Heq;clear Heq;subst;simpl. symmetry;apply Zlt_is_lt_bool. rewrite Zle_is_le_bool;tauto. rewrite Zge_iff_le. unfold Zge_bool;rewrite <- Zcompare_antisym. rewrite Zle_is_le_bool;unfold Zle_bool. destruct (Zeval_expr (interp_vmap vm') pe2 ?= Zeval_expr (interp_vmap vm') pe1)%Z; simpl;tauto. symmetry;apply Zgt_is_gt_bool. destruct t0;inversion H13;clear H13;subst. simpl. apply (Z.eqb_eq (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz