proposition: Lemma cancel_sound' i sh1 sh2 unm fs : interp i sh2 = interp i (sh1 ++ unm) -> def (interp i sh2) -> eval i fs -> eval i (cancel' i sh1 sh2 unm fs).
proof: Proof. elim: sh1 sh2 unm fs=>[|[sx sd|sv] sh1 IH] sh2 unm fs. - case: unm=>[|[sxu sdu|svu] [|[sxu' sud'|svu'] unm']]; case: sh2=>[|[sx2 sd2|sv2] sh2'] /=; try by case: fs. case A: (onth _ sx2)=>[a|]; last by case sh2'. case D: (onth _ sxu)=>[d|]; last by move->. case: sh2'=>[/= H2 Def|e sh2']; last by rewrite /= A D =>->; case: fs. case: (pts_injP Def H2)=>[H3 H4]. rewrite A D H3; split=>//. case: sdu sd2 H4 H2 Def=>b1 b2 [c1 c2] /= H4; move: b2. rewrite -H4 H3=> b2 H2 Def. by move/(pts_inj Def): H2=>->; case: fs H. - rewrite [eval _ (cancel' _ _ _ _ _)]/=. case: ifP=>H1 H2 D E; last first. - apply: (IH _ _ _ _ D E). by rewrite H2 2!interp_cat 2!interp_cons unCA unA. apply: IH; last 2 first. - by apply: pfree_def. - rewrite -ptr_has in H1; rewrite /= -(lookR D H1). rewrite H2 interp_cons /= in D *. case A: (onth _ sx)=>[a|//] in D *. by rewrite (lookPtUn D) -dyn_eta; case: fs E. rewrite -ptr_has in H1; rewrite -(freeR D H1). rewrite H2 cat_cons /= in D *. case A: (onth _ sx)=>[a /=|] in D *; last by case: (sh1 ++ unm) D. case: (sh1 ++ unm) D=>[|c s D]; last by rewrite (freePtUn D). by rewrite freeU defU eq_refl; case/andP; move/negbTE=>-> _; rewrite free0. rewrite [eval _ (cancel' _ _ _ _ _)]/=. case: ifP=>H1 H2 D E; last first. - apply: (IH _ _ _ _ D E). by rewrite H2 2!interp_cat 2!interp_cons unCA unA. apply: IH=>//; last by apply: hfree_def. rewrite -has_pred1 has_count in H1. case H1: (count _ _) H1=>[//|[|n]] _; last first. - have H3: count (pred1 sv) (vars sh2) > 1 by rewrite H1. move: (countN_varfree H3 D)=>/= H4. by rewrite (empty_hfree sh2 H4) H2 interp_cons /= H4 un0h. move/(interp_perm i): (count1_hfree H1)=>H6. rewrite -H6 cat_cons 2!interp_cons in H2. rewrite -H6 interp_cons H2 in D. by apply: (unhKr D H2). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)