proposition: Theorem godel_beta_inv n (v : vec nat n) : { a : nat & { b | forall p, godel_beta a b (pos2nat p) = vec_pos v p } }.
proof: Proof. set (j := S (lmax (n :: vec_list v))). assert (n < j) as Hm1. { apply le_n_S, lmax_prop; left; auto. } assert (forall p, vec_pos v p < j) as Hm2. { intros p; apply le_n_S, lmax_prop. right; apply vec_list_In. } revert Hm1 Hm2; generalize j; clear j. intros j Hj1 Hj2. set (m := vec_set_pos (fun p : pos n => 1+(S (pos2nat p)*fact j))). destruct (CRT_informative m v) as (w & Hw). + intros p; unfold m; rewrite vec_pos_set; discriminate. + intros p q H; unfold m; repeat rewrite vec_pos_set. apply seq_of_coprimes. * generalize (pos2nat_prop p); lia. * generalize (pos2nat_prop q); lia. * contradict H; inversion H. apply pos2nat_inj; auto. + exists w, (fact j). intros p; unfold godel_beta. generalize (Hw p); unfold m; repeat rewrite vec_pos_set. intros E; unfold plus in E; rewrite E. apply rem_idem. apply Nat.lt_le_trans with (1 := Hj2 _). apply Nat.le_trans with (S (1*j)); try lia. apply le_n_S, Nat.mul_le_mono; try lia. apply divides_le. * generalize (fact_gt_0 j); lia. * apply divides_n_fact_n; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd prime binomial) Undecidability.Shared.Libs.DLW.Vec(pos vec)