Add turing to library

front/package.json

@@ -76,7 +76,7 @@
     "typescript": "^4.1.2",
     "url-loader": "4.1.1",
     "web-vitals": "^1.0.1",
-    "webpack": "5.62.1",
+    "webpack": "5.64.4",
     "webpack-dev-server": "3.11.1",
     "webpack-manifest-plugin": "4.0.2",
     "yaml-include-loader": "^1.0.0",
@@ -103,4 +103,4 @@
     "ts-node": "^10.8.1",
     "webpack-cli": "^4.9.1"
   }
-}
+}

front/yarn.lock

@@ -10186,10 +10186,10 @@ walker@^1.0.7, walker@~1.0.5:
   dependencies:
     makeerror "1.0.x"
 
-watchpack@^2.2.0:
-  version "2.2.0"
-  resolved "https://registry.npmjs.org/watchpack/-/watchpack-2.2.0.tgz"
-  integrity sha512-up4YAn/XHgZHIxFBVCdlMiWDj6WaLKpwVeGQk2I5thdYxF/KmF0aaz6TfJZ/hfl1h/XlcDr7k1KH7ThDagpFaA==
+watchpack@^2.3.0:
+  version "2.4.0"
+  resolved "https://registry.yarnpkg.com/watchpack/-/watchpack-2.4.0.tgz#fa33032374962c78113f93c7f2fb4c54c9862a5d"
+  integrity sha512-Lcvm7MGST/4fup+ifyKi2hjyIAwcdI4HRgtvTpIUxBRhB+RFtUh8XtDOxUfctVCnhVi+QQj49i91OyvzkJl6cg==
   dependencies:
     glob-to-regexp "^0.4.1"
     graceful-fs "^4.1.2"
@@ -10324,15 +10324,15 @@ webpack-sources@^2.2.0:
     source-list-map "^2.0.1"
     source-map "^0.6.1"
 
-webpack-sources@^3.2.0:
-  version "3.2.1"
-  resolved "https://registry.npmjs.org/webpack-sources/-/webpack-sources-3.2.1.tgz"
-  integrity sha512-t6BMVLQ0AkjBOoRTZgqrWm7xbXMBzD+XDq2EZ96+vMfn3qKgsvdXZhbPZ4ElUOpdv4u+iiGe+w3+J75iy/bYGA==
+webpack-sources@^3.2.2:
+  version "3.2.3"
+  resolved "https://registry.yarnpkg.com/webpack-sources/-/webpack-sources-3.2.3.tgz#2d4daab8451fd4b240cc27055ff6a0c2ccea0cde"
+  integrity sha512-/DyMEOrDgLKKIG0fmvtz+4dUX/3Ghozwgm6iPp8KRhvn+eQf9+Q7GWxVNMk3+uCPWfdXYC4ExGBckIXdFEfH1w==
 
-webpack@5.62.1:
-  version "5.62.1"
-  resolved "https://registry.npmjs.org/webpack/-/webpack-5.62.1.tgz"
-  integrity sha512-jNLtnWChS2CMZ7vqWtztv0G6fYB5hz11Zsadp5tE7e4/66zVDj7/KUeQZOsOl8Hz5KrLJH1h2eIDl6AnlyE12Q==
+webpack@5.64.4:
+  version "5.64.4"
+  resolved "https://registry.yarnpkg.com/webpack/-/webpack-5.64.4.tgz#e1454b6a13009f57cc2c78e08416cd674622937b"
+  integrity sha512-LWhqfKjCLoYJLKJY8wk2C3h77i8VyHowG3qYNZiIqD6D0ZS40439S/KVuc/PY48jp2yQmy0mhMknq8cys4jFMw==
   dependencies:
     "@types/eslint-scope" "^3.7.0"
     "@types/estree" "^0.0.50"
@@ -10356,8 +10356,8 @@ [email protected]:
     schema-utils "^3.1.0"
     tapable "^2.1.1"
     terser-webpack-plugin "^5.1.3"
-    watchpack "^2.2.0"
-    webpack-sources "^3.2.0"
+    watchpack "^2.3.0"
+    webpack-sources "^3.2.2"
 
 websocket-driver@>=0.5.1, websocket-driver@^0.7.4:
   version "0.7.4"

library/Automata.v

@@ -112,3 +112,72 @@ Axiom pumping_lemma: ∀ sigma, ∀ A: DFA sigma,
     ∀ s, IsWord sigma s → |s| ≥ |A| → ∀ start, 0 ≤ start ∧ start < |A| →
     ∃ x y z, s = x + y + z ∧ |y| > 0 ∧ |x| + |z| ≤ |A| ∧ ∀ i, i ≥ 0 → run_dfa A start (x + rep y i + z) = run_dfa A start s;
 
