proposition: Lemma triple_alloc: forall x sz, [[ emp ]] ALLOC x sz [[ aexists (fun l => aequal (VAR x) l //\\ valid_N l sz) ]].
proof: Proof. intros; intros R IND s h (h1 & h2 & EMP & R1 & DISJ & EQ). destruct (isfinite h) as (l0 & FIN). set (l := Z.max l0 1). do 2 econstructor; split. - apply star_one. apply red_alloc with (l := l). intros; apply FIN; lia. lia. - exists (hinit l sz hempty), h2; intuition auto. + exists l; split. red; cbn. apply update_same. assert (REC: forall s1 sz1 l1, valid_N l1 sz1 s1 (hinit l1 sz1 hempty)). { induction sz1; cbn; intros. * red; auto. * exists (hupdate l1 0 hempty), (hinit (l1 + 1) sz1 hempty); intuition auto. ** exists 0; red; auto. ** red; intros. cbn. destruct (Z.eq_dec l1 l2); auto. right; apply hinit_outside; lia. ** apply heap_extensionality; intros. cbn. destruct (Z.eq_dec l1 l2); auto. } apply REC. + apply IND with s; auto. cbn; intros. apply update_other; auto. + intros l'. destruct (Z.lt_ge_cases l' l). left; apply hinit_outside; auto. right. assert (L: h l' = None) by (apply FIN; lia). rewrite EQ in L; cbn in L. destruct (h1 l'); congruence. + rewrite EQ, EMP, hunion_empty. apply heap_extensionality; intros l'; cbn. destruct (Z.lt_ge_cases l' l). rewrite ! hinit_outside by auto. auto. destruct (Z.lt_ge_cases l' (l + Z.of_nat sz)). rewrite ! hinit_inside by auto. auto. rewrite ! hinit_outside by auto. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)