proposition: Lemma correct (f:falsity_flag) rho (phi : (@form _ _ full_operators f)) : (rho ⊨ translate_form phi <-> rho f⊨ phi) /\ (rho ⊨ translate_negated phi <-> ~ (rho f⊨ phi)) /\ (forall P wterm, (rho ⊨ wterm <-> P) -> rho ⊨ conj_to_impl_chain phi wterm <-> ((rho f⊨ phi) -> P)) /\ (forall P wterm, (rho ⊨ wterm <-> P) -> rho ⊨ disj_to_impl_chain phi wterm <-> (~(rho f⊨ phi) -> P)).
proof: Proof. Proof using Ddec. induction phi as [|p v|f [| |] l IHl r IHr|f [|] s IHs] in rho|-*. - cbn. recsplit 3. 1-2:easy. 1-2:intros term wterm ->; tauto. - recsplit 3. + cbn. erewrite (Vector.map_ext). 1: apply eval_same_atom. apply eval_same. + cbn. erewrite (Vector.map_ext). 1: apply equiv_impl; apply eval_same_atom. apply eval_same. + intros term wterm H. cbn. rewrite <- eval_same_atom. rewrite <- H. erewrite (Vector.map_ext). 1:easy. apply eval_same. + intros term wterm H. cbn. rewrite H. apply equiv_impl, equiv_impl. erewrite (Vector.map_ext). 1:apply eval_same_atom. apply eval_same. - destruct (IHl rho) as [l1 [l2 [l3 l4]]], (IHr rho) as [r1 [r2 [r3 r4]]]. recsplit 3. + cbn. rewrite l3. 2:easy. rewrite r3. 2:easy. split. * intros H. destruct (Ddec l rho) as [Hl|Hnl], (Ddec r rho) as [Hr|Hnr]. 1:easy. all:exfalso; apply H; intros Hcl Hcr; cbn; easy. * intros [Hl Hr] H. now apply H. + cbn. rewrite l3. 2:easy. rewrite r3. 2:easy. tauto. + intros term wterm H. cbn. rewrite l3. 2:easy. rewrite r3. 2:easy. rewrite H. tauto. + intros term wterm H. cbn. rewrite l3. 2:easy. rewrite r3. 2:easy. rewrite H. apply equiv_impl. tauto. - destruct (IHl rho) as [l1 [l2 [l3 l4]]], (IHr rho) as [r1 [r2 [r3 r4]]]. cbn. recsplit 3. + rewrite l4. 2:easy. rewrite r4. 2:easy. split. * intros H. destruct (Ddec l rho) as [Hl|Hnl], (Ddec r rho) as [Hr|Hnr]. 1-3:tauto. exfalso. now apply H. * tauto. + rewrite l4. 2:easy. rewrite r4. 2:easy. tauto. + intros term wterm H. rewrite l4. 2:easy. rewrite r4. 2:easy. rewrite H. apply equiv_impl. split. 2:tauto. intros Hc. destruct (Ddec l rho) as [Hl|Hnl], (Ddec r rho) as [Hr|Hnr]. 1-3:tauto. exfalso. now apply Hc. + intros term wtertranslate_formm H. rewrite l4. 2:easy. rewrite r4. 2:easy. rewrite H. tauto. - destruct (IHl rho) as [l1 [l2 [l3 l4]]], (IHr rho) as [r1 [r2 [r3 r4]]]. cbn. rewrite l3. 2:easy. rewrite r1. recsplit 3. + tauto. + tauto. + intros term wterm H. rewrite l3. 2:easy. rewrite H. rewrite r1. tauto. + intros term wterm H. rewrite l3. 2:easy. rewrite H. rewrite r1. tauto. - cbn. recsplit 3. + split. * intros H d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH1. apply H. * intros H d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH1. apply H. + split. * intros Hc H. apply Hc. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH1. apply H. * intros Hc H. apply Hc. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH1. apply H. + intros term wterm ->. split. * intros Hc H. apply Hc. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH1. apply H. * intros Hc H. apply Hc. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH1. apply H. + intros term wterm ->. split. * intros Hc H. apply Hc. intros Hcc. apply H. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH1. apply Hcc. * intros Hc H. apply Hc. intros Hcc. apply H. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH1. apply Hcc. - cbn. recsplit 3. + split. * intros H. destruct (Ddec (∃ s) rho) as [[e He]|Hne]. -- now exists e. -- exfalso. apply H. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH2. intros Hc. apply Hne. now exists d. * intros [d Hd] Hc. contradict Hd. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH2. apply Hc. + split. * intros Hc [d Hd]. contradict Hd. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH2. apply Hc. * intros Hc d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH2. intros H. apply Hc. now exists d. + intros term wterm ->. apply equiv_impl. split. * intros H. destruct (Ddec (∃ s) rho) as [[e He]|Hne]. -- now exists e. -- exfalso. apply H. intros d. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite IH2. intros Hc. apply Hne. now exists d. * intros [d Hd] Hc. contradict Hd. destruct (IHs (d.:rho)) as [IH1 [IH2 [IH3 IH4]]]. rewrite <- IH2. apply Hc. + intros term wterm ->. apply equiv_impl. firstorder. Qed.
imports: Vector Undecidability.FOL(Syntax.Facts) Undecidability.FOL.Semantics.Tarski(FullFacts FragmentFacts) Undecidability.FOL.Semantics.FiniteTarski(Full Fragment) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.Synthetic(Definitions)