add(named): a named metaterm calculus with the C equation and the RX rule (M5 named rules)

graphs/dependency.dot

@@ -40,6 +40,15 @@ digraph theorem_deps {
   mfvs_lift_m [label="mfvs_lift_m", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mfvs_lift_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   mfvs_close_m [label="mfvs_close_m", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mfvs_close_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   mfvs_open_m [label="mfvs_open_m", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mfvs_open_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  of_trm_plug [label="of_trm_plug", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_plug theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_of_red1 [label="mred_of_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_of_red1 theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_context [label="mred_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_context theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_term_context [label="mred_term_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_term_context theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  of_trm_moccurs [label="of_trm_moccurs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_moccurs theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  of_trm_moccurs0 [label="of_trm_moccurs0", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="of_trm_moccurs0 theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_B_intro [label="mred_B_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_B_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_gc_intro [label="mred_gc_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_gc_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_r_intro [label="mred_r_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_r_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   Plus_red1_context [label="Plus_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   occurs_count_zero [label="occurs_count_zero", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   occurs_count_false [label="occurs_count_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -58,6 +67,12 @@ digraph theorem_deps {
   lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
   Plus_trans [label="Plus_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   Plus_step_trans [label="Plus_step_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_step_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  isubst_meta_in [label="isubst_meta_in", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="isubst_meta_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  isubst_meta_notin [label="isubst_meta_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="isubst_meta_notin theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  eqC_in_Es [label="eqC_in_Es", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="eqC_in_Es theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_refl_any [label="Es_refl_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_refl_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_sym_any [label="Es_sym_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_sym_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_trans_any [label="Es_trans_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_trans_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -138,6 +153,8 @@ digraph theorem_deps {
   steps_complete -> enumerate_complete;
   of_trm_lift -> of_trm_open;
   mfvs_lift_m -> mfvs_open_m;
+  of_trm_plug -> mred_term_context;
+  of_trm_moccurs -> of_trm_moccurs0;
   occurs_count_zero -> occurs_count_pos;
   occurs_count_false -> occurs_count_zfill_plug;
   occurs_lift_self -> occurs_count_zfill_plug;

graphs/index.txt

@@ -1,4 +1,27 @@
 status	milestone	kind	name	file
+proved	M0	infra	Es_refl_any	theory/NamedMeta.v
+proved	M0	infra	Es_sym_any	theory/NamedMeta.v
+proved	M0	infra	Es_trans_any	theory/NamedMeta.v
+proved	M0	infra	eqC_in_Es	theory/NamedMeta.v
+proved	M0	infra	isubst_meta_in	theory/NamedMeta.v
+proved	M0	infra	isubst_meta_notin	theory/NamedMeta.v
+proved	M0	infra	mfvs_close_m	theory/Metaterm.v
+proved	M0	infra	mfvs_lift_m	theory/Metaterm.v
+proved	M0	infra	mfvs_open_m	theory/Metaterm.v
+proved	M0	infra	mred_B_intro	theory/Metaterm.v
+proved	M0	infra	mred_context	theory/Metaterm.v
+proved	M0	infra	mred_gc_intro	theory/Metaterm.v
+proved	M0	infra	mred_of_red1	theory/Metaterm.v
+proved	M0	infra	mred_r_intro	theory/Metaterm.v
+proved	M0	infra	mred_term_context	theory/Metaterm.v
+proved	M0	infra	of_trm_close	theory/Metaterm.v
+proved	M0	infra	of_trm_fvs	theory/Metaterm.v
+proved	M0	infra	of_trm_injective	theory/Metaterm.v
+proved	M0	infra	of_trm_lift	theory/Metaterm.v
+proved	M0	infra	of_trm_moccurs	theory/Metaterm.v
+proved	M0	infra	of_trm_moccurs0	theory/Metaterm.v
+proved	M0	infra	of_trm_open	theory/Metaterm.v
+proved	M0	infra	of_trm_plug	theory/Metaterm.v
 proved	M1	infra	at_ctx_comp	theory/Reduction.v
 proved	M1	infra	close_rec_fvar	theory/Binding.v
 proved	M1	infra	close_rec_fvs	theory/Binding.v

graphs/theorems.json

@@ -373,6 +373,100 @@
         "mfvs_lift_m"
       ]
     },
+    {
+      "id": "of_trm_plug",
+      "label": "of_trm_plug",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "mred_of_red1",
+      "label": "mred_of_red1",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "mred_context",
+      "label": "mred_context",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "mred_term_context",
+      "label": "mred_term_context",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": [
+        "of_trm_plug"
+      ]
+    },
+    {
+      "id": "of_trm_moccurs",
+      "label": "of_trm_moccurs",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "of_trm_moccurs0",
+      "label": "of_trm_moccurs0",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": [
+        "of_trm_moccurs"
+      ]
+    },
+    {
+      "id": "mred_B_intro",
+      "label": "mred_B_intro",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "mred_gc_intro",
+      "label": "mred_gc_intro",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "mred_r_intro",
+      "label": "mred_r_intro",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
     {
       "id": "Plus_red1_context",
       "label": "Plus_red1_context",
@@ -582,6 +676,66 @@
       "file": "theory/Metatheory.v",
       "depends": []
     },
+    {
+      "id": "isubst_meta_in",
+      "label": "isubst_meta_in",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "isubst_meta_notin",
+      "label": "isubst_meta_notin",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "eqC_in_Es",
+      "label": "eqC_in_Es",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "Es_refl_any",
+      "label": "Es_refl_any",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "Es_sym_any",
+      "label": "Es_sym_any",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "Es_trans_any",
+      "label": "Es_trans_any",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
     {
       "id": "par_red1_iff",
       "label": "par_red1_iff",

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 Closure Subsystem Substitution Parallel Metaterm Tests Random Enumerate; do
+for f in ExecReducer Binding Reduction Metatheory Closure Subsystem Substitution Parallel Metaterm NamedMeta Tests Random Enumerate; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"

theory/NamedMeta.v

@@ -0,0 +1,106 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+
+Definition atom := nat.
+
+Inductive ntrm : Type :=
+| NVar : atom -> ntrm
+| NApp : ntrm -> ntrm -> ntrm
+| NLam : atom -> ntrm -> ntrm
+| NESub : ntrm -> atom -> ntrm -> ntrm
+| NMVar : atom -> list atom -> ntrm.
+
+Fixpoint nfv (t : ntrm) : list atom :=
+  match t with
+  | NVar x => [x]
+  | NApp a b => nfv a ++ nfv b
+  | NLam x a => filter (fun y => negb (Nat.eqb y x)) (nfv a)
+  | NESub a x b => filter (fun y => negb (Nat.eqb y x)) (nfv a) ++ nfv b
+  | NMVar _ d => d
+  end.
+
+Definition isubst_meta (X : atom) (d : list atom) (x : atom) (v : ntrm) : ntrm :=
+  if existsb (Nat.eqb x) d then NESub (NMVar X d) x v else NMVar X d.
+
+Lemma isubst_meta_in : forall X d x v, In x d -> isubst_meta X d x v = NESub (NMVar X d) x v.
+Proof.
+  intros X d x v H. unfold isubst_meta.
+  destruct (existsb (Nat.eqb x) d) eqn:E; [reflexivity |].
+  assert (Hex : existsb (Nat.eqb x) d = true)
+    by (apply existsb_exists; exists x; split; [exact H | apply Nat.eqb_refl]).
+  rewrite Hex in E. discriminate E.
+Qed.
+
+Lemma isubst_meta_notin : forall X d x v, ~ In x d -> isubst_meta X d x v = NMVar X d.
+Proof.
+  intros X d x v H. unfold isubst_meta.
+  destruct (existsb (Nat.eqb x) d) eqn:E; [| reflexivity].
+  exfalso. apply existsb_exists in E. destruct E as [y [Hy HE]].
+  apply Nat.eqb_eq in HE. subst y. apply H. exact Hy.
+Qed.
+
+Inductive nctx : Type :=
+| nHole : nctx
+| nAppL : nctx -> ntrm -> nctx
+| nAppR : ntrm -> nctx -> nctx
+| nLam : atom -> nctx -> nctx
+| nESubL : nctx -> atom -> ntrm -> nctx
+| nESubR : ntrm -> atom -> nctx -> nctx.
+
+Fixpoint nplug (C : nctx) (t : ntrm) : ntrm :=
+  match C with
+  | nHole => t
+  | nAppL C1 u => NApp (nplug C1 t) u
+  | nAppR u C1 => NApp u (nplug C1 t)
+  | nLam x C1 => NLam x (nplug C1 t)
+  | nESubL C1 x u => NESub (nplug C1 t) x u
+  | nESubR t1 x C1 => NESub t1 x (nplug C1 t)
+  end.
+
+Fixpoint is_subst_chain (C : nctx) : bool :=
+  match C with
+  | nHole => true
+  | nESubL C1 _ _ => is_subst_chain C1
+  | _ => false
+  end.
+
+Inductive Es : ntrm -> ntrm -> Prop :=
+| Es_refl : forall t, Es t t
+| Es_sym : forall t u, Es t u -> Es u t
+| Es_trans : forall t u v, Es t u -> Es u v -> Es t v
+| Es_C : forall t x u y v,
+    y <> x -> ~ In y (nfv u) -> ~ In x (nfv v) ->
+    Es (NESub (NESub t x u) y v) (NESub (NESub t y v) x u).
+
+Inductive nred : ntrm -> ntrm -> Prop :=
+| nred_B : forall t x u, nred (NApp (NLam x t) u) (NESub t x u)
+| nred_Gc : forall t x u, ~ In x (nfv t) -> nred (NESub t x u) t
+| nred_RX : forall C X d x u phi,
+    In x d ->
+    In x phi ->
+    (forall y, In y (nfv u) -> In y phi) ->
+    is_subst_chain C = false ->
+    nred (NESub (nplug C (NMVar X d)) x u)
+         (NESub (nplug C (NESub (NMVar X d) x u)) x u)
+| nred_ctx : forall C t t', nred t t' -> nred (nplug C t) (nplug C t').
+
+Lemma eqC_in_Es : forall t x u y v,
+  y <> x -> ~ In y (nfv u) -> ~ In x (nfv v) ->
+  Es (NESub (NESub t x u) y v) (NESub (NESub t y v) x u).
+Proof. intros. apply Es_C; assumption. Qed.
+
+Lemma Es_refl_any : forall t, Es t t.
+Proof. intros. apply Es_refl. Qed.
+
+Lemma Es_sym_any : forall t u, Es t u -> Es u t.
+Proof. intros. apply Es_sym. exact H. Qed.
+
+Lemma Es_trans_any : forall t u v, Es t u -> Es u v -> Es t v.
+Proof. intros. apply Es_trans with (u := u); assumption. Qed.
+
+Print Assumptions isubst_meta_in.
+Print Assumptions isubst_meta_notin.
+Print Assumptions eqC_in_Es.
+Print Assumptions Es_refl_any.
+Print Assumptions Es_sym_any.
+Print Assumptions Es_trans_any.