text:
open import Agda.Primitive using (_⊔_)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian

open import SingleSorted.Context

module SingleSorted.Power
       {o ℓ e}
       (𝒞 : Category.Category o ℓ e) where

  open Category.Category 𝒞
  open HomReasoning

  record Powered (A : Obj) : Set (o ⊔ ℓ ⊔ e) where

    field
      pow : Context → Obj
      π : ∀ {Γ} → var Γ → pow Γ ⇒ A
      tuple : ∀ Γ {B} → (var Γ → B ⇒ A) → B ⇒ pow Γ
      project : ∀ {Γ} {B} {x : var Γ} {fs : var Γ → B ⇒ A} → π x ∘ tuple Γ fs ≈ fs x
      unique : ∀ {Γ} {B} {fs : var Γ → B ⇒ A} {g : B ⇒ pow Γ} → (∀ i → π i ∘ g ≈ fs i) → tuple Γ fs ≈ g

    η : ∀ {Γ} → tuple Γ π ≈ id
    η = unique (λ i → identityʳ)

    ! : ∀ {B : Obj} → B ⇒ pow ctx-empty
    ! = tuple ctx-empty ctx-empty-absurd

    !-unique : ∀ {B : Obj} {f : B ⇒ pow ctx-empty} → ! ≈ f
    !-unique = unique λ i → ctx-empty-absurd i

    !-unique₂ : ∀ {B : Obj} {f g : B ⇒ pow ctx-empty} → f ≈ g
    !-unique₂ = (⟺ !-unique) ○ !-unique

    tuple-cong : ∀ {B : Obj} {Γ} {fs gs : var Γ → B ⇒ A} → (∀ i → fs i ≈ gs i) →
                 tuple Γ fs ≈ tuple Γ gs
    tuple-cong ξ = unique (λ i →  project ○ ⟺ (ξ i))

    ∘-distribʳ-tuple : ∀ {B C} {Γ} {fs : var Γ → B ⇒ A} {g : C ⇒ B}  →
                       tuple Γ (λ x → fs x ∘ g) ≈ tuple Γ fs ∘ g
    ∘-distribʳ-tuple = unique (λ i → ⟺ assoc ○ ∘-resp-≈ˡ project)

  -- A cartesian category has a standard power structure (which we need not use)
  module _ (cartesian-𝒞 : Cartesian.Cartesian 𝒞) (A : Obj) where
    open Cartesian.Cartesian cartesian-𝒞

    standard-pow : Context → Obj
    standard-pow ctx-empty = ⊤
    standard-pow ctx-slot = A
    standard-pow (ctx-concat Γ Δ) = standard-pow Γ × standard-pow Δ

    standard-π : ∀ {Γ} → var Γ → standard-pow Γ ⇒ A
    standard-π var-var = id
    standard-π (var-inl i) = standard-π i ∘ π₁
    standard-π (var-inr i) = standard-π i ∘ π₂

    standard-tuple : ∀ Γ {B} → (var Γ → B ⇒ A) → B ⇒ standard-pow Γ
    standard-tuple ctx-empty fs = !
    standard-tuple ctx-slot fs = fs var-var
    standard-tuple (ctx-concat Γ Δ) fs = ⟨ standard-tuple Γ (λ i → fs (var-inl i)) , standard-tuple Δ (λ j → fs (var-inr j)) ⟩

    standard-project : ∀ {Γ} {B} {x : var Γ} {fs : var Γ → B ⇒ A} →
                       standard-π x ∘ standard-tuple Γ fs ≈ fs x
    standard-project {x = var-var} = identityˡ
    standard-project {x = var-inl x} = assoc ○ ((∘-resp-≈ʳ project₁) ○ standard-project {x = x})
    standard-project {x = var-inr x} = assoc ○ ((∘-resp-≈ʳ project₂) ○ standard-project {x = x})

    standard-unique : ∀ {Γ} {B} {fs : var Γ → B ⇒ A} {g : B ⇒ standard-pow Γ} → (∀ i → standard-π i ∘ g ≈ fs i) →
                      standard-tuple Γ fs ≈ g
    standard-unique {ctx-empty} ξ = !-unique _
    standard-unique {ctx-slot} ξ = ⟺ (ξ var-var) ○ identityˡ
    standard-unique {ctx-concat Γ Δ} {fs = fs} ξ =
      unique
         (⟺ (standard-unique (λ x → sym-assoc ○ (ξ (var-inl x)))))
         (⟺ (standard-unique (λ y → sym-assoc ○ (ξ (var-inr y)))))

    StandardPowered : Powered A
    StandardPowered =
      record
      { pow = standard-pow
      ; π = standard-π
      ; tuple = standard-tuple
      ; project = λ {Γ} → standard-project {Γ}
      ; unique = standard-unique }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- {-# OPTIONS -v tc.conv.coerce:10 -v tc.conv.size:40 -v tc.size.solve:40 #-}
-- Andreas, 2014-06-16 Coercion for sizes
open import Common.Size

data Nat (i : Size) : Set where
  zero : Nat i
  suc  : (j : Size< i) → Nat j → Nat i

three : (i : Size) → Nat (↑ ↑ ↑ i)
three i = suc _ (suc _ (suc i zero))

-- Should be ok, but we get the error:
-- ∞ !=< i of type Size
-- when checking that the expression _ has type Size< (↑ (↑ (↑ i)))

-- Works now.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}
{-# OPTIONS --allow-unsolved-metas #-}

module Light.Implementation.Standard.Data.Product where

open import Light.Library.Data.Product using (Library ; Dependencies)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableEquality)
open import Light.Variable.Sets

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            open import Data.Product using (Σ) renaming (proj₁ to first ; proj₂ to second ; _,_ to both) public

            equals :
                  ∀ ⦃ a‐c‐equals : DecidableEquality 𝕒 𝕔 ⦄ ⦃ b‐d‐equals : DecidableEquality 𝕓 𝕕 ⦄
                  → DecidableEquality (Σ 𝕒 (λ _ → 𝕓)) (Σ 𝕔 (λ _ → 𝕕))
            equals = {!!}

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym2 where

open import Symmetric
open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import FLutil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin
open import Data.Fin.Permutation

sym2solvable : solvable (Symmetric 2)
solvable.dervied-length sym2solvable = 1
solvable.end sym2solvable x d = solved x d where

   open import Data.List using ( List ; [] ; _∷_ )

   open Solvable (Symmetric 2)
   -- open Group (Symmetric 2) using (_⁻¹)

   p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
   p0 = pleq _ _ refl

   p0r :  perm→FL pid ≡  ((# 0) :: ((# 0 ) :: f0))
   p0r = refl

   p1 :  FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid
   p1 = pleq _ _ refl

   p1r :  perm→FL (pswap pid) ≡  ((# 1) :: ((# 0 ) :: f0))
   p1r = refl

   -- FL→iso : (fl : FL 2 )  → perm→FL ( FL→perm fl ) ≡ fl
   -- FL→iso  (zero :: (zero :: f0)) = refl
   -- FL→iso ((suc zero) :: (zero :: f0)) = refl

   open _=p=_
   open ≡-Reasoning

   sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
   sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
   sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} | record { eq = h=00}  = begin
             [ g , h ]  ⟨$⟩ʳ q
           ≡⟨⟩
              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨ cong (λ k → h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ  k))) ((peqˡ sym2lem1 _ )) ⟩
              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
           ≡⟨ cong (λ k →  h ⟨$⟩ʳ k ) (peq sym2lem1 _ )  ⟩
              h ⟨$⟩ʳ  (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
           ≡⟨⟩
             [ pid , h ]  ⟨$⟩ʳ q
           ≡⟨ peq (idcomtl h) q ⟩
             q
           ∎ where
             sym2lem1 :  g =p= pid
             sym2lem1 = FL-inject  g=00
   sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00} = begin
             [ g , h ]  ⟨$⟩ʳ q
           ≡⟨⟩
              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨ peq sym2lem2 _   ⟩
              pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
              pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨⟩
             [ g , pid ]  ⟨$⟩ʳ q
           ≡⟨ peq (idcomtr g) q ⟩
             q
          ∎ where
             sym2lem2 :  h =p= pid
             sym2lem2 = FL-inject h=00
   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00}= begin
             [ g , h ]  ⟨$⟩ʳ q
           ≡⟨⟩
              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨ peq (psym g=h ) _  ⟩
              g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨ cong (λ k →   g ⟨$⟩ʳ  (g ⟨$⟩ʳ  k) ) (peqˡ (psym g=h) _)  ⟩
              g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
           ≡⟨ cong (λ k → g  ⟨$⟩ʳ k) ( inverseʳ g )  ⟩
              g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q )
           ≡⟨ inverseʳ g   ⟩
             q
          ∎ where
              g=h :  g =p= h
              g=h =  FL-inject (trans g=00 (sym h=00))
   solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
   solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  }
   solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
      cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
      cc q = begin
             x ⟨$⟩ʳ q
          ≡⟨ sym (f=g q) ⟩
             f ⟨$⟩ʳ q
          ≡⟨ f=e q ⟩
             q
          ∎ where open ≡-Reasoning

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
open import Nat
open import Prelude
open import List
open import core
open import contexts
open import typed-expansion
open import lemmas-freevars

module livelit-reasoning-principles where
  record reasoning-principles (Φ : livelitctx)
                              (Γ : tctx)
                              (a : livelitname)
                              (dm : iexp)
                              (τsplice : typ)
                              (êsplice : uexp)
                              (eresult : eexp)
                              (τresult : typ) : Set where
    field
      π   : livelitdef
      domain : dom (Φ ₁) a
      eexpanded : eexp
      esplice : eexp

      expanded-application-form : eresult == (eexpanded ·: τsplice ==> τresult) ∘ esplice
      expansion-typing          : (Γ ⊢ eresult => τresult) × (τresult == livelitdef.expansion-type π)
      responsibility            : Σ[ denc ∈ iexp ] (((livelitdef.expand π) ∘ dm) ⇓ denc × denc ↑ eexpanded)
      splice-typing             : Φ , Γ ⊢ êsplice ~~> esplice ⇐ τsplice × Γ ⊢ esplice <= τsplice
      context-independence      : free-vars (eexpanded ·: τsplice ==> τresult) == []

  livelit-reasoning-principles : ∀{Φ Γ a dm τsplice psplice eresult τresult u} →
        Φ , Γ ⊢ ＄ a ⟨ dm ⁏ (τsplice , psplice) :: [] ⟩[ u ] ~~> eresult ⇒ τresult →
        reasoning-principles Φ Γ a dm τsplice psplice eresult τresult
  livelit-reasoning-principles h@(SPEApLivelit {dm = dm} {π} {denc} {eexpanded} {esplice = esplice} x x₁ x₂ x₃ x₄ x₅ x₆ x₇) =
       record
         { π                         = π
         ; domain                    = _ , x₂
         ; eexpanded                 = eexpanded
         ; esplice                   = esplice
         ; expanded-application-form = refl
         ; expansion-typing          = typed-expansion-synth h , refl
         ; responsibility            = denc , x₄ , x₅
         ; splice-typing             = x₆ , typed-expansion-ana x₆
         ; context-independence      = ∅∈l→l==[] (λ x → fv-lemma-ana refl x₇)
         }

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


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

   Copyright (c) 2020, 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.Prelude

-- This module defines functionality modeling an RWS monad, which we use to
-- define an implementation, and functionality for proving properties about
-- programs written using this RWS monad. The main definitions are:
-- 1. RWS, a datatype for the ASTs of stateful programs that read from an
--    environment and produce output.
--    This datatype includes constructors for branching code, to aid in the
--    verification effort (see below).
-- 2. RWS-weakestPre, a large elimination that, given an RWS program and a
--    post condition for the program, produces the weakest precondition needed
--    to satisfy that post condition. Branches in code using the constructors
--    `RWS-if` and friends are translated into products, with each component of
--    the product corresponding to a possible branch taken.
-- 3. RWS-Contract is the type of proofs that, given a stateful computation and
--    a post condition, the weakest precondition suffices to prove that post
--    condition.
-- 4. RWS-contract proves RWS-Contract, i.e., for every stateful computation
--    `m` and post condition `P`, given a proof over a pre-state `pre` the
--    weakest precondition for `P` holds, then postcondition `P` holds for the
--    post-state obtained from running `m` in state `pre`.

-- TODO-2: this module is independent of any particular implementation
-- and arguably belongs somewhere more general, such as next to Optics.

module LibraBFT.ImplShared.Util.Dijkstra.RWS where

-- RWS, the AST of computations with state `St` reading from an environment
-- `Ev` and producing a list of outputs of type `Wr`
data RWS (Ev Wr St : Set) : Set → Set₁ where
  -- Primitive combinators
  RWS-return : ∀ {A}   → A                                       → RWS Ev Wr St A
  RWS-bind   : ∀ {A B} → RWS Ev Wr St A → (A → RWS Ev Wr St B)   → RWS Ev Wr St B
  RWS-gets   : ∀ {A} → (St → A)                                  → RWS Ev Wr St A
  RWS-put    : St                                                → RWS Ev Wr St Unit
  RWS-ask    :                                                     RWS Ev Wr St Ev
  RWS-tell   : List Wr                                           → RWS Ev Wr St Unit
  -- Branching combinators (used for creating more convenient contracts)
  RWS-if     : ∀ {A} → Guards (RWS Ev Wr St A)                   → RWS Ev Wr St A
  RWS-either : ∀ {A B C} → Either B C
                → (B → RWS Ev Wr St A) → (C → RWS Ev Wr St A)    → RWS Ev Wr St A
  RWS-ebind  : ∀ {A B C}
                → RWS Ev Wr St (Either C A)
                → (A → RWS Ev Wr St (Either C B))                → RWS Ev Wr St (Either C B)
  RWS-maybe  : ∀ {A B} → Maybe B
                → (RWS Ev Wr St A) → (B → RWS Ev Wr St A)        → RWS Ev Wr St A

private
  variable
    Ev Wr St : Set
    A B C    : Set

-- To execute an RWS program, you provide an environment and prestate. This
-- produces a result value, poststate, and list of outputs.
RWS-run : RWS Ev Wr St A → Ev → St → A × St × List Wr
RWS-run (RWS-return x) ev st  = x , st , []
RWS-run (RWS-bind m f) ev st
   with RWS-run m ev st
...| x₁ , st₁ , outs₁
   with RWS-run (f x₁) ev st₁
...| x₂ , st₂ , outs₂           = x₂ , st₂ , outs₁ ++ outs₂
RWS-run (RWS-gets f) ev st    = f st , st , []
RWS-run (RWS-put st) ev _     = unit , st , []
RWS-run RWS-ask ev st         = ev , st , []
RWS-run (RWS-tell outs) ev st = unit , st , outs
RWS-run (RWS-if (clause (b ≔ c) gs)) ev st =
  if toBool b then RWS-run c ev st else RWS-run (RWS-if gs) ev st
RWS-run (RWS-if (otherwise≔ c)) ev st = RWS-run c ev st
RWS-run (RWS-either (Left x) f₁ f₂) ev st = RWS-run (f₁ x) ev st
RWS-run (RWS-either (Right y) f₁ f₂) ev st = RWS-run (f₂ y) ev st
RWS-run (RWS-ebind m f) ev st
   with RWS-run m ev st
...| Left c , st₁ , outs₁ = Left c , st₁ , outs₁
...| Right a , st₁ , outs₁
   with RWS-run (f a) ev st₁
...| r , st₂ , outs₂ = r , st₂ , outs₁ ++ outs₂
RWS-run (RWS-maybe nothing f₁ f₂) ev st = RWS-run f₁ ev st
RWS-run (RWS-maybe (just x) f₁ f₂) ev st = RWS-run (f₂ x) ev st

-- Accessors for the result, poststate, and outputs.
RWS-result : RWS Ev Wr St A → Ev → St → A
RWS-result m ev st = proj₁ (RWS-run m ev st)

RWS-post : RWS Ev Wr St A → Ev → St → St
RWS-post m ev st = proj₁ (proj₂ (RWS-run m ev st))

RWS-outs : RWS Ev Wr St A → Ev → St → List Wr
RWS-outs m ev st = proj₂ (proj₂ (RWS-run m ev st))

-- Preconditions are predicates over environments and prestates.
RWS-Pre : (Ev St : Set) → Set₁
RWS-Pre Ev St = (ev : Ev) (pre : St) → Set

-- Postconditions are predicates over a result, poststate, and list of outputs.
RWS-Post : (Wr St A : Set) → Set₁
RWS-Post Wr St A = (x : A) (post : St) (outs : List Wr) → Set

RWS-Post-⇒ : (P Q : RWS-Post Wr St A) → Set
RWS-Post-⇒ P Q = ∀ r st outs → P r st outs → Q r st outs

-- RWS-weakestPre computes a predicate transformer: it maps a RWS
-- computation `m` and desired postcondition `Post` to the weakest precondition
-- needed to prove `P` holds after running `m`.
RWS-PredTrans : (Ev Wr St A : Set) → Set₁
RWS-PredTrans Ev Wr St A = RWS-Post Wr St A → RWS-Pre Ev St

-- When RWS computations are sequenced, e.g., `RWS-bind m λ x → f x`,
-- outputs are concatenated. The postcondition desired for the above sequence
-- becomes a postcondition for `f x` in which the outputs of `m` are prepended
-- to the outputs of `f x`.
RWS-Post++ : ∀ {Wr St A} → RWS-Post Wr St A → List Wr → RWS-Post Wr St A
RWS-Post++ P outs x post outs₁ = P x post (outs ++ outs₁)

-- Consider again the sequence `RWS-bind m₁ λ x → f x`. We also translate a
-- postcondition `P` for the sequence into a postcondition for `m` ---
-- specifically, the post condition we want for `m` is that the weakest
-- precondition for `RWS-Post++ P outs` holds, where `outs` are the outputs of
-- `m`.
RWS-weakestPre-bindPost  : (ev : Ev) (f : A → RWS Ev Wr St B) → RWS-Post Wr St B → RWS-Post Wr St A
RWS-weakestPre-ebindPost : (ev : Ev) (f : A → RWS Ev Wr St (C ⊎ B)) → RWS-Post Wr St (C ⊎ B) → RWS-Post Wr St (C ⊎ A)

RWS-weakestPre : (m : RWS Ev Wr St A) → RWS-PredTrans Ev Wr St A
RWS-weakestPre (RWS-return x) P ev pre = P x pre []
RWS-weakestPre (RWS-bind m f) P ev pre =
  RWS-weakestPre m (RWS-weakestPre-bindPost ev f P) ev pre
RWS-weakestPre (RWS-gets f) P ev pre = P (f pre) pre []
RWS-weakestPre (RWS-put post) P ev pre = P unit post []
RWS-weakestPre RWS-ask P ev pre = P ev pre []
RWS-weakestPre (RWS-tell outs) P ev pre = P unit pre outs
RWS-weakestPre (RWS-if (clause (b ≔ c) gs)) P ev pre =
  (toBool b ≡ true → RWS-weakestPre c P ev pre)
  × (toBool b ≡ false → RWS-weakestPre (RWS-if gs) P ev pre)
RWS-weakestPre (RWS-if (otherwise≔ c)) P ev pre =
  RWS-weakestPre c P ev pre
RWS-weakestPre (RWS-either e f₁ f₂) P ev pre =
    (∀ x → (e ≡ Left x) →
      RWS-weakestPre (f₁ x) P ev pre)
  × (∀ y → (e ≡ Right y) →
       RWS-weakestPre (f₂ y) P ev pre)
RWS-weakestPre (RWS-ebind m f) P ev pre =
  RWS-weakestPre m (RWS-weakestPre-ebindPost ev f P) ev pre
RWS-weakestPre (RWS-maybe m f₁ f₂) P ev pre =
  (m ≡ nothing → RWS-weakestPre f₁ P ev pre)
  × (∀ j → m ≡ just j → RWS-weakestPre (f₂ j) P ev pre)

RWS-weakestPre-ebindPost ev f Post (Left r) post outs =
  Post (Left r) post outs
RWS-weakestPre-ebindPost ev f Post (Right r) post outs =
  ∀ c → c ≡ r → RWS-weakestPre (f c) (RWS-Post++ Post outs) ev post

RWS-weakestPre-bindPost ev f Post x post outs =
  ∀ r → r ≡ x → RWS-weakestPre (f r) (RWS-Post++ Post outs) ev post

-- The post condition `P` holds for `m` with environment `ev` and prestate `pre`
RWS-Post-True : (P : RWS-Post Wr St A) (m : RWS Ev Wr St A) (ev : Ev) (pre : St) → Set
RWS-Post-True P m ev pre =
  let (x , post , outs) = RWS-run m ev pre in
  P x post outs

-- For every RWS computation `m`, `RWS-Contract m` is the type of proofs that,
-- for all post conditions `P`, starting environments `ev` and prestates `pre`,
-- to prove that `P` holds after running `m` in `ev` and `pre`, it suffices to
-- provide a proof of the weakest precondition for `P` with respect to `m`,
-- `ev`, and `pre`.
RWS-Contract : (m : RWS Ev Wr St A) → Set₁
RWS-Contract{Ev}{Wr}{St}{A} m =
  (P : RWS-Post Wr St A)
  → (ev : Ev) (pre : St) → RWS-weakestPre m P ev pre
  → RWS-Post-True P m ev pre

-- This proves that `RWS-weakestPre` gives a *sufficient* precondition for
-- establishing a desired postcondition. Note thought that it does not prove
-- that this precondition is the weakest such one; even though this is true, it
-- is not important for our purposes.
RWS-contract : (m : RWS Ev Wr St A) → RWS-Contract m
RWS-contract (RWS-return x₁) P ev pre wp = wp
RWS-contract (RWS-bind m f) P ev pre wp
   with RWS-contract m _ ev pre wp
...| con
   with RWS-run m ev pre
...| x₁ , st₁ , outs₁ =
  RWS-contract (f x₁) _ ev st₁ (con x₁ refl)
RWS-contract (RWS-gets f) P ev pre wp = wp
RWS-contract (RWS-put x₁) P ev pre wp = wp
RWS-contract RWS-ask P ev pre wp = wp
RWS-contract (RWS-tell x₁) P ev pre wp = wp
RWS-contract{Ev}{Wr}{St}{A} (RWS-if gs) P ev pre wp = RWS-contract-if gs P ev pre wp
  where
  RWS-contract-if : (gs : Guards (RWS Ev Wr St A)) → RWS-Contract (RWS-if gs)
  RWS-contract-if (clause (b ≔ c) gs) P ev pre (wp₁ , wp₂)
    with toBool b
  ...| true = RWS-contract c _ ev pre (wp₁ refl)
  ...| false = RWS-contract-if gs _ ev pre (wp₂ refl)
  RWS-contract-if (otherwise≔ x) P ev pre wp =
    RWS-contract x P ev pre wp
RWS-contract (RWS-either (Left x) f₁ f₂) P ev pre (wp₁ , wp₂) =
  RWS-contract (f₁ x) _ ev pre (wp₁ x refl)
RWS-contract (RWS-either (Right y) f₁ f₂) P ev pre (wp₁ , wp₂) =
  RWS-contract (f₂ y) _ ev pre (wp₂ y refl)
RWS-contract (RWS-ebind m f) P ev pre wp
   with RWS-contract m _ ev pre wp
...| con
   with RWS-run m ev pre
... | Left x , st₁ , outs₁ = con
... | Right y , st₁ , outs₁ = RWS-contract (f y) _ ev st₁ (con y refl)
RWS-contract (RWS-maybe nothing f₁ f₂) P ev pre (wp₁ , wp₂)
  = RWS-contract f₁ _ ev pre (wp₁ refl)
RWS-contract (RWS-maybe (just x) f₁ f₂) P ev pre (wp₁ , wp₂) =
  RWS-contract (f₂ x) _ ev pre (wp₂ x refl)

-- This helper function is primarily used to take a proof concerning one
-- computation `m` and show that that proof implies a property concerning a
-- larger computation which contains `m`.
RWS-⇒
  : (P Q : RWS-Post Wr St A) → (RWS-Post-⇒ P Q)
    → ∀ m (ev : Ev) st → RWS-weakestPre m P ev st → RWS-weakestPre m Q ev st
RWS-⇒ P Q pf (RWS-return x) ev st pre = pf x st [] pre
RWS-⇒ P Q pf (RWS-bind m f) ev st pre =
  RWS-⇒ _ _
    (λ r₁ st₁ outs₁ pf₁ x x≡ →
      RWS-⇒ _ _
        (λ r₂ st₂ outs₂ pf₂ → pf r₂ st₂ (outs₁ ++ outs₂) pf₂)
        (f x) ev st₁ (pf₁ x x≡))
    m ev st pre
RWS-⇒ P Q pf (RWS-gets f) ev st pre = pf _ _ _ pre
RWS-⇒ P Q pf (RWS-put x) ev st pre = pf _ _ _ pre
RWS-⇒ P Q pf RWS-ask ev st pre = pf _ _ _ pre
RWS-⇒ P Q pf (RWS-tell x) ev st pre = pf _ _ _ pre
RWS-⇒ P Q pf (RWS-if (otherwise≔ x)) ev st pre = RWS-⇒ _ _ pf x ev st pre
RWS-⇒ P Q pf (RWS-if (clause (b ≔ c) cs)) ev st (pre₁ , pre₂) =
  (λ pf' → RWS-⇒ _ _ pf c ev st (pre₁ pf'))
  , λ pf' → RWS-⇒ _ _ pf (RWS-if cs) ev st (pre₂ pf')
proj₁ (RWS-⇒ P Q pf (RWS-either (Left x) f₁ f₂) ev st (pre₁ , pre₂)) x₁ x₁≡ =
  RWS-⇒ _ _ pf (f₁ x₁) ev st (pre₁ x₁ x₁≡)
proj₂ (RWS-⇒ P Q pf (RWS-either (Left x) f₁ f₂) ev st (pre₁ , pre₂)) y ()
proj₁ (RWS-⇒ P Q pf (RWS-either (Right y) f₁ f₂) ev st (pre₁ , pre₂)) y₁ ()
proj₂ (RWS-⇒ P Q pf (RWS-either (Right y) f₁ f₂) ev st (pre₁ , pre₂)) y₁ y₁≡ =
  RWS-⇒ _ _ pf (f₂ y₁) ev st (pre₂ y₁ y₁≡)
RWS-⇒ P Q pf (RWS-ebind m f) ev st pre =
  RWS-⇒ _ _
    (λ { (Left x₁) st₁ outs x → pf _ _ _ x
       ; (Right y) st₁ outs x → λ c x₁ →
           RWS-⇒ _ _ (λ r st₂ outs₁ x₂ → pf r st₂ (outs ++ outs₁) x₂) (f c) ev st₁ (x c x₁)})
    m ev st pre
proj₁ (RWS-⇒ P Q pf (RWS-maybe x m f) ev st (pre₁ , pre₂)) ≡nothing = RWS-⇒ _ _ pf m ev st (pre₁ ≡nothing)
proj₂ (RWS-⇒ P Q pf (RWS-maybe x m f) ev st (pre₁ , pre₂)) b b≡ = RWS-⇒ _ _ pf (f b) ev st (pre₂ b b≡)

RWS-⇒-bind
  : (P : RWS-Post Wr St A) (Q : RWS-Post Wr St B)
    → (f : A → RWS Ev Wr St B) (ev : Ev)
    → RWS-Post-⇒ P (RWS-weakestPre-bindPost ev f Q)
    → ∀ m st → RWS-weakestPre m P ev st
    → RWS-weakestPre (RWS-bind m f) Q ev st
RWS-⇒-bind P Q f ev pf m st con =
  RWS-⇒ P ((RWS-weakestPre-bindPost ev f Q)) pf m ev st con

RWS-⇒-ebind
  : (P : RWS-Post Wr St (Either C A)) (Q : RWS-Post Wr St (Either C B))
    → (f : A → RWS Ev Wr St (Either C B)) (ev : Ev)
    → RWS-Post-⇒ P (RWS-weakestPre-ebindPost ev f Q)
    → ∀ m st → RWS-weakestPre m P ev st
    → RWS-weakestPre (RWS-ebind m f) Q ev st
