proposition: Lemma build_pexpr_atom_aux_correct' : forall (build_pexpr : vmap -> hatom -> vmap * PExpr Z), (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))-> forall a vm vm' pe, check_atom a Typ.TZ -> build_pexpr_atom_aux build_pexpr vm a = (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 /\ interp_atom a = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe).
proof: Proof. intros build_pexpr Hb a. Opaque build_z_atom interp_aux. case a;simpl; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). intro u; destruct u; intros ind vm vm' pe Ht; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). generalize (Hb ind vm); clear Hb. destruct (build_pexpr vm ind) as (vm0,pe0); intro IH. intros Heq Hwf;inversion Heq;clear Heq;subst. assert (W:= IH vm' pe0 Ht (refl_equal _) Hwf). decompose [and] W;clear W IH. destruct H;repeat split;trivial. Transparent interp_aux. simpl;rewrite H4;trivial. intro b; destruct b; intros j k vm vm' pe Ht; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). generalize (Hb j vm). destruct (build_pexpr vm j) as (vm0,pe0); intro IH. generalize (Hb k vm0); clear Hb. destruct (build_pexpr vm0 k) as (vm1,pe1); intro IH'. simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; decompose [and] Ht;clear Ht. intros Heq Hwf;inversion Heq;clear Heq;subst. assert (W:= IH _ _ H (refl_equal _) Hwf);clear IH. decompose [and] W;clear W. assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'. decompose [and] W;clear W. destruct H5;repeat split;trivial. apply le_trans with (1:= H3);trivial. intros p Hlt;rewrite H2, H7;trivial. apply lt_le_trans with (1:=Hlt);trivial. simpl;rewrite H9, andb_true_r. apply (bounded_pexpr_le (fst vm0));auto with arith. simpl;rewrite H6, H11;simpl. rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. generalize (Hb j vm). destruct (build_pexpr vm j) as (vm0,pe0); intro IH. generalize (Hb k vm0); clear Hb. destruct (build_pexpr vm0 k) as (vm1,pe1); intro IH'. simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; decompose [and] Ht;clear Ht. intros Heq Hwf;inversion Heq;clear Heq;subst. assert (W:= IH _ _ H (refl_equal _) Hwf);clear IH. decompose [and] W;clear W. assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'. decompose [and] W;clear W. destruct H5;repeat split;trivial. apply le_trans with (1:= H3);trivial. intros p Hlt;rewrite H2, H7;trivial. apply lt_le_trans with (1:=Hlt);trivial. simpl;rewrite H9, andb_true_r. apply (bounded_pexpr_le (fst vm0));auto with arith. simpl;rewrite H6, H11;simpl. rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. generalize (Hb j vm). destruct (build_pexpr vm j) as (vm0,pe0); intro IH. generalize (Hb k vm0); clear Hb. destruct (build_pexpr vm0 k) as (vm1,pe1); intro IH'. simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; decompose [and] Ht;clear Ht. intros Heq Hwf;inversion Heq;clear Heq;subst. assert (W:= IH _ _ H (refl_equal _) Hwf);clear IH. decompose [and] W;clear W. assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'. decompose [and] W;clear W. destruct H5;repeat split;trivial. apply le_trans with (1:= H3);trivial. intros p Hlt;rewrite H2, H7;trivial. apply lt_le_trans with (1:=Hlt);trivial. simpl;rewrite H9, andb_true_r. apply (bounded_pexpr_le (fst vm0));auto with arith. simpl;rewrite H6, H11;simpl. rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz