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

open import Examples.Sorting.Parallel.Comparable

module Examples.Sorting.Parallel.MergeSortPar (M : Comparable) where

open Comparable M
open import Examples.Sorting.Parallel.Core M

open import Calf costMonoid
open import Calf.ParMetalanguage parCostMonoid
open import Calf.Types.Nat
open import Calf.Types.List
open import Calf.Types.Bounded costMonoid
open import Calf.Types.BigO costMonoid

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s; _+_; _*_; _^_; ⌊_/2⌋; ⌈_/2⌉; _⊔_)
open import Data.Nat.Properties as N using (module ≤-Reasoning)
open import Data.Nat.Log2
open import Data.Nat.Square
open import Data.Nat.PredExp2

open import Examples.Sorting.Parallel.MergeSort.Split M public
open import Examples.Sorting.Parallel.MergeSortPar.Merge M public

sort/clocked : cmp (Π nat λ _ → Π (list A) λ _ → F (list A))
sort/clocked zero    l = ret l
sort/clocked (suc k) l =
  bind (F (list A)) (split l) λ (l₁ , l₂) →
    bind (F (list A)) (sort/clocked k l₁ & sort/clocked k l₂) merge

sort/clocked/correct : ∀ k l → ⌈log₂ length l ⌉ Nat.≤ k → SortResult (sort/clocked k) l
sort/clocked/correct zero    l h u = l , refl , refl , short-sorted (⌈log₂n⌉≡0⇒n≤1 (N.n≤0⇒n≡0 h))
sort/clocked/correct (suc k) l h u =
  let (l₁ , l₂ , ≡ , length₁ , length₂ , ↭) = split/correct l u in
  let (l₁' , ≡₁ , ↭₁ , sorted₁) = sort/clocked/correct k l₁ (
                                    let open ≤-Reasoning in
                                    begin
                                      ⌈log₂ length l₁ ⌉
                                    ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩
                                      ⌈log₂ ⌊ length l /2⌋ ⌉
                                    ≤⟨ log₂-mono (N.⌊n/2⌋≤⌈n/2⌉ (length l)) ⟩
                                      ⌈log₂ ⌈ length l /2⌉ ⌉
                                    ≤⟨ log₂-suc (length l) h ⟩
                                      k
                                    ∎
                                  ) u in
  let (l₂' , ≡₂ , ↭₂ , sorted₂) = sort/clocked/correct k l₂ (
                                    let open ≤-Reasoning in
                                    begin
                                      ⌈log₂ length l₂ ⌉
                                    ≡⟨ Eq.cong ⌈log₂_⌉ length₂ ⟩
                                      ⌈log₂ ⌈ length l /2⌉ ⌉
                                    ≤⟨ log₂-suc (length l) h ⟩
                                      k
                                    ∎
                                  ) u in
  let (l' , ≡' , h-sorted) = merge/correct l₁' l₂' u
      (↭' , sorted) = h-sorted sorted₁ sorted₂
  in
  l' , (
    let open ≡-Reasoning in
    begin
      sort/clocked (suc k) l
    ≡⟨⟩
      (bind (F (list A)) (split l) λ (l₁ , l₂) →
        bind (F (list A)) (sort/clocked k l₁ & sort/clocked k l₂) merge)
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) ≡ ⟩
      bind (F (list A)) (sort/clocked k l₁ & sort/clocked k l₂) merge
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e merge) (Eq.cong₂ _&_ ≡₁ ≡₂) ⟩
      merge (l₁' , l₂')
    ≡⟨ ≡' ⟩
      ret l'
    ∎
  ) , (
    let open PermutationReasoning in
    begin
      l
    ↭⟨ ↭ ⟩
      l₁ ++ l₂
    ↭⟨ ++⁺-↭ ↭₁ ↭₂ ⟩
      l₁' ++ l₂'
    ↭⟨ ↭' ⟩
      l'
    ∎
  ) , sorted

sort/clocked/cost : cmp (Π nat λ _ → Π (list A) λ _ → cost)
sort/clocked/cost zero    l = 𝟘
sort/clocked/cost (suc k) l =
  bind cost (split l) λ (l₁ , l₂) → split/cost l ⊕
    bind cost (sort/clocked k l₁ & sort/clocked k l₂) λ (l₁' , l₂') → (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕
      merge/cost/closed (l₁' , l₂')

sort/clocked/cost/closed : cmp (Π nat λ _ → Π (list A) λ _ → cost)
sort/clocked/cost/closed k l = k * length l * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , k * ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²

sort/clocked/cost≤sort/clocked/cost/closed : ∀ k l → ⌈log₂ length l ⌉ Nat.≤ k → ◯ (sort/clocked/cost k l ≤ₚ sort/clocked/cost/closed k l)
sort/clocked/cost≤sort/clocked/cost/closed zero    l h u = z≤n , z≤n
sort/clocked/cost≤sort/clocked/cost/closed (suc k) l h u =
  let (l₁ , l₂ , ≡ , length₁ , length₂ , ↭) = split/correct l u in
  let h₁ : ⌈log₂ length l₁ ⌉ Nat.≤ k
      h₁ =
        let open ≤-Reasoning in
        begin
          ⌈log₂ length l₁ ⌉
        ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩
          ⌈log₂ ⌊ length l /2⌋ ⌉
        ≤⟨ log₂-mono (N.⌊n/2⌋≤⌈n/2⌉ (length l)) ⟩
          ⌈log₂ ⌈ length l /2⌉ ⌉
        ≤⟨ log₂-suc (length l) h ⟩
          k
        ∎

      h₂ : ⌈log₂ length l₂ ⌉ Nat.≤ k
      h₂ =
        let open ≤-Reasoning in
        begin
          ⌈log₂ length l₂ ⌉
        ≡⟨ Eq.cong ⌈log₂_⌉ length₂ ⟩
          ⌈log₂ ⌈ length l /2⌉ ⌉
        ≤⟨ log₂-suc (length l) h ⟩
          k
        ∎
  in
  let (l₁' , ≡₁ , ↭₁ , sorted₁) = sort/clocked/correct k l₁ h₁ u in
  let (l₂' , ≡₂ , ↭₂ , sorted₂) = sort/clocked/correct k l₂ h₂ u in
  let open ≤ₚ-Reasoning in
  begin
    sort/clocked/cost (suc k) l
  ≡⟨⟩
    (bind cost (split l) λ (l₁ , l₂) → split/cost l ⊕
      bind cost (sort/clocked k l₁ & sort/clocked k l₂) λ (l₁' , l₂') → (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕
        merge/cost/closed (l₁' , l₂'))
  ≡⟨ Eq.cong (λ e → bind cost e _) (≡) ⟩
    (split/cost l ⊕
      bind cost (sort/clocked k l₁ & sort/clocked k l₂) λ (l₁' , l₂') → (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕
        merge/cost/closed (l₁' , l₂'))
  ≡⟨⟩
    (𝟘 ⊕
      bind cost (sort/clocked k l₁ & sort/clocked k l₂) λ (l₁' , l₂') → (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕
        merge/cost/closed (l₁' , l₂'))
  ≡⟨ ⊕-identityˡ _ ⟩
    (bind cost (sort/clocked k l₁ & sort/clocked k l₂) λ (l₁' , l₂') → (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕
      merge/cost/closed (l₁' , l₂'))
  ≡⟨
    Eq.cong (λ e → bind cost e λ (l₁' , l₂') → (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕ merge/cost/closed (l₁' , l₂')) (
      Eq.cong₂ _&_
        ≡₁
        ≡₂
    )
  ⟩
    (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) ⊕ merge/cost/closed (l₁' , l₂')
  ≤⟨
    ⊕-monoˡ-≤ (merge/cost/closed (l₁' , l₂')) (
      ⊗-mono-≤
        (sort/clocked/cost≤sort/clocked/cost/closed k l₁ h₁ u)
        (sort/clocked/cost≤sort/clocked/cost/closed k l₂ h₂ u)
    )
  ⟩
    (sort/clocked/cost/closed k l₁ ⊗ sort/clocked/cost/closed k l₂) ⊕ merge/cost/closed (l₁' , l₂')
  ≡⟨⟩
    (sort/clocked/cost/closed k l₁ ⊗ sort/clocked/cost/closed k l₂) ⊕
      (pred[2^ ⌈log₂ suc (length l₁') ⌉ ] * ⌈log₂ suc (length l₂') ⌉ , ⌈log₂ suc (length l₁') ⌉ * ⌈log₂ suc (length l₂') ⌉)
  ≡˘⟨
    Eq.cong ((sort/clocked/cost/closed k l₁ ⊗ sort/clocked/cost/closed k l₂) ⊕_) (
      Eq.cong₂ (λ n₁ n₂ →  pred[2^ ⌈log₂ suc n₁ ⌉ ] * ⌈log₂ suc n₂ ⌉ , ⌈log₂ suc n₁ ⌉ * ⌈log₂ suc n₂ ⌉)
        (↭-length ↭₁)
        (↭-length ↭₂)
    )
  ⟩
    (sort/clocked/cost/closed k l₁ ⊗ sort/clocked/cost/closed k l₂) ⊕
      (pred[2^ ⌈log₂ suc (length l₁) ⌉ ] * ⌈log₂ suc (length l₂) ⌉ , ⌈log₂ suc (length l₁) ⌉ * ⌈log₂ suc (length l₂) ⌉)
  ≡⟨⟩
    ((k * length l₁ * ⌈log₂ suc ⌈ length l₁ /2⌉ ⌉ , k * ⌈log₂ suc ⌈ length l₁ /2⌉ ⌉ ²) ⊗
      (k * length l₂ * ⌈log₂ suc ⌈ length l₂ /2⌉ ⌉ , k * ⌈log₂ suc ⌈ length l₂ /2⌉ ⌉ ²)) ⊕
      (pred[2^ ⌈log₂ suc (length l₁) ⌉ ] * ⌈log₂ suc (length l₂) ⌉ , ⌈log₂ suc (length l₁) ⌉ * ⌈log₂ suc (length l₂) ⌉)
  ≡⟨
    Eq.cong₂ (
      λ n₁ n₂ →
        ((k * n₁ * ⌈log₂ suc ⌈ n₁ /2⌉ ⌉ , k * ⌈log₂ suc ⌈ n₁ /2⌉ ⌉ ²) ⊗
          (k * n₂ * ⌈log₂ suc ⌈ n₂ /2⌉ ⌉ , k * ⌈log₂ suc ⌈ n₂ /2⌉ ⌉ ²)) ⊕
          (pred[2^ ⌈log₂ suc (n₁) ⌉ ] * ⌈log₂ suc (n₂) ⌉ , ⌈log₂ suc (n₁) ⌉ * ⌈log₂ suc (n₂) ⌉)
    )
      length₁
      length₂
  ⟩
    ((k * ⌊ length l /2⌋ * ⌈log₂ suc ⌈ ⌊ length l /2⌋ /2⌉ ⌉ , k * ⌈log₂ suc ⌈ ⌊ length l /2⌋ /2⌉ ⌉ ²) ⊗
      (k * ⌈ length l /2⌉ * ⌈log₂ suc ⌈ ⌈ length l /2⌉ /2⌉ ⌉ , k * ⌈log₂ suc ⌈ ⌈ length l /2⌉ /2⌉ ⌉ ²)) ⊕
      (pred[2^ ⌈log₂ suc ⌊ length l /2⌋ ⌉ ] * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , ⌈log₂ suc ⌊ length l /2⌋ ⌉ * ⌈log₂ suc ⌈ length l /2⌉ ⌉)
  ≤⟨
    ⊕-mono-≤
      (
        let h-⌊n/2⌋ = log₂-mono (s≤s (N.⌈n/2⌉-mono (N.⌊n/2⌋≤n (length l))))
            h-⌈n/2⌉ = log₂-mono (s≤s (N.⌈n/2⌉-mono (N.⌈n/2⌉≤n (length l)))) in
        ⊗-mono-≤
          (N.*-monoʳ-≤ (k * ⌊ length l /2⌋) h-⌊n/2⌋ , N.*-monoʳ-≤ k (²-mono h-⌊n/2⌋))
          (N.*-monoʳ-≤ (k * ⌈ length l /2⌉) h-⌈n/2⌉ , N.*-monoʳ-≤ k (²-mono h-⌈n/2⌉))
      )
      (
        let h = log₂-mono (s≤s (N.⌊n/2⌋≤⌈n/2⌉ (length l))) in
        N.*-monoˡ-≤ ⌈log₂ suc ⌈ length l /2⌉ ⌉ (pred[2^]-mono h) ,
        N.*-monoˡ-≤ ⌈log₂ suc ⌈ length l /2⌉ ⌉ h
      )
  ⟩
    ((k * ⌊ length l /2⌋ * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , k * ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²) ⊗
      (k * ⌈ length l /2⌉ * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , k * ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²)) ⊕
      (pred[2^ ⌈log₂ suc ⌈ length l /2⌉ ⌉ ] * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²)
  ≤⟨
    arithmetic/work (length l) ,
    (N.≤-reflexive (arithmetic/span (⌈log₂ suc ⌈ length l /2⌉ ⌉ ²)))
  ⟩
    suc k * length l * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , suc k * ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²
  ≡⟨⟩
    sort/clocked/cost/closed (suc k) l
  ∎
    where
      arithmetic/work : (n : ℕ) →
        (k * ⌊ n /2⌋ * ⌈log₂ suc ⌈ n /2⌉ ⌉ + k * ⌈ n /2⌉ * ⌈log₂ suc ⌈ n /2⌉ ⌉)
          + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉
        Nat.≤ suc k * n * ⌈log₂ suc ⌈ n /2⌉ ⌉
      arithmetic/work n =
        begin
          (k * ⌊ n /2⌋ * ⌈log₂ suc ⌈ n /2⌉ ⌉ + k * ⌈ n /2⌉ * ⌈log₂ suc ⌈ n /2⌉ ⌉)
            + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ≡⟨
          Eq.cong
            (_+ pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉)
            (Eq.cong₂ _+_
              (N.*-assoc k ⌊ n /2⌋ ⌈log₂ suc ⌈ n /2⌉ ⌉)
              (N.*-assoc k ⌈ n /2⌉ ⌈log₂ suc ⌈ n /2⌉ ⌉))
        ⟩
          (k * (⌊ n /2⌋ * ⌈log₂ suc ⌈ n /2⌉ ⌉) + k * (⌈ n /2⌉ * ⌈log₂ suc ⌈ n /2⌉ ⌉))
            + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ≡˘⟨
          Eq.cong (_+ pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉) (
            N.*-distribˡ-+ k (⌊ n /2⌋ * ⌈log₂ suc ⌈ n /2⌉ ⌉) (⌈ n /2⌉ * ⌈log₂ suc ⌈ n /2⌉ ⌉)
          )
        ⟩
          k * (⌊ n /2⌋ * ⌈log₂ suc ⌈ n /2⌉ ⌉ + ⌈ n /2⌉ * ⌈log₂ suc ⌈ n /2⌉ ⌉)
            + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ≡˘⟨
          Eq.cong
            (λ m → k * m + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉)
            (N.*-distribʳ-+ ⌈log₂ suc ⌈ n /2⌉ ⌉ ⌊ n /2⌋ ⌈ n /2⌉)
        ⟩
          k * ((⌊ n /2⌋ + ⌈ n /2⌉) * ⌈log₂ suc ⌈ n /2⌉ ⌉) + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ≡⟨
          Eq.cong
            (λ m → k * (m * ⌈log₂ suc ⌈ n /2⌉ ⌉) + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉)
            (N.⌊n/2⌋+⌈n/2⌉≡n n)
        ⟩
          k * (n * ⌈log₂ suc ⌈ n /2⌉ ⌉) + pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ≤⟨ N.+-monoʳ-≤ (k * (n * ⌈log₂ suc ⌈ n /2⌉ ⌉)) (N.*-monoˡ-≤ ⌈log₂ suc ⌈ n /2⌉ ⌉ (pred[2^log₂] n)) ⟩
          k * (n * ⌈log₂ suc ⌈ n /2⌉ ⌉) + n * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ≡⟨ N.+-comm (k * (n * ⌈log₂ suc ⌈ n /2⌉ ⌉)) (n * ⌈log₂ suc ⌈ n /2⌉ ⌉) ⟩
          n * ⌈log₂ suc ⌈ n /2⌉ ⌉ + k * (n * ⌈log₂ suc ⌈ n /2⌉ ⌉)
        ≡⟨⟩
          suc k * (n * ⌈log₂ suc ⌈ n /2⌉ ⌉)
        ≡˘⟨ N.*-assoc (suc k) n ⌈log₂ suc ⌈ n /2⌉ ⌉ ⟩
          suc k * n * ⌈log₂ suc ⌈ n /2⌉ ⌉
        ∎
          where open ≤-Reasoning

      arithmetic/span : (n : ℕ) → ((k * n) ⊔ (k * n)) + n ≡ suc k * n
      arithmetic/span n =
        begin
          ((k * n) ⊔ (k * n)) + n
        ≡⟨ Eq.cong (_+ n) (N.⊔-idem (k * n)) ⟩
          k * n + n
        ≡⟨ N.+-comm (k * n) n ⟩
          n + k * n
        ≡⟨⟩
          suc k * n
        ∎
          where open ≡-Reasoning

sort/clocked≤sort/clocked/cost : ∀ k l → IsBounded (list A) (sort/clocked k l) (sort/clocked/cost k l)
sort/clocked≤sort/clocked/cost zero    l = bound/ret
sort/clocked≤sort/clocked/cost (suc k) l =
  bound/bind (split/cost l) _ (split≤split/cost l) λ (l₁ , l₂) →
    bound/bind (sort/clocked/cost k l₁ ⊗ sort/clocked/cost k l₂) _ (bound/par (sort/clocked≤sort/clocked/cost k l₁) (sort/clocked≤sort/clocked/cost k l₂)) λ (l₁' , l₂') →
      merge≤merge/cost/closed l₁' l₂'

sort/clocked≤sort/clocked/cost/closed : ∀ k l → ⌈log₂ length l ⌉ Nat.≤ k → IsBounded (list A) (sort/clocked k l) (sort/clocked/cost/closed k l)
sort/clocked≤sort/clocked/cost/closed k l h = bound/relax (sort/clocked/cost≤sort/clocked/cost/closed k l h) (sort/clocked≤sort/clocked/cost k l)

sort/depth : cmp (Π (list A) λ _ → meta ℕ)
sort/depth l = ⌈log₂ length l ⌉

sort : cmp (Π (list A) λ _ → F (list A))
sort l = sort/clocked (sort/depth l) l

sort/correct : IsSort sort
sort/correct l = sort/clocked/correct (sort/depth l) l N.≤-refl

sort/cost : cmp (Π (list A) λ _ → cost)
sort/cost l = sort/clocked/cost (sort/depth l) l

sort/cost/closed : cmp (Π (list A) λ _ → cost)
sort/cost/closed l = sort/clocked/cost/closed (sort/depth l) l

sort≤sort/cost : ∀ l → IsBounded (list A) (sort l) (sort/cost l)
sort≤sort/cost l = sort/clocked≤sort/clocked/cost (sort/depth l) l

sort≤sort/cost/closed : ∀ l → IsBounded (list A) (sort l) (sort/cost/closed l)
sort≤sort/cost/closed l = sort/clocked≤sort/clocked/cost/closed (sort/depth l) l N.≤-refl

sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n * ⌈log₂ n ⌉ ² , ⌈log₂ n ⌉ ^ 3)
sort/asymptotic = 2 ≤n⇒f[n]≤g[n]via λ l h →
  bound/relax
    (λ u → let open ≤-Reasoning in
      (
        begin
          ⌈log₂ length l ⌉ * length l * ⌈log₂ suc ⌈ length l /2⌉ ⌉
        ≤⟨ N.*-monoʳ-≤ (⌈log₂ length l ⌉ * length l) (lemma (length l) h) ⟩
          ⌈log₂ length l ⌉ * length l * ⌈log₂ length l ⌉
        ≡⟨ N.*-assoc ⌈log₂ length l ⌉ (length l) ⌈log₂ length l ⌉ ⟩
          ⌈log₂ length l ⌉ * (length l * ⌈log₂ length l ⌉)
        ≡⟨ N.*-comm ⌈log₂ length l ⌉ (length l * ⌈log₂ length l ⌉) ⟩
          length l * ⌈log₂ length l ⌉ * ⌈log₂ length l ⌉
        ≡⟨ N.*-assoc (length l) ⌈log₂ length l ⌉ ⌈log₂ length l ⌉ ⟩
          length l * ⌈log₂ length l ⌉ ²
        ∎
      ) , (
        begin
          ⌈log₂ length l ⌉ * ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²
        ≤⟨ N.*-monoʳ-≤ ⌈log₂ length l ⌉ (²-mono (lemma (length l) h)) ⟩
          ⌈log₂ length l ⌉ * ⌈log₂ length l ⌉ ²
        ≡⟨⟩
          ⌈log₂ length l ⌉ * (⌈log₂ length l ⌉ * ⌈log₂ length l ⌉)
        ≡˘⟨ Eq.cong (λ n → ⌈log₂ length l ⌉ * (⌈log₂ length l ⌉ * n)) (N.*-identityʳ _) ⟩
          ⌈log₂ length l ⌉ * (⌈log₂ length l ⌉ * (⌈log₂ length l ⌉ * 1))
        ≡⟨⟩
          ⌈log₂ length l ⌉ ^ 3
        ∎
      )
    )
    (sort≤sort/cost/closed l)
  where
    lemma : ∀ n → 2 Nat.≤ n → ⌈log₂ suc ⌈ n /2⌉ ⌉ Nat.≤ ⌈log₂ n ⌉
    lemma (suc (suc n)) (s≤s (s≤s h)) = log₂-mono (s≤s (s≤s (N.⌈n/2⌉≤n n)))

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --without-K #-}
module Model.Exponential where

open import Cats.Category

open import Model.RGraph as RG using (RGraph)
open import Model.Type.Core
open import Model.Product
open import Util.HoTT.HLevel
open import Util.Prelude hiding (_×_ ; id ; _∘_)

open RGraph
open RG._⇒_

private
  variable Δ : RGraph

infixr 9 _↝_

Ap : ⟦Type⟧ Δ → Δ .Obj → RGraph
Ap {Δ} T δ = record
  { ObjHSet = T .ObjHSet δ
  ; eqHProp = eqHProp T (Δ .eq-refl _)
  ; eq-refl = λ x → T .eq-refl x
  }

_↝_ : (T U : ⟦Type⟧ Δ) → ⟦Type⟧ Δ
_↝_ T U = record
  { ObjHSet = λ γ → HLevel⁺ (Ap T γ RG.⇒ Ap U γ) (RG.⇒-IsSet {Ap T γ} {Ap U γ})
  ; eqHProp = λ γ≈γ′ f g
      → ∀∙-HProp λ x
      → ∀∙-HProp λ y
      → T .eqHProp γ≈γ′ x y →-HProp′ U .eqHProp γ≈γ′ (f .RG.fobj x) (g .RG.fobj y)
  ; eq-refl = λ f → f .RG.feq
  }

curry : (T U V : ⟦Type⟧ Δ)
  → T × U ⇒ V → T ⇒ U ↝ V
curry {Δ} T U V f = record
  { fobj = λ {δ} t → record
    { fobj = λ u → f .fobj (t , u)
    ; feq = λ x≈y → f .feq (Δ .eq-refl δ) (T .eq-refl t , x≈y)
    }
  ; feq = λ γ≈γ′ x≈y v≈w → f .feq γ≈γ′ (x≈y , v≈w)
  }

eval : (T U : ⟦Type⟧ Δ)
  → (T ↝ U) × T ⇒ U
eval T U = record
  { fobj = λ { (f , x) → f .RG.fobj x }
  ; feq = λ { γ≈γ′ (f≈g , x≈y) → f≈g x≈y }
  }

eval∘curry : (T U V : ⟦Type⟧ Δ) {f : T × U ⇒ V}
  → eval U V ∘ ⟨_×_⟩ {B = U} (curry T U V f) id ≈ f
eval∘curry T U V = ≈⁺ λ γ x → refl

instance
  hasExponentials : ∀ {Δ} → HasExponentials (⟦Types⟧ Δ)
  hasExponentials .HasExponentials.hasBinaryProducts = hasBinaryProducts
  hasExponentials .HasExponentials._↝′_ T U = record
    { Cᴮ = T ↝ U
    ; eval = eval T U
    ; curry′ = λ {A} f → record
      { arr = curry A T U f
      ; prop = eval∘curry A T U
      ; unique = λ {g} g-prop → ≈⁺ λ γ h → RG.≈→≡ (RG.≈⁺ λ x
          → sym (g-prop .≈⁻ γ (h , x)))
      }
    }

module ⟦Types⟧↝ {Δ} = HasExponentials (hasExponentials {Δ})

↝-resp-≈⟦Type⟧ : ∀ {Δ} (T T′ U U′ : ⟦Type⟧ Δ)
  → T ≈⟦Type⟧ T′
  → U ≈⟦Type⟧ U′
  → T ↝ U ≈⟦Type⟧ T′ ↝ U′
↝-resp-≈⟦Type⟧ {Δ} T T′ U U′ T≈T′ U≈U′
  = ⟦Types⟧↝.↝-resp-≅ {Δ} {T} {T′} {U} {U′} T≈T′ U≈U′

subT-↝ : ∀ {Γ Δ} (f : Γ RG.⇒ Δ)
  → (T U : ⟦Type⟧ Δ)
  → subT f T ↝ subT f U ≈⟦Type⟧ subT f (T ↝ U)
subT-↝ {Γ} {Δ} f T U = record
  { forth = record
    { fobj = λ g → record
      { fobj = g .fobj
      ; feq = λ {x y} x≈y → transportEq U (g .feq (transportEq T x≈y))
      }
    ; feq = λ γ≈γ′ f≈g x≈y → f≈g x≈y
    }
  ; back = record
    { fobj = λ g → record
      { fobj = g .fobj
      ; feq = λ {x y} x≈y → transportEq U (g .feq (transportEq T x≈y))
      }
    ; feq = λ γ≈γ′ f≈g x≈y → f≈g x≈y
    }
  ; back-forth = ≈⁺ λ γ x → RG.≈→≡ (RG.≈⁺ λ y → refl)
  ; forth-back = ≈⁺ λ γ x → RG.≈→≡ (RG.≈⁺ λ y → refl)
  }

ext: agda

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------
-- Simple expressions
------------------------------------------------------------------------

-- Several examples based on Matsuda and Wang's "FliPpr: A Prettier
-- Invertible Printing System".

{-# OPTIONS --guardedness #-}

module Examples.Expression where

open import Algebra
open import Codata.Musical.Notation
open import Data.List
open import Data.List.Properties
open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

private
  module LM {A : Set} = Monoid (++-monoid A)

open import Examples.Identifier
import Grammar.Infinite as Grammar
import Pretty
open import Renderer
open import Utilities

-- Very simple expressions.

module Expression₁ where

  data Expr : Set where
    one : Expr
    sub : Expr → Expr → Expr

  module _ where

    open Grammar

    mutual

      expr : Grammar Expr
      expr = term
           ∣ sub <$> ♯ expr
                  <⊛ whitespace ⋆
                  <⊛ string′ "-"
                  <⊛ whitespace ⋆
                  ⊛  term

      term : Grammar Expr
      term = one <$ string′ "1"
           ∣    string′ "("
             ⊛> whitespace ⋆
             ⊛> ♯ expr
             <⊛ whitespace ⋆
             <⊛ string′ ")"

  open Pretty

  one-doc : Doc term one
  one-doc = left (<$ text)

  mutual

    expr-printer : Pretty-printer expr
    expr-printer one         = left one-doc
    expr-printer (sub e₁ e₂) =
      group (right (<$> expr-printer e₁ <⊛-tt
                    nest 2 line⋆ <⊛ text <⊛ space ⊛
                    nest 2 (term-printer e₂)))

    term-printer : Pretty-printer term
    term-printer one = one-doc
    term-printer e   =
      right (text ⊛> nil-⋆ ⊛> expr-printer e <⊛ nil-⋆ <⊛ text)

  example : Expr
  example = sub (sub one one) (sub one one)

  test₁ : render 80 (expr-printer example) ≡ "1 - 1 - (1 - 1)"
  test₁ = refl

  test₂ : render 11 (expr-printer example) ≡ "1 - 1\n  - (1 - 1)"
  test₂ = refl

  test₃ : render 8 (expr-printer example) ≡ "1 - 1\n  - (1\n    - 1)"
  test₃ = refl

-- Expression₁.expr does not accept final whitespace. The grammar
-- below does.

module Expression₂ where

  open Expression₁ using (Expr; one; sub; example)

  module _ where

    open Grammar

    mutual

      expr : Grammar Expr
      expr = term
           ∣ sub <$> ♯ expr <⊛ symbol′ "-" ⊛ term

      term : Grammar Expr
      term = one <$ symbol′ "1"
           ∣ symbol′ "(" ⊛> ♯ expr <⊛ symbol′ ")"

    private

      -- A manual proof of Trailing-whitespace expr (included for
      -- illustrative purposes; not used below).

      Trailing-whitespace″ : ∀ {A} → Grammar A → Set₁
      Trailing-whitespace″ g =
        ∀ {x s s₁ s₂} →
        x ∈ g · s₁ → s ∈ whitespace ⋆ · s₂ → x ∈ g · s₁ ++ s₂

      tw′-whitespace : Trailing-whitespace′ (whitespace ⋆)
      tw′-whitespace ⋆-[]-sem                                  w = _ , w
      tw′-whitespace (⋆-+-sem (⊛-sem {s₁ = s₁} (<$>-sem p) q)) w
        with tw′-whitespace q w
      ... | _ , r = _ , cast (P.sym $ LM.assoc s₁ _ _)
                             (⋆-+-sem (⊛-sem (<$>-sem p) r))

      tw″-symbol : ∀ {s} → Trailing-whitespace″ (symbol s)
      tw″-symbol (<⊛-sem {s₁ = s₁} p q) w =
        cast (P.sym $ LM.assoc s₁ _ _)
             (<⊛-sem p (proj₂ (tw′-whitespace q w)))

      tw″-term : Trailing-whitespace″ term
      tw″-term (left-sem (<$-sem p)) w =
        left-sem (<$-sem (tw″-symbol p w))
      tw″-term (right-sem (<⊛-sem {s₁ = s₁} p q)) w =
        cast (P.sym $ LM.assoc s₁ _ _)
             (right-sem (<⊛-sem p (tw″-symbol q w)))

      tw″-expr : Trailing-whitespace″ expr
      tw″-expr (left-sem p) w =
        left-sem (tw″-term p w)
      tw″-expr (right-sem (⊛-sem {s₁ = s₁} p q)) w =
        cast (P.sym $ LM.assoc s₁ _ _)
             (right-sem (⊛-sem p (tw″-term q w)))

      tw-expr : Trailing-whitespace expr
      tw-expr (<⊛-sem p w) = tw″-expr p w

  open Pretty

  one-doc : Doc term one
  one-doc = left (<$ symbol)

  mutual

    expr-printer : Pretty-printer expr
    expr-printer one         = left one-doc
    expr-printer (sub e₁ e₂) =
      group (right (<$> final-line 6 (expr-printer e₁) 2 <⊛
                    symbol-space ⊛ nest 2 (term-printer e₂)))

    term-printer : Pretty-printer term
    term-printer one = one-doc
    term-printer e   = right (symbol ⊛> expr-printer e <⊛ symbol)

  test₁ : render 80 (expr-printer example) ≡ "1 - 1 - (1 - 1)"
  test₁ = refl

  test₂ : render 11 (expr-printer example) ≡ "1 - 1\n  - (1 - 1)"
  test₂ = refl

  test₃ : render 8 (expr-printer example) ≡ "1 - 1\n  - (1\n    - 1)"
  test₃ = refl

-- A somewhat larger expression example.

module Expression₃ where

  -- Expressions.

  data Expr : Set where
    one : Expr
    sub : Expr → Expr → Expr
    div : Expr → Expr → Expr
    var : Identifier → Expr

  -- Precedences.

  data Prec : Set where
    ′5 ′6 ′7 : Prec

  module _ where

    open Grammar

    -- One expression grammar for each precedence level.

    expr : Prec → Grammar Expr
    expr ′5 = ♯ expr ′6
            ∣ sub <$> ♯ expr ′5 <⊛ symbol′ "-" ⊛ ♯ expr ′6
    expr ′6 = ♯ expr ′7
            ∣ div <$> ♯ expr ′6 <⊛ symbol′ "/" ⊛ ♯ expr ′7
    expr ′7 = one <$ symbol′ "1"
            ∣ var <$> identifier-w
            ∣ symbol′ "(" ⊛> ♯ expr ′5 <⊛ symbol′ ")"

  open Pretty

  -- Document for one.

  one-doc : Doc (expr ′7) one
  one-doc = left (left (<$ symbol))

  -- Documents for variables.

  var-doc : ∀ x → Doc (expr ′7) (var x)
  var-doc x = left (right (<$> identifier-w-printer x))

  -- Adds parentheses to a document.

  parens : ∀ {e} → Doc (expr ′5) e → Doc (expr ′7) e
  parens d = right (symbol ⊛> d <⊛ symbol)

  -- Adds parentheses only when necessary (when p₁ < p₂).

  parens-if[_<_] : ∀ p₁ p₂ {e} → Doc (expr p₁) e → Doc (expr p₂) e
  parens-if[ ′5 < ′5 ] = id
  parens-if[ ′5 < ′6 ] = left ∘ parens
  parens-if[ ′5 < ′7 ] = parens
  parens-if[ ′6 < ′5 ] = left
  parens-if[ ′6 < ′6 ] = id
  parens-if[ ′6 < ′7 ] = parens ∘ left
  parens-if[ ′7 < ′5 ] = left ∘ left
  parens-if[ ′7 < ′6 ] = left
  parens-if[ ′7 < ′7 ] = id

  mutual

    -- Pretty-printers.

    expr-printer : ∀ p → Pretty-printer (expr p)
    expr-printer p (sub e₁ e₂) = parens-if[ ′5 < p ] (sub-printer e₁ e₂)
    expr-printer p (div e₁ e₂) = parens-if[ ′6 < p ] (div-printer e₁ e₂)
    expr-printer p one         = parens-if[ ′7 < p ] one-doc
    expr-printer p (var x)     = parens-if[ ′7 < p ] (var-doc x)

    sub-printer : ∀ e₁ e₂ → Doc (expr ′5) (sub e₁ e₂)
    sub-printer e₁ e₂ =
      group (right (<$> final-line 10 (expr-printer ′5 e₁) 2 <⊛
                    symbol-space ⊛ nest 2 (expr-printer ′6 e₂)))

    div-printer : ∀ e₁ e₂ → Doc (expr ′6) (div e₁ e₂)
    div-printer e₁ e₂ =
      group (right (<$> final-line 10 (expr-printer ′6 e₁) 2 <⊛
                    symbol-space ⊛ nest 2 (expr-printer ′7 e₂)))

  -- Unit tests.

  example : Expr
  example = sub (div (var (str⁺ "x")) one) (sub one (var (str⁺ "y")))

  test₁ : render 80 (expr-printer ′5 example) ≡ "x / 1 - (1 - y)"
  test₁ = refl

  test₂ : render 11 (expr-printer ′5 example) ≡ "x / 1\n  - (1 - y)"
  test₂ = refl

  test₃ : render 8 (expr-printer ′5 example) ≡ "x / 1\n  - (1\n    - y)"
  test₃ = refl

  test₄ : render 11 (expr-printer ′6 example) ≡ "(x / 1\n  - (1\n    - y))"
  test₄ = refl

  test₅ : render 12 (expr-printer ′6 example) ≡ "(x / 1\n  - (1 - y))"
  test₅ = refl

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Nat using ( ℕ ; zero ; suc )
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import FRP.LTL.RSet.Core using ( RSet ; _[_,_⟩ ; _[_,_] ; ⟦_⟧ )
open import FRP.LTL.RSet.Causal using ( _⊵_ ; identity )
open import FRP.LTL.RSet.Stateless using ( _⇒_ )
open import FRP.LTL.RSet.Globally using ( □ )
open import FRP.LTL.RSet.Product using ( _∧_ ; _&&&_ ; fst ; snd )
open import FRP.LTL.Time using
  ( Time ; _+_ ; _∸_ ; _≤_ ; _<_
  ; ≤-refl ; _≤-trans_ ; <-impl-≤ ; <-impl-≱ ; _<-transˡ_ ; _<-transʳ_
  ; ≡-impl-≤ ; +-unit ; _≮[_]_ ; <-wo )

module FRP.LTL.RSet.Decoupled where

infixr 2 _▹_
infixr 3 _⋙ˡ_ _⋙ʳ_ _⋙ˡʳ_

-- Decoupled function space

_▹_ : RSet → RSet → RSet
(A ▹ B) t = ∀ {u} → (t ≤ u) → (A [ t , u ⟩) → B u

-- Upcast a decoupled function to a causal function

couple : ∀ {A B} → ⟦ (A ▹ B) ⇒ (A ⊵ B) ⟧
couple {A} {B} {s} f {u} s≤u σ = f s≤u σ′ where

  σ′ : A [ s , u ⟩
  σ′ s≤t t<u = σ s≤t (<-impl-≤ t<u)

-- Variants on composition which produce decoupled functions

_beforeˡ_ : ∀ {A s u v} → (A [ s , v ⟩) → (u ≤ v) → (A [ s , u ⟩)
(σ beforeˡ u≤v) s≤t t<u = σ s≤t (t<u <-transˡ u≤v)

_$ˡ_ : ∀ {A B s u} → (A ▹ B) s → (A [ s , u ⟩) → (B [ s , u ])
(f $ˡ σ) s≤t t≤u = f s≤t (σ beforeˡ t≤u)

_⋙ˡ_ : ∀ {A B C} → ⟦ (A ▹ B) ⇒ (B ⊵ C) ⇒ (A ▹ C) ⟧
(f ⋙ˡ g) s≤t σ = g s≤t (f $ˡ σ)

_beforeʳ_ : ∀ {A s u v} → (A [ s , v ⟩) → (u < v) → (A [ s , u ])
(σ beforeʳ u<v) s≤t t≤u = σ s≤t (t≤u <-transʳ u<v)

_$ʳ_ : ∀ {A B s u} → (A ⊵ B) s → (A [ s , u ⟩) → (B [ s , u ⟩)
(f $ʳ σ) s≤t t<u = f s≤t (σ beforeʳ t<u)

_⋙ʳ_ : ∀ {A B C} → ⟦ (A ⊵ B) ⇒ (B ▹ C) ⇒ (A ▹ C) ⟧
(f ⋙ʳ g) s≤t σ = g s≤t (f $ʳ σ)

_⋙ˡʳ_ : ∀ {A B C} → ⟦ (A ▹ B) ⇒ (B ▹ C) ⇒ (A ▹ C) ⟧
(f ⋙ˡʳ g) = (f ⋙ˡ couple g)

-- Fixed points

-- The following type-checks, but fails to pass the termination
-- checker, as the well-ordering on time is not made explicit:
--
-- fix : ∀ {A} → ⟦ (A ▹ A) ⇒ □ A ⟧
-- fix {A} {s} f {u} s≤u = f s≤u (σ u) where
--
--   σ : (u : Time) → A [ s , u ⟩
--   σ u {t} s≤t t<u = f s≤t (σ t)
--
-- To get this to pass the termination checker, we have to
-- be explicit about the induction scheme, which is
-- over < being a well-ordering on an interval.

fix : ∀ {A} → ⟦ (A ▹ A) ⇒ □ A ⟧
fix {A} {s} f {u} s≤u = f s≤u (σ (<-wo s≤u)) where

  σ : ∀ {u} → (∃ λ n → (s ≮[ n ] u)) → A [ s , u ⟩
  σ (zero , ())      s≤t t<u
  σ (suc n , s≮ⁿ⁺¹u) s≤t t<u = f s≤t (σ (n , s≮ⁿ⁺¹u s≤t t<u))

-- Indexed fixed points are derivable from fixed points

ifix : ∀ {A B} → ⟦ ((A ∧ B) ▹ A) ⇒ (B ▹ A) ⟧
ifix {A} {B} {s} f {v} s≤v τ = fix g s≤v ≤-refl where

  A′ : RSet
  A′ t = (t ≤ v) → A t

  g : (A′ ▹ A′) s
  g {u} s≤u σ u≤v = f s≤u ρ where

    ρ : (A ∧ B) [ s , u ⟩
    ρ s≤t t<u = (σ s≤t t<u (<-impl-≤ t<u ≤-trans u≤v) , τ s≤t (t<u <-transˡ u≤v))

-- Loops are derivable from indexed fixed points

loop : ∀ {A B C} → ⟦ ((A ∧ B) ▹ (A ∧ C)) ⇒ (B ▹ C) ⟧
loop f = (couple (ifix (f ⋙ˡ fst)) &&& identity) ⋙ʳ f ⋙ˡ snd

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
-- Correctness conditions for the boolean AND gate

f : Tensor Real [2] -> Tensor Real [1]
f = evaluate _ _

truthy : Real -> Set
truthy x = x >= 0.5

falsey : Real -> Set
falsey x = x <= 0.5

validInput : Tensor Real [2] -> Set
validInput x = All (λ xi -> 0 <= xi ∧ xi <= 1) x

correctOutput : Tensor Real [2] -> Set
correctOutput x =
  let y : Real
      y = f x ! 0
  in (truthy x!0 and falsey x!1 => truthy y) and
     (truthy x!0 and truthy x!1 => truthy y) and
     (falsey x!0 and falsey x!1 => truthy y) and
     (falsey x!0 and truthy x!1 => truthy y)

correct : ∀ x -> validInput x -> correctOutput x
correct = prove _ _

max_stars_repo_name: bobatkey/vehicle

max_issues_repo_name: bobatkey/vehicle

max_forks_repo_name: bobatkey/vehicle


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Sequent where

open import OscarPrelude
open import Formula

infix 15 _╱_
record Sequent : Set
 where
  constructor _╱_
  field
    statement : Formula
    suppositions : List Formula

open Sequent public

instance EqSequent : Eq Sequent
Eq._==_ EqSequent ( φᵗ₁ ╱ φˢs₁ ) ( φᵗ₂ ╱ φˢs₂ ) = decEq₂ (cong statement) (cong suppositions) (φᵗ₁ ≟ φᵗ₂) (φˢs₁ ≟ φˢs₂)

open import HasNegation

instance HasNegationSequent : HasNegation Sequent
HasNegation.~ HasNegationSequent ( φᵗ ╱ φˢs ) = ~ φᵗ ╱ φˢs

open import 𝓐ssertion

instance 𝓐ssertionSequent : 𝓐ssertion Sequent
𝓐ssertionSequent = record {}

open import HasSatisfaction

instance HasSatisfactionSequent : HasSatisfaction Sequent
HasSatisfaction._⊨_ HasSatisfactionSequent I (φᵗ ╱ φˢs) = I ⊨ φˢs → I ⊨ φᵗ

open import HasDecidableValidation

instance HasDecidableValidationSequent : HasDecidableValidation Sequent
HasDecidableValidationSequent = {!!}

open import HasSubstantiveDischarge

instance HasSubstantiveDischargeSequentSequent : HasSubstantiveDischarge Sequent Sequent
HasSubstantiveDischarge._≽_ HasSubstantiveDischargeSequentSequent (+ᵗ ╱ +ᵖs) (-ᵗ ╱ -ᵖs) = {!!} -- +ᵗ ≽ -ᵗ × +ᵖs ≽ -ᵖs -- use "unification into", from John's "Natural Deduction"

open import HasDecidableSubstantiveDischarge

instance HasDecidableSubstantiveDischargeSequentSequent : HasDecidableSubstantiveDischarge Sequent Sequent
HasDecidableSubstantiveDischarge._≽?_ HasDecidableSubstantiveDischargeSequentSequent = {!!}


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

module Dodo.Binary.Subtraction where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Relation.Binary using (REL)
-- Local imports
open import Dodo.Binary.Empty using (¬₂_)
open import Dodo.Binary.Intersection using (_∩₂_)

-- # Definitions

infixl 30 _\₂_

_\₂_ : {a b ℓ₀ ℓ₁ : Level} {A : Set a} {B : Set b} → REL A B ℓ₀ → REL A B ℓ₁ → REL A B (ℓ₀ ⊔ ℓ₁)
_\₂_ R Q = R ∩₂ (¬₂ Q)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

module Properties.StrictMode where

import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=; ··)
open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp)
open import Luau.Var using (_≡ⱽ_)
open import Luau.Addr using (_≡ᴬ_)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
open import Luau.VarCtxt using (VarCtxt; ∅)
open import Properties.Remember using (remember; _,_)
open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber; mustBeString)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (valueType)

src = Luau.Type.src strict

data _⊑_ (H : Heap yes) : Heap yes → Set where
  refl : (H ⊑ H)
  snoc : ∀ {H′ a V} → (H′ ≡ᴴ H ⊕ a ↦ V) → (H ⊑ H′)

rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′)
rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′)

rednᴱ⊑ (function a p) = snoc p
rednᴱ⊑ (app₁ s) = rednᴱ⊑ s
rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s
rednᴱ⊑ (beta O v p q) = refl
rednᴱ⊑ (block s) = rednᴮ⊑ s
rednᴱ⊑ (return v) = refl
rednᴱ⊑ done = refl
rednᴱ⊑ (binOp₀ p) = refl
rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s
rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s

rednᴮ⊑ (local s) = rednᴱ⊑ s
rednᴮ⊑ (subst v) = refl
rednᴮ⊑ (function a p) = snoc p
rednᴮ⊑ (return s) = rednᴱ⊑ s

data LookupResult (H : Heap yes) a V : Set where
  just : (H [ a ]ᴴ ≡ just V) → LookupResult H a V
  nothing : (H [ a ]ᴴ ≡ nothing) → LookupResult H a V

lookup-⊑-nothing : ∀ {H H′} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ nothing) → (H [ a ]ᴴ ≡ nothing)
lookup-⊑-nothing {H} a refl p = p
lookup-⊑-nothing {H} a (snoc defn) p with a ≡ᴬ next H
lookup-⊑-nothing {H} a (snoc defn) p | yes refl = refl
lookup-⊑-nothing {H} a (snoc o) p | no q = trans (lookup-not-allocated o q) p

data OrWarningᴱ {Γ M T} (H : Heap yes) (D : Γ ⊢ᴱ M ∈ T) A : Set where
  ok : A → OrWarningᴱ H D A
  warning : Warningᴱ H D → OrWarningᴱ H D A

data OrWarningᴮ {Γ B T} (H : Heap yes) (D : Γ ⊢ᴮ B ∈ T) A : Set where
  ok : A → OrWarningᴮ H D A
  warning : Warningᴮ H D → OrWarningᴮ H D A

data OrWarningᴴᴱ {Γ M T} H (D : Γ ⊢ᴴᴱ H ▷ M ∈ T) A : Set where
  ok : A → OrWarningᴴᴱ H D A
  warning : Warningᴴᴱ H D → OrWarningᴴᴱ H D A

data OrWarningᴴᴮ {Γ B T} H (D : Γ ⊢ᴴᴮ H ▷ B ∈ T) A : Set where
  ok : A → OrWarningᴴᴮ H D A
  warning : Warningᴴᴮ H D → OrWarningᴴᴮ H D A

heap-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M)
heap-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B)

heap-weakeningᴱ H (var x) h = ok refl
heap-weakeningᴱ H (val nil) h = ok refl
heap-weakeningᴱ H (val (addr a)) refl = ok refl
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} defn) with a ≡ᴬ b
heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl)
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q)))
heap-weakeningᴱ H (val (number n)) h = ok refl
heap-weakeningᴱ H (val (bool b)) h = ok refl
heap-weakeningᴱ H (val (string x)) h = ok refl
heap-weakeningᴱ H (binexp M op N) h = ok refl
heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h
heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p)
heap-weakeningᴱ H (M $ N) h | warning W = warning (app₁ W)
heap-weakeningᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h = ok refl
heap-weakeningᴱ H (block var b ∈ T is B end) h = ok refl
heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h with heap-weakeningᴮ H B h
heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | ok p = ok p
heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ W)
heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h with heap-weakeningᴮ H B h
heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | ok p = ok p
heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | warning W = warning (local₂ W)
heap-weakeningᴮ H (return M ∙ B) h with heap-weakeningᴱ H M h
heap-weakeningᴮ H (return M ∙ B) h | ok p = ok p
heap-weakeningᴮ H (return M ∙ B) h | warning W = warning (return W)
heap-weakeningᴮ H (done) h = ok refl

none-not-obj : ∀ O → none ≢ typeOfᴼ O
none-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) ()

typeOf-val-not-none : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (none ≢ typeOfᴱ H Γ (val v))
typeOf-val-not-none nil = ok (λ ())
typeOf-val-not-none (number n) = ok (λ ())
typeOf-val-not-none (bool b) = ok (λ ())
typeOf-val-not-none (string x) = ok (λ ())
typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ)
typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q → none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p))))
typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p)

substitutivityᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ))
substitutivityᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p)))
substitutivityᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p)))
substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ))
substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p)))
substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p)))

substitutivityᴱ H (var y) v x p with x ≡ⱽ y
substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p
substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q p
substitutivityᴱ H (val w) v x p = refl
substitutivityᴱ H (binexp M op N) v x p = refl
substitutivityᴱ H (M $ N) v x p = cong tgt (substitutivityᴱ H M v x p)
substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = refl
substitutivityᴱ H (block var b ∈ T is B end) v x p = refl
substitutivityᴱ-whenever-yes H v x x refl q = cong orNone q
substitutivityᴱ-whenever-no H v x y p q = cong orNone ( sym (⊕-lookup-miss x y _ _ p))
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x f q p (⊕-over q)
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x f q p (⊕-swap q)
substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y
substitutivityᴮ H (local var y ∈ T  ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q)
substitutivityᴮ H (local var y ∈ T  ← M ∙ B) v x p | no q =  substitutivityᴮ-unless-no H B v x y q p (⊕-swap q)
substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p
substitutivityᴮ H done v x p = refl
substitutivityᴮ-unless-yes H B v x x refl q refl = refl
substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q

binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x))
binOpPreservation H (+ m n) = refl
binOpPreservation H (- m n) = refl
binOpPreservation H (/ m n) = refl
binOpPreservation H (* m n) = refl
binOpPreservation H (< m n) = refl
binOpPreservation H (> m n) = refl
binOpPreservation H (<= m n) = refl
binOpPreservation H (>= m n) = refl
binOpPreservation H (== v w) = refl
binOpPreservation H (~= v w) = refl
binOpPreservation H (·· v w) = refl

preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′)
preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′)

preservationᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) = ok refl
preservationᴱ H (M $ N) (app₁ s) with preservationᴱ H M s
preservationᴱ H (M $ N) (app₁ s) | ok p = ok (cong tgt p)
preservationᴱ H (M $ N) (app₁ s) | warning (expr W) = warning (expr (app₁ W))
preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W)
preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s)
preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q)
preservationᴱ H (M $ N) (app₂ p s) | warning W  = warning (expr (app₁ W))
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v)
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orNone (cong typeOfᴹᴼ p)))
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (FunctionDefnMismatch r)))
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (FunctionCallMismatch (λ s → r (trans (trans (sym (cong src (cong orNone (cong typeOfᴹᴼ p)))) s) (cong orNone q)))))
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-none v
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (cong orNone q)))
preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W))
preservationᴱ H (block var b ∈ T is B end) (block s) = ok refl
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) with T ≡ᵀ typeOfᴱ H ∅ (val v)
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | yes p = ok p
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (BlockMismatch p))
preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil
preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p
preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (BlockMismatch p))
preservationᴱ H (binexp M op N) (binOp₀ s) = ok (binOpPreservation H s)
preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl
preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl

preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s)
preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p
preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warning (block (local₂ W))
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) with remember (typeOfⱽ H v)
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) with T ≡ᵀ U
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p))
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r → q (trans r (cong orNone p)))))
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-none v
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orNone p)))
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W))
preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) with heap-weakeningᴮ H B (snoc defn)
preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | ok r = ok (trans r (substitutivityᴮ _ B (addr a) f refl))
preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ W))
preservationᴮ H (return M ∙ B) (return s) with preservationᴱ H M s
preservationᴮ H (return M ∙ B) (return s) | ok p = ok p
preservationᴮ H (return M ∙ B) (return s) | warning (expr W) = warning (block (return W))
preservationᴮ H (return M ∙ B) (return s) | warning (heap W) = warning (heap W)

