proposition: Theorem dc_list_h10c_spec l : (exists φ, Forall (dc_eval φ ν) l) <-> (exists Ψ, Forall (fun c => h10c_sem c Ψ) (dc_list_h10c l)).
proof: Proof. split. + intros (phi & Hphi). set (psy n := match div2 n with | (0 , false) => 1 | (S n, false) => n | (n , true) => phi n end). assert (Hpsy_0 : psy 0 = 1) by reflexivity. assert (Hpsy_even : forall n, psy (even n) = n). { intros n. unfold even. replace (2*n+2) with (2*(S n)) by lia. unfold psy; rewrite div2_2p0; trivial. } assert (Hpsy_odd : forall n, psy (odd n) = phi n). { intros n. unfold odd, psy; rewrite div2_2p1; trivial; destruct n; auto. } exists psy. unfold dc_list_h10c; constructor; try reflexivity. apply Forall_app; split; apply Forall_forall. * intros c; rewrite in_map_iff. intros (k & Hk); revert Hk. unfold dc_list_const; rewrite list_an_spec. intros (H1 & H2). unfold h10c_nat in H1. destruct k as [ | k ]; rewrite <- H1; simpl; auto. repeat rewrite Hpsy_even. rewrite Hpsy_0; lia. * intros c; rewrite in_map_iff. intros (k & H1 & H2). rewrite <- H1, <- dc_h10c_equiv with (φ := phi); auto. rewrite Forall_forall in Hphi; auto. + intros (psy & Hpsy). simpl in Hpsy. apply Forall_cons_inv in Hpsy. destruct Hpsy as (H1 & H2). apply Forall_app in H2. destruct H2 as (H2 & H3). rewrite Forall_forall in H2. rewrite Forall_forall in H3. exists (fun n => psy (odd n)). rewrite Forall_forall. intros c Hc. rewrite dc_h10c_equiv with (Ψ := psy); auto. * apply H3, in_map_iff; exists c; auto. * assert (forall n, n <= dc_max l -> h10c_sem (h10c_nat n) psy) as H4. { intros n Hn; apply H2, in_map_iff; exists n; split; auto. apply list_an_spec; lia. } simpl in H1. clear H2 H3. intros n Hn. apply dc_list_const_prop with (1 := Hc) in Hn. apply list_an_spec in Hn. clear Hc. assert (n <= dc_max l) as H5 by lia. clear Hn. revert n H4 H5; generalize (dc_max l). intros m n H2. induction n as [ | n IHn ]; intros Hn; specialize (H2 _ Hn); simpl in H2. - lia. - rewrite IHn, H1 in H2; lia. Qed.
imports: List Arith Lia Max Undecidability.Synthetic.Definitions Undecidability(Shared.Libs.DLW.Utils.utils H10.Dio.dio_logic H10.Dio.dio_elem) Undecidability(H10.FRACTRAN_DIO FRACTRAN.FRACTRAN) Undecidability.DiophantineConstraints.H10C