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

module README where

------------------------------------------------------------------------
-- Chapter 2: Programming and Proving in Cubical Agda
------------------------------------------------------------------------

-- 2.1: Basic Functional Programming in Agda
import Snippets.Bool using
  ( Bool -- 2.1
  ; Boolean
  ; a-boolean)

-- 2.2: Some Functions
import Snippets.Bool using
  ( not
  ; module LambdaNot)

import Function using
  ( id
  )

import Snippets.Nat using
  ( ℕ -- 2.2
  ; add
  ; _-_ -- 2.3
  ; module NonCoveringSub
  ; _+_ -- 2.4
  ; module NonTermAdd
  )

-- 2.3: An Expression Evaluator
import Snippets.Expr using
  ( Op -- 2.5
  ; Expr -- 2.6
  ; module IncorrectEval -- 2.7
  )

-- 2.4: Safe Evaluation with Maybe
import Data.Maybe using
  ( Maybe -- 2.8
  )

import Snippets.Maybe using
  ( maybe-two
  ; maybe-func
  )

import Snippets.Expr using
  ( _-_ -- 2.9
  ; ⟦_⟧
  )

import Data.Maybe.Sugar using
  ( pure
  ; _<*>_
  ; _>>=_ -- 2.10
  )

-- 2.5: Statically Proving the Evaluation is Safe

import Snippets.Expr using
  ( example-eval
  ; is-just
  )

import Data.Bool using
  ( T
  )

import Data.Empty using
  ( ⊥
  )

import Snippets.Introduction using
  ( ⊤
  )

import Data.Empty using
  ( ¬_
  )

import Snippets.Expr using
  ( Pair -- 2.11
  ; Valid -- 2.12
  ; ⟦_⟧!
  ; example-static-eval -- 2.13
  )

import Snippets.Implicits using
  ( module Normal
  ; module ImplicitType -- 2.14
  )

-- 2.6: Equalities

import Snippets.Equality using
  ( module MLTTEquality -- 2.15
  ; sym
  )

-- 2.7: Some Proofs of Equality
import Snippets.Equality using
  ( refl -- 2.16
  )

import Snippets.Expr using
  ( example-static-proof
  )

import Data.Nat.Properties using
  ( +-assoc
  )

-- 2.8: Quotients

import Cubical.HITs.S1 using
  ( S¹ -- 2.17
  )

-- 2.9: Basic Type Formers

import Snippets.Formers using
  ( ℕ-or-String
  ; Pair
  ; fst
  ; snd
  ; pair
  )

import Data.Sigma using
  ( Σ
  ; _×_ -- 2.18
  )

import Data.Sum using
  ( _⊎_ -- 2.19
  )

-- 2.11: Comparing Classical and Constructive Proofs in Agda

import Snippets.Classical using
  ( Classical -- 2.20
  ; lem
  ; pure
  ; _>>=_
  )

import Relation.Nullary.Stable using
  ( Stable
  )

------------------------------------------------------------------------
-- Chapter 3: Finiteness Predicates
------------------------------------------------------------------------

-- 3.1: Split Enumerability

import Cardinality.Finite.SplitEnumerable.Container using
  ( ℰ!
  )

import Container.List using
  ( List -- 3.1
  )

import Data.Fin.Base using
  (module DisplayImpl)

import Data.List using
  (List)

import Container using
  ( ⟦_⟧ -- 3.3
  )

import Container.Membership using
  ( _∈_ -- 3.4
  )

import Function.Fiber using
  ( fiber -- 3.5
  )

import Function.Surjective using
  ( SplitSurjective -- 3.6
  ; _↠!_
  )

import Cardinality.Finite.SplitEnumerable using
  ( ℰ!⇔Fin↠!
  )

import Data.Sigma.Properties using
  ( reassoc
  )

import Cardinality.Finite.SplitEnumerable using
  ( split-enum-is-split-surj
  ; ℰ!⟨2⟩ -- 3.7
  )

import Function.Surjective.Properties using
  ( ↠!-ident
  )

import Relation.Nullary.Discrete using
  ( Discrete
  )

import Snippets.Dec using
  ( Dec
  )

import Function.Injective using
  ( Injective
  ; _↣_
  )

import Function.Injective.Properties using
  (Discrete-pull-inj)

import Function.Surjective.Properties using
  ( surj-to-inj
  ; Discrete-distrib-surj
  )

import Cardinality.Finite.SplitEnumerable using
  (ℰ!⇒Discrete)

-- 3.2: Manifest Bishop Finiteness

import Cardinality.Finite.SplitEnumerable using
  ( module BoolSlop -- 3.8
  )

import HLevels using
  ( isContr -- 3.9
  )

import Container.Membership using
  ( _∈!_ -- 3.10
  )

import Cardinality.Finite.ManifestBishop.Container using
  ( ℬ
  )

import Snippets.Equivalence using
  ( isEquiv -- 3.11
  ; _≃_
  )

import Cardinality.Finite.ManifestBishop using
  ( ℬ⇔Fin≃
  )

-- 3.3: Cardinal Finiteness

import Cardinality.Finite.SplitEnumerable using
  ( ℰ!⟨2⟩
  ; ℰ!⟨2⟩′
  )

import HLevels using
  ( isProp -- 3.12
  )

import HITs.PropositionalTruncation using
  ( ∥_∥ -- 3.13
  ; rec -- 3.14
  )

import Cardinality.Finite.Cardinal using
  ( 𝒞
  ; 𝒞⇒Discrete
  )

import Relation.Nullary.Discrete.Properties using
  ( isPropDiscrete
  )

import HLevels using
  ( isSet -- 3.15
  )

import Relation.Nullary.Discrete.Properties using
  ( Discrete→isSet
  )

import HITs.PropositionalTruncation using
  ( rec→set -- 3.16
  )

import Cardinality.Finite.Cardinal using
  ( cardinality-is-unique
  )

import Data.List.Sort using
  ( insert
  ; sort
  ; sort-sorts
  ; sort-perm
  )

import Data.List.Relation.Binary.Permutation using
  ( _↭_
  )

import Data.List.Sort using
  ( sorted-perm-eq
  ; perm-invar
  )

import Cardinality.Finite.Cardinal using
  ( ¬⟨𝒞⋂ℬᶜ⟩
  )

import Snippets.Classical using
  ( classical-impl
  )

-- 3.4: Manifest Enumerability

import Cubical.HITs.S1 using
  ( S¹ -- 3.19
  )

import HLevels using
  ( isGroupoid -- 3.20
  )

import Cardinality.Finite.ManifestEnumerable.Container using
  ( ℰ
  )

import Cardinality.Finite.ManifestEnumerable using
  ( ℰ⟨S¹⟩
  )

import Cubical.HITs.S1 using
  ( isConnectedS¹
  )

import Function.Surjective using
  ( Surjective -- 3.21
  ; _↠_
  )

import Cardinality.Finite.ManifestEnumerable using
  (  ℰ⇔Fin↠
  )

import HITs.PropositionalTruncation.Properties using
  ( recompute -- 3.22
  )

-- 3.5: Kuratowski Finiteness

import Algebra.Construct.Free.Semilattice using
  ( 𝒦 -- 3.23
  )

import Algebra.Construct.Free.Semilattice.Direct using
  ( 𝒦
  )

import Algebra.Construct.Free.Semilattice.Relation.Unary.Membership using
  ( _∈_
  )

import Cardinality.Finite.Kuratowski using
  ( 𝒦ᶠ
  ; 𝒞⇔𝒦×Discrete -- 3.24
  )

------------------------------------------------------------------------
-- Chapter 4: Topos
------------------------------------------------------------------------

-- 4.1: Categories in HoTT

import Categories using
  ( PreCategory -- 4.1
  )

-- 4.2: The Category of Sets

import Categories.HSets using
  ( Ob
  )

-- 4.3: Closure

import Cardinality.Finite.SplitEnumerable using
  ( _|Σ|_
  ; sup-Σ
  )

import Cardinality.Finite.ManifestBishop using
  ( _|Π|_
  )

import Data.Tuple.UniverseMonomorphic using
  ( Tuple
  )

import Cardinality.Finite.Cardinal using
  ( _∥×∥_
  ; 𝒞⇒Choice
  )

-- 4.4: The Absence of the Subobject Classifier

import Snippets.Topos using
  ( Prop-univ
  ; prop-resize
  )

------------------------------------------------------------------------
-- Chapter 5: Search
------------------------------------------------------------------------

import Snippets.Bool using
  ( _∧_
  ; ∧-assoc -- 5.1
  ; some-assoc
  )

-- 5.1: How to make the Typechecker do Automation

import Snippets.Bool using
  ( obvious
  ; True
  ; toWitness
  ; extremely-obvious
  )

-- 5.2: Omniscience

import Relation.Nullary.Omniscience using
  ( Exhaustible
  ; Omniscient
  )

import Relation.Nullary.Decidable.Properties using
  ( Dec→DoubleNegElim
  )

import Relation.Nullary.Omniscience using
  ( Omniscient→Exhaustible
  )

import Cardinality.Finite.Kuratowski using
  ( 𝒦ᶠ⇒Exhaustible
  )

import Cardinality.Finite.ManifestEnumerable using
  ( ℰ⇒Omniscient
  )

import Relation.Nullary.Omniscience using
  ( Prop-Omniscient
  )

import Cardinality.Finite.Kuratowski using
  ( 𝒦ᶠ⇒Prop-Omniscient
  )

-- 5.3: An Interface for Proof Automation

import Cardinality.Finite.SplitEnumerable.Search using
  ( ∀?
  ; ∃?
  ; module PreInst
  )

import Snippets.Bool using
  ( module PreInst′
  )

import Cardinality.Finite.SplitEnumerable.Search using
  ( module WithInst
  )

import Snippets.Bool using
  ( ∧-idem -- 5.2
  ; module BadCurrying
  )

import Instance using
  ( it
  )

import Data.Product.NAry using
  ( Levels
  ; max-level
  ; Types
  ; ⦅_⦆⁺
  ; ⦅_⦆
  ; ArgForm
  ; _[_]→_
  ; [_$]
  ; Π[_$]
  ; ⦅_⦆[_]→_
  ; pi-arrs-plus
  ; Π[_^_$]
  )

import Cardinality.Finite.SplitEnumerable.Search using
  ( ∃?ⁿ
  ; ∃↯ⁿ
  )

import Snippets.Bool using
  ( ∧-comm
  )

-- 5.4: Countdown

import Countdown using
  ( ℰ!⟨Vec⟩
  ; ℰ!⟨Op⟩
  ; module WrongPerm
  ; module IsoPerm
  ; Perm
  ; ℰ!⟨Perm⟩
  )

import Dyck using
  ( Dyck
  ; module NonParamTree
  )

import Countdown using
  ( ExprTree
  ; Transformation
  ; ℰ!⟨ExprTree⟩
  ; ℰ!⟨Transformation⟩
  ; eval
  ; _!⟨_⟩!_
  ; Solution
  ; exampleSolutions
  )

------------------------------------------------------------------------
-- Chapter 6: Countably Infinite Types
------------------------------------------------------------------------

-- 6.1: Countability

import Cardinality.Infinite.Split using
  ( ℵ!
  )

import Codata.Stream using
  ( Stream
  )

import Cardinality.Infinite.Split using
  ( ℵ!⇔ℕ↠!
  )

-- 6.2: Closure

import Data.List.Kleene using
  ( _⁺
  ; _⋆
  )

import Cardinality.Infinite.Split using
  ( _*⋆_[_]
  ; _*_
  ; _|Σ|_
  ; |star|
  ; cantor-diag
  )

max_stars_repo_name: oisdk/masters-thesis

max_issues_repo_name: oisdk/masters-thesis

max_forks_repo_name: oisdk/masters-thesis


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

record U : Set where
  coinductive
  field out : U

u : {A : Set} → U
u = {!!}

record Wrap (A : Set) : Set where
  field
    wrapped : A

wrap : ∀{A}{a : A} → Wrap A
wrap = {!!}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-
   Copyright (c) 2017 Diego Pedraza.

   This is Free/Libre Open Source Software, released under the MIT License.
   For the full copyright and license information, please view the LICENSE
   file that was distributed with this source code.
 -}

module R2 where

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

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

{- ---------------------------------------------------------------
  Ejercicio 1.1. Definir la función
     sumaImpares :: nat ⇒ nat
  tal que (sumaImpares n) es la suma de los n primeros números
  impares. Por ejemplo,
     sumaImpares 5  =  25
  ---------------------------------------------------------------- -}

sumaImpares : ℕ → ℕ
sumaImpares 0 = 0
sumaImpares (suc n) = (2 * n + 1) + sumaImpares n

{- ---------------------------------------------------------------
  Ejercicio 1.2. Demostrar que
     sumaImpares n = n*n
  ----------------------------------------------------------------- -}
_≡_ : ℕ → ℕ → Bool
0 ≡ 0 = true
(suc n) ≡ (suc m) = n ≡ m
n ≡ 0 = false
0 ≡ m = false

lemaSumaImpares : {n : ℕ} → (sumaImpares n) ≡ (n * n)
lemaSumaImpares {zero} = ?
lemaSumaImpares {suc n} = ?

