Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Switch from MM to MMA #161

Draft
wants to merge 12 commits into
base: coq-8.15
Choose a base branch
from
Draft

Switch from MM to MMA #161

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
600a4ed
added direct reductions
DmxLarchey Aug 22, 2022
2622146
description of the problem to use the instruction compiler to remove
DmxLarchey Sep 6, 2022
5efc88e
added an interface for the generic syntactic compiler and proved that…
DmxLarchey Sep 9, 2022
1a9ce2e
removal of self loops in MMA using the generic compiler with its synt…
DmxLarchey Sep 9, 2022
2f06c28
simplified and strenghtened the statement of cs_not_between
DmxLarchey Sep 9, 2022
dbb8ee7
trying to move the compiler_correction to the new interface
DmxLarchey Sep 9, 2022
464fe67
removal of self loops from MMA using syntactic properties of the gene…
DmxLarchey Sep 12, 2022
4ec39b4
added a direct reduction MMA_HALTING n < FRACTRAN_REG_HALTING
DmxLarchey Sep 29, 2022
11a02f6
nicer proofs in mma_fractran.v
DmxLarchey Sep 30, 2022
032023b
WIP: an alternate/shorter elimination of self loops within MM using t…
DmxLarchey Oct 3, 2022
14a6d54
finished the alternate self-loop removal algo for MM
DmxLarchey Oct 4, 2022
1f78ce1
small additions
DmxLarchey Oct 6, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/DiophantineConstraints/H10C_undec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
7 changes: 4 additions & 3 deletions theories/FRACTRAN/FRACTRAN/mm_fractran.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
Loading