add(confluence): parallel reduction with reflexivity contextual closure and the inclusion of red1 (M4 infrastructure)

scripts/audit.sh

@@ -35,7 +35,7 @@ done < <(find theory -name '*.v' -print0 2>/dev/null)
 echo "== Print Assumptions =="
 WORK="$(mktemp -d ./.audit-work.XXXXXX)"
 cp theory/*.v "$WORK"/
-for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Tests; do
+for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel Tests; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"

theory/Parallel.v

@@ -0,0 +1,44 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction.
+
+Inductive par : trm -> trm -> Prop :=
+| par_refl : forall t, par t t
+| par_step : forall t t', red1 t t' -> par t t'
+| par_ctx : forall C t t', par t t' -> par (plug C t) (plug C t').
+
+Lemma par_red1_iff : forall t t', par t t' <-> t = t' \/ red1 t t'.
+Proof.
+  intros t t'. split.
+  - intros H. induction H.
+    + left. reflexivity.
+    + right. exact H.
+    + destruct IHpar as [Heq|Hr].
+      * left. subst. reflexivity.
+      * right. destruct Hr as [r Hr]. exists r. apply rctx. exact Hr.
+  - intros [Heq|Hr].
+    + subst. apply par_refl.
+    + apply par_step. exact Hr.
+Qed.
+
+Lemma red1_in_par : forall t t', red1 t t' -> par t t'.
+Proof. intros. apply par_step. exact H. Qed.
+
+Lemma par_context : forall C t t', par t t' -> par (plug C t) (plug C t').
+Proof. intros. apply par_ctx. exact H. Qed.
+
+Lemma par_to_red1_or_eq : forall t t', par t t' -> t = t' \/ red1 t t'.
+Proof. intros. apply par_red1_iff. exact H. Qed.
+
+Lemma red1_or_eq_to_par : forall t t', t = t' \/ red1 t t' -> par t t'.
+Proof. intros. apply par_red1_iff. exact H. Qed.
+
+Lemma par_reflexive : forall t, par t t.
+Proof. intros. apply par_refl. Qed.
+
+Print Assumptions par_red1_iff.
+Print Assumptions red1_in_par.
+Print Assumptions par_context.
+Print Assumptions par_to_red1_or_eq.
+Print Assumptions red1_or_eq_to_par.
+Print Assumptions par_reflexive.