add TransGen lemmas

m4lvin · Jul 9, 2024 · 6c1a5ea · 6c1a5ea
1 parent 31420fc
commit 6c1a5ea
Showing 1 changed file with 32 additions and 7 deletions.
diff --git 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)