From 6c1a5eaed45d07e044910f86fe243771f6b16365 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Tue, 9 Jul 2024 23:02:06 +0200
Subject: [PATCH] add TransGen lemmas

---
 Pdl/Star.lean | 39 ++++++++++++++++++++++++++++++++-------
 1 file changed, 32 insertions(+), 7 deletions(-)

diff --git a/Pdl/Star.lean b/Pdl/Star.lean
index adbd36f..b0d8004 100644
--- a/Pdl/Star.lean
+++ b/Pdl/Star.lean
@@ -108,26 +108,51 @@ theorem ReflTransGen.iff_finitelyManySteps (r : α → α → Prop) (x z : α) :
     ReflTransGen.from_finitelyManySteps r x z ys ⟨x_is_head, z_is_last, rhs⟩⟩
 
 theorem Relation.ReflTransGen_or_left {r r' : α → α → Prop} {a b : α} :
-  Relation.ReflTransGen r a b
-  → Relation.ReflTransGen (fun x y => r x y ∨ r' x y) a b := by
+    Relation.ReflTransGen r a b
+    → Relation.ReflTransGen (fun x y => r x y ∨ r' x y) a b := by
   intro a_b
   induction a_b
   case refl => exact ReflTransGen.refl
   case tail _ b_c IH => exact ReflTransGen.tail IH (Or.inl b_c)
 
 theorem Relation.ReflTransGen_or_right {r r' : α → α → Prop} {a b : α} :
-  Relation.ReflTransGen r a b
-  → Relation.ReflTransGen (fun x y => r' x y ∨ r x y) a b := by
+    Relation.ReflTransGen r a b
+    → Relation.ReflTransGen (fun x y => r' x y ∨ r x y) a b := by
   intro a_b
   induction a_b
   case refl => exact ReflTransGen.refl
   case tail _ b_c IH => exact ReflTransGen.tail IH (Or.inr b_c)
 
 theorem Relation.ReflTransGen_imp {r r' : α → α → Prop} {a b : α} :
-  (∀ x y, r x y → r' x y)
-  → Relation.ReflTransGen r a b
-  → Relation.ReflTransGen r' a b := by
+    (∀ x y, r x y → r' x y)
+    → Relation.ReflTransGen r a b
+    → Relation.ReflTransGen r' a b := by
   intro hyp a_b
   induction a_b
   case refl => exact ReflTransGen.refl
   case tail _ b_c IH => exact ReflTransGen.tail IH (hyp _ _ b_c)
+
+theorem Relation.TransGen_or_left {r r' : α → α → Prop} {a b : α} :
+    Relation.TransGen r a b
+    → Relation.TransGen (fun x y => r x y ∨ r' x y) a b := by
+  intro a_b
+  induction a_b
+  case single => apply TransGen.single; left; assumption
+  case tail _ b_c IH => exact TransGen.tail IH (Or.inl b_c)
+
+theorem Relation.TransGen_or_right {r r' : α → α → Prop} {a b : α} :
+    Relation.TransGen r a b
+    → Relation.TransGen (fun x y => r' x y ∨ r x y) a b := by
+  intro a_b
+  induction a_b
+  case single => apply TransGen.single; right; assumption
+  case tail _ b_c IH => exact TransGen.tail IH (Or.inr b_c)
+
+theorem Relation.TransGen_imp {r r' : α → α → Prop} {a b : α} :
+    (∀ x y, r x y → r' x y)
+    → Relation.TransGen r a b
+    → Relation.TransGen r' a b := by
+  intro hyp a_b
+  induction a_b
+  case single => apply TransGen.single; apply hyp; assumption
+  case tail _ b_c IH => exact TransGen.tail IH (hyp _ _ b_c)