add(named): an Es setoid rewriting layer with the modulo reduction (M5 metatheory)

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

scripts/extract_metadata.py

@@ -25,6 +25,10 @@ MILESTONE = {
     "Substitution": "M2",
     "Subsystem": "M3",
     "Parallel": "M4",
+    "Metaterm": "M5",
+    "NamedMeta": "M5",
+    "NamedEs": "M5",
+    "NamedMeasure": "M5",
     "Tests": "M2",
     "Random": "M2",
     "Enumerate": "M2",

theory/NamedEs.v

@@ -0,0 +1,173 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+From Stdlib Require Import Setoid Morphisms.
+Import ListNotations.
+From LambdaSub Require Import NamedMeta.
+
+(* A setoid rewriting layer for the C equivalence Es on named metaterms.
+
+   Es is the congruence generated by the equation C (together with the
+   implicit alpha convention of the paper, which the named core does not
+   quotient). We register Es as an equivalence and as a congruence for the
+   term constructors and for every context, so that setoid rewriting can
+   move along Es. We then define the reduction relation modulo Es (subred)
+   and prove that it is stable on both sides and under every context. *)
+
+Instance Es_Equivalence : Equivalence Es.
+Proof.
+  split.
+  - intro t. apply Es_refl.
+  - intros a b Hab. apply Es_sym. exact Hab.
+  - intros a b c Hab Hbc. apply Es_trans with (u := b); assumption.
+Qed.
+
+Instance Es_NVar_Proper : Proper (eq ==> Es) NVar.
+Proof. intros a b Hab. subst b. apply Es_refl. Qed.
+
+Instance Es_NMVar_Proper : Proper (eq ==> eq ==> Es) NMVar.
+Proof. intros a b Hab c d Hcd. subst b d. apply Es_refl. Qed.
+
+Instance Es_NApp_Proper : Proper (Es ==> Es ==> Es) NApp.
+Proof.
+  intros a b Hab c d Hcd.
+  apply Es_trans with (u := NApp b c).
+  - apply Es_ctx with (C := nAppL nHole c). exact Hab.
+  - apply Es_ctx with (C := nAppR b nHole). exact Hcd.
+Qed.
+
+Instance Es_NLam_Proper (x : atom) : Proper (Es ==> Es) (NLam x).
+Proof. intros a b Hab. apply Es_ctx with (C := nLam x nHole). exact Hab. Qed.
+
+Instance Es_NESub_Proper : Proper (Es ==> eq ==> Es ==> Es) NESub.
+Proof.
+  intros a b Hab x y Hxy c d Hcd. subst y.
+  apply Es_trans with (u := NESub b x c).
+  - apply Es_ctx with (C := nESubL nHole x c). exact Hab.
+  - apply Es_ctx with (C := nESubR b x nHole). exact Hcd.
+Qed.
+
+Instance Es_nplug_Proper (C : nctx) : Proper (Es ==> Es) (nplug C).
+Proof. intros a b Hab. apply Es_ctx. exact Hab. Qed.
+
+Instance Es_nfv_Proper (z : atom) : Proper (Es ==> iff) (fun t => In z (nfv t)).
+Proof. intros a b Hab. apply (Es_fv a b Hab z). Qed.
+
+(* The reduction relation modulo Es, as in the paper:
+   t ->sub t' iff there are s, s' with t =Es s ->sm s' =Es t'. *)
+Definition subred (t t' : ntrm) : Prop :=
+  exists s, exists s', Es t s /\ nred s s' /\ Es s' t'.
+
+Lemma subred_intro : forall t s s' t',
+    Es t s -> nred s s' -> Es s' t' -> subred t t'.
+Proof. intros. unfold subred. exists s, s'. split; [| split]; assumption. Qed.
+
+Lemma subred_nred : forall t u, nred t u -> subred t u.
+Proof.
+  intros t u H. apply subred_intro with (s := t) (s' := u).
+  - apply Es_refl.
+  - exact H.
+  - apply Es_refl.
+Qed.
+
+Lemma subred_Es_l : forall t s u, Es t s -> subred s u -> subred t u.
+Proof.
+  intros t s u Ht [a [b [Ha [Hn Hb]]]].
+  apply subred_intro with (s := a) (s' := b).
+  - apply Es_trans with (u := s); assumption.
+  - exact Hn.
+  - exact Hb.
+Qed.
+
+Lemma subred_Es_r : forall t u v, subred t u -> Es u v -> subred t v.
+Proof.
+  intros t u v [a [b [Ha [Hn Hb]]]] Huv.
+  apply subred_intro with (s := a) (s' := b).
+  - exact Ha.
+  - exact Hn.
+  - apply Es_trans with (u := u); assumption.
+Qed.
+
+Lemma subred_Es_lr : forall t s s' t',
+    Es t s -> subred s s' -> Es s' t' -> subred t t'.
+Proof.
+  intros t s s' t' Hts Hss' Hs't'.
+  apply subred_Es_r with (u := s').
+  - apply subred_Es_l with (s := s); assumption.
+  - exact Hs't'.
+Qed.
+
+Lemma subred_context : forall C t t', subred t t' -> subred (nplug C t) (nplug C t').
+Proof.
+  intros C t t' [a [b [Ha [Hn Hb]]]].
+  apply subred_intro with (s := nplug C a) (s' := nplug C b).
+  - apply Es_ctx. exact Ha.
+  - apply nred_ctx. exact Hn.
+  - apply Es_ctx. exact Hb.
+Qed.
+
+Lemma subred_context_rule : forall C t t', nred t t' -> subred (nplug C t) (nplug C t').
+Proof. intros. apply subred_context. apply subred_nred. exact H. Qed.
+
+Lemma subred_of_Es_nred_Es : forall t s s' t',
+    Es t s -> nred s s' -> Es s' t' -> subred t t'.
+Proof. intros. apply subred_intro with (s := s) (s' := s'); assumption. Qed.
+
+(* The rules are stable modulo Es: rewriting the redex or the reduct by Es
+   gives a valid subred step. *)
+Lemma nred_stable_source : forall t s u, Es t s -> nred s u -> subred t u.
+Proof. intros. apply subred_intro with (s := s) (s' := u); [exact H | exact H0 | apply Es_refl]. Qed.
+
+Lemma nred_stable_target : forall t u v, nred t u -> Es u v -> subred t v.
+Proof. intros. apply subred_intro with (s := t) (s' := u); [apply Es_refl | exact H | exact H0]. Qed.
+
+Print Assumptions Es_Equivalence.
+Print Assumptions Es_NApp_Proper.
+Print Assumptions Es_NLam_Proper.
+Print Assumptions Es_NESub_Proper.
+Print Assumptions Es_nplug_Proper.
+Print Assumptions Es_nfv_Proper.
+Print Assumptions subred_nred.
+Print Assumptions subred_Es_l.
+Print Assumptions subred_Es_r.
+Print Assumptions subred_context.
+Print Assumptions nred_stable_source.
+Print Assumptions nred_stable_target.
+
+Inductive StarN (R : ntrm -> ntrm -> Prop) : ntrm -> ntrm -> Prop :=
+| starN_refl : forall t, StarN R t t
+| starN_step : forall t u v, R t u -> StarN R u v -> StarN R t v.
+
+Inductive PlusN (R : ntrm -> ntrm -> Prop) : ntrm -> ntrm -> Prop :=
+| plusN1 : forall t u, R t u -> PlusN R t u
+| plusNS : forall t u v, R t u -> PlusN R u v -> PlusN R t v.
+
+Lemma StarN_trans : forall R a b c, StarN R a b -> StarN R b c -> StarN R a c.
+Proof.
+  intros R a b c H. induction H; intros Hbc.
+  - exact Hbc.
+  - apply starN_step with (u := u). exact H. apply IHStarN. exact Hbc.
+Qed.
+
+Lemma StarN_one_trans : forall R a b c, R a b -> StarN R b c -> StarN R a c.
+Proof. intros. apply starN_step with (u := b); assumption. Qed.
+
+Lemma PlusN_to_StarN : forall R t u, PlusN R t u -> StarN R t u.
+Proof.
+  intros R t u H. induction H.
+  - apply starN_step with (u := u); [exact H | apply starN_refl].
+  - apply starN_step with (u := u); [exact H | exact IHPlusN].
+Qed.
+
+Lemma StarN_subred_context : forall C t t',
+    StarN subred t t' -> StarN subred (nplug C t) (nplug C t').
+Proof.
+  intros C t t' H. induction H.
+  - apply starN_refl.
+  - apply starN_step with (u := nplug C u).
+    + apply subred_context. exact H.
+    + exact IHStarN.
+Qed.
+
+Print Assumptions StarN_trans.
+Print Assumptions StarN_one_trans.
+Print Assumptions PlusN_to_StarN.
+Print Assumptions StarN_subred_context.