proposition: Lemma reduction_forwards rho phi : rho ⊨ phi <-> msp_sat (env2stack rho) interp2heap (encode phi).
proof: Proof. Proof using LD_ex f_dec. induction phi in rho |- *; try destruct P; try destruct b0; try destruct q; cbn. - tauto. - rewrite f_dec, map_tl, !map_hd. destruct (Vector.hd t) as [x|[]] eqn : Hx. destruct (Vector.hd (Vector.tl t)) as [y|[]] eqn : Hy. cbn. split. + pose (d := rho x). pose (e := rho y). intros H. repeat split. * exists (Some (enc_pair d e)), (enc_pair d e). split; trivial. apply in_app_iff. right. apply in_map_iff. exists (d, e). split; try reflexivity. apply filter_In. split; trivial. apply in_prod_iff. split; apply LD_ex. * exists (enc_point d). split; trivial. apply in_app_iff. left. apply in_map_iff. exists d; auto. * exists (enc_point e). split; trivial. apply in_app_iff. left. apply in_map_iff. exists e; auto. + intros [[v[l[-> Hl]]] _]. apply in_app_iff in Hl as [Hl|Hl]. * apply in_map_iff in Hl as [d [H1 H2]]. discriminate. * apply in_map_iff in Hl as [[d e] [H1 H2]]. apply filter_In in H2 as [_ H2]. unfold env2stack in H1. injection H1. now intros -> % enc_point_inj -> % enc_point_inj _. - now rewrite IHphi1, IHphi2. - now rewrite IHphi1, IHphi2. - now rewrite IHphi1, IHphi2. - split; intros H. + intros [l|] [l'[H1 H2]]; try discriminate. injection H1. intros <-. clear H1. apply in_app_iff in H2 as [[d[[=] _]] % in_map_iff |[[][]] % in_map_iff]; try discriminate; subst. eapply msp_sat_ext; try apply IHphi, (H d). now intros []. + intros d. apply IHphi. eapply msp_sat_ext; try apply (H (Some (enc_point d))). * now intros []. * exists (enc_point d). split; trivial. apply in_app_iff. left. apply in_map_iff. exists d; auto. - split. + intros [d H]. exists (Some (enc_point d)). split. * exists (enc_point d). split; trivial. apply in_app_iff. left. apply in_map_iff. exists d; auto. * eapply msp_sat_ext; try apply IHphi, H. now intros []. + intros [v[[l [-> Hl]] H]]. apply in_app_iff in Hl as [[d[[=] _]] % in_map_iff |[[][]] % in_map_iff]; try discriminate; subst. exists d. apply IHphi. eapply msp_sat_ext; try apply H. now intros []. 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