{-

{- ---------------------------------------------------------------
  Ejercicio 2.1. Definir la función
     sumaPotenciasDeDosMasUno :: nat ⇒ nat
  tal que
     (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
  Por ejemplo,
     sumaPotenciasDeDosMasUno 3  =  16
  ---------------------------------------------------------------- -}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
  "sumaPotenciasDeDosMasUno n = undefined"

{- ---------------------------------------------------------------
  Ejercicio 2.2. Demostrar que
     sumaPotenciasDeDosMasUno n = 2^(n+1)
  ----------------------------------------------------------------- -}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
  oops

{- ---------------------------------------------------------------
  Ejercicio 3.1. Definir la función
     copia :: nat ⇒ 'a ⇒ 'a list
  tal que (copia n x) es la lista formado por n copias del elemento
  x. Por ejemplo,
     copia 3 x = [x,x,x]
  ---------------------------------------------------------------- -}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
  "copia n x = undefined"

{- ---------------------------------------------------------------
  Ejercicio 3.2. Definir la función
     todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (todos p xs) se verifica si todos los elementos de xs cumplen
  la propiedad p. Por ejemplo,
     todos (λx. x>(1::nat)) [2,6,4] = True
     todos (λx. x>(2::nat)) [2,6,4] = False
  Nota: La conjunción se representa por ∧
  --------------------------------------------------------------- -}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p xs = undefined"

{- ---------------------------------------------------------------
  Ejercicio 3.3. Demostrar que todos los elementos de (copia n x) son
  iguales a x.
  ----------------------------------------------------------------- -}

lemma "todos (λy. y=x) (copia n x)"
  oops

{- ---------------------------------------------------------------
  Ejercicio 4.1. Definir, recursivamente y sin usar (@), la función
     amplia :: 'a list ⇒ 'a ⇒ 'a list
  tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
  final de la lista xs. Por ejemplo,
     amplia [d,a] t = [d,a,t]
  ---------------------------------------------------------------- -}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia xs y = undefined"

{- ---------------------------------------------------------------
  Ejercicio 4.2. Demostrar que
     amplia xs y = xs @ [y]
  ----------------------------------------------------------------- -}

lemma "amplia xs y = xs @ [y]"
  oops
-}

max_stars_repo_name: Zegeri/TFG-TeoriaCategorias

max_issues_repo_name: Zegeri/TFG-TeoriaCategorias

max_forks_repo_name: Zegeri/TFG-TeoriaCategorias


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.NatSolver.Solver where

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base
open import Cubical.Algebra.NatSolver.NatExpression
open import Cubical.Algebra.NatSolver.HornerForms
open import Cubical.Algebra.NatSolver.EvalHom

private
  variable
    ℓ : Level

module EqualityToNormalform where
  open Eval
  open IteratedHornerOperations
  open HomomorphismProperties

  normalize : {n : ℕ} → Expr n → IteratedHornerForms n
  normalize {n = n} (K r) = Constant n r
  normalize {n = n} (∣ k) = Variable n k
  normalize (x +' y) =
    (normalize x) +ₕ (normalize y)
  normalize (x ·' y) =
    (normalize x) ·ₕ (normalize y)

  isEqualToNormalform :
            {n : ℕ}
            (e : Expr n) (xs : Vec ℕ n)
          → eval (normalize e) xs ≡ ⟦ e ⟧ xs
  isEqualToNormalform (K r) [] = refl
  isEqualToNormalform {n = ℕ.suc n} (K r) (x ∷ xs) =
     eval (Constant (ℕ.suc n) r) (x ∷ xs)           ≡⟨ refl ⟩
     eval (0ₕ ·X+ Constant n r) (x ∷ xs)             ≡⟨ refl ⟩
     eval 0ₕ (x ∷ xs) · x + eval (Constant n r) xs
    ≡⟨ cong (λ u → u · x + eval (Constant n r) xs) (eval0H (x ∷ xs)) ⟩
     0 · x + eval (Constant n r) xs
    ≡⟨ refl ⟩
     eval (Constant n r) xs
    ≡⟨ isEqualToNormalform (K r) xs ⟩
     r ∎

  isEqualToNormalform (∣ zero) (x ∷ xs) =
    eval (1ₕ ·X+ 0ₕ) (x ∷ xs)           ≡⟨ refl ⟩
    eval 1ₕ (x ∷ xs) · x + eval 0ₕ xs   ≡⟨ cong (λ u → u · x + eval 0ₕ xs)
                                               (eval1ₕ (x ∷ xs)) ⟩
    1 · x + eval 0ₕ xs                  ≡⟨ cong (λ u → 1 · x + u ) (eval0H xs) ⟩
    1 · x + 0                          ≡⟨ +-zero _ ⟩
    1 · x                               ≡⟨ ·-identityˡ _ ⟩
    x ∎
  isEqualToNormalform {n = ℕ.suc n} (∣ (suc k)) (x ∷ xs) =
      eval (0ₕ ·X+ Variable n k) (x ∷ xs)             ≡⟨ refl ⟩
      eval 0ₕ (x ∷ xs) · x + eval (Variable n k) xs
    ≡⟨ cong (λ u → u · x + eval (Variable n k) xs) (eval0H (x ∷ xs)) ⟩
      0 · x + eval (Variable n k) xs
    ≡⟨ refl ⟩
      eval (Variable n k) xs
    ≡⟨ isEqualToNormalform (∣ k) xs ⟩
      ⟦ ∣ (suc k) ⟧ (x ∷ xs) ∎

  isEqualToNormalform (e +' e₁) [] =
        eval (normalize e +ₕ normalize e₁) []
      ≡⟨ +Homeval (normalize e) _ [] ⟩
        eval (normalize e) []
        + eval (normalize e₁) []
      ≡⟨ cong (λ u → u + eval (normalize e₁) [])
              (isEqualToNormalform e []) ⟩
        ⟦ e ⟧ []
        + eval (normalize e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] + u) (isEqualToNormalform e₁ []) ⟩
        ⟦ e ⟧ [] + ⟦ e₁ ⟧ [] ∎
  isEqualToNormalform (e +' e₁) (x ∷ xs) =
        eval (normalize e
              +ₕ normalize e₁) (x ∷ xs)
      ≡⟨ +Homeval (normalize e) _ (x ∷ xs) ⟩
        eval (normalize e) (x ∷ xs)
        + eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u + eval (normalize e₁) (x ∷ xs))
              (isEqualToNormalform e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs)
        + eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) + u)
              (isEqualToNormalform e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) + ⟦ e₁ ⟧ (x ∷ xs) ∎

  isEqualToNormalform (e ·' e₁) [] =
        eval (normalize e ·ₕ normalize e₁) []
      ≡⟨ ·Homeval (normalize e) _ [] ⟩
        eval (normalize e) []
        · eval (normalize e₁) []
      ≡⟨ cong (λ u → u · eval (normalize e₁) [])
              (isEqualToNormalform e []) ⟩
        ⟦ e ⟧ []
        · eval (normalize e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] · u) (isEqualToNormalform e₁ []) ⟩
        ⟦ e ⟧ [] · ⟦ e₁ ⟧ [] ∎

  isEqualToNormalform (e ·' e₁) (x ∷ xs) =
        eval (normalize e ·ₕ normalize e₁) (x ∷ xs)
      ≡⟨ ·Homeval (normalize e) _ (x ∷ xs) ⟩
        eval (normalize e) (x ∷ xs)
        · eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u · eval (normalize e₁) (x ∷ xs))
              (isEqualToNormalform e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs)
        · eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) · u)
              (isEqualToNormalform e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) · ⟦ e₁ ⟧ (x ∷ xs) ∎

  solve :
    {n : ℕ} (e₁ e₂ : Expr n) (xs : Vec ℕ n)
    (p : eval (normalize e₁) xs ≡ eval (normalize e₂) xs)
    → ⟦ e₁ ⟧ xs ≡ ⟦ e₂ ⟧ xs
  solve e₁ e₂ xs p =
    ⟦ e₁ ⟧ xs                ≡⟨ sym (isEqualToNormalform e₁ xs) ⟩
    eval (normalize e₁) xs ≡⟨ p ⟩
    eval (normalize e₂) xs ≡⟨ isEqualToNormalform e₂ xs ⟩
    ⟦ e₂ ⟧ xs ∎

max_stars_repo_name: FernandoLarrain/cubical


text:
open import Nat
open import Prelude
open import Hazelnut-core

