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

open import Function using (_$_)
open import Data.Bool
import Data.String as String

open import Leftovers.TraverseTerm
open import Leftovers.Utils

import Level as Level
open import Reflection
open import Reflection.Term
open import Reflection.TypeChecking.Monad.Instances
open import Reflection.Argument using (unArg)

open import Data.Fin using (toℕ ; Fin)

open import Data.Unit
open import Data.Nat as Nat hiding (_⊓_)
open import Data.Nat.Show as NShow
open import Data.Product
open import Data.List as List
import Data.Vec as Vec
open import Data.Vec using (Vec)
import Data.Vec.Categorical as VCat

import Data.List.Categorical
open Data.List.Categorical.TraversableM {m = Level.zero} tcMonad

open import Data.Maybe using (just ; nothing)

open import Function.Nary.NonDependent
open import Data.Product.Nary.NonDependent

open import Category.Monad.State
import Category.Monad as Monad

open import Level.Literals using (#_)

import Data.Fin.Reflection

import Leftovers.Monad as L

data Holes (n : ℕ) (levels : Levels n) (sets : Sets n levels ) : Set (⨆ n levels)    where
  makeHoles : Product n sets → Holes n levels sets

getHoles : ∀ {n ls sets} → Holes n ls sets → Product n sets
getHoles (makeHoles p) = p
{-# INLINE getHoles #-}

nthHole : ∀ n {ls} {as : Sets n ls } k → Holes n ls as → Projₙ as k
nthHole n k h = projₙ n k (getHoles h)
{-# INLINE nthHole #-}

infixr 10 _∥_

_∥_ : ∀ {n : ℕ} {levels : Levels n} {sets : Sets n levels}
   {ℓ} {X : Set ℓ} →
  Holes n levels sets → X →
  Holes (suc n) (ℓ , levels) (X , sets)
_∥_ {n = zero} {sets = sets} {X = X} holes x = makeHoles x
_∥_ {n = suc n} {sets = sets} {X = X} holes x = makeHoles (x , getHoles holes)

-- fillHoles : ∀ {ℓ} {n} {ls} {types : Sets n ls} {T : Set ℓ} → (Holes n ls types → T) → Product n types → T
-- fillHoles f args = f (makeHoles args)

-- quoteSets {n = suc n} (x Vec.∷ v) = app (app (quoteTerm (_,_   {A = Set} {B = λ x₁ → Sets n (proj₂ nSet)}  )) x) (quoteSets v)

-- record MetaInContext : Set where
--   constructor Cmeta
--   field
--     context : LCxt
--     unapplied : Term
--     applied : Term
--
--
open import Agda.Builtin.Nat using (_-_)

--Given a hole, infer its function type,
--taking anything in the hole's context that's not in the current context
-- as an argument
inferHoleType : L.Hole → TC Type
inferHoleType hole = do
  currentContext ← getContext
  let
    numExtras = (List.length (L.Hole.context hole)) - (List.length currentContext)
    extras = List.take numExtras (L.Hole.context hole)
  holeType ← inContext (L.Hole.context hole) (inferType (L.Hole.hole hole))
  addArrows extras holeType
  where
    open import Agda.Builtin.Nat
    addArrows : List (Arg Type) → Term → TC Type
    addArrows [] holeType = return holeType
    addArrows (x ∷ extras) holeType = do
      rec ← addArrows extras holeType
      return (pi x (abs "ctx" rec))

data Dummy : Set where
  dummy : Dummy

sep : Term → TC Term
sep t = do
  debugPrint "" 2 (strErr "Finding sep for " ∷ strErr (showTerm t) ∷ [])
  ty ← inferType t
  debugPrint "" 2 (strErr "sep got type " ∷ strErr (showTerm ty) ∷ [])
  let ret = (def (quote  identity) [ vArg t ]) ⦂ ty
  return ret

open import Reflection.DeBruijn using (weaken)
open import Leftovers.Everywhere tcMonad

-- Hack using case-lambda to convince Agda that a term is a definition
-- Helps with the termination checker
-- makeDef : Term → TC Term
-- makeDef t = do

--   ty ← inferType t
--   let ret = pat-lam [ clause [] [ vArg (con (quote dummy) []) ] t ] []
--   return (app (def (quote the) (vArg (pi (vArg (quoteTerm Dummy)) (abs "_" (weaken 1 ty))) ∷ vArg ret ∷ [])) (quoteTerm dummy))

getMetas : Term → TC (List L.Hole)
getMetas t = do
    -- body <- newMeta goalType
    debugPrint "Hello" 2 (strErr "Ran macro, body var is " ∷ termErr t ∷ [])
    -- L.runLeftovers (theMacro body)
      --Now we see what holes are left
    let
        handleMetas : _ → Meta → Data.Maybe.Maybe L.Hole
        handleMetas ctx m = just (L.mkHole m (meta m (List.map (λ x → vArg (var x [])) (List.downFrom (length ctx )))) (List.map proj₂ ctx))
    debugPrint "L" 2 (strErr "After ALLMETAS " ∷ [])
      -- debugPrint "L" 2 (strErr "ALLMETAS NORM " ∷ List.map termErr normMetas)
    let metaList =  (collectFromSubterms
                      (record
                        { onVar = λ _ _ → nothing
                        ; onMeta = handleMetas
                        ; onCon = λ _ _ → nothing
                        ; onDef = λ _ _ → nothing }) t
              )
    return (List.deduplicate L.equivDec metaList)

-- Given the size of the starting context, a hole,
-- and the list of parameters to add to the start context,
-- Generate a new hole whose context has the new parameters
-- inserted into the middle.
-- We need this because a meta might occur in a deeper scope than
-- where we're inserting the new variables.
-- weakenMeta : ℕ → List (Arg Type) → L.Hole → L.Hole
-- weakenMeta startSize newParams hole =
--   L.mkHole (Reflection.DeBruijn.weakenFrom (numNew + 1) (length newParams) (L.Hole.hole hole)) fullCtx
--   where
--     numNew = List.length (L.Hole.context hole) - startSize
--     fullCtx : List (Arg Type)
--     fullCtx with (newCtx , startCtx) ← List.splitAt numNew (L.Hole.context hole)
--       = newCtx ++ newParams ++ startCtx

-- Given the length of the current context
-- and a meta in a possibly deeper context
-- return the type of the meta in the original context
-- e.g. a function type abstracting over any new variables
abstractMetaType : ℕ → (L.Hole × Type) → Type
abstractMetaType numStart (hole , ty) =
  foldr (λ param ty → pi param (abs "arg" ty)) ty
    (take (length (L.Hole.context hole) - numStart) (L.Hole.context hole))

-- Given the size of the current context and a list of new parameter types to add
-- freshen all metas to take new parameters and weaken DeBruijn variables accordingly
-- Also forgets any blocked constraints on those metas, since they're replaced by new ones
injectParameters : List Type → List Type → Term → TC Term
injectParameters currentCtx injectedCtx t = everywhere defaultActions freshenMeta  (weaken (length injectedCtx) t)
  where
    freshenMeta : Cxt → Term → TC Term
    freshenMeta innerVars (meta m xs) = do
      mtype ← inferType (meta m xs)
      newMeta mtype
    freshenMeta innerVars t = return t

open import Data.Maybe using (Maybe ; just ; nothing)

record MacroResult : Set where
  constructor macroResult
  field
    body : Term
    numMetas : ℕ
    holes : Vec L.Hole numMetas
    types : Vec Type numMetas
    indexFor : Meta → Maybe (Fin numMetas)

getMacroHoles : Type → List (Arg Type) → (Term → L.Leftovers ⊤) → TC MacroResult
getMacroHoles targetType ctx theMacro = runSpeculative $
      do
        (body , _) ← L.runLeftovers
          ((L.freshMeta targetType) L.>>=
          λ hole → theMacro hole L.>> L.pure hole)
        normBody ← normalise body
        metas ← getMetas normBody
        let metaVec = Vec.fromList metas
        debugPrint "Leftovers" 2 (strErr "All holes " ∷ [])
      -- debugPrint "Leftovers" 2 (strErr "All holes " ∷ List.map (λ m → termErr (L.Hole.hole m)) metas)
      -- Now we know how many arguments we need to take
        debugPrint "Leftovers" 2 (strErr "Unified num holes " ∷ [])
    -- Get the type of each hole *in its context*
        types <- VCat.TraversableM.forM {a = Level.zero} {n = length metas} tcMonad (metaVec)
          λ hole → inContext (L.Hole.context hole ++ ctx) do
             -- debugPrint "" 2 (strErr "Context : " ∷ strErr (String.intersperse ",, " (List.map (λ x → showTerm (unArg x)) (contextForHole hole))) ∷ [])
             debugPrint "" 2 (strErr "Getting type of hole " ∷ termErr ( (L.Hole.hole hole) ) ∷ strErr " !" ∷  [])
             ty ← inferType (L.Hole.hole hole)
             debugPrint "" 2 [ strErr "got type" ]
             return ty
        let indexedHoles = Vec.toList (Vec.zip (Vec.allFin (length metas)) metaVec)
        debugPrint "" 2 (strErr "Indexed holes: " ∷ List.map (λ x → termErr (meta (L.Hole.holeMeta (proj₂ x)) [])) indexedHoles)
        let
          indexForMeta m =
            Data.Maybe.map proj₁ $
              head (filter (λ y → m Meta.≟ L.Hole.holeMeta (proj₂ y)) indexedHoles)
        debugPrint "Hello" 2 (strErr "normalised MacroBody " ∷ termErr normBody ∷ [])
        return (macroResult normBody _ metaVec types indexForMeta , false) -- ((body , metas , types) , false)
        where
          open import Reflection.Meta as Meta

metaToArg : MacroResult → Cxt → Term → TC Term
metaToArg results cxt t@(meta m _) with (MacroResult.indexFor results m)
... | just i = do
  let
    ithHole = Vec.lookup (MacroResult.holes results) i
    numNewInContext = length (L.Hole.context ithHole)
    argNum = (numNewInContext + ((MacroResult.numMetas results - 1) - toℕ i))
  debugPrint "" 2 (strErr "Replacing meta " ∷ strErr (showTerm (meta m [])) ∷ strErr " with arg " ∷ strErr (NShow.show argNum) ∷ [])
  return (var argNum (List.map (λ x → vArg (var x [])) (List.upTo numNewInContext)))
... | nothing = typeError (strErr "Internal Error: unfound meta " ∷ termErr (meta m []) ∷ strErr " when finding Leftover holes" ∷ [])
metaToArg _ _ t = return t

findLeftovers : ∀ {ℓ} → Set ℓ → (Term → L.Leftovers ⊤) → Term → TC ⊤
findLeftovers targetSet theMacro goal =
  do
    startContext ← getContext
    let startCtxLen = List.length startContext
    targetType ← quoteTC targetSet
    -- Unification variable for number of holes, we don't know how many yet
    numHoles ← newMeta (quoteTerm ℕ)
    -- Unification variables for the HVec of holes
    let levelsType = (def (quote Levels) (vArg numHoles ∷ []))
    levels ← newMeta levelsType -- def (quote nSet) [ hArg numHoles ]
    let setsType = (def (quote Sets) (vArg numHoles ∷ vArg levels ∷ []))
    sets ← newMeta setsType
    let productType = def (quote Holes) (vArg numHoles ∷ vArg levels ∷ vArg sets ∷ [])

    -- Make sure the type of the function we produce matches (unifies with)
    -- (Holes -> Target Type)
    let funType = pi (vArg productType) (abs "holes" targetType)
    checkType goal funType
    let extContext = vArg productType ∷ startContext
    let
      contextForHole : L.Hole → List (Arg Type)
      contextForHole hole = (L.Hole.context hole) ++ extContext

    debugPrint "Leftovers" 2 (strErr "Goal function type " ∷ termErr funType ∷ [])
    -- The return type of the function we're producing
    -- (argType , goalAbs) ← case funType of λ
    --   { (pi (arg _ dom) cod) → return (dom , cod)
    --   ; _ → typeError (strErr "Need to give as argument to applyPartial" ∷ [])}
    -- unify productType argType
    -- -- goalType ← extendContext (vArg productType) (newMeta (quoteTerm Set))
    -- unify funType (pi (vArg productType) goalAbs)

    -- Run the given macro on a fresh hole
    -- in a context extended with the argument with the Holes
    debugPrint "Leftovers" 2 (strErr "goalType before run theMacro" ∷ termErr targetType ∷ [])
    result ← getMacroHoles targetType startContext theMacro
    let numMetas = MacroResult.numMetas result
    debugPrint "Leftovers" 2 (strErr "Got holes types " ∷ [])
    -- debugPrint "Hello" 2 (strErr "Got hole types" ∷ List.map termErr (Vec.toList holeTypes))
    let
      abstractedTypes = (Vec.map (abstractMetaType startCtxLen)
            (Vec.zip (MacroResult.holes result) (MacroResult.types result)))
      setsFromTypes =
        quoteSets abstractedTypes
    debugPrint "Hello" 2 (strErr "Made sets " ∷ strErr (showTerm setsFromTypes) ∷ [])
    levelsFromTypes ← quoteLevels abstractedTypes
    debugPrint "Hello" 2 (strErr "Made levels " ∷ strErr (showTerm levelsFromTypes) ∷ [])
      -- Now we know the types of our holes
    unify sets setsFromTypes
    unify levels levelsFromTypes

    --This gives us enough information to make a function parameterized over the types of holes
    --We traverse the result of the macro, replacing each meta with a parameter
    --and wrap the hole thing in an n-ary lambda taking parameters of the hole types
    funBody ← everywhere defaultActions (metaToArg result) (MacroResult.body result)
    sepBody ← inContext (List.map vArg (List.reverse $ Vec.toList abstractedTypes) ++ startContext) $ sep funBody
    -- let sepBody = funBody
    -- Pair each meta with its index
    -- let indexedMetas = (Vec.zip (Vec.allFin _) (Vec.fromList {!!}))
    -- -- Replace the ith meta with the ith element of the HList
    -- forM (Vec.toList indexedMetas) λ ( i , hole ) → inContext (contextForHole hole) do
    --   -- TODO is this bad? why re-infer?
    --     holeType ← inferType (L.Hole.hole hole)
    --     let
    --        holeCtx = L.Hole.context hole
    --        numArgs = length holeCtx
    --        rhs =
    --         (def (quote nthHole)
    --           (vArg (lit (nat (length {!!})))
    --           -- ∷ hArg (quoteTerm nSet)
    --           ∷ hArg (levels ⦂ levelsType)
    --           ∷ hArg (sets ⦂ setsType)
    --           ∷ vArg (Data.Fin.Reflection.toTerm i)
    --           --TODO hidden args for context vars?
    --           ∷ vArg (var numArgs [] ⦂ productType)
    --           ∷ (List.map (λ n → vArg (var n [])) (List.upTo numArgs))))
    --     debugPrint "Hello" 2 (strErr "Unify LHS " ∷ strErr (showTerm (L.Hole.hole hole)) ∷ [] )
    --     debugPrint "Hello" 2 (strErr "Unify RHS " ∷ strErr (showTerm rhs) ∷ [] )
    --     unify (L.Hole.hole hole) (rhs )
    --     debugPrint "" 2 (strErr "done unify" ∷ [])
      --Hack to help with termination
    debugPrint "" 2 (strErr "got fun body " ∷ strErr (showTerm sepBody) ∷ [])
    nflam ← normalise (naryLam numMetas sepBody ⦂ def (quote _⇉_) (vArg sets ∷ vArg targetType ∷ []))
    debugPrint "" 2 (strErr "making fun fun " ∷ strErr (showTerm nflam) ∷ [])
    --Produce the function that gives the result of the last macro
    let finalResult = (lam visible (abs "holes"
                    (app (def (quote uncurryₙ) (vArg numHoles ∷ vArg (naryLam numMetas sepBody) ∷ []))
                    (def (quote getHoles) [ vArg (var 0 []) ])
                    )))
    unify goal finalResult
    debugPrint "Hello" 2 (strErr "Final Result" ∷ termErr finalResult ∷ [])
    -- return tt

  where
    naryLam : ℕ → Term → Term
    naryLam 0 x = x
    naryLam (suc n) x = lam visible (abs ("hole" String.++ NShow.show (suc n)) (naryLam n x))

    quoteLevels : ∀ {n} → Vec.Vec Term n → TC Term
    quoteLevels Vec.[] = return (con (quote Level.lift) (vArg (quoteTerm tt) ∷ []))
    quoteLevels {n = suc n} (x Vec.∷ v) = do
      rec ← quoteLevels {n = n} v
      typeOfType ← inferType x
      let
        theLevel = case typeOfType of λ
          { (sort (set l)) →  l
          ; (sort (lit l)) →  (def (quote #_) (vArg (lit (nat l)) ∷ [] ))
          ;  _ → quoteTerm Level.zero }

      return (con (quote _,_) (vArg theLevel ∷ vArg rec ∷ [] ))

    quoteSets : ∀ {n} → Vec.Vec Term n → Term
    quoteSets Vec.[] = con (quote Level.lift) (vArg (quoteTerm tt) ∷ [])
    quoteSets {n = suc n} (x Vec.∷ v) = (con (quote _,_) (vArg x ∷ vArg (quoteSets v) ∷ [] ))

-- infixr 10 [_⇒_]

by : ∀ {ℓ} {A : Set ℓ} {n} {ls} {types : Sets n ls}
  → (theMacro : Term → L.Leftovers ⊤)
  → {@(tactic findLeftovers A theMacro) f : Holes n ls types → A}
  → Product n types → A
by {n = n} _ {f} x = f (makeHoles x)

by' : ∀ {ℓ} {A : Set ℓ} {n} {ls} {types : Sets n ls}
  → (theMacro : Term → L.Leftovers ⊤)
  → {@(tactic findLeftovers A theMacro) f : Holes n ls types → A}
  → ⊤ → Product n types → A
by' {n = n} _ {f} _ x = f (makeHoles x)

-- by {n = n} _ {f} = curryₙ n (λ x → f (makeHoles x))

open import Relation.Nullary

-- syntax withLeftovers tac x = ► tac ⇒ x ◄
macro
  getNormal : ∀ {X : Set} → X → Term → TC ⊤
  getNormal {X = X} x goal = do
    t ← quoteTC x
    ttype ← quoteTC X
    checkType goal ttype
    debugPrint "" 2 (strErr "get Normal term " ∷ termErr t ∷ [])
    debugPrint "" 2 (strErr "get Normal term type " ∷ termErr ttype ∷ [])
    goalType ← inferType goal
    debugPrint "" 2 (strErr "get Normal goal type " ∷ termErr goalType ∷ [])
    unify goalType ttype
    nf ← normalise t
    nfSimplified ←  everywhere defaultActions action t
    debugPrint "" 2 (strErr "get Normal term nf " ∷ termErr nf ∷ [])
    unify goal nfSimplified
    where
      open import Reflection.Name as N
      action : Cxt → Term → TC Term
      action ctx t@(def gholes (arg _ arg1 ∷ []) ) = do
        case  (gholes N.≟ quote getHoles) of λ
          { (yes _) → do
            nf1 ← normalise arg1
            case nf1 of λ
              { (def mholes (arg _ tup ∷ [])) →
                case (mholes N.≟ quote makeHoles) of λ
                  {(yes _) → normalise tup
                  ; (no _) → return t}
              ; _ → return t}
          ; (no _) → return t }

      action _ t = return t

  -- applyNormal : ∀ {ℓ1 ℓ2} {X : Set ℓ1} {Y : Set ℓ2} → (X → Y) → X → Term → TC ⊤
  -- applyNormal {X = X} {Y} f x goal = do
  --   goalType ← inferType goal
  --   tX ← quoteTC X
  --   tY ← quoteTC Y
  --   tf ← quoteTC f
  --   tx ← quoteTC x
  --   nf ← normalise (app tf tx)
  --   unify goalType tY
  --   unify nf goal

default : {A : Set} → A → Term → TC ⊤
default x hole = bindTC (quoteTC x) (unify hole)

ext: agda

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Pushout.Base where

open import Cubical.Core.Glue

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

open import Cubical.Data.Unit

open import Cubical.HITs.Susp

data Pushout {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
             (f : A → B) (g : A → C) : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
  inl : B → Pushout f g
  inr : C → Pushout f g
  push : (a : A) → inl (f a) ≡ inr (g a)

-- Suspension defined as a pushout

PushoutSusp : ∀ {ℓ} (A : Type ℓ) → Type ℓ
PushoutSusp A = Pushout {A = A} {B = Unit} {C = Unit} (λ _ → tt) (λ _ → tt)

PushoutSusp→Susp : ∀ {ℓ} {A : Type ℓ} → PushoutSusp A → Susp A
PushoutSusp→Susp (inl _) = north
PushoutSusp→Susp (inr _) = south
PushoutSusp→Susp (push a i) = merid a i

Susp→PushoutSusp : ∀ {ℓ} {A : Type ℓ} → Susp A → PushoutSusp A
Susp→PushoutSusp north = inl tt
Susp→PushoutSusp south = inr tt
Susp→PushoutSusp (merid a i) = push a i

Susp→PushoutSusp→Susp : ∀ {ℓ} {A : Type ℓ} (x : Susp A) →
                        PushoutSusp→Susp (Susp→PushoutSusp x) ≡ x
Susp→PushoutSusp→Susp north = refl
Susp→PushoutSusp→Susp south = refl
Susp→PushoutSusp→Susp (merid _ _) = refl

PushoutSusp→Susp→PushoutSusp : ∀ {ℓ} {A : Type ℓ} (x : PushoutSusp A) →
                               Susp→PushoutSusp (PushoutSusp→Susp x) ≡ x
PushoutSusp→Susp→PushoutSusp (inl _) = refl
PushoutSusp→Susp→PushoutSusp (inr _) = refl
PushoutSusp→Susp→PushoutSusp (push _ _) = refl

PushoutSusp≃Susp : ∀ {ℓ} {A : Type ℓ} → PushoutSusp A ≃ Susp A
PushoutSusp≃Susp = isoToEquiv (iso PushoutSusp→Susp Susp→PushoutSusp Susp→PushoutSusp→Susp PushoutSusp→Susp→PushoutSusp)

PushoutSusp≡Susp : ∀ {ℓ} {A : Type ℓ} → PushoutSusp A ≡ Susp A
PushoutSusp≡Susp = isoToPath (iso PushoutSusp→Susp Susp→PushoutSusp Susp→PushoutSusp→Susp PushoutSusp→Susp→PushoutSusp)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-

  Generic UARel, DUARel, and SubstRel: the path relation is always univalent

-}
{-# OPTIONS --safe #-}
module Cubical.Displayed.Generic where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport

open import Cubical.Displayed.Base
open import Cubical.Displayed.Subst

private
  variable
    ℓ ℓA ℓA' ℓP ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓ≅B' ℓC ℓ≅C : Level

-- UARel for an arbitrary type

𝒮-generic : (A : Type ℓA) → UARel A ℓA
UARel._≅_ (𝒮-generic A) = _≡_
UARel.ua (𝒮-generic A) a a' = idEquiv (a ≡ a')

-- DUARel for an arbitrary family

𝒮ᴰ-generic : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (B : A → Type ℓB) → DUARel 𝒮-A B ℓB
𝒮ᴰ-generic 𝒮-A B .DUARel._≅ᴰ⟨_⟩_ b p b' = PathP (λ i → B (UARel.≅→≡ 𝒮-A p i)) b b'
𝒮ᴰ-generic 𝒮-A B .DUARel.uaᴰ b p b' = idEquiv _

-- SubstRel for an arbitrary family

𝒮ˢ-generic : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (B : A → Type ℓB) → SubstRel 𝒮-A B
𝒮ˢ-generic 𝒮-A B .SubstRel.act p = substEquiv B (UARel.≅→≡ 𝒮-A p)
𝒮ˢ-generic 𝒮-A B .SubstRel.uaˢ p b = refl

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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

mutual
  data D : Set where
    c : R → D

  record R : Set where
    coinductive
    field
      out : D
open R

mutual
  d : D
  d = c r

  r : R
  out r = d

f : D → {A : Set} → A
f (c x) = f (out x)
-- should not termination check

absurd : {A : Set} → A
absurd = f d

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module _ (A : Set) where

record R : Set where
  data D : Set where

open R (record {})

F : D → Set₃
F _ with Set₁
F _ | _ = Set₂

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import SOAS.Metatheory.Syntax

-- Second-order equational logic library
module SOAS.Metatheory.SecondOrder.Equality {T : Set} (Syn : Syntax {T}) where

open import SOAS.Common
open import SOAS.Families.Core {T}
open import SOAS.Context
open import SOAS.Variable

open import SOAS.Metatheory.FreeMonoid Syn

open import SOAS.Metatheory.SecondOrder.Metasubstitution Syn
open import SOAS.Metatheory.SecondOrder.Unit Syn

open import SOAS.ContextMaps.CategoryOfRenamings {T}
open import SOAS.Families.Build

open import SOAS.Metatheory Syn
open Syntax Syn
open Theory

private
  variable
    α β γ : T
    Γ Δ Π : Ctx
    𝔐 𝔑 : MCtx

-- Equational reasoning system extended from an axiom relation on terms
module EqLogic (_▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ 𝕋) α Γ → (𝔐 ▷ 𝕋) α Γ → Set) where

  -- Equality between terms: smallest equivalence relation closed under the axioms
  -- and parametrised metasubstitution
  data _▹_⊢_≋_ : (𝔐 : MCtx){α : T}(Γ : Ctx) → (𝔐 ▷ 𝕋) α Γ → (𝔐 ▷ 𝕋) α Γ → Set₁ where
    ax  : {t s : (𝔐 ▷ 𝕋) α Γ} → 𝔐 ▹ Γ ⊢ t ≋ₐ s →  𝔐 ▹ Γ ⊢ t ≋ s
    eq  : {t s : (𝔐 ▷ 𝕋) α Γ} → t ≡ s → 𝔐 ▹ Γ ⊢ t ≋ s
    sy  : {t s : (𝔐 ▷ 𝕋) α Γ} → 𝔐 ▹ Γ ⊢ t ≋ s → 𝔐 ▹ Γ ⊢ s ≋ t
    tr  : {t s u : (𝔐 ▷ 𝕋) α Γ} → 𝔐 ▹ Γ ⊢ t ≋ s → 𝔐 ▹ Γ ⊢ s ≋ u → 𝔐 ▹ Γ ⊢ t ≋ u
    □ms : {t s : (𝔐 ▷ 𝕋) α Γ}
        → 𝔐 ▹ Γ ⊢ t ≋ s
        → (ρ : Γ ↝ Δ)
        → (ζ ξ : MSub Δ 𝔐 𝔑)
        → (∀{τ Π}(𝔪 : Π ⊩ τ ∈ 𝔐) → 𝔑 ▹ (Π ∔ Δ) ⊢ (ix≀ ζ 𝔪) ≋ (ix≀ ξ 𝔪))
        → 𝔑 ▹ Δ ⊢ (□msub≀ t ρ ζ) ≋ (□msub≀ s ρ ξ)

  -- Reflexivity of ≋ lifted from refl
  rf : {t : (𝔐 ▷ 𝕋) α Γ} → 𝔐 ▹ Γ ⊢ t ≋ t
  rf = eq refl

  infix 1 _▹_⊢_≋_

  -- Helpers for equational reasoning
  module ≋-Reasoning where

    _≋⟨_⟩_ : (t : (𝔐 ▷ 𝕋) α Γ) {s u : (𝔐 ▷ 𝕋) α Γ}
           → 𝔐 ▹ Γ ⊢ t ≋ s
           → 𝔐 ▹ Γ ⊢ s ≋ u
           → 𝔐 ▹ Γ ⊢ t ≋ u
    t ≋⟨ t≋s ⟩ s≋u = tr {t = t} t≋s s≋u
    _≋⟨_⟩ₛ_ : (t : (𝔐 ▷ 𝕋) α Γ) {s u : (𝔐 ▷ 𝕋) α Γ}
           → 𝔐 ▹ Γ ⊢ s ≋ t
           → 𝔐 ▹ Γ ⊢ s ≋ u
           → 𝔐 ▹ Γ ⊢ t ≋ u
    t ≋⟨ s≋t ⟩ₛ s≋u = tr {t = t} (sy s≋t) s≋u

    _≡⟨_⟩_ : (t : (𝔐 ▷ 𝕋) α Γ){s : (𝔐 ▷ 𝕋) α Γ} {u : (𝔐 ▷ 𝕋) α Γ}
           → t ≡ s
           → 𝔐 ▹ Γ ⊢ s ≋ u
           → 𝔐 ▹ Γ ⊢ t ≋ u
    t ≡⟨ t≡s ⟩ s≋u = t ≋⟨ eq t≡s ⟩ s≋u

    _≡⟨⟩_ : (t : (𝔐 ▷ 𝕋) α Γ) {s : (𝔐 ▷ 𝕋) α Γ}
           → 𝔐 ▹ Γ ⊢ t ≋ s
           → 𝔐 ▹ Γ ⊢ t ≋ s
    t ≡⟨⟩ t≋s = t ≡⟨ refl ⟩ t≋s

    begin_ : {t s : (𝔐 ▷ 𝕋) α Γ} → 𝔐 ▹ Γ ⊢ t ≋ s → 𝔐 ▹ Γ ⊢ t ≋ s
    begin t≋s = t≋s

    _∎ : (t : (𝔐 ▷ 𝕋) α Γ) → 𝔐 ▹ Γ ⊢ t ≋ t
    t ∎ = rf

    infix  1 begin_
    infixr 2 _≋⟨_⟩_
    infixr 2 _≋⟨_⟩ₛ_
    infixr 2 _≡⟨_⟩_
    infixr 2 _≡⟨⟩_
    infix  3 _∎

  -- Rewrite two sides of ≋ with ≡
  rw : {t t′ s s′ : (𝔐 ▷ 𝕋) α Γ}
     → t ≡ t′ → s ≡ s′ → 𝔐 ▹ Γ ⊢ t ≋ s → 𝔐 ▹ Γ ⊢ t′ ≋ s′
  rw {t = t}{t′}{s}{s′} t≡t′ s≡s′ t≋s =
    begin t′ ≡⟨ sym t≡t′ ⟩ t ≋⟨ t≋s ⟩ s ≡⟨ s≡s′ ⟩ s′ ∎
      where open ≋-Reasoning

  -- Closure under base metasubstitution
  ms : {t s : (𝔐 ▷ 𝕋) α Γ}
     → 𝔐 ▹ Γ ⊢ t ≋ s
     → (ζ ξ : MSub Γ 𝔐 𝔑)
     → (∀{τ Π}(𝔪 : Π ⊩ τ ∈ 𝔐) → 𝔑 ▹ (Π ∔ Γ) ⊢ (ix≀ ζ 𝔪) ≋ (ix≀ ξ 𝔪))
     → 𝔑 ▹ Γ ⊢ msub≀ t ζ ≋ msub≀ s ξ
  ms {t = t}{s} t≋s ζ ξ ζ≋ξ = rw (□msub-id t (ix≀ ζ)) (□msub-id s (ix≀ ξ)) (□ms t≋s id ζ ξ ζ≋ξ)

  -- Metasubstitution of same mapping applied to two equivalent terms
  ms-eq : {t s : (𝔐 ▷ 𝕋) α Γ}
     → 𝔐 ▹ Γ ⊢ t ≋ s
     → (ζ : MSub Γ 𝔐 𝔑)
     → 𝔑 ▹ Γ ⊢ msub≀ t ζ ≋ msub≀ s ζ
  ms-eq {t = t}{s} t≋s ζ = ms t≋s ζ ζ (λ 𝔪 → rf)

  -- Closure under renaming
  ren≋ : {t s : (𝔐 ▷ 𝕋) α Γ}
         → 𝔐 ▹ Γ ⊢ t ≋ s
         → (ρ : Γ ↝ Δ)
         → 𝔐 ▹ Δ ⊢ 𝕣𝕖𝕟 ∥ 𝔐 ∥ t ρ ≋ 𝕣𝕖𝕟 ∥ 𝔐 ∥ s ρ
  ren≋ {𝔐}{α}{Γ}{Δ}{t = t}{s} t≋s ρ =
    begin
        (𝕣𝕖𝕟 ∥ 𝔐 ∥ t ρ)
    ≡⟨ sym (□msub-runit t ρ) ⟩
        □msub t ρ ms-unit
    ≡⟨ sym (cong (□msub t ρ) (iext (dext (id≀≈ms-unit Δ)))) ⟩
        □msub≀ t ρ (id≀ Δ)
    ≋⟨ □ms t≋s ρ (id≀ Δ) (id≀ Δ) (λ 𝔪 → rf) ⟩
        □msub≀ s ρ (id≀ Δ)
    ≡⟨ cong (□msub s ρ) (iext (dext (id≀≈ms-unit Δ))) ⟩
        □msub s ρ ms-unit
    ≡⟨ □msub-runit s ρ ⟩
        (𝕣𝕖𝕟 ∥ 𝔐 ∥ s ρ)
    ∎ where open ≋-Reasoning

  -- Lemma to apply equality to terms attached to the end of a metasubstitution
  ▹-eq : {Π′ : Ctx}{s u : (𝔑 ▷ 𝕋) β (Π′ ∔ Γ)}
       → 𝔑 ▹ (Π′ ∔ Γ) ⊢ s ≋ u → (ζ ξ : MSub Γ 𝔐 𝔑)
       → (∀{τ Π}(𝔪 : Π ⊩ τ ∈ 𝔐) → 𝔑 ▹ (Π ∔ Γ) ⊢ (ix≀ ζ 𝔪) ≋ (ix≀ ξ 𝔪))
       → (𝔪 : Π ⊩ α ∈ (𝔐 ⁅ Π′ ⊩ₙ β ⁆))
       → 𝔑 ▹ Π ∔ Γ ⊢ ix≀ (ζ ▹ s) 𝔪 ≋ ix≀ (ξ ▹ u) 𝔪
  ▹-eq e ◦ ◦ ζ≋ξ ↓ = e
  ▹-eq e (x ◃ ζ) (y ◃ ξ) ζ≋ξ ↓ = ζ≋ξ ↓
  ▹-eq e (x ◃ ζ) (y ◃ ξ) ζ≋ξ (↑ 𝔪) = ▹-eq e ζ ξ (λ 𝔫 → ζ≋ξ (↑ 𝔫)) 𝔪

  -- Congruence: metasubstitution of equivalent terms into a term extended with
  -- a new metavariable
  cong≋ : (t : (𝔐 ⁅ Π ⊩ₙ β ⁆ ▷ 𝕋) α Γ)
      → {s u : (𝔐 ▷ 𝕋) β (Π ∔ Γ)}
      → 𝔐 ▹ (Π ∔ Γ) ⊢ s ≋ u
      → 𝔐 ▹ Γ ⊢ instₑ t s ≋ instₑ t u
  cong≋ t {s} {u} s≋u = ms rf (id≀ _ ▹ s) (id≀ _ ▹ u) (▹-eq s≋u (id≀ _) (id≀ _) λ _ → rf)

  -- Double congruence
  cong₂≋ : {Π₁ Π₂ : Ctx}{β₁ β₂ : T}
        (t : ((𝔐 ⁅ Π₁ ⊩ₙ β₁ ⁆) ⁅ Π₂ ⊩ₙ β₂ ⁆ ▷ 𝕋) α Γ)
      → {s₁ u₁ : (𝔐 ▷ 𝕋) β₁ (Π₁ ∔ Γ)}
      → {s₂ u₂ : (𝔐 ▷ 𝕋) β₂ (Π₂ ∔ Γ)}
      → 𝔐 ▹ (Π₁ ∔ Γ) ⊢ s₁ ≋ u₁
      → 𝔐 ▹ (Π₂ ∔ Γ) ⊢ s₂ ≋ u₂
      → 𝔐 ▹ Γ ⊢ instₑ₂ t s₁ s₂ ≋ instₑ₂ t u₁ u₂
  cong₂≋ t {s₁}{u₁}{s₂}{u₂} s≋u₁ s≋u₂ =
    ms rf ((id≀ _ ▹ s₁) ▹ s₂) ((id≀ _ ▹ u₁) ▹ u₂)
    (▹-eq s≋u₂ (id≀ _ ▹ s₁) (id≀ _ ▹ u₁) (▹-eq s≋u₁ (id≀ _) (id≀ _) (λ - → rf)))

  -- Syntactic sugar
  cong[_]inside_ : {s u : (𝔐 ▷ 𝕋) β (Π ∔ Γ)}
      → 𝔐 ▹ (Π ∔ Γ) ⊢ s ≋ u
      → (t : (𝔐 ⁅ Π ⊩ₙ β ⁆ ▷ 𝕋) α Γ)
      → 𝔐 ▹ Γ ⊢ instₑ t s ≋ instₑ t u
  cong[ s≋u ]inside t = cong≋ t s≋u
  infix 05 cong[_]inside_
  cong₂[_][_]inside_ : {Π₁ Π₂ : Ctx}{β₁ β₂ : T}
      → {s₁ u₁ : (𝔐 ▷ 𝕋) β₁ (Π₁ ∔ Γ)}
      → {s₂ u₂ : (𝔐 ▷ 𝕋) β₂ (Π₂ ∔ Γ)}
      → 𝔐 ▹ (Π₁ ∔ Γ) ⊢ s₁ ≋ u₁
      → 𝔐 ▹ (Π₂ ∔ Γ) ⊢ s₂ ≋ u₂
      → (t : ((𝔐 ⁅ Π₁ ⊩ₙ β₁ ⁆) ⁅ Π₂ ⊩ₙ β₂ ⁆ ▷ 𝕋) α Γ)
      → 𝔐 ▹ Γ ⊢ instₑ₂ t s₁ s₂ ≋ instₑ₂ t u₁ u₂
  cong₂[ s≋u₁ ][ s≋u₂ ]inside t = cong₂≋ t s≋u₁ s≋u₂
  infix 05 cong₂[_][_]inside_

  -- Linear metasubstitution
  ○ms : {t s : (𝔐 ▷ 𝕋) α Γ}
     → 𝔐 ▹ Γ ⊢ t ≋ s
     → (ζ ξ : MSub Δ 𝔐 𝔑)
     → (∀{τ Π}(𝔪 : Π ⊩ τ ∈ 𝔐) → 𝔑 ▹ (Π ∔ Δ) ⊢ (ix≀ ζ 𝔪) ≋ (ix≀ ξ 𝔪))
     → 𝔑 ▹ Γ ∔ Δ ⊢ ○msub≀ t ζ ≋ ○msub≀ s ξ
  ○ms {Γ = Γ}{𝔑 = 𝔑}{t = t}{s} t≋s ζ ξ ζ≋ξ = □ms t≋s (inl Γ) (inr≀ Γ ζ) (inr≀ Γ ξ) (λ {τ}{Π} 𝔪 → begin
        ix≀ (inr≀ Γ ζ) 𝔪
    ≡⟨ ix-inr≀ ζ 𝔪 ⟩
        (𝕣𝕖𝕟 ∥ 𝔑 ∥ (ix≀ ζ 𝔪) (Π ∔∣ inr Γ))
    ≋⟨ ren≋ (ζ≋ξ 𝔪) (Π ∔∣ inr Γ) ⟩
        (𝕣𝕖𝕟 ∥ 𝔑 ∥ (ix≀ ξ 𝔪) (Π ∔∣ inr Γ))
    ≡⟨ sym (ix-inr≀ ξ 𝔪) ⟩
        ix≀ (inr≀ Γ ξ) 𝔪
    ∎) where open ≋-Reasoning

  -- Linear metasubstitution of same mapping applied to two equivalent terms
  ○ms-eq : {t s : (𝔐 ▷ 𝕋) α Π}
     → 𝔐 ▹ Π ⊢ t ≋ s
     → (ζ : MSub Γ 𝔐 𝔑)
     → 𝔑 ▹ Π ∔ Γ ⊢ ○msub≀ t ζ ≋ ○msub≀ s ζ
  ○ms-eq {t = t}{s} t≋s ζ = ○ms t≋s ζ ζ (λ 𝔪 → rf)

  -- Application of an axiom as a rewrite rule, and syntactic sugar
  ax≋ : {t s : (𝔐 ▷ 𝕋) α Π}
      → 𝔐 ▹ Π ⊢ t ≋ₐ s → (ζ : MSub Γ 𝔐 𝔑)
      → 𝔑 ▹ Π ∔ Γ ⊢ ○msub≀ t ζ ≋ ○msub≀ s ζ
  ax≋ a ζ = ○ms-eq (ax a) ζ

  ax_with《_ : {t s : (𝔐 ▷ 𝕋) α Π}
      → 𝔐 ▹ Π ⊢ t ≋ₐ s → (ζ : MSub Γ 𝔐 𝔑)
      → 𝔑 ▹ Π ∔ Γ ⊢ ○msub≀ t ζ ≋ ○msub≀ s ζ
  ax_with《_ = ax≋

  infix 15 ax_with《_

  -- Application of an equivalence as a rewrite rule, and syntactic sugar
  thm_with《_ : {t s : (𝔐 ▷ 𝕋) α Π}
     → 𝔐 ▹ Π ⊢ t ≋ s
     → (ζ : MSub Γ 𝔐 𝔑)
     → 𝔑 ▹ Π ∔ Γ ⊢ ○msub≀ t ζ ≋ ○msub≀ s ζ
  thm_with《_ = ○ms-eq
  infix 15 thm_with《_

  -- Application of theorem with no metavariables
  thm : {t s : (⁅⁆ ▷ 𝕋) α Π}
      → ⁅⁆ ▹ Π ⊢ t ≋ s
      → 𝔐 ▹ Π ∔ Γ ⊢ ○msub≀ t ◦ ≋ ○msub≀ s ◦
  thm e = thm e with《 ◦


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Equality
open import Agda.Builtin.Int
open import Agda.Builtin.String
open import Common.Prelude

getFixity = primQNameFixity

infixl -1729 _to_
_to_ : Set → Set → Set
A to B = A → B

data Check : Set₁ where
  equal : {A : Set} (x y : A) → x ≡ y → Check

pattern _==_ x y = equal x y refl

check-cons = getFixity (quote _∷_)  == fixity right-assoc (related (pos 5))
check-to   = getFixity (quote _to_) == fixity left-assoc  (related (negsuc 1728))
check-eq   = getFixity (quote _≡_)  == fixity non-assoc   (related (pos 4))
check-list = getFixity (quote List) == fixity non-assoc   unrelated

showAssoc : Associativity → String
showAssoc left-assoc  = "infixl"
showAssoc right-assoc = "infixr"
showAssoc non-assoc   = "infix"

showFixity : Fixity → String
showFixity (fixity a unrelated)   = "(no fixity)"
showFixity (fixity a (related p)) = showAssoc a +S+ " " +S+ intToString p

showFix : Name → String
showFix x = showFixity (getFixity x)

main : IO Unit
main = putStrLn (showFix (quote _∷_))  >>= λ _ →
       putStrLn (showFix (quote _to_)) >>= λ _ →
       putStrLn (showFix (quote _≡_))  >>= λ _ →
       putStrLn (showFix (quote List)) >>= λ _ →
       return unit


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

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

open import Vehicle
open import Data.Rational as ℝ using () renaming (ℚ to ℝ)

module monotonicity-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

f : ℝ → ℝ
f = evaluate record
  { projectFile = VEHICLE_PROJECT_FILE
  ; networkUUID = "TODO_networkUUID"
  }

abstract
  monotonic : ∀ (x1 : ℝ) → ∀ (x2 : ℝ) → x1 ℝ.≤ x2 → f x1 ℝ.≤ f x2
  monotonic = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


text:
-- Operations on natural number

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

-- agad-stdlib
open import Relation.Binary.PropositionalEquality

module TypeTheory.Nat.Operations
  {a}
  -- | Type of natural number
  (N : Set a)
  -- | Zero
  (zero : N)
  -- | Successor function
  (suc : N → N)
  -- | Induction principle
  (ind : ∀ {p} (P : N → Set p) → P zero → (∀ k → P k → P (suc k)) → ∀ n → P n)
  -- | Computation rule for `zero`
  (ind-base : ∀ {p} (P : N → Set p) P-base P-step →
              ind P P-base P-step zero ≡ P-base)
  -- | Computation rule for `suc`
  (ind-step : ∀ {p} (P : N → Set p) P-base P-step n →
              ind P P-base P-step (suc n) ≡ P-step n (ind P P-base P-step n))
  where

-- agda-stdlib
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Empty
open import Data.Bool using (Bool; true; false)
open import Data.Product
open import Function.Base

private
  variable
    A : Set a

-- recursion
rec : ∀ {l} {A : Set l} → A → (A → A) → N → A
rec {l} {A} z s n = ind (λ _ → A) z (λ k x → s x) n

caseNat : ∀ {l} {A : Set l} (z s : A) → N → A
caseNat {A = A} z s n = ind (λ x → A) z (λ k x → s) n

-- predcessor
pred : N → N
pred n = ind (λ _ → N) zero (λ k x → k) n

-- Arithematic
infixl 6 _+_ _∸_
infixl 7 _*_
infix 4 _≤_ _≰_ _≥_ _≱_ _<_ _≮_ _>_ _≯_
infix 5 _≤ᵇ_

-- Addition
_+_ : N → N → N
m + n = rec n suc m

-- Multiplication
_*_ : N → N → N
m * n = rec zero (λ k → n + k) m

-- Monus
_∸_ : N → N → N
m ∸ n = rec m pred n

-- Order
_≤_ : N → N → Set a
m ≤ n = ∃ λ o → m + o ≡ n

_≰_ : N → N → Set a
m ≰ n = m ≤ n → ⊥

_≥_ : N → N → Set a
m ≥ n = n ≤ m

_≱_ : N → N → Set a
m ≱ n = m ≥ n → ⊥

_<_ : N → N → Set a
m < n = suc m ≤ n

_≮_ : N → N → Set a
m ≮ n = m < n → ⊥

_>_ : N → N → Set a
m > n = n < m

_≯_ : N → N → Set a
m ≯ n = m > n → ⊥

-- Order (Bool)
_≤ᵇ_ : N → N → Bool
m ≤ᵇ n = caseNat true false (m ∸ n)

-- induction
ind2 :
  ∀ {p} (P : N → N → Set p) →
  P zero zero →
  (∀ m n → P m n → P m (suc n)) →
  (∀ m n → P m n → P (suc m) n) →
  ∀ m n → P m n
ind2 P Pzz Pmn→Pms Pmn→Psn m n = ind
  (λ o → P o n)
  (ind (λ p → P zero p) Pzz (λ k Pzk → Pmn→Pms zero k Pzk) n)
  (λ k Pkn → ind (λ r → P (suc k) r) (P[k,0] (suc k))
    (λ k₁ P[1+k,k₁] → Pmn→Pms (suc k) k₁ P[1+k,k₁]) n)
  m
  where
  P[k,0] : ∀ k → P k zero
  P[k,0] = λ k → ind (λ x → P x zero) Pzz (λ k₂ → Pmn→Psn k₂ zero) k

-- Constant
one : N
one = suc zero


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

open import PathInduction
open import Pushout

module JamesSecondComposite {i} (A : Type i) (⋆A : A) where

open import JamesTwoMaps A ⋆A public

-- Second composite

to-ε∞ : to ε∞ == εJ
to-ε∞ = idp

to-α∞-in∞ : (a : A) (n : ℕ) (x : J n) → to (α∞ a (in∞ n x)) == αJ a (inJ n x)
to-α∞-in∞ a n x = inJS-α n a x

to-α∞-push∞ : (a : A) (n : ℕ) (x : J n) → Square (ap to (ap (α∞ a) (push∞ n x))) (inJS-α n a x) idp (ap (αJ a) (ap to (push∞ n x)))
to-α∞-push∞ = λ a n x → & coh (ap-shape-∙! to (push∞-β  {in∞* = α∞-in∞ a} {push∞* = α∞-push∞ a} n x))
                              (to-push∞-S n (α n a x))
                              (ap-δJ (inJS-α n a x))
                              (∘-ap _ _ _)
                              (inJSS-γ n a x)
                              (ap-square (αJ a) (to-push∞ n x))  module Toα∞Push∞ where

  coh : Coh ({A : Type i} {a c : A} {q : a == c} {d : A} {r : a == d}
             {b : A} {s : b == d} {p : a == b} (p= : p == r ∙ ! s)
             {r' : a == d} (y= : r == r') {g : A} {w : d == g}
             {v : c == g} (sq : Square r' q w v) {e : A} {u : c == e}
             {s' : b == d} (s= : s == s') {t : b == e} (u= : Square s' t w (! u ∙ v))
             {x : c == b} (x= : Square x idp t u)
      → Square p q idp x)
  coh = path-induction

to-α∞ : (a : A) (x : J∞A) → to (α∞ a x) == αJ a (to x)
to-α∞ a = J∞A-elim (to-α∞-in∞ a) (λ n x → ↓-='-from-square (ap-∘ to (α∞ a) (push∞ n x)) (ap-∘ (αJ a) to (push∞ n x)) (square-symmetry (to-α∞-push∞ a n x)))

to-δ∞-in∞ : (n : ℕ) (x : J n) → Square (ap to (δ∞ (in∞ n x))) idp (to-α∞ ⋆A (in∞ n x)) (δJ (to (in∞ n x)))
to-δ∞-in∞ = λ n x → & coh (∘-ap _ _ _) (ap-square to (δ∞-in∞-β n x)) (to-push∞ n x) (inJS-β n x)  module Toδ∞In where

  coh : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {r r' : b == c} (r= : r == r')
             {s : a == c} (sq1 : Square p idp r s) {d : A} {t : c == d}
             {u : a == d} (sq2 : Square s idp t u)
             {rt : b == d} (rt= : Square r' rt t idp)
             → Square p idp rt u)
  coh = path-induction

module _ (n : ℕ) (x : J n) where

  side1 : Square (ap to (push∞ (S n) (α n ⋆A x))) (inJS-α n ⋆A x) (ap (αJ ⋆A) (inJS-α n ⋆A x)) (δJ (αJ ⋆A (inJ n x)))
  side1 = to-push∞-S n (α n ⋆A x) |∙ idp |∙ ap-δJ (inJS-α n ⋆A x)

  side2 : Square (ap to (ap (in∞ (S n)) (β n x))) (inJS-α n ⋆A x) (inJS-ι n x) idp
  side2 = idp |∙ ∘-ap to (in∞ (S n)) (β n x) |∙ inJS-β n x

  side3 : Square (ap to (ap (in∞ (S (S n))) (ap inr (β n x)))) (ap (αJ ⋆A) (inJS-α n ⋆A x)) (ap (αJ ⋆A) (inJS-ι n x)) (ap (αJ ⋆A) idp)
  side3 = idp |∙ (∘-ap to (in∞ (S (S n))) _ ∙ ap-inJSS-ι n (β n x)) |∙ ap-square (αJ ⋆A) (inJS-β n x)

  side4 : Square (ap to (push∞ (S n) (ι n x))) (inJS-ι n x) (ap (λ z → αJ ⋆A z) (inJS-ι n x)) (δJ (αJ ⋆A (inJ n x)))
  side4 = to-push∞-S n (ι n x) |∙ idp |∙ ap-δJ (inJS-ι n x)

  side5 : Square (ap to (ap (in∞ (S (S n))) (γ n ⋆A x))) (ap (αJ ⋆A) (inJS-ι n x)) (ap (αJ ⋆A) (inJS-α n ⋆A x)) (γJ ⋆A (inJ n x))
  side5 = ∘-ap to (in∞ (S (S n))) (γ n ⋆A x) |∙ inJSS-γ n ⋆A x

  side6 : Square (ap to (ap (in∞ (S (S n))) (β (S n) (ι n x)))) (ap (αJ ⋆A) (inJS-ι n x)) (ap (αJ ⋆A) (inJS-ι n x)) idp
  side6 = ∘-ap to (in∞ (S (S n))) _ |∙ inJS-βS n (ι n x) |∙ vid-square

  side7 : Square (ap to (ap (α∞ ⋆A) (push∞ n x))) (inJS-α n ⋆A x) (ap (αJ ⋆A) (inJS-ι n x)) (ap (αJ ⋆A) (δJ (inJ n x)))
  side7 = adapt-square (to-α∞-push∞ ⋆A n x ∙□ ap-square (αJ ⋆A) (to-push∞ n x)) ∙idp idp∙

  to-push∞-βn : Cube (ap-square to (natural-square (push∞ (S n)) (β n x) idp (ap-∘ (in∞ (S (S n))) inr (β n x))))
                    hid-square
                    side1
                    side2
                    side3
                    side4
  to-push∞-βn = & (ap-square-natural-square to) (β n x) (push∞ (S n)) ∙idp idp
               -∙³ & natural-square-homotopy (to-push∞-S n) (β n x)
               |∙³ & (natural-square-∘ (β n x) (inJS n)) δJ idp idp
               -∙³ & natural-square= δJ idp (coh1 to (in∞ (S n)) (β n x)) (coh2 to (in∞ (S (S n))) inr (β n x) (ap-∘ (αJ ⋆A) (inJS n) (β n x)))
               |∙³ & natural-cube2 δJ (inJS-β n x) (ap-square-idf (inJS-β n x)) (hid-flatcube _)  where

    coh1 : {A B C : Type i} (g : B → C) (f : A → B) {x y : A} (p : x == y) → Square idp (∘-ap (λ z → z) (g ∘ f) p ∙ ap-∘ g f p) (ap-idf _) (∘-ap g f p)
    coh1 g f idp = ids

    coh2 : {A B C D : Type i} (h : C → D) (g : B → C) (f : A → B) {x y : A} (p : x == y) {z : h (g (f x)) == h (g (f y))} (q : ap (h ∘ g ∘ f) p == z)
         → Square idp (! q ∙ ap-∘ h (g ∘ f) p ∙ ap (ap h) (ap-∘ g f p)) idp (∘-ap h g (ap f p) ∙ ∘-ap (h ∘ g) f p ∙ q)
    coh2 h g f idp idp = ids

  to-in∞-η : Cube (ap-square to (ap-square (in∞ (S (S n))) (η n x)))
                  (horiz-degen-square (ηJ (inJ n x)))
                  side5
                  vid-square
                  side3
                  side6
  to-in∞-η = adapt-cube-idp (∘-ap-square to (in∞ (S (S n))) (η n x)
                            |∙³ inJSS-η n x)
                            idp (& coh1) (& coh2) idp  where

    coh1 : Coh ({A : Type i} {a b : A} {p : a == b} → idp |∙ vid-square {p = p} == vid-square)
    coh1 = path-induction

    coh2 : Coh ({A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} {sq : Square p q r s}
                {p' : a == b} {p= : p' == p} {p'' : a == b} {p=' : p'' == p'} → p=' |∙ p= |∙ sq == idp |∙ (p=' ∙ p=) |∙ sq)
    coh2 = path-induction

  coh-last-one : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : a == c} → p == q ∙ ! (! p ∙ q))
  coh-last-one = path-induction

  last-one : Cube (horiz-degen-square (ap-shape-∙! to (push∞-β {in∞* = α∞-in∞ ⋆A} {push∞* = α∞-push∞ ⋆A} n x)))
                  (horiz-degen-square (& coh-last-one))
                  side7
                  vid-square
                  vid-square
                  (vcomp! side1 side5)
  last-one = & coh  where

    coh : Coh ({A : Type i} {a : A}
               {c : A} {q : a == c} {d : A} {r : a == d} {b : A} {s : b == d}
               {p : a == b} {p= : p == r ∙ ! s}
               {r' : a == d} {y= : r == r'}
               {g : A} {w : d == g} {v : c == g} {sq : Square r' q w v}
               {e : A} {u : c == e} {s' : b == d} {s= : s == s'}
               {t : b == e} {u= : Square s' t w (! u ∙ v)}
               {x : c == b} {x= : Square x idp t u}
               → Cube (horiz-degen-square p=) (horiz-degen-square (& coh-last-one)) (adapt-square (& Toα∞Push∞.coh p= y= sq s= u= x= ∙□ x=) ∙idp idp∙) vid-square vid-square (vcomp! (y= |∙ idp |∙ sq) (s= |∙ u=)))
    coh = path-induction

  δ∞Push∞Coh-coh : Coh ({A : Type i} {a b : A} {p : a == b} {d : A} {s : d == b}
        {c : A} {r : b == c} {f : A} {u : f == c} {e : A} {t : e == c}
        {w : f == e} {eta : Square w idp t u}
        {v : d == e} {nat : Square v s t r}
        {vw : d == f} {vw-eq : vw == v ∙ ! w}
        {a' : _} {a= : a == a'}
        {b' : _} {b= : b == b'}
        {p' : _} {p= : Square p a= b= p'}
        {d' : _} {d= : d == d'}
        {s' : _} {s= : Square s d= b= s'}
        {c' : _} {c= : c == c'}
        {r' : _} {r= : Square r b= c= r'}
        {f' : _} {f= : f == f'}
        {u' : _} {u= : Square u f= c= u'}
        {e' : _} {e= : e == e'}
        {t' : _} {t= : Square t e= c= t'}
        {w' : _} {w= : Square w f= e= w'}
        {eta' : _} (eta= : Cube eta eta' w= vid-square t= u=)
        {v' : _} {v= : Square v d= e= v'}
        {nat' : _} (nat= : Cube nat nat' v= s= t= r=)
        {vw' : _} {vw= : Square vw d= f= vw'}
        {vw-eq' : _} (vw-eq= : Cube (horiz-degen-square vw-eq) (horiz-degen-square vw-eq') vw= vid-square vid-square (vcomp! v= w=))
        → Cube (& δ∞Push∞.coh p eta nat vw-eq) (& δ∞Push∞.coh p' eta' nat' vw-eq') (vcomp! p= s=) p= vw= (vcomp! r= u=))
  δ∞Push∞Coh-coh = path-induction

  piece1 : FlatCube (ap-square to (& δ∞Push∞.coh (push∞ n x) (ap-square (in∞ (S (S n))) (η n x))
                                                (natural-square (push∞ (S n)) (β n x) idp (ap-∘ _ _ _))
                                                (push∞-β {in∞* = α∞-in∞ ⋆A} {push∞* = α∞-push∞ ⋆A} n x)))
                    (& δ∞Push∞.coh (ap to (push∞ n x))
                                  (ap-square to (ap-square (in∞ (S (S n))) (η n x)))
                                  (ap-square to
                                    (natural-square (push∞ (S n)) (β n x) idp
                                                    (ap-∘ (in∞ (S (S n))) (ι (S n)) (β n x))))
                                  (ap-shape-∙! to (push∞-β {in∞* = α∞-in∞ ⋆A} {push∞* = α∞-push∞ ⋆A} n x)))
                    (ap-∙! _ _ _) idp idp (ap-∙! _ _ _)
  piece1 = & (δ∞Push∞.ap-coh to) {b = in∞ (S n) (ι n x)} {d = in∞ (S n) (α n ⋆A x)}

  piece2 : Cube (& δ∞Push∞.coh (ap to (push∞ n x))
                              (ap-square to (ap-square (in∞ (S (S n))) (η n x)))
                              (ap-square to (natural-square (push∞ (S n)) (β n x) idp (ap-∘ (in∞ (S (S n))) inr (β n x))))
                              (ap-shape-∙! to (push∞-β {in∞* = α∞-in∞ ⋆A} {push∞* = α∞-push∞ ⋆A} n x)))
                (& δ∞Push∞.coh (δJ (inJ n x)) (horiz-degen-square (ηJ (inJ n x))) hid-square (& coh-last-one))
                (vcomp! (to-push∞ n x) side2)
                (to-push∞ n x)
                side7
                (vcomp! side4 side6)
  piece2 = & δ∞Push∞Coh-coh to-in∞-η to-push∞-βn last-one

  piece3 : FlatCube (& δ∞Push∞.coh (δJ (inJ n x)) (horiz-degen-square (ηJ (inJ n x))) hid-square (& coh-last-one))
                    (ap-δJ (δJ (inJ n x)))
                    ∙idp idp idp ∙idp
  piece3 = & coh where

    coh : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q q' : b == c} {sq : Square p p q q'}
              → FlatCube (& δ∞Push∞.coh p (horiz-degen-square (& (ηIfy.coh αJ δJ) sq)) hid-square (& coh-last-one)) sq ∙idp idp idp ∙idp)
    coh = path-induction

  piece4 : Cube (ap-δJ (ap to (push∞ n x)))
                (ap-δJ (δJ (inJ n x)))
                hid-square (to-push∞ n x) (ap-square (αJ ⋆A) (to-push∞ n x)) (ap-δJ (inJS-ι n x))
  piece4 = & natural-cube2 δJ (to-push∞ n x) (ap-square-idf _) (hid-flatcube _)

  to-δ∞-push∞ : Cube (ap-square to (natural-square δ∞ (push∞ n x) (ap-idf _) idp))
                    (ap-δJ (ap to (push∞ n x)))
                    (to-δ∞-in∞ n x)
                    hid-square
                    (to-α∞-push∞ ⋆A n x)
                    (to-δ∞-in∞ (S n) (ι n x))
  to-δ∞-push∞ = adapt-cube (ap (ap-square to) (natural-square-β δ∞ (push∞ n x) (push∞-βd n x))
                          -∙³ piece1
                          |∙³ piece2
                          ∙³x piece3
                          |∙³ !³ piece4)
                 idp ∙idp !-inv-r !-inv-r
                 (& coh1 (& (coh-flat to) {b = in∞ (S n) (α n ⋆A x)})) (& coh2) (& coh3) (& coh4 (& (coh-flat to) {a = in∞ (S n) (ι n x)})) where

    flat : Coh ({A : Type i} {a c : A} {s : a == c} {b : A} {r : b == c} {p : a == b} (sq : Square p idp r s) → p == s ∙ ! r)
    flat = path-induction

    coh-flat : {A B : Type i} (f : A → B) → Coh ({a c : A} {s : a == c} {b : A} {r : b == c} → & flat (ap-square f (& δ∞Inβ.coh)) == ap-∙! f s r)
    coh-flat f = path-induction

    coh1 : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {r r' : b == c} {r= : r == r'}
                {s : a == c} {sq1 : Square p idp r s} {d : A} {t : c == d}
                {u : a == d} {sq2 : Square s idp t u}
                {rt : b == d} {sq3 : Square r' rt t idp}
                {p= : p == s ∙ ! r} (p== : & flat sq1 == p=)
               → adapt-square (p= |∙ vcomp! sq2 (idp |∙ r= |∙ sq3) ∙□ ∙idp |∙ !² hid-square) idp ∙idp == & Toδ∞In.coh r= sq1 sq2 sq3)
    coh1 = path-induction

    coh2 : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {r : b == c} {s : a == c} {sq : Square p idp r s}
               → adapt-square (idp |∙ sq ∙□ idp |∙ !² sq) idp !-inv-r == hid-square)
    coh2 = path-induction

    coh3 : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : a == c} {s : c == b} {sq1 : Square p q idp s} {d : A} {t : b == d} {u : c == d} {sq2 : Square s idp t u}
                → adapt-square (idp |∙ adapt-square (sq1 ∙□ sq2) ∙idp idp∙ ∙□ idp |∙ !² sq2) ∙idp !-inv-r == sq1)
    coh3 = path-induction

    coh4 : Coh ({A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} {sq : Square p q r s}
                {p' : a == b} {p=□ : Square p' idp idp p} {t : b == b} {t=□ : t == idp} {t' : b == b} {t=' : t' == t}
                {pt' : a == b} {pt=2 : Square pt' idp t' p'} {pt= : pt' == p' ∙ ! t'} (pt== : & flat pt=2 == pt=)
               → adapt-square (pt= |∙ vcomp! (horiz-degen-path p=□ |∙ idp |∙ sq) (t=' |∙ t=□ |∙ vid-square) ∙□ ∙idp |∙ !² sq) !-inv-r !-inv-r
               == & Toδ∞In.coh t=' pt=2 p=□ (horiz-degen-square t=□))
    coh4 = path-induction

natural-square-idp-symm : {A B : Type i} {f : A → B} {x y : A} {p : x == y} → natural-square (λ a → idp {a = f a}) p idp idp == square-symmetry hid-square
natural-square-idp-symm {p = idp} = idp

to-δ∞ : (x : J∞A) → Square (ap to (δ∞ x)) idp (to-α∞ ⋆A x) (δJ (to x))
to-δ∞ = J∞A-elim to-δ∞-in∞ (λ n x → cube-to-↓-path idp (ap-∘ _ _ _) idp (ap-∘ _ _ _)
  (adapt-cube-idp (cube-rotate (to-δ∞-push∞ n x))
                  (& (ap-square-natural-square to) (push∞ n x) δ∞ coh ∙idp)
                  (! natural-square-idp-symm)
                  (! (natural-square-β (to-α∞ ⋆A) (push∞ n x) (push∞-βd n x)))
                  (! (& (natural-square-∘ (push∞ n x) to) δJ coh2 (!-inv-l)))))  where

  coh : {A B : Type i} {f : A → B} {x y : A} {p : x == y} → ap-∘ f (λ z → z) p ∙ ap (ap f) (ap-idf p) == idp
  coh {p = idp} = idp

  coh2 : {A B : Type i} {f : A → B} {x y : A} {p : x == y} → ∘-ap (λ z → z) f p ∙ idp == ap-idf (ap f p)
  coh2 {p = idp} = idp

to-from : (x : JA) → to (from x) == x
to-from = JA-elim to-ε∞
                   (λ a x y → to-α∞ a (from x) ∙ ap (αJ a) y)
                   (λ x y → ↓-='-from-square (ap-∘ to from (δJ x) ∙ ap (ap to) (δJ-β x)) (ap-idf (δJ x))
                     (square-symmetry (adapt-square (to-δ∞ (from x) ∙□ ap-δJ y) idp∙ idp)))

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
module Relation.Ternary.Separation.Bigstar where

open import Level
open import Data.Bool
open import Data.Product
open import Relation.Unary
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Monad.Error
open import Relation.Ternary.Separation.Morphisms
open Monads

module _
  {a p} {A : Set a} (P : Pred A p)
  {{ r : RawSep A }} {u} {{ _ : IsUnitalSep r u }} where

  data Bigstar : SPred (a ⊔ p) where
    emp  : ε[ Bigstar ]
    cons : ∀[ P ✴ Bigstar ⇒ Bigstar ]

module _
  {a} {A : Set a} {P : Pred A a}
  {{ r : RawSep A }} {u} {{ _ : IsUnitalSep r u }} where

  [_] : ∀[ P ⇒ Bigstar P ]
  [ px ] = cons (px ×⟨ ⊎-idʳ ⟩ emp)

  head : ∀[ Bigstar P ⇒ Error (P ✴ Bigstar P) ]
  head emp = error err
  head pool@(cons (px ×⟨ σ ⟩ pxs)) = do
    th₂ ×⟨ σ ⟩ pool' ×⟨ σ₂ ⟩ th₁ ← mapM (head pxs &⟨ ⊎-comm σ ⟩ px) ✴-assocᵣ
    return (th₂ ×⟨ σ ⟩ cons (th₁ ×⟨ ⊎-comm σ₂ ⟩ pool'))

  find : (∀ {Φ} → P Φ → Bool) → ∀[ Bigstar P ⇒ Error (P ✴ Bigstar P) ]
  find f emp = error err
  find f (cons (px ×⟨ σ ⟩ pxs)) =
    if f px
      then return (px ×⟨ σ ⟩ pxs)
      else do
        px' ×⟨ σ₁ ⟩ pxs' ×⟨ σ₂ ⟩ px ← mapM (find f pxs &⟨ P ∥ ⊎-comm σ ⟩ px) ✴-assocᵣ
        return (px' ×⟨ σ₁ ⟩ cons (px ×⟨ ⊎-comm σ₂ ⟩ pxs'))

  append : ∀[ P ⇒ Bigstar P ─✴ Bigstar P ]
  app (append px) emp σ rewrite ⊎-id⁻ʳ σ = [ px ]
  app (append px) (cons (qx ×⟨ σ₁ ⟩ pxs)) σ =
    let _ , σ₂ , σ₃ = ⊎-unassoc σ (⊎-comm σ₁)
        qxs = app (append px) pxs σ₂
    in cons (qx ×⟨ ⊎-comm σ₃ ⟩ qxs)


text:
------------------------------------------------------------------------
-- A partial order
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Delay-monad.Partial-order {a} {A : Type a} where

open import Equality.Propositional as E
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Double-negation equality-with-J
open import Excluded-middle equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Monad equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity as B
  hiding (reflexive; symmetric; laterˡ⁻¹; laterʳ⁻¹)
open import Delay-monad.Bisimilarity.Alternative
open import Delay-monad.Bisimilarity.Negative
import Delay-monad.Termination as T

-- An ordering relation.
--
-- Capretta defines a pointwise logically equivalent relation in
-- "General Recursion via Coinductive Types".
--
-- Benton, Kennedy and Varming define a relation that is perhaps
-- pointwise logically equivalent in "Some Domain Theory and
-- Denotational Semantics in Coq".

infix 4 [_]_⊑_ [_]_⊑′_ _⊑_ _⊑′_

mutual

  data [_]_⊑_ (i : Size) : Delay A ∞ → Delay A ∞ → Type a where
    now    : ∀ {x} → [ i ] now x ⊑ now x
    laterʳ : ∀ {x y} → [ i ] x ⊑ force y → [ i ] x ⊑ later y
    laterˡ : ∀ {x y} → [ i ] force x ⊑′ y → [ i ] later x ⊑ y

  record [_]_⊑′_ (i : Size) (x y : Delay A ∞) : Type a where
    coinductive
    field
      force : {j : Size< i} → [ j ] x ⊑ y

open [_]_⊑′_ public

_⊑_ : Delay A ∞ → Delay A ∞ → Type a
_⊑_ = [ ∞ ]_⊑_

_⊑′_ : Delay A ∞ → Delay A ∞ → Type a
_⊑′_ = [ ∞ ]_⊑′_

-- A derived "constructor".

later-cong : ∀ {i x y} →
             [ i ] force x ⊑′ force y → [ i ] later x ⊑ later y
later-cong p = laterʳ (laterˡ p)

-- Termination predicates.

Terminates : Size → Delay A ∞ → A → Type a
Terminates i x y = [ i ] now y ⊑ x

_⇓_ : Delay A ∞ → A → Type a
_⇓_ = Terminates ∞

-- If x terminates with the values y and z, then y is equal to z.

⇓→⇓→≡ : ∀ {i x y z} → Terminates i x y → Terminates i x z → y ≡ z
⇓→⇓→≡ now        now        = refl
⇓→⇓→≡ (laterʳ p) (laterʳ q) = ⇓→⇓→≡ p q

-- If x is smaller than or equal to now y, and x terminates, then
-- x terminates with the value y.

⊑now→⇓→⇓ : ∀ {i x} {y z : A} →
           x ⊑ now y → Terminates i x z → Terminates i x y
⊑now→⇓→⇓ now        now        = now
⊑now→⇓→⇓ (laterˡ p) (laterʳ q) = laterʳ (⊑now→⇓→⇓ (force p) q)

-- The notion of termination defined here is pointwise isomorphic to
-- the one defined in Delay-monad.Termination.

⇓↔⇓ : ∀ {i x y} → Terminates i x y ↔ T.Terminates i x y
⇓↔⇓ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : ∀ {i x y} → Terminates i x y → T.Terminates i x y
  to now        = now
  to (laterʳ p) = laterʳ (to p)

  from : ∀ {i x y} → T.Terminates i x y → Terminates i x y
  from now        = now
  from (laterʳ p) = laterʳ (from p)

  from∘to : ∀ {i x y} (p : Terminates i x y) → from (to p) ≡ p
  from∘to now        = refl
  from∘to (laterʳ p) = cong laterʳ (from∘to p)

  to∘from : ∀ {i x y} (p : T.Terminates i x y) → to (from p) ≡ p
  to∘from now        = refl
  to∘from (laterʳ p) = cong laterʳ (to∘from p)

-- Terminates i is pointwise isomorphic to Terminates ∞.

Terminates↔⇓ : ∀ {i x y} → Terminates i x y ↔ x ⇓ y
Terminates↔⇓ {i} {x} {y} =
  Terminates i x y    ↝⟨ ⇓↔⇓ ⟩
  T.Terminates i x y  ↝⟨ T.Terminates↔⇓ ⟩
  x T.⇓ y             ↝⟨ inverse ⇓↔⇓ ⟩□
  x ⇓ y               □

-- The computation never is smaller than or equal to all other
-- computations.

never⊑ : ∀ {i} x → [ i ] never ⊑ x
never⊑ (now x)   = laterˡ λ { .force → never⊑ (now x) }
never⊑ (later x) = later-cong λ { .force → never⊑ (force x) }

-- The computation never does not terminate.

now⋢never : ∀ {i x} → ¬ Terminates i never x
now⋢never (laterʳ p) = now⋢never p

-- One can remove later constructors.

laterˡ⁻¹ : ∀ {i} {j : Size< i} {x y} →
           [ i ] later x ⊑ y →
           [ j ] force x ⊑ y
laterˡ⁻¹ (laterʳ p) = laterʳ (laterˡ⁻¹ p)
laterˡ⁻¹ (laterˡ p) = force p

laterʳ⁻¹ : ∀ {i x y} →
           [ i ] x ⊑ later y →
           [ i ] x ⊑ force y
laterʳ⁻¹ (laterʳ p) = p
laterʳ⁻¹ (laterˡ p) = laterˡ λ { .force → laterʳ⁻¹ (force p) }

later-cong⁻¹ : ∀ {i} {j : Size< i} {x y} →
               [ i ] later x ⊑ later y →
               [ j ] force x ⊑ force y
later-cong⁻¹ p = laterʳ⁻¹ (laterˡ⁻¹ p)

-- Weak bisimilarity is contained in the ordering relation.

≈→⊑ : ∀ {i x y} → [ i ] x ≈ y → [ i ] x ⊑ y
≈→⊑ now        = now
≈→⊑ (later  p) = later-cong λ { .force → ≈→⊑ (force p) }
≈→⊑ (laterˡ p) = laterˡ λ { .force → ≈→⊑ p }
≈→⊑ (laterʳ p) = laterʳ (≈→⊑ p)

-- The ordering relation is antisymmetric (with respect to weak
-- bisimilarity).

antisymmetric : ∀ {i x y} →
                [ i ] x ⊑ y → [ i ] y ⊑ x → [ i ] x ≈ y
antisymmetric {x = now   x} {y = now  .x} now        _          = now
antisymmetric {x = now   x} {y = later y} (laterʳ p) q          = laterʳ (_↔_.to ⇓↔⇓ p)
antisymmetric {x = later x} {y = now   y} p          (laterʳ q) = laterˡ (B.symmetric (_↔_.to ⇓↔⇓ q))
antisymmetric {x = later x} {y = later y} p          q          =
  later λ { .force → antisymmetric (later-cong⁻¹ p) (later-cong⁻¹ q) }

-- An alternative characterisation of weak bisimilarity.

≈⇔⊑×⊒ : ∀ {i x y} → [ i ] x ≈ y ⇔ ([ i ] x ⊑ y × [ i ] y ⊑ x)
≈⇔⊑×⊒ = record
  { to   = λ p → ≈→⊑ p , ≈→⊑ (B.symmetric p)
  ; from = uncurry antisymmetric
  }

-- The ordering relation is reflexive.

reflexive : ∀ {i} x → [ i ] x ⊑ x
reflexive (now x)   = now
reflexive (later x) = later-cong λ { .force → reflexive (force x) }

-- Certain instances of symmetry also hold.

symmetric : ∀ {i} {x : A} {y} →
            Terminates i y x → [ i ] y ⊑ now x
symmetric now        = now
symmetric (laterʳ p) = laterˡ λ { .force → symmetric p }

-- The ordering relation is transitive.

transitive : ∀ {i} {x y z : Delay A ∞} →
             [ i ] x ⊑ y → y ⊑ z → [ i ] x ⊑ z
transitive p          now        = p
transitive p          (laterʳ q) = laterʳ (transitive p q)
transitive (laterʳ p) (laterˡ q) = transitive p (force q)
transitive (laterˡ p) q          = laterˡ λ { .force →
                                     transitive (force p) q }

-- The termination relation respects weak bisimilarity.

⇓-respects-≈ : ∀ {i x y z} → Terminates i x z → x ≈ y → Terminates i y z
⇓-respects-≈ now        q = ≈→⊑ q
⇓-respects-≈ (laterʳ p) q = ⇓-respects-≈ p (B.laterˡ⁻¹ q)

-- The ordering relation respects weak bisimilarity.

transitive-≈⊑ : ∀ {i x y z} → [ i ] x ≈ y → y ⊑ z → [ i ] x ⊑ z
transitive-≈⊑ p q = transitive (≈→⊑ p) q

transitive-⊑≈ : ∀ {i x y z} → [ i ] x ⊑ y → y ≈ z → [ i ] x ⊑ z
transitive-⊑≈ p          now        = p
transitive-⊑≈ (laterʳ p) (later  q) = laterʳ (transitive-⊑≈ p (force q))
transitive-⊑≈ (laterˡ p) q          = laterˡ λ { .force →
                                        transitive-⊑≈ (force p) q }
transitive-⊑≈ (laterʳ p) (laterˡ q) = transitive-⊑≈ p q
transitive-⊑≈ p          (laterʳ q) = laterʳ (transitive-⊑≈ p q)

-- There is a transitivity-like function that produces an ordering
-- proof from one weak bisimilarity proof and one ordering proof, in
-- such a way that the size of the ordering proof is preserved, iff A
-- is uninhabited.

Transitivity-≈⊑ʳ =
  ∀ {i} {x y z : Delay A ∞} → x ≈ y → [ i ] y ⊑ z → [ i ] x ⊑ z

size-preserving-transitivity-≈⊑ʳ⇔uninhabited : Transitivity-≈⊑ʳ ⇔ ¬ A
size-preserving-transitivity-≈⊑ʳ⇔uninhabited = record
  { to   = Transitivity-≈⊑ʳ                                    ↝⟨ (λ trans {i x} →

               [ i ] later (record { force = now x }) ∼ never        ↝⟨ ≈→⊑ ∘ ∼→ ⟩
               [ i ] later (record { force = now x }) ⊑ never        ↝⟨ trans (laterʳ now) ⟩
               [ i ] now x ⊑ never                                   ↝⟨ _↔_.to ⇓↔⇓ ⟩□
               [ i ] now x ≈ never                                   □) ⟩

           Laterˡ⁻¹-∼≈′                                        ↝⟨ _⇔_.to size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited ⟩

           ¬ A                                                 □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial _ _ → ≈→⊑ (trivial _ _)) ⟩
           (∀ x y → x ⊑ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≈⊑ʳ  □
  }

-- Transitivity can be made size-preserving in the second argument iff
-- A is uninhabited.

Transitivityʳ =
  ∀ {i} {x y z : Delay A ∞} → x ⊑ y → [ i ] y ⊑ z → [ i ] x ⊑ z

size-preserving-transitivityʳ⇔uninhabited : Transitivityʳ ⇔ ¬ A
size-preserving-transitivityʳ⇔uninhabited = record
  { to   = Transitivityʳ     ↝⟨ _∘ ≈→⊑ ⟩
           Transitivity-≈⊑ʳ  ↝⟨ _⇔_.to size-preserving-transitivity-≈⊑ʳ⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial _ _ → ≈→⊑ (trivial _ _)) ⟩
           (∀ x y → x ⊑ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivityʳ    □
  }

-- There is a transitivity-like function that produces an ordering
-- proof from one ordering proof and one weak bisimilarity proof, in
-- such a way that the size of the weak bisimilarity proof is
-- preserved, iff A is uninhabited.

Transitivity-⊑≈ʳ =
  ∀ {i} {x y z : Delay A ∞} → x ⊑ y → [ i ] y ≈ z → [ i ] x ⊑ z

size-preserving-transitivity-⊑≈ʳ⇔uninhabited : Transitivity-⊑≈ʳ ⇔ ¬ A
size-preserving-transitivity-⊑≈ʳ⇔uninhabited = record
  { to   = Transitivity-⊑≈ʳ                                    ↝⟨ (λ trans {i x} →

               [ i ] later (record { force = now x }) ∼ never        ↝⟨ ∼→ ⟩
               [ i ] later (record { force = now x }) ≈ never        ↝⟨ trans (laterʳ now) ⟩
               [ i ] now x ⊑ never                                   ↝⟨ _↔_.to ⇓↔⇓ ⟩□
               [ i ] now x ≈ never                                   □) ⟩

           Laterˡ⁻¹-∼≈′                                        ↝⟨ _⇔_.to size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited ⟩

           ¬ A                                                 □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial _ _ → ≈→⊑ (trivial _ _)) ⟩
           (∀ x y → x ⊑ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-⊑≈ʳ  □
  }

-- An alternative characterisation of the ordering relation.
--
-- Capretta proves a similar result in "General Recursion via
-- Coinductive Types".
--
-- One might wonder if the equivalence can be made size-preserving in
-- some way. However, note that x ⇓ y is in bijective correspondence
-- with Terminates i x y for any size i (see Terminates↔⇓).

⊑⇔⇓→⇓ : ∀ {x y} → x ⊑ y ⇔ (∀ z → x ⇓ z → y ⇓ z)
⊑⇔⇓→⇓ = record
  { to   = to
  ; from = from _
  }
  where
  to : ∀ {x y} → x ⊑ y → ∀ z → x ⇓ z → y ⇓ z
  to p          z now   = p
  to (laterʳ p) z q          = laterʳ (to p z q)
  to (laterˡ p) z (laterʳ q) = to (force p) z q

  from : ∀ {i} x {y} → (∀ z → x ⇓ z → y ⇓ z) → [ i ] x ⊑ y
  from (now x)   p = p x now
  from (later x) p = laterˡ λ { .force →
                       from (force x) (λ z q → p z (laterʳ q)) }

-- An alternative characterisation of weak bisimilarity.
--
-- Capretta proves a similar result in "General Recursion via
-- Coinductive Types".

≈⇔≈₂ : {x y : Delay A ∞} → x ≈ y ⇔ x ≈₂ y
≈⇔≈₂ {x} {y} =
  x ≈ y                                                  ↝⟨ ≈⇔⊑×⊒ ⟩
  x ⊑ y × y ⊑ x                                          ↝⟨ ⊑⇔⇓→⇓ ×-cong ⊑⇔⇓→⇓ ⟩
  (∀ z → x ⇓ z → y ⇓ z) × (∀ z → y ⇓ z → x ⇓ z)          ↝⟨ ∀-cong _ (λ _ → →-cong _ (from-bijection ⇓↔⇓) (from-bijection ⇓↔⇓))
                                                              ×-cong
                                                            ∀-cong _ (λ _ → →-cong _ (from-bijection ⇓↔⇓) (from-bijection ⇓↔⇓)) ⟩
  (∀ z → x T.⇓ z → y T.⇓ z) × (∀ z → y T.⇓ z → x T.⇓ z)  ↝⟨ record { to   = uncurry λ to from z → record { to = to z; from = from z }
                                                                   ; from = λ hyp → _⇔_.to ∘ hyp , _⇔_.from ∘ hyp
                                                                   } ⟩□
  (∀ z → x T.⇓ z ⇔ y T.⇓ z)                              □

-- If A is a set, then every computation is weakly bisimilar to either
-- never or now something (assuming excluded middle and
-- extensionality).

⇑⊎⇓ :
  Excluded-middle a → E.Extensionality a a →
  Is-set A → (x : Delay A ∞) → never ≈ x ⊎ ∃ λ y → x T.⇓ y
⇑⊎⇓ em ext A-set x =
  ⊎-map (_⇔_.from ≈⇔≈₂) id $
  Excluded-middle→Double-negation-elimination em
    (⊎-closure-propositional
       (λ { x⇑ (y , x⇓y) →
            now≉never (now y  ≈⟨ x⇓y ⟩
                       x      ≈⟨ B.symmetric (_⇔_.from ≈⇔≈₂ x⇑) ⟩∎
                       never  ∎) })
       (≈₂-propositional ext A-set)
       (T.∃-Terminates-propositional A-set))
    (⊎-map (_⇔_.to ≈⇔≈₂) id ⟨$⟩ T.¬¬[⇑⊎⇓] x)

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Relation.Binary.Base
open import Cubical.Core.Everything

module Cubical.Relation.Binary.Structures
  {a ℓ} {A : Type a} -- The underlying type
  (_<>_ : Rel A ℓ)   -- The relation
  where

open import Cubical.Foundations.Prelude using (refl; sym; isSet)
open import Cubical.Foundations.Function using (_∘_; id)
open import Cubical.Foundations.Logic hiding (¬_)

open import Cubical.Relation.Nullary.Decidable
open import Cubical.Relation.Binary.Definitions
open import Cubical.Relation.Binary.Properties

open import Cubical.HITs.PropositionalTruncation

import Cubical.Relation.Binary.Raw.Structures [ _<>_ ] as Raw

private
  variable
    ℓ₂ : Level

------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------

record IsPreorder : Type (ℓ-max a ℓ) where
  constructor ispreorder
  field
    reflexive  : Reflexive _<>_
    transitive : Transitive _<>_

  fromEq : FromEq _<>_
  fromEq = reflx→fromeq _<>_ reflexive

  raw : Raw.IsPreorder
  raw = record
    { reflexive = reflexive
    ; transitive = transitive
    }

------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------

record IsPartialEquivalence : Type (ℓ-max a ℓ) where
  constructor ispartialeq
  field
    symmetric  : Symmetric _<>_
    transitive : Transitive _<>_

  raw : Raw.IsPartialEquivalence
  raw = record
    { symmetric = symmetric
    ; transitive = transitive
    }

record IsEquivalence : Type (ℓ-max a ℓ) where
  constructor isequivalence
  field
    reflexive            : Reflexive _<>_
    isPartialEquivalence : IsPartialEquivalence

  open IsPartialEquivalence isPartialEquivalence public hiding (raw)

  from-≡ : FromEq _<>_
  from-≡ = reflx→fromeq _<>_ reflexive

  isPreorder : IsPreorder
  isPreorder = record
    { reflexive  = reflexive
    ; transitive = transitive
    }

  raw : Raw.IsEquivalence
  raw = record
    { reflexive = reflexive
    ; isPartialEquivalence = IsPartialEquivalence.raw isPartialEquivalence
    }

record IsDecEquivalence : Type (ℓ-max a ℓ) where
  constructor isdeceq
  infix 4 _≟_
  field
    isEquivalence : IsEquivalence
    _≟_           : Decidable _<>_

  open IsEquivalence isEquivalence public hiding (raw)

  raw : Raw.IsDecEquivalence
  raw = record
    { isEquivalence = IsEquivalence.raw isEquivalence
    ; _≟_ = _≟_
    }

------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------

record IsPartialOrder : Type (ℓ-max a ℓ) where
  constructor ispartialorder
  field
    isPreorder : IsPreorder
    antisym    : Antisymmetric _<>_

  open IsPreorder isPreorder public hiding (raw)

  raw : isSet A → Raw.IsPartialOrder
  raw isSetA = record
    { isPreorder = IsPreorder.raw isPreorder
    ; antisym = λ x y → rec (isSetA _ _) id (antisym x y)
    }

record IsDecPartialOrder : Type (ℓ-max a ℓ) where
  constructor isdecpartialorder
  infix 4 _≤?_
  field
    isPartialOrder : IsPartialOrder
    _≤?_           : Decidable _<>_

  open IsPartialOrder isPartialOrder public hiding (raw)

  private
    lemma : ∀ {x y} → ¬ ⟨ x <> y ⟩ → ¬ x ≡ y
    lemma x≰y x≡y = x≰y (fromEq ∣ x≡y ∣)

  raw : isSet A → Raw.IsDecPartialOrder
  raw isSetA = record
    { isPartialOrder = IsPartialOrder.raw isPartialOrder isSetA
    ; _≤?_ = _≤?_
    }

record IsStrictPartialOrder : Type (ℓ-max a ℓ) where
  constructor isstrictpartialorder
  field
    irrefl     : Irreflexive _<>_
    transitive : Transitive _<>_

  asym : Asymmetric _<>_
  asym {x} {y} = trans∧irr→asym _<>_ transitive irrefl

  raw : Raw.IsStrictPartialOrder
  raw = record
    { irrefl = irrefl
    ; transitive = transitive
    }

record IsDecStrictPartialOrder : Type (ℓ-max a ℓ) where
  constructor isdecstrictpartialorder
  infix 4 _<?_
  field
    isStrictPartialOrder : IsStrictPartialOrder
    _<?_                 : Decidable _<>_

  open IsStrictPartialOrder isStrictPartialOrder public hiding (raw)

  raw : isSet A → Raw.IsDecStrictPartialOrder
  raw isSetA = record
    { isStrictPartialOrder = IsStrictPartialOrder.raw isStrictPartialOrder
    ; _<?_ = _<?_
    }

------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------

record IsTotalOrder : Type (ℓ-max a ℓ) where
  constructor istotalorder
  field
    isPartialOrder : IsPartialOrder
    total          : Total _<>_

  open IsPartialOrder isPartialOrder public hiding (raw)

  raw : isSet A → Raw.IsTotalOrder
  raw isSetA = record
    { isPartialOrder = IsPartialOrder.raw isPartialOrder isSetA
    ; total = total
    }

record IsDecTotalOrder : Type (ℓ-max a ℓ) where
  constructor isdectotalorder
  infix 4 _≤?_
  field
    isTotalOrder : IsTotalOrder
    _≤?_         : Decidable _<>_

  open IsTotalOrder isTotalOrder public hiding (raw)

  isDecPartialOrder : IsDecPartialOrder
  isDecPartialOrder = record
    { isPartialOrder = isPartialOrder
    ; _≤?_           = _≤?_
    }

  raw : isSet A → Raw.IsDecTotalOrder
  raw isSetA = record
    { isTotalOrder = IsTotalOrder.raw isTotalOrder isSetA
    ; _≤?_ = _≤?_
    }

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
-- definition capturing these three properties implies decidability
-- as `Trichotomous` necessarily separates out the equality case.

record IsStrictTotalOrder : Type (ℓ-max a ℓ) where
  constructor isstricttotalorder
  field
    transitive : Transitive _<>_
    compare    : Trichotomous _<>_

  infix 4 _<?_

  _<?_ : Decidable _<>_
  _<?_ = tri→dec< _<>_ compare

  _≟_ : Discrete A
  _≟_ = tri→dec≡ _<>_ compare

  isStrictPartialOrder : IsStrictPartialOrder
  isStrictPartialOrder = record
    { irrefl     = tri→irr _<>_ compare
    ; transitive = transitive
    }

  isDecStrictPartialOrder : IsDecStrictPartialOrder
  isDecStrictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    ; _<?_                 = _<?_
    }

  open IsStrictPartialOrder isStrictPartialOrder public hiding (transitive; raw)

  raw : isSet A → Raw.IsStrictTotalOrder
  raw isSetA = record
    { transitive = transitive
    ; compare = triRaw compare
    }
    where
      import Cubical.Relation.Binary.Raw.Definitions as RawDefinitions
      triRaw : Trichotomous _<>_ → RawDefinitions.Trichotomous [ _<>_ ]
      triRaw tri x y with tri x y
      ... | tri< a b c = RawDefinitions.tri< a b c
      ... | tri≡ a b c = RawDefinitions.tri≡ a b c
      ... | tri> a b c = RawDefinitions.tri> a b c


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2020 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 Data.Unit.NonEta
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Product.Properties
open import Data.Fin hiding (_<_; _≤_)
open import Data.Fin.Properties using () renaming (_≟_ to _≟Fin_)
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Properties
open import Data.List renaming (map to List-map)
open import Data.List.Properties using (∷-injective; length-map)
open import Data.List.Relation.Unary.Any renaming (map to Any-map)
open import Data.List.Relation.Unary.All renaming (lookup to All-lookup; map to All-map)
open import Data.List.Relation.Unary.All.Properties hiding (All-map)
open import Data.List.Relation.Unary.Any.Properties renaming (map⁺ to Any-map⁺)
open import Data.List.Relation.Binary.Pointwise using (decidable-≡)
open import Data.Bool hiding (_<_; _≤_)
open import Data.Maybe renaming (map to Maybe-map)
open import Function

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Relation.Nullary

open import AAOSL.Lemmas
open import AAOSL.Abstract.Hash
open import AAOSL.Abstract.DepRel

-- This module defines the DepRel type, which represents the class of AAOSLs we
-- consider, and proves properties about any DepRel.

module AAOSL.Abstract.Advancement
   -- A Hash function maps a bytestring into a hash.
   (hash    : ByteString → Hash)
   -- And is collision resistant
   (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)

   -- Indexes can be encoded in an injective way
   (encodeI     : ℕ → ByteString)
   (encodeI-inj : (m n : ℕ) → encodeI m ≡ encodeI n → m ≡ n)

   (dep  : DepRel)
 where

  -- Brings the DepRel names into scope instantiated
  -- for the module parameters in question.
  open DepRel dep

  hop-prog : ∀{m}(h : HopFrom m) → hop-tgt h ≢ m
  hop-prog = <⇒≢ ∘ hop-<

  hop-≤ : ∀{m}(h : HopFrom m) → hop-tgt h ≤ m
  hop-≤ = <⇒≤ ∘ hop-<

  depsof : ℕ → List ℕ
  depsof 0       = []
  depsof (suc i) = List-map hop-tgt (nats (lvlof (suc i)))

  depsof-ne : ∀ m → depsof m ≡ [] → m ≡ 0
  depsof-ne 0       hyp = refl
  depsof-ne (suc m) hyp =
    let le0 = trans (sym (length-map hop-tgt (nats (lvlof (suc m)))) )
                    (cong length hyp)
        le-nz = nats-length (lvlof-s m)
     in ⊥-elim (1≤0-⊥ (subst (1 ≤_) le0 le-nz))

  hopFromZ-⊥ : (h : HopFrom 0) → ⊥
  hopFromZ-⊥ h = fin0-⊥ (subst Fin lvlof-z h)
    where fin0-⊥ : Fin 0 → ⊥
          fin0-⊥ ()

  hop-tgt-is-dep : {m : ℕ}(h : HopFrom m)
                 → hop-tgt h ∈ depsof m
  hop-tgt-is-dep {0}     h = ⊥-elim (hopFromZ-⊥ h)
  hop-tgt-is-dep {suc m} h = Any-map⁺ (Any-map (cong hop-tgt) (nats-correct h))

  -- Two simple but useful lemmas made to work over our abstract
  -- index type.
  ≤-≢-mon : ∀{i j tgt} → tgt ≢ j → tgt ≤ j → i ≤ tgt → i ≢ j
  ≤-≢-mon tgt≢j tgt≤j i≤tgt i≡j
    = tgt≢j (sym (≤-antisym (subst (_≤ _) i≡j i≤tgt) tgt≤j))

  ≟ℕ-refl : (s : ℕ) → (s ≟ℕ s) ≡ yes refl
  ≟ℕ-refl s with s ≟ℕ s
  ...| no abs   = ⊥-elim (abs refl)
  ...| yes refl = refl

  ⊥-prop : (a b : ⊥) → a ≡ b
  ⊥-prop () ()

  ≟ℕ-neg : (m n : ℕ) → (p : m ≢ n) → (m ≟ℕ n) ≡ no p
  ≟ℕ-neg m n p with m ≟ℕ n
  ...| yes imp = ⊥-elim (p imp)
  ...| no  r   = cong no (fun-ext (λ x → ⊥-prop (r x) (p x)))

  HopFrom≢0 : ∀{j}(h : HopFrom j) → j ≢ 0
  HopFrom≢0 {j} h refl = hopFromZ-⊥ h

  open WithCryptoHash hash hash-cr

  -- This function is total, even though we won't always know a hash for every
  -- index.  That's ok, we only use the hashes of the relevant indexes.
  View : Set
  View = ℕ → Hash

  -- An inhabitant of 'Agree s t ixs' is a proof that the views s and t
  -- agree on the hash of every index i ∈ ixs.
  Agree : View → View → List ℕ → Set
  Agree v u = All (λ s → v s ≡ u s)

  -- Returns the list of hashes that the authenticator
  -- at the given index depends on.
  deps-hash : ℕ → View → List Hash
  deps-hash s tbl = List-map tbl (depsof s)

  -- TODO-2: Make auth, auth-inj-1 and auth-inj-2 module parameters
  -- TODO-1: Make sure the names are consistent with the paper

  --------------------------
  -- Defining authenticators

  -- Authenticators will depend on all p-auths of the
  -- dependencies of a node.
  auth : (s : ℕ) → Hash → View → Hash
  auth s h tbl = hash-concat (hash (encodeI s) ∷ h ∷ deps-hash s tbl)

  -- We will be using two separate injectivity functions. One is
  -- for the hash of the data in a node, which can't be the
  -- initial node!
  auth-inj-1 : {j : ℕ}{h₁ h₂ : Hash}{t₁ t₂ : View}
             → j ≢ 0
             → auth j h₁ t₁ ≡ auth j h₂ t₂
             → HashBroke ⊎ h₁ ≡ h₂
  auth-inj-1 {j} {h₁} {h₂} {t₁} {t₂} j≢s₀ hip
    with hash-concat-inj { hash (encodeI j) ∷ h₁ ∷ deps-hash j t₁ }
                         { hash (encodeI j) ∷ h₂ ∷ deps-hash j t₂ } hip
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ r  = inj₂ (proj₁ (∷-injective (proj₂ (∷-injective r))))

  -- The second one does induction on the list of dependencies.
  auth-inj-2 : {i : ℕ}{h : Hash}(t₁ t₂ : View)
             → auth i h t₁ ≡ auth i h t₂
             → HashBroke ⊎ Agree t₁ t₂ (depsof i)
  auth-inj-2 {i} {h} t₁ t₂ hip
    with hash-concat-inj { hash (encodeI i) ∷ h ∷ deps-hash i t₁ }
                         { hash (encodeI i) ∷ h ∷ deps-hash i t₂ } hip
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ r  = inj₂ (auth-inj-2-aux t₁ t₂ (depsof i) (proj₂ (∷-injective (proj₂ (∷-injective r)))))
    where
      auth-inj-2-aux : (t₁ t₂ : View)(l : List ℕ)
                     → List-map t₁ l ≡ List-map t₂ l
                     → Agree t₁ t₂ l
      auth-inj-2-aux t1 t2 [] hyp = []
      auth-inj-2-aux t1 t2 (x ∷ l) hyp = proj₁ (∷-injective hyp) ∷ auth-inj-2-aux t1 t2 l (proj₂ (∷-injective hyp))

  ------------------------
  ------------------------
  -- Advancement Proofs --
  ------------------------
  ------------------------

  -- Finally, advancement proofs in their simple variant
  data AdvPath : ℕ → ℕ → Set where
    AdvDone  : ∀{i} → AdvPath i i
    AdvThere : ∀{j i}
             → Hash -- datum digest
             → (h : HopFrom j)
             → AdvPath (hop-tgt h) i
             → AdvPath j i

  -- Override a view with a hash for a specific index.
  _∪₁_ : View → ℕ × Hash → View
  _∪₁_ tbl (s , h) s'
     with s ≟ℕ s'
  ...| yes _ = h
  ...| no  _ = tbl s'

  -- The rebuild function is, essentially, a transformer over
  -- the current view of the skiplog. It is PARAMOUNT to return
  -- a new 'view' of the world, as we can see in rebuild-⊕ lemma.
  -- Otherwise, it becomes seriously intricate to express
  -- that rebuilding the hash of index j "depends on" the rebuilt
  -- hashes of j's dependencies.
  rebuild : ∀{i j} → AdvPath j i → View → View
  rebuild {i} AdvDone tbl = tbl
  rebuild (AdvThere {j = j} x h prf) tbl
    = let tbl' = rebuild prf tbl
       in tbl' ∪₁ (j , auth j x tbl')

  lemma1 : ∀{j i} → AdvPath j i → i ≤ j
  lemma1 AdvDone              = ≤-refl
  lemma1 {j} (AdvThere x h a) = ≤-trans (lemma1 a) (hop-≤ h)

  rebuild-tgt-lemma : ∀{j i}(a : AdvPath j i){t : View}
                    → rebuild a t i ≡ t i
  rebuild-tgt-lemma AdvDone = refl
  rebuild-tgt-lemma {j} {i} (AdvThere x h a)
    rewrite ≟ℕ-neg j i (<⇒≢ (≤-<-trans (lemma1 a) (hop-< h)) ∘ sym)
          = rebuild-tgt-lemma a

  lemma2 : ∀{i}(a : AdvPath i i) → a ≡ AdvDone
  lemma2 AdvDone = refl
  lemma2 (AdvThere x h a)
    = ⊥-elim (hop-prog h (sym (≤-antisym (lemma1 a) (hop-≤ h))))

  -- Lemma3 states that if a hop exists, then it is not from
  -- s₀. This is necessary to eliminate some nasty cases.
  lemma3 : ∀{j i} → (h : HopFrom j) → AdvPath (hop-tgt h) i → j ≢ 0
  lemma3 h a = HopFrom≢0 h

  ----------------------
  -- Proof Splitting  --
  ----------------------

  _⊕_ : ∀{j k i} → AdvPath j k → AdvPath k i → AdvPath j i
  AdvDone          ⊕ rest = rest
  (AdvThere d h a) ⊕ rest = AdvThere d h (a ⊕ rest)

  ⊕-id-r : ∀{j i}(a : AdvPath j i) → a ⊕ AdvDone ≡ a
  ⊕-id-r AdvDone = refl
  ⊕-id-r (AdvThere x h a) = cong (AdvThere x h) (⊕-id-r a)

  -- A value of type 'i ∈AP a' illustrates index i as a dependency
  -- of 'a'.
  data _∈AP_ (i₀ : ℕ) : {j i : ℕ} → AdvPath j i → Set where
    hereTgtDone  : i₀ ∈AP (AdvDone {i₀})

    hereTgtThere : ∀{i}{d : Hash}{hop : HopFrom i₀}{a : AdvPath (hop-tgt hop) i}
                 → i₀ ∈AP (AdvThere d hop a)

    step         : ∀{i j}{d : Hash}{hop : HopFrom j}{a : AdvPath (hop-tgt hop) i}
                 → i₀ ≢ j
                 → i₀ ∈AP a
                 → i₀ ∈AP (AdvThere d hop a)

  ∈AP-src : ∀{j i}{a : AdvPath j i}
          → j ∈AP a
  ∈AP-src {a = AdvDone}        = hereTgtDone
  ∈AP-src {a = AdvThere x h a} = hereTgtThere

  ∈AP-tgt : ∀{j i}{a : AdvPath j i}
          → i ∈AP a
  ∈AP-tgt {a = AdvDone}        = hereTgtDone
  ∈AP-tgt {a = AdvThere x h a} = step (<⇒≢ (≤-<-trans (lemma1 a) (hop-< h))) ∈AP-tgt

  ∈AP-≤ : ∀{j i}{a : AdvPath j i}
               → {i0 : ℕ} → i0 ∈AP a
               → i0 ≤ j
  ∈AP-≤ hereTgtDone  = ≤-refl
  ∈AP-≤ hereTgtThere = ≤-refl
  ∈AP-≤ (step _ hyp) = ≤-trans (∈AP-≤ hyp) (hop-≤ _)

  ∈AP-≥ : ∀{j i}{a : AdvPath j i}
        → {i0 : ℕ} → i0 ∈AP a
        → i ≤ i0
  ∈AP-≥ hereTgtDone = ≤-refl
  ∈AP-≥ {a = a} hereTgtThere = lemma1 a
  ∈AP-≥ (step _ hyp) = ∈AP-≥ hyp

  rebuild-⊕' : ∀{j k i}
             → {t : View}
             → (a₁ : AdvPath j k)
             → (a₂ : AdvPath k i)
             → ∀{l} → l ∈AP a₂
             → rebuild (a₁ ⊕ a₂) t l ≡ rebuild a₂ t l
  rebuild-⊕' AdvDone a₂ hyp = refl
  rebuild-⊕' {j} (AdvThere x h a₁) a₂ {l} hyp
    with j ≟ℕ l
  ...| yes nope = ⊥-elim (≤-≢-mon (hop-prog h) (hop-≤ h)
                          (≤-trans (∈AP-≤ hyp) (lemma1 a₁)) (sym nope))
  ...| no ok    = rebuild-⊕' a₁ a₂ hyp

  ∈AP-cut : ∀{j k i}
          → (a : AdvPath j i)
          → k ∈AP a
          → Σ (AdvPath j k × AdvPath k i)
              (λ { (x , y) → a ≡ x ⊕ y })
  ∈AP-cut AdvDone hereTgtDone
    = (AdvDone , AdvDone) , refl
  ∈AP-cut (AdvThere d h a) hereTgtThere
    = (AdvDone , AdvThere d h a) , refl
  ∈AP-cut (AdvThere d h a) (step x prf)
    with ∈AP-cut a prf
  ...| xy , ind = (AdvThere d h (proj₁ xy) , proj₂ xy)
                , cong (AdvThere d h) ind

  ∈AP-cut₁ : ∀{j k i}
           → (a : AdvPath j i)
           → k ∈AP a
           → AdvPath k i
  ∈AP-cut₁ a prf = proj₂ (proj₁ (∈AP-cut a prf))

  ∈AP-∈-cut
    : ∀{j k i}
    → (a : AdvPath j i)
    → (prf : k ∈AP a)
    → ∀{m} → m ∈AP a → m ≤ k
    → m ∈AP (∈AP-cut₁ a prf)
  ∈AP-∈-cut AdvDone hereTgtDone m∈ap hyp = m∈ap
  ∈AP-∈-cut (AdvThere _ _ _) hereTgtThere m∈ap hyp = m∈ap
  ∈AP-∈-cut (AdvThere d h a) (step x prf) hereTgtThere hyp
    = ⊥-elim (<⇒≱ (hop-< h) (≤-trans hyp (∈AP-≤ prf)))
  ∈AP-∈-cut (AdvThere d h a) (step x prf) (step x₁ m∈ap) hyp
    = ∈AP-∈-cut a prf m∈ap hyp

  ∈AP-cut₁-rebuild
    : ∀{j k i}
    → (a : AdvPath j i)
    → (prf : k ∈AP a)
    → {s : ℕ} → (s ∈AP (∈AP-cut₁ a prf))
    → ∀{t} → rebuild a t s ≡ rebuild (∈AP-cut₁ a prf) t s
  ∈AP-cut₁-rebuild a prf s∈cut {t}
    with ∈AP-cut a prf
  ...| (x , y) , refl = rebuild-⊕' x y s∈cut

  rebuild-⊕ : ∀{j k i}
            → {t : View}
            → (a₁ : AdvPath j k)
            → (a₂ : AdvPath k i)
            → rebuild (a₁ ⊕ a₂) t k ≡ rebuild a₂ t k
  rebuild-⊕ {k = k} a₁ AdvDone = rebuild-⊕' a₁ AdvDone {k} hereTgtDone
  rebuild-⊕ {k = k} {i = i} a₁ (AdvThere .{k} d h p) = rebuild-⊕' a₁ (AdvThere d h p) hereTgtThere

  ∈AP-⊕ : ∀{j i₁ k i₂ i}
        → {e  : AdvPath j k}{a₁ : AdvPath k i₁}
        → {a₂ : AdvPath k i₂}
        → i ∈AP (e ⊕ a₁)
        → i ∈AP a₂
        → i ∈AP a₁
  ∈AP-⊕ {e = AdvDone}        hyp1 hyp2 = hyp1
  ∈AP-⊕ {e = AdvThere x h e} hereTgtThere   hyp2
    with ≤-antisym (∈AP-≤ hyp2) (lemma1 (AdvThere x h e))
  ...| refl = ⊥-elim (hop-prog h (≤-antisym (hop-≤ h) (lemma1 e)))
  ∈AP-⊕ {e = AdvThere x h e} (step x₁ hyp1) hyp2 = ∈AP-⊕ hyp1 hyp2

  ∈AP-point' : ∀{j k i}
             → {a₁ : AdvPath j k}
             → {a₂ : AdvPath k i}
             → {m : ℕ} → m ∈AP a₁ → m ∈AP a₂
             → m ≡ k
  ∈AP-point' hereTgtDone h2 = refl
  ∈AP-point' {a₁ = AdvThere d h a₁} {a₂} hereTgtThere h2
    = ⊥-elim (≤-≢-mon (≤-≢-mon (hop-prog h) (hop-≤ h) (lemma1 a₁) ∘ sym)
                      (∈AP-≤ h2)
                      (lemma1 (AdvThere d h a₁)) refl)
  ∈AP-point' (step x h1) h2 = ∈AP-point' h1 h2

  ∈AP-point'' : ∀{j₁ j₂ i₁ i₂}
              → {a₁ : AdvPath j₁ i₁}
              → {a₂ : AdvPath j₂ i₂}
              → j₂ < i₁
              → {i : ℕ} → i ∈AP a₁ → i ∈AP a₂
              → ⊥
  ∈AP-point'' j<i hereTgtDone h2
    = (<⇒≢ j<i) (≤-antisym (<⇒≤ j<i) (∈AP-≤ h2))
  ∈AP-point'' {a₁ = a₁} j<i hereTgtThere h2
    = (<⇒≢ j<i) (≤-antisym (<⇒≤ j<i) (≤-trans (lemma1 a₁) (∈AP-≤ h2)))
  ∈AP-point'' j<i (step x h1) h2 = ∈AP-point'' j<i h1 h2

  ∈AP-point : ∀{j₁ j₂ i₁ i₂}
            → {a₁ : AdvPath j₁ i₁}
            → {a₂ : AdvPath j₂ i₂}
            → j₂ ≤ i₁
            → {i : ℕ} → i ∈AP a₁ → i ∈AP a₂
            → j₂ ≡ i₁ × i ≡ j₂
  ∈AP-point {j₂ = j₂} {i₁ = i₁} j₂≤i₁ h1 h2
    with j₂ ≟ℕ i₁
  ...| no abs = ⊥-elim (∈AP-point'' (≤∧≢⇒< j₂≤i₁ abs) h1 h2)
  ...| yes refl = refl , ∈AP-point' h1 h2

  ∈AP-AdvDone-≡ : ∀{i j}
                → i ∈AP (AdvDone {j})
                → i ≡ j
  ∈AP-AdvDone-≡ hereTgtDone = refl

  -- It is important that we can split proofs. Here, we know that 'a'
  -- and the guide are proofs that come from jump from the same source, j.
  split-⊕ : ∀{J j i}
           → {H : HopFrom J}
           → {h : HopFrom j}
           → j ≤ J
           → hop-tgt H < hop-tgt h
           → i ≤ hop-tgt H
           → (a : AdvPath (hop-tgt h) i)
           → Σ (AdvPath (hop-tgt h) (hop-tgt H) × AdvPath (hop-tgt H) i)
               (λ { (x , y) → a ≡ x ⊕ y })
  split-⊕ j≤J H<h i≤H AdvDone
    = ⊥-elim (≤-≢-mon (<⇒≢ H<h) (<⇒≤ H<h) i≤H refl)
  split-⊕ {i = i} {H} {h} j≤J H<h i≤H (AdvThere d h' a)
    with hop-tgt h' ≟ℕ hop-tgt H
  ...| yes sameHop = (AdvThere d h' (subst (AdvPath (hop-tgt h')) sameHop AdvDone)
                     , subst (λ P → AdvPath P i) sameHop a)
                     , aux sameHop a
     where
      aux : ∀{i j k}{h : HopFrom j} → (stop : hop-tgt h ≡ k)
          → (a : AdvPath (hop-tgt h) i)
          → AdvThere d h a
            ≡ (AdvThere d h (subst (AdvPath (hop-tgt h)) stop AdvDone)
               ⊕ subst (λ P → AdvPath P i) stop a)
      aux refl a = refl
  ...| no  diffHop
    with ≤-total (hop-tgt h') (hop-tgt H)
  ...| inj₁ crossover with hops-nested-or-nonoverlapping (≤∧≢⇒< crossover diffHop)
                                                         H<h
  ...| abs = ⊥-elim (≤-≢-mon (mmm (hop-≤ h) (hop-prog h) j≤J) (≤-trans (hop-≤ h) j≤J) abs refl)
     where mmm : ∀{h j J} → h ≤ j → h ≢ j → j ≤ J → h ≢ J
           mmm h≤j h≢j j≤J refl = h≢j (≤-antisym h≤j j≤J)
  split-⊕ {i = i} {H} {h} j≤J H<h i≤H (AdvThere d h' a)
     | no diffHop
     | inj₂ go
    with split-⊕ {H = H} (≤-trans (hop-≤ h) j≤J) (≤∧≢⇒< go (diffHop ∘ sym)) i≤H a
  ...| ((x , y) , prf) = (AdvThere d h' x , y) , cong (AdvThere d h') prf

  ---------------------
  -- Evolutionary CR --
  ---------------------

  -- The type 'AgreeOnCommon t₁ t₂ a₁ a₂', or 'AOC' for short, is inhabited if
  -- and only if the advancement proofs a₁ and a₂ agree on the hash they rebuild
  -- for every index that is visited by both. Moreover, the views must also
  -- agree on the dependencies of said indexes.
  data AOC (t₁ t₂ : View)
      : ∀{i₁ i₂ j} → AdvPath j i₁ → AdvPath j i₂ → Set where
    PDoneDone : ∀{i} → t₁ i ≡ t₂ i → AOC t₁ t₂ {i} {i} AdvDone AdvDone

    --                        h
    --             ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
    --             |                     |
    --             |         ⌜⁻⁻⁻ a₁ ⁻⁻⁻⁻|
    --             |         |           |
    --   i₂  ⋯  hop-tgt h  ≤ i₁          j
    PDoneL : ∀{j i₁ i₂}{d}{h : HopFrom j}
           → (a₁ : AdvPath j i₁)
           → (a₂ : AdvPath (hop-tgt h) i₂)
           → hop-tgt h ≤ i₁
           → rebuild a₁ t₁ j ≡ rebuild (AdvThere d h a₂) t₂ j
           → AOC t₁ t₂ a₁ (AdvThere d h a₂)

    PDoneR : ∀{j i₁ i₂}{d}{h : HopFrom j}
           → (a₁ : AdvPath (hop-tgt h) i₁)
           → (a₂ : AdvPath j i₂)
           → hop-tgt h ≤ i₂
           → rebuild (AdvThere d h a₁) t₁ j ≡ rebuild a₂ t₂ j
           → AOC t₁ t₂ (AdvThere d h a₁) a₂

    PCong : ∀{j i₁ i₂}{d}{h : HopFrom j}
          → i₁ ≤ i₂
          → (a₁ : AdvPath (hop-tgt h) i₁)
          → (a₂ : AdvPath (hop-tgt h) i₂)
          → Agree (rebuild a₁ t₁) (rebuild a₂ t₂) (depsof j)
          → AOC t₁ t₂ a₁ a₂
          → AOC t₁ t₂ (AdvThere d h a₁)
                      (AdvThere d h a₂)

    PMeetR : ∀{j i₁ i₂ d}{h₁ h₂ : HopFrom j}
           → (e  : AdvPath (hop-tgt h₁) (hop-tgt h₂))
           → (a₁ : AdvPath (hop-tgt h₂) i₁)
           → (a₂ : AdvPath (hop-tgt h₂) i₂)
           → hop-tgt h₂ < hop-tgt h₁
           → Agree (rebuild (e ⊕ a₁) t₁) (rebuild a₂ t₂) (depsof j)
           → AOC t₁ t₂ a₁ a₂
           → AOC t₁ t₂ (AdvThere d h₁ (e ⊕ a₁))
                       (AdvThere d h₂ a₂)

    PMeetL : ∀{j i₁ i₂ d}{h₁ h₂ : HopFrom j}
           → (e  : AdvPath (hop-tgt h₂) (hop-tgt h₁))
           → (a₁ : AdvPath (hop-tgt h₁) i₁)
           → (a₂ : AdvPath (hop-tgt h₁) i₂)
           → hop-tgt h₁ < hop-tgt h₂
           → Agree (rebuild a₁ t₁) (rebuild (e ⊕ a₂) t₂) (depsof j)
           → AOC t₁ t₂ a₁ a₂
           → AOC t₁ t₂ (AdvThere d h₁ a₁)
                       (AdvThere d h₂ (e ⊕ a₂))

  -- We use the 'TERMINATING' pragma because we use a recursive call on
  -- an argument that Agda can't infer being structurally smaller.
  -- TODO-1: provide clear and detailed explanation of this, which argument, why smaller?
  -- An interesting longer-term TODO-2 would be to use 'Sized Types' to inform
  -- the typechecker of this fact, or perhaps a custom-made moral equivalent.
  {-# TERMINATING #-}
  aoc : ∀{i₁ i₂ j}
      → i₁ ≤ i₂ -- wlog
      → (t₁ t₂ : View)(a₁ : AdvPath j i₁)(a₂ : AdvPath j i₂)
      → rebuild a₁ t₁ j ≡ rebuild a₂ t₂ j
      → HashBroke ⊎ AOC t₁ t₂ a₁ a₂
  aoc _ t1 t2 AdvDone AdvDone hip
    = inj₂ (PDoneDone hip)
  aoc _ t1 t2 AdvDone (AdvThere x h a2) hip
    = inj₂ (PDoneL AdvDone a2 (hop-≤ h) hip)
  aoc _ t1 t2 (AdvThere x h a1) AdvDone hip
    = inj₂ (PDoneR a1 AdvDone (hop-≤ h) hip)
  aoc {i₁} {i₂} {j} k t₁ t₂ (AdvThere d₁ h₁ a₁) (AdvThere d₂ h₂ a₂) hip
    with ≤-total i₂ (hop-tgt h₁)
  ...| inj₂ h₁≤i₂ = inj₂ (PDoneR a₁ (AdvThere d₂ h₂ a₂) h₁≤i₂ hip)
  ...| inj₁ go
    rewrite ≟ℕ-refl j
    with auth-inj-1 {j} {d₁} {d₂} (lemma3 h₁ a₁) hip
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ refl
    with auth-inj-2 {j} {d₁} (rebuild a₁ t₁) (rebuild a₂ t₂) hip
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ agree
    with h₁ ≟Hop h₂
  ...| yes refl
    with witness (hop-tgt-is-dep h₁) agree
  ...| wit rewrite (≟ℕ-refl (hop-tgt h₁))
    with aoc k t₁ t₂ a₁ a₂ wit
  ...| inj₁ hb  = inj₁ hb
  ...| inj₂ rec = inj₂ (PCong k a₁ a₂ agree rec)
  aoc {i₁} {i₂} {j} k t₁ t₂ (AdvThere d₁ h₁ a₁) (AdvThere d₂ h₂ a₂) hip
     | inj₁ go
     | inj₂ refl
     | inj₂ agree
     | no diffHop
    with ≤-total (hop-tgt h₁) (hop-tgt h₂)
  ...| inj₁ h₁<h₂ with split-⊕ ≤-refl (≤∧≢⇒< h₁<h₂ (diffHop ∘ hop-tgt-inj)) go a₂
  ...| ((x , y) , refl)
    with aoc k t₁ t₂ a₁ y (trans (witness (hop-tgt-is-dep h₁) agree) (rebuild-⊕ x y))
  ...| inj₁ hb  = inj₁ hb
  ...| inj₂ res = inj₂ (PMeetL x a₁ y (≤∧≢⇒< h₁<h₂ (diffHop ∘ hop-tgt-inj)) agree res)
  aoc {j = j} k t₁ t₂ (AdvThere d₁ h₁ a₁) (AdvThere d₂ h₂ a₂) hip
     | inj₁ go
     | inj₂ refl
     | inj₂ agree
     | no diffHop
     | inj₂ h₂<h₁ with split-⊕ ≤-refl (≤∧≢⇒< h₂<h₁ (diffHop ∘ hop-tgt-inj ∘ sym))
                         (≤-trans k (lemma1 a₂)) a₁
  ...| ((x , y) , refl)
    with aoc k t₁ t₂ y a₂ (trans (sym (rebuild-⊕ x y))
                                 (witness (hop-tgt-is-dep h₂) agree))
  ...| inj₁ hb  = inj₁ hb
  ...| inj₂ res = inj₂ (PMeetR x y a₂ (≤∧≢⇒< h₂<h₁ (diffHop ∘ hop-tgt-inj ∘ sym)) agree res)

  -- TODO: rename AGREEONCOMMON for consistency with paper, or comment to make connection
  aoc-correct : ∀{j i₁ i₂}{a₁ : AdvPath j i₁}{a₂ : AdvPath j i₂}
              → {t₁ t₂ : View}
              → AOC t₁ t₂ a₁ a₂
              → {i : ℕ} → i ∈AP a₁ → i ∈AP a₂
              → HashBroke ⊎ rebuild a₁ t₁ i ≡ rebuild a₂ t₂ i
  aoc-correct (PDoneDone x) hereTgtDone hereTgtDone = inj₂ x
  aoc-correct (PDoneL a₁ a₂ x x₁) hyp1 hereTgtThere = inj₂ x₁
  aoc-correct {j} {t₁ = t₁} {t₂} (PDoneL {d = d} {h} a₁ a₂ x x₁) {i} hyp1 (step x₂ hyp2)
    with j ≟ℕ i
  ...| yes nope = ⊥-elim (x₂ (sym nope))
  ...| no  ok
    with a₁
  ...| AdvDone rewrite ∈AP-AdvDone-≡ hyp1 = ⊥-elim (x₂ refl)
  ...| AdvThere d₁ h₁ a₁'
    with ∈AP-point x hyp1 hyp2
  ...| refl , refl
    with j ≟ℕ hop-tgt h
  ...| yes nope = ⊥-elim (x₂ (sym nope))
  ...| no ok' rewrite ≟ℕ-refl j
    with auth-inj-1 {h₁ = d₁} {d} (HopFrom≢0 h) x₁
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ refl
    with auth-inj-2 {j} {d₁} (rebuild a₁' t₁) (rebuild a₂ t₂) x₁
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ r  = inj₂ (witness (hop-tgt-is-dep h) r)
  aoc-correct (PDoneR a₁ a₂ x x₁) hereTgtThere hyp2 = inj₂ x₁
  aoc-correct {j} {t₁ = t₁} {t₂} (PDoneR {d = d} {h} a₁ a₂ x x₁) {i} (step x₂ hyp1) hyp2
    with j ≟ℕ i
  ...| yes nope = ⊥-elim (x₂ (sym nope))
  ...| no  ok
    with a₂
  ...| AdvDone rewrite ∈AP-AdvDone-≡ hyp2 = ⊥-elim (x₂ refl)
  ...| AdvThere d₂ h₂ a₂'
    with ∈AP-point x hyp2 hyp1
  ...| refl , refl
    with j ≟ℕ hop-tgt h
  ...| yes nope = ⊥-elim (x₂ (sym nope))
  ...| no ok' rewrite ≟ℕ-refl j
    with auth-inj-1 {h₁ = d₂} {d} (HopFrom≢0 h) (sym x₁)
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ refl
    with auth-inj-2 {j} {d₂} (rebuild a₁ t₁) (rebuild a₂' t₂) x₁
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ r  = inj₂ (witness (hop-tgt-is-dep h) r)
  aoc-correct {j} {t₁ = t₁} {t₂} (PCong x a₁ a₂ x₁ aoc₁) hereTgtThere hereTgtThere
    rewrite ≟ℕ-refl j
          | List-map-≡-All (rebuild a₁ t₁) (rebuild a₂ t₂) (depsof j) x₁
          = inj₂ refl
  aoc-correct (PCong x a₁ a₂ x₁ aoc₁) hereTgtThere (step x₂ hyp2)
    = ⊥-elim (x₂ refl)
  aoc-correct (PCong x a₁ a₂ x₁ aoc₁) (step x₂ hyp1) hereTgtThere
    = ⊥-elim (x₂ refl)
  aoc-correct {j} (PCong x a₁ a₂ x₁ aoc₁) {i} (step x₂ hyp1) (step x₃ hyp2)
    with j ≟ℕ i
  ...| yes nope = ⊥-elim (x₂ (sym nope))
  ...| no  ok   = aoc-correct aoc₁ hyp1 hyp2
  aoc-correct {j} {t₁ = t₁} {t₂} (PMeetR e a₁ a₂ x₁ x₂ aoc₁) hereTgtThere hereTgtThere
    rewrite ≟ℕ-refl j
          | List-map-≡-All (rebuild (e ⊕ a₁) t₁) (rebuild a₂ t₂) (depsof j) x₂
          = inj₂ refl
  aoc-correct (PMeetR e a₁ a₂ x₁ x₂ aoc₁) hereTgtThere (step x₃ hyp2)
    = ⊥-elim (x₃ refl)
  aoc-correct (PMeetR e a₁ a₂ x₁ x₂ aoc₁) (step x₃ hyp1) hereTgtThere
    = ⊥-elim (x₃ refl)
  aoc-correct {j} (PMeetR e a₁ a₂ x₁ x₂ aoc₁) {i} (step x₃ hyp1) (step x₄ hyp2)
    with j ≟ℕ i
  ...| yes nope = ⊥-elim (x₃ (sym nope))
  ...| no  ok
    with aoc-correct aoc₁ (∈AP-⊕ hyp1 hyp2) hyp2
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ r  = inj₂ (trans (rebuild-⊕' e a₁ (∈AP-⊕ hyp1 hyp2)) r)

  aoc-correct {j} {t₁ = t₁} {t₂} (PMeetL e a₁ a₂ x₁ x₂ aoc₁) hereTgtThere hereTgtThere
    rewrite ≟ℕ-refl j
          | List-map-≡-All (rebuild a₁ t₁) (rebuild (e ⊕ a₂) t₂) (depsof j) x₂
          = inj₂ refl
  aoc-correct (PMeetL e a₁ a₂ x₁ x₂ aoc₁) hereTgtThere (step x₃ hyp2)
    = ⊥-elim (x₃ refl)
  aoc-correct (PMeetL e a₁ a₂ x₁ x₂ aoc₁) (step x₃ hyp1) hereTgtThere
    = ⊥-elim (x₃ refl)
  aoc-correct {j} (PMeetL e a₁ a₂ x₁ x₂ aoc₁) {i} (step x₃ hyp1) (step x₄ hyp2)
    with j ≟ℕ i
  ...| yes nope = ⊥-elim (x₃ (sym nope))
  ...| no  ok
    with aoc-correct aoc₁ hyp1 (∈AP-⊕ hyp2 hyp1)
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ r  = inj₂ (trans r (sym (rebuild-⊕' e a₂ (∈AP-⊕ hyp2 hyp1))))

  AgreeOnCommon : ∀{j i₁ i₂}
                → {t₁ t₂ : View}
                → (a₁ : AdvPath j i₁)(a₂ : AdvPath j i₂)
                → rebuild a₁ t₁ j ≡ rebuild a₂ t₂ j
                → {i : ℕ} → i ∈AP a₁ → i ∈AP a₂
                → HashBroke ⊎ rebuild a₁ t₁ i ≡ rebuild a₂ t₂ i
  AgreeOnCommon {i₁ = i₁} {i₂} {t₁} {t₂} a₁ a₂ rebuild-to-j i∈a₁ i∈a₂
     with ≤-total i₁ i₂
  ...| inj₁ i₁≤i₂ with aoc i₁≤i₂ t₁ t₂ a₁ a₂ rebuild-to-j
  ...|              inj₁ hb = inj₁ hb
  ...|              inj₂ xx = aoc-correct xx i∈a₁ i∈a₂

  AgreeOnCommon {i₁ = i₁} {i₂} {t₁} {t₂} a₁ a₂ rebuild-to-j i∈a₁ i∈a₂
     | inj₂ i₂≤i₁ with aoc i₂≤i₁ t₂ t₁ a₂ a₁ (sym rebuild-to-j)
  ...|              inj₁ hb = inj₁ hb
  ...|              inj₂ xx with aoc-correct xx i∈a₂ i∈a₁
  ...|                        inj₁ hb = inj₁ hb
  ...|                        inj₂ xx1 = inj₂ (sym xx1)

  AgreeOnCommon-∈ : ∀{j₁ j₂ i₁ i₂}
                → {t₁ t₂ : View}
                → (a₁ : AdvPath j₁ i₁)(a₂ : AdvPath j₂ i₂)
                → j₂ ∈AP a₁
                → rebuild a₁ t₁ j₂ ≡ rebuild a₂ t₂ j₂
                → {i : ℕ} → i ∈AP a₁ → i ∈AP a₂
                → HashBroke ⊎ rebuild a₁ t₁ i ≡ rebuild a₂ t₂ i
  AgreeOnCommon-∈ a₁ a₂ j2∈a1 hyp ia1 ia2
    with ∈AP-cut a₁ j2∈a1
  ...| ((a₁₁ , a₁₂) , refl)
    with AgreeOnCommon a₁₂ a₂ (trans (sym (rebuild-⊕' a₁₁ a₁₂ ∈AP-src)) hyp) (∈AP-⊕ ia1 ia2) ia2
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ res = inj₂ (trans (rebuild-⊕' a₁₁ a₁₂ (∈AP-⊕ ia1 ia2)) res)

  -----------------------
  -- Membership Proofs --
  -----------------------

  -- A membership proof for i is simply an advancement proof from j to i,
  -- a digest of the data in i and the authenticators that i depends on (which
  -- come in the view)
  MembershipProof : ℕ → ℕ → Set
  MembershipProof j i = AdvPath j i × Hash × i ≢ 0

  mbr-datum : ∀{j i} → MembershipProof j i → Hash
  mbr-datum (_ , d , _) = d

  mbr-proof : ∀{j i} → MembershipProof j i → AdvPath j i
  mbr-proof (p , _ , _) = p

  mbr-not-init : ∀{j i} → MembershipProof j i → i ≢ 0
  mbr-not-init (_ , _ , m) = m

  -- Rebuilding it is the same as rebuilding an advancement proof, but we
  -- explicitely compute the authenticator at i.
  rebuildMP : ∀{j i} → MembershipProof j i → View → View
  rebuildMP {j} {i} mbr t = rebuild (mbr-proof mbr)
                                    (t ∪₁ (i , auth i (mbr-datum mbr) t))

  semi-evo-cr : ∀{j i₁ i₂}{t₁ t₂ : View}
         → (a₁ : AdvPath j i₁)
         → (a₂ : AdvPath j i₂)
         → rebuild a₁ t₁ j ≡ rebuild a₂ t₂ j
         → ∀{s₁ s₂ tgt}{u₁ u₂ : View}
         → (m₁ : MembershipProof s₁ tgt)(m₂ : MembershipProof s₂ tgt)
         → s₁ ∈AP a₁ → s₂ ∈AP a₂
         → tgt ∈AP a₁ → tgt ∈AP a₂
         → tgt ≢ 0
         → rebuildMP m₁ u₁ s₁ ≡ rebuild a₁ t₁ s₁
         → rebuildMP m₂ u₂ s₂ ≡ rebuild a₂ t₂ s₂
         → HashBroke ⊎ (mbr-datum m₁ ≡ mbr-datum m₂)
  semi-evo-cr {t₁ = t₁} {t₂} a₁ a₂ hyp {tgt = tgt} {u₁} {u₂} m₁ m₂ s₁∈a₁ s₂∈a₂ t∈a₁ t∈a₂ t≢0 c₁ c₂
     with AgreeOnCommon (mbr-proof m₁) (∈AP-cut₁ a₁ s₁∈a₁)
                       (trans c₁ (∈AP-cut₁-rebuild a₁ s₁∈a₁ ∈AP-src {t₁}))
                       ∈AP-tgt (∈AP-∈-cut a₁ s₁∈a₁ t∈a₁ (lemma1 (mbr-proof m₁)))
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ hyp1
    with AgreeOnCommon (mbr-proof m₂) (∈AP-cut₁ a₂ s₂∈a₂)
                       (trans c₂ (∈AP-cut₁-rebuild a₂ s₂∈a₂ ∈AP-src {t₂}))
                       ∈AP-tgt (∈AP-∈-cut a₂ s₂∈a₂ t∈a₂ (lemma1 (mbr-proof m₂)))
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ hyp2
    with AgreeOnCommon a₁ a₂ hyp t∈a₁ t∈a₂
  ...| inj₁ hb   = inj₁ hb
  ...| inj₂ hyp3
    rewrite sym (∈AP-cut₁-rebuild a₁ s₁∈a₁
                  (∈AP-∈-cut a₁ s₁∈a₁ t∈a₁ (lemma1 (mbr-proof m₁))) {t₁})
          | sym (∈AP-cut₁-rebuild a₂ s₂∈a₂
                  (∈AP-∈-cut a₂ s₂∈a₂ t∈a₂ (lemma1 (mbr-proof m₂))) {t₂})

    with trans hyp1 (trans hyp3 (sym hyp2))
  ...| half     with rebuild-tgt-lemma (mbr-proof m₁)
                       {u₁ ∪₁ (tgt , auth tgt (mbr-datum m₁) u₁) }
                   | rebuild-tgt-lemma (mbr-proof m₂)
                       {u₂ ∪₁ (tgt , auth tgt (mbr-datum m₂) u₂) }
  ...| l1 | l2
    rewrite ≟ℕ-refl tgt = auth-inj-1 {tgt} {mbr-datum m₁} {mbr-datum m₂} t≢0 (trans (sym l1) (trans half l2))

max_stars_repo_name: VictorCMiraldo/aaosl-agda

max_issues_repo_name: VictorCMiraldo/aaosl-agda

max_forks_repo_name: VictorCMiraldo/aaosl-agda


text:
import Oscar.Class.Transextensionality.Proposequality -- FIXME why not use the instance here?
open import Oscar.Class
open import Oscar.Class.IsPrecategory
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transitivity
open import Oscar.Data.Proposequality
open import Oscar.Prelude
open import Oscar.Property.Setoid.Proposequality

module Test.ConfusionAboutExtension where

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

  instance

    𝓣ransextensionalityProposequality : Transextensionality.class Proposequality⟦ A ⟧ Proposequality transitivity
    -- 𝓣ransextensionalityProposequality = Oscar.Class.Transextensionality.Proposequality.𝓣ransextensionalityProposequality -- using this instead avoids the below-mentioned errors
    𝓣ransextensionalityProposequality .⋆ ∅ ∅ = !

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

  testme : Transextensionality.class Proposequality⟦ A ⟧ (Proposequality) (transitivity)
  testme = ! -- errors

  instance

    IsPrecategoryExtension : IsPrecategory Proposequality⟦ A ⟧ Proposequality transitivity
    IsPrecategoryExtension .IsPrecategory.`𝓣ransextensionality = {!!!} -- FIXME I'd like to use instance search to find this instance, but this errors b/c of
    IsPrecategoryExtension .IsPrecategory.`𝓣ransassociativity = magic