text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT

module stash.modalities.gbm.GbmUtil where

  BM-Relation : ∀ {ℓ} (M : Modality ℓ) {A : Type ℓ} {B : Type ℓ} (Q : A → B → Type ℓ) → Type ℓ
  BM-Relation M {A} {B} Q =
    {a₀ : A} {b₀ : B} (q₀ : Q a₀ b₀)
    {a₁ : A} (q₁ : Q a₁ b₀)
    {b₁ : B} (q₂ : Q a₀ b₁) →
    Modality.is-◯-connected M (((a₀ , q₀) == (a₁ , q₁)) * ((b₀ , q₀) == (b₁ , q₂)))

  prop-lemma : ∀ {ℓ} {A : Type ℓ} {a₀ a₁ : A} (P : A → hProp ℓ)
               (p : a₀ == a₁) (x₀ : (fst ∘ P) a₀) (x₁ : (fst ∘ P) a₁) →
               x₀ == x₁ [ (fst ∘ P) ↓ p ]
  prop-lemma P idp x₀ x₁ = prop-has-all-paths (snd (P _)) x₀ x₁

  pths-ovr-is-prop : ∀ {ℓ} {A : Type ℓ} {a₀ a₁ : A} (P : A → hProp ℓ)
                     (p : a₀ == a₁) (x₀ : (fst ∘ P) a₀) (x₁ : (fst ∘ P) a₁) →
                     is-prop (x₀ == x₁ [ (fst ∘ P) ↓ p ])
  pths-ovr-is-prop P idp x₀ x₁ = =-preserves-level (snd (P _))

  pths-ovr-contr : ∀ {ℓ} {A : Type ℓ} {a₀ a₁ : A} (P : A → hProp ℓ)
                     (p : a₀ == a₁) (x₀ : (fst ∘ P) a₀) (x₁ : (fst ∘ P) a₁) →
                     is-contr (x₀ == x₁ [ (fst ∘ P) ↓ p ])
  pths-ovr-contr P idp x₀ x₁ = =-preserves-level (inhab-prop-is-contr x₀ (snd (P _)))

  eqv-square : ∀ {i j} {A : Type i} {B : Type j} (e : A ≃ B)
    {b b' : B} (p : b == b')
    → ap (–> e ∘ <– e) p == (<–-inv-r e b) ∙ p ∙ (! (<–-inv-r e b'))
  eqv-square e idp = ! (!-inv-r (<–-inv-r e _))

  eqv-square' : ∀ {i j} {A : Type i} {B : Type j} (e : A ≃ B)
    {a a' : A} (p : a == a')
    → ap (<– e ∘ –> e) p == <–-inv-l e a ∙ p ∙ ! (<–-inv-l e a')
  eqv-square' e idp = ! (!-inv-r (<–-inv-l e _))

  ↓-==-in : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
    {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → (u ∙ ap g p) == (ap f p ∙ v)
    → (u == v [ (λ x → f x == g x) ↓ p ])
  ↓-==-in {p = idp} q = ! (∙-unit-r _) ∙ q

  ↓-==-out : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
    {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → (u == v [ (λ x → f x == g x) ↓ p ])
    → (u ∙ ap g p) == (ap f p ∙ v)
  ↓-==-out {p = idp} q = (∙-unit-r _) ∙ q

  module HFiberSrcEquiv {i₀ i₁ i₂} {A : Type i₀} {B : Type i₁} {C : Type i₂}
    (f : A → B) (h : B → C) (k : A → C)
    (w : (a : A) → h (f a) == k a)
    (ise-f : is-equiv f)
    where

     private
       g = is-equiv.g ise-f
       f-g = is-equiv.f-g ise-f
       g-f = is-equiv.g-f ise-f
       adj = is-equiv.adj ise-f
       adj' = is-equiv.adj' ise-f

       to : (c : C) → hfiber k c → hfiber h c
       to .(k a) (a , idp) = f a , w a

       to-lem₀ : (c : C) (x : hfiber k c) → fst (to c x) == f (fst x)
       to-lem₀ .(k a) (a , idp) = idp

       to-lem₁ : (c : C) (x : hfiber k c) → snd (to c x) == ap h (to-lem₀ c x) ∙ w (fst x) ∙ snd x
       to-lem₁ .(k a) (a , idp) = ! (∙-unit-r (w a))

       from : (c : C) → hfiber h c → hfiber k c
       from .(h b) (b , idp) = g b , ! (w (g b)) ∙ ap h (f-g b)

       from-lem₀ : (c : C) (x : hfiber h c) → fst (from c x) == g (fst x)
       from-lem₀ .(h b) (b , idp) = idp

       from-lem₁ : (c : C) (x : hfiber h c) → snd (from c x) == ap k (from-lem₀ c x) ∙ (! (w (g (fst x)))) ∙ ap h (f-g (fst x)) ∙ snd x
       from-lem₁ .(h b) (b , idp) = ap (λ p → ! (w (g b)) ∙ p) (! (∙-unit-r (ap h (f-g b))))

       to-from : (c : C) (x : hfiber h c) → to c (from c x) == x
       to-from .(h b) (b , idp) = pair= (q ∙ f-g b) (↓-app=cst-in (r ∙ eq))

         where c = h b
               p = ! (w (g b)) ∙ ap h (f-g b)
               q = to-lem₀ c (g b , p)
               r = to-lem₁ c (g b , p)

               eq = ap h q ∙ w (g b) ∙ ! (w (g b)) ∙ ap h (f-g b)
                      =⟨ ! (∙-assoc (w (g b)) (! (w (g b))) (ap h (f-g b))) |in-ctx (λ x → ap h q ∙ x) ⟩
                    ap h q ∙ (w (g b) ∙ (! (w (g b)))) ∙ ap h (f-g b)
                      =⟨ !-inv-r (w (g b)) |in-ctx (λ x → ap h q ∙ x ∙ ap h (f-g b)) ⟩
                    ap h q ∙ ap h (f-g b)
                      =⟨ ∙-ap h q (f-g b) ⟩
                    ap h (q ∙ f-g b)
                      =⟨ ! (∙-unit-r (ap h (q ∙ f-g b))) ⟩
                    ap h (q ∙ f-g b) ∙ idp ∎

       from-to : (c : C) (x : hfiber k c) → from c (to c x) == x
       from-to .(k a) (a , idp) = pair= (p ∙ g-f a) (↓-app=cst-in (q ∙ eq))

         where c = k a
               p = from-lem₀ c (f a , w a)
               q = from-lem₁ c (f a , w a)

               eq = ap k p ∙ ! (w (g (f a))) ∙ ap h (f-g (f a)) ∙ w a
                       =⟨ ! (adj a) |in-ctx (λ x → ap k p ∙ ! (w (g (f a))) ∙ ap h x ∙ w a) ⟩
                    ap k p ∙ ! (w (g (f a))) ∙ ap h (ap f (g-f a)) ∙ w a
                       =⟨ ∘-ap h f (g-f a) |in-ctx (λ x → ap k p ∙ ! (w (g (f a))) ∙ x ∙ w a) ⟩
                    ap k p ∙ ! (w (g (f a))) ∙ ap (h ∘ f) (g-f a) ∙ w a
                       =⟨ ! (↓-='-out (apd w (g-f a))) |in-ctx (λ x → ap k p ∙ ! (w (g (f a))) ∙ x) ⟩
                    ap k p ∙ ! (w (g (f a))) ∙ w (g (f a)) ∙' ap k (g-f a)
                       =⟨ ∙'=∙ (w (g (f a))) (ap k (g-f a)) |in-ctx (λ x → ap k p ∙ ! (w (g (f a))) ∙ x) ⟩
                    ap k p ∙ ! (w (g (f a))) ∙ w (g (f a)) ∙ ap k (g-f a)
                       =⟨ ! (∙-assoc (! (w (g (f a)))) (w (g (f a))) (ap k (g-f a))) |in-ctx (λ x → ap k p ∙ x) ⟩
                    ap k p ∙ (! (w (g (f a))) ∙ w (g (f a))) ∙ ap k (g-f a)
                       =⟨ !-inv-l (w (g (f a))) |in-ctx (λ x → ap k p ∙ x ∙ ap k (g-f a)) ⟩
                    ap k p ∙ ap k (g-f a)
                       =⟨ ∙-ap k p (g-f a) ⟩
                    ap k (p ∙ g-f a)
                      =⟨ ! (∙-unit-r (ap k (p ∙ g-f a))) ⟩
                    ap k (p ∙ g-f a) ∙ idp ∎

     eqv : (c : C) → hfiber k c ≃ hfiber h c
     eqv c = equiv (to c) (from c) (to-from c) (from-to c)

  module HFiberTgtEquiv {i₀ i₁ i₂} {A : Type i₀} {B : Type i₁} {C : Type i₂}
    (h : A → B) (k : A → C) (f : B → C)
    (w : (a : A) → k a == f (h a))
    (ise-f : is-equiv f)
    where

     private
       g = is-equiv.g ise-f
       f-g = is-equiv.f-g ise-f
       g-f = is-equiv.g-f ise-f
       adj = is-equiv.adj ise-f
       adj' = is-equiv.adj' ise-f

       to : (b : B) → hfiber h b → hfiber k (f b)
       to .(h a) (a , idp) = a , w a

       to-lem₀ : (b : B) (x : hfiber h b) → fst (to b x) == fst x
       to-lem₀ .(h a) (a , idp) = idp

       to-lem₁ : (b : B) (x : hfiber h b) → snd (to b x) == ap k (to-lem₀ b x) ∙ w (fst x) ∙ ap f (snd x)
       to-lem₁ .(h a) (a , idp) = ! (∙-unit-r (w a))

       from : (b : B) → hfiber k (f b) → hfiber h b
       from b (a , p) = a , (! (g-f (h a)) ∙ ap g (! (w a) ∙ p) ∙ g-f b)

       to-from : (b : B) (x : hfiber k (f b)) → to b (from b x) == x
       to-from b (a , p) = pair= r (↓-app=cst-in (s ∙ (ap (λ x → ap k r ∙ x) eq)))

         where q = ! (g-f (h a)) ∙ ap g (! (w a) ∙ p) ∙ g-f b
               r = to-lem₀ b (a , q)
               s = to-lem₁ b (a , q)

               eq = w a ∙ ap f q
                      =⟨ ! (∙-ap f (! (g-f (h a))) (ap g (! (w a) ∙ p) ∙ g-f b)) |in-ctx (λ x → w a ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ ap f (ap g (! (w a) ∙ p) ∙ g-f b)
                      =⟨ ! (∙-ap f (ap g (! (w a) ∙ p)) (g-f b)) |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ ap f (ap g (! (w a) ∙ p)) ∙ ap f (g-f b)
                      =⟨ ∘-ap f g (! (w a) ∙ p) |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ x ∙ ap f (g-f b)) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ ap (f ∘ g) (! (w a) ∙ p) ∙ ap f (g-f b)
                      =⟨ ap (λ x → w a ∙ ap f (! (g-f (h a))) ∙ x ∙ ap f (g-f b)) (eqv-square (f , ise-f) (! (w a) ∙ p)) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ (f-g (f (h a)) ∙ (! (w a) ∙ p) ∙ ! (f-g (f b))) ∙ ap f (g-f b)
                      =⟨ adj b |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ (f-g (f (h a)) ∙ (! (w a) ∙ p) ∙ ! (f-g (f b))) ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ (f-g (f (h a)) ∙ (! (w a) ∙ p) ∙ ! (f-g (f b))) ∙ f-g (f b)
                      =⟨ ∙-assoc (f-g (f (h a))) ((! (w a) ∙ p) ∙ ! (f-g (f b))) (f-g (f b)) |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ ((! (w a) ∙ p) ∙ ! (f-g (f b))) ∙ f-g (f b)
                      =⟨ ∙-assoc (! (w a) ∙ p) (! (f-g (f b))) (f-g (f b)) |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ (! (w a) ∙ p) ∙ ! (f-g (f b)) ∙ f-g (f b)
                      =⟨ !-inv-l (f-g (f b)) |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ (! (w a) ∙ p) ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ (! (w a) ∙ p) ∙ idp
                      =⟨ ∙-unit-r (! (w a) ∙ p) |in-ctx (λ x → w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ x) ⟩
                    w a ∙ ap f (! (g-f (h a))) ∙ f-g (f (h a)) ∙ ! (w a) ∙ p
                      =⟨ ap-! f (g-f (h a)) |in-ctx (λ x → w a ∙ x ∙ f-g (f (h a)) ∙ ! (w a) ∙ p) ⟩
                    w a ∙ ! (ap f (g-f (h a))) ∙ f-g (f (h a)) ∙ ! (w a) ∙ p
                      =⟨ ! (adj (h a)) |in-ctx (λ x → w a ∙ ! (ap f (g-f (h a))) ∙ x ∙ ! (w a) ∙ p) ⟩
                    w a ∙ ! (ap f (g-f (h a))) ∙ ap f (g-f (h a)) ∙ ! (w a) ∙ p
                      =⟨ ! (∙-assoc (! (ap f (g-f (h a)))) (ap f (g-f (h a))) (! (w a) ∙ p)) |in-ctx (λ x → w a ∙ x)⟩
                    w a ∙ (! (ap f (g-f (h a))) ∙ ap f (g-f (h a))) ∙ ! (w a) ∙ p
                      =⟨ !-inv-l (ap f (g-f (h a))) |in-ctx (λ x → w a ∙ x ∙ ! (w a) ∙ p)⟩
                    w a ∙ ! (w a) ∙ p
                      =⟨ ! (∙-assoc (w a) (! (w a)) p) ⟩
                    (w a ∙ ! (w a)) ∙ p
                      =⟨ !-inv-r (w a) |in-ctx (λ x → x ∙ p) ⟩
                    p ∎

       from-to : (b : B) (x : hfiber h b) → from b (to b x) == x
       from-to .(h a) (a , idp) = pair= idp eq

         where eq = ! (g-f (h a)) ∙ ap g (! (w a) ∙ w a) ∙ g-f (h a)
                      =⟨ !-inv-l (w a)|in-ctx (λ x → ! (g-f (h a)) ∙ ap g x ∙ g-f (h a)) ⟩
                    ! (g-f (h a)) ∙ g-f (h a)
                      =⟨ !-inv-l (g-f (h a)) ⟩
                    idp ∎

     eqv : (b : B) → hfiber h b ≃ hfiber k (f b)
     eqv b = equiv (to b) (from b) (to-from b) (from-to b)

  module HFiberSqEquiv {i₀ i₁ j₀ j₁}
    {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
    (f₀ : A₀ → B₀) (f₁ : A₁ → B₁) (hA : A₀ → A₁) (hB : B₀ → B₁)
    (sq : CommSquare f₀ f₁ hA hB) (ise-hA : is-equiv hA) (ise-hB : is-equiv hB) where

    open CommSquare

    private
      gB = is-equiv.g ise-hB

    module Src = HFiberSrcEquiv hA f₁ (hB ∘ f₀) (λ a₀ → ! (commutes sq a₀)) ise-hA
    module Tgt = HFiberTgtEquiv f₀ (f₁ ∘ hA) hB (λ a₀ → ! (commutes sq a₀)) ise-hB

    eqv : (b₀ : B₀) → hfiber f₀ b₀ ≃ hfiber f₁ (hB b₀)
    eqv b₀ = Src.eqv (hB b₀)
      ∘e coe-equiv (ap (λ s → hfiber s (hB b₀)) (λ= (λ a₀ → ! (commutes sq a₀))))
      ∘e Tgt.eqv b₀

  hfiber-sq-eqv : ∀ {i₀ i₁ j₀ j₁}
    {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
    (f₀ : A₀ → B₀) (f₁ : A₁ → B₁) (hA : A₀ → A₁) (hB : B₀ → B₁)
    (sq : CommSquare f₀ f₁ hA hB) (ise-hA : is-equiv hA) (ise-hB : is-equiv hB) →
    (b₀ : B₀) → hfiber f₀ b₀ ≃ hfiber f₁ (hB b₀)
  hfiber-sq-eqv f₀ f₁ hA hB sq ise-hA ise-hB b₀ = M.eqv b₀

    where module M = HFiberSqEquiv f₀ f₁ hA hB sq ise-hA ise-hB

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import homotopy.EilenbergMacLane
open import groups.ToOmega
open import cohomology.Theory
open import cohomology.SpectrumModel

module cohomology.EMModel where

module _ {i} (G : AbGroup i) where

  open EMExplicit G using (⊙EM; EM-level; EM-conn; spectrum)

  private
    E : (n : ℤ) → Ptd i
    E (pos m) = ⊙EM m
    E (negsucc m) = ⊙Lift ⊙Unit

    E-spectrum : (n : ℤ) → ⊙Ω (E (succ n)) ⊙≃ E n
    E-spectrum (pos n) = spectrum n
    E-spectrum (negsucc O) = ≃-to-⊙≃ {X = ⊙Ω (E 0)}
      (equiv (λ _ → _) (λ _ → idp)
             (λ _ → idp) (prop-has-all-paths _))
      idp
    E-spectrum (negsucc (S n)) = ≃-to-⊙≃ {X = ⊙Ω (E (negsucc n))}
      (equiv (λ _ → _) (λ _ → idp)
             (λ _ → idp) (prop-has-all-paths {{=-preserves-level ⟨⟩}} _))
      idp

  EM-Cohomology : CohomologyTheory i
  EM-Cohomology = spectrum-cohomology E E-spectrum

  open CohomologyTheory EM-Cohomology

  EM-dimension : {n : ℤ} → n ≠ 0 → is-trivialᴳ (C n (⊙Lift ⊙S⁰))
  EM-dimension {pos O} neq = ⊥-rec (neq idp)
  EM-dimension {pos (S n)} _ =
    contr-is-trivialᴳ (C (pos (S n)) (⊙Lift ⊙S⁰))
      {{connected-at-level-is-contr
        {{⟨⟩}}
        {{Trunc-preserves-conn $
           equiv-preserves-conn
            (pre⊙∘-equiv ⊙lower-equiv ∘e ⊙Bool→-equiv-idf _ ⁻¹)
            {{path-conn (connected-≤T (⟨⟩-monotone-≤ (≤-ap-S (O≤ n)))
                                     )}}}}}}
  EM-dimension {negsucc O} _ =
    contr-is-trivialᴳ (C (negsucc O) (⊙Lift ⊙S⁰))
      {{Trunc-preserves-level 0 (Σ-level (Π-level λ _ →
        inhab-prop-is-contr idp) ⟨⟩)}}

  EM-dimension {negsucc (S n)} _ =
    contr-is-trivialᴳ (C (negsucc (S n)) (⊙Lift ⊙S⁰))
      {{Trunc-preserves-level 0 (Σ-level (Π-level λ _ →
        =-preserves-level ⟨⟩) λ _ → =-preserves-level (=-preserves-level ⟨⟩))}}

  EM-Ordinary : OrdinaryTheory i
  EM-Ordinary = ordinary-theory EM-Cohomology EM-dimension

ext: agda


text:
------------------------------------------------------------------------
-- Laws related to _⊛_ and return
------------------------------------------------------------------------

module TotalParserCombinators.Laws.ApplicativeFunctor where

open import Algebra
open import Category.Monad
open import Codata.Musical.Notation
open import Data.List
import Data.List.Categorical
import Data.List.Relation.Binary.BagAndSetEquality as BSEq
open import Function
open import Level

open RawMonad {f = zero} Data.List.Categorical.monad
  using () renaming (_⊛_ to _⊛′_; _>>=_ to _>>=′_)
private
  module BagMonoid {k} {A : Set} =
    CommutativeMonoid (BSEq.commutativeMonoid k A)

open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Congruence
  hiding (return; fail) renaming (_∣_ to _∣′_)
import TotalParserCombinators.Laws.AdditiveMonoid as AdditiveMonoid
open import TotalParserCombinators.Laws.Derivative as Derivative
import TotalParserCombinators.Laws.Monad as Monad
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- _⊛_, return, _∣_ and fail form an applicative functor "with a zero
-- and a plus"

-- Together with the additive monoid laws we get something which
-- resembles an idempotent semiring (if we restrict ourselves to
-- language equivalence).

-- First note that _⊛_ can be defined using _>>=_.

private

  -- A variant of "flip map".

  pam : ∀ {Tok R₁ R₂ xs} →
        Parser Tok R₁ xs → (f : R₁ → R₂) →
        Parser Tok R₂ (xs >>=′ [_] ∘ f)
  pam p f = p >>= (return ∘ f)

  infixl 10 _⊛″_

  -- Note that this definition forces the argument parsers.

  _⊛″_ : ∀ {Tok R₁ R₂ fs xs} →
         ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)               →
         ∞⟨ fs ⟩Parser Tok  R₁                     (flatten xs) →
                Parser Tok       R₂  (flatten fs ⊛′ flatten xs)
  p₁ ⊛″ p₂ = ♭? p₁ >>= pam (♭? p₂)

⊛-in-terms-of->>= :
  ∀ {Tok R₁ R₂ fs xs}
  (p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)            )
  (p₂ : ∞⟨ fs ⟩Parser Tok  R₁                   (flatten xs)) →
  p₁ ⊛ p₂ ≅P p₁ ⊛″ p₂
⊛-in-terms-of->>= {R₁ = R₁} {R₂} {fs} {xs} p₁ p₂ =
  BagMonoid.reflexive (Claims.⊛flatten-⊛-flatten (flatten fs) xs) ∷ λ t → ♯ (
    D t (p₁ ⊛ p₂)                                         ≅⟨ D-⊛ p₁ p₂ ⟩

    D t (♭? p₁) ⊛ ♭? p₂ ∣
    return⋆ (flatten fs) ⊛ D t (♭? p₂)                    ≅⟨ ⊛-in-terms-of->>= (D t (♭? p₁)) (♭? p₂) ∣′
                                                             ⊛-in-terms-of->>= (return⋆ (flatten fs)) (D t (♭? p₂)) ⟩
    D t (♭? p₁) ⊛″ ♭? p₂ ∣
    return⋆ (flatten fs) ⊛″ D t (♭? p₂)                   ≅⟨ (D t (♭? p₁) ⊛″ ♭? p₂ ∎) ∣′
                                                             ([ ○ - ○ - ○ - ○ ] return⋆ (flatten fs) ∎ >>= λ f →
                                                                                sym $ lemma t f) ⟩
    D t (♭? p₁) >>= pam (♭? p₂) ∣
    return⋆ (flatten fs) >>= (λ f → D t (pam (♭? p₂) f))  ≅⟨ sym $ D->>= (♭? p₁) (pam (♭? p₂)) ⟩

    D t (♭? p₁ >>= pam (♭? p₂))                           ∎)
  where
  lemma : ∀ t (f : R₁ → R₂) →
          D t (♭? p₂ >>= λ x → return (f x)) ≅P
          D t (♭? p₂) >>= λ x → return (f x)
  lemma t f =
    D t (pam (♭? p₂) f)                    ≅⟨ D->>= (♭? p₂) (return ∘ f) ⟩

    pam (D t (♭? p₂)) f ∣
    (return⋆ (flatten xs) >>= λ _ → fail)  ≅⟨ (pam (D t (♭? p₂)) f ∎) ∣′
                                              Monad.right-zero (return⋆ (flatten xs)) ⟩
    pam (D t (♭? p₂)) f ∣ fail             ≅⟨ AdditiveMonoid.right-identity (pam (D t (♭? p₂)) f) ⟩
    pam (D t (♭? p₂)) f                    ∎

-- We can then reduce all the laws to corresponding laws for _>>=_.

-- The zero laws have already been proved.

open Derivative public
  using () renaming (left-zero-⊛  to left-zero;
                     right-zero-⊛ to right-zero)

-- _⊛_ distributes from the left over _∣_.

left-distributive : ∀ {Tok R₁ R₂ fs xs₁ xs₂}
                    (p₁ : Parser Tok (R₁ → R₂) fs)
                    (p₂ : Parser Tok R₁ xs₁)
                    (p₃ : Parser Tok R₁ xs₂) →
                    p₁ ⊛ (p₂ ∣ p₃) ≅P p₁ ⊛ p₂ ∣ p₁ ⊛ p₃
left-distributive p₁ p₂ p₃ =
  p₁ ⊛  (p₂ ∣ p₃)                     ≅⟨ ⊛-in-terms-of->>= p₁ (p₂ ∣ p₃) ⟩
  p₁ ⊛″ (p₂ ∣ p₃)                     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
                                            Monad.right-distributive p₂ p₃ (return ∘ f)) ⟩
  (p₁ >>= λ f → pam p₂ f ∣ pam p₃ f)  ≅⟨ Monad.left-distributive p₁ (pam p₂) (pam p₃) ⟩
  p₁ ⊛″ p₂ ∣ p₁ ⊛″ p₃                 ≅⟨ sym $ ⊛-in-terms-of->>= p₁ p₂ ∣′
                                               ⊛-in-terms-of->>= p₁ p₃ ⟩
  p₁ ⊛  p₂ ∣ p₁ ⊛  p₃                 ∎

-- _⊛_ distributes from the right over _∣_.

right-distributive : ∀ {Tok R₁ R₂ fs₁ fs₂ xs}
                     (p₁ : Parser Tok (R₁ → R₂) fs₁)
                     (p₂ : Parser Tok (R₁ → R₂) fs₂)
                     (p₃ : Parser Tok R₁ xs) →
                     (p₁ ∣ p₂) ⊛ p₃ ≅P p₁ ⊛ p₃ ∣ p₂ ⊛ p₃
right-distributive p₁ p₂ p₃ =
  (p₁ ∣ p₂) ⊛  p₃      ≅⟨ ⊛-in-terms-of->>= (p₁ ∣ p₂) p₃ ⟩
  (p₁ ∣ p₂) ⊛″ p₃      ≅⟨ Monad.right-distributive p₁ p₂ (pam p₃) ⟩
  p₁ ⊛″ p₃ ∣ p₂ ⊛″ p₃  ≅⟨ sym $ ⊛-in-terms-of->>= p₁ p₃ ∣′
                                ⊛-in-terms-of->>= p₂ p₃ ⟩
  p₁ ⊛  p₃ ∣ p₂ ⊛  p₃  ∎

-- Applicative functor laws.

identity : ∀ {Tok R xs} (p : Parser Tok R xs) → return id ⊛ p ≅P p
identity p =
  return id ⊛  p  ≅⟨ ⊛-in-terms-of->>= (return id) p ⟩
  return id ⊛″ p  ≅⟨ Monad.left-identity id (pam p) ⟩
  p >>= return    ≅⟨ Monad.right-identity p ⟩
  p               ∎

homomorphism : ∀ {Tok R₁ R₂} (f : R₁ → R₂) (x : R₁) →
               return f ⊛ return x ≅P return {Tok = Tok} (f x)
homomorphism f x =
  return f ⊛  return x  ≅⟨ ⊛-in-terms-of->>= (return f) (return x) ⟩
  return f ⊛″ return x  ≅⟨ Monad.left-identity f (pam (return x)) ⟩
  pam (return x) f      ≅⟨ Monad.left-identity x (return ∘ f) ⟩
  return (f x)          ∎

private

  infixl 10 _⊛-cong_

  _⊛-cong_ :
    ∀ {k Tok R₁ R₂ xs₁ xs₂ fs₁ fs₂}
      {p₁ : Parser Tok (R₁ → R₂) fs₁} {p₂ : Parser Tok R₁ xs₁}
      {p₃ : Parser Tok (R₁ → R₂) fs₂} {p₄ : Parser Tok R₁ xs₂} →
    p₁ ∼[ k ]P p₃ → p₂ ∼[ k ]P p₄ → p₁ ⊛″ p₂ ∼[ k ]P p₃ ⊛″ p₄
  _⊛-cong_ {p₁ = p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄ =
    p₁ ⊛″ p₂  ≅⟨ sym $ ⊛-in-terms-of->>= p₁ p₂ ⟩
    p₁ ⊛  p₂  ∼⟨ [ ○ - ○ - ○ - ○ ] p₁≈p₃ ⊛ p₂≈p₄ ⟩
    p₃ ⊛  p₄  ≅⟨ ⊛-in-terms-of->>= p₃ p₄ ⟩
    p₃ ⊛″ p₄  ∎

  pam-lemma : ∀ {Tok R₁ R₂ R₃ xs} {g : R₂ → List R₃}
              (p₁ : Parser Tok R₁ xs) (f : R₁ → R₂)
              (p₂ : (x : R₂) → Parser Tok R₃ (g x)) →
              pam p₁ f >>= p₂ ≅P p₁ >>= λ x → p₂ (f x)
  pam-lemma p₁ f p₂ =
    pam p₁ f >>= p₂                     ≅⟨ sym $ Monad.associative p₁ (return ∘ f) p₂ ⟩
    (p₁ >>= λ x → return (f x) >>= p₂)  ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ x →
                                              Monad.left-identity (f x) p₂) ⟩
    (p₁ >>= λ x → p₂ (f x))             ∎

composition :
  ∀ {Tok R₁ R₂ R₃ fs gs xs}
  (p₁ : Parser Tok (R₂ → R₃) fs)
  (p₂ : Parser Tok (R₁ → R₂) gs)
  (p₃ : Parser Tok R₁        xs) →
  return _∘′_ ⊛ p₁ ⊛ p₂ ⊛ p₃ ≅P p₁ ⊛ (p₂ ⊛ p₃)
composition p₁ p₂ p₃ =
  return _∘′_ ⊛  p₁ ⊛  p₂ ⊛  p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁ ⊛ p₂) p₃ ⟩
  return _∘′_ ⊛  p₁ ⊛  p₂ ⊛″ p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁) p₂ ⊛-cong (p₃ ∎) ⟩
  return _∘′_ ⊛  p₁ ⊛″ p₂ ⊛″ p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_) p₁ ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
  return _∘′_ ⊛″ p₁ ⊛″ p₂ ⊛″ p₃                   ≅⟨ Monad.left-identity _∘′_ (pam p₁) ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
  pam p₁ _∘′_ ⊛″ p₂ ⊛″ p₃                         ≅⟨ pam-lemma p₁ _∘′_ (pam p₂) ⊛-cong (p₃ ∎) ⟩
  ((p₁ >>= λ f → pam p₂ (_∘′_ f)) ⊛″ p₃)          ≅⟨ sym $ Monad.associative p₁ (λ f → pam p₂ (_∘′_ f)) (pam p₃) ⟩
  (p₁ >>= λ f → pam p₂ (_∘′_ f) >>= pam p₃)       ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
                                                      pam-lemma p₂ (_∘′_ f) (pam p₃)) ⟩
  (p₁ >>= λ f → p₂ >>= λ g → pam p₃ (f ∘′ g))     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
                                                      [ ○ - ○ - ○ - ○ ] p₂ ∎ >>= λ g →
                                                      sym $ pam-lemma p₃ g (return ∘ f)) ⟩
  (p₁ >>= λ f → p₂ >>= λ g → pam (pam p₃ g) f)    ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
                                                      Monad.associative p₂ (pam p₃) (return ∘ f)) ⟩
  p₁ ⊛″ (p₂ ⊛″ p₃)                                ≅⟨ sym $ (p₁ ∎) ⊛-cong ⊛-in-terms-of->>= p₂ p₃ ⟩
  p₁ ⊛″ (p₂ ⊛  p₃)                                ≅⟨ sym $ ⊛-in-terms-of->>= p₁ (p₂ ⊛ p₃) ⟩
  p₁ ⊛  (p₂ ⊛  p₃)                                ∎

