proposition: Lemma sat_comp_p rho σ phi : sat rho (phi[σ]p) <-> sat ⟨get_indi rho, get_func rho, σ >>> eval_predicate rho⟩ phi.
proof: Proof. induction phi in rho, σ |- *; cbn. - reflexivity. - destruct p; cbn; rename t into v; enough (map (eval rho) v = map (eval ⟨get_indi rho, get_func rho, σ >>> eval_predicate rho⟩) v) as -> by reflexivity; apply map_ext_forall; induction v; firstorder; now apply eval_ext. - specialize (IHphi1 rho σ); specialize (IHphi2 rho σ). destruct b; cbn; intuition easy. - destruct q. + setoid_rewrite IHphi. split; intros H d; eapply sat_ext. 2, 4: apply (H d). all: easy. + setoid_rewrite IHphi. split; intros [d H]; exists d; eapply sat_ext. 2, 4: apply H. all: easy. - destruct q. + setoid_rewrite IHphi. split; intros H f; eapply sat_ext. 2, 4: apply (H f). all: easy. + setoid_rewrite IHphi. split; intros [f H]; exists f; eapply sat_ext. 2, 4: apply H. all: easy. - destruct q. + setoid_rewrite IHphi; split; intros H P; eapply sat_ext. 2, 4: apply (H P). all: clear; intros []; split; try easy; split; try easy; cbn; destruct Nat.eq_dec as [->|]; cbn. 1, 5: destruct Nat.eq_dec; try easy; rewrite Eqdep_dec.UIP_dec with (p1 := e) (p2 := eq_refl); try easy; decide equality. 1-3: now rewrite eval_predicate_subst_cons_shift_p with (Q := P). all: now rewrite <- eval_predicate_subst_cons_shift_p with (Q := P). + setoid_rewrite IHphi; split; intros [P H]; exists P; eapply sat_ext. 2, 4: apply H. all: clear; intros []; split; try easy; split; try easy; cbn; destruct Nat.eq_dec as [->|]; cbn. 1, 5: destruct Nat.eq_dec; try easy; rewrite Eqdep_dec.UIP_dec with (p1 := e) (p2 := eq_refl); try easy; decide equality. 1-3: now rewrite eval_predicate_subst_cons_shift_p with (Q := P). all: now rewrite <- eval_predicate_subst_cons_shift_p with (Q := P). Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector