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

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

module Data.Integer.DivMod where

open import Data.Nat as ℕ using (ℕ)
import Data.Nat.Properties as NProp
import Data.Nat.DivMod as NDM

import Data.Sign as S
import Data.Sign.Properties as SProp

open import Data.Integer as ℤ
open import Data.Integer.Properties

open import Data.Fin as Fin using (Fin)
import Data.Fin.Properties as FProp

open import Function

open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality

infixl 7 _divℕ_ _div_ _modℕ_ _mod_
_divℕ_ : (dividend : ℤ) (divisor : ℕ) {≢0 : False (divisor ℕ.≟ 0)} → ℤ
(+ n      divℕ d) {d≠0} = + (n NDM.div d) {d≠0}
(-[1+ n ] divℕ d) {d≠0} with (ℕ.suc n NDM.divMod d) {d≠0}
... | NDM.result q Fin.zero    eq = - (+ q)
... | NDM.result q (Fin.suc r) eq = -[1+ q ]

_div_ : (dividend divisor : ℤ) {≢0 : False (∣ divisor ∣ ℕ.≟ 0)} → ℤ
(n div d) {d≢0} = (sign d ◃ 1) ℤ.* (n divℕ ∣ d ∣) {d≢0}

_modℕ_ : (dividend : ℤ) (divisor : ℕ) {≠0 : False (divisor ℕ.≟ 0)} → ℕ
(+ n      modℕ d) {d≠0} = (n NDM.% d) {d≠0}
(-[1+ n ] modℕ d) {d≠0} with (ℕ.suc n NDM.divMod d) {d≠0}
... | NDM.result q Fin.zero    eq = 0
... | NDM.result q (Fin.suc r) eq = d ℕ.∸ ℕ.suc (Fin.toℕ r)

_mod_ : (dividend divisor : ℤ) {≠0 : False (∣ divisor ∣ ℕ.≟ 0)} → ℕ
(n mod d) {d≢0} = (n modℕ ∣ d ∣) {d≢0}

n%ℕd<d : ∀ n d {d≢0} → (n modℕ d) {d≢0} ℕ.< d
n%ℕd<d n ℕ.zero {()}
n%ℕd<d (+ n)    sd@(ℕ.suc d) = NDM.a%n<n n d
n%ℕd<d -[1+ n ] sd@(ℕ.suc d) with ℕ.suc n NDM.divMod sd
... | NDM.result q Fin.zero    eq = ℕ.s≤s ℕ.z≤n
... | NDM.result q (Fin.suc r) eq = ℕ.s≤s (NProp.n∸m≤n (Fin.toℕ r) d)

n%d<d : ∀ n d {d≢0} → (n mod d) {d≢0} ℕ.< ℤ.∣ d ∣
n%d<d n (+ 0) {()}
n%d<d n (+ ℕ.suc d) = n%ℕd<d n (ℕ.suc d)
n%d<d n -[1+ d ]    = n%ℕd<d n (ℕ.suc d)

a≡a%ℕn+[a/ℕn]*n : ∀ n d {d≢0} → n ≡ + (n modℕ d) {d≢0} + (n divℕ d) {d≢0} * + d
a≡a%ℕn+[a/ℕn]*n _ ℕ.zero {()}
a≡a%ℕn+[a/ℕn]*n (+ n) sd@(ℕ.suc d) = let q = n NDM.div sd; r = n NDM.% sd in begin
  + n                ≡⟨ cong +_ (NDM.a≡a%n+[a/n]*n n d) ⟩
  + (r ℕ.+ q ℕ.* sd) ≡⟨ pos-+-commute r (q ℕ.* sd) ⟩
  + r + + (q ℕ.* sd) ≡⟨ cong (_+_ (+ (+ n modℕ sd))) (sym (pos-distrib-* q sd)) ⟩
  + r + + q * + sd   ∎ where open ≡-Reasoning
a≡a%ℕn+[a/ℕn]*n -[1+ n ] sd@(ℕ.suc d) with (ℕ.suc n) NDM.divMod (ℕ.suc d)
... | NDM.result q Fin.zero    eq = begin
  -[1+ n ]            ≡⟨ cong (-_ ∘′ +_) eq ⟩
  - + (q ℕ.* sd)      ≡⟨ cong -_ (sym (pos-distrib-* q sd)) ⟩
  - (+ q * + sd)      ≡⟨ neg-distribˡ-* (+ q) (+ sd) ⟩
  - (+ q) * + sd      ≡⟨ sym (+-identityˡ (- (+ q) * + sd)) ⟩
  + 0 + - (+ q) * + sd ∎ where open ≡-Reasoning
... | NDM.result q (Fin.suc r) eq = begin
  let sd = ℕ.suc d; sr = ℕ.suc (Fin.toℕ r); sq = ℕ.suc q in
  -[1+ n ]
    ≡⟨ cong (-_ ∘′ +_) eq ⟩
  - + (sr ℕ.+ q ℕ.* sd)
    ≡⟨ cong -_ (pos-+-commute sr (q ℕ.* sd)) ⟩
  - (+ sr + + (q ℕ.* sd))
    ≡⟨ neg-distrib-+ (+ sr) (+ (q ℕ.* sd)) ⟩
  - + sr - + (q ℕ.* sd)
    ≡⟨ cong (_-_ (- + sr)) (sym (pos-distrib-* q sd)) ⟩
  - + sr - (+ q) * (+ sd)
    ≡⟨⟩
  - + sr - pred (+ sq) * (+ sd)
    ≡⟨ cong (_-_ (- + sr)) (*-distribʳ-+ (+ sd) (- + 1)  (+ sq)) ⟩
  - + sr - (- (+ 1) * + sd + (+ sq * + sd))
    ≡⟨ cong (_+_ (- (+ sr))) (neg-distrib-+ (- (+ 1) * + sd) (+ sq * + sd)) ⟩
  - + sr + (- (-[1+ 0 ] * + sd) + - (+ sq * + sd))
    ≡⟨ cong₂ (λ p q → - + sr + (- p + q)) (-1*n≡-n (+ sd))
                                            (neg-distribˡ-* (+ sq) (+ sd)) ⟩
  - + sr + ((- - + sd) + -[1+ q ] * + sd)
    ≡⟨ sym (+-assoc (- + sr) (- - + sd) (-[1+ q ] * + sd)) ⟩
  (+ sd - + sr) + -[1+ q ] * + sd
    ≡⟨ cong (_+ -[1+ q ] * + sd) (fin-inv d r) ⟩
  + (sd ℕ.∸ sr) + -[1+ q ] * + sd
    ∎ where

    open ≡-Reasoning

    fin-inv : ∀ d (k : Fin d) → + (ℕ.suc d) - + ℕ.suc (Fin.toℕ k) ≡ + (d ℕ.∸ Fin.toℕ k)
    fin-inv (ℕ.suc n) Fin.zero    = refl
    fin-inv (ℕ.suc n) (Fin.suc k) = ⊖-≥ {n} {Fin.toℕ k} (NProp.<⇒≤ (FProp.toℕ<n k))

[n/ℕd]*d≤n : ∀ n d {d≢0} → (n divℕ d) {d≢0} ℤ.* ℤ.+ d ℤ.≤ n
[n/ℕd]*d≤n n ℕ.zero {()}
[n/ℕd]*d≤n n (ℕ.suc d) = let q = n divℕ ℕ.suc d; r = n modℕ ℕ.suc d in begin
  q ℤ.* ℤ.+ (ℕ.suc d)           ≤⟨ n≤m+n r ⟩
  ℤ.+ r ℤ.+ q ℤ.* ℤ.+ (ℕ.suc d) ≡⟨ sym (a≡a%ℕn+[a/ℕn]*n n (ℕ.suc d)) ⟩
  n                             ∎ where open ≤-Reasoning

div-pos-is-divℕ : ∀ n d {d≢0} → (n div + d) {d≢0} ≡ (n divℕ d) {d≢0}
div-pos-is-divℕ n ℕ.zero {()}
div-pos-is-divℕ n (ℕ.suc d) = *-identityˡ (n divℕ ℕ.suc d)

div-neg-is-neg-divℕ : ∀ n d {d≢0} {∣d∣≢0} → (n div (- ℤ.+ d)) {∣d∣≢0} ≡ - (n divℕ d) {d≢0}
div-neg-is-neg-divℕ n ℕ.zero {()}
div-neg-is-neg-divℕ n (ℕ.suc d) = -1*n≡-n (n divℕ ℕ.suc d)

0≤n⇒0≤n/ℕd : ∀ n d {d≢0} → + 0 ℤ.≤ n → + 0 ℤ.≤ (n divℕ d) {d≢0}
0≤n⇒0≤n/ℕd (+ n) d (+≤+ m≤n) = +≤+ ℕ.z≤n

0≤n⇒0≤n/d : ∀ n d {d≢0} → + 0 ℤ.≤ n → + 0 ℤ.≤ d → + 0 ℤ.≤ (n div d) {d≢0}
0≤n⇒0≤n/d n (+ d) {d≢0} 0≤n (+≤+ 0≤d)
  rewrite div-pos-is-divℕ n d {d≢0}
        = 0≤n⇒0≤n/ℕd n d 0≤n

[n/d]*d≤n : ∀ n d {d≢0} → (n div d) {d≢0} ℤ.* d ℤ.≤ n
[n/d]*d≤n n (+ 0) {()}
[n/d]*d≤n n (+ ℕ.suc d) = begin let sd = ℕ.suc d in
  n div + sd * + sd ≡⟨ cong (_* (+ sd)) (div-pos-is-divℕ n sd) ⟩
  n divℕ sd * + sd  ≤⟨ [n/ℕd]*d≤n n sd ⟩
  n ∎ where open ≤-Reasoning
[n/d]*d≤n n -[1+ d ]    = begin let sd = ℕ.suc d in
  n div (- + sd) * - + sd ≡⟨ cong (_* (- + sd)) (div-neg-is-neg-divℕ n sd) ⟩
  - (n divℕ sd) * - + sd  ≡⟨ sym (neg-distribˡ-* (n divℕ sd) (- + sd)) ⟩
  - (n divℕ sd * - + sd)  ≡⟨ neg-distribʳ-* (n divℕ sd) (- + sd) ⟩
  n divℕ sd * + sd        ≤⟨ [n/ℕd]*d≤n n sd ⟩
  n ∎ where open ≤-Reasoning

n<s[n/ℕd]*d : ∀ n d {d≢0} → n ℤ.< ℤ.suc ((n divℕ d) {d≢0}) ℤ.* ℤ.+ d
n<s[n/ℕd]*d n ℕ.zero {()}
n<s[n/ℕd]*d n sd@(ℕ.suc d) = begin
  suc n                     ≡⟨ cong suc (a≡a%ℕn+[a/ℕn]*n n sd) ⟩
  suc (ℤ.+ r ℤ.+ q ℤ.* +sd) ≤⟨ +-monoˡ-< (q ℤ.* +sd) {ℤ.+ r} (ℤ.+≤+ (n%ℕd<d n sd)) ⟩
  +sd ℤ.+ q ℤ.* +sd         ≡⟨ sym ([1+m]*n≡n+m*n q +sd) ⟩
  ℤ.suc q ℤ.* +sd           ∎ where
  q = n divℕ sd; +sd = ℤ.+ sd; r = n modℕ sd
  open ≤-Reasoning

a≡a%n+[a/n]*n : ∀ a n {≢0} → a ≡ + (a mod n) {≢0} + (a div n) {≢0} * n
a≡a%n+[a/n]*n n (+ 0) {()}
a≡a%n+[a/n]*n n (+ ℕ.suc d) = begin
  let sd = ℕ.suc d; r = n modℕ sd; q = n divℕ sd; qsd = q * + sd in
  n                       ≡⟨ a≡a%ℕn+[a/ℕn]*n n sd ⟩
  + r + qsd               ≡⟨ cong (λ p → + r + p * + sd) (sym (div-pos-is-divℕ n sd)) ⟩
  + r + n div + sd * + sd ∎ where open ≡-Reasoning
a≡a%n+[a/n]*n n -[1+ d ]    = begin
  let sd = ℕ.suc d; r = n modℕ sd; q = n divℕ sd; qsd = q * + sd in
  n                      ≡⟨ a≡a%ℕn+[a/ℕn]*n n sd ⟩
  + r + q * + sd         ≡⟨⟩
  + r + q * - -[1+ d ]   ≡⟨ cong (_+_ (+ r)) (sym (neg-distribʳ-* q -[1+ d ])) ⟩
  + r + - (q * -[1+ d ]) ≡⟨ cong (_+_ (+ r)) (neg-distribˡ-* q -[1+ d ]) ⟩
  + r + - q * -[1+ d ]   ≡⟨ cong (_+_ (+ r) ∘′ (_* -[1+ d ])) (sym (-1*n≡-n q)) ⟩
  + r + n div -[1+ d ] * -[1+ d ] ∎ where open ≡-Reasoning


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.CohomologyRings.S0 where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Bool
open import Cubical.Data.Unit

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.DirectProd
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-notationZ

open import Cubical.HITs.Sn

open import Cubical.ZCohomology.RingStructure.CohomologyRing
open import Cubical.ZCohomology.CohomologyRings.Coproduct
open import Cubical.ZCohomology.CohomologyRings.Unit

-----------------------------------------------------------------------------
-- Warning
-- H*(S0) is not Z[X]/X²
-- It is Z[X]/X × Z[X]/X or Z[X] /(X² - X)
-- Beware that H*(X ⊔ Y) ≅ H*(X) × H*(Y)
-- Which would apply for H*(Unit ⊔ Unit)

-----------------------------------------------------------------------------
-- Computation of the cohomology ring

open RingEquivs