interchange : ∀ {Tok R₁ R₂ fs}
              (p : Parser Tok (R₁ → R₂) fs) (x : R₁) →
              p ⊛ return x ≅P return (λ f → f x) ⊛ p
interchange p x =
  p ⊛  return x               ≅⟨ ⊛-in-terms-of->>= p (return x) ⟩
  p ⊛″ return x               ≅⟨ ([ ○ - ○ - ○ - ○ ] p ∎ >>= λ f →
                                    Monad.left-identity x (return ∘ f)) ⟩
  (p >>= λ f → return (f x))  ≅⟨ pam p (λ f → f x) ∎ ⟩
  pam p (λ f → f x)           ≅⟨ sym $ Monad.left-identity (λ f → f x) (pam p) ⟩
  return (λ f → f x) ⊛″ p     ≅⟨ sym $ ⊛-in-terms-of->>= (return (λ f → f x)) p ⟩
  return (λ f → f x) ⊛  p     ∎

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --no-termination-check #-}
module RunTests where

open import Prelude.Bool
open import Prelude.Char
open import Prelude.Nat
open import Prelude.List
open import Prelude.IO
open import Prelude.String
open import Prelude.Unit
open import Prelude.Product

postulate
  Stream : Set
  popen  : String -> String -> IO Stream
  pclose : Stream -> IO Unit
  readChar : Stream -> IO Char
  strLen : String -> Nat
  charAt : (s : String) -> Nat -> Char

