From 76e3b49f7cbb2dd6b1cc74f771dacd2dec632563 Mon Sep 17 00:00:00 2001
From: Anatolay <nihonvasserman228@gmail.com>
Date: Fri, 16 Aug 2024 11:18:44 +0300
Subject: [PATCH] Add utility definitions

---
 Extended/Reduction/Parallel/Definition.lean | 26 +++++++++++++++++++++
 Extended/Reduction/Regular/Definition.lean  |  7 ++++++
 2 files changed, 33 insertions(+)

diff --git a/Extended/Reduction/Parallel/Definition.lean b/Extended/Reduction/Parallel/Definition.lean
index 7369a146..e62feff8 100644
--- a/Extended/Reduction/Parallel/Definition.lean
+++ b/Extended/Reduction/Parallel/Definition.lean
@@ -198,3 +198,29 @@ inductive PReduce : Ctx → Term → Term → Type where
     → PReduce ctx glob glob
 
 end
+
+def PReducesTo (t t' : Term) := PReduce {glob := t, scope := t} t t'
+def PReducesToMany := ReflTransGen PReducesTo
+
+infix:20 " ⇛ " => PReducesTo
+infix:20 " ⇛* " => PReducesToMany
+
+def get_form_premise
+  {attrs : List Attr}
+  {ρ : Option Term}
+  {bnds bnds' : Bindings attrs}
+  {ctx : Ctx}
+  (preduce : PReduce ctx (obj ρ bnds) (obj ρ bnds'))
+  : FormationPremise {glob := ctx.glob, scope := obj ρ bnds} bnds bnds'
+  := match preduce with
+    | .pr_cong_obj premise => premise
+
+def get_application_premise
+  {attrs : List Attr}
+  {t : Term}
+  {apps apps' : Record Term attrs}
+  {ctx : Ctx}
+  (preduce : PReduce ctx (app t apps) (app t apps'))
+  : ApplicationPremise ctx apps apps'
+  := match preduce with
+    | .pr_cong_app premise _ => premise
diff --git a/Extended/Reduction/Regular/Definition.lean b/Extended/Reduction/Regular/Definition.lean
index ec31a357..2684d1ad 100644
--- a/Extended/Reduction/Regular/Definition.lean
+++ b/Extended/Reduction/Regular/Definition.lean
@@ -159,3 +159,10 @@ inductive Reduce : Ctx → Term → Term → Type where
         {glob := g, scope := l}
         (obj ρ bnds)
         (obj ρ (Record.insert bnds attr t'))
+
+
+def ReducesTo (t t' : Term) := Reduce {glob := t, scope := t} t t'
+def ReducesToMany := ReflTransGen ReducesTo
+
+infix:20 " ⇝ " => ReducesTo
+infix:20 " ⇝* " => ReducesToMany