proposition: Lemma build_pexpr_correct_aux : forall h vm vm' pe, (to_Z h < to_Z (length t_atom))%Z -> 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. unfold build_pexpr. apply foldi_ind. apply leb_0. intros h vm vm' pe Hh. assert (W:=to_Z_bounded h);rewrite to_Z_0 in Hh. elimtype False;lia. intros i cont Hpos Hlen Hrec. intros h vm vm' pe;unfold is_true;rewrite <-ltb_spec;intros. rewrite t_interp_wf;trivial. apply build_pexpr_atom_aux_correct with cont h (i + 1);trivial. intros;apply Hrec;auto. unfold is_true in H3;rewrite ltb_spec in H, H3, Hlen; rewrite to_Z_add_1_wB in H; generalize (to_Z_bounded (length t_atom)); lia. unfold wf, is_true in wf_t_atom. rewrite aforallbi_spec in wf_t_atom. apply wf_t_atom. rewrite ltb_spec in H, Hlen;rewrite ltb_spec; rewrite to_Z_add_1_wB in H; generalize (to_Z_bounded (length t_atom)); lia. unfold wt, is_true in wt_t_atom. rewrite aforallbi_spec in wt_t_atom. change (is_true(Typ.eqb (get_type t_i t_func t_atom h) Typ.TZ)) in H0. rewrite Typ.eqb_spec in H0;rewrite <- H0. apply wt_t_atom. rewrite ltb_spec in H, Hlen; rewrite ltb_spec; rewrite to_Z_add_1_wB in H; generalize (to_Z_bounded (length t_atom)); lia. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz