text:
module binding-preserve where

open import utility
  renaming (_U̬_ to _∪_ ; _|̌_ to _-_)
open import sn-calculus
open import Function using (_∋_ ; _$_ ; _∘_)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
  using (done; halted ; paused ; value-max)
open import Esterel.Context
open import Esterel.Context.Properties
open import Esterel.Environment
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open done
open halted
open paused
open Context1
open EvaluationContext1

open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; [_] ; _++_)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using (++⁻)
  renaming ( ++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ )
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_)
open import Data.Product
  using (Σ ; proj₁ ; proj₂ ; ∃ ; _,_ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; id)
open import Relation.Nullary
  using (Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; sym ; module ≡-Reasoning ; subst)

open ≡-Reasoning using (_≡⟨_⟩_ ; _≡⟨⟩_ ; _∎)

open ListSet Data.Nat._≟_
  using (set-subtract ; set-subtract-merge ; set-subtract-notin; set-subtract-[]; set-subtract-split)

++-distribute-subtract : ∀ xs ys zs →
  set-subtract (xs ++ ys) zs ≡
  set-subtract xs zs ++ set-subtract ys zs
++-distribute-subtract []       ys zs = refl
++-distribute-subtract (x ∷ xs) ys zs with any (_≟_ x) zs
... | yes x∈zs = ++-distribute-subtract xs ys zs
... | no  x∉zs = cong (x ∷_) (++-distribute-subtract xs ys zs)

subtract-⊆¹ : ∀ xs ys → set-subtract xs ys ⊆¹ xs
subtract-⊆¹ []       ys = ⊆¹-refl
subtract-⊆¹ (x ∷ xs) ys with any (_≟_ x) ys
... | yes x∈ys = λ   w w∈xs-ys         → ++ʳ [ x ] (subtract-⊆¹ xs ys w w∈xs-ys)
... | no  x∉ys = λ { w (here refl)     → here refl
                   ; w (there w∈xs-ys) → there (subtract-⊆¹ xs ys w w∈xs-ys) }

R-maintain-raise-shared-0 : ∀{xs θ e} → ∀ s e' →
  (ShrMap.keys (ShrMap.[ s ↦ SharedVar.old ,′ δ {θ} {e} e' ]) ++ xs)
  ⊆¹ (SharedVar.unwrap s ∷ xs)
R-maintain-raise-shared-0 s e' s' s'∈[s]++BV
  rewrite ShrMap.keys-1map s (SharedVar.old ,′ δ e')
  = s'∈[s]++BV

R-maintain-raise-shared-1 : ∀ ys {θ e} → ∀ s e' →
  set-subtract ys (ShrMap.keys ShrMap.[ s ↦ SharedVar.old ,′ δ {θ} {e} e' ])
  ⊆¹ set-subtract ys (SharedVar.unwrap s ∷ [])
R-maintain-raise-shared-1 ys s e' s' s'∈ys-[s]
  rewrite ShrMap.keys-1map s (SharedVar.old ,′ δ e')
  = s'∈ys-[s]

R-maintain-raise-sig-0 : ∀{xs} → ∀ S →
  (SigMap.keys (SigMap.[ S ↦ Signal.unknown ]) ++ xs)
  ⊆¹ (Signal.unwrap S ∷ xs)
R-maintain-raise-sig-0 S S' S'∈[S]++BV
  rewrite SigMap.keys-1map S Signal.unknown
  = S'∈[S]++BV

R-maintain-raise-sig-1 : ∀ ys → ∀ S →
  set-subtract ys (SigMap.keys SigMap.[ S ↦ Signal.unknown ])
  ⊆¹ set-subtract ys (Signal.unwrap S ∷ [])
R-maintain-raise-sig-1 ys S S' S'∈ys-[S]
  rewrite SigMap.keys-1map S Signal.unknown
  = S'∈ys-[S]

R-maintain-lift-1 : ∀ S xs ys {zs} →
  set-subtract xs ys ⊆¹ zs → set-subtract (S ∷ xs) ys ⊆¹ (S ∷ zs)
R-maintain-lift-1 S xs ys xs-ys⊆zs S' S'∈⟨S∷xs⟩-ys with any (_≟_ S) ys
R-maintain-lift-1 S xs ys xs-ys⊆zs S' (here refl)      | no  _ =
  here refl
R-maintain-lift-1 S xs ys xs-ys⊆zs S' (there S'∈xs-ys) | no  _ =
  there (xs-ys⊆zs S' S'∈xs-ys)
...                                                    | yes _ =
  there (xs-ys⊆zs S' S'∈⟨S∷xs⟩-ys)

R-maintain-lift-2' : ∀ {zs ws} xs ys →
  set-subtract xs ys ⊆¹ zs →
  set-subtract (xs ++ ws) ys ⊆¹ (zs ++ ws)
R-maintain-lift-2' {zs} {ws} xs ys xs-ys⊆zs
  rewrite ++-distribute-subtract xs ws ys =
  ∪¹-join-⊆¹ (λ u → ++ˡ ∘ xs-ys⊆zs u)
  (⊆¹-trans (subtract-⊆¹ ws ys) (λ u → ++ʳ zs ∘ ⊆¹-refl u))

R-maintain-lift-6' : ∀ {zs} ws xs ys →
  set-subtract xs ys ⊆¹ zs →
  set-subtract (ws ++ xs) ys ⊆¹ (ws ++ zs)
R-maintain-lift-6' {zs} ws xs ys xs-ys⊆zs
  rewrite ++-distribute-subtract ws xs ys =
  ∪¹-join-⊆¹ (⊆¹-trans (subtract-⊆¹ ws ys) (λ u → ++ˡ ∘ ⊆¹-refl u))
  (λ u → ++ʳ ws ∘ xs-ys⊆zs u)

R-maintain-lift-2 : ∀ {zs³ ws³} xs³ ys³ →
  (xs³ - ys³) ⊆ zs³ →
  ((xs³ ∪ ws³) - ys³) ⊆ (zs³ ∪ ws³)
R-maintain-lift-2 xs³ ys³ xs³-ys³⊆zs³ =
  R-maintain-lift-2' ,′ R-maintain-lift-2' ,′ R-maintain-lift-2' #
    xs³ # ys³ # xs³-ys³⊆zs³

R-maintain-lift-6 : ∀ {zs³} ws³ xs³ ys³ →
  (xs³ - ys³) ⊆ zs³ →
  ((ws³ ∪ xs³) - ys³) ⊆ (ws³ ∪ zs³)
R-maintain-lift-6 ws³ xs³ ys³ xs³-ys³⊆zs³ =
  R-maintain-lift-6' ,′ R-maintain-lift-6' ,′ R-maintain-lift-6' #
    ws³ # xs³ # ys³ # xs³-ys³⊆zs³

R-maintain-lift-3' : ∀ {ys zs ws} xs →
  (xs ++ ys) ⊆¹ zs →
  distinct' zs ws →
  distinct' ys ws
R-maintain-lift-3' xs xs++ys⊆zs zs≠ws x x∈ys x∈ws =
  zs≠ws x (xs++ys⊆zs x (++ʳ xs x∈ys)) x∈ws

R-maintain-lift-3 : ∀ {ys³ zs³ ws³} xs³ →
  (xs³ ∪ ys³) ⊆ zs³ →
  distinct zs³ ws³ →
  distinct ys³ ws³
R-maintain-lift-3 xs³ xs³∪ys³⊆zs³ zs³≠ws³ =
  R-maintain-lift-3' ,′ R-maintain-lift-3' ,′ R-maintain-lift-3' #
    xs³ # xs³∪ys³⊆zs³ # zs³≠ws³

R-maintain-lift-4' : ∀ {xs ws us vs zs} ys →
  set-subtract xs ys ⊆¹ us → distinct' us zs →
  (ys ++ ws) ⊆¹ vs →         distinct' vs zs →
  distinct' xs zs
R-maintain-lift-4' {.a ∷ xs} ys xs-ys⊆us us≠zs ys++ws⊆vs vs≠zs
                   a (here refl) a∈zs with any (_≟_ a) ys
... | yes a∈ys = vs≠zs a (ys++ws⊆vs a (++ˡ a∈ys)) a∈zs
... | no  a∉ys = us≠zs a (xs-ys⊆us a (here refl)) a∈zs
R-maintain-lift-4' {x ∷ xs} ys xs-ys⊆us us≠zs ys++ws⊆vs vs≠zs
                   a (there a∈xs) a∈zs with any (_≟_ x) ys
... | yes x∈ys = R-maintain-lift-4' ys xs-ys⊆us us≠zs ys++ws⊆vs vs≠zs a a∈xs a∈zs
... | no  x∉ys = R-maintain-lift-4' ys (proj₂ (∪¹-unjoin-⊆¹ [ x ] xs-ys⊆us))
                                       us≠zs ys++ws⊆vs vs≠zs a a∈xs a∈zs

R-maintain-lift-4 : ∀ {ws³ us³ vs³ xs³ zs³} ys³ →
  (xs³ - ys³) ⊆ us³ → distinct us³ zs³ →
  (ys³ ∪ ws³) ⊆ vs³ → distinct vs³ zs³ →
  distinct xs³ zs³
R-maintain-lift-4 ys³ xs³-ys³⊆us³ us³≠zs³ ys³∪ws³⊆vs³ vs³≠zs³ =
  R-maintain-lift-4' ,′ R-maintain-lift-4' ,′ R-maintain-lift-4' #
    ys³ # xs³-ys³⊆us³ # us³≠zs³ # ys³∪ws³⊆vs³ # vs³≠zs³

R-maintain-lift-5 : ∀ xs³ ys³ {zs³ ws³} →
  (ys³ ∪ zs³) ⊆ ws³ →
  (ys³ ∪ (xs³ ∪ zs³)) ⊆ (xs³ ∪ ws³)
R-maintain-lift-5 xs³ ys³ ys³∪zs³⊆ws³ with ∪-unjoin-⊆ ys³ ys³∪zs³⊆ws³
... | ys³⊆ws³ , zs³⊆ws³ = ∪-join-⊆ (∪ʳ xs³ ys³⊆ws³) (∪-respect-⊆-right xs³ zs³⊆ws³)

R-maintain-lift-0 : ∀{p θ q BVp FVp E A} →
  CorrectBinding p BVp FVp →
  p ≐ E  ⟦ ρ⟨ θ , A ⟩· q ⟧e →
  Σ (VarList × VarList)
    λ { (BV' , FV') →
      (BV' ⊆ BVp × FV' ⊆ FVp) ×
      CorrectBinding (ρ⟨ θ , A ⟩· E ⟦ q ⟧e) BV' FV' }
R-maintain-lift-0 cbp dehole = _ , (⊆-refl , ⊆-refl) , cbp
R-maintain-lift-0 (CBpar {BVq = BVq'} {FVq = FVq'} cbp' cbq'
                         BVp'≠BVq' FVp'≠BVq' BVp'≠FVq' Xp'≠Xq')
                  (depar₁ p'≐E⟦ρθ⟧)
  with R-maintain-lift-0 cbp' p'≐E⟦ρθ⟧
... | (BV' , FV') , (BV'⊆BVp' , FV'⊆FVp') ,
      CBρ {θ} {_} {_} {BVp''} {FVp''} cbp'' =
  _ ,
  (⊆-subst-left (∪-assoc (Dom θ) BVp'' BVq') (∪-respect-⊆-left BV'⊆BVp') ,′
   R-maintain-lift-2 FVp'' (Dom θ) FV'⊆FVp') ,′
  CBρ (CBpar cbp'' cbq'
             (R-maintain-lift-3 (Dom θ) BV'⊆BVp' BVp'≠BVq')
             (R-maintain-lift-4 (Dom θ) FV'⊆FVp' FVp'≠BVq' BV'⊆BVp' BVp'≠BVq')
             (R-maintain-lift-3 (Dom θ) BV'⊆BVp' BVp'≠FVq')
             (R-maintain-lift-4' (proj₂ (proj₂ (Dom θ))) (proj₂ (proj₂ FV'⊆FVp'))
                                 Xp'≠Xq' (proj₂ (proj₂ BV'⊆BVp')) (proj₂ (proj₂ BVp'≠FVq'))))
R-maintain-lift-0 (CBpar {BVp = BVp'} {FVp = FVp'} cbp' cbq'
                         BVp'≠BVq' FVp'≠BVq' BVp'≠FVq' Xp'≠Xq')
                  (depar₂ q'≐E⟦ρθ⟧)
  with R-maintain-lift-0 cbq' q'≐E⟦ρθ⟧
... | (BV' , FV') , (BV'⊆BVq' , FV'⊆FVq') ,
      CBρ {θ} {_} {_} {BVq''} {FVq''} cbq'' =
  _ ,
  (R-maintain-lift-5 BVp' (Dom θ) BV'⊆BVq' ,′
   R-maintain-lift-6 FVp' FVq'' (Dom θ) FV'⊆FVq') ,′
  CBρ (CBpar cbp' cbq''
             (distinct-sym (R-maintain-lift-3 (Dom θ) BV'⊆BVq' (distinct-sym BVp'≠BVq')))
             (distinct-sym (R-maintain-lift-3 (Dom θ) BV'⊆BVq' (distinct-sym FVp'≠BVq')))
             (distinct-sym (R-maintain-lift-4 (Dom θ)
                                              FV'⊆FVq' (distinct-sym BVp'≠FVq')
                                              BV'⊆BVq' (distinct-sym BVp'≠BVq')))
             (distinct'-sym
              (R-maintain-lift-4' (proj₂ (proj₂ (Dom θ))) (proj₂ (proj₂ FV'⊆FVq'))
                                  (distinct'-sym Xp'≠Xq') (proj₂ (proj₂ BV'⊆BVq'))
                                  (distinct'-sym (proj₂ (proj₂ FVp'≠BVq'))))))
R-maintain-lift-0 (CBseq cbp' cbq' BV≠FV) (deseq p'≐E⟦ρθ⟧)
  with R-maintain-lift-0 cbp' p'≐E⟦ρθ⟧
... | (BV' , FV') , (BV'⊆BVp' , FV'⊆FVp') ,
      CBρ {θ} {_} {_} {BVp''} {FVp''} cbp'' =
  _ ,
  (∪-join-⊆
    (∪ˡ (∪-unjoin-⊆ˡ {Dom θ} BV'⊆BVp'))
    (∪-respect-⊆-left (∪-unjoin-⊆ʳ (Dom θ) BV'⊆BVp')) ,′
   R-maintain-lift-2 FVp'' (Dom θ) FV'⊆FVp') ,′
  CBρ (CBseq cbp'' cbq'
             (⊆-respect-distinct-left (∪-unjoin-⊆ʳ (Dom θ) BV'⊆BVp') BV≠FV))
R-maintain-lift-0 (CBloopˢ cbp' cbq' BVp'≠FVq' BVq'≠FVq') (deloopˢ p'≐E⟦ρθ⟧)
  with R-maintain-lift-0 cbp' p'≐E⟦ρθ⟧
... | (BV' , FV') , (BV'⊆BVp' , FV'⊆FVp') ,
      CBρ {θ} {_} {_} {BVp''} {FVp''} cbp'' =
  _ ,
  (∪-join-⊆
    (∪ˡ (∪-unjoin-⊆ˡ {Dom θ} BV'⊆BVp'))
    (∪-respect-⊆-left (∪-unjoin-⊆ʳ (Dom θ) BV'⊆BVp')) ,′
   R-maintain-lift-2 FVp'' (Dom θ) FV'⊆FVp') ,′
  CBρ (CBloopˢ cbp'' cbq'
               (⊆-respect-distinct-left (∪-unjoin-⊆ʳ (Dom θ) BV'⊆BVp') BVp'≠FVq') BVq'≠FVq')
R-maintain-lift-0 (CBsusp {S = S} cbp' S∉BV) (desuspend p'≐E⟦ρθ⟧)
  with R-maintain-lift-0 cbp' p'≐E⟦ρθ⟧
... | (BV' , FV') , (BV'⊆BVp' , FV'⊆FVp') ,
      CBρ {θ} {_} {_} {BVp''} {FVp''} cbp'' =
  _ ,
  (BV'⊆BVp' ,′
   (R-maintain-lift-1 (Signal.unwrap S) (proj₁ FVp'') (proj₁ (Dom θ)) (proj₁ FV'⊆FVp') ,′
    proj₁ (proj₂ FV'⊆FVp') ,′
    proj₂ (proj₂ FV'⊆FVp'))) ,′
  CBρ (CBsusp cbp''
              (λ S' S'∈[S] S'∈BV →
                 S∉BV S' S'∈[S] (proj₁ BV'⊆BVp' S' (++ʳ (proj₁ (Dom θ)) S'∈BV))))
R-maintain-lift-0 (CBtrap cbp') (detrap p'≐E⟦ρθ⟧)
  with R-maintain-lift-0 cbp' p'≐E⟦ρθ⟧
... | (BV' , FV') , ⟨BV'⊆BVp'⟩×⟨FV'⊆FVp'⟩ , CBρ cbp'' =
  _ , ⟨BV'⊆BVp'⟩×⟨FV'⊆FVp'⟩ ,′ CBρ (CBtrap cbp'')

R-maintain-raise-var-0 : ∀{xs θ e} → ∀ x e' →
  (VarMap.keys (VarMap.[ x ↦ δ {θ} {e} e' ]) ++ xs)
  ⊆¹ (SeqVar.unwrap x ∷ xs)
R-maintain-raise-var-0 x e' x' x'∈[x]++BV
  rewrite VarMap.keys-1map x (δ e')
  = x'∈[x]++BV

R-maintain-raise-var-1 : ∀ ys {θ e} → ∀ x e' →
  set-subtract ys (VarMap.keys VarMap.[ x ↦ δ {θ} {e} e' ])
  ⊆¹ set-subtract ys (SeqVar.unwrap x ∷ [])
R-maintain-raise-var-1 ys x e' x' x'∈ys-[x]
  rewrite VarMap.keys-1map x (δ e')
  = x'∈ys-[x]

R-maintains-binding : ∀{p q BV FV} → CorrectBinding p BV FV → p sn⟶₁ q → Σ (VarList × VarList) λ { (BV' , FV') → CorrectBinding q BV' FV' × BV' ⊆ BV × FV' ⊆ FV}
R-maintains-binding (CBpar{BVp = BVp}{FVp = FVp} cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-right hnothin (dhalted q')) = _ , cbq , ∪ʳ BVp ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁)) , ∪ʳ FVp ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-right (hexit _) (dhalted hnothin))
  = _ , CBexit , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ()))) , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-right (hexit _) (dhalted (hexit _))) = _ , CBexit , (((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))) , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))
R-maintains-binding (CBpar{BVp = BVp}{FVp = FVp} cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-right hnothin (dpaused q')) = _ , cbq , ∪ʳ BVp ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁)) , ∪ʳ FVp ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-right (hexit _) (dpaused q')) = _ , CBexit , (((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))) , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))
R-maintains-binding (CBpar{BVp = BVp}{FVp = FVp} cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-left (dhalted hnothin) q') = _ , cbq , ∪ʳ BVp ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁)) , ∪ʳ FVp ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-left (dhalted (hexit _)) hnothin) = _ , CBexit , (((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))) , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-left (dhalted (hexit _)) (hexit _)) = _ , CBexit , (((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))) , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-left (dpaused p') hnothin) = _ , cbp , ∪ˡ ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁)), ∪ˡ ((λ x x₁ → x₁) , (λ x x₁ → x₁) , (λ x x₁ → x₁))
R-maintains-binding (CBpar cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (rpar-done-left (dpaused p') (hexit _)) = _ , CBexit , (((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))) , ((λ x → λ ()) , ((λ x → λ ()) , (λ x → λ ())))
R-maintains-binding {(ρ⟨ θ , A ⟩· p)} (CBρ cb) red@(ris-present S∈ θS≡present p≐E⟦presentS⟧)
  with binding-extract cb p≐E⟦presentS⟧
... | _ , _ , cbpresent@(CBpresent {S = S} cbp' cbq')
  with binding-subst cb p≐E⟦presentS⟧
                     cbpresent (∪ˡ ⊆-refl) (∪ʳ (+S S base) (∪ˡ ⊆-refl))
                     cbp'
... | _ , (a , b) , cb' = _ , CBρ cb' , ∪-respect-⊆-right (Dom θ) a , ⊆-respect-|̌ (Dom θ) b
R-maintains-binding {(ρ⟨ θ , A ⟩· p)} (CBρ cb) red@(ris-absent S∈ θS≡absent p≐E⟦presentS⟧)
  with binding-extract cb p≐E⟦presentS⟧
... | _ , _ , cbpresent@(CBpresent {S = S} {BVp = BVp'} {FVp = FVp'} cbp' cbq')
  with binding-subst cb p≐E⟦presentS⟧
                     cbpresent (∪ʳ BVp' ⊆-refl) (∪ʳ (+S S base) (∪ʳ FVp' ⊆-refl))
                     cbq'
... | _ , (a , b) , cb' = _ , CBρ cb' , ∪-respect-⊆-right (Dom θ) a , ⊆-respect-|̌ (Dom θ) b
R-maintains-binding {(ρ⟨ θ , A ⟩· p)} (CBρ cb) (remit{S = S} S∈ θS≢absent p≐E⟦emitS⟧)
  with binding-extract cb p≐E⟦emitS⟧
... | _ , _ , cbemit
  with binding-subst cb p≐E⟦emitS⟧
                     cbemit ⊆-empty-left ⊆-empty-left
                     CBnothing
... | _ , (a , b) , cbp'
      rewrite cong fst (sig-set-dom-eq S Signal.present  θ S∈)
   = _ , CBρ cbp' , ∪-respect-⊆-right (Dom θ') a , ⊆-respect-|̌ (Dom θ') b
     where θ' = (set-sig{S} θ S∈ Signal.present)
R-maintains-binding {(loop p)} {FV = FV2} (CBloop {BV = BV}{FV = FV} cb BV≠FV) rloop-unroll =
   _ , (CBloopˢ cb cb BV≠FV BV≠FV) , (sub BV , sub FV)
   where
     sub1 : ∀ x → (x ++ x) ⊆¹ x
     sub1 x z y with ++⁻ x y
     ... | inj₁ a = a
     ... | inj₂ a = a
     sub : ∀ x → (x ∪ x) ⊆ x
     sub x = sub1 , sub1 , sub1 # x
R-maintains-binding (CBseq{BVp = BVp}{FVp = FVp} cbp cbq BV≠FV) rseq-done = _ , cbq , ∪ʳ BVp ⊆-refl , ∪ʳ FVp ⊆-refl
R-maintains-binding (CBseq cbp cbq BV≠FV) rseq-exit = _ , CBexit , ⊆-empty-left , ⊆-empty-left
R-maintains-binding (CBloopˢ cbp cbq BV≠FV _) rloopˢ-exit = _ , CBexit , ⊆-empty-left , ⊆-empty-left
R-maintains-binding (CBsusp cb _) (rsuspend-done _) = _ , cb , ⊆-refl , ((λ x x₁ → there x₁) , (λ x z → z) , (λ x z → z))
R-maintains-binding (CBtrap cb) (rtrap-done hnothin) = _ , CBnothing ,  ⊆-empty-left ,  ⊆-empty-left
R-maintains-binding (CBtrap cb) (rtrap-done (hexit zero)) = _ , CBnothing ,  ⊆-empty-left ,  ⊆-empty-left
R-maintains-binding (CBtrap cb) (rtrap-done (hexit (suc n))) = _ , CBexit , ⊆-empty-left ,  ⊆-empty-left
R-maintains-binding (CBsig{S = S}{FV = FV} cb) rraise-signal
   = _ , CBρ cb
       , ( (R-maintain-raise-sig-0 S) ,′ ⊆¹-refl ,′ ⊆¹-refl)
       , ((R-maintain-raise-sig-1 (fst FV) S) ,′ ⊆¹-refl ,′ ⊆¹-refl)
R-maintains-binding (CBρ{θ = θ} cb) (rraise-shared {s = s} {e} e' p≐E⟦shared⟧)
  with binding-extract cb p≐E⟦shared⟧
... | _ , _ , cbshr@(CBshared {FV = FV} cbp)
  with binding-subst cb p≐E⟦shared⟧
                     cbshr (⊆¹-refl ,′ -- S'∈BVp
                            R-maintain-raise-shared-0 s e' ,′
                            ⊆¹-refl)   -- x'∈BVp
                           (∪ʳ (FVₑ e)
                               (⊆¹-refl ,′  -- S'∈FVe+⟨FVp-s⟩
                                R-maintain-raise-shared-1 (proj₁ (proj₂ FV)) s e' ,′
                                ⊆¹-refl))   -- x'∈FVe+⟨FVp-s⟩
                     (CBρ cbp)
... | _ , (a , b) , cbp' = _ , CBρ cbp' ,  ∪-respect-⊆-right (Dom θ) a ,  ⊆-respect-|̌ (Dom θ) b
R-maintains-binding (CBρ{θ = θ} cb) (rset-shared-value-old{s = s} e' s∈ θs≡old p≐E⟦s⇐e⟧)
  with binding-extract cb p≐E⟦s⇐e⟧
... | _ , _ , cbshrset
  with binding-subst cb p≐E⟦s⇐e⟧
                     cbshrset ⊆-empty-left ⊆-empty-left
                     CBnothing
... | _ , (a , b) , cb'
      rewrite cong snd (shr-set-dom-eq s SharedVar.new (δ e') θ s∈)
     = _ , CBρ cb' , ∪-respect-⊆-right (Dom (set-shr{s = s} θ s∈ SharedVar.new (δ e'))) a ,  ⊆-respect-|̌ (Dom (set-shr{s = s} θ s∈ SharedVar.new (δ e'))) b
R-maintains-binding (CBρ{θ = θ} cb) (rset-shared-value-new{s = s} e' s∈ θs≡new p≐E⟦s⇐e⟧)
  with binding-extract cb p≐E⟦s⇐e⟧
... | _ , _ , cbshrset
  with binding-subst cb p≐E⟦s⇐e⟧
                     cbshrset ⊆-empty-left ⊆-empty-left
                     CBnothing
... | _ , (a , b) , cb'
      rewrite cong snd (shr-set-dom-eq s SharedVar.new ((shr-vals{s} θ s∈) + (δ e')) θ s∈)
     = _ , CBρ cb' , ( ∪-respect-⊆-right (Dom (set-shr{s = s} θ s∈ SharedVar.new _)) a) , ⊆-respect-|̌ (Dom (set-shr{s = s} θ s∈ SharedVar.new _)) b
R-maintains-binding (CBρ{θ = θ} cb) (rraise-var {x = x} {e = e} e' p≐E⟦var⟧)
  with binding-extract cb p≐E⟦var⟧
... | _ , _ , cbvar@(CBvar {FV = FV} cbp)
  with binding-subst cb p≐E⟦var⟧
                     cbvar (⊆¹-refl ,′
                            ⊆¹-refl ,′
                            R-maintain-raise-var-0 x e')
                           (∪ʳ (FVₑ e)
                               (⊆¹-refl ,′
                                ⊆¹-refl ,′
                                R-maintain-raise-var-1 (proj₂ (proj₂ FV)) x e'))
                     (CBρ cbp)
... | _ , (a , b) , cb' = _ , CBρ cb' , ( ∪-respect-⊆-right (Dom θ) a) , ⊆-respect-|̌ (Dom θ) b
R-maintains-binding (CBρ{θ = θ} cb) (rset-var{x = x} x∈ e' p≐E⟦x≔e⟧)
  with binding-extract cb p≐E⟦x≔e⟧
... | _ , _ , cbvarset
  with binding-subst cb p≐E⟦x≔e⟧
                     cbvarset ⊆-empty-left ⊆-empty-left
                     CBnothing
... | _ , (a , b) , cb'
    rewrite cong thd (seq-set-dom-eq x (δ e') θ x∈)
   = _ , CBρ cb' ,  ∪-respect-⊆-right (Dom (set-var{x} θ x∈ (δ e'))) a , ⊆-respect-|̌ (Dom (set-var{x} θ x∈ (δ e'))) b
R-maintains-binding (CBρ{θ = θ} cb) (rif-false x∈ θx≡zero p≐E⟦if⟧)
  with binding-extract cb p≐E⟦if⟧
... | _ , _ , cbif@(CBif {x = x} {BVp = BVp} {FVp = FVp} cbp cbq)
  with binding-subst cb p≐E⟦if⟧
                     cbif (∪ʳ BVp ⊆-refl) (∪ʳ (+x x base) (∪ʳ FVp ⊆-refl))
                     cbq
... | _ , (a , b) , cb' = _ , CBρ cb' , ( ∪-respect-⊆-right (Dom θ) a) , ( ⊆-respect-|̌ (Dom θ) b)
R-maintains-binding (CBρ{θ = θ} cb) (rif-true x∈ θx≡suc p≐E⟦if⟧)
  with binding-extract cb p≐E⟦if⟧
... | _ , _ , cbif@(CBif {x = x} cbp cbq)
  with binding-subst cb p≐E⟦if⟧
                     cbif (∪ˡ ⊆-refl) (∪ʳ (+x x base) (∪ˡ ⊆-refl))
                     cbp
... | _ , (a , b) , cb' = _ , CBρ cb' , ∪-respect-⊆-right (Dom θ) a , ( ⊆-respect-|̌ (Dom θ) b)
R-maintains-binding (CBρ{θ = θ} cb) (rabsence{S = S} S∈ θS≡unknown S∉canₛ) rewrite cong fst (sig-set-dom-eq S Signal.absent θ S∈) = _ , CBρ cb , ⊆-refl , ⊆-refl
R-maintains-binding (CBρ{θ = θ} cb) (rreadyness{s = s} s∈ θs≡old⊎θs≡new s∉canₛₕ)  rewrite cong snd (shr-set-dom-eq s SharedVar.ready (shr-vals{s} θ s∈) θ s∈) = _ , CBρ cb , ⊆-refl , ⊆-refl
R-maintains-binding (CBρ{θ = θo}{BV = BVo}{FV = FVo} cb) (rmerge{θ₂ = θi} p≐E⟦ρθ⟧) with R-maintain-lift-0 cb p≐E⟦ρθ⟧
... | _ , (a , b) , cb'@(CBρ{BV = BVi}{FV = FVi} cbp'')
        = _ , CBρ cbp'' ,
         bvsub ,
         fvsub
     where
     fvsubS : (set-subtract (fst FVi) (fst (Dom (θo ← θi)))) ⊆¹ (set-subtract (fst FVo) (fst (Dom θo)))
     fvsubS x x∈FVi\Dom⟨θo←θi⟩ with set-subtract-merge{fst FVi}{(fst (Dom (θo ← θi)))}{x} x∈FVi\Dom⟨θo←θi⟩
     ... | (x∈FVi , x∉Dom⟨θo←θi⟩) = set-subtract-notin ((fst b) x (set-subtract-notin x∈FVi x∉Dom⟨θi⟩)) x∉Dom⟨θo⟩
       where
          x∉Dom⟨θo⟩ : x ∉ fst (Dom θo)
          x∉Dom⟨θo⟩ x∈Dom⟨θo⟩ = x∉Dom⟨θo←θi⟩ (sig-←-monoˡ (x ₛ) θo θi x∈Dom⟨θo⟩)

          x∉Dom⟨θi⟩ : x ∉ fst (Dom θi)
          x∉Dom⟨θi⟩ x∈Dom⟨θi⟩ = x∉Dom⟨θo←θi⟩ (sig-←-monoʳ (x ₛ) θi θo x∈Dom⟨θi⟩)

     fvsubs : (set-subtract (snd FVi) (snd (Dom (θo ← θi)))) ⊆¹ (set-subtract (snd FVo) (snd (Dom θo)))
     fvsubs x x∈FVi\Dom⟨θo←θi⟩ with set-subtract-merge{snd FVi}{(snd (Dom (θo ← θi)))}{x} x∈FVi\Dom⟨θo←θi⟩
     ... | (x∈FVi , x∉Dom⟨θo←θi⟩) = set-subtract-notin ((snd b) x (set-subtract-notin x∈FVi x∉Dom⟨θi⟩)) x∉Dom⟨θo⟩
       where
          x∉Dom⟨θo⟩ : x ∉ snd (Dom θo)
          x∉Dom⟨θo⟩ x∈Dom⟨θo⟩ = x∉Dom⟨θo←θi⟩ (shr-←-monoˡ (x ₛₕ) θo θi x∈Dom⟨θo⟩)

          x∉Dom⟨θi⟩ : x ∉ snd (Dom θi)
          x∉Dom⟨θi⟩ x∈Dom⟨θi⟩ = x∉Dom⟨θo←θi⟩ (shr-←-monoʳ (x ₛₕ) θi θo x∈Dom⟨θi⟩)

     fvsubx : (set-subtract (thd FVi) (thd (Dom (θo ← θi)))) ⊆¹ (set-subtract (thd FVo) (thd (Dom θo)))
     fvsubx x x∈FVi\Dom⟨θo←θi⟩ with set-subtract-merge{thd FVi}{(thd (Dom (θo ← θi)))}{x} x∈FVi\Dom⟨θo←θi⟩
     ... | (x∈FVi , x∉Dom⟨θo←θi⟩) = set-subtract-notin ((thd b) x (set-subtract-notin x∈FVi x∉Dom⟨θi⟩)) x∉Dom⟨θo⟩
       where
          x∉Dom⟨θo⟩ : x ∉ thd (Dom θo)
          x∉Dom⟨θo⟩ x∈Dom⟨θo⟩ = x∉Dom⟨θo←θi⟩ (seq-←-monoˡ (x ᵥ) θo θi x∈Dom⟨θo⟩)

          x∉Dom⟨θi⟩ : x ∉ thd (Dom θi)
          x∉Dom⟨θi⟩ x∈Dom⟨θi⟩ = x∉Dom⟨θo←θi⟩ (seq-←-monoʳ (x ᵥ) θi θo x∈Dom⟨θi⟩)

     fvsub : (FVi - (Dom (θo ← θi))) ⊆ (FVo - (Dom θo))
     fvsub = fvsubS , fvsubs , fvsubx
     bvsubS : ((fst (Dom (θo ← θi))) ++ (fst BVi)) ⊆¹ ((fst (Dom θo)) ++ (fst BVo))
     bvsubS x y with ++⁻ (fst (Dom (θo ← θi))) y
     ... | inj₂ x∈BVi = ++ʳ (fst $ Dom θo) ((fst a) x (++ʳ (fst $ Dom θi) x∈BVi))
     ... | inj₁ x∈⟨θo←θi⟩ with sig-←⁻{θo}{θi} (x ₛ) x∈⟨θo←θi⟩
     ... | inj₁ x∈θo = ++ˡ x∈θo
     ... | inj₂ x∈θi = ++ʳ (fst $ Dom θo) ((fst a) x (++ˡ x∈θi))

     bvsubs : ((snd (Dom (θo ← θi))) ++ (snd BVi)) ⊆¹ ((snd (Dom θo)) ++ (snd BVo))
     bvsubs x y with ++⁻ (snd (Dom (θo ← θi))) y
     ... | inj₂ x∈BVi = ++ʳ (snd $ Dom θo) ((snd a) x (++ʳ (snd $ Dom θi) x∈BVi))
     ... | inj₁ x∈⟨θo←θi⟩ with shr-←⁻{θo}{θi} (x ₛₕ) x∈⟨θo←θi⟩
     ... | inj₁ x∈θo = ++ˡ x∈θo
     ... | inj₂ x∈θi = ++ʳ (snd $ Dom θo) ((snd a) x (++ˡ x∈θi))

     bvsubx : ((thd (Dom (θo ← θi))) ++ (thd BVi)) ⊆¹ ((thd (Dom θo)) ++ (thd BVo))
     bvsubx x y with ++⁻ (thd (Dom (θo ← θi))) y
     ... | inj₂ x∈BVi = ++ʳ (thd $ Dom θo) ((thd a) x (++ʳ (thd $ Dom θi) x∈BVi))
     ... | inj₁ x∈⟨θo←θi⟩ with seq-←⁻{θo}{θi} (x ᵥ) x∈⟨θo←θi⟩
     ... | inj₁ x∈θo = ++ˡ x∈θo
     ... | inj₂ x∈θi = ++ʳ (thd $ Dom θo) ((thd a) x (++ˡ x∈θi))

     bvsub : ((Dom (θo ← θi)) ∪ BVi) ⊆ ((Dom θo) ∪ BVo)
     bvsub = bvsubS , bvsubs , bvsubx

-- R-maintains-binding : ∀{p q BV FV} → CorrectBinding p BV FV → p sn⟶₁ q → Σ (VarList × VarList) λ { (BV' , FV') → CorrectBinding q BV' FV' }
sn⟶-maintains-binding : ∀ {p BV FV q} → CorrectBinding p BV FV → p sn⟶ q → Σ (VarList × VarList) λ {(BVq , FVq) → CorrectBinding q BVq FVq × BVq ⊆ BV × FVq ⊆ FV }
sn⟶-maintains-binding CBp (rcontext C dc p₁sn⟶₁q₁)
  with binding-extractc' CBp dc
... | (BVp₁ , FVp₁) , CBp₁
  with R-maintains-binding CBp₁ p₁sn⟶₁q₁
... | (BVq₁ , FVq₁) , (CBq₁ , BVq₁⊆BVp₁ , FVq₁⊆FVp₁)
  with binding-substc' CBp dc CBp₁ BVq₁⊆BVp₁ FVq₁⊆FVp₁ CBq₁
... | (BVq , FVq) , ((BVq⊆BVp , FVq⊆FVp), CBq) =
  (BVq , FVq) , (CBq , BVq⊆BVp , FVq⊆FVp)

sn⟶*-maintains-binding : ∀ {p BV FV q} → CorrectBinding p BV FV → p sn⟶* q → Σ (VarList × VarList) λ {(BVq , FVq) → CorrectBinding q BVq FVq}

sn⟶*-maintains-binding cb rrefl = _ , cb
sn⟶*-maintains-binding cb (rstep x psn⟶*q)
  = sn⟶*-maintains-binding (proj₁ (proj₂ (sn⟶-maintains-binding cb x))) psn⟶*q

CB-preservation :  ∀ p q C → CB (C ⟦ p ⟧c) → p sn⟶₁ q → CB (C ⟦ q ⟧c)
CB-preservation p q C CBp psn⟶₁q with
  sn⟶-maintains-binding{p = C ⟦ p ⟧c}{q = C ⟦ q ⟧c} CBp (rcontext C Crefl psn⟶₁q)
... | (BV , FV) , CBq , _ with BVFVcorrect (C ⟦ q ⟧c) BV FV CBq
... | refl , refl = CBq

CB-preservation* :  ∀ p q → CB p → p sn⟶* q → CB q
CB-preservation* p q CBp psn⟶*q with
  sn⟶*-maintains-binding CBp psn⟶*q
... | (BV , FV) , CBq with BVFVcorrect q BV FV CBq
... | refl , refl = CBq

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module sn-calculus-confluence.rec where

open import Data.Nat using (_+_)
open import Function using (_∋_ ; _∘_)
open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc )
open import utility
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import sn-calculus
open import context-properties
open import Esterel.Lang.Binding
open import Data.Maybe using ( just )
open import Data.List.Any
open import Data.List.Any.Properties

open import Data.FiniteMap
import Data.OrderedListMap as OMap
open import Data.Nat as Nat using (ℕ)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar

open import sn-calculus-confluence.helper
open import sn-calculus-confluence.recrec

ρ-conf-rec : ∀{θ El Er ql qr i oli ori qro qlo FV BV θl θr A Al Ar}
             → CorrectBinding (ρ⟨ θ , A ⟩· i) FV BV
             → (ieql : i ≐ El ⟦ ql ⟧e)
             → (ieqr : i ≐ Er ⟦ qr ⟧e)
             → El a~ Er
             → (rl : (ρ⟨ θ , A ⟩· i) sn⟶₁ (ρ⟨ θl , Al ⟩· oli))
             → (rr : (ρ⟨ θ , A ⟩· i) sn⟶₁ (ρ⟨ θr , Ar ⟩· ori))
             → (olieq : oli ≐ El ⟦ qlo ⟧e)
             → (orieq : ori ≐ Er ⟦ qro ⟧e)
             → (->E-view rl ieql olieq)
             → (->E-view rr ieqr orieq)
             → (
             Σ[ θo ∈ Env ]
             Σ[ Ao ∈ Ctrl ]
             Σ[ si ∈ Term ]
             Σ[ Elo ∈ EvaluationContext ]
             Σ[ Ero ∈ EvaluationContext ]
             Σ[ oorieq ∈ ori ≐ Elo ⟦ ql ⟧e ]
             Σ[ oolieq ∈ oli ≐ Ero ⟦ qr ⟧e ]
             Σ[ sireq ∈ (si ≐ Elo ⟦ qlo ⟧e ) ]
             Σ[ sileq ∈ (si ≐ Ero ⟦ qro ⟧e ) ]
             Σ[ redl ∈ ((ρ⟨ θl , Al ⟩· oli) sn⟶₁ (ρ⟨ θo , Ao ⟩· si )) ]
             Σ[ redr ∈ ((ρ⟨ θr , Ar ⟩· ori) sn⟶₁ (ρ⟨ θo , Ao ⟩· si )) ]
             ((->E-view redl oolieq sileq) × (->E-view redr oorieq sireq)))

ρ-conf-rec {p₂} {El = El@.(epar₂ _ ∷ _)} {Er@.(epar₁ _ ∷ _)} {i = .(_ ∥ _)} cb (depar₂ ieqr) (depar₁ ieql) par redl redr olieq orieq viewl viewr with ρ-conf-rec2{El = El}{Er} cb (depar₂ ieqr) (depar₁ ieql) par redl redr olieq orieq viewl viewr refl refl
... | (θo , Ao , whatever , Erl , Ero , thig , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro , _) = θo , Ao , whatever , Erl , Ero , thig , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro

ρ-conf-rec {p₂} {El = (epar₁ q ∷ El)} {(epar₂ p ∷ Er)} {i = .(_ ∥ _)}{oli = (olp ∥ .q)}{ori = (.p ∥ orq)} cb@(CBρ (CBpar cbl cbr a b c d))  (depar₁ ieql) (depar₂ ieqr) par2 redl redr (depar₁ olieq) (depar₂ orieq) viewl viewr
  with unwrap-rho redl (depar₁ ieql) (depar₁ olieq) ieql olieq viewl | unwrap-rho redr (depar₂ ieqr) (depar₂ orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with wrap-rho redli ieql olieq viewli (epar₂ q) (depar₂ ieql) (depar₂ olieq) | wrap-rho redri ieqr orieq viewri (epar₁ p) (depar₁ ieqr) (depar₁ orieq)
... | (redl2 , viewl2) | (redr2 , viewr2) with ρ-conf-rec2{El = epar₂ q ∷ El}{epar₁ p ∷ Er}{oli = oli2}{ori = ori2} (CBρ (CBpar cbr cbl (distinct-sym a) (distinct-sym c) (distinct-sym b) (distinct'-sym d))) (depar₂ ieql) (depar₁ ieqr) par redl2 redr2  (depar₂ olieq) (depar₁ orieq) viewl2 viewr2 refl refl
      where
       oli2 = Term ∋ (q ∥ olp)
       ori2 = orq ∥ p
... | (θo , Ao , (sil@.orq ∥ sir@.olp) , (epar₂ _ ∷ Erl) , (epar₁ _ ∷ Ero) , (depar₂ oorieq) , (depar₁ oolieq) , (depar₂ sireq) , (depar₁ sileq) , rlout , rrout , viewlo , viewro , ((.Erl , .Ero , _ , _) , refl , refl))
    with unwrap-rho rlout (depar₁ oolieq) (depar₁ sileq) oolieq sileq viewlo | unwrap-rho rrout (depar₂ oorieq) (depar₂ sireq) oorieq sireq viewro
... | (roli , roliview) | (rori , roriview)
      with wrap-rho roli oolieq sileq roliview (epar₂ sir) (depar₂ oolieq) (depar₂ sileq) | wrap-rho rori oorieq sireq roriview (epar₁ sil) (depar₁ oorieq) (depar₁ sireq)
... | (rolo , roloview) | (roro , roroview) = θo , Ao , sir ∥ sil , epar₁ orq ∷ Erl ,
                                                                 epar₂ olp ∷ Ero ,
                                                                 depar₁ oorieq ,
                                                                 depar₂ oolieq ,
                                                                 depar₁ sireq , depar₂ sileq , rolo , roro , roloview , roroview -- _ , _ , _ , _ , _ , rolo , roro , roloview , roroview -- {! !}

ρ-conf-rec {El = epar₁ q ∷ El} {epar₁ .q ∷ Er} {ql} {qr} {.(_ ∥ q)} (CBρ (CBpar cb cb₁ x x₁ x₂ x₃)) (depar₁ ieql) (depar₁ ieqr) (parr a~~) redl redr (depar₁ olieq) (depar₁ orieq) viewl viewr
  with unwrap-rho redl (depar₁ ieql) (depar₁ olieq) ieql olieq viewl | unwrap-rho redr (depar₁ ieqr) (depar₁ orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with ρ-conf-rec (CBρ cb) ieql ieqr a~~ redli redri olieq orieq viewli viewri
... | ( θo , Ao , si , Elo , Ero , oorieq , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro )
    with wrap-rho rlout oolieq sileq viewlo (epar₁ q) (depar₁ oolieq) (depar₁ sileq) | wrap-rho rrout oorieq sireq viewro (epar₁ q) (depar₁ oorieq) (depar₁ sireq)
... | (rol , rolview) | (ror , rorview) = θo , Ao , si ∥ q , (epar₁ q) ∷ Elo , (epar₁ q) ∷ Ero , depar₁ oorieq ,
                                                                                depar₁ oolieq , depar₁ sireq , depar₁ sileq , rol , ror , rolview , rorview

ρ-conf-rec {El = (epar₂ p ∷ El)} {(epar₂ .p ∷ Er)} {i = .(_ ∥ _)} (CBρ (CBpar cb₁ cb x x₁ x₂ x₃)) (depar₂ ieql) (depar₂ ieqr) (parl a~~) redl redr (depar₂ olieq) (depar₂ orieq) viewl viewr
  with unwrap-rho redl (depar₂ ieql) (depar₂ olieq) ieql olieq viewl | unwrap-rho redr (depar₂ ieqr) (depar₂ orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with ρ-conf-rec (CBρ cb) ieql ieqr a~~ redli redri olieq orieq viewli viewri
... | ( θo , Ao , si , Elo , Ero , oorieq , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro )
    with wrap-rho rlout oolieq sileq viewlo (epar₂ p) (depar₂ oolieq) (depar₂ sileq) | wrap-rho rrout oorieq sireq viewro (epar₂ p) (depar₂ oorieq) (depar₂ sireq)
... | (rol , rolview) | (ror , rorview) = θo , Ao , p ∥ si , (epar₂ p) ∷ Elo , (epar₂ p) ∷ Ero , depar₂ oorieq ,
                                                                                depar₂ oolieq , depar₂ sireq , depar₂ sileq , rol , ror , rolview , rorview
ρ-conf-rec {El = (eseq q ∷ El)} {(eseq .q ∷ Er)} {i = .(_ >> q)} (CBρ (CBseq cb cb₁ x)) (deseq ieql) (deseq ieqr) (seq a~~) redl redr (deseq olieq) (deseq orieq) viewl viewr
  with unwrap-rho redl (deseq ieql) (deseq olieq) ieql olieq viewl | unwrap-rho redr (deseq ieqr) (deseq orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with ρ-conf-rec (CBρ cb) ieql ieqr a~~ redli redri olieq orieq viewli viewri
... | ( θo , Ao , si , Elo , Ero , oorieq , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro )
    with wrap-rho rlout oolieq sileq viewlo (eseq q) (deseq oolieq) (deseq sileq) | wrap-rho rrout oorieq sireq viewro (eseq q) (deseq oorieq) (deseq sireq)
... | (rol , rolview) | (ror , rorview) = θo , Ao , (si >> q) , (eseq q) ∷ Elo , (eseq q) ∷ Ero , deseq oorieq ,
                                                                                deseq oolieq , deseq sireq , deseq sileq , rol , ror , rolview , rorview

ρ-conf-rec {El = (eloopˢ q ∷ El)} {(eloopˢ .q ∷ Er)} {i = .(loopˢ _ q)} (CBρ (CBloopˢ cb cb₁ x _)) (deloopˢ ieql) (deloopˢ ieqr) (loopˢ a~~) redl redr (deloopˢ olieq) (deloopˢ orieq) viewl viewr
  with unwrap-rho redl (deloopˢ ieql) (deloopˢ olieq) ieql olieq viewl | unwrap-rho redr (deloopˢ ieqr) (deloopˢ orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with ρ-conf-rec (CBρ cb) ieql ieqr a~~ redli redri olieq orieq viewli viewri
... | ( θo , Ao , si , Elo , Ero , oorieq , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro )
    with wrap-rho rlout oolieq sileq viewlo (eloopˢ q) (deloopˢ oolieq) (deloopˢ sileq) | wrap-rho rrout oorieq sireq viewro (eloopˢ q) (deloopˢ oorieq) (deloopˢ sireq)
... | (rol , rolview) | (ror , rorview) = θo , Ao , (loopˢ si q) , (eloopˢ q) ∷ Elo , (eloopˢ q) ∷ Ero , deloopˢ oorieq ,
                                                                                deloopˢ oolieq , deloopˢ sireq , deloopˢ sileq , rol , ror , rolview , rorview

ρ-conf-rec {El = (esuspend S ∷ El)} {(esuspend .S ∷ Er)} {i = .(suspend _ _)} (CBρ (CBsusp cb x)) (desuspend ieql) (desuspend ieqr) (susp a~~) redl redr (desuspend olieq) (desuspend orieq) viewl viewr
  with unwrap-rho redl (desuspend ieql) (desuspend olieq) ieql olieq viewl | unwrap-rho redr (desuspend ieqr) (desuspend orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with ρ-conf-rec (CBρ cb) ieql ieqr a~~ redli redri olieq orieq viewli viewri
... | ( θo , Ao , si , Elo , Ero , oorieq , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro )
    with wrap-rho rlout oolieq sileq viewlo (esuspend S) (desuspend oolieq) (desuspend sileq) | wrap-rho rrout oorieq sireq viewro (esuspend S) (desuspend oorieq) (desuspend sireq)
... | (rol , rolview) | (ror , rorview) = θo , Ao , (suspend si S) , (esuspend S) ∷ Elo , (esuspend S) ∷ Ero , desuspend oorieq ,
                                                                                desuspend oolieq , desuspend sireq , desuspend sileq , rol , ror , rolview , rorview

ρ-conf-rec {El = (etrap ∷ El)} {(etrap ∷ Er)} {i = .(trap _)} (CBρ (CBtrap cb)) (detrap ieql) (detrap ieqr) (trp a~~) redl redr (detrap olieq) (detrap orieq) viewl viewr
  with unwrap-rho redl (detrap ieql) (detrap olieq) ieql olieq viewl | unwrap-rho redr (detrap ieqr) (detrap orieq) ieqr orieq viewr
... | (redli , viewli) | (redri , viewri) with ρ-conf-rec (CBρ cb) ieql ieqr a~~ redli redri olieq orieq viewli viewri
... | ( θo , Ao , si , Elo , Ero , oorieq , oolieq , sireq , sileq , rlout , rrout , viewlo , viewro )
    with wrap-rho rlout oolieq sileq viewlo (etrap) (detrap oolieq) (detrap sileq) | wrap-rho rrout oorieq sireq viewro (etrap) (detrap oorieq) (detrap sireq)
... | (rol , rolview) | (ror , rorview) = θo , Ao , (trap si) , (etrap) ∷ Elo , (etrap) ∷ Ero , detrap oorieq ,
                                                                                detrap oolieq , detrap sireq , detrap sileq , rol , ror , rolview , rorview

ext: agda


text:
{-# OPTIONS --without-K #-}
module hott.level where

open import hott.level.core public
open import hott.level.sets public
open import hott.level.closure public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat renaming (_+_ to _+n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Vec
open import Cubical.Data.Vec.DepVec

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.DirectSumFun
open import Cubical.Algebra.AbGroup.Instances.DirectSumHIT
open import Cubical.Algebra.AbGroup.Instances.NProd

open import Cubical.Algebra.DirectSum.DirectSumFun.Base
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.DirectSum.DirectSumHIT.Properties
open import Cubical.Algebra.DirectSum.DirectSumHIT.PseudoNormalForm

private variable
  ℓ : Level

open GroupTheory
open AbGroupTheory
open AbGroupStr

-----------------------------------------------------------------------------
-- Notation

module Equiv-Properties
  (G : ℕ → Type ℓ)
  (Gstr : (n : ℕ) → AbGroupStr (G n))
  where

  -- the convention is a bit different and had a -
  -- because otherwise it is unreadable

  open AbGroupStr (snd (⊕HIT-AbGr ℕ G Gstr)) using ()
    renaming
    ( 0g       to 0⊕HIT
    ; _+_      to _+⊕HIT_
    ; -_       to -⊕HIT_
    ; +Assoc   to +⊕HIT-Assoc
    ; +IdR     to +⊕HIT-IdR
    ; +IdL     to +⊕HIT-IdL
    ; +InvR    to +⊕HIT-InvR
    ; +InvL    to +⊕HIT-InvL
    ; +Comm     to +⊕HIT-Comm
    ; is-set   to isSet⊕HIT)

  open AbGroupStr (snd (⊕Fun-AbGr G Gstr)) using ()
    renaming
    ( 0g       to 0⊕Fun
    ; _+_      to _+⊕Fun_
    ; -_       to -⊕Fun_
    ; +Assoc   to +⊕Fun-Assoc
    ; +IdR     to +⊕Fun-IdR
    ; +IdL     to +⊕Fun-IdL
    ; +InvR    to +⊕Fun-InvR
    ; +InvL    to +⊕Fun-InvL
    ; +Comm     to +⊕Fun-Comm
    ; is-set   to isSet⊕Fun)

-----------------------------------------------------------------------------
-- AbGroup on Fun -> produit ? sequence ?

  open AbGroupStr (snd (NProd-AbGroup G Gstr)) using ()
      renaming
    ( 0g       to 0Fun
    ; _+_      to _+Fun_
    ; -_       to -Fun_
    ; +Assoc   to +FunAssoc
    ; +IdR     to +FunIdR
    ; +IdL     to +FunIdL
    ; +InvR    to +FunInvR
    ; +InvL    to +FunInvL
    ; +Comm     to +FunComm
    ; is-set   to isSetFun)

-----------------------------------------------------------------------------
-- Some simplification for transport

  open SubstLemma ℕ G Gstr

  substG : (g : (n : ℕ) → G n) → {k n : ℕ} → (p : k ≡ n) → subst G p (g k) ≡ g n
  substG g {k} {n} p = J (λ n p → subst G p (g k) ≡ g n) (transportRefl _) p

-----------------------------------------------------------------------------
-- Direct Sense

  -- To facilitate the proof the translation to the function
  -- and its properties are done in two times

  ---------------------------------------------------------------------------
  -- Translation to the function

  fun-trad : (k : ℕ) → (a : G k) → (n : ℕ) → G n
  fun-trad k a n with (discreteℕ k n)
  ... | yes p = subst G p a
  ... | no ¬p = 0g (Gstr n)

  fun-trad-eq : (k : ℕ) → (a : G k) → fun-trad k a k ≡ a
  fun-trad-eq k a with discreteℕ k k
  ... | yes p = cong (λ X → subst G X a) (isSetℕ _ _ _ _) ∙ transportRefl a
  ... | no ¬p = ⊥.rec (¬p refl)

  fun-trad-neq : (k : ℕ) → (a : G k) → (n : ℕ) → (k ≡ n → ⊥) → fun-trad k a n ≡ 0g (Gstr n)
  fun-trad-neq k a n ¬q with discreteℕ k n
  ... | yes p = ⊥.rec (¬q p)
  ... | no ¬p = refl

  ⊕HIT→Fun : ⊕HIT ℕ G Gstr → (n : ℕ) → G n
  ⊕HIT→Fun = DS-Rec-Set.f _ _ _ _ isSetFun
              0Fun
              fun-trad
              _+Fun_
              +FunAssoc
              +FunIdR
              +FunComm
              (λ k → funExt (λ n → base0-eq k n))
              λ k a b → funExt (λ n → base-add-eq k a b n)
           where
           base0-eq : (k : ℕ) → (n : ℕ) → fun-trad k (0g (Gstr k)) n ≡ 0g (Gstr n)
           base0-eq k n with (discreteℕ k n)
           ... | yes p = subst0g _
           ... | no ¬p = refl

           base-add-eq : (k : ℕ) → (a b : G k) → (n : ℕ) →
                         PathP (λ _ → G n) (Gstr n ._+_ (fun-trad k a n) (fun-trad k b n))
                                                         (fun-trad k ((Gstr k + a) b) n)
           base-add-eq k a b n with (discreteℕ k n)
           ... | yes p = subst+ _ _ _
           ... | no ¬p = +IdR (Gstr n)_

  ⊕HIT→Fun-pres0 : ⊕HIT→Fun 0⊕HIT ≡ 0Fun
  ⊕HIT→Fun-pres0 = refl

  ⊕HIT→Fun-pres+ : (x y : ⊕HIT ℕ G Gstr) → ⊕HIT→Fun (x +⊕HIT y) ≡ ((⊕HIT→Fun x) +Fun (⊕HIT→Fun y))
  ⊕HIT→Fun-pres+ x y = refl

  ---------------------------------------------------------------------------
  -- Translation to the properties

  nfun-trad : (k : ℕ) → (a : G k) → AlmostNull G Gstr (fun-trad k a)
  nfun-trad k a = k , fix-eq
    where
    fix-eq : (n : ℕ) → k < n → fun-trad k a n ≡ 0g (Gstr n)
    fix-eq n q with (discreteℕ k n)
    ... | yes p = ⊥.rec (<→≢ q p)
    ... | no ¬p = refl

  ⊕HIT→⊕AlmostNull : (x : ⊕HIT ℕ G Gstr) → AlmostNullP G Gstr (⊕HIT→Fun x)
  ⊕HIT→⊕AlmostNull = DS-Ind-Prop.f _ _ _ _ (λ x → squash₁)
                      ∣ (0 , (λ n q → refl)) ∣₁
                      (λ r a → ∣ (nfun-trad r a) ∣₁)
                      λ {U} {V} → PT.elim (λ _ → isPropΠ (λ _ → squash₁))
                                   (λ { (k , nu) → PT.elim (λ _ → squash₁)
                                    λ { (l , nv) →
                                   ∣ ((k +n l) , (λ n q → cong₂ ((Gstr n)._+_) (nu n (<-+k-trans q)) (nv n (<-k+-trans q))
                                                          ∙ +IdR (Gstr n) _)) ∣₁} })

  ---------------------------------------------------------------------------
  -- Translation + Morphism

  ⊕HIT→⊕Fun : ⊕HIT ℕ G Gstr → ⊕Fun G Gstr
  ⊕HIT→⊕Fun x = (⊕HIT→Fun x) , (⊕HIT→⊕AlmostNull x)

  ⊕HIT→⊕Fun-pres0 : ⊕HIT→⊕Fun 0⊕HIT ≡ 0⊕Fun
  ⊕HIT→⊕Fun-pres0 = refl

  ⊕HIT→⊕Fun-pres+ : (x y : ⊕HIT ℕ G Gstr) → ⊕HIT→⊕Fun (x +⊕HIT y) ≡ ((⊕HIT→⊕Fun x) +⊕Fun (⊕HIT→⊕Fun y))
  ⊕HIT→⊕Fun-pres+ x y = ΣPathTransport→PathΣ _ _ (refl , (squash₁ _ _))

-----------------------------------------------------------------------------
-- Converse sense

  -----------------------------------------------------------------------------
  -- Prood that ⊕HIT→⊕Fun is injective

  open DefPNF G Gstr

  sumFun : {m : ℕ} → depVec G m → (n : ℕ) → G n
  sumFun {0} ⋆ = 0Fun
  sumFun {suc m} (a □ dv) = (⊕HIT→Fun (base m a)) +Fun (sumFun dv)

  SumHIT→SumFun : {m : ℕ} → (dv : depVec G m) → ⊕HIT→Fun (sumHIT dv) ≡ sumFun dv
  SumHIT→SumFun {0} ⋆ = refl
  SumHIT→SumFun {suc m} (a □ dv) = cong₂ _+Fun_ refl (SumHIT→SumFun dv)

  sumFun< : {m : ℕ} → (dv : depVec G m) → (i : ℕ) → (m ≤ i) → sumFun dv i ≡ 0g (Gstr i)
  sumFun< {0} ⋆ i r = refl
  sumFun< {suc m} (a □ dv) i r with discreteℕ m i
  ... | yes p = ⊥.rec (<→≢ r p)
  ... | no ¬p = +IdL (Gstr i) _ ∙ sumFun< dv i (≤-trans ≤-sucℕ r)

  sumFunHead : {m : ℕ} → (a b : (G m)) → (dva dvb : depVec G m) →
               (x : sumFun (a □ dva) ≡ sumFun (b □ dvb)) → a ≡ b
  sumFunHead {m} a b dva dvb x =
               a
                        ≡⟨ sym (+IdR (Gstr m) _) ⟩
               (Gstr m)._+_ a (0g (Gstr m))
                        ≡⟨ cong₂ (Gstr m ._+_) (sym (fun-trad-eq m a)) (sym (sumFun< dva m ≤-refl)) ⟩
               (Gstr m)._+_ (fun-trad m a m) (sumFun dva m)
                        ≡⟨ funExt⁻ x m ⟩
               (Gstr m)._+_ (fun-trad m b m) (sumFun dvb m)
                        ≡⟨ cong₂ (Gstr m ._+_) (fun-trad-eq m b) (sumFun< dvb m ≤-refl) ⟩
               (Gstr m)._+_ b (0g (Gstr m))
                        ≡⟨ +IdR (Gstr m) _ ⟩
               b ∎

  substSumFun : {m : ℕ} → (dv : depVec G m) → (n : ℕ) → (p : m ≡ n)
                → subst G p (sumFun dv m) ≡ sumFun dv n
  substSumFun {m} dv n p = J (λ n p → subst G p (sumFun dv m) ≡ sumFun dv n)
                             (transportRefl _)
                             p

  sumFunTail : {m : ℕ} → (a b : (G m)) → (dva dvb : depVec G m) →
             (x : sumFun (a □ dva) ≡ sumFun (b □ dvb)) → (n : ℕ) →
             sumFun dva n ≡ sumFun dvb n
  sumFunTail {m} a b dva dvb x n with discreteℕ m n
  ... | yes p = sumFun dva n                   ≡⟨ sym (substSumFun dva n p) ⟩
                subst G p (sumFun dva m)       ≡⟨ cong (subst G p) (sumFun< dva m ≤-refl) ⟩
                subst G p (0g (Gstr m))        ≡⟨ subst0g p ⟩
                0g (Gstr n)                    ≡⟨ sym (subst0g p) ⟩
                subst G p (0g (Gstr m))        ≡⟨ sym (cong (subst G p) (sumFun< dvb m ≤-refl)) ⟩
                subst G p (sumFun dvb m)       ≡⟨ substSumFun dvb n p ⟩
                sumFun dvb n ∎
  ... | no ¬p = sumFun dva n                                 ≡⟨ sym (+IdL (Gstr n) _) ⟩
                (Gstr n)._+_ (0g (Gstr n)) (sumFun dva n)    ≡⟨ cong (λ X → (Gstr n)._+_ X (sumFun dva n))
                                                                             (sym (fun-trad-neq m a n ¬p)) ⟩
                Gstr n ._+_ (fun-trad m a n) (sumFun dva n)  ≡⟨ funExt⁻ x n ⟩
                Gstr n ._+_ (fun-trad m b n) (sumFun dvb n)  ≡⟨ cong (λ X → Gstr n ._+_ X (sumFun dvb n))
                                                                             (fun-trad-neq m b n ¬p) ⟩
                (Gstr n)._+_ (0g (Gstr n)) (sumFun dvb n)    ≡⟨ +IdL (Gstr n) _ ⟩
                sumFun dvb n ∎

  injSumFun : {m : ℕ} → (dva dvb : depVec G m) → sumFun dva ≡ sumFun dvb → dva ≡ dvb
  injSumFun {0} ⋆ ⋆ x = refl
  injSumFun {suc m} (a □ dva) (b □ dvb) x = depVecPath.decode G (a □ dva) (b □ dvb)
                                         ((sumFunHead a b dva dvb x)
                                         , (injSumFun dva dvb (funExt (sumFunTail a b dva dvb x))))

  injSumHIT : {m : ℕ} → (dva dvb : depVec G m) → ⊕HIT→Fun (sumHIT dva) ≡ ⊕HIT→Fun (sumHIT dvb) → dva ≡ dvb
  injSumHIT dva dvb r = injSumFun dva dvb (sym (SumHIT→SumFun dva) ∙ r ∙ SumHIT→SumFun dvb)

  inj-⊕HIT→Fun : (x y : ⊕HIT ℕ G Gstr) → ⊕HIT→Fun x ≡ ⊕HIT→Fun y → x ≡ y
  inj-⊕HIT→Fun x y r = helper (⊕HIT→PNF2 x y) r
    where
    helper : PNF2 x y → ⊕HIT→Fun x ≡ ⊕HIT→Fun y → x ≡ y
    helper = PT.elim (λ _ → isPropΠ (λ _ → isSet⊕HIT _ _))
                     λ { (m , dva , dvb , p , q) r →
                         p
                         ∙ cong sumHIT (injSumHIT dva dvb (sym (cong ⊕HIT→Fun p) ∙ r ∙ cong ⊕HIT→Fun q))
                         ∙ sym q}

  inj-⊕HIT→⊕Fun : (x y : ⊕HIT ℕ G Gstr) → ⊕HIT→⊕Fun x ≡ ⊕HIT→⊕Fun y → x ≡ y
  inj-⊕HIT→⊕Fun x y p = inj-⊕HIT→Fun x y (fst (PathΣ→ΣPathTransport _ _ p))

  lemProp : (g : ⊕Fun G Gstr) → isProp (Σ[ x ∈ ⊕HIT ℕ G Gstr ] ⊕HIT→⊕Fun x ≡ g )
  lemProp g (x , p) (y , q) = ΣPathTransport→PathΣ _ _
                              ((inj-⊕HIT→⊕Fun x y (p ∙ sym q)) , isSet⊕Fun _ _ _ _)

  ---------------------------------------------------------------------------
  --  General translation for underliyng function

  Strad : (g : (n : ℕ) → G n) → (i : ℕ) → ⊕HIT ℕ G Gstr
  Strad g zero = base 0 (g 0)
  Strad g (suc i) = (base (suc i) (g (suc i))) +⊕HIT (Strad g i)

  Strad-pres+ : (f g : (n : ℕ) → G n) → (i : ℕ) → Strad (f +Fun g) i ≡ Strad f i +⊕HIT Strad g i
  Strad-pres+ f g zero = sym (base-add 0 (f 0) (g 0))
  Strad-pres+ f g (suc i) = cong₂ _+⊕HIT_ (sym (base-add _ _ _))
                                          (Strad-pres+ f g i)
                            ∙ comm-4 (⊕HIT-AbGr ℕ G Gstr) _ _ _ _

  -- Properties in the converse sens
  Strad-max : (f : (n : ℕ) → G n) → (k : ℕ) → (ng : AlmostNullProof G Gstr f k)
              → (i : ℕ) → (r : k ≤ i) → Strad f i ≡ Strad f k
  Strad-max f k ng zero r = sym (cong (Strad f) (≤0→≡0 r))
  Strad-max f k ng (suc i) r with ≤-split r
  ... | inl x = cong₂ _+⊕HIT_
                      (cong (base (suc i)) (ng (suc i) x) ∙ base-neutral (suc i))
                      (Strad-max f k ng i (pred-≤-pred x))
                ∙ +⊕HIT-IdL _
  ... | inr x = cong (Strad f) (sym x)

  -- if m < n then the translation of sum up to i is 0
  Strad-m<n : (g : (n : ℕ) → G n) → (m : ℕ) → (n : ℕ) → (r : m < n)
            → ⊕HIT→Fun (Strad g m) n ≡ 0g (Gstr n)
  Strad-m<n g zero n r with discreteℕ 0 n
  ... | yes p = ⊥.rec (<→≢ r p)
  ... | no ¬p = refl
  Strad-m<n g (suc m) n r with discreteℕ (suc m) n
  ... | yes p = ⊥.rec (<→≢ r p)
  ... | no ¬p = +IdL (Gstr n) _ ∙ Strad-m<n g m n (<-trans ≤-refl r)

  {- if n ≤ m, prove ⊕HIT→Fun (∑_{i ∈〚0, m〛} base i (g i)) ≡ g n
     then n is equal to only one〚0, m〛=> induction on m
     case 0 : ok
     case suc m : if n ≡ suc m, then the rest of the sum is 0 by trad-m<n
                  if n ≢ suc m, then it is in the rest of the sum => recursive call -}
  Strad-n≤m : (g : (n : ℕ) → G n) → (m : ℕ) → (n : ℕ) → (r : n ≤ m) → ⊕HIT→Fun (Strad g m) n ≡ g n
  Strad-n≤m g zero n r with discreteℕ 0 n
  ... | yes p = substG g p
  ... | no ¬p = ⊥.rec (¬p (sym (≤0→≡0 r)))
  Strad-n≤m g (suc m) n r with discreteℕ (suc m) n
  ... | yes p = cong₂ ((Gstr n)._+_) (substG g p) (Strad-m<n g m n (0 , p)) ∙ +IdR (Gstr n) _
  ... | no ¬p = +IdL (Gstr n) _ ∙ Strad-n≤m g m n (≤-suc-≢ r λ x → ¬p (sym x))

  ---------------------------------------------------------------------------
  -- Translation + Morphsim

  -- translation
  ⊕Fun→⊕HIT+ : (g : ⊕Fun G Gstr) → Σ[ x ∈ ⊕HIT ℕ G Gstr ] ⊕HIT→⊕Fun x ≡ g
  ⊕Fun→⊕HIT+ (g , Ang) = PT.rec (lemProp (g , Ang))
                          (λ { (k , ng)
                               → Strad g k , ΣPathTransport→PathΣ _ _
                                              ((funExt (trad-section g k ng)) , (squash₁ _ _)) })
                          Ang
             where
             trad-section : (g : (n : ℕ) → G n) → (k : ℕ) → (ng : (n : ℕ) → ( k < n) → g n ≡ 0g (Gstr n))
                            → (n : ℕ) → ⊕HIT→Fun (Strad g k) n ≡ g n
             trad-section g k ng n with splitℕ-≤ n k
             ... | inl x = Strad-n≤m g k n x
             ... | inr x = Strad-m<n g k n x ∙ sym (ng n x)

  ⊕Fun→⊕HIT : ⊕Fun G Gstr → ⊕HIT ℕ G Gstr
  ⊕Fun→⊕HIT g = fst (⊕Fun→⊕HIT+ g)

  -- morphism
  ⊕Fun→⊕HIT-pres0 : ⊕Fun→⊕HIT 0⊕Fun ≡ 0⊕HIT
  ⊕Fun→⊕HIT-pres0 = base-neutral 0

  ⊕Fun→⊕HIT-pres+ : (f g : ⊕Fun G Gstr) → ⊕Fun→⊕HIT (f +⊕Fun g) ≡ (⊕Fun→⊕HIT f) +⊕HIT (⊕Fun→⊕HIT g)
  ⊕Fun→⊕HIT-pres+ (f , Anf) (g , Ang) = PT.elim2 (λ x y → isSet⊕HIT (⊕Fun→⊕HIT ((f , x) +⊕Fun (g , y)))
                                                                   ((⊕Fun→⊕HIT (f , x)) +⊕HIT (⊕Fun→⊕HIT (g , y))))
                                                  (λ x y → AN f x g y)
                                                   Anf Ang

    where
    AN : (f : (n : ℕ) → G n) → (x : AlmostNull G Gstr f) → (g : (n : ℕ) → G n) → (y : AlmostNull G Gstr g)
                     → ⊕Fun→⊕HIT ((f , ∣ x ∣₁) +⊕Fun (g , ∣ y ∣₁)) ≡ (⊕Fun→⊕HIT (f , ∣ x ∣₁)) +⊕HIT (⊕Fun→⊕HIT (g , ∣ y ∣₁))
    AN f (k , nf) g (l , ng) = Strad-pres+ f g (k +n l)
                               ∙ cong₂ _+⊕HIT_ (Strad-max f k nf (k +n l) (l , (+-comm l k)))
                                               (Strad-max g l ng (k +n l) (k , refl))

-----------------------------------------------------------------------------
-- Section

  e-sect : (g : ⊕Fun G Gstr) → ⊕HIT→⊕Fun (⊕Fun→⊕HIT g) ≡ g
  e-sect g = snd (⊕Fun→⊕HIT+ g)

-----------------------------------------------------------------------------
-- Retraction

  lemmaSkk : (k : ℕ) → (a : G k) → (i : ℕ) → (r : i < k) → Strad (λ n → fun-trad k a n) i ≡ 0⊕HIT
  lemmaSkk k a zero r with discreteℕ k 0
  ... | yes p = ⊥.rec (<→≢ r (sym p))
  ... | no ¬p = base-neutral 0
  lemmaSkk k a (suc i) r with discreteℕ k (suc i)
  ... | yes p = ⊥.rec (<→≢ r (sym p))
  ... | no ¬p = cong₂ _+⊕HIT_ (base-neutral (suc i)) (lemmaSkk k a i (<-trans ≤-refl r)) ∙ +⊕HIT-IdR _

  lemmakk : (k : ℕ) → (a : G k) → ⊕Fun→⊕HIT (⊕HIT→⊕Fun (base k a)) ≡ base k a
  lemmakk zero a = cong (base 0) (transportRefl a)
  lemmakk (suc k) a with (discreteℕ (suc k) (suc k)) | (discreteℕ k k)
  ... | yes p | yes q = cong₂ _add_
                             (sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base (cong suc q) a))
                             (lemmaSkk (suc k) a k ≤-refl)
                        ∙ +⊕HIT-IdR _
  ... | yes p | no ¬q = ⊥.rec (¬q refl)
  ... | no ¬p | yes q = ⊥.rec (¬p refl)
  ... | no ¬p | no ¬q = ⊥.rec (¬q refl)

  e-retr : (x : ⊕HIT ℕ G Gstr) → ⊕Fun→⊕HIT (⊕HIT→⊕Fun x) ≡ x
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕HIT _ _)
           (base-neutral 0)
           lemmakk
           λ {U} {V} ind-U ind-V → cong ⊕Fun→⊕HIT (⊕HIT→⊕Fun-pres+ U V)
                                    ∙ ⊕Fun→⊕HIT-pres+ (⊕HIT→⊕Fun U) (⊕HIT→⊕Fun V)
                                    ∙ cong₂ _+⊕HIT_ ind-U ind-V

module _
  (G : ℕ → Type ℓ)
  (Gstr : (n : ℕ) → AbGroupStr (G n))
  where

  open Iso
  open Equiv-Properties G Gstr

  Equiv-DirectSum : AbGroupEquiv (⊕HIT-AbGr ℕ G Gstr) (⊕Fun-AbGr G Gstr)
  fst Equiv-DirectSum = isoToEquiv is
    where
    is : Iso (⊕HIT ℕ G Gstr) (⊕Fun G Gstr)
    fun is = ⊕HIT→⊕Fun
    Iso.inv is = ⊕Fun→⊕HIT
    rightInv is = e-sect
    leftInv is = e-retr
  snd Equiv-DirectSum = makeIsGroupHom ⊕HIT→⊕Fun-pres+

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- The empty type; also used as absurd proposition (``Falsity'').

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

module Tools.Empty where

open import Data.Empty public


text:
module STT where

-- simple type theory

{-
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Data.Nat hiding (_>_)
-}

open import StdLibStuff

open import Syntax

-- inference system

data ⊢_ : ∀ {n} → {Γ : Ctx n} → Form Γ $o → Set where
 ax-1 : ∀ {n} → {Γ : Ctx n} {x : Var Γ} →
  (p : lookup-Var Γ x ≡ $o) →
  ⊢ ((var x p || var x p) => var x p)

 ax-2 : ∀ {n} → {Γ : Ctx n} {x y : Var Γ} →
  (px : lookup-Var Γ x ≡ $o) →
  (py : lookup-Var Γ y ≡ $o) →
  ⊢ (var x px => (var x px || var y py))

 ax-3 : ∀ {n} → {Γ : Ctx n} {x y : Var Γ} →
  (px : lookup-Var Γ x ≡ $o) →
  (py : lookup-Var Γ y ≡ $o) →
  ⊢ ((var x px || var y py) => (var y py || var x px))

 ax-4 : ∀ {n} → {Γ : Ctx n} {x y z : Var Γ} →
  (px : lookup-Var Γ x ≡ $o) →
  (py : lookup-Var Γ y ≡ $o) →
  (pz : lookup-Var Γ z ≡ $o) →
  ⊢ ((var x px => var y py) => ((var z pz || var x px) => (var z pz || var y py)))

 ax-5 : ∀ {n} → {Γ : Ctx n} {α : Type n} {x y : Var Γ} →
  (px : lookup-Var Γ x ≡ α > $o) →
  (py : lookup-Var Γ y ≡ α) →
  ⊢ (app Π (var x px) => app (var x px) (var y py))

 ax-6 : ∀ {n} → {Γ : Ctx n} {α : Type n} {x y : Var Γ} →
  (px : lookup-Var Γ x ≡ α > $o) →
  (py : lookup-Var Γ y ≡ $o) →
  ⊢ ((![ α ] (weak (var y py) || app (weak (var x px)) (var this refl))) => (var y py || app Π (var x px)))

 ax-10-a : ∀ {n} → {Γ : Ctx n} {x y : Var Γ} →
  (px : lookup-Var Γ x ≡ $o) →
  (py : lookup-Var Γ y ≡ $o) →
  ⊢ ((var x px <=> var y py) => (var x px == var y py))

 ax-10-b : ∀ {n} → {Γ : Ctx n} {α β : Type n} {f g : Var Γ} →
  (pf : lookup-Var Γ f ≡ α > β) →
  (pg : lookup-Var Γ g ≡ α > β) →
  ⊢ ((![ α ] (app (weak (var f pf)) (var this refl) == app (weak (var g pg)) (var this refl))) => (var f pf == var g pg))

 ax-11 : ∀ {n} → {Γ : Ctx n} {α : Type n} {f : Var Γ} →
  (pf : lookup-Var Γ f ≡ α > $o) →
  ⊢ ((?[ α ] (app (weak (var f pf)) (var this refl))) => (app (var f pf) (app i (var f pf))))

 -- inf-I in Henkin is α-conversion
 -- with de Bruijn-indeces we need context extension instead
 extend-context : ∀ {n} {Γ : Ctx n} (α : Type n) {F : Form Γ $o} →
  ⊢_ {_} {α ∷ Γ} (weak F) →
  ⊢ F

 inf-II : ∀ {n} → (Γ Γ' : Ctx n) {α β : Type n} (F : Form (Γ' ++ Γ) β → Form Γ $o) (G : Form (α ∷ (Γ' ++ Γ)) β) (H : Form (Γ' ++ Γ) α) →
  ⊢ (F ((^[ α ] G) · H) => F (sub H G))  -- formulated as an inference rule in Henkin, as an axiom (containing expressions) here

 inf-III : ∀ {n} → (Γ Γ' : Ctx n) {α β : Type n} (F : Form (Γ' ++ Γ) β → Form Γ $o) (G : Form (α ∷ (Γ' ++ Γ)) β) (H : Form (Γ' ++ Γ) α) →
  ⊢ (F (sub H G) => F ((^[ α ] G) · H))  -- formulated as an inference rule in Henkin, as an axiom (containing expressions) here

 inf-IV : ∀ {n} → {Γ : Ctx n} {α : Type n} (F : Form Γ (α > $o)) (x : Var Γ) (G : Form Γ α) →
  occurs x F ≡ false →
  (p : lookup-Var Γ x ≡ α) →
  ⊢ (app F (var x p)) →
  ⊢ (app F G)

 inf-V : ∀ {n} → {Γ : Ctx n} {F G : Form Γ $o} →
  ⊢ (F => G) →   ⊢ F →
  ⊢ G

 inf-VI : ∀ {n} → {Γ : Ctx n} {α : Type n} {F : Form Γ (α > $o)} (x : Var Γ) →
  occurs x F ≡ false →
  (p : lookup-Var Γ x ≡ α) →
  ⊢ (app F (var x p) => app Π F)  -- formulated as an inference rule in Henkin, as an axiom (containing expressions) here

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

-- Variants of the axioms that are simpler to work with

ax-1-s : ∀ {n} → {Γ : Ctx n} {F : Form Γ $o} →
 ⊢ ((F || F) => F)

ax-2-s : ∀ {n} → {Γ : Ctx n} {F G : Form Γ $o} →
 ⊢ (F => (F || G))

ax-3-s : ∀ {n} → {Γ : Ctx n} {F G : Form Γ $o} →
 ⊢ ((F || G) => (G || F))

ax-4-s : ∀ {n} → {Γ : Ctx n} {F G H : Form Γ $o} →
 ⊢ ((F => G) => ((H || F) => (H || G)))

ax-5-s : ∀ {n} → {Γ : Ctx n} {α : Type n} (F : Form (α ∷ Γ) $o) (G : Form Γ α) →
  ⊢ (![ α ] F => sub G F)

ax-5-s2 : ∀ {n} → {Γ : Ctx n} {α : Type n} (F : Form Γ (α > $o)) (G : Form Γ α) →
  ⊢ ((![ α ] (~ (weak F · $ this {refl}))) => (~ (F · G)))

ax-5-s3 : ∀ {n} → {Γ : Ctx n} {α : Type n} (F : Form Γ (α > $o)) (G : Form Γ α) →
  ⊢ ((!'[ α ] F) => (F · G))

ax-6-s : ∀ {n} → {Γ : Ctx n} {α : Type n} {F : Form Γ $o} {G : Form (α ∷ Γ) $o} →
 ⊢ ((![ α ] (weak F || G)) => (F || (![ α ] G)))

ax-10-a-s : ∀ {n} → {Γ : Ctx n} {F G : Form Γ $o} →
 ⊢ ((F <=> G) => (F == G))

ax-10-b-s : ∀ {n} → {Γ : Ctx n} {α β : Type n} {F G : Form (α ∷ Γ) β} → ⊢ ((![ α ] (F == G)) => (^[ α ] F == ^[ α ] G))

ax-10-b-s2 : ∀ {n} → {Γ : Ctx n} {α β : Type n} {F G : Form Γ (α > β)} →
 ⊢ ((![ α ] (app (weak F) (var this refl) == app (weak G) (var this refl))) => (F == G))

ax-11-s : ∀ {n} → {Γ : Ctx n} {α : Type n} {F : Form (α ∷ Γ) $o} →
 ⊢ ((?[ α ] F => sub (ι α F) F))

ax-11-s2 : ∀ {n} → {Γ : Ctx n} {α : Type n} (F : Form Γ (α > $o)) →
 ⊢ ((?'[ α ] F) => (F · ι' α F))

inf-II-samectx : ∀ {n} → {Γ : Ctx n} {α β : Type n} (F : Form Γ β → Form Γ $o) (G : Form (α ∷ Γ) β) (H : Form Γ α) →
  ⊢ (F ((^[ α ] G) · H) => F (sub H G))
inf-II-samectx {_} {Γ} = inf-II Γ ε

inf-III-samectx : ∀ {n} → {Γ : Ctx n} {α β : Type n} (F : Form Γ β → Form Γ $o) (G : Form (α ∷ Γ) β) (H : Form Γ α) →
  ⊢ (F (sub H G) => F ((^[ α ] G) · H))
inf-III-samectx {_} {Γ} = inf-III Γ ε

inf-VI-s : ∀ {n} → {Γ : Ctx n} {α : Type n} {F : Form (α ∷ Γ) $o} →
 ⊢ F →
 ⊢ ![ α ] F

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

ax-5-s F G = inf-V (inf-II-samectx (λ z → (![ _ ] F) => z) F G) (subst (λ z → ⊢ ((![ _ ] F) => ((^[ _ ] F) · z))) (sym (sub-weak-p-1' G (^[ _ ] F))) (inf-V (inf-II-samectx (λ z → z) (app Π (var this refl) => app (var this refl) (weak G)) (^[ _ ] F)) (extend-context (_ > $o) (inf-IV _ this _ (occurs-p-2 (lam _ (weak G))) refl (inf-V (inf-III-samectx (λ z → z) (app Π (var this refl) => app (var this refl) (weak-i (_ ∷ ε) _ (weak G))) (var this refl)) (extend-context _ (inf-V (inf-II-samectx (λ z → z) (app Π (var (next (next this)) refl) => app (var (next (next this)) refl) (var this refl)) _) (inf-IV _ this _ refl refl (inf-V (inf-III-samectx (λ z → z) _ _) (ax-5 {_} {_} {_} {next this} {this} refl refl))))))))))

inf-VI-s {_} {Γ} {α} {F} = λ h → extend-context α (inf-V (inf-VI this (occurs-p-2 (lam α F)) refl) (inf-V (inf-III-samectx (λ z → z) (weak-i (α ∷ ε) Γ F) (var this refl)) (subst (λ z → ⊢ z) (sym (sub-sub-weak-weak-p-3 F)) h)))

ax-6-s {_} {Γ} {α} {F} {G} =
 subst (λ z → ⊢ ((![ α ] (weak F || z)) => (F || ![ α ] G))) (sub-sub-weak-weak-p F G)
 (inf-V (inf-II Γ (α ∷ ε) (λ z → ((![ α ] (weak F || z)) => (F || app Π (lam α G)))) (sub-i (α ∷ (α ∷ ε)) Γ F (weak-i (α ∷ ε) ($o ∷ Γ) (weak-i (α ∷ ε) Γ G))) (var this refl))
 (subst (λ z → ⊢ ((![ α ] (weak F || app (sub-i (α ∷ ε) Γ F (weak (weak (lam α G)))) (var this refl))) => (F || app Π z))) (sym (sub-weak-p-1' (lam α G) F))
 (inf-V (ax-5-s _ F) (inf-VI-s (inf-V (ax-5-s _ (weak (lam α G))) (inf-VI-s (ax-6 {_} {_} {α} {this} {next this} refl refl)))))))

ax-10-b-s {_} {Γ} {α} {β} {F} {G} =
 subst (λ z → ⊢ ((![ α ] (F == z) => (lam α F == lam α G)))) (sub-sub-weak-weak-p-3 G) (
 inf-V (inf-II Γ (α ∷ ε) (λ z → ((![ α ] (F == z)) => (lam α F == lam α G))) (weak-i (α ∷ ε) Γ G) (var this refl)) (
 subst (λ z → ⊢ ((![ α ] (z == app (weak (lam α G)) (var this refl))) => (lam α F == lam α G))) (sub-sub-weak-weak-p-2 F G) (
 inf-V (inf-II Γ (α ∷ ε) (λ z → (((![ α ] (z == app (weak (lam α G)) (var this refl)) => (lam α F == lam α G))))) (sub-i (α ∷ (α ∷ ε)) Γ (lam α G) (weak-i (α ∷ ε) ((α > β) ∷ Γ) (weak-i (α ∷ ε) Γ F))) (var this refl)) (
 subst (λ z → ⊢ (((![ α ] (app (sub-i (α ∷ ε) Γ (lam α G) (weak (weak (lam α F)))) (var this refl) == app (weak (lam α G)) (var this refl)) => (z == lam α G))))) (sym (sub-weak-p-1' (lam α F) (lam α G)))
 (inf-V (ax-5-s _ (lam α G)) (inf-VI-s (inf-V (ax-5-s _ (weak (lam α F))) (inf-VI-s (ax-10-b {_} {_} {α} {β} {this} {next this} refl refl)))))))))

ax-10-b-s2 {_} {Γ} {α} {β} {F} {G} =
 subst (λ z → (⊢ ((![ α ] (app (weak F) (var this refl) == app (weak G) (var this refl))) => (F == z)))) (sym (sub-weak-p-1' G F)) (
 subst (λ z → (⊢ ((![ α ] (app (weak F) (var this refl) == app z (var this refl))) => (F == sub F (weak G))))) (sym (sub-weak-p-1 G F)) (
 inf-V (ax-5-s ((![ α ] (app (weak (var this refl)) (var this refl) == app (weak (weak G)) (var this refl))) => (var this refl == weak G)) F) (
 inf-VI-s (
 inf-V (ax-5-s ((![ α ] (app (weak (var (next this) refl)) (var this refl) == app (weak (var this refl)) (var this refl))) => (var (next this) refl == var this refl)) (weak G)) (
 inf-VI-s (
 ax-10-b refl refl))))))

ax-11-s {_} {Γ} {α} {F} =
 subst (λ z → ⊢ ((?[ α ] z) => sub (app i (lam α F)) F)) (sub-sub-weak-weak-p-3 F) (
 inf-V (inf-II Γ (α ∷ ε) (λ z → ((?[ α ] z) => sub (app i (lam α F)) F)) (weak-i (α ∷ ε) Γ F) (var this refl)) (
 inf-V (inf-II Γ ε (λ z → ((?[ α ] app (weak (lam α F)) (var this refl)) => z)) F (app i (lam α F))) (
 inf-V (ax-5-s _ (lam α F)) (inf-VI-s (ax-11 {_} {_} {α} {this} refl)))))

ax-1-s {_} {_} {F} = inf-V (ax-5-s ((var this refl || var this refl) => var this refl) F) (inf-VI-s (ax-1 refl))

ax-2-s {_} {_} {F} {G} = subst (λ z → ⊢ (F => (F || z))) (sym (sub-weak-p-1' G F)) (inf-V (ax-5-s (var this refl => (var this refl || weak G)) F) (inf-VI-s (inf-V (ax-5-s (var (next this) refl => (var (next this) refl || var this refl)) (weak G)) (inf-VI-s (ax-2 refl refl)))))

ax-3-s {_} {_} {F} {G} = subst (λ z → ⊢ ((F || z) => (z || F))) (sym (sub-weak-p-1' G F)) (inf-V (ax-5-s _ F) (inf-VI-s (inf-V (ax-5-s _ (weak G)) (inf-VI-s (ax-3 {_} {_} {next this} {this} refl refl)))))

ax-4-s {_} {_} {F} {G} {H} = subst (λ z → ⊢ ((F => G) => ((z || F) => (z || G)))) (sym (sub-weak-p-1' H F)) (subst (λ z → ⊢ ((F => z) => ((sub F (weak H) || F) => (sub F (weak H) || z)))) (sym (sub-weak-p-1' G F)) (subst (λ z → ⊢ ((F => sub F (weak G)) => ((sub F z || F) => (sub F z || sub F (weak G))))) (sym (sub-weak-p-1' (weak H) (weak G))) (inf-V (ax-5-s _ F) (inf-VI-s (inf-V (ax-5-s _ (weak G)) (inf-VI-s (inf-V (ax-5-s _ (weak (weak H))) (inf-VI-s (ax-4 {_} {_} {next (next this)} {next this} {this} refl refl refl)))))))))

ax-10-a-s {_} {_} {F} {G} = subst (λ z → ⊢ ((F <=> z) => (F == z))) (sym (sub-weak-p-1' G F)) (inf-V (ax-5-s _ F) (inf-VI-s (inf-V (ax-5-s _ (weak G)) (inf-VI-s (ax-10-a {_} {_} {next this} {this} refl refl)))))

ax-5-s2 = λ F G → subst (λ z → ⊢ ((![ _ ] ~ (weak F · $ this {refl})) => ~ (z · G))) (sym (sub-weak-p-1' F G)) (ax-5-s (~ (weak F · $ this {refl})) G)

ax-5-s3 = λ F G →
 subst (λ z → ⊢ ((!'[ _ ] F) => (F · z))) (sym (sub-weak-p-1' G F)) (
 inf-V (ax-5-s ((!'[ _ ] ($ this {refl})) => (($ this {refl}) · weak G)) F) (
 inf-VI-s (
 inf-V (ax-5-s ((!'[ _ ] ($ (next this) {refl})) => (($ (next this) {refl}) · ($ this {refl}))) (weak G)) (
 inf-VI-s (
 ax-5 {_} {_} {_} {next this} {this} refl refl)))))

ax-11-s2 F =
 inf-V (ax-5-s ((?'[ _ ] ($ this {refl})) => (($ this {refl}) · ι' _ ($ this {refl}))) F) (
 inf-VI-s (
 ax-11 refl))

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

mutual
 hn-form : ∀ {n} → {Γ : Ctx n} {β : Type n} (F : Form Γ β → Form Γ $o) (G : Form Γ β) (m : ℕ) →
           ⊢ F (headNorm m G) → ⊢ F G
 hn-form F (app G H) m p = hn-form' F G H m (hn-form (λ z → F (headNorm' m z H)) G m p)
 hn-form F (var _ _) m p = p
 hn-form F N m p = p
 hn-form F A m p = p
 hn-form F Π m p = p
 hn-form F i m p = p
 hn-form F (lam _ _) m p = p

 hn-form' : ∀ {n} → {Γ : Ctx n} {α β : Type n} (F : Form Γ β → Form Γ $o) (G : Form Γ (α > β)) (H : Form Γ α) (m : ℕ) →
            ⊢ F (headNorm' m G H) → ⊢ F (app G H)
 hn-form' F (lam α G) H (suc m) p = inf-V (inf-III-samectx F G H) (hn-form F (sub H G) m p)
 hn-form' F (lam α G) H 0 p = p
 hn-form' F (var _ _) H zero p = p
 hn-form' F (var _ _) H (suc _) p = p
 hn-form' F N H zero p = p
 hn-form' F N H (suc _) p = p
 hn-form' F A H zero p = p
 hn-form' F A H (suc _) p = p
 hn-form' F Π H zero p = p
 hn-form' F Π H (suc _) p = p
 hn-form' F i H zero p = p
 hn-form' F i H (suc _) p = p
 hn-form' F (app _ _) H zero p = p
 hn-form' F (app _ _) H (suc _) p = p

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


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

open import Algebra

module Loop.Properties
  {a ℓ} (L : Loop a ℓ) where

open Loop L


text:
-- Load me
module QuotationMark where
open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Agda.Builtin.String

s : List Char
s = ")"

max_stars_repo_name: EdNutting/agda-mode-vscode


text:
-- Andreas, 2017-05-26
-- Expand ellipsis with C-c C-c . RET

open import Agda.Builtin.Nat

test0 : Nat → Nat
test0 x with zero

... | q = {!.!}  -- C-c C-c

-- Expected result:
-- test0 x | q = ?

data Fin : Nat → Set where
  zero : ∀ n → Fin (suc n)
  suc  : ∀{n} → Fin n → Fin (suc n)

test1 : ∀{n} → Fin n → Nat

test1 (zero _) with Nat

... | q = {!.!} -- C-c C-c

-- Expected result:
-- test1 (zero _) | q = ?

test1 {.(suc n)} (suc {n} i) with Fin zero

... | q = {!.!} -- C-c C-c

-- Expected result:
-- test1 {.(suc n)} (suc {n} i) | q = ?

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module Lib.Monad where

open import Lib.Nat
open import Lib.List
open import Lib.IO hiding (IO; mapM)
open import Lib.Maybe
open import Lib.Prelude

infixr 40 _>>=_ _>>_
infixl 90 _<*>_ _<$>_

-- Wrapper type, used to ensure that ElM is constructor-headed.

record IO (A : Set) : Set where
  constructor io
  field unIO : Lib.IO.IO A

open IO

-- State monad transformer

data StateT (S : Set)(M : Set -> Set)(A : Set) : Set where
  stateT : (S -> M (A × S)) -> StateT S M A

runStateT : forall {S M A} -> StateT S M A -> S -> M (A × S)
runStateT (stateT f) = f

-- Reader monad transformer

data ReaderT (E : Set)(M : Set -> Set)(A : Set) : Set where
  readerT : (E -> M A) -> ReaderT E M A

runReaderT : forall {E M A} -> ReaderT E M A -> E -> M A
runReaderT (readerT f) = f

-- The monad class

data Monad : Set1 where
  maybe  : Monad
  list   : Monad
  io     : Monad
  state  : Set -> Monad -> Monad
  reader : Set -> Monad -> Monad

ElM : Monad -> Set -> Set
ElM maybe        = Maybe
ElM list         = List
ElM io           = IO
ElM (state S m)  = StateT S (ElM m)
ElM (reader E m) = ReaderT E (ElM m)

return : {m : Monad}{A : Set} -> A -> ElM m A
return {maybe}      x = just x
return {list}       x = x :: []
return {io}         x = io (returnIO x)
return {state _ m}  x = stateT \s -> return (x , s)
return {reader _ m} x = readerT \_ -> return x

_>>=_ : {m : Monad}{A B : Set} -> ElM m A -> (A -> ElM m B) -> ElM m B
_>>=_ {maybe}     nothing    k = nothing
_>>=_ {maybe}     (just x)   k = k x
_>>=_ {list}      xs         k = foldr (\x ys -> k x ++ ys) [] xs
_>>=_ {io}        (io m)     k = io (bindIO m (unIO ∘ k))
_>>=_ {state S m} (stateT f) k = stateT \s -> f s >>= rest
  where
    rest : _ × _ -> ElM m _
    rest (x , s) = runStateT (k x) s
_>>=_ {reader E m} (readerT f) k = readerT \e -> f e >>= \x -> runReaderT (k x) e

-- State monad class

data StateMonad (S : Set) : Set1 where
  state : Monad -> StateMonad S
  reader : Set -> StateMonad S -> StateMonad S

ElStM : {S : Set} -> StateMonad S -> Monad
ElStM {S} (state m)    = state S m
ElStM     (reader E m) = reader E (ElStM m)

ElSt : {S : Set} -> StateMonad S -> Set -> Set
ElSt m = ElM (ElStM m)

get : {S : Set}{m : StateMonad S} -> ElSt m S
get {m = state m}    = stateT \s -> return (s , s)
get {m = reader E m} = readerT \_ -> get

put : {S : Set}{m : StateMonad S} -> S -> ElSt m Unit
put {m = state m}    s = stateT  \_ -> return (unit , s)
put {m = reader E m} s = readerT \_ -> put s

-- Reader monad class

data ReaderMonad (E : Set) : Set1 where
  reader : Monad -> ReaderMonad E
  state  : Set -> ReaderMonad E -> ReaderMonad E

ElRdM : {E : Set} -> ReaderMonad E -> Monad
ElRdM {E} (reader m)  = reader E m
ElRdM     (state S m) = state S (ElRdM m)

ElRd : {E : Set} -> ReaderMonad E -> Set -> Set
ElRd m = ElM (ElRdM m)

ask : {E : Set}{m : ReaderMonad E} -> ElRd m E
ask {m = reader m } = readerT \e -> return e
ask {m = state S m} = stateT \s -> ask >>= \e -> return (e , s)

local : {E A : Set}{m : ReaderMonad E} -> (E -> E) -> ElRd m A -> ElRd m A
local {m = reader _ } f (readerT m) = readerT \e -> m (f e)
local {m = state S _} f (stateT m)  = stateT \s -> local f (m s)

-- Derived functions

-- Monad operations

_>>_ : {m : Monad}{A B : Set} -> ElM m A -> ElM m B -> ElM m B
m₁ >> m₂ = m₁ >>= \_ -> m₂

_<*>_ : {m : Monad}{A B : Set} -> ElM m (A -> B) -> ElM m A -> ElM m B
mf <*> mx = mf >>= \f -> mx >>= \x -> return (f x)

_<$>_ : {m : Monad}{A B : Set} -> (A -> B) -> ElM m A -> ElM m B
f <$> m = return f <*> m

mapM : {m : Monad}{A B : Set} -> (A -> ElM m B) -> List A -> ElM m (List B)
mapM f []        = return []
mapM f (x :: xs) = _::_ <$> f x <*> mapM f xs

-- State monad operations

modify : {S : Set}{m : StateMonad S} -> (S -> S) -> ElSt m Unit
modify f = get >>= \s -> put (f s)

-- Test

-- foo : Nat -> Maybe (Nat × Nat)
-- foo s = runReaderT (runStateT m s) s
--  where

-- m₁ : StateT Nat (ReaderT Nat Maybe) Nat
-- m₁ = local suc (ask >>= \s -> put (s + 3) >> get)

-- The problem: nested injective function don't seem to work
-- as well as one could hope. In this case:
--   ElM (ElRd ?0) == ReaderT Nat Maybe
-- inverts to
--    ElRd ?0 == reader Nat ?1
--    ElM ?1 == Maybe
-- it seems that the injectivity of ElRd isn't taken into account(?)
-- m : ReaderT Nat Maybe Nat
-- m = ask

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --sized-types #-}

module SizedTypesMergeSort where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

-- sized lists

data List (A : Set) : {_ : Size} -> Set where
  []   : {size : Size} -> List A {size ^}
  _::_ : {size : Size} -> A -> List A {size} -> List A {size ^}

-- CPS split

split : {A : Set}{i : Size} -> List A {i} ->
        {C : Set} -> (List A {i} -> List A {i} -> C) -> C
split []        k = k [] []
split (x :: xs) k = split xs (\ l r -> k (x :: r) l)

module Sort (A : Set) (compare : A -> A -> {B : Set} -> B -> B -> B) where

{- merge is currently rejected by the termination checker
   it would be nice if it worked
   see test/succeed/SizedTypesMergeSort.agda
 -}
  merge : List A -> List A -> List A
  merge [] ys = ys
  merge xs [] = xs
  merge (x :: xs) (y :: ys) =
    compare x y (x :: merge xs (y :: ys))
                (y :: merge (x :: xs) ys)

  sort : {i : Size} -> List A {i} -> List A
  sort [] = []
  sort (x :: []) = x :: []
  sort (x :: (y :: xs)) = split xs (\ l r -> merge (sort (x :: l))
                                                   (sort (y :: r)))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Minimal.NaturalDeduction.Tree (𝔏 : Signature) where
open Signature(𝔏)

open import Data.DependentWidthTree as Tree hiding (height)
import      Lvl
open import Formalization.PredicateLogic.Minimal.NaturalDeduction (𝔏)
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Functional using (_∘_ ; _∘₂_ ; _∘₃_ ; _∘₄_ ; swap ; _←_)
open import Numeral.Finite
open import Numeral.Natural.Relation.Order
open import Numeral.Natural
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇] ; map ; unmap) renaming (•_ to · ; _≡_ to _≡ₛ_)
open import Structure.Relator
open import Type.Properties.Inhabited
open import Type

module _ {vars} ⦃ pos-term : ◊(Term(vars)) ⦄ where
  private variable ℓ : Lvl.Level
  private variable Γ Γ₁ Γ₂ : PredSet{ℓ}(Formula(vars))
  private variable φ ψ γ φ₁ ψ₁ γ₁ φ₂ ψ₂ γ₂ φ₃ ψ₃ φ₄ ψ₄ φ₅ ψ₅ δ₁ δ₂ : Formula(vars)

  {-
  height : Term(_) → (Γ ⊢ φ) → ℕ
  height t (direct p)         = 𝟎
  height t [⊤]-intro          = 𝟎
  height t ([∧]-intro  p q)   = 𝐒((height t p) ⦗ max ⦘ᵣ (height t q))
  height t ([∧]-elimₗ  p)     = 𝐒(height t p)
  height t ([∧]-elimᵣ  p)     = 𝐒(height t p)
  height t ([∨]-introₗ p)     = 𝐒(height t p)
  height t ([∨]-introᵣ p)     = 𝐒(height t p)
  height t ([∨]-elim   p q r) = 𝐒((height t p) ⦗ max ⦘ᵣ (height t q) ⦗ max ⦘ᵣ (height t r))
  height t ([⟶]-intro  p)     = 𝐒(height t p)
  height t ([⟶]-elim   p q)   = 𝐒((height t p) ⦗ max ⦘ᵣ (height t q))
  height t ([Ɐ]-intro  p)     = 𝐒(height t (p{t}))
  height t ([Ɐ]-elim   p)     = 𝐒(height t p)
  height t ([∃]-intro  p)     = 𝐒(height t p)
  height t ([∃]-elim   p q)   = 𝐒((height t (p{t})) ⦗ max ⦘ᵣ (height t q))

  test : ∀{t : Term(n)}{p q : Γ ⊢ φ} → (height t p ≤ height t ([∧]-intro p q))
  test = [≤]-successor max-orderₗ
  -}

  tree : (Γ ⊢ φ) → FiniteTreeStructure
  tree(direct x)         = Node 0 \()
  tree [⊤]-intro         = Node 0 \()
  tree([∧]-intro  p q)   = Node 2 \{𝟎 → tree p; (𝐒 𝟎) → tree q}
  tree([∧]-elimₗ  p)     = Node 1 \{𝟎 → tree p}
  tree([∧]-elimᵣ  p)     = Node 1 \{𝟎 → tree p}
  tree([∨]-introₗ p)     = Node 1 \{𝟎 → tree p}
  tree([∨]-introᵣ p)     = Node 1 \{𝟎 → tree p}
  tree([∨]-elim   p q r) = Node 3 \{𝟎 → tree p ; (𝐒 𝟎) → tree q ; (𝐒(𝐒 𝟎)) → tree r}
  tree([⟶]-intro  p)     = Node 1 \{𝟎 → tree p}
  tree([⟶]-elim   p q)   = Node 2 \{𝟎 → tree p ; (𝐒 𝟎) → tree q}
  tree([Ɐ]-intro  p)     = Node 1 \{𝟎 → tree (p{[◊]-existence})}
  tree([Ɐ]-elim   p)     = Node 1 \{𝟎 → tree p}
  tree([∃]-intro  p)     = Node 1 \{𝟎 → tree p}
  tree([∃]-elim   p q)   = Node 2 \{𝟎 → tree (p{[◊]-existence}) ; (𝐒 𝟎) → tree q}

  height : (Γ ⊢ φ) → ℕ
  height = Tree.height ∘ tree

  open import Data.Tuple as Tuple using (_⨯_ ; _,_)
  import      Functional.Dependent
  open        Functional using (_on₂_)
  open import Numeral.Natural.Induction
  open import Numeral.Natural.Inductions
  open import Numeral.Natural.Relation.Order.Proofs
  open import Structure.Relator.Ordering
  open import Structure.Relator.Ordering.Proofs
  open import Type.Dependent

  -- Ordering of natural deduction proofs on height.
  _<⊢↑_ : Σ(PredSet{ℓ}(Formula(vars)) ⨯ Formula(vars))(Tuple.uncurry(_⊢_)) → Σ(PredSet(Formula(vars)) ⨯ Formula(vars))(Tuple.uncurry(_⊢_)) → Type
  _<⊢↑_ = (_<_) on₂ (height Functional.Dependent.∘ Σ.right)

  instance
    [<⊢↑]-wellfounded : Strict.Properties.WellFounded(_<⊢↑_ {ℓ})
    [<⊢↑]-wellfounded = wellfounded-image-by-trans {f = height Functional.Dependent.∘ Σ.right}

  -- induction-on-height : ∀{P : ∀{Γ : PredSet{ℓₚ}(Formula(vars))}{φ} → (Γ ⊢ φ) → Type{ℓ}} → (∀{x : Prop(vars)} → P(direct x)) → P([⊤]-intro) → (∀{p₂ : Γ ⊢ φ} → (∀{Γ₁}{φ₁}{p₁ : Γ₁ ⊢ φ₁} → (height p₁ < height p₂) → P(p₁)) → P(p₂)) → (∀{p : (Γ ⊢ φ)} → P(p))
  -- induction-on-height {Γ = Γ}{φ = φ} {P = P} dir top step {p} = Strict.Properties.wellfounded-induction(_<⊢↑_) {P = P Functional.Dependent.∘ Σ.right} {!!} {intro (Γ , φ) p}

  -- substitute0-height : ∀{t} → height(substitute0 t φ) ≡

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Categories.Diagram.Limit.Ran where

open import Level
open import Data.Product using (Σ)

open import Categories.Category
open import Categories.Category.Complete
open import Categories.Category.Construction.Cones
open import Categories.Category.Construction.Comma
open import Categories.Category.Construction.Properties.Comma
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Limit.Properties
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≊_)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; module ≃; _ⓘˡ_)
open import Categories.Kan
open import Categories.Diagram.Limit

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

-- construct a Ran from a limit
module _ {o ℓ e o′ ℓ′ e′} {C : Category o′ ℓ′ e′} {D : Category o ℓ e}
         (F : Functor C D) (X : Functor C E) (Com : Complete (o′ ⊔ ℓ) (ℓ′ ⊔ e) e′ E) where
  private
    module C = Category C
    module D = Category D
    module E = Category E
    module F = Functor F
    module X = Functor X
    open Limit
    open Cone renaming (commute to K-commute)
    open Cone⇒ renaming (commute to ⇒-commute)
    open Mor E

    G   : (d : D.Obj) → Functor (d ↙ F) E
    G d   = X ∘F Cod (const! d) F
    ⊤Gd : ∀ d → Limit (G d)
    ⊤Gd d = Com (G d)
    module ⊤Gd d = Limit (⊤Gd d)
    f↙F : ∀ {Y Z} (f : Y D.⇒ Z) → Functor (Z ↙ F) (Y ↙ F)
    f↙F   = along-natˡ′ F

    Gf≃ : ∀ {Y Z} (f : Y D.⇒ Z) → G Z ≃ G Y ∘F f↙F f
    Gf≃ f = record
      { F⇒G = ntHelper record
        { η       = λ _ → X.F₁ C.id
        ; commute = λ _ → [ X ]-resp-square id-comm-sym
        }
      ; F⇐G = ntHelper record
        { η       = λ _ → X.F₁ C.id
        ; commute = λ _ → [ X ]-resp-square id-comm-sym
        }
      ; iso = λ _ → record
        { isoˡ = [ X ]-resp-∘ C.identity² ○ X.identity
        ; isoʳ = [ X ]-resp-∘ C.identity² ○ X.identity
        }
      }
      where open MR C
            open E.HomReasoning

    limY⇒limZ∘ : ∀ {Y Z} (f : Y D.⇒ Z) → Cones (G Y ∘F f↙F f) [ F-map-Coneʳ (f↙F f) (limit (Com (G Y))) , limit (Com (G Y ∘F f↙F f)) ]
    limY⇒limZ∘ {Y} f     = F⇒arr Com (f↙F f) (G Y)
    limZ∘≅limZ : ∀ {Y Z} (f : Y D.⇒ Z) → apex (⊤Gd Z) ≅ apex (Com (G Y ∘F f↙F f))
    limZ∘≅limZ {Y} {Z} f = ≃⇒lim≅ (Gf≃ f) (⊤Gd Z) (Com _)

  limit-is-ran : Ran F X
  limit-is-ran = record
    { R        = R
    ; ε        = ε
    ; δ        = δ
    ; δ-unique = λ {M γ} δ′ eq → δ-unique {M} {γ} δ′ eq
    ; commutes = commutes
    }
    where open MR E
          open E.HomReasoning
          open D.HomReasoning using () renaming (_○_ to _●_ ; ⟺ to ⟷)

          R₀ : D.Obj → E.Obj
          R₀ d = apex (⊤Gd d)
          R₁ : ∀ {A B} → D [ A , B ] → E [ R₀ A , R₀ B ]
          R₁ {A} f = _≅_.to (limZ∘≅limZ f) E.∘ arr (limY⇒limZ∘ f)

          proj-red : ∀ {Y Z} K (f : Y D.⇒ Z) → ⊤Gd.proj Z K E.∘ R₁ f E.≈ ⊤Gd.proj Y (record { f = D.id D.∘ CommaObj.f K D.∘ f })
          proj-red {Y} {Z} K f = begin
            ⊤Gd.proj Z K E.∘ R₁ f                                 ≈⟨ pullˡ (⇒-commute (≃⇒Cone⇒ (≃.sym (Gf≃ f)) (Com _) (⊤Gd Z))) ⟩
            (X.F₁ C.id E.∘ proj (Com _) K) E.∘ arr (limY⇒limZ∘ f) ≈⟨ pullʳ (⇒-commute (limY⇒limZ∘ f)) ⟩
            X.F₁ C.id E.∘ ⊤Gd.proj Y _                            ≈⟨ elimˡ X.identity ⟩
            ⊤Gd.proj Y _                                          ∎

          proj≈ : ∀ {d b} {f g : d D.⇒ F.F₀ b} → f D.≈ g → ⊤Gd.proj d record { f = f } E.≈ ⊤Gd.proj d record { f = g }
          proj≈ {d} {b} {f} {g} eq = begin
            ⊤Gd.proj d _               ≈⟨ introˡ X.identity ⟩
            X.F₁ C.id E.∘ ⊤Gd.proj d _ ≈⟨ K-commute _ (⊤Gd.limit d) (record { h = C.id ; commute = D.∘-resp-≈ F.identity eq ● MR.id-comm-sym D }) ⟩
            ⊤Gd.proj d _               ∎

          R : Functor D E
          R = record
            { F₀           = R₀
            ; F₁           = R₁
            ; identity     = λ {d} → terminal.⊤-id (⊤Gd d) record
              { commute = λ {Z} → begin
                ⊤Gd.proj d Z ∘ R₁ D.id                                   ≈⟨ proj-red Z D.id ⟩
                ⊤Gd.proj d record { f = D.id D.∘ CommaObj.f Z D.∘ D.id } ≈⟨ proj≈ (D.identityˡ ● D.identityʳ) ⟩
                ⊤Gd.proj d Z                                             ∎
              }
            ; homomorphism = λ {Y Z W} {f g} →
              terminal.!-unique₂ (⊤Gd W)
                {let module ⊤GY = Cone _ (⊤Gd.limit Y)
                     module H   = Functor (f↙F (g D.∘ f))
                 in record
                 { apex = record
                   { ψ       = λ K → ⊤GY.ψ (H.F₀ K)
                   ; commute = λ h → ⊤GY.commute (H.F₁ h)
                   }
                 }}
                {record
                  { arr     = R₁ (g D.∘ f)
                  ; commute = λ {K} → proj-red K (g D.∘ f)
                  }}
                {record
                  { arr     = R₁ g ∘ R₁ f
                  ; commute = λ {K} → begin
                    ⊤Gd.proj W K ∘ R₁ g ∘ R₁ f
                      ≈⟨ sym-assoc ⟩
                    (⊤Gd.proj W K ∘ R₁ g) ∘ R₁ f
                      ≈⟨ proj-red K g ⟩∘⟨refl ⟩
                    ⊤Gd.proj Z record { f = D.id D.∘ CommaObj.f K D.∘ g } ∘ R₁ f
                      ≈⟨ proj-red _ f ⟩
                    ⊤Gd.proj Y record { f = D.id D.∘ (D.id D.∘ CommaObj.f K D.∘ g) D.∘ f }
                      ≈⟨ proj≈ (D.identityˡ ● (MR.assoc²' D)) ⟩
                    ⊤Gd.proj Y record { f = D.id D.∘ CommaObj.f K D.∘ g D.∘ f }
                      ∎
                  }}
            ; F-resp-≈     = λ {Y Z} {f g} eq →
              terminal.!-unique₂ (⊤Gd Z)
                {let module ⊤GY = Cone _ (⊤Gd.limit Y)
                     module H = Functor (f↙F f)
                 in record
                    { apex = record
                      { ψ       = λ K → ⊤GY.ψ (H.F₀ K)
                      ; commute = λ h → ⊤GY.commute (H.F₁ h)
                      }
                    }}
                {record
                  { arr     = R₁ f
                  ; commute = F-resp-≈-commute D.Equiv.refl
                  }}
                {record
                  { arr     = R₁ g
                  ; commute = F-resp-≈-commute eq
                  }}
            }
            where open E
                  F-resp-≈-commute : ∀ {Y Z} {K : Category.Obj (Z ↙ F)} {f g : Y D.⇒ Z} → f D.≈ g →
                                       ⊤Gd.proj Z K ∘ R₁ g ≈ ⊤Gd.proj Y record { f = D.id D.∘ CommaObj.f K D.∘ f }
                  F-resp-≈-commute {Y} {Z} {K} {f} {g} eq = begin
                    ⊤Gd.proj Z K ∘ R₁ g ≈⟨ proj-red K g ⟩
                    ⊤Gd.proj Y _        ≈⟨ proj≈ (D.∘-resp-≈ʳ (D.∘-resp-≈ʳ (D.Equiv.sym eq))) ⟩
                    ⊤Gd.proj Y _        ∎

          ε : NaturalTransformation (R ∘F F) X
          ε = ntHelper record
            { η       = λ c → ⊤Gd.proj (F.F₀ c) record { f = D.id }
            ; commute = λ {Y Z} f → begin
              ⊤Gd.proj (F.F₀ Z) _ ∘ Functor.F₁ (R ∘F F) f ≈⟨ proj-red _ (F.F₁ f) ⟩
              ⊤Gd.proj (F.F₀ Y) _                         ≈˘⟨ K-commute _ (⊤Gd.limit (F.F₀ Y)) record { h = f ; commute = ⟷ (D.∘-resp-≈ˡ D.identityˡ ● D.∘-resp-≈ˡ D.identityˡ) } ⟩
              X.F₁ f ∘ ⊤Gd.proj (F.F₀ Y) _                ∎
            }
            where open E

          δ-Cone : ∀ d (M : Functor D E) → NaturalTransformation (M ∘F F) X → Cone (G d)
          δ-Cone d M γ = record
            { apex = record
              { ψ       = λ K → γ.η (CommaObj.β K) E.∘ M.F₁ (CommaObj.f K)
              ; commute = λ {Y Z} f → begin
                X.F₁ (Comma⇒.h f) E.∘ γ.η (CommaObj.β Y) E.∘ M.F₁ (CommaObj.f Y)
                  ≈˘⟨ pushˡ (γ.commute (Comma⇒.h f)) ⟩
                (γ.η (CommaObj.β Z) E.∘ M.F₁ (F.F₁ (Comma⇒.h f))) E.∘ M.F₁ (CommaObj.f Y)
                  ≈⟨ pullʳ ([ M ]-resp-∘ (Comma⇒.commute f ● D.identityʳ)) ⟩
                γ.η (CommaObj.β Z) E.∘ M.F₁ (CommaObj.f Z)
                  ∎
              }
            }
            where module M = Functor M
                  module γ = NaturalTransformation γ

          δ : (M : Functor D E) → NaturalTransformation (M ∘F F) X → NaturalTransformation M R
          δ M γ = ntHelper record
            { η       = λ d → ⊤Gd.rep d (δ-Cone d M γ)
            ; commute = λ {Y Z} f →
              terminal.!-unique₂ (⊤Gd Z)
                {record
                  { apex = record
                    { ψ       = λ W → δ-Cone.ψ Z W E.∘ M.F₁ f
                    ; commute = λ {W V} g → begin
                      X.F₁ (Comma⇒.h g) E.∘ (γ.η (CommaObj.β W) E.∘ M.F₁ (CommaObj.f W)) E.∘ M.F₁ f
                        ≈⟨ E.sym-assoc ⟩
                      (X.F₁ (Comma⇒.h g) E.∘ γ.η (CommaObj.β W) E.∘ M.F₁ (CommaObj.f W)) E.∘ M.F₁ f
                        ≈⟨ δ-Cone.commute Z g ⟩∘⟨refl ⟩
                      (γ.η (CommaObj.β V) E.∘ M.F₁ (CommaObj.f V)) E.∘ M.F₁ f
                        ∎
                    }
                  }}
                {record
                  { arr     = ⊤Gd.rep Z (δ-Cone Z M γ) E.∘ M.F₁ f
                  ; commute = pullˡ (⇒-commute (⊤Gd.rep-cone Z (δ-Cone Z M γ)))
                  }}
                {record
                  { arr     = R₁ f E.∘ ⊤Gd.rep Y (δ-Cone Y M γ)
                  ; commute = λ {W} → begin
                    ⊤Gd.proj Z W E.∘ R₁ f E.∘ ⊤Gd.rep Y (δ-Cone Y M γ)
                      ≈⟨ pullˡ (proj-red W f) ⟩
                    ⊤Gd.proj Y (record { f = D.id D.∘ CommaObj.f W D.∘ f }) E.∘ ⊤Gd.rep Y (δ-Cone Y M γ)
                      ≈⟨ ⇒-commute (⊤Gd.rep-cone Y (δ-Cone Y M γ)) ⟩
                    γ.η (CommaObj.β W) E.∘ M.F₁ (D.id D.∘ CommaObj.f W D.∘ f)
                      ≈˘⟨ refl⟩∘⟨ [ M ]-resp-∘ (⟷ D.identityˡ) ⟩
                    γ.η (CommaObj.β W) E.∘ M.F₁ (CommaObj.f W) E.∘ M.F₁ f
                      ≈⟨ E.sym-assoc ⟩
                    (γ.η (CommaObj.β W) E.∘ M.F₁ (CommaObj.f W)) E.∘ M.F₁ f
                      ∎
                  }}
            }
            where module M        = Functor M
                  module γ        = NaturalTransformation γ
                  module δ-Cone d = Cone _ (δ-Cone d M γ)

          δ-unique : ∀ {M : Functor D E} {α : NaturalTransformation (M ∘F F) X}
                       (δ′ : NaturalTransformation M R) → α ≊ ε ∘ᵥ δ′ ∘ʳ F → δ′ ≊ δ M α
          δ-unique {M} {γ} δ′ eq {d} = ⟺ (⊤Gd.terminal.!-unique d record
            { arr     = δ′.η d
            ; commute = λ {W} → begin
              ⊤Gd.proj d W E.∘ δ′.η d
                ≈˘⟨ proj≈ (D.identityˡ ● D.identityˡ) ⟩∘⟨refl ⟩
              ⊤Gd.proj d (record { f = D.id D.∘ D.id D.∘ CommaObj.f W }) E.∘ δ′.η d
                ≈˘⟨ pullˡ (proj-red _ (CommaObj.f W)) ⟩
              ⊤Gd.proj (F.F₀ (CommaObj.β W)) _ E.∘ R₁ (CommaObj.f W) E.∘ δ′.η d
                ≈˘⟨ pullʳ (δ′.commute (CommaObj.f W)) ⟩
              (⊤Gd.proj (F.F₀ (CommaObj.β W)) (record { f = D.id}) E.∘ δ′.η (F.F₀ (CommaObj.β W))) E.∘ M.F₁ (CommaObj.f W)
                ≈˘⟨ eq ⟩∘⟨refl ⟩
              γ.η (CommaObj.β W) E.∘ M.F₁ (CommaObj.f W)
                ∎
            })
            where module M  = Functor M
                  module γ  = NaturalTransformation γ
                  module δ′ = NaturalTransformation δ′

          commutes : (M : Functor D E) (α : NaturalTransformation (M ∘F F) X) → α ≊ ε ∘ᵥ δ M α ∘ʳ F
          commutes M γ {c} = ⟺ (⇒-commute (⊤Gd.rep-cone (F.F₀ c) (δ-Cone (F.F₀ c) M γ)) ○ elimʳ M.identity)
            where module M  = Functor M
                  module γ  = NaturalTransformation γ

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module regular-language where

open import Level renaming ( suc to Suc ; zero to Zero )
open import Data.List
open import Data.Nat hiding ( _≟_ )
open import Data.Fin hiding ( _+_ )
open import Data.Empty
open import Data.Unit
open import Data.Product
-- open import Data.Maybe
open import  Relation.Nullary
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import nat
open import automaton

language : { Σ : Set } → Set
language {Σ} = List Σ → Bool

language-L : { Σ : Set } → Set
language-L {Σ} = List (List Σ)

Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Union {Σ} A B x = (A x ) \/ (B x)

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] /\ y []
split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Concat {Σ} A B = split A B

{-# TERMINATING #-}
Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
Star {Σ} A [] = true
Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t)

open import automaton-ex

test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
       ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  )
   )
test-AB→split {_} {A} {B} = refl

star-nil : {Σ : Set} → ( A : language {Σ} ) → Star A [] ≡ true
star-nil A = refl

open Automaton
open import finiteSet
open import finiteSetUtil

record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
   field
      states : Set
      astart : states
      afin : FiniteSet states
      automaton : Automaton states Σ
   contain : List Σ → Bool
   contain x = accept automaton astart x

open RegularLanguage

isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
isRegular A x r = A x ≡ contain r x

RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ  → language {Σ}
RegularLanguage-is-language {Σ} R = RegularLanguage.contain R

RegularLanguage-is-language' : { Σ : Set } → RegularLanguage Σ  → List Σ  → Bool
RegularLanguage-is-language' {Σ} R x = accept (automaton R) (astart R) x where
   open RegularLanguage

--  a language is implemented by an automaton

-- postulate
--   fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}

M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
M-Union {Σ} A B = record {
       states =  states A × states B
     ; astart = ( astart A , astart B )
     ; afin = fin-× (afin A) (afin B)
     ; automaton = record {
             δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
           ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
        }
   }

closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
closed-in-union A B [] = lemma where
   lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
           aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
   lemma = refl
closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
   lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
     accept (automaton A) qa t \/ accept (automaton B) qb  t
       ≡ accept (automaton (M-Union A B)) (qa , qb) t
   lemma1 [] qa qb = refl
   lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Truncation.FromNegTwo where

open import Cubical.HITs.Truncation.FromNegTwo.Base public
open import Cubical.HITs.Truncation.FromNegTwo.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
open import Empty

module Boolean where

  data Bool : Set where
    true : Bool
    false : Bool

  {-# BUILTIN BOOL Bool #-}
  {-# BUILTIN TRUE true #-}
  {-# BUILTIN FALSE false #-}

  T : Bool → Set
  T true = ⊤
  T false = ⊥

  not : Bool → Bool
  not true = false
  not false = true

  and : Bool → Bool → Bool
  and true true = true
  and _ _ = false

  or : Bool → Bool → Bool
  or false false = false
  or _ _ = true

  xor : Bool → Bool → Bool
  xor false true = true
  xor true false = true
  xor _ _ = false

  infixr 6 _∧_
  infixr 5 _∨_

  ¬_ : Set → Set
  ¬ A = A → ⊥

  data _∨_ A B : Set where
    Inl : A → A ∨ B
    Inr : B → A ∨ B

  data _∧_ A B : Set where
    Conj : A → B → A ∧ B

  _⇔_ : (P : Set) → (Q : Set) → Set
  a ⇔ b = (a → b) ∧ (b → a)

  ∧-symmetry : ∀ { A B : Set } → A ∧ B → B ∧ A
  ∧-symmetry (Conj x y) = Conj y x

  ∨-symmetry : ∀ { A B : Set } → A ∨ B → B ∨ A
  ∨-symmetry (Inl x) = Inr x
  ∨-symmetry (Inr y) = Inl y

  and_over : { A B C : Set } → A ∧ ( B ∨ C ) → ( A ∧ B ) ∨ ( A ∧ C )
  and_over (Conj x (Inl y)) = Inl (Conj x y)
  and_over (Conj x (Inr y)) = Inr (Conj x y)

  and_over' : { A B C : Set } → ( A ∧ B ) ∨ ( A ∧ C ) → A ∧ ( B ∨ C )
  and_over' (Inl (Conj x y)) = Conj x (Inl y)
  and_over' (Inr (Conj x y)) = Conj x (Inr y)

  or_over : { A B C : Set } → A ∨ ( B ∧ C ) → ( A ∨ B ) ∧ ( A ∨ C )
  or_over (Inl x) = Conj (Inl x) (Inl x)
  or_over (Inr (Conj x y)) = Conj (Inr x) (Inr y)

  or_over' : { A B C : Set } → ( A ∨ B ) ∧ ( A ∨ C ) → A ∨ ( B ∧ C )
  or_over' (Conj (Inl x) _) = Inl x
  or_over' (Conj _ (Inl y)) = Inl y
  or_over' (Conj (Inr x) (Inr y)) = Inr (Conj x y)

  or_over_negated : { A B : Set } → ( A ∨ ( ¬ A ∧ B ) ) → ( A ∨ B )
  or_over_negated (Inl x) = Inl x
  or_over_negated (Inr (Conj _ y)) = Inr y

  private
    proof₁ : { P Q : Set } → (P ∧ Q) → P
    proof₁ (Conj p q) = p

    proof₂ : { P Q : Set } → (P ∧ Q) → Q
    proof₂ (Conj p q) = q

  deMorgan₁ : { A B : Set } → ¬ A ∧ ¬ B → ¬ (A ∨ B)
  deMorgan₁ (Conj ¬x ¬y) (Inl x) = ¬x x
  deMorgan₁ (Conj ¬x ¬y) (Inr y) = ¬y y
  -- above is clearer if you re-write the type annotation as:
  --deMorgan₁ : { A B : Set } → (A → ⊥) ∧ (B → ⊥) → (A ∨ B) → ⊥

  deMorgan₂ : { A B : Set } → ¬ (A ∨ B) → ¬ A ∧ ¬ B
  deMorgan₂ z = Conj (λ x → z (Inl x)) (λ y → z (Inr y))

  deMorgan₃ : { A B : Set } → ¬ A ∨ ¬ B → ¬ (A ∧ B)
  deMorgan₃ (Inl ¬x) (Conj x _) = ¬x x
  deMorgan₃ (Inr ¬y) (Conj _ y) = ¬y y

  -- NOT provable.
  -- deMorgan₄ : { A B : Set } → ¬ (A ∧ B) → ¬ A ∨ ¬ B

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


text:
-- Andreas, 2016-12-30, issues #555 and #1886, reported by nad

-- Hidden parameters can be omitted in the repetition
-- of the parameter list.

record R {a} (A : Set a) : Set a

record R A where
  constructor c
  field f : A

testR : ∀{a}{A : Set a}(x : A) → R A
testR x = c x

data D {a} (A : Set a) : Set a

data D A where
  c : A → D A

testD : ∀{a}{A : Set a}(x : A) → D A
testD x = c x

-- Now, c is overloaded, should still work.
testR' : ∀{a}{A : Set a}(x : A) → R A
testR' x = c x


text:
{-# OPTIONS --no-print-pattern-synonyms #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data Fin : Nat → Set where
  fzero : ∀ {n} → Fin (suc n)
  fsuc  : ∀ {n} → Fin n → Fin (suc n)

pattern #1 = fsuc fzero

prf : (i : Fin 2) → i ≡ #1
prf i = refl  -- should say i != fsuc fzero


text:
module Numeral.Sign where

import      Lvl
open import Type

-- The set of plus or minus sign
data +|− : Type{Lvl.𝟎} where
  ➕ : (+|−)
  ➖ : (+|−)

−|+ = +|−

elim₂ : ∀{ℓ}{P : (+|−) → Type{ℓ}} → P(➖) → P(➕) → ((s : (+|−)) → P(s))
elim₂ neg pos ➖ = neg
elim₂ neg pos ➕ = pos

-- The set of signs: plus, minus and neutral
data +|0|− : Type{Lvl.𝟎} where
  ➕ : (+|0|−)
  𝟎 : (+|0|−)
  ➖ : (+|0|−)

−|0|+ = +|0|−

elim₃ : ∀{ℓ}{P : (+|0|−) → Type{ℓ}} → P(➖) → P(𝟎) → P(➕) → ((s : (+|0|−)) → P(s))
elim₃ neg zero pos ➖ = neg
elim₃ neg zero pos 𝟎 = zero
elim₃ neg zero pos ➕ = pos

zeroable : (+|−) → (+|0|−)
zeroable (➕) = (➕)
zeroable (➖) = (➖)


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRules as SafetyRules
import      LibraBFT.Impl.Consensus.TestUtils.MockStorage   as MockStorage
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.MetricsSafetyRules where

module performInitialize
  (self : SafetyRules)
  (obmPersistentLivenessStorage : PersistentLivenessStorage)
  where

  step₀ : EitherD ErrLog SafetyRules
  step₁ : EpochChangeProof → EitherD ErrLog SafetyRules

  step₀ = do
    let consensusState = SafetyRules.consensusState self
        srWaypoint     = consensusState ^∙ csWaypoint
    proofs             ← MockStorage.retrieveEpochChangeProofED
                           (srWaypoint ^∙ wVersion) obmPersistentLivenessStorage
    step₁ proofs
  step₁ proofs = SafetyRules.initialize-ed-abs self proofs

abstract
  performInitialize-ed-abs = performInitialize.step₀
  performInitialize-abs : SafetyRules → PersistentLivenessStorage → Either ErrLog SafetyRules
  performInitialize-abs sr storage = toEither $ performInitialize-ed-abs sr storage
  performInitialize-abs-≡ : (sr : SafetyRules) (storage : PersistentLivenessStorage)
                          → performInitialize-abs sr storage ≡ EitherD-run (performInitialize-ed-abs sr storage)
  performInitialize-abs-≡ sr storage = refl


text:
-- Andreas, 2011-10-04, transcription of Dan Doel's post on the Agda list
{-# OPTIONS --experimental-irrelevance #-}
module IrrelevantMatchRefl where

import Common.Level
open import Common.Equality hiding (subst)

-- irrelevant subst should be rejected, because it suggests
-- that the equality proof is irrelevant also for reduction
subst : ∀ {i j}{A : Set i}(P : A → Set j){a b : A} → .(a ≡ b) → P a → P b
subst P refl x = x

postulate
  D   : Set
  lie : (D → D) ≡ D

-- the following two substs may not reduce! ...
abs : (D → D) → D
abs f = subst (λ T → T) lie f

app : D → D → D
app d = subst (λ T → T) (sym lie) d

ω : D
ω = abs (λ d → app d d)

-- ... otherwise Ω loops
Ω : D
Ω = app ω ω

-- ... and this would be a real fixed-point combinator
Y : (D → D) → D
Y f = app δ δ
  where δ = abs (λ x → f (app x x))

K : D → D
K x = abs (λ y → x)

K∞ : D
K∞ = Y K

mayloop : K∞ ≡ abs (λ y → K∞)
mayloop = refl
-- gives error D != D → D

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda