proposition: Lemma int_or_ptr_inject: forall v m res f v' m', int_or_ptr v m res -> Val.inject f v v' -> Mem.inject f m m' -> exists res', int_or_ptr v' m' res' /\ Val.inject f res res'.
proof: Proof. destruct 1; intros VI MI; inv VI. - exists Vfalse; split. + constructor; auto. + constructor. - assert (AL: (2 | delta)). { change 2 with (align_chunk Mint16unsigned). clear H0. eauto using Mem.mi_align, Mem.mi_inj, Mem.range_perm_max. } assert (OF: Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta)) = Ptrofs.unsigned ofs + delta). { eapply Mem.address_inject; eauto. apply H. omega. } exists Vtrue; split. + constructor. * rewrite OF. replace (Ptrofs.unsigned ofs + delta + 2) with ((Ptrofs.unsigned ofs + 2) + delta) by omega. eapply Mem.range_perm_inject; eauto. * apply ptrofs_2_aligned in H0. apply ptrofs_2_aligned. rewrite OF. apply Z.divide_add_r; auto. + constructor. Qed.
imports: compcert.lib.Coqlib compcert.lib.Zbits compcert.common.AST compcert.lib.Integers compcert.common.Values compcert.common.Memory compcert.common.Globalenvs compcert.common.Events