reflect-substitutionᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M)
reflect-substitutionᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))
reflect-substitutionᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H  (Γ ⊕ x ↦ T) (var y))
reflect-substitutionᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B)
reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B)

reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y
reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W
reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W
reflect-substitutionᴱ H (val (addr a)) v x p (UnallocatedAddress r) = UnallocatedAddress r
reflect-substitutionᴱ H (M $ N) v x p (FunctionCallMismatch q) = FunctionCallMismatch (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p))))
reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W)
reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W)
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r))))
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r))))
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y)
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (BlockMismatch q) = BlockMismatch (λ r → q (trans r (substitutivityᴮ H B v x p)))
reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W)
reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₁ q) = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H M x v p)) q)
reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₂ q) = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H N x v p)) q)
reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W)
reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W)

reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable r) = UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) r)
reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q)
reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | ()

reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r))))
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r))))
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) with (x ≡ⱽ y)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W) with (x ≡ⱽ f)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (LocalVarMismatch q) = LocalVarMismatch (λ r → q (trans r (substitutivityᴱ H M v x p)))
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
reflect-substitutionᴮ H (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W)

reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W
reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W

reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M)
reflect-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B)

reflect-weakeningᴱ H (var x) h (UnboundVariable p) = (UnboundVariable p)
reflect-weakeningᴱ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | ok q₁ | ok q₂ = FunctionCallMismatch (λ r → p (trans (cong src (sym q₁)) (trans r q₂)))
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | warning W | _ = app₁ W
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | _ | warning W = app₂ W
reflect-weakeningᴱ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ H M h W)
reflect-weakeningᴱ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ H N h W)
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) with heap-weakeningᴱ H M h
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | ok q = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | warning W = bin₁ W
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) with heap-weakeningᴱ H N h
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | ok q = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p)
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | warning W = bin₂ W
reflect-weakeningᴱ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ H M h W′)
reflect-weakeningᴱ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ H N h W′)
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | warning W = function₁ W
reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W)
reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) with heap-weakeningᴮ H B h
reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | ok q = BlockMismatch (λ r → p (trans r q))
reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | warning W = block₁ W
reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W)

reflect-weakeningᴮ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ H M h W)
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) with heap-weakeningᴱ H M h
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | ok q = LocalVarMismatch (λ r → p (trans r q))
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | warning W = local₁ W
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ H M h W)
reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ H B h W)
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) with heap-weakeningᴮ H C h
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | warning W = function₁ W
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W)
reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ H B h W)

reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O)
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | warning W = function₁ W
reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ W′) = function₁ (reflect-weakeningᴮ H B h W′)

reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M)
reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)

reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s)
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p (trans (trans (cong src (sym q)) r) q′)))
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (expr W) | _ = expr (app₁ W)
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (heap W) | _ = heap W
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | _ | warning W  = expr (app₂ W)
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) with reflectᴱ H M s W′
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | heap W = heap W
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | expr W = expr (app₁ W)
reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p′ (trans (trans (cong src (sym q)) r) q′)))
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | warning W | _ = expr (app₁ W)
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (expr W) = expr (app₂ W)
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (heap W) = heap W
reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W)
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with remember (typeOfⱽ H v)
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) with S ≡ᵀ T
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just T , r) | yes refl = heap (addr a p (FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ H B v x (sym r))))))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) | no s = expr (FunctionCallMismatch (λ t → s (trans (cong orNone (sym r)) (trans (sym t) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-none v
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (cong orNone (sym r)))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | warning W = expr (app₂ W)
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with remember (typeOfⱽ H v)
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) with S ≡ᵀ T
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W′)))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (FunctionCallMismatch (λ s → r (trans (cong orNone (sym q)) (trans (sym s) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-none v
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (cong orNone (sym q)))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | warning W = expr (app₂ W)
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) with preservationᴮ H B s
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | ok q = expr (BlockMismatch (λ r → p (trans r q)))
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (heap W) = heap W
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (block W) = expr (block₁ W)
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W)
reflectᴱ H (block var b ∈ T is B end) (return v) W′ = expr (block₁ (return W′))
reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) with preservationᴱ H M s
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (heap W) = heap W
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (expr W) = expr (bin₁ W)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ ((subst₁ (BinOpWarning op) (sym q) p)))
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | warning W = expr (bin₂ W)
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) with reflectᴱ H M s W′
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | heap W = heap W
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | expr W = expr (bin₁ W)
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s)
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | warning W = expr (bin₁ W)
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) with preservationᴱ H N s
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (heap W) = heap W
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (expr W) = expr (bin₂ W)
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) with reflectᴱ H N s W′
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | heap W = heap W
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | expr W = expr (bin₂ W)

reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) with preservationᴱ H M s
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | ok q = block (LocalVarMismatch (λ r → p (trans r q)))
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (expr W) = block (local₁ W)
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (heap W) = heap W
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) with reflectᴱ H M s W′
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | heap W = heap W
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | expr W = block (local₁ W)
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W′))
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ with remember (typeOfⱽ H v)
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) with S ≡ᵀ T
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W′))
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (LocalVarMismatch (λ r → q (trans (cong orNone (sym p)) (sym r))))
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-none v
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (cong orNone (sym p)))
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | warning W = block (local₁ W)
reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ = block (function₂ (reflect-weakeningᴮ H B (snoc defn) (reflect-substitutionᴮ _ B (addr a) f refl W′)))
reflectᴮ H (return M ∙ B) (return s) (return W′) with reflectᴱ H M s W′
reflectᴮ H (return M ∙ B) (return s) (return W′) | heap W = heap W
reflectᴮ H (return M ∙ B) (return s) (return W′) | expr W = block (return W)

reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴᴱ H′ (typeCheckᴴᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M)
reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)

reflectᴴᴱ H M s (expr W′) = reflectᴱ H M s W′
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H B (snoc defn)
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = expr (FunctionDefnMismatch λ q → p (trans q r))
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = expr (function₁ W)
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W′))
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′))
reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | heap W = heap W
reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | expr W = expr (app₁ W)
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) with reflectᴴᴱ H N s (heap W′)
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | heap W = heap W
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W)
reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′)
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W)
reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′
reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′
reflectᴴᴱ H (binexp M op N) (binOp₀ s) (heap W′) = heap W′
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | heap W = heap W
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | expr W = expr (bin₁ W)
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) with reflectᴴᴱ H N s (heap W′)
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | heap W = heap W
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | expr W = expr (bin₂ W)

reflectᴴᴮ H B s (block W′) = reflectᴮ H B s W′
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) with reflectᴴᴱ H M s (heap W′)
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | heap W = heap W
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | expr W = block (local₁ W)
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) (heap W′) = heap W′
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H C (snoc defn)
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = block (FunctionDefnMismatch (λ q → p (trans q r)))
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = block (function₁ W)
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W′))
reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′))
reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) with reflectᴴᴱ H M s (heap W′)
reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | heap W = heap W
reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | expr W = block (return W)

reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)
reflect* H B refl W = W
reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)

runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → BinOpWarning op (orNone (typeOfⱽ H v))
runtimeBinOpWarning H v (+ p) = + (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (- p) = - (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (* p) = * (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (/ p) = / (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (< p) = < (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (> p) = > (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (·· p) = ·· (λ q → p (mustBeString H ∅ v q))

runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)

runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl
runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-none w
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = FunctionCallMismatch (λ r → p (mustBeFunction H ∅ v (λ r′ → q (trans r′ r))))
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W
runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err)
runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err)
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₁ v w p) = BinOpMismatch₁ (runtimeBinOpWarning H v p)
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₂ v w p) = BinOpMismatch₂ (runtimeBinOpWarning H w p)
runtimeWarningᴱ H (binexp M op N) (bin₁ err) = bin₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (binexp M op N) (bin₂ err) = bin₂ (runtimeWarningᴱ H N err)

runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err)
runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err)

wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B)
wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (block (runtimeWarningᴮ H′ B′ err))
wellTypedProgramsDontGoWrong H′ B B′ t err | heap (addr a refl ())
wellTypedProgramsDontGoWrong H′ B B′ t err | block W = W

max_stars_repo_name: gideros/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------------
-- Properties for the relation LTL
------------------------------------------------------------------------------

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

module FOTC.Data.List.WF-Relation.LT-Length.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI as Nat using ()
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Length

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

xs<[]→⊥ : ∀ {xs} → List xs → ¬ (LTL xs [])
xs<[]→⊥ Lxs xs<[] = lg-xs<lg-[]→⊥ Lxs xs<[]

x∷xs<y∷ys→xs<ys : ∀ {x xs y ys} → List xs → List ys →
                  LTL (x ∷ xs) (y ∷ ys) → LTL xs ys
x∷xs<y∷ys→xs<ys {x} {xs} {y} {ys} Lxs Lys x∷xs<y∷ys = Nat.Sx<Sy→x<y helper
  where
  helper : succ₁ (length xs) < succ₁ (length ys)
  helper =
    lt (succ₁ (length xs)) (succ₁ (length ys))
      ≡⟨ subst₂ (λ t t' → lt (succ₁ (length xs)) (succ₁ (length ys)) ≡ lt t t')
                (sym (length-∷ x xs))
                (sym (length-∷ y ys))
                refl
      ⟩
    lt (length (x ∷ xs)) (length (y ∷ ys))
      ≡⟨ x∷xs<y∷ys ⟩
    true ∎

<-trans : ∀ {xs ys zs} → List xs → List ys → List zs →
          LTL xs ys → LTL ys zs → LTL xs zs

<-trans Lxs Lys Lzs xs<ys ys<zs =
  Nat.<-trans (lengthList-N Lxs) (lengthList-N Lys) (lengthList-N Lzs) xs<ys ys<zs

lg-xs≡lg-ys→ys<zx→xs<zs : ∀ {xs ys zs} → length xs ≡ length ys →
                          LTL ys zs → LTL xs zs
lg-xs≡lg-ys→ys<zx→xs<zs {xs} {ys} {zs} h ys<zs =
  lt (length xs) (length zs)
    ≡⟨ subst (λ t → lt (length xs) (length zs) ≡ lt t (length zs)) h refl ⟩
  lt (length ys) (length zs)
    ≡⟨ ys<zs ⟩
  true ∎

xs<y∷ys→xs<ys∨lg-xs≡lg-ys : ∀ {xs y ys} → List xs → List ys →
                            LTL xs (y ∷ ys) →
                            LTL xs ys ∨ length xs ≡ length ys
xs<y∷ys→xs<ys∨lg-xs≡lg-ys {xs} {y} {ys} Lxs Lys xs<y∷ys =
  Nat.x<Sy→x<y∨x≡y (lengthList-N Lxs) (lengthList-N Lys) helper
  where
  helper : length xs < succ₁ (length ys)
  helper =
    lt (length xs) (succ₁ (length ys))
      ≡⟨ subst (λ t → lt (length xs) (succ₁ (length ys)) ≡ lt (length xs) t)
               (sym (length-∷ y ys))
               refl
      ⟩
    lt (length xs) (length (y ∷ ys))
      ≡⟨ xs<y∷ys ⟩
    true ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Optics.Lens where
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Data.Product using (_×_; _,_; ∃-syntax)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; module ≡-Reasoning; cong)

open import Category.Functor.Arr
open import Category.Functor.Const
open import Category.Profunctor.Star
open import Category.Strong
open import Optics

Lens : ∀ {l} (S T A B : Set l) → Set (lsuc l)
Lens = Optic StrongImp

module Lens {l} {S T A B : Set l} (lens : Lens S T A B) where
  get : S → A
  get = getOptic S T A B (starStrong constFunctor) lens
  set : S → B → T
  set = setOptic S T A B (starStrong arrFunctor) lens

record LawfulLens {l} {S A : Set l} (lens' : Lens S S A A) : Set (lsuc l) where
  open Lens lens' public
  lens : Lens S S A A
  lens = lens'
  field
    setget : ∀ (s : S) → set s (get s) ≡ s
    getset : ∀ (s : S) (a : A) → get (set s a) ≡ a
    setset : ∀ (s : S) (a a' : A) → set (set s a) ≡ set s

lensIso : ∀ {l} {S A : Set l} {lens : Lens S S A A} → (lawful : LawfulLens lens) → S ↔ (∃[ a ] ∃[ c ] ∃[ s ] (c ≡ Lens.set lens s × Lens.get lens s ≡ a))
lensIso {_} {S} {A} lawful = inverse to from from∘to to∘from
   where
     open LawfulLens lawful
     to : S → ∃[ a ] ∃[ c ] ∃[ s ] (c ≡ set s × get s ≡ a)
     to s = get s , set s , s , refl , refl
     from : ∃[ a ] ∃[ c ] ∃[ s ] (c ≡ set s × get s ≡ a) → S
     from (a , c , _ , _  , _) = c a
     from∘to : (s : S) → from (to s) ≡ s
     from∘to = setget
     to∘from : (elem : ∃[ a ] ∃[ c ] ∃[ s ] (c ≡ set s × get s ≡ a)) → to (from elem) ≡ elem
     open ≡-Reasoning
     to∘from (.(get s) , .(set s) , s , refl , refl) = begin
       (get (set s (get s)) , set (set s (get s)) , set s (get s) , _ , _) ≡⟨ cong (λ sᵢ → get sᵢ , set sᵢ , sᵢ , refl , refl) (setget s) ⟩
       (get s , set s , s , _ , _) ∎

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


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

{-
Imports everything that is not imported by something else.
This is not supposed to be used anywhere, this is just a simple way to
do `make all'

This file is intentionally named index.agda so that
Agda will generate index.html.
-}

module index where

{- some group theory results -}
import groups.ReducedWord
import groups.ProductRepr
import groups.CoefficientExtensionality

{- homotopy groups of circles -}
import homotopy.LoopSpaceCircle
import homotopy.PinSn
import homotopy.HopfJunior
import homotopy.Hopf

{- cohomology -}
import cohomology.EMModel
import cohomology.Sigma
import cohomology.Coproduct
import cohomology.Torus
-- import cohomology.MayerVietorisExact -- FIXME

{- prop * prop is still a prop -}
import homotopy.PropJoinProp

{- a space with preassigned homotopy groups -}
import homotopy.SpaceFromGroups

{- pushout 3x3 lemma -}
{- These takes lots of time and memory to check. -}
-- import homotopy.3x3.Commutes -- commented out because this does not run on travis.
-- import homotopy.JoinAssoc3x3 -- commented out because this does not run on travis.

{- covering spaces -}
import homotopy.GroupSetsRepresentCovers
import homotopy.AnyUniversalCoverIsPathSet
import homotopy.PathSetIsInitalCover

{- van kampen -}
import homotopy.VanKampen

{- blakers massey -}
import homotopy.BlakersMassey

{- cw complexes -}
import cw.CW
import cw.examples.Examples
-- cellular cohomology groups
import cw.cohomology.CellularChainComplex
-- Eilenberg-Steenred cohomology groups rephrased
import cw.cohomology.ReconstructedCohomologyGroups
-- isomorphisms between the cochains the heads
import cw.cohomology.ReconstructedCochainsIsoCellularCochains

-- There are some unported theorems

-- import Spaces.IntervalProps
-- import Algebra.F2NotCommutative
-- import Spaces.LoopSpaceDecidableWedgeCircles
-- import Homotopy.PullbackIsPullback
-- import Homotopy.PushoutIsPushout
-- import Homotopy.Truncation
-- import Sets.QuotientUP

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda