Generalize reflexive transitive closure

Strata/DL/Imperative/StmtSemanticsSmallStep.lean

@@ -5,6 +5,7 @@
 -/
 
 import Strata.DL.Imperative.CmdSemantics
+import Strata.DL.Util.Relations
 
 ---------------------------------------------------------------------
 
@@ -111,20 +112,14 @@ inductive StepStmt
 /--
 Multi-step execution: reflexive transitive closure of single steps.
 -/
-inductive StepStmtStar
+def StepStmtStar
   {CmdT : Type}
   (P : PureExpr)
   (EvalCmd : EvalCmdParam P CmdT)
   [HasVarsImp P (List (Stmt P CmdT))]
   [HasVarsImp P CmdT] [HasFvar P] [HasVal P]
   [HasBool P] [HasNot P] :
-  SemanticEval P → SemanticStore P → Config P CmdT → Config P CmdT → Prop where
-  | refl :
-    StepStmtStar P EvalCmd δ σ c c
-  | step :
-    StepStmt P EvalCmd δ σ c₁ c₂ →
-    StepStmtStar P EvalCmd δ σ c₂ c₃ →
-    StepStmtStar P EvalCmd δ σ c₁ c₃
+  SemanticEval P → SemanticStore P → Config P CmdT → Config P CmdT → Prop := fun δ σ => ReflTrans (StepStmt P EvalCmd δ σ)
 
 /-- A statement evaluates successfully if it can step to a terminal
 configuration.
@@ -174,9 +169,9 @@ theorem evalStmtsSmallNil
   (EvalCmd : EvalCmdParam P CmdT) :
   EvalStmtsSmall P EvalCmd δ σ [] σ := by
     unfold EvalStmtsSmall
-    apply StepStmtStar.step
+    apply ReflTrans.step
     · exact StepStmt.step_stmts_nil
-    · exact StepStmtStar.refl
+    · apply ReflTrans.refl
 
 /--
 Configuration is terminal if no further steps are possible.

Strata/DL/Lambda/Semantics.lean

@@ -8,6 +8,7 @@ import Strata.DL.Lambda.LExpr
 import Strata.DL.Lambda.LExprEval
 import Strata.DL.Lambda.LExprWF
 import Strata.DL.Lambda.LState
+import Strata.DL.Util.Relations
 
 ---------------------------------------------------------------------
 
@@ -136,10 +137,8 @@ theorem step_const_stuck:
 /--
 Multi-step execution: reflexive transitive closure of single steps.
 -/
-inductive StepStar (F:@Factory Tbase) (rf:Env Tbase)
-  : LExpr Tbase.mono → LExpr Tbase.mono → Prop where
-| refl : StepStar F rf e e
-| step : ∀ e e' e'', Step F rf e e' → StepStar F rf e' e''
-        → StepStar F rf e e''
+def StepStar (F:@Factory Tbase) (rf:Env Tbase)
+  : LExpr Tbase.mono → LExpr Tbase.mono → Prop :=
+  ReflTrans (Step F rf)
 
 end Lambda

Strata/DL/Util/Relations.lean

@@ -0,0 +1,28 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+section Relation
+
+def Relation (A: Type) := A → A → Prop
+def Reflexive (r: Relation A) : Prop := ∀ x, r x x
+def Transitive (r: Relation A) : Prop := ∀ x y z, r x y → r y z → r x z
+
+inductive ReflTrans {A: Type} (r: Relation A) : Relation A where
+  | refl : ∀ x, ReflTrans r x x
+  | step: ∀ x y z, r x y → ReflTrans r y z → ReflTrans r x z
+
+theorem ReflTrans_Reflexive {A: Type} (r: Relation A):
+  Reflexive (ReflTrans r) := by apply ReflTrans.refl
+
+theorem ReflTrans_Transitive {A: Type} (r: Relation A):
+  Transitive (ReflTrans r) := by
+  unfold Transitive; intros x y z rxy
+  induction rxy generalizing z
+  case refl => simp
+  case step x1 y1 z1 rxy1 ryz1 IH =>
+    intros rzz1;
+    apply (ReflTrans.step _ y1 _ rxy1 (IH _ rzz1))
+
+end Relation

StrataTest/DL/Lambda/LExprEvalTests.lean

@@ -33,11 +33,11 @@ macro "discharge_isCanonicalValue": tactic => `(tactic|
   )
 -- Take a small step.
 macro "take_step": tactic => `(tactic |
-    (conv => lhs; reduce) <;> apply StepStar.step
+    (conv => lhs; reduce) <;> apply ReflTrans.step
   )
 -- Finish taking small steps!
 macro "take_refl": tactic => `(tactic |
-    (conv => lhs; reduce) <;> apply StepStar.refl
+    (conv => lhs; reduce) <;> apply ReflTrans.refl
   )
 -- Do beta reduction.
 macro "reduce_beta": tactic => `(tactic |
@@ -112,7 +112,7 @@ example: steps_well test2 := by
   · apply Step.eq_reduce <;> try discharge_isCanonicalValue
     · inhabited_metadata
   take_step; apply Step.ite_reduce_else
-  apply StepStar.refl
+  apply ReflTrans.refl
 
 
 def test3 := TestCase.mk