text:
module Esterel.Lang.CanFunction.MergePotentialRuleLeftInductive where

open import utility
  renaming (_U̬_ to _∪_ ; _|̌_ to _-_)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Base
open import Esterel.Lang.CanFunction.CanThetaContinuation
open import Esterel.Lang.CanFunction.MergePotentialRuleCan
open import Esterel.Lang.CanFunction.MergePotentialRuleLeftBase
open import Esterel.Context
  using (EvaluationContext1 ; EvaluationContext ; _⟦_⟧e ; _≐_⟦_⟧e)
open import Esterel.Context.Properties
  using (plug ; unplug)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
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 EvaluationContext1
open _≐_⟦_⟧e

open import Data.Bool
  using (Bool ; not ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; _++_ ; map ; concatMap ; foldr)
open import Data.List.Properties
  using (map-id)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_)
open import Data.Nat.Properties.Simple
  using (+-comm)
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.Nullary.Decidable
  using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; _≢_ ; refl ; trans ; sym ; cong ; subst ; module ≡-Reasoning)

open ListSet Data.Nat._≟_
  using (set-subtract ; set-subtract-[] ; set-subtract-split ; set-subtract-merge
       ; set-subtract-notin
       ; set-remove ; set-remove-mono-∈ ; set-remove-removed ; set-remove-not-removed
       ; set-subtract-[a]≡set-remove)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ≡-Reasoning

canθₖ-mergeˡ-E-induction : ∀ {E E⟦nothin⟧ BV FV A} sigs' shrs' vars' r θ →
  E⟦nothin⟧ ≐ E ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧ BV FV →
  distinct' (SigMap.keys sigs') (proj₁ FV) →
    Canθₖ sigs' 0 (E ⟦ r ⟧e) θ ≡
    Canₖ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ

canθₖ-mergeˡ-sigs-induction : ∀ {E E⟦nothin⟧ BV FV A} sigs S sigs' shrs' vars' r θ →
  E⟦nothin⟧ ≐ E ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧ BV FV →
  distinct' (SigMap.keys sigs') (proj₁ FV) →
  ∀ k →
    k ∈ proj₁ (proj₂ (Canθ' sigs S (Canθ sigs' 0 (E ⟦ r ⟧e)) θ)) →
    k ∈ Canθₖ sigs S (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ

canθₛ-mergeˡ-E-induction : ∀ {E E⟦nothin⟧ BV FV A} sigs' shrs' vars' r θ →
  E⟦nothin⟧ ≐ E ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧ BV FV →
  distinct' (SigMap.keys sigs') (proj₁ FV) →
  ∀ S' →
    S' ∉ SigMap.keys sigs' →
    S' ∈ Canθₛ sigs' 0 (E ⟦ r ⟧e) θ →
    S' ∈ Canₛ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
canθₛ-mergeˡ-E-induction {[]} sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ =
    set-subtract-notin S'∈canθ-sigs'-E⟦r⟧-θ S'∉sigs'
