Prove that resume and eval are inverses

Author: WhatisRT

formal-spec/CategoricalCrypto/SFun.agda

@@ -7,6 +7,7 @@ open import abstract-set-theory.Prelude hiding (id; _∘_; _⊗_; lookup; Dec; 
 import abstract-set-theory.Prelude as P
 open import Data.Vec hiding (init)
 open import Data.Nat using (_+_)
+open import Relation.Binary
 
 -- M = id, Maybe, Powerset (relation), Giry (probability)
 -- SFunType A B S = S × A → M (S × B)
@@ -45,6 +46,11 @@ record SFunⁱ (A B : Type) : Type where
   apply₁ : A → SFunⁱ A B
   apply₁ a = record { fun = λ as → tail (fun (a ∷ as)) ; take-fun = {!!} }
 
+module _ where
+  open SFunⁱ
+  fun-∷ : ∀ {f : SFunⁱ A B} {a} {as : Vec A n} → fun f (a ∷ as) ≡ fun₁ f a ∷ fun (apply₁ f a) as
+  fun-∷ = {!!}
+
 eval : SFunᵉ A B → SFunⁱ A B
 eval f = let open SFunᵉ f in record { fun = trace fun init ; take-fun = take-trace }
 
@@ -57,12 +63,58 @@ resume f = record
 _≈ⁱ_ : SFunⁱ A B → SFunⁱ A B → Type
 f ≈ⁱ g = let open SFunⁱ in ∀ {n} → fun f {n} ≗ fun g {n}
 
-open SFunⁱ
-≈ⁱ-ind : ∀ {f g : SFunⁱ A B} a → fun₁ f a ≡ fun₁ g a → apply₁ f a ≈ⁱ apply₁ g a → f ≈ⁱ g
-≈ⁱ-ind = {!!}
-
 _≈ᵉ_ : SFunᵉ A B → SFunᵉ A B → Type
 f ≈ᵉ g = eval f ≈ⁱ eval g
 
+eval∘resume≡id : ∀ {f : SFunⁱ A B} → eval (resume f) ≈ⁱ f
+eval∘resume≡id {f = f} [] with SFunⁱ.fun f []
+... | [] = refl
+eval∘resume≡id {f = f} (a ∷ as) = begin
+  head (fun f (a ∷ [])) ∷ fun (eval (resume (apply₁ f a))) as
+    ≡⟨ cong (_ ∷_) (eval∘resume≡id as) ⟩
+  fun₁ f a ∷ fun (apply₁ f a) as
+    ≡⟨ sym (fun-∷ {f = f}) ⟩
+  fun f (a ∷ as) ∎
+  where open ≡-Reasoning
+        open SFunⁱ
+
 resume∘eval≡id : ∀ {f : SFunᵉ A B} → resume (eval f) ≈ᵉ f
-resume∘eval≡id {f = f} {n} as = {!!}
+resume∘eval≡id {f = f} {n} = eval∘resume≡id {f = eval f}
+
+IsEquivalence-≈ⁱ : IsEquivalence (_≈ⁱ_ {A} {B})
+IsEquivalence-≈ⁱ = {!!}
+
+IsEquivalence-≈ᵉ : IsEquivalence (_≈ᵉ_ {A} {B})
+IsEquivalence-≈ᵉ = {!!}
+
+SFunⁱ-Setoid : (A B : Type) → Setoid ℓ0 ℓ0
+SFunⁱ-Setoid A B = record { Carrier = SFunⁱ A B ; _≈_ = _≈ⁱ_ ; isEquivalence = IsEquivalence-≈ⁱ }
+
+SFunᵉ-Setoid : (A B : Type) → Setoid (sucˡ ℓ0) ℓ0
+SFunᵉ-Setoid A B = record { Carrier = SFunᵉ A B ; _≈_ = _≈ᵉ_ ; isEquivalence = IsEquivalence-≈ᵉ }
+
+import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+
+Inverse-resume-eval : Inverse (SFunⁱ-Setoid A B) (SFunᵉ-Setoid A B)
+Inverse-resume-eval {A} {B} = record { to = resume ; from = eval ; Go }
+  where
+    open SetoidReasoning (SFunⁱ-Setoid A B)
+    module Go where
+      to-cong : Congruent _≈ⁱ_ _≈ᵉ_ resume
+      to-cong {x} {y} x≈y = begin
+        eval (resume x) ≈⟨ eval∘resume≡id ⟩ x ≈⟨ x≈y ⟩ y ≈⟨ eval∘resume≡id ⟨ eval (resume y) ∎
+      from-cong : Congruent _≈ᵉ_ _≈ⁱ_ eval
+      from-cong f≈g = f≈g
+      inverse : Inverseᵇ _≈ⁱ_ _≈ᵉ_ resume eval
+      inverse = (λ {x} {y} y≈eval[x] → begin
+                 eval (resume y)
+                   ≈⟨ from-cong (to-cong y≈eval[x]) ⟩
+                 eval (resume (eval x))
+                   ≈⟨ resume∘eval≡id ⟩
+                 eval x ∎)
+              , λ {x} {y} y≈resume[x] → begin
+                  eval y
+                    ≈⟨ from-cong y≈resume[x] ⟩
+                  eval (resume x)
+                    ≈⟨ eval∘resume≡id ⟩
+                  x ∎