From 728ed42efc07265667b44f2ca714fec0c6ca6d6d Mon Sep 17 00:00:00 2001 From: milner Date: Tue, 22 Sep 2026 22:43:00 +0200 Subject: [PATCH] add(metaterm): full composition for the term fragment of metaterms (M5 full composition) --- theory/Metaterm.v | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/theory/Metaterm.v b/theory/Metaterm.v index 9ad183e..024e6b8 100644 --- a/theory/Metaterm.v +++ b/theory/Metaterm.v @@ -1,6 +1,6 @@ From Stdlib Require Import List Bool Arith Lia PeanoNat. Import ListNotations. -From LambdaSub Require Import ExecReducer Binding Reduction Closure. +From LambdaSub Require Import ExecReducer Binding Reduction Closure Metatheory. Inductive mtrm : Type := | mBVar : nat -> mtrm @@ -296,3 +296,32 @@ Lemma mred_r_intro : forall C body u, mzfill C 0 = body -> Proof. intros. apply mred_r. exact H. Qed. Print Assumptions mred_r_intro. + +Inductive Plus_m (R : mtrm -> mtrm -> Prop) : mtrm -> mtrm -> Prop := +| plusm1 : forall t u, R t u -> Plus_m R t u +| plusmS : forall t u v, R t u -> Plus_m R u v -> Plus_m R t v. + +Lemma Plus_mred_of_Plus_red1 : forall a b, + Plus red1 a b -> Plus_m mred (of_trm a) (of_trm b). +Proof. + intros a b H. induction H as [a0 b0 HR | a0 b0 u0 HR HP IH]. + - apply plusm1. apply mred_emb. exact HR. + - apply plusmS with (u := of_trm b0). + + apply mred_emb. exact HR. + + exact IH. +Qed. + +Lemma mred_full_comp_pure : forall body u, + Plus_m mred (mESub (of_trm body) (of_trm u)) (of_trm (open_rec 0 u body)). +Proof. + intros body u. + change (Plus_m mred (of_trm (ESub body u)) (of_trm (open_rec 0 u body))). + apply Plus_mred_of_Plus_red1. apply lemma_2_2_full_comp. +Qed. + +Lemma mred_plus_one : forall a b, red1 a b -> Plus_m mred (of_trm a) (of_trm b). +Proof. intros. apply plusm1. apply mred_emb. exact H. Qed. + +Print Assumptions Plus_mred_of_Plus_red1. +Print Assumptions mred_full_comp_pure. +Print Assumptions mred_plus_one.