proposition: Lemma build_pexpr_atom_aux_correct_z : forall (h : atom) (vm vm' : vmap) (pe : PExpr Z), check_atom h Typ.TZ -> match build_z_atom h with | Some z => (vm, PEc z) | None => let (vm0, p) := find_var vm h in (vm0, PEX p) end = (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 h = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe).
proof: Proof. intros h vm vm' pe Hh. case_eq (build_z_atom h). intros z Hb Heq;inversion Heq;clear Heq;subst. intros (Hwf1, Hwf2). repeat split;auto with zarith. rewrite (build_z_atom_correct _ _ Hb);trivial. intros _;unfold find_var;destruct vm as (pvm,lvm). case_eq (find_var_aux h pvm lvm). intros p Hf Heq;inversion Heq;clear Heq;subst. intros (Hwf1, Hwf2);repeat split;auto with zarith. simpl; unfold is_true;rewrite <- Zlt_is_lt_bool. rewrite <- !Z_of_nat_of_P; apply inj_lt;simpl in Hwf1. apply find_var_aux_lt with (1:= Hf);trivial. revert lvm pvm p Hf Hwf1 Hwf2. unfold interp_vmap;simpl. induction lvm;simpl;try discriminate. intros pvm p Heq1 Heq. assert (1 < pvm)%positive. rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;lia. assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat. rewrite Ppred_minus, Pminus_minus;trivial. change (nat_of_P 1) with 1%nat ;try lia. revert Heq1. destruct (Atom.reflect_eqb h a);subst. intros Heq1;inversion Heq1;clear Heq1;subst. unfold is_true;rewrite andb_true_iff;intros (H1,H2). assert (1 < nat_of_P pvm)%nat by (rewrite Plt_lt in H;trivial). assert (W:=nat_of_P_pos (Pos.pred pvm)). assert (nat_of_P (pvm - Pos.pred pvm) - 1 = 0)%nat. rewrite Pminus_minus;lia. rewrite H4;simpl. destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ H1) as (z,Hz). rewrite Hz;trivial. unfold is_true;rewrite andb_true_iff;intros Heq1 (H1,H2). assert (W:= find_var_aux_lt _ _ _ _ Heq1 H0). assert (nat_of_P (pvm - p) - 1 = S (nat_of_P (Pos.pred pvm - p) - 1))%nat. assert (W1:= W);rewrite <- Plt_lt in W. rewrite !Pminus_minus;trivial. assert (W2:=nat_of_P_pos (Pos.pred pvm)). lia. rewrite Plt_lt. apply lt_trans with (1:= W1);lia. rewrite H3;simpl;apply IHlvm;trivial. intros _ Heq;inversion Heq;clear Heq;subst;unfold wf_vmap; simpl;intros (Hwf1, Hwf2);repeat split;simpl. rewrite Psucc_S; assert (W:= nat_of_P_pos pvm);lia. rewrite Hh;trivial. rewrite Psucc_S;lia. intros p Hlt; assert (nat_of_P (Pos.succ pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat. assert (W1:= Hlt);rewrite <- Plt_lt in W1. rewrite !Pminus_minus;trivial. rewrite Psucc_S;lia. rewrite Plt_lt, Psucc_S;lia. rewrite H;trivial. unfold is_true;rewrite <- Zlt_is_lt_bool. rewrite Zpos_succ_morphism;lia. destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ Hh) as (z,Hz). rewrite Hz;unfold interp_vmap;simpl. assert (nat_of_P (Pos.succ pvm - pvm) = 1%nat). rewrite Pplus_one_succ_l, Pminus_minus, Pplus_plus. change (nat_of_P 1) with 1%nat;lia. rewrite Plt_lt, Pplus_plus. change (nat_of_P 1) with 1%nat;lia. rewrite H;simpl;rewrite Hz;trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz