diff --git a/theories/DiophantineConstraints/H10C_undec.v b/theories/DiophantineConstraints/H10C_undec.v index 0a0076a9d..ef442ddd8 100644 --- a/theories/DiophantineConstraints/H10C_undec.v +++ b/theories/DiophantineConstraints/H10C_undec.v @@ -23,7 +23,7 @@ Require Import Undecidability.Synthetic.ReducibilityFacts. Require Import Undecidability.DiophantineConstraints.H10C. (* For the reduction chain to complement_HaltL_undec *) -From Undecidability.FRACTRAN Require Import FRACTRAN Reductions.MM_FRACTRAN. +From Undecidability.FRACTRAN Require Import FRACTRAN Reductions.MM_FRACTRAN Reductions.FRACTRAN_FRACTRAN. From Undecidability.MinskyMachines Require Import MM Reductions.BSM_MM. From Undecidability.StackMachines Require Import BSM Reductions.SBTM_HALT_to_HaltBSM. Require Import Undecidability.TM.SBTM_undec. diff --git a/theories/FRACTRAN/FRACTRAN/mm_fractran.v b/theories/FRACTRAN/FRACTRAN/mm_fractran.v index 2ab5a9550..256b68628 100644 --- a/theories/FRACTRAN/FRACTRAN/mm_fractran.v +++ b/theories/FRACTRAN/FRACTRAN/mm_fractran.v @@ -151,14 +151,15 @@ Proof with eauto; try lia. 2,3: cbn- [subcode]. 1: intros [] % divides_mult_inv_l. 2: intros [ | ] % divides_mult_inv... * eapply divides_mult_inv in H0 as [? | ?]... - eapply primestream_divides in H0... - eapply divides_encode_state in H0... + -- eapply primestream_divides in H0... + -- eapply divides_encode_state in H0... * eapply primestream_divides in H0... subst. eapply (H n t). eauto. * eapply divides_encode_state in H0... * specialize (IHl (S k)). revert IHl. cbn - [subcode]. ring_simplify (S (k + length l)). - intros IHl. eapply IHl. 2:exact H1. + intros IHl. eapply IHl. + 2:exact H1. intros ? ? ?. eapply H. eapply subcode_cons. eassumption. Qed. diff --git a/theories/FRACTRAN/FRACTRAN/mma_fractran.v b/theories/FRACTRAN/FRACTRAN/mma_fractran.v new file mode 100644 index 000000000..073d4065e --- /dev/null +++ b/theories/FRACTRAN/FRACTRAN/mma_fractran.v @@ -0,0 +1,443 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* Yannick Forster [+] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(* [+] Affiliation Saarland Univ. *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +(* ** Compiler from MM to FRACTRAN *) + +Require Import List Arith Lia Permutation. + +Import ListNotations. + +From Undecidability.Shared.Libs.DLW + Require Import utils utils_tac utils_list utils_nat gcd rel_iter prime + pos vec subcode sss. + +From Undecidability.MinskyMachines.MMA Require Import mma_defs mma_no_self. +From Undecidability.FRACTRAN Require Import FRACTRAN fractran_utils prime_seq FRACTRAN_sss. + +Set Implicit Arguments. + +Tactic Notation "rew" "length" := autorewrite with length_db. + +Local Notation "e #> x" := (vec_pos e x). +Local Notation "e [ v / x ]" := (vec_change e x v). + +Local Notation "I // s -1> t" := (mma_sss I s t). +Local Notation "P /MMA/ s → t" := (sss_step (@mma_sss _) P s t) (at level 70, no associativity). +Local Notation "P /MMA/ s -[ k ]-> t" := (sss_steps (@mma_sss _) P k s t) (at level 70, no associativity). +Local Notation "P /MMA/ s ▹ t" := (sss_output (@mma_sss _) P s t) (at level 70, no associativity). +Local Notation "P /MMA/ s ↓" := (sss_terminates (@mma_sss _) P s) (at level 70, no associativity). + +Local Notation "l /F/ x → y" := (fractran_step l x y) (at level 70, no associativity). +Local Notation "l /F/ x -[ k ]-> y" := (fractran_steps l k x y) (at level 70, no associativity). +Local Notation "l /F/ x ▹ y" := (fractran_eval l x y) (at level 70, no associativity). + +Set Implicit Arguments. + +(* Fractran simulates MMA *) + +(* let a MMA program 1: INC ... k: DEC ... n: _ *) +(* with variables x1...xm *) + +(* we use p1...pn,q1...qm distinct primes and *) +(* encode the state (i,v1,...,vm) *) +(* as p1^0*...*pi^1*...*pn^0*q1^v1*...*qm^vm *) + +(* i: INC xu ---> (qu*p(i+1) / pi) *) +(* i: DEC xu j ---> (pj / pi*qu) and (p(i+1) / pi) (the second constraint should appear AFTER in the list) *) + +Local Definition encode_inc n i (u : pos n) := (ps (i + 1) * qs u, ps i). +Local Definition encode_dec n i (u : pos n) j := (ps j, ps i * qs u). +Local Definition encode_dec2 n i (u : pos n) (_ : nat) := (ps (i + 1), ps i). + +Local Definition encode_one_instr m i (rho : mm_instr (pos m)) := + match rho with + | INC u => encode_inc i u :: nil + | DEC u j => encode_dec i u j :: encode_dec2 i u j :: nil + end. + +Local Fixpoint encode_mma_instr n i (l : list (mm_instr (pos n))) : list (nat * nat) := + match l with + | nil => nil + | rho :: l => encode_one_instr i rho ++ encode_mma_instr (S i) l + end. + +Local Fact encode_mma_instr_app n i l r : @encode_mma_instr n i (l++r) = encode_mma_instr i l + ++ encode_mma_instr (length l+i) r. +Proof. + revert i; induction l as [ | ? ? IHl ]; intros ?; simpl; auto; rewrite IHl, app_ass. + do 3 f_equal; lia. +Qed. + +Local Fact encode_mma_instr_regular n i l : Forall (fun c => fst c <> 0 /\ snd c <> 0) (@encode_mma_instr n i l). +Proof. + revert i; induction l as [ | [ | ] ]; intro; simpl. + + constructor. + + constructor; auto; unfold encode_inc; simpl; split; + [ apply Nat.neq_mul_0; split | ]; apply prime_neq_0; apply nthprime_prime. + + constructor; [ | constructor ]; auto; split; unfold encode_dec, encode_dec2; simpl. + 2: apply Nat.neq_mul_0; split. + all: apply prime_neq_0; apply nthprime_prime. +Qed. + +Local Fact encode_mma_instr_regular' n i l : fractran_regular (@encode_mma_instr n i l). +Proof. generalize (encode_mma_instr_regular i l); apply Forall_impl; tauto. Qed. + +Local Fact encode_mma_instr_in_inv n i P el c er : + @encode_mma_instr n i P = el++c::er + -> exists l rho r, P = l++rho::r /\ In c (encode_one_instr (length l+i) rho). +Proof. + revert i el c er; induction P as [ | rho P IHP ]; simpl; intros i el c er H. + + now destruct el. + + destruct list_app_cons_eq_inv with (1 := H) + as [ (m & H1 & H2) | (m & H1 & H2) ]. + * destruct IHP with (1 := H2) as (l & rho' & r & G1 & G2). + exists (rho::l), rho', r; subst; split; auto. + eq goal G2; do 2 f_equal; simpl; lia. + * exists nil, rho, P; split; simpl; auto. + rewrite <- H1; apply in_or_app; simpl; auto. +Qed. + +Local Notation divides_mult_inv := prime_div_mult. + +Local Ltac inv H := inversion H; subst; clear H. + +(* ps n = nthprime (2n); sq = nthprim (2n+1) *) + +Local Lemma ps_prime n : prime (ps n). +Proof. apply nthprime_prime. Qed. + +#[local] Opaque ps qs. + +(* The divisibility results are no so complicated when + we do not need to show that encode_state is injective ... *) + +Local Fact divides_from_eq x y t : x*y = t -> divides x t. +Proof. intros <-; apply divides_mult_r, divides_refl. Qed. + +Local Fact prime_div_mult3 p x y z : prime p -> divides p (x*y*z) -> divides p x \/ divides p y \/ divides p z. +Proof. intros ? [ [] % prime_div_mult | ] % prime_div_mult; auto. Qed. + +Local Fact prime_div_mult4 p w x y z : prime p -> divides p (w*x*y*z) -> divides p w \/ divides p x \/ divides p y \/ divides p z. +Proof. intros ? [ [] % prime_div_mult | ] % prime_div_mult3; auto. Qed. + +(** Gödel encoding if MMA states as numbers *) + +Local Definition encode_state {n} (c : nat * vec nat n) := ps (fst c) * exp 0 (snd c). + +Local Lemma divides_ps_encode_state i k n (v : vec nat n) : + divides (ps i) (encode_state (k,v)) <-> i = k. +Proof. + unfold encode_state; split. + * induction v as [ | n x v IHv ]. + - simpl; replace (ps k * 1) with (ps k) by lia. + apply primestream_divides. + - simpl; intros [ H | [ H | H ] % divides_mult_inv ] % divides_mult_inv; eauto. + + now eapply primestream_divides in H. + + now apply divides_pow, ps_qs_div in H; auto. + + now eapply ps_exp in H. + * intros <-; simpl; apply divides_mult_r, divides_refl. +Qed. + +Local Lemma divides_qs_encode_state i k n (v : vec nat n) : + divides (qs i) (encode_state (k,v)) <-> divides (qs i) (exp 0 v). +Proof. + split. + - intros [ | ] % divides_mult_inv; eauto. + now eapply qs_ps_div in H. + - intros. + unfold encode_state. + now eapply divides_mult. +Qed. + +Local Lemma qs_encode_state i n (u : pos n) (v : vec nat n) : + divides (qs u) (encode_state (i,v)) <-> v#>u > 0. +Proof. + rewrite divides_qs_encode_state. + enough (forall i, divides (qs (i + u)) (exp i v) <-> v #> u > 0). + 1: eapply H. + intros j; revert u; induction v as [ | x n v IHv ]; intros u; invert pos u. + - cbn; rewrite pos2nat_fst, Nat.add_0_r. + split. + * intros [ H | H ] % divides_mult_inv; eauto. + + destruct x; try lia; cbn in H. + apply divides_1_inv in H. + generalize (str_prime qs j); rewrite H. + intros [] % not_prime_1. + + now apply qs_exp_div in H; auto. + * intros H; destruct x as [|x]; try lia; clear H. + simpl; apply divides_mult_r, divides_mult_r, divides_refl. + - rewrite <- IHv, pos2nat_nxt. + rewrite qs_shift with (m := 1). + simpl. + replace (j+S (pos2nat u)) with (S (j+u)). + 2: now rewrite (plus_comm _ (S _)); simpl; rewrite plus_comm. + split; intros H. + * apply divides_mult_inv in H as [ | ]; auto. eauto. + apply divides_pow in H; auto. + apply primestream_divides in H; lia. + * now apply divides_mult. +Qed. + +Local Lemma encode_state_inj n st1 st2 : + @encode_state n st1 = @encode_state n st2 -> st1 = st2. +Proof. + intros H. + destruct st1 as (i1, v1), st2 as (i2, v2). + assert (i1 = i2); subst. + - eapply divides_ps_encode_state. rewrite <- H. + unfold encode_state. cbn. rewrite mult_comm. eapply divides_mult, divides_refl. + - f_equal. unfold encode_state in H. cbn in H. + replace (ps i2) with (ps i2 ^ 1) in H by (cbn; lia). + eapply power_factor_uniq in H as [_ H]. + + eapply exp_inj. eauto. + + pose proof (ps_prime i2) as ? % prime_ge_2. lia. + + eapply ps_exp. + + eapply ps_exp. +Qed. + +(** Skiping over leading fractions *) + +Local Lemma skip_steps n k l r (v : vec _ n) st : + @mma_no_self_loops n (k, l ++ r) + -> encode_mma_instr (k + length l) r /F/ encode_state (k + length l,v) → encode_state st + -> encode_mma_instr k (l ++ r) /F/ encode_state (k + length l,v) → @encode_state n st. +Proof with eauto; try lia. + revert k. + induction l as [ | rho l IHl ]; cbn - [subcode] in *; intros k. + - ring_simplify (k + 0); auto. + - ring_simplify (k + S (length l)). + intros Hk H. + destruct rho as [ u | u j ]. + + constructor 2. + * intros [[ H1 | H1 ] % divides_mult_inv | H1 ] % divides_mult_inv; eauto. + -- apply primestream_divides in H1; lia. + -- now apply ps_qs_div in H1. + -- apply divides_ps_encode_state in H1; lia. + * specialize IHl with (k := 1+k). + revert IHl; cbn - [subcode]; ring_simplify (S (k + length l)); intros IHl. + apply IHl; trivial. + revert Hk; apply mma_no_self_loops_cons_inv. + + repeat constructor 2. + * intros [[H1|H1] % divides_mult_inv [H2|H2] % divides_mult_inv ] % divides_mult_inv_l... + -- now apply qs_ps_div in H2. + -- apply primestream_divides in H1; subst. + eapply (Hk j u); auto. + -- now apply qs_ps_div in H2. + -- apply divides_ps_encode_state in H1... + * intros [H1|H1] % divides_mult_inv... + -- apply primestream_divides in H1... + -- apply divides_ps_encode_state in H1... + * specialize (IHl (S k)). + revert IHl; cbn - [subcode]; ring_simplify (S (k + length l)); intros IHl. + apply IHl; trivial. + revert Hk; apply mma_no_self_loops_cons_inv. +Qed. + +Local Hint Resolve encode_mma_instr_regular' : core. + +Section steps_forward. + + Variable (n i : _) (P : list (mm_instr (pos _))) + (HP : @mma_no_self_loops n (i,P)). + + Local Lemma one_step_forward st1 st2 : + (i,P) /MMA/ st1 → st2 + -> encode_mma_instr i P /F/ encode_state st1 → encode_state st2. + Proof using HP. + intros (k & l & rho & r & v & H1 & H2 & H3). + inversion H1; subst i P; clear H1. + destruct H3 as [ i x v1 | i x j v1 | i x j v1 u ]; + inversion H2; subst i v1; clear H2; + apply skip_steps; auto. + + constructor. + ring_simplify. + replace (1 + (k + length l)) with (k + length l + 1) by lia. + unfold encode_state, fst, snd. + rewrite vec_prod_mult. + rewrite Nat.add_0_r; ring. + + simpl; constructor 2. + * intros [H2 H3] % divides_mult_inv_l... + eapply divides_mult_inv in H3 as [ H3 | H3 ]; auto... + -- now apply qs_ps_div in H3. + -- apply qs_encode_state in H3; lia. + * constructor. + unfold encode_state, fst, snd. + replace (k + length l + 1) with (S (k + length l)); ring. + + simpl; constructor. + unfold encode_state, fst, snd. + rewrite <- vec_prod_div with (1 := H), Nat.add_0_r; ring. + Qed. + + Local Lemma steps_forward k st1 st2 : + (i,P) /MMA/ st1 -[k]-> st2 + -> encode_mma_instr i P /F/ encode_state st1 -[k]-> encode_state st2. + Proof using HP. + induction 1 as [ st1 | k st1 st2 st3 H1 H2 IH2 ]. + + simpl; reflexivity. + + exists (encode_state st2); split; auto. + now apply one_step_forward. + Qed. + +End steps_forward. + +Section steps_backward. + + Variable (n i : _) (P : list (mm_instr (pos _))) + (HP : @mma_no_self_loops n (i,P)). + + (* Since /F/ is functional and /MMA/ is total, we can use forward + steps to recover backward steps *) + + Local Lemma one_step_backward i1 v1 st : + encode_mma_instr i P /F/ encode_state (i1,v1) → st + -> exists i2 v2, st = encode_state (i2,v2) + /\ (i,P) /MMA/ (i1,v1) → (i2,v2). + Proof using HP. + intros H2. + destruct fractran_step_inv with (1 := H2) + as (el & p & q & er & H3 & H4 & H5). + apply divides_from_eq in H5. + (* we search the instruction which generates p/q *) + destruct encode_mma_instr_in_inv with (1 := H3) + as (l & rho & r & -> & G2). + (* the initial PC must be at instruction rho *) + assert (length l + i = i1) as E. + { apply divides_ps_encode_state with (v := v1). + unfold encode_one_instr in G2. + destruct rho as [ u | u j ]; unfold encode_inc, encode_dec, encode_dec2 in G2; + [ destruct G2 as [ G2 | [] ] | destruct G2 as [ G2 | [ G2 | [] ] ] ]; + inversion G2; subst p q; clear G2; + repeat rewrite mult_assoc in H5. + * apply prime_div_mult3 in H5 as [ H5 | [ H5 | H5 ] ]; auto. + + apply primestream_divides in H5; lia. + + now apply ps_qs_div in H5. + * apply divides_mult_inv_l in H5 as [ H5 _ ]. + apply prime_div_mult in H5 as [ H5 | H5 ]; auto. + apply primestream_divides in H5; subst j. + destruct HP with (length l+i) u; auto. + * apply prime_div_mult in H5 as [ H5 | H5 ]; auto. + apply primestream_divides in H5; lia. } + destruct mma_sss_total with (ii := rho) (s := (i1,v1)) + as ((i2 & v2) & H7). + exists i2, v2. + assert ((i, l++rho::r) /MMA/ (i1,v1) → (i2,v2)) as H8. + { apply in_sss_step; auto; simpl; lia. } + split; auto. + apply one_step_forward in H8; auto. + revert H2 H8; apply fractran_step_fun; auto. + Qed. + + Local Lemma steps_backward k i1 v1 st : + encode_mma_instr i P /F/ encode_state (i1,v1) -[k]-> st + -> exists i2 v2, (i, P) /MMA/ (i1, v1) -[k]-> (i2,v2) + /\ st = encode_state (i2,v2). + Proof using HP. + revert i1 v1 st; induction k as [ | k IHk ]; intros i1 v1 st H; simpl in H. + - subst; exists i1, v1; split; auto; constructor. + - destruct H as (st1 & H2 & H3). + destruct one_step_backward with (1 := H2) + as (i2 & v2 & -> & H5); auto. + destruct IHk with (1 := H3) as (i3 & v3 & ? & ->). + exists i3, v3; split; auto. + constructor 2 with (i2,v2); auto. + Qed. + +End steps_backward. + +Theorem mma_fractran_simulation n P v : + @mma_no_self_loops n (1,P) + -> (1,P) /MMA/ (1,v) ↓ + <-> encode_mma_instr 1 P /F/ ps 1 * exp 0 v ↓. +Proof. + intros HP. + change (ps 1* exp 0 v) with (encode_state (1,v)). + split. + + intros ((j,w) & (k & H1) & H2); simpl fst in *. + exists (encode_state (j,w)); split. + * exists k; apply steps_forward in H1; auto. + * intros x Hx. + destruct one_step_backward with (2 := Hx) + as (i2 & v2 & -> & ?); auto. + revert H; apply sss_out_step_stall; auto. + + intros (st & (k & H1) & H2). + destruct steps_backward with (2 := H1) + as (i2 & v2 & H3 & ->); auto. + exists (i2,v2); split. + * exists k; auto. + * simpl fst. + destruct (in_out_code_dec i2 (1,P)) as [ H4 | H4 ]; auto; exfalso. + destruct in_code_subcode with (1 := H4) as (rho & l & r & G1 & G2). + destruct (mma_sss_total rho (i2,v2)) as ((i3,v3) & G3). + apply H2 with (encode_state (i3,v3)). + apply one_step_forward; auto. + subst P; apply in_sss_step; auto. +Qed. + +Theorem mma_fractran_simulation_forward n P v j v' : + @mma_no_self_loops n (1,P) + -> (1,P) /MMA/ (1,v) ▹ (j,v') -> encode_mma_instr 1 P /F/ ps 1 * exp 0 v ▹ encode_state (j,v'). +Proof. + intros HP. + change (ps 1* exp 0 v) with (encode_state (1,v)). + intros ((k & H1) & H2); simpl fst in *. + rewrite eval_iff. split. + * exists k; apply steps_forward in H1; auto. + * intros x Hx. + destruct one_step_backward with (2 := Hx) + as (i2 & v2 & -> & ?); auto. + revert H; apply sss_out_step_stall; auto. +Qed. + +Theorem mma_fractran_simulation_strong n P v j v' : + @mma_no_self_loops n (1, P) + -> (1,P) /MMA/ (1,v) ▹ (j, v') <-> encode_mma_instr 1 P /F/ ps 1 * exp 0 v ▹ encode_state (j, v'). +Proof. + intros HP. + change (ps 1* exp 0 v) with (encode_state (1,v)). + split. + - now eapply mma_fractran_simulation_forward. + - intros [H1 H2] % eval_iff. + edestruct mma_fractran_simulation as [_ [[j' w] Hw]]; [ eauto | eexists; eauto | ]. + pose proof (Hw' := Hw). + eapply mma_fractran_simulation_forward in Hw as [Hw1 Hw2] % eval_iff; [ | eauto]. + eapply fractran_compute_fun in H1; eauto. + enough ((j', w) = (j, v')) as <- by eassumption. + eapply encode_state_inj in H1; eauto. +Qed. + +Theorem mma_fractran_not_zero n (P : list (mm_instr (pos n))) : + { l | Forall (fun c => fst c <> 0 /\ snd c <> 0) l + /\ forall v, (1,P) /MMA/ (1,v) ↓ <-> l /F/ ps 1 * exp 0 v ↓ }. +Proof. + destruct mma_remove_self_loops with (P := P) as (Q & H1 & _ & H2). + exists (encode_mma_instr 1 Q); split. + + apply encode_mma_instr_regular. + + intros x. + rewrite H2, mma_fractran_simulation; tauto. +Qed. + +Theorem mma_fractran_n n (P : list (mm_instr (pos n))) : + { l | Forall (fun c => snd c <> 0) l + /\ forall v, (1,P) /MMA/ (1,v) ↓ <-> l /F/ ps 1 * exp 0 v ↓ }. +Proof. + destruct (mma_fractran_not_zero P) as (l & H1 & H2). + exists l; split; auto. + revert H1; apply Forall_impl; intros; tauto. +Qed. + +Theorem mma_fractran n (P : list (mm_instr (pos (S n)))) : + { l | forall x, (1,P) /MMA/ (1,x##vec_zero) ↓ <-> l /F/ 5*3^x ↓ }. +Proof. + destruct mma_fractran_n with (P := P) as (l & _ & Hl). + rewrite <- ps_1, <- qs_0. + exists l; intros x; rewrite Hl; simpl. + rewrite exp_zero, Nat.mul_1_r; tauto. +Qed. diff --git a/theories/FRACTRAN/FRACTRAN_undec.v b/theories/FRACTRAN/FRACTRAN_undec.v index 1699c85f5..75f727b46 100644 --- a/theories/FRACTRAN/FRACTRAN_undec.v +++ b/theories/FRACTRAN/FRACTRAN_undec.v @@ -17,7 +17,7 @@ From Undecidability.MinskyMachines Require Import MM MM_undec. From Undecidability.FRACTRAN - Require Import FRACTRAN Reductions.MM_FRACTRAN FRACTRAN_sss. + Require Import FRACTRAN MM_FRACTRAN FRACTRAN_FRACTRAN FRACTRAN_sss. Theorem FRACTRAN_REG_undec : undecidable FRACTRAN_REG_HALTING. Proof. diff --git a/theories/FRACTRAN/Reductions/FRACTRAN_FRACTRAN.v b/theories/FRACTRAN/Reductions/FRACTRAN_FRACTRAN.v new file mode 100644 index 000000000..ed53e9e36 --- /dev/null +++ b/theories/FRACTRAN/Reductions/FRACTRAN_FRACTRAN.v @@ -0,0 +1,52 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* Yannick Forster [+] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(* [+] Affiliation Saarland Univ. *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +From Undecidability.FRACTRAN + Require Import FRACTRAN FRACTRAN_sss prime_seq. + +Require Import Undecidability.Synthetic.Definitions. +Require Import Undecidability.Synthetic.ReducibilityFacts. + +Set Implicit Arguments. + +Section FRACTRAN_ALT_HALTING_HALTING. + + Let f : FRACTRAN_ALT_PROBLEM -> FRACTRAN_PROBLEM. + Proof. + intros (l & n & v). + exact (l,(ps 1 * exp 1 v)). + Defined. + + Theorem FRACTRAN_ALT_HALTING_HALTING : FRACTRAN_ALT_HALTING ⪯ Halt_FRACTRAN. + Proof. + exists f; intros (n & P & v). + rewrite Halt_FRACTRAN_iff. simpl. firstorder. + Qed. + +End FRACTRAN_ALT_HALTING_HALTING. + +Check FRACTRAN_ALT_HALTING_HALTING. + +Section FRACTRAN_REG_FRACTRAN_HALTING. + + Let f : FRACTRAN_REG_PROBLEM -> FRACTRAN_PROBLEM. + Proof. + intros (l & v & _); exact (l,v). + Defined. + + Theorem FRACTRAN_REG_FRACTRAN_HALTING : FRACTRAN_REG_HALTING ⪯ Halt_FRACTRAN. + Proof. + exists f; intros (n & P & v). rewrite Halt_FRACTRAN_iff. tauto. + Qed. + +End FRACTRAN_REG_FRACTRAN_HALTING. + +Check FRACTRAN_REG_FRACTRAN_HALTING. diff --git a/theories/FRACTRAN/Reductions/MMA_FRACTRAN.v b/theories/FRACTRAN/Reductions/MMA_FRACTRAN.v new file mode 100644 index 000000000..acc843c39 --- /dev/null +++ b/theories/FRACTRAN/Reductions/MMA_FRACTRAN.v @@ -0,0 +1,51 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +From Undecidability.Shared.Libs.DLW + Require Import pos vec sss. + +From Undecidability.MinskyMachines + Require Import mma_defs. + +From Undecidability.FRACTRAN + Require Import FRACTRAN fractran_utils mma_fractran prime_seq FRACTRAN_sss FRACTRAN_FRACTRAN. + +Require Import Undecidability.Synthetic.Definitions. +Require Import Undecidability.Synthetic.ReducibilityFacts. + +Set Implicit Arguments. + +Section MMA_HALTING_FRACTRAN_REG_HALTING. + + Variable n : nat. + + Let f : MMA_PROBLEM n -> FRACTRAN_REG_PROBLEM. + Proof. + intros (P & v); red. + destruct (mma_fractran_n P) as (l & H1 & _). + exists l, (ps 1 * exp 0 v); assumption. + Defined. + + Theorem MMA_FRACTRAN_REG_HALTING : MMA_HALTING n ⪯ FRACTRAN_REG_HALTING. + Proof. + exists f; intros (P & v); simpl. + destruct (mma_fractran_n P) as (l & H1 & H2); simpl; auto. + apply H2. + Qed. + +End MMA_HALTING_FRACTRAN_REG_HALTING. + +Corollary MMA_FRACTRAN_HALTING n : MMA_HALTING n ⪯ Halt_FRACTRAN. +Proof. + eapply reduces_transitive. apply MMA_FRACTRAN_REG_HALTING. + apply FRACTRAN_REG_FRACTRAN_HALTING. +Qed. + +Check MMA_FRACTRAN_HALTING. + diff --git a/theories/FRACTRAN/Reductions/MM_FRACTRAN.v b/theories/FRACTRAN/Reductions/MM_FRACTRAN.v index 34e25c207..c48c32421 100644 --- a/theories/FRACTRAN/Reductions/MM_FRACTRAN.v +++ b/theories/FRACTRAN/Reductions/MM_FRACTRAN.v @@ -16,7 +16,7 @@ From Undecidability.MinskyMachines Require Import mm_defs. From Undecidability.FRACTRAN - Require Import FRACTRAN fractran_utils mm_fractran prime_seq FRACTRAN_sss. + Require Import FRACTRAN fractran_utils mm_fractran prime_seq FRACTRAN_sss FRACTRAN_FRACTRAN. Require Import Undecidability.Synthetic.Definitions. Require Import Undecidability.Synthetic.ReducibilityFacts. @@ -43,22 +43,6 @@ Section MM_HALTING_FRACTRAN_ALT_HALTING. End MM_HALTING_FRACTRAN_ALT_HALTING. -Section FRACTRAN_ALT_HALTING_HALTING. - - Let f : FRACTRAN_ALT_PROBLEM -> FRACTRAN_PROBLEM. - Proof. - intros (l & n & v). - exact (l,(ps 1 * exp 1 v)). - Defined. - - Theorem FRACTRAN_ALT_HALTING_HALTING : FRACTRAN_ALT_HALTING ⪯ Halt_FRACTRAN. - Proof. - exists f; intros (n & P & v). - rewrite Halt_FRACTRAN_iff. simpl. firstorder. - Qed. - -End FRACTRAN_ALT_HALTING_HALTING. - Corollary MM_FRACTRAN_HALTING : Halt_MM ⪯ Halt_FRACTRAN. Proof. eapply reduces_transitive. apply MM_FRACTRAN_ALT_HALTING. @@ -85,18 +69,3 @@ End MM_HALTING_FRACTRAN_REG_HALTING. Check MM_FRACTRAN_REG_HALTING. -Section FRACTRAN_REG_FRACTRAN_HALTING. - - Let f : FRACTRAN_REG_PROBLEM -> FRACTRAN_PROBLEM. - Proof. - intros (l & v & _); exact (l,v). - Defined. - - Theorem FRACTRAN_REG_FRACTRAN_HALTING : FRACTRAN_REG_HALTING ⪯ Halt_FRACTRAN. - Proof. - exists f; intros (n & P & v). rewrite Halt_FRACTRAN_iff. tauto. - Qed. - -End FRACTRAN_REG_FRACTRAN_HALTING. - -Check FRACTRAN_REG_FRACTRAN_HALTING. diff --git a/theories/FRACTRAN/Util/prime_seq.v b/theories/FRACTRAN/Util/prime_seq.v index f0402f743..c7549f681 100644 --- a/theories/FRACTRAN/Util/prime_seq.v +++ b/theories/FRACTRAN/Util/prime_seq.v @@ -219,6 +219,9 @@ Proof. intros; apply nthprime_inj in H; lia. Defined. +Fact ps_0 : ps 0 = 2. +Proof. simpl; apply nthprime_0. Qed. + Fact ps_1 : ps 1 = 5. Proof. simpl; apply nthprime_2. Qed. @@ -228,6 +231,9 @@ Proof. intros; apply nthprime_inj in H; lia. Defined. +Fact qs_0 : qs 0 = 3. +Proof. simpl; apply nthprime_1. Qed. + Fact qs_1 : qs 1 = 7. Proof. simpl; apply nthprime_3. Qed. diff --git a/theories/MinskyMachines/MM/mm_defs.v b/theories/MinskyMachines/MM/mm_defs.v index 89adc61e3..f9709cc2e 100644 --- a/theories/MinskyMachines/MM/mm_defs.v +++ b/theories/MinskyMachines/MM/mm_defs.v @@ -41,7 +41,7 @@ Section Minsky_Machine. rewrite H in H6; discriminate. rewrite H in H6; inversion H6; subst; auto. Qed. - + Fact mm_sss_total ii s : { t | ii // s -1> t }. Proof. destruct s as (i,v). @@ -50,6 +50,9 @@ Section Minsky_Machine. * exists (j,v); constructor; auto. * exists (1+i,v[k/x]); constructor; auto. Qed. + + Fact mm_sss_total_ni ii s : exists t, ii // s -1> t. + Proof. destruct (mm_sss_total ii s); eauto. Qed. Fact mm_sss_INC_inv x i v j w : INC x // (i,v) -1> (j,w) -> j=1+i /\ w = v[(S (v#>x))/x]. Proof. inversion 1; subst; auto. Qed. diff --git a/theories/MinskyMachines/MM/mm_no_self.v b/theories/MinskyMachines/MM/mm_no_self.v index aa065b1f2..0501952d9 100644 --- a/theories/MinskyMachines/MM/mm_no_self.v +++ b/theories/MinskyMachines/MM/mm_no_self.v @@ -430,24 +430,6 @@ Section remove_self_loops. * destruct G1 as [ (? & _) | [ (? & _) | (? & _) ] ]; simpl in H5; lia. Qed. - Theorem mm_remove_self_loops : { Q | mm_no_self_loops (1,Q) - /\ (forall i x j, (i,DEC x j::nil) j < 1+length Q) - /\ forall v, (1,P) // (1,v) ↓ <-> (1,Q) // (1,0##v) ↓ }. - Proof. - destruct (eq_nat_dec lP 0) as [ HlP | HlP ]. - + exists nil. - split; [ | split ]. - - intros i rho ([ | ] & ? & ? & ?); discriminate. - - intros i x j ([ | ] & ? & ? & ?); discriminate. - - destruct P; try discriminate. - split. - * exists (1,0##v); split; simpl; try lia; mm sss stop. - * exists (1,v); split; simpl; try lia; mm sss stop. - + exists Q; split; auto; split; auto; intros v; split. - * intros (s0 & H); revert H; apply P_imp_Q; simpl; lia. - * intros (s0 & H); revert H; apply Q_imp_P; simpl; lia. - Qed. - Theorem mm_remove_self_loops_strong : { Q | mm_no_self_loops (1,Q) /\ (forall i x j, (i,DEC x j::nil) j < 1+length Q) /\ (forall v w, (exists j, (1,P) // (1,v) ~~> (j, w)) -> (exists j, (1,Q) // (1,0##v) ~~> (j, 0 ## w))) @@ -470,39 +452,34 @@ Section remove_self_loops. * intros v (s0 & H); revert H; apply Q_imp_P; simpl; lia. Qed. + Theorem mm_remove_self_loops : { Q | mm_no_self_loops (1,Q) + /\ (forall i x j, (i,DEC x j::nil) j < 1+length Q) + /\ forall v, (1,P) // (1,v) ↓ <-> (1,Q) // (1,0##v) ↓ }. + Proof. + destruct mm_remove_self_loops_strong as (Q' & H1 & H2 & H3 & H4). + exists Q'; msplit 2; auto. + intros v; split; auto. + intros ((j,w) & Hw). + destruct (H3 v w) as (j' & Hj'); eauto. + now exists (j',0##w). + Qed. + Theorem mm_remove_self_loops_strong' : { Q | mm_no_self_loops (1,Q) /\ (forall i x j, (i,DEC x j::nil) j < 1+length Q) /\ forall v w, (exists j, (1,P) // (1,v) ~~> (j, w)) <-> (exists j, (1,Q) // (1,0##v) ~~> (j, 0 ## w)) }. Proof. - destruct (eq_nat_dec lP 0) as [ HlP | HlP ]. - + exists nil. - split; [ | split ]. - - intros i rho ([ | ] & ? & ? & ?); discriminate. - - intros i x j ([ | ] & ? & ? & ?); discriminate. - - destruct P; try discriminate. - split. - * exists 1. split; simpl; try lia; mm sss stop. - destruct H as [j [[i Hj] ?]]. - eapply sss_steps_stall in Hj as [_ [=]]. 2:cbn; lia. now subst. - * exists 1. split; simpl; try lia; mm sss stop. - destruct H as [j [[i Hj] ?]]. - eapply sss_steps_stall in Hj as [_ ? % (f_equal snd) % (f_equal (@vec_tail _ _))]. cbn in H0. congruence. - cbn; lia. - + exists Q; split; auto; split; auto; intros v; split. - * intros [j H]. exists 0. - eapply (@P_imp_Q_strong (1,v) (j,w)); simpl; try lia; eauto. - * intros [j H]. - destruct (@Q_imp_P (1, 0 ## v) (j, 0 ## w)) as [[j' w'] H2]; eauto. - -- simpl; lia. - -- exists j'. cbn in H2. enough (w' = w) as <- by eauto. - eapply P_imp_Q_strong in H2. - 2: simpl; lia. cbn in H2. - destruct H2 as [H2 ?]. destruct H as [H ?]. - eapply sss_compute_fun in H; eauto. - eapply (f_equal snd) in H. - cbn in H. - eapply (f_equal (@vec_tail _ _)) in H. - exact H. eapply mm_sss_fun. + destruct mm_remove_self_loops_strong as (Q' & H1 & H2 & H3 & H4). + exists Q'; msplit 2; auto. + intros v w; split; auto. + intros (j & Hj). + destruct (H4 v) as ((i,w') & Hiw'). + + now exists (j,0##w). + + destruct (H3 v w') as (i' & Hi'); eauto. + exists i. + generalize (sss_output_fun (@mm_sss_fun _) Hj Hi'); intros E. + apply f_equal with (f := snd), vec_cons_inv, proj2 in E; simpl in E; subst; auto. Qed. End remove_self_loops. + + \ No newline at end of file diff --git a/theories/MinskyMachines/MM/mm_no_self_alt.v b/theories/MinskyMachines/MM/mm_no_self_alt.v new file mode 100644 index 000000000..aa161cff6 --- /dev/null +++ b/theories/MinskyMachines/MM/mm_no_self_alt.v @@ -0,0 +1,243 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +(* * Minsky machines to FRACTRAN programs *) +(* ** Removal of self-loops in MMAs using syntactic and semantic + properties of the generic compiler *) + +Require Import List Arith Lia. + +Import ListNotations. + +From Undecidability.Shared.Libs.DLW + Require Import utils pos vec subcode sss compiler compiler_correction. + +From Undecidability.MinskyMachines.MM + Require Import mm_defs. + +Set Implicit Arguments. + +Tactic Notation "rew" "length" := autorewrite with length_db. + +Local Notation "e #> x" := (vec_pos e x). +Local Notation "e [ v / x ]" := (vec_change e x v). (* clashes with ListNotations below *) + +Local Notation "I // s -1> t" := (mm_sss I s t). +Local Notation "P // s -+> t" := (sss_progress (@mm_sss _) P s t). +Local Notation "P // s ->> t" := (sss_compute (@mm_sss _) P s t). +Local Notation "P // s ~~> t" := (sss_output (@mm_sss _) P s t). +Local Notation "P // s ↓" := (sss_terminates (@mm_sss _) P s). + +Section no_self_loops. + + Variables (n : nat). + + Definition mm_no_self_loops (Q : nat * list (mm_instr (pos n))) := + forall i x, ~ (i,[DEC x i]) mm_no_self_loops (length P+i,Q) + -> mm_no_self_loops (i,P++Q). + Proof. + intros H1 H2 j x H. + apply subcode_app_invert_right in H. + destruct H as [ H | H ]; revert H. + + apply H1. + + apply H2. + Qed. + + Fact mm_no_self_loops_cons_inv i ρ P : + mm_no_self_loops (i,ρ::P) + -> mm_no_self_loops (1+i,P). + Proof. + intros H j x Hj. + now apply (H j x), subcode_cons. + Qed. + +End no_self_loops. + +Section remove_self_loops. + + Variable (n : nat). + + Implicit Type ρ : mm_instr (pos n). + + Local Definition il ρ := + match ρ with + | INC x => 1 + | DEC x j => 3 + end. + + Section instr_compiler. + + Variable (lnk : nat -> nat). + + Local Definition ic i ρ := + match ρ with + | INC x => [ INC (pos_nxt x) ] + | DEC x j => [ DEC (pos_nxt x) (2+lnk i) ; + DEC pos0 (3+lnk i) ; + DEC pos0 (lnk j) ] + end. + + Local Fact il_ic_length i ρ : length (ic i ρ) = il ρ. + Proof. now destruct ρ. Qed. + + Local Fact il_le ρ : 1 <= il ρ. + Proof. destruct ρ; simpl; lia. Qed. + + End instr_compiler. + + Hint Resolve subcode_refl : core. + + Let simul (v : vec nat n) (w : vec nat (S n)) := w#>pos0 = 0 /\ v = vec_tail w. + + Local Fact ic_correct : instruction_compiler_sound ic (@mm_sss _) (@mm_sss _) simul. + Proof. + intros lnk I i1 v1 i2 v2 w1. + change i1 with (fst (i1,v1)) at 2 3 4 5 6 7. + change i2 with (fst (i2,v2)) at 2. + change v1 with (snd (i1,v1)) at 5. + change v2 with (snd (i2,v2)) at 3. + generalize (i1,v1) (i2,v2); intros st1 st2; clear i1 v1 i2 v2. + induction 1 as [ i x v | i x k v H | i x k v u H ]; simpl. + + intros -> [H1 ->]; rew vec. + exists (vec_change w1 (pos_nxt x) (S (w1#>(pos_nxt x)))); msplit 2; rew vec; auto. + * mm sss INC with (pos_nxt x). + mm sss stop. + * clear H1; vec split w1 with y; rew vec. + + vec split w1 with y; intros H1 [H2 H3]. + revert H2 H3; simpl; rew vec; intros -> ->. + exists (0##w1); msplit 2; auto. + mm sss DEC zero with (pos_nxt x) (S (S (lnk i))). + mm sss DEC zero with pos0 (lnk k). + mm sss stop. + + vec split w1 with y; intros H1 [H2 H3]. + revert H2 H3; simpl; rew vec; intros -> ->. + exists (0##vec_change w1 x u); msplit 2; auto. + mm sss DEC S with (pos_nxt x) (S (S (lnk i))) u. + mm sss DEC zero with pos0 (S (S (S (lnk i)))). + mm sss stop. + now simpl; rew vec; f_equal. + Qed. + + Section no_self_loops. + + Let gc := generic_syntactic_compiler _ _ il_le il_ic_length. + + Variables (P : list (mm_instr (pos n))). + + Let Q := cs_code gc (1,P) 1. + + Local Fact gc_no_self_loops : mm_no_self_loops (1,Q). + Proof. + generalize (cs_not_between gc). + destruct gc as [ lnk code H0 H1 H2 H3 H4 H5 H6 ]; simpl; clear gc; intro H7. + intros j x H. + apply H6 in H as (k & [ x' | x' j' ] & G1 & G2); simpl ic in G2. + + apply subcode_cons_invert_right in G2 as [ (_ & ?) | G2 ]; try easy. + now apply subcode_nil_invert in G2. + + repeat apply subcode_cons_invert_right in G2 as [ (E1 & E2) | G2 ]. + * inversion E2; lia. + * inversion E2; lia. + * inversion E2; clear E2. + specialize (H7 (1,P) 1 j' k). + apply H2 with (i := 1) in G1; simpl in G1; lia. + * now apply subcode_nil_invert in G2. + Qed. + + Local Fact gc_bounded i x j : (i,DEC x j::nil) j <= 1+length Q. + Proof. + generalize (cs_between gc (1,P) 1); fold Q; intros H10. + destruct gc as [ lnk code H0 H1 H2 H3 H4 H5 H6 ]; clear gc. + simpl in Q, H10. + intros H. + apply H6 in H as (k' & [ x' | x' j' ] & G1 & G2); simpl ic in G2. + + apply subcode_cons_invert_right in G2 as [ (_ & ?) | G2 ]; try easy. + now apply subcode_nil_invert in G2. + + generalize G1; intros G0. + apply H5 with (i := i) in G0; fold Q in G0; apply subcode_length' in G0; simpl in G0. + apply (H2 _ 1) in G1; simpl in G1. + repeat apply subcode_cons_invert_right in G2 as [ (G3 & G4) | G2 ]. + * specialize (H10 (S k')); inversion G4; lia. + * specialize (H10 (S k')); inversion G4; lia. + * specialize (H10 j'); inversion G4; lia. + * now apply subcode_nil_invert in G2. + Qed. + + Hint Resolve il_ic_length ic_correct mm_sss_total_ni : core. + + Let lnk := cs_link gc (1,P) 1. + + Theorem mm_remove_self_loops_strong : { Q | mm_no_self_loops (1,Q) + /\ (forall i x j, (i,DEC x j::nil) j <= 1+length Q) + /\ (forall v w, (exists j, (1,P) // (1,v) ~~> (j, w)) -> (exists j, (1,Q) // (1,0##v) ~~> (j, 0 ## w))) + /\ (forall v, (1,Q) // (1,0##v) ↓ -> (1,P) // (1,v) ↓)}. + Proof. + destruct (eq_nat_dec (length P) 0) as [ HlP | HlP ]. + + (** This is the case where P is empty *) + exists nil; msplit 2. + * intros i rho ([ | ] & ? & ? & ?); discriminate. + * intros i x j ([ | ] & ? & ? & ?); discriminate. + * destruct P; try discriminate. + split. + - exists 1. + split; simpl; try lia; mm sss stop; do 2 f_equal. + destruct H as [j [[i Hj] ?]]. + eapply sss_steps_stall in Hj as [_ [=]]; auto. + simpl; lia. + - intros v [(j, w) H]. + exists (1,v);split; simpl; try lia; mm sss stop. + + exists Q; msplit 3. + * apply gc_no_self_loops. + * apply gc_bounded. + * intros v w (j & Hw). + destruct ((compiler_syntactic_sound_output il_ic_length gc ic_correct (P := (1,P)) 1) 1 v j w (0##v)) as (w' & (H1 & H2) & H3). + - split; auto; split; rew vec. + - revert H1 H2 H3; vec split w' with y; simpl; intros -> <- H3. + exists (cs_link gc (1,P) 1 j). + now rewrite <- (cs_fst gc (1,P) 1) at 2. + * intros v. + apply (compiler_syntactic_term_equiv il_ic_length gc (@mm_sss_total_ni _) (@mm_sss_fun _) ic_correct 1 P 1). + split; rew vec. + Qed. + + Theorem mm_remove_self_loops : { Q | mm_no_self_loops (1,Q) + /\ (forall i x j, (i,DEC x j::nil) j <= 1+length Q) + /\ forall v, (1,P) // (1,v) ↓ <-> (1,Q) // (1,0##v) ↓ }. + Proof. + destruct mm_remove_self_loops_strong as (Q' & H1 & H2 & H3 & H4). + exists Q'; msplit 2; auto. + intros v; split; auto. + intros ((j,w) & Hw). + destruct (H3 v w) as (j' & Hj'); eauto. + now exists (j',0##w). + Qed. + + Theorem mm_remove_self_loops_strong' : { Q | mm_no_self_loops (1,Q) + /\ (forall i x j, (i,DEC x j::nil) j <= 1+length Q) + /\ forall v w, (exists j, (1,P) // (1,v) ~~> (j, w)) <-> (exists j, (1,Q) // (1,0##v) ~~> (j, 0 ## w)) }. + Proof. + destruct mm_remove_self_loops_strong as (Q' & H1 & H2 & H3 & H4). + exists Q'; msplit 2; auto. + intros v w; split; auto. + intros (j & Hj). + destruct (H4 v) as ((i,w') & Hiw'). + + now exists (j,0##w). + + destruct (H3 v w') as (i' & Hi'); eauto. + exists i. + generalize (sss_output_fun (@mm_sss_fun _) Hj Hi'); intros E. + apply f_equal with (f := snd), vec_cons_inv, proj2 in E; simpl in E; subst; auto. + Qed. + + End no_self_loops. + +End remove_self_loops. \ No newline at end of file diff --git a/theories/MinskyMachines/MMA.v b/theories/MinskyMachines/MMA.v index b10707266..4b2201525 100644 --- a/theories/MinskyMachines/MMA.v +++ b/theories/MinskyMachines/MMA.v @@ -77,12 +77,16 @@ Section MMA_problems. Definition MMA_PROBLEM n := (list (mm_instr (pos n)) * vec nat n)%type. - Definition MMA_HALTS_ON_ZERO {n} (P : MMA_PROBLEM n) := (1,fst P) // (1,snd P) ~~> (0,vec_zero). - Definition MMA_HALTING {n} (P : MMA_PROBLEM n) := (1,fst P) // (1,snd P) ↓. + Definition MMA_HALTS_ON_ZERO n (P : MMA_PROBLEM n) := (1,fst P) // (1,snd P) ~~> (0,vec_zero). + Definition MMA_HALTING n (P : MMA_PROBLEM n) := (1,fst P) // (1,snd P) ↓. + + Global Arguments MMA_HALTS_ON_ZERO : clear implicits. + Global Arguments MMA_HALTING : clear implicits. Definition MMA2_PROBLEM := MMA_PROBLEM 2. - Definition MMA2_HALTS_ON_ZERO := @MMA_HALTS_ON_ZERO 2. - Definition MMA2_HALTING := @MMA_HALTING 2. + Definition MMA2_HALTS_ON_ZERO := MMA_HALTS_ON_ZERO 2. + Definition MMA2_HALTING := MMA_HALTING 2. + +End MMA_problems. -End MMA_problems. \ No newline at end of file diff --git a/theories/MinskyMachines/MMA/mma_no_self.v b/theories/MinskyMachines/MMA/mma_no_self.v new file mode 100644 index 000000000..96514ad2a --- /dev/null +++ b/theories/MinskyMachines/MMA/mma_no_self.v @@ -0,0 +1,194 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +(* * Minsky machines to FRACTRAN programs *) +(* ** Removal of self-loops in MMAs using syntactic and semantic + properties of the generic compiler *) + +Require Import List Arith Lia. + +Import ListNotations. + +From Undecidability.Shared.Libs.DLW + Require Import utils pos vec subcode sss compiler compiler_correction. + +From Undecidability.MinskyMachines.MMA + Require Import mma_defs. + +Set Implicit Arguments. + +Tactic Notation "rew" "length" := autorewrite with length_db. + +Local Notation "e #> x" := (vec_pos e x). +Local Notation "e [ v / x ]" := (vec_change e x v). (* clashes with ListNotations below *) + +Local Notation "I // s -1> t" := (mma_sss I s t). +Local Notation "P // s -+> t" := (sss_progress (@mma_sss _) P s t). +Local Notation "P // s ->> t" := (sss_compute (@mma_sss _) P s t). +Local Notation "P // s ↓" := (sss_terminates (@mma_sss _) P s). + +Section no_self_loops. + + Variables (n : nat). + + Definition mma_no_self_loops (Q : nat * list (mm_instr (pos n))) := + forall i x, ~ (i,[DEC x i]) mma_no_self_loops (length P+i,Q) + -> mma_no_self_loops (i,P++Q). + Proof. + intros H1 H2 j x H. + apply subcode_app_invert_right in H. + destruct H as [ H | H ]; revert H. + + apply H1. + + apply H2. + Qed. + + Fact mma_no_self_loops_cons_inv i ρ P : + mma_no_self_loops (i,ρ::P) + -> mma_no_self_loops (1+i,P). + Proof. + intros H j x Hj. + now apply (H j x), subcode_cons. + Qed. + +End no_self_loops. + +Section remove_self_loops. + + Variable (n : nat). + + Implicit Type ρ : mm_instr (pos n). + + Local Definition il ρ := + match ρ with + | INCₐ x => 1 + | DECₐ x j => 5 + end. + + Section instr_compiler. + + Variable (lnk : nat -> nat). + + Local Definition ic i ρ := + match ρ with + | INCₐ x => [ INCₐ x ] + | DECₐ x j => [ DECₐ x (3+lnk i) ; + INCₐ x ; + DECₐ x (5+lnk i) ; + INCₐ x ; + DECₐ x (lnk j) ] + end. + + Local Fact il_ic_length i ρ : length (ic i ρ) = il ρ. + Proof. now destruct ρ. Qed. + + Local Fact il_le ρ : 1 <= il ρ. + Proof. destruct ρ; simpl; lia. Qed. + + End instr_compiler. + + Hint Resolve subcode_refl : core. + + Local Fact ic_correct : instruction_compiler_sound ic (@mma_sss _) (@mma_sss _) eq. + Proof. + intros lnk I i1 v1 i2 v2 w1. + change i1 with (fst (i1,v1)) at 2 3 4 5 6 7. + change i2 with (fst (i2,v2)) at 2. + change v1 with (snd (i1,v1)) at 5. + change v2 with (snd (i2,v2)) at 3. + generalize (i1,v1) (i2,v2); intros st1 st2; clear i1 v1 i2 v2. + induction 1 as [ i x v | i x k v H | i x k v u H ]; simpl. + + intros -> <-. + exists (vec_change v x (S (v#>x))); split; auto. + mma sss INC with x. + mma sss stop. + + intros -> <-. + exists v; split; auto. + mma sss DEC zero with x (S (S (S (lnk i)))). + mma sss INC with x. + mma sss DEC S with x (S (S (S (S (S (lnk i)))))) (v#>x); rew vec. + mma sss stop. + + intros _ <-. + exists (vec_change v x u); split; auto. + mma sss DEC S with x (S (S (S (lnk i)))) u. + mma sss INC with x. + 1: do 2 apply subcode_cons; subcode_tac. + mma sss DEC S with x (lnk k) u; rew vec. + mma sss stop. + Qed. + + Section no_self_loops. + + Let gc := generic_syntactic_compiler _ _ il_le il_ic_length. + + Variables (P : list (mm_instr (pos n))). + + Let Q := cs_code gc (1,P) 1. + + Local Fact gc_no_self_loops : mma_no_self_loops (1,Q). + Proof. + generalize (cs_not_between gc). + destruct gc as [ lnk code H0 H1 H2 H3 H4 H5 H6 ]; simpl; clear gc; intro H7. + intros j x H. + apply H6 in H as (k & [ x' | x' j' ] & G1 & G2); simpl ic in G2. + + apply subcode_cons_invert_right in G2 as [ (_ & ?) | G2 ]; try easy. + now apply subcode_nil_invert in G2. + + repeat apply subcode_cons_invert_right in G2 as [ (E1 & E2) | G2 ]. + * inversion E2; lia. + * easy. + * inversion E2; lia. + * easy. + * inversion E2; clear E2. + specialize (H7 (1,P) 1 j' k). + apply H2 with (i := 1) in G1; simpl in G1; lia. + * now apply subcode_nil_invert in G2. + Qed. + + Local Fact gc_bounded i x j : (i,DEC x j::nil) j <= 1+length Q. + Proof. + generalize (cs_between gc (1,P) 1); fold Q; intros H10. + destruct gc as [ lnk code H0 H1 H2 H3 H4 H5 H6 ]; clear gc. + simpl in Q, H10. + intros H. + apply H6 in H as (k' & [ x' | x' j' ] & G1 & G2); simpl ic in G2. + + apply subcode_cons_invert_right in G2 as [ (_ & ?) | G2 ]; try easy. + now apply subcode_nil_invert in G2. + + generalize G1; intros G0. + apply H5 with (i := i) in G0; fold Q in G0; apply subcode_length' in G0; simpl in G0. + apply (H2 _ 1) in G1; simpl in G1. + repeat apply subcode_cons_invert_right in G2 as [ (G3 & G4) | G2 ]; try easy. + * specialize (H10 (S k')); inversion G4; lia. + * specialize (H10 (S k')); inversion G4; lia. + * specialize (H10 j'); inversion G4; lia. + * now apply subcode_nil_invert in G2. + Qed. + + Hint Resolve il_ic_length ic_correct mma_sss_total_ni : core. + + Let lnk := cs_link gc (1,P) 1. + + Theorem mma_remove_self_loops : { Q | mma_no_self_loops (1,Q) + /\ (forall i x j, (i,DEC x j::nil) j <= 1+length Q) + /\ forall v, (1,P) // (1,v) ↓ <-> (1,Q) // (1,v) ↓ }. + Proof. + exists Q; msplit 2. + + apply gc_no_self_loops. + + apply gc_bounded. + + intros; apply compiler_syntactic_term_equiv with (simul := eq); auto. + * apply mma_sss_total_ni. + * apply mma_sss_fun. + Qed. + + End no_self_loops. + +End remove_self_loops. \ No newline at end of file diff --git a/theories/MinskyMachines/MMA/mma_simul.v b/theories/MinskyMachines/MMA/mma_simul.v index 1001234d3..9dab820a5 100644 --- a/theories/MinskyMachines/MMA/mma_simul.v +++ b/theories/MinskyMachines/MMA/mma_simul.v @@ -34,7 +34,7 @@ Section mma_sim. Variables (n : nat). - (* The identity compiler behaves a relinking the code so that the + (* The identity compiler behaves as relinking the code so that the output PC value is always at the code end *) Definition mma_instr_compile lnk (_ : nat) (ii : mm_instr (pos n)) := @@ -119,11 +119,11 @@ Section mma_mma0_sim. Let Q := proj1_sig (mma_auto_simulator i P). Let HQ := proj2_sig (mma_auto_simulator i P). - Definition mma_mma0_sim := Q ++ mma_null_all _ (length Q+1) ++ mma_jump 0 pos0. + Definition mma_mma0_sim := Q ++ mma_zeroify pos0 (length Q+1). Notation R := mma_mma0_sim. - Hint Rewrite mma_null_all_length : length_db. + Hint Rewrite mma_zeroify_length : length_db. Theorem mma_mma0_sim_spec v : (i,P) //ₐ (i,v) ↓ <-> (1,R) //ₐ (1,v) ~~> (0,vec_zero). Proof. @@ -134,8 +134,8 @@ Section mma_mma0_sim. split; [ | simpl; lia ]. unfold R. apply subcode_sss_compute_trans with (2 := H); auto. - apply subcode_sss_compute_trans with (2 := mma_null_all_spec _ _); auto. - apply subcode_sss_compute with (2 := mma_jump_spec _ pos0 _ _); auto. + apply sss_progress_compute. + apply subcode_sss_progress with (2 := mma_zeroify_spec pos0 _ _); auto. + intros H. apply HQ; fold Q. apply subcode_sss_terminates with (Q := (1,R)). @@ -145,7 +145,12 @@ Section mma_mma0_sim. End mma_mma0_sim. -(* Termination can be simulated with termination on (0,vec_zero) *) +(* Termination can be simulated with termination on (0,vec_zero) + One cannot enforce a jump to PC=0 if there is no register at all + hence the pos (S n) below. + + In case of the registers (pos 0), P must be empty (as would be Q) but + it is not possible for Q=[] to terminate on PC=0 when starting from PC=1 *) Theorem mma2_simulator n i (P : list (mm_instr (pos (S n)))) : { Q | forall v, (i,P) //ₐ (i,v) ↓ <-> (1,Q) //ₐ (1,v) ~~> (0,vec_zero) }. diff --git a/theories/MinskyMachines/MMA/mma_utils.v b/theories/MinskyMachines/MMA/mma_utils.v index 5d911b8a2..9b9cfaaf9 100644 --- a/theories/MinskyMachines/MMA/mma_utils.v +++ b/theories/MinskyMachines/MMA/mma_utils.v @@ -165,6 +165,29 @@ Section Minsky_Machine_alt_utils. End mma_null_all. + Hint Rewrite mma_null_all_length : length_db. + + Section mma_zeroify. + + Variable (x : pos n) (i : nat). + + Definition mma_zeroify := mma_null_all i ++ JUMPₐ 0 x. + + Fact mma_zeroify_length : length mma_zeroify = 2+n. + Proof. unfold mma_zeroify; rew length; lia. Qed. + + Fact mma_zeroify_spec v : (i,mma_zeroify) // (i,v) -+> (0,vec_zero). + Proof. + unfold mma_zeroify. + apply sss_compute_progress_trans with (n+i,vec_zero). + + apply subcode_sss_compute with (P := (i,mma_null_all i)); auto. + apply mma_null_all_spec. + + apply subcode_sss_progress with (P := (n+i,JUMPₐ 0 x)); auto. + now apply mma_jump_progress. + Qed. + + End mma_zeroify. + Section mma_incs. (* Add a constant value k to register x *) diff --git a/theories/MinskyMachines/MMA2_undec.v b/theories/MinskyMachines/MMA2_undec.v index 51cee9ee3..ef4d4a8e5 100644 --- a/theories/MinskyMachines/MMA2_undec.v +++ b/theories/MinskyMachines/MMA2_undec.v @@ -10,7 +10,7 @@ Require Import Undecidability.Synthetic.Undecidability. From Undecidability.FRACTRAN - Require Import FRACTRAN FRACTRAN_undec. + Require Import FRACTRAN FRACTRAN_FRACTRAN FRACTRAN_undec. From Undecidability.MinskyMachines Require Import MMA FRACTRAN_to_MMA2. diff --git a/theories/MinskyMachines/Reductions/BSM_HALTING_to_MMA_zero_HALTING.v b/theories/MinskyMachines/Reductions/BSM_HALTING_to_MMA_zero_HALTING.v new file mode 100644 index 000000000..8df2218ef --- /dev/null +++ b/theories/MinskyMachines/Reductions/BSM_HALTING_to_MMA_zero_HALTING.v @@ -0,0 +1,28 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +From Undecidability.StackMachines Require Import bsm_defs. + +From Undecidability.MinskyMachines Require Import MMA. + +From Undecidability.MinskyMachines + Require BSM_to_MMA_HALTING MMA_to_MMA_zero. + +From Undecidability.Synthetic + Require Import Definitions ReducibilityFacts. + +Theorem reduction n : BSMn_HALTING n ⪯ MMA_HALTS_ON_ZERO (1+n). +Proof. + eapply reduces_transitive. apply BSM_to_MMA_HALTING.reduction. + apply MMA_to_MMA_zero.reduction. +Qed. + + + + diff --git a/theories/MinskyMachines/Reductions/BSM_to_MMA_HALTING.v b/theories/MinskyMachines/Reductions/BSM_to_MMA_HALTING.v index 78449f0ae..0f9da17d4 100644 --- a/theories/MinskyMachines/Reductions/BSM_to_MMA_HALTING.v +++ b/theories/MinskyMachines/Reductions/BSM_to_MMA_HALTING.v @@ -13,8 +13,8 @@ From Undecidability.Shared.Libs.DLW From Undecidability.StackMachines Require Import bsm_defs. -From Undecidability.MinskyMachines.MMA - Require Import mma_defs mma_utils_bsm bsm_mma. +From Undecidability.MinskyMachines + Require Import mma_defs mma_utils_bsm bsm_mma MMA_to_MMA_zero. From Undecidability.Synthetic Require Import Definitions ReducibilityFacts. @@ -28,3 +28,5 @@ Proof. intros; rew vec. Qed. + + diff --git a/theories/MinskyMachines/Reductions/MMA2_to_MMA2_zero.v b/theories/MinskyMachines/Reductions/MMA2_to_MMA2_zero.v index e8555fced..d50ab7daa 100644 --- a/theories/MinskyMachines/Reductions/MMA2_to_MMA2_zero.v +++ b/theories/MinskyMachines/Reductions/MMA2_to_MMA2_zero.v @@ -13,14 +13,10 @@ Require Import Undecidability.Synthetic.Definitions. Require Import Undecidability.Synthetic.ReducibilityFacts. From Undecidability.Shared.Libs.DLW Require Import utils pos vec sss subcode. -From Undecidability.MinskyMachines Require Import mma_defs mma_simul. +From Undecidability.MinskyMachines Require Import MMA. +From Undecidability.MinskyMachines Require MMA_to_MMA_zero. Set Implicit Arguments. Theorem MMA2_MMA2_HALTS_ON_ZERO : MMA2_HALTING ⪯ MMA2_HALTS_ON_ZERO. -Proof. - apply reduces_dependent; exists. - intros (P,v). - destruct mma2_simulator with 1 1 P as (Q & HQ). - exists (Q,v); apply HQ. -Qed. +Proof. apply MMA_to_MMA_zero.reduction. Qed. diff --git a/theories/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.v b/theories/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.v index 9d906f114..597ab991b 100644 --- a/theories/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.v +++ b/theories/MinskyMachines/Reductions/MMA3_to_MMA2_HALTING.v @@ -18,7 +18,7 @@ From Undecidability.Synthetic Local Notation "e #> x" := (vec_pos e x). -Theorem reduction n : @MMA_HALTING (3+n) ⪯ @MMA_HALTING (2+n). +Theorem reduction n : MMA_HALTING (3+n) ⪯ MMA_HALTING (2+n). Proof. apply reduces_dependent; exists. intros (P,v). diff --git a/theories/MinskyMachines/Reductions/MMA_to_MMA_zero.v b/theories/MinskyMachines/Reductions/MMA_to_MMA_zero.v new file mode 100644 index 000000000..f6d93e133 --- /dev/null +++ b/theories/MinskyMachines/Reductions/MMA_to_MMA_zero.v @@ -0,0 +1,26 @@ +(**************************************************************) +(* Copyright Dominique Larchey-Wendling [*] *) +(* *) +(* [*] Affiliation LORIA -- CNRS *) +(**************************************************************) +(* This file is distributed under the terms of the *) +(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) +(**************************************************************) + +Require Import List Arith Relations Lia. + +Require Import Undecidability.Synthetic.Definitions. +Require Import Undecidability.Synthetic.ReducibilityFacts. + +From Undecidability.Shared.Libs.DLW Require Import utils pos vec sss subcode. +From Undecidability.MinskyMachines Require Import mma_defs mma_simul. + +Set Implicit Arguments. + +Theorem reduction n : MMA_HALTING (1+n) ⪯ MMA_HALTS_ON_ZERO (1+n). +Proof. + apply reduces_dependent; exists. + intros (P,v). + destruct mma2_simulator with n 1 P as (Q & HQ). + exists (Q,v); apply HQ. +Qed. diff --git a/theories/Shared/Libs/DLW/Code/compiler.v b/theories/Shared/Libs/DLW/Code/compiler.v index d5882ce6a..94e7f08d4 100644 --- a/theories/Shared/Libs/DLW/Code/compiler.v +++ b/theories/Shared/Libs/DLW/Code/compiler.v @@ -12,6 +12,8 @@ Require Import List Arith Lia. From Undecidability.Shared.Libs.DLW Require Import utils subcode. +Import ListNotations. + Set Implicit Arguments. (* * A certified low-level compiler *) @@ -63,7 +65,20 @@ Section linker. Proof. revert i j; induction ll; simpl; intros; f_equal; auto. Qed. - + + Fact link_le i ll j: + (forall x, In x ll -> 1 <= lc x) + -> forall p k, In (p,k) (link i ll j) -> j <= k < lsum ll + j. + Proof. + revert i j; induction ll as [ | x ll IH ]; simpl; intros i j Hlc p k. + + intros []. + + intros [ E | H ]. + * inversion E; subst p k. + generalize (Hlc x (or_introl eq_refl)); lia. + * apply IH in H; try lia. + intros; apply Hlc; auto. + Qed. + Section comp. Variable lnk : nat -> nat. @@ -85,7 +100,28 @@ Section linker. revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; auto. rew length; rewrite IH, Hc; trivial. Qed. - + + Fact comp_in_inv i ll j l' y r' : + comp i ll j = l'++y::r' + -> exists l x r a b, ll = l++x::r + /\ c lnk (length l+i) x = a++y::b + /\ l' = comp i l j ++ a + /\ r' = b ++ comp (1+length l+i) r (lsum (l++[x])+j). + Proof. + revert i j l' y r'; induction ll as [ | x ll IH ]; simpl; intros i j l' y r' H. + + now destruct l'. + + apply list_app_cons_eq_inv in H + as [ (m & H1 & H2) | (m & H1 & H2) ]. + * apply IH in H2 as (l & x' & r & a & b & H2 & H3 & H4 & H5). + exists (x::l), x', r, a, b; msplit 3; simpl. + - f_equal; auto. + - rewrite <- H3; f_equal; lia. + - rewrite <- H1, app_ass; f_equal; auto. + - rewrite H5; f_equal; f_equal; lia. + * exists [], x, ll, l', m; msplit 3; auto. + rewrite H2; do 2 f_equal; simpl; lia. + Qed. + End comp. Variable (P : nat * list X) (i : nat) (err : nat). @@ -130,6 +166,24 @@ Section linker. rewrite link_fst, list_an_spec in H1; simpl in H1; lia. Qed. + Fact linker_mono j k : fst P <= j -> j <= k -> k < length (snd P) + fst P -> linker j <= linker k. + Proof. + intros H1 H2 H3. + destruct (@list_split_length _ (snd P) (j - fst P)) + as (l1 & ll & H4 & H5); try lia. + destruct (@list_split_length _ ll (k-j)) + as (l2 & l3 & H6 & H7). + + rewrite H4, app_length in H3; lia. + + subst ll. + generalize (linker_app _ _ H4); intros E1. + rewrite <- app_ass in H4. + generalize (linker_app _ _ H4); intros E2. + replace (length l1+fst P) with j in E1; try lia. + replace (length (l1++l2)+fst P) with k in E2. + * rewrite E1, E2, length_compiler_app; lia. + * rewrite app_length; lia. + Qed. + Definition compiler := comp linker (fst P) (snd P) i. Fact compiler_length : length compiler = length_compiler (snd P). @@ -180,7 +234,22 @@ Section linker. rewrite comp_app; simpl; do 3 f_equal; lia. rewrite comp_length; lia. Qed. - + + Fact compiler_subcode_inv k µ : + (k,[µ]) exists j ρ, (j,[ρ]) nat) -> nat -> X -> list Y) (* instruction compiler w.r.t. a given linker & a position *) + (lc : X -> nat) (* compiled code length does not depend on linker or position *) + . + + Record compiler_syntactic := MkCompSynt { + cs_link : (nat*list X) -> nat -> nat -> nat; + cs_code : (nat*list X) -> nat -> list Y; + cs_fst : forall P i, cs_link P i (fst P) = i; + cs_in : forall P i j, in_code j P -> in_code (cs_link P i j) (i,cs_code P i); + cs_next : forall P i j ρ, (j,[ρ]) cs_link P i (1+j) = lc ρ + cs_link P i j; + cs_out : forall P i j, out_code j P -> cs_link P i j = code_end (i,cs_code P i); + cs_mono : forall P i j k, code_start P <= j -> j <= k -> k < code_end P -> cs_link P i j <= cs_link P i k; + cs_subcode : forall P i j ρ, (j,[ρ]) (cs_link P i j, c (cs_link P i) j ρ) exists j ρ, (j,[ρ]) . + simpl; lia. + Qed. + + Hypotheses (Hc1 : forall x, 1 <= lc x) + (Hc2 : forall lnk n x, length (c lnk n x) = lc x). + + Section generic_syntactic_compiler. + + Implicit Type P : nat*list X. + + Let err P iQ := iQ+length_compiler lc (snd P). + Let link P iQ := linker lc P iQ (err P iQ). + Let code P iQ := compiler c lc P iQ (err P iQ). + + Local Fact fst_ok : forall P i, link P i (fst P) = i. + Proof. intros [] ?; apply linker_code_start. Qed. + + Local Fact out_ok : forall P i j, out_code j P -> link P i j = code_end(i,code P i). + Proof using Hc2. + intros (iP,cP) iQ j H. + unfold link, code_end. + rewrite linker_out_err; unfold err; simpl; auto. + * unfold code; rewrite compiler_length; auto. + * lia. + Qed. + + Theorem generic_syntactic_compiler : compiler_syntactic. + Proof using Hc1 Hc2. + exists link code; auto. + + apply fst_ok. + + intros Hlc P i j; now apply linker_in_code. + + intros ? ? ? ? Hρ; apply compiler_subcode with (1 := Hc2) (2 := Hρ). + + apply out_ok. + + intros; apply linker_mono; try assumption. + unfold code_end in *; lia. + + intros ? ? ? ? Hρ; apply compiler_subcode with (1 := Hc2) (2 := Hρ). + + intros; apply compiler_subcode_inv; auto. + Qed. + + End generic_syntactic_compiler. + +End compiler_syntactic. + +Print compiler_syntactic. +Check generic_syntactic_compiler. + + diff --git a/theories/Shared/Libs/DLW/Code/compiler_correction.v b/theories/Shared/Libs/DLW/Code/compiler_correction.v index 8518fe62f..bf6c9f08b 100644 --- a/theories/Shared/Libs/DLW/Code/compiler_correction.v +++ b/theories/Shared/Libs/DLW/Code/compiler_correction.v @@ -19,7 +19,7 @@ Import ListNotations. Set Implicit Arguments. Set Default Goal Selector "!". -Section comp. +Section correctness_generic. (* This is an abstract proof of compiler soundness & completeness @@ -40,14 +40,15 @@ Section comp. whether this assumption is strong or not is debatable but we only encountered cases which satisfy this assuption *) - (Hilen : forall lnk n x, length (icomp lnk n x) = ilen x) - (*Hilen2 : forall x, 1 <= ilen x*). (* compiled code should not be empty, even if the source + (Hilen1 : forall lnk n x, length (icomp lnk n x) = ilen x) + (*Hilen2 : forall x, 1 <= ilen x*). (* compiled code should not be empty, even if the source instruction is something like NO-OP, to ensure progress in the simulation as source code executes also not a strong requirement - This can be removed because it can be deduced (where it - is used) from Hilen & step_X_tot & Hicomp + This could be removed because it can be deduced (where it + is used) from Hilen & step_X_tot & Hicomp, but this mixed + semantic and syntactic conditions so we keep it. *) (* Semantics for X and Y instructions *) @@ -125,7 +126,8 @@ Section comp. (Q : nat * list Y) (HPQ : forall i ρ, (i,[ρ]) (linker i, icomp linker i ρ) out_code (linker i) Q). (* From semantic correctness of individually compiled instructions and syntactic correctness of the whole compiled program, we derive @@ -137,7 +139,8 @@ Section comp. -> exists w₂, v₂ ⋈ w₂ /\ Q /Y/ (linker i₁,w₁) ->> (linker i₂,w₂). Theorem compiler_sound : compiled_sound. - Proof using HPQ Hilen Hicomp. + Proof using HPQ Hilen1 Hicomp. + clear Hlink. intros i1 v1 i2 v2 w1. change i1 with (fst (i1,v1)) at 2; change v1 with (snd (i1,v1)) at 1. change i2 with (fst (i2,v2)) at 2; change v2 with (snd (i2,v2)) at 2. @@ -149,7 +152,7 @@ Section comp. inversion G2; subst v' i1; clear G2. destruct (Hicomp linker) with (1 := G3) (3 := H0) as (w2 & G4 & G5). - * rewrite Hilen; apply HPQ; subst; exists l, r; auto. + * rewrite Hilen1; apply HPQ; subst; exists l, r; auto. * destruct (IH2 _ G5) as (w3 & G6 & G7). exists w3; split; auto. apply sss_compute_trans with (2 := G7); simpl. @@ -158,6 +161,18 @@ Section comp. apply HPQ; subst; exists l, r; auto. Qed. + Definition compiled_sound_output := forall i₁ v₁ i₂ v₂ w₁, + v₁ ⋈ w₁ /\ P /X/ (i₁,v₁) ~~> (i₂,v₂) + -> exists w₂, v₂ ⋈ w₂ /\ Q /Y/ (linker i₁,w₁) ~~> (linker i₂,w₂). + + Theorem compiler_sound_output : compiled_sound_output. + Proof using HPQ Hilen1 Hicomp Hlink. + intros i1 v1 i2 v2 w1 (H1 & H2 & H3). + destruct compiler_sound with (1 := conj H1 H2) as (w2 & H4 & H5). + exists w2; msplit 2; auto. + revert H3; simpl fst; auto. + Qed. + (* When still inside of P, the computation in Q simulates a computation in P *) @@ -172,7 +187,7 @@ Section comp. /\ P /X/ st1 ->> st2 /\ Q /Y/ w2 -[q]-> w3 /\ q < p. - Proof using HPQ Hicomp Hilen step_Y_fun step_X_tot. + Proof using HPQ Hicomp Hilen1 step_Y_fun step_X_tot. revert st1 w1 w3; intros (i1,v1) (j1,w1) (j3,w3); simpl fst; simpl snd. intros H1 H2 H3 H4 H5. destruct (in_code_subcode H3) as (I & HI). @@ -183,17 +198,17 @@ Section comp. { intros H. destruct (step_X_tot I (i1,v1)) as ((i2,v2) & Hst). apply (Hicomp linker) with (3 := H1) in Hst; auto. - 2: rewrite Hilen; auto. + 2: rewrite Hilen1; auto. destruct Hst as (w2 & (q & Hq1 & Hq2) & _). - rewrite <- (Hilen linker i1) in H. + rewrite <- (Hilen1 linker i1) in H. destruct (icomp linker i1 I); try discriminate. apply sss_steps_stall, proj1 in Hq2; simpl; lia. } assert (in_code (linker i1) (linker i1, icomp linker i1 I)) as G3. - { simpl; rewrite (Hilen linker i1 I); lia. } + { simpl; rewrite (Hilen1 linker i1 I); lia. } rewrite <- H2 in H5. destruct (step_X_tot I (i1,v1)) as ((i2,v2) & G4). destruct (Hicomp linker) with (1 := G4) (3 := H1) as (w2 & G5 & G6). - * rewrite H7, Hilen; auto. + * rewrite H7, Hilen1; auto. * apply subcode_sss_progress_inv with (3 := H6) (4 := G5) in H5; auto. destruct H5 as (q & H5 & G7). exists q, (i2,v2), (linker i2, w2); simpl; repeat (split; auto). @@ -207,7 +222,7 @@ Section comp. Theorem compiler_complete i1 v1 w1 : v1 ⋈ w1 -> Q /Y/ (linker i1,w1) ↓ -> P /X/ (i1,v1) ↓. - Proof using HPQ Hicomp Hilen step_Y_fun step_X_tot. + Proof using HPQ Hicomp Hilen1 step_Y_fun step_X_tot. intros H1 (st & (q & H2) & H3). revert i1 v1 w1 H1 H2 H3. induction q as [ q IHq ] using (well_founded_induction lt_wf). @@ -227,7 +242,7 @@ Section comp. v₁ ⋈ w₁ /\ Q /Y/ (linker i₁,w₁) ~~> st -> exists i₂ v₂ w₂, v₂ ⋈ w₂ /\ P /X/ (i₁,v₁) ~~> (i₂,v₂) /\ Q /Y/ (linker i₂,w₂) ~~> st. - Proof using HPQ Hicomp Hilen step_Y_fun step_X_tot. + Proof using HPQ Hicomp Hilen1 step_Y_fun step_X_tot. intros i1 v1 w1 st (H1 & H2). destruct compiler_complete with (1 := H1) (2 := ex_intro (fun x => Q /Y/ (linker i1, w1) ~~> x) _ H2) as ((i2,v2) & H3 & H4). @@ -243,6 +258,20 @@ Section comp. v₁ ⋈ w₁ /\ Q /Y/ (linker i₁,w₁) ~~> (j₂,w₂) -> exists i₂ v₂, v₂ ⋈ w₂ /\ P /X/ (i₁,v₁) ~~> (i₂,v₂) /\ j₂ = linker i₂. + Corollary compiler_complete'' : compiled_complete. + Proof using HPQ Hicomp Hilen1 Hlink step_Y_fun step_X_tot. + intros i1 v1 w1 j2 w2 H. + destruct compiler_complete' with (1 := H) as (i2 & v2 & w2' & G1 & G2 & G3 & G4). + destruct H as (H1 & H2). + exists i2, v2. + match type of G3 with _ /Y/ (?a,?b) ->> (?c,?d) => assert (a = c /\ b = d) as E end. + 1:{ apply sss_compute_stop in G3. + + inversion G3; auto. + + simpl fst. + apply Hlink, G2. } + destruct E as (<- & ->); auto. + Qed. + End correctness. Record compiler_t := MkGenComp { @@ -268,7 +297,7 @@ Section comp. Proof. intros [] ?; apply linker_code_start. Qed. Local Fact out_ok : forall P i j, out_code j P -> link P i j = code_end(i,code P i). - Proof using Hilen. + Proof using Hilen1. intros (iP,cP) iQ j H. unfold link, code_end. rewrite linker_out_err; unfold err; simpl; auto. @@ -277,33 +306,24 @@ Section comp. Qed. Local Fact sound : forall P i, compiled_sound (link P i) P (i,code P i). - Proof using Hilen Hicomp. + Proof using Hilen1 Hicomp. intros (iP,cP) iQ; apply compiler_sound. intros; apply compiler_subcode; auto. Qed. Local Fact complete : forall P i, compiled_complete (link P i) P (i,code P i). - Proof using Hilen Hicomp step_Y_fun step_X_tot. + Proof using Hilen1 Hicomp step_Y_fun step_X_tot. intros (iP,cP) iQ; unfold link, code. - intros i1 v1 w1 j2 w2 H1. - destruct compiler_complete' with (2 := H1) (P := (iP,cP)) - as (i2 & v2 & w2' & H2 & H3 & H4 & H5); auto. + apply compiler_complete''. + intros; apply compiler_subcode; auto. - + exists i2, v2. - match type of H4 with _ /Y/ (?a,?b) ->> (?c,?d) => assert (a = c /\ b = d) as E end. - 1:{ apply sss_compute_stop in H4. - * inversion H4; auto. - * simpl fst. - apply linker_out_code; auto. - - right; unfold err; lia. - - apply H3. } - destruct E as [ E -> ]; auto. + + intro; apply linker_out_code; auto. + right; unfold err; simpl; lia. Qed. Hint Resolve fst_ok out_ok sound complete : core. Theorem generic_compiler : compiler_t. - Proof using Hilen Hicomp step_Y_fun step_X_tot. + Proof using Hilen1 Hicomp step_Y_fun step_X_tot. exists link code; auto. Defined. @@ -359,7 +379,71 @@ Section comp. apply compiler_t_term_correct. Qed. -End comp. +End correctness_generic. + +Section correctness_syntactic. + + Variables (X Y : Set) + (ic : (nat -> nat) -> nat -> X -> list Y) + (il : X -> nat) + (Hil : forall lnk i x, length (ic lnk i x) = il x) + (cs : compiler_syntactic ic il). + + Variables (state_X state_Y : Type) + (step_X : X -> (nat*state_X) -> (nat*state_X) -> Prop) + (step_Y : Y -> (nat*state_Y) -> (nat*state_Y) -> Prop). + + Notation "ρ '/X/' s -1> t" := (step_X ρ s t) (at level 70, no associativity). + Notation "µ '/Y/' s -1> t" := (step_Y µ s t) (at level 70, no associativity). + + Hypothesis (step_X_tot : forall ρ st1, exists st2, ρ /X/ st1 -1> st2) + (step_Y_fun : forall µ st st1 st2, µ /Y/ st -1> st1 -> µ /Y/ st -1> st2 -> st1 = st2). + + Variables (simul : state_X -> state_Y -> Prop) + (Hsimul : instruction_compiler_sound ic step_X step_Y simul). + + Theorem compiler_syntactic_sound P i : compiled_sound step_X step_Y simul (cs_link cs P i) P (i,cs_code cs P i). + Proof using Hsimul Hil. + destruct cs as [ link code C1 C2 C3 C4 C5 C6 C7 ]; simpl. + apply compiler_sound with ic il; auto. + Qed. + + Theorem compiler_syntactic_sound_output P i : compiled_sound_output step_X step_Y simul (cs_link cs P i) P (i,cs_code cs P i). + Proof using Hsimul Hil. + destruct cs as [ link code C1 C2 C3 C4 C5 C6 C7 ]; simpl. + apply compiler_sound_output with ic il; auto. + intros j Hj. + rewrite C4; simpl; auto. + Qed. + + Theorem compiler_syntactic_complete P i : compiled_complete step_X step_Y simul (cs_link cs P i) P (i,cs_code cs P i). + Proof using step_Y_fun step_X_tot Hsimul Hil. + destruct cs as [ link code C1 C2 C3 C4 C5 C6 C7 ]; simpl. + apply compiler_complete'' with ic il; auto. + intros j Hj. + apply C4 with (i := i) in Hj as ->. + right; auto. + Qed. + + Theorem compiler_syntactic_term_equiv i P j v w : simul v w -> sss_terminates step_X (i,P) (i,v) + <-> sss_terminates step_Y (j,cs_code cs (i,P) j) (j,w). + Proof using step_Y_fun step_X_tot Hsimul Hil. + intros Hvw; split. + + intros ((i',v') & H2 & H3). + destruct compiler_syntactic_sound with (1 := conj Hvw H2) (i := j) + as (w' & H4 & H5). + rewrite <- (cs_fst cs (i,P) j) at 3; simpl fst. + exists (cs_link cs (i, P) j i', w'); split; auto. + simpl fst in H3 |- *. + rewrite (cs_out cs _ H3); simpl; lia. + + intros ((j',w') & H1). + rewrite <- (cs_fst cs (i,P) j) in H1 at 3; simpl fst in H1. + destruct compiler_syntactic_complete with (1 := conj Hvw H1) + as (j'' & v' & H2 & H3 & H4). + now exists (j'', v'). + Qed. + +End correctness_syntactic. Section compiler_t_simul_equiv. @@ -386,5 +470,3 @@ Section compiler_t_simul_equiv. Qed. End compiler_t_simul_equiv. - - diff --git a/theories/Shared/Libs/DLW/Code/subcode.v b/theories/Shared/Libs/DLW/Code/subcode.v index 464e1fc64..b22d14081 100644 --- a/theories/Shared/Libs/DLW/Code/subcode.v +++ b/theories/Shared/Libs/DLW/Code/subcode.v @@ -140,6 +140,9 @@ Section subcode. + exists a, l, r; split; auto; lia. Qed. + Fact subcode_nil_invert j i I : ~ (i,I::nil) (i,I::nil)