proposition: Lemma prove_exists m (e:env (model m)) frm n ee : (fun k => if leq_dec (S k) n then ee k else e (k-n)) ⊨ frm -> e ⊨ emplace_exists n frm.
proof: Proof. unfold emplace_exists. induction n as [|n IH] in frm,e,ee|-*. - cbn. intros H. eapply sat_ext. 2:exact H. intros x. cbn. f_equal. lia. - cbn -[leq_dec]. intros H. exists (ee n). apply IH with ee. eapply sat_ext. 2:exact H. intros x. cbn -[leq_dec]. destruct (leq_dec (S x) n) as [Hl|Hr], (leq_dec (S x) (S n)) as [Hl2|Hr2]. + easy. + lia. + assert (x=n) as -> by lia. assert (n-n=0) as -> by lia. easy. + assert (S x > n) as Hxn by lia. assert (x-n = S (x-S n)) as -> by lia. easy. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions