proposition: Lemma prove_single (a b c d h: nat) (cc:chain h): b <= h -> a <= h -> c <= h -> d <= h -> h10upc_sem_direct ((a,b),(c,d)) -> (chain_exists cc ++ (F_succ_right :: F_succ_left :: F_zero :: nil)) ⊢I Not (erel_findNum a b c d cc) 1.
proof: Proof. intros Hb. induction b as [|b IH] in h,cc,a,c,d,Hb|-*; intros Ha Hc Hd Habcd. - cbn in Habcd. assert (c = S a /\ d = 0) as [Hc' Hd']. 1:lia. rewrite Hc', Hd'. apply II. rewrite Hc' in Hc. apply (@chain_proves_E_rel h a cc). 1:lia. 1: now apply incl_tl,incl_appl. eapply Weak with (erel_findNum a 0 (S a) 0 cc::nil). 2:intros k [->|[]]; now left. unfold erel_findNum, erel_i. change (∀∀ ?e) with (emplace_forall 2 e). eapply specialize_list with (findPairLow cc (S a)::findPairHigh cc (S a)::nil). 1:easy. unfold findNum. rewrite ! chainData_0. apply Ctx. now left. - destruct (@h10upc_inv a b c d Habcd) as [c' [d' [Habcd' [Hc' Hd']]]]. rewrite <- Hc', <- Hd' in *. assert (h10upc_sem_direct ((d',b),(d'+b+1,d'))) as Hdb. 1: split; [now lia|apply Habcd']. apply erel_findNum_II. eapply IE. 1: eapply Weak; [apply (@IH a c' d' h); easy + lia | now apply incl_tl]. apply erel_findNum_ExI. intros pab pc'd'. eapply IE. 1: eapply Weak; [apply (@IH d' (d'+b+1) d' h); lia + easy|idtac]. 1: now apply incl_appr; apply incl_tl. apply erel_findNum_ExI. intros pd'b psd'. apply (IE (phi:=erel_findNum a (S b) (S c') (d' + b + 1) cc)). 2: apply Ctx, in_or_app; right; apply in_or_app; right; now left. apply (@chain_proves_E_rel h c' cc). 1:lia. 1: now apply incl_appr, incl_appr, incl_tl, incl_appl. apply (@chain_proves_E_rel h b cc). 1:lia. 1: now apply incl_appr, incl_appr, incl_tl, incl_appl. apply (@erel_findNum_H_E d' b (d' + b + 1) d' pd'b psd' h cc). 1: now apply incl_appl. apply (@erel_findNum_H_E a b c' d' pab pc'd' h cc). 1: now apply incl_appr, incl_appl. apply Weak with (F_succ_right::nil). 2: apply incl_appr, incl_appr, incl_tl, incl_appr; intros k [->|[]]; now left. unfold F_succ_right. rewrite erel_ereli. change (∀∀∀∀∀∀∀∀∀∀∀∀∀∀∀ ?a) with (emplace_forall 15 a). pose ( (findNum cc a) ::(findNum cc b) ::(findNum cc c') ::(findNum cc d') ::(findNum cc (d'+b+1)) ::(findNum cc (S b)) ::(findNum cc (S c')) ::pab::pc'd'::pd'b::psd' ::(findPairLow cc (S b))::(findPairHigh cc (S b)) ::(findPairLow cc (S c'))::(findPairHigh cc (S c'))::nil) as mylist. eapply specialize_list with mylist. 1:easy. apply Ctx. now left. 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.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)