proposition: Lemma prove_emplace_forall (n:nat) (i:form) (r:env D) : r ⊨ emplace_forall n i -> forall f, (fun v => if v <? n then f v else r (v-n)) ⊨ i.
proof: Proof. induction n as [|n IH] in r|-*. - cbn. intros H f. apply (sat_ext I (rho := r) (xi:=fun v => r(v-0)) i). + intros x. now rewrite Nat.sub_0_r. + easy. - intros H f. cbn. cbn in H. specialize (H (f n)). specialize (IH (f n .: r) H f). eapply (sat_ext I (xi := (fun v : nat => if v <? n then f v else (f n .: r) (v - n))) i). + intros x. destruct (Nat.eq_dec x n) as [Hxn|Hnxn]. * destruct (Nat.leb_le x n) as [_ Hr]. specialize (Hr ltac:(lia)). rewrite Hr. destruct (Nat.ltb_ge x n) as [_ Hr2]. specialize (Hr2 ltac:(lia)). rewrite Hr2. assert (x-n=0) as Hxn0. 1:lia. rewrite Hxn0. cbn. now f_equal. * destruct (x <? n) as [|] eqn:Hxn. -- apply (Nat.ltb_lt) in Hxn. assert (x <=? n = true) as Hxn2. 1: apply Nat.leb_le; lia. rewrite Hxn2. easy. -- apply (Nat.ltb_ge) in Hxn. assert (x <=? n = Datatypes.false) as Hxn2. 1: apply Nat.leb_gt; lia. rewrite Hxn2. assert (x-n = S(x-S n)) as Hxn3. 1:lia. rewrite Hxn3. cbn. easy. + easy. 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)