proposition: Lemma reduction_backwards (s : stack) (h : heap) (d0 : dom h) phi : (forall x, x el FV phi -> exists l, s x = Some l /\ (l, (None, None)) el h) -> env s h d0 ⊨ phi <-> msp_sat s h (encode phi).
proof: Proof. induction phi in s |- *; try destruct P; try destruct b0; try destruct q; cbn; intros HV. - tauto. - rewrite map_tl, !map_hd. destruct (Vector.hd t) as [x|[]] eqn : Hx. destruct (Vector.hd (Vector.tl t)) as [y|[]] eqn : Hy. cbn. split. + intros [l Hl]. destruct (HV x) as (l1 & H1 & H2). { apply in_map_iff. exists (Vector.hd t). split; try now rewrite Hx. apply to_list_in, in_hd. } destruct (HV y) as (l2 & H3 & H4). { apply in_map_iff. exists (Vector.hd (Vector.tl t)). split; try now rewrite Hy. apply to_list_in, in_hd_tl. } unfold env in Hl. rewrite H1, H3 in Hl. do 2 destruct Dec; try tauto. cbn in Hl. repeat split. * exists (Some l), l. split; trivial. now rewrite H1, H3. * now exists l1. * now exists l2. + intros [[v[l[-> Hl]]][[l1[H1 H2]][l2[H3 H4]]]]. exists l. unfold env. rewrite H1, H3. do 2 destruct Dec; try tauto. cbn. now rewrite <- H1, <- H3. - rewrite IHphi1, IHphi2; try tauto. all: intros x Hx; apply HV; apply in_app_iff; auto. - rewrite IHphi1, IHphi2; try tauto. all: intros x Hx; apply HV; apply in_app_iff; auto. - rewrite IHphi1, IHphi2; try tauto. all: intros x Hx; apply HV; apply in_app_iff; auto. - split; intros H. + intros [l|] [l'[H1 H2]]; try discriminate. injection H1. intros <-. apply IHphi. * intros [|x] Hx; try now exists l. apply HV. apply in_map_iff. exists (S x). split; trivial. now apply filter_In. * eapply sat_ext; try apply (H (loc2dom H2)). intros x. now rewrite update_stack_cons. + intros [l Hl]. assert (Hl' : (l, (None, None)) el h) by now eapply squash_iff. eapply sat_ext, IHphi, H; cbn. * apply update_stack_cons. * intros [|x] Hx; try now exists l. apply HV. apply in_map_iff. exists (S x). split; trivial. now apply filter_In. * exists l. split; trivial. - split; intros H. + destruct H as [[l Hl] H]. assert (Hl' : (l, (None, None)) el h) by now eapply squash_iff. exists (Some l). split; try now exists l. apply IHphi. * intros [|x] Hx; try now exists l. apply HV. apply in_map_iff. exists (S x). split; trivial. now apply filter_In. * eapply sat_ext; try apply H. intros x. now rewrite update_stack_cons. + destruct H as [[l|][[l'[H1 H2]] H]]; try discriminate. injection H1. intros <-. exists (loc2dom H2). eapply sat_ext, IHphi, H. * intros x. now erewrite update_stack_cons. * intros [|x] Hx; try now exists l. apply HV. apply in_map_iff. exists (S x). split; trivial. now apply filter_In. Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List