proposition: Lemma t_interp_wf_lt : forall i, i <? PArray.length t_atom -> t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
proof: Proof. assert (Bt := to_Z_bounded (length t_atom)). set (P' i t := length t = length t_atom -> forall j, j <? i -> t.[j] = interp_aux (PArray.get t) (t_atom.[j])). assert (P' (length t_atom) t_interp). unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i. unfold t_interp;apply foldi_ind;unfold P';intros. rewrite leb_spec, to_Z_0; lia. elim (ltb_0 _ H0). rewrite length_set in H2. destruct (Misc.reflect_eqb j i). rewrite e, PArray.get_set_same. apply lt_interp_aux with (2:= wf_t_i i H0). intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial. rewrite H2;trivial. assert (j <? i). assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);auto with zarith. rewrite get_set_other, H1;auto. apply lt_interp_aux with (2:= wf_t_i j (ltb_trans _ _ _ H4 H0)). intros;rewrite get_set_other;trivial. intros Heq;elim (not_ltb_refl i);apply ltb_trans with j; [ rewrite Heq| ];trivial. apply H;apply length_t_interp. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList