proposition: Lemma m_deq (m:nat) (e : env (model m)) (l r : nat) : m > 0 -> e ⊨ deq l r <-> e l = e r.
proof: Proof. intros Hm0. destruct (e l) as [[n1 Hn1]|[a Ha] [b Hb]] eqn:Hel, (e r) as [[n2 Hn2]|[c Hc] [d Hd]] eqn:Her; split. * unfold deq. intros H. specialize (H (Pair (fN Hn1) (fN Hn1))). cbn in H. rewrite Hel, Her in H. assert (n1 = n2) as -> by firstorder congruence. do 2 f_equal. apply le_unique. * cbn -[model_rel]. intros H d. unfold model_rel. rewrite Hel,Her. cbn. assert (n1 = n2) as -> by firstorder congruence. firstorder. * intros H. change H with (forall d : model m, ((d # e l <-> d # e r)) /\ (e l # d <-> e r # d)). destruct (differentNums (fN Hn1) Hm0) as [m1 [m2 [Hm12 [[Hm2a1 Hm2a2]|[Hm2b1 Hm2b2]]]]]; pose proof (H (Num m1)) as [Hl1 Hl2]; pose proof (H (Num m2)) as [Hh1 Hh2]; destruct m1 as [nm1 Hm1], m2 as [nm2 Hm2]; cbn -[model_rel] in *; rewrite Hel in *; rewrite Her in *. - contradict Hm12. apply (proj1 Hl1) in Hm2a1. apply (proj1 Hh1) in Hm2a2. assert (nm1 = nm2) as -> by congruence. f_equal. apply le_unique. - contradict Hm12. apply (proj1 Hl2) in Hm2b1. apply (proj1 Hh2) in Hm2b2. assert (nm1 = nm2) as -> by congruence. f_equal. apply le_unique. * intros H. discriminate. * intros H. destruct (differentNums (fN Hn2) Hm0) as [m1 [m2 [Hm12 [[Hm2a1 Hm2a2]|[Hm2b1 Hm2b2]]]]]; pose proof (H (Num m1)) as [Hl1 Hl2]; pose proof (H (Num m2)) as [Hh1 Hh2]; destruct m1 as [nm1 Hm1], m2 as [nm2 Hm2]; cbn -[model_rel] in *; rewrite Hel in *; rewrite Her in *. - contradict Hm12. apply (proj2 Hl1) in Hm2a1. apply (proj2 Hh1) in Hm2a2. assert (nm1 = nm2) as -> by congruence. f_equal. apply le_unique. - contradict Hm12. apply (proj2 Hl2) in Hm2b1. apply (proj2 Hh2) in Hm2b2. assert (nm1 = nm2) as -> by congruence. f_equal. apply le_unique. * intros H. discriminate. * intros H. pose proof (H (Num (fN Ha))) as HHa. pose proof (H (Num (fN Hb))) as HHb. cbn in H, HHa, HHb. cbn. f_equal. all: rewrite Hel in *; rewrite Her in *. - assert (a = c) as -> by firstorder congruence. f_equal. apply le_unique. - assert (d = b) as -> by firstorder congruence. f_equal. apply le_unique. * cbn -[model_rel]. rewrite !Hel,! Her. intros ->. firstorder. 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