module Hazelnut-deterministic where
  -- theorem 2

  -- the same action applied to the same type makes the same resultant
  -- type.
  actdet1 : {t t' t'' : τ̂} {α : action} →
            (t + α +> t') →
            (t + α +> t'') →
            (t' == t'')
  actdet1 TMFirstChild TMFirstChild = refl
  actdet1 TMParent1 TMParent1 = refl
  actdet1 TMParent1 (TMZip1 ())
  actdet1 TMParent2 TMParent2 = refl
  actdet1 TMParent2 (TMZip2 ())
  actdet1 TMNextSib TMNextSib = refl
  actdet1 TMNextSib (TMZip1 ())
  actdet1 TMPrevSib TMPrevSib = refl
  actdet1 TMPrevSib (TMZip2 ())
  actdet1 TMDel TMDel = refl
  actdet1 TMConArrow TMConArrow = refl
  actdet1 TMConNum TMConNum = refl
  actdet1 (TMZip1 ()) TMParent1
  actdet1 (TMZip1 ()) TMNextSib
  actdet1 (TMZip1 p1) (TMZip1 p2) with actdet1 p1 p2
  ... | refl = refl
  actdet1 (TMZip2 ()) TMParent2
  actdet1 (TMZip2 ()) TMPrevSib
  actdet1 (TMZip2 p1) (TMZip2 p2) with actdet1 p1 p2
  ... | refl = refl

  -- all expressions only move to one other expression
  movedet : {e e' e'' : ê} {δ : direction} →
            (e + move δ +>e e') →
            (e + move δ +>e e'') →
            e' == e''
  movedet EMAscFirstChild EMAscFirstChild = refl
  movedet EMAscParent1 EMAscParent1 = refl
  movedet EMAscParent2 EMAscParent2 = refl
  movedet EMAscNextSib EMAscNextSib = refl
  movedet EMAscPrevSib EMAscPrevSib = refl
  movedet EMLamFirstChild EMLamFirstChild = refl
  movedet EMLamParent EMLamParent = refl
  movedet EMPlusFirstChild EMPlusFirstChild = refl
  movedet EMPlusParent1 EMPlusParent1 = refl
  movedet EMPlusParent2 EMPlusParent2 = refl
  movedet EMPlusNextSib EMPlusNextSib = refl
  movedet EMPlusPrevSib EMPlusPrevSib = refl
  movedet EMApFirstChild EMApFirstChild = refl
  movedet EMApParent1 EMApParent1 = refl
  movedet EMApParent2 EMApParent2 = refl
  movedet EMApNextSib EMApNextSib = refl
  movedet EMApPrevSib EMApPrevSib = refl
  movedet EMFHoleFirstChild EMFHoleFirstChild = refl
  movedet EMFHoleParent EMFHoleParent = refl

  -- if a move action on a synthetic action makes a new form, it's unique
  synthmovedet : {Γ : ·ctx} {e e' e'' : ê} {t' t'' : τ̇} {δ : direction} →
         (Γ ⊢ e => t' ~ move δ ~> e'' => t'') →
         (e + move δ +>e e') →
         e'' == e'
  synthmovedet (SAMove EMAscFirstChild) EMAscFirstChild = refl
  synthmovedet (SAMove EMAscParent1) EMAscParent1 = refl
  synthmovedet (SAMove EMAscParent2) EMAscParent2 = refl
  synthmovedet (SAMove EMAscNextSib) EMAscNextSib = refl
  synthmovedet (SAMove EMAscPrevSib) EMAscPrevSib = refl
  synthmovedet (SAMove EMLamFirstChild) EMLamFirstChild = refl
  synthmovedet (SAMove EMLamParent) EMLamParent = refl
  synthmovedet (SAMove EMPlusFirstChild) EMPlusFirstChild = refl
  synthmovedet (SAMove EMPlusParent1) EMPlusParent1 = refl
  synthmovedet (SAMove EMPlusParent2) EMPlusParent2 = refl
  synthmovedet (SAMove EMPlusNextSib) EMPlusNextSib = refl
  synthmovedet (SAMove EMPlusPrevSib) EMPlusPrevSib = refl
  synthmovedet (SAMove EMApFirstChild) EMApFirstChild = refl
  synthmovedet (SAMove EMApParent1) EMApParent1 = refl
  synthmovedet (SAMove EMApParent2) EMApParent2 = refl
  synthmovedet (SAMove EMApNextSib) EMApNextSib = refl
  synthmovedet (SAMove EMApPrevSib) EMApPrevSib = refl
  synthmovedet (SAMove EMFHoleFirstChild) EMFHoleFirstChild = refl
  synthmovedet (SAMove EMFHoleParent) EMFHoleParent = refl
  -- all these cases lead to absurdities after a few levels
  synthmovedet (SAZipAsc1 (AASubsume _ (SAMove ()) _)) EMAscParent1
  synthmovedet (SAZipAsc1 (AAMove ())) EMAscParent1
  synthmovedet (SAZipAsc1 (AASubsume _ (SAMove ()) _)) EMAscNextSib
  synthmovedet (SAZipAsc1 (AAMove ())) EMAscNextSib
  synthmovedet (SAZipAsc2 () _) EMAscParent2
  synthmovedet (SAZipAsc2 () _) EMAscPrevSib
  synthmovedet (SAZipAp1 _ (SAMove ()) (ASubsume _ _)) EMApParent1
  synthmovedet (SAZipAp1 _ (SAMove ()) (ALam _ _)) EMApParent1
  synthmovedet (SAZipAp1 _ (SAMove ()) _) EMApNextSib
  synthmovedet (SAZipAp2 _ (SAMove ()) _) EMApParent1
  synthmovedet (SAZipAp2 _ (SAMove ()) _) EMApNextSib
  synthmovedet (SAZipAp3 _ (AASubsume _ (SAMove ()) _)) EMApParent2
  synthmovedet (SAZipAp3 _ (AAMove ())) EMApParent2
  synthmovedet (SAZipAp3 _ (AASubsume _ (SAMove ()) _)) EMApPrevSib
  synthmovedet (SAZipAp3 _ (AAMove ())) EMApPrevSib
  synthmovedet (SAZipAp4 _ (AASubsume _ (SAMove ()) _)) EMApParent2
  synthmovedet (SAZipAp4 _ (AAMove ())) EMApParent2
  synthmovedet (SAZipAp4 _ (AASubsume _ (SAMove ()) _)) EMApPrevSib
  synthmovedet (SAZipAp4 _ (AAMove ())) EMApPrevSib
  synthmovedet (SAZipPlus1 (AASubsume _ (SAMove ()) _)) EMPlusParent1
  synthmovedet (SAZipPlus1 (AAMove ())) EMPlusParent1
  synthmovedet (SAZipPlus1 (AASubsume _ (SAMove ()) _)) EMPlusNextSib
  synthmovedet (SAZipPlus1 (AAMove ())) EMPlusNextSib
  synthmovedet (SAZipPlus2 (AASubsume _ (SAMove ()) _)) EMPlusParent2
  synthmovedet (SAZipPlus2 (AAMove ())) EMPlusParent2
  synthmovedet (SAZipPlus2 (AASubsume _ (SAMove ()) _)) EMPlusPrevSib
  synthmovedet (SAZipPlus2 (AAMove ())) EMPlusPrevSib
  synthmovedet (SAZipHole1 _ (SAMove ()) x) EMFHoleParent
  synthmovedet (SAZipHole2 _ (SAMove ())) EMFHoleParent

  -- these are all a bunch of small techincal lemmas for the cases below. i
  -- don't understand why some of them can't be inlined.
  lem1 : {Γ : ·ctx} {t1 t2 : τ̇} →
           Γ ⊢ <||> <= (t1 ==> t2) →
           (t1 ==> t2) ~ (<||> ==> <||>)
  lem1 (ASubsume SEHole TCHole1) = TCArr TCHole1 TCHole1

  lem3 : ∀{ Γ e t } → Γ ⊢ (e ·: t) <= t → Γ ⊢ e <= t
  lem3 (ASubsume (SAsc x) x₁) = x

  lem4 : ∀{ Γ e eh t t2 } →
         Γ ⊢ e ∘ (eh ◆e) => t →
         Γ ⊢ e => (t2 ==> t) →
         Γ ⊢ (eh ◆e) <= t2
  lem4 (SAp (SAsc x₁) x) (SAsc x₂) = x
  lem4 {Γ = G} (SAp (SVar x₁) x) (SVar x₂)
    with ctxunicity {Γ = G}  x₁ x₂
  ... | refl = x
  lem4 (SAp (SAp d1 x₁) x) (SAp d2 x₂)
    with synthunicity d1 d2
  ... | refl = x
  lem4 (SApHole () x) (SAsc x₁)
  lem4 {Γ = G} (SApHole (SVar x₁) x) (SVar x₂)
    with ctxunicity {Γ = G} x₁ x₂
  ... | ()
  lem4 (SApHole (SAp d1 x₁) x) (SAp d2 x₂)
    with synthunicity d1 d2
  ... | ()
  lem4 (SApHole (SApHole d1 x₁) x) (SAp d2 x₂)
    with synthunicity d1 d2
  ... | ()

  lem5 : ∀ {Γ e eh} →
        Γ ⊢ e => <||> →
        Γ ⊢ e ∘ (eh ◆e) => <||> →
        Γ ⊢ eh ◆e <= <||>
  lem5 d1 (SAp d2 x) with synthunicity d1 d2
  ... | ()
  lem5 d1 (SApHole d2 x) = x

  lem6 : ∀ {Γ e1 e2} →
         Γ ⊢ e1 ·+ e2 => num →
         Γ ⊢ e1 <= num × Γ ⊢ e2 <= num
  lem6 (SPlus x x₁) = x , x₁

  lem7 : ∀{Γ e t e' t'} →
         Γ ⊢ <| e |> => <||> →
         Γ ⊢ ▹ e ◃ => t ~ move parent ~> e' => t' →
         ⊥
  lem7 (SFHole _) (SAMove ())

  lem8a : ∀ {Γ e e' t} →
        Γ ⊢ ▹ e ◃ ~ move nextSib ~> e' ⇐ t → ⊥
  lem8a (AASubsume x (SAMove ()) x₂)
  lem8a (AAMove ())

  -- expressions in focus don't move to next sib
  lem8s : ∀ {Γ e e' t t'} →
        Γ ⊢ ▹ e ◃ => t ~ move nextSib ~> e' => t' → ⊥
  lem8s (SAMove ())

    -- expressions in focus don't move to prev sib
  lem9a : ∀ {Γ e e' t} →
        Γ ⊢ ▹ e ◃ ~ move prevSib ~> e' ⇐ t → ⊥
  lem9a (AASubsume x (SAMove ()) x₂)
  lem9a (AAMove ())

  -- expressions in focus don't move to prev sib
  lem9s : ∀ {Γ e e' t t'} →
        Γ ⊢ ▹ e ◃ => t ~ move prevSib ~> e' => t' → ⊥
  lem9s (SAMove ())

  lem10 : ∀{Γ x t1 t2 e} →
          Γ ⊢ ·λ x (e ◆e) <= (t1 ==> t2) →
          (Γ ,, (x , t1)) ⊢ e ◆e <= t2
  lem10 (ASubsume () x₂)
  lem10 (ALam x₁ d1) = d1

    -- expressions in focus don't move to parent
  lem11 : ∀ {Γ e e' t} →
        Γ ⊢ ▹ e ◃ ~ move parent ~> e' ⇐ t → ⊥
  lem11 (AASubsume x (SAMove ()) x₂)
  lem11 (AAMove ())

  -- if a type isn't compatible with hole to hole, it isn't compatible with
  -- any function type at all.
  lem12 : {t : τ̇} → (t ~̸ (<||> ==> <||>)) → ((t1 t2 : τ̇) → t ~̸ (t1 ==> t2))
  lem12 {num} p t1 t2 ()
  lem12 {<||>} p t1 t2 TCHole2 = p TCHole2
  lem12 {(t ==> t')} p t1 t2 x = p (TCArr TCHole1 TCHole1)

  mutual
    -- an action on an expression in a synthetic position produces one
    -- resultant expression and type.
    actdet2 : {Γ : ·ctx} {e e' e'' : ê} {t t' t'' : τ̇} {α : action} →
              (Γ ⊢ (e ◆e) => t) →
              (Γ ⊢ e => t ~ α ~> e'  => t') →
              (Γ ⊢ e => t ~ α ~> e'' => t'') →
              (e' == e'' × t' == t'')
    actdet2 wt (SAMove x) (SAMove x₁) = movedet x x₁ , refl
      -- every other case of move in the left is an absurdity after a
      -- couple of levels
    actdet2 wt (SAMove EMAscParent1) (SAZipAsc1 (AASubsume _ (SAMove ()) _))
    actdet2 wt (SAMove EMAscParent1) (SAZipAsc1 (AAMove ()))
    actdet2 wt (SAMove EMAscNextSib) (SAZipAsc1 (AASubsume _ (SAMove ()) _))
    actdet2 wt (SAMove EMAscNextSib) (SAZipAsc1 (AAMove ()))
    actdet2 wt (SAMove EMAscParent2) (SAZipAsc2 () x₂)
    actdet2 wt (SAMove EMAscPrevSib) (SAZipAsc2 () x₂)
    actdet2 wt (SAMove EMApParent1) (SAZipAp1 x₁ (SAMove ()) x₂)
    actdet2 wt (SAMove EMApNextSib) (SAZipAp1 x₁ (SAMove ()) x₂)
    actdet2 wt (SAMove EMApParent1) (SAZipAp2 x₁ (SAMove ()) x₂)
    actdet2 wt (SAMove EMApNextSib) (SAZipAp2 x₁ (SAMove ()) x₂)
    actdet2 wt (SAMove EMApParent2) (SAZipAp3 x₁ (AASubsume x (SAMove ()) x₃))
    actdet2 wt (SAMove EMApParent2) (SAZipAp3 x₁ (AAMove ()))
    actdet2 wt (SAMove EMApPrevSib) (SAZipAp3 x₁ (AASubsume x (SAMove ()) x₃))
    actdet2 wt (SAMove EMApPrevSib) (SAZipAp3 x₁ (AAMove ()))
    actdet2 wt (SAMove EMApParent2) (SAZipAp4 x₁ (AASubsume x (SAMove ()) x₃))
    actdet2 wt (SAMove EMApParent2) (SAZipAp4 x₁ (AAMove ()))
    actdet2 wt (SAMove EMApPrevSib) (SAZipAp4 x₁ (AASubsume x (SAMove ()) x₃))
    actdet2 wt (SAMove EMApPrevSib) (SAZipAp4 x₁ (AAMove ()))
    actdet2 wt (SAMove EMPlusParent1) (SAZipPlus1 (AASubsume x (SAMove ()) x₂))
    actdet2 wt (SAMove EMPlusParent1) (SAZipPlus1 (AAMove ()))
    actdet2 wt (SAMove EMPlusNextSib) (SAZipPlus1 (AASubsume x (SAMove ()) x₂))
    actdet2 wt (SAMove EMPlusNextSib) (SAZipPlus1 (AAMove ()))
    actdet2 wt (SAMove EMPlusParent2) (SAZipPlus2 (AASubsume x (SAMove ()) x₂))
    actdet2 wt (SAMove EMPlusParent2) (SAZipPlus2 (AAMove ()))
    actdet2 wt (SAMove EMPlusPrevSib) (SAZipPlus2 (AASubsume x (SAMove ()) x₂))
    actdet2 wt (SAMove EMPlusPrevSib) (SAZipPlus2 (AAMove ()))
    actdet2 wt (SAMove EMFHoleParent) (SAZipHole1 x₁ (SAMove ()) x₂)
    actdet2 wt (SAMove EMFHoleParent) (SAZipHole2 x₁ (SAMove ()))

    actdet2 wt SADel SADel = refl , refl

    actdet2 wt SAConAsc SAConAsc = refl , refl

    actdet2 {Γ = G} wt (SAConVar p) (SAConVar p₁)
      with ctxunicity {Γ = G} p p₁
    ... | refl = refl , refl

    actdet2 wt (SAConLam x₁) (SAConLam x₂) = refl , refl

    actdet2 wt SAConAp1 SAConAp1 = refl , refl
    actdet2 wt SAConAp1 (SAConAp3 x) = abort (lem12 x _ _ TCRefl)

    actdet2 wt SAConAp2 SAConAp2 = refl , refl
    actdet2 wt SAConAp2 (SAConAp3 x) = abort (x TCHole2)

    actdet2 wt (SAConAp3 x) SAConAp1 = abort (lem12 x _ _ TCRefl)
    actdet2 wt (SAConAp3 x) SAConAp2 = abort (x TCHole2)
    actdet2 wt (SAConAp3 x) (SAConAp3 x₁) = refl , refl

    actdet2 wt SAConArg SAConArg = refl , refl

    actdet2 wt SAConNumlit SAConNumlit = refl , refl

    actdet2 wt (SAConPlus1 x) (SAConPlus1 x₁) = refl , refl
    actdet2 wt (SAConPlus1 x) (SAConPlus2 x₁) = abort (x₁ x)

    actdet2 wt (SAConPlus2 x) (SAConPlus1 x₁) = abort (x x₁)
    actdet2 wt (SAConPlus2 x) (SAConPlus2 x₁) = refl , refl

    actdet2 wt (SAFinish x) (SAFinish x₁)
      with synthunicity x x₁
    ... | refl = refl , refl

    actdet2 wt (SAZipAsc1 (AASubsume _ (SAMove ()) _)) (SAMove EMAscParent1)
    actdet2 wt (SAZipAsc1 (AAMove ())) (SAMove EMAscParent1)
    actdet2 wt (SAZipAsc1 x) (SAMove EMAscNextSib) = abort (lem8a x)
    actdet2 {t = t} wt (SAZipAsc1 x) (SAZipAsc1 x₁) =
         ap1 (λ q → q ·:₁ t) (actdet3 (lem3 (ASubsume wt TCRefl)) x x₁) , refl

    actdet2 wt (SAZipAsc2 () x₁) (SAMove EMAscParent2)
    actdet2 wt (SAZipAsc2 () x₁) (SAMove EMAscPrevSib)
    actdet2 wt (SAZipAsc2 x x₁) (SAZipAsc2 x₂ x₃) with actdet1 x x₂
    ... | refl = refl , refl

    actdet2 wt (SAZipAp1 x (SAMove ()) x₁) (SAMove EMApParent1)
    actdet2 wt (SAZipAp1 x (SAMove ()) x₁) (SAMove EMApNextSib)
    actdet2 wt (SAZipAp1 x d1 x₁) (SAZipAp1 x₂ d2 x₃)
      with synthunicity x₂ x
    ... | refl with actdet2 x d1 d2 -- todo: double-barrelded with here ..
    ... | p1 , refl = (ap1 (λ q → q ∘₁ _) p1) , refl
    actdet2 wt (SAZipAp1 x d1 x₁) (SAZipAp2 x₂ d2 x₃)
      with synthunicity x x₂
    ... | refl with actdet2 x d1 d2 -- todo: .. and here
    actdet2 wt (SAZipAp1 _ _ _ ) (SAZipAp2 _ _ _) | refl | _ , ()

    actdet2 wt (SAZipAp2 x (SAMove ()) x₁) (SAMove EMApParent1)
    actdet2 wt (SAZipAp2 x (SAMove ()) x₁) (SAMove EMApNextSib)
    actdet2 wt (SAZipAp2 x d1 x₁) (SAZipAp1 x₂ d2 x₃)
      with synthunicity x x₂
    ... | refl with actdet2 x d1 d2
    actdet2 wt (SAZipAp2 x d1 x₁) (SAZipAp1 x₂ d2 x₃) | refl | p1 , ()
    actdet2 wt (SAZipAp2 x d1 _) (SAZipAp2 x₂ d2 _)
      with synthunicity x x₂
    ... | refl = (ap1 (λ q → q ∘₁ _) (π1 (actdet2 x₂ d1 d2))) , refl

    actdet2 wt (SAZipAp3 x (AASubsume x₁ (SAMove ()) x₃)) (SAMove EMApParent2)
    actdet2 wt (SAZipAp3 x (AAMove ())) (SAMove EMApParent2)
    actdet2 wt (SAZipAp3 x x₁) (SAMove EMApPrevSib) = abort (lem9a x₁)
    actdet2 wt (SAZipAp3 {eh = eh} x x₁) (SAZipAp3 x₂ x₃)
      with synthunicity x x₂
    ... | refl = ap1 (_∘₂_ _) (actdet3 (lem4 {eh = eh} wt x) x₁ x₃) , refl
    actdet2 wt (SAZipAp3 x x₁) (SAZipAp4 x₂ x₃)
      with synthunicity x x₂
    ... | ()

    actdet2 wt (SAZipAp4 x (AASubsume x₁ (SAMove ()) x₃)) (SAMove EMApParent2)
    actdet2 wt (SAZipAp4 x (AAMove ())) (SAMove EMApParent2)
    actdet2 wt (SAZipAp4 x (AASubsume x₁ x₂ x₃)) (SAMove EMApPrevSib) = abort (lem9s x₂)
    actdet2 wt (SAZipAp4 x (AAMove ())) (SAMove EMApPrevSib)
    actdet2 wt (SAZipAp4 x x₁) (SAZipAp3 x₂ x₃)
      with synthunicity x x₂
    ... | ()
    actdet2 wt (SAZipAp4 {eh = eh} x x₁ ) (SAZipAp4 x₂ x₃)
      with actdet3 (lem5 {eh = eh} x₂ wt) x₁ x₃
    ... | refl = refl , refl

    actdet2 wt (SAZipPlus1 (AASubsume x (SAMove ()) x₂)) (SAMove EMPlusParent1)
    actdet2 wt (SAZipPlus1 (AAMove ())) (SAMove EMPlusParent1)
    actdet2 wt (SAZipPlus1 (AASubsume x x₁ x₂)) (SAMove EMPlusNextSib) = abort (lem8s x₁)
    actdet2 wt (SAZipPlus1 (AAMove ())) (SAMove EMPlusNextSib)
    actdet2 wt (SAZipPlus1 x) (SAZipPlus1 x₁)
      with actdet3 (π1 (lem6 wt)) x x₁ -- todo: not sure why this needs to be a lemma
    ... | refl = refl , refl

    actdet2 wt (SAZipPlus2 (AASubsume x (SAMove ()) x₂)) (SAMove EMPlusParent2)
    actdet2 wt (SAZipPlus2 (AASubsume x x₁ x₂)) (SAMove EMPlusPrevSib) = abort (lem9s x₁)
    actdet2 wt (SAZipPlus2 (AAMove ())) (SAMove EMPlusParent2)
    actdet2 wt (SAZipPlus2 (AAMove ())) (SAMove EMPlusPrevSib)
    actdet2 wt (SAZipPlus2 x) (SAZipPlus2 x₁)
      with actdet3 (π2 (lem6 wt)) x x₁ -- .. or this one
    ... | refl = refl , refl

    actdet2 wt (SAZipHole1 x d1 x₁) (SAMove EMFHoleParent) = abort (lem7 wt d1)
    actdet2 wt (SAZipHole1 x d1 x₁) (SAZipHole1 x₂ d2 x₃)
      with synthunicity x x₂
    ... | refl with actdet2 x d1 d2
    ... | refl , refl = refl , refl
    actdet2 wt (SAZipHole1 x d1 x₁) (SAZipHole2 x₂ d2)
      with synthunicity x x₂
    ... | refl with actdet2 x d1 d2
    ... | p , _ = abort (x₁ p)

    actdet2 wt (SAZipHole2 x d1) (SAMove EMFHoleParent) = abort (lem7 wt d1)
    actdet2 wt (SAZipHole2 x d1) (SAZipHole1 x₁ d2 x₂)
      with synthunicity x x₁
    ... | refl with actdet2 x d1 d2
    ... | p , q  = abort (x₂ (! p))
    actdet2 wt (SAZipHole2 x d1) (SAZipHole2 x₁ d2)
      with synthunicity x x₁
    ... | refl with actdet2 x d1 d2
    ... | refl , refl = refl , refl

    -- an action on an expression in an analytic position produces one
    -- resultant expression and type.
    actdet3 : {Γ : ·ctx} {e e' e'' : ê} {t : τ̇} {α : action} →
              (Γ ⊢ (e ◆e) <= t) →
              (Γ ⊢ e ~ α ~> e' ⇐ t) →
              (Γ ⊢ e ~ α ~> e'' ⇐ t) →
              (e' == e'')
    actdet3 D1 (AASubsume x x₁ x₂) (AASubsume x₃ x₄ x₅)
     with synthunicity x x₃
    ... | refl = π1 (actdet2 x x₁ x₄)

    actdet3 D1 (AASubsume _ y _) (AAMove w) = synthmovedet y w
    actdet3 D1 (AASubsume _ SADel _) AADel = refl
    actdet3 D1 (AASubsume {p = p} x SAConAsc x₂) AAConAsc = abort (π1 p refl)
    actdet3 {Γ = G} (ASubsume x x₁) (AASubsume x₂ (SAConVar p) x₄) (AAConVar x₅ p₁)
     with ctxunicity {Γ = G} p p₁
    ... | refl = abort (x₅ x₄)
    actdet3 D1 (AASubsume {p = p} x₁ (SAConLam x₂) x₃) (AAConLam1 x₄) = abort (π2 p _ refl)
    actdet3 D1 (AASubsume x₁ (SAConLam x₃) x₂) (AAConLam2 x₄ x₅) = abort (x₅ x₂)
    actdet3 D1 (AASubsume x SAConNumlit x₂) (AAConNumlit x₃) = abort (x₃ x₂)
    actdet3 D1 (AASubsume x (SAFinish x₁) x₂) (AAFinish x₃) = refl
    actdet3 D1 (AASubsume x₁ (SAMove EMLamParent) x₂) (AAZipLam x₄ (AASubsume x₃ (SAMove ()) x₆))
    actdet3 D1 (AASubsume x₁ (SAMove EMLamParent) x₂) (AAZipLam x₄ (AAMove ()))

    actdet3 D1 (AAMove x) (AASubsume x₁ x₂ x₃) =  ! (synthmovedet x₂ x)
    actdet3 D1 (AAMove x) (AAMove x₁) = movedet x x₁
    actdet3 D1 (AAMove EMLamParent) (AAZipLam x₃ (AASubsume x₁ (SAMove ()) x₄))
    actdet3 D1 (AAMove EMLamParent) (AAZipLam x₃ (AAMove ()))

    actdet3 D1 AADel (AASubsume _ SADel _) = refl
    actdet3 D1 AADel AADel = refl

    actdet3 D1 AAConAsc (AASubsume {p = p} x SAConAsc x₂) = abort (π1 p refl)
    actdet3 D1 AAConAsc AAConAsc = refl

    actdet3 {Γ = G} D1 (AAConVar x₁ p) (AASubsume x₂ (SAConVar p₁) x₄)
     with ctxunicity {Γ = G} p p₁
    ... | refl = abort (x₁ x₄)
    actdet3 D1 (AAConVar x₁ p) (AAConVar x₂ p₁) = refl

    actdet3 D1 (AAConLam1 x₃) (AASubsume {p = p} SEHole (SAConLam x₅) x₆) = abort (π2 p _ refl)
    actdet3 D1 (AAConLam1 x₁) (AAConLam1 x₂) = refl
    actdet3 D1 (AAConLam1 x₃) (AAConLam2 x₄ x₅) = abort (x₅ (lem1 D1))

    actdet3 D1 (AAConLam2 x₁ x₂) (AASubsume x₃ (SAConLam x₄) x₅) = abort (x₂ x₅)
    actdet3 D1 (AAConLam2 x₁ x₂) (AAConLam1 x₃) = abort (x₂ (lem1 D1))
    actdet3 D1 (AAConLam2 x₁ x₂) (AAConLam2 x₃ x₄) = refl

    actdet3 D1 (AAConNumlit x) (AASubsume x₁ SAConNumlit x₃) = abort (x x₃)
    actdet3 D1 (AAConNumlit x) (AAConNumlit x₁) = refl

    actdet3 D1 (AAFinish x) (AASubsume x₁ (SAFinish x₂) x₃) = refl
    actdet3 D1 (AAFinish x) (AAFinish x₁) = refl

    actdet3 D1 (AAZipLam x₃ D2) (AASubsume x₁ (SAMove EMLamParent) x₄) = abort (lem11 D2)
    actdet3 D1 (AAZipLam x₃ (AASubsume x₁ (SAMove ()) x₄)) (AAMove EMLamParent)
    actdet3 D1 (AAZipLam x₃ (AAMove ())) (AAMove EMLamParent)
    actdet3 D1 (AAZipLam {e = e} x₃ D2) (AAZipLam x₁ D3)
      with actdet3 (lem10 {e = e} D1) D2 D3
    ... | refl = refl


text:
module Text.Greek.SBLGNT-Query where

open import Data.Bool
open import Data.Nat hiding (_≟_)
open import Data.List
open import Data.Maybe
open import Data.Product hiding (map)
open import Function
open import Relation.Binary.PropositionalEquality
open import Text.Greek.Bible
open import Text.Greek.Script
open import Text.Greek.SBLGNT.1John

texts = ΙΩΑΝΝΟΥ-Α ∷ []

wordCount = length ΙΩΑΝΝΟΥ-Α
--tokenCount = length (concat ΙΩΑΝΝΟΥ-Α)

getLetters : Word → List Token
getLetters (word x _) = x

tokens = concatMap getLetters ΙΩΑΝΝΟΥ-Α

adjacent-accent : (Token → Maybe Accent) → List Token → List (Σ Token (const Token))
adjacent-accent f [] = []
adjacent-accent f (_ ∷ []) = []
adjacent-accent f (t₁ ∷ t₂ ∷ ts) with (f t₁) , (f t₂) , adjacent-accent f (t₂ ∷ ts)
… | (just circumflex-mark , just circumflex-mark , ts′)  = (t₁ , t₂) ∷ ts′
… | (_ , _ , ts′) = ts′

adj = adjacent-accent get-accent tokens

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
{-# OPTIONS --without-K #-}
open import Type using (Type₀; Type_)
open import Type.Identities
open import Function.NP using (Π; _∘_; const)
open import Function.Extensionality using (FunExt)
open import Data.One using (0₁)
open import Data.Two.Base using (0₂; 1₂)
open import Data.Product.NP using (_,_; fst)
open import Data.Sum.NP using (inl; inr)
open import Relation.Binary.PropositionalEquality.NP using (_≡_; idp; ap; !_; _∙_; tr)
open import HoTT using (ua; UA; module Equivalences)
open        Equivalences using (_≃_)

open import Explore.Core
open import Explore.Zero
open import Explore.One
open import Explore.Two
open import Explore.Product
open        Explore.Product.Operators
open import Explore.Sum
open import Explore.Properties
open import Explore.Explorable
open import Explore.Isomorphism
import      Explore.Universe.Type

module Explore.Universe.FromE
  (X : Type₀) (Xᵉ : ∀ {ℓ} → Explore ℓ X) where

open Explore.Universe.Type {X}

explore : ∀ {ℓ} u → Explore ℓ (El u)
explore 𝟘ᵁ = 𝟘ᵉ
explore 𝟙ᵁ = 𝟙ᵉ
explore 𝟚ᵁ = 𝟚ᵉ
explore (u₀ ×ᵁ u₁) = explore u₀ ×ᵉ explore u₁
explore (u₀ ⊎ᵁ u₁) = explore u₀ ⊎ᵉ explore u₁
explore (Σᵁ u f) = exploreΣ (explore u) λ {x} → explore (f x)
explore Xᵁ = Xᵉ
explore (≃ᵁ u A e) = explore-iso e (explore u)

module FromXⁱ (Xⁱ : ∀ {ℓ p} → ExploreInd p (Xᵉ {ℓ})) where
  explore-ind : ∀ {ℓ p} u → ExploreInd {ℓ} p (explore u)
  explore-ind 𝟘ᵁ = 𝟘ⁱ
  explore-ind 𝟙ᵁ = 𝟙ⁱ
  explore-ind 𝟚ᵁ = 𝟚ⁱ
  explore-ind (u₀ ×ᵁ u₁) = explore-ind u₀ ×ⁱ explore-ind u₁
  explore-ind (u₀ ⊎ᵁ u₁) = explore-ind u₀ ⊎ⁱ explore-ind u₁
  explore-ind (Σᵁ u f) = exploreΣ-ind (explore-ind u) λ {x} → explore-ind (f x)
  explore-ind Xᵁ = Xⁱ
  explore-ind (≃ᵁ u A e) = explore-iso-ind e (explore-ind u)

  module _ (u : U) where
    private
      uᵉ : ∀ {ℓ} → Explore ℓ (El u)
      uᵉ = explore u
      uⁱ : ∀ {ℓ p} → ExploreInd {ℓ} p uᵉ
      uⁱ = explore-ind u

    open FromExploreInd uⁱ public hiding (⟦explore⟧)

    ΣᵉU : ∀ {ℓ} → (El u → Type ℓ) → Type ℓ
    ΣᵉU = Σᵉ uᵉ
    ΠᵉU : ∀ {ℓ} → (El u → Type ℓ) → Type ℓ
    ΠᵉU = Πᵉ uᵉ

  module Xᴱ = FromExploreInd Xⁱ
  ΣᵉX : ∀ {ℓ} → (X → Type ℓ) → Type ℓ
  ΣᵉX = Σᵉ Xᵉ
  ΠᵉX : ∀ {ℓ} → (X → Type ℓ) → Type ℓ
  ΠᵉX = Πᵉ Xᵉ

  open Adequacy _≡_
  module FromXˢ-ok (Xˢ-ok : Adequate-sum Xᴱ.sum){{_ : UA}}{{_ : FunExt}} where
    adequate-sum : ∀ u → Adequate-sum (sum u)
    adequate-sum 𝟘ᵁ       = 𝟘ˢ-ok
    adequate-sum 𝟙ᵁ       = 𝟙ˢ-ok
    adequate-sum 𝟚ᵁ       = 𝟚ˢ-ok
    adequate-sum (u₀ ×ᵁ u₁) = adequate-sumΣ (adequate-sum u₀) (adequate-sum u₁)
    adequate-sum (u₀ ⊎ᵁ u₁) = adequate-sum⊎ (adequate-sum u₀) (adequate-sum u₁)
    adequate-sum (Σᵁ u f) = adequate-sumΣ (adequate-sum u) (λ {x} → adequate-sum (f x))
    adequate-sum Xᵁ = Xˢ-ok
    adequate-sum (≃ᵁ u A e) = sum-iso-ok e (adequate-sum u)

  module FromXˡ (Xˡ : ∀ {ℓ} → Lookup {ℓ} Xᵉ) where
    lookup : ∀ {ℓ} u → Lookup {ℓ} (explore u)
    lookup 𝟘ᵁ = 𝟘ˡ
    lookup 𝟙ᵁ = 𝟙ˡ
    lookup 𝟚ᵁ = 𝟚ˡ
    lookup (u₀ ×ᵁ u₁) = lookup× {eᴬ = explore u₀} {eᴮ = explore u₁} (lookup u₀) (lookup u₁)
    lookup (u₀ ⊎ᵁ u₁) = lookup⊎ {eᴬ = explore u₀} {eᴮ = explore u₁} (lookup u₀) (lookup u₁)
    lookup (Σᵁ u f) = lookupΣ {eᴬ = explore u} {eᴮ = λ {x} → explore (f x)} (lookup u) (λ {x} → lookup (f x))
    lookup Xᵁ = Xˡ
    lookup (≃ᵁ u A e) = lookup-iso e {Aᵉ = explore u} (lookup u)

  module FromXᶠ (Xᶠ : ∀ {ℓ} → Focus {ℓ} Xᵉ) where
    focus : ∀ {ℓ} u → Focus {ℓ} (explore u)
    focus 𝟘ᵁ = 𝟘ᶠ
    focus 𝟙ᵁ = 𝟙ᶠ
    focus 𝟚ᵁ = 𝟚ᶠ
    focus (u₀ ×ᵁ u₁) = focus× {eᴬ = explore u₀} {eᴮ = explore u₁} (focus u₀) (focus u₁)
    focus (u₀ ⊎ᵁ u₁) = focus⊎ {eᴬ = explore u₀} {eᴮ = explore u₁} (focus u₀) (focus u₁)
    focus (Σᵁ u f) = focusΣ {eᴬ = explore u} {eᴮ = λ {x} → explore (f x)} (focus u) (λ {x} → focus (f x))
    focus Xᵁ = Xᶠ
    focus (≃ᵁ u A e) = focus-iso e {Aᵉ = explore u} (focus u)

  module FromΣᵉX-ok (ΣᵉX-ok : ∀ {ℓ} → Adequate-Σ {ℓ} ΣᵉX){{_ : UA}}{{_ : FunExt}} where
    Σᵉ-ok : ∀ {ℓ} u → Adequate-Σ {ℓ} (ΣᵉU u)
    Σᵉ-ok 𝟘ᵁ       = Σᵉ𝟘-ok
    Σᵉ-ok 𝟙ᵁ       = Σᵉ𝟙-ok
    Σᵉ-ok 𝟚ᵁ       = Σᵉ𝟚-ok
    Σᵉ-ok (u₀ ×ᵁ u) = Σᵉ×-ok {eᴬ = explore u₀} {eᴮ = explore u} (Σᵉ-ok u₀) (Σᵉ-ok u)
    Σᵉ-ok (u₀ ⊎ᵁ u) = Σᵉ⊎-ok {eᴬ = explore u₀} {eᴮ = explore u} (Σᵉ-ok u₀) (Σᵉ-ok u)
    Σᵉ-ok (Σᵁ u f) = ΣᵉΣ-ok {eᴬ = explore u} {eᴮ = λ {x} → explore (f x)} (Σᵉ-ok u) (λ {x} → Σᵉ-ok (f x))
    Σᵉ-ok Xᵁ = ΣᵉX-ok
    Σᵉ-ok (≃ᵁ u A e) = Σ-iso-ok e {Aᵉ = explore u} (Σᵉ-ok u)

  module FromΠᵉX-ok (ΠᵉX-ok : ∀ {ℓ} → Adequate-Π {ℓ} ΠᵉX){{_ : UA}}{{_ : FunExt}} where
    Πᵉ-ok : ∀ {ℓ} u → Adequate-Π {ℓ} (ΠᵉU u)
    Πᵉ-ok 𝟘ᵁ       = Πᵉ𝟘-ok
    Πᵉ-ok 𝟙ᵁ       = Πᵉ𝟙-ok
    Πᵉ-ok 𝟚ᵁ       = Πᵉ𝟚-ok
    Πᵉ-ok (u₀ ×ᵁ u) = Πᵉ×-ok {eᴬ = explore u₀} {eᴮ = explore u} (Πᵉ-ok u₀) (Πᵉ-ok u)
    Πᵉ-ok (u₀ ⊎ᵁ u) = Πᵉ⊎-ok {eᴬ = explore u₀} {eᴮ = explore u} (Πᵉ-ok u₀) (Πᵉ-ok u)
    Πᵉ-ok (Σᵁ u f) = ΠᵉΣ-ok {eᴬ = explore u} {eᴮ = λ {x} → explore (f x)} (Πᵉ-ok u) (λ {x} → Πᵉ-ok (f x))
    Πᵉ-ok Xᵁ = ΠᵉX-ok
    Πᵉ-ok (≃ᵁ u A e) = Π-iso-ok e {Aᵉ = explore u} (Πᵉ-ok u)

module From⟦Xᵉ⟧≡ (⟦Xᵉ⟧≡ : ∀ {ℓ₀ ℓ₁} ℓᵣ → ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ _≡_ Xᵉ Xᵉ) {ℓ₀ ℓ₁} ℓᵣ where
  ⟦explore⟧≡ : ∀ u → ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ _≡_ (explore u) (explore u)
  ⟦explore⟧≡ 𝟘ᵁ        = ⟦𝟘ᵉ⟧ {ℓᵣ = ℓᵣ}
  ⟦explore⟧≡ 𝟙ᵁ        = ⟦𝟙ᵉ⟧ {ℓᵣ = ℓᵣ} {_≡_} {idp}
  ⟦explore⟧≡ 𝟚ᵁ        = ⟦𝟚ᵉ⟧ {ℓᵣ = ℓᵣ} {_≡_} {idp} {idp}
  ⟦explore⟧≡ (u₀ ×ᵁ u₁) = ⟦explore×⟧≡ {ℓᵣ = ℓᵣ} (⟦explore⟧≡ u₀) (⟦explore⟧≡ u₁)
  ⟦explore⟧≡ (u₀ ⊎ᵁ u₁) = ⟦explore⊎⟧≡ {ℓᵣ = ℓᵣ} (⟦explore⟧≡ u₀) (⟦explore⟧≡ u₁)
  ⟦explore⟧≡ (Σᵁ u F)  = ⟦exploreΣ⟧≡ {ℓᵣ = ℓᵣ} (⟦explore⟧≡ u) (λ x → ⟦explore⟧≡ (F x))
  ⟦explore⟧≡ Xᵁ        = ⟦Xᵉ⟧≡ ℓᵣ
  ⟦explore⟧≡ (≃ᵁ u A e) = ⟦explore-iso⟧ e {ℓᵣ = ℓᵣ} (ap (fst e)) (⟦explore⟧≡ u)

module FromΠX (ΠX : (X → U) → U) where
  Πᵁ : (u : U) (v : El u → U) → U
  Πᵁ 𝟘ᵁ        v = 𝟙ᵁ
  Πᵁ 𝟙ᵁ        v = v _
  Πᵁ 𝟚ᵁ        v = v 0₂ ×ᵁ v 1₂
  Πᵁ (u ×ᵁ u₁) v = Πᵁ u λ x → Πᵁ u₁ λ y → v (x , y)
  Πᵁ (u ⊎ᵁ u₁) v = (Πᵁ u (v ∘ inl)) ×ᵁ (Πᵁ u₁ (v ∘ inr))
  Πᵁ (Σᵁ u f)  v = Πᵁ u λ x → Πᵁ (f x) (v ∘ _,_ x)
  Πᵁ Xᵁ        v = ΠX v
  Πᵁ (≃ᵁ u A e)v = Πᵁ u (v ∘ fst e)

  _→ᵁ_ : (u : U) (v : U) → U
  u →ᵁ v = Πᵁ u (const v)

  module FromΠX≃ (ΠX≃ : ∀ v → El (ΠX v) ≃ Π X (El ∘ v)) where
    private
      module ΠX≃ {v} = Equivalences.Equiv (ΠX≃ v)

    module _ {{_ : FunExt}}{{_ : UA}} where
      Πᵁ-Π : ∀ u v → El (Πᵁ u v) ≡ Π (El u) (El ∘ v)
      Πᵁ-Π 𝟘ᵁ        v = ! Π𝟘-uniq₀ _
      Πᵁ-Π 𝟙ᵁ        v = ! Π𝟙-uniq _
      Πᵁ-Π 𝟚ᵁ        v = ! Π𝟚-×
      Πᵁ-Π (u ×ᵁ u₁) v = Πᵁ-Π u (λ x → Πᵁ u₁ (v ∘ _,_ x)) ∙ Π=′ _ (λ _ → Πᵁ-Π u₁ _) ∙ ! ΠΣ-curry
      Πᵁ-Π (u ⊎ᵁ u₁) v = ×= (Πᵁ-Π u (v ∘ inl)) (Πᵁ-Π u₁ (v ∘ inr)) ∙ ! dist-×-Π
      Πᵁ-Π (Σᵁ u f)  v = Πᵁ-Π u (λ x → Πᵁ (f _) (v ∘ _,_ x)) ∙ Π=′ _ (λ _ → Πᵁ-Π (f _) _) ∙ ! ΠΣ-curry
      Πᵁ-Π Xᵁ        v = ua (ΠX≃ v)
      Πᵁ-Π (≃ᵁ u A e)v = Πᵁ-Π u (v ∘ fst e) ∙ Π≃ e λ _ → idp

      →ᵁ-→ : ∀ u v → El (u →ᵁ v) ≡ (El u → El v)
      →ᵁ-→ u v = Πᵁ-Π u (const v)

    Πᵁ→Π : ∀ u v → El (Πᵁ u v) → Π (El u) (El ∘ v)
    Πᵁ→Π 𝟘ᵁ v x₂ ()
    Πᵁ→Π 𝟙ᵁ v x₂ x₃ = x₂
    Πᵁ→Π 𝟚ᵁ v (x , y) 0₂ = x
    Πᵁ→Π 𝟚ᵁ v (x , y) 1₂ = y
    Πᵁ→Π (u ×ᵁ u₁) v x (z , t) = Πᵁ→Π u₁ (v ∘ _,_ z) (Πᵁ→Π u (λ x → Πᵁ u₁ (v ∘ _,_ x)) x z) t
    Πᵁ→Π (u ⊎ᵁ _) v (x , _) (inl y) = Πᵁ→Π u (v ∘ inl) x y
    Πᵁ→Π (_ ⊎ᵁ u) v (_ , x) (inr y) = Πᵁ→Π u (v ∘ inr) x y
    Πᵁ→Π (Σᵁ u f) v x       (y , z) = Πᵁ→Π (f _) (v ∘ _,_ y) (Πᵁ→Π u (λ x → Πᵁ (f _) (v ∘ _,_ x)) x y) z
    Πᵁ→Π Xᵁ v = ΠX≃.·→
    Πᵁ→Π (≃ᵁ u A e) v f x = tr (El ∘ v) (·←-inv-r x) (Πᵁ→Π u (v ∘ ·→) f (·← x))
      where open Equivalences.Equiv e

    Π→Πᵁ : ∀ u v → Π (El u) (El ∘ v) → El (Πᵁ u v)
    Π→Πᵁ 𝟘ᵁ v f = 0₁
    Π→Πᵁ 𝟙ᵁ v f = f 0₁
    Π→Πᵁ 𝟚ᵁ v f = f 0₂ , f 1₂
    Π→Πᵁ (u ×ᵁ u₁) v f = Π→Πᵁ u (λ x → Πᵁ u₁ (v ∘ _,_ x))
                           (λ x → Π→Πᵁ u₁ (v ∘ _,_ x) (f ∘ _,_ x))
    Π→Πᵁ (u ⊎ᵁ u₁) v f = Π→Πᵁ u (v ∘ inl) (f ∘ inl) ,
                           Π→Πᵁ u₁ (v ∘ inr) (f ∘ inr)
    Π→Πᵁ (Σᵁ u F) v f = Π→Πᵁ u (λ x → Πᵁ (F x) (v ∘ _,_ x))
                          (λ x → Π→Πᵁ (F x) (v ∘ _,_ x) (f ∘ _,_ x))
    Π→Πᵁ Xᵁ v = ΠX≃.·←
    Π→Πᵁ (≃ᵁ u A e) v f = Π→Πᵁ u (v ∘ ·→) (f ∘ ·→)
      where open Equivalences.Equiv e

    →ᵁ→→ : ∀ u v → El (u →ᵁ v) → (El u → El v)
    →ᵁ→→ u v = Πᵁ→Π u (const v)

    →→→ᵁ : ∀ u v → (El u → El v) → El (u →ᵁ v)
    →→→ᵁ u v = Π→Πᵁ u (const v)

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import FRP.JS.Bool using ( Bool ; true ; false ; not ; _∨_ )
open import FRP.JS.True using ( True )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )
open import FRP.JS.Primitive using ( ℤ ; String )

module FRP.JS.Float where

infixr 4 _≤_ _<_ _≟_ _≠_
infixl 6 _+_ _-_
infixl 7 _*_ _/_ _/?_

open import FRP.JS.Primitive public using ( ℝ )

primitive
  primFloatPlus      : ℝ -> ℝ -> ℝ
  primFloatMinus     : ℝ -> ℝ -> ℝ
  primFloatTimes     : ℝ -> ℝ -> ℝ
  primFloatDiv       : ℝ -> ℝ -> ℝ
  primFloatLess      : ℝ -> ℝ -> Bool
  primFloor          : ℝ -> ℤ
  primCeiling        : ℝ -> ℤ
  primExp            : ℝ -> ℝ
  primLog            : ℝ -> ℝ
  primSin            : ℝ -> ℝ
  primShowFloat      : ℝ -> String
  primShowInteger    : ℤ → String
  primIntegerToFloat : ℤ → ℝ

_+_   = primFloatPlus
_-_   = primFloatMinus
_*_   = primFloatTimes
_<_   = primFloatLess
⌊_⌋   = primFloor
⌈_⌉   = primCeiling
exp   = primExp
log   = primLog
sin   = primSin

{-# COMPILED_JS _+_   function(x) { return function(y) { return x + y; }; } #-}
{-# COMPILED_JS _-_   function(x) { return function(y) { return x - y; }; } #-}
{-# COMPILED_JS _*_   function(x) { return function(y) { return x * y; }; } #-}
{-# COMPILED_JS _<_   function(x) { return function(y) { return x < y; }; } #-}
{-# COMPILED_JS ⌊_⌋   Math.floor #-}
{-# COMPILED_JS ⌈_⌉   Math.ceil #-}
{-# COMPILED_JS exp   Math.exp #-}
{-# COMPILED_JS log   Math.log #-}
{-# COMPILED_JS sin   Math.sin #-}

-_ : ℝ → ℝ
- x = 0.0 - x

_≠_ : ℝ → ℝ → Bool
(x ≠ y) = (x < y) ∨ (y < x)

_≟_ : ℝ → ℝ → Bool
(x ≟ y) = not (x ≠ y)

_≤_ : ℝ → ℝ → Bool
(x ≤ y) = not (y < x)

-- Some hoop-jumping to avoid division by zero, so we don't end up with
-- Infinity, -Infinity or NaN.

_/_ : (x y : ℝ) → {y≠0 : True (y ≠ 0.0)} → ℝ
x / y = primFloatDiv x y

_/?_ : ℝ → ℝ → Maybe ℝ
x /? 0.0 = nothing
x /? y   = just (primFloatDiv x y)

show : ℝ → String
show x
 with (x ≟ primIntegerToFloat ⌊ x ⌋)
... | true  = primShowInteger ⌊ x ⌋
... | false = primShowFloat x

{-# COMPILED_JS -_   function(x) { return -x; } #-}
{-# COMPILED_JS _≠_ function(x) { return function(y) { return x !== y; }; } #-}
{-# COMPILED_JS _≟_ function(x) { return function(y) { return x === y; }; } #-}
{-# COMPILED_JS _≤_  function(x) { return function(y) { return x <= y; }; } #-}
{-# COMPILED_JS _/_  function(x) { return function(y) { return function() { return x / y; }; }; } #-}
{-# COMPILED_JS _/?_  function(x) { return function(y) { if (y === 0) { return null; } else { return x / y; } }; } #-}
{-# COMPILED_JS show  function(x) { return x.toString(); } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some Vec-related properties
------------------------------------------------------------------------

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

module Data.Vec.Properties where

open import Algebra.FunctionProperties
open import Data.Empty using (⊥-elim)
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
open import Data.Fin.Properties using (_+′_)
open import Data.List.Base as List using (List)
open import Data.Nat
open import Data.Nat.Properties using (+-assoc; ≤-step)
open import Data.Product as Prod
  using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
open import Data.Vec
open import Function
open import Function.Inverse using (_↔_; inverse)
open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; _≗_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- Properties of propositional equality over vectors

module _ {a} {A : Set a} {n} {x y : A} {xs ys : Vec A n} where

 ∷-injectiveˡ : x ∷ xs ≡ y ∷ ys → x ≡ y
 ∷-injectiveˡ refl = refl

 ∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys
 ∷-injectiveʳ refl = refl

 ∷-injective : (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
 ∷-injective refl = refl , refl

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

  ≡-dec : B.Decidable _≡_ → ∀ {n} → B.Decidable {A = Vec A n} _≡_
  ≡-dec _≟_ []       []       = yes refl
  ≡-dec _≟_ (x ∷ xs) (y ∷ ys) with x ≟ y | ≡-dec _≟_ xs ys
  ... | yes refl | yes refl = yes refl
  ... | no  x≢y  | _        = no (x≢y   ∘ ∷-injectiveˡ)
  ... | yes _    | no xs≢ys = no (xs≢ys ∘ ∷-injectiveʳ)

------------------------------------------------------------------------
-- _[_]=_

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

  []=-injective : ∀ {n} {xs : Vec A n} {i x y} →
                  xs [ i ]= x → xs [ i ]= y → x ≡ y
  []=-injective here          here          = refl
  []=-injective (there xsᵢ≡x) (there xsᵢ≡y) = []=-injective xsᵢ≡x xsᵢ≡y

  -- See also Data.Vec.Properties.WithK.[]=-irrelevant.

------------------------------------------------------------------------
-- lookup

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

  []=⇒lookup : ∀ {n} {x : A} {xs} {i : Fin n} →
               xs [ i ]= x → lookup xs i ≡ x
  []=⇒lookup here            = refl
  []=⇒lookup (there xs[i]=x) = []=⇒lookup xs[i]=x

  lookup⇒[]= : ∀ {n} (i : Fin n) {x : A} xs →
               lookup xs i ≡ x → xs [ i ]= x
  lookup⇒[]= zero    (_ ∷ _)  refl = here
  lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)

  []=↔lookup : ∀ {n i} {x} {xs : Vec A n} →
               xs [ i ]= x ↔ lookup xs i ≡ x
  []=↔lookup {i = i} =
    inverse []=⇒lookup (lookup⇒[]= _ _)
            lookup⇒[]=∘[]=⇒lookup ([]=⇒lookup∘lookup⇒[]= _ i)
    where
    lookup⇒[]=∘[]=⇒lookup :
      ∀ {n x xs} {i : Fin n} (p : xs [ i ]= x) →
      lookup⇒[]= i xs ([]=⇒lookup p) ≡ p
    lookup⇒[]=∘[]=⇒lookup here      = refl
    lookup⇒[]=∘[]=⇒lookup (there p) =
      P.cong there (lookup⇒[]=∘[]=⇒lookup p)

    []=⇒lookup∘lookup⇒[]= :
      ∀ {n} xs (i : Fin n) {x} (p : lookup xs i ≡ x) →
      []=⇒lookup (lookup⇒[]= i xs p) ≡ p
    []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero    refl = refl
    []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p    =
      []=⇒lookup∘lookup⇒[]= xs i p

------------------------------------------------------------------------
-- updateAt (_[_]%=_)

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

  -- (+) updateAt i actually updates the element at index i.

  updateAt-updates : ∀ {n} (i : Fin n) {f : A → A} (xs : Vec A n) {x : A} →
                     xs [ i ]= x → (updateAt i f xs) [ i ]= f x
  updateAt-updates zero    (x ∷ xs) here        = here
  updateAt-updates (suc i) (x ∷ xs) (there loc) = there (updateAt-updates i xs loc)

  -- (-) updateAt i does not touch the elements at other indices.

  updateAt-minimal : ∀ {n} (i j : Fin n) {f : A → A} {x : A} (xs : Vec A n) →
                     i ≢ j → xs [ i ]= x → (updateAt j f xs) [ i ]= x
  updateAt-minimal zero    zero    (x ∷ xs) 0≢0 here        = ⊥-elim (0≢0 refl)
  updateAt-minimal zero    (suc j) (x ∷ xs) _   here        = here
  updateAt-minimal (suc i) zero    (x ∷ xs) _   (there loc) = there loc
  updateAt-minimal (suc i) (suc j) (x ∷ xs) i≢j (there loc) =
    there (updateAt-minimal i j xs (i≢j ∘ P.cong suc) loc)

  -- The other properties are consequences of (+) and (-).
  -- We spell the most natural properties out.
  -- Direct inductive proofs are in most cases easier than just using
  -- the defining properties.

  -- In the explanations, we make use of shorthand  f = g ↾ x
  -- meaning that f and g agree at point x, i.e.  f x ≡ g x.

  -- updateAt i  is a morphism from the monoid of endofunctions  A → A
  -- to the monoid of endofunctions  Vec A n → Vec A n

  -- 1a. relative identity:  f = id ↾ (lookup xs i)
  --                implies  updateAt i f = id ↾ xs

  updateAt-id-relative : ∀ {n} (i : Fin n) (xs : Vec A n) {f : A → A} →
                         f (lookup xs i) ≡ lookup xs i →
                         updateAt i f xs ≡ xs
  updateAt-id-relative zero    (x ∷ xs) eq = P.cong (_∷ xs) eq
  updateAt-id-relative (suc i) (x ∷ xs) eq = P.cong (x ∷_) (updateAt-id-relative i xs eq)

  -- 1b. identity:  updateAt i id ≗ id

  updateAt-id : ∀ {n} (i : Fin n) (xs : Vec A n) →
                updateAt i id xs ≡ xs
  updateAt-id i xs = updateAt-id-relative i xs refl

  -- 2a. relative composition:  f ∘ g = h ↾ (lookup i xs)
  --                   implies  updateAt i f ∘ updateAt i g ≗ updateAt i h

  updateAt-compose-relative : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vec A n) →
                              f (g (lookup xs i)) ≡ h (lookup xs i) →
                              updateAt i f (updateAt i g xs) ≡ updateAt i h xs
  updateAt-compose-relative zero    (x ∷ xs) fg=h = P.cong (_∷ xs) fg=h
  updateAt-compose-relative (suc i) (x ∷ xs) fg=h =
    P.cong (x ∷_) (updateAt-compose-relative i xs fg=h)

  -- 2b. composition:  updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)

  updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} →
                     updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
  updateAt-compose i xs = updateAt-compose-relative i xs refl

  -- 3. congruence:  updateAt i  is a congruence wrt. extensional equality.

  -- 3a.  If    f = g ↾ (lookup i xs)
  --      then  updateAt i f = updateAt i g ↾ xs

  updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vec A n) →
                           f (lookup xs i) ≡ g (lookup xs i) →
                           updateAt i f xs ≡ updateAt i g xs
  updateAt-cong-relative zero    (x ∷ xs) f=g = P.cong (_∷ xs) f=g
  updateAt-cong-relative (suc i) (x ∷ xs) f=g = P.cong (x ∷_) (updateAt-cong-relative i xs f=g)

  -- 3b. congruence:  f ≗ g → updateAt i f ≗ updateAt i g

  updateAt-cong : ∀ {n} (i : Fin n) {f g : A → A} →
                  f ≗ g → updateAt i f ≗ updateAt i g
  updateAt-cong i f≗g xs = updateAt-cong-relative i xs (f≗g (lookup xs i))

  -- The order of updates at different indices i ≢ j does not matter.

  -- This a consequence of updateAt-updates and updateAt-minimal
  -- but easier to prove inductively.

  updateAt-commutes : ∀ {n} (i j : Fin n) {f g : A → A} → i ≢ j →
                      updateAt i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
  updateAt-commutes zero    zero    0≢0 (x ∷ xs) = ⊥-elim (0≢0 refl)
  updateAt-commutes zero    (suc j) i≢j (x ∷ xs) = refl
  updateAt-commutes (suc i) zero    i≢j (x ∷ xs) = refl
  updateAt-commutes (suc i) (suc j) i≢j (x ∷ xs) =
    P.cong (x ∷_) (updateAt-commutes i j (i≢j ∘ P.cong suc) xs)

  -- lookup after updateAt reduces.

  -- For same index this is an easy consequence of updateAt-updates
  -- using []=↔lookup.

  lookup∘updateAt : ∀ {n} (i : Fin n) {f : A → A} →
                    ∀ xs → lookup (updateAt i f xs) i ≡ f (lookup xs i)
  lookup∘updateAt i xs =
    []=⇒lookup (updateAt-updates i xs (lookup⇒[]= i _ refl))

  -- For different indices it easily follows from updateAt-minimal.

  lookup∘updateAt′ : ∀ {n} (i j : Fin n) {f : A → A} → i ≢ j →
                     ∀ xs → lookup (updateAt j f xs) i ≡ lookup xs i
  lookup∘updateAt′ i j xs i≢j =
    []=⇒lookup (updateAt-minimal i j i≢j xs (lookup⇒[]= i _ refl))

  -- Aliases for notation _[_]%=_

  []%=-id : ∀ {n} (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs
  []%=-id xs i = updateAt-id i xs

  []%=-compose : ∀ {n} (xs : Vec A n) (i : Fin n) {f g : A → A} →
       xs [ i ]%= f
          [ i ]%= g
     ≡ xs [ i ]%= g ∘ f
  []%=-compose xs i = updateAt-compose i xs

------------------------------------------------------------------------
-- _[_]≔_ (update)
--
-- _[_]≔_ is defined in terms of updateAt, and all of its properties
-- are special cases of the ones for updateAt.

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

  []≔-idempotent : ∀ {n} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
                   (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
  []≔-idempotent xs i = updateAt-compose i xs

  []≔-commutes : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j →
                 (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
  []≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ P.sym) xs

  []≔-updates : ∀ {n} (xs : Vec A n) (i : Fin n) {x : A} →
                (xs [ i ]≔ x) [ i ]= x
  []≔-updates xs i = updateAt-updates i xs (lookup⇒[]= i xs refl)

  []≔-minimal : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j →
                xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
  []≔-minimal xs i j i≢j loc = updateAt-minimal i j xs i≢j loc

  []≔-lookup : ∀ {n} (xs : Vec A n) (i : Fin n) →
               xs [ i ]≔ lookup xs i ≡ xs
  []≔-lookup xs i = updateAt-id-relative i xs refl

  lookup∘update : ∀ {n} (i : Fin n) (xs : Vec A n) x →
                  lookup (xs [ i ]≔ x) i ≡ x
  lookup∘update i xs x = lookup∘updateAt i xs

  lookup∘update′ : ∀ {n} {i j : Fin n} → i ≢ j → ∀ (xs : Vec A n) y →
                   lookup (xs [ j ]≔ y) i ≡ lookup xs i
  lookup∘update′ {n} {i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs

------------------------------------------------------------------------
-- map

map-id : ∀ {a n} {A : Set a} → map {n = n} {A} id ≗ id
map-id []       = refl
map-id (x ∷ xs) = P.cong (x ∷_) (map-id xs)

map-cong : ∀ {a b n} {A : Set a} {B : Set b} {f g : A → B} →
           f ≗ g → map {n = n} f ≗ map g
map-cong f≗g []       = refl
map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

map-∘ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
        (f : B → C) (g : A → B) →
        map {n = n} (f ∘ g) ≗ map f ∘ map g
map-∘ f g []       = refl
map-∘ f g (x ∷ xs) = P.cong (f (g x) ∷_) (map-∘ f g xs)

lookup-map : ∀ {a b n} {A : Set a} {B : Set b}
             (i : Fin n) (f : A → B) (xs : Vec A n) →
             lookup (map f xs) i ≡ f (lookup xs i)
lookup-map zero    f (x ∷ xs) = refl
lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs

map-updateAt : ∀ {n a b} {A : Set a} {B : Set b} →
  ∀ {f : A → B} {g : A → A} {h : B → B} (xs : Vec A n) (i : Fin n)
  → f (g (lookup xs i)) ≡ h (f (lookup xs i))
  → map f (updateAt i g xs) ≡ updateAt i h (map f xs)
map-updateAt (x ∷ xs) zero    eq = P.cong (_∷ _) eq
map-updateAt (x ∷ xs) (suc i) eq = P.cong (_ ∷_) (map-updateAt xs i eq)

map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b}
          (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
          map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
map-[]≔ f xs i = map-updateAt xs i refl

------------------------------------------------------------------------
-- _++_

module _ {a} {A : Set a} {m} {ys ys' : Vec A m} where

  -- See also Data.Vec.Properties.WithK.++-assoc.

  ++-injectiveˡ : ∀ {n} (xs xs' : Vec A n) →
                  xs ++ ys ≡ xs' ++ ys' → xs ≡ xs'
  ++-injectiveˡ []       []         _  = refl
  ++-injectiveˡ (x ∷ xs) (x' ∷ xs') eq =
    P.cong₂ _∷_ (∷-injectiveˡ eq) (++-injectiveˡ _ _ (∷-injectiveʳ eq))

  ++-injectiveʳ : ∀ {n} (xs xs' : Vec A n) →
                  xs ++ ys ≡ xs' ++ ys' → ys ≡ ys'
  ++-injectiveʳ []       []         eq = eq
  ++-injectiveʳ (x ∷ xs) (x' ∷ xs') eq =
    ++-injectiveʳ xs xs' (∷-injectiveʳ eq)

  ++-injective  : ∀ {n} (xs xs' : Vec A n) →
                  xs ++ ys ≡ xs' ++ ys' → xs ≡ xs' × ys ≡ ys'
  ++-injective xs xs' eq =
    (++-injectiveˡ xs xs' eq , ++-injectiveʳ xs xs' eq)

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

  lookup-++-< : ∀ {m n} (xs : Vec A m) (ys : Vec A n) →
                ∀ i (i<m : toℕ i < m) →
                lookup (xs ++ ys)i  ≡ lookup xs (Fin.fromℕ≤ i<m)
  lookup-++-< []       ys i       ()
  lookup-++-< (x ∷ xs) ys zero    (s≤s z≤n)       = refl
  lookup-++-< (x ∷ xs) ys (suc i) (s≤s (s≤s i<m)) =
    lookup-++-< xs ys i (s≤s i<m)

  lookup-++-≥ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) →
                ∀ i (i≥m : toℕ i ≥ m) →
                lookup (xs ++ ys) i ≡ lookup ys (Fin.reduce≥ i i≥m)
  lookup-++-≥ []       ys i       i≥m       = refl
  lookup-++-≥ (x ∷ xs) ys zero    ()
  lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m

  lookup-++-inject+ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) i →
                      lookup (xs ++ ys) (Fin.inject+ n i) ≡ lookup xs i
  lookup-++-inject+ []       ys ()
  lookup-++-inject+ (x ∷ xs) ys zero    = refl
  lookup-++-inject+ (x ∷ xs) ys (suc i) = lookup-++-inject+ xs ys i

  lookup-++-+′ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) i →
                 lookup (xs ++ ys) (fromℕ m +′ i) ≡ lookup ys i
  lookup-++-+′ []       ys       zero    = refl
  lookup-++-+′ []       (y ∷ xs) (suc i) = lookup-++-+′ [] xs i
  lookup-++-+′ (x ∷ xs) ys       i       = lookup-++-+′ xs ys i

  []≔-++-inject+ : ∀ {m n x} (xs : Vec A m) (ys : Vec A n) i →
                   (xs ++ ys) [ Fin.inject+ n i ]≔ x ≡ (xs [ i ]≔ x) ++ ys
  []≔-++-inject+ []       ys ()
  []≔-++-inject+ (x ∷ xs) ys zero    = refl
  []≔-++-inject+ (x ∷ xs) ys (suc i) =
    P.cong (x ∷_) $ []≔-++-inject+ xs ys i

------------------------------------------------------------------------
-- zipWith

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

  zipWith-assoc : Associative _≡_ f → ∀ {n} →
                  Associative _≡_ (zipWith {n = n} f)
  zipWith-assoc assoc []       []       []       = refl
  zipWith-assoc assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) =
    P.cong₂ _∷_ (assoc x y z) (zipWith-assoc assoc xs ys zs)

  zipWith-idem : Idempotent _≡_ f → ∀ {n} →
                 Idempotent _≡_ (zipWith {n = n} f)
  zipWith-idem idem []       = refl
  zipWith-idem idem (x ∷ xs) =
    P.cong₂ _∷_ (idem x) (zipWith-idem idem xs)

  zipWith-identityˡ : ∀ {1#} → LeftIdentity _≡_ 1# f → ∀ {n} →
                      LeftIdentity _≡_ (replicate 1#) (zipWith {n = n} f)
  zipWith-identityˡ idˡ []       = refl
  zipWith-identityˡ idˡ (x ∷ xs) =
    P.cong₂ _∷_ (idˡ x) (zipWith-identityˡ idˡ xs)

  zipWith-identityʳ : ∀ {1#} → RightIdentity _≡_ 1# f → ∀ {n} →
                      RightIdentity _≡_ (replicate 1#) (zipWith {n = n} f)
  zipWith-identityʳ idʳ []       = refl
  zipWith-identityʳ idʳ (x ∷ xs) =
    P.cong₂ _∷_ (idʳ x) (zipWith-identityʳ idʳ xs)

  zipWith-zeroˡ : ∀ {0#} → LeftZero _≡_ 0# f → ∀ {n} →
                  LeftZero _≡_ (replicate 0#) (zipWith {n = n} f)
  zipWith-zeroˡ zeˡ []       = refl
  zipWith-zeroˡ zeˡ (x ∷ xs) =
    P.cong₂ _∷_ (zeˡ x) (zipWith-zeroˡ zeˡ xs)

  zipWith-zeroʳ : ∀ {0#} → RightZero _≡_ 0# f → ∀ {n} →
                  RightZero _≡_ (replicate 0#) (zipWith {n = n} f)
  zipWith-zeroʳ zeʳ []       = refl
  zipWith-zeroʳ zeʳ (x ∷ xs) =
    P.cong₂ _∷_ (zeʳ x) (zipWith-zeroʳ zeʳ xs)

  zipWith-inverseˡ : ∀ {⁻¹ 0#} → LeftInverse _≡_ 0# ⁻¹ f → ∀ {n} →
                     LeftInverse _≡_ (replicate {n = n} 0#) (map ⁻¹) (zipWith f)
  zipWith-inverseˡ invˡ []       = refl
  zipWith-inverseˡ invˡ (x ∷ xs) =
    P.cong₂ _∷_ (invˡ x) (zipWith-inverseˡ invˡ xs)

  zipWith-inverseʳ : ∀ {⁻¹ 0#} → RightInverse _≡_ 0# ⁻¹ f → ∀ {n} →
                     RightInverse _≡_ (replicate {n = n} 0#) (map ⁻¹) (zipWith f)
  zipWith-inverseʳ invʳ []       = refl
  zipWith-inverseʳ invʳ (x ∷ xs) =
    P.cong₂ _∷_ (invʳ x) (zipWith-inverseʳ invʳ xs)

  zipWith-distribˡ : ∀ {g} → _DistributesOverˡ_ _≡_ f g → ∀ {n} →
                     _DistributesOverˡ_ _≡_ (zipWith {n = n} f) (zipWith g)
  zipWith-distribˡ distribˡ []        []      []       = refl
  zipWith-distribˡ distribˡ (x ∷ xs) (y ∷ ys) (z ∷ zs) =
    P.cong₂ _∷_ (distribˡ x y z) (zipWith-distribˡ distribˡ xs ys zs)

  zipWith-distribʳ : ∀ {g} → _DistributesOverʳ_ _≡_ f g → ∀ {n} →
                     _DistributesOverʳ_ _≡_ (zipWith {n = n} f) (zipWith g)
  zipWith-distribʳ distribʳ []        []      []       = refl
  zipWith-distribʳ distribʳ (x ∷ xs) (y ∷ ys) (z ∷ zs) =
    P.cong₂ _∷_ (distribʳ x y z) (zipWith-distribʳ distribʳ xs ys zs)

  zipWith-absorbs : ∀ {g} → _Absorbs_ _≡_ f g → ∀ {n} →
                   _Absorbs_ _≡_ (zipWith {n = n} f) (zipWith g)
  zipWith-absorbs abs []       []       = refl
  zipWith-absorbs abs (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ (abs x y) (zipWith-absorbs abs xs ys)

module _ {a b} {A : Set a} {B : Set b} {f : A → A → B} where

  zipWith-comm : (∀ x y → f x y ≡ f y x) → ∀ {n}
                 (xs ys : Vec A n) → zipWith f xs ys ≡ zipWith f ys xs
  zipWith-comm comm []       []       = refl
  zipWith-comm comm (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ (comm x y) (zipWith-comm comm xs ys)

module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where

  zipWith-map₁ : ∀ {n} (_⊕_ : B → C → D) (f : A → B)
                 (xs : Vec A n) (ys : Vec C n) →
                 zipWith _⊕_ (map f xs) ys ≡ zipWith (λ x y → f x ⊕ y) xs ys
  zipWith-map₁ _⊕_ f []       []       = refl
  zipWith-map₁ _⊕_ f (x ∷ xs) (y ∷ ys) =
    P.cong (f x ⊕ y ∷_) (zipWith-map₁ _⊕_ f xs ys)

  zipWith-map₂ : ∀ {n} (_⊕_ : A → C → D) (f : B → C)
                 (xs : Vec A n) (ys : Vec B n) →
                 zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys
  zipWith-map₂ _⊕_ f []       []       = refl
  zipWith-map₂ _⊕_ f (x ∷ xs) (y ∷ ys) =
    P.cong (x ⊕ f y ∷_) (zipWith-map₂ _⊕_ f xs ys)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  lookup-zipWith : ∀ (f : A → B → C) {n} (i : Fin n) xs ys →
                   lookup (zipWith f xs ys) i ≡ f (lookup xs i) (lookup ys i)
  lookup-zipWith _ zero    (x ∷ _)  (y ∷ _)   = refl
  lookup-zipWith _ (suc i) (_ ∷ xs) (_ ∷ ys)  = lookup-zipWith _ i xs ys

------------------------------------------------------------------------
-- zip

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

  lookup-zip : ∀ {n} (i : Fin n) (xs : Vec A n) (ys : Vec B n) →
               lookup (zip xs ys) i ≡ (lookup xs i , lookup ys i)
  lookup-zip = lookup-zipWith _,_

  -- map lifts projections to vectors of products.

  map-proj₁-zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
                  map proj₁ (zip xs ys) ≡ xs
  map-proj₁-zip []       []       = refl
  map-proj₁-zip (x ∷ xs) (y ∷ ys) = P.cong (x ∷_) (map-proj₁-zip xs ys)

  map-proj₂-zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
                  map proj₂ (zip xs ys) ≡ ys
  map-proj₂-zip []       []       = refl
  map-proj₂-zip (x ∷ xs) (y ∷ ys) = P.cong (y ∷_) (map-proj₂-zip xs ys)

-- map lifts pairing to vectors of products.

map-<,>-zip : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
              (f : A → B) (g : A → C) (xs : Vec A n) →
              map < f , g > xs ≡ zip (map f xs) (map g xs)
map-<,>-zip f g []       = P.refl
map-<,>-zip f g (x ∷ xs) = P.cong (_ ∷_) (map-<,>-zip f g xs)

map-zip : ∀ {a b c d n} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          (f : A → B) (g : C → D) (xs : Vec A n) (ys : Vec C n) →
          map (Prod.map f g) (zip xs ys) ≡ zip (map f xs) (map g ys)
map-zip f g []       []       = refl
map-zip f g (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (map-zip f g xs ys)

------------------------------------------------------------------------
-- unzip

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

  lookup-unzip : ∀ {n} (i : Fin n) (xys : Vec (A × B) n) →
                 let xs , ys = unzip xys
                 in (lookup xs i , lookup ys i) ≡ lookup xys i
  lookup-unzip ()      []
  lookup-unzip zero    ((x , y) ∷ xys) = refl
  lookup-unzip (suc i) ((x , y) ∷ xys) = lookup-unzip i xys

  map-unzip : ∀ {c d n} {C : Set c} {D : Set d}
              (f : A → B) (g : C → D) (xys : Vec (A × C) n) →
              let xs , ys = unzip xys
              in (map f xs , map g ys) ≡ unzip (map (Prod.map f g) xys)
  map-unzip f g []              = refl
  map-unzip f g ((x , y) ∷ xys) =
    P.cong (Prod.map (f x ∷_) (g y ∷_)) (map-unzip f g xys)

  -- Products of vectors are isomorphic to vectors of products.

  unzip∘zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
              unzip (zip xs ys) ≡ (xs , ys)
  unzip∘zip [] []             = refl
  unzip∘zip (x ∷ xs) (y ∷ ys) =
    P.cong (Prod.map (x ∷_) (y ∷_)) (unzip∘zip xs ys)

  zip∘unzip : ∀ {n} (xys : Vec (A × B) n) →
              uncurry zip (unzip xys) ≡ xys
  zip∘unzip []              = refl
  zip∘unzip ((x , y) ∷ xys) = P.cong ((x , y) ∷_) (zip∘unzip xys)

  ×v↔v× : ∀ {n} → (Vec A n × Vec B n) ↔ Vec (A × B) n
  ×v↔v× = inverse (uncurry zip) unzip (uncurry unzip∘zip) zip∘unzip

------------------------------------------------------------------------
-- _⊛_

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

  lookup-⊛ : ∀ {n} i (fs : Vec (A → B) n) (xs : Vec A n) →
             lookup (fs ⊛ xs) i ≡ (lookup fs i $ lookup xs i)
  lookup-⊛ zero    (f ∷ fs) (x ∷ xs) = refl
  lookup-⊛ (suc i) (f ∷ fs) (x ∷ xs) = lookup-⊛ i fs xs

  map-is-⊛ : ∀ {n} (f : A → B) (xs : Vec A n) →
             map f xs ≡ (replicate f ⊛ xs)
  map-is-⊛ f []       = refl
  map-is-⊛ f (x ∷ xs) = P.cong (_ ∷_) (map-is-⊛ f xs)

  ⊛-is-zipWith : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) →
                 (fs ⊛ xs) ≡ zipWith _$_ fs xs
  ⊛-is-zipWith []       []       = refl
  ⊛-is-zipWith (f ∷ fs) (x ∷ xs) = P.cong (f x ∷_) (⊛-is-zipWith fs xs)

  zipWith-is-⊛ : ∀ {c} {C : Set c} {n} (f : A → B → C) →
                 (xs : Vec A n) (ys : Vec B n) →
                 zipWith f xs ys ≡ (replicate f ⊛ xs ⊛ ys)
  zipWith-is-⊛ f []       []       = refl
  zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (zipWith-is-⊛ f xs ys)

------------------------------------------------------------------------
-- foldr

-- See also Data.Vec.Properties.WithK.foldr-cong.

-- The (uniqueness part of the) universality property for foldr.

foldr-universal : ∀ {a b} {A : Set a} (B : ℕ → Set b)
                  (f : ∀ {n} → A → B n → B (suc n)) {e}
                  (h : ∀ {n} → Vec A n → B n) →
                  h [] ≡ e →
                  (∀ {n} x → h ∘ (x ∷_) ≗ f {n} x ∘ h) →
                  ∀ {n} → h ≗ foldr B {n} f e
foldr-universal B f {_} h base step []       = base
foldr-universal B f {e} h base step (x ∷ xs) = begin
  h (x ∷ xs)
    ≡⟨ step x xs ⟩
  f x (h xs)
    ≡⟨ P.cong (f x) (foldr-universal B f h base step xs) ⟩
  f x (foldr B f e xs)
    ∎
  where open P.≡-Reasoning

foldr-fusion : ∀ {a b c} {A : Set a}
               {B : ℕ → Set b} {f : ∀ {n} → A → B n → B (suc n)} e
               {C : ℕ → Set c} {g : ∀ {n} → A → C n → C (suc n)}
               (h : ∀ {n} → B n → C n) →
               (∀ {n} x → h ∘ f {n} x ≗ g x ∘ h) →
               ∀ {n} → h ∘ foldr B {n} f e ≗ foldr C g (h e)
foldr-fusion {B = B} {f} e {C} h fuse =
  foldr-universal C _ _ refl (λ x xs → fuse x (foldr B f e xs))

idIsFold : ∀ {a n} {A : Set a} → id ≗ foldr (Vec A) {n} _∷_ []
idIsFold = foldr-universal _ _ id refl (λ _ _ → refl)

------------------------------------------------------------------------
-- sum

sum-++-commute : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
                 sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []       {_}  = refl
sum-++-commute (x ∷ xs) {ys} = begin
  x + sum (xs ++ ys)     ≡⟨ P.cong (x +_) (sum-++-commute xs) ⟩
  x + (sum xs + sum ys)  ≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
  sum (x ∷ xs) + sum ys  ∎
  where open P.≡-Reasoning

------------------------------------------------------------------------
-- replicate

lookup-replicate : ∀ {a n} {A : Set a} (i : Fin n) (x : A) →
                   lookup (replicate x) i ≡ x
lookup-replicate zero    = λ _ → refl
lookup-replicate (suc i) = lookup-replicate i

map-replicate :  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) →
                 ∀ n → map f (replicate x) ≡ replicate {n = n} (f x)
map-replicate f x zero = refl
map-replicate f x (suc n) = P.cong (f x ∷_) (map-replicate f x n)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  zipWith-replicate₁ : ∀ {n} (_⊕_ : A → B → C) (x : A) (ys : Vec B n) →
                     zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys
  zipWith-replicate₁ _⊕_ x []       = refl
  zipWith-replicate₁ _⊕_ x (y ∷ ys) =
    P.cong (x ⊕ y ∷_) (zipWith-replicate₁ _⊕_ x ys)

  zipWith-replicate₂ : ∀ {n} (_⊕_ : A → B → C) (xs : Vec A n) (y : B) →
                     zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs
  zipWith-replicate₂ _⊕_ []       y = refl
  zipWith-replicate₂ _⊕_ (x ∷ xs) y =
    P.cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)

------------------------------------------------------------------------
-- tabulate

lookup∘tabulate : ∀ {a n} {A : Set a} (f : Fin n → A) (i : Fin n) →
                  lookup (tabulate f) i ≡ f i
lookup∘tabulate f zero    = refl
lookup∘tabulate f (suc i) = lookup∘tabulate (f ∘ suc) i

tabulate∘lookup : ∀ {a n} {A : Set a} (xs : Vec A n) →
                  tabulate (lookup xs) ≡ xs
tabulate∘lookup []       = refl
tabulate∘lookup (x ∷ xs) = P.cong (x ∷_) (tabulate∘lookup xs)

tabulate-∘ : ∀ {n a b} {A : Set a} {B : Set b}
             (f : A → B) (g : Fin n → A) →
             tabulate (f ∘ g) ≡ map f (tabulate g)
tabulate-∘ {zero}  f g = refl
tabulate-∘ {suc n} f g = P.cong (f (g zero) ∷_) (tabulate-∘ f (g ∘ suc))

tabulate-cong : ∀ {n a} {A : Set a} {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
tabulate-cong {zero} p = refl
tabulate-cong {suc n} p = P.cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))

------------------------------------------------------------------------
-- allFin

lookup-allFin : ∀ {n} (i : Fin n) → lookup (allFin n) i ≡ i
lookup-allFin = lookup∘tabulate id

allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
allFin-map n = P.cong (zero ∷_) $ tabulate-∘ suc id

tabulate-allFin : ∀ {n a} {A : Set a} (f : Fin n → A) →
                  tabulate f ≡ map f (allFin n)
tabulate-allFin f = tabulate-∘ f id

-- If you look up every possible index, in increasing order, then you
-- get back the vector you started with.

map-lookup-allFin : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
                    map (lookup xs) (allFin n) ≡ xs
map-lookup-allFin {n = n} xs = begin
  map (lookup xs) (allFin n) ≡˘⟨ tabulate-∘ (lookup xs) id ⟩
  tabulate (lookup xs)       ≡⟨ tabulate∘lookup xs ⟩
  xs                         ∎
  where open P.≡-Reasoning

------------------------------------------------------------------------
-- count

module _ {a p} {A : Set a} {P : Pred A p} (P? : Decidable P) where

  count≤n : ∀ {n} (xs : Vec A n) → count P? xs ≤ n
  count≤n []       = z≤n
  count≤n (x ∷ xs) with P? x
  ... | yes _ = s≤s (count≤n xs)
  ... | no  _ = ≤-step (count≤n xs)

------------------------------------------------------------------------
-- insert

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

  insert-lookup : ∀ {n} (xs : Vec A n) (i : Fin (suc n)) (v : A) →
                  lookup (insert xs i v) i ≡ v
  insert-lookup xs       zero     v = refl
  insert-lookup []       (suc ()) v
  insert-lookup (x ∷ xs) (suc i)  v = insert-lookup xs i v

  insert-punchIn : ∀ {n} (xs : Vec A n) (i : Fin (suc n)) (v : A)
                   (j : Fin n) →
                   lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j
  insert-punchIn xs       zero     v j       = refl
  insert-punchIn []       (suc ()) v j
  insert-punchIn (x ∷ xs) (suc i)  v zero    = refl
  insert-punchIn (x ∷ xs) (suc i)  v (suc j) = insert-punchIn xs i v j

  remove-punchOut : ∀ {n} (xs : Vec A (suc n))
                    {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
                    lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j
  remove-punchOut (x ∷ xs) {zero} {zero} i≢j = ⊥-elim (i≢j refl)
  remove-punchOut (x ∷ xs) {zero} {suc j} i≢j = refl
  remove-punchOut (x ∷ []) {suc ()} {j} i≢j
  remove-punchOut (x ∷ y ∷ xs) {suc i} {zero} i≢j = refl
  remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
    remove-punchOut (y ∷ xs) (i≢j ∘ P.cong suc)

------------------------------------------------------------------------
-- remove

  remove-insert : ∀ {n} (xs : Vec A n) (i : Fin (suc n)) (v : A) →
                  remove (insert xs i v) i ≡ xs
  remove-insert xs           zero           v = refl
  remove-insert []           (suc ())       v
  remove-insert (x ∷ xs)     (suc zero)     v = refl
  remove-insert (x ∷ [])     (suc (suc ())) v
  remove-insert (x ∷ y ∷ xs) (suc (suc i))  v =
    P.cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v)

  insert-remove : ∀ {n} (xs : Vec A (suc n)) (i : Fin (suc n)) →
                  insert (remove xs i) i (lookup xs i) ≡ xs
  insert-remove (x ∷ xs)     zero     = refl
  insert-remove (x ∷ [])     (suc ())
  insert-remove (x ∷ y ∷ xs) (suc i)  =
    P.cong (x ∷_) (insert-remove (y ∷ xs) i)

------------------------------------------------------------------------
-- Conversion function

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

  toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
  toList∘fromList List.[]       = refl
  toList∘fromList (x List.∷ xs) = P.cong (x List.∷_) (toList∘fromList xs)


text:
-- ASR (2016-12-23). UHC and GHC have different behaviours. This test
-- only is disabled for the UHC backend.

-- Issue #1856: UHC prints doubles with lower precision than GHC
--
-- For example, printing √2
--
-- GHC (8.0.1):   1.4142135623730951
-- UHC (1.1.9.5): 1.414213562373095

module _ where

open import Common.Prelude

print : Float → IO Unit
print x = putStrLn (primShowFloat x)

pi : Float
pi = 3.141592653589793

main : IO Unit
main =
  -- See Issue #1856.
  putStr "√2 = " ,, print (primFloatSqrt 2.0) ,,
  putStr "√2 = " ,, print (primFloatTimes 2.0 (primSin (primFloatDiv pi 4.0))) ,,
  return unit

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
data A : Set₁ → Set where
  C : (S : Set₁) → A S