+Axiom TM: U;
+Axiom turing_accept: TM -> list char -> U;
+Axiom turing_reject: TM -> list char -> U;
+Axiom turing_halt: TM -> list char -> U;
+Axiom halt_unfold: ∀ t: TM, ∀ s, turing_halt t s -> turing_accept t s ∨ turing_reject t s;
+Axiom halt_fold: ∀ t: TM, ∀ s, turing_accept t s ∨ turing_reject t s -> turing_halt t s;
+Suggest goal default apply halt_fold with label Destruct;
+Suggest hyp default apply halt_unfold in $n with label Destruct;
+
+Axiom turing_accept_not_reject: ∀ t: TM, ∀ s, turing_accept t s -> ~ turing_reject t s;
+Axiom turing_reject_not_accept: ∀ t: TM, ∀ s, turing_reject t s -> ~ turing_accept t s;
+
+Axiom accept_everything: TM;
+Axiom accept_everything_def: ∀ s, turing_accept accept_everything s;
+Suggest goal auto apply accept_everything_def with label Trivial;
+Axiom reject_everything: TM;
+Axiom reject_everything_def: ∀ s, turing_reject reject_everything s;
+Suggest goal auto apply reject_everything_def with label Trivial;
+Axiom loop_on_everything: TM;
+Axiom loop_on_everything_def: ∀ s, ~ turing_halt loop_on_everything s;
+Suggest goal auto apply loop_on_everything with label Trivial;
+
+Axiom decider: TM -> U;
+Axiom decider_fold: ∀ t: TM, (∀ s, turing_halt t s) -> decider t;
+Axiom decider_unfold: ∀ t: TM, decider t -> (∀ s, turing_halt t s);
+Suggest goal default apply decider_fold with label Destruct;
+Suggest hyp default apply decider_unfold in $n with label Destruct;
+
+Axiom turing_to_str: TM -> list char;
+
+Axiom universal_turing_machine: TM;
+
+Axiom utm_accept_unfold: ∀ t: TM, ∀ s, turing_accept universal_turing_machine (turing_to_str t + "*" + s) -> turing_accept t s;
+Axiom utm_accept_fold: ∀ t: TM, ∀ s, turing_accept t s -> turing_accept universal_turing_machine (turing_to_str t + "*" + s);
+Suggest goal default apply utm_accept_fold with label Destruct;
+Suggest hyp default apply utm_accept_unfold in $n with label Destruct;
+
+Axiom utm_reject_unfold: ∀ t: TM, ∀ s, turing_reject universal_turing_machine (turing_to_str t + "*" + s) -> turing_reject t s;
+Axiom utm_reject_fold: ∀ t: TM, ∀ s, turing_reject t s -> turing_reject universal_turing_machine (turing_to_str t + "*" + s);
+Suggest goal default apply utm_reject_fold with label Destruct;
+Suggest hyp default apply utm_reject_unfold in $n with label Destruct;
+
+Axiom utm_halt_unfold: ∀ t: TM, ∀ s, turing_halt universal_turing_machine (turing_to_str t + "*" + s) -> turing_halt t s;
+Axiom utm_halt_fold: ∀ t: TM, ∀ s, turing_halt t s -> turing_halt universal_turing_machine (turing_to_str t + "*" + s);
+Suggest goal default apply utm_halt_fold with label Destruct;
+Suggest hyp default apply utm_halt_unfold in $n with label Destruct;
+
+Axiom select_tm: list char -> TM;
+Axiom select_tm_fold: ∀ s, turing_accept (select_tm s) s;
+Axiom select_tm_unfold: ∀ s1 s2, turing_accept (select_tm s1) s2 -> s1 = s2;
+Axiom select_tm_decider: ∀ s, decider (select_tm s);
+
+Axiom conditional_tm: TM -> TM -> TM -> TM;
+Axiom conditional_tm_accept_unfold: ∀ cond then else: TM, ∀ s, turing_accept (conditional_tm cond then else) s
+    -> turing_accept cond s ∧ turing_accept then s ∨ turing_reject cond s ∧ turing_accept else s;
+Axiom conditional_tm_accept_fold: ∀ cond then else: TM, ∀ s,
+    turing_accept cond s ∧ turing_accept then s ∨ turing_reject cond s ∧ turing_accept else s
+    -> turing_accept (conditional_tm cond then else) s;
+Axiom conditional_tm_reject_unfold: ∀ cond then else: TM, ∀ s, turing_reject (conditional_tm cond then else) s
+    -> turing_accept cond s ∧ turing_reject then s ∨ turing_reject cond s ∧ turing_reject else s;
+Axiom conditional_tm_reject_fold: ∀ cond then else: TM, ∀ s,
+    turing_accept cond s ∧ turing_reject then s ∨ turing_reject cond s ∧ turing_reject else s
+    -> turing_reject (conditional_tm cond then else) s;
+
+Axiom is_decidable: set (list char) -> U;
+Axiom is_decidable_fold: ∀ lang, (∃ t, decider t ∧ ∀ s, s ∈ lang ↔ turing_accept t s) -> is_decidable lang;
+Axiom is_decidable_unfold: ∀ lang, is_decidable lang -> (∃ t, decider t ∧ ∀ s, s ∈ lang ↔ turing_accept t s);
+Suggest goal default apply is_decidable_fold with label Destruct;
+Suggest hyp default apply is_decidable_unfold in $n with label Destruct;