_`_`_ : {A B C : Set}(x : A)(f : A -> B -> C)(y : B) -> C
x ` f ` y = f x y

infixr 9 _∘_

_∘_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
      (f : {a : A}(b : B a)-> C a b)
      (g : (a : A) -> B a)(x : A) -> C x (g x)
f ∘ g = λ x -> f (g x)

infixr 1 _$_

_$_ : {A : Set}{B : A -> Set}(f : (x : A) -> B x)(x : A) -> B x
f $ x = f x

{-# COMPILED_EPIC popen (s : String, m : String, u : Unit) -> Ptr = foreign Ptr "popen" (mkString(s) : String, mkString(m) : String) #-}
{-# COMPILED_EPIC pclose (s : Ptr, u : Unit) -> Unit = foreign Int "pclose" (s : Ptr) ; u #-}
{-# COMPILED_EPIC readChar (s : Ptr, u : Unit) -> Int = foreign Int "fgetc" (s : Ptr) #-}
{-# COMPILED_EPIC strLen (s : Any) -> BigInt = foreign BigInt "intToBig" (foreign Int "strlen" (mkString(s) : String) : Int) #-}
{-# COMPILED_EPIC charAt (s : Any, n : BigInt) -> Int = foreign Int "charAtBig" (mkString(s) : String, n : BigInt) #-}

readStream : Stream -> IO (List Char)
readStream stream =
    c <- readChar stream ,
    if' charEq eof c
        then pclose stream ,, return []
        else ( cs <- readStream stream
             , return (c :: cs))

system : String -> IO (List Char)
system s =
    putStrLn $ "system " +S+ s ,,
    x <- popen s "r" ,
    y <- readStream x ,
    return y

span : {A : Set} -> (p : A -> Bool) -> List A -> List A × List A
span p [] = [] , []
span p (a :: as) with p a
... | false = [] , a :: as
... | true with span p as
...        | xs , ys = (a :: xs) , ys

groupBy : {A : Set} -> (A -> A -> Bool) -> List A -> List (List A)
groupBy _  []           = []
groupBy eq (x :: xs) with span (eq x) xs
... | ys , zs = (x :: ys) :: groupBy eq zs

comparing : {A B : Set} -> (A -> B) -> (B -> B -> Bool) -> A -> A -> Bool
comparing f _==_ x y = f x == f y

FilePath : Set
FilePath = String

and : List Bool -> Bool
and [] = true
and (true :: xs) = and xs
and (false :: _) = false

sequence : {A : Set} -> List (IO A) -> IO (List A)
sequence [] = return []
sequence (x :: xs) =
    r <- x ,
    rs <- sequence xs ,
    return (r :: rs)

mapM : {A B : Set} -> (A -> IO B) -> List A -> IO (List B)
mapM f xs = sequence (map f xs)

printList : List Char -> IO Unit
printList xs =
  mapM printChar xs ,,
  printChar '\n'

printResult : FilePath -> List Char -> List Char -> IO Unit
printResult filename l1 l2 with l1 ` listEq charEq ` l2
... | true  = putStrLn (filename +S+ ": Success!")
... | false = putStrLn (filename +S+ ": Fail!") ,,
              putStrLn "Expected:" ,,
              printList l2       ,,
              putStrLn "Got:"      ,,
              printList l1

compile : FilePath -> FilePath -> IO Unit
compile dir file =
    system $ "agda --epic --compile-dir=" +S+ dir +S+ "bin/ " +S+ dir +S+ file ,,
    return unit

readFile : FilePath -> IO (List Char)
readFile file = system $ "cat " +S+ file

-- This won't work because of a bug in Epic...

{-
validFile : List Char -> Bool
validFile f with span (not ∘ charEq '.') f
... | _ , ('.' :: 'a' :: 'g' :: 'd' :: 'a' :: []) = true
... | _ , ('.' :: 'o' :: 'u' :: 't' :: [])        = true
... | _                                           = false
-}

stripFileEnding : FilePath -> FilePath
stripFileEnding fp = fromList $ fst $ span (not ∘ charEq '.') (fromString fp)

testFile : FilePath -> FilePath -> FilePath -> IO Bool
testFile outdir agdafile outfile =
    compile outdir (agdafile)           ,,
    out      <- system $ outdir +S+ "bin/" +S+ stripFileEnding agdafile ,
    expected <- readFile (outdir +S+ outfile)    ,
    printResult agdafile out expected ,,
    return (out ` listEq charEq ` expected)

testFile' : FilePath -> List (List Char) -> IO Bool
testFile' outdir (agdafile :: outfile :: _) = testFile outdir (fromList agdafile) (fromList outfile)
testFile' _      _                          = return true

isNewline : Char -> Bool
isNewline '\n' = true
isNewline _    = false

lines : List Char -> List (List Char)
lines list with span (not ∘ isNewline) list
... | l , [] = l :: []
... | l , _ :: s' = l :: lines s'

getFiles : FilePath -> IO (List (List Char))
getFiles dir =
    out <- system $ "ls " +S+ dir ,
    putStrLn "getFiles after ls" ,,
   -- mapM (printList ∘ snd) $ map (span (not ∘ charEq '.')) $ lines out ,,
    return $ lines out -- filter validFile $ lines out

isDot : Char -> Bool
isDot '.' = true
isDot _   = false

testFiles : FilePath -> IO Bool
testFiles dir =
    files <- getFiles dir ,
    putStrLn "Found the following files in the tests directory:" ,,
    mapM printList files   ,,
    res   <- mapM (testFile' dir) (groupBy (comparing (fst ∘ span (not ∘ isDot)) (listEq charEq)) files) ,
    return $ and res

getCurrentDirectory : IO FilePath
getCurrentDirectory =
   fromList <$> system "pwd"

main : IO Unit
main =
    dir' <- getCurrentDirectory ,
    putStrLn (fromList (fromString dir')) ,,
    putStrLn "hello" ,,
    putStrLn (fromList (tail ('h' :: 'e' :: 'j' :: []))) ,,
    printList (fromString "hej igen") ,,
    putStrLn (fromList (tail (fromString "hello"))) ,,
    dir <- fromList ∘ init ∘ fromString <$> getCurrentDirectory ,
    putStrLn dir ,,
    system ("rm " +S+ dir +S+ "/tests/*.agdai") ,,
    res <- testFiles (dir +S+ "/tests/") ,
    (if res
      then putStrLn "All tests succeeded! "
      else putStrLn "Not all tests succeeded ")

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
-- ----------------------------------------------------------------------
-- The Agda σ-library
--
-- Renamings
-- ----------------------------------------------------------------------

-- A renaming is defined as a substitution ρ, mapping
-- indices to indices (w/ explicit bounds). It is a subclass
-- of substitutions.
--
-- The σ-library provides renamings as primitives.

module Sigma.Renaming.Base where

open import Data.Nat using (ℕ; suc; zero; _+_)
open import Data.Fin using (Fin; zero; suc)

open import Function as Fun using (_∘_)

open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)

open import Sigma.Subst.Base using (Sub; _∷_; []; _++_)

-- ------------------------------------------------------------------------

-- A renaming ρ : 𝕀ⁿ → 𝕀ᵐ is denoted { i ↦ j : i ∈ 𝕀ⁿ, j ∈ 𝕀ᵐ }
Ren : ℕ → ℕ → Set
Ren m n = Sub (Fin n) m

space : ∀ { m n } → Ren m n → ℕ × ℕ
space { m } { n } _ = ⟨ m , n ⟩

dom : ∀ { m n } → Ren m n → ℕ
dom = proj₁ ∘ space

rng : ∀ { m n } → Ren m n → ℕ
rng = proj₂ ∘ space

-- Identity renaming idₙ : 𝕀ⁿ → 𝕀ⁿ.
-- Defined by idₙ = { i ↦ i : i ∈ 𝕀ⁿ }.
id : ∀ { n } → Ren n n
id = Fun.id

-- Shift operator ↑ₙ : 𝕀ⁿ → 𝕀ⁿ⁺¹
-- Defined by ↑ₙ i = 1 + i
↑ : ∀ { n } → Ren n (1 + n)
↑ = suc

infix 10 _⇑

-- Lift operator ρ ⇑
-- Defined by ρ ⇑ = { 0 ↦ 0 } ∪ { ↑ i ↦ ↑ j : i ∈ 𝕀ⁿ, j ∈ 𝕀ᵐ }
-- This operator is used for defining a capture avoiding renaming.
--
-- For example in λ. e, free variables of e are now shifted:
--  e   :     0   1   2
--  λ e : 0   1   2   3
-- since λ binds 0.
_⇑ : ∀ { m n } → Ren m n → Ren (1 + m) (1 + n)
ρ ⇑ = zero ∷ ↑ ∘ ρ

-- ------------------------------------------------------------------------

-- Generalizing the above primitives to "multi-variable binders"
-- allows for formalization of binders that bind multiple variables,
-- such as patterns. So-called multi-variate binders.

-- Multi-variate identity idₙᵐ : 𝕀ᵐ → 𝕀ᵐ⁺ⁿ
-- Defined by idₙᵐ = { i ↦ i' : i ∈ 𝕀ᵐ, i' ∈ 𝕀ᵐ⁺ⁿ, i = i' }.
--
-- For example:
-- id✶ 1 = 0 ∷ []ₙ
-- id✶ 2 = 0 ∷ ↑ ∘ (0 ∷ []) = 0 ∷ 1 ∷ []ₙ
-- id✶ 3 = 0 ∷ ↑ ∘ id✶ 2 = 0 ∷ 1 ∷ 2 ∷ []ₙ
id✶ : ∀ { n } m → Ren m (m + n)
id✶ zero = []
id✶ (suc m) = zero ∷ ↑ ∘ id✶ m

-- Multi-variate shift operator ↑ₙᵐ : 𝕀ⁿ → 𝕀ᵐ⁺ⁿ
-- Defined by ↑ₙᵐ = { i ↦ m + i : i ∈ 𝕀ⁿ }
↑✶_ : ∀ { n } k → Ren n (k + n)
↑✶ zero = id
↑✶ suc k = ↑ ∘ ↑✶ k

-- Multi-variate lift operator ρ ⇑ᵏ
-- Defined by ρ ⇑ᵏ = { i ↦ i' } ∪ { ↑ᵏ i ↦ ↑ᵏ j : i ∈ 𝕀ⁿ, j ∈ 𝕀ᵐ }
-- This operator is used for defining a multi-variate capture avoiding renaming.
--
-- For example in λ. e, free variables of e are now shifted by k:
--  e   :         0   1       2       3
--  λ e : 0   ... k   k + 1   k + 2   k + 3
-- since λ binds 0, ..., k - 1.
_⇑✶_ :  ∀ { m n } → Ren m n → ∀ k → Ren (k + m) (k + n)
ρ ⇑✶ k = id✶ k ++ (↑✶ k ∘ ρ)

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


text:
------------------------------------------------------------------------
-- Isomorphism of monoids on sets coincides with equality (assuming
-- univalence)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- This module has been developed in collaboration with Thierry
-- Coquand.

open import Equality

module Univalence-axiom.Isomorphism-is-equality.Monoid
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq using (_↔_; Σ-≡,≡↔≡; ↑↔)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq hiding (id)
open import H-level eq
open import H-level.Closure eq
open import Prelude hiding (id)
open import Univalence-axiom eq

-- Monoid laws (including the assumption that the carrier type is a
-- set).

Is-monoid : (C : Type) → (C → C → C) → C → Type
Is-monoid C _∙_ id =

  -- C is a set.
  Is-set C ×

  -- Left and right identity laws.
  (∀ x → (id ∙ x) ≡ x) ×
  (∀ x → (x ∙ id) ≡ x) ×

  -- Associativity.
  (∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z))

-- Monoids (on sets).

Monoid : Type₁
Monoid =
  -- Carrier.
  Σ Type λ C →

  -- Binary operation.
  Σ (C → C → C) λ _∙_ →

  -- Identity.
  Σ C λ id →

  -- Laws.
  Is-monoid C _∙_ id

-- The carrier type.

Carrier : Monoid → Type
Carrier M = proj₁ M

-- The binary operation.

op : (M : Monoid) → Carrier M → Carrier M → Carrier M
op M = proj₁ (proj₂ M)

-- The identity element.

id : (M : Monoid) → Carrier M
id M = proj₁ (proj₂ (proj₂ M))

-- The monoid laws.

laws : (M : Monoid) → Is-monoid (Carrier M) (op M) (id M)
laws M = proj₂ (proj₂ (proj₂ M))

-- Monoid morphisms.

Is-homomorphism :
  (M₁ M₂ : Monoid) → (Carrier M₁ → Carrier M₂) → Type
Is-homomorphism M₁ M₂ f =
  (∀ x y → f (op M₁ x y) ≡ op M₂ (f x) (f y)) ×
  (f (id M₁) ≡ id M₂)

-- Monoid isomorphisms.

_≅_ : Monoid → Monoid → Type
M₁ ≅ M₂ =
  Σ (Carrier M₁ ↔ Carrier M₂) λ f →
  Is-homomorphism M₁ M₂ (_↔_.to f)

-- The monoid laws are propositional (assuming extensionality).

laws-propositional :
  Extensionality (# 0) (# 0) →
  (M : Monoid) →
  Is-proposition (Is-monoid (Carrier M) (op M) (id M))
laws-propositional ext M =
  ×-closure 1 (H-level-propositional ext 2)
  (×-closure 1 (Π-closure ext 1 λ _ →
                is-set)
  (×-closure 1 (Π-closure ext 1 λ _ →
                is-set)
               (Π-closure ext 1 λ _ →
                Π-closure ext 1 λ _ →
                Π-closure ext 1 λ _ →
                is-set)))
  where is-set = proj₁ (laws M)

-- Monoid equality is isomorphic to equality of the carrier sets,
-- binary operations and identity elements, suitably transported
-- (assuming extensionality).

equality-triple-lemma :
  Extensionality (# 0) (# 0) →
  (M₁ M₂ : Monoid) →
  M₁ ≡ M₂ ↔
  Σ (Carrier M₁ ≡ Carrier M₂) λ C-eq →
    subst (λ C → C → C → C) C-eq (op M₁) ≡ op M₂ ×
    subst (λ C → C) C-eq (id M₁) ≡ id M₂
equality-triple-lemma
  ext (C₁ , op₁ , id₁ , laws₁) (C₂ , op₂ , id₂ , laws₂) =

  ((C₁ , op₁ , id₁ , laws₁) ≡ (C₂ , op₂ , id₂ , laws₂))               ↔⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ bij ⟩

  (((C₁ , op₁ , id₁) , laws₁) ≡ ((C₂ , op₂ , id₂) , laws₂))           ↝⟨ inverse $ ignore-propositional-component $
                                                                           laws-propositional ext (C₂ , op₂ , id₂ , laws₂) ⟩

  ((C₁ , op₁ , id₁) ≡ (C₂ , op₂ , id₂))                               ↝⟨ inverse Σ-≡,≡↔≡ ⟩

  (Σ (C₁ ≡ C₂) λ C-eq →
     subst (λ C → (C → C → C) × C) C-eq (op₁ , id₁) ≡ (op₂ , id₂))    ↝⟨ ∃-cong (λ _ → ≡⇒↝ _ $ cong (λ x → x ≡ _) $
                                                                             push-subst-, (λ C → C → C → C) (λ C → C)) ⟩
  (Σ (C₁ ≡ C₂) λ C-eq →
     (subst (λ C → C → C → C) C-eq op₁ , subst (λ C → C) C-eq id₁) ≡
     (op₂ , id₂))                                                     ↝⟨ ∃-cong (λ _ → inverse ≡×≡↔≡) ⟩□

  (Σ (C₁ ≡ C₂) λ C-eq →
     subst (λ C → C → C → C) C-eq op₁ ≡ op₂ ×
     subst (λ C → C) C-eq id₁ ≡ id₂)                                  □

  where
  bij =

    (Σ Type λ C → Σ (C → C → C) λ op → Σ C λ id → Is-monoid C op id)  ↝⟨ ∃-cong (λ _ → Σ-assoc) ⟩

    (Σ Type λ C → Σ ((C → C → C) × C) λ { (op , id) →
     Is-monoid C op id })                                             ↝⟨ Σ-assoc ⟩□

    (Σ (Σ Type λ C → (C → C → C) × C) λ { (C , op , id) →
     Is-monoid C op id })                                             □

-- If two monoids are isomorphic, then they are equal (assuming
-- univalence).

isomorphic-equal :
  Univalence (# 0) →
  Univalence (# 1) →
  (M₁ M₂ : Monoid) → M₁ ≅ M₂ → M₁ ≡ M₂
isomorphic-equal univ univ₁ M₁ M₂ (bij , bij-op , bij-id) = goal
  where
  open _≃_

  -- Our goal:

  goal : M₁ ≡ M₂

  -- Extensionality follows from univalence.

  ext : Extensionality (# 0) (# 0)
  ext = dependent-extensionality univ₁ univ

  -- Hence the goal follows from monoids-equal-if, if we can prove
  -- three equalities.

  C-eq  : Carrier M₁ ≡ Carrier M₂
  op-eq : subst (λ A → A → A → A) C-eq (op M₁) ≡ op M₂
  id-eq : subst (λ A → A) C-eq (id M₁) ≡ id M₂

  goal = _↔_.from (equality-triple-lemma ext M₁ M₂)
                  (C-eq , op-eq , id-eq)

  -- Our bijection can be converted into an equivalence.

  equiv : Carrier M₁ ≃ Carrier M₂
  equiv = Eq.↔⇒≃ bij

  -- Hence the first equality follows directly from univalence.

  C-eq = ≃⇒≡ univ equiv

  -- For the second equality, let us first define a "cast" operator.

  cast₂ : {A B : Type} → A ≃ B → (A → A → A) → (B → B → B)
  cast₂ eq f = λ x y → to eq (f (from eq x) (from eq y))

  -- The transport theorem implies that cast₂ equiv can be expressed
  -- using subst.

  cast₂-equiv-is-subst :
    ∀ f → cast₂ equiv f ≡ subst (λ A → A → A → A) C-eq f
  cast₂-equiv-is-subst f =
    transport-theorem (λ A → A → A → A) cast₂ refl univ equiv f

  -- The second equality op-eq follows from extensionality,
  -- cast₂-equiv-is-subst, and the fact that the bijection is a
  -- monoid homomorphism.

  op-eq = apply-ext ext λ x → apply-ext ext λ y →
    subst (λ A → A → A → A) C-eq (op M₁) x y                   ≡⟨ cong (λ f → f x y) $ sym $ cast₂-equiv-is-subst (op M₁) ⟩
    to equiv (op M₁ (from equiv x) (from equiv y))             ≡⟨ bij-op (from equiv x) (from equiv y) ⟩
    op M₂ (to equiv (from equiv x)) (to equiv (from equiv y))  ≡⟨ cong₂ (op M₂) (right-inverse-of equiv x) (right-inverse-of equiv y) ⟩∎
    op M₂ x y                                                  ∎

  -- The development above can be repeated for the identity
  -- elements.

  cast₀ : {A B : Type} → A ≃ B → A → B
  cast₀ eq x = to eq x

  cast₀-equiv-is-subst : ∀ x → cast₀ equiv x ≡ subst (λ A → A) C-eq x
  cast₀-equiv-is-subst x =
    transport-theorem (λ A → A) cast₀ refl univ equiv x

  id-eq =
    subst (λ A → A) C-eq (id M₁)  ≡⟨ sym $ cast₀-equiv-is-subst (id M₁) ⟩
    to equiv (id M₁)              ≡⟨ bij-id ⟩∎
    id M₂                         ∎

-- Equality of monoids is in fact in bijective correspondence with
-- isomorphism of monoids (assuming univalence).

isomorphism-is-equality :
  Univalence (# 0) →
  Univalence (# 1) →
  (M₁ M₂ : Monoid) → (M₁ ≅ M₂) ↔ (M₁ ≡ M₂)
isomorphism-is-equality univ univ₁
  (C₁ , op₁ , id₁ , laws₁) (C₂ , op₂ , id₂ , laws₂) =

  (Σ (C₁ ↔ C₂) λ f → Is-homomorphism M₁ M₂ (_↔_.to f))          ↝⟨ Σ-cong (Eq.↔↔≃ ext C₁-set) (λ _ → _ □) ⟩

  (Σ (C₁ ≃ C₂) λ C-eq → Is-homomorphism M₁ M₂ (_≃_.to C-eq))    ↝⟨ ∃-cong (λ C-eq → op-lemma C-eq ×-cong id-lemma C-eq) ⟩

  (Σ (C₁ ≃ C₂) λ C-eq →
     subst (λ C → C → C → C) (≃⇒≡ univ C-eq) op₁ ≡ op₂ ×
     subst (λ C → C) (≃⇒≡ univ C-eq) id₁ ≡ id₂)                 ↝⟨ inverse $ Σ-cong (≡≃≃ univ) (λ C-eq → ≡⇒↝ _ $
                                                                     cong (λ eq → subst (λ C → C → C → C) eq op₁ ≡ op₂ ×
                                                                                subst (λ C → C) eq id₁ ≡ id₂) $ sym $
                                                                       _≃_.left-inverse-of (≡≃≃ univ) C-eq) ⟩
  (Σ (C₁ ≡ C₂) λ C-eq →
     subst (λ C → C → C → C) C-eq op₁ ≡ op₂ ×
     subst (λ C → C) C-eq id₁ ≡ id₂)                            ↝⟨ inverse $ equality-triple-lemma ext M₁ M₂ ⟩

  ((C₁ , op₁ , id₁ , laws₁) ≡ (C₂ , op₂ , id₂ , laws₂))         □

  where

  -- The two monoids.

  M₁ = (C₁ , op₁ , id₁ , laws₁)
  M₂ = (C₂ , op₂ , id₂ , laws₂)

  -- Extensionality follows from univalence.

  ext : Extensionality (# 0) (# 0)
  ext = dependent-extensionality univ₁ univ

  -- C₁ is a set.

  C₁-set : Is-set C₁
  C₁-set = proj₁ laws₁

  module _ (C-eq : C₁ ≃ C₂) where

    open _≃_ C-eq

    -- Two component lemmas.

    op-lemma :
      (∀ x y → to (op₁ x y) ≡ op₂ (to x) (to y)) ↔
      subst (λ C → C → C → C) (≃⇒≡ univ C-eq) op₁ ≡ op₂
    op-lemma =
      (∀ x y → to (op₁ x y) ≡ op₂ (to x) (to y))                  ↔⟨ ∀-cong ext (λ _ → Eq.extensionality-isomorphism ext) ⟩

      (∀ x → (λ y → to (op₁ x y)) ≡ (λ y → op₂ (to x) (to y)))    ↝⟨ ∀-cong ext (λ _ → inverse $ ∘from≡↔≡∘to ext C-eq) ⟩

      (∀ x → (λ y → to (op₁ x (from y))) ≡ (λ y → op₂ (to x) y))  ↔⟨ Eq.extensionality-isomorphism ext ⟩

      ((λ x y → to (op₁ x (from y))) ≡ (λ x y → op₂ (to x) y))    ↝⟨ inverse $ ∘from≡↔≡∘to ext C-eq ⟩

      ((λ x y → to (op₁ (from x) (from y))) ≡ (λ x y → op₂ x y))  ↝⟨ ≡⇒↝ _ $ cong (λ o → o ≡ op₂) $
                                                                       transport-theorem
                                                                         (λ C → C → C → C)
                                                                         (λ eq f x y → _≃_.to eq (f (_≃_.from eq x) (_≃_.from eq y)))
                                                                         refl univ C-eq op₁ ⟩
      (subst (λ C → C → C → C) (≃⇒≡ univ C-eq) op₁ ≡ op₂)         □

    id-lemma : (to id₁ ≡ id₂) ↔
               (subst (λ C → C) (≃⇒≡ univ C-eq) id₁ ≡ id₂)
    id-lemma =
      (to id₁ ≡ id₂)                               ↝⟨ ≡⇒↝ _ $ cong (λ i → i ≡ id₂) $
                                                        transport-theorem (λ C → C) _≃_.to refl univ C-eq id₁ ⟩□
      (subst (λ C → C) (≃⇒≡ univ C-eq) id₁ ≡ id₂)  □

-- Equality of monoids is thus equal to equality (assuming
-- univalence).

isomorphism-is-equal-to-equality :
  Univalence (# 0) →
  Univalence (# 1) →
  (M₁ M₂ : Monoid) → ↑ _ (M₁ ≅ M₂) ≡ (M₁ ≡ M₂)
isomorphism-is-equal-to-equality univ univ₁ M₁ M₂ =
  ≃⇒≡ univ₁ $ Eq.↔⇒≃ (
    ↑ _ (M₁ ≅ M₂)  ↝⟨ ↑↔ ⟩
    (M₁ ≅ M₂)      ↝⟨ isomorphism-is-equality univ univ₁ M₁ M₂ ⟩□
    (M₁ ≡ M₂)      □)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Haskell.Prim.Char where

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Char
open import Agda.Builtin.Bool
open import Agda.Builtin.Int using (pos; negsuc)

open import Haskell.Prim
open import Haskell.Prim.Int
open import Haskell.Prim.Integer
open import Haskell.Prim.Enum
open import Haskell.Prim.Real

ord : Char -> Int
ord c = fromEnum ((pos ∘ primCharToNat) c)

chr1 : Integer -> Char
chr1 (pos n) = primNatToChar n
chr1 _ = '_'

chr : Int -> Char
chr n = chr1 (toInteger n)


text:
module TestLib where

import Lib.Bool
import Lib.Eq
import Lib.Fin
import Lib.IO
import Lib.Id
import Lib.List
import Lib.Logic
import Lib.Maybe
import Lib.Monad
import Lib.Nat
import Lib.Prelude
import Lib.Vec

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module UniDB.Morph.Shift where

open import UniDB.Spec
open import UniDB.Morph.Depth
open import UniDB.Morph.Weaken

--------------------------------------------------------------------------------

data Shift : MOR where
  shift : {γ₁ γ₂ : Dom} (ξ : Depth Weaken γ₁ γ₂) → Shift γ₁ γ₂

instance
  iUpShift : Up Shift
  _↑₁ {{iUpShift}} (shift ζ) = shift (ζ ↑₁)
  _↑_ {{iUpShift}} ξ 0 = ξ
  _↑_ {{iUpShift}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpShift}} ξ = refl
  ↑-suc {{iUpShift}} ξ δ⁺ = refl

  iWkmShift : Wkm Shift
  wkm {{iWkmShift}} δ = shift (depth (weaken δ) 0)

  iIdmShift : Idm Shift
  idm {{iIdmShift}} _ = wkm {Shift} 0

module _ {T : STX} {{vrT : Vr T}} where

  instance
    iLkShift : Lk T Shift
    lk {{iLkShift}} (shift ζ) i = vr {T} (lk {Ix} {Depth Weaken} ζ i)

    iLkUpShift : {{wkT : Wk T}} {{wkVrT : WkVr T}} → LkUp T Shift
    lk-↑₁-zero {{iLkUpShift}} (shift ξ) = cong (vr {T}) (lk-↑₁-zero {Ix} {_} ξ )
    lk-↑₁-suc {{iLkUpShift}} (shift ξ) i = begin
      vr {T} (lk {Ix} (ξ ↑₁) (suc i)) ≡⟨ cong (vr {T}) (lk-↑₁-suc ξ i) ⟩
      vr {T} (wk₁ {Ix} (lk {Ix} ξ i)) ≡⟨ sym (wk₁-vr {T} (lk {Ix} ξ i)) ⟩
      wk₁ {T} (vr {T} (lk {Ix} ξ i))  ∎

    iLkWkmShift : LkWkm T Shift
    lk-wkm {{iLkWkmShift}} δ i = refl

    iLkIdmShift : LkIdm T Shift
    lk-idm {{iLkIdmShift}} i = refl

module _ {T : STX} {{vrT : Vr T}} where

  instance
    iLkRenShift : LkRen T Shift
    lk-ren {{iLkRenShift}} (shift ξ) i = refl

--------------------------------------------------------------------------------

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
------------------------------------------------------------------------------
-- Subtraction using the fixed-point operator
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.LTC-PCF.Data.Nat.SubtractionFixedPointOperator where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/Nat.agda).
infixl 9 _∸_

------------------------------------------------------------------------------
-- Subtraction's definition

∸-helper : D → D
∸-helper f = lam (λ m → lam (λ n →
               if (iszero₁ n)
                 then m
                 else if (iszero₁ m)
                        then zero
                        else f · pred₁ m · pred₁ n))

_∸_ : D → D → D
_∸_ m n = fix ∸-helper · m · n

------------------------------------------------------------------------------
-- Conversion rules from the Agda standard library 0.8.1 (see
-- Data/Nat.agda) without use induction.

private
  ----------------------------------------------------------------------------
  -- The steps

  -- See doc in LTC-PCF.Program.GCD.Total.Equations.

  -- Initially, the conversion rule fix-eq is applied.
  ∸-s₁ : D → D → D
  ∸-s₁ m n = ∸-helper (fix ∸-helper) · m · n

  -- First argument application.
  ∸-s₂ : D → D
  ∸-s₂ m = lam (λ n →
               if (iszero₁ n)
                 then m
                 else if (iszero₁ m)
                        then zero
                        else fix ∸-helper · pred₁ m · pred₁ n)

  -- Second argument application.
  ∸-s₃ : D → D → D
  ∸-s₃ m n = if (iszero₁ n)
               then m
               else if (iszero₁ m)
                      then zero
                      else fix ∸-helper · pred₁ m · pred₁ n

  -- First if_then_else_ iszero₁ n = b.
  ∸-s₄ : D → D → D → D
  ∸-s₄ m n b = if b
                 then m
                 else if (iszero₁ m)
                        then zero
                        else fix ∸-helper · pred₁ m · pred₁ n

  -- First if_then_else_ when if true ...
  ∸-s₅ : D → D
  ∸-s₅ m = m

  -- First if_then_else_ when if false ...
  ∸-s₆ : D → D → D
  ∸-s₆ m n = if (iszero₁ m)
               then zero
               else fix ∸-helper · pred₁ m · pred₁ n

  -- Second if_then_else_ iszero₁ m = b.
  ∸-s₇ : D → D → D → D
  ∸-s₇ m n b = if b then zero else fix ∸-helper · pred₁ m · pred₁ n

  -- Second if_then_else_ when if true ...
  ∸-s₈ : D
  ∸-s₈ = zero

  -- Second if_then_else_ when if false ...
  ∸-s₉ : D → D → D
  ∸-s₉ m n = fix ∸-helper · pred₁ m · pred₁ n

  ----------------------------------------------------------------------------
  -- Congruence properties

  ∸-s₄Cong₃ : ∀ {m n b₁ b₂} → b₁ ≡ b₂ → ∸-s₄ m n b₁ ≡ ∸-s₄ m n b₂
  ∸-s₄Cong₃ refl = refl

  ∸-s₇Cong₃ : ∀ {m n b₁ b₂} → b₁ ≡ b₂ → ∸-s₇ m n b₁ ≡ ∸-s₇ m n b₂
  ∸-s₇Cong₃ refl = refl

  ----------------------------------------------------------------------------
  -- The execution steps

  -- See doc in LTC-PCF.Program.GCD.Total.Equations.

  proof₀₋₁ : ∀ m n → fix ∸-helper · m · n ≡ ∸-s₁ m n
  proof₀₋₁ m n = subst (λ x → x · m · n ≡ ∸-helper (fix ∸-helper) · m · n)
                       (sym (fix-eq ∸-helper))
                       refl

  proof₁₋₂ : ∀ m n → ∸-s₁ m n ≡ ∸-s₂ m · n
  proof₁₋₂ m n = subst (λ x → x · n ≡ ∸-s₂ m · n)
                       (sym (beta ∸-s₂ m))
                       refl

  proof₂₋₃ : ∀ m n → ∸-s₂ m · n ≡ ∸-s₃ m n
  proof₂₋₃ m n = beta (∸-s₃ m) n

  proof₃₋₄ : ∀ m n b → iszero₁ n ≡ b → ∸-s₃ m n ≡ ∸-s₄ m n b
  proof₃₋₄ m n b = ∸-s₄Cong₃

  proof₄₊ : ∀ m n → ∸-s₄ m n true ≡ ∸-s₅ m
  proof₄₊ m _ = if-true (∸-s₅ m)

  proof₄₋₆ : ∀ m n → ∸-s₄ m n false ≡ ∸-s₆ m n
  proof₄₋₆ m n = if-false (∸-s₆ m n)

  proof₆₋₇ : ∀ m n b → iszero₁ m ≡ b → ∸-s₆ m n ≡ ∸-s₇ m n b
  proof₆₋₇ m n b = ∸-s₇Cong₃

  proof₇₊ : ∀ m n → ∸-s₇ m n true ≡ ∸-s₈
  proof₇₊ m n = if-true ∸-s₈

  proof₇₋₉ : ∀ m n → ∸-s₇ m n false ≡ ∸-s₉ m n
  proof₇₋₉ m n = if-false (∸-s₉ m n)

------------------------------------------------------------------------------
-- The equations for subtraction

∸-x0 : ∀ n → n ∸ zero ≡ n
∸-x0 n =
  n ∸ zero         ≡⟨ proof₀₋₁ n zero ⟩
  ∸-s₁ n zero      ≡⟨ proof₁₋₂ n zero ⟩
  ∸-s₂ n · zero    ≡⟨ proof₂₋₃ n zero ⟩
  ∸-s₃ n zero      ≡⟨ proof₃₋₄ n zero true iszero-0 ⟩
  ∸-s₄ n zero true ≡⟨ proof₄₊ n zero ⟩
  n                ∎

∸-0S : ∀ n → zero ∸ succ₁ n ≡ zero
∸-0S n =
  zero ∸ succ₁ n            ≡⟨ proof₀₋₁ zero (succ₁ n) ⟩
  ∸-s₁ zero (succ₁ n)       ≡⟨ proof₁₋₂ zero (succ₁ n) ⟩
  ∸-s₂ zero · (succ₁ n)     ≡⟨ proof₂₋₃ zero (succ₁ n) ⟩
  ∸-s₃ zero (succ₁ n)       ≡⟨ proof₃₋₄ zero (succ₁ n) false (iszero-S n) ⟩
  ∸-s₄ zero (succ₁ n) false ≡⟨ proof₄₋₆ zero (succ₁ n) ⟩
  ∸-s₆ zero (succ₁ n)       ≡⟨ proof₆₋₇ zero (succ₁ n) true iszero-0 ⟩
  ∸-s₇ zero (succ₁ n) true  ≡⟨ proof₇₊  zero (succ₁ n) ⟩
  zero                      ∎

∸-SS : ∀ m n → succ₁ m ∸ succ₁ n ≡ m ∸ n
∸-SS m n =
  succ₁ m ∸ succ₁ n
    ≡⟨ proof₀₋₁ (succ₁ m) (succ₁ n) ⟩
  ∸-s₁ (succ₁ m) (succ₁ n)
    ≡⟨ proof₁₋₂ (succ₁ m) (succ₁ n) ⟩
  ∸-s₂ (succ₁ m) · (succ₁ n)
    ≡⟨ proof₂₋₃ (succ₁ m) (succ₁ n) ⟩
  ∸-s₃ (succ₁ m) (succ₁ n)
    ≡⟨ proof₃₋₄ (succ₁ m) (succ₁ n) false (iszero-S n) ⟩
  ∸-s₄ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₄₋₆ (succ₁ m) (succ₁ n) ⟩
  ∸-s₆ (succ₁ m) (succ₁ n)
    ≡⟨ proof₆₋₇ (succ₁ m) (succ₁ n) false (iszero-S m) ⟩
  ∸-s₇ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₇₋₉ (succ₁ m) (succ₁ n) ⟩
  fix ∸-helper · pred₁ (succ₁ m) · pred₁ (succ₁ n)
    ≡⟨ ·-rightCong (pred-S n) ⟩
  fix ∸-helper · pred₁ (succ₁ m) · n
    ≡⟨ ·-leftCong (·-rightCong (pred-S m)) ⟩
  fix ∸-helper · m · n ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-#  OPTIONS --type-in-type #-}
module examplesPaperJFP.agdaCodeBrady where

open import Data.List
open import Agda.Builtin.Unit public renaming (⊤ to Unit; tt to triv)
open import Data.Product
open import examplesPaperJFP.StateDependentIO

{- Brady's Effect -}

Effect : Set₁
Effect = (Result : Set) → (InResource : Set) →  (OutResource : Result → Set) → Set

record MyEffect : Set₁ where
  field  Ops          :  Set
         Result       :  Ops → Set
         InResource   :  Ops → Set
         OutResource  :  (o : Ops) → Result o → Set

open MyEffect

effectToIOInterfaceˢ : Effect → IOInterfaceˢ
Stateˢ     (effectToIOInterfaceˢ  eff)     =  Set
Commandˢ   (effectToIOInterfaceˢ  eff)  s  =
                   Σ[ Result ∈ Set ] (Σ[ outR ∈ (Result → Set) ] (eff Result s outR))
Responseˢ  (effectToIOInterfaceˢ  eff)  s (result , outR , op)  =  result
nextˢ      (effectToIOInterfaceˢ  eff)  s (result , outR , op)  =  outR

const : { A B  : Set} → B → A → B
const b = λ _ → b

data EFFECT′ : Set₁  where
  MkEff : Set → Effect → EFFECT′

EFFECT : Set₁
EFFECT = Set × Effect

data State : Effect where
  Get : (a : Set) → State   a    a (λ _ →  a)
  Put : (a : Set) → (b : Set) → State a a (λ _ → b)

data myStateOps : Set₁ where
  get :  Set → myStateOps
  put : Set → Set → myStateOps

myState : MyEffect
Ops myState            = myStateOps
Result myState (get a) = a
InResource myState (get a) = a
OutResource myState (get a) _ = a
Result myState (put a b) = a
InResource myState (put a b) = a
OutResource myState (put a b) _ = b

STATE : Set → EFFECT
STATE x = ( x , State )

postulate String : Set

data Stdio : Effect where
  PutStr : String → Stdio Unit Unit (const Unit)
  GetStr : Stdio String  String (const String)

STDIO : EFFECT
STDIO = ( Unit , Stdio )

data Eff : (x : Set) → List EFFECT → (x → List EFFECT) → Set where
  get : (x : Set) → Eff x [ STATE x ] (const [ STATE x ])
  put : (x : Set) → x → Eff Unit [ STATE x ] (const [ STATE x  ])
  putM : (x : Set) → (y : Set) → y → Eff Unit [ STATE x ] (const  [ STATE y ])
  update : (x : Set) → (x → x) → Eff Unit [ STATE x ] (const [ STATE x ])

data EffM : (m : Set → Set) → (res : Set) →
            (inEffects : List EFFECT) →
            (outEffects : res → List EFFECT)
            → Set where
   _>>=_ : {m : Set → Set} → {res : Set} →
           {inEffects : List EFFECT} →
            {outEffects : res → List EFFECT} →
            {res′ : Set} →
            {inEffects′ : res → List EFFECT} →
            {outEffects′ : res′  → List EFFECT} →
            EffM m res inEffects outEffects →
            ((x : res) → EffM m res′ (inEffects′ x) outEffects′) →
            EffM m res′ inEffects outEffects′

record SetInterfaceˢ : Set where
  field  Commandˢ′  :  Set → Set
         Responseˢ′ :  (s : Set) → Commandˢ′ s → Set
         nextˢ′     :  (s : Set) → (c : Commandˢ′ s) → Responseˢ′ s c → Set

open SetInterfaceˢ

module _  (I   : SetInterfaceˢ ) (let Stateˢ = Set)
          (let C  = Commandˢ′ I) (let  R  = Responseˢ′ I)
          (let next = nextˢ′ I) where
  handle :  (M : Set → Set) → Set
  handle M =
     (A : Set) → (s : Stateˢ)  → (c : C s) →  (f : (r : R s c) → next s c r → M A) → M A

postulate Char : Set

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- Andreas, Ulf, 2016-06-01, discussing issue #679
-- {-# OPTIONS -v tc.with.strip:20 #-}

postulate anything : {A : Set} → A

data Ty : Set where
  _=>_ : (a b : Ty) → Ty

⟦_⟧ : Ty → Set
⟦ a => b ⟧ = ⟦ a ⟧ → ⟦ b ⟧

eq : (a : Ty) → ⟦ a ⟧ → ⟦ a ⟧ → Set
eq (a => b) f g = ∀ {x y : ⟦ a ⟧} → eq a x y → eq b (f x) (g y)

bad : (a : Ty) (x : ⟦ a ⟧) → eq a x x
bad (a => b) f h with b
bad (a => b) f h | _ = anything
-- ERROR WAS: Too few arguments in with clause!
-- Should work now.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-09-23
-- Issue 1194, reported by marco.vax91, 2014-06-13

-- {-# OPTIONS -v scope.operators:50 #-}

module _ where

module A where

  data D1 : Set where
    c : D1

  -- Just default notation for c here.

module B where

  data D2 : Set where
    c : A.D1 → D2

  -- Interesting notation for c here.
  syntax c x = ⟦ x ⟧

open A
open B

-- Since there is only one interesting notation for c in scope
-- we should be able to use it.

test : D2
test = ⟦ c ⟧


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax CommGroup | CG

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20
  neg  : *  ->  * | ⊖_ r40

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊖N⊕ᴸ) a |> add (neg (a), a) = unit
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = unit
  (⊕C) a b |> add(a, b) = add(b, a)
-}

module CommGroup.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data CGₒ : Set where
  unitₒ addₒ negₒ : CGₒ

-- Term signature
CG:Sig : Signature CGₒ
CG:Sig = sig λ
  {  unitₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  negₒ   → (⊢₀ *) ⟼₁ *
  }

open Signature CG:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- {-# OPTIONS --safe #-}
module Language where

open import Map
open import Relation.Binary.PropositionalEquality
open import Data.String using (String)
open import Data.Nat
open import Data.Bool
open import Data.Maybe using (Maybe; just; nothing)
open import Agda.Builtin.Unit
open import Data.Empty
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_)
open import Data.List

-- I separated this because of function calls
data VarId : Set where
  Var : (x : String) → VarId

-- This is the language of expressions
data Aexp {A : Set} : Set where
  _+`_ : ∀(x1 x2 : Aexp {A}) → Aexp
  _-`_ : ∀(x1 x2 : Aexp {A}) → Aexp
  _*`_ : ∀(x1 x2 : Aexp {A}) → Aexp
  Avar : ∀(x : String) → Aexp
  Anum : ∀(x : A) → Aexp
  -- Type A should be comparable to 0
  -- _/_ : ∀(x1 x2 : A) → (x2 ≡ 0) → Aexp

-- Special - for ℕ
_~-~_ : (a b : ℕ) → ℕ
zero ~-~ b = 0
suc a ~-~ b = a ~-~ b

-- Evaluation of Arithexp
aeval : (st : String → ℕ) → (exp : Aexp {ℕ}) → ℕ
aeval st (e +` e₁) = aeval st e + aeval st e₁
aeval st (e -` e₁) = aeval st e ~-~ aeval st e₁
aeval st (e *` e₁) = aeval st e * aeval st e₁
aeval st (Avar x) = st x
aeval st (Anum x) = x

-- This is the language of boolean expressions
data Bexp {A : Set} : Set where
  TRUE : Bexp
  FALSE : Bexp
  _<`_ : ∀ (x1 x2 : Aexp {A}) → Bexp
  _>`_ : ∀ (x1 x2 : Aexp {A}) → Bexp
  _≤`_ : ∀ (x1 x2 : Aexp {A}) → Bexp
  _≥`_ : ∀ (x1 x2 : Aexp {A}) → Bexp
  _≡`_ : ∀ (x1 x2 : Aexp {A}) → Bexp
  ¬`_ : ∀ (b : Bexp {A}) → Bexp
  _&&`_ : ∀ (b1 b2 : Bexp {A}) → Bexp
  _||`_ : ∀ (b1 b2 : Bexp {A}) → Bexp

-- Bool evaluation for ℕ
beval : (st : String → ℕ) → (b : Bexp {ℕ}) → Bool
beval st TRUE = true
beval st FALSE = false
beval st (x1 <` x2) = let ql = aeval st x1 in
                       let qr = aeval st x2 in
                       ((not ((ql ≤ᵇ qr) ∧ (qr ≤ᵇ ql))) ∧ (ql ≤ᵇ qr))
beval st (x1 >` x2) = let ql = aeval st x1 in
                       let qr = aeval st x2 in
                       ((not ((ql ≤ᵇ qr) ∧ (qr ≤ᵇ ql))) ∧ (qr ≤ᵇ ql))
beval st (x1 ≤` x2) = let l = aeval st x1 in
                       let r = aeval st x2 in
                       l ≤ᵇ r
beval st (x1 ≥` x2) = let l = aeval st x1 in
                       let r = aeval st x2 in
                       r ≤ᵇ l
beval st (x1 ≡` x2) = let l = aeval st x1 in
                       let r = aeval st x2 in
                       (l ≤ᵇ r) ∧ (r ≤ᵇ l)
beval st (¬` b) = not (beval st b)
beval st (b &&` b₁) = beval st b ∧ beval st b₁
beval st (b ||` b₁) = beval st b ∨ beval st b₁

data ATuple : Set where
  Arg : (v : String) → ATuple
  _,`_ : (f : ATuple) → (n : ATuple) → ATuple

data RTuple : Set where
  Ret : (v : String) → RTuple
  _,`_ : (f : RTuple) → (n : RTuple) → RTuple

-- Make a list of RTuple
rtuple2list : RTuple → List (String)
rtuple2list (Ret v) = v ∷ []
rtuple2list (r ,` r₁) = rtuple2list r ++ rtuple2list r₁

-- Name of functions are in different namespace
data FuncCall {A : Set} : Set where
  -- Calling a function
  <_>:=_<_> : (ret : RTuple) → (f : String) →
              (args : ATuple) → FuncCall
  -- XXX: Note that the below allows writing code like
  -- this: F()||F()//F()
  _||`_ : (l r : FuncCall {A}) → FuncCall
  -- _//`_ : (l r : FuncCall {A}) → FuncCall

-- This is the command language that we have
data Cmd {A : Set} : Set where
  SKIP : Cmd
  _:=_ : (l : VarId) → (r : Aexp {A}) → Cmd
  _;_ : (c1 c2 : Cmd {A}) → Cmd
  IF_THEN_ELSE_END : (b : Bexp {A}) → (t : Cmd {A}) →
                   (c : Cmd {A}) → Cmd
  WHILE_DO_END : (b : Bexp {A}) → (bo : Cmd {A}) → Cmd

  -- This makes calling the function a command
  EXEC : FuncCall {A} → Cmd

-- This is defining a function
-- This should give state of type (f → Maybe (Ret strings, args string, Cmd))
-- This should be an eval function, not a relation
-- This will be called from funccall and go from st => st'
data FuncDef {A : Set} : Set where
  -- Define a function/thread
  DEF_<_>⇒<_>:_END : (f : String) → (ATuple)
                   → (RTuple) → (c : Cmd {A}) → FuncDef

-- Toplevel
-- This should start from MAIN
-- This should be an topeval function KP => st
data Top {A : Set} : Set where
  MAIN:_END :  (c : Cmd {A}) → Top
  _;_ : FuncDef {A} → (a : Top {A}) → Top

infix 22 _:=_
infixl 21 _;_
infixl 20 _||`_
-- infixl 20 _//`_
infixl 23 _-`_
infixl 23 _+`_
infixl 24 _*`_
infixl 25 _,`_                  -- Highest precedence and left assoc

-- Example of a program with multiple functions
Main : Top
Main = DEF "Factorial" < Arg "K" >⇒< Ret "fact" ,` Ret "K" >:
            Var "n" := Avar "K" ;
            Var "fact" := Anum 1 ;
            WHILE (Avar "n" >` Anum 0) DO
              Var "fact" := Avar "fact" *` Avar "n" ;
              Var "n" := Avar "n" -` Anum 1
            END ;
            Var "res" := Anum 0 ;
            IF ((Avar "K" ≡` Anum 4) &&` (Avar "fact" ≡` Anum 24)) THEN
              Var "res" := Anum 1
            ELSE
              Var "res" := Anum 0
            END
       END ;
       MAIN:
        Var "K" := Anum 4 ;
        -- The below 2 have to be declared before being used
        Var "fact" := Anum 0 ;
        -- We should also have a tuple with each function/thread for
        -- pre-post.
        EXEC < Ret "fact" ,` Ret "K" >:= "Factorial" < Arg "K" >
       END

-- Making the tuple type needed to hold the program
data ProgTuple {A : Set} : Set where
  _,_,_ : (a : ATuple) → (r : RTuple) → (c : Cmd {A}) → ProgTuple

-- Getting stuff from the Progtuple
getProgCmd : {A : Set} → (p : Maybe (ProgTuple {A})) → Cmd {A}
getProgCmd (just (a , r , c)) = c
getProgCmd nothing = SKIP       -- Dangerous

getProgArgs : {A : Set} → (p : Maybe (ProgTuple {A})) → ATuple
getProgArgs (just (a , r , c)) = a
getProgArgs nothing = Arg "VOID"

getProgRets : {A : Set} → (p : Maybe (ProgTuple {A})) → RTuple
getProgRets (just (a , r , c)) = r
getProgRets nothing = Ret "VOID"

-- Semantics from here

-- All stacks should come from point of function call
-- Here Γ is the caller' stack
data _,_-[_]->ᴬ_ {A : Set} (Γ : (String → ( A))) :
                (String → ( A)) → (ATuple)
                → (String →  A) → Set where
  hd : ∀ (v : String) → ∀ (st : (String →  A)) →
         -- Γ v ≡ just vv →  -- Make sure that Arg is in the caller' stack
         -----------------------------------------------------------
         Γ , st -[ Arg v ]->ᴬ (Store st v (Γ v))

  tl : (l r : ATuple) → (st st' st'' : (String →  A)) →
        (Γ , st -[ l ]->ᴬ st') → (Γ , st' -[ r ]->ᴬ st'') →
        -----------------------------------------------------------
        Γ , st -[ (l ,` r) ]->ᴬ st''

-- Here Γ is the callee' stack
data _,_-[_]->ᴿ_ {A : Set}
                 (Γ : (String →  A))  :
                 (String →  A) → RTuple → (String →  A)
                 → Set where
  hd : ∀ (v : String) → ∀ (v1 v2 : A) → ∀ (st : (String →  A)) →
       -- → Γ v ≡ just v1 → st v ≡ just v2 →
       -- (_⊕_ : A → A → A) → ∀ (a b c : A) → (a ⊕ b ≡ b ⊕ a)
       -- → ((a ⊕ b) ⊕ c ≡ a ⊕ (b ⊕ c)) →
       -----------------------------------------------------------
       Γ , st -[ Ret v  ]->ᴿ (Store st v (Γ v))
       -- Γ , st -[ Ret v  ]->ᴿ (Store st v (Γ v ⊕ st v))

  tl : ∀ (l r : RTuple) → (st st' st'' : (String →  A)) →
       (Γ , st -[ l ]->ᴿ st') → (Γ , st' -[ r ]->ᴿ st'') →
       -----------------------------------------------------------
       Γ , st -[ (l ,` r) ]->ᴿ st''

mutual

-- These are the relations for ℕ
 data _,_=[_]=>_ (Γ : String → Maybe (ProgTuple {ℕ})) :
                 (String →  ℕ) →
                 Cmd {ℕ} → (String →  ℕ) →
                 Set where
  CSKIP : ∀ (st : (String →  ℕ)) →
          -----------------------
          Γ , st =[ SKIP ]=> st

  CASSIGN : ∀ (st : (String →  ℕ)) → ∀ (x : String) →
            ∀ (e : Aexp {ℕ}) →
          -----------------------------------------------------------
          Γ , st =[ Var x := e ]=> (Store st x (aeval st e))

  CSEQ : ∀ (st st' st'' : (String →  ℕ)) → ∀ (c1 c2 : Cmd {ℕ}) →
         Γ , st =[ c1 ]=> st' →
         Γ , st' =[ c2 ]=> st'' →
         -----------------------------------------------------------
         Γ , st =[ (c1 ; c2)]=> st''

  CIFT : ∀ (st st' : (String →  ℕ)) → (b : Bexp {ℕ}) →
         (t e : Cmd {ℕ}) →
         beval st b ≡ true →
         Γ , st =[ t ]=> st' →
         -----------------------------------------------------------
         Γ , st =[ (IF b THEN t ELSE e END)]=> st'

  CIFE : ∀ (st st' : (String →  ℕ)) →
         (b : Bexp {ℕ}) → (t e : Cmd {ℕ}) →
         beval st b ≡ false →
         Γ , st =[ e ]=> st' →
         -----------------------------------------------------------
         Γ , st =[ (IF b THEN t ELSE e END)]=> st'

  CLF : (st : (String →  ℕ)) →
        (b : Bexp {ℕ}) → (c : Cmd {ℕ}) →
         beval st b ≡ false →
         -----------------------------------------------------------
         Γ , st =[ (WHILE b DO c END) ]=> st

  CLT :  (st st' st'' : (String →  ℕ)) →
         (b : Bexp {ℕ}) → (c : Cmd {ℕ}) →
         beval st b ≡ true →
         Γ , st =[ c ]=> st' →
         Γ , st' =[ (WHILE b DO c END) ]=> st'' →
         -----------------------------------------------------------
         Γ , st =[ (WHILE b DO c END) ]=> st''

  -- XXX: Done.
  CEX : ∀ (f : FuncCall {ℕ}) → ∀ (st st' : (String → ℕ))
        → Γ , st =[ f ]=>ᶠ st'
        -----------------------------------------------------------
        → Γ , st =[ EXEC f ]=> st'

-- TODO: The function calls and definition with ℕ
 data _,_=[_]=>ᶠ_ (Γ : String → (Maybe (ProgTuple {ℕ}))) :
                (String → ℕ) → FuncCall {ℕ} → (String → ℕ)
                → Set where

  Base : ∀ (fname : String) →        -- name of the function
         ∀ (stm : String → ℕ) -- caller stack,
         → (stf' stf'' : String → ℕ) -- These are the pre-call and
                                     -- post-call callee stack,
                                     -- respectively.
         → (stm' : String → ℕ)       -- The resultant caller stack

         -- res of putting values on callee stack
         → stm , (K 0) -[ getProgArgs (Γ fname) ]->ᴬ stf'

         -- result of running the function
         → Γ , stf' =[ getProgCmd (Γ fname) ]=> stf''

         -- copying ret values back on caller' stack
         → stf'' , stm -[ getProgRets (Γ fname) ]->ᴿ stm'

         -----------------------------------------------------------
         → Γ , stm =[ < getProgRets (Γ fname) >:=
             fname < getProgArgs (Γ fname) > ]=>ᶠ stm'
         -- XXX: The above needs to be extended to return a list of
         -- fname with stm'. This will allow merge to be called in ||
         -- and //

-- Doing the evaluation of top
evalProg : {A : Set} → (p : Top {A}) →
           (st : String → Maybe (ProgTuple {A})) →
           (String → Maybe (ProgTuple {A}))
evalProg MAIN: c END st = (StoreP st "MAIN" (Arg "void" , Ret "void" , c))
evalProg (DEF f < x >⇒< x1 >: c END ; p) st =
              StoreP (evalProg p st) f (x , x1 , c)

-- Example of relation on ℕ
ex1 : ∀ (Γ : (String → Maybe ProgTuple)) → ∀ (st : (String →  ℕ))
      → Γ , st =[ SKIP ]=> st
ex1 Γ st = CSKIP st

-- Hoare logic starts here!
{-# NO_POSITIVITY_CHECK #-}

-- XXX: Maybe later define another language for it?
-- Logical expressions with ℕ as relations (used for Hoare Propositions)
data _|=_ (st : String →  ℕ) : Bexp {ℕ} → Set where
  LT : ∀ (l r : Aexp {ℕ}) → (aeval st l) Data.Nat.< (aeval st r)
       → st |= (l <` r)
  LE : ∀ (l r : Aexp {ℕ}) → (aeval st l) Data.Nat.≤ (aeval st r)
       → st |= (l ≤` r)
  GT : ∀ (l r : Aexp {ℕ}) → (aeval st l) Data.Nat.> (aeval st r)
       → st |= (l >` r)
  GE : ∀ (l r : Aexp {ℕ}) → (aeval st l) Data.Nat.≥ (aeval st r)
       → st |= (l ≥` r)
  EQ : ∀ (l r : Aexp {ℕ}) → (aeval st l) ≡ (aeval st r)
       → st |= (l ≡` r)
  TT : st |= TRUE
  AND : ∀ (b1 b2 : Bexp {ℕ}) → (st |= b1) → (st |= b2)
        → st |= (b1 &&` b2)
  ORL : ∀ (b1 b2 : Bexp {ℕ}) → (st |= b1) → (st |= (b1 ||` b2))
  ORR : ∀ (b1 b2 : Bexp {ℕ}) → (st |= b2) → (st |= (b1 ||` b2))
  -- XXX: Had to disable POSITIVITY_CHECK
  NOT : ∀ (b : Bexp {ℕ}) → ((st |= b) → ⊥) → st |= (¬` b)

-- Assert with ℙrops
Assertℙ : ∀ (b : Bexp {ℕ}) → (String → ℕ) → Set
Assertℙ b st = st |= b

-- Defn of substitution rule with ℙrop
Subsℙ : ∀ (b : Bexp {ℕ})       -- b is my assertion
       → (X : String)
       → (e : Aexp {ℕ}) → (String → ℕ)
       → Set
Subsℙ b X e st = (Store st X (aeval st e)) |= b

getStates : ∀ (stf stm : String → ℕ) → ATuple → (String → ℕ)
getStates stf stm (Arg v) = Store stf v (stm v)
getStates stf stm (l ,` r) = getStates (getStates stf stm l) stm r

getStatesR : ∀ (stm stf : String → ℕ) → RTuple → (String → ℕ)
getStatesR stm stf (Ret v) = Store stm v (stf v)
getStatesR stm stf (rets ,` rets₁) = getStatesR (getStatesR stm stf rets) stf rets₁

-- Subs for the input arguments before calling a function
SubsArgs : ∀ (Q : Bexp {ℕ}) → (args : ATuple) → (stf stm : (String → ℕ))
           → Set
SubsArgs Q args stf stm = (getStates stf stm args) |= Q

-- Subs for the output rets after calling function
SubsRets : ∀ (R : Bexp {ℕ}) → (rets : RTuple) → (stm stf : (String → ℕ))
           → Set
SubsRets R rets stm stf = (getStatesR stm stf rets) |= R

-- Lemma for getStates
getstates-eq-lemma : ∀ (st stm st' : (String → ℕ)) → (args : ATuple)
                     → stm , st -[ args ]->ᴬ st'
                     → (getStates st stm args) ≡ st'
getstates-eq-lemma st stm .(Store st v (stm v)) (Arg v) (hd .v .st) = refl
getstates-eq-lemma st stm st' (args ,` args₁) (tl .args .args₁ .st st'' .st' cmd cmd₁) with
  getstates-eq-lemma st stm st'' args cmd
... | refl = getstates-eq-lemma st'' stm st' args₁ cmd₁

-- Lemma for getStatesR
getstatesr-eq-lemma : ∀ (stm stf stm' : (String → ℕ)) → (rets : RTuple)
                      → (stf , stm -[ rets ]->ᴿ stm')
                      → (getStatesR stm stf rets) ≡ stm'
getstatesr-eq-lemma stm stf .(Store stm v (stf v)) .(Ret v) (hd v v1 v2 .stm) = refl
getstatesr-eq-lemma stm stf stm' .(l ,` r) (tl l r .stm st' .stm' cmd cmd₁) with
  getstatesr-eq-lemma stm stf st' l cmd
... | refl = getstatesr-eq-lemma st' stf stm' r cmd₁

-- Now the soundness proof for SubsArgs
SubsArgs-theorem : ∀ (stf stm stf' : (String → ℕ)) → (Q : Bexp {ℕ})
                   → (args : ATuple) → (P : SubsArgs Q args stf stm)
                   → (cmd : stm , stf -[ args ]->ᴬ stf')
                   → (stf' |= Q)
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(l <` r) .(Arg v) (LT l r x) (hd v .stf) = LT l r x
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(l ≤` r) .(Arg v) (LE l r x) (hd v .stf) = LE l r x
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(l >` r) .(Arg v) (GT l r x) (hd v .stf) = GT l r x
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(l ≥` r) .(Arg v) (GE l r x) (hd v .stf) = GE l r x
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(l ≡` r) .(Arg v) (EQ l r x) (hd v .stf) = EQ l r x
SubsArgs-theorem stf stm .(Store stf v (stm v)) .TRUE .(Arg v) TT (hd v .stf) = TT
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(b1 &&` b2) .(Arg v) (AND b1 b2 P P₁) (hd v .stf) = AND b1 b2 P P₁
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(b1 ||` b2) .(Arg v) (ORL b1 b2 P) (hd v .stf) = ORL b1 b2 P
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(b1 ||` b2) .(Arg v) (ORR b1 b2 P) (hd v .stf) = ORR b1 b2 P
SubsArgs-theorem stf stm .(Store stf v (stm v)) .(¬` b) .(Arg v) (NOT b x) (hd v .stf) = NOT b x
SubsArgs-theorem stf stm stf' .(l₁ <` r₁) .(l ,` r) (LT l₁ r₁ x) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = LT l₁ r₁ x
SubsArgs-theorem stf stm stf' .(l₁ ≤` r₁) .(l ,` r) (LE l₁ r₁ x) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = LE l₁ r₁ x
SubsArgs-theorem stf stm stf' .(l₁ >` r₁) .(l ,` r) (GT l₁ r₁ x) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = GT l₁ r₁ x
SubsArgs-theorem stf stm stf' .(l₁ ≥` r₁) .(l ,` r) (GE l₁ r₁ x) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = GE l₁ r₁ x
SubsArgs-theorem stf stm stf' .(l₁ ≡` r₁) .(l ,` r) (EQ l₁ r₁ x) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = EQ l₁ r₁ x
SubsArgs-theorem stf stm stf' .TRUE .(l ,` r) TT (tl l r .stf st' .stf' cmd cmd₁) = TT
SubsArgs-theorem stf stm stf' .(b1 &&` b2) .(l ,` r) (AND b1 b2 P P₁) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = AND b1 b2 P P₁
SubsArgs-theorem stf stm stf' .(b1 ||` b2) .(l ,` r) (ORL b1 b2 P) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = ORL b1 b2 P
SubsArgs-theorem stf stm stf' .(b1 ||` b2) .(l ,` r) (ORR b1 b2 P) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = ORR b1 b2 P
SubsArgs-theorem stf stm stf' .(¬` b) .(l ,` r) (NOT b x) (tl l r .stf st' .stf' cmd cmd₁) rewrite
 getstates-eq-lemma stf stm st' l cmd | getstates-eq-lemma st' stm stf' r cmd₁ = NOT b x

-- The inductive case for concurrent function calls either (// or ||)
-- This thorem is saying that if the product (conjunction) of two
-- pre-conditions holds on the caller' stack then the pre-condition
-- holds for each of the Funccall in the concurrent execution.

-- TODO: The below theorem can be extended to N instead of just two
-- inductively with ease. Leaving it to two for now as proof of concept.
conc-pre-theorem : ∀ (stm stf1 stf1' stf2 stf2' : (String → ℕ))
                   → ∀ (a1 a2 : ATuple)
                   → (c1 : stm , stf1 -[ a1 ]->ᴬ stf1')
                   → (c2 : stm , stf2 -[ a2 ]->ᴬ stf2')
                   → ∀ (Q1 Q2 : Bexp {ℕ})
                   → (SubsArgs Q1 a1 stf1 stm) × (SubsArgs Q2 a2 stf2 stm)
                   → (stf1' |= Q1) × (stf2' |= Q2)
conc-pre-theorem stm stf1 stf1' stf2 stf2' a1 a2 c1 c2 Q1 Q2 (fst Data.Product., snd)
  = (SubsArgs-theorem stf1 stm stf1' Q1 a1 fst c1) Data.Product.,
    (SubsArgs-theorem stf2 stm stf2' Q2 a2 snd c2)

-- DONE: We do the same as Subsargs for ret but with stacks swapped
SubsRets-theorem : ∀ (stm stf stm' : (String → ℕ)) → (Q : Bexp {ℕ})
                   → (rets : RTuple) → (P : SubsRets Q rets stm stf)
                   → (cmd : stf , stm -[ rets ]->ᴿ stm')
                   → (stm' |= Q)
SubsRets-theorem stm stf .(Store stm v (stf v)) .(l <` r) .(Ret v) (LT l r x) (hd v v1 v2 .stm) = LT l r x
SubsRets-theorem stm stf .(Store stm v (stf v)) .(l ≤` r) .(Ret v) (LE l r x) (hd v v1 v2 .stm) = LE l r x
SubsRets-theorem stm stf .(Store stm v (stf v)) .(l >` r) .(Ret v) (GT l r x) (hd v v1 v2 .stm) = GT l r x
SubsRets-theorem stm stf .(Store stm v (stf v)) .(l ≥` r) .(Ret v) (GE l r x) (hd v v1 v2 .stm) = GE l r x
SubsRets-theorem stm stf .(Store stm v (stf v)) .(l ≡` r) .(Ret v) (EQ l r x) (hd v v1 v2 .stm) = EQ l r x
SubsRets-theorem stm stf .(Store stm v (stf v)) .TRUE .(Ret v) TT (hd v v1 v2 .stm) = TT
SubsRets-theorem stm stf .(Store stm v (stf v)) .(b1 &&` b2) .(Ret v) (AND b1 b2 P P₁) (hd v v1 v2 .stm) =
 AND b1 b2 P P₁
SubsRets-theorem stm stf .(Store stm v (stf v)) .(b1 ||` b2) .(Ret v) (ORL b1 b2 P) (hd v v1 v2 .stm) = ORL b1 b2 P
SubsRets-theorem stm stf .(Store stm v (stf v)) .(b1 ||` b2) .(Ret v) (ORR b1 b2 P) (hd v v1 v2 .stm) = ORR b1 b2 P
SubsRets-theorem stm stf .(Store stm v (stf v)) .(¬` b) .(Ret v) (NOT b x) (hd v v1 v2 .stm) = NOT b x
SubsRets-theorem stm stf stm' .(l₁ <` r₁) .(l ,` r) (LT l₁ r₁ x) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = LT l₁ r₁ x
SubsRets-theorem stm stf stm' .(l₁ ≤` r₁) .(l ,` r) (LE l₁ r₁ x) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = LE l₁ r₁ x
SubsRets-theorem stm stf stm' .(l₁ >` r₁) .(l ,` r) (GT l₁ r₁ x) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = GT l₁ r₁ x
SubsRets-theorem stm stf stm' .(l₁ ≥` r₁) .(l ,` r) (GE l₁ r₁ x) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = GE l₁ r₁ x
SubsRets-theorem stm stf stm' .(l₁ ≡` r₁) .(l ,` r) (EQ l₁ r₁ x) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = EQ l₁ r₁ x
SubsRets-theorem stm stf stm' .TRUE .(l ,` r) TT (tl l r .stm st' .stm' cmd cmd₁) = TT
SubsRets-theorem stm stf stm' .(b1 &&` b2) .(l ,` r) (AND b1 b2 P P₁) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = AND b1 b2 P P₁
SubsRets-theorem stm stf stm' .(b1 ||` b2) .(l ,` r) (ORL b1 b2 P) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = ORL b1 b2 P
SubsRets-theorem stm stf stm' .(b1 ||` b2) .(l ,` r) (ORR b1 b2 P) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = ORR b1 b2 P
SubsRets-theorem stm stf stm' .(¬` b) .(l ,` r) (NOT b x) (tl l r .stm st' .stm' cmd cmd₁) rewrite
 getstatesr-eq-lemma stm stf st' l cmd | getstatesr-eq-lemma st' stf stm' r cmd₁ = NOT b x

-- FIXME: The post condition is being proved only for 2 concurrent
-- calls, but can be easily extended to N using an inductive
-- data-structure.
conc-post-lemma : ∀ (stf1 stf2 stm1 stm1' stm2 stm2' : (String → ℕ)) → (Q1 Q2 : Bexp {ℕ})
                  → (r1 r2 : RTuple)
                  → (c1 : stf1 , stm1 -[ r1 ]->ᴿ stm1')
                  → (c2 : stf2 , stm2 -[ r2 ]->ᴿ stm2')
                  → (SubsRets Q1 r1 stm1 stf1) × (SubsRets Q2 r2 stm2 stf2)
                  → (stm1' |= Q1 × stm2' |= Q2)
conc-post-lemma stf1 stf2 stm1 stm1' stm2 stm2' Q1 Q2 r1 r2 c1 c2 (fst Data.Product., snd) =
  (SubsRets-theorem stm1 stf1 stm1' Q1 r1 fst c1) Data.Product., SubsRets-theorem stm2 stf2 stm2' Q2 r2 snd c2

-- TODO: We need to show that stm2 |= Q2 ≡ stm |= Q2. This requires us
-- to show that merge does not change the values of stm2, which
-- guarantee stm2 |= Q2. This is from the rule of constancy

-- TODO: Rule of constancy can be proven, by first using t_update_neq
-- from Map and then proving the lookup on aeval.

merge-cong : ∀ (v1 v2 : String) → (v1 ≡ v2) → (Ret v1 ≡ Ret v2)
merge-cong v1 .v1 refl = refl

postulate merge-lemma : ∀ (stm1 stm2 stm : (String → ℕ)) → (Q2 : Bexp {ℕ})
              → (r1 r2 : RTuple) → (merge : stm1 , stm2 -[ r1 ]->ᴿ stm)
              → stm2 |= Q2 → ¬ (r2 ≡ r1) → stm |= Q2
-- merge-lemma stm1 stm2 .(Store stm2 v (stm1 v)) Q2 .(Ret v) (Ret v₂) (hd v v1 v2 .stm2) p q rewrite t-update-neq stm2 v v₂ (stm1 v) λ x → ⊥-elim (q (merge-cong v₂ v x)) = {!!}
-- merge-lemma stm1 stm2 .(Store stm2 v (stm1 v)) Q2 .(Ret v) (r2 ,` r3) (hd v v1 v2 .stm2) p q = {!!}
-- merge-lemma stm1 stm2 stm Q2 .(l ,` r) r2 (tl l r .stm2 st' .stm merge merge₁) p q = {!!}

-- Now the theorem that Q1 &&` Q2 hold on the merged stm stack XXX:
-- Again this is being done only for two concurrent functions, but can
-- be extended to N via an inductive data type.
conc-post-theorem : ∀ (stm1 stm2 stm : (String → ℕ)) → (Q1 Q2 : Bexp {ℕ})
                    -- stm is the merged stack
                    → (r1 r2 : RTuple) → (merge : stm1 , stm2 -[ r1 ]->ᴿ stm)
                    → (stm1 |= Q1 × stm2 |= Q2)
                    → (P : SubsRets Q1 r1 stm2 stm1)
                    → ¬ (r2 ≡ r1)
                    → (stm |= (Q1 &&` Q2))
conc-post-theorem stm1 stm2 stm Q1 Q2 r1 r2 merge (_ Data.Product., snd) P nr =
  AND Q1 Q2 (SubsRets-theorem stm2 stm1 stm Q1 r1 P merge) (merge-lemma stm1 stm2 stm Q2 r1 r2 merge snd nr)

-- TODO: This is the theorem for post-condition for two concurrent
-- function calls. This is harder than the pre-condition.

-- 1.) In this case caller stack goes from stm -> stm' and stm -> stm''
-- for the two functions called concurrently.

-- 2.) stm'' and stm' need to be combined into a single stm''' after the
-- execution of the two functions concurrently? But how? This will be
-- done in FuncCall relational semantics data type above.

-- 3.) Once we have point 2 done then we can prove the correctness same
-- as conc-pre-theorem but for post-condition of || or //.

-- XXX: Use the above lemma to show the side condition state of R' X ≡
-- stf I and so on for all outputs.

-- Subs theorem states that Hoare' subs rule is valid (or sound)
subs-theoremℙ : ∀ (Γ : String → Maybe (ProgTuple {ℕ}))
          → ∀ (st st' : (String → ℕ)) → (X : String) → (e : Aexp {ℕ})
          → (Q : Bexp {ℕ}) → (P : (Subsℙ Q X e st))
          → (C : Γ , st =[ Var X := e ]=> st')
          → (Assertℙ Q st')
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(l <` r) (LT l r x) (CASSIGN .st .X .e) = LT l r x
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(l ≤` r) (LE l r x) (CASSIGN .st .X .e) = LE l r x
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(l >` r) (GT l r x) (CASSIGN .st .X .e) = GT l r x
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(l ≥` r) (GE l r x) (CASSIGN .st .X .e) = GE l r x
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(l ≡` r) (EQ l r x) (CASSIGN .st .X .e) = EQ l r x
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .TRUE TT (CASSIGN .st .X .e) = TT
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(b1 &&` b2) (AND b1 b2 p p₁) (CASSIGN .st .X .e) = AND b1 b2 p p₁
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(b1 ||` b2) (ORL b1 b2 p) (CASSIGN .st .X .e) = ORL b1 b2 p
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(b1 ||` b2) (ORR b1 b2 p) (CASSIGN .st .X .e) = ORR b1 b2 p
subs-theoremℙ Γ st .(Store st X (aeval st e)) X e .(¬` b) (NOT b p) (CASSIGN .st .X .e) = NOT b p

-- Consequence hoare rule theorem the general case soundness theorem.
-- This works for both P₁ ⇒ P ∧ Q ⇒ Q₁. Model the implication using (¬`
-- P₁) ||` P and (¬` Q) ||` Q₁
cons-theorem : ∀ (st : (String → ℕ)) → ∀ (P Q : Bexp {ℕ}) → Assertℙ P st
             → st |= ((¬` P) ||` Q) → Assertℙ Q st
cons-theorem st P Q a (ORL .(¬` P) .Q (NOT .P x)) = ⊥-elim (x a)
cons-theorem st P Q a (ORR .(¬` P) .Q b) = b

-- The SKIP Hoare rule soundness theorem
skip-theorem : ∀ (Γ : String → Maybe (ProgTuple {ℕ})) →
               ∀ (st st' : (String → ℕ)) → ∀ (P : Bexp {ℕ})
               → Assertℙ P st → Γ , st =[ SKIP ]=> st'
               → Assertℙ P st'
skip-theorem Γ st .st p sk (CSKIP .st) = sk

-- The Sequence Hoare rule soundness theorem.

-- Definition of a sound sequence rule
data _,≪_≫_≪_≫ (Γ : String → Maybe (ProgTuple {ℕ})) : Bexp {ℕ}
                  → Cmd {ℕ} → Bexp {ℕ} → Set where
  HSEQ : ∀ (st st' :  (String → ℕ))
         → (c1 c2 : Cmd {ℕ})
         → (P Q : Bexp {ℕ})
         → st |= P
         → Γ , st =[ c1 ; c2 ]=> st'
         → st' |= Q
         →
         -----------------------------------------------------------
         Γ ,≪ P ≫ (c1 ; c2) ≪ Q ≫

-- The sequence rule soundness theorem
-- this is a different way of looking at it
seq-theorem : ∀ (Γ : String → Maybe (ProgTuple {ℕ}))
              → ∀ (st st' st'' : (String → ℕ))
              → (c1 c2 : Cmd {ℕ})
              → (P Q R : Bexp {ℕ})
              → (Γ , st =[ c1 ]=> st')
              → (Γ , st' =[ c2 ]=> st'')
              → st |= P
              → st' |= Q
              → st'' |= R
              → Γ ,≪ P ≫ c1 ; c2 ≪ R ≫
seq-theorem Γ st st' st'' c1 c2 P Q R sc1 sc2 p _ r
  = HSEQ st st'' c1 c2 P R p (CSEQ st st' st'' c1 c2 sc1 sc2) r

-- Help lemma
contradiction-lemma : ∀ (b : Bexp {ℕ}) → ∀ (st : (String → ℕ))
                      → (beval st b ≡ true)
                      → (beval st b ≡ false) → ⊥
contradiction-lemma b st p rewrite p = λ ()

-- Deterministic lemma for argument passing
deterministic-ret-lemma : ∀ (stf stm stm' stm'' : (String → ℕ)) → (rets : RTuple)
                          → (stm , stf -[ rets ]->ᴿ stm') → (stm , stf   -[ rets ]->ᴿ stm'')
                          → (stm' ≡ stm'')
deterministic-ret-lemma stf stm .(Store stf v (stm v)) .(Store stf v (stm v)) .(Ret v) (hd v v1 v2 .stf) (hd .v v3 v4 .stf) = refl
deterministic-ret-lemma stf stm stm' stm'' .(l ,` r) (tl l r .stf st' .stm' p1 p3) (tl .l .r .stf st'' .stm'' p2 p4) with deterministic-ret-lemma stf stm st' st'' l p1 p2
... | refl with deterministic-ret-lemma st' stm stm' stm'' r p3 p4
... | refl = refl

-- Deterministic lemma for argument passing
deterministic-arg-lemma : ∀ (stm stf stf' stf'' : (String → ℕ)) → (args : ATuple)
                          → (stm , stf -[ args ]->ᴬ stf') → (stm , stf -[ args ]->ᴬ stf'')
                          → (stf' ≡ stf'')
deterministic-arg-lemma stm stf .(Store stf v (stm v)) .(Store stf v (stm v)) .(Arg v) (hd v .stf) (hd .v .stf) = refl
deterministic-arg-lemma stm stf stf' stf'' .(l ,` r) (tl l r .stf st' .stf' p1 p3) (tl .l .r .stf st'' .stf'' p2 p4) with deterministic-arg-lemma stm stf st' st'' l p1 p2
... | refl with deterministic-arg-lemma stm st' stf' stf'' r p3 p4
... | refl = refl

mutual
-- The deterministic execution for function calls
 deterministic-func-theorem : ∀ (Γ : (String → Maybe (ProgTuple {ℕ})))
                              → ∀ (stm stm1 stm2 : (String → ℕ))
                              → ∀ (f : FuncCall {ℕ} )
                              → Γ , stm =[ f ]=>ᶠ stm2
                              → Γ , stm =[ f ]=>ᶠ stm1
                              → stm2 ≡ stm1
 deterministic-func-theorem Γ stm stm1 stm2 .(< getProgRets (Γ fname) >:= fname < getProgArgs (Γ fname) >) (Base fname .stm stf' stf'' .stm2 x x₁ x₂) (Base .fname .stm stf''' stf'''' .stm1 x₃ x₄ x₅) with deterministic-arg-lemma stm (K 0) stf' stf''' (getProgArgs (Γ fname)) x x₃
 ... | refl with deterministic-exec-theorem Γ stf' stf'' stf'''' (getProgCmd (Γ fname)) x₁ x₄
 ... | refl with deterministic-ret-lemma stm stf'' stm1 stm2 (getProgRets (Γ fname)) x₅ x₂
 ... | refl = refl

-- Lemma for deterministic execution of commands
 deterministic-exec-theorem : ∀ (Γ : String → Maybe (ProgTuple {ℕ}))
                           → ∀ (st st' st'' : String → ℕ)
                           → ∀ (c : Cmd {ℕ})
                           → Γ , st =[ c ]=> st'
                           → Γ , st =[ c ]=> st''
                           → st' ≡ st''
 deterministic-exec-theorem Γ st .st .st .SKIP (CSKIP .st) (CSKIP .st) = refl
 deterministic-exec-theorem Γ st .(Store st x (aeval st e)) .(Store st x (aeval st e)) .(Var x := e) (CASSIGN .st x e) (CASSIGN .st .x .e) = refl
 deterministic-exec-theorem Γ st st' st'' .(c1 ; c2) (CSEQ .st st''' .st' c1 c2 e1 e3) (CSEQ .st st'''' .st'' .c1 .c2 e2 e4) with deterministic-exec-theorem Γ st st''' st'''' c1 e1 e2
 ... | refl  with deterministic-exec-theorem Γ st''' st'' st' c2 e4 e3
 ... | refl = refl
 deterministic-exec-theorem Γ st st' st'' .(IF b THEN t ELSE e END) (CIFT .st .st' b t e x e1) (CIFT .st .st'' .b .t .e x₁ e2) with deterministic-exec-theorem Γ st st'' st' t e2 e1
 ... | refl = refl
 deterministic-exec-theorem Γ st st' st'' .(IF b THEN t ELSE e END) (CIFT .st .st' b t e x e1) (CIFE .st .st'' .b .t .e x₁ e2) = ⊥-elim (contradiction-lemma b st x x₁)
 deterministic-exec-theorem Γ st st' st'' .(IF b THEN t ELSE e END) (CIFE .st .st' b t e x e1) (CIFT .st .st'' .b .t .e x₁ e2) = ⊥-elim (contradiction-lemma b st x₁ x)
 deterministic-exec-theorem Γ st st' st'' .(IF b THEN t ELSE e END) (CIFE .st .st' b t e x e1) (CIFE .st .st'' .b .t .e x₁ e2) with deterministic-exec-theorem Γ st st'' st' e e2 e1
 ... | refl = refl
 deterministic-exec-theorem Γ st .st .st .(WHILE b DO c END) (CLF .st b c x) (CLF .st .b .c x₁) = refl
 deterministic-exec-theorem Γ st .st st'' .(WHILE b DO c END) (CLF .st b c x) (CLT .st st' .st'' .b .c x₁ e2 e3) = ⊥-elim (contradiction-lemma b st x₁ x)
 deterministic-exec-theorem Γ st st' .st .(WHILE b DO c END) (CLT .st st''' .st' b c x e1 e3) (CLF .st .b .c x₁) = ⊥-elim (contradiction-lemma b st x x₁)
 deterministic-exec-theorem Γ st st' st'' .(WHILE b DO c END) (CLT .st st''' .st' b c x e1 e3) (CLT .st st'''' .st'' .b .c x₁ e2 e4) with deterministic-exec-theorem Γ st st'''' st''' c e2 e1
 ... | refl with deterministic-exec-theorem Γ st''' st'' st' (WHILE b DO c END) e4 e3
 ... | refl = refl
 deterministic-exec-theorem Γ st st' st'' (EXEC < ret >:= f < args >) (CEX .(< ret >:= f < args >) .st .st' x) (CEX .(< ret >:= f < args >) .st .st'' x₁) with deterministic-func-theorem Γ st  st' st'' < ret >:= f < args > x₁ x
 ... | refl = refl

-- Proving seq rule soundness via standard technique
seq-theorem1 : ∀ (Γ : String → Maybe (ProgTuple {ℕ}))
              → ∀ (st1 st2 st3 st4 : (String → ℕ))
              → (c1 c2 : Cmd {ℕ})
              → (P Q R : Bexp {ℕ})
              → (Γ , st1 =[ c1 ]=> st2)
              → (Γ , st2 =[ c2 ]=> st3)
              → st1 |= P
              → st2 |= Q
              → st3 |= R
              → Γ , st1 =[ c1 ; c2 ]=> st4
              → st4 |= R
seq-theorem1 Γ st1 st2 st3 st4 c1 c2 P Q R ec1 ec2 st1p st2q st3r (CSEQ .st1 st' .st4 .c1 .c2 ec12 ec13) with deterministic-exec-theorem Γ st1 st2 st' c1 ec1 ec12
... | refl with deterministic-exec-theorem Γ st2 st3 st4 c2 ec2 ec13
... | refl = st3r

-- TODO: Add If-else and while soundness rules if you want here

-- This is the derivable one (completely syntactic, not semantic)

-- In my case I will follow the same technique as SF, but instead of
-- taking propositions I will take the state and the boolean expression
-- for each proposition. This will make the syntactic derivation of
-- Hoare rules possible.


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Category.Finite.Fin.Instance.Parallel where

open import Data.Nat using (ℕ)
open import Data.Fin
open import Data.Fin.Patterns
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Categories.Category.Finite.Fin
open import Categories.Category

private
  variable
    a b c d : Fin 2

--
--  /---0---\
-- 0         1
--  \---1---/
--
ParallelShape : FinCatShape
ParallelShape = record
  { size     = 2
  ; ∣_⇒_∣    = card
  ; hasShape = record
    { id        = id
    ; _∘_       = _∘_
    ; assoc     = assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    }
  }
  where card : Fin 2 → Fin 2 → ℕ
        card 0F 0F = 1
        card 0F 1F = 2
        card 1F 0F = 0
        card 1F 1F = 1

        id : Fin (card a a)
        id {0F} = 0F
        id {1F} = 0F

        _∘_ : ∀ {a b c} → Fin (card b c) → Fin (card a b) → Fin (card a c)
        _∘_ {0F} {0F} {0F} 0F 0F = 0F
        _∘_ {0F} {0F} {1F} 0F 0F = 0F
        _∘_ {0F} {0F} {1F} 1F 0F = 1F
        _∘_ {0F} {1F} {1F} 0F 0F = 0F
        _∘_ {0F} {1F} {1F} 0F 1F = 1F
        _∘_ {1F} {1F} {1F} 0F 0F = 0F

        assoc : ∀ {f : Fin (card a b)} {g : Fin (card b c)} {h : Fin (card c d)} →
                  ((h ∘ g) ∘ f) ≡ (h ∘ (g ∘ f))
        assoc {0F} {0F} {0F} {0F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {0F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {0F} {1F} {0F} {0F} {1F} = refl
        assoc {0F} {0F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {1F} {1F} {0F} {1F} {0F} = refl
        assoc {0F} {1F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {1F} {1F} {1F} {1F} {0F} {0F} = refl
        assoc {1F} {1F} {1F} {1F} {0F} {0F} {0F} = refl

        identityˡ : ∀ {a b} {f : Fin (card a b)} → (id ∘ f) ≡ f
        identityˡ {0F} {0F} {0F} = refl
        identityˡ {0F} {1F} {0F} = refl
        identityˡ {0F} {1F} {1F} = refl
        identityˡ {1F} {1F} {0F} = refl

        identityʳ : ∀ {a b} {f : Fin (card a b)} → (f ∘ id) ≡ f
        identityʳ {0F} {0F} {0F} = refl
        identityʳ {0F} {1F} {0F} = refl
        identityʳ {0F} {1F} {1F} = refl
        identityʳ {1F} {1F} {0F} = refl

Parallel : Category _ _ _
Parallel = FinCategory ParallelShape

module Parallel = Category Parallel

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories