proposition: Lemma build_pexpr_correct : forall h vm vm' pe, Typ.eqb (get_type t_i t_func t_atom h) Typ.TZ -> build_pexpr vm h = (vm',pe) -> 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_pexpr (fst vm') pe /\ t_interp.[h] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe).
proof: Proof. intros. case_eq (h <? length t_atom);intros. apply build_pexpr_correct_aux;trivial. rewrite <- ltb_spec;trivial. revert H;unfold get_type,get_type'. rewrite PArray.get_outofbound, default_t_interp. revert H0. unfold build_pexpr. apply foldi_ind. apply leb_0. discriminate. intros i a _ Hi IH. rewrite PArray.get_outofbound by exact H2. Opaque build_z_atom. rewrite def_t_atom; simpl. intros HH H. revert HH H1. apply build_pexpr_atom_aux_correct_z; trivial. rewrite length_t_interp;trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz