proposition: Lemma mkchain (d:D) : iN d -> exists n f, chain d n f.
proof: Proof. Proof using vTrans vSucc vPred rho rho' m fini decP Hrho. induction d as [dd IH] using (well_founded_ind less_wf). intros H. destruct (eqDec dd z) as [H0|HS]. - exists 0, (fun k => if eqDec k dd then Some 0 else None). recsplit 5. + intros d. split. * intros dl. destruct (eqDec d dd) as [Ht|Hf]. 1:easy. intros _. eapply aZeroS with d. split. 1: now rewrite <- H0. intros HH; apply Hf. transitivity z. 1:easy. now symmetry. * destruct (eqDec d dd) as [Hl|Hr]. 2: easy. intros _. apply leq_eq. all: easy. + intros n. intros [d [ddd Hdd]]. destruct (eqDec d dd). 1: assert (n=0) by congruence;lia. easy. + rewrite eqDec_eq; easy. + rewrite eqDec_eq. 1:easy. now symmetry. + intros dl dh l h H1 H2; split; intros H3; destruct (eqDec dl dd), (eqDec dh dd). 1-4: congruence. all: destruct (vpSucc H3) as [[H321 H322] H33]; exfalso; apply H322; transitivity dd; [easy|now symmetry]. + intros d1 d2. intros H1. split; intros H2; destruct (eqDec d1 dd), (eqDec d2 dd) as [Ht|Hf]. 2-5,7-8:easy. -- intros. transitivity dd; [easy|now symmetry]. -- exfalso. apply Hf. transitivity d1; [now symmetry|easy]. - destruct (@vpPred dd) as [p Hp]. 1-2:firstorder'. destruct (vpSucc Hp) as [Hless Hclose]. destruct (IH p) as [n [f Hnf]]. 1-2: firstorder'. exists (S n). exists (fun v => if eqDec v dd then Some (S n) else f v). destruct Hnf as [xH1 [xH2 [xH3 [xH4 [xH5 xH6]]]]]. recsplit 5. + intros d. split. * intros Hdd. destruct (eqDec d dd) as [Heq|Neq]. -- easy. -- apply xH1, Hclose. now split. * destruct (eqDec d dd) as [Heq|Neq]. -- intros; now apply leq_eq. -- intros HN. eapply leq_trans with p. ++ rewrite <- xH1 in HN. easy. ++ apply Hless. + intros n0. intros [d [Hddd HSome]]. destruct (eqDec d dd). 1: assert (S n = n0) by congruence;lia. enough (n0 <= n) by lia. apply (xH2 n0). exists d. split. 2:easy. apply Hclose. easy. + rewrite (eqDec_eq). 1:easy. firstorder'. + destruct (eqDec z dd) as [H0|Hn0]. 2: apply xH4. exfalso. apply HS. now symmetry. + intros dl dh l h HH1 HH2; split; intros HH3; destruct (eqDec dl dd) as [Hl1|Hh1], (eqDec dh dd) as [Hl2|Hh2]. * exfalso. assert (S l = l) by congruence. lia. * assert (h = S (S n)) as Hc by congruence. enough (h <= n) by lia. apply xH2. exists dh. split. 2:easy. apply xH1. intros Hh; congruence. * assert (l = n) as Hc by congruence. rewrite Hl2. enough (dl == p) as -> by easy. apply xH6; congruence. * apply xH5 with l h; easy. * destruct (vpSucc HH3) as [[H321 H322] H33]; exfalso; apply H322. now rewrite <- Hl2 in Hl1. * exfalso. apply less_irref with dd. eapply vpTrans with dh. -- rewrite <- Hl1. now destruct (vpSucc HH3). -- eapply leq_less with p. 2:easy. rewrite xH1. congruence. * rewrite Hl2 in HH3. assert (dl == p) as Hdlp. -- apply antiSym. ++ apply Hclose. destruct (vpSucc HH3) as [H32 H33]. apply H32. ++ destruct (vpSucc HH3) as [[H321 H322] H33]. apply H33. easy. -- assert (f p = f dl) as Heq. ++ apply xH6. 1:congruence. now symmetry. ++ assert (n = l) by congruence. subst n. congruence. * erewrite xH5. 1:exact HH3. all:easy. + intros d1 d2. intros HSome. split; intros Heq; destruct (eqDec d1 dd) as [Htt|Hff], (eqDec d2 dd) as [Ht|Hf]. -- now rewrite Htt,Ht. -- exfalso. enough (S n <= n) by lia. apply xH2. exists d2. split. 2:easy. apply xH1. now rewrite <- Heq. -- exfalso. enough (S n <= n) by lia. apply xH2. exists d1. split. 2:easy. apply xH1. now rewrite Heq. -- now apply xH6. -- easy. -- exfalso. apply Hf. rewrite <- Htt. now symmetry. -- exfalso. apply Hff. now rewrite Heq. -- apply xH6; 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