Cohomology-Ring-S⁰P : RingEquiv (H*R (S₊ 0)) (DirectProd-Ring (CommRing→Ring ℤ[X]/X) (CommRing→Ring ℤ[X]/X))
Cohomology-Ring-S⁰P =  compRingEquiv (CohomologyRing-Equiv (invIso Iso-⊤⊎⊤-Bool))
                     (compRingEquiv (CohomologyRing-Coproduct Unit Unit)
                                    (Coproduct-Equiv.Coproduct-Equiv-12 CohomologyRing-UnitP CohomologyRing-UnitP))

Cohomology-Ring-S⁰ℤ : RingEquiv (H*R (S₊ 0)) (DirectProd-Ring (CommRing→Ring ℤCR) (CommRing→Ring ℤCR))
Cohomology-Ring-S⁰ℤ =  compRingEquiv (CohomologyRing-Equiv (invIso Iso-⊤⊎⊤-Bool))
                     (compRingEquiv (CohomologyRing-Coproduct Unit Unit)
                                    (Coproduct-Equiv.Coproduct-Equiv-12 CohomologyRing-Unitℤ CohomologyRing-Unitℤ))

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2015-06-11, issue reported by Peter Thiemann
-- Ulf, 2015-09-23:
--   This test was still taking 12s, which is annoyingly much.
--   I commented out a few of the constructors to bring it down
--   to 2s. With agda-2.4.2 it checks in 18s, which should be long
--   enough to notice.

open import Common.Coinduction

mutual

  -- an stype

  data SType' : Set where
    Skip : SType'
    Semi : ∞ SType' → ∞ SType' → SType'
    Case : ∞ SType' → ∞ SType' → SType'
    c    : (SType' → SType') → SType'

  -- equivalence

  data _∼_ : SType' → SType' → Set where
    ∼-Skip : Skip ∼ Skip
    ∼-Case : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Case s₁ s₂ ∼ Case s₁' s₂'
    ∼-Semi : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Semi s₁ s₂ ∼ Semi s₁' s₂'
    ∼-Semi-Skip-Left-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → Semi s₁ s₂ ∼ s₃
    -- ∼-Semi-Skip-Right-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → Semi s₁ s₂ ∼ s₃
    -- ∼-Semi-Skip-Left-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → s₃ ∼ Semi s₁ s₂
    -- ∼-Semi-Skip-Right-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → s₃ ∼ Semi s₁ s₂
    ∼-Semi-Case-Left : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
      → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Case sl1 sl2 ∼ Semi sr s₃
    ∼-Semi-Case-Right : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
      → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Semi sr s₃ ∼ Case sl1 sl2

  -- reflexivity

  ∼-refl : (s : SType') → s ∼ s
  ∼-refl Skip = ∼-Skip
  ∼-refl (Semi x x₁) = ∼-Semi (♯ ∼-refl (♭ x)) (♯ ∼-refl (♭ x₁))
  ∼-refl (Case s₁ s₂) = ∼-Case (♯ ∼-refl (♭ s₁)) (♯ ∼-refl (♭ s₂))
  ∼-refl (c f)        = {!!}

  -- symmetry

  ∼-sym : ∀ {s₁ s₂} → s₁ ∼ s₂ → s₂ ∼ s₁
  ∼-sym ∼-Skip = ∼-Skip
  ∼-sym (∼-Case s₁' s₂') = ∼-Case (♯ ∼-sym (♭ s₁')) (♯ ∼-sym (♭ s₂'))
  ∼-sym (∼-Semi s₁' s₂') = ∼-Semi (♯ ∼-sym (♭ s₁')) (♯ ∼-sym (♭ s₂'))
  ∼-sym (∼-Semi-Skip-Left-Left s₁∼s₂ s₁∼s₃) = {!∼-Semi-Skip-Left-Right s₁∼s₂ s₁∼s₃!}
  -- ∼-sym (∼-Semi-Skip-Right-Left s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Right-Right s₁∼s₂ s₁∼s₃
  -- ∼-sym (∼-Semi-Skip-Left-Right s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Left-Left s₁∼s₂ s₁∼s₃
  -- ∼-sym (∼-Semi-Skip-Right-Right s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Right-Left s₁∼s₂ s₁∼s₃
  ∼-sym (∼-Semi-Case-Left sl1 sl2 sr) = ∼-Semi-Case-Right sl1 sl2 sr
  ∼-sym (∼-Semi-Case-Right sl1 sl2 sr) = ∼-Semi-Case-Left sl1 sl2 sr

  -- transitivity

  ∼-trans : ∀ {s₁ s₂ s₃} → s₁ ∼ s₂ → s₂ ∼ s₃ → s₁ ∼ s₃
  ∼-trans ∼-Skip ∼-Skip = ∼-Skip
  -- ∼-trans ∼-Skip (∼-Semi-Skip-Left-Right x x₁) = ∼-Semi-Skip-Left-Right x x₁
  -- ∼-trans ∼-Skip (∼-Semi-Skip-Right-Right x x₁) = ∼-Semi-Skip-Right-Right x x₁
  ∼-trans (∼-Case x x₁) (∼-Case x₂ x₃) = ∼-Case (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃))
  -- ∼-trans (∼-Case x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = ∼-Semi-Skip-Left-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Case (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  -- ∼-trans (∼-Case x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = ∼-Semi-Skip-Right-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Case (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  ∼-trans (∼-Case x x₁) (∼-Semi-Case-Left x₂ x₃ x₄) = ∼-Semi-Case-Left (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃)) x₄
  ∼-trans (∼-Semi x x₁) (∼-Semi x₂ x₃) = ∼-Semi (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃))
  ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = ∼-Semi-Skip-Left-Left (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃))
  -- ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = ∼-Semi-Skip-Right-Left (♯ ∼-trans (♭ x₁) (♭ x₂)) (♯ ∼-trans (♭ x) (♭ x₃))
  -- ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = ∼-Semi-Skip-Left-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Semi (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  -- ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = ∼-Semi-Skip-Right-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Semi (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  ∼-trans (∼-Semi x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = ∼-Semi-Case-Right (♯ ∼-trans (♭ x₂) (∼-Semi (♯ ∼-refl _) (♯ ∼-sym (♭ x₁)))) (♯ ∼-trans (♭ x₃) (∼-Semi (♯ ∼-refl _) (♯ ∼-sym (♭ x₁)))) (♯ ∼-trans (♭ x) (♭ x₄))
  ∼-trans (∼-Semi-Skip-Left-Left x x₁) ∼-Skip = ∼-Semi-Skip-Left-Left x x₁
  ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Case x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Case x₂ x₃))
  ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi x₂ x₃))
  ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Left-Left x₂ x₃))
  -- ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Right-Left x₂ x₃))
  -- ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Left-Right x₂ x₃))
  -- ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Right-Right x₂ x₃))
  ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Case-Left x₂ x₃ x₄) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Case-Left x₂ x₃ x₄))
  ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Case-Right x₂ x₃ x₄))
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) ∼-Skip = ∼-Semi-Skip-Right-Left x x₁
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Case x₂ x₃) = ∼-Semi-Skip-Right-Left x (♯ ∼-trans (♭ x₁) (∼-Case x₂ x₃))
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Right-Left x (♯ ∼-trans (♭ x₁) (∼-Semi x₂ x₃))
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Case-Left x₂ x₃ x₄) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = {!!}
  --∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Left-Right (♯ ∼-trans (∼-sym (♭ x₂)) (♭ x)) (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x₁))
  -- ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Right-Right (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x)) (♯ ∼-trans (∼-sym (♭ x₂)) (♭ x₁))
  -- ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = {!!}
  -- ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = {!!}
  ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi x₃ x₄) = ∼-Semi-Case-Left {!!} (♯ ∼-trans (♭ x₁) (∼-Semi (♯ ∼-refl _) x₄)) (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x₂))
  ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Left-Left x₃ x₄) = {!!}
  -- ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Right-Left x₃ x₄) = {!!}
  -- ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Left-Right x₃ x₄) = {!!}
  -- ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Right-Right x₃ x₄) = {!!}
  ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Case-Right x₃ x₄ x₅) = {!!}
  ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Case x₃ x₄) = ∼-Semi-Case-Right (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x)) (♯ ∼-trans (∼-sym (♭ x₄)) (♭ x₁)) x₂
  -- ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Semi-Skip-Left-Right x₃ x₄) = {!!}
  -- ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Semi-Skip-Right-Right x₃ x₄) = {!!}
  ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Semi-Case-Left x₃ x₄ x₅) = {!!}


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

-- Big-O bound on the cost of a computation.

open import Calf.CostMonoid

module Calf.Types.BigO (costMonoid : CostMonoid) where

open CostMonoid costMonoid

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.Step costMonoid

open import Calf.Types.Nat using (nat)
open import Calf.Types.Bounded costMonoid

