proposition: Lemma prove_constraints : (zero .: cr2 .: cr1 .: rho) ⊨ translate_constraints h10.
proof: Proof. Proof using φ Hφ. pose (S (highest_var_list h10)) as h10vars. unfold translate_constraints. fold h10vars. pose (highest_num φ h10vars) as h10max. pose (@constr_nums h10max) as Hcons. intros HH. cbn. pose proof (prove_emplace_forall HH) as H. clear HH. apply Hcons. intros f Hrepr. specialize (H (fun t => f (φ t))). pose ((fun v : nat => if v <? h10vars then (fun t : nat => f (φ t)) v else (zero .: cr2 .: cr1 .: rho) (v - h10vars))) as newenv. assert (newenv (S h10vars) = cr2) as Hne1. 1: { unfold newenv. assert (S h10vars <? h10vars = false) as ->. 1: apply Nat.leb_gt; now lia. assert (S h10vars - h10vars = 1) as ->. 1:now lia. easy. } assert (newenv (S (S h10vars)) = cr1) as Hne2. 1: { unfold newenv. assert (S (S h10vars) <? h10vars = false) as ->. 1: apply Nat.leb_gt;lia. assert (S (S h10vars) - h10vars = 2) as ->. 1:now lia. easy. } fold newenv in H. assert (forall c:h10upc, In c h10 -> newenv ⊨ translate_single c (S h10vars)) as Hmain. - intros [[a b][c d]] Hin. pose (@highest_var_list_descr h10 ((a,b),(c,d)) Hin) as Habcdmax. cbn in Habcdmax. intros HH. cbn. rewrite Hne1, Hne2. apply (@constr_rel (φ a) (φ b) (φ c) (φ d) f h10max). 1:easy. 1-4: eapply highest_num_descr; lia. 1: apply (@Hφ ((a,b),(c,d)) Hin). intros pab pcd [Ha [Hb [Hab [Haab Hbab]]]] [Hc [Hd [Hcd [Hccd Hdcd]]]] Hpp. assert (forall k:nat, k < h10vars -> newenv k = f (φ k)) as Hvars. 1:{ unfold newenv, h10vars. intros k Hk. destruct (Nat.ltb_lt k h10vars) as [_ Hr]. fold h10vars. now rewrite Hr. } cbn in HH. rewrite Hne1, Hne2, (Hvars a), (Hvars b), (Hvars c), (Hvars d) in HH. 2-5: unfold h10vars;lia. now apply (@HH pcd pab). - induction h10 as [|hx hr IH] in H,Hmain|-*. + cbn in H. rewrite Hne1,Hne2 in H. apply H. + apply IH. * cbn in H. apply H. apply Hmain. now left. * intros c Hhr. apply Hmain. now right. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.FOL.Reductions(H10UPC_to_FOL_minimal H10UPC_to_FOL_constructions) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Synthetic(Definitions) Coq(Arith Lia List)