Reverse the index of ReflexiveTransitiveClosureᵢ

IntersectMBO · Apr 29, 2024 · 42bca56 · 42bca56
1 parent ed315b0
commit 42bca56
Showing 1 changed file with 23 additions and 14 deletions.
diff --git a/src/Interface/STS.agda b/src/Interface/STS.agda
@@ -35,6 +35,7 @@ private
            s s' s'' : S
            sig : Sig
            sigs : List Sig
+           n : ℕ
 
 -- small-step to big-step transformer
 
@@ -50,21 +51,24 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Set) (_⊢_⇀⟦_⟧_
         Γ ⊢ s  ⇀⟦ sig  ⟧  s'
       → Γ ⊢ s' ⇀⟦ sigs ⟧* s''
         ───────────────────────────────────────
-        Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''
+        Γ ⊢ s  ⇀⟦ sig ∷ sigs ⟧* s''
 
 module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Set) (_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Set) where
-  data _⊢_⇀⟦_⟧ᵢ*_ : C → S → List Sig → S → Set where
+  data _⊢_⇀⟦_⟧ᵢ*'_ : C × ℕ → S → List Sig → S → Set where
 
     BS-base :
       Γ ⊢ s ⇀⟦ _ ⟧ᵇ s'
       ───────────────────────────────────────
-      Γ ⊢ s ⇀⟦ [] ⟧ᵢ* s'
+      (Γ , n) ⊢ s ⇀⟦ [] ⟧ᵢ*' s'
 
     BS-ind :
-        (Γ , length sigs) ⊢ s  ⇀⟦ sig  ⟧  s'
-      → Γ                ⊢ s' ⇀⟦ sigs ⟧ᵢ* s''
+        (Γ , n)     ⊢ s  ⇀⟦ sig  ⟧  s'
+      → (Γ , suc n) ⊢ s' ⇀⟦ sigs ⟧ᵢ*' s''
         ───────────────────────────────────────
-        Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧ᵢ* s''
+        (Γ , n)     ⊢ s  ⇀⟦ sig ∷ sigs ⟧ᵢ*' s''
+
+  _⊢_⇀⟦_⟧ᵢ*_ : C → S → List Sig → S → Set
+  _⊢_⇀⟦_⟧ᵢ*_ Γ = _⊢_⇀⟦_⟧ᵢ*'_ (Γ , 0)
 
 data IdSTS {C S} : C → S → ⊤ → S → Set where
   Id-nop : IdSTS Γ s _ s
@@ -73,9 +77,11 @@ data IdSTS {C S} : C → S → ⊤ → S → Set where
 ReflexiveTransitiveClosure : (C → S → Sig → S → Set) → C → S → List Sig → S → Set
 ReflexiveTransitiveClosure = _⊢_⇀⟦_⟧*_ IdSTS
 
+STS-total : (C → S → Sig → S → Set) → Set
+STS-total _⊢_⇀⟦_⟧_ = ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s'
+
 ReflexiveTransitiveClosure-total : {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Set}
-            → (∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s')
-            → (∀ {Γ s sig} → ∃[ s' ] ReflexiveTransitiveClosure _⊢_⇀⟦_⟧_ Γ s sig s')
+  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosure _⊢_⇀⟦_⟧_)
 ReflexiveTransitiveClosure-total SS-total {Γ} {s} {[]} = s , BS-base Id-nop
 ReflexiveTransitiveClosure-total SS-total {Γ} {s} {x ∷ sig} =
   case SS-total of λ where
@@ -85,12 +91,15 @@ ReflexiveTransitiveClosureᵢ : (C × ℕ → S → Sig → S → Set) → C →
 ReflexiveTransitiveClosureᵢ = _⊢_⇀⟦_⟧ᵢ*_ IdSTS
 
 ReflexiveTransitiveClosureᵢ-total : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Set}
-             → (∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s')
-             → (∀ {Γ s sig} → ∃[ s' ] ReflexiveTransitiveClosureᵢ _⊢_⇀⟦_⟧_ Γ s sig s')
-ReflexiveTransitiveClosureᵢ-total SS-total {s = s} {[]} = s , BS-base Id-nop
-ReflexiveTransitiveClosureᵢ-total SS-total {s = s} {x ∷ sig} =
-  case SS-total of λ where
-    (s' , Ps') → map₂′ (BS-ind Ps') $ ReflexiveTransitiveClosureᵢ-total SS-total
+  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosureᵢ _⊢_⇀⟦_⟧_)
+ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total
+  where
+    helper : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Set}
+      → STS-total _⊢_⇀⟦_⟧_ → STS-total (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⟦_⟧_)
+    helper SS-total {s = s} {[]} = s , BS-base Id-nop
+    helper SS-total {s = s} {x ∷ sig} =
+      case SS-total of λ where
+        (s' , Ps') → map₂′ (BS-ind Ps') $ helper SS-total
 
 -- with a given base case
 ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_