open import Data.Nat as Nat using (ℕ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

[_]*_ : ℕ → ℂ → ℂ
[ ℕ.zero  ]* c = zero
[ ℕ.suc k ]* c = c + [ k ]* c

record given_measured-via_,_∈𝓞_
  (A : tp pos) {B : tp pos}
  (∣_∣ : val A → val nat)
  (f : cmp (Π A λ _ → F B)) (g : ℕ → ℂ) : □
  where
    constructor _≤n⇒f[n]≤_g[n]via_
    field
      n' : val nat
      k : val nat
      h : ∀ x → n' Nat.≤ ∣ x ∣ → IsBounded B (f x) ([ k ]* g ∣ x ∣)

_≤n⇒f[n]≤g[n]via_ : ∀ {A B f ∣_∣ g} → (n' : val nat) → (∀ x → n' Nat.≤ ∣ x ∣ → IsBounded B (f x) (g ∣ x ∣)) → given A measured-via ∣_∣ , f ∈𝓞 g
n' ≤n⇒f[n]≤g[n]via h = n' ≤n⇒f[n]≤ 1 g[n]via (λ x h≤ → Eq.subst (IsBounded _ _) (Eq.sym (+-identityʳ _)) (h x h≤))

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
import      Lvl
open import Type

module Data.ListSized {ℓ} (T : Type{ℓ}) where

import      Data.IndexedList
open import Functional
open import Numeral.Natural

open Data.IndexedList(T){ℕ} using (IndexedList ; intro)

-- A list is a container/collection with elements in order and which allows multiples
List : ℕ → Type{ℓ}
List(n) = IndexedList(intro 𝟎 (const 𝐒))(n)

open Data.IndexedList(T){ℕ} using (∅ ; _⊰_ ; singleton) public

elim = Data.IndexedList.elim(T){ℕ} (intro 𝟎 (const 𝐒))

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:
module SizedPoly.SimpleCell where

open import Data.Product
open import Data.String.Base

open import Size
open import Level using (_⊔_) renaming (suc to lsuc; zero to lzero)

open import SizedPolyIO.Object
open import SizedPolyIO.IOObject
open import SizedPolyIO.ConsoleObject

open import SizedPolyIO.Base
open import SizedPolyIO.Console hiding (main)

open import NativePolyIO

data CellMethod A : Set where
    get : CellMethod A
    put : A → CellMethod A

CellResponse : ∀{A} → CellMethod A → Set
CellResponse {A} get = A
CellResponse (put _) = Unit

-- cellI is the interface of the object of a simple cell
cellI : (A : Set) → Interface lzero lzero
Method  (cellI A)    =  CellMethod A
Result  (cellI A) m  =  CellResponse m

-- cellC is the type of consoleObjects with interface (cellI String)
CellC : (i : Size) → Set
CellC i = ConsoleObject i (cellI String)

-- cellP is constructor for the consoleObject for interface (cellI String)
cellP : ∀{i} (s : String) → CellC i
force (method (cellP s) get) =
  exec' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  return (s , cellP s)
force (method (cellP s) (put x)) =
  exec' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  return (_ , (cellP x))

-- Program is another program
program : String → IOConsole ∞ Unit
program arg =
  let c₀ = cellP "Start" in
  method c₀ get       >>= λ{ (s , c₁) →
  exec1 (putStrLn s)         >>
  method c₁ (put arg) >>= λ{ (_ , c₂) →
  method c₂ get       >>= λ{ (s' , c₃) →
  exec1 (putStrLn s')        }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Type.Equiv where

open import Function.Proofs
open import Logic.Predicate
import      Lvl
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Setoid
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂ : Lvl.Level

-- Invertible function existence.
-- The standard equivalence/isomorphism for types.
_≍_ : (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ → Type
A ≍ B = ∃(InversePair{A = A}{B = B})

open import Logic.Propositional.Theorems using ([↔]-reflexivity ; [↔]-symmetry ; [↔]-transitivity)
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties

module _ {ℓ ℓₑ} ⦃ equiv : ∀{T : Type{ℓ}} → Equiv{ℓₑ}(T) ⦄ where
  [≍]-reflexivity : Reflexivity{T = Type{ℓ}}(\A B → (A ≍ B))
  Reflexivity.proof [≍]-reflexivity = [∃]-intro _ ⦃ id-inversePair ⦄

  [≍]-symmetry : Symmetry{T = Type{ℓ}}(\A B → (A ≍ B))
  Symmetry.proof [≍]-symmetry _ = [∃]-intro _ ⦃ sym-inversePair ⦄

  module _ ⦃ func : ∀{A B : Type{ℓ}}{f : A → B} → Function(f) ⦄ where
    [≍]-transitivity : Transitivity{T = Type{ℓ}}(\A B → (A ≍ B))
    Transitivity.proof [≍]-transitivity ([∃]-intro xy ⦃ p ⦄) ([∃]-intro yz ⦃ q ⦄) = [∃]-intro _ ⦃ trans-inversePair ⦃ inv₁ = p ⦄ ⦃ inv₂ = q ⦄ ⦄

    [≍]-equivalence : Equivalence{T = Type{ℓ}}(\A B → (A ≍ B))
    [≍]-equivalence = intro ⦃ [≍]-reflexivity ⦄ ⦃ [≍]-symmetry ⦄ ⦃ [≍]-transitivity ⦄


text:
module defns where

open import prelude

record NavigationHistory(D : Set) : Set₁ where

  field A : Subset(D)
  field Fo : Forest(D)
  field FTO : FiniteTotalOrder(D)
  field Eq : Equivalence(D)

  open FiniteTotalOrder FTO public
  open Forest Fo public
  open Equivalence Eq public

  field active : D → D
  field active-A : ∀ d → A(active d)
  field active-~ : ∀ d → (active d ~ d)
  field active-uniq : ∀ d e → A(e) → (d ~ e) → (e ≡ active d)

  field ⇒-impl-≤ : ∀ d e → (d ⇒ e) → (d ≤ e)

  _≲_ : Rel(D)
  (d ≲ e) = (d < e) ∧ (d ~ e)

  ≲-trans : ∀ {d e f} → (d ≲ e) → (e ≲ f) → (d ≲ f)
  ≲-trans (d<e , d~e) (e<f , e~f) = ((<-trans d<e e<f) , (~-trans d~e e~f))

  ≲-impl-< : ∀ {d e} → (d ≲ e) → (d < e)
  ≲-impl-< (d<e , d~e) = d<e

  ≲-impl-~ : ∀ {d e} → (d ≲ e) → (d ~ e)
  ≲-impl-~ (d<e , d~e) = d~e

  active-~-impl-≡ : ∀ {d e} → (d ∈ A) → (e ∈ A) → (d ~ e) → (d ≡ e)
  active-~-impl-≡ {d} {e} d∈A e∈A d~e = trans (active-uniq d d d∈A ~-refl) (sym (active-uniq d e e∈A d~e))

  SessionPast : D → Subset(D)
  SessionPast(d) e = (e ≲ d)

  SessionFuture : D → Subset(D)
  SessionFuture(d) e = (d ≲ e)

  JointSessionPast : Subset(D)
  JointSessionPast d = Inhabited (A ∩ SessionFuture(d))

  JointSessionFuture : Subset(D)
  JointSessionFuture d = Inhabited (A ∩ SessionPast(d))

  CanGoBack : Subset(D)
  CanGoBack d = Inhabited(SessionPast(d))

  FwdTarget : Subset(D)
  FwdTarget = Min(JointSessionFuture)

  BackTarget : Subset(D)
  BackTarget = Max(A ∩ CanGoBack)

  FwdTarget* : ∀ {n} → Subset(D ^ n)
  FwdTarget* = Min*(Increasing ∩ All(JointSessionFuture))

  BackTarget* : ∀ {n} → Subset(D ^ n)
  BackTarget* = Max*(Decreasing ∩ All((A ∪ JointSessionPast) ∩ CanGoBack))

open NavigationHistory public using (FwdTarget ; BackTarget ; FwdTarget* ; BackTarget*)

_traverse-to_ : ∀ {D} → NavigationHistory(D) → D → NavigationHistory(D)
H traverse-to d = H′ where

  D = _
  open NavigationHistory H

  A′ : Subset(D)
  A′(e) = (¬(d ~ e) ∧ A(e)) ∨ (d ≡ e)

  active′ : D → D
  active′ e with (d ~? e)
  active′ e | in₁ d~e = d
  active′ e | in₂ ¬d~e = active e

  active′-A′ :  ∀ d → A′(active′ d)
  active′-A′ e with (d ~? e)
  active′-A′ e | in₁ d~e = in₂ refl
  active′-A′ e | in₂ ¬d~e = in₁ ((λ d~ae → ¬d~e (~-trans d~ae (active-~ e))) , active-A e)

  active′-~ :  ∀ d → (active′ d ~ d)
  active′-~ e with (d ~? e)
  active′-~ e | in₁ d~e = d~e
  active′-~ e | in₂ ¬d~e = active-~ e

  active′-uniq : ∀ d e → A′ e → (d ~ e) → (e ≡ active′ d)
  active′-uniq e f (in₁ (¬d~f , f∈A)) e~f with (d ~? e)
  active′-uniq e f (in₁ (¬d~f , f∈A)) e~f | in₁ d~e = contradiction (¬d~f (~-trans d~e e~f))
  active′-uniq e f (in₁ (¬d~f , f∈A)) e~f | in₂ ¬d~e = active-uniq e f f∈A e~f
  active′-uniq e .d (in₂ refl) e~d with (d ~? e)
  active′-uniq e .d (in₂ refl) e~d | in₁ d~e = refl
  active′-uniq e .d (in₂ refl) e~d | in₂ ¬d~e = contradiction (¬d~e (~-sym e~d))

  H′ = record { A = A′ ; Fo = Fo ; FTO = FTO ; Eq = Eq
              ; active = active′ ; active-A = active′-A′ ; active-~ = active′-~ ; active-uniq = active′-uniq
              ; ⇒-impl-≤ = ⇒-impl-≤ }

WellFormed : ∀ {D} → (NavigationHistory(D)) → Set
WellFormed H = ∀ {a b c d} → (a ≲ b) → (c ≲ d) → (a ∈ A) → (d ∈ A) → (d ≤ b) where open NavigationHistory H

_traverses-to_ : ∀ {D n} → NavigationHistory(D) → (D ^ n) → NavigationHistory(D)
(H traverses-to nil) = H
(H traverses-to (d ∷ ds)) = (H traverse-to d) traverses-to ds

_traverse-from_∵_ : ∀ {D} (H : NavigationHistory(D)) d →
  let open NavigationHistory H in
  (d ∈ CanGoBack) →
  NavigationHistory(D)
(H traverse-from d ∵ d∈CGB) with max(SessionPast(d)) ∵ d∈CGB where open NavigationHistory H
(H traverse-from d ∵ d∈CGB) | (c , _) = (H traverse-to c)

_traverses-from_∵_ : ∀ {D n} (H : NavigationHistory(D)) (ds : D ^ n) →
  let open NavigationHistory H in
  (ds ∈ All(CanGoBack)) →
  NavigationHistory(D)
(H traverses-from nil ∵ tt) = H
(H traverses-from (d ∷ ds) ∵ (d∈CGB , ds∈CGB)) = (H traverse-from d ∵ d∈CGB) traverses-from ds ∵ ds∈CGB

data _traverses-by_to_ {D} (H : NavigationHistory(D)) : ℤ → (H : NavigationHistory(D)) → Set where
  fwd : ∀ {δ} (ds : D ^ (succ δ)) → (ds ∈ FwdTarget*(H)) → (H traverses-by (succ δ) to (H traverses-to ds))
  back : ∀ {δ} (ds : D ^ δ) ds∈CGB → (ds ∈ BackTarget*(H)) → (H traverses-by (-ve δ) to (H traverses-from ds ∵ ds∈CGB))

max_stars_repo_name: cbrewster/ServoNavigation

max_issues_repo_name: cbrewster/ServoNavigation

max_forks_repo_name: cbrewster/ServoNavigation


text:
{-# OPTIONS --without-K #-}
-- Big-endian binary natural numbers in agda.
-- The type of natural numbers is called Simp, because of a canonical bijection between (binary) natural numbers
-- and the simplices of the standard ∞-dimensional simple.
-- The type of bineary natural numbers with leading zeros is called Face, because of a canonical biejction
-- between such data and face maps of standard simplices.
-- For both data types, we keep track of the number of bits and the number of 1's in the type signature.
-- This is because we are interested in thinking about face maps, and this data encodes the (co)domains of these maps.
-- Based off little-endian agda code by Anders Mortberg
-- https://github.com/agda/cubical/blob/master/Cubical/Data/BinNat/BinNat.agda

-- Besides a few variants of the successor relation (we do not prove the relation is functional here),
-- This module also provides the relation isPB, which is relevant to the simplicial interpretation of
-- binary natural numbers.
module big-endian where
  open import Data.Nat

  -- A "simplex" is the same thing as a big-endian natural number.
  data Simp : ∀ (n : ℕ) →
              ∀ (d : ℕ) →
              Set
  -- A "face" is the same thing as a big-endian natural number, possibly with leading zeros.
  data Face : ∀ (n : ℕ) →
              ∀ (d : ℕ) →
              Set
  -- This mutually inductive definition is inspired by a definition of little-endian natural numbers
  -- which Anders Mortberg has implemented in Agda.
  -- A simplex is either empty, or it's a face capped by a leading 1.
  data Simp where
    emp : Simp zero zero
    1x : ∀ {n d : ℕ} → Face n d →
         Simp (suc n) (suc d)
  -- A face is either just (the inclusion of) a simplex, or it's a face capped with a leading 0.
  data Face where
    inc : ∀ {n d : ℕ} → Simp n d →
          Face n d
    0x : ∀ {n d : ℕ} → Face n d →
         Face (suc n) d

  -- These tell you if there is a carry when taking the successor of your simplex / face.
  -- That is, they hold if and only if your simplex / face is all 1's.
  data ModCarryS : ∀ {n d : ℕ} → Simp n d →
                   Set
  data ModCarryF : ∀ {n d : ℕ} → Face n d →
                   Set
  data ModCarryS where
    empcarry : ModCarryS emp
    1carry : ∀ {n d : ℕ} → ∀ {F : Face n d} → ModCarryF F →
             ModCarryS (1x F)
  data ModCarryF where
    inccarry : ∀ {n d : ℕ} → ∀ {S : Simp n d} → ModCarryS S →
               ModCarryF (inc S)

  -- isModSuc F sF holds iff
  -- F and sF have the same number n of bits AND sF is the successor of F MODULO 2^n
  -- (isModSuc might be redundant, Really just need it for the carry-over from 1111 to 0000.
  --  This could be done by hand;
  -- possibly it would be annoying if you needed some simplex to be definitionally equal to 1111 to invoke it?)
  data isModSuc : ∀ {n d : ℕ} → Face n d →
                  ∀ {d' : ℕ} → Face n d' →
                  Set
  --Then isSucF F sF holds iff
  --F,sF have the same number on of bits AND sF is the successor of F (in particular, 2^n - 1 has no "flat successor")
  --Apologies: "flat successor" is a weird name.
  data isSucF : ∀ {n d : ℕ} → Face n d →
                ∀ {d' : ℕ} → Face n (suc d') →
                Set
  --isSuc is a vanilla successor indicator:
  -- isSuc S sS holds iff suc(S) = sS (they may fail to have the same number of bits)
  data isSuc : ∀ {n d : ℕ} → Simp n d →
               ∀ {n' d' : ℕ} → Simp (suc n') (suc d') →
               Set
  data isModSuc where
    -- suc(0) = 0 mod 2^0
    msemp : isModSuc (inc emp) (inc emp)
    -- The mod-successor of 1111 is 0000.
    mscarry : ∀ {n d : ℕ} → ∀ {F : Face n d} → ∀ {d' : ℕ} → ∀ {msF : Face n d'} → isModSuc F msF →
                    ModCarryF F →
                    isModSuc (inc (1x F)) (0x msF)
    -- If F has a successor sF with the same number of bits, then suc(0F) = 0(sF) (with the same number of bits).
    ms0x : ∀ {n d : ℕ} → ∀ {F : Face (suc n) d} → ∀ {d' : ℕ} → ∀ {sF : Face (suc n) (suc d')} → isSucF F sF →
                isModSuc (0x F) (0x sF)
    -- If F has a successor sF with the same number of bits, then suc(1F) = 1(sF) (with the same number of bits).
    ms1x : ∀ {n d : ℕ} → ∀ {F : Face (suc n) d} → ∀ {d' : ℕ} → ∀ {sF : Face (suc n) (suc d')} → isSucF F sF →
                isModSuc (inc (1x F)) (inc (1x sF))
  data isSucF where
    -- Note that (inc emp) has no flat-successor.
    --- This says that the successor of 01111 is 10000 (with the same number of bits)
    sfcarry : ∀ {n d : ℕ} → ∀ {F : Face n d} → ∀ {d' : ℕ} → ∀ {msF : Face n d'} → isModSuc F msF →
                   ModCarryF F →
                   isSucF (0x F) (inc (1x msF))
    -- This says that if F has a successor sF with the same number of bits,
    -- then suc(0F) = 0(sF) (with the same number of bits)
    sf0x : ∀ {n d : ℕ} → ∀ {F : Face (suc n) d} → ∀ {d' : ℕ} → ∀ {sF : Face (suc n) (suc d')} → isSucF F sF →
                isSucF (0x F) (0x sF)
    -- This says that if F has a successor sF with the same number of bits,
    -- then suc(1F) = 1(sF) (with the same number of bits)
    sf1x : ∀ {n d : ℕ} → ∀ {F : Face (suc n) d} → ∀ {d' : ℕ} → ∀ {sF : Face (suc n) (suc d')} → isSucF F sF →
                isSucF (inc (1x F)) (inc (1x sF))
  data isSuc where
    -- This says that if (inc S) has a successor (inc sS) with the same number of bits, then S has a successor sS
    fromsf : ∀ {n d : ℕ} → ∀ {S : Simp (suc n) d} → ∀ {d' : ℕ} → ∀ {sS : Simp (suc n) (suc d')} → isSucF (inc S) (inc sS) →
                  isSuc S sS
    -- This says that if (inc S) has a mod-successor msS,
    -- and if a carry happened there (so that inc S = 1111 and msS = 0000),
    -- then suc(S) = 1(msS)
    fromcarry : ∀ {n d : ℕ} → ∀ {S : Simp n d} → ∀ {d' : ℕ} → ∀ {msS : Face n d'} → isModSuc (inc S) msS →
                       ModCarryS S →
                       isSuc S (1x msS)

  -- isPB F G H holds if and only if
  -- the G-face of the ideal represented by F is the ideal represented by H.
  -- In other words, if F is an ideal and G is a face, then the pullback H of F by G is
  -- the ideal obtained by looking at the simplices in F which have 0's wherever G has 0's,
  -- and then deleting those bits where G has 0's.
  --
  -- This is again an ideal because we are pulling back along the face map G, which
  -- is an order-preserving self-map of the natural numbers.
  --
  -- G should have the same number of bits as F.
  -- The resulting H has as many bits as G has 1's.
  --
  -- It's natural for G to be of type Face, but F and H should really be of type Simp.
  -- However, the induction goes smoother if F and G are allowed to be faces.
  -- Moreover, later we will be using Face's to represent Simp's, using the "hack-y" fact
  -- that a Face with n bits is equivalent data to a Simp with =< n bits.
  --
  -- This pullback operation is similar to the composition of face maps.
  -- In fact, composition of face maps may be defined as a relation in a similar style,
  -- and when you do this, the definition looks exactly the same except for the 4th constructor below, 10pb.
  -- It differs because F and H are representing ideals rather than faces.
  -- F and H generate bigger ideals than just themselves.
  data isPB : ∀ {n d : ℕ} → ∀ (F : Face n d) →
              ∀ {m : ℕ} → ∀ (G : Face n m) →
              ∀ {l : ℕ} → ∀ (H : Face m l) →
              Set where
    -- The pullback of the empty ideal by the empty face is the empty ideal.
    emppb : isPB (inc emp) (inc emp) (inc emp)
    -- If you add a leading 0 to F and to G, you get the same pullback as before.
    00pb : ∀ {n d : ℕ} → ∀ {F : Face n d} → ∀ {m : ℕ} → ∀ {G : Face n m} → ∀ {l : ℕ} → ∀ {H : Face m l} → isPB F G H →
                isPB (0x F) (0x G) H
    -- If you add a leading 0 to F and a leading 1 to G, you tack on a leading 0 to the pullback.
    01pb : ∀ {n d : ℕ} → ∀ {F : Face n d} → ∀ {m : ℕ} → ∀ {G : Face n m} → ∀ {l : ℕ} → ∀ {H : Face m l} → isPB F G H →
                isPB (0x F) (inc (1x G)) (0x H)
    -- If you add a leading 1 to F and a leading 0 to G,
    -- your pullback will now be all 1's -- the same as pulling back G by itself.
    -- NOT CLEAR THIS IS THE BEST WAY TO ENCODE THIS!
    10pb : ∀ {n d : ℕ} → ∀ (F : Face n d) → ∀ {m : ℕ} → ∀ {G : Face n m} → ∀ {H : Face m m} → isPB G G H →
                isPB (inc (1x F)) (0x G) H
    -- If you add a leading 1 to F and to G, your pullback will have a leading 1 tacked on.
    11pb : ∀ {n d : ℕ} → ∀ {F : Face n d} → ∀ {m : ℕ} → ∀ {G : Face n m} → ∀ {l : ℕ} → ∀ {H : Face m l} → isPB F G H →
               isPB (inc (1x F)) (inc (1x G)) (inc (1x H))

  --isPadOF F 00F holds if 00F is obtained from F by tacking on an arbitrary number of leading 0's.
  -- I worry that the use of this relation is going to cause headaches trying to write pattern-matching proofs later.
  data isPadOf : ∀ {n d : ℕ} → ∀ (F : Face n d) →
                 ∀ {n' : ℕ} → ∀ (00F : Face n' d) →
                 Set where
    -- F is obtained from itself by tacking on zero leading 0's.
    reflPad : ∀ {n d : ℕ} → ∀ (F : Face n d) →
              isPadOf F F
    -- If 00F is obtained from F by tacking on leading 0's, then so is 0(00F).
    sucPad : ∀ {n d : ℕ} → ∀ {F : Face n d} → ∀ {n' : ℕ} → ∀ {00F : Face n' d} → ∀ (pf : isPadOf F 00F) →
             isPadOf F (0x 00F)

  Delta+ : ∀ (n : ℕ) → Simp n n
  Delta+ zero = emp
  Delta+ (suc n) = 1x (inc (Delta+ n))

  EmpInc : ∀ (n : ℕ) → Face n zero
  EmpInc zero = inc emp
  EmpInc (suc n) = 0x (EmpInc n)

  Point : ∀ (n : ℕ) → Simp (suc n) (suc zero)
  Point n = 1x (EmpInc n)

  predN : ℕ → ℕ
  predN zero = zero
  predN (suc n) = n

  PreDelta+ : ∀ (n : ℕ) → Face n (predN n)
  PreDelta+ zero = inc emp
  PreDelta+ (suc zero) = 0x (inc emp)
  PreDelta+ (suc (suc n)) = inc (1x (PreDelta+(suc n)))

  PreDelta : ∀ (n : ℕ) → Face (suc n) n
  PreDelta zero = 0x (inc emp)
  PreDelta (suc n) = inc (1x (PreDelta n))

max_stars_repo_name: tcampion/Semisimplicial

max_issues_repo_name: tcampion/Semisimplicial

max_forks_repo_name: tcampion/Semisimplicial


text:
module HeapLemmasForSplitting where
  open import HeapPropertiesDefs

  open import Silica

  import Relation.Binary.PropositionalEquality as Eq
  import Context

  open import Data.List.Relation.Unary.All
  import Relation.Unary
  import Data.List.Properties
  import Data.List

  open import Data.Sum
  open import Data.Maybe

  open import Data.List.Membership.DecSetoid ≡-decSetoid
  open import Data.List.Relation.Unary.Any

  open import Data.Empty

  open TypeEnvContext

  ----------- PROPERTIES OF SPLITTING -----------
  -- The results of splitting are always compatible.
  splitCompatibility : ∀ {Γ}
                       → ∀ {t₁ t₂ t₃ : Type}
                       → Γ ⊢ t₁ ⇛ t₂ / t₃
                       → t₂ ⟷ t₃
  splitCompatibility voidSplit = voidCompat
  splitCompatibility booleanSplit = booleanCompat
  splitCompatibility (unownedSplit {Γ} {t₁} {t₂} {t₃} eqNames1 eqNames2 eqPerms t3IsUnowned) = symCompat (unownedCompat t3IsUnowned (Eq.trans (Eq.sym eqNames2) eqNames1))
  splitCompatibility (shared-shared-shared {Γ} {t} eq)  = sharedCompat eq eq refl
  splitCompatibility (owned-shared notAsset) = sharedCompat refl refl refl
  splitCompatibility (states-shared x) = sharedCompat refl refl refl

  compatibleContractsHaveSameNames : ∀ {T : Type}
                                     → ∀ {t : Tc}
                                     → ∀ {t' : Tc}
                                     → contractType t ⟷ T
                                     → T ≡ contractType t'
                                     → Tc.contractName t ≡ Tc.contractName t'
  compatibleContractsHaveSameNames {T} {t} {t'} (symCompat compat) refl = sym (compatibleContractsHaveSameNames compat refl)
  compatibleContractsHaveSameNames {T} {t} {t'} (unownedCompat x x₁) refl = x₁
  compatibleContractsHaveSameNames {T} {t} {t'} (sharedCompat x x₁ x₂) refl = x₂

  typesCompatibleWithContractsAreContracts : ∀ {T : Type}
                                             → ∀ {t : Tc}
                                             → contractType t ⟷ T
                                             → ∃[ t' ] (T ≡ contractType t')

  typesCompatibleWithContractsAreContracts {T} {t} (symCompat (symCompat compat)) = typesCompatibleWithContractsAreContracts compat
  typesCompatibleWithContractsAreContracts {(contractType (tc _ _))} {(tc _ _)} (symCompat (unownedCompat {C} {C'} {perm} {perm'} x x₁)) = ⟨ tc C perm , refl ⟩
  typesCompatibleWithContractsAreContracts {(contractType (tc _ _))} {(tc _ _)} (symCompat (sharedCompat {t} {t'} x x₁ x₂)) = ⟨ t , refl ⟩
  typesCompatibleWithContractsAreContracts {T} {t} (unownedCompat {C} {C'} {perm} {perm'} refl refl) = ⟨ tc C perm' , refl ⟩
  typesCompatibleWithContractsAreContracts {T} {t} (sharedCompat {tc C Shared} {tc C' Shared} refl refl refl) = ⟨ tc C Shared , refl ⟩

  splittingRespectsHeap : ∀ {Γ}
                          → ∀ {T t₁ t₂ t₃ : Type}
                          → Γ ⊢ t₁ ⇛ t₂ / t₃
                          → T ⟷ t₁
                          → (T ⟷ t₂) × (T ⟷ t₃)

  splittingRespectsHeap {Γ} {T} {(base Void)} {(base Void)} {(base Void)} voidSplit consis = ⟨ consis , consis ⟩
  splittingRespectsHeap {Γ} {T} {.(base Boolean)} {.(base Boolean)} {.(base Boolean)} booleanSplit consis = ⟨ consis , consis ⟩

  -- t₁ => t₁ / t₃ because t₃ is Unowned.
  splittingRespectsHeap {Γ} {T} {contractType t₁} {contractType t₂} {contractType t₃} (unownedSplit {Γ} {t₁} {t₂} {t₃} x x₁ x₂ x₃) (symCompat consis) rewrite (eqContractTypes x₂ x) | (proj₂ (typesCompatibleWithContractsAreContracts {T} {t₂} consis))  =
    let
      TIsContractTypeEx = typesCompatibleWithContractsAreContracts {T} consis -- T is a contractType.
      TContractType = proj₁ TIsContractTypeEx
      TIsContractType = proj₂ TIsContractTypeEx
      compatTypes = (compatibleContractsHaveSameNames consis TIsContractType)
      C = Tc.contractName t₃
      C' = Tc.contractName TContractType
    in
      ⟨ symCompat ( Eq.subst (λ a → contractType t₂ ⟷ a) TIsContractType consis) , symCompat (unownedCompat x₃ (Eq.trans (Eq.sym x₁) compatTypes)) ⟩

  -- t1 => t1 / Unowned
  splittingRespectsHeap {Γ} {(contractType (tc C perm))} {contractType (tc C' perm')} {contractType t₂} {contractType t₃} (unownedSplit x x₁ x₂ x₃) (unownedCompat x₄ x₅) =
    ⟨ unownedCompat x₄ (Eq.trans x₅ x), unownedCompat x₄ (Eq.trans x₅ x₁) ⟩
  splittingRespectsHeap {Γ} {(contractType t)} {contractType t₁} {contractType t₂} {contractType t₃} (unownedSplit x x₁ x₂ x₃) (sharedCompat t₁Shared t₂Shared t₁t₂Names) rewrite x₂ =
    ⟨ sharedCompat t₁Shared t₂Shared (Eq.trans t₁t₂Names x) , symCompat (unownedCompat x₃ (Eq.trans (Eq.sym x₁) (Eq.sym t₁t₂Names))) ⟩

  splittingRespectsHeap {Γ} {T} {.(contractType _)} {.(contractType _)} {.(contractType _)} (shared-shared-shared x) consis = ⟨ consis , consis ⟩

  -- Owned => Shared / Shared. Requires that T be Unowned.
  splittingRespectsHeap {Γ} {T} {contractType (tc _ Owned)} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (owned-shared x) (symCompat (symCompat consis)) = splittingRespectsHeap (owned-shared x) consis
  splittingRespectsHeap {Γ} {.(contractType (tc _ _))} {contractType (tc _ Owned)} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (owned-shared x) (symCompat (unownedCompat () x₂))
  splittingRespectsHeap {Γ} {.(contractType _)} {contractType (tc _ Owned)} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (owned-shared x) (symCompat (sharedCompat () x₂ x₃))
  splittingRespectsHeap {Γ} {.(contractType (tc _ _))} {.(contractType (tc _ Owned))} {.(contractType (tc _ Shared))} {.(contractType (tc _ Shared))} (owned-shared x) (unownedCompat x₁ x₂) = ⟨ unownedCompat x₁ x₂ , unownedCompat x₁ x₂ ⟩
  splittingRespectsHeap {Γ} {.(contractType _)} {.(contractType (tc _ Owned))} {.(contractType (tc _ Shared))} {.(contractType (tc _ Shared))} (owned-shared x) (sharedCompat x₁ () x₃)

  -- States => Shared / Shared. Requires that T be Unowned.
  splittingRespectsHeap {Γ} {T} {contractType (tc _ (S _))} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (states-shared x) (symCompat (symCompat consis)) = splittingRespectsHeap (states-shared x) consis
  splittingRespectsHeap {Γ} {.(contractType (tc _ _))} {contractType (tc _ (S _))} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (states-shared x) (symCompat (unownedCompat () x₃))
  splittingRespectsHeap {Γ} {.(contractType _)} {contractType (tc _ (S _))} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (states-shared x) (symCompat (sharedCompat () x₃ x₄))
  splittingRespectsHeap {Γ} {.(contractType (tc _ _))} {contractType (tc _ (S _))} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (states-shared x) (unownedCompat x₁ x₂) =  ⟨ unownedCompat x₁ x₂ , unownedCompat x₁ x₂ ⟩
  splittingRespectsHeap {Γ} {.(contractType _)} {contractType (tc _ (S _))} {contractType (tc _ Shared)} {contractType (tc _ Shared)} (states-shared x) (sharedCompat x₂ () x₄)

  splitSymmetric : ∀ {T T'}
                   → T ⟷ T'
                   → T' ⟷ T
  splitSymmetric {T} {T'} compat = symCompat compat

 -- =================== LEMMAS RELATED TO HEAP CONSISTENCY =================

  -- If a location is in ρ, then there is a corresponding item in envTypesList.
  findLocationInEnvTypes : ∀ {Σ Δ l o T forbiddenRefs}
                           → (envTypesList : List Type)
                           → EnvTypes Σ (Δ ,ₗ l ⦂ T) o forbiddenRefs envTypesList
                           → IsConnectedTypeList envTypesList
                           → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l ⦂ objVal o)
                           → T ∈ₜ envTypesList × All (λ T' → (T' ≢ T) → T ⟷ T') envTypesList
-- The argument will have the form: look, I found T in envTypes, so it must be compatible with everything in fieldTypes already.
  findLocationInEnvTypes {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {Δ} {l} {o} {T} .(T' ∷ R)
    (envTypesConcatMatchFound {R = R} {l = l₁} {T = T'} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = forbiddenRefs} .(Δ ,ₗ l ⦂ T) o envTypes l₁HasTypeT l₁NotForbidden)
    (consTypeList firstConnected restConnected)
    lInρ with l ≟ l₁
  ... | yes lEql₁ =
    -- We must have T' ≡ T because we looked up l in (Δ ,ₗ l ⦂ T).
    let
      TInEnvTypesList =  here (Eq.sym TEqContractTypet₁)
      TCompatWithRest = transformConnected R (Eq.subst (λ a → All (λ T' → a ⟷ T') R) TEqContractTypet₁ firstConnected)
    in
      ⟨ TInEnvTypesList ,  (λ TNeqT' → ⊥-elim (TNeqT' (TEqContractTypet₁))) ∷ TCompatWithRest ⟩ -- Eq.subst (λ a → All (λ a → T ⟷ a) (T' ∷ R)) TEqContractTypet₁ firstConnected ⟩
    where
      lInΔ' : ((StaticEnv.locEnv Δ) , l ⦂ T) ∋ l ⦂ T
      lInΔ' = Z

      TEqContractTypet₁ : T' ≡ T
      TEqContractTypet₁ = contextLookupUnique l₁HasTypeT (Eq.subst (λ a → (StaticEnv.locEnv Δ) TypeEnvContext., l ⦂ T ∋ a ⦂ T) lEql₁ lInΔ')

      transformConnected : ∀ L → All (λ T' → T ⟷ T') L → All (λ T' → (T' ≢ T) → T ⟷ T') L
      transformConnected L [] = []
      transformConnected (T' ∷ L) (h ∷ r) =  (λ tNeqT' → h) ∷ (transformConnected L r)
  ... | no lNeql₁ =
      -- envTypesList is T ∷ R, but T is not the one we were interested in. l ⦂ o is in ρ, but not at the end.
      -- Eventually we'll look up l in  (Δ ,ₗ l ⦂ T) and find T.
    let
      lInRestOfρ = IndirectRefContext.irrelevantReductionsOK lInρ lNeql₁
      recurse = findLocationInEnvTypes {re μ ρ φ ψ} {Δ} {l} {o} {T} R envTypes restConnected lInRestOfρ
      TInR = proj₁ recurse
      TCompatT' = Data.List.Relation.Unary.All.lookup firstConnected TInR
    in
      ⟨ there TInR , (λ TNeqT' → symCompat TCompatT') ∷ proj₂ recurse ⟩ -- firstConnected ⟩
  findLocationInEnvTypes {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {Δ} {l} {o} {T} envTypesList
    (envTypesConcatMatchNotFound {R = .envTypesList} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = forbiddenRefs} .(Δ ,ₗ l ⦂ T) o envTypes lNotInΔ')
    connected
    lInρ =
      let
        lNeql₁ = ≢-sym (∉dom-≢ lNotInΔ')
        lInRestOfρ = IndirectRefContext.irrelevantReductionsOK lInρ lNeql₁
      in
      findLocationInEnvTypes envTypesList envTypes connected lInRestOfρ
  findLocationInEnvTypes {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o') φ ψ)} {Δ} {l} {o} {T} envTypesList
    (envTypesConcatMismatch {R = .envTypesList} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = forbiddenRefs} .(Δ ,ₗ l ⦂ T) o o' oNeqo' envTypes)
    connected
    lInρ =
      let
        -- from o ≢ o' I need to prove that objVal o ≢ objVal o'
        -- so I assume objVal o ≡ objVal o' and derive o ≡ o', which is a contradiction.
        oExprNeqo'Expr = λ objValsEq → (objValInjective oNeqo') (Eq.sym objValsEq)
        lInRestOfρ = IndirectRefContext.irrelevantReductionsInValuesOK lInρ oExprNeqo'Expr
      in
        findLocationInEnvTypes envTypesList envTypes connected lInRestOfρ

  -- If a list of types was all compatible with the env types for (Δ ,ₗ l ⦂ T), then everything in that list is compatible with T.
  prevCompatibilityImpliesCompatibility : ∀ {Σ Δ l o T}
                                          → (RT : RefTypes Σ (Δ ,ₗ l ⦂ T) o)
                                          → (TL : List Type)
                                          → All (λ T → All (_⟷_ T) TL) (RefTypes.envTypesList RT)
                                          → IsConnectedTypeList (RefTypes.envTypesList RT)
                                          → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l ⦂ objVal o)
                                          → All (_⟷_ (T)) TL
  prevCompatibilityImpliesCompatibility {Σ} {Δ} {l} {o} {T} RT TL envTypesCompatibleWithTypes connected lInρ =
    let
      TInEnvTypes = proj₁ (findLocationInEnvTypes (RefTypes.envTypesList RT) (RefTypes.envTypes RT) connected lInρ)
    in
      Data.List.Relation.Unary.All.lookup envTypesCompatibleWithTypes TInEnvTypes

  envTypesForbiddenRefsObserved : ∀ {l forbiddenRefs T T' Σ R}
                                  → (Δ : StaticEnv)
                                  → (o : ObjectRef)
                                  → l ∈ forbiddenRefs
                                  → EnvTypes Σ (Δ ,ₗ l ⦂ T) o forbiddenRefs R
                                  → EnvTypes Σ (Δ ,ₗ l ⦂ T') o forbiddenRefs R

      -- We previously found l₁ ⦂ o at the END of ρ, and found l₁ : T in (Δ ,ₗ l ⦂ T). By "l₁NotInForbiddenRefs" we may derive l ≢ l₁.
      -- ρ , l₁ : objVal o
      -- WTS: when we look up l₁ in  (Δ ,ₗ l ⦂ T'), we'll still get objVal o.
  envTypesForbiddenRefsObserved {l} {forbiddenRefs} {T} {T'} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {.(T₁ ∷ R)} Δ o lInLs
    envTypes@(envTypesConcatMatchFound {R = R} {l = l₁} {T = T₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = forbiddenRefs} .(Δ ,ₗ l ⦂ T) .o origEnvTypes l₁HasTypeT₁WithL l₁NotInForbiddenRefs) =
       let
         l₁NeqL : l₁ ≢ l
         l₁NeqL = listNoncontainment l₁NotInForbiddenRefs lInLs

         l₁HasSameTypeInNewContext = irrelevantExtensionsOK {y = l} {t' = T'} (irrelevantReductionsOK l₁HasTypeT₁WithL l₁NeqL) l₁NeqL

         recursiveCall = envTypesForbiddenRefsObserved {l = l} {T = T} {T' = T'} Δ o (there lInLs) origEnvTypes
      in
         envTypesConcatMatchFound {R = R} (Δ ,ₗ l ⦂ T') o recursiveCall l₁HasSameTypeInNewContext l₁NotInForbiddenRefs

  envTypesForbiddenRefsObserved {l} {forbiddenRefs} {T} {T'} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {R} Δ o lInLs
    (envTypesConcatMatchNotFound {R = .R} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} .(Δ ,ₗ l ⦂ T) .o origEnvTypes l₁NotInDomΔ') =
      let
        prevEnvTypesObserved = envTypesForbiddenRefsObserved Δ o lInLs origEnvTypes
      in
        envTypesConcatMatchNotFound (Δ ,ₗ l ⦂ T') o prevEnvTypesObserved (∉domPreservation l₁NotInDomΔ')

  envTypesForbiddenRefsObserved {l} {forbiddenRefs} {T} {T'} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o') φ ψ)} {R} Δ o lInLs
    (envTypesConcatMismatch {R = .R} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} .(Δ ,ₗ l ⦂ T) .o o' oNeqO' origEnvTypes) =
      let
        prevEnvTypesObserved = envTypesForbiddenRefsObserved Δ o lInLs origEnvTypes
      in
        envTypesConcatMismatch (Δ ,ₗ l ⦂ T') o o' oNeqO' prevEnvTypesObserved

  envTypesForbiddenRefsObserved {l} {forbiddenRefs} {T} {T'} {.(re μ IndirectRefContext.∅ φ ψ)} {.[]} Δ o lInLs
    (envTypesEmpty {μ = μ} {φ = φ} {ψ = ψ} {Δ = .(Δ ,ₗ l ⦂ T)} {o = .o} {forbiddenRefs = .forbiddenRefs}) =
    envTypesEmpty

  -- Inversion for isConnected
  isConnectedImpliesOsConnected : ∀ {Σ Δ o R}
                                  → IsConnected Σ Δ o R
                                  → IsConnectedTypeList (RefTypes.oTypesList R)
  isConnectedImpliesOsConnected {Σ} {Δ} {o} {R} (isConnected R cl _ _ _ ) = cl

  singleElementListsAreConnected : (T : Type)
                                 → IsConnectedTypeList [ T ]
  singleElementListsAreConnected T = consTypeList [] (emptyTypeList refl)

  -- Basic properties of contexts
  ctxTypesExtension : ∀ {Δ o T}
                      → [ T ] ≡ ctxTypes (Δ , o ⦂ T) o
  ctxTypesExtension {Δ} {o} {T} with o ≟ o
  ... | yes oEq = refl
  ... | no oNeq = ⊥-elim (oNeq refl)

  ctxTypesExtensionNeq : ∀ {Δ o o' T}
                         → o' ≢ o
                         → ctxTypes (Δ , o ⦂ T) o' ≡ ctxTypes Δ o'
  ctxTypesExtensionNeq {Δ} {o} {o'} {T} oNeq with o' ≟ o
  ... | yes p = ⊥-elim (oNeq p)
  ... | no ¬p = refl

  t₁CompatibilityImpliest₂Compatibility : ∀ {Γ TL T₁ T₂ T₃}
                                          → All (λ T' → T₁ ⟷ T') TL
                                          →  Γ ⊢ T₁ ⇛ T₂ / T₃
                                          → All (λ T' → T₂ ⟷ T') TL
  t₁CompatibilityImpliest₂Compatibility {Γ} {.[]} {T₁} {T₂} {T₃} [] spl = []
  t₁CompatibilityImpliest₂Compatibility {Γ} {.(x ∷ xs)} {T₁} {T₂} {T₃} (_∷_ {x = x} {xs = xs} TCompat restCompat) spl =
    let
      TCompat' = proj₁ (splittingRespectsHeap spl (symCompat TCompat))
    in
      (symCompat TCompat') ∷ t₁CompatibilityImpliest₂Compatibility restCompat spl

  t₁CompatibilityImpliest₃Compatibility : ∀ {Γ TL T₁ T₂ T₃}
                                          → All (λ T' → T₁ ⟷ T') TL
                                          →  Γ ⊢ T₁ ⇛ T₂ / T₃
                                          → All (λ T' → T₃ ⟷ T') TL
  t₁CompatibilityImpliest₃Compatibility {Γ} {.[]} {T₁} {T₂} {T₃} [] spl = []
  t₁CompatibilityImpliest₃Compatibility {Γ} {.(x ∷ xs)} {T₁} {T₂} {T₃} (_∷_ {x = x} {xs = xs} TCompat restCompat) spl =
    let
      TCompat' = proj₂ (splittingRespectsHeap spl (symCompat TCompat))
    in
      (symCompat TCompat') ∷ t₁CompatibilityImpliest₃Compatibility restCompat spl

  connectedTypeListsAreConnected : ∀ {T Ts}
                                    → IsConnectedTypeList Ts
                                    → (TIncluded : T ∈ₜ Ts)
                                    → (T'Included : T ∈ₜ Ts)
                                    → TIncluded ≢ T'Included
                                    → T ⟷ T
  connectedTypeListsAreConnected {.x} {.(x ∷ xs)} TsConnected (here {x = x} {xs = xs} refl) (here {x = .x} {xs = .xs} refl) TNeqT' = ⊥-elim (TNeqT' refl)
  connectedTypeListsAreConnected {T} {.(T ∷ D)} (consTypeList {T = .T} {D = D} TConnectedToRest TsConnected) (here {x = .T} {xs = .D} refl) (there {x = .T} {xs = .D} T'InTs) TNeqT' = Data.List.Relation.Unary.All.lookup TConnectedToRest T'InTs
  connectedTypeListsAreConnected {T} {.(T ∷ D)} (consTypeList {T = .T} {D = D} TConnectedToRest TsConnected) (there {x = .T} {xs = .D} TInTs) (here {x = .T} {xs = .D} refl) TNeqT' =  Data.List.Relation.Unary.All.lookup TConnectedToRest TInTs
  connectedTypeListsAreConnected {T} {.(x ∷ xs)} (consTypeList {T = .x} {D = .xs} x₁ restConnected) (there {x = x} {xs = xs} TInTs) (there {x = .x} {xs = .xs} T'InTs) TNeqT' =
    connectedTypeListsAreConnected restConnected TInTs T'InTs λ prfsEqual → TNeqT' (Eq.cong there prfsEqual)

{-
  record EnvTypesForSplitResult (Σ : RuntimeEnv) (Δ : StaticEnv) (T₂ : Type) (T₃ : Type) (l : IndirectRef) (o : ObjectRef) : Set where
    field
      Ts' : List Type
      T₂Compat : (All (λ T' → T₂ ⟷ T') Ts')
      et : (EnvTypes Σ (Δ ,ₗ l ⦂ T₃) o forbiddenRefs Ts')
      connected : (IsConnectedTypeList Ts')
      externalCompat : (λ T' → All (λ T'' → T' ⟷ T'') Ts → All (λ T'' → T' ⟷ T'') Ts')
-}

  -- Trying to assume that T₁ is compatible with all the Ts is too strong, since T₁ may be in the Ts.
  -- What do I actually need here I need to show that T₂ is compatible with all the new types.
  -- So
  envTypesForSplit : ∀ {Γ Σ Δ l o T₁ T₂ T₃ Ts forbiddenRefs}
                                   → EnvTypes Σ (Δ ,ₗ l ⦂ T₁) o forbiddenRefs Ts
                                   → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l ⦂ objVal o)
                                   → All (λ T' → (T' ≢ T₁) → T₁ ⟷ T') Ts
                                   → IsConnectedTypeList Ts
                                   → Γ ⊢ T₁ ⇛ T₂ / T₃
                                   → ∃[ Ts' ] ((EnvTypes Σ (Δ ,ₗ l ⦂ T₃) o forbiddenRefs Ts') ×
                                              (All (λ T' → T₂ ⟷ T') Ts') ×
                                              (IsConnectedTypeList Ts') ×
                                              (∀ T' → All (λ T'' → T' ⟷ T'') Ts → All (λ T'' → T' ⟷ T'') Ts'))
  envTypesForSplit {Γ} {Σ@.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {Δ} {l} {o} {T₁} {T₂} {T₃} {.(T₄ ∷ R)} {forbiddenRefs}
    origMatch@(envTypesConcatMatchFound {R = R} {l = l₁} {T = T₄} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} .(Δ ,ₗ l ⦂ T₁) o origEnvTypes lookupResult l₁NotForbidden)
    lInρ
    (T₁Connected ∷ RConnected)
    (consTypeList firstConnected restConnected)
    spl with l₁ ≟ l
  ... | yes eq
    =
      -- The last step in the proof of EnvTypes (ρ , l₁ ⦂ o) (Δ ,ₗ l ⦂ T₃) o T₁∷R is that we looked up l₁ and prepended the result to the rest of the Ts.
      -- If l₁ ≡ l, then Ts' is T₃ ∷ R. Otherwise, we found l₁ ⦂ T₄ in Δ and Ts' is T₄ ∷ (recurse with the rest).
        ⟨ Ts' , ⟨ envTypesTs' , ⟨ T₂CompatWithT₃ ∷ T₂CompatWithRestOfEnvTypes ,  ⟨ (consTypeList T₃CompatWithRestOfEnvTypes restConnected) , externalCompat ⟩ ⟩ ⟩ ⟩
      where
        Ts'' = R
        Ts' = T₃ ∷ Ts''

        -- WTS: (EnvTypes Σ (Δ ,ₗ l ⦂ T₃) o Ts') × All (λ T' → T ⟷ T') Ts')
        lookupResultWithl : (StaticEnv.locEnv Δ , l ⦂ T₁) ∋ l ⦂ T₄
        lookupResultWithl = Eq.subst (λ a → StaticEnv.locEnv Δ , l ⦂ T₁ ∋ a ⦂ T₄) eq lookupResult

        origEnvTypesWithL : EnvTypes (re μ ρ φ ψ) (Δ ,ₗ l₁ ⦂ T₁) o (l₁ ∷ forbiddenRefs) R
        origEnvTypesWithL = Eq.subst (λ a → EnvTypes (re μ ρ φ ψ) (Δ ,ₗ a ⦂ T₁) o (l₁ ∷ forbiddenRefs) R) (Eq.sym eq) origEnvTypes

        forbiddenOK = envTypesForbiddenRefsObserved {T' = T₃} Δ o (here refl) origEnvTypesWithL
        forbiddenOKInL₁ : EnvTypes (re μ ρ φ ψ) (Δ ,ₗ l ⦂ T₃) o (l₁ ∷ forbiddenRefs) R
        forbiddenOKInL₁ = Eq.subst (λ a →  EnvTypes (re μ ρ φ ψ) (Δ ,ₗ a ⦂ T₃) o (l₁ ∷ forbiddenRefs) R) eq forbiddenOK

        -- We already know that the first match in ρ for o is l, so the new Ts' has to be right.
        envTypesTs' : EnvTypes Σ (Δ ,ₗ l ⦂ T₃) o forbiddenRefs Ts'
        envTypesTs' = envTypesConcatMatchFound {l = l₁} (Δ ,ₗ l ⦂ T₃) o forbiddenOKInL₁
          (Eq.subst (λ a →  StaticEnv.locEnv Δ , a ⦂ T₃ ∋ l₁ ⦂ T₃) eq Z) l₁NotForbidden

        T₄EqT₁ : T₄ ≡ T₁
        T₄EqT₁ = contextLookupUnique lookupResultWithl Z

        T₄CompatWithRestOfEnvTypes = firstConnected
        T₁CompatWithRestOfEnvTypes = Eq.subst (λ a → All (λ T' → a ⟷ T') R) T₄EqT₁ T₄CompatWithRestOfEnvTypes

        T₂CompatWithRestOfEnvTypes : All (λ T' → T₂ ⟷ T') R
        T₂CompatWithRestOfEnvTypes = t₁CompatibilityImpliest₂Compatibility T₁CompatWithRestOfEnvTypes spl

        T₂CompatWithT₃ = splitCompatibility spl

        -- Need to prove everything in R is connected to T₃, given that everything in R is connected to T₄ (≡ T₁).
        -- Follows from splittingRespectsHeap.
        T₃CompatWithRestOfEnvTypes : All (λ T' → T₃ ⟷ T') R
        T₃CompatWithRestOfEnvTypes = t₁CompatibilityImpliest₃Compatibility T₁CompatWithRestOfEnvTypes spl

        externalCompat : (T' : Type) →  All (λ T'' → T' ⟷ T'') (T₄ ∷ R) → All (λ T'' → T' ⟷ T'') Ts'
        externalCompat T' (_∷_ {x = x} {xs = xs} px T'CompatWithTs) =
          let
            T'CompatT₁ = Eq.subst (λ a →  T' ⟷ a) T₄EqT₁ px
            T'CompatT₃ = proj₂ (splittingRespectsHeap spl T'CompatT₁)
          in
            T'CompatT₃ ∷ T'CompatWithTs
  envTypesForSplit {Γ} {Σ@.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {Δ} {l} {o} {T₁} {T₂} {T₃} {.(T₄ ∷ R)} {forbiddenRefs}
    origMatch@(envTypesConcatMatchFound {R = R} {l = l₁} {T = T₄} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} .(Δ ,ₗ l ⦂ T₁) o origEnvTypes lookupResult l₁NotForbidden)
    lInρ
    (T₁Connected ∷ RConnected)
    allConnected@(consTypeList firstConnected restConnected)
    spl | no nEq with T₄ ≟t T₁
  ... | yes T₄EqT₁ =
        ⟨ Ts' , ⟨ envTypesTs' , ⟨ Ts'Compat , ⟨ consTypeList T₄CompatWithR' (proj₁ (proj₂ (proj₂ (proj₂ R'WithProof)))) , externCompatibility' ⟩ ⟩ ⟩ ⟩
      where
       -- Because we're in envTypeConcatMatchFound, l₁ ⦂ o was at the end of the context, and we found l₁ ⦂ T₄ in Δ , l ⦂ T₁.
        -- But l ≢ l₁, so we will be able to find l₁ ⦂ T₄ in Δ and use the same rule.
        -- However, there may be l's in ρ, which may result in a different R than before! Some T₁'s may be replaced with T₃'s.
        lInRestOfρ = IndirectRefContext.irrelevantReductionsOK lInρ (≢-sym nEq)
        R'WithProof = envTypesForSplit origEnvTypes lInRestOfρ RConnected restConnected spl
        R' = proj₁ R'WithProof
        Ts' = T₄ ∷ R'

        l₁InΔ : ((StaticEnv.locEnv Δ) , l ⦂ T₃) ∋ l₁ ⦂ T₄
        l₁InΔ = irrelevantExtensionsOK {t = T₄} {t' = T₃} (irrelevantReductionsOK lookupResult nEq) nEq

        envTypesTs' = envTypesConcatMatchFound (Δ ,ₗ l ⦂ T₃) o (proj₁ (proj₂ R'WithProof)) l₁InΔ l₁NotForbidden

        -- Previously, we knew that T₄ was compatible with everything in R.
        -- Specificially, we have T₁Connected : (T₄ ≢ T₁) → T₁ ⟷ T₄.
        -- Everything that was compatible with T₁ has to be compatible with T₂.

        foundLocationInRest = findLocationInEnvTypes R origEnvTypes restConnected lInRestOfρ
        T₁InR : T₁  ∈ₜ R
        T₁InR = proj₁ foundLocationInRest

        proofsNotEq : (there T₁InR) ≢ (here (Eq.sym T₄EqT₁))
        proofsNotEq ()

        T₁CompatWithT₁ : T₁ ⟷ T₁
        T₁CompatWithT₁ = connectedTypeListsAreConnected allConnected (there T₁InR) (here (Eq.sym T₄EqT₁)) proofsNotEq
        -- We found another copy of T₁ in the original envTypes. But we know the original envTypes was all connected.
        -- There has to be ANOTHER copy of T₁ in R. We know THIS T₁ is connected to THAT T₁ because THIS T₁ is connected to everything in R.
        T₂CompatWithT₁ : T₂ ⟷ T₁
        T₂CompatWithT₁ = symCompat (proj₁ (splittingRespectsHeap spl T₁CompatWithT₁))
        T₂CompatWithT₄ = Eq.subst (λ a → T₂ ⟷ a) (Eq.sym T₄EqT₁) T₂CompatWithT₁

        T₂CompatWithR' = proj₁ (proj₂ (proj₂ R'WithProof))
        Ts'Compat = T₂CompatWithT₄ ∷ T₂CompatWithR'

        externCompatibility = proj₂ (proj₂ (proj₂ (proj₂ R'WithProof)))
        T₄CompatWithR' : All (λ T' → T₄ ⟷ T') R'
        T₄CompatWithR' = externCompatibility T₄ firstConnected

        externCompatibility' : (T' : Type) →  All (λ T'' → T' ⟷ T'') (T₄ ∷ R) → All (λ T'' → T' ⟷ T'') Ts'
        externCompatibility' T' (_∷_ {x = x} {xs = xs} px T'CompatWithTs) =
          px ∷ externCompatibility T' T'CompatWithTs

  ... | no T₄NeqT₁ =
        ⟨ Ts' , ⟨ envTypesTs' , ⟨ Ts'Compat ,  ⟨ consTypeList T₄CompatWithR' (proj₁ (proj₂ (proj₂ (proj₂ R'WithProof)))) , externCompatibility' ⟩ ⟩ ⟩ ⟩
      where
        -- Because we're in envTypeConcatMatchFound, l₁ ⦂ o was at the end of the context, and we found l₁ ⦂ T₄ in Δ , l ⦂ T₁.
        -- But l ≢ l₁, so we will be able to find l₁ ⦂ T₄ in Δ and use the same rule.
        -- However, there may be l's in ρ, which may result in a different R than before! Some T₁'s may be replaced with T₃'s.
        lInRestOfρ = IndirectRefContext.irrelevantReductionsOK lInρ (≢-sym nEq)
        R'WithProof = envTypesForSplit origEnvTypes lInRestOfρ RConnected restConnected spl

        R' = proj₁ R'WithProof
        Ts' = T₄ ∷ R'

        l₁InΔ : ((StaticEnv.locEnv Δ) , l ⦂ T₃) ∋ l₁ ⦂ T₄
        l₁InΔ = irrelevantExtensionsOK {t = T₄} {t' = T₃} (irrelevantReductionsOK lookupResult nEq) nEq

        envTypesTs' = envTypesConcatMatchFound (Δ ,ₗ l ⦂ T₃) o (proj₁ (proj₂ R'WithProof)) l₁InΔ l₁NotForbidden

        -- Previously, we knew that T₄ was compatible with everything in R.
        -- Specificially, we have T₁Connected : (T₄ ≢ T₁) → T₁ ⟷ T₄.
        -- Everything that was compatible with T₁ has to be compatible with T₂.
        T₄CompatWithT₁ :  T₄ ⟷ T₁
        T₄CompatWithT₁ = symCompat (T₁Connected T₄NeqT₁)
        T₄CompatWithT₂ : T₄ ⟷ T₂
        T₄CompatWithT₂ = proj₁ (splittingRespectsHeap spl T₄CompatWithT₁)

        T₂CompatWithT₄ = symCompat T₄CompatWithT₂
        T₂CompatWithR'  = proj₁ (proj₂ (proj₂ R'WithProof))
        Ts'Compat = T₂CompatWithT₄ ∷ T₂CompatWithR'

        externCompatibility = proj₂ (proj₂ (proj₂ (proj₂ R'WithProof)))
        T₄CompatWithR' : All (λ T' → T₄ ⟷ T') R'
        T₄CompatWithR' = externCompatibility T₄ firstConnected

        externCompatibility' : (T' : Type) →  All (λ T'' → T' ⟷ T'') (T₄ ∷ R) → All (λ T'' → T' ⟷ T'') Ts'
        externCompatibility' T' (_∷_ {x = x} {xs = xs} px T'CompatWithTs) =
          px ∷ externCompatibility T' T'CompatWithTs

  envTypesForSplit {Γ} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o) φ ψ)} {Δ} {l} {o} {T₁} {T₂} {T₃} {Ts} {T}
    (envTypesConcatMatchNotFound {R = .Ts} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} .(Δ ,ₗ l ⦂ T₁) o origEnvTypes l₁NotInΔ') lInρ T₁Connected origCompat spl =
    let
      lNeql₁ = ≢-sym (∉dom-≢ l₁NotInΔ')
      lInRestOfρ = IndirectRefContext.irrelevantReductionsOK lInρ lNeql₁
      compatibilityWithOrigρ = envTypesForSplit origEnvTypes lInRestOfρ T₁Connected origCompat spl
      envTypes = envTypesConcatMatchNotFound (Δ ,ₗ l ⦂ T₃) o (proj₁ (proj₂ compatibilityWithOrigρ)) (∉domPreservation l₁NotInΔ' )
    in
      ⟨ proj₁ compatibilityWithOrigρ , ⟨ envTypes ,  proj₂ (proj₂ compatibilityWithOrigρ) ⟩ ⟩

  envTypesForSplit {Γ} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o') φ ψ)} {Δ} {l} {o} {T₁} {T₂} {T₃} {Ts} {T}
    (envTypesConcatMismatch {R = .Ts} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} .(Δ ,ₗ l ⦂ T₁) o o' oNeqo' origEnvTypes) lInρ T₁Connected origCompat spl =
      let
        oExprNeqo'Expr = λ objValsEq → (objValInjective oNeqo') (Eq.sym objValsEq)
        lInRestOfρ = IndirectRefContext.irrelevantReductionsInValuesOK lInρ oExprNeqo'Expr

        compatibilityWithOrigρ = envTypesForSplit origEnvTypes lInRestOfρ T₁Connected origCompat spl
        envTypes = envTypesConcatMismatch (Δ ,ₗ l ⦂ T₃) o o' oNeqo' (proj₁ (proj₂ compatibilityWithOrigρ))
      in
        ⟨ proj₁ compatibilityWithOrigρ , ⟨ envTypes , proj₂ (proj₂ compatibilityWithOrigρ) ⟩ ⟩

  envTypesForSplit {Γ} {.(re μ IndirectRefContext.∅ φ ψ)} {Δ} {l} {o} {T₁} {T₂} {T₃} {.[]} {T}
    (envTypesEmpty {μ = μ} {φ = φ} {ψ = ψ} {Δ = .(Δ ,ₗ l ⦂ T₁)} {o = .o}) T₁InTs T₁Connected origCompat spl =
      ⟨ [] , ⟨ envTypesEmpty , ⟨ [] , ⟨ emptyTypeList refl , (λ T' → λ a → []) ⟩ ⟩ ⟩ ⟩

  oExtensionIrrelevantToEnvTypes :  ∀ {Σ Δ R o o' forbiddenRefs T}
                                    → EnvTypes Σ Δ o' forbiddenRefs R
                                    → EnvTypes Σ (Δ ,ₒ o ⦂ T) o' forbiddenRefs R
  oExtensionIrrelevantToEnvTypes {.(re μ (ρ IndirectRefContext., l ⦂ objVal o₁) φ ψ)} {Δ} {.(T₁ ∷ R)} {o} {.o₁} {forbiddenRefs} {T}
    (envTypesConcatMatchFound {R = R} {l = l} {T = T₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} Δ o₁ envTypes x x₁) =
      let
        recurse = oExtensionIrrelevantToEnvTypes envTypes
      in
        envTypesConcatMatchFound (Δ ,ₒ o ⦂ T) o₁ recurse x x₁
  oExtensionIrrelevantToEnvTypes {.(re μ (ρ IndirectRefContext., l ⦂ objVal o₁) φ ψ)} {Δ} {R} {o} {.o₁} {forbiddenRefs} {T}
    (envTypesConcatMatchNotFound {R = .R} {l = l} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} Δ o₁ envTypes x) =
      let
        recurse = oExtensionIrrelevantToEnvTypes envTypes
      in
        envTypesConcatMatchNotFound (Δ ,ₒ o ⦂ T) o₁ recurse x
  oExtensionIrrelevantToEnvTypes {.(re μ (ρ IndirectRefContext., l ⦂ objVal o') φ ψ)} {Δ} {R} {o} {.o₁} {forbiddenRefs} {T}
    (envTypesConcatMismatch {R = .R} {l = l} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} Δ o₁ o' x envTypes) =
       let
        recurse = oExtensionIrrelevantToEnvTypes envTypes
      in
        envTypesConcatMismatch (Δ ,ₒ o ⦂ T) o₁ o' x recurse
  oExtensionIrrelevantToEnvTypes {.(re μ IndirectRefContext.∅ φ ψ)} {Δ} {.[]} {o} {o'} {forbiddenRefs} {T}
    (envTypesEmpty {μ = μ} {φ = φ} {ψ = ψ} {Δ = .Δ} {o = .o'} {forbiddenRefs = .forbiddenRefs}) =
      envTypesEmpty

  envTypesForSplitOMismatch : ∀ {Γ Σ Δ l o' T₁ T₂ T₃ Ts forbiddenRefs}
                                   → EnvTypes Σ (Δ ,ₗ l ⦂ T₁) o' forbiddenRefs Ts
                                   → IsConnectedTypeList Ts
                                   → Γ ⊢ T₁ ⇛ T₂ / T₃
                                   → ∃[ Ts' ] ((EnvTypes Σ (Δ ,ₗ l ⦂ T₃) o' forbiddenRefs Ts') ×
                                              (IsConnectedTypeList Ts') ×
                                              (∀ T' → All (λ T'' → T' ⟷ T'') Ts → All (λ T'' → T' ⟷ T'') Ts'))
  envTypesForSplitOMismatch {Γ} {Σ@.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o') φ ψ)} {Δ} {l} {.o'} {T₁} {T₂} {T₃} {.(T ∷ R)} {forbiddenRefs}
    (envTypesConcatMatchFound {R = R} {l = l₁} {T = T} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} .(Δ ,ₗ l ⦂ T₁) o' origEnvTypes lookupResult l₁NotForbidden)
    (consTypeList firstConnected restConnected)
    spl with l₁ ≟ l
  ... | yes l₁Eql =
      -- We looked up l₁ in Δ' and got T₁. We're going to give T₃ now.
      ⟨ Ts' , ⟨ envTypesTs' , ⟨ (consTypeList T₃CompatWithRestOfEnvTypes restConnected) , externalCompat ⟩ ⟩ ⟩
      where
        Ts' = T₃ ∷ R

        origEnvTypesWithL1 : EnvTypes (re μ ρ φ ψ) (Δ ,ₗ l₁ ⦂ T₁) o' (l₁ ∷ forbiddenRefs) R
        origEnvTypesWithL1 = Eq.subst (λ a → EnvTypes (re μ ρ φ ψ) (Δ ,ₗ a ⦂ T₁) o' (l₁ ∷ forbiddenRefs) R) (Eq.sym l₁Eql) origEnvTypes

        forbiddenOK = envTypesForbiddenRefsObserved {T' = T₃} Δ o' (here refl) origEnvTypesWithL1
        forbiddenOKInL₁ : EnvTypes (re μ ρ φ ψ) (Δ ,ₗ l ⦂ T₃) o' (l₁ ∷ forbiddenRefs) R
        forbiddenOKInL₁ = Eq.subst (λ a →  EnvTypes (re μ ρ φ ψ) (Δ ,ₗ a ⦂ T₃) o' (l₁ ∷ forbiddenRefs) R) l₁Eql forbiddenOK

        envTypesTs' : EnvTypes Σ (Δ ,ₗ l ⦂ T₃) o' forbiddenRefs Ts'
        envTypesTs' = envTypesConcatMatchFound ((Δ ,ₗ l ⦂ T₃)) o' forbiddenOKInL₁ ( (Eq.subst (λ a →  StaticEnv.locEnv Δ , a ⦂ T₃ ∋ l₁ ⦂ T₃) l₁Eql Z)) l₁NotForbidden

        lookupResultWithl : (StaticEnv.locEnv Δ , l ⦂ T₁) ∋ l ⦂ T
        lookupResultWithl = Eq.subst (λ a → StaticEnv.locEnv Δ , l ⦂ T₁ ∋ a ⦂ T) l₁Eql lookupResult

        TEqT₁ : T ≡ T₁
        TEqT₁ = contextLookupUnique lookupResultWithl Z

        T₄CompatWithRestOfEnvTypes = firstConnected
        T₁CompatWithRestOfEnvTypes = Eq.subst (λ a → All (λ T' → a ⟷ T') R) TEqT₁ T₄CompatWithRestOfEnvTypes

        T₂CompatWithRestOfEnvTypes : All (λ T' → T₂ ⟷ T') R
        T₂CompatWithRestOfEnvTypes = t₁CompatibilityImpliest₂Compatibility T₁CompatWithRestOfEnvTypes spl

        T₂CompatWithT₃ = splitCompatibility spl

        -- Need to prove everything in R is connected to T₃, given that everything in R is connected to T₄ (≡ T₁).
        -- Follows from splittingRespectsHeap.
        T₃CompatWithRestOfEnvTypes : All (λ T' → T₃ ⟷ T') R
        T₃CompatWithRestOfEnvTypes = t₁CompatibilityImpliest₃Compatibility T₁CompatWithRestOfEnvTypes spl

        externalCompat : (T' : Type) →  All (λ T'' → T' ⟷ T'') (T ∷ R) → All (λ T'' → T' ⟷ T'') Ts'
        externalCompat T' (_∷_ {x = x} {xs = xs} px T'CompatWithTs) =
          let
            T'CompatT₁ = Eq.subst (λ a →  T' ⟷ a) TEqT₁ px
            T'CompatT₃ = proj₂ (splittingRespectsHeap spl T'CompatT₁)
          in
            T'CompatT₃ ∷ T'CompatWithTs

  ... | no l₁Neql  with T ≟t T₁
  ... | yes TEqT₁ =
        ⟨ Ts' , ⟨ envTypesTs' , ⟨ consTypeList TCompatWithR' (proj₁ (proj₂ (proj₂ R'WithProof))) , externCompatibility' ⟩ ⟩ ⟩
      where
       -- Because we're in envTypeConcatMatchFound, l₁ ⦂ o was at the end of the context, and we found l₁ ⦂ T₄ in Δ , l ⦂ T₁.
        -- But l ≢ l₁, so we will be able to find l₁ ⦂ T₄ in Δ and use the same rule.
        -- However, there may be l's in ρ, which may result in a different R than before! Some T₁'s may be replaced with T₃'s.
        R'WithProof = envTypesForSplitOMismatch origEnvTypes restConnected spl
        R' = proj₁ R'WithProof
        Ts' = T ∷ R'

        l₁InΔ : ((StaticEnv.locEnv Δ) , l ⦂ T₃) ∋ l₁ ⦂ T
        l₁InΔ = irrelevantExtensionsOK {t = T} {t' = T₃} (irrelevantReductionsOK lookupResult l₁Neql) l₁Neql

        envTypesTs' = envTypesConcatMatchFound (Δ ,ₗ l ⦂ T₃) o' (proj₁ (proj₂ R'WithProof)) l₁InΔ l₁NotForbidden

        externCompatibility = proj₂ (proj₂ (proj₂ R'WithProof))
        TCompatWithR' : All (λ T' → T ⟷ T') R'
        TCompatWithR' = externCompatibility T firstConnected

        externCompatibility' : (T' : Type) →  All (λ T'' → T' ⟷ T'') (T ∷ R) → All (λ T'' → T' ⟷ T'') Ts'
        externCompatibility' T' (_∷_ {x = x} {xs = xs} px T'CompatWithTs) =
          px ∷ externCompatibility T' T'CompatWithTs

  ... | no TNeqT₁ =
        ⟨ Ts' , ⟨ envTypesTs' ,  ⟨ consTypeList T₄CompatWithR' (proj₁ (proj₂ (proj₂ R'WithProof))) , externCompatibility' ⟩ ⟩ ⟩
      where
        -- Because we're in envTypeConcatMatchFound, l₁ ⦂ o was at the end of the context, and we found l₁ ⦂ T₄ in Δ , l ⦂ T₁.
        -- But l ≢ l₁, so we will be able to find l₁ ⦂ T₄ in Δ and use the same rule.
        -- However, there may be l's in ρ, which may result in a different R than before! Some T₁'s may be replaced with T₃'s.
        R'WithProof = envTypesForSplitOMismatch origEnvTypes restConnected spl

        R' = proj₁ R'WithProof
        Ts' = T ∷ R'

        l₁InΔ : ((StaticEnv.locEnv Δ) , l ⦂ T₃) ∋ l₁ ⦂ T
        l₁InΔ = irrelevantExtensionsOK {t = T} {t' = T₃} (irrelevantReductionsOK lookupResult l₁Neql) l₁Neql

        envTypesTs' = envTypesConcatMatchFound (Δ ,ₗ l ⦂ T₃) o' (proj₁ (proj₂ R'WithProof)) l₁InΔ l₁NotForbidden

        externCompatibility = proj₂ (proj₂ (proj₂ R'WithProof))
        T₄CompatWithR' : All (λ T' → T ⟷ T') R'
        T₄CompatWithR' = externCompatibility T firstConnected

        externCompatibility' : (T' : Type) →  All (λ T'' → T' ⟷ T'') (T ∷ R) → All (λ T'' → T' ⟷ T'') Ts'
        externCompatibility' T' (_∷_ {x = x} {xs = xs} px T'CompatWithTs) =
          px ∷ externCompatibility T' T'CompatWithTs

  envTypesForSplitOMismatch {Γ} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o') φ ψ)} {Δ} {l} {.o'} {T₁} {T₂} {T₃} {Ts} {forbiddenRefs}
    (envTypesConcatMatchNotFound {R = .Ts} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} .(Δ ,ₗ l ⦂ T₁) o' origEnvTypes l₁NotInΔ')
    origCompat
    spl =
      let
        compatibilityWithOrigρ = envTypesForSplitOMismatch origEnvTypes origCompat spl
        envTypes = envTypesConcatMatchNotFound (Δ ,ₗ l ⦂ T₃) o' (proj₁ (proj₂ compatibilityWithOrigρ)) (∉domPreservation l₁NotInΔ' )
      in
        ⟨ proj₁ compatibilityWithOrigρ , ⟨ envTypes ,  proj₂ (proj₂ compatibilityWithOrigρ) ⟩ ⟩

  envTypesForSplitOMismatch {Γ} {.(re μ (ρ IndirectRefContext., l₁ ⦂ objVal o') φ ψ)} {Δ} {l} {o''} {T₁} {T₂} {T₃} {Ts} {forbiddenRefs}
    (envTypesConcatMismatch {R = .Ts} {l = l₁} {μ = μ} {ρ = ρ} {φ = φ} {ψ = ψ} {forbiddenRefs = .forbiddenRefs} .(Δ ,ₗ l ⦂ T₁) o'' o' o''Neqo' origEnvTypes)
    origCompat
    spl =
      -- We know l : o is in ρ, and we're looking for matches o'', but the last item doesn't match because o' ≢ o''.
         let
           compatibilityWithOrigρ = envTypesForSplitOMismatch origEnvTypes origCompat spl -- o'NeqO origCompat spl
           envTypes = envTypesConcatMismatch (Δ ,ₗ l ⦂ T₃) o'' o' o''Neqo' (proj₁ (proj₂ compatibilityWithOrigρ))
         in
           ⟨ proj₁ compatibilityWithOrigρ , ⟨ envTypes , proj₂ (proj₂ compatibilityWithOrigρ) ⟩ ⟩
  envTypesForSplitOMismatch {Γ} {.(re μ IndirectRefContext.∅ φ ψ)} {Δ} {l} {o} {T₁} {T₂} {T₃} {.[]} {T}
    (envTypesEmpty {μ = μ} {φ = φ} {ψ = ψ} {Δ = .(Δ ,ₗ l ⦂ T₁)} {o = .o})
    origCompat
    spl =
      ⟨ [] , ⟨ envTypesEmpty , ⟨ emptyTypeList refl , (λ T' → λ a → []) ⟩ ⟩ ⟩

  iterateExternalCompat : ∀ {E E'}
                          → {L : List Type}
                          → (∀ T' → All (λ T'' → T' ⟷ T'') E → All (λ T'' → T' ⟷ T'') E')
                          → All (λ T → All (λ T' → T ⟷ T') E) L
                          → All (λ T → All (λ T' → T ⟷ T') E') L
  iterateExternalCompat {L = []} externalCompat allCompat = []
  iterateExternalCompat {L = T ∷ rest} externalCompat (_∷_ {x = .T} {xs = .rest} TCompat restCompat) =
    (externalCompat T TCompat) ∷ (iterateExternalCompat {L = rest} externalCompat restCompat)

  -- Previously, all the types aliasing o were connected. Now, we've extended the context due to a split, and we need to show we still have connectivity.
  -- The idea here is that the expression in question is of type T₂, so the reference left in the heap is of type T₃.
  -- o corresponds to the bject that was affected by the split, whereas o' is the reference we are interested in analyzing aliases to.
  splitReplacementOK : ∀ {Γ Σ Δ o o' l}
                       → {t₁ t₂ : Tc}
                       → {T₁ T₂ T₃ : Type}
                       → (T₁EqctT₁ : T₁ ≡ (contractType t₁))
                       → (T₂EqctT₂ : T₂ ≡ (contractType t₂))
                       → (globalConsistency : (Σ & (Δ ,ₗ l ⦂ T₁) ok))
                       → o ≡ proj₁ (locLookup {T = t₁} globalConsistency (Eq.subst (λ a → StaticEnv.locEnv (Δ ,ₗ l ⦂ T₁) ∋ l ⦂ a) T₁EqctT₁ (TypeEnvContext.Z {StaticEnv.locEnv Δ} {l} {T₁}) ))
                       → (RT : RefTypes Σ (Δ ,ₗ l ⦂ T₁) o')
                       → IsConnected Σ (Δ ,ₗ l ⦂ T₁) o' RT
                       → Γ ⊢ T₁ ⇛ T₂ / T₃
                       → ∃[ RT' ] (IsConnected Σ ((Δ ,ₗ l ⦂ T₃) ,ₒ o ⦂ T₂) o' RT')
  splitReplacementOK {Γ} {Σ} {Δ} {o} {o'} {l} {t₁} {t₂} {T₁} {T₂} {T₃}
    refl
    refl
    origConsis@(ok _ _ _ objLookup refConsistencyFunc)
    refl
    RT
    rConnected@(isConnected _ oTypesListConnected oConnectedToFieldTypes oConnectedToLTypes envFieldConnected@(envTypesConnected _ etc fieldTypesConnected fieldEnvTypesConnected))
    spl
    with (o' ≟ o)
  ... | yes osEq =
    -- In this case, there are no O types yet, but adding o ⦂ T₂ will add one.
      ⟨ RT' , isConnected RT' TsForOsConnected  TsForOsConnectedToFieldTypes TsForOsConnectedToLTypes envAndFieldConnected ⟩
    where
      Δ' = ((Δ ,ₗ l ⦂ T₃) ,ₒ o ⦂ T₂)

      TsForOs = [ T₂ ] -- Since o ≡ o', when we look up o' in the new context, we'll get T₂.

      o'TypeExtension : [ T₂ ] ≡  ctxTypes (StaticEnv.objEnv Δ Context., o' ⦂ T₂) o'
      o'TypeExtension = ctxTypesExtension {StaticEnv.objEnv (Δ ,ₗ l ⦂ T₃)} {o'} {T₂}

      RT'o'TypesEq : [ T₂ ] ≡ ctxTypes (StaticEnv.objEnv Δ') o'
      RT'o'TypesEq =  Eq.subst (λ a → ([ T₂ ] ≡ (ctxTypes (StaticEnv.objEnv Δ , a ⦂ T₂) o'))) (osEq) o'TypeExtension

      lLookupResult = objLookup l t₁ Z
      oForL = proj₁ lLookupResult
      lInρ = proj₁ (proj₂ lLookupResult)

      -- Can I show that T₂ is compatible with all of the old env types? Because that's really what I need.
      lInρForFindLocation = (Eq.subst (λ a → RuntimeEnv.ρ Σ IndirectRefContext.∋ l ⦂ objVal a) (Eq.sym osEq) lInρ)
      TInEnvTypes = findLocationInEnvTypes (RefTypes.envTypesList RT) (RefTypes.envTypes RT) etc lInρForFindLocation
      newEnvTypes = envTypesForSplit (RefTypes.envTypes RT) lInρForFindLocation (proj₂ TInEnvTypes) etc spl

      RT' : RefTypes Σ Δ' o'
      RT' = record {oTypesList = TsForOs ;
                   oTypes = Eq.sym (RT'o'TypesEq) ;
                   envTypesList = proj₁ newEnvTypes ;
                   envTypes = oExtensionIrrelevantToEnvTypes (proj₁ (proj₂ newEnvTypes)) ;
                   fieldTypesList = RefTypes.fieldTypesList RT} -- field types are unchanged.

      TsForOsIsRight : TsForOs ≡ (RefTypes.oTypesList RT')
      TsForOsIsRight =  Eq.trans RT'o'TypesEq (RefTypes.oTypes RT')

      TsForOsConnected : IsConnectedTypeList (RefTypes.oTypesList RT')
      TsForOsConnected = (Eq.subst (λ a → IsConnectedTypeList a) TsForOsIsRight (singleElementListsAreConnected T₂))

      -- Need to find the proof that T₁ is compatible with all the field types and use it directly. It has to be in there somewhere.
      -- Specifically, it has to be in envFieldConnected because T₁ has to have been in the old env types.

      oldEnvFieldsCompatible : All (λ T → All (_⟷_ T) (RefTypes.fieldTypesList RT)) (RefTypes.envTypesList RT)
      oldEnvFieldsCompatible = envFieldInversion3 envFieldConnected
      -- One of the items in oldEnvFieldsCompatible is proof that T₁ is connected to everything in fieldTypesList! But which one?

      T₁CompatWithAllFieldTypes : All (λ T' → T₁ ⟷ T') (RefTypes.fieldTypesList RT)
      T₁CompatWithAllFieldTypes =
        prevCompatibilityImpliesCompatibility RT (RefTypes.fieldTypesList RT) oldEnvFieldsCompatible etc (Eq.subst (λ a → RuntimeEnv.ρ Σ IndirectRefContext.∋ l ⦂ objVal a) (Eq.sym osEq) lInρ)

      T₂CompatWithAllFieldTypes = t₁CompatibilityImpliest₂Compatibility T₁CompatWithAllFieldTypes spl

      TsForOsConnectedToFieldTypes :  All (λ T → All (λ T' → T ⟷ T') (RefTypes.fieldTypesList RT')) (RefTypes.oTypesList RT')
      TsForOsConnectedToFieldTypes = T₂CompatWithAllFieldTypes ∷ []

      T₂ConnectedToLTypes :  All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) [ T₂ ]
      T₂ConnectedToLTypes =  proj₁ (proj₂ (proj₂ newEnvTypes)) ∷ []

      TsForOsConnectedToLTypes :  All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) (RefTypes.oTypesList RT')
      TsForOsConnectedToLTypes =  Eq.subst (λ a →  All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) a) TsForOsIsRight T₂ConnectedToLTypes

      externalCompat : ∀ T' → All (λ T'' → T' ⟷ T'') (RefTypes.envTypesList RT) → All (λ T'' → T' ⟷ T'') (RefTypes.envTypesList RT')
      externalCompat =  proj₂ (proj₂ (proj₂ (proj₂ newEnvTypes)))

      insideOutEnvTypesFieldTypesCompat : All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT)) (RefTypes.fieldTypesList RT)
      insideOutEnvTypesFieldTypesCompat = allInsideOut splitSymmetric fieldEnvTypesConnected -- turn prev. inside out

      newEnvTypesCompatWithFieldTypes :  All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) (RefTypes.fieldTypesList RT)
      newEnvTypesCompatWithFieldTypes = iterateExternalCompat {L = RefTypes.fieldTypesList RT} externalCompat insideOutEnvTypesFieldTypesCompat

      newEnvTypesCompatWithNewFieldTypes : All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) (RefTypes.fieldTypesList RT')
      newEnvTypesCompatWithNewFieldTypes = newEnvTypesCompatWithFieldTypes -- b/c old field types ≡ new field types

      envTypesCompatibleWithFieldTypes : All (λ T → All (λ T' → T ⟷ T') (RefTypes.fieldTypesList RT')) (RefTypes.envTypesList RT')
      envTypesCompatibleWithFieldTypes =  allInsideOut splitSymmetric newEnvTypesCompatWithNewFieldTypes  -- turn prev. inside out

      envAndFieldConnected : IsConnectedEnvAndField Σ ((Δ ,ₗ l ⦂ T₃) ,ₒ o ⦂ T₂) o' RT'
      envAndFieldConnected = envTypesConnected RT' ( proj₁ (proj₂ (proj₂ (proj₂ newEnvTypes)))) fieldTypesConnected envTypesCompatibleWithFieldTypes

  ... | no osNeq =
        --  The change in Δ has no impact on looking up o', since o' ≢ o.
        let
          lLookupResult = objLookup l t₁ Z
          oForL = proj₁ lLookupResult
          lInρ = proj₁ (proj₂ lLookupResult)
          Δ' = ((Δ ,ₗ l ⦂ T₃) ,ₒ o ⦂ T₂)

          oTypesUnchanged : ctxTypes (StaticEnv.objEnv Δ') o' ≡ ctxTypes (StaticEnv.objEnv (Δ ,ₗ l ⦂ T₃)) o'
          oTypesUnchanged = ctxTypesExtensionNeq osNeq

          newEnvTypes = envTypesForSplitOMismatch (RefTypes.envTypes RT) etc spl
          RT' = record { oTypesList = RefTypes.oTypesList RT ;
                         oTypes = Eq.trans oTypesUnchanged (RefTypes.oTypes RT) ;
                         envTypesList = proj₁ newEnvTypes ;
                         envTypes = oExtensionIrrelevantToEnvTypes (proj₁ (proj₂ newEnvTypes)) ;
                         fieldTypesList = RefTypes.fieldTypesList RT
                       }

          externalCompat = proj₂ (proj₂ (proj₂ newEnvTypes))
          TsForOsConnectedToLTypes = iterateExternalCompat externalCompat oConnectedToLTypes

          insideOutEnvTypesFieldTypesCompat : All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT)) (RefTypes.fieldTypesList RT)
          insideOutEnvTypesFieldTypesCompat = allInsideOut splitSymmetric fieldEnvTypesConnected -- turn prev. inside out

          newEnvTypesCompatWithFieldTypes :  All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) (RefTypes.fieldTypesList RT)
          newEnvTypesCompatWithFieldTypes = iterateExternalCompat {L = RefTypes.fieldTypesList RT} externalCompat insideOutEnvTypesFieldTypesCompat

          newEnvTypesCompatWithNewFieldTypes : All (λ T → All (λ T' → T ⟷ T') (RefTypes.envTypesList RT')) (RefTypes.fieldTypesList RT')
          newEnvTypesCompatWithNewFieldTypes = newEnvTypesCompatWithFieldTypes -- b/c old field types ≡ new field types

          envTypesCompatibleWithFieldTypes : All (λ T → All (λ T' → T ⟷ T') (RefTypes.fieldTypesList RT')) (RefTypes.envTypesList RT')
          envTypesCompatibleWithFieldTypes =  allInsideOut splitSymmetric newEnvTypesCompatWithNewFieldTypes  -- turn prev. inside out

          envAndFieldConnected =  envTypesConnected RT' ( proj₁ (proj₂ (proj₂ newEnvTypes))) fieldTypesConnected envTypesCompatibleWithFieldTypes
        in
            ⟨ RT' , isConnected RT' oTypesListConnected  oConnectedToFieldTypes TsForOsConnectedToLTypes envAndFieldConnected ⟩

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Nat
open import Agda.Builtin.Size
open import Agda.Builtin.Unit

mutual

  data Delay (A : Set) (i : Size) : Set where
    now   : A → Delay A i
    later : Delay′ A i → Delay A i

  record Delay′ (A : Set) (i : Size) : Set where
    coinductive
    field
      force : {j : Size< i} → Delay A j

open Delay′ public

delay : ∀ {A i} → Nat → A → Delay A i
delay zero    x = now x
delay (suc n) x = later λ { .force → delay n x }

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}

run : ∀ {A} → Nat → Delay A ∞ → Maybe A
run zero    _         = nothing
run (suc n) (now x)   = just x
run (suc n) (later x) = run n (force x)

postulate
  wrapper : Maybe Nat → IO ⊤

{-# COMPILE GHC wrapper = print #-}

main : IO ⊤
main = wrapper (run 10 (delay 5 12))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda