proposition: Lemma valid (e:env (model m)) : e ⊨ F.
proof: Proof. Proof using H10sat. exists (Num (fN le0)). exists (Num(into_fin m m)). split. 1:split. 1:split. 1:split. 1:split. - cbn. intros x y z. rewrite ! m_less; cbn. 2-4: solve_m. intros [n1 [u1 [n2 [u2 [Hx [Hy Hr]]]]]] [n2' [u2' [n3 [u3 [Hy' [Hz Hr2]]]]]]. exists n1,u1,n3,u3. split. 2:split. 1-2:easy. enough (n2 = n2') by lia. rewrite Hy in Hy'. congruence. - cbn. unfold succ. intros k. rewrite m_N, m_deq. 2:solve_m. cbn. intros [n1 [u1 ->]] Hn0. assert (n1 <> 0) as Hn0'. + intros Hc. apply Hn0. subst n1. f_equal. f_equal. apply le_unique. + destruct n1 as [|n1]. 1:lia. assert (n1 <= m) as Hn1 by lia. exists (Num (fN Hn1)). rewrite m_rel. 2:solve_m. exists n1,Hn1,0,le0,(S n1),u1,0,le0. cbn. repeat split. lia. - cbn. intros l r. rewrite !m_N, m_rel, m_less. 2-3:solve_m. cbn. intros [nl [ul ->]] [nr [ur ->]] [na [ua [nb [ub [nc [uc [nd [ud [-> [Hnb [-> [-> H]]]]]]]]]]]]. split. + exists na,ua,nc,uc. repeat split. lia. + intros k. rewrite ! m_less, ! m_leq. 2-3:solve_m. cbn. intros [nk [uk [nc' [uc' [Hk1 [Hk2 Hk3]]]]]]. exists nk,uk,na,ua. repeat split. 1:easy. assert (nc = nc') as -> by congruence. enough (nb = 0) by lia. congruence. - unfold aDescr. intros a b c d [na [ua Ha]]%m_N [nb [ub Hb]]%m_N [nc [uc Hc]]%m_N [nd [ud Hd]]%m_N. cbn in Ha,Hb,Hc,Hd. cbn. rewrite !m_deq. 2:solve_m. unfold succ. cbn. intros Hnz. rewrite !m_rel. 2:solve_m. rewrite Ha,Hb,Hc,Hd. cbn. intros [na' [ua' [nb' [ub' [nc' [uc' [nd' [ud' [Ha' [Hb' [Hc' [Hd' H]]]]]]]]]]]]. assert (na = na') as -> by congruence. assert (nb = nb') as -> by congruence. assert (nc = nc') as -> by congruence. assert (nd = nd') as -> by congruence. assert (nb' <> 0) as Hb0. 1: { intros Hcc. apply Hnz. rewrite Hb. f_equal. subst nb'. f_equal. apply le_unique. } destruct nb' as [|nb']. 1:lia. assert (nc' <> 0) as Hc0 by lia. destruct nc' as [|nc']. 1:lia. assert (nb' <= m) as Hnb' by lia. assert (nc' <= m) as Hnc' by lia. assert (nd'-nb'-1 <= m) as Hnd' by lia. exists (Num (fN Hnb')), (Num (fN Hnc')), (Num (fN Hnd')). rewrite !m_rel. 2-5:solve_m. cbn -[h10upc_sem_direct]. split. 1:split. 1:split. 1:split. + exists nb',Hnb',0,le0,(S nb'),ub,0,le0. repeat split; lia. + exists nc',Hnc',0,le0,(S nc'),uc,0,le0. repeat split; lia. + exists (nd'-nb'-1),Hnd',nb',Hnb',nd',ud,(nd'-nb'-1),Hnd'. repeat split; lia. + exists na',ua,nb',Hnb',nc',Hnc',(nd'-nb'-1),Hnd'. repeat split; lia. + rewrite ! m_less. 2:solve_m. cbn. exists (nd' - nb' - 1), Hnd',nd',ud. split. 1:easy. split. 1:easy. lia. - unfold aDescr2. intros a b c d [na [ua Ha]]%m_N [nb [ub Hb]]%m_N [nc [uc Hc]]%m_N [nd [ud Hd]]%m_N. intros [na' [ua' [nb' [ub' [nc' [uc' [nd' [ud' [Ha' [Hb' [Hc' [Hd' H]]]]]]]]]]]]%m_rel. 2:solve_m. cbn in *. rewrite ! m_deq. 2-3:solve_m. cbn. intros ->. rewrite Hd'. assert (nb' = 0) as -> by congruence. assert (nd' = 0) as Hnd' by lia. subst nd'. f_equal. f_equal. apply le_unique. - eapply prove_exists with myenv. pose (highest_var_list h10) as lh10. fold lh10. assert (highest_var_list h10 <= lh10) as Hvl by easy. induction h10 as [|h10v h10r IH] in H10sat,Hvl|-*. + cbn. tauto. + cbn -[leq_dec]. split. * destruct h10v as [[a b][c d]]. unfold translate_single. cbn in Hvl. destruct (@myenv_desc a) as [ua Ha]. 1:lia. destruct (@myenv_desc b) as [ub Hb]. 1:lia. destruct (@myenv_desc c) as [uc Hc]. 1:lia. destruct (@myenv_desc d) as [ud Hd]. 1:lia. split. 1:split. 1:split. 1:split. -- rewrite m_rel. 2:solve_m. exists (rho a). exists ua. exists (rho b). exists ub. exists (rho c). exists uc. exists (rho d). exists ud. repeat destruct leq_dec. 2-16:lia. split. 2:split. 3:split. 4:split. 1-4:easy. apply (@H10sat ((a,b),(c,d))). now left. -- rewrite m_leq. 2:solve_m. unfold into_fin. destruct (leq_dec m m) as [Hml|Hmnl]; repeat destruct leq_dec. 1,3,5,7,6,4:lia. 2:lia. exists (rho a), ua, m, Hml. split. 1:easy. split. 1: assert (forall k,k-k=0) as -> by lia. 2:lia. cbn. easy. -- rewrite m_leq. 2:solve_m. unfold into_fin. destruct (leq_dec m m) as [Hml|Hmnl]; repeat destruct leq_dec. 1,3,5,7,6,4:lia. 2:lia. exists (rho b), ub, m, Hml. split. 1:easy. split. 1: assert (forall k,k-k=0) as -> by lia. 2:lia. cbn. easy. -- rewrite m_leq. 2:solve_m. unfold into_fin. destruct (leq_dec m m) as [Hml|Hmnl]; repeat destruct leq_dec. 1,3,5,7,6,4:lia. 2:lia. exists (rho c), uc, m, Hml. split. 1:easy. split. 1: assert (forall k,k-k=0) as -> by lia. 2:lia. cbn. easy. -- rewrite m_leq. 2:solve_m. unfold into_fin. destruct (leq_dec m m) as [Hml|Hmnl]; repeat destruct leq_dec. 1,3,5,7,6,4:lia. 2:lia. exists (rho d), ud, m, Hml. split. 1:easy. split. 1: assert (forall k,k-k=0) as -> by lia. 2:lia. cbn. easy. * apply IH. -- intros k Hk. apply H10sat. now right. -- cbn in Hvl. lia. 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