canθₛ-mergeˡ-E-induction {epar₁ q ∷ E} {A = A} sigs' shrs' vars' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar cbp _ _ _ _ _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  rewrite Env.←-comm Env.[]env θ distinct-empty-left
  with canθₛ-mergeˡ-E-induction-base-par₁ sigs' 0 r θ Env.[]env (depar₁ E⟦nothin⟧) cb
         (subst (distinct' _)
           (sym (map-id (SigMap.keys sigs')))
           (distinct'-sym sigs'≠FV))
         S' S'∈canθ-sigs'-E⟦r⟧-θ
... | inj₁ S'∈canθ'-sigs'-E⟦r⟧-θ←[] =
  ++ˡ (canθₛ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
        E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
        S' S'∉sigs' S'∈canθ'-sigs'-E⟦r⟧-θ←[])
... | inj₂ S'∈can-q-θ←[] =
  ++ʳ (Canₛ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
    S'∈can-q-θ←[]
canθₛ-mergeˡ-E-induction {epar₂ p ∷ E} sigs' shrs' vars' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  rewrite Env.←-comm Env.[]env θ distinct-empty-left
  with canθₛ-mergeˡ-E-induction-base-par₂ sigs' 0 r θ Env.[]env (depar₂ E⟦nothin⟧) cb
         (subst (distinct' _)
           (sym (map-id (SigMap.keys sigs')))
           (distinct'-sym sigs'≠FV))
         S' S'∈canθ-sigs'-E⟦r⟧-θ
... | inj₁ S'∈canθ'-sigs'-E⟦r⟧-θ←[] =
  ++ʳ (Canₛ p (θ ← Env.[]env))
      (canθₛ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
        E⟦nothin⟧ cbq (dist'++ʳ {V2 = proj₁ FVp} sigs'≠FV)
        S' S'∉sigs' S'∈canθ'-sigs'-E⟦r⟧-θ←[])
... | inj₂ S'∈can-q-θ←[] =
  ++ˡ S'∈can-q-θ←[]
canθₛ-mergeˡ-E-induction {eseq q ∷ E} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp _ _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  rewrite Env.←-comm Env.[]env θ distinct-empty-left
  with canθₛ-mergeˡ-E-induction-base-seq sigs' 0 r θ Env.[]env (deseq E⟦nothin⟧) cb
         (subst (distinct' _)
           (sym (map-id (SigMap.keys sigs')))
           (distinct'-sym sigs'≠FV))
         S' S'∈canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-E-induction {eseq q ∷ E} {A = A} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp _ _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  | inj₁ S'∈canθ'-sigs'-E⟦r⟧-θ←[]
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
... | yes nothin∈can-E⟦ρΘ⟧-θ←[] =
  ++ˡ (canθₛ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
        E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
        S' S'∉sigs' S'∈canθ'-sigs'-E⟦r⟧-θ←[])
... | no  nothin∉can-E⟦ρΘ⟧-θ←[] =
  canθₛ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
    E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
    S' S'∉sigs' S'∈canθ'-sigs'-E⟦r⟧-θ←[]
canθₛ-mergeˡ-E-induction {eseq q ∷ E} {A = A} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp _ _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  | inj₂ (S'∈can-q-θ←[] , nothin∈canθ-sigs'-E⟦r⟧-θ←[])
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
... | yes nothin∈can-E⟦ρΘ⟧-θ←[] =
  ++ʳ (Canₛ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
    S'∈can-q-θ←[]
... | no  nothin∉can-E⟦ρΘ⟧-θ←[]
  rewrite canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r (θ ← Env.[]env)
            E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
  = ⊥-elim (nothin∉can-E⟦ρΘ⟧-θ←[] nothin∈canθ-sigs'-E⟦r⟧-θ←[])
canθₛ-mergeˡ-E-induction {eloopˢ q ∷ E} sigs' shrs' vars' r θ
  (deloopˢ E⟦nothin⟧) cb@(CBloopˢ cbp cbq _ _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  rewrite unfold sigs' 0 (loopˢ (E ⟦ r ⟧e) q) θ
        | sym (unfold sigs' 0 (E ⟦ r ⟧e) θ)
  = canθₛ-mergeˡ-E-induction sigs' shrs' vars' r θ E⟦nothin⟧ cbp
      (dist'++ˡ sigs'≠FV)
      S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-E-induction {esuspend S ∷ E} sigs' shrs' vars' r θ
  (desuspend E⟦nothin⟧) cb@(CBsusp cb' _) sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  rewrite unfold sigs' 0 (suspend (E ⟦ r ⟧e) S) θ
        | sym (unfold sigs' 0 (E ⟦ r ⟧e) θ)
  = canθₛ-mergeˡ-E-induction sigs' shrs' vars' r θ E⟦nothin⟧ cb'
      (dist'++ʳ {V2 = Signal.unwrap S ∷ []} sigs'≠FV)
      S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-E-induction {etrap ∷ E} sigs' shrs' vars' r θ
  (detrap E⟦nothin⟧) cb@(CBtrap cb') sigs'≠FV
  S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ
  rewrite unfold sigs' 0 (trap (E ⟦ r ⟧e)) θ
        | canθ'-map-comm (map Code.↓*) sigs' 0 (Can (E ⟦ r ⟧e)) θ
        | sym (unfold sigs' 0 (E ⟦ r ⟧e) θ)
  = canθₛ-mergeˡ-E-induction sigs' shrs' vars' r θ E⟦nothin⟧ cb' sigs'≠FV
      S' S'∉sigs' S'∈canθ-sigs'-E⟦r⟧-θ

canθₛ-mergeˡ-sigs-induction : ∀ {E E⟦nothin⟧ BV FV A} sigs S sigs' shrs' vars' r θ →
  E⟦nothin⟧ ≐ E ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧ BV FV →
  distinct' (SigMap.keys sigs') (proj₁ FV) →
  ∀ S' →
    S' ∉ SigMap.keys sigs' →
    S' ∈ proj₁ (Canθ' sigs S (Canθ sigs' 0 (E ⟦ r ⟧e)) θ) →
    S' ∈ Canθₛ sigs S (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
canθₛ-mergeˡ-sigs-induction [] S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛ-mergeˡ-E-induction sigs' shrs' vars'
      r θ E⟦nothin⟧ cb sigs'≠FV
      S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-sigs-induction (nothing ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r θ E⟦nothin⟧ cb sigs'≠FV
      S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-sigs-induction (just Signal.present ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-present (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-sigs-induction (just Signal.absent ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛ-mergeˡ-sigs-induction {E} {A = A} (just Signal.unknown ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
  with any (_≟_ S) (proj₁
                     (Canθ' sigs (suc S) (Canθ sigs' 0 (E ⟦ r ⟧e))
                       (θ ← [S]-env (S ₛ))))
     | any (_≟_ S) (proj₁
                     (Canθ sigs (suc S) (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e)
                       (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | yes S∈canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
... | no  S∉canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | no  S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
... | no  S∉canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | yes S∈canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₛ-add-sig-monotonic sigs (suc S) (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
    (S ₛ) Signal.absent S'
    (canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      S' S'∉sigs' S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ)
... | yes S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | no  S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S]
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs' =
  canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    S' S'∉sigs'
    (subst (S' ∈_)
      (cong proj₁
        (trans
          (canθ'-inner-shadowing-irr sigs (suc S) sigs' (E ⟦ r ⟧e)
            S Signal.unknown θ S∈sigs')
          (sym (canθ'-inner-shadowing-irr sigs (suc S) sigs' (E ⟦ r ⟧e)
                 S Signal.absent θ S∈sigs'))))
      S'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ)
... | no  S∉sigs' =
  ⊥-elim
    (S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S]
      (canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
        r (θ ← [S]-env (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
        S S∉sigs' S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S]))

canθₛₕ-mergeˡ-E-induction : ∀ {E E⟦nothin⟧ BV FV A} sigs' shrs' vars' r θ →
  E⟦nothin⟧ ≐ E ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧ BV FV →
  distinct' (SigMap.keys sigs') (proj₁ FV) →
  ∀ s' →
    s' ∉ ShrMap.keys shrs' →
    s' ∈ Canθₛₕ sigs' 0 (E ⟦ r ⟧e) θ →
    s' ∈ Canₛₕ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
canθₛₕ-mergeˡ-E-induction {[]} sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ =
    set-subtract-notin s'∈canθ-sigs'-E⟦r⟧-θ s'∉shrs'
canθₛₕ-mergeˡ-E-induction {epar₁ q ∷ E} {A = A} sigs' shrs' vars' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar cbp _ _ _ _ _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  rewrite Env.←-comm Env.[]env θ distinct-empty-left
  with canθₛₕ-mergeˡ-E-induction-base-par₁ sigs' 0 r θ Env.[]env (depar₁ E⟦nothin⟧) cb
         (subst (distinct' _)
           (sym (map-id (SigMap.keys sigs')))
           (distinct'-sym sigs'≠FV))
         s' s'∈canθ-sigs'-E⟦r⟧-θ
... | inj₁ s'∈canθ'-sigs'-E⟦r⟧-θ←[] =
  ++ˡ (canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
        E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
        s' s'∉shrs' s'∈canθ'-sigs'-E⟦r⟧-θ←[])
... | inj₂ s'∈can-q-θ←[] =
  ++ʳ (Canₛₕ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
    s'∈can-q-θ←[]
canθₛₕ-mergeˡ-E-induction {epar₂ p ∷ E} sigs' shrs' vars' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  rewrite Env.←-comm Env.[]env θ distinct-empty-left
  with canθₛₕ-mergeˡ-E-induction-base-par₂ sigs' 0 r θ Env.[]env (depar₂ E⟦nothin⟧) cb
         (subst (distinct' _)
           (sym (map-id (SigMap.keys sigs')))
           (distinct'-sym sigs'≠FV))
         s' s'∈canθ-sigs'-E⟦r⟧-θ
... | inj₁ s'∈canθ'-sigs'-E⟦r⟧-θ←[] =
  ++ʳ (Canₛₕ p (θ ← Env.[]env))
      (canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
        E⟦nothin⟧ cbq (dist'++ʳ {V2 = proj₁ FVp} sigs'≠FV)
        s' s'∉shrs' s'∈canθ'-sigs'-E⟦r⟧-θ←[])
... | inj₂ s'∈can-q-θ←[] =
  ++ˡ s'∈can-q-θ←[]
canθₛₕ-mergeˡ-E-induction {eseq q ∷ E} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp _ _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  rewrite Env.←-comm Env.[]env θ distinct-empty-left
  with canθₛₕ-mergeˡ-E-induction-base-seq sigs' 0 r θ Env.[]env (deseq E⟦nothin⟧) cb
         (subst (distinct' _)
           (sym (map-id (SigMap.keys sigs')))
           (distinct'-sym sigs'≠FV))
         s' s'∈canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-E-induction {eseq q ∷ E} {A = A} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp _ _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  | inj₁ s'∈canθ'-sigs'-E⟦r⟧-θ←[]
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
... | yes nothin∈can-E⟦ρΘ⟧-θ←[] =
  ++ˡ (canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
        E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
        s' s'∉shrs' s'∈canθ'-sigs'-E⟦r⟧-θ←[])
... | no  nothin∉can-E⟦ρΘ⟧-θ←[] =
  canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r (θ ← Env.[]env)
    E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
    s' s'∉shrs' s'∈canθ'-sigs'-E⟦r⟧-θ←[]
canθₛₕ-mergeˡ-E-induction {eseq q ∷ E} {A = A} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp _ _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  | inj₂ (s'∈can-q-θ←[] , nothin∈canθ-sigs'-E⟦r⟧-θ←[])
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
... | yes nothin∈can-E⟦ρΘ⟧-θ←[] =
  ++ʳ (Canₛₕ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) (θ ← Env.[]env))
    s'∈can-q-θ←[]
... | no  nothin∉can-E⟦ρΘ⟧-θ←[]
  rewrite canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r (θ ← Env.[]env)
            E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
  = ⊥-elim (nothin∉can-E⟦ρΘ⟧-θ←[] nothin∈canθ-sigs'-E⟦r⟧-θ←[])
canθₛₕ-mergeˡ-E-induction {eloopˢ q ∷ E} sigs' shrs' vars' r θ
  (deloopˢ E⟦nothin⟧) cb@(CBloopˢ cbp cbq _ _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  rewrite unfold sigs' 0 (loopˢ (E ⟦ r ⟧e) q) θ
        | sym (unfold sigs' 0 (E ⟦ r ⟧e) θ)
  = canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r θ E⟦nothin⟧ cbp
      (dist'++ˡ sigs'≠FV)
      s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-E-induction {esuspend S ∷ E} sigs' shrs' vars' r θ
  (desuspend E⟦nothin⟧) cb@(CBsusp cb' _) sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  rewrite unfold sigs' 0 (suspend (E ⟦ r ⟧e) S) θ
        | sym (unfold sigs' 0 (E ⟦ r ⟧e) θ)
  = canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r θ E⟦nothin⟧ cb'
      (dist'++ʳ {V2 = Signal.unwrap S ∷ []} sigs'≠FV)
      s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-E-induction {etrap ∷ E} sigs' shrs' vars' r θ
  (detrap E⟦nothin⟧) cb@(CBtrap cb') sigs'≠FV
  s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ
  rewrite unfold sigs' 0 (trap (E ⟦ r ⟧e)) θ
        | canθ'-map-comm (map Code.↓*) sigs' 0 (Can (E ⟦ r ⟧e)) θ
        | sym (unfold sigs' 0 (E ⟦ r ⟧e) θ)
  = canθₛₕ-mergeˡ-E-induction sigs' shrs' vars' r θ E⟦nothin⟧ cb' sigs'≠FV
      s' s'∉shrs' s'∈canθ-sigs'-E⟦r⟧-θ

canθₛₕ-mergeˡ-sigs-induction : ∀ {E E⟦nothin⟧ BV FV A} sigs S sigs' shrs' vars' r θ →
  E⟦nothin⟧ ≐ E ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧ BV FV →
  distinct' (SigMap.keys sigs') (proj₁ FV) →
  ∀ s' →
    s' ∉ ShrMap.keys shrs' →
    s' ∈ proj₂ (proj₂ (Canθ' sigs S (Canθ sigs' 0 (E ⟦ r ⟧e)) θ)) →
    s' ∈ Canθₛₕ sigs S (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
canθₛₕ-mergeˡ-sigs-induction [] S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛₕ-mergeˡ-E-induction sigs' shrs' vars'
      r θ E⟦nothin⟧ cb sigs'≠FV
      s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-sigs-induction (nothing ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r θ E⟦nothin⟧ cb sigs'≠FV
      s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-sigs-induction (just Signal.present ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-present (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-sigs-induction (just Signal.absent ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₛₕ-mergeˡ-sigs-induction {E} {A = A} (just Signal.unknown ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
  with any (_≟_ S) (proj₁
                     (Canθ' sigs (suc S) (Canθ sigs' 0 (E ⟦ r ⟧e))
                       (θ ← [S]-env (S ₛ))))
     | any (_≟_ S) (proj₁
                     (Canθ sigs (suc S) (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e)
                       (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | yes S∈canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
... | no  S∉canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | no  S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
... | no  S∉canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | yes S∈canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₛₕ-add-sig-monotonic sigs (suc S) (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
    (S ₛ) Signal.absent s'
    (canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      s' s'∉shrs' s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ)
... | yes S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | no  S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S]
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs' =
  canθₛₕ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    s' s'∉shrs'
    (subst (s' ∈_)
      (cong (proj₂ ∘ proj₂)
        (trans
          (canθ'-inner-shadowing-irr sigs (suc S) sigs' (E ⟦ r ⟧e)
            S Signal.unknown θ S∈sigs')
          (sym (canθ'-inner-shadowing-irr sigs (suc S) sigs' (E ⟦ r ⟧e)
                 S Signal.absent θ S∈sigs'))))
      s'∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ)
... | no  S∉sigs' =
  ⊥-elim
    (S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S]
      (canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
        r (θ ← [S]-env (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
        S S∉sigs' S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S]))

canθₖ-mergeˡ-E-induction {[]} sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV =
    refl
canθₖ-mergeˡ-E-induction {epar₁ q ∷ E} sigs' shrs' vars' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar cbp cbq _ _ _ _) sigs'≠FV
  rewrite canθₖ-mergeˡ-E-induction-base-par₁ sigs' 0 r θ
            (depar₁ E⟦nothin⟧) cb
            (subst (distinct' _)
              (sym (map-id (SigMap.keys sigs')))
              (distinct'-sym sigs'≠FV))
        | canθₖ-mergeˡ-E-induction sigs' shrs' vars' r θ
            E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV)
  = refl
canθₖ-mergeˡ-E-induction {epar₂ p ∷ E} sigs' shrs' vars' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbp cbq _ _ _ _) sigs'≠FV
  rewrite canθₖ-mergeˡ-E-induction-base-par₂ sigs' 0 r θ
            (depar₂ E⟦nothin⟧) cb
            (subst (distinct' _)
              (sym (map-id (SigMap.keys sigs')))
              (distinct'-sym sigs'≠FV))
        | canθₖ-mergeˡ-E-induction sigs' shrs' vars' r θ
            E⟦nothin⟧ cbq (dist'++ʳ {V2 = proj₁ FVp} sigs'≠FV)
  = refl
canθₖ-mergeˡ-E-induction {eseq q ∷ E} {A = A} sigs' shrs' vars' r θ
  (deseq E⟦nothin⟧) cb@(CBseq cbp cbq _) sigs'≠FV
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ)
... | no nothin∉can-E⟦ρΘ⟧-θ
  rewrite sym (canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r θ
                E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV))
        | canθₖ-mergeˡ-E-induction-base-seq-notin sigs' 0 r θ
            (deseq E⟦nothin⟧) cb
            (subst (distinct' _)
              (sym (map-id (SigMap.keys sigs')))
              (distinct'-sym sigs'≠FV))
            nothin∉can-E⟦ρΘ⟧-θ
  = refl
... | yes nothin∈can-E⟦ρΘ⟧-θ
  rewrite sym (canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r θ
                E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV))
        | canθₖ-mergeˡ-E-induction-base-seq-in sigs' 0 r θ
            (deseq E⟦nothin⟧) cb
            (subst (distinct' _)
              (sym (map-id (SigMap.keys sigs')))
              (distinct'-sym sigs'≠FV))
            nothin∈can-E⟦ρΘ⟧-θ
  = refl
canθₖ-mergeˡ-E-induction {eloopˢ q ∷ E} {A = A} sigs' shrs' vars' r θ
  (deloopˢ E⟦nothin⟧) cb@(CBloopˢ cbp cbq _ _) sigs'≠FV
  rewrite sym (canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r θ
                E⟦nothin⟧ cbp (dist'++ˡ sigs'≠FV))
        | unfold sigs' 0 (loopˢ (E ⟦ r ⟧e) q) θ
        | unfold sigs' 0 (E ⟦ r ⟧e) θ
  = refl
canθₖ-mergeˡ-E-induction {esuspend S ∷ E} {A = A} sigs' shrs' vars' r θ
  (desuspend E⟦nothin⟧) cb@(CBsusp cb' _) sigs'≠FV
  rewrite sym (canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r θ
                E⟦nothin⟧ cb' (dist'++ʳ {V2 = Signal.unwrap S ∷ []} sigs'≠FV))
        | unfold sigs' 0 (suspend (E ⟦ r ⟧e) S) θ
        | unfold sigs' 0 (E ⟦ r ⟧e) θ
  = refl
canθₖ-mergeˡ-E-induction {etrap ∷ E} {A = A} sigs' shrs' vars' r θ
  (detrap E⟦nothin⟧) cb@(CBtrap cb') sigs'≠FV
  rewrite sym (canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars' r θ E⟦nothin⟧ cb' sigs'≠FV)
        | unfold sigs' 0 (trap (E ⟦ r ⟧e)) θ
        | unfold sigs' 0 (E ⟦ r ⟧e) θ
        | canθ'-map-comm (map Code.↓*) sigs' 0 (Can (E ⟦ r ⟧e)) θ
  = refl

canθₖ-mergeˡ-sigs-induction {A = A} [] S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
  rewrite canθₖ-mergeˡ-E-induction {A = A} sigs' shrs' vars'
            r θ E⟦nothin⟧ cb sigs'≠FV
  = k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₖ-mergeˡ-sigs-induction (nothing ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r θ E⟦nothin⟧ cb sigs'≠FV
      k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₖ-mergeˡ-sigs-induction (just Signal.present ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-present (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₖ-mergeˡ-sigs-induction (just Signal.absent ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ =
    canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
canθₖ-mergeˡ-sigs-induction {E} {A = A} (just Signal.unknown ∷ sigs) S sigs' shrs' vars' r θ
  E⟦nothin⟧ cb sigs'≠FV k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
  with any (_≟_ S) (proj₁
                     (Canθ' sigs (suc S) (Canθ sigs' 0 (E ⟦ r ⟧e))
                       (θ ← [S]-env (S ₛ))))
     | any (_≟_ S) (proj₁
                     (Canθ sigs (suc S) (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e)
                       (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | yes S∈canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
... | no  S∉canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | no  S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ
... | no  S∉canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | yes S∈canθ-sigs-E⟦ρΘsigs'⟧-θ←[S] =
  canθₖ-add-sig-monotonic sigs (suc S) (E ⟦ ρ⟨ Θ sigs' shrs' vars' , A ⟩· r ⟧e) θ
    (S ₛ) Signal.absent k
    (canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
      r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
      k k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ)
... | yes S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S] | no  S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S]
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs' =
  canθₖ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
    r (θ ← [S]-env-absent (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
    k
    (subst (k ∈_)
      (cong (proj₁ ∘ proj₂)
        (trans
          (canθ'-inner-shadowing-irr sigs (suc S) sigs' (E ⟦ r ⟧e)
            S Signal.unknown θ S∈sigs')
          (sym (canθ'-inner-shadowing-irr sigs (suc S) sigs' (E ⟦ r ⟧e)
                 S Signal.absent θ S∈sigs'))))
      k∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ)
... | no  S∉sigs' =
  ⊥-elim
    (S∉canθ-sigs-E⟦ρΘsigs'⟧-θ←[S]
      (canθₛ-mergeˡ-sigs-induction sigs (suc S) sigs' shrs' vars'
        r (θ ← [S]-env (S ₛ)) E⟦nothin⟧ cb sigs'≠FV
        S S∉sigs' S∈canθ'-sigs-canθ-sigs'-E⟦r⟧-θ←[S]))

ext: agda

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Equivalences.PreXModReflGraph where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Relation.Binary

open import Cubical.Structures.Subtype
open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction
open import Cubical.Algebra.Group.Semidirect

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.DStructures.Meta.Isomorphism
open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.SplitEpi
open import Cubical.DStructures.Structures.ReflGraph
open import Cubical.DStructures.Structures.Action
open import Cubical.DStructures.Structures.XModule
open import Cubical.DStructures.Equivalences.GroupSplitEpiAction

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓC ℓ≅C ℓ≅ᴰ ℓ≅ᴰ' ℓ≅B' : Level

open Kernel
open GroupHom -- such .fun!
open GroupLemmas
open MorphismLemmas
open ActionLemmas

{-
After associating, we have

  B × isEqui   - B × isSecRet
    |        /      |
    |      /        |
  Action    ≃    SplitMono

Fix any action and its
corresponding split mono
    α             π₂
G₀ --> H   ↦  G₀ ↔ H ⋊⟨ α ⟩ G₀
                  ι₂

Precrossed module
α : G₀ --> H
φ : G₀ ← H
isEquivariant (α , φ)

gives internal reflexive graph
ι₂ : G₀ → H⋊⟨ α ⟩ G₀
     G₀ ← H⋊⟨ α ⟩ G₀ : π₂
     G₀ ← H⋊⟨ α ⟩ G₀ : τ_φ
τ_φ (h , g) := φ h + g
isSecRet (ι₂ , π₂)
isSecRet (ι₂ , τ_φ)

Conversely, a internal reflexive graph

ι₂ : G₀ → H⋊⟨ α ⟩ G₀
     G₀ ← H⋊⟨ α ⟩ G₀ : π₂
     G₀ ← H⋊⟨ α ⟩ G₀ : τ
isSecRet (ι₂ , π₂)
isSecRet (ι₂ , τ)

Then
ι₁ : H ≃ ker σ ↪ H ⋊⟨ α ⟩ G₀
α : G₀ --> H
    G₀ ← H : φ
φ := τ ∘ ι₁ is equivariant

-}

module _ (ℓ ℓ' : Level) where
  private
    ℓℓ' = ℓ-max ℓ ℓ'

    F = Iso.fun (IsoActionSplitEpi ℓ ℓℓ')

  -- reassociate: Display B + isSplitEpi over SplitEpi
  ReflGraph' = Σ[ (((G₀ , G₁) , (ι , σ)) , split-σ) ∈ SplitEpi ℓ ℓℓ' ] Σ[ τ ∈ GroupHom G₁ G₀ ] isGroupSplitEpi ι τ

  𝒮ᴰ-ReflGraph' : URGStrᴰ (𝒮-SplitEpi ℓ ℓℓ')
                          (λ (((G₀ , G₁) , (ι , σ)) , split-σ) → Σ[ τ ∈ GroupHom G₁ G₀ ] isGroupSplitEpi ι τ)
                          ℓℓ'
  𝒮ᴰ-ReflGraph' = splitTotal-𝒮ᴰ (𝒮-SplitEpi ℓ ℓℓ') (𝒮ᴰ-G²FBSplit\B ℓ ℓℓ') (𝒮ᴰ-ReflGraph ℓ ℓℓ')

  -- reassociate: Display B + isEquivar over Action
  PreXModule' = Σ[ (((G₀ , H) , _α_) , isAct) ∈ Action ℓ ℓℓ' ] Σ[ φ ∈ GroupHom H G₀ ] (isEquivariant (((G₀ , H) , _α_) , isAct) φ)

  𝒮ᴰ-PreXModule' : URGStrᴰ (𝒮-Action ℓ ℓℓ')
                           (λ (((G₀ , H) , _α_) , isAct) → Σ[ φ ∈ GroupHom H G₀ ] (isEquivariant (((G₀ , H) , _α_) , isAct) φ))
                           ℓℓ'
  𝒮ᴰ-PreXModule' = splitTotal-𝒮ᴰ (𝒮-Action ℓ ℓℓ') (𝒮ᴰ-Action\PreXModuleStr ℓ ℓℓ') (𝒮ᴰ-PreXModule ℓ ℓℓ')

  -- Establish ♭-relational isomorphism of precrossed modules and reflexive graphs
  -- over the isomorphism of actions and split epis
  𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' : 𝒮ᴰ-♭PIso F 𝒮ᴰ-PreXModule' 𝒮ᴰ-ReflGraph'
  RelIso.fun (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui) .fst = τ
    where
      -- notation
      open GroupNotation₀ G₀
      open GroupNotationᴴ H
      f = GroupHom.fun φ
      A = groupaction _α_ isAct
      H⋊G₀ : Group {ℓ-max ℓ ℓ'}
      H⋊G₀ = H ⋊⟨ A ⟩ G₀

      -- define the morphism τ
      τ : GroupHom H⋊G₀ G₀
      τ .fun (h , g) = f h +₀ g
      τ .isHom (h , g) (h' , g') = q
        where
          abstract
            q = f (h +ᴴ (g α h')) +₀ (g +₀ g')
                  ≡⟨ cong (_+₀ (g +₀ g')) (φ .isHom h (g α h')) ⟩
                (f h +₀ f (g α h')) +₀ (g +₀ g')
                  ≡⟨ cong (λ z → (f h +₀ z) +₀ (g +₀ g')) (isEqui g h') ⟩
                (f h +₀ ((g +₀ (f h')) -₀ g)) +₀ (g +₀ g')
                  ≡⟨ cong (λ z → (f h +₀ z) +₀ (g +₀ g') ) (sym (assoc₀ g (f h') (-₀ g))) ⟩
                (f h +₀ (g +₀ (f h' +₀ (-₀ g)))) +₀ (g +₀ g')
                  ≡⟨ cong (_+₀ (g +₀ g')) (assoc₀ (f h) g (f h' +₀ (-₀ g))) ⟩
                ((f h +₀ g) +₀ (f h' +₀ (-₀ g))) +₀ (g +₀ g')
                  ≡⟨ sym (assoc₀ (f h +₀ g) (f h' +₀ (-₀ g)) (g +₀ g')) ⟩
                (f h +₀ g) +₀ ((f h' +₀ (-₀ g)) +₀ (g +₀ g'))
                  ≡⟨ cong ((f h +₀ g) +₀_)
                          (sym (assoc₀ (f h') (-₀ g) (g +₀ g'))
                          ∙ (cong (f h' +₀_)
                                  (assoc₀ (-₀ g) g g'
                                  ∙∙ cong (_+₀ g') (lCancel₀ g)
                                  ∙∙ lId₀ g')))⟩
                (f h +₀ g) +₀ (f  h' +₀ g') ∎

  RelIso.fun (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui) .snd = q
    where
      -- notation
      open GroupNotation₀ G₀
      open GroupNotationᴴ H
      f = GroupHom.fun φ
      τ = RelIso.fun (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui) .fst
      ι = Iso.fun (IsoActionSplitEpi ℓ ℓℓ') (((G₀ , H) , _α_) , isAct) .fst .snd .fst

      -- prove that τ as constructed above is split
      abstract
        q : isGroupSplitEpi ι τ
        q = GroupMorphismExt λ g → f 0ᴴ +₀ g
                                             ≡⟨ cong (_+₀ g) (mapId φ) ⟩
                                           0₀ +₀ g
                                             ≡⟨ lId₀ g ⟩
                                           g ∎

  -- end of RelIso.fun (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui)

  RelIso.inv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (τ , split-τ) = φ , isEqui
    where
      -- notation
      ℬ = F (((G₀ , H) , _α_) , isAct)
      A = groupaction _α_ isAct

      -- σ = snd (snd (fst ℬ))
      -- φ should be τ| ker σ
      -- but ker σ ≅ H so we "restrict" τ to that
      -- by precomposing with the inclusion H → H⋊G₀
      ι1 = ι₁ A
      𝒾 = ι1 .fun

      t = τ .fun

      H⋊G₀ = H ⋊⟨ A ⟩ G₀
      _+α_ =  GroupStr._+_ (snd H⋊G₀)

      open GroupNotationᴴ H
      open GroupNotation₀ G₀

      -- define φ
      φ : GroupHom H G₀
      φ = compGroupHom ι1 τ
      f = φ .fun

      -- prove equivariance
      abstract
        isEqui : isEquivariant (((G₀ , H) , _α_) , isAct) φ
        isEqui g h = f (g α h)
                       ≡⟨ refl ⟩
                     t (g α h , 0₀)
                       ≡⟨ cong t
                               (g α h , 0₀
                                 ≡⟨ ΣPathP (sym ((cong (_+ᴴ ((g +₀ 0₀) α 0ᴴ)) (lIdᴴ (g α h)))
                                                ∙∙ cong ((g α h) +ᴴ_) (actOnUnit A (g +₀ 0₀))
                                                ∙∙ rIdᴴ (g α h))
                                           , sym (cong (_+₀ (-₀ g)) (rId₀ g) ∙ rCancel₀ g)) ⟩
                               (0ᴴ +ᴴ (g α h)) +ᴴ ((g +₀ 0₀) α 0ᴴ) , (g +₀ 0₀) -₀ g
                                 ≡⟨ refl ⟩
                               ((0ᴴ , g) +α (h , 0₀)) +α (0ᴴ , -₀ g) ∎) ⟩
                     t (((0ᴴ , g) +α (h , 0₀)) +α (0ᴴ , -₀ g))
                       ≡⟨ hom-homl τ (0ᴴ , g) (h , 0₀) (0ᴴ , -₀ g) ⟩
                     ((t (0ᴴ , g)) +₀ t (h , 0₀)) +₀ t (0ᴴ , -₀ g)
                       ≡⟨ cong (((t (0ᴴ , g)) +₀ t (h , 0₀)) +₀_) (funExt⁻ (cong fun split-τ) (-₀ g)) ⟩
                     ((t (0ᴴ , g)) +₀ t (h , 0₀)) -₀ g
                       ≡⟨ cong (λ z → (z +₀ t (h , 0₀)) -₀ g) (funExt⁻ (cong fun split-τ) g) ⟩
                     (g +₀ f h) -₀ g ∎

  -- RelIso.inv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (τ , split-τ)

  RelIso.leftInv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui) .fst = φ-≅
    where
      open GroupNotation₀ G₀

      abstract
        -- φ ≅ inv (fun φ) ≡ τ ∘ ι₁
        φ-≅ : (h : ⟨ H ⟩) → φ .fun h +₀ 0₀ ≡ φ .fun h
        φ-≅ h = rId₀ (φ .fun h)

  RelIso.leftInv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui) .snd = isEqui-≅
    where
      abstract
        isEqui-≅ : Unit
        isEqui-≅ = tt

  -- end of RelIso.leftInv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (φ , isEqui)

  RelIso.rightInv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (τ , split-τ) .fst = τ-≅
    where
      A = groupaction _α_ isAct
      H⋊G₀ = H ⋊⟨ A ⟩ G₀
      t = τ .fun
      open GroupNotation₀ G₀
      open GroupNotationᴴ H

      abstract
        τ-≅ : ((h , g) : ⟨ H⋊G₀ ⟩) → t (h , 0₀) +₀ g ≡ t (h , g)
        τ-≅ (h , g) = t (h , 0₀) +₀ g
                        ≡⟨ cong (t (h , 0₀) +₀_) (sym (funExt⁻ (cong GroupHom.fun split-τ) g)) ⟩
                      t (h , 0₀) +₀ t (0ᴴ , g)
                        ≡⟨ sym (τ .isHom (h , 0₀) (0ᴴ , g)) ⟩
                      t (h +ᴴ (0₀ α 0ᴴ) , 0₀ +₀ g)
                        ≡⟨ cong t (ΣPathP (cong (h +ᴴ_) (actOnUnit A 0₀) ∙ rIdᴴ h , lId₀ g)) ⟩
                      t (h , g) ∎

  RelIso.rightInv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (τ , split-τ) .snd = split-τ-≅
    where
      abstract
        split-τ-≅ : Unit
        split-τ-≅ = tt

  -- end of RelIso.rightInv (𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' (((G₀ , H) , _α_) , isAct)) (τ , split-τ)

  -- end of 𝒮ᴰ-♭PIso-PreXModule'-ReflGraph' : 𝒮ᴰ-♭PIso F 𝒮ᴰ-PreXModule' 𝒮ᴰ-ReflGraph'

  -- turn the ♭-relational isomorphism into a (normal) iso
  Iso-PreXModule-ReflGraph' : Iso PreXModule' ReflGraph'
  Iso-PreXModule-ReflGraph' = 𝒮ᴰ-♭PIso-Over→TotalIso (IsoActionSplitEpi ℓ ℓℓ') 𝒮ᴰ-PreXModule' 𝒮ᴰ-ReflGraph' 𝒮ᴰ-♭PIso-PreXModule'-ReflGraph'

  -- reassociate on both sides
  Iso-PreXModule-ReflGraph : Iso (PreXModule ℓ ℓℓ') (ReflGraph ℓ ℓℓ')
  Iso-PreXModule-ReflGraph = compIso (compIso Σ-assoc-Iso
                                            Iso-PreXModule-ReflGraph')
                                   (invIso Σ-assoc-Iso)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- Well-typed polymorphic and iso-recursive lambda terms
------------------------------------------------------------------------

module SystemF.WtTerm where

import Category.Functor as Functor
import Category.Applicative.Indexed as Applicative
open Functor.Morphism using (op-<$>)
open import Data.Fin using (Fin; zero; suc; inject+)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.List using (List; _∷_)
open import Data.List.All using (All; []; _∷_)
open import Data.Nat using (zero; suc; ℕ; _+_)
open import Data.Product using (_,_)
open import Data.Vec using (Vec; []; _∷_; _++_; lookup; map; toList; zip)
open import Data.Vec.Properties
  using (map-∘; map-cong; lookup-++-inject+)
open import Data.Vec.Categorical
  using (lookup-functor-morphism)
open import Function as Fun using (_∘_)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; cong; cong₂; subst; sym)
open PropEq.≡-Reasoning
open import Relation.Nullary using (¬_)

open import SystemF.Type
open import SystemF.Term

------------------------------------------------------------------------
-- Typing derivations for polymorphic and iso-recursive lambda terms

-- Typing contexts mapping free (term) variables to types.  A context
-- of type Ctx m n maps m free variables to types containing up to n
-- free type variables each.
Ctx : ℕ → ℕ → Set
Ctx m n = Vec (Type n) m

-- Type and variable substitutions lifted to typing contexts
module CtxSubst where

  infixl 8 _/_ _/Var_

  -- Type substitution lifted to typing contexts
  _/_ : ∀ {m n k} → Ctx m n → Sub Type n k → Ctx m k
  Γ / σ = Γ TypeSubst.⊙ σ

  -- Weakening of typing contexts with additional type variables
  weaken : ∀ {m n} → Ctx m n → Ctx m (1 + n)
  weaken Γ = map TypeSubst.weaken Γ

  -- Variable substitution (renaming) lifted to typing contexts
  _/Var_ : ∀ {m n k} → Sub Fin m k → Ctx k n → Ctx m n
  σ /Var Γ = map (λ x → lookup Γ x) σ

open TypeSubst using () renaming (_[/_]  to _[/tp_])
open CtxSubst  using () renaming (weaken to weakenCtx)

infix  4 _⊢_∈_ _⊢_∉_ _⊢val_∈_ _⊢ⁿ_∈_
infixl 9 _·_ _[_]

-- Typing derivations for well-typed terms
data _⊢_∈_ {m n} (Γ : Ctx m n) : Term m n → Type n → Set where
  var    : (x : Fin m) → Γ ⊢ var x ∈ lookup Γ x
  Λ      : ∀ {t a} → (weakenCtx Γ) ⊢ t ∈ a → Γ ⊢ Λ t ∈ ∀' a
  λ'     : ∀ {t b} → (a : Type n) → a ∷ Γ ⊢ t ∈ b → Γ ⊢ λ' a t ∈ a →' b
  μ      : ∀ {t} → (a : Type n) → a ∷ Γ ⊢ t ∈ a → Γ ⊢ μ a t ∈ a
  _[_]   : ∀ {t a} → Γ ⊢ t ∈ ∀' a → (b : Type n) → Γ ⊢ t [ b ] ∈ a [/tp b ]
  _·_    : ∀ {s t a b} → Γ ⊢ s ∈ a →' b → Γ ⊢ t ∈ a → Γ ⊢ s · t ∈ b
  fold   : ∀ {t} → (a : Type (1 + n)) → Γ ⊢ t ∈ a [/tp μ a ] →
           Γ ⊢ fold a t ∈ μ a
  unfold : ∀ {t} → (a : Type (1 + n)) → Γ ⊢ t ∈ μ a →
           Γ ⊢ unfold a t ∈ a [/tp μ a ]

-- Negation of well-typedness.
_⊢_∉_ : ∀ {m n} → Ctx m n → Term m n → Type n → Set
Γ ⊢ t ∉ a = ¬ Γ ⊢ t ∈ a

-- Typing derivations for well-typed values.
data _⊢val_∈_ {m n} (Γ : Ctx m n) : Val m n → Type n → Set where
  Λ    : ∀ {t a} → (weakenCtx Γ) ⊢ t ∈ a → Γ ⊢val Λ t ∈ ∀' a
  λ'   : ∀ {t b} → (a : Type n) → a ∷ Γ ⊢ t ∈ b → Γ ⊢val λ' a t ∈ a →' b
  fold : ∀ {v} → (a : Type (1 + n)) → Γ ⊢val v ∈ a [/tp μ a ] →
         Γ ⊢val fold a v ∈ μ a

-- Conversion from well-typed values to well-typed terms.
⊢⌜_⌝ : ∀ {m n} {Γ : Ctx m n} {v a} → Γ ⊢val v ∈ a → Γ ⊢ ⌜ v ⌝ ∈ a
⊢⌜ Λ x      ⌝ = Λ x
⊢⌜ λ' a t   ⌝ = λ' a t
⊢⌜ fold a t ⌝ = fold a ⊢⌜ t ⌝

-- Collections of typing derivations for well-typed terms.
data _⊢ⁿ_∈_ {m n} (Γ : Ctx m n) :
  ∀ {k} → Vec (Term m n) k → Vec (Type n) k → Set where
    []  : Γ ⊢ⁿ [] ∈ []
    _∷_ : ∀ {t a k} {ts : Vec (Term m n) k} {as : Vec (Type n) k} →
          Γ ⊢ t ∈ a → Γ ⊢ⁿ ts ∈ as → Γ ⊢ⁿ t ∷ ts ∈ a ∷ as

-- Lookup a well-typed term in a collection thereof.
lookup-⊢ : ∀ {m n k} {Γ : Ctx m n} {ts : Vec (Term m n) k}
             {as : Vec (Type n) k} →
           (x : Fin k) → Γ ⊢ⁿ ts ∈ as → Γ ⊢ lookup ts x ∈ lookup as x
lookup-⊢ zero    (⊢t ∷ ⊢ts) = ⊢t
lookup-⊢ (suc x) (⊢t ∷ ⊢ts) = lookup-⊢ x ⊢ts

------------------------------------------------------------------------
-- Lemmas about type and variable substitutions (renaming) lifted to
-- typing contexts

module CtxLemmas where
  open CtxSubst public

  private module Tp  = TypeLemmas
  private module Var = VarSubst

  -- Term variable substitution (renaming) commutes with type
  -- substitution.
  /Var-/ : ∀ {m n k l} (ρ : Sub Fin m k) (Γ : Ctx k n) (σ : Sub Type n l) →
           (ρ /Var Γ) / σ ≡ ρ /Var (Γ / σ)
  /Var-/ ρ Γ σ = begin
      (ρ /Var Γ) / σ
    ≡⟨ sym (map-∘ _ _ ρ) ⟩
      map (λ x → (lookup Γ x) Tp./ σ) ρ
    ≡⟨ map-cong (λ x → sym (Tp.lookup-⊙ x {ρ₁ = Γ})) ρ ⟩
      map (λ x → lookup (Γ / σ) x) ρ
    ∎

  -- Term variable substitution (renaming) commutes with weakening of
  -- typing contexts with an additional type variable.
  /Var-weaken : ∀ {m n k} (ρ : Sub Fin m k) (Γ : Ctx k n) →
                weaken (ρ /Var Γ) ≡ ρ /Var (weaken Γ)
  /Var-weaken ρ Γ = begin
    weaken (ρ /Var Γ)    ≡⟨ Tp.map-weaken ⟩
    (ρ /Var Γ) / Tp.wk   ≡⟨ /Var-/ ρ Γ Tp.wk ⟩
    ρ /Var (Γ / Tp.wk)   ≡⟨ sym (cong (_/Var_ ρ) (Tp.map-weaken {ρ = Γ})) ⟩
    ρ /Var (weaken Γ)    ∎

  -- Term variable substitution (renaming) commutes with term variable
  -- lookup in typing context.
  /Var-lookup : ∀ {m n k} (x : Fin m) (ρ : Sub Fin m k) (Γ : Ctx k n) →
                lookup (ρ /Var Γ) x ≡ lookup Γ (lookup ρ x)
  /Var-lookup x ρ Γ = op-<$> (lookup-functor-morphism x) (λ x → lookup Γ x) ρ

  -- Term variable substitution (renaming) commutes with weakening of
  -- typing contexts with an additional term variable.
  /Var-∷ : ∀ {m n k} (a : Type n) (ρ : Sub Fin m k) (Γ : Ctx k n) →
           a ∷ (ρ /Var Γ) ≡ (ρ Var.↑) /Var (a ∷ Γ)
  /Var-∷ a []      Γ = refl
  /Var-∷ a (x ∷ ρ) Γ = cong (_∷_ a) (cong (_∷_ (lookup Γ x)) (begin
    map (λ x → lookup Γ x) ρ                   ≡⟨ refl ⟩
    map (λ x → lookup (a ∷ Γ) (suc x)) ρ       ≡⟨ map-∘ _ _ ρ ⟩
    map (λ x → lookup (a ∷ Γ) x) (map suc ρ)   ∎))

  -- Invariants of term variable substitution (renaming)
  idVar-/Var   : ∀ {m n} (Γ : Ctx m n) → Γ ≡ (Var.id /Var Γ)
  wkVar-/Var-∷ : ∀ {m n} (Γ : Ctx m n) (a : Type n) → Γ ≡ (Var.wk /Var (a ∷ Γ))

  idVar-/Var []      = refl
  idVar-/Var (a ∷ Γ) = cong (_∷_ a) (wkVar-/Var-∷ Γ a)

  wkVar-/Var-∷ Γ a = begin
    Γ                    ≡⟨ idVar-/Var Γ ⟩
    Var.id /Var Γ         ≡⟨ map-∘ _ _ VarSubst.id ⟩
    Var.wk /Var (a ∷ Γ)   ∎

------------------------------------------------------------------------
-- Substitutions in well-typed terms

-- Helper lemmas for applying type and term equalities in typing
-- derivations
⊢subst : ∀ {m n} {Γ₁ Γ₂ : Ctx m n} {t₁ t₂ : Term m n} {a₁ a₂ : Type n} →
  Γ₁ ≡ Γ₂ → t₁ ≡ t₂ → a₁ ≡ a₂ → Γ₁ ⊢ t₁ ∈ a₁ → Γ₂ ⊢ t₂ ∈ a₂
⊢subst refl refl refl hyp = hyp

⊢substCtx : ∀ {m n} {Γ₁ Γ₂ : Ctx m n} {t : Term m n} {a : Type n} →
  Γ₁ ≡ Γ₂ → Γ₁ ⊢ t ∈ a → Γ₂ ⊢ t ∈ a
⊢substCtx refl hyp = hyp

⊢substTp : ∀ {m n} {Γ : Ctx m n} {t : Term m n} {a₁ a₂ : Type n} →
  a₁ ≡ a₂ → Γ ⊢ t ∈ a₁ → Γ ⊢ t ∈ a₂
⊢substTp refl hyp = hyp

-- Type substitutions lifted to well-typed terms
module WtTermTypeSubst where
  open TypeLemmas hiding (_/_; _[/_]; weaken)
  private
    module Tp = TypeLemmas
    module Tm = TermTypeLemmas
    module C  = CtxSubst

  infixl 8 _/_

  -- Type substitutions lifted to well-typed terms
  _/_ : ∀ {m n k} {Γ : Ctx m n} {t : Term m n} {a : Type n} →
        Γ ⊢ t ∈ a → (σ : Sub Type n k) → Γ C./ σ ⊢ t Tm./ σ ∈ a Tp./ σ
  _/_  {Γ = Γ} (var x) σ = ⊢substTp (lookup-⊙ x {ρ₁ = Γ}) (var x)
  _/_ {Γ = Γ} (Λ ⊢t)  σ =
    Λ (⊢substCtx (sym (map-weaken-⊙ Γ σ)) (⊢t / σ ↑))
  λ' a ⊢t           / σ = λ' (a Tp./ σ) (⊢t / σ)
  μ a ⊢t            / σ = μ  (a Tp./ σ) (⊢t / σ)
  _[_] {a = a} ⊢t b / σ =
    ⊢substTp (sym (sub-commutes a)) ((⊢t / σ) [ b Tp./ σ ])
  ⊢s · ⊢t           / σ = (⊢s / σ) · (⊢t / σ)
  fold a ⊢t         / σ =
    fold (a Tp./ σ ↑) (⊢substTp (sub-commutes a) (⊢t / σ))
  unfold a ⊢t       / σ =
    ⊢substTp (sym (sub-commutes a)) (unfold (a Tp./ σ ↑) (⊢t / σ))

  -- Weakening of terms with additional type variables lifted to
  -- well-typed terms.
  weaken : ∀ {m n} {Γ : Ctx m n} {t : Term m n} {a : Type n} →
           Γ ⊢ t ∈ a → C.weaken Γ ⊢ Tm.weaken t ∈ Tp.weaken a
  weaken {t = t} {a = a} ⊢t =
    ⊢subst (sym map-weaken) (Tm./-wk t) (/-wk {t = a}) (⊢t / wk)

  -- Weakening of terms with additional type variables lifted to
  -- collections of well-typed terms.
  weakenAll : ∀ {m n k} {Γ : Ctx m n} {ts : Vec (Term m n) k}
                {as : Vec (Type n) k} → Γ ⊢ⁿ ts ∈ as →
                C.weaken Γ ⊢ⁿ map Tm.weaken ts ∈ map Tp.weaken as
  weakenAll {ts = []}    {[]}    []         = []
  weakenAll {ts = _ ∷ _} {_ ∷ _} (⊢t ∷ ⊢ts) = weaken ⊢t ∷ weakenAll ⊢ts

  -- Shorthand for single-variable type substitutions in well-typed
  -- terms.
  _[/_] : ∀ {m n} {Γ : Ctx m (1 + n)} {t a} →
          Γ ⊢ t ∈ a → (b : Type n) → Γ C./ sub b ⊢ t Tm./ sub b ∈ a Tp./ sub b
  ⊢t [/ b ] = ⊢t / sub b

  -- A weakened version of the shorthand for single-variable type
  -- substitutions that fits well with well-typed type application.
  _[/_]′ : ∀ {m n} {Γ : Ctx m n} {t a} → C.weaken Γ ⊢ t ∈ a →
           (b : Type n) → Γ ⊢ t Tm./ sub b ∈ a Tp./ sub b
  ⊢t [/ b ]′ = ⊢substCtx Tp.map-weaken-⊙-sub (⊢t / sub b)

-- Term substitutions lifted to well-typed terms
module WtTermTermSubst where
  private
    module Tp  = TermTypeSubst
    module Tm  = TermTermSubst
    module Var = VarSubst
    module C   = CtxLemmas
    TmSub = Tm.TermSub Term

  infix 4 _⇒_⊢_

  -- Well-typed term substitutions are collections of well-typed terms.
  _⇒_⊢_ : ∀ {m n k} → Ctx m n → Ctx k n → TmSub m n k → Set
  Γ ⇒ Δ ⊢ ρ = Δ ⊢ⁿ ρ ∈ Γ

  infixl 8  _/_ _/Var_
  infix  10 _↑

  -- Application of term variable substitutions (renaming) lifted to
  -- well-typed terms.
  _/Var_ : ∀ {m n k} {Γ : Ctx k n} {t : Term m n} {a : Type n}
             (ρ : Sub Fin m k) → ρ C./Var Γ ⊢ t ∈ a → Γ ⊢ t Tm./Var ρ ∈ a
  _/Var_ {Γ = Γ} ρ (var x)   =
    ⊢substTp (sym (C./Var-lookup x ρ Γ)) (var (lookup ρ x))
  _/Var_ {Γ = Γ} ρ (Λ ⊢t)    =
    Λ    (ρ      /Var ⊢substCtx (C./Var-weaken ρ Γ) ⊢t)
  _/Var_ {Γ = Γ} ρ (λ' a ⊢t) =
    λ' a (ρ Var.↑ /Var ⊢substCtx (C./Var-∷ a ρ Γ) ⊢t)
  _/Var_ {Γ = Γ} ρ (μ a ⊢t)  =
    μ  a (ρ Var.↑ /Var ⊢substCtx (C./Var-∷ a ρ Γ) ⊢t)
  ρ /Var (⊢t [ b ])          = (ρ /Var ⊢t) [ b ]
  ρ /Var (⊢s · ⊢t)           = (ρ /Var ⊢s) · (ρ /Var ⊢t)
  ρ /Var (fold a ⊢t)         = fold   a (ρ /Var ⊢t)
  ρ /Var (unfold a ⊢t)       = unfold a (ρ /Var ⊢t)

  -- Weakening of terms with additional term variables lifted to
  -- well-typed terms.
  weaken : ∀ {m n} {Γ : Ctx m n} {t : Term m n} {a b : Type n} →
           Γ ⊢ t ∈ a → b ∷ Γ ⊢ Tm.weaken t ∈ a
  weaken {Γ = Γ} {b = b} ⊢t =
    Var.wk /Var ⊢substCtx (C.wkVar-/Var-∷ Γ b) ⊢t

  -- Weakening of terms with additional term variables lifted to
  -- collections of well-typed terms.
  weakenAll : ∀ {m n k} {Γ : Ctx m n} {ts : Vec (Term m n) k}
                {as : Vec (Type n) k} {b : Type n} →
              Γ ⊢ⁿ ts ∈ as → b ∷ Γ ⊢ⁿ map Tm.weaken ts ∈ as
  weakenAll {ts = []}    {[]}    []         = []
  weakenAll {ts = _ ∷ _} {_ ∷ _} (⊢t ∷ ⊢ts) = weaken ⊢t ∷ weakenAll ⊢ts

  -- Lifting of well-typed term substitutions.
  _↑ : ∀ {m n k} {Γ : Ctx m n} {Δ : Ctx k n} {ρ b} →
       Γ ⇒ Δ ⊢ ρ → b ∷ Γ ⇒ b ∷ Δ ⊢ ρ Tm.↑
  ⊢ρ ↑ = var zero ∷ weakenAll ⊢ρ

  -- The well-typed identity substitution.
  id : ∀ {m n} {Γ : Ctx m n} → Γ ⇒ Γ ⊢ Tm.id
  id {zero}  {Γ = []}    = []
  id {suc m} {Γ = a ∷ Γ} = id ↑

  -- Well-typed weakening (as a substitution).
  wk : ∀ {m n} {Γ : Ctx m n} {a} → Γ ⇒ a ∷ Γ ⊢ Tm.wk
  wk = weakenAll id

  -- A well-typed substitution which only replaces the first variable.
  sub : ∀ {m n} {Γ : Ctx m n} {t a} → Γ ⊢ t ∈ a → a ∷ Γ ⇒ Γ ⊢ Tm.sub t
  sub ⊢t = ⊢t ∷ id

  -- Application of term substitutions lifted to well-typed terms
  _/_ : ∀ {m n k} {Γ : Ctx m n} {Δ : Ctx k n} {t a ρ} →
        Γ ⊢ t ∈ a → Γ ⇒ Δ ⊢ ρ → Δ ⊢ t Tm./ ρ ∈ a
  var x       / ⊢ρ = lookup-⊢ x ⊢ρ
  Λ ⊢t        / ⊢ρ = Λ (⊢t / (WtTermTypeSubst.weakenAll ⊢ρ))
  λ' a ⊢t     / ⊢ρ = λ' a (⊢t / ⊢ρ ↑)
  μ a ⊢t      / ⊢ρ = μ a (⊢t / ⊢ρ ↑)
  (⊢t [ a ])  / ⊢ρ = (⊢t / ⊢ρ) [ a ]
  (⊢s · ⊢t)   / ⊢ρ = (⊢s / ⊢ρ) · (⊢t / ⊢ρ)
  fold a ⊢t   / ⊢ρ = fold a (⊢t / ⊢ρ)
  unfold a ⊢t / ⊢ρ = unfold a (⊢t / ⊢ρ)

  -- Shorthand for well-typed single-variable term substitutions.
  _[/_] : ∀ {m n} {Γ : Ctx m n} {s t a b} →
          b ∷ Γ ⊢ s ∈ a → Γ ⊢ t ∈ b → Γ ⊢ s Tm./ Tm.sub t ∈ a
  ⊢s [/ ⊢t ] = ⊢s / sub ⊢t

------------------------------------------------------------------------
-- Encoding of additional well-typed term operators
--
-- These correspond to admissible typing rules for the asscociated
-- term operators.

module WtTermOperators where
  open TypeOperators renaming (id to idTp)
  open TypeOperatorLemmas
  open TypeLemmas hiding (id)
  private
    module Ut   = TermOperators
    module ⊢Tp  = WtTermTypeSubst
    module ⊢Tm  = WtTermTermSubst

  -- Polymorphic identity function
  id : ∀ {m n} {Γ : Ctx m n} → Γ ⊢ Ut.id ∈ idTp
  id = Λ (λ' (var (zero)) (var zero))

  -- Bottom elimination/univeral property of the initial type
  ⊥-elim : ∀ {m n} {Γ : Ctx m n} (a : Type n) → Γ ⊢ Ut.⊥-elim a ∈ ⊥ →' a
  ⊥-elim a = λ' ⊥ ((var zero) [ a ])

  -- Unit value
  tt : ∀ {m n} {Γ : Ctx m n} → Γ ⊢ Ut.tt ∈ ⊤
  tt = id

  -- Top introduction/universal property of the terminal type
  ⊤-intro : ∀ {m n} {Γ : Ctx m n} → (a : Type n) → Γ ⊢ Ut.⊤-intro a ∈ a →' ⊤
  ⊤-intro {n = n} a = λ' a (id {n = n})

  -- Packing existential types
  as-∃_pack_,_ : ∀ {m n} {Γ : Ctx m n}
                   (a : Type (1 + n)) (b : Type n) {t : Term m n} →
                 Γ ⊢ t ∈ a [/tp b ] → Γ ⊢ Ut.as-∃ a pack b , t ∈ ∃ a
  as-∃ a pack b , ⊢t =
    Λ (λ' (∀' (weaken↑ a →' var (suc zero))) ((var zero [ weaken b ]) · ⊢t′))
    where ⊢t′ = ⊢Tm.weaken (⊢substTp (weaken-sub a b) (⊢Tp.weaken ⊢t))

  -- Unpacking existential types
  unpack_in'_ : ∀ {m n} {Γ : Ctx m n} {s : Term m n}
                  {t : Term (1 + m) (1 + n)} {a : Type (1 + n)} {b : Type n} →
                Γ ⊢ s ∈ ∃ a → a ∷ weakenCtx Γ ⊢ t ∈ weaken b →
                Γ ⊢ Ut.unpack_in'_ s t {a} {b} ∈ b
  unpack_in'_ {a = a} {b = b} ⊢s ⊢t = (⊢s [ b ]) · Λ (⊢substTp a≡ (λ' a ⊢t))
    where
      a≡ : a →' weaken b ≡ weaken↑ a / (sub b) ↑ →' weaken b
      a≡ = cong (λ a → a →' weaken b) (begin
        a                       ≡⟨ sym (id-vanishes a) ⟩
        a / TypeLemmas.id       ≡⟨ cong (λ σ → a / σ) (sym (id-↑⋆ 1)) ⟩
        a / (TypeLemmas.id) ↑   ≡⟨ cong (λ σ → a / σ ↑) (sym wk-⊙-sub) ⟩
        a / (wk ⊙ sub b) ↑      ≡⟨ cong (λ σ → a / σ) (↑⋆-distrib 1) ⟩
        a / wk ↑ ⊙ (sub b) ↑    ≡⟨ /-⊙ a ⟩
        a / wk ↑ / (sub b) ↑    ∎)

  -- n-ary term abstraction
  λⁿ : ∀ {m n k} {Γ : Ctx m n} (as : Vec (Type n) k) {b : Type n}
       {t : Term (k + m) n} → as ++ Γ ⊢ t ∈ b → Γ ⊢ Ut.λⁿ as t ∈ as →ⁿ b
  λⁿ []       ⊢t = ⊢t
  λⁿ (a ∷ as) ⊢t = λⁿ as (λ' a ⊢t)

  infixl 9 _·ⁿ_

  -- n-ary term application
  _·ⁿ_ : ∀ {m n k} {Γ : Ctx m n} {s : Term m n} {ts : Vec (Term m n) k}
           {as : Vec (Type n) k} {b : Type n} →
         Γ ⊢ s ∈ as →ⁿ b → Γ ⊢ⁿ ts ∈ as → Γ ⊢ s Ut.·ⁿ ts ∈ b
  _·ⁿ_ {ts = []}    {[]}    ⊢s []         = ⊢s
  _·ⁿ_ {ts = _ ∷ _} {_ ∷ _} ⊢s (⊢t ∷ ⊢ts) = ⊢s ·ⁿ ⊢ts · ⊢t

  -- Record/tuple constructor
  new : ∀ {m n k} {Γ : Ctx m n} {ts : Vec (Term m n) k} {as : Vec (Type n) k} →
        Γ ⊢ⁿ ts ∈ as → Γ ⊢ Ut.new ts {as} ∈ rec as
  new {ts = []}    {[]}     []         = tt
  new {ts = _ ∷ _} {a ∷ as} (⊢t ∷ ⊢ts) =
    Λ (λ' (map weaken (a ∷ as) →ⁿ var zero)
          (var zero ·ⁿ ⊢Tm.weakenAll (⊢Tp.weakenAll (⊢t ∷ ⊢ts))))

  -- Field access/projection
  π : ∀ {m n k} {Γ : Ctx m n} (x : Fin k) {t : Term m n}
        {as : Vec (Type n) k} →
      Γ ⊢ t ∈ rec as → Γ ⊢ Ut.π x t {as} ∈ lookup as x
  π             () {as = []}     ⊢t
  π {m} {Γ = Γ} x  {as = a ∷ as} ⊢t =
    (⊢t [ b ]) · ⊢substTp as′→ⁿb′≡ (λⁿ as′ (var x′))
    where
      as′ = a ∷ as
      x′  = inject+ m x
      b   = lookup as′ x
      b′  = lookup (as′ ++ Γ) x′
      as′→ⁿb′≡ : as′ →ⁿ b′ ≡ (map weaken as′ →ⁿ var zero) [/tp b ]
      as′→ⁿb′≡ = begin
          as′ →ⁿ b′
        ≡⟨ cong (λ b → as′ →ⁿ b) (lookup-++-inject+ as′ Γ x) ⟩
          as′ →ⁿ b
        ≡⟨ cong (λ as′ → as′ →ⁿ b) (sym (map-weaken-⊙-sub {ρ = as′})) ⟩
          map weaken as′ ⊙ sub b →ⁿ b
        ≡⟨ sym (/-→ⁿ (map weaken as′) (var zero) (sub b)) ⟩
          (map weaken as′ →ⁿ var zero) [/tp b ]
        ∎

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFmap
open import lib.types.Sigma
open import lib.types.Span

module lib.types.Join  where

module _ {i j} (A : Type i) (B : Type j) where

  *-span : Span
  *-span = span A B (A × B) fst snd

  infix 80 _*_

  _*_ : Type _
  _*_ = Pushout *-span

module _ {i j} {A : Type i} {B : Type j} where
  jleft : A → A * B
  jleft = left

  jright : B → A * B
  jright = right

  jglue : ∀ a b → jleft a == jright b
  jglue = curry glue

  module JoinElim {k} {P : A * B → Type k}
    (jleft* : (a : A) → P (jleft a)) (jright* : (b : B) → P (jright b))
    (jglue* : ∀ a b → jleft* a == jright* b [ P ↓ jglue a b ]) where

    private
      module M = PushoutElim {d = *-span A B} {P = P} jleft* jright* (uncurry jglue*)
    f = M.f
    glue-β = curry M.glue-β

  Join-elim = JoinElim.f

  module JoinRec {k} {C : Type k}
    (jleft* : (a : A) → C) (jright* : (b : B) → C)
    (jglue* : ∀ a b → jleft* a == jright* b) where

    private
      module M = PushoutRec jleft* jright* (uncurry jglue*)
    f = M.f
    glue-β = curry M.glue-β

  Join-rec = JoinRec.f

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙*-span : ⊙Span
  ⊙*-span = ⊙span X Y (X ⊙× Y) ⊙fst ⊙snd

  infix 80 _⊙*_

  _⊙*_ : Ptd _
  _⊙*_ = ⊙Pushout ⊙*-span

module _ {i i' j j'} {A : Type i} {A' : Type i'} {B : Type j} {B' : Type j'}
  (eqA : A ≃ A') (eqB : B ≃ B') where

  *-span-emap : SpanEquiv (*-span A B) (*-span A' B')
  *-span-emap = ( span-map (fst eqA) (fst eqB) (×-fmap (fst eqA) (fst eqB)) (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)
                , snd eqA , snd eqB , ×-isemap (snd eqA) (snd eqB))

  *-emap : A * B ≃ A' * B'
  *-emap = Pushout-emap *-span-emap

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'} where

  ⊙*-emap : X ⊙≃ X' → Y ⊙≃ Y' → X ⊙* Y ⊙≃ X' ⊙* Y'
  ⊙*-emap ⊙eqX ⊙eqY = ≃-to-⊙≃ (*-emap (⊙≃-to-≃ ⊙eqX) (⊙≃-to-≃ ⊙eqY)) (ap left (snd (⊙–> ⊙eqX)))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module OlderBasicILP.Indirect.Hilbert.Sequential where

open import OlderBasicILP.Indirect public

-- Derivations, as Hilbert-style combinator sequences.

mutual
  data Tm : Set where
    NIL   : Tm
    VAR   : ℕ → Tm → Tm
    MP    : ℕ → ℕ → Tm → Tm
    CI    : Tm → Tm
    CK    : Tm → Tm
    CS    : Tm → Tm
    NEC   : Tm → Tm → Tm
    CDIST : Tm → Tm
    CUP   : Tm → Tm
    CDOWN : Tm → Tm
    CPAIR : Tm → Tm
    CFST  : Tm → Tm
    CSND  : Tm → Tm
    UNIT  : Tm → Tm

  _⧻ᵀᵐ_ : Tm → Tm → Tm
  US ⧻ᵀᵐ NIL       = US
  US ⧻ᵀᵐ VAR I TS  = VAR I (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ MP I J TS = MP I J (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CI TS     = CI (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CK TS     = CK (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CS TS     = CS (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ NEC SS TS = NEC SS (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CDIST TS  = CDIST (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CUP TS    = CUP (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CDOWN TS  = CDOWN (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CPAIR TS  = CPAIR (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CFST TS   = CFST (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ CSND TS   = CSND (US ⧻ᵀᵐ TS)
  US ⧻ᵀᵐ UNIT TS   = UNIT (US ⧻ᵀᵐ TS)

  APP : Tm → Tm → Tm
  APP TS US = MP 0 0 (US ⧻ᵀᵐ TS)

  BOX : Tm → Tm
  BOX TS = NEC TS NIL

  infix 3 _⊢×_
  data _⊢×_ (Γ : Cx (Ty Tm)) : Cx (Ty Tm) → Set where
    nil   : Γ ⊢× ∅
    var   : ∀ {Ξ A}         → A ∈ Γ → Γ ⊢× Ξ → Γ ⊢× Ξ , A
    mp    : ∀ {Ξ A B}       → A ▻ B ∈ Ξ → A ∈ Ξ → Γ ⊢× Ξ → Γ ⊢× Ξ , B
    ci    : ∀ {Ξ A}         → Γ ⊢× Ξ → Γ ⊢× Ξ , A ▻ A
    ck    : ∀ {Ξ A B}       → Γ ⊢× Ξ → Γ ⊢× Ξ , A ▻ B ▻ A
    cs    : ∀ {Ξ A B C}     → Γ ⊢× Ξ → Γ ⊢× Ξ , (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
    nec   : ∀ {Ξ Ξ′ A}      → (ss : ∅ ⊢× Ξ′ , A) → Γ ⊢× Ξ → Γ ⊢× Ξ , [ ss ]× ⦂ A
    cdist : ∀ {Ξ A B TS US} → Γ ⊢× Ξ → Γ ⊢× Ξ , TS ⦂ (A ▻ B) ▻ US ⦂ A ▻ APP TS US ⦂ B
    cup   : ∀ {Ξ A TS}      → Γ ⊢× Ξ → Γ ⊢× Ξ , TS ⦂ A ▻ BOX TS ⦂ TS ⦂ A
    cdown : ∀ {Ξ A TS}      → Γ ⊢× Ξ → Γ ⊢× Ξ , TS ⦂ A ▻ A
    cpair : ∀ {Ξ A B}       → Γ ⊢× Ξ → Γ ⊢× Ξ , A ▻ B ▻ A ∧ B
    cfst  : ∀ {Ξ A B}       → Γ ⊢× Ξ → Γ ⊢× Ξ , A ∧ B ▻ A
    csnd  : ∀ {Ξ A B}       → Γ ⊢× Ξ → Γ ⊢× Ξ , A ∧ B ▻ B
    unit  : ∀ {Ξ}           → Γ ⊢× Ξ → Γ ⊢× Ξ , ⊤

  [_]× : ∀ {Ξ Γ} → Γ ⊢× Ξ → Tm
  [ nil ]×       = NIL
  [ var i ts ]×  = VAR [ i ]ⁱ [ ts ]×
  [ mp i j ts ]× = MP [ i ]ⁱ [ j ]ⁱ [ ts ]×
  [ ci ts ]×     = CI [ ts ]×
  [ ck ts ]×     = CK [ ts ]×
  [ cs ts ]×     = CS [ ts ]×
  [ nec ss ts ]× = NEC [ ss ]× [ ts ]×
  [ cdist ts ]×  = CDIST [ ts ]×
  [ cup ts ]×    = CUP [ ts ]×
  [ cdown ts ]×  = CDOWN [ ts ]×
  [ cpair ts ]×  = CPAIR [ ts ]×
  [ cfst ts ]×   = CFST [ ts ]×
  [ csnd ts ]×   = CSND [ ts ]×
  [ unit ts ]×   = UNIT [ ts ]×

infix 3 _⊢_
_⊢_ : Cx (Ty Tm) → Ty Tm → Set
Γ ⊢ A = ∃ (λ Ξ → Γ ⊢× Ξ , A)

[_] : ∀ {A Γ} → Γ ⊢ A → Tm
[ Ξ , ts ] = [ ts ]×

-- Monotonicity with respect to context inclusion.

mono⊢× : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢× Ξ → Γ′ ⊢× Ξ
mono⊢× η nil         = nil
mono⊢× η (var i ts)  = var (mono∈ η i) (mono⊢× η ts)
mono⊢× η (mp i j ts) = mp i j (mono⊢× η ts)
mono⊢× η (ci ts)     = ci (mono⊢× η ts)
mono⊢× η (ck ts)     = ck (mono⊢× η ts)
mono⊢× η (cs ts)     = cs (mono⊢× η ts)
mono⊢× η (nec ss ts) = nec ss (mono⊢× η ts)
mono⊢× η (cdist ts)  = cdist (mono⊢× η ts)
mono⊢× η (cup ts)    = cup (mono⊢× η ts)
mono⊢× η (cdown ts)  = cdown (mono⊢× η ts)
mono⊢× η (cpair ts)  = cpair (mono⊢× η ts)
mono⊢× η (cfst ts)   = cfst (mono⊢× η ts)
mono⊢× η (csnd ts)   = csnd (mono⊢× η ts)
mono⊢× η (unit ts)   = unit (mono⊢× η ts)

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (Ξ , ts) = Ξ , mono⊢× η ts

-- Concatenation of derivations.

_⧻_ : ∀ {Γ Ξ Ξ′} → Γ ⊢× Ξ → Γ ⊢× Ξ′ → Γ ⊢× Ξ ⧺ Ξ′
us ⧻ nil       = us
us ⧻ var i ts  = var i (us ⧻ ts)
us ⧻ mp i j ts = mp (mono∈ weak⊆⧺₂ i) (mono∈ weak⊆⧺₂ j) (us ⧻ ts)
us ⧻ ci ts     = ci (us ⧻ ts)
us ⧻ ck ts     = ck (us ⧻ ts)
us ⧻ cs ts     = cs (us ⧻ ts)
us ⧻ nec ss ts = nec ss (us ⧻ ts)
us ⧻ cdist ts  = cdist (us ⧻ ts)
us ⧻ cup ts    = cup (us ⧻ ts)
us ⧻ cdown ts  = cdown (us ⧻ ts)
us ⧻ cpair ts  = cpair (us ⧻ ts)
us ⧻ cfst ts   = cfst (us ⧻ ts)
us ⧻ csnd ts   = csnd (us ⧻ ts)
us ⧻ unit ts   = unit (us ⧻ ts)

-- Modus ponens and necessitation in expanded form.

app : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
app {A} {B} (Ξ , ts) (Ξ′ , us) = Ξ″ , vs
  where Ξ″ = (Ξ′ , A) ⧺ (Ξ , A ▻ B)
        vs = mp top (mono∈ (weak⊆⧺₁ (Ξ , A ▻ B)) top) (us ⧻ ts)

box : ∀ {A Γ} → (t : ∅ ⊢ A) → Γ ⊢ [ t ] ⦂ A
box (Ξ , ts) = ∅ , nec ts nil

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --without-K --safe --overlapping-instances #-}
module SmallInterpreter where

open import Data.Char hiding (_≤_)
open import Data.Bool hiding (_≤_)
open import Data.Nat hiding (_≤_)
open import Data.Unit
import Data.Nat as N
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
import Data.String as Str
open import Data.Nat.Show
import Data.List as List
open import Data.Empty

infix 3 _:::_,_
infix 2 _∈_

infix 1 _⊢_

data `Set : Set where
  `Bool : `Set
  _`⇨_  : `Set → `Set → `Set
  `⊤    : `Set
  _`×_  : `Set → `Set → `Set
infixr 2 _`⇨_

data Var : Set where
  x' : Var
  y' : Var
  z' : Var

-- Inequality proofs on variables
data _≠_ : Var → Var → Set where
  x≠y : x' ≠ y'
  x≠z : x' ≠ z'
  y≠x : y' ≠ x'
  y≠z : y' ≠ z'
  z≠x : z' ≠ x'
  z≠y : z' ≠ y'

⟦_⟧ : `Set → Set
⟦ `Bool ⟧ = Bool
⟦ (t `⇨ s) ⟧ =  ⟦ t ⟧ → ⟦ s ⟧
⟦ `⊤ ⟧ = ⊤
⟦ (t `× s) ⟧ = ⟦ t ⟧ × ⟦ s ⟧

data Γ : Set where
  ·         : Γ
  _:::_,_   : Var → `Set → Γ → Γ

data _∈_ :  Var → Γ → Set where
  H  : ∀ {x Δ t } → x ∈ x ::: t , Δ
  TH : ∀ {x y Δ t } → ⦃ prf : x ∈ Δ ⦄ → ⦃ neprf : x ≠ y ⦄ → x ∈ y ::: t , Δ

!Γ_[_] : ∀ {x} → (Δ : Γ) → x ∈ Δ → `Set
!Γ_[_] · ()
!Γ _ ::: t , Δ [ H ]     = t
!Γ _ ::: _ , Δ [ TH ⦃ prf = i ⦄ ]  = !Γ Δ [ i ]

infix 30 `v_
infix 30 `not_
infix 27 _`∧_
infix 26 _`∨_
infix 25 _`xor_
infix 24 _`,_
infixl 22 _`₋_

data _⊢_ : Γ → `Set → Set where
  `false           : ∀ {Δ} → Δ ⊢ `Bool
  `true            : ∀ {Δ} → Δ ⊢ `Bool
  `v_              : ∀ {Δ} → (x : Var) → ⦃ i : x ∈ Δ ⦄ → Δ ⊢ !Γ Δ [ i ]
  _`₋_             : ∀ {Δ t s} → Δ ⊢ t `⇨ s → Δ ⊢ t → Δ ⊢ s --application
  `λ_`:_⇨_         : ∀ {Δ tr} → (x : Var) → (tx : `Set)
                        → x ::: tx , Δ ⊢ tr → Δ ⊢ tx `⇨ tr
  `not_            : ∀ {Δ} → Δ ⊢ `Bool → Δ ⊢ `Bool
  _`∧_             : ∀ {Δ} → Δ ⊢ `Bool → Δ ⊢ `Bool → Δ ⊢ `Bool
  _`∨_             : ∀ {Δ} → Δ ⊢ `Bool → Δ ⊢ `Bool → Δ ⊢ `Bool
  _`xor_           : ∀ {Δ} → Δ ⊢ `Bool → Δ ⊢ `Bool → Δ ⊢ `Bool
  _`,_             : ∀ {Δ t s} → Δ ⊢ t →  Δ ⊢ s →  Δ ⊢ t `× s
  `fst             : ∀ {Δ t s} → Δ ⊢ t `× s → Δ ⊢ t
  `snd             : ∀ {Δ t s} → Δ ⊢ t `× s → Δ ⊢ s
  `tt              : ∀ {Δ} → Δ ⊢ `⊤

data ⟨_⟩ : Γ → Set₁ where
  []   : ⟨ · ⟩
  _∷_  : ∀ {x t Δ} → ⟦ t ⟧ → ⟨ Δ ⟩ → ⟨ x ::: t , Δ ⟩

!_[_] : ∀ {x Δ} → ⟨ Δ ⟩ → (i : x ∈ Δ) → ⟦ !Γ Δ [ i ] ⟧
!_[_] [] ()
!_[_] (val ∷ env) H      = val
!_[_] (val ∷ env) (TH ⦃ prf = i ⦄) = ! env [ i ]

interpret : ∀ {t} → · ⊢ t → ⟦ t ⟧
interpret = interpret' []
  where interpret' : ∀ {Δ t} → ⟨ Δ ⟩ → Δ ⊢ t → ⟦ t ⟧
        interpret' env `true                = true
        interpret' env `false               = false
        interpret' env `tt                  = tt
        interpret' env ((`v x) ⦃ i = idx ⦄) = ! env [ idx ]
        interpret' env (f `₋ x)             = (interpret' env f) (interpret' env x)
        interpret' env (`λ _ `: tx ⇨ body)  = λ (x : ⟦ tx ⟧) → interpret' (x ∷ env) body
        interpret' env (`not x)             = not (interpret' env x)
        interpret' env (l `∧ r)             = interpret' env l ∧ interpret' env r
        interpret' env (l `∨ r)             = interpret' env l ∨ interpret' env r
        interpret' env (l `xor r )          = interpret' env l xor interpret' env r
        interpret' env (f `, s)             = interpret' env f ,′ interpret' env s
        interpret' env (`fst p) with interpret' env p
        interpret' env (`fst p) | f , s     = f
        interpret' env (`snd p) with interpret' env p
        interpret' env (`snd p) | f , s     = s

instance
  v_type₁ : ∀ {x Δ t} → x ∈ x ::: t , Δ
  v_type₁ = H

  v_type₂ : ∀ {x y Δ t} → ⦃ prf : x ∈ Δ ⦄ → ⦃ x ≠ y ⦄ → x ∈ y ::: t , Δ
  v_type₂ = TH

instance
  xy : x' ≠ y'
  xy = x≠y

  xz : x' ≠ z'
  xz = x≠z

  yx : y' ≠ x'
  yx = y≠x

  yz : y' ≠ z'
  yz = y≠z

  zx : z' ≠ x'
  zx = z≠x

  zy : z' ≠ y'
  zy = z≠y

pf : interpret (`λ x' `: `Bool ⇨ `v x') ≡ λ x → x
pf = refl

max_stars_repo_name: sseefried/well-typed-agda-interpreter

max_issues_repo_name: sseefried/well-typed-agda-interpreter

max_forks_repo_name: sseefried/well-typed-agda-interpreter


text:
-- Intuitionistic propositional calculus.
-- Hilbert-style formalisation of closed syntax.
-- Nested terms.

module IPC.Syntax.ClosedHilbert where

open import IPC.Syntax.Common public

-- Derivations.

infix 3 ⊢_
data ⊢_ : Ty → Set where
  app   : ∀ {A B}   → ⊢ A ▻ B → ⊢ A → ⊢ B
  ci    : ∀ {A}     → ⊢ A ▻ A
  ck    : ∀ {A B}   → ⊢ A ▻ B ▻ A
  cs    : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  cpair : ∀ {A B}   → ⊢ A ▻ B ▻ A ∧ B
  cfst  : ∀ {A B}   → ⊢ A ∧ B ▻ A
  csnd  : ∀ {A B}   → ⊢ A ∧ B ▻ B
  unit  : ⊢ ⊤
  cboom : ∀ {C}     → ⊢ ⊥ ▻ C
  cinl  : ∀ {A B}   → ⊢ A ▻ A ∨ B
  cinr  : ∀ {A B}   → ⊢ B ▻ A ∨ B
  ccase : ∀ {A B C} → ⊢ A ∨ B ▻ (A ▻ C) ▻ (B ▻ C) ▻ C

infix 3 ⊢⋆_
⊢⋆_ : Cx Ty → Set
⊢⋆ ∅     = 𝟙
⊢⋆ Ξ , A = ⊢⋆ Ξ × ⊢ A

-- Cut and multicut.

cut : ∀ {A B} → ⊢ A → ⊢ A ▻ B → ⊢ B
cut t u = app u t

multicut : ∀ {Ξ A} → ⊢⋆ Ξ → ⊢ Ξ ▻⋯▻ A → ⊢ A
multicut {∅}     ∙        u = u
multicut {Ξ , B} (ts , t) u = app (multicut ts u) t

-- Contraction.

ccont : ∀ {A B} → ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = app (app cs cs) (app ck ci)

cont : ∀ {A B} → ⊢ A ▻ A ▻ B → ⊢ A ▻ B
cont t = app ccont t

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = app (app cs (app (app cs (app ck cs))
                         (app (app cs (app ck ck)) cs)))
            (app ck ck)

exch : ∀ {A B C} → ⊢ A ▻ B ▻ C → ⊢ B ▻ A ▻ C
exch t = app cexch t

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C} → ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = app (app cs (app ck cs)) ck

comp : ∀ {A B C} → ⊢ B ▻ C → ⊢ A ▻ B → ⊢ A ▻ C
comp t u = app (app ccomp t) u

-- Useful theorems in functional form.

pair : ∀ {A B} → ⊢ A → ⊢ B → ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B} → ⊢ A ∧ B → ⊢ A
fst t = app cfst t

snd : ∀ {A B} → ⊢ A ∧ B → ⊢ B
snd t = app csnd t

boom : ∀ {C} → ⊢ ⊥ → ⊢ C
boom t = app cboom t

inl : ∀ {A B} → ⊢ A → ⊢ A ∨ B
inl t = app cinl t

inr : ∀ {A B} → ⊢ B → ⊢ A ∨ B
inr t = app cinr t

case : ∀ {A B C} → ⊢ A ∨ B → ⊢ A ▻ C → ⊢ B ▻ C → ⊢ C
case t u v = app (app (app ccase t) u) v

-- Convertibility.

data _⋙_ : ∀ {A} → ⊢ A → ⊢ A → Set where
  refl⋙     : ∀ {A} → {t : ⊢ A}
                     → t ⋙ t

  trans⋙    : ∀ {A} → {t t′ t″ : ⊢ A}
                     → t ⋙ t′ → t′ ⋙ t″
                     → t ⋙ t″

  sym⋙      : ∀ {A} → {t t′ : ⊢ A}
                     → t ⋙ t′
                     → t′ ⋙ t

  congapp⋙  : ∀ {A B} → {t t′ : ⊢ A ▻ B} → {u u′ : ⊢ A}
                       → t ⋙ t′ → u ⋙ u′
                       → app t u ⋙ app t′ u′

  congi⋙    : ∀ {A} → {t t′ : ⊢ A}
                     → t ⋙ t′
                     → app ci t ⋙ app ci t′

  congk⋙    : ∀ {A B} → {t t′ : ⊢ A} → {u u′ : ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app ck t) u ⋙ app (app ck t′) u′

  congs⋙    : ∀ {A B C} → {t t′ : ⊢ A ▻ B ▻ C} → {u u′ : ⊢ A ▻ B} → {v v′ : ⊢ A}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′
                         → app (app (app cs t) u) v ⋙ app (app (app cs t′) u′) v′

  congpair⋙ : ∀ {A B} → {t t′ : ⊢ A} → {u u′ : ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app cpair t) u ⋙ app (app cpair t′) u′

  congfst⋙  : ∀ {A B} → {t t′ : ⊢ A ∧ B}
                       → t ⋙ t′
                       → app cfst t ⋙ app cfst t′

  congsnd⋙  : ∀ {A B} → {t t′ : ⊢ A ∧ B}
                       → t ⋙ t′
                       → app csnd t ⋙ app csnd t′

  congboom⋙ : ∀ {C} → {t t′ : ⊢ ⊥}
                     → t ⋙ t′
                     → app (cboom {C = C}) t ⋙ app cboom t′

  conginl⋙  : ∀ {A B} → {t t′ : ⊢ A}
                       → t ⋙ t′
                       → app (cinl {A = A} {B}) t ⋙ app cinl t′

  conginr⋙  : ∀ {A B} → {t t′ : ⊢ B}
                       → t ⋙ t′
                       → app (cinr {A = A} {B}) t ⋙ app cinr t′

  congcase⋙ : ∀ {A B C} → {t t′ : ⊢ A ∨ B} → {u u′ : ⊢ A ▻ C} → {v v′ : ⊢ B ▻ C}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′
                         → app (app (app ccase t) u) v ⋙ app (app (app ccase t′) u′) v′

  -- TODO: Verify this.
  beta▻ₖ⋙   : ∀ {A B} → {t : ⊢ A} → {u : ⊢ B}
                       → app (app ck t) u ⋙ t

  -- TODO: Verify this.
  beta▻ₛ⋙   : ∀ {A B C} → {t : ⊢ A ▻ B ▻ C} → {u : ⊢ A ▻ B} → {v : ⊢ A}
                         → app (app (app cs t) u) v ⋙ app (app t v) (app u v)

  -- TODO: What about eta for ▻?

  beta∧₁⋙   : ∀ {A B} → {t : ⊢ A} → {u : ⊢ B}
                       → app cfst (app (app cpair t) u) ⋙ t

  beta∧₂⋙   : ∀ {A B} → {t : ⊢ A} → {u : ⊢ B}
                       → app csnd (app (app cpair t) u) ⋙ u

  eta∧⋙     : ∀ {A B} → {t : ⊢ A ∧ B}
                       → t ⋙ app (app cpair (app cfst t)) (app csnd t)

  eta⊤⋙    : ∀ {t : ⊢ ⊤} → t ⋙ unit

  -- TODO: Verify this.
  beta∨₁⋙   : ∀ {A B C} → {t : ⊢ A} → {u : ⊢ A ▻ C} → {v : ⊢ B ▻ C}
                         → app (app (app ccase (app cinl t)) u) v ⋙ app u t

  -- TODO: Verify this.
  beta∨₂⋙   : ∀ {A B C} → {t : ⊢ B} → {u : ⊢ A ▻ C} → {v : ⊢ B ▻ C}
                         → app (app (app ccase (app cinr t)) u) v ⋙ app v t

  -- TODO: What about eta and commuting conversions for ∨? What about ⊥?


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Sets.Facts.Product where

open import Data.Bool using (Bool ; true ; false)
open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong₂)

open import Cats.Category
open import Cats.Category.Sets using (Sets)

import Cats.Category.Sets.Facts.Terminal

instance
  hasBinaryProducts : ∀ {l} → HasBinaryProducts (Sets l)
  hasBinaryProducts .HasBinaryProducts._×′_ A B = record
    { prod = A × B
    ; proj = λ where
        true → proj₁
        false → proj₂
    ; isProduct = λ p → record
        { arr = λ x → p true x , p false x
        ; prop = λ where
            true → λ _ → refl
            false → λ _ → refl
        ; unique = λ eq x → cong₂ _,_ (eq true x) (eq false x)
        }
    }

  hasFiniteProducts :  ∀ {l} → HasFiniteProducts (Sets l)
  hasFiniteProducts = record {}

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.String
open import Agda.Builtin.List

Id : (A : Set) → A → A → Set
Id _ = _≡_

pattern suc² n = suc (suc n)
pattern suc³ n = suc (suc² n)

_ : (n : Nat) → Id Nat (suc³ n) (suc (suc n))
_ = {!!}

data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

pattern [_] x = x ∷ []

foo : List Nat → List Nat
foo [] = {!!}
foo (x ∷ xs) = {!!}

bar : Nat → Nat
bar zero = {!!}
bar (suc zero) = {!!}
bar (suc² n) = {!!}

_ : ∀ x → Id (Vec Nat _) [ x ] [ x ]
_ = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Integer division
------------------------------------------------------------------------

module Issue846.OldDivMod where

open import Data.Nat as Nat
open import Data.Nat.Properties
open SemiringSolver
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
import Data.Fin.Properties as Fin
open import Induction.Nat
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function

------------------------------------------------------------------------
-- Some boring lemmas

private

  lem₁ : (m k : ℕ) →
         Nat.suc m ≡ suc (toℕ (Fin.inject+ k (fromℕ m)) + 0)
  lem₁ m k = cong suc $ begin
    m
      ≡⟨ sym $ Fin.to-from m ⟩
    toℕ (fromℕ m)
      ≡⟨ Fin.inject+-lemma k (fromℕ m) ⟩
    toℕ (Fin.inject+ k (fromℕ m))
      ≡⟨ solve 1 (λ x → x := x :+ con 0) refl _ ⟩
    toℕ (Fin.inject+ k (fromℕ m)) + 0
      ∎

  lem₂ : ∀ n → _
  lem₂ = solve 1 (λ n → con 1 :+ n  :=  con 1 :+ (n :+ con 0)) refl

  lem₃ : ∀ n k q (r : Fin n) eq → suc n + k ≡ toℕ r + suc q * n
  lem₃ n k q r eq = begin
      suc n + k
        ≡⟨ solve 2 (λ n k → con 1 :+ n :+ k  :=  n :+ (con 1 :+ k))
                   refl n k ⟩
      n + suc k
        ≡⟨ cong (_+_ n) eq ⟩
      n + (toℕ r + q * n)
        ≡⟨ solve 3 (λ n r q → n :+ (r :+ q :* n)  :=
                              r :+ (con 1 :+ q) :* n)
                   refl n (toℕ r) q ⟩
      toℕ r + suc q * n
        ∎

------------------------------------------------------------------------
-- Division

infixl 7 _divMod_ _div_ _mod_

-- A specification of integer division.

record DivMod (dividend divisor : ℕ) : Set where
  constructor result
  field
    quotient  : ℕ
    remainder : Fin divisor
    property  : dividend ≡ toℕ remainder + quotient * divisor

-- Integer division with remainder.

-- Note that Induction.Nat.<-rec is used to establish termination of
-- division. The run-time complexity of this implementation of integer
-- division should be linear in the size of the dividend, assuming
-- that well-founded recursion and the equality type are optimised
-- properly (see "Inductive Families Need Not Store Their Indices"
-- (Brady, McBride, McKinna, TYPES 2003)).

_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
           DivMod dividend divisor
_divMod_ m n {≢0} = <-rec Pred dm m n {≢0}
  where
  Pred : ℕ → Set
  Pred dividend = (divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
                  DivMod dividend divisor

  1+_ : ∀ {k n} → DivMod (suc k) n → DivMod (suc n + k) n
  1+_ {k} {n} (result q r eq) = result (1 + q) r (lem₃ n k q r eq)

  dm : (dividend : ℕ) → <-Rec Pred dividend → Pred dividend
  dm m       rec zero    {≢0 = ()}
  dm zero    rec (suc n)            = result 0 zero refl
  dm (suc m) rec (suc n)            with compare m n
  dm (suc m) rec (suc .(suc m + k)) | less .m k    = result 0 r (lem₁ m k)
                                        where r = suc (Fin.inject+ k (fromℕ m))
  dm (suc m) rec (suc .m)           | equal .m     = result 1 zero (lem₂ m)
  dm (suc .(suc n + k)) rec (suc n) | greater .n k =
    1+ rec (suc k) le (suc n)
    where le = s≤′s (s≤′s (n≤′m+n n k))

-- Integer division.

_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
_div_ m n {≢0} = DivMod.quotient $ _divMod_ m n {≢0}

-- The remainder after integer division.

_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
_mod_ m n {≢0} = DivMod.remainder $ _divMod_ m n {≢0}


text:
postulate
  A : Set
  T : A → Set
  g : {{a : A}} → Set → T a

test : {{a b : A}} → Set
test {{a}} {{b}} = {!g A!} -- C-u C-u C-c C-d gives T b

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

module A where

  syntax c x = ⟦ x

  data D₁ : Set where
    b : D₁
    c : D₁ → D₁

module B where

  syntax c x = ⟦ x ⟧

  data D₂ : Set where
    c : A.D₁ → D₂

open A
open B

test₁ : D₂
test₁ = ⟦ (⟦ c b) ⟧

test₂ : D₂ → D₁
test₂ ⟦ x ⟧ = ⟦ x

test₃ : D₁ → D₂
test₃ b     = c b
test₃ (⟦ x) = ⟦ x ⟧

test₄ : D₁ → D₂
test₄ A.b     = B.c A.b
test₄ (A.⟦ x) = B.⟦ x ⟧

test₅ : D₂ → D₁
test₅ B.⟦ x ⟧ = A.⟦ x

-- Should work.


text:
module simpleAgda where

-- main : IO ()
-- main = putStrLn "Testing simple Idris"

--
-- Some simple equivalent Idris and Agda code.
--

-- data N = Z | Suc N
data N : Set where
  Z : N
  suc : N -> N

-- one : N
-- one = Suc Z
one : N
one = suc Z

-- addOne : N -> N
-- addOne Z = Suc Z
-- addOne (Suc n) = Suc (Suc n)

addOne : N -> N
addOne Z = suc Z
addOne (suc a) = suc (suc a)

-- add : N -> N -> N
-- add Z s = s
-- add (Suc a) b = add a (Suc b)
add : N -> N -> N
add Z s = s
add (suc a) b = add a (suc b)

-- data Vec : Type -> N -> Type where
--   Nil : Vec a Z
--   (::) : a -> Vec a n -> Vec a (Suc n)
data Vec (A : Set) : N -> Set where
  Nil : Vec A Z
  cons : {n : N} -> A -> Vec A n -> Vec A (suc n)

-- empt : Vec N Z
-- empt = Nil
empt : Vec N Z
empt = Nil

open import Agda.Builtin.Nat
-- test : Vec Nat (Suc Main.one)
-- test = 1 :: 2 :: Nil
test : Vec Nat (suc (suc Z))
test = cons 1 (cons 2 Nil)

-- test2 : Vec Nat (Suc (Suc Main.one))
-- test2 = 3 :: 4 :: 5 :: Nil
test2 : Vec Nat (suc (suc (suc Z)))
test2 = cons 3 (cons 4 (cons 5 Nil))

-- concat : Vec g a -> Vec g b -> Vec g (add a b)
-- concat Nil rest = rest
-- concat (a :: rest) b = concat rest (a :: b)
concat : {a b : N} {g : Set} -> (Vec g a) -> (Vec g b) -> (Vec g (add a b))
concat Nil rest = rest
concat (cons a rest) b = concat rest (cons a b)

-- t3 : Vec (addOne $ addOne $ addOne $ addOne Main.one) Nat
-- t3 = concat test test2
t3 : Vec Nat (addOne (addOne (addOne (addOne one))))
t3 = concat test test2

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
-- Andreas, 2015-07-10, issue reported by asr
-- {-# OPTIONS -v scope:20 #-}
-- {-# OPTIONS -v scope.createModule:10 #-}
module _ where

module A where
  module Y where

module B where
  -- FAILS:
  module X = A
  open X public
  -- open A public  --WORKS

module C = B

-- On maint and master:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Scope/Monad.hs:107

{-
createModule Issue1607.C
module macro
ScopeInfo
  current = Issue1607
  context = TopCtx
  modules
    scope
    scope Issue1607
      public
        modules
          A --> [Issue1607.A]
          B --> [Issue1607.B]
    scope Issue1607.A
      public
        modules
          Y --> [Issue1607.A.Y]
    scope Issue1607.A.Y
    scope Issue1607.B
      public
        modules
          X --> [Issue1607.B.X]
          Y --> [Issue1607.B.X.Y]
    scope Issue1607.B.X
      public
        modules
          Y --> [Issue1607.B.X.Y]
    scope Issue1607.B.X.Y
    scope Issue1607.C

Copying scope Issue1607.B to Issue1607.C
createModule Issue1607.C.X
Copying scope Issue1607.B.X to Issue1607.C.X
createModule Issue1607.C.X.Y
Copying scope Issue1607.B.X.Y to Issue1607.C.X.Y
createModule Issue1607.C.X.Y
Copying scope Issue1607.B.X.Y to Issue1607.C.X.Y
-}


text:
module Foundation.Bottom where

open import Foundation.Primitive

record IsBottom {ℓ-⊥} (⊥ : Set ℓ-⊥) ℓ-elim : ℞ ⟰ ℓ-elim ⊔ ℓ-⊥ where
  field
    ⊥-elim : ⊥ → {A : Set ℓ-elim} → A

open IsBottom ⦃ … ⦄ public

record Bottom ℓ-⊥ ℓ-elim : ℞₁ ℓ-elim ⊔ ℓ-⊥ where
  field
    ⊥ : Set ℓ-⊥
    instance ⦃ isBottom ⦄ : IsBottom ⊥ ℓ-elim

  ¬_ : ∀ {a} → Set a → ℞ a ⊔ ℓ-⊥
  ¬_ p = p → ⊥

open Bottom ⦃ … ⦄ public


text:
{-
  Define finitely generated ideals of commutative rings and
  show that they are an ideal.
  Parts of this should be reusable for explicit constructions
  of free modules over a finite set.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.FGIdeal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.FinData hiding (elim)
open import Cubical.Data.Nat using (ℕ)

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.Ring.QuotientRing
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

module _ (Ring@(R , str) : CommRing ℓ) where
  infixr 5 _holds
  _holds : hProp ℓ → Type ℓ
  P holds = fst P
  open CommRingStr str
  open RingTheory (CommRing→Ring Ring)
  open Sum (CommRing→Ring Ring)

  linearCombination : {n : ℕ} → FinVec R n → FinVec R n → R
  linearCombination α V = ∑ (λ i → α i · V i)

  sumDist+ : ∀ {n : ℕ} (α β V : FinVec R n)
           → linearCombination (λ i → α i + β i) V ≡ linearCombination α V + linearCombination β V
  sumDist+ α β V = ∑Ext (λ i → ·Ldist+ (α i) (β i) (V i)) ∙ ∑Split (λ i → α i · V i) (λ i → β i · V i)

  dist- : ∀ {n : ℕ} (α V : FinVec R n)
        → linearCombination (λ i → - α i) V ≡ - linearCombination α V
  dist- α V = ∑Ext (λ i → -DistL· (α i) (V i)) ∙ ∑Dist- (λ i → α i · V i)

  dist0 : ∀ {n : ℕ} (V : FinVec R n)
        → linearCombination (replicateFinVec n 0r) V ≡ 0r
  dist0 {n = n} V = ∑Ext (λ i → 0LeftAnnihilates (V i)) ∙ ∑0r n

  isLinearCombination : {n : ℕ} → FinVec R n → R → Type ℓ
  isLinearCombination V x = ∃[ α ∈ FinVec R _ ] x ≡ linearCombination α V

  {- If x and y are linear combinations of l, then (x + y) is
     a linear combination. -}
  isLinearCombination+ : {n : ℕ} {x y : R} (V : FinVec R n)
                         → isLinearCombination V x
                         → isLinearCombination V y
                         → isLinearCombination V (x + y)
  isLinearCombination+ V = map2 λ α β → (λ i → α .fst i + β .fst i)
                                       , cong₂ (_+_) (α .snd) (β .snd) ∙ sym (sumDist+ _ _ V)

  {- If x is a linear combinations of l, then -x is
     a linear combination. -}
  isLinearCombination- : {n : ℕ} {x : R} (V : FinVec R n)
                       → isLinearCombination V x → isLinearCombination V (- x)
  isLinearCombination- V = map λ α → (λ i → - α .fst i) , cong (-_) (α .snd) ∙ sym (dist- _ V)

  {- 0r is the trivial linear Combination -}
  isLinearCombination0 : {n : ℕ} (V : FinVec R n)
                       → isLinearCombination V 0r
  isLinearCombination0 V = ∣ _ , sym (dist0 V) ∣

  {- Linear combinations are stable under left multiplication -}
  isLinearCombinationL· : {n : ℕ} (V : FinVec R n) (r : R) {x : R}
                        → isLinearCombination V x → isLinearCombination V (r · x)
  isLinearCombinationL· V r = map λ α → (λ i → r · α .fst i) , cong (r ·_) (α .snd)
                                                            ∙∙ ∑Mulrdist r (λ i → α .fst i · V i)
                                                            ∙∙ ∑Ext λ i → ·Assoc r (α .fst i) (V i)

  generatedIdeal : {n : ℕ} → FinVec R n → IdealsIn Ring
  generatedIdeal V = makeIdeal Ring
                               (λ x → isLinearCombination V x , isPropPropTrunc)
                               (isLinearCombination+ V)
                               (isLinearCombination0 V)
                               λ r → isLinearCombinationL· V r

open isCommIdeal
genIdeal : {n : ℕ} (R : CommRing ℓ) → FinVec (fst R) n → CommIdeal R
fst (genIdeal R V) x = isLinearCombination R V x , isPropPropTrunc
+Closed (snd (genIdeal R V)) = isLinearCombination+ R V
contains0 (snd (genIdeal R V)) = isLinearCombination0 R V
·Closed (snd (genIdeal R V)) r = isLinearCombinationL· R V r

syntax genIdeal R V = ⟨ V ⟩[ R ]

FGIdealIn : (R : CommRing ℓ) → Type (ℓ-suc ℓ)
FGIdealIn R = Σ[ I ∈ CommIdeal R ] ∃[ n ∈ ℕ ] ∃[ V ∈ FinVec (fst R) n ] I ≡ ⟨ V ⟩[ R ]

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts

module lemmas-gcomplete where
  -- if you add a complete type to a complete context, the result is also a
  -- complete context
  gcomp-extend : ∀{Γ τ x} → Γ gcomplete → τ tcomplete → x # Γ → (Γ ,, (x , τ)) gcomplete
  gcomp-extend {Γ} {τ} {x} gc tc apart x_query τ_query x₁ with natEQ x x_query
  gcomp-extend {Γ} {τ} {x} gc tc apart .x τ_query x₂ | Inl refl = tr (λ qq → qq tcomplete) (someinj x₂) tc
  gcomp-extend {Γ} {τ} {x} gc tc apart x_query τ_query x₂ | Inr x₁ = gc x_query τ_query x₂

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda