proposition: Lemma chain_proves (a b c d: D) (nm : nat) (f:D->option nat): chain m nm f -> b <<= m -> irel a b c d -> a <<= m -> c <<= m -> d <<= m -> exists a' b' c' d', h10upc_sem_direct ((a',b'),(c',d')) /\ f a = Some a' /\ f b = Some b' /\ f c = Some c' /\ f d = Some d'.
proof: Proof. Proof using vTrans vSucc vDescr2 vDescr rho' rho fini decP Hrho. intros Hf. pose Hf as HHf. destruct HHf as [Hf1 [_ [_ [xHf4 [Hf5 xHf6]]]]]. induction b as [b IH] in a,c,d|-* using (well_founded_ind less_wf); intros Hb Habcd Ha Hc Hd. destruct (eqDec b z) as [Hbz|Hnbz]. - destruct (f a) as [na|] eqn:Heqfa. 2: exfalso; apply (Hf1 a); easy. exists na, 0, (S na), 0. assert (d == z) as Hdd0. 2: recsplit 4. 2:easy. + specialize (@vDescr2 a b c d). fold sat in vDescr2. cbn in vDescr2. rewrite ! to_N, to_rel, ! to_deq, Hrho in vDescr2. cbn in vDescr2. apply vDescr2. 1-4:firstorder'. all:easy. + easy. + rewrite <- xHf4. apply xHf6. 1: now apply Hf1. easy. + assert (isucc a c z) as Hsucc. * unfold isucc. rewrite <- Hbz at 1. now rewrite <- Hdd0. * destruct (f c) as [Sna|] eqn:Hfc. -- f_equal. symmetry. erewrite (Hf5 a c); easy. -- exfalso. contradict Hfc. rewrite <- Hf1. easy. + symmetry. rewrite <- xHf4, xHf6. 2:congruence. now symmetry. - specialize (@vDescr a b c d). fold sat in vDescr. cbn in vDescr. setoid_rewrite Hrho in vDescr. cbn in vDescr. setoid_rewrite to_N in vDescr. cbn in vDescr. setoid_rewrite to_rel in vDescr. cbn in vDescr. setoid_rewrite to_deq in vDescr. cbn in vDescr. setoid_rewrite to_less in vDescr. cbn in vDescr. destruct vDescr as [b' [c' [d' [[[[Hb' Hc'] Hd'1] Hd'2] Hd'3]]]]. 1-4,6:firstorder'. 1: intros H; rewrite H in Hnbz; firstorder'. destruct (vpSucc Hb') as [Hb'1 Hb'2]. destruct (vpSucc Hc') as [Hc'1 Hc'2]. edestruct (IH b' (ltac:(firstorder')) d' d d') as [nd' [nb' [nd [nd'2 [HIH1 [Hnd' [Hnb2 [Hnd2 Hnd'2]]]]]]]]. 2:easy. 3:easy. 2: apply leq_trans with d; firstorder. 1: eapply leq_trans with b; firstorder. 1: eapply leq_trans with d; firstorder. edestruct (IH b' (ltac:(firstorder')) a c' d') as [na [nb'3 [nc' [nd'3 [HIH2 [Hna [Hnb3 [Hnc' Hnd'3]]]]]]]]. 2-3:easy. 1: apply leq_trans with b; firstorder. 1: eapply leq_trans with c; firstorder. 1: eapply leq_trans with d; firstorder. exists na, (S nb'), (S nc'), (1+nb'+nd'). recsplit 4. + cbn. cbn in HIH1, HIH2. assert (nd'2 = nd') as -> by congruence. assert (nd'3 = nd') as -> by congruence. assert (nb'3 = nb') as -> by congruence. split;nia. + easy. + destruct (f b) as [nb|] eqn:Hfb. 2: exfalso;now eapply Hf1 with b. f_equal. symmetry. erewrite Hf5. 1: exact Hb'. all:easy. + destruct (f c) as [nc|] eqn:Hfc. 2: exfalso;now eapply Hf1 with c. f_equal. symmetry. erewrite Hf5. 1: exact Hc'. all:easy. + assert (f d = Some nd) as -> by easy. f_equal. cbn in *; nia. 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