RWS-⇒-ebind P Q f ev pf m st con =
  RWS-⇒ P ((RWS-weakestPre-ebindPost ev f Q)) pf m ev st con

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
{-# OPTIONS --cubical-compatible #-}
module Issue388 where

data P (A : Set₁) : A → Set₁ where
  p : ∀ x → P A x

data D : Set → Set₁ where
  d : ∀ A → D A

Foo : ∀ A → P (D A) (d A) → Set
Foo A x = {!x!}


text:
{-# OPTIONS -v treeless.opt:20 #-}
module _ where

open import Common.Prelude

module _ {a} {A : Set a} (_<_ : A → A → Bool) where
  merge : List A → List A → List A
  merge [] ys = ys
  merge xs [] = xs
  merge xs@(x ∷ xs₁) ys@(y ∷ ys₁) =
    if x < y then (x ∷ merge xs₁ ys)  -- Generated treeless code should preserve
             else (y ∷ merge xs ys₁)  -- xs and ys (and not expand to _∷_).

open import Agda.Builtin.Nat

mapM! : {A : Set} → (A → IO Unit) → List A → IO Unit
mapM! f [] = return unit
mapM! f (x ∷ xs) = f x >>= λ _ → mapM! f xs

xs ys : List Nat
xs = 2 ∷ 3 ∷ 5 ∷ 10 ∷ 20 ∷ []
ys = 0 ∷ 1 ∷ 2 ∷ 8 ∷ 10 ∷ 15 ∷ []

main : IO Unit
main = mapM! printNat (merge _<_ xs ys)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --warning=error #-}

module UselessAbstractAbstract where

A : Set₁
abstract
  abstract
    A = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Instances.Initial where

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

open import Cubical.Data.Unit
open import Cubical.Data.Sigma.Properties using (Σ≡Prop)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom)
open import Cubical.Algebra.CommAlgebra.Base

private
  variable
    ℓ : Level

module _ ((R , str) : CommRing ℓ) where

  initialCAlg : CommAlgebra (R , str) ℓ
  initialCAlg =
    let open CommRingStr str
    in  (R , commalgebrastr _ _ _ _ _ (λ r x → r · x)
                    (makeIsCommAlgebra (isSetRing (CommRing→Ring (R , str)))
                       +Assoc +Rid +Rinv +Comm
                       ·Assoc ·Lid
                       ·Ldist+ ·Comm
                        (λ x y z → sym (·Assoc x y z)) ·Ldist+ ·Rdist+ ·Lid
                         λ x y z → sym (·Assoc x y z)))

  module _ (A : CommAlgebra (R , str) ℓ) where
    open CommAlgebraStr ⦃... ⦄
    private
      instance
        _ : CommAlgebraStr (R , str) (fst A)
        _ = snd A
        _ : CommAlgebraStr (R , str) R
        _ = snd initialCAlg

    _*_ : R → (fst A) → (fst A)
    r * a = CommAlgebraStr._⋆_ (snd A) r a

    initialMap : CommAlgebraHom initialCAlg A
    initialMap =
      makeCommAlgebraHom {M = initialCAlg} {N = A}
        (λ r → r * 1a)
        (⋆-lid _)
        (λ x y → ⋆-ldist x y 1a)
        (λ x y →  (x · y) * 1a ≡⟨ ⋆-assoc _ _ _ ⟩
                           x * (y * 1a)                   ≡[ i ]⟨ x * (·Lid (y * 1a) (~ i)) ⟩
                           x * (1a · (y * 1a))            ≡⟨ sym (⋆-lassoc _ _ _) ⟩
                           (x * 1a) · (y * 1a) ∎)
        (λ r x → (r · x) * 1a   ≡⟨ ⋆-assoc _ _ _ ⟩
                         (r * (x * 1a)) ∎)

    initialMapEq : (f : CommAlgebraHom initialCAlg A)
                   → f ≡ initialMap
    initialMapEq f =
      let open IsAlgebraHom (snd f)
      in Σ≡Prop
           (isPropIsCommAlgebraHom {M = initialCAlg} {N = A})
             λ i x →
               ((fst f) x                              ≡⟨ cong (fst f) (sym (·Rid _)) ⟩
               fst f (x · 1a)                          ≡⟨ pres⋆ x 1a ⟩
               CommAlgebraStr._⋆_ (snd A) x (fst f 1a) ≡⟨ cong
                                                           (λ u → (snd A CommAlgebraStr.⋆ x) u)
                                                           pres1 ⟩
               (CommAlgebraStr._⋆_ (snd A) x 1a) ∎) i

    initialityIso : Iso (CommAlgebraHom initialCAlg A) (Unit* {ℓ = ℓ})
    initialityIso = iso (λ _ → tt*)
                        (λ _ → initialMap)
                        (λ {tt*x → refl})
                        λ f → sym (initialMapEq f)

    initialityPath : CommAlgebraHom initialCAlg A ≡ Unit*
    initialityPath = isoToPath initialityIso

max_stars_repo_name: FernandoLarrain/cubical


text:
module z02-theorem-proving-with-booleans where

open import bool
open import eq
open import level

-- p 28
~~tt : ~ ~ tt ≡ tt
~~tt = refl

-- p 32
~~ff : ~ ~ ff ≡ ff
~~ff = refl

-- p 33
~~-elim : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim tt = refl
~~-elim ff = refl

-- p 34
~~-elim2 : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim2 tt = ~~tt
~~-elim2 ff = ~~ff

{-
-- p 34 - does not typecheck (on purpose) because of IMPLICIT ARGS
-- IMPLICIT ARGS: stated inside curly brackets (like IF previously)
~~-elim3 : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim3 tt = ~~ff
~~-elim3 ff = ~~tt

'refl' has implicit args
- the expression 'x' in 'x ≡ x' (e.g., in ~~tt the implicit is 'tt')
  - in ~~-elim3 implicit arg 'tt' does not match '~~ff'
-}

{-
-- p 35 : HOLES

~~-elim4 : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim4 tt = ?
~~-elim4 ff = ?
-}

-- p 36
&&-same : ∀ (b : 𝔹) → b && b ≡ b
&&-same tt = refl
&&-same ff = refl

-- infer type of 'b'
&&-same2 : ∀ b → b && b ≡ b
&&-same2 tt = refl
&&-same2 ff = refl

-- 'b' as implicit argument
&&-same3 : ∀ {b} → b && b ≡ b
&&-same3 {tt} = refl
&&-same3 {ff} = refl

-- p 37
-- so no need to supply implicit arg to &&-same3
test-&&-same : tt && tt ≡ tt
test-&&-same = &&-same3

-- ok to explicitly supply implicit arg
test-&&-same2 : tt && tt ≡ tt
test-&&-same2 = &&-same3 {tt}

-- p 38
||-same : ∀ {b} → b || b ≡ b
||-same {tt} = refl
||-same {ff} = refl

------------------------------------------------------------------------------
-- p. 38 2.4 Theorems with Hypotheses

{-
to express an assumption, write fun that
- takes a proof of assumption
- returns proof of desired result
-}

-- if b1 || b2 is false, then b1 must be false
||≡ff₁ : ∀ {b1 b2}
       → b1 || b2 ≡ ff -- assumption
       → b1       ≡ ff -- desired result

-- 1st (implicit) arg is 'ff'
-- 2nd (explicit) arg is ((b1 || b2) ≡ ff) bound to 'p' (but not used)
||≡ff₁ {ff} p = refl -- b1 = ff ≡ ff

-- absurd pattern '()'
||≡ff₁ {tt} ()       -- no '=' sign because impossible

{-
To prove the impossible, but only if some impossible assumption is true,
use absurd, since that impossible assumption can never be satisfied by a use of this theorem.
-}

-- p 41 alternative

||≡ff₁-2 : ∀ {b1 b2} → b1 || b2 ≡ ff → b1 ≡ ff
||≡ff₁-2 {ff} p = refl
||≡ff₁-2 {tt} p = p -- 'p' is equal to 'tt ≡ ff' -- the desired result of 'b1' instantiated to 'tt'

-- prefer version that uses absurd -- more robust to later changes

------------------------------------------------------------------------------
-- p 42 2.4.3 Matching on equality proofs

{-
special case on CONGRUENCE
if X equals Y then any TYPE containing X is equal to that same TYPE with X's replaced by Y

Congruence holds for definitional equality automatically.
Congruence must be proved for PROPOSITIONAL equalities 'a ≡ b'
-}

||-cong₁ : ∀ {b1 b1’ b2}        -- implicit args
         → b1       ≡ b1’       -- explicit arg
         → b1 || b2 ≡ b1’ || b2 -- desired result
||-cong₁ refl = refl

{-
-- p 43

only one way to construct an equality proof : via 'refl' constructor

refl can only prove something of the form  x ≡ x
- so Agda deduces b1 must be exactly b1’

Agda uses definitional
- knows b1 must be definitionally equal to b1’
- so refines the desired type using this definitional equality

So only need to prove : ((b1 || b2) ≡ (b1 || b2)) -- b1' replaced with b1 since equal
- via 'refl'

------------------------------------------------------------------------------
REFL

Important rule about using type refinements (refl).

Not allowed in such a way that non-variable terms are discovered
 to be definitionally equal to other such terms.

e.g.,

two non-variable terms are definitionally equal:
  b1 || b2
  ff

------------------------------------------------------------------------------
DOT PATTERN

b1, b1’, and b2 are implicit arguments above.

To include them in the pattern on the left-hand side of the equation:

||-cong₁ : ∀ {b1 b1’ b2}        -- implicit args
         → b1       ≡ b1’       -- explicit arg
         → b1 || b2 ≡ b1’ || b2 -- desired result
||-cong₁ {b1}{b1’}{b2} refl = refl

but Agda will complain because to type check this pattern, b1 and b1' can NOT be distinct.
Agda deduces b1 and b1’ to be definitionally equal.

Workaround : dot pattern:

||-cong₁ : ∀ {b1 b1’ b2}        -- implicit args
         → b1       ≡ b1’       -- explicit arg
         → b1 || b2 ≡ b1’ || b2 -- desired result
||-cong₁ {b1}{.b1}{b2} refl = refl

Writing “.” in front of term in pattern tells Agda that term is not a subpattern to match.
Rather it has a form which is dictated by the type of the whole pattern.
-}

------------------------------------------------------------------------------
-- p 44 2.4.4 The REWRITE directive

||-cong₂ : ∀ {b1 b2 b2'}
         → b2       ≡ b2'
         → b1 || b2 ≡ b1 || b2'
||-cong₂ p rewrite p = refl

{-
pattern variable p : with type b2 ≡ b2’

rewrite every occurrence of the left-hand side,
as it appears in the current goal,
with the right-hand side.

goal is formula to prove on right-hand side of current equation

rewrite p : transform the b2 (the left side of p) in
   b1 || b2  ≡ b1 || b2'
to
         b2' (the right side of p)
so goal (the type Agda is checking against the right-hand side of the equation) becomes
   b1 || b2’ ≡ b1 || b2’

REWRITE

given proof 'p' of some equation X ≡ Y
(any expression which has X ≡ Y as its type, e.g., call to lemma of that type)
look in goal
for any occurrences of X
transform those into Y

X and Y can be complex expressions (not just variables)

------------------------------------------------------------------------------
-- p 44 2.5 Further examples

proving a polymorphic theorem

for every type level ℓ
and every type A at that level
and for all booleans
the given ITE holds
-}

ite-same : ∀ {ℓ} {A : Set ℓ}    -- two implicit args
                                --     so no patterns needed on left hand side of equations
         → ∀ (b : 𝔹) (x : A)    -- two explicit args
         → if b then x else x
         ≡ x
-- reason by cases on 'b'
ite-same tt _ = refl -- x ≡ x
ite-same ff _ = refl

------------------------------------------------------------------------------
-- p 45

B-contra : ff ≡ tt           -- if ff ≡ tt holds
         → (∀ {P : Set} → P) -- then can prove anything
                             --      every formula P is true (which is NOT true)
B-contra ()

------------------------------------------------------------------------------
-- p 46 SUMMARY

{-
- equality TYPE t ≡ t’ expresses equality of expressions t and t’, which must have the same type

- prove equality with refl; will prove t ≡ t' for any definitionally equal t and t’

- two exprs definitionally equal if they can be proved equal using their defining equations

- proof is program defined using pattern matching

- Pattern matching can instantiate universally quantified variables which appear in the type.
  Has the effect of specializing the desired formula to the specific instances of those variables.

- Args can be declared implicit with curly braces in the type.
  Can pattern match on implicit arguments,
  using curly braces around the pattern on left-hand side of equation

- assumptions in theorems are args to programs which serve as proofs of those theorems

- absurd pattern can be used when an assumption is definitionally equal to an impossible equality,
  where the equated terms start with different constructors

- When using refl as the pattern for an equality assumption t ≡ t’,
  Agda will try to refine the type by making t and t’ definitionally equal.
-}

------------------------------------------------------------------------------
-- p 47 Exercises

-- 1

&&-idem : ∀ {b}         -- implicit arg
        → b && b ≡ b    -- result
&&-idem {tt} = refl
&&-idem {ff} = refl

||-idem : ∀ {b}         -- implicit arg
        → b || b ≡ b    -- result
||-idem {tt} = refl
||-idem {ff} = refl

||≡ff₂ : ∀ {b1 b2}      -- implicit args
       → b1 || b2 ≡ ff  -- explicit arg
       →       b2 ≡ ff  -- result
||≡ff₂ {ff}{ff} _ = refl
{-
||≡ff₂ {tt} ()
||≡ff₂ {ff}{tt} ()
-}

||-tt : ∀ (b : 𝔹)       -- explicit arg
      → b || tt ≡ tt    -- result
||-tt tt = refl
||-tt ff = refl

ite-arg : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}                    -- implicit args
        → (f : A → B) (b : 𝔹) (x y : A)                       -- explicit args
        → (f (if b then x else y)) ≡ (if b then f x else f y) -- result
ite-arg _ tt _ _ = refl
ite-arg _ ff _ _ = refl

𝔹-contra : ff ≡ tt
         → ∀{ℓ} {P : Set ℓ}
         → P
𝔹-contra ()
{-
open import sum
||-split : ∀ {b b' : 𝔹}
         → b || b' ≡ tt
         → b ≡ tt ⊎ b' ≡ tt
||-split{tt}{tt} p = inj₁ refl
||-split{tt}{ff} p = inj₁ refl
||-split{ff}{tt} p = inj₂ refl
||-split{ff}{ff} ()

𝔹-dec : ∀ (b : 𝔹)
      → b ≡ tt ⊎ b ≡ ff
𝔹-dec tt = inj₁ refl
𝔹-dec ff = inj₂ refl
-}
&&-snd : {p1 p2 : 𝔹}    -- implicit args
       → p1 && p2 ≡ tt  -- explicit arg
       →       p2 ≡ tt  -- result
&&-snd {tt} {tt} _ = refl
--&&-snd{ff} ()

&&-fst : {p1 p2 : 𝔹}
       → p1 && p2 ≡ tt
       → p1       ≡ tt
&&-fst {tt} {tt} _ = refl
-- &&-fst{ff} ()

&&-combo : {p1 p2 : 𝔹}         -- implicit
         → p1       ≡ tt       -- explcit
         →       p2 ≡ tt       -- explcit
         → p1 && p2 ≡ tt       -- result
&&-combo {tt} {tt} _ _ = refl
{- alternative
&&-combo{tt} pr1 pr2 = pr2
&&-combo{ff} pr1 pr2 = 𝔹-contra pr1
-}

&&-ff : ∀(b : 𝔹)
      → b && ff ≡ ff
&&-ff tt = refl
&&-ff ff = refl

------------------------------------------------------------------------------
-- 2

ff-imp : ∀ (b : 𝔹)
       → ff imp b ≡ tt
ff-imp tt = refl
ff-imp ff = refl

imp-tt : ∀ (b : 𝔹)
       → b imp tt ≡ tt
imp-tt tt = refl
imp-tt ff = refl

imp-ff : ∀ (b : 𝔹)
       → b imp ff ≡ ~ b
imp-ff tt = refl
imp-ff ff = refl

tt-imp : ∀ (b : 𝔹)
       → tt imp b ≡ b
tt-imp tt = refl
tt-imp ff = refl

&&-tt : ∀ (b : 𝔹)
      → b && tt ≡ b
&&-tt tt = refl
&&-tt ff = refl

||-ff : ∀ (b : 𝔹)
      → b || ff ≡ b
||-ff tt = refl
||-ff ff = refl

&&-contra : ∀ (b : 𝔹)
          → b && ~ b ≡ ff
&&-contra tt = refl
&&-contra ff = refl

&&-comm : ∀ (b1 b2 : 𝔹)
        → b1 && b2 ≡ b2 && b1
&&-comm ff ff = refl
&&-comm ff tt = refl
&&-comm tt ff = refl
&&-comm tt tt = refl

||-comm : ∀ (b1 b2 : 𝔹)
        → b1 || b2 ≡ b2 || b1
||-comm ff ff = refl
||-comm ff tt = refl
||-comm tt ff = refl
||-comm tt tt = refl

&&-assoc : ∀ (b1 b2 b3 : 𝔹)
         → b1 && (b2 && b3) ≡ (b1 && b2) && b3
&&-assoc ff ff ff = refl
&&-assoc ff ff tt = refl
&&-assoc ff tt ff = refl
&&-assoc ff tt tt = refl
&&-assoc tt ff ff = refl
&&-assoc tt ff tt = refl
&&-assoc tt tt ff = refl
&&-assoc tt tt tt = refl

||-assoc : ∀ (b1 b2 b3 : 𝔹)
         → b1 || (b2 || b3) ≡ (b1 || b2) || b3
||-assoc ff ff ff = refl
||-assoc ff ff tt = refl
||-assoc ff tt ff = refl
||-assoc ff tt tt = refl
||-assoc tt ff ff = refl
||-assoc tt ff tt = refl
||-assoc tt tt ff = refl
||-assoc tt tt tt = refl

~-over-&& : ∀ (b1 b2 : 𝔹)
          → ~ ( b1 && b2 ) ≡ (~ b1 || ~ b2)
~-over-&& ff ff = refl
~-over-&& ff tt = refl
~-over-&& tt ff = refl
~-over-&& tt tt = refl

~-over-|| : ∀ (b1 b2 : 𝔹)
          → ~ ( b1 || b2 ) ≡ (~ b1 && ~ b2)
~-over-|| ff ff = refl
~-over-|| ff tt = refl
~-over-|| tt ff = refl
~-over-|| tt tt = refl

&&-over-||-l : ∀ (a b c : 𝔹)
             → a && (b || c) ≡ (a && b) || (a && c)
&&-over-||-l ff ff ff = refl
&&-over-||-l ff ff tt = refl
&&-over-||-l ff tt ff = refl
&&-over-||-l ff tt tt = refl
&&-over-||-l tt ff ff = refl
&&-over-||-l tt ff tt = refl
&&-over-||-l tt tt ff = refl
&&-over-||-l tt tt tt = refl
{-
&&-over-||-r : ∀ (a b c : 𝔹) → (a || b) && c ≡ (a && c) || (b && c)
||-over-&&-l : ∀ (a b c : 𝔹) → a || (b && c) ≡ (a || b) && (a || c)
||-over-&&-r : ∀ (a b c : 𝔹) → (a && b) || c ≡ (a || c) && (b || c)
&&-cong₁ : ∀ {b1 b1' b2 : 𝔹} → b1 ≡ b1' → b1 && b2 ≡ b1' && b2
&&-cong₂ : ∀ {b1 b2 b2' : 𝔹} → b2 ≡ b2' → b1 && b2 ≡ b1 && b2'
&&-intro : ∀ {b1 b2 : 𝔹} → b1 ≡ tt → b2 ≡ tt → b1 && b2 ≡ tt
||-intro1 : ∀ {b1 b2 : 𝔹} → b1 ≡ tt → b1 || b2 ≡ tt
--&&-elim : ∀ {b1 b2 : 𝔹} → b1 && b2 ≡ tt → b1 ≡ tt ∧ b2 ≡ tt
&&-elim1 : ∀ {b1 b2 : 𝔹} → b1 && b2 ≡ tt → b1 ≡ tt
&&-elim2 : ∀ {b1 b2 : 𝔹} → b1 && b2 ≡ tt → b2 ≡ tt
--||-elim : ∀ {b1 b2 : 𝔹} → b1 || b2 ≡ tt → b1 ≡ tt ∨ b2 ≡ tt
-}
~-cong : ∀ {b b' : 𝔹}
       →   b ≡   b'
       → ~ b ≡ ~ b'
~-cong refl = refl

ite-cong₁ : ∀{ℓ}{A : Set ℓ} {b b' : 𝔹}
            (x y : A)
          →     b                ≡     b'
          → (if b then x else y) ≡ (if b' then x else y)
ite-cong₁ _ _ refl = refl

ite-cong₂ : ∀{ℓ} {A : Set ℓ}
            (b : 𝔹)
            {x x' : A}
            (y : A)
          →            x         ≡            x'
          → (if b then x else y) ≡ (if b then x' else y)
ite-cong₂ _ _ refl = refl

ite-cong₃ : ∀{ℓ}{A : Set ℓ}
            (b : 𝔹)
            (x : A)
            {y y' : A}
          →                   y  ≡                   y'
          → (if b then x else y) ≡ (if b then x else y')
ite-cong₃ _ _ refl = refl

--&&-split : ∀ {b b' : 𝔹} → b || b' ≡ ff → b ≡ ff ⊎ b' ≡ ff
{-
imp-same : ∀ (b : 𝔹) → b imp b ≡ tt
imp-to-|| : ∀ (b1 b2 : 𝔹) → (b1 imp b2) ≡ (~ b1 || b2)
imp-mp : ∀ {b b' : 𝔹} → b imp b' ≡ tt → b ≡ tt → b' ≡ tt
imp-antisymm : ∀ {b1 b2 : 𝔹} → b1 imp b2 ≡ tt → b2 imp b1 ≡ tt → b1 ≡ b2
ff-xor : ∀ (b : 𝔹) → ff xor b ≡ b
tt-xor : ∀ (b : 𝔹) → tt xor b ≡ ~ b
~-xor-distrb : ∀ (a b : 𝔹) → ~ (a xor b) ≡ ~ a xor b
xor-distrib-&& : ∀ (x y : 𝔹) → x xor (y && x) ≡ ~ y && x
xor~hop : ∀ (a b : 𝔹) → ~ a xor b ≡ a xor ~ b
xor-comm : ∀ (b1 b2 : 𝔹) → b1 xor b2 ≡ b2 xor b1
xor-assoc : (b1 b2 b3 : 𝔹) → b1 xor (b2 xor b3) ≡ (b1 xor b2) xor b3
xor-anti-idem : (b : 𝔹) → b xor b ≡ ff
xor-≡ : {b1 b2 : 𝔹} → b1 xor b2 ≡ ff → b1 ≡ b2
nor-not : ∀ (b : 𝔹) → b nor b ≡ ~ b
nor-or : ∀ (b1 b2 : 𝔹) → (b1 nor b2) nor (b1 nor b2) ≡ b1 || b2
nor-and : ∀ (b1 b2 : 𝔹) → (b1 nor b1) nor (b2 nor b2) ≡ b1 && b2
nor-comm : ∀ (b1 b2 : 𝔹) → b1 nor b2 ≡ b2 nor b1
nand-comm : ∀ (b1 b2 : 𝔹) → b1 nand b2 ≡ b2 nand b1
-}
------------------------------------------------------------------------------
-- 3

z02-3a : tt ≡ tt
z02-3a = refl

z02-3b : ff ≡ ff
z02-3b = refl

-- NO z02-3c : ff ≡ tt

z02-3d : ff && ff ≡ ~ tt
z02-3d = refl

z02-3e : ∀ (x : 𝔹)
       → tt && x
       ≡ x
z02-3e _ = refl

z02-3f : ∀ (x : 𝔹)
       → x && tt
       ≡ x
z02-3f tt = refl
z02-3f ff = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import typed-elaboration
open import lemmas-gcomplete
open import lemmas-complete

module complete-elaboration where
  mutual
    complete-elaboration-synth : ∀{e τ Γ Δ d} →
                                 Γ gcomplete →
                                 e ecomplete →
                                 Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                                 (d dcomplete × τ tcomplete × Δ == ∅)
    complete-elaboration-synth gc ec ESNum = DCNum , TCNum , refl
    complete-elaboration-synth gc (ECPlus ec₁ ec₂) (ESPlus {Δ1 = Δ1} {Δ2 = Δ2} apt dis x₁ x₂)
      with complete-elaboration-ana gc ec₁ TCNum x₁ | complete-elaboration-ana gc ec₂ TCNum x₂
    ... | d1comp , t1comp , refl | d2comp , t2comp , refl =
      DCPlus (DCCast d1comp t1comp TCNum) (DCCast d2comp t2comp TCNum) , TCNum , refl
    complete-elaboration-synth gc ec (ESVar x₁) = DCVar , gc _ _ x₁ , refl
    complete-elaboration-synth gc (ECLam2 ec x₁) (ESLam x₂ exp)
      with complete-elaboration-synth (gcomp-extend gc x₁ x₂) ec exp
    ... | ih1 , ih2 , ih3 = DCLam ih1 x₁ , TCArr x₁ ih2 , ih3
    complete-elaboration-synth gc (ECAp ec ec₁) (ESAp _ _ x MAHole x₂ x₃)
      with comp-synth gc ec x
    ... | ()
    complete-elaboration-synth gc (ECAp ec ec₁) (ESAp {Δ1 = Δ1} {Δ2 = Δ2} _ _ x MAArr x₂ x₃)
      with comp-synth gc ec x
    ... | TCArr t1 t2
      with complete-elaboration-ana gc ec (TCArr t1 t2) x₂ | complete-elaboration-ana gc ec₁ t1 x₃
    ... | ih1 , _ ,  ih4 | ih2 , _ , ih3 = DCAp (DCCast ih1 (comp-ana gc x₂ ih1) (TCArr t1 t2)) (DCCast ih2 (comp-ana gc x₃ ih2) t1) ,
                                  t2 ,
                                  tr (λ qq → (qq ∪ Δ2) == ∅) (! ih4) (tr (λ qq → (∅ ∪ qq) == ∅) (! ih3) refl)
    complete-elaboration-synth gc () ESEHole
    complete-elaboration-synth gc () (ESNEHole _ exp)
    complete-elaboration-synth gc (ECAsc x ec) (ESAsc x₁)
      with complete-elaboration-ana gc ec x x₁
    ... | ih1 , _ , ih2 = DCCast ih1 (comp-ana gc x₁ ih1) x , x , ih2
    complete-elaboration-synth gc (ECPair ec ec₁) (ESPair {Δ1 = Δ1} {Δ2 = Δ2} x x₁ x₂ x₃)
      with complete-elaboration-synth gc ec x₂ | complete-elaboration-synth gc ec₁ x₃
    ... | ih1 , ih2 , ih3 | ih1' , ih2' , ih3' = DCPair ih1 ih1' , TCProd ih2 ih2' , tr (λ qq → (qq ∪ Δ2) == ∅) (! ih3) ih3'
    complete-elaboration-synth gc (ECFst ec) (ESFst x MPHole x₂)
      with comp-synth gc ec x
    ... | ()
    complete-elaboration-synth gc (ECFst ec) (ESFst x MPProd x₂)
      with comp-synth gc ec x
    ... | TCProd τc1 τc2 with complete-elaboration-ana gc ec (TCProd τc1 τc2) x₂
    ... | ih1 , ih2 , ih3 = DCFst (DCCast ih1 ih2 (TCProd τc1 τc2)) , τc1 , ih3
    complete-elaboration-synth gc (ECSnd ec) (ESSnd x MPHole x₂)
      with comp-synth gc ec x
    ... | ()
    complete-elaboration-synth gc (ECSnd ec) (ESSnd x MPProd x₂)
      with comp-synth gc ec x
    ... | TCProd τc1 τc2 with complete-elaboration-ana gc ec (TCProd τc1 τc2) x₂
    ... | ih1 , ih2 , ih3 = DCSnd (DCCast ih1 ih2 (TCProd τc1 τc2)) , τc2 , ih3

    complete-elaboration-ana : ∀{e τ τ' Γ Δ d} →
                               Γ gcomplete →
                               e ecomplete →
                               τ tcomplete →
                               Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                               (d dcomplete × τ' tcomplete × Δ == ∅)
    complete-elaboration-ana gc (ECLam1 ec) () (EALam x₁ MAHole exp)
    complete-elaboration-ana gc (ECLam1 ec) (TCArr t1 t2)  (EALam x₁ MAArr exp)
      with complete-elaboration-ana (gcomp-extend gc t1 x₁) ec t2 exp
    ... | ih , ih3 , ih2 = DCLam ih t1 , TCArr t1 ih3 , ih2
    complete-elaboration-ana gc ec tc (EASubsume x x₁ x₂ x₃)
      with complete-elaboration-synth gc ec x₂
    ... | ih1 , ih2 , ih3 = ih1 , ih2 , ih3
    complete-elaboration-ana gc (ECInl ec) (TCSum tc tc₁) (EAInl MSSum x₁)
      with complete-elaboration-ana gc ec tc x₁
    ... | ih1 , ih2 , ih3 = DCInl tc₁ ih1 , TCSum ih2 tc₁ , ih3
    complete-elaboration-ana gc (ECInr ec) (TCSum tc tc₁) (EAInr MSSum x₁)
      with complete-elaboration-ana gc ec tc₁ x₁
    ... | ih1 , ih2 , ih3 = DCInr tc ih1 , TCSum tc ih2 , ih3
    complete-elaboration-ana gc (ECCase ec ec₁ ec₂) tc (EACase x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ MSHole x₁₀ x₁₁)
      with complete-elaboration-synth gc ec x₈
    ... | ih1 , () , ih3
    complete-elaboration-ana gc (ECCase ec ec₁ ec₂) tc (EACase {Δ = Δ} {Δ1 = Δ1} {Δ2 = Δ2} x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ MSSum x₁₀ x₁₁)
      with complete-elaboration-synth gc ec x₈
    ... | ih1 , TCSum ih2 ih4 , ih3  with complete-elaboration-ana (gcomp-extend gc ih2 x₆) ec₁ tc x₁₀
    ... | ih1' , ih2' , ih3' with complete-elaboration-ana (gcomp-extend gc ih4 x₇) ec₂ tc x₁₁
    ... | ih1'' , ih2'' , ih3'' = DCCase (DCCast ih1 (TCSum ih2 ih4) (TCSum ih2 ih4)) (DCCast ih1' ih2' tc) (DCCast ih1'' ih2'' tc) , tc , tr (λ qq → qq ∪ (Δ1 ∪ Δ2) == ∅) (! ih3) (tr (λ qq → ∅ ∪ (qq ∪ Δ2) == ∅) (! ih3') (tr (λ qq → ∅ ∪ (∅ ∪ qq) == ∅) (! ih3'') refl))

    -- this is just a convenience since it shows up a few times above
    comp-ana : ∀{Γ e τ d τ' Δ} →
               Γ gcomplete →
               Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
               d dcomplete →
               τ' tcomplete
    comp-ana gc ex dc = complete-ta gc (π2 (typed-elaboration-ana ex)) dc

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

open import level using (lsuc)
open import sum using (_,_ ; proj₁)
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.isomorphism.core using (_≅_ ; module _≅_)
open import hott.equivalence.core

-- mapping from equality to function
coerce : ∀ {i} {X Y : Set i} → X ≡ Y → X → Y
coerce refl = id

coerce-equiv : ∀ {i} {X Y : Set i} → (p : X ≡ Y) → weak-equiv (coerce p)
coerce-equiv refl x = (x , refl) , λ { (.x , refl) → refl }

coerce-hom : ∀ {i} {X Y Z : Set i}
           → (p : X ≡ Y)(q : Y ≡ Z)
           → coerce (p · q) ≡ coerce q ∘ coerce p
coerce-hom refl q = refl

-- mapping from propositional equality to weak equivalence
≡⇒≈ : ∀ {i} {X Y : Set i} → X ≡ Y → X ≈ Y
≡⇒≈ p = coerce p , coerce-equiv p

Univalence : ∀ i → Set (lsuc i)
Univalence i = {X Y : Set i} → weak-equiv $ ≡⇒≈ {X = X} {Y = Y}

postulate univalence : ∀ {i} → Univalence i

private
  module Properties {i} {X Y : Set i} where
    uni-equiv : (X ≡ Y) ≈ (X ≈ Y)
    uni-equiv = ≡⇒≈ , univalence

    uni-iso : (X ≡ Y) ≅ (X ≈ Y)
    uni-iso = ≈⇒≅ uni-equiv
    open _≅_ uni-iso public using ()
      renaming (from to ≈⇒≡)

    uni-coherence : (f : X ≈ Y) → coerce (≈⇒≡ f) ≡ proj₁ f
    uni-coherence f = begin
        coerce (≈⇒≡ f)
      ≡⟨ refl ⟩
        proj₁ (≡⇒≈ (≈⇒≡ f))
      ≡⟨ ap proj₁ (iso₂ f) ⟩
        proj₁ f
      ∎
      where
        open ≡-Reasoning
        open _≅_ uni-iso using (iso₂)

open Properties public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Luau.Type where

open import FFI.Data.Maybe using (Maybe; just; nothing; just-inv)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Equality using (cong)
open import FFI.Data.Maybe using (Maybe; just; nothing)

data Type : Set where
  nil : Type
  _⇒_ : Type → Type → Type
  never : Type
  unknown : Type
  boolean : Type
  number : Type
  string : Type
  _∪_ : Type → Type → Type
  _∩_ : Type → Type → Type

data Scalar : Type → Set where

  number : Scalar number
  boolean : Scalar boolean
  string : Scalar string
  nil : Scalar nil

lhs : Type → Type
lhs (T ⇒ _) = T
lhs (T ∪ _) = T
lhs (T ∩ _) = T
lhs nil = nil
lhs never = never
lhs unknown = unknown
lhs number = number
lhs boolean = boolean
lhs string = string

rhs : Type → Type
rhs (_ ⇒ T) = T
rhs (_ ∪ T) = T
rhs (_ ∩ T) = T
rhs nil = nil
rhs never = never
rhs unknown = unknown
rhs number = number
rhs boolean = boolean
rhs string = string

_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
nil ≡ᵀ nil = yes refl
nil ≡ᵀ (S ⇒ T) = no (λ ())
nil ≡ᵀ never = no (λ ())
nil ≡ᵀ unknown = no (λ ())
nil ≡ᵀ number = no (λ ())
nil ≡ᵀ boolean = no (λ ())
nil ≡ᵀ (S ∪ T) = no (λ ())
nil ≡ᵀ (S ∩ T) = no (λ ())
nil ≡ᵀ string = no (λ ())
(S ⇒ T) ≡ᵀ string = no (λ ())
never ≡ᵀ string = no (λ ())
unknown ≡ᵀ string = no (λ ())
boolean ≡ᵀ string = no (λ ())
number ≡ᵀ string = no (λ ())
(S ∪ T) ≡ᵀ string = no (λ ())
(S ∩ T) ≡ᵀ string = no (λ ())
(S ⇒ T) ≡ᵀ nil = no (λ ())
(S ⇒ T) ≡ᵀ (U ⇒ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
(S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl
(S ⇒ T) ≡ᵀ (U ⇒ V) | _ | no p = no (λ q → p (cong rhs q))
(S ⇒ T) ≡ᵀ (U ⇒ V) | no p | _ = no (λ q → p (cong lhs q))
(S ⇒ T) ≡ᵀ never = no (λ ())
(S ⇒ T) ≡ᵀ unknown = no (λ ())
(S ⇒ T) ≡ᵀ number = no (λ ())
(S ⇒ T) ≡ᵀ boolean = no (λ ())
(S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ())
(S ⇒ T) ≡ᵀ (U ∩ V) = no (λ ())
never ≡ᵀ nil = no (λ ())
never ≡ᵀ (U ⇒ V) = no (λ ())
never ≡ᵀ never = yes refl
never ≡ᵀ unknown = no (λ ())
never ≡ᵀ number = no (λ ())
never ≡ᵀ boolean = no (λ ())
never ≡ᵀ (U ∪ V) = no (λ ())
never ≡ᵀ (U ∩ V) = no (λ ())
unknown ≡ᵀ nil = no (λ ())
unknown ≡ᵀ (U ⇒ V) = no (λ ())
unknown ≡ᵀ never = no (λ ())
unknown ≡ᵀ unknown = yes refl
unknown ≡ᵀ number = no (λ ())
unknown ≡ᵀ boolean = no (λ ())
unknown ≡ᵀ (U ∪ V) = no (λ ())
unknown ≡ᵀ (U ∩ V) = no (λ ())
number ≡ᵀ nil = no (λ ())
number ≡ᵀ (T ⇒ U) = no (λ ())
number ≡ᵀ never = no (λ ())
number ≡ᵀ unknown = no (λ ())
number ≡ᵀ number = yes refl
number ≡ᵀ boolean = no (λ ())
number ≡ᵀ (T ∪ U) = no (λ ())
number ≡ᵀ (T ∩ U) = no (λ ())
boolean ≡ᵀ nil = no (λ ())
boolean ≡ᵀ (T ⇒ U) = no (λ ())
boolean ≡ᵀ never = no (λ ())
boolean ≡ᵀ unknown = no (λ ())
boolean ≡ᵀ boolean = yes refl
boolean ≡ᵀ number = no (λ ())
boolean ≡ᵀ (T ∪ U) = no (λ ())
boolean ≡ᵀ (T ∩ U) = no (λ ())
string ≡ᵀ nil = no (λ ())
string ≡ᵀ (x ⇒ x₁) = no (λ ())
string ≡ᵀ never = no (λ ())
string ≡ᵀ unknown = no (λ ())
string ≡ᵀ boolean = no (λ ())
string ≡ᵀ number = no (λ ())
string ≡ᵀ string = yes refl
string ≡ᵀ (U ∪ V) = no (λ ())
string ≡ᵀ (U ∩ V) = no (λ ())
(S ∪ T) ≡ᵀ nil = no (λ ())
(S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
(S ∪ T) ≡ᵀ never = no (λ ())
(S ∪ T) ≡ᵀ unknown = no (λ ())
(S ∪ T) ≡ᵀ number = no (λ ())
(S ∪ T) ≡ᵀ boolean = no (λ ())
(S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
(S ∪ T) ≡ᵀ (S ∪ T) | yes refl | yes refl = yes refl
(S ∪ T) ≡ᵀ (U ∪ V) | _ | no p = no (λ q → p (cong rhs q))
(S ∪ T) ≡ᵀ (U ∪ V) | no p | _ = no (λ q → p (cong lhs q))
(S ∪ T) ≡ᵀ (U ∩ V) = no (λ ())
(S ∩ T) ≡ᵀ nil = no (λ ())
(S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ())
(S ∩ T) ≡ᵀ never = no (λ ())
(S ∩ T) ≡ᵀ unknown = no (λ ())
(S ∩ T) ≡ᵀ number = no (λ ())
(S ∩ T) ≡ᵀ boolean = no (λ ())
(S ∩ T) ≡ᵀ (U ∪ V) = no (λ ())
(S ∩ T) ≡ᵀ (U ∩ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
(S ∩ T) ≡ᵀ (U ∩ V) | yes refl | yes refl = yes refl
(S ∩ T) ≡ᵀ (U ∩ V) | _ | no p = no (λ q → p (cong rhs q))
(S ∩ T) ≡ᵀ (U ∩ V) | no p | _ = no (λ q → p (cong lhs q))

_≡ᴹᵀ_ : ∀ (T U : Maybe Type) → Dec(T ≡ U)
nothing ≡ᴹᵀ nothing = yes refl
nothing ≡ᴹᵀ just U = no (λ ())
just T ≡ᴹᵀ nothing = no (λ ())
just T ≡ᴹᵀ just U with T ≡ᵀ U
(just T ≡ᴹᵀ just T) | yes refl = yes refl
(just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q))

src : Type → Type
src nil = never
src number = never
src boolean = never
src string = never
src (S ⇒ T) = S
src (S ∪ T) = (src S) ∩ (src T)
src (S ∩ T) = (src S) ∪ (src T)
src never = unknown
src unknown = never

tgt : Type → Type
tgt nil = never
tgt (S ⇒ T) = T
tgt never = never
tgt unknown = unknown
tgt number = never
tgt boolean = never
tgt string = never
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
tgt (S ∩ T) = (tgt S) ∩ (tgt T)

optional : Type → Type
optional nil = nil
optional (T ∪ nil) = (T ∪ nil)
optional T = (T ∪ nil)

normalizeOptional : Type → Type
normalizeOptional (S ∪ T) with normalizeOptional S | normalizeOptional T
normalizeOptional (S ∪ T) | (S′ ∪ nil) | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | S′         | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | (S′ ∪ nil) | T′         = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | S′         | nil        = optional S′
normalizeOptional (S ∪ T) | nil        | T′         = optional T′
normalizeOptional (S ∪ T) | S′         | T′         = S′ ∪ T′
normalizeOptional T = T

max_stars_repo_name: MeltzDev/luau

max_issues_repo_name: MeltzDev/luau

max_forks_repo_name: MeltzDev/luau


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

module LogicalTopology where
  open import Basics

  open import lib.types.Truncation

  -- For convenience, we define the "power type" ℘ A
  ℘ : {i : ULevel} (j : ULevel) (A : Type i) → Type _
  ℘ j A = A → Prop j

  _∩_ : {i j k : ULevel} {A : Type i}
        → ℘ j A → ℘ k A → ℘ _ A
  U ∩ V = λ a → (U a) ∧ (V a)

  _∪_ : ∀ {i j k} {A : Type i}
        → ℘ j A → ℘ k A → ℘ _ A
  P ∪ Q = λ a → (P a) ∨ (Q a)

  ⋃ : {i j : ULevel} {A : Type i}
      {I : Type j} (U : I → ℘ (lmax i j) A)
      → ℘ _ A
  ⋃ U = λ a → ∃ₚ λ i → (U i a)

  infix 30 _⊆_
  _⊆_ : ∀ {i j k} {A : Type i} (P : ℘ j A) (Q : ℘ k A)
        → Prop _
  _⊆_ {A = A} P Q = ∀ₚ \(a : A) → (P a) ⇒ (Q a)

  -- The definition of logically (Penon) open.
  _is-open : {i j : ULevel} {A : Type i} (U : ℘ j A) → Type (lmax i j)
  U is-open = ∀ x y → (p : (U x) holds) → ∥ (x ≠ y) ⊔ ((U y) holds) ∥

  _is-closed : ∀ {i j} {A : Type i} (U : ℘ j A) → Type (lmax i j)
  C is-closed = (not ∘ C) is-open

  maps-are-cts : {i j k : ULevel} {A : Type i} {B : Type j}
                 {f : A → B} {U : ℘ k B} (p : U is-open)
                 → (U ∘ f) is-open
  maps-are-cts {A = A} {f = f} {U = U} p x y q =
    let[ p' ]:= (p (f x) (f y) q) in-
      [ (case₀ ⊔→ case₁) p' ]
    where
      case₀ : (f x ≠ f y) → x ≠ y
      case₀ ne p = ne (ap f p)

      case₁ : (U (f y)) holds → (U (f y)) holds
      case₁ z = z

  maps-are-cts-closed : {i j k : ULevel} {A : Type i} {B : Type j}
                        {f : A → B} {C : ℘ k B} (p : C is-closed)
                        → (C ∘ f) is-closed
  maps-are-cts-closed {C = C} = maps-are-cts {U = not ∘ C}

  unions-of-opens-are-open : {i j : ULevel} {A : Type i}
                             {I : Type j} (U : I → ℘ _ A)
                             (o : (i : I) → (U i) is-open)
                             → (⋃ U) is-open
  unions-of-opens-are-open U o x y p = -- Supposing that x is in ⋃ U,
    let[ q ]:= p in- -- We know that x is in some particular U i (i ≡ fst q), so
      let[ z ]:= (o (fst q) x y (snd q)) in- -- we use the open-ness of U i to split into two cases
           [ z |> -- z : (x ≠ y) ⊔ (U i y) holds
             ((idf (x ≠ y)) -- Case₀: x already isn't y
                   ⊔→
             ((λ (w : U (fst q) y holds) → -- Case₁: y is in U i and therefore ⋃ U
               [ (fst q) , w ])))
           ]

  _is-logically-connected : ∀ {i j} {A : Type i} (U : ℘ j A) → Prop _
  _is-logically-connected {j = j} {A = A} U =
    ∀ₚ λ (P : ℘ j A) → (U ⊆ (P ∪ (not ∘ P)))
                     ⇒ ((U ⊆ P) ∨ (U ⊆ not ∘ P))

  _is-detachable : ∀ {i j} {A : Type i} (P : ℘ j A) → Prop _
  _is-detachable {A = A} P =
    ∀ₚ λ (a : A) → (P a) ∨ (not $ P a)

  _is-inhabited : ∀ {i j} {A : Type i} (P : ℘ j A) → Prop _
  _is-inhabited {A = A} P =
    ∃ₚ λ (a : A) → P a

  _is-logical-ctd-cmp : ∀ {i j} {A : Type i} (P : ℘ j A) → Prop _
  P is-logical-ctd-cmp =
    (P is-inhabited) ∧
    (P is-detachable) ∧
    (P is-logically-connected)

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

{-
In this module, we show that languages are represented by causal stream
functions.

To this end, let A be a non-empty set (the alphabet) and 2 the
Booleans. For a stream s, we denote the list of the first n elements in
s by s ↓ n and by s[n] the element at the n-th position of s.

A function f : Aω → 2ω from streams over A to Boolean streams is
_causal_, if for all natural numbers n : ℕ and streams s,t : Aω, if
s ↓ n = t ↓ n implies that F(s)[n] = F(t)[n]. We denote by
  C(Aω,2ω) = {f : Aω → 2ω | F causal}
the set of all causal stream functions.

A _language_ is a subset of A⋆, the set of finite words over A. Thus the set
of all languages over A is given by the function space A⋆ → 2.

Now we can show that C(Aω,2ω) ≅ A⋆ → 2 by establishing an isomorphism
  α : (A⋆ → 2) → C(Aω,2ω)
with its inverse
  β : C(Aω,2ω) → (A⋆ → 2).

This explains, why the set of languages is the final coalgebra for the
functor F = 2 × (A → Id).
The coinductive extension of a coalgebra c : X → F X is thereby given by
  ĉ : X → C(Aω,2ω)
  (ĉ x s)[0] = c₁ x
  (ĉ x s)'   = ĉ (c₂ x s[0]) s'
where cᵢ = πᵢ ∘ c.
-}

module CausIsLang where

open import Size
open import Function
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
open ≡-Reasoning

open import Data.Bool using (Bool)
open import Data.List
open import Data.Nat
open import Data.Product

open import Stream

-- Convenience

∥_∥ : ∀ {a} {A : Set a} → List A → ℕ
∥ l ∥ = length l

_⋆ : Set → Set
A ⋆ = List A

ε : ∀{A} → A ⋆
ε = []

-- Non-empty sets
record NonEmptyS (A : Set) : Set where
  field
    x : A

-- | Causal stream functions
record Causal (A B : Set) : Set where
  field
    F : Stream {∞} A → Stream {∞} B
    caus : ∀ {n : ℕ} {s t : Stream A} →
           s ↓ (1 + n) ≡ t ↓ (1 + n) → (F s) at n ≡ (F t) at n

record IsCaus {A B : Set} (f : Stream A → Stream B) : Set where
  coinductive
  field
    out : ∀ {s t} →
          hd s ≡ hd t →
          hd (f s) ≡ hd (f t)
          × (IsCaus (λ x → tl (f(scons (hd s) x))))

open IsCaus public

foo : ∀{A : Set} {x y : A} {u v : List A} → _≡_ {A = List A} (x ∷ u) (y ∷ v) → x ≡ y
foo refl = refl

bar : ∀{A : Set} {x y : A} {u v : List A} → _≡_ {A = List A} (x ∷ u) (y ∷ v) → u ≡ v
bar refl = refl

-- Cheat!
postulate
  baz : ∀{A} (s : Stream A) → s ≡ scons (hd s) (tl s)

lem : ∀{A B} {f : Stream A → Stream B} → IsCaus f →
      ∀ {n s t} → s ↓ (1 + n) ≡ t ↓ (1 + n) → (f s) at n ≡ (f t) at n
lem caus {zero} sn=tn = proj₁ (IsCaus.out caus (foo sn=tn))
lem caus {suc n} {s} {t} sn=tn with IsCaus.out caus {s} {t} (foo sn=tn)
lem {f = f} caus {suc n} {s} {t} sn=tn | p , q =
  let r = q
      u = bar sn=tn
      v = lem r u
  in
    begin
      tl (f s) at n
    ≡⟨ cong (λ x → tl (f x) at n) (baz s) ⟩
      tl (f (scons (hd s) (tl s))) at n
    ≡⟨ v ⟩
      tl (f (scons (hd s) (tl t))) at n
    ≡⟨ cong (λ x → tl (f (scons x (tl t))) at n) (foo sn=tn) ⟩
      tl (f (scons (hd t) (tl t))) at n
    ≡⟨ cong (λ x → tl (f x) at n) (sym (baz t)) ⟩
      tl (f t) at n
    ∎

lem₂ : ∀{A B} {f : Stream A → Stream B} →
       (∀ {n s t} → s ↓ (1 + n) ≡ t ↓ (1 + n) → (f s) at n ≡ (f t) at n) →
       IsCaus f
out (lem₂ p) q = p {0} (cong (λ x → x ∷ []) q) , lem₂ {!x!}

lang-to-caus : ∀{A} → (A ⋆ → Bool) → (Stream A → Stream Bool)
hd (lang-to-caus L s) = L ε
tl (lang-to-caus L s) = lang-to-caus (λ w → L (hd s ∷ w)) (tl s)

lang-to-caus-explicit : ∀{A} {L : A ⋆ → Bool} {s : Stream A} →
                        (n : ℕ) → (lang-to-caus L s) at n ≡ L(s ↓ n)
lang-to-caus-explicit zero = refl
lang-to-caus-explicit {A} {L} {s} (suc n) =
  begin
    (lang-to-caus L s) at (suc n)
  ≡⟨ refl ⟩
    hd (δ (suc n) (lang-to-caus L s))
  ≡⟨ refl ⟩
    hd (δ n (tl (lang-to-caus L s)))
  ≡⟨ refl ⟩
    hd (δ n (lang-to-caus (λ w → L (hd s ∷ w)) (tl s)))
  ≡⟨ refl ⟩
   (lang-to-caus (λ w → L (hd s ∷ w)) (tl s)) at n
  ≡⟨ lang-to-caus-explicit n ⟩
    (λ w → L (hd s ∷ w))((tl s) ↓ n)
  ≡⟨ refl ⟩
    L (hd s ∷ ((tl s) ↓ n))
  ≡⟨ refl ⟩
    L (s ↓ (suc n))
  ∎

lang-to-caus-is-causal : ∀{A} {L : A ⋆ → Bool} →
                         ∀ {n : ℕ} {s t : Stream A} →
                         s ↓ n ≡ t ↓ n →
                         (lang-to-caus L s) at n ≡ (lang-to-caus L t) at n
lang-to-caus-is-causal {A} {L} {n} {s} {t} p =
  begin
    (lang-to-caus L s) at n
  ≡⟨ lang-to-caus-explicit n ⟩
    L(s ↓ n)
  ≡⟨ cong (λ u → L u) p ⟩
    L(t ↓ n)
  ≡⟨ sym (lang-to-caus-explicit n) ⟩
    (lang-to-caus L t) at n
  ∎

-- Isomorphisms between languages and causal stream transformations

α : ∀{A} → (A ⋆ → Bool) → (Causal A Bool)
α L = record
  { F = lang-to-caus L
  ; caus = lang-to-caus-is-causal
  }

β : ∀{A} {p : NonEmptyS A} → (Causal A Bool) → (A ⋆ → Bool)
β {A} {p} F′ w =
  let open Causal F′
  in F (w ++ˢ repeat (NonEmptyS.x p)) at ∥ w ∥

lemma-restr-extension-to-length-is-id :
  ∀ {A} {s : Stream A} (w : A ⋆) →
  (w ++ˢ s) ↓ ∥ w ∥ ≡ w
lemma-restr-extension-to-length-is-id         []      = refl
lemma-restr-extension-to-length-is-id {A} {s} (a ∷ w) =
  begin
    ((a ∷ w) ++ˢ s) ↓ ∥ a ∷ w ∥
  ≡⟨ refl ⟩
    ((a ∷ w) ++ˢ s) ↓ (suc ∥ w ∥)
  ≡⟨ refl ⟩
    (hd ((a ∷ w) ++ˢ s)) ∷ ((tl ((a ∷ w) ++ˢ s)) ↓ ∥ w ∥)
  ≡⟨ refl ⟩
    a ∷ ((tl ((a ∷ w) ++ˢ s)) ↓ ∥ w ∥)
  ≡⟨ refl ⟩
    a ∷ ((w ++ˢ s) ↓ ∥ w ∥)
  ≡⟨ cong (λ u → a ∷ u) (lemma-restr-extension-to-length-is-id w) ⟩
    a ∷ w
  ∎

{-
lemma-β-indep-of-choice : ∀ {A} {F′ : Causal A Bool}
                            {p q : NonEmptyS A} {w : A ⋆} →
                          β {A} {p} F′ w ≡ β {A} {q} F′ w
lemma-β-indep-of-choice {A} {F′} {p} {q} {w} =
  let
    open Causal F′
    n = ∥ w ∥
    x = NonEmptyS.x p
    y = NonEmptyS.x q
  in begin
    β {A} {p} F′ w
  ≡⟨ refl ⟩
    F (w ++ˢ repeat x) at n
  ≡⟨ caus {n} {(w ++ˢ repeat x)} {(w ++ˢ repeat y)}
          (trans (lemma-restr-extension-to-length-is-id w)
                 (sym (lemma-restr-extension-to-length-is-id w))) ⟩
    F (w ++ˢ repeat y) at n
  ≡⟨ refl ⟩
    β {A} {q} F′ w
  ∎

lang-iso-caus→ : ∀{A} {p : NonEmptyS A} {L : A ⋆ → Bool} (w : A ⋆) →
                 β {A} {p} (α L) w ≡ L w
lang-iso-caus→             []      = refl
lang-iso-caus→ {A} {p} {L} (a ∷ w) =
  let
    F′ = α L
    F = Causal.F F′
    n = ∥ w ∥
    x = NonEmptyS.x p
    s = (a ∷ w) ++ˢ repeat x
    K = (λ w → L (hd s ∷ w))
    G′ = α K
    G = Causal.F G′
  in begin
    β F′ (a ∷ w)
  ≡⟨ refl ⟩
    F ((a ∷ w) ++ˢ repeat x) at (suc n)
  ≡⟨ refl ⟩
    F s at (suc n)
  ≡⟨ refl ⟩
    lang-to-caus L s at (suc n)
  ≡⟨ refl ⟩
    hd (δ (suc n) (lang-to-caus L s))
  ≡⟨ refl ⟩
    hd (δ n (tl (lang-to-caus L s)))
  ≡⟨ refl ⟩
    tl (lang-to-caus L s) at n
  ≡⟨ refl ⟩
    lang-to-caus (λ w → L (hd s ∷ w)) (tl s) at n
  ≡⟨ refl ⟩
    G (tl s) at n
  ≡⟨ refl ⟩
    G (w ++ˢ repeat x) at n
  ≡⟨ refl ⟩
    β G′ w
  ≡⟨ refl ⟩
    β (α K) w
  ≡⟨ lang-iso-caus→ w ⟩
    K w
  ≡⟨ refl ⟩
    L (a ∷ w)
  ∎

-- This doesn't work as long as we don't have a notion of causality
-- that does not depend on explicit indexing.
{-
.lang-iso-caus← : ∀{A} {x : A} {F′ : Causal A Bool} (s : Stream A) →
                 Causal.F (α (β x F′)) s ∼ˢ Causal.F F′ s
hd≡ (lang-iso-caus← {A} {x} {F′} s) =
  let
    F = Causal.F F′
    L = β x F′
    G′ = α L
    G = Causal.F G′
  in begin
    hd (G s)
  ≡⟨ refl ⟩
    hd (lang-to-caus L s)
  ≡⟨ refl ⟩
    L ε
  ≡⟨ refl ⟩
    F (ε ++ˢ repeat x) at ∥ ε {A} ∥
  ≡⟨ refl ⟩
    F (repeat x) at 0
  ≡⟨ refl ⟩
    F (repeat x) at 0
  ≡⟨ Causal.caus F′ {0} {repeat x} {s} refl ⟩
    F s at 0
  ≡⟨ refl ⟩
    hd (F s)
  ∎

tl∼ (lang-iso-caus← {A} {x} {F′} s) =
  let
    F = Causal.F F′
    L = β x F′
    G′ = α L
    G = Causal.F G′
    K = (λ w → L (hd s ∷ w))
  in beginˢ
    tl (G s)
  ∼ˢ⟨ s-bisim-refl ⟩
    tl (lang-to-caus L s)
  ∼ˢ⟨ s-bisim-refl ⟩
    lang-to-caus (λ w → L (hd s ∷ w)) (tl s)
  ∼ˢ⟨ s-bisim-refl ⟩
    lang-to-caus K (tl s)
  ∼ˢ⟨ s-bisim-refl ⟩
    Causal.F (α K) (tl s)
  ∼ˢ⟨ {!!} ⟩
    tl (F s)
  ∎ˢ
-}

lemma-length-restr : ∀ {A} {s : Stream A} (n : ℕ) → ∥ (s ↓ n) ∥ ≡ n
lemma-length-restr         zero    = refl
lemma-length-restr {A} {s} (suc n) =
  begin
    ∥ (s ↓ (suc n)) ∥
  ≡⟨ refl ⟩
    ∥ hd s ∷ ((tl s) ↓ n) ∥
  ≡⟨ refl ⟩
    suc ∥ (tl s) ↓ n ∥
  ≡⟨ cong (λ u → suc u) (lemma-length-restr n) ⟩
    suc n
  ∎

lang-iso-caus← : ∀ {A} {p : NonEmptyS A} {F′ : Causal A Bool} {s : Stream A}
                   (n : ℕ) → Causal.F (α (β F′)) s at n ≡ Causal.F F′ s at n
lang-iso-caus← {A} {p} {F′} {s} n =
  let
    F = Causal.F F′
    L = β F′
  in begin
    Causal.F (α L) s at n
  ≡⟨ refl ⟩
    lang-to-caus L s at n
  ≡⟨ lang-to-caus-explicit n ⟩
    L (s ↓ n)
  ≡⟨ refl ⟩
    F ((s ↓ n) ++ˢ repeat x) at ∥ s ↓ n ∥
  ≡⟨ Causal.caus F′ {∥ s ↓ n ∥} {(s ↓ n) ++ˢ repeat x} {s} lemma-restr-ext ⟩
    F s at  ∥ (s ↓ n) ∥
  ≡⟨ cong (λ u → F s at u) (lemma-length-restr n) ⟩
    F s at n
  ∎
  where
    x = NonEmptyS.x p

    lemma-restr-ext : ((s ↓ n) ++ˢ repeat x) ↓ ∥ s ↓ n ∥ ≡ s ↓ ∥ s ↓ n ∥
    lemma-restr-ext =
      begin
        ((s ↓ n) ++ˢ repeat x) ↓ ∥ s ↓ n ∥
      ≡⟨ lemma-restr-extension-to-length-is-id (s ↓ n) ⟩
        s ↓ n
      ≡⟨ cong (λ u → s ↓ u) (sym (lemma-length-restr n)) ⟩
        s ↓ ∥ s ↓ n ∥
      ∎
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{- Conatural number properties (Tesla Ice Zhang et al., Feb. 2019)

This file defines operations and properties on conatural numbers:

- Infinity (∞).

- Proof that ∞ + 1 is equivalent to ∞.

- Proof that conatural is an hSet.

- Bisimulation on conatural

- Proof that bisimulation is equivalent to equivalence (Coinductive Proof
  Principle).

- Proof that this bisimulation is prop valued

The standard library also defines bisimulation on conaturals:

https://github.com/agda/agda-stdlib/blob/master/src/Codata/Conat/Bisimilarity.agda
-}

{-# OPTIONS --safe --guardedness #-}
module Cubical.Codata.Conat.Properties where

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
  renaming (Bool→Type to ⟨_⟩)

import Cubical.Data.Nat as Nat
import Cubical.Data.Nat.Order.Recursive as Nat

open import Cubical.Core.Everything

open import Cubical.Functions.Embedding

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Relation.Nullary
open import Cubical.Codata.Conat.Base

import Cubical.Axiom.Omniscience as Omni

Unwrap-prev : Conat′ → Type₀
Unwrap-prev  zero   = Unit
Unwrap-prev (suc _) = Conat

unwrap-prev : (n : Conat′) -> Unwrap-prev n
unwrap-prev  zero   = _
unwrap-prev (suc x) = x

private -- tests
  𝟘 = conat zero
  𝟙  = succ 𝟘
  𝟚  = succ 𝟙

  succ𝟙≡𝟚 : succ 𝟙 ≡ 𝟚
  succ𝟙≡𝟚 i = 𝟚

  pred𝟚≡𝟙 : unwrap-prev (force 𝟚) ≡ 𝟙
  pred𝟚≡𝟙 i = 𝟙

∞ : Conat
force ∞ = suc ∞

∞+1≡∞ : succ ∞ ≡ ∞
force (∞+1≡∞ _) = suc ∞

∞+2≡∞ : succ (succ ∞) ≡ ∞
∞+2≡∞ = (cong succ ∞+1≡∞) ∙ ∞+1≡∞

_+_ : Conat → Conat → Conat
_+′_ : Conat′ → Conat → Conat′

force (x + y) = force x +′ y
zero +′ y = force y
suc x +′ y = suc (x + y)

n+∞≡∞ : ∀ n → n + ∞ ≡ ∞
n+′∞≡∞′ : ∀ n → n +′ ∞ ≡ suc ∞

force (n+∞≡∞ n i) = n+′∞≡∞′ (force n) i
n+′∞≡∞′ zero = refl
n+′∞≡∞′ (suc n) = λ i → suc (n+∞≡∞ n i)

∞+∞≡∞ : ∞ + ∞ ≡ ∞
force (∞+∞≡∞ i) = suc (∞+∞≡∞ i)

+-zeroˡ : ∀ n → 𝟘 + n ≡ n
force (+-zeroˡ n _) = force n

+-zeroʳ : ∀ n → n + 𝟘 ≡ n
+′-zeroʳ : ∀ n → n +′ 𝟘 ≡ n

force (+-zeroʳ n i) = +′-zeroʳ (force n) i
+′-zeroʳ zero _ = zero
+′-zeroʳ (suc n) i = suc (+-zeroʳ n i)

+-assoc : ∀ m n p → (m + n) + p ≡ m + (n + p)
+′-assoc : ∀ m n p → (m +′ n) +′ p ≡ m +′ (n + p)

force (+-assoc m n p i) = +′-assoc (force m) n p i
+′-assoc zero _ _ = refl
+′-assoc (suc m) n p i = suc (+-assoc m n p i)

conat-absurd : ∀ {y : Conat} {ℓ} {Whatever : Type ℓ} → zero ≡ suc y → Whatever
conat-absurd eq = ⊥.rec (transport (cong diag eq) tt)
  where
  diag : Conat′ → Type₀
  diag zero = Unit
  diag (suc _) = ⊥

embed : Nat.ℕ → Conat
embed Nat.zero .force = zero
embed (Nat.suc n) .force = suc (embed n)

embed-inj : ∀ m n → embed m ≡ embed n → m ≡ n
embed-inj m n p with ⊎Path.encode _ _ (cong force p)
embed-inj Nat.zero Nat.zero _ | _ = refl
embed-inj (Nat.suc m) (Nat.suc n) _ | lift q
  = cong Nat.suc (embed-inj m n q)

embed≢∞ : ∀ n → embed n ≡ ∞ → ⊥
embed≢∞ Nat.zero = lower ∘ ⊎Path.encode _ _ ∘ cong force
embed≢∞ (Nat.suc n) = embed≢∞ n ∘ lower ∘ ⊎Path.encode _ _ ∘ cong force

cover : Nat.ℕ → Conat
cover Nat.zero = ∞
cover (Nat.suc n) = embed n

cover-inj : ∀ m n → cover m ≡ cover n → m ≡ n
cover-inj Nat.zero Nat.zero _ = refl
cover-inj (Nat.suc m) (Nat.suc n) p = cong Nat.suc (embed-inj m n p)
cover-inj Nat.zero (Nat.suc n) = ⊥.rec ∘ embed≢∞ n ∘ sym
cover-inj (Nat.suc m) Nat.zero = ⊥.rec ∘ embed≢∞ m

module IsSet where
  ≡-stable  : {x y : Conat} → Stable (x ≡ y)
  ≡′-stable : {x y : Conat′} → Stable (x ≡ y)

  force (≡-stable ¬¬p i) = ≡′-stable (λ ¬p → ¬¬p (λ p → ¬p (cong force p))) i
  ≡′-stable {zero}  {zero}  ¬¬p′ = refl
  ≡′-stable {suc x} {suc y} ¬¬p′ =
     cong′ suc (≡-stable λ ¬p → ¬¬p′ λ p → ¬p (cong pred′′ p))
  ≡′-stable {zero}  {suc y} ¬¬p′ = ⊥.rec (¬¬p′ conat-absurd)
  ≡′-stable {suc x} {zero}  ¬¬p′ = ⊥.rec (¬¬p′ λ p → conat-absurd (sym p))

  isSetConat : isSet Conat
  isSetConat _ _ = Separated→isSet (λ _ _ → ≡-stable) _ _

  isSetConat′ : isSet Conat′
  isSetConat′ m n p′ q′ = cong (cong force) (isSetConat (conat m) (conat n) p q)
    where p = λ where i .force → p′ i
          q = λ where i .force → q′ i

module Bisimulation where
  open IsSet using (isSetConat)

  record _≈_ (x y : Conat) : Type₀
  data _≈′_ (x y : Conat′) : Type₀
  _≈′′_ : Conat′ → Conat′ → Type₀
  zero  ≈′′ zero  = Unit
  suc x ≈′′ suc y = x ≈ y
  -- So impossible proofs are preserved
  x ≈′′ y = ⊥

  record _≈_ x y where
    coinductive
    field prove : force x ≈′ force y

  data _≈′_  x y where
    con : x ≈′′ y → x ≈′ y

  open _≈_ public

  bisim : ∀ {x y} → x ≈ y → x ≡ y
  bisim′ : ∀ {x y} → x ≈′ y → x ≡ y

  bisim′ {zero} {zero} (con tt) = refl
  bisim′ {zero} {suc x} (con ())
  bisim′ {suc x} {zero} (con ())
  bisim′ {suc x} {suc y} (con eq) i = suc (bisim eq i)
  force (bisim eq i) = bisim′ (prove eq) i

  misib : ∀ {x y} → x ≡ y → x ≈ y
  misib′ : ∀ {x y} → x ≡ y → x ≈′ y

  misib′ {zero} {zero} _ = con tt
  misib′ {zero} {suc x} = conat-absurd
  misib′ {suc x} {zero} p = conat-absurd (sym p)
  -- misib′ {suc x} {suc y} p = con λ where .prove → misib′ (cong pred′ p)
  misib′ {suc x} {suc y} p = con (misib (cong pred′′ p))
  prove (misib x≡y) = misib′ (cong force x≡y)

  iso″ : ∀ {x y} → (p : x ≈ y) → misib (bisim p) ≡ p
  iso′ : ∀ {x y} → (p : x ≈′ y) → misib′ (bisim′ p) ≡ p

  iso′ {zero} {zero} (con p) = refl
  iso′ {zero} {suc x} (con ())
  iso′ {suc x} {zero} (con ())
  iso′ {suc x} {suc y} (con p) = cong con (iso″ p)
  prove (iso″ p i) = iso′ (prove p) i

  osi : ∀ {x y} → (p : x ≡ y) → bisim (misib p) ≡ p
  osi p = isSetConat _ _ _ p

  path≃bisim : ∀ {x y} → (x ≡ y) ≃ (x ≈ y)
  path≃bisim = isoToEquiv (iso misib bisim iso″ osi)

  path≡bisim : ∀ {x y} → (x ≡ y) ≡ (x ≈ y)
  path≡bisim = ua path≃bisim

  isProp≈ : ∀ {x y} → isProp (x ≈ y)
  isProp≈ = subst isProp path≡bisim (isSetConat _ _)

module WLPO where
  -- search a decidable predicate on ℕ for the first true
  search : (Nat.ℕ → Bool) → Conat
  search′ : (Nat.ℕ → Bool) → Bool → Conat′

  search f .force = search′ f (f 0)

  search′ _  true = zero
  search′ f false = suc (search (f ∘ Nat.suc))

  -- the constantly false predicate searches to ∞
  search-false : search (const false) ≡ ∞
  search-false i .force = suc (search-false i)

  wrap : Conat′ → Conat
  wrap zero = ∞
  wrap (suc m) = m

  search-lemma : ∀ α n → search α ≡ ∞ → α n ≡ false
  search-lemma α Nat.zero p with α 0 | cong force p
  ... | false | q = refl
  ... | true | q = ⊥.rec (⊎Path.encode zero (suc ∞) q .lower)
  search-lemma α (Nat.suc n) p with α 0 | cong force p
  ... | false | q = search-lemma (α ∘ Nat.suc) n (cong wrap q)
  ... |  true | q = ⊥.rec (⊎Path.encode zero (suc ∞) q .lower)

  search-n : ∀ α n → search α ≡ embed n → α n ≡ true
  search-n α Nat.zero p with α 0 | ⊎Path.encode _ _ (cong force p)
  ... |  true | _ = refl
  search-n α (Nat.suc n) p with α 0 | ⊎Path.encode _ _ (cong force p)
  ... | false | q = search-n (α ∘ Nat.suc) n (q .lower)

  module _ (f : Conat → Nat.ℕ) (emb : isEmbedding f) where
    discreteConat : Discrete Conat
    discreteConat
      = Embedding-into-Discrete→Discrete (f , emb) Nat.discreteℕ

    wlpo' : Omni.WLPO' Nat.ℕ
    wlpo' α with discreteConat (search α) ∞
    ... | yes p = yes λ i n → search-lemma α n p i
    ... | no ¬p = no (¬p ∘ _∙ search-false ∘ cong search)

module LPO where
  open WLPO using (search; search-lemma; search-n)

  module Un (uncover : Conat → Nat.ℕ) (sect : section cover uncover) where
    search-0 : ∀ α → uncover (search α) ≡ 0 → ∀ n → α n ≡ false
    search-0 α p n
      = search-lemma α n (sym (sect (search α)) ∙ cong cover p)

    search-n' : ∀ α n → uncover (search α) ≡ Nat.suc n → α n ≡ true
    search-n' α n p = search-n α n (sym (sect (search α)) ∙ cong cover p)

    -- So, surjectivity of `cover` implies LPO, since `cover` has
    -- already been shown injective, and surjectivity would make it an
    -- equivalence (as ℕ and Conat are sets).
    lpo' : Omni.LPO∞ Nat.ℕ
    lpo' α = disc (uncover (search α)) refl where
      disc : ∀ n → uncover (search α) ≡ n → _
      disc Nat.zero p = inl λ n → subst ⟨_⟩ (search-0 α p n)
      disc (Nat.suc n) p = inr (n , subst⁻ ⟨_⟩ (search-n' α n p) _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --universe-polymorphism #-}

module PatternMatchingOnCodata where

data Level : Set where
  zero : Level
  suc  : (i : Level) → Level

_⊔_ : Level → Level → Level
zero  ⊔ j     = j
suc i ⊔ zero  = suc i
suc i ⊔ suc j = suc (i ⊔ j)

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

infix 1000 ♯_

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

my-♭ : ∀ {a} {A : Set a} → ∞ A → A
my-♭ (♯ x) = x


text:
module lemmas where

open import prelude
open import defns

postulate NH-CONG : ∀ {D} (H H′ : NavigationHistory(D)) → let open NavigationHistory H in let open NavigationHistory H′ using () renaming ( A to A′ ; Fo to Fo′ ; Eq to Eq′ ; FTO to FTO′ ) in (A ⊆ A′) → (A′ ⊆ A) → (Fo ≣ Fo′) → (Eq ≣ Eq′) → (FTO ≣ FTO′) → (H ≣ H′)

BT-hd : ∀ {D} {H : NavigationHistory(D)} {n} d (ds : D ^ n) →
  ((d ∷ ds) ∈ BackTarget*(H)) →
  (d ∈ BackTarget(H))
BT-hd {D} {H} {n} d ds d∷ds∈BT with Max-hd ((A ∪ JointSessionPast) ∩ CanGoBack) d ds d∷ds∈BT where open NavigationHistory H
BT-hd {D} {H} {n} d ds d∷ds∈BT | ((in₁ d∈A , d∈CGB), d-max′) = ((d∈A , d∈CGB) , d-max) where

  open NavigationHistory H

  d-max : ∀ e → (e ∈ (A ∩ CanGoBack) → (e ≤ d))
  d-max e (e∈A , e∈CGB) = d-max′ e ((in₁ e∈A) , e∈CGB)

BT-hd {D} {H} {n} d ds d∷ds∈BT | ((in₂ (a , (a∈A , (d<a , d~a))) , d∈CGB), d-max) = contradiction (<-impl-≱ d<a (d-max a ((in₁ a∈A) , (d , (d<a , d~a))))) where open NavigationHistory H

BT-tl : ∀ {D} {H : NavigationHistory(D)} {n} d d∈CGB (ds : D ^ n) →
  ((d ∷ ds) ∈ BackTarget*(H)) →
  (ds ∈ BackTarget*(H traverse-from d ∵ d∈CGB))
BT-tl {D} {H} {n} d d∈CGB ds d∷ds∈BT with Max-tl ((A ∪ JointSessionPast) ∩ CanGoBack) d ds d∷ds∈BT where open NavigationHistory H
BT-tl {D} {H} {n} d d∈CGB ds d∷ds∈BT | ((d>ds , (ds↓ , ds∈BT′)) , ds-max′) with max(SessionPast(d)) ∵ d∈CGB where open NavigationHistory H
BT-tl {D} {H} {n} d d∈CGB ds d∷ds∈BT | ((d>ds , (ds↓ , ds∈BT′)) , ds-max′) | (c , ((c<d , c~d) , c-max)) = ((ds↓ , ds∈BT) , ds-max) where

  open NavigationHistory H
  open NavigationHistory (H traverse-to c) using () renaming (A to A′ ; JointSessionPast to JointSessionPast′)

  d∈A : (d ∈ A)
  d∈A with BT-hd {H = H} d ds d∷ds∈BT
  d∈A | ((d∈A , _) , _) = d∈A

  d-max : ∀ e → (e ∈ (A ∩ CanGoBack) → (e ≤ d))
  d-max with BT-hd {H = H} d ds d∷ds∈BT
  d-max | ((_ , _) , d-max) = d-max

  lemma : (Past(d) ∩ ((A ∪ JointSessionPast) ∩ CanGoBack)) ⊆ ((A′ ∪ JointSessionPast′) ∩ CanGoBack)
  lemma e  (e<d , (_                              , e∈CGB)) with c ~? e
  lemma e  (e<d , (_                              , e∈CGB)) | in₁ c~e with ≤-total c e
  lemma e  (e<d , (_                              , e∈CGB)) | in₁ c~e | in₁ c≤e with ≤-asym c≤e (c-max e (e<d , ~-trans (~-sym c~e) c~d))
  lemma ._ (e<d , (_                              , e∈CGB)) | in₁ c~e | in₁ c≤e | refl = ((in₁ (in₂ refl)) , e∈CGB)
  lemma e  (e<d , (_                              , e∈CGB)) | in₁ c~e | in₂ e<c = (in₂ (_ , (in₂ refl , (e<c , ~-sym c~e))) , e∈CGB)
  lemma e  (e<d , (in₁ e∈A                        , e∈CGB)) | in₂ c≁e = ((in₁ (in₁ (c≁e , e∈A))) , e∈CGB)
  lemma e  (e<d , (in₂ (a , (a∈A ,  (e<a , e~a))) , e∈CGB)) | in₂ c≁e = (in₂ (a , (in₁ ((λ c~a → c≁e (~-trans c~a (~-sym e~a))) , a∈A) , (e<a , e~a))) , e∈CGB)

  lemma′ : ((A′ ∪ JointSessionPast′) ∩ CanGoBack) ⊆ ((A ∪ JointSessionPast) ∩ CanGoBack)
  lemma′ e  (in₁ (in₁ (c≁e , e∈A)) , e∈CGB) = ((in₁ e∈A) , e∈CGB)
  lemma′ ._ (in₁ (in₂ refl) , c∈CGB) = ((in₂ (d , (d∈A , (c<d , c~d)))) , c∈CGB)
  lemma′ e (in₂ (a , (in₁ (c≁a , a∈A) , e≲a)) , e∈CGB) = (in₂ (a , (a∈A , e≲a)) , e∈CGB)
  lemma′ e (in₂ (._ , (in₂ refl , e≲c)) , e∈CGB) = ((in₂ (d , (d∈A , ≲-trans e≲c (c<d , c~d)))) , e∈CGB)

  lemma″ : ((A′ ∪ JointSessionPast′) ∩ CanGoBack) ⊆ (Past(d))
  lemma″ e  (in₁ (in₁ (c≁e , e∈A)) , e∈CGB) = (d-max e (e∈A , e∈CGB) , (λ e≡d → c≁e (~-trans c~d (≡-impl-~ (sym e≡d)))))
  lemma″ ._ (in₁ (in₂ refl) , c∈CGB) = c<d
  lemma″ e (in₂ (a , (in₁ (c≁a , a∈A) , e≲a)) , e∈CGB) = <-trans-≤ (≲-impl-< e≲a) (d-max a (a∈A , (e , e≲a)))
  lemma″ e (in₂ (._ , (in₂ refl , (e<c , e~c))) , e∈CGB) = <-trans e<c c<d

  ds∈BT : ds ∈ All((A′ ∪ JointSessionPast′) ∩ CanGoBack)
  ds∈BT = All-resp-⊆ lemma ds (All-resp-∩ ds (d>ds , ds∈BT′))

  ds-max : ∀ es → (es ∈ (Decreasing ∩ All((A′ ∪ JointSessionPast′) ∩ CanGoBack))) → (es ≤* ds)
  ds-max es (es↓ , es∈BT′) = ds-max′ es (All-resp-⊆ lemma″ es es∈BT′ , (es↓ , All-resp-⊆ lemma′ es es∈BT′))

BT-nil :  ∀ {D} {H : NavigationHistory(D)} →
  (nil ∈ BackTarget*(H))
BT-nil = ((tt , tt) , λ { nil (tt , tt) → tt })

BT-cons : ∀ {D} {H : NavigationHistory(D)} {n} d d∈CGB (ds : D ^ n) →
  (d ∈ BackTarget(H)) →
  (ds ∈ BackTarget*(H traverse-from d ∵ d∈CGB)) →
  ((d ∷ ds) ∈ BackTarget*(H))
BT-cons {D} {H} d d∈CGB ds ((d∈A , _) , d-max) ((ds↓ , ds∈JSP′∩CGB) , ds-max) with max(SessionPast(d)) ∵ d∈CGB where open NavigationHistory H
BT-cons {D} {H} d d∈CGB ds ((d∈A , _) , d-max) ((ds↓ , ds∈JSP′∩CGB) , ds-max) | (c , ((c<d , c~d) , c-max)) = (((d<ds , ds↓) , (((in₁ d∈A) , d∈CGB) , All-resp-⊆ lemma′ ds ds∈JSP′∩CGB)) , d∷ds-max) where

  open NavigationHistory H
  open NavigationHistory (H traverse-to c) using () renaming (A to A′ ; JointSessionPast to JointSessionPast′)

  lemma : (Past(d) ∩ ((A ∪ JointSessionPast) ∩ CanGoBack)) ⊆ ((A′ ∪ JointSessionPast′) ∩ CanGoBack)
  lemma e  (e<d , (_                              , e∈CGB)) with c ~? e
  lemma e  (e<d , (_                              , e∈CGB)) | in₁ c~e with ≤-total c e
  lemma e  (e<d , (_                              , e∈CGB)) | in₁ c~e | in₁ c≤e with ≤-asym c≤e (c-max e (e<d , ~-trans (~-sym c~e) c~d))
  lemma ._ (e<d , (_                              , e∈CGB)) | in₁ c~e | in₁ c≤e | refl = ((in₁ (in₂ refl)) , e∈CGB)
  lemma e  (e<d , (_                              , e∈CGB)) | in₁ c~e | in₂ e<c = (in₂ (_ , (in₂ refl , (e<c , ~-sym c~e))) , e∈CGB)
  lemma e  (e<d , (in₁ e∈A                        , e∈CGB)) | in₂ c≁e = ((in₁ (in₁ (c≁e , e∈A))) , e∈CGB)
  lemma e  (e<d , (in₂ (a , (a∈A ,  (e<a , e~a))) , e∈CGB)) | in₂ c≁e = (in₂ (a , (in₁ ((λ c~a → c≁e (~-trans c~a (~-sym e~a))) , a∈A) , (e<a , e~a))) , e∈CGB)

  lemma′ : ((A′ ∪ JointSessionPast′) ∩ CanGoBack) ⊆ ((A ∪ JointSessionPast) ∩ CanGoBack)
  lemma′ e  (in₁ (in₁ (c≁e , e∈A)) , e∈CGB) = ((in₁ e∈A) , e∈CGB)
  lemma′ ._ (in₁ (in₂ refl) , c∈CGB) = ((in₂ (d , (d∈A , (c<d , c~d)))) , c∈CGB)
  lemma′ e (in₂ (a , (in₁ (c≁a , a∈A) , e≲a)) , e∈CGB) = (in₂ (a , (a∈A , e≲a)) , e∈CGB)
  lemma′ e (in₂ (._ , (in₂ refl , e≲c)) , e∈CGB) = ((in₂ (d , (d∈A , ≲-trans e≲c (c<d , c~d)))) , e∈CGB)

  lemma″ : ((A′ ∪ JointSessionPast′) ∩ CanGoBack) ⊆ (Past(d))
  lemma″ e  (in₁ (in₁ (c≁e , e∈A)) , e∈CGB) = (d-max e (e∈A , e∈CGB) , (λ e≡d → c≁e (~-trans c~d (≡-impl-~ (sym e≡d)))))
  lemma″ ._ (in₁ (in₂ refl) , c∈CGB) = c<d
  lemma″ e (in₂ (a , (in₁ (c≁a , a∈A) , e≲a)) , e∈CGB) = <-trans-≤ (≲-impl-< e≲a) (d-max a (a∈A , (e , e≲a)))
  lemma″ e (in₂ (._ , (in₂ refl , (e<c , e~c))) , e∈CGB) = <-trans e<c c<d

  d<ds : (ds ∈ All(Past(d)))
  d<ds = All-resp-⊆ lemma″ ds ds∈JSP′∩CGB

  d∷ds-max : ∀ es → es ∈ (Decreasing ∩ All ((A ∪ JointSessionPast) ∩ CanGoBack)) → (es ≤* (d ∷ ds))
  d∷ds-max (e ∷ es) ((es<e , es↓) , ((e∈A∪JSP , e∈CGB) , es∈A∪JSP∩CGB)) = (e≤d , es≤ds) where

    lemma‴ : ∀ f → (f ∈ ((A ∪ JointSessionPast) ∩ CanGoBack)) → (f ≤ d)
    lemma‴ f (in₁ f∈A , f∈CGB) = d-max f (f∈A , f∈CGB)
    lemma‴ f (in₂ (a , (a∈A , ((f≤a , f≠a) , f~a))) , f∈CGB) = ≤-trans f≤a (d-max a (a∈A , (f , ((f≤a , f≠a) , f~a))))

    e≤d : (e ≤ d)
    e≤d = lemma‴ e (e∈A∪JSP , e∈CGB)

    es<d : es ∈ All(Past(d))
    es<d = All-resp-⊆ (λ f f<e → <-trans-≤ f<e e≤d) es es<e

    es≤ds : es ≤* ds
    es≤ds = ds-max es (es↓ , All-resp-⊆ lemma es (All-resp-∩ es (es<d , es∈A∪JSP∩CGB)))

fwd? : ∀ {D} {H : NavigationHistory(D)} {δ} (ds : D ^ δ) →
  (ds ∈ FwdTarget*(H)) →
  (H traverses-by (+ve δ) to (H traverses-to ds))
fwd? {D} {H} {δ = zero} nil nil∈FT = back nil tt (BT-nil {H = H})
fwd? {D} {H} {δ = succ δ} ds ds∈FT = fwd ds ds∈FT

FT-hd : ∀ {D} {H : NavigationHistory(D)} {n} d (ds : D ^ n) →
  ((d ∷ ds) ∈ FwdTarget*(H)) →
  (d ∈ FwdTarget(H))
FT-hd {D} {H} d ds (((d<ds , ds↑) , (d∈JSF , ds∈JSF)) , d∷ds-min) = (d∈JSF , d-min) where

  open NavigationHistory H

  d-min : ∀ e → (e ∈ JointSessionFuture) → (d ≤ e)
  d-min e e∈JSF with ≤-total d e
  d-min e e∈JSF | in₁ d≤e = d≤e
  d-min e e∈JSF | in₂ e<d with d∷ds-min (e ∷ ds) (((All-resp-⊆ (λ f → <-trans e<d) ds d<ds) , ds↑) , (e∈JSF , ds∈JSF))
  d-min e e∈JSF | in₂ e<d | (d≤e , ds≤ds) = d≤e

FT-tl : ∀ {D} {H : NavigationHistory(D)} {n} d (ds : D ^ n) →
  ((d ∷ ds) ∈ FwdTarget*(H)) →
  (ds ∈ FwdTarget*(H traverse-to d))
FT-tl {D} {H} d ds (((d<ds , ds↑) , ((a , (a∈A , (a<d , a~d))) , ds∈JSF)) , d∷ds-min) = ((ds↑ , ds∈JSF′) , ds-min) where

  H′ = (H traverse-to d)

  open NavigationHistory H
  open NavigationHistory H′ using () renaming (JointSessionFuture to JointSessionFuture′)

  lemma : ((Future(d) ∩ JointSessionFuture) ⊆ JointSessionFuture′)
  lemma e (d<e , (b , (b∈A , (b<e , b~e)))) with d ~? b
  lemma e (d<e , (b , (b∈A , (b<e , b~e)))) | in₁ d~b = (d , (in₂ refl , (d<e , (~-trans d~b b~e))))
  lemma e (d<e , (b , (b∈A , (b<e , b~e)))) | in₂ d≁b = (b , (in₁ (d≁b , b∈A) , (b<e , b~e)))

  lemma′ : (JointSessionFuture′ ⊆ Future(d))
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) with ≤-total e d
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) | in₁ e≤d with d∷ds-min (e ∷ ds) (((All-resp-⊆ (λ f → ≤-trans-< e≤d) ds d<ds) , ds↑) , ((b , (b∈A , (b<e , b~e))) , ds∈JSF))
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) | in₁ e≤d | (d≤e , ds≤ds) = contradiction (d≁b (~-trans (≡-impl-~ (≤-asym d≤e e≤d)) (~-sym b~e)))
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) | in₂ d<e = d<e
  lemma′ e (.d , (in₂ refl        , (d<e , d~e))) = d<e

  lemma″ : (JointSessionFuture′ ⊆ JointSessionFuture)
  lemma″ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) = (b , (b∈A , (b<e , b~e)))
  lemma″ e (.d , (in₂ refl        , (d<e , d~e))) = a , (a∈A , (<-trans a<d d<e , ~-trans a~d d~e))

  ds∈JSF′ : (ds ∈ All(JointSessionFuture′))
  ds∈JSF′ = All-resp-⊆ lemma ds (All-resp-∩ ds (d<ds , ds∈JSF))

  ds-min : ∀ es → (es ∈ (Increasing ∩ All(JointSessionFuture′))) → (ds ≤* es)
  ds-min es (es↑ , es∈JSF′) with d∷ds-min (d ∷ es) ((d<es , es↑) , ((a , (a∈A , (a<d , a~d))) , es∈JSF)) where

    d<es : es ∈ All(Future(d))
    d<es = All-resp-⊆ lemma′ es es∈JSF′

    es∈JSF : es ∈ All(JointSessionFuture)
    es∈JSF = All-resp-⊆ lemma″ es es∈JSF′

  ds-min es (es↑ , es∈JSF′) | (d≤d , ds≤es) = ds≤es

FT-nil :  ∀ {D} {H : NavigationHistory(D)} →
  (nil ∈ FwdTarget*(H))
FT-nil = ((tt , tt) , λ { nil (tt , tt) → tt })

FT-cons : ∀ {D} {H : NavigationHistory(D)} {n} d (ds : D ^ n) →
  (d ∈ FwdTarget(H)) →
  (ds ∈ FwdTarget*(H traverse-to d)) →
  ((d ∷ ds) ∈ FwdTarget*(H))
FT-cons {D} {H} d ds ((a , (a∈A , (a<d , a~d))) , d-min) ((ds↑ , ds∈JSF′) , ds-min) = (((d<ds , ds↑) , ((a , (a∈A , (a<d , a~d))) , ds∈JSF)) , d∷ds-min) where

  H′ = (H traverse-to d)

  open NavigationHistory H
  open NavigationHistory H′ using () renaming (JointSessionFuture to JointSessionFuture′)

  lemma : ((Future(d) ∩ JointSessionFuture) ⊆ JointSessionFuture′)
  lemma e (d<e , (b , (b∈A , (b<e , b~e)))) with d ~? b
  lemma e (d<e , (b , (b∈A , (b<e , b~e)))) | in₁ d~b = (d , (in₂ refl , (d<e , (~-trans d~b b~e))))
  lemma e (d<e , (b , (b∈A , (b<e , b~e)))) | in₂ d≁b = (b , (in₁ (d≁b , b∈A) , (b<e , b~e)))

  lemma′ : (JointSessionFuture′ ⊆ Future(d))
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) with ≤-total e d
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) | in₁ e≤d with d-min e (b , (b∈A , (b<e , b~e)))
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) | in₁ e≤d | d≤e = contradiction (d≁b (~-trans (≡-impl-~ (≤-asym d≤e e≤d)) (~-sym b~e)))
  lemma′ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) | in₂ d<e = d<e
  lemma′ e (.d , (in₂ refl        , (d<e , d~e))) = d<e

  lemma″ : (JointSessionFuture′ ⊆ JointSessionFuture)
  lemma″ e (b  , (in₁ (d≁b , b∈A) , (b<e , b~e))) = (b , (b∈A , (b<e , b~e)))
  lemma″ e (.d , (in₂ refl        , (d<e , d~e))) = (a , (a∈A , (<-trans a<d d<e , ~-trans a~d d~e)))

  d<ds : ds ∈ All(Future(d))
  d<ds = All-resp-⊆ lemma′ ds ds∈JSF′

  ds∈JSF : ds ∈ All(JointSessionFuture)
  ds∈JSF = All-resp-⊆ lemma″ ds ds∈JSF′

  d∷ds-min : ∀ es → (es ∈ (Increasing ∩ All(JointSessionFuture))) → ((d ∷ ds) ≤* es)
  d∷ds-min (e ∷ es) ((e<es , es↑) , (e∈JSF , es∈JSF)) = (d≤e , ds≤es) where

    d≤e : (d ≤ e)
    d≤e = d-min e e∈JSF

    d<es : es ∈ All(Future(d))
    d<es = All-resp-⊆ (λ f → ≤-trans-< d≤e) es e<es

    es∈JSF′ : (es ∈ All(JointSessionFuture′))
    es∈JSF′ = All-resp-⊆ lemma es (All-resp-∩ es (d<es , es∈JSF))

    ds≤es : (ds ≤* es)
    ds≤es = ds-min es (es↑ , es∈JSF′)

from-to : ∀ {D} {H : NavigationHistory(D)} d e d∈CGB →
  (WellFormed(H)) →
  (d ∈ BackTarget(H)) →
  (e ∈ FwdTarget(H traverse-from d ∵ d∈CGB)) →
  (H ≣ ((H traverse-from d ∵ d∈CGB) traverse-to e))
from-to {D} {H} d e d∈CGB H∈WF ((d∈A , _) , d-max) e∈FT′ with lemma e∈FT′ where

  H′ = (H traverse-from d ∵ d∈CGB)

  open NavigationHistory H
  open NavigationHistory H′ using () renaming (JointSessionFuture to JointSessionFuture′ ; FwdTarget to FwdTarget′)

  lemma : (e ∈ FwdTarget′) → (d ≡ e)
  lemma (e∈JSP′ , e-min) with max(SessionPast(d)) ∵ d∈CGB | ≤-total d e
  lemma (e∈JSP′ , e-min) | (c , ((c<d , c~d) , c-max)) | in₁ d≤e = ≤-asym d≤e (e-min d (c , (in₂ refl , (c<d , c~d))))
  lemma ((a  , (in₁ (c≁a , a∈A) , (a<e , a~e))) , e-min) | c , ((c<d , c~d) , c-max) | in₂ e<d = contradiction (<-impl-≱ e<d (H∈WF (a<e , a~e) (c<d , c~d) a∈A d∈A))
  lemma ((.c , (in₂ refl , (c<e , c~e))) , e-min) | c , ((c<d , c~d) , c-max) | in₂ e<d = contradiction (<-impl-≱ c<e (c-max e (e<d , ~-trans (~-sym c~e) c~d)))

from-to {D} {H} d .d d∈CGB H∈WF ((d∈A , _) , d-max) e∈FT′ | refl = H=H″ where

  H′ = (H traverse-from d ∵ d∈CGB)
  H″ = (H′ traverse-to d)

  open NavigationHistory H
  open NavigationHistory H″ using () renaming (A to A″)

  A⊆A″ : (A ⊆ A″)
  A⊆A″ f f∈A with d ~? f
  A⊆A″ f f∈A | in₁ d~f with active-~-impl-≡ d∈A f∈A d~f
  A⊆A″ .d  _ | in₁ d~f | refl = in₂ refl
  A⊆A″ f f∈A | in₂ d≁f with max(SessionPast(d)) ∵ d∈CGB
  A⊆A″ f f∈A | in₂ d≁f | (c , ((c<d , c~d) , c-max)) = in₁ (d≁f , (in₁ ((λ c~f → d≁f (~-trans (~-sym c~d) c~f)) , f∈A)))

  A″⊆A : (A″ ⊆ A)
  A″⊆A f (in₁ (d≁f , in₁ (c≁f , f∈A))) = f∈A
  A″⊆A ._ (in₁ (d≁c , in₂ refl)) with max(SessionPast(d)) ∵ d∈CGB
  A″⊆A ._ (in₁ (d≁c , in₂ refl)) | (c , ((c<d , c~d) , c-max)) = contradiction (d≁c (~-sym c~d))
  A″⊆A ._ (in₂ refl) = d∈A

  H=H″ : (H ≣ H″)
  H=H″ = NH-CONG H H″ A⊆A″ A″⊆A REFL REFL REFL

to-from : ∀ {D} {H : NavigationHistory(D)} d e e∈CGB →
  (WellFormed(H)) →
  (d ∈ FwdTarget(H)) →
  (e ∈ BackTarget(H traverse-to d)) →
  (H ≣ ((H traverse-to d) traverse-from e ∵ e∈CGB))
to-from {D} {H} d e e∈CGB H∈WF ((a , (a∈A , (a<d , a~d))) , d-min) e∈BT′ with lemma e∈BT′ | max(SessionPast(e)) ∵ e∈CGB where

  H′ = (H traverse-to d)

  open NavigationHistory H
  open NavigationHistory H′ using () renaming (BackTarget to BackTarget′)

  lemma : (e ∈ BackTarget′) → (d ≡ e)
  lemma ((in₁ (d≁e , e∈A) , (b , (b<e , b~e))) , e-max) = ≤-asym d≤e e≤d where

    d≤e : (d ≤ e)
    d≤e = e-max d (in₂ refl , (a , (a<d , a~d)))

    e≤d : (e ≤ d)
    e≤d = H∈WF (a<d , a~d) (b<e , b~e) a∈A e∈A

  lemma ((in₂ d≡e , _) , _) = d≡e

to-from {D} {H} d .d d∈CGB H∈WF ((a , (a∈A , (a<d , a~d))) , d-min) (_ , d-max) | refl | (c , ((c<d , c~d) , c-max)) with ≤-asym a≤c c≤a where

  open NavigationHistory H

  c≤a : (c ≤ a)
  c≤a with ≤-total c a
  c≤a | in₁ c≤a = c≤a
  c≤a | in₂ a<c = contradiction (<-impl-≱ (<-trans-≤ c<d (d-min c (a , (a∈A , (a<c , (~-trans a~d (~-sym c~d))))))) ≤-refl)

  a≤c : (a ≤ c)
  a≤c = c-max a (a<d , a~d)

to-from {D} {H} d .d d∈CGB H∈WF ((a , (a∈A , (a<d , a~d))) , d-min) (_ , d-max) | refl | (.a , ((_ , _) , a-max)) | refl = H=H″ where

  H′ = (H traverse-to d)
  H″ = (H′ traverse-to a)

  open NavigationHistory H
  open NavigationHistory H″ using () renaming (A to A″)

  A⊆A″ : (A ⊆ A″)
  A⊆A″ f f∈A with a ~? f
  A⊆A″ f f∈A | in₁ a~f = in₂ (active-~-impl-≡ a∈A f∈A (~-trans (~-trans a~d (~-sym a~d)) a~f))
  A⊆A″ f f∈A | in₂ a≁f = in₁ (a≁f , (in₁ ((λ d~f → a≁f (~-trans a~d d~f)) , f∈A)))

  A″⊆A : (A″ ⊆ A)
  A″⊆A f  (in₁ (_ , in₁ (_ , f∈A))) = f∈A
  A″⊆A .d (in₁ (a≁d , in₂ refl)) = contradiction (a≁d a~d)
  A″⊆A .a (in₂ refl) = a∈A

  H=H″ : (H ≣ H″)
  H=H″ = NH-CONG H H″ A⊆A″ A″⊆A REFL REFL REFL

fwd-WF : ∀ {D} (H : NavigationHistory(D)) e →
  WellFormed(H) →
  (e ∈ FwdTarget(H)) →
  WellFormed(H traverse-to e)
fwd-WF H e H∈WF ((f , (f∈A , f≲e)) , e-min) a≲b c≲d (in₁ (e≁a , a∈A)) (in₁ (e≁d , d∈A)) = H∈WF a≲b c≲d a∈A d∈A
fwd-WF H e H∈WF ((f , (f∈A , f≲e)) , e-min) a≲b c≲e (in₁ (e≁a , a∈A)) (in₂ refl)        = e-min _ (_ , (a∈A , a≲b))
fwd-WF H e H∈WF ((f , (f∈A , f≲e)) , e-min) e≲b c≲d (in₂ refl)        (in₁ (e≁d , d∈A)) = H∈WF (≲-trans f≲e e≲b) c≲d f∈A d∈A where open NavigationHistory H
fwd-WF H e H∈WF ((f , (f∈A , f≲e)) , e-min) e≲b c≲e (in₂ refl)        (in₂ refl)        = e-min _ (f , (f∈A , ≲-trans f≲e e≲b)) where open NavigationHistory H

back-WF : ∀ {D} (H : NavigationHistory(D)) e e∈CGB →
  WellFormed(H) →
  (e ∈ BackTarget(H)) →
  WellFormed(H traverse-from e ∵ e∈CGB)
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (a<b , a~b) c≲d a∈A′              d∈A′              with max(SessionPast(e)) ∵ e∈CGB where open NavigationHistory H
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (a<b , a~b) c≲d (in₁ (f≁a , a∈A)) (in₁ (f≁d , d∈A)) | (f , ((f<e , f~e) , f-max)) = H∈WF (a<b , a~b) c≲d a∈A d∈A
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (a<b , a~b) c≲f (in₁ (f≁a , a∈A)) (in₂ refl)        | (f , ((f<e , f~e) , f-max)) = ≤-trans (<-impl-≤ f<e) (H∈WF (a<b , a~b) (f<e , f~e) a∈A e∈A) where open NavigationHistory H
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max) {b = b} (f<b , f~b) c≲d (in₂ refl)        (in₁ (f≁d , d∈A)) | (f , ((f<e , f~e) , f-max)) with ≤-total b e | ≤-total e b where open NavigationHistory H
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (f<b , f~b) c≲d (in₂ refl)        (in₁ (f≁d , d∈A)) | (f , ((f<e , f~e) , f-max)) | in₁ b≤e | in₁ e≤b with ≤-asym b≤e e≤b where open NavigationHistory H
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (f<b , f~b) c≲d (in₂ refl)        (in₁ (f≁d , d∈A)) | (f , ((f<e , f~e) , f-max)) | in₁ b≤e | in₁ e≤b | refl = e-max _ (d∈A , (_ , c≲d))
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (f<b , f~b) c≲d (in₂ refl)        (in₁ (f≁d , d∈A)) | (f , ((f<e , f~e) , f-max)) | in₁ b≤e | in₂ b<e = contradiction (<-impl-≱ f<b (f-max _ (b<e , ~-trans (~-sym f~b) f~e))) where open NavigationHistory H
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (f<b , f~b) c≲d (in₂ refl)        (in₁ (f≁d , d∈A)) | (f , ((f<e , f~e) , f-max)) | in₂ e<b | _ = H∈WF (e<b , ~-trans (~-sym f~e) f~b) c≲d e∈A d∈A where open NavigationHistory H
back-WF H e e∈CGB H∈WF ((e∈A , _) , e-max)         (f<b , f~b) c≲f (in₂ refl)        (in₂ refl)        | (f , ((f<e , f~e) , f-max)) = <-impl-≤ f<b where open NavigationHistory H

max_stars_repo_name: cbrewster/ServoNavigation

max_issues_repo_name: cbrewster/ServoNavigation

max_forks_repo_name: cbrewster/ServoNavigation


text:
open import FRP.LTL.RSet.Core using ( RSet ; ⟦_⟧ )
open import FRP.LTL.RSet.Stateless using ( _⇒_ )
open import FRP.LTL.Time using ( _≤_ ; ≤-refl ; _≤-trans_ )

module FRP.LTL.RSet.Globally where

-- □ A is "A holds globally in the future"

□ : RSet → RSet
□ A t = ∀ {u} → (t ≤ u) → A u

-- Comonad structure of □

extend : ∀ {A B} → ⟦ A ⇒ B ⟧ → ⟦ □ A ⇒ □ B ⟧
extend f a s≤t = f (a s≤t)

extract : ∀ {A} → ⟦ □ A ⇒ A ⟧
extract a = a ≤-refl

duplicate : ∀ {A} → ⟦ □ A ⇒ □ (□ A) ⟧
duplicate a s≤t t≤u = a (s≤t ≤-trans t≤u)

-- Applicative structure of □

[_] : ∀ {A} → ⟦ A ⟧ → ⟦ □ A ⟧
[ a ] s≤t = a

_⟨*⟩_ : ∀ {A B} → ⟦ □ (A ⇒ B) ⇒ □ A ⇒ □ B ⟧
(f ⟨*⟩ a) s≤t = f s≤t (a s≤t)

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl