add(subsystem): define the relation generated by R and Gc and prove its embedding into red1 (M3 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 Tests; do
+for f in ExecReducer Binding Reduction Metatheory Subsystem Tests; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"

theory/Subsystem.v

@@ -0,0 +1,40 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction.
+
+Inductive red_sub_root : trm -> trm -> Prop :=
+| rs_gc : forall body u, occurs0 body = false -> red_sub_root (ESub body u) body
+| rs_r : forall C body u, zfill C 0 = body ->
+    red_sub_root (ESub body u) (ESub (zplug_lift C 0 u) u).
+
+Inductive red_sub : trm -> trm -> Prop :=
+| red_sub_base : forall t t', red_sub_root t t' -> red_sub t t'
+| red_sub_ctx : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
+
+Lemma red_sub_root_to_red1 : forall t t', red_sub_root t t' -> red1 t t'.
+Proof.
+  intros t t' H. destruct H.
+  - exists RGc. apply red1r_root. apply rGc. exact H.
+  - exists RR. apply red1r_root. apply rR. exact H.
+Qed.
+
+Lemma red_sub_to_red1 : forall t t', red_sub t t' -> red1 t t'.
+Proof.
+  intros t t' H. induction H.
+  - apply red_sub_root_to_red1. exact H.
+  - destruct IHred_sub as [r Hr]. exists r. apply rctx. exact Hr.
+Qed.
+
+Lemma red_sub_context : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
+Proof. intros. apply red_sub_ctx. exact H. Qed.
+
+Lemma red_sub_gc : forall body u, occurs0 body = false -> red_sub (ESub body u) body.
+Proof. intros. apply red_sub_base. apply rs_gc. exact H. Qed.
+
+Lemma red_sub_r : forall C body u, zfill C 0 = body ->
+  red_sub (ESub body u) (ESub (zplug_lift C 0 u) u).
+Proof. intros. apply red_sub_base. apply rs_r. exact H. Qed.
+
+Print Assumptions red_sub_root_to_red1.
+Print Assumptions red_sub_to_red1.
+Print Assumptions red_sub_context.