text:
------------------------------------------------------------------------------
-- The Booleans properties
------------------------------------------------------------------------------

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

module FOTC.Data.Bool.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Bool
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.Type

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

&&-leftCong : ∀ {a b c} → a ≡ b → a && c ≡ b && c
&&-leftCong refl = refl

&&-rightCong : ∀ {a b c} → b ≡ c → a && b ≡ a && c
&&-rightCong refl = refl

&&-cong : ∀ {a b c d } → a ≡ c → b ≡ d → a && b ≡ c && d
&&-cong refl refl = refl

notCong : ∀ {a b} → a ≡ b → not a ≡ not b
notCong refl = refl

------------------------------------------------------------------------------
-- Basic properties

t&&x≡x : ∀ b → true && b ≡ b
t&&x≡x b = if-true b

f&&x≡f : ∀ b → false && b ≡ false
f&&x≡f b = if-false false

not-t : not true ≡ false
not-t = if-true false

not-f : not false ≡ true
not-f = if-false true

&&-Bool : ∀ {a b} → Bool a → Bool b → Bool (a && b)
&&-Bool {b = b} btrue  Bb = subst Bool (sym (t&&x≡x b)) Bb
&&-Bool {b = b} bfalse Bb = subst Bool (sym (f&&x≡f b)) bfalse

not-Bool : ∀ {b} → Bool b → Bool (not b)
not-Bool btrue  = subst Bool (sym not-t) bfalse
not-Bool bfalse = subst Bool (sym not-f) btrue

&&-comm : ∀ {a b} → Bool a → Bool b → a && b ≡ b && a
&&-comm btrue  btrue  = refl
&&-comm btrue  bfalse = trans (t&&x≡x false) (sym (f&&x≡f true))
&&-comm bfalse btrue  = trans (f&&x≡f true) (sym (t&&x≡x false))
&&-comm bfalse bfalse = refl

&&-assoc : ∀ {a b c} → Bool a → Bool b → Bool c → (a && b) && c ≡ a && b && c
&&-assoc btrue btrue btrue = &&-cong (t&&x≡x true) (sym (t&&x≡x true))
&&-assoc btrue btrue bfalse = &&-cong (t&&x≡x true) (sym (t&&x≡x false))
&&-assoc btrue bfalse btrue =
  (true && false) && true ≡⟨ &&-comm (&&-Bool btrue bfalse) btrue ⟩
  true && (true && false) ≡⟨ t&&x≡x (true && false) ⟩
  true && false           ≡⟨ &&-rightCong (sym (f&&x≡f true)) ⟩
  true && false && true   ∎
&&-assoc btrue bfalse bfalse =
  (true && false) && false ≡⟨ &&-comm (&&-Bool btrue bfalse) bfalse ⟩
  false && (true && false) ≡⟨ f&&x≡f (true && false) ⟩
  false                    ≡⟨ sym (f&&x≡f false) ⟩
  false && false           ≡⟨ sym (t&&x≡x (false && false)) ⟩
  true && false && false   ∎
&&-assoc bfalse btrue btrue = &&-cong (f&&x≡f true) (sym (t&&x≡x true))
&&-assoc bfalse btrue bfalse = &&-cong (f&&x≡f true) (sym (t&&x≡x false))
&&-assoc bfalse bfalse btrue =
  (false && false) && true ≡⟨ &&-comm (&&-Bool bfalse bfalse) btrue ⟩
  true && (false && false) ≡⟨ t&&x≡x (false && false) ⟩
  false && false           ≡⟨ f&&x≡f false ⟩
  false                    ≡⟨ sym (f&&x≡f (false && true)) ⟩
  false && false && true   ∎
&&-assoc bfalse bfalse bfalse = &&-cong (f&&x≡f false) (sym (f&&x≡f false))

&&-list₂-t : ∀ {a b} → Bool a → Bool b → a && b ≡ true → a ≡ true ∧ b ≡ true
&&-list₂-t btrue  btrue  h = refl , refl
&&-list₂-t btrue  bfalse h = ⊥-elim (t≢f (trans (sym h) (t&&x≡x false)))
&&-list₂-t bfalse btrue  h = ⊥-elim (t≢f (trans (sym h) (f&&x≡f true)))
&&-list₂-t bfalse bfalse h = ⊥-elim (t≢f (trans (sym h) (f&&x≡f false)))

&&-list₂-t₁ : ∀ {a b} → Bool a → Bool b → a && b ≡ true → a ≡ true
&&-list₂-t₁ Ba Bb h = ∧-proj₁ (&&-list₂-t Ba Bb h)

&&-list₂-t₂ : ∀ {a b} → Bool a → Bool b → a && b ≡ true → b ≡ true
&&-list₂-t₂ Ba Bb h = ∧-proj₂ (&&-list₂-t Ba Bb h)

&&-list₂-all-t : ∀ {a b} → Bool a → Bool b →
                 (a ≡ true ∧ b ≡ true) →
                 a && b ≡ true
&&-list₂-all-t btrue  btrue  h         = t&&x≡x true
&&-list₂-all-t btrue  bfalse (h₁ , h₂) = ⊥-elim (t≢f (sym h₂))
&&-list₂-all-t bfalse Bb     (h₁ , h₂) = ⊥-elim (t≢f (sym h₁))

&&-list₃-all-t : ∀ {a b c} → Bool a → Bool b → Bool c →
                 a ≡ true ∧ b ≡ true ∧ c ≡ true →
                 a && b && c ≡ true
&&-list₃-all-t btrue btrue btrue h = trans (t&&x≡x (true && true)) (t&&x≡x true)
&&-list₃-all-t btrue btrue bfalse (h₁ , h₂ , h₃) = ⊥-elim (t≢f (sym h₃))
&&-list₃-all-t btrue bfalse Bc (h₁ , h₂ , h₃) = ⊥-elim (t≢f (sym h₂))
&&-list₃-all-t bfalse Bb Bc (h₁ , h₂ , h₃) = ⊥-elim (t≢f (sym h₁))

&&-list₄-all-t : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
                 a ≡ true ∧ b ≡ true ∧ c ≡ true ∧ d ≡ true →
                 a && b && c && d ≡ true
&&-list₄-all-t btrue btrue btrue btrue h =
  trans₂ (t&&x≡x (true && true && true)) (t&&x≡x (true && true)) (t&&x≡x true)
&&-list₄-all-t btrue btrue btrue bfalse (h₁ , h₂ , h₃ , h₄) = ⊥-elim (t≢f (sym h₄))
&&-list₄-all-t btrue btrue bfalse Bd (h₁ , h₂ , h₃ , h₄) = ⊥-elim (t≢f (sym h₃))
&&-list₄-all-t btrue bfalse Bc Bd (h₁ , h₂ , h₃ , h₄) = ⊥-elim (t≢f (sym h₂))
&&-list₄-all-t bfalse Bb Bc Bd (h₁ , h₂ , h₃ , h₄) = ⊥-elim (t≢f (sym h₁))

&&-list₄-some-f : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
                  a ≡ false ∨ b ≡ false ∨ c ≡ false ∨ d ≡ false →
                  a && b && c && d ≡ false
&&-list₄-some-f btrue Bb Bc Bd (inj₁ h) = ⊥-elim (t≢f h)
&&-list₄-some-f btrue btrue Bc Bd (inj₂ (inj₁ h)) = ⊥-elim (t≢f h)
&&-list₄-some-f btrue btrue btrue Bd (inj₂ (inj₂ (inj₁ h))) = ⊥-elim (t≢f h)
&&-list₄-some-f btrue btrue btrue btrue (inj₂ (inj₂ (inj₂ h))) = ⊥-elim (t≢f h)
&&-list₄-some-f btrue btrue btrue bfalse (inj₂ (inj₂ (inj₂ h))) =
  trans (t&&x≡x (true && true && false))
        (trans (t&&x≡x (true && false)) (t&&x≡x false))
&&-list₄-some-f btrue btrue bfalse btrue (inj₂ (inj₂ (inj₁ h))) =
  trans (t&&x≡x (true && false && true))
        (trans (t&&x≡x (false && true)) (f&&x≡f true))
&&-list₄-some-f btrue btrue bfalse btrue (inj₂ (inj₂ (inj₂ h))) = ⊥-elim (t≢f h)
&&-list₄-some-f btrue btrue bfalse bfalse (inj₂ (inj₂ h)) =
  trans (t&&x≡x (true && false && false))
        (trans (t&&x≡x (false && false)) (f&&x≡f false))
&&-list₄-some-f {c = c} {d} btrue bfalse Bc Bd (inj₂ h) =
  trans (t&&x≡x (false && c && d)) (f&&x≡f (c && d))
&&-list₄-some-f {b = b} {c} {d} bfalse Bb Bc Bd _ = f&&x≡f (b && c && d)

&&-list₄-t : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
             a && b && c && d ≡ true →
             a ≡ true ∧ b ≡ true ∧ c ≡ true ∧ d ≡ true
&&-list₄-t btrue btrue btrue btrue h = refl , refl , refl , refl
&&-list₄-t btrue btrue btrue bfalse h =
  ⊥-elim (t≢f
           (trans (sym h)
                  (&&-list₄-some-f btrue btrue btrue bfalse (inj₂ (inj₂ (inj₂ refl))))))
&&-list₄-t btrue btrue bfalse Bd h =
  ⊥-elim (t≢f
           (trans (sym h)
                  (&&-list₄-some-f btrue btrue bfalse Bd (inj₂ (inj₂ (inj₁ refl))))))
&&-list₄-t btrue bfalse Bc Bd h =
  ⊥-elim (t≢f
           (trans (sym h) (&&-list₄-some-f btrue bfalse Bc Bd (inj₂ (inj₁ refl)))))
&&-list₄-t bfalse Bb Bc Bd h =
  ⊥-elim (t≢f (trans (sym h) (&&-list₄-some-f bfalse Bb Bc Bd (inj₁ refl))))

&&-list₄-t₁ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → a ≡ true
&&-list₄-t₁ Ba Bb Bc Bd h = ∧-proj₁ (&&-list₄-t Ba Bb Bc Bd h)

&&-list₄-t₂ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → b ≡ true
&&-list₄-t₂ Ba Bb Bc Bd h = ∧-proj₁ (∧-proj₂ (&&-list₄-t Ba Bb Bc Bd h))

&&-list₄-t₃ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → c ≡ true
&&-list₄-t₃ Ba Bb Bc Bd h =
  ∧-proj₁ (∧-proj₂ (∧-proj₂ (&&-list₄-t Ba Bb Bc Bd h)))

&&-list₄-t₄ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → d ≡ true
&&-list₄-t₄ Ba Bb Bc Bd h =
  ∧-proj₂ (∧-proj₂ (∧-proj₂ (&&-list₄-t Ba Bb Bc Bd h)))

x≢not-x : ∀ {b} → Bool b → b ≢ not b
x≢not-x btrue  h = t≢f (trans h not-t)
x≢not-x bfalse h = t≢f (sym (trans h not-f))

not-x≢x : ∀ {b} → Bool b → not b ≢ b
not-x≢x Bb h = x≢not-x Bb (sym h)

not-involutive : ∀ {b} → Bool b → not (not b) ≡ b
not-involutive btrue  = trans (notCong not-t) not-f
not-involutive bfalse = trans (notCong not-f) not-t

------------------------------------------------------------------------------
-- Properties with inequalities

lt-Bool : ∀ {m n} → N m → N n → Bool (lt m n)
lt-Bool nzero          nzero          = subst Bool (sym lt-00) bfalse
lt-Bool nzero          (nsucc {n} Nn) = subst Bool (sym (lt-0S n)) btrue
lt-Bool (nsucc {m} Nm) nzero          = subst Bool (sym (lt-S0 m)) bfalse
lt-Bool (nsucc {m} Nm) (nsucc {n} Nn) = subst Bool (sym (lt-SS m n)) (lt-Bool Nm Nn)

le-Bool : ∀ {m n} → N m → N n → Bool (le m n)
le-Bool {n = n} nzero          Nn             = subst Bool (sym (lt-0S n)) btrue
le-Bool         (nsucc Nm)     nzero          = subst Bool (sym (Sx≰0 Nm)) bfalse
le-Bool         (nsucc {m} Nm) (nsucc {n} Nn) =
  subst Bool (sym (lt-SS m (succ₁ n))) (le-Bool Nm Nn)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Concepts from rewriting theory
-- Definitions are based on "Term Rewriting Systems" by J.W. Klop
------------------------------------------------------------------------

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

module Relation.Binary.Rewriting where

open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Data.Product using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂)
open import Data.Empty
open import Data.Sum.Base as Sum using (_⊎_)
open import Function using (flip)
open import Induction.WellFounded
open import Level
open import Relation.Binary.Core
open import Relation.Binary.Construct.Closure.Equivalence using (EqClosure)
open import Relation.Binary.Construct.Closure.Equivalence.Properties
open import Relation.Binary.Construct.Closure.Reflexive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.Symmetric
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- The following definitions are taken from Klop [5]
module _ {a ℓ} {A : Set a} (_⟶_ : Rel A ℓ) where

  private
    _⟵_  = flip _⟶_
    _—↠_ = Star _⟶_
    _↔_  = EqClosure _⟶_

  IsNormalForm : A → Set _
  IsNormalForm a = ¬ ∃ λ b → (a ⟶ b)

  HasNormalForm : A → Set _
  HasNormalForm b = ∃ λ a → IsNormalForm a × (b —↠ a)

  NormalForm : Set _
  NormalForm = ∀ {a b} → IsNormalForm a → b ↔ a → b —↠ a

  WeaklyNormalizing : Set _
  WeaklyNormalizing = ∀ a → HasNormalForm a

  StronglyNormalizing : Set _
  StronglyNormalizing = WellFounded _⟵_

  UniqueNormalForm : Set _
  UniqueNormalForm = ∀ {a b} → IsNormalForm a → IsNormalForm b → a ↔ b → a ≡ b

  Confluent : Set _
  Confluent = ∀ {A B C} → A —↠ B → A —↠ C → ∃ λ D → (B —↠ D) × (C —↠ D)

  WeaklyConfluent : Set _
  WeaklyConfluent = ∀ {A B C} → A ⟶ B → A ⟶ C → ∃ λ D → (B —↠ D) × (C —↠ D)

Deterministic : ∀ {a b ℓ₁ ℓ₂} → {A : Set a} → {B : Set b} → Rel B ℓ₁ → REL A B ℓ₂ → Set _
Deterministic _≈_ _—→_ = ∀ {x y z} → x —→ y → x —→ z → y ≈ z

module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where

  private
    _—↠_ = Star _⟶_
    _↔_  = EqClosure _⟶_
    _⟶₊_ = Plus _⟶_

  det⇒conf : Deterministic _≡_ _⟶_ → Confluent _⟶_
  det⇒conf det ε          rs₂        = -, rs₂ , ε
  det⇒conf det rs₁        ε          = -, ε , rs₁
  det⇒conf det (r₁ ◅ rs₁) (r₂ ◅ rs₂)
    rewrite det r₁ r₂ = det⇒conf det rs₁ rs₂

  conf⇒wcr : Confluent _⟶_ → WeaklyConfluent _⟶_
  conf⇒wcr c fst snd = c (fst ◅ ε) (snd ◅ ε)

  conf⇒nf : Confluent _⟶_ → NormalForm _⟶_
  conf⇒nf c aIsNF ε = ε
  conf⇒nf c aIsNF (fwd x ◅ rest) = x ◅ conf⇒nf c aIsNF rest
  conf⇒nf c aIsNF (bwd y ◅ rest) with c (y ◅ ε) (conf⇒nf c aIsNF rest)
  ... | _ , _    , x ◅ _ = ⊥-elim (aIsNF (_ , x))
  ... | _ , left , ε     = left

  conf⇒unf : Confluent _⟶_ → UniqueNormalForm _⟶_
  conf⇒unf _ _     _     ε           = refl
  conf⇒unf _ aIsNF _     (fwd x ◅ _) = ⊥-elim (aIsNF (_ , x))
  conf⇒unf c aIsNF bIsNF (bwd y ◅ r) with c (y ◅ ε) (conf⇒nf c bIsNF r)
  ... | _ , ε     , x ◅ _ = ⊥-elim (bIsNF (_ , x))
  ... | _ , x ◅ _ , _     = ⊥-elim (aIsNF (_ , x))
  ... | _ , ε     , ε     = refl

  un&wn⇒cr : UniqueNormalForm _⟶_ → WeaklyNormalizing _⟶_ → Confluent _⟶_
  un&wn⇒cr un wn {a} {b} {c} aToB aToC with wn b | wn c
  ... | (d , (d-nf , bToD)) | (e , (e-nf , cToE))
    with un d-nf e-nf (a—↠b&a—↠c⇒b↔c (aToB ◅◅ bToD) (aToC ◅◅ cToE))
  ... | refl = d , bToD , cToE

-- Newman's lemma
  sn&wcr⇒cr : StronglyNormalizing _⟶₊_ → WeaklyConfluent _⟶_ → Confluent _⟶_
  sn&wcr⇒cr sn wcr = helper (sn _) where

    starToPlus : ∀ {a b c} → (a ⟶ b) → b —↠ c → a ⟶₊ c
    starToPlus aToB ε = [ aToB ]
    starToPlus {a} aToB (e ◅ bToC) = a ∼⁺⟨ [ aToB ] ⟩ (starToPlus e bToC)

    helper : ∀ {a b c} → (acc : Acc (flip _⟶₊_) a) →
             a —↠ b → a —↠ c → ∃ λ d → (b —↠ d) × (c —↠ d)
    helper _       ε           snd         = -, snd , ε
    helper _       fst         ε           = -, ε   , fst
    helper (acc g) (toJ ◅ fst) (toK ◅ snd) = result where

        wcrProof = wcr toJ toK
        innerPoint = proj₁ wcrProof
        jToInner = proj₁ (proj₂ wcrProof)
        kToInner = proj₂ (proj₂ wcrProof)

        lhs = helper (g _ [ toJ ]) fst jToInner
        rhs = helper (g _ [ toK ]) snd kToInner

        fromAB = proj₁ (proj₂ lhs)
        fromInnerB = proj₂ (proj₂ lhs)

        fromAC = proj₁ (proj₂ rhs)
        fromInnerC = proj₂ (proj₂ rhs)

        aToInner : _ ⟶₊ innerPoint
        aToInner = starToPlus toJ jToInner

        finalRecursion = helper (g innerPoint aToInner) fromInnerB fromInnerC

        bMidToDest = proj₁ (proj₂ finalRecursion)
        cMidToDest = proj₂ (proj₂ finalRecursion)

        result : ∃ λ d → (_ —↠ d) × (_ —↠ d)
        result = _ , fromAB ◅◅ bMidToDest , fromAC ◅◅ cMidToDest

ext: agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Semirings.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Integers.RingStructure.Ring
open import Groups.Orders.Archimedean
open import Rings.Orders.Partial.Definition
open import Numbers.Integers.Order

module Numbers.Integers.RingStructure.Archimedean where

open import Groups.Cyclic.Definition ℤGroup
open import Semirings.Solver ℕSemiring multiplicationNIsCommutative

private
  lemma : (x y : ℕ) → positiveEltPower (nonneg x) y ≡ nonneg (x *N y)
  lemma x zero rewrite Semiring.productZeroRight ℕSemiring x = refl
  lemma x (succ y) rewrite lemma x y | multiplicationNIsCommutative x (succ y) | multiplicationNIsCommutative y x = equalityCommutative (+Zinherits x (x *N y))

ℤArchimedean : Archimedean (toGroup ℤRing ℤPOrderedRing)
ℤArchimedean (nonneg (succ a)) (nonneg (succ b)) 0<a 0<b = succ (succ b) , t
  where
    v : b +N (a +N (a +N a *N b)) ≡ a +N (a +N (b +N a *N b))
    v rewrite Semiring.+Associative ℕSemiring a a (a *N b) | Semiring.+Associative ℕSemiring b (a +N a) (a *N b) | Semiring.+Associative ℕSemiring a b (a *N b) | Semiring.+Associative ℕSemiring a (a +N b) (a *N b) | Semiring.commutative ℕSemiring b (a +N a) | Semiring.+Associative ℕSemiring a a b = refl
    u : succ ((a +N (a +N a *N b)) +N b) ≡ a +N succ (a +N (b +N a *N b))
    u = from (succ (plus (plus (const a) (plus (const a) (times (const a) (const b)))) (const b))) to (plus (const a) (succ (plus (const a) (plus (const b) (times (const a) (const b)))))) by applyEquality succ v
    t : nonneg (succ b) <Z nonneg (succ a) +Z (nonneg (succ a) +Z positiveEltPower (nonneg (succ a)) b)
    t rewrite lemma (succ a) b = lessInherits (succPreservesInequality (le (a +N (a +N a *N b)) u))


text:
------------------------------------------------------------------------
-- Subject reduction for typing in Fω with interval kinds
------------------------------------------------------------------------

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

-- This module proves a variant of subject reduction (aka the
-- "preservation" theorem) for term reduction in Fω with interval
-- kinds.  The subject reduction property proved here is weaker than
-- the one typically found in the literature on other variants of Fω:
-- subject reduction does not hold in arbitrary typing contexts in Fω
-- with interval types because type variables of interval kind can be
-- used to introduce arbitrary typing (in)equalities into the
-- subtyping relation.  In other words, subject reduction does not
-- hold for full β-reduction as reductions under type abstractions are
-- not safe in general.  Note, however, that subject reduction does
-- hold for arbitrary β-reductions in *types* (see `pres-Tp∈-→β*' in
-- the Kinding.Declarative.Validity module for a proof).
--
-- NOTE.  Here we use the CBV evaluation strategy, but this is
-- unnecessarily restrictive.  Other evaluation strategies work so
-- long as they do not allow reductions under type abstractions.
--
-- Together with the "progress" theorem from Typing.Progress, subject
-- reduction ensures type safety.  For details, see e.g.
--
--  * B. C. Pierce, TAPL (2002), pp. 95.
--
--  * A. Wright and M. Felleisen, "A Syntactic Approach to Type
--    Soundness" (1994).

module FOmegaInt.Typing.Preservation where

open import Data.Product using (_,_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)
open import Relation.Binary.PropositionalEquality using (subst)
open import Relation.Nullary.Negation using (contradiction)

open import FOmegaInt.Syntax
open import FOmegaInt.Typing
open import FOmegaInt.Typing.Inversion
open import FOmegaInt.Reduction.Cbv
open import FOmegaInt.Reduction.Full

open Syntax
open TermCtx
open Substitution using (_[_]; weaken-sub)
open Typing
open TypedSubstitution using (Tm∈-[]; <:-[])

-- Types of closed terms are preserved under single-step reduction.
pres : ∀ {a b c} → [] ⊢Tm a ∈ c → a →v b → [] ⊢Tm b ∈ c
pres (∈-var () _ _)
pres (∈-∀-i k-kd a∈b)    ()
pres (∈-→-i a∈* b∈c c∈*) ()
pres (∈-∀-e Λja∈Πkc b∈k) (cont-⊡ j a b) with Tm∈-gen Λja∈Πkc
... | ∈-∀-i j-kd a∈d Πjd<:Πkc =
  let k<∷j , d<:c = <:-∀-inv Πjd<:Πkc
  in ∈-⇑ (Tm∈-[] a∈d (∈-tp (∈-⇑ b∈k k<∷j))) (<:-[] d<:c (∈-tp b∈k))
pres (∈-∀-e a∈Πcd b∈c)   (a→e ⊡ b) = ∈-∀-e (pres a∈Πcd a→e) b∈c
pres (∈-→-e ƛea∈c⇒d v∈c) (cont-· e a v) with Tm∈-gen ƛea∈c⇒d
... | ∈-→-i e∈* a∈f e⇒f<:c⇒d =
  let c<:e , f<:d =  <:-→-inv e⇒f<:c⇒d
  in ∈-⇑ (subst (_ ⊢Tm _ ∈_) (weaken-sub _) (Tm∈-[] a∈f (∈-tm (∈-⇑ v∈c c<:e))))
         f<:d
pres (∈-→-e a∈c⇒d b∈c)   (a→e ·₁ b) = ∈-→-e (pres a∈c⇒d a→e) b∈c
pres (∈-→-e a∈c⇒d b∈c)   (v ·₂ b→e) = ∈-→-e a∈c⇒d (pres b∈c b→e)
pres (∈-⇑ a∈c c<:d)      a→b   = ∈-⇑ (pres a∈c a→b) c<:d

-- Weak preservation (aka subject reduction): types of closed terms
-- are preserved under reduction.
pres* : ∀ {a b c} → [] ⊢Tm a ∈ c → a →v* b → [] ⊢Tm b ∈ c
pres* a∈c ε            = a∈c
pres* a∈d (a→b ◅ b→*c) = pres* (pres a∈d a→b) b→*c

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text: module Unsolved-meta-in-module-telescope (A : _) where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Categories.Category.Construction.CartesianClosedFunctors where

open import Categories.Category
open import Categories.Category.CartesianClosed.Bundle
open import Categories.Functor.CartesianClosed
open import Categories.NaturalTransformation using (NaturalTransformation; id; _∘ᵥ_)
import Categories.NaturalTransformation.Equivalence as NTEq
open import Categories.NaturalTransformation.NaturalIsomorphism
import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence as Eq

open import Data.Product using (_,_)

open import Level

private
  variable o ℓ e o′ ℓ′ e′ : Level

CCCat≅ : (C : CartesianClosedCategory o ℓ e)
  -> (D : CartesianClosedCategory o′ ℓ′ e′)
  -> Category (levelOfTerm C ⊔ levelOfTerm D) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
CCCat≅ C D = record
               { Obj = CartesianClosedF C D
               ; _⇒_ = λ F G → NaturalIsomorphism (CartesianClosedF.F F) (CartesianClosedF.F G)
               ; _≈_ = Eq._≅_
               ; id = refl
               ; _∘_ = _ⓘᵥ_
               ; assoc = assoc , sym-assoc
               ; sym-assoc = sym-assoc , assoc
               ; identityˡ = identityˡ , identityʳ
               ; identityʳ = identityʳ , identityˡ
               ; identity² = identity² , identity²
               ; equiv = Eq.≅-isEquivalence
               ; ∘-resp-≈ = λ (f≅h , f≅h′) (g≅i , g≅i′) → ∘-resp-≈ f≅h g≅i , ∘-resp-≈ g≅i′ f≅h′
               }
  where
    open Category (CartesianClosedCategory.U D)

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
module #4 where

open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Nat

{-
  Exercise 2.4. Define, by induction on n, a general notion of n-dimensional path in a
  type A, simultaneously with the type of boundaries for such paths.
-}

-- We need pointed sets for this part
Set• : ∀ i → Set _
Set• i = Σ (Set i) λ X → X

Ω₁ : ∀ {i} → Set• i → Set• i
Ω₁ (X , x) = ((x ≡ x) , refl)

Ωⁿ : ∀ {i} → ℕ → Set• i → Set• _
Ωⁿ 0 x = x
Ωⁿ (suc n) x = Ωⁿ n (Ω₁ x)

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Function.Iteration where

open import Data
open import Functional
open import Numeral.Natural
open import Type
open import Syntax.Number

module _ {ℓ} {T : Type{ℓ}} where
  -- Repeated function composition
  -- Example:
  --   f ^ 0 = id
  --   f ^ 1 = f
  --   f ^ 2 = f ∘ f
  --   f ^ 3 = f ∘ f ∘ f
  --   f ^ 4 = f ∘ f ∘ f ∘ f
  _^_ : (T → T) → ℕ → (T → T)
  _^_ f 𝟎      = id
  _^_ f (𝐒(n)) = f ∘ (f ^ n)

  _⁰ : (T → T) → (T → T)
  _⁰ = _^ 0

  _¹ : (T → T) → (T → T)
  _¹ = _^ 1

  _² : (T → T) → (T → T)
  _² = _^ 2

  _³ : (T → T) → (T → T)
  _³ = _^ 3

  _⁴ : (T → T) → (T → T)
  _⁴ = _^ 4

  _⁵ : (T → T) → (T → T)
  _⁵ = _^ 5

  _⁶ : (T → T) → (T → T)
  _⁶ = _^ 6

  _⁷ : (T → T) → (T → T)
  _⁷ = _^ 7

  _⁸ : (T → T) → (T → T)
  _⁸ = _^ 8

  _⁹ : (T → T) → (T → T)
  _⁹ = _^ 9

module _ {ℓ₁}{ℓ₂} {X : Type{ℓ₁}} {Y : Type{ℓ₂}} where
  -- Repeat a binary operation n times for the same element and an initial element
  -- Example: repeatₗ 3 id (_∘_) f = ((id ∘ f) ∘ f) ∘ f
  -- Example in Haskell: (foldl (.) (id) (take 5 (repeat f)))
  -- Implementation in Haskell: (\n null op elem -> foldl op null (take n (repeat elem))) :: Int -> a -> (b -> a -> b) -> b -> b
  repeatₗ : ℕ → (Y → X → Y) → (Y → X → Y)
  repeatₗ n (_▫_) null elem = ((_▫ elem) ^ n) (null)

  -- Repeat a binary operation n times for the same element and an initial element
  -- Example: repeatᵣ 3 id (_∘_) f = f ∘ (f ∘ (f ∘ id))
  -- Implementation in Haskell: (\n elem op null -> foldr op null (take n (repeat elem))) :: Int -> a -> (a -> b -> b) -> b -> b
  repeatᵣ : ℕ → (X → Y → Y) → (X → Y → Y)
  repeatᵣ n (_▫_) elem = (elem ▫_) ^ n

module _ {ℓ} {X : Type{ℓ}} where
  -- Repeat a binary operation n times for the same element and using the default element on zero.
  -- Examples:
  --   repeatₗ 0 def (_∘_) f = def
  --   repeatₗ 1 def (_∘_) f = f
  --   repeatₗ 4 def (_∘_) f = ((f ∘ f) ∘ f) ∘ f
  repeatₗ-default : ℕ → (X → X → X) → X → (X → X)
  repeatₗ-default 𝟎      _     def  _    = def
  repeatₗ-default (𝐒(n)) (_▫_) _    elem = repeatₗ(n) (_▫_) elem elem

  -- Repeat a binary operation n times for the same element and using the default element on zero.
  -- Examples:
  --   repeatᵣ 0 f (_∘_) def = def
  --   repeatᵣ 1 f (_∘_) def = f
  --   repeatᵣ 4 f (_∘_) def = f ∘ (f ∘ (f ∘ f))
  repeatᵣ-default : ℕ → (X → X → X) → X → (X → X)
  repeatᵣ-default 𝟎      _     _    def = def
  repeatᵣ-default (𝐒(n)) (_▫_) elem _   = repeatᵣ(n) (_▫_) elem elem

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Conversion {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.RedSteps
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Conversion of syntactic reduction closures.
convRed:*: : ∀ {t u A B Γ} → Γ ⊢ t :⇒*: u ∷ A → Γ ⊢ A ≡ B → Γ ⊢ t :⇒*: u ∷ B
convRed:*: [ ⊢t , ⊢u , d ] A≡B = [ conv ⊢t  A≡B , conv ⊢u  A≡B , conv* d  A≡B ]

mutual
  -- Helper function for conversion of terms converting from left to right.
  convTermT₁ : ∀ {l l′ Γ A B t} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
             → ShapeView Γ l l′ A B [A] [B]
             → Γ ⊩⟨ l ⟩  A ≡ B / [A]
             → Γ ⊩⟨ l ⟩  t ∷ A / [A]
             → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
  convTermT₁ (ℕᵥ D D′) A≡B (ιx (ℕₜ n d n≡n prop)) = ιx (ℕₜ n d n≡n prop)
  convTermT₁ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (ne₌ M D′ neM K≡M))
             (ιx (neₜ k d (neNfₜ neK₂ ⊢k k≡k))) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in ιx (neₜ k (convRed:*: d K≡K₁)
            (neNfₜ neK₂ (conv ⊢k K≡K₁) (~-conv k≡k K≡K₁)))
  convTermT₁ {Γ = Γ} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                         (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
             (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
             (Πₜ f d funcF f≡f [f] [f]₁) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , G₁≡G′ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x) (PE.sym ΠF₁G₁≡ΠF′G′)
                             (≅-eq A≡B)
    in  Πₜ f (convRed:*: d ΠFG≡ΠF₁G₁) funcF (≅-conv f≡f ΠFG≡ΠF₁G₁)
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [b]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [b]
                  [a≡b]₁ = convEqTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a≡b]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a]₁)
                                           ([G≡G′] [ρ] ⊢Δ [a]₁)
              in  convEqTerm₁ ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a]) [G≡G₁]
                              ([f] [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁))
          (λ {ρ} [ρ] ⊢Δ [a] →
             let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                          ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                 [a]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                 [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                   (PE.sym G₁≡G′))
                                          ([G] [ρ] ⊢Δ [a]₁)
                                          ([G≡G′] [ρ] ⊢Δ [a]₁)
             in  convTerm₁ ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a]) [G≡G₁] ([f]₁ [ρ] ⊢Δ [a]₁))
  convTermT₁ (Uᵥ .⁰ 0<1 ⊢Γ .⁰ 0<1 ⊢Γ₁) A≡B t = t
  convTermT₁ (emb⁰¹ PE.refl x) (ιx A≡B) (ιx t) = convTermT₁ x A≡B t
  convTermT₁ (emb¹⁰ PE.refl x) A≡B t = ιx (convTermT₁ x A≡B t)

  -- Helper function for conversion of terms converting from right to left.
  convTermT₂ : ∀ {l l′ Γ A B t} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
           → ShapeView Γ l l′ A B [A] [B]
           → Γ ⊩⟨ l ⟩  A ≡ B / [A]
           → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
           → Γ ⊩⟨ l ⟩  t ∷ A / [A]
  convTermT₂ (ℕᵥ D D′) A≡B (ιx (ℕₜ n d n≡n prop)) = ιx (ℕₜ n d n≡n prop)
  convTermT₂ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (ne₌ M D′ neM K≡M))
             (ιx (neₜ k d (neNfₜ neK₂ ⊢k k≡k))) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in ιx (neₜ k (convRed:*: d K₁≡K)
            (neNfₜ neK₂ (conv ⊢k K₁≡K) (~-conv k≡k K₁≡K)))
  convTermT₂ {Γ = Γ} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                         (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
             (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
             (Πₜ f d funcF f≡f [f] [f]₁) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , G₁≡G′ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x)
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ f (convRed:*: d (sym ΠFG≡ΠF₁G₁)) funcF (≅-conv f≡f (sym ΠFG≡ΠF₁G₁))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [b]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [b]
                  [a≡b]₁ = convEqTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a≡b]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a])
                                           ([G≡G′] [ρ] ⊢Δ [a])
              in  convEqTerm₂ ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                              [G≡G₁] ([f] [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a])
                                           ([G≡G′] [ρ] ⊢Δ [a])
              in  convTerm₂ ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                            [G≡G₁] ([f]₁ [ρ] ⊢Δ [a]₁))
  convTermT₂ (Uᵥ .⁰ 0<1 ⊢Γ .⁰ 0<1 ⊢Γ₁) A≡B t = t
  convTermT₂ (emb⁰¹ PE.refl x) (ιx A≡B) t = ιx (convTermT₂ x A≡B t)
  convTermT₂ (emb¹⁰ PE.refl x) A≡B (ιx t) = convTermT₂ x A≡B t

  -- Conversion of terms converting from left to right.
  convTerm₁ : ∀ {Γ A B t l l′} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
            → Γ ⊩⟨ l ⟩  A ≡ B / [A]
            → Γ ⊩⟨ l ⟩  t ∷ A / [A]
            → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
  convTerm₁ [A] [B] A≡B t = convTermT₁ (goodCases [A] [B] A≡B) A≡B t

  -- Conversion of terms converting from right to left.
  convTerm₂ : ∀ {Γ A B t l l′} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
          → Γ ⊩⟨ l ⟩  A ≡ B / [A]
          → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
          → Γ ⊩⟨ l ⟩  t ∷ A / [A]
  convTerm₂ [A] [B] A≡B t = convTermT₂ (goodCases [A] [B] A≡B) A≡B t

  -- Conversion of terms converting from right to left
  -- with some propsitionally equal types.
  convTerm₂′ : ∀ {Γ A B B′ t l l′} → B PE.≡ B′
          → ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
          → Γ ⊩⟨ l ⟩  A ≡ B′ / [A]
          → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
          → Γ ⊩⟨ l ⟩  t ∷ A / [A]
  convTerm₂′ PE.refl [A] [B] A≡B t = convTerm₂ [A] [B] A≡B t

  -- Helper function for conversion of term equality converting from left to right.
  convEqTermT₁ : ∀ {l l′ Γ A B t u} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
               → ShapeView Γ l l′ A B [A] [B]
               → Γ ⊩⟨ l ⟩  A ≡ B / [A]
               → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
               → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
  convEqTermT₁ (ℕᵥ D D′) A≡B (ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)) = ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)
  convEqTermT₁ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (ne₌ M D′ neM K≡M))
               (ιx (neₜ₌ k m d d′ (neNfₜ₌ neK₂ neM₁ k≡m))) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in ιx (neₜ₌ k m (convRed:*: d K≡K₁)
                 (convRed:*: d′ K≡K₁)
                 (neNfₜ₌ neK₂ neM₁ (~-conv k≡m K≡K₁)))
  convEqTermT₁ {Γ = Γ} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                           (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
               (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
               (Πₜ₌ f g d d′ funcF funcG t≡u [t] [u] [t≡u]) =
    let [A] = Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Πᵣ′ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x)
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ₌ f g (convRed:*: d ΠFG≡ΠF₁G₁) (convRed:*: d′ ΠFG≡ΠF₁G₁)
            funcF funcG (≅-conv t≡u ΠFG≡ΠF₁G₁)
            (convTerm₁ [A] [B] [A≡B] [t]) (convTerm₁ [A] [B] [A≡B] [u])
            (λ {ρ} [ρ] ⊢Δ [a] →
               let F₁≡F′ , G₁≡G′ = Π-PE-injectivity (whrDet* (red D₁ , Πₙ) (D′ , Πₙ))
                   [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                            ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                   [a]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                   [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                     (PE.sym G₁≡G′))
                                            ([G] [ρ] ⊢Δ [a]₁)
                                            ([G≡G′] [ρ] ⊢Δ [a]₁)
               in  convEqTerm₁ ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a])
                               [G≡G₁] ([t≡u] [ρ] ⊢Δ [a]₁))
  convEqTermT₁ (Uᵥ .⁰ 0<1 ⊢Γ .⁰ 0<1 ⊢Γ₁) A≡B t≡u = t≡u
  convEqTermT₁ (emb⁰¹ PE.refl x) (ιx A≡B) (ιx t≡u) = convEqTermT₁ x A≡B t≡u
  convEqTermT₁ (emb¹⁰ PE.refl x) A≡B t≡u = ιx (convEqTermT₁ x A≡B t≡u)

  -- Helper function for conversion of term equality converting from right to left.
  convEqTermT₂ : ∀ {l l′ Γ A B t u} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
             → ShapeView Γ l l′ A B [A] [B]
             → Γ ⊩⟨ l ⟩  A ≡ B / [A]
             → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
             → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
  convEqTermT₂ (ℕᵥ D D′) A≡B (ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)) = ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)
  convEqTermT₂ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (ne₌ M D′ neM K≡M))
               (ιx (neₜ₌ k m d d′ (neNfₜ₌ neK₂ neM₁ k≡m))) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in ιx (neₜ₌ k m (convRed:*: d K₁≡K) (convRed:*: d′ K₁≡K)
                 (neNfₜ₌ neK₂ neM₁ (~-conv k≡m K₁≡K)))
  convEqTermT₂ {Γ = Γ} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                           (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
               (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
               (Πₜ₌ f g d d′ funcF funcG t≡u [t] [u] [t≡u]) =
    let [A] = Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Πᵣ′ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x)
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ₌ f g (convRed:*: d (sym ΠFG≡ΠF₁G₁)) (convRed:*: d′ (sym ΠFG≡ΠF₁G₁))
            funcF funcG (≅-conv t≡u (sym ΠFG≡ΠF₁G₁))
            (convTerm₂ [A] [B] [A≡B] [t]) (convTerm₂ [A] [B] [A≡B] [u])
            (λ {ρ} [ρ] ⊢Δ [a] →
               let F₁≡F′ , G₁≡G′ = Π-PE-injectivity (whrDet* (red D₁ , Πₙ) (D′ , Πₙ))
                   [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                            ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                   [a]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                   [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                     (PE.sym G₁≡G′))
                                            ([G] [ρ] ⊢Δ [a])
                                            ([G≡G′] [ρ] ⊢Δ [a])
               in  convEqTerm₂ ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                               [G≡G₁] ([t≡u] [ρ] ⊢Δ [a]₁))
  convEqTermT₂ (Uᵥ .⁰ 0<1 ⊢Γ .⁰ 0<1 ⊢Γ₁) A≡B t≡u = t≡u
  convEqTermT₂ (emb⁰¹ PE.refl x) (ιx A≡B) t≡u = ιx (convEqTermT₂ x A≡B t≡u)
  convEqTermT₂ (emb¹⁰ PE.refl x) A≡B (ιx t≡u) = convEqTermT₂ x A≡B t≡u

  -- Conversion of term equality converting from left to right.
  convEqTerm₁ : ∀ {l l′ Γ A B t u} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
              → Γ ⊩⟨ l ⟩  A ≡ B / [A]
              → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
              → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
  convEqTerm₁ [A] [B] A≡B t≡u = convEqTermT₁ (goodCases [A] [B] A≡B) A≡B t≡u

  -- Conversion of term equality converting from right to left.
  convEqTerm₂ : ∀ {l l′ Γ A B t u} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
            → Γ ⊩⟨ l ⟩  A ≡ B / [A]
            → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
            → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
  convEqTerm₂ [A] [B] A≡B t≡u = convEqTermT₂ (goodCases [A] [B] A≡B) A≡B t≡u

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
-- Reported by Andrea, 2014-05-xx
-- We cannot prune from a meta if one of its arguments is a lambda.
-- (In some cases we could, but it is hard to get this right,
--  probably needs a flow analysis.)
-- {-# OPTIONS -v tc.meta.assign:25 -v tc.meta.kill:40 #-}

open import Common.Equality
open import Common.Product

postulate
  F : Set → Set
  A : Set

test : let H : Set
           H = _
           M : ((Set → Set) → Set) → Set
           M = _
       in {Z : Set} → H   ≡ F (M (\ G → A → G Z))
                     × F H ≡ F (F (A → A))
                     × M   ≡ \ K → K (\ _ → A)
test = refl
     , refl
     , refl

#1 : {A : Set} →
     let H : Set
         H = _
         M : (Set → Set) → Set → Set
         M = _
     in {Z : Set} → H ≡ F (M (\ _ → A) Z)
                   × M ≡ (\ F X → F X)
#1 = refl , refl

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Type.Size where

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

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

_≍_ : (A : Type{ℓ₁}) → ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ → (B : Type{ℓ₂}) → ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → Stmt
A ≍ B = ∃{Obj = A → B}(Bijective)

_≼_ : (A : Type{ℓ₁}) → ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ → (B : Type{ℓ₂}) → ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → Stmt
A ≼ B = ∃{Obj = A → B}(Injective)

_≽_ : (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → Stmt
A ≽ B = ∃{Obj = A → B}(Surjective)

_≭_ : (A : Type{ℓ₁}) → ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ → (B : Type{ℓ₂}) → ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → Stmt
A ≭ B = ¬(A ≍ B)

_≺_ : (A : Type{ℓ₁}) → ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ → (B : Type{ℓ₂}) → ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → Stmt
A ≺ B = (A ≼ B) ∧ (A ≭ B)

_≻_ : (A : Type{ℓ₁}) → ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ → (B : Type{ℓ₂}) → ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ → Stmt
A ≻ B = (A ≽ B) ∧ (A ≭ B)


text:
------------------------------------------------------------------------
-- Definitional interpreters can model systems with unbounded space
------------------------------------------------------------------------

-- As a follow-up to the development in Bounded-space I asked Ancona,
-- Dagnino and Zucca for further examples of properties for which it
-- is not clear to them if definitional interpreters work well. They
-- asked for a semantics that returns the largest heap size used by
-- the program, or infinity if there is no bound on this size. They
-- also asked how one can prove that a program transformation does not
-- increase the maximum heap usage.

-- It is impossible to write an Agda program that computes the maximum
-- heap usage, but one can at least produce a potentially infinite
-- list containing all heap sizes encountered in the execution of a
-- program, and then reason about this list. This approach is taken
-- below.

module Unbounded-space where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Tactic.By.Propositional
open import Prelude.Size

open import Colist equality-with-J as Colist
open import Conat equality-with-J as Conat
  hiding (pred) renaming (_+_ to _⊕_)
open import Function-universe equality-with-J as F hiding (_∘_)
open import Nat equality-with-J as Nat using (_≤_; _≤↑_; pred)
open import Omniscience equality-with-J

open import Only-allocation
open import Upper-bounds

------------------------------------------------------------------------
-- Definitional interpreter

-- Modifies the heap size according to the given instruction.

modify : Stmt → ℕ → ℕ
modify alloc   = suc
modify dealloc = pred

-- A definitional interpreter. It returns a trace of all heap sizes
-- encountered during the program's run. The input is the initial heap
-- size.

mutual

  ⟦_⟧ : ∀ {i} → Program i → ℕ → Colist ℕ i
  ⟦ p ⟧ h = h ∷ ⟦ p ⟧′ h

  ⟦_⟧′ : ∀ {i} → Program i → ℕ → Colist′ ℕ i
  ⟦ []    ⟧′ h .force = []
  ⟦ s ∷ p ⟧′ h .force = ⟦ p .force ⟧ (modify s h)

------------------------------------------------------------------------
-- The maximum heap usage predicate

-- The smallest heap size that is required to run the given program
-- when the initial heap is empty.

Heap-usage : Program ∞ → Conat ∞ → Type
Heap-usage p n = LUB (⟦ p ⟧ 0) n

-- The smallest extra heap size that is required to run the given
-- program, for arbitrary initial heaps.

Heap-usage′ : Program ∞ → Conat ∞ → Type
Heap-usage′ p n =
  (∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝)
    ×
  (∀ n′ → (∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n′ ⊕ ⌜ h ⌝) → [ ∞ ] n ≤ n′)

-- The number n is an upper bound of the heap size required for a
-- program when it is started with an empty heap iff, for any initial
-- heap h, n plus the size of h is an upper bound.
--
-- Note that this kind of property might not hold for a more
-- complicated programming language, in which a program's actions
-- could depend on the contents of the initial heap.

∀⟦⟧⊑⇔⟦⟧⊑ :
  ∀ {p n i} →
  [ i ] ⟦ p ⟧ 0 ⊑ n ⇔ (∀ h → [ i ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝)
∀⟦⟧⊑⇔⟦⟧⊑ {p} {n} {i} = record
  { to   = to p
  ; from = (∀ h → [ i ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝)  ↝⟨ _$ 0 ⟩
           [ i ] ⟦ p ⟧ 0 ⊑ n ⊕ ⌜ 0 ⌝          ↝⟨ flip transitive-⊑≤ (∼→≤ (+-right-identity _)) ⟩□
           [ i ] ⟦ p ⟧ 0 ⊑ n                  □
  }
  where
  +⊕-cong :
    ∀ {m₁ m₂ n i} → [ i ] ⌜ m₁ ⌝ ≤ m₂ → [ i ] ⌜ m₁ + n ⌝ ≤ m₂ ⊕ ⌜ n ⌝
  +⊕-cong {m₁} {m₂} {n} {i} =
    [ i ] ⌜ m₁ ⌝ ≤ m₂                  ↝⟨ _+-mono reflexive-≤ _ ⟩
    [ i ] ⌜ m₁ ⌝ ⊕ ⌜ n ⌝ ≤ m₂ ⊕ ⌜ n ⌝  ↝⟨ transitive-≤ (∼→≤ (⌜⌝-+ m₁)) ⟩□
    [ i ] ⌜ m₁ + n ⌝ ≤ m₂ ⊕ ⌜ n ⌝      □

  to : ∀ {m i} p →
       [ i ] ⟦ p ⟧ m ⊑ n → ∀ h → [ i ] ⟦ p ⟧ (m + h) ⊑ n ⊕ ⌜ h ⌝
  to []      (m≤n ∷ _)  _ = +⊕-cong m≤n ∷ λ { .force → [] }
  to (s ∷ p) (m≤n ∷ p⊑) h = +⊕-cong m≤n ∷ λ { .force →
                              to′ _ s (force p⊑) }
    where
    to′ : ∀ {i} m s →
          [ i ] ⟦ force p ⟧ (modify s m)       ⊑ n →
          [ i ] ⟦ force p ⟧ (modify s (m + h)) ⊑ n ⊕ ⌜ h ⌝
    to′ _       alloc   p⊑ = to (force p) p⊑ h
    to′ (suc m) dealloc p⊑ = to (force p) p⊑ h
    to′ zero    dealloc p⊑ = transitive-⊑≤ (to (force p) p⊑ (pred h))
                                           (reflexive-≤ n
                                              +-mono
                                            ⌜⌝-mono (Nat.pred≤ _))

-- Heap-usage p n holds iff Heap-usage′ p n holds. For this reason the
-- former, less complicated definition will be used below.

Heap-usage⇔Heap-usage′ :
  ∀ p n → Heap-usage p n ⇔ Heap-usage′ p n
Heap-usage⇔Heap-usage′ p n =
  ([ ∞ ] ⟦ p ⟧ 0 ⊑ n                  ↝⟨ ∀⟦⟧⊑⇔⟦⟧⊑ ⟩□
   (∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝)  □)

    ×-cong

  ((∀ n′ → [ ∞ ] ⟦ p ⟧ 0 ⊑ n′ → [ ∞ ] n ≤ n′)                  ↝⟨ ∀-cong _ (λ _ → →-cong _ ∀⟦⟧⊑⇔⟦⟧⊑ F.id) ⟩□
   (∀ n′ → (∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n′ ⊕ ⌜ h ⌝) → [ ∞ ] n ≤ n′)  □)

-- The maximum heap usage is unique (up to bisimilarity).

max-unique :
  ∀ {p m n i} →
  Heap-usage p m → Heap-usage p n → Conat.[ i ] m ∼ n
max-unique = lub-unique

-- Heap-usage p respects bisimilarity.

max-respects-∼ :
  ∀ {p q m n} →
  Colist.[ ∞ ] ⟦ p ⟧ 0 ∼ ⟦ q ⟧ 0 →
  Conat.[ ∞ ] m ∼ n →
  Heap-usage p m → Heap-usage q n
max-respects-∼ {p} {q} {m} {n} p∼q m∼n = Σ-map

  ([ ∞ ] ⟦ p ⟧ 0 ⊑ m  ↝⟨ (λ hyp → transitive-⊑≤ (□-∼ p∼q hyp) (∼→≤ m∼n)) ⟩□
   [ ∞ ] ⟦ q ⟧ 0 ⊑ n  □)

  ((∀ o → [ ∞ ] ⟦ p ⟧ 0 ⊑ o → [ ∞ ] m ≤ o)  ↝⟨ (λ hyp₁ o hyp₂ → transitive-≤ (∼→≤ (Conat.symmetric-∼ m∼n))
                                                                             (hyp₁ o (□-∼ (Colist.symmetric-∼ p∼q) hyp₂))) ⟩□
   (∀ o → [ ∞ ] ⟦ q ⟧ 0 ⊑ o → [ ∞ ] n ≤ o)  □)

-- If the semantics of a program started in the empty heap does not
-- have a finite upper bound, then the maximum heap usage of the
-- program is infinity.

no-finite-max→infinite-max :
  ∀ p → (∀ n → ¬ [ ∞ ] ⟦ p ⟧ 0 ⊑ ⌜ n ⌝) → Heap-usage p infinity
no-finite-max→infinite-max p hyp =
    (⟦ p ⟧ 0 ⊑infinity)
  , λ n′ →
      [ ∞ ] ⟦ p ⟧ 0 ⊑ n′         ↝⟨ no-finite→infinite hyp ⟩
      Conat.[ ∞ ] n′ ∼ infinity  ↝⟨ ∼→≤ ∘ Conat.symmetric-∼ ⟩□
      [ ∞ ] infinity ≤ n′        □

-- If the maximum heap usage could always be determined (in a certain
-- sense), then WLPO (which is a constructive taboo) would hold.

max→wlpo : (∀ p → ∃ λ n → Heap-usage p n) → WLPO
max→wlpo find-max = λ f → case find-max (p f) of λ where
    (zero  , max-0) → inj₁ (_⇔_.to 0⇔≡false max-0)
    (suc _ , max-+) → inj₂ (+→≢false max-+)
  where
  -- If f takes the value true, then p f contains exactly one
  -- occurrence of alloc, at the first index for which f takes the
  -- value true. Otherwise p f contains zero occurrences of alloc.

  p : ∀ {i} → (ℕ → Bool) → Program i
  p f = helper (f 0)
    module P where
    helper : ∀ {i} → Bool → Program i
    helper =
      if_then alloc   ∷′ []
         else dealloc ∷  λ { .force → p (λ n → f (1 + n)) }

  -- The maximum heap usage of p f is zero iff f always takes the
  -- value false.

  0⇔≡false :
    ∀ {f} → Heap-usage (p f) ⌜ 0 ⌝ ⇔ (∀ n → f n ≡ false)
  0⇔≡false = record
    { to   = →≡false _ ∘ proj₁
    ; from = λ ≡false →
          ≡false→ _ ≡false Nat.≤-refl
        , (λ _ _ → zero)
    }
    where
    →≡false : ∀ f → [ ∞ ] ⟦ p f ⟧ 0 ⊑ ⌜ 0 ⌝ → ∀ n → f n ≡ false
    →≡false f ⟦pf⟧0⊑0 _ = helper _ _ refl ⟦pf⟧0⊑0
      where
      helper : ∀ b n →
               f 0 ≡ b →
               [ ∞ ] ⟦ P.helper f b ⟧ 0 ⊑ ⌜ 0 ⌝ →
               f n ≡ false
      helper false zero    f0≡false = λ _ → f0≡false
      helper false (suc n) _        =
        [ ∞ ] ⟦ P.helper f false ⟧ 0 ⊑ ⌜ 0 ⌝  ↝⟨ □-tail ⟩
        [ ∞ ] ⟦ p (f ∘ suc)      ⟧ 0 ⊑ ⌜ 0 ⌝  ↝⟨ (λ hyp → →≡false (f ∘ suc) hyp n) ⟩□
        (f ∘ suc) n ≡ false                   □
      helper true n _ =
        [ ∞ ] ⟦ P.helper f true ⟧ 0 ⊑ ⌜ 0 ⌝  ↝⟨ □-head ∘ □-tail ⟩
        ([ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝)                ↝⟨ ⌜⌝-mono⁻¹ ⟩
        1 ≤ 0                                ↝⟨ Nat.+≮ 0 ⟩
        ⊥                                    ↝⟨ ⊥-elim ⟩□
        f n ≡ false                          □

    ≡false→ :
      ∀ {m n i} f →
      (∀ n → f n ≡ false) →
      m ≤ n → [ i ] ⟦ p f ⟧ m ⊑ ⌜ n ⌝
    ≡false→ {m} {n} f ≡false m≤n with f 0 | ≡false 0
    ... | true  | ()
    ... | false | _  =
      zero +-mono ⌜⌝-mono m≤n ∷ λ { .force →
      ≡false→ (f ∘ suc) (≡false ∘ suc) (
        pred m  Nat.≤⟨ Nat.pred≤ _ ⟩
        m       Nat.≤⟨ m≤n ⟩∎
        n       ∎≤) }

  -- If the maximum heap usage of p f is positive, then f does not
  -- always take the value false.

  +→≢false :
    ∀ {f n} → Heap-usage (p f) (suc n) → ¬ (∀ n → f n ≡ false)
  +→≢false {f} {n} =
    Heap-usage (p f) (suc n)     ↝⟨ (λ max-+ →

      Heap-usage (p f) ⌜ 0 ⌝           ↝⟨ max-unique max-+ ⟩
      Conat.[ ∞ ] suc n ∼ ⌜ 0 ⌝        ↝⟨ (λ ()) ⟩□
      ⊥                                □) ⟩

    ¬ Heap-usage (p f) ⌜ 0 ⌝     ↝⟨ (λ hyp ≡false → hyp (_⇔_.from 0⇔≡false ≡false)) ⟩□
    ¬ (∀ n → f n ≡ false)        □

-- In fact, WLPO is logically equivalent to a certain formulation of
-- "the maximum heap usage can always be determined".

wlpo⇔max : WLPO ⇔ (∀ p → ∃ λ n → Heap-usage p n)
wlpo⇔max = record
  { to   = λ wlpo p → wlpo→lub wlpo (⟦ p ⟧ 0)
  ; from = max→wlpo
  }

-- We also get that WLPO is logically equivalent to a certain
-- formulation of "least upper bounds of colists of natural numbers
-- can always be determined".

wlpo⇔lub : WLPO ⇔ (∀ ms → ∃ λ n → LUB ms n)
wlpo⇔lub = record
  { to   = wlpo→lub
  ; from = λ find-lub → max→wlpo (λ p → find-lub (⟦ p ⟧ 0))
  }

------------------------------------------------------------------------
-- Some examples

-- When this semantics is used all three programs are non-terminating,
-- in the sense that their traces are infinitely long.

bounded-loops :
  ∀ {i n} → Conat.[ i ] length (⟦ bounded ⟧ n) ∼ infinity
bounded-loops =
  suc λ { .force →
  suc λ { .force →
  bounded-loops }}

bounded₂-loops :
  ∀ {i n} → Conat.[ i ] length (⟦ bounded₂ ⟧ n) ∼ infinity
bounded₂-loops =
  suc λ { .force →
  suc λ { .force →
  suc λ { .force →
  suc λ { .force →
  bounded₂-loops }}}}

unbounded-loops :
  ∀ {i n} → Conat.[ i ] length (⟦ unbounded ⟧ n) ∼ infinity
unbounded-loops =
  suc λ { .force →
  unbounded-loops }

-- Zero is not an upper bound of the semantics of bounded when it is
-- started with an empty heap.

⟦bounded⟧⋢0 : ¬ [ ∞ ] ⟦ bounded ⟧ 0 ⊑ ⌜ 0 ⌝
⟦bounded⟧⋢0 =
  [ ∞ ] ⟦ bounded ⟧ 0 ⊑ ⌜ 0 ⌝  ↝⟨ □-head ∘ □-tail ⟩
  [ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝          ↝⟨ ⌜⌝-mono⁻¹ ⟩
  (1 ≤ 0)                      ↝⟨ Nat.+≮ 0 ⟩□
  ⊥                            □

-- However, one is.

⟦bounded⟧⊑1 :
  ∀ {i} → [ i ] ⟦ bounded ⟧ 0 ⊑ ⌜ 1 ⌝
⟦bounded⟧⊑1 =
  ≤suc          ∷ λ { .force →
  reflexive-≤ _ ∷ λ { .force →
  ⟦bounded⟧⊑1 }}

-- The maximum heap usage of bounded is 1.

max-bounded-1 : Heap-usage bounded ⌜ 1 ⌝
max-bounded-1 =
    ⟦bounded⟧⊑1
  , λ n′ →
      [ ∞ ] ⟦ bounded ⟧ 0 ⊑ n′  ↝⟨ □-head ∘ □-tail ⟩□
      [ ∞ ] ⌜ 1 ⌝ ≤ n′          □

-- Two is an upper bound of the semantics of bounded₂ when it is
-- started in an empty heap.

⟦bounded₂⟧⊑2 :
  ∀ {i} → [ i ] ⟦ bounded₂ ⟧ 0 ⊑ ⌜ 2 ⌝
⟦bounded₂⟧⊑2 =
  zero                      ∷ λ { .force →
  suc (λ { .force → zero }) ∷ λ { .force →
  reflexive-≤ _             ∷ λ { .force →
  suc (λ { .force → zero }) ∷ λ { .force →
  ⟦bounded₂⟧⊑2 }}}}

-- The maximum heap usage of bounded₂ is 2.

max-bounded₂-2 : Heap-usage bounded₂ ⌜ 2 ⌝
max-bounded₂-2 =
    ⟦bounded₂⟧⊑2
  , λ n′ →
    [ ∞ ] ⟦ bounded₂ ⟧ 0 ⊑ n′  ↝⟨ □-head ∘ □-tail ∘ □-tail ⟩□
    [ ∞ ] ⌜ 2 ⌝ ≤ n′           □

-- There is no finite upper bound of the semantics of unbounded.

⟦unbounded⟧⋢⌜⌝ :
  ∀ {n} → ¬ [ ∞ ] ⟦ unbounded ⟧ 0 ⊑ ⌜ n ⌝
⟦unbounded⟧⋢⌜⌝ {n} = helper (Nat.≤→≤↑ (Nat.zero≤ _))
  where
  helper :
    ∀ {h} → h ≤↑ 1 + n → ¬ [ ∞ ] ⟦ unbounded ⟧ h ⊑ ⌜ n ⌝
  helper (Nat.≤↑-refl refl) =
    [ ∞ ] ⟦ unbounded ⟧ (1 + n) ⊑ ⌜ n ⌝  ↝⟨ □-head ⟩
    [ ∞ ] ⌜ 1 + n ⌝ ≤ ⌜ n ⌝              ↝⟨ ⌜⌝-mono⁻¹ ⟩
    (1 + n ≤ n)                          ↝⟨ Nat.+≮ 0 ⟩□
    ⊥                                    □
  helper {h} (Nat.≤↑-step 1+h≤1+n) =
    [ ∞ ] ⟦ unbounded ⟧ h ⊑ ⌜ n ⌝        ↝⟨ □-tail ⟩
    [ ∞ ] ⟦ unbounded ⟧ (1 + h) ⊑ ⌜ n ⌝  ↝⟨ helper 1+h≤1+n ⟩□
    ⊥                                    □

-- The maximum heap usage of unbounded is infinity.

max-unbounded-∞ : Heap-usage unbounded infinity
max-unbounded-∞ =
  no-finite-max→infinite-max unbounded λ _ → ⟦unbounded⟧⋢⌜⌝

------------------------------------------------------------------------
-- A simple optimiser

-- An optimiser that replaces subsequences of the form "alloc, alloc,
-- dealloc" with "alloc".

opt : ∀ {i} → Program ∞ → Program i
opt     []            = []
opt     (dealloc ∷ p) = dealloc ∷ λ { .force → opt (p .force) }
opt {i} (alloc   ∷ p) = opt₁ (p .force)
  module Opt where
  default : Program i
  default = alloc ∷ λ { .force → opt (p .force) }

  opt₂ : Program ∞ → Program i
  opt₂ (dealloc ∷ p″) = alloc ∷ λ { .force → opt (p″ .force) }
  opt₂ _              = default

  opt₁ : Program ∞ → Program i
  opt₁ (alloc ∷ p′) = opt₂ (p′ .force)
  opt₁ _            = default

-- The semantics of opt bounded₂ matches that of bounded.

opt-bounded₂∼bounded :
  ∀ {i n} →
  Colist.[ i ] ⟦ opt bounded₂ ⟧ n ∼ ⟦ bounded ⟧ n
opt-bounded₂∼bounded =
  refl ∷ λ { .force →
  refl ∷ λ { .force →
  opt-bounded₂∼bounded }}

-- Sometimes the optimised program's maximum heap usage is less than
-- that of the original program.

opt-improves :
  ∃ λ p → Heap-usage p ⌜ 2 ⌝ × Heap-usage (opt p) ⌜ 1 ⌝
opt-improves =
    bounded₂
  , max-bounded₂-2
  , max-respects-∼
      (Colist.symmetric-∼ opt-bounded₂∼bounded)
      (_ ∎∼)
      max-bounded-1

-- The optimised program's maximum heap usage is at most as large as
-- that of the original program (assuming that these maximums exist).

mutual

  opt-correct :
    ∀ {i m n} p →
    Heap-usage (opt p) m → Heap-usage p n → [ i ] m ≤ n
  opt-correct p max₁ max₂ =
    _⇔_.to (≲⇔least-upper-bounds-≤ max₁ max₂) (opt-correct-≲ p)

  opt-correct-≲ : ∀ {h i} p → [ i ] ⟦ opt p ⟧ h ≲ ⟦ p ⟧ h
  opt-correct-≲ {h} [] =
    ⟦ opt [] ⟧ h  ∼⟨ ∷∼∷′ ⟩≲
    h ∷′ []       ∼⟨ Colist.symmetric-∼ ∷∼∷′ ⟩□≲
    ⟦ [] ⟧ h

  opt-correct-≲ {h} (dealloc ∷ p) =
    ⟦ opt (dealloc ∷ p) ⟧ h           ∼⟨ ∷∼∷′ ⟩≲
    h ∷′ ⟦ opt (p .force) ⟧ (pred h)  ≲⟨ (cons′-≲ λ { hyp .force → opt-correct-≲ (p .force) hyp }) ⟩
    h ∷′ ⟦ p .force ⟧ (pred h)        ∼⟨ Colist.symmetric-∼ ∷∼∷′ ⟩□≲
    ⟦ dealloc ∷ p ⟧ h

  opt-correct-≲ {h} (alloc ∷ p) =
    ⟦ opt (alloc ∷ p) ⟧ h        ≡⟨⟩≲
    ⟦ Opt.opt₁ p (p .force) ⟧ h  ≲⟨ opt-correct₁ _ refl ⟩
    h ∷′ ⟦ p .force ⟧ (1 + h)    ∼⟨ Colist.symmetric-∼ ∷∼∷′ ⟩□≲
    ⟦ alloc ∷ p ⟧ h
    where
    default-correct :
      ∀ {p′ i} →
      p′ ≡ p .force →
      [ i ] ⟦ Opt.default p ⟧ h ≲ h ∷′ ⟦ p′ ⟧ (1 + h)
    default-correct refl =
      ⟦ Opt.default p ⟧ h              ∼⟨ ∷∼∷′ ⟩≲
      h ∷′ ⟦ opt (p .force) ⟧ (1 + h)  ≲⟨ (cons′-≲ λ { hyp .force → opt-correct-≲ (p .force) hyp }) ⟩□
      h ∷′ ⟦ p .force ⟧ (1 + h)

    opt-correct₁ :
      ∀ {i} p′ →
      p′ ≡ p .force →
      [ i ] ⟦ Opt.opt₁ p p′ ⟧ h ≲ h ∷′ ⟦ p′ ⟧ (1 + h)
    opt-correct₁ []             []≡ = default-correct []≡
    opt-correct₁ (dealloc ∷ p′) d∷≡ = default-correct d∷≡
    opt-correct₁ (alloc   ∷ p′) a∷≡ =
      ⟦ Opt.opt₂ p (p′ .force) ⟧ h         ≲⟨ opt-correct₂ (p′ .force) refl ⟩
      h ∷′ 1 + h ∷′ ⟦ p′ .force ⟧ (2 + h)  ∼⟨ (refl ∷ λ { .force → Colist.symmetric-∼ ∷∼∷′ }) ⟩□≲
      h ∷′ ⟦ alloc ∷ p′ ⟧ (1 + h)
      where
      default-correct′ :
        ∀ {i p″} →
        p″ ≡ p′ .force →
        [ i ] ⟦ Opt.default p ⟧ h ≲ h ∷′ 1 + h ∷′ ⟦ p″ ⟧ (2 + h)
      default-correct′ refl =
        ⟦ Opt.default p ⟧ h                  ≲⟨ default-correct refl ⟩
        h ∷′ ⟦ p .force ⟧ (1 + h)            ≡⟨ by a∷≡ ⟩≲
        h ∷′ ⟦ alloc ∷ p′ ⟧ (1 + h)          ∼⟨ (refl ∷ λ { .force → ∷∼∷′ }) ⟩□≲
        h ∷′ 1 + h ∷′ ⟦ p′ .force ⟧ (2 + h)

      opt-correct₂ :
        ∀ {i} p″ →
        p″ ≡ p′ .force →
        [ i ] ⟦ Opt.opt₂ p p″ ⟧ h ≲ h ∷′ 1 + h ∷′ ⟦ p″ ⟧ (2 + h)
      opt-correct₂ []             []≡ = default-correct′ []≡
      opt-correct₂ (alloc   ∷ p″) a∷≡ = default-correct′ a∷≡
      opt-correct₂ (dealloc ∷ p″) _   =
        ⟦ Opt.opt₂ p (dealloc ∷ p″) ⟧ h               ∼⟨ ∷∼∷′ ⟩≲
        h ∷′ ⟦ opt (p″ .force) ⟧ (1 + h)              ≲⟨ (cons′-≲ λ { hyp .force → opt-correct-≲ (p″ .force) hyp }) ⟩
        h ∷′ ⟦ p″ .force ⟧ (1 + h)                    ≲⟨ (cons′-≲ λ { hyp .force → consʳ-≲ (consʳ-≲ (_ □≲)) hyp }) ⟩
        h ∷′ 1 + h ∷′ 2 + h ∷′ ⟦ p″ .force ⟧ (1 + h)  ∼⟨ (refl ∷ λ { .force → refl ∷ λ { .force → Colist.symmetric-∼ ∷∼∷′ } }) ⟩□≲
        h ∷′ 1 + h ∷′ ⟦ dealloc ∷ p″ ⟧ (2 + h)

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


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

open import HoTT
open import homotopy.SuspSectionDecomp
open import homotopy.CofiberComp

module homotopy.SuspProduct where

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

  private
    i₁ : fst (X ⊙→ X ⊙× Y)
    i₁ = ((λ x → (x , snd Y)) , idp)

    i₂ : fst (Y ⊙→ X ⊙× Y)
    i₂ = ((λ y → (snd X , y)) , idp)

    j₂ : fst (⊙Cof i₁) → fst Y
    j₂ = CofiberRec.f (snd Y) snd (λ x → idp)

  ⊙path : ⊙Susp (X ⊙× Y) == ⊙Susp X ⊙∨ (⊙Susp Y ⊙∨ ⊙Susp (X ⊙∧ Y))
  ⊙path =
    ⊙ua (⊙≃-in (SuspSectionDecomp.eq i₁ fst (λ x → idp))
                 (! $ ap winl $ merid (snd X)))
    ∙ ap (λ Z → ⊙Susp X ⊙∨ Z)
         (⊙ua (⊙≃-in (SuspSectionDecomp.eq (⊙cfcod' i₁ ⊙∘ i₂) j₂ (λ y → idp))
                       (! $ ap winl $ merid (snd Y))))
    ∙ ap (λ Z → ⊙Susp X ⊙∨ (⊙Susp Y ⊙∨ ⊙Susp Z))
         (CofiberComp.⊙path i₁ i₂)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Unary using ( _∈_ ; _∉_ ; ∅ ; U ; _∪_ ; _∩_ ; ∁ )
open import Web.Semantic.DL.Concept using ( Concept ; ⟨_⟩ ; ¬⟨_⟩ ; ⊤ ; ⊥ ; _⊓_ ; _⊔_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1 ; >1 ; neg )
open import Web.Semantic.DL.Role.Model using ( _⟦_⟧₂ ; ⟦⟧₂-resp-≈ ; ⟦⟧₂-resp-≲ ; ⟦⟧₂-galois )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using ( Interp ; Δ ; _⊨_≈_ ; _⊨_≉_ ; con ; con-≈ ; ≈-refl ; ≈-sym ; ≈-trans )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( _≲_ ; _≃_ ; ≲-resp-con ; ≲-resp-≈ ; ≃-impl-≲ ; ≃-impl-≳ ; ≃-iso ; ≃-iso⁻¹ ; ≃-image ; ≃-image⁻¹ ; ≃-refl-≈ ; ≃-sym )
open import Web.Semantic.Util using ( Subset ; tt ; _∘_ ; ExclMiddle ; elim )

module Web.Semantic.DL.Concept.Model {Σ : Signature} where

_⟦_⟧₁ : ∀ (I : Interp Σ) → Concept Σ → Subset (Δ I)
I ⟦ ⟨ c ⟩    ⟧₁ = con I c
I ⟦ ¬⟨ c ⟩   ⟧₁ = ∁ (con I c)
I ⟦ ⊤        ⟧₁ = U
I ⟦ ⊥        ⟧₁ = ∅
I ⟦ C ⊓ D    ⟧₁ = I ⟦ C ⟧₁ ∩ I ⟦ D ⟧₁
I ⟦ C ⊔ D    ⟧₁ = I ⟦ C ⟧₁ ∪ I ⟦ D ⟧₁
I ⟦ ∀[ R ] C ⟧₁ = λ x → ∀   y → ((x , y) ∈ I ⟦ R ⟧₂) → (y ∈ I ⟦ C ⟧₁)
I ⟦ ∃⟨ R ⟩ C ⟧₁ = λ x → ∃ λ y → ((x , y) ∈ I ⟦ R ⟧₂) × (y ∈ I ⟦ C ⟧₁)
I ⟦ ≤1 R     ⟧₁ = λ x → ∀ y z → ((x , y) ∈ I ⟦ R ⟧₂) → ((x , z) ∈ I ⟦ R ⟧₂) → (I ⊨ y ≈ z)
I ⟦ >1 R     ⟧₁ = λ x → ∃ λ y → ∃ λ z → ((x , y) ∈ I ⟦ R ⟧₂) × ((x , z) ∈ I ⟦ R ⟧₂) × (I ⊨ y ≉ z)

⟦⟧₁-resp-≈ : ∀ I C {x y} → (x ∈ I ⟦ C ⟧₁) → (I ⊨ x ≈ y) → (y ∈ I ⟦ C ⟧₁)
⟦⟧₁-resp-≈ I ⟨ c ⟩      x∈⟦c⟧                           x≈y =
  con-≈ I c x∈⟦c⟧ x≈y
⟦⟧₁-resp-≈ I ¬⟨ c ⟩     x∉⟦c⟧                           x≈y =
  λ y∈⟦c⟧ → x∉⟦c⟧ (con-≈ I c y∈⟦c⟧ (≈-sym I x≈y))
⟦⟧₁-resp-≈ I ⊤          x∈⊤                             x≈y =
  tt
⟦⟧₁-resp-≈ I (C ⊓ D)    (x∈⟦C⟧ , x∈⟦D⟧)                 x≈y =
  (⟦⟧₁-resp-≈ I C x∈⟦C⟧ x≈y , ⟦⟧₁-resp-≈ I D x∈⟦D⟧ x≈y)
⟦⟧₁-resp-≈ I (C ⊔ D)    (inj₁ x∈⟦C⟧)                    x≈y =
  inj₁ (⟦⟧₁-resp-≈ I C x∈⟦C⟧ x≈y)
⟦⟧₁-resp-≈ I (C ⊔ D)    (inj₂ x∈⟦D⟧)                    x≈y =
  inj₂ (⟦⟧₁-resp-≈ I D x∈⟦D⟧ x≈y)
⟦⟧₁-resp-≈ I (∀[ R ] C) x∈⟦∀RC⟧                         x≈y =
  λ z yz∈⟦R⟧ → x∈⟦∀RC⟧ z (⟦⟧₂-resp-≈ I R x≈y yz∈⟦R⟧ (≈-refl I))
⟦⟧₁-resp-≈ I (∃⟨ R ⟩ C) (z , xz∈⟦R⟧ , z∈⟦C⟧)            x≈y =
  (z , ⟦⟧₂-resp-≈ I R (≈-sym I x≈y) xz∈⟦R⟧ (≈-refl I) , z∈⟦C⟧)
⟦⟧₁-resp-≈ I (≤1 R)     x∈⟦≤1R⟧                         x≈y =
  λ w z yw∈⟦R⟧ yz∈⟦R⟧ → x∈⟦≤1R⟧ w z
    (⟦⟧₂-resp-≈ I R x≈y yw∈⟦R⟧ (≈-refl I))
    (⟦⟧₂-resp-≈ I R x≈y yz∈⟦R⟧ (≈-refl I))
⟦⟧₁-resp-≈ I (>1 R)     (w , z , xw∈⟦R⟧ , xz∈⟦R⟧ , w≉z) x≈y =
  ( w , z
  , ⟦⟧₂-resp-≈ I R (≈-sym I x≈y) xw∈⟦R⟧ (≈-refl I)
  , ⟦⟧₂-resp-≈ I R (≈-sym I x≈y) xz∈⟦R⟧ (≈-refl I)
  , w≉z)
⟦⟧₁-resp-≈ I ⊥          ()                              x≈y

mutual

  ⟦⟧₁-refl-≃ : ∀ {I J : Interp Σ} → (I≃J : I ≃ J) → ∀ {x} C → (≃-image⁻¹ I≃J x ∈ I ⟦ C ⟧₁) → (x ∈ J ⟦ C ⟧₁)
  ⟦⟧₁-refl-≃ {I} {J} I≃J {x} C x∈⟦C⟧ = ⟦⟧₁-resp-≈ J C (⟦⟧₁-resp-≃ I≃J C x∈⟦C⟧) (≃-iso⁻¹ I≃J x)

  ⟦⟧₁-resp-≃ : ∀ {I J : Interp Σ} → (I≃J : I ≃ J) → ∀ {x} C → (x ∈ I ⟦ C ⟧₁) → (≃-image I≃J x ∈ J ⟦ C ⟧₁)
  ⟦⟧₁-resp-≃ {I} {J} I≃J ⟨ c ⟩ x∈⟦c⟧ =
    ≲-resp-con (≃-impl-≲ I≃J) x∈⟦c⟧
  ⟦⟧₁-resp-≃ {I} {J} I≃J {x} ¬⟨ c ⟩ x∉⟦c⟧ =
    λ x∈⟦c⟧ → x∉⟦c⟧ (con-≈ I c (≲-resp-con (≃-impl-≳ I≃J) x∈⟦c⟧) (≃-iso I≃J x))
  ⟦⟧₁-resp-≃ {I} {J} I≃J ⊤ _ =
    tt
  ⟦⟧₁-resp-≃ {I} {J} I≃J ⊥ ()
  ⟦⟧₁-resp-≃ {I} {J} I≃J (C ⊓ D) (x∈⟦C⟧ , x∈⟦D⟧) =
    (⟦⟧₁-resp-≃ I≃J C x∈⟦C⟧ , ⟦⟧₁-resp-≃ I≃J D x∈⟦D⟧)
  ⟦⟧₁-resp-≃ {I} {J} I≃J (C ⊔ D) (inj₁ x∈⟦C⟧) =
    inj₁ (⟦⟧₁-resp-≃ I≃J C x∈⟦C⟧)
  ⟦⟧₁-resp-≃ {I} {J} I≃J (C ⊔ D) (inj₂ x∈⟦D⟧) =
    inj₂ (⟦⟧₁-resp-≃ I≃J D x∈⟦D⟧)
  ⟦⟧₁-resp-≃ {I} {J} I≃J (∀[ R ] C) x∈⟦∀RC⟧ =
    λ y xy∈⟦R⟧ → ⟦⟧₁-refl-≃ I≃J C
      (x∈⟦∀RC⟧ (≃-image⁻¹ I≃J y) (⟦⟧₂-galois (≃-sym I≃J) R xy∈⟦R⟧))
  ⟦⟧₁-resp-≃ {I} {J} I≃J (∃⟨ R ⟩ C) (y , xy∈⟦R⟧ , y∈⟦C⟧) =
    ( ≃-image I≃J y
    , ⟦⟧₂-resp-≲ (≃-impl-≲ I≃J) R xy∈⟦R⟧
    , ⟦⟧₁-resp-≃ I≃J C y∈⟦C⟧ )
  ⟦⟧₁-resp-≃ {I} {J} I≃J (≤1 R) x∈⟦≤1R⟧ =
    λ y z xy∈⟦R⟧ xz∈⟦R⟧ → ≃-refl-≈ I≃J
      (x∈⟦≤1R⟧ (≃-image⁻¹ I≃J y) (≃-image⁻¹ I≃J z)
      (⟦⟧₂-galois (≃-sym I≃J) R xy∈⟦R⟧) (⟦⟧₂-galois (≃-sym I≃J) R xz∈⟦R⟧))
  ⟦⟧₁-resp-≃ {I} {J} I≃J (>1 R) (y , z , xy∈⟦R⟧ , xz∈⟦R⟧ , y≉z) =
    ( ≃-image I≃J y , ≃-image I≃J z
    , ⟦⟧₂-resp-≲ (≃-impl-≲ I≃J) R xy∈⟦R⟧
    , ⟦⟧₂-resp-≲ (≃-impl-≲ I≃J) R xz∈⟦R⟧
    , y≉z ∘ ≃-refl-≈ (≃-sym I≃J) )

neg-sound : ∀ I {x} C → (x ∈ I ⟦ neg C ⟧₁) → (x ∉ I ⟦ C ⟧₁)
neg-sound I ⟨ c ⟩ x∉⟦c⟧ x∈⟦c⟧ = x∉⟦c⟧ x∈⟦c⟧
neg-sound I ¬⟨ c ⟩ x∈⟦c⟧ x∉⟦c⟧ = x∉⟦c⟧ x∈⟦c⟧
neg-sound I ⊤ () _
neg-sound I ⊥ _ ()
neg-sound I (C ⊓ D) (inj₁ x∈⟦¬C⟧) (x∈⟦C⟧ , x∈⟦D⟧) = neg-sound I C x∈⟦¬C⟧ x∈⟦C⟧
neg-sound I (C ⊓ D) (inj₂ x∈⟦¬D⟧) (x∈⟦C⟧ , x∈⟦D⟧) = neg-sound I D x∈⟦¬D⟧ x∈⟦D⟧
neg-sound I (C ⊔ D) (x∈⟦¬C⟧ , x∈⟦¬D⟧) (inj₁ x∈⟦C⟧) = neg-sound I C x∈⟦¬C⟧ x∈⟦C⟧
neg-sound I (C ⊔ D) (x∈⟦¬C⟧ , x∈⟦¬D⟧) (inj₂ x∈⟦D⟧) = neg-sound I D x∈⟦¬D⟧ x∈⟦D⟧
neg-sound I (∀[ R ] C) (y , xy∈⟦R⟧ , y∈⟦¬C⟧) x∈⟦∀RC⟧ = neg-sound I C y∈⟦¬C⟧ (x∈⟦∀RC⟧ y xy∈⟦R⟧)
neg-sound I (∃⟨ R ⟩ C) x∈⟦∀R¬C⟧ (y , xy∈⟦R⟧ , y∈⟦C⟧) = neg-sound I C (x∈⟦∀R¬C⟧ y xy∈⟦R⟧) y∈⟦C⟧
neg-sound I (≤1 R) (y , z , xy∈⟦R⟧ , xz∈⟦R⟧ , y≉z) x∈⟦≤1R⟧ = y≉z (x∈⟦≤1R⟧ y z xy∈⟦R⟧ xz∈⟦R⟧)
neg-sound I (>1 R) x∈⟦≤1R⟧ (y , z , xy∈⟦R⟧ , xz∈⟦R⟧ , y≉z) = y≉z (x∈⟦≤1R⟧ y z xy∈⟦R⟧ xz∈⟦R⟧)

neg-complete : ExclMiddle → ∀ I {x} C → (x ∉ I ⟦ C ⟧₁) → (x ∈ I ⟦ neg C ⟧₁)
neg-complete excl-middle I ⟨ c ⟩ x∉⟦c⟧ = x∉⟦c⟧
neg-complete excl-middle I {x} ¬⟨ c ⟩ ¬x∉⟦c⟧ with excl-middle (x ∈ con I c)
neg-complete excl-middle I ¬⟨ c ⟩ ¬x∉⟦c⟧ | yes x∈⟦c⟧ = x∈⟦c⟧
neg-complete excl-middle I ¬⟨ c ⟩ ¬x∉⟦c⟧ | no  x∉⟦c⟧ = elim (¬x∉⟦c⟧ x∉⟦c⟧)
neg-complete excl-middle I ⊤ x∉⟦⊤⟧ = x∉⟦⊤⟧ tt
neg-complete excl-middle I ⊥ x∉⟦⊥⟧ = tt
neg-complete excl-middle I {x} (C ⊓ D) x∉⟦C⊓D⟧ with excl-middle (x ∈ I ⟦ C ⟧₁)
neg-complete excl-middle I (C ⊓ D) x∉⟦C⊓D⟧ | yes x∈⟦C⟧ =
  inj₂ (neg-complete excl-middle I D (λ x∈⟦D⟧ → x∉⟦C⊓D⟧ (x∈⟦C⟧ , x∈⟦D⟧)))
neg-complete excl-middle I (C ⊓ D) x∉⟦C⊓D⟧ | no x∉⟦C⟧ =
  inj₁ (neg-complete excl-middle I C x∉⟦C⟧)
neg-complete excl-middle I (C ⊔ D) x∉⟦C⊔D⟧ =
  ( neg-complete excl-middle I C (x∉⟦C⊔D⟧ ∘ inj₁)
  , neg-complete excl-middle I D (x∉⟦C⊔D⟧ ∘ inj₂))
neg-complete excl-middle I {x} (∀[ R ] C) x∉⟦∀RC⟧
  with excl-middle (∃ λ y → ((x , y) ∈ I ⟦ R ⟧₂) × (y ∉ I ⟦ C ⟧₁))
neg-complete excl-middle I {x} (∀[ R ] C) x∉⟦∀RC⟧ | yes (y , xy∈⟦R⟧ , y∉⟦C⟧) =
  (y , xy∈⟦R⟧ , neg-complete excl-middle I C y∉⟦C⟧)
neg-complete excl-middle I {x} (∀[ R ] C) x∉⟦∀RC⟧ | no ∄xy∈⟦R⟧∙y∉⟦C⟧ =
  elim (x∉⟦∀RC⟧ lemma) where
  lemma : x ∈ I ⟦ ∀[ R ] C ⟧₁
  lemma y xy∈⟦R⟧ with excl-middle (y ∈ I ⟦ C ⟧₁)
  lemma y xy∈⟦R⟧ | yes y∈⟦C⟧ = y∈⟦C⟧
  lemma y xy∈⟦R⟧ | no  y∉⟦C⟧ = elim (∄xy∈⟦R⟧∙y∉⟦C⟧ (y , xy∈⟦R⟧ , y∉⟦C⟧))
neg-complete excl-middle I (∃⟨ R ⟩ C) x∉⟦∃RC⟧ =
  λ y xy∈⟦R⟧ → neg-complete excl-middle I C
    (λ y∈⟦C⟧ → x∉⟦∃RC⟧ (y , xy∈⟦R⟧ , y∈⟦C⟧))
neg-complete excl-middle I {x} (≤1 R) x∉⟦≤1R⟧ = lemma where
  lemma : x ∈ I ⟦ >1 R ⟧₁
  lemma with excl-middle (x ∈ I ⟦ >1 R ⟧₁)
  lemma | yes x∈⟦>1R⟧ = x∈⟦>1R⟧
  lemma | no x∉⟦>1R⟧ = elim (x∉⟦≤1R⟧ lemma′) where
    lemma′ : x ∈ I ⟦ ≤1 R ⟧₁
    lemma′ y z xy∈⟦R⟧ xz∈⟦R⟧ with excl-middle (I ⊨ y ≈ z)
    lemma′ y z xy∈⟦R⟧ xz∈⟦R⟧ | yes y≈z = y≈z
    lemma′ y z xy∈⟦R⟧ xz∈⟦R⟧ | no y≉z =
      elim (x∉⟦>1R⟧ (y , z , xy∈⟦R⟧ , xz∈⟦R⟧ , y≉z))
neg-complete excl-middle I {x} (>1 R) x∉⟦>1R⟧ = lemma where
  lemma : x ∈ I ⟦ ≤1 R ⟧₁
  lemma y z xy∈⟦R⟧ xz∈⟦R⟧ with excl-middle (I ⊨ y ≈ z)
  lemma y z xy∈⟦R⟧ xz∈⟦R⟧ | yes y≈z = y≈z
  lemma y z xy∈⟦R⟧ xz∈⟦R⟧ | no y≉z =
    elim (x∉⟦>1R⟧ (y , z , xy∈⟦R⟧ , xz∈⟦R⟧ , y≉z))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
{-# OPTIONS --universe-polymorphism --no-irrelevant-projections --without-K #-}
module SafeFlagSafePragmas where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module *-assoc where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)

open import *-distrib-+ using (*-distrib-+)

-- 積の結合律 (associativity)
*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p =
  begin
    (zero * n) * p
  ≡⟨⟩
    zero * p
  ≡⟨⟩
    zero
  ≡⟨⟩
    zero * (n * p)
  ∎
*-assoc (suc m) n p =
  begin
    ((suc m) * n) * p
  ≡⟨⟩
    (n + m * n) * p
  ≡⟨ *-distrib-+ n (m * n) p ⟩
    (n * p) + m * n * p
  ≡⟨ cong ((n * p) +_) (*-assoc m n p) ⟩
    (n * p) + m * (n * p)
  ≡⟨⟩
    (suc m) * (n * p)
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
open import Agda.Primitive using (Level; lsuc)

variable
  ℓ p   : Level
  A B   : Set ℓ
  x y z : A

postulate
  easy : A

record R a : Set (lsuc a) where
  field
    _≡_ : {A : Set a} → A → A → Set a

module _ (r : ∀ ℓ → R ℓ) where

  open module R′ {ℓ} = R (r ℓ)

  postulate
    refl      : (x : A) → x ≡ x
    cong      : (f : A → B) → x ≡ y → f x ≡ f y
    subst     : (P : A → Set p) → x ≡ y → P x → P y
    trans     : x ≡ y → y ≡ z → x ≡ z
    elim      : (P : {x y : A} → x ≡ y → Set p) →
                (∀ x → P (refl x)) →
                (x≡y : x ≡ y) → P x≡y
    elim-refl : (P : {x y : A} → x ≡ y → Set p)
                (r : ∀ x → P (refl x)) →
                elim P r (refl x) ≡ r x

  [subst≡]≡[trans≡trans] :
    {p : x ≡ y} {q : x ≡ x} {r : y ≡ y} →
    (subst (λ z → z ≡ z) p q ≡ r)
      ≡
    (trans q p ≡ trans p r)
  [subst≡]≡[trans≡trans] {p = p} {q} {r} = elim
    (λ {x y} p → {q : x ≡ x} {r : y ≡ y} →
                 (subst (λ z → z ≡ z) p q ≡ r)
                   ≡
                 (trans q p ≡ trans p r))
    (λ _ → easy)
    p

  [subst≡]≡[trans≡trans]-refl :
    {q r : x ≡ x} →
    [subst≡]≡[trans≡trans] {p = refl x} {q = q} {r = r} ≡
    easy
  [subst≡]≡[trans≡trans]-refl {q = q} {r = r} =
    cong (λ f → f {q = q} {r = r})
      (elim-refl (λ {x y} _ → {q : x ≡ x} {r : y ≡ y} → _) _)


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-notationZ where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.FinData

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.CommRing.Instances.Int

open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
     renaming (PolyCommRing to A[X1,···,Xn] ; Poly to A[x1,···,xn])
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient

-- Notations for ℤ polynomial rings

ℤ[X] : CommRing ℓ-zero
ℤ[X] = A[X1,···,Xn] ℤCommRing 1

ℤ[x] : Type ℓ-zero
ℤ[x] = fst ℤ[X]

ℤ[X,Y] : CommRing ℓ-zero
ℤ[X,Y] = A[X1,···,Xn] ℤCommRing 2

ℤ[x,y] : Type ℓ-zero
ℤ[x,y] = fst ℤ[X,Y]

ℤ[X,Y,Z] : CommRing ℓ-zero
ℤ[X,Y,Z] = A[X1,···,Xn] ℤCommRing 3

ℤ[x,y,z] : Type ℓ-zero
ℤ[x,y,z] = fst ℤ[X,Y,Z]

ℤ[X1,···,Xn] : (n : ℕ) → CommRing ℓ-zero
ℤ[X1,···,Xn] n = A[X1,···,Xn] ℤCommRing n

ℤ[x1,···,xn] : (n : ℕ) → Type ℓ-zero
ℤ[x1,···,xn] n = fst (ℤ[X1,···,Xn] n)

-- Notation for quotiented ℤ polynomial ring

<X> : FinVec ℤ[x] 1
<X> = <Xkʲ> ℤCommRing 1 0 1

<X²> : FinVec ℤ[x] 1
<X²> = <Xkʲ> ℤCommRing 1 0 2

<X³> : FinVec ℤ[x] 1
<X³> = <Xkʲ> ℤCommRing 1 0 3

<Xᵏ> : (k  : ℕ) → FinVec ℤ[x] 1
<Xᵏ> k = <Xkʲ> ℤCommRing 1 0 k

ℤ[X]/X : CommRing ℓ-zero
ℤ[X]/X = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 1

ℤ[x]/x : Type ℓ-zero
ℤ[x]/x = fst ℤ[X]/X

ℤ[X]/X² : CommRing ℓ-zero
ℤ[X]/X² = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 2

ℤ[x]/x² : Type ℓ-zero
ℤ[x]/x² = fst ℤ[X]/X²

ℤ[X]/X³ : CommRing ℓ-zero
ℤ[X]/X³ = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 3

ℤ[x]/x³ : Type ℓ-zero
ℤ[x]/x³ = fst ℤ[X]/X³

ℤ[X1,···,Xn]/<X1,···,Xn> : (n : ℕ) → CommRing ℓ-zero
ℤ[X1,···,Xn]/<X1,···,Xn> n = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing n

ℤ[x1,···,xn]/<x1,···,xn> : (n : ℕ) → Type ℓ-zero
ℤ[x1,···,xn]/<x1,···,xn> n = fst (ℤ[X1,···,Xn]/<X1,···,Xn> n)

-- Warning there is two possible definitions of ℤ[X]
-- they only holds up to a path

ℤ'[X]/X : CommRing ℓ-zero
ℤ'[X]/X = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing 1

-- there is a unification problem that keep pop in up everytime I modify something
-- equivℤ[X] : ℤ'[X]/X ≡ ℤ[X]/X
-- equivℤ[X] = cong₂ _/_ refl (cong (λ X → genIdeal (A[X1,···,Xn] ℤCommRing {!!}) X) {!!})

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

-- a categorical (i.e. non-skeletal) version of Lawvere Theory,
-- as per https://ncatlab.org/nlab/show/Lawvere+theory

module Categories.Theory.Lawvere where

open import Data.Nat using (ℕ)
open import Data.Product using (Σ; _,_)
open import Level

open import Categories.Category.Cartesian
open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Instance.Setoids
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
open import Categories.Category.Product
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Cartesian
open import Categories.Functor.Cartesian.Properties
import Categories.Morphism as Mor
open import Categories.NaturalTransformation using (NaturalTransformation)

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

record FiniteProduct (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    T : Category o ℓ e
  open Mor T
  field
    cart : Cartesian T
    generic : Category.Obj T
  open Cartesian cart using (power)
  field
    obj-iso-to-generic-power : (x : Category.Obj T) → Σ ℕ (λ n → x ≅ power generic n)

record LT-Hom (T₁ : FiniteProduct o ℓ e) (T₂ : FiniteProduct o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module T₁ = FiniteProduct T₁
    module T₂ = FiniteProduct T₂

  field
    F : Functor T₁.T T₂.T
    cartF : CartesianF T₁.cart T₂.cart F

LT-id : {A : FiniteProduct o ℓ e} → LT-Hom A A
LT-id = record { F = idF ; cartF = idF-Cartesian }

LT-∘ : {A : FiniteProduct o ℓ e} {B : FiniteProduct o′ ℓ′ e′} {C : FiniteProduct o″ ℓ″ e″} →
  LT-Hom B C → LT-Hom A B → LT-Hom A C
LT-∘ G H = record { F = F G ∘F F H ; cartF = ∘-Cartesian (cartF G) (cartF H) }
  where open LT-Hom

record T-Algebra (FP : FiniteProduct o ℓ e) : Set (o ⊔ ℓ ⊔ e ⊔ suc (ℓ′ ⊔ e′)) where
  private
    module FP = FiniteProduct FP
  field
    Mod : Functor FP.T (Setoids ℓ′ e′)
    Cart : CartesianF FP.cart Setoids-Cartesian Mod


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

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

open import LibraBFT.Impl.OBM.Rust.Duration as Duration
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import Util.Prelude

module LibraBFT.Impl.OBM.Time where

postulate -- TODO-1 : iPlus, timeT
  iPlus : Instant → Duration → Instant
  timeT : Instant


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Unit
open import Data.Nat as ℕ using (ℕ)
open import Data.Integer as ℤ using (ℤ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List
open import Relation.Binary.PropositionalEquality

module simple-quantifier-temp-output where

abstract
  bool : ∀ (x : ℤ) → ⊤
  bool = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  expandedExpr : ∀ (x : Tensor ℤ (2 ∷ [])) → x (# 0) ≡ x (# 1)
  expandedExpr = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  multiple : ∀ (x : ℕ) → ∀ (y : ℕ) → x ≡ y
  multiple = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Bool where

open import Cubical.Data.Bool.Base public

open import Cubical.Data.Bool.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Cubical.Categories.Limits.Limits where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

private
  variable
    ℓJ ℓJ' ℓC ℓC' : Level
    ℓ ℓ' ℓ'' : Level

module _ {J : Category ℓJ ℓJ'}
         {C : Category ℓC ℓC'} where
  open Category
  open Functor
  open NatTrans

  -- functor which sends all objects to c and all
  -- morphisms to the identity
  constF : (c : C .ob) → Functor J C
  constF c .F-ob _ = c
  constF c .F-hom _ = C .id
  constF c .F-id = refl
  constF c .F-seq _ _ = sym (C .⋆IdL _)

  -- a cone is a natural transformation from the constant functor at x to K
  Cone : (K : Functor J C) → C .ob → Type _
  Cone K x = NatTrans (constF x) K

  module _ {K : Functor J C} where

    -- precomposes a cone with a morphism
    _◼_ : ∀ {d c : C .ob}
        → (f : C [ d , c ])
        → Cone K c
        → Cone K d
    (f ◼ μ) .N-ob x = f ⋆⟨ C ⟩ μ ⟦ x ⟧
    (f ◼ μ) .N-hom {x = x} {y} k
      = C .id ⋆⟨ C ⟩ (f ⋆⟨ C ⟩ μ ⟦ y ⟧)
      ≡⟨ C .⋆IdL _ ⟩
        f ⋆⟨ C ⟩ μ ⟦ y ⟧
      ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) (sym (C .⋆IdL _)) ⟩
        f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ μ ⟦ y ⟧)
      ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) (μ .N-hom k) ⟩
        f ⋆⟨ C ⟩ (μ ⟦ x ⟧ ⋆⟨ C ⟩ K ⟪ k ⟫)
      ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
        f ⋆⟨ C ⟩ μ ⟦ x ⟧ ⋆⟨ C ⟩ K ⟪ k ⟫
      ∎

    -- μ factors ν if there's a morphism such that the natural transformation
    -- from precomposing it with ν gives you back μ
    _factors_ : {u v : C .ob} (μ : Cone K u) (ν : Cone K v) → Type _
    _factors_ {u} {v} μ ν = Σ[ mor ∈ C [ v , u ] ] ν ≡ (mor ◼ μ)

    -- μ uniquely factors ν if the factor from above is contractible
    _uniquelyFactors_ : {u v : C .ob} (μ : Cone K u) (ν : Cone K v) → Type _
    _uniquelyFactors_ {u} {v} μ ν = isContr (μ factors ν)

  module _ (K : Functor J C) where

    -- a Limit is a cone such that all cones are uniquely factored by it
    record isLimit (head : C .ob) : Type (ℓ-max (ℓ-max ℓJ ℓJ') (ℓ-max ℓC ℓC'))  where
      constructor islimit
      field
        cone : Cone K head
        -- TODO: change this to terminal object in category of Cones?
        up   : ∀ {v} (ν : Cone K v) → cone uniquelyFactors ν

    record Limit : Type (ℓ-max (ℓ-max ℓJ ℓJ') (ℓ-max ℓC ℓC'))  where
      field
        head : C .ob
        islim : isLimit head

-- a Category is complete if it has all limits
complete' : {ℓJ ℓJ' : Level} (C : Category ℓC ℓC') → Type _
complete' {ℓJ = ℓJ} {ℓJ'} C = (J : Category ℓJ ℓJ') (K : Functor J C) → Limit K

complete : (C : Category ℓC ℓC') → Typeω
complete C = ∀ {ℓJ ℓJ'} → complete' {ℓJ = ℓJ} {ℓJ'} C


text:
{-# OPTIONS --cubical --safe #-}

module Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Map where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Def
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Membership

private
  variable p : Level
  variable P : A → Type p

-- map-◇-fn : ∀ x → P x → ∀ y xs → (x ∈ xs → ◇ P xs) → (y ≡ x) ⊎ (x ∈ xs) → ◇ P (y ∷ xs)
-- map-◇-fn {P = P} x Px y xs k (inl y≡x) = ∣ inl (subst P (sym y≡x) Px) ∣
-- map-◇-fn x Px y xs k (inr x∈xs) = ∣ inr (k x∈xs) ∣

-- map-◇-prop : ∀ (x : A) {xs} → isProp (x ∈ xs → ◇ P xs)
-- map-◇-prop {P = P} x {xs} p q i x∈xs = ◇′ P xs .snd (p x∈xs) (q x∈xs) i

-- map-◇ : ∀ (x : A) → P x → (xs : 𝒦 A) → x ∈ xs → ◇ P xs
-- map-◇ {A = A} {P = P} x Px =
--   𝒦-elim-prop {A = A} {P = λ ys → x ∈ ys → ◇ P ys}
--     (map-◇-prop {A = A} {P = P} x)
--     (λ y xs Pxs → recPropTrunc squash (map-◇-fn x Px y xs Pxs))
--     (λ ())

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Prelude

module Implicits.Substitutions.Lemmas.Type where

open import Implicits.Syntax.Type
open import Implicits.Substitutions

open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec.Properties
open import Extensions.Substitution
open import Data.Star using (Star; ε; _◅_)
open import Data.Product hiding (map)

typeLemmas : TermLemmas Type
typeLemmas = record { termSubst = TypeSubst.typeSubst; app-var = refl ; /✶-↑✶ = Lemma./✶-↑✶ }
  where
    open TypeSubst
    module Lemma {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} where

      open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
      open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

      /✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                          (∀ k x → (simpl (tvar x)) /✶₁ σs₁ ↑✶₁ k ≡ (simpl (tvar x)) /✶₂ σs₂ ↑✶₂ k) →
                          ∀ k t → t /✶₁ σs₁ ↑✶₁ k ≡ t /✶₂ σs₂ ↑✶₂ k
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tvar x)) = hyp k x
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tc c)) = begin
          (simpl $ tc c) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.tc-/✶-↑✶ _ k ρs₁ ⟩
          (simpl $ tc c)
          ≡⟨ sym $ TypeApp.tc-/✶-↑✶ _ k ρs₂ ⟩
          (simpl $ tc c) /✶₂ ρs₂ ↑✶₂ k ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (a →' b)) = begin
          (simpl $ a →' b) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.→'-/✶-↑✶ _ k ρs₁ ⟩
          simpl ((a /✶₁ ρs₁ ↑✶₁ k) →' (b /✶₁ ρs₁ ↑✶₁ k))
          ≡⟨ cong₂ (λ a b → simpl (a →' b)) (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
          simpl ((a /✶₂ ρs₂ ↑✶₂ k) →' (b /✶₂ ρs₂ ↑✶₂ k))
          ≡⟨ sym (TypeApp.→'-/✶-↑✶ _ k ρs₂) ⟩
          (simpl $ a →' b) /✶₂ ρs₂ ↑✶₂ k
          ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (a ⇒ b) = begin
          (a ⇒ b) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.⇒-/✶-↑✶ _ k ρs₁ ⟩ --
          (a /✶₁ ρs₁ ↑✶₁ k) ⇒ (b /✶₁ ρs₁ ↑✶₁ k)
          ≡⟨ cong₂ _⇒_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
          (a /✶₂ ρs₂ ↑✶₂ k) ⇒ (b /✶₂ ρs₂ ↑✶₂ k)
          ≡⟨ sym (TypeApp.⇒-/✶-↑✶ _ k ρs₂) ⟩
          (a ⇒ b) /✶₂ ρs₂ ↑✶₂ k
          ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (∀' a) = begin
          (∀' a) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.∀'-/✶-↑✶ _ k ρs₁ ⟩
          ∀' (a /✶₁ ρs₁ ↑✶₁ (suc k))
          ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) a) ⟩
          ∀' (a /✶₂ ρs₂ ↑✶₂ (suc k))
          ≡⟨ sym (TypeApp.∀'-/✶-↑✶ _ k ρs₂) ⟩
          (∀' a) /✶₂ ρs₂ ↑✶₂ k
          ∎

open TermLemmas typeLemmas public hiding (var; id)
open AdditionalLemmas typeLemmas public
open TypeSubst using (module Lifted)

-- The above lemma /✶-↑✶ specialized to single substitutions
/-↑⋆ : ∀ {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} →
    let open Lifted lift₁ using () renaming (_↑⋆_ to _↑⋆₁_; _/_ to _/₁_)
        open Lifted lift₂ using () renaming (_↑⋆_ to _↑⋆₂_; _/_ to _/₂_)
    in
    ∀ {n k} (ρ₁ : Sub T₁ n k) (ρ₂ : Sub T₂ n k) →
    (∀ i x → (simpl (tvar x)) /₁ ρ₁ ↑⋆₁ i ≡ (simpl (tvar x)) /₂ ρ₂ ↑⋆₂ i) →
        ∀ i a → a /₁ ρ₁ ↑⋆₁ i ≡ a /₂ ρ₂ ↑⋆₂ i
/-↑⋆ ρ₁ ρ₂ hyp i a = /✶-↑✶ (ρ₁ ◅ ε) (ρ₂ ◅ ε) hyp i a

-- weakening a simple type gives a simple type
simpl-wk : ∀ {ν} k (τ : SimpleType (k + ν)) → ∃ λ τ' → (simpl τ) / wk ↑⋆ k ≡ simpl τ'
simpl-wk k (tc x) = , refl
simpl-wk k (tvar n) = , var-/-wk-↑⋆ k n
simpl-wk k (x →' x₁) = , refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive lists
------------------------------------------------------------------------

{-# OPTIONS --without-K --sized-types --guardedness #-}

module Codata.Musical.Colist where

open import Category.Monad
open import Codata.Musical.Notation
open import Codata.Musical.Conat using (Coℕ; zero; suc)
open import Data.Bool.Base using (Bool; true; false)
open import Data.BoundedVec.Inefficient as BVec
  using (BoundedVec; []; _∷_)
open import Data.Empty using (⊥)
open import Data.Maybe using (Maybe; nothing; just; Is-just)
open import Data.Maybe.Relation.Unary.Any using (just)
open import Data.Nat.Base using (ℕ; zero; suc; _≥′_; ≤′-refl; ≤′-step)
open import Data.Nat.Properties using (s≤′s)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
open import Data.Product as Prod using (∃; _×_; _,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
open import Level using (_⊔_)
open import Relation.Binary
import Relation.Binary.Construct.FromRel as Ind
import Relation.Binary.Reasoning.Preorder as PreR
import Relation.Binary.Reasoning.PartialOrder as POR
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Negation

module ¬¬Monad {p} where
  open RawMonad (¬¬-Monad {p}) public
open ¬¬Monad  -- we don't want the RawMonad content to be opened publicly

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

data Colist {a} (A : Set a) : Set a where
  []  : Colist A
  _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

{-# FOREIGN GHC
  data AgdaColist a    = Nil | Cons a (MAlonzo.RTE.Inf (AgdaColist a))
  type AgdaColist' l a = AgdaColist a
  #-}
{-# COMPILE GHC Colist = data AgdaColist' (Nil | Cons) #-}
{-# COMPILE UHC Colist = data __LIST__ (__NIL__ | __CONS__) #-}

module Colist-injective {a} {A : Set a} where

 ∷-injectiveˡ : ∀ {x y : A} {xs ys} → (Colist A ∋ x ∷ xs) ≡ y ∷ ys → x ≡ y
 ∷-injectiveˡ P.refl = P.refl

 ∷-injectiveʳ : ∀ {x y : A} {xs ys} → (Colist A ∋ x ∷ xs) ≡ y ∷ ys → xs ≡ ys
 ∷-injectiveʳ P.refl = P.refl

data Any {a p} {A : Set a} (P : A → Set p) :
         Colist A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)          → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P (♭ xs)) → Any P (x ∷ xs)

module _  {a p} {A : Set a} {P : A → Set p} where

 here-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ here p) ≡ here q → p ≡ q
 here-injective P.refl = P.refl

 there-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ there p) ≡ there q → p ≡ q
 there-injective P.refl = P.refl

data All {a p} {A : Set a} (P : A → Set p) :
         Colist A → Set (a ⊔ p) where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)

module All-injective {a p} {A : Set a} {P : A → Set p} where

 ∷-injectiveˡ : ∀ {x xs} {px qx pxs qxs} →
                (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → px ≡ qx
 ∷-injectiveˡ P.refl = P.refl

 ∷-injectiveʳ : ∀ {x xs} {px qx pxs qxs} →
                (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → pxs ≡ qxs
 ∷-injectiveʳ P.refl = P.refl

------------------------------------------------------------------------
-- Some operations

null : ∀ {a} {A : Set a} → Colist A → Bool
null []      = true
null (_ ∷ _) = false

length : ∀ {a} {A : Set a} → Colist A → Coℕ
length []       = zero
length (x ∷ xs) = suc (♯ length (♭ xs))

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Colist A → Colist B
map f []       = []
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

fromList : ∀ {a} {A : Set a} → List A → Colist A
fromList []       = []
fromList (x ∷ xs) = x ∷ ♯ fromList xs

take : ∀ {a} {A : Set a} (n : ℕ) → Colist A → BoundedVec A n
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

replicate : ∀ {a} {A : Set a} → Coℕ → A → Colist A
replicate zero    x = []
replicate (suc n) x = x ∷ ♯ replicate (♭ n) x

lookup : ∀ {a} {A : Set a} → ℕ → Colist A → Maybe A
lookup n       []       = nothing
lookup zero    (x ∷ xs) = just x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

infixr 5 _++_

_++_ : ∀ {a} {A : Set a} → Colist A → Colist A → Colist A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

-- Interleaves the two colists (until the shorter one, if any, has
-- been exhausted).

infixr 5 _⋎_

_⋎_ : ∀ {a} {A : Set a} → Colist A → Colist A → Colist A
[]       ⋎ ys = ys
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)

concat : ∀ {a} {A : Set a} → Colist (List⁺ A) → Colist A
concat []                     = []
concat ((x ∷ [])       ∷ xss) = x ∷ ♯ concat (♭ xss)
concat ((x ∷ (y ∷ xs)) ∷ xss) = x ∷ ♯ concat ((y ∷ xs) ∷ xss)

[_] : ∀ {a} {A : Set a} → A → Colist A
[ x ] = x ∷ ♯ []

------------------------------------------------------------------------
-- Any lemmas

-- Any lemma for map.

Any-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
          {f : A → B} {xs} →
          Any P (map f xs) ↔ Any (P ∘ f) xs
Any-map {P = P} {f} {xs} = inverse to from from∘to to∘from
  where
  to : ∀ {xs} → Any P (map f xs) → Any (P ∘ f) xs
  to {[]}     ()
  to {x ∷ xs} (here px) = here px
  to {x ∷ xs} (there p) = there (to p)

  from : ∀ {xs} → Any (P ∘ f) xs → Any P (map f xs)
  from (here px) = here px
  from (there p) = there (from p)

  from∘to : ∀ {xs} (p : Any P (map f xs)) → from (to p) ≡ p
  from∘to {[]}     ()
  from∘to {x ∷ xs} (here px) = P.refl
  from∘to {x ∷ xs} (there p) = P.cong there (from∘to p)

  to∘from : ∀ {xs} (p : Any (P ∘ f) xs) → to (from p) ≡ p
  to∘from (here px) = P.refl
  to∘from (there p) = P.cong there (to∘from p)

-- Any lemma for _⋎_. This lemma implies that every member of xs or ys
-- is a member of xs ⋎ ys, and vice versa.

Any-⋎ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
        Any P (xs ⋎ ys) ↔ (Any P xs ⊎ Any P ys)
Any-⋎ {P = P} = λ xs → record
  { to         = P.→-to-⟶ (to xs)
  ; from       = P.→-to-⟶ (from xs)
  ; inverse-of = record
    { left-inverse-of  = from∘to xs
    ; right-inverse-of = to∘from xs
    }
  }
  where
  to : ∀ xs {ys} → Any P (xs ⋎ ys) → Any P xs ⊎ Any P ys
  to []       p         = inj₂ p
  to (x ∷ xs) (here px) = inj₁ (here px)
  to (x ∷ xs) (there p) = [ inj₂ , inj₁ ∘ there ]′ (to _ p)

  mutual

    from-left : ∀ {xs ys} → Any P xs → Any P (xs ⋎ ys)
    from-left           (here px) = here px
    from-left {ys = ys} (there p) = there (from-right ys p)

    from-right : ∀ xs {ys} → Any P ys → Any P (xs ⋎ ys)
    from-right []       p = p
    from-right (x ∷ xs) p = there (from-left p)

  from : ∀ xs {ys} → Any P xs ⊎ Any P ys → Any P (xs ⋎ ys)
  from xs = Sum.[ from-left , from-right xs ]

  from∘to : ∀ xs {ys} (p : Any P (xs ⋎ ys)) → from xs (to xs p) ≡ p
  from∘to []                 p                          = P.refl
  from∘to (x ∷ xs)           (here px)                  = P.refl
  from∘to (x ∷ xs) {ys = ys} (there p)                  with to ys p | from∘to ys p
  from∘to (x ∷ xs) {ys = ys} (there .(from-left q))     | inj₁ q | P.refl = P.refl
  from∘to (x ∷ xs) {ys = ys} (there .(from-right ys q)) | inj₂ q | P.refl = P.refl

  mutual

    to∘from-left : ∀ {xs ys} (p : Any P xs) →
                   to xs {ys = ys} (from-left p) ≡ inj₁ p
    to∘from-left           (here px) = P.refl
    to∘from-left {ys = ys} (there p)
      rewrite to∘from-right ys p = P.refl

    to∘from-right : ∀ xs {ys} (p : Any P ys) →
                    to xs (from-right xs p) ≡ inj₂ p
    to∘from-right []                 p = P.refl
    to∘from-right (x ∷ xs) {ys = ys} p
      rewrite to∘from-left {xs = ys} {ys = ♭ xs} p = P.refl

  to∘from : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) → to xs (from xs p) ≡ p
  to∘from xs = Sum.[ to∘from-left , to∘from-right xs ]

------------------------------------------------------------------------
-- Equality

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {a} {A : Set a} : (xs ys : Colist A) → Set a where
  []  :                                       []     ≈ []
  _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys

-- The equality relation forms a setoid.

setoid : ∀ {ℓ} → Set ℓ → Setoid _ _
setoid A = record
  { Carrier       = Colist A
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {[]}     = []
  refl {x ∷ xs} = x ∷ ♯ refl

  sym : Symmetric _≈_
  sym []        = []
  sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)

  trans : Transitive _≈_
  trans []        []         = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

module ≈-Reasoning where
  import Relation.Binary.Reasoning.Setoid as EqR
  private
    open module R {a} {A : Set a} = EqR (setoid A) public

-- map preserves equality.

map-cong : ∀ {a b} {A : Set a} {B : Set b}
           (f : A → B) → _≈_ =[ map f ]⇒ _≈_
map-cong f []        = []
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)

-- Any respects pointwise implication (for the predicate) and equality
-- (for the colist).

Any-resp : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
           {xs ys} → (∀ {x} → P x → Q x) → xs ≈ ys →
           Any P xs → Any Q ys
Any-resp f (x ∷ xs≈) (here px) = here (f px)
Any-resp f (x ∷ xs≈) (there p) = there (Any-resp f (♭ xs≈) p)

-- Any maps pointwise isomorphic predicates and equal colists to
-- isomorphic types.

Any-cong : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
           {xs ys} → P ↔̇ Q → xs ≈ ys → Any P xs ↔ Any Q ys
Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q = λ xs≈ys → record
  { to         = P.→-to-⟶ (to xs≈ys)
  ; from       = P.→-to-⟶ (from xs≈ys)
  ; inverse-of = record
    { left-inverse-of  = from∘to _
    ; right-inverse-of = to∘from _
    }
  }
  where
  open Setoid (setoid _) using (sym)

  to : ∀ {xs ys} → xs ≈ ys → Any P xs → Any Q ys
  to xs≈ys = Any-resp (Inverse.to P↔Q ⟨$⟩_) xs≈ys

  from : ∀ {xs ys} → xs ≈ ys → Any Q ys → Any P xs
  from xs≈ys = Any-resp (Inverse.from P↔Q ⟨$⟩_) (sym xs≈ys)

  to∘from : ∀ {xs ys} (xs≈ys : xs ≈ ys) (q : Any Q ys) →
            to xs≈ys (from xs≈ys q) ≡ q
  to∘from (x ∷ xs≈) (there q) = P.cong there (to∘from (♭ xs≈) q)
  to∘from (x ∷ xs≈) (here qx) =
    P.cong here (Inverse.right-inverse-of P↔Q qx)

  from∘to : ∀ {xs ys} (xs≈ys : xs ≈ ys) (p : Any P xs) →
            from xs≈ys (to xs≈ys p) ≡ p
  from∘to (x ∷ xs≈) (there p) = P.cong there (from∘to (♭ xs≈) p)
  from∘to (x ∷ xs≈) (here px) =
    P.cong here (Inverse.left-inverse-of P↔Q px)

------------------------------------------------------------------------
-- Indices

-- Converts Any proofs to indices into the colist. The index can also
-- be seen as the size of the proof.

index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → Any P xs → ℕ
index (here px) = zero
index (there p) = suc (index p)

-- The position returned by index is guaranteed to be within bounds.

lookup-index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} (p : Any P xs) →
               Is-just (lookup (index p) xs)
lookup-index (here px) = just _
lookup-index (there p) = lookup-index p

-- Any-resp preserves the index.

index-Any-resp :
  ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
    {f : ∀ {x} → P x → Q x} {xs ys}
  (xs≈ys : xs ≈ ys) (p : Any P xs) →
  index (Any-resp f xs≈ys p) ≡ index p
index-Any-resp (x ∷ xs≈) (here px) = P.refl
index-Any-resp (x ∷ xs≈) (there p) =
  P.cong suc (index-Any-resp (♭ xs≈) p)

-- The left-to-right direction of Any-⋎ returns a proof whose size is
-- no larger than that of the input proof.

index-Any-⋎ :
  ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} (p : Any P (xs ⋎ ys)) →
  index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎ xs) ⟨$⟩ p)
index-Any-⋎ []                 p         = ≤′-refl
index-Any-⋎ (x ∷ xs)           (here px) = ≤′-refl
index-Any-⋎ (x ∷ xs) {ys = ys} (there p)
  with Inverse.to (Any-⋎ ys) ⟨$⟩ p | index-Any-⋎ ys p
... | inj₁ q | q≤p = ≤′-step q≤p
... | inj₂ q | q≤p = s≤′s    q≤p

------------------------------------------------------------------------
-- Memberships, subsets, prefixes

-- x ∈ xs means that x is a member of xs.

infix 4 _∈_

_∈_ : ∀ {a} → {A : Set a} → A → Colist A → Set a
x ∈ xs = Any (_≡_ x) xs

-- xs ⊆ ys means that xs is a subset of ys.

infix 4 _⊆_

_⊆_ : ∀ {a} → {A : Set a} → Colist A → Colist A → Set a
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

-- xs ⊑ ys means that xs is a prefix of ys.

infix 4 _⊑_

data _⊑_ {a} {A : Set a} : Colist A → Colist A → Set a where
  []  : ∀ {ys}                            → []     ⊑ ys
  _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys

-- Any can be expressed using _∈_ (and vice versa).

Any-∈ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
        Any P xs ↔ ∃ λ x → x ∈ xs × P x
Any-∈ {P = P} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ (λ { (x , x∈xs , p) → from x∈xs p })
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = λ { (x , x∈xs , p) → to∘from x∈xs p }
    }
  }
  where
  to : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
  to (here  p) = _ , here P.refl , p
  to (there p) = Prod.map id (Prod.map there id) (to p)

  from : ∀ {x xs} → x ∈ xs → P x → Any P xs
  from (here P.refl) p = here p
  from (there x∈xs)  p = there (from x∈xs p)

  to∘from : ∀ {x xs} (x∈xs : x ∈ xs) (p : P x) →
            to (from x∈xs p) ≡ (x , x∈xs , p)
  to∘from (here P.refl) p = P.refl
  to∘from (there x∈xs)  p =
    P.cong (Prod.map id (Prod.map there id)) (to∘from x∈xs p)

  from∘to : ∀ {xs} (p : Any P xs) →
            let (x , x∈xs , px) = to p in from x∈xs px ≡ p
  from∘to (here _)  = P.refl
  from∘to (there p) = P.cong there (from∘to p)

-- Prefixes are subsets.

⊑⇒⊆ : ∀ {a} → {A : Set a} → _⊑_ {A = A} ⇒ _⊆_
⊑⇒⊆ []          ()
⊑⇒⊆ (x ∷ xs⊑ys) (here ≡x)    = here ≡x
⊑⇒⊆ (_ ∷ xs⊑ys) (there x∈xs) = there (⊑⇒⊆ (♭ xs⊑ys) x∈xs)

-- The prefix relation forms a poset.

⊑-Poset : ∀ {ℓ} → Set ℓ → Poset _ _ _
⊑-Poset A = record
  { Carrier        = Colist A
  ; _≈_            = _≈_
  ; _≤_            = _⊑_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Setoid.isEquivalence (setoid A)
      ; reflexive     = reflexive
      ; trans         = trans
      }
    ; antisym  = antisym
    }
  }
  where
  reflexive : _≈_ ⇒ _⊑_
  reflexive []        = []
  reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈)

  trans : Transitive _⊑_
  trans []        _          = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

  tail : ∀ {x xs y ys} → x ∷ xs ⊑ y ∷ ys → ♭ xs ⊑ ♭ ys
  tail (_ ∷ p) = ♭ p

  antisym : Antisymmetric _≈_ _⊑_
  antisym []       [] = []
  antisym (x ∷ p₁) p₂ = x ∷ ♯ antisym (♭ p₁) (tail p₂)

module ⊑-Reasoning where
  private
    open module R {a} {A : Set a} = POR (⊑-Poset A)
      public renaming (_≤⟨_⟩_ to _⊑⟨_⟩_)

-- The subset relation forms a preorder.

⊆-Preorder : ∀ {ℓ} → Set ℓ → Preorder _ _ _
⊆-Preorder A = Ind.preorder (setoid A) _∈_
                 (λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys))
  where module ⊑P = Poset (⊑-Poset A)

module ⊆-Reasoning where
  private
    open module R {a} {A : Set a} = PreR (⊆-Preorder A)
      public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

  infix 1 _∈⟨_⟩_

  _∈⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {xs ys} →
           x ∈ xs → xs IsRelatedTo ys → x ∈ ys
  x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

-- take returns a prefix.

take-⊑ : ∀ {a} {A : Set a} n (xs : Colist A) →
         let toColist = fromList {a} ∘ BVec.toList in
         toColist (take n xs) ⊑ xs
take-⊑ zero    xs       = []
take-⊑ (suc n) []       = []
take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ n (♭ xs)

------------------------------------------------------------------------
-- Finiteness and infiniteness

-- Finite xs means that xs has finite length.

data Finite {a} {A : Set a} : Colist A → Set a where
  []  : Finite []
  _∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs)

module Finite-injective {a} {A : Set a} where

 ∷-injective : ∀ {x : A} {xs p q} → (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
 ∷-injective P.refl = P.refl

-- Infinite xs means that xs has infinite length.

data Infinite {a} {A : Set a} : Colist A → Set a where
  _∷_ : ∀ x {xs} (inf : ∞ (Infinite (♭ xs))) → Infinite (x ∷ xs)

module Infinite-injective {a} {A : Set a} where

 ∷-injective : ∀ {x : A} {xs p q} → (Infinite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
 ∷-injective P.refl = P.refl

-- Colists which are not finite are infinite.

not-finite-is-infinite :
  ∀ {a} {A : Set a} (xs : Colist A) → ¬ Finite xs → Infinite xs
not-finite-is-infinite []       hyp with hyp []
... | ()
not-finite-is-infinite (x ∷ xs) hyp =
  x ∷ ♯ not-finite-is-infinite (♭ xs) (hyp ∘ _∷_ x)

-- Colists are either finite or infinite (classically).

finite-or-infinite :
  ∀ {a} {A : Set a} (xs : Colist A) → ¬ ¬ (Finite xs ⊎ Infinite xs)
finite-or-infinite xs = helper <$> excluded-middle
  where
  helper : Dec (Finite xs) → Finite xs ⊎ Infinite xs
  helper (yes fin) = inj₁ fin
  helper (no ¬fin) = inj₂ $ not-finite-is-infinite xs ¬fin

-- Colists are not both finite and infinite.

not-finite-and-infinite :
  ∀ {a} {A : Set a} {xs : Colist A} → Finite xs → Infinite xs → ⊥
not-finite-and-infinite []        ()
not-finite-and-infinite (x ∷ fin) (.x ∷ inf) =
  not-finite-and-infinite fin (♭ inf)

------------------------------------------------------------------------
-- Legacy

import Codata.Colist as C
open import Codata.Thunk
import Size

module _ {a} {A : Set a} where

  fromMusical : ∀ {i} → Colist A → C.Colist A i
  fromMusical []       = C.[]
  fromMusical (x ∷ xs) = x C.∷ λ where .force → fromMusical (♭ xs)

  toMusical : C.Colist A Size.∞ → Colist A
  toMusical C.[]       = []
  toMusical (x C.∷ xs) = x ∷ ♯ toMusical (xs .force)


text:
data ⊥ : Set where

data Maybe : Set where
  just : ⊥ → Maybe
  nothing : Maybe

test : Set → Set
test x with nothing
test x | just ()
test x | nothing = test x