Merge pull request #190 from JoJoDeveloping/coq-8.16

Remove dependency on Synthetic.Undecidability for non-_undec files

Author: yforster

theories/ILL/Reductions/iBPCP_MM.v

@@ -11,7 +11,7 @@ Require Import List.
 
 Import ListNotations.
 
-Require Import Undecidability.Synthetic.Undecidability.
+Require Import Undecidability.Synthetic.Definitions.
 Require Import Undecidability.Synthetic.ReducibilityFacts.
 
 From Undecidability.Shared.Libs.DLW
@@ -26,7 +26,7 @@ From Undecidability.StackMachines
 From Undecidability.MinskyMachines
   Require Import MM BSM_MM MM_sss.
 
-Import ReductionChainNotations UndecidabilityNotations.
+Import ReductionChainNotations.
 
 Lemma iBPCP_chain_MM : 
   iPCPb ⪯ Halt_BSM /\

theories/MuRec/Reductions/Diophantine_to_MuRec_computable.v

@@ -1,7 +1,5 @@
 Require Import List Lia.
 
-From Undecidability.Synthetic Require Import Undecidability.
-
 From Undecidability.Shared.Libs.DLW.Utils
   Require Import utils_tac utils_nat.
 

theories/PCP/Reductions/HaltTM_1_to_PCPb.v

@@ -16,7 +16,7 @@ Require Import List.
 From Undecidability.Shared.Libs.DLW
   Require Import utils.
 
-Require Import Undecidability.Synthetic.Undecidability.
+Require Import Undecidability.Synthetic.Definitions.
 Require Import Undecidability.Synthetic.ReducibilityFacts.
 
 Require Import Undecidability.TM.TM.
@@ -39,7 +39,7 @@ From Undecidability.StringRewriting.Reductions
 From Undecidability.PCP.Reductions
   Require SR_to_MPCP MPCP_to_PCP PCP_to_PCPb PCPb_iff_iPCPb.
 
-Import ReductionChainNotations UndecidabilityNotations.
+Import ReductionChainNotations.
 
 Lemma HaltTM_1_chain_iPCPb : 
   HaltTM 1 ⪯ SBTM_HALT /\

theories/StackMachines/BSM/bsm_pctm.v

@@ -10,7 +10,7 @@
 Require Import List Arith Lia Bool.
 
 From Undecidability.Synthetic
-  Require Import Undecidability ReducibilityFacts.
+  Require Import ReducibilityFacts.
 
 From Undecidability.Shared.Libs.DLW 
   Require Import utils list_bool pos vec subcode sss compiler_correction.

theories/StackMachines/Reductions/PCTM_HALT_to_BSM_HALTING.v

@@ -10,7 +10,7 @@
 Require Import List Bool.
 
 From Undecidability.Synthetic
-  Require Import Undecidability ReducibilityFacts.
+  Require Import Definitions ReducibilityFacts.
 
 From Undecidability.Shared.Libs.DLW 
   Require Import pos vec sss compiler_correction.

theories/Synthetic/ReducibilityFacts.v

@@ -120,4 +120,7 @@ Tactic Notation "red" "chain" "step" constr(H) := constructor 2; [ apply H | ].
 Tactic Notation "red" "chain" "app" constr(H) := apply reduction_chain_app with (1 := H).
 *)
 
+Tactic Notation "reduce" "with" "chain" constr(H) := 
+  repeat (apply (reduces_reflexive _) || (eapply reduces_transitive; [ apply H | ])).
+
 End ReductionChainNotations.

theories/Synthetic/Undecidability.v

@@ -45,13 +45,11 @@ Proof.
 Qed.
 
 Module UndecidabilityNotations.
+Import ReductionChainNotations.
 
 Tactic Notation "undec" "from" constr(H) :=
   apply (undecidability_from_reducibility H).
 
-Tactic Notation "reduce" "with" "chain" constr(H) := 
-  repeat (apply (reduces_reflexive _) || (eapply reduces_transitive; [ apply H | ])).
-
 Tactic Notation "undec" "from" constr(U) "using" "chain" constr(C) :=
   undec from U; reduce with chain C.
 

theories/TM/PCTM/pctm_sbtm.v

@@ -13,7 +13,7 @@ From Undecidability.Shared.Libs.DLW
   Require Import utils pos subcode sss.
 
 From Undecidability.Synthetic
-  Require Import Undecidability ReducibilityFacts.
+  Require Import ReducibilityFacts.
 
 From Undecidability.TM 
   Require Import SBTM pctm_defs.

theories/TM/Reductions/SBTM_HALT_to_PCTM_HALT.v

@@ -10,7 +10,7 @@
 Require Import List Bool.
 
 From Undecidability.Synthetic
-  Require Import Undecidability ReducibilityFacts.
+  Require Import Definitions ReducibilityFacts.
 
 From Undecidability.Shared.Libs.DLW 
   Require Import pos sss.