proposition: Lemma emplace_exists_spec rho' n i : (exists f, (fun k => if k <? n then f (k) else rho' (k-n)) ⊨ i) -> rho' ⊨ emplace_exists n i.
proof: Proof. intros [f Hf]. unfold emplace_exists. induction n as [|n IH] in rho',f,Hf|-*. - cbn. eapply sat_ext. 2:exact Hf. intros x. cbn. now rewrite Nat.sub_0_r. - cbn. exists (f n). eapply sat_ext. 2:apply (IH (f n .: rho') f). + intros x. easy. + eapply sat_ext. 2:apply Hf. intros x. cbv beta. destruct (x <? n) eqn:Heq, (x <? S n) eqn:HSeq. * easy. * exfalso. rewrite Nat.ltb_lt in Heq. rewrite Nat.ltb_ge in HSeq. lia. * rewrite Nat.ltb_ge in Heq. rewrite Nat.ltb_lt in HSeq. assert (x = n) as -> by lia. rewrite Nat.sub_diag. easy. * rewrite Nat.ltb_ge in Heq. rewrite Nat.ltb_ge in HSeq. assert (x-n=S(x-S n)) as -> by lia. cbn. easy. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions