From 1c594c4a15de28836713fdaaa367ae35724d7901 Mon Sep 17 00:00:00 2001
From: Benjamin Moosherr <benjamin.moosherr@uni-ulm.de>
Date: Thu, 14 Mar 2024 19:58:35 +0100
Subject: [PATCH] Inline `map-cong` for the termination checker

---
 src/Lang/CCC.lagda.md | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md
index 5ec88942..773da2d5 100644
--- a/src/Lang/CCC.lagda.md
+++ b/src/Lang/CCC.lagda.md
@@ -142,17 +142,8 @@ module Encode where
     ; from = λ _ → tt
     }
 
-  {-|
-  Unfortunately, I had to flag this function as terminating.
-  One solution to prove its termination is to use a sized variant (instead of using ∞).
-  The problem is that the semantics ⟦_⟧ forgets the size and sets it to ∞ and hence,
-  the types of ⟦ encode v ⟧ c and v are different and hence their values can never be equivalent regarding ≡.
-
-  The function below indeed terminates but proving it within our framework became a _technical_ challenge (not a mathematical one) for which I found no solution yet.
-  -}
-  {-# TERMINATING #-}
   ccc-encode-idemp : ∀ {A} (v : Rose ∞ A) → (c : Configuration) → ⟦ encode v ⟧ c ≡ v
-  ccc-encode-idemp v@(rose (a At.-< cs >-)) c =
+  ccc-encode-idemp {A} v@(rose (a At.-< cs >-)) c =
     begin
       ⟦ encode v ⟧ c
     ≡⟨⟩
@@ -161,12 +152,13 @@ module Encode where
           Eq.cong (a At.-<_>-) (map-∘ cs) ⟩
       rose (a At.-< map (λ x → ⟦ encode x ⟧ c) cs >-)
     ≡⟨ Eq.cong rose $
-          Eq.cong (a At.-<_>-) (map-cong (λ x → ccc-encode-idemp x c) cs) ⟩
-      rose (a At.-< map id cs >-)
-    ≡⟨ Eq.cong rose $
-          Eq.cong (a At.-<_>-) (map-id cs) ⟩
+          Eq.cong (a At.-<_>-) (go cs) ⟩
       v
     ∎
+    where
+    go : (cs' : List (Rose ∞ A)) → map (λ c' → ⟦ encode c' ⟧ c) cs' ≡ cs'
+    go [] = refl
+    go (c' ∷ cs') = Eq.cong₂ _∷_ (ccc-encode-idemp c' c) (go cs')
 
   preserves : ∀ {A} → (v : Rose ∞ A)
     → Semantics (Variant-is-VL V) v ≅[ to confs ][ from confs ] ⟦ encode v ⟧