From 6235dee2ee06eeb8bf8af64fa094dd3dce0cc782 Mon Sep 17 00:00:00 2001 From: milner Date: Wed, 23 Sep 2026 00:54:00 +0200 Subject: [PATCH] add(named): an Es setoid rewriting layer with the modulo reduction (M5 metatheory) --- scripts/audit.sh | 2 +- scripts/extract_metadata.py | 4 + theory/NamedEs.v | 173 ++++++++++++++++++++++++++++++++++++ 3 files changed, 178 insertions(+), 1 deletion(-) create mode 100644 theory/NamedEs.v diff --git a/scripts/audit.sh b/scripts/audit.sh index 7ad07f4..35692b5 100755 --- a/scripts/audit.sh +++ b/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" diff --git a/scripts/extract_metadata.py b/scripts/extract_metadata.py index 0173a34..3e6d5df 100755 --- a/scripts/extract_metadata.py +++ b/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", diff --git a/theory/NamedEs.v b/theory/NamedEs.v new file mode 100644 index 0000000..d4bc8f4 --- /dev/null +++ b/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.