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

module FarmFugue where

open import Data.Bool       using (Bool; true; false; if_then_else_)
open import Data.Fin        using (#_)
open import Data.List       using (List; _∷_; []; map; _++_)
open import Data.Nat        using (ℕ; _*_; _+_)
open import Data.Sign       using () renaming (+ to s+ ; - to s-)
open import Data.Vec        using (Vec; _∷_; []; lookup; foldl₁) renaming (map to vmap)
open import Function        using (_∘_)

open import Canon           using (makeCanon)
open import Interval
open import Instruments     using (pianos)
open import MakeTracks      using (makeTrackList)
open import Music           using (melody→notes; notes→melody; fixLength; dropPoints)
open import Note            using (Note; tone; rest; 8th; qtr; dqtr; half; whole; transposeNoteInterval)
open import Pitch           using (a; b; c; d; e; f; g)
open import MidiEvent       using (MidiTrack)
open import Util            using (repeat)
open import Transformation

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

b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 : List Note

b1 =
  tone 8th  (c 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (e 5) ∷
  rest 8th        ∷
  tone 8th  (e 5) ∷
  rest 8th        ∷
  tone 8th  (c 5) ∷
  rest 8th        ∷
  []

b2 =
  tone 8th  (c 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (c 5) ∷
  tone 8th  (d 5) ∷
  tone qtr  (e 5) ∷
  tone qtr  (c 5) ∷
  []

b3 =
  tone dqtr (e 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (e 5) ∷
  []

b4 =
  tone dqtr (e 5) ∷
  tone 8th  (e 5) ∷
  tone qtr  (g 4) ∷
  tone qtr  (b 4) ∷
  []

b5 =
  tone 8th  (c 6) ∷
  rest 8th        ∷
  tone 8th  (a 5) ∷
  rest 8th        ∷
  tone 8th  (e 5) ∷
  tone 8th  (f 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (f 5) ∷
  []

b6 =
  tone 8th  (c 6) ∷
  rest 8th        ∷
  tone 8th  (a 5) ∷
  rest 8th        ∷
  tone half (c 5) ∷
  []

b7 =
  tone 8th  (c 5) ∷
  rest 8th        ∷
  tone 8th  (e 5) ∷
  rest 8th        ∷
  tone 8th  (f 5) ∷
  rest 8th        ∷
  tone 8th  (d 5) ∷
  rest 8th        ∷
  []

b8 =
  tone 8th  (g 5) ∷
  tone 8th  (g 5) ∷
  tone 8th  (f 5) ∷
  tone 8th  (f 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (d 5) ∷
  []

b9 =
  tone qtr  (g 5) ∷
  tone qtr  (f 5) ∷
  tone qtr  (e 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (d 5) ∷
  []

b10 =
  tone dqtr (c 5) ∷
  tone 8th  (c 5) ∷
  tone 8th  (c 5) ∷
  rest 8th        ∷
  tone 8th  (c 5) ∷
  rest 8th        ∷
  []

b11 =
  tone qtr  (b 5) ∷
  tone qtr  (a 5) ∷
  tone qtr  (g 5) ∷
  tone qtr  (f 5) ∷
  []

b12 =
  tone qtr (c 4) ∷
  tone qtr (c 4) ∷
  []

b13 =
  tone 8th (c 4) ∷
  tone 8th (c 4) ∷
  tone 8th (c 4) ∷
  tone 8th (c 4) ∷
  []

subject countersubject extra base : List Note

subject = b1 ++ b3 ++ b1 ++ b4
countersubject = map (transposeNoteInterval (makeSigned s- per5)) (b5 ++ b6 ++ b5 ++ b7)
extra = b8 ++ b10 ++ b9 ++ b10
base = subject ++ countersubject ++ extra

transpositions : Vec Opi 3
transpositions = vmap (makeSigned s-) (per1 ∷ per5 ∷ per8 ∷ [])

-- Exposition is a truncated canon
expo exposition : Vec (List Note) 3
expo = makeCanon base 2 (whole + whole + whole + whole) transpositions
-- Truncate to first 20 bars (16 16th notes per bar in 4/4 time)
exposition = vmap (melody→notes ∘ fixLength (20 * 16) ∘ notes→melody) expo

-- Variation

doubleLastDuration : List Note → List Note
doubleLastDuration []                         = []
doubleLastDuration (m ∷ n ∷ ns)               = m ∷ doubleLastDuration (n ∷ ns)
doubleLastDuration (tone d p ∷ []) = tone (2 * d) p ∷ []
doubleLastDuration (rest d   ∷ []) = rest (2 * d) ∷ []

makeVariation : List Note → List Note → List Note → Vec (List Note) 3
makeVariation s c e =
  let base = s ++ c ++ e
      expo = makeCanon base 2 (whole + whole + whole + whole) transpositions
  in vmap (melody→notes ∘ fixLength (20 * 16) ∘ notes→melody) expo

makeVariation' : List Note → List Note → List Note → Vec (List Note) 3
makeVariation' s c e =
  let base = s ++ c ++ e
      expo = makeCanon base 2 (whole + whole + whole + whole) transpositions
  in vmap (melody→notes ∘ dropPoints (2 * 16) ∘ fixLength (16 * 16) ∘ notes→melody) expo

v1 v2 v3 variations : Vec (List Note) 3
v1 = makeVariation (doubleLastDuration subject) countersubject extra
v2 = makeVariation' (doubleLastDuration countersubject) extra subject
v3 = makeVariation' (doubleLastDuration extra) subject countersubject
variations = v1
--  (lookup v1 (# 0) ++ {- lookup v2 (# 0) ++ -} lookup v3 (# 0)) ∷
--  (lookup v1 (# 1) ++ {- lookup v2 (# 1) ++ -} lookup v3 (# 1)) ∷
--  (lookup v1 (# 2) ++ {- lookup v2 (# 2) ++ -} lookup v3 (# 2)) ∷
--  []

dev1 dev2 dev3 end1 end2 end3 line1 line2 line3 : List Note

dev1 =
  map (transposeNoteInterval (makeSigned s+ per12)) countersubject ++
  map (transposeNoteInterval (makeSigned s+ per12)) subject ++
  map (transposeNoteInterval (makeSigned s+ per12)) b8 ++
  map (transposeNoteInterval (makeSigned s+ per8))  b8 ++
  map (transposeNoteInterval (makeSigned s+ per4))  b8 ++
  map (transposeNoteInterval (makeSigned s- maj2))  b9 ++
  map (transposeNoteInterval (makeSigned s- per4))  subject ++
  map (transposeNoteInterval (makeSigned s- per5))  countersubject ++
  map (transposeNoteInterval (makeSigned s+ min3))  b12 ++
  map (transposeNoteInterval (makeSigned s+ maj3))  b12 ++
  map (transposeNoteInterval (makeSigned s+ min3))  b12 ++
  map (transposeNoteInterval (makeSigned s+ maj3))  b13

dev2 =
  map (transposeNoteInterval (makeSigned s+ per8)) subject ++
  map (transposeNoteInterval (makeSigned s+ per8)) countersubject ++
  map (transposeNoteInterval (makeSigned s+ per8)) b8 ++
  map (transposeNoteInterval (makeSigned s+ per4)) b8 ++
  map (transposeNoteInterval (makeSigned s- maj2)) b8 ++
  map (transposeNoteInterval (makeSigned s- maj6)) b9 ++
  map (transposeNoteInterval (makeSigned s- per8)) countersubject ++
  map (transposeNoteInterval (makeSigned s- per8)) subject ++
  map (transposeNoteInterval (makeSigned s- per4)) (b12 ++ b12 ++ b12 ++ b13)

dev3 =
  map (transposeNoteInterval (makeSigned s+ per5))  countersubject ++
  map (transposeNoteInterval (makeSigned s+ per5))  subject ++
  map (transposeNoteInterval (makeSigned s+ per5))  b8 ++
  map (transposeNoteInterval (makeSigned s+ per1))  b8 ++
  map (transposeNoteInterval (makeSigned s- per5))  b8 ++
  map (transposeNoteInterval (makeSigned s- maj9))  b9 ++
  map (transposeNoteInterval (makeSigned s- per12)) subject ++
  map (transposeNoteInterval (makeSigned s- per12)) countersubject ++
  map (transposeNoteInterval (makeSigned s- maj6))  b12 ++
  map (transposeNoteInterval (makeSigned s- min6))  b12 ++
  map (transposeNoteInterval (makeSigned s- maj6))  b12 ++
  map (transposeNoteInterval (makeSigned s- min6))  b13

end1 =
  map (transposeNoteInterval (makeSigned s+ per8)) b1
  ++ tone whole (e 6) ∷ []

end2 =
  map (transposeNoteInterval (makeSigned s+ per1)) b1
  ++ tone whole (g 5) ∷ []

end3 =
  map (transposeNoteInterval (makeSigned s- per8)) b1
  ++ tone whole (c 4) ∷ []

line1 = lookup exposition (# 0) ++ dev1 ++ lookup variations (# 0) ++ end1
line2 = lookup exposition (# 1) ++ dev2 ++ lookup variations (# 1) ++ end2
line3 = lookup exposition (# 2) ++ dev3 ++ lookup variations (# 2) ++ end3

fugue : Vec (List Note) 3
fugue = line1 ∷ line2 ∷ line3 ∷ []

tempo : ℕ
tempo = 160

fugueTracks : List MidiTrack
fugueTracks = makeTrackList pianos tempo fugue

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module PatternShadowsConstructor where

module A where

  data B : Set where
    x : B

  data C : Set where
    c : B → C

open A using (C; c)

f : C → C
f (c x) = x

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module STLCRef.Readme where

open import STLCRef.Syntax
open import STLCRef.Welltyped
open import STLCRef.Eval
open import STLCRef.Properties.Soundness


text:
{-# OPTIONS --type-in-type #-}
module prelude.io where
open import prelude
open import functors
open import Agda.Builtin.IO public using (IO)
open import Data.String
open import prelude.Stream as Stream using (Stream)
open import Data.List as L using (List)

IO[_,_] : Set → Set → Set
IO[ A , B ] = A → IO B

infixl 1 _>>=_

postulate
  return : ∀ {a} {A : Set a} → A → IO A
  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
  return>>= : ∀ {a b} (f : a → IO b) → (λ x → return x >>= f) ≡ f
  >>=return : ∀ {a b} (f : a → IO b) → (λ x → f x >>= return) ≡ f

{-# COMPILE GHC return = \_ _ -> return    #-}
{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}

-- record Category {O : Set} (𝒞[_,_] : O → O → Set) : Set where
--   constructor 𝒾:_▸:_𝒾▸:_▸𝒾:
--   infixl 8 _▸_
--   field
--     𝒾 : ∀ {x} → 𝒞[ x , x ]
--     _▸_ : ∀ {x y z} → 𝒞[ x , y ] → 𝒞[ y , z ] → 𝒞[ x , z ]
--     𝒾▸ : ∀ {x y} (f : 𝒞[ x , y ]) → (𝒾 ▸ f) ≡ f
--     ▸𝒾 : ∀ {x y} (f : 𝒞[ x , y ]) → (f ▸ 𝒾) ≡ f
-- open Category ⦃...⦄ public

instance
  io-cat : Category IO[_,_]
  io-cat = 𝒾: return ▸: (λ f g x → f x >>= g) 𝒾▸: return>>= ▸𝒾: >>=return

{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# FOREIGN GHC import qualified Data.Text.IO as T #-}

postulate
  getContents : IO String
  putStrLn    : String → IO ⊤

{-# COMPILE GHC getContents = T.getContents #-}
{-# COMPILE GHC putStrLn = T.putStrLn #-}

postulate
  showℕ : ℕ → String
{-# COMPILE GHC showℕ = T.pack . show #-}

{-# NON_TERMINATING #-}
printStream : Stream ℕ → IO ⊤
printStream s = putStrLn (showℕ (Stream.hd s)) >>= λ _ → printStream (Stream.tl s)

printList : List ℕ → IO ⊤
printList L.[] = return tt
printList (x L.∷ xs) = putStrLn (showℕ x) >>= λ _ → printList xs

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
-- 2014-05-26 Andrea & Andreas
-- hasBadRigids (in pruning) should reduce term before checking.

open import Common.Equality

postulate
  Fence : Set → Set

id : ∀{a}{A : Set a}(x : A) → A
id x = x

test : let H : Set; H = _; M : Set → Set; M = _ in
       (A : Set) → H ≡ Fence (M (id A))
test A = refl

-- Expected output:
-- M remains unsolved,
-- but H is solved by pruning the argument of M!

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Reflection.Helpers where

open import Agda.Builtin.Reflection
open import Function
open import Data.List as List using (List; _∷_; [])
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Nat.GeneralisedArithmetic using (fold)
open import Data.Fin as Fin using (Fin)
open import Data.Vec as Vec using (Vec)
open import Data.Nat.Table as Table using (Table)
open import Data.String using (String)
open import Data.Maybe as Maybe using (Maybe; just; nothing)

module _ {a} {A : Set a} where
  pure : A → TC A
  pure = returnTC
  {-# INLINE pure #-}

  infixl 3 _<|>_
  _<|>_ : TC A → TC A → TC A
  _<|>_ = catchTC
  {-# INLINE _<|>_ #-}

module _ {a b} {A : Set a} {B : Set b} where
  infixl 1 _>>=_ _>>_ _<&>_
  _>>=_ : TC A → (A → TC B) → TC B
  _>>=_ = bindTC
  {-# INLINE _>>=_ #-}

  _>>_ : TC A → TC B → TC B
  xs >> ys = bindTC xs (λ _ → ys)
  {-# INLINE _>>_ #-}

  infixl 4 _<$>_ _<*>_ _<$_
  _<*>_ : TC (A → B) → TC A → TC B
  fs <*> xs = bindTC fs (λ f → bindTC xs (λ x → returnTC (f x)))
  {-# INLINE _<*>_ #-}

  _<$>_ : (A → B) → TC A → TC B
  f <$> xs = bindTC xs (λ x → returnTC (f x))
  {-# INLINE _<$>_ #-}

  _<$_ : A → TC B → TC A
  x <$ xs = bindTC xs (λ _ → returnTC x)
  {-# INLINE _<$_ #-}

  _<&>_ : TC A → (A → B) → TC B
  xs <&> f = bindTC xs (λ x → returnTC (f x))
  {-# INLINE _<&>_ #-}

infixr 5 _⟨∷⟩_ _⟅∷⟆_
pattern _⟨∷⟩_ x xs = arg (arg-info visible relevant) x ∷ xs
pattern _⟅∷⟆_ x xs = arg (arg-info hidden  relevant) x ∷ xs

infixr 5 _⋯⟅∷⟆_
_⋯⟅∷⟆_ : ℕ → List (Arg Term) → List (Arg Term)
zero  ⋯⟅∷⟆ xs = xs
suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ i ⋯⟅∷⟆ xs
{-# INLINE _⋯⟅∷⟆_ #-}

ℕ′ : ℕ → Term
ℕ′ zero = quote zero ⟨ con ⟩ []
ℕ′ (suc i) = quote suc ⟨ con ⟩ ℕ′ i ⟨∷⟩ []

Fin′ : ℕ → Term
Fin′ zero = quote Fin.zero ⟨ con ⟩ 1 ⋯⟅∷⟆ []
Fin′ (suc i) = quote Fin.suc ⟨ con ⟩ 1 ⋯⟅∷⟆ Fin′ i ⟨∷⟩ []

curriedTerm : Table → Term
curriedTerm = List.foldr go (quote Vec.[] ⟨ con ⟩ 2 ⋯⟅∷⟆ []) ∘ Table.toList
  where
  go : ℕ → Term → Term
  go x xs = quote Vec._∷_ ⟨ con ⟩ 3 ⋯⟅∷⟆ var x [] ⟨∷⟩ xs ⟨∷⟩ []

hlams : ∀ {n} → Vec String n → Term → Term
hlams vs xs = Vec.foldr (const Term) (λ v vs → lam hidden (abs v vs)) xs vs

vlams : ∀ {n} → Vec String n → Term → Term
vlams vs xs = Vec.foldr (const Term) (λ v vs → lam visible (abs v vs)) xs vs

getVisible : Arg Term → Maybe Term
getVisible (arg (arg-info visible relevant) x) = just x
getVisible (arg (arg-info visible irrelevant) x) = nothing
getVisible (arg (arg-info hidden r) x) = nothing
getVisible (arg (arg-info instance′ r) x) = nothing

getArgs : ∀ n → Term → Maybe (Vec Term n)
getArgs n (def _ xs) = Maybe.map Vec.reverse (List.foldl f b (List.mapMaybe getVisible xs) n)
  where
  f : (∀ n → Maybe (Vec Term n)) → Term → ∀ n → Maybe (Vec Term n)
  f xs x zero = just Vec.[]
  f xs x (suc n) = Maybe.map (x Vec.∷_) (xs n)

  b : ∀ n → Maybe (Vec Term n)
  b zero = just Vec.[]
  b (suc _ ) = nothing
getArgs _ _ = nothing

open import Data.Product

underPi : Term → ∃[ n ] (Vec String n × Term)
underPi = go (λ xs y → _ , xs , y)
  where
  go : {A : Set} → (∀ {n} → Vec String n → Term → A) → Term → A
  go k (pi a (abs s x)) = go (k ∘ (s Vec.∷_)) x
  go k t = k Vec.[] t

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


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

module Bundles where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Structures.CommRing
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
-- open import Cubical.Structures.Poset
open import Cubical.Foundations.Function
open import Cubical.Structures.Ring
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_)

open import Function.Base using (_∋_)
-- open import Function.Reasoning using (∋-syntax)
open import Function.Base using (it) -- instance search

open import Utils
open import MoreLogic
open MoreLogic.Reasoning
open MoreLogic.Properties
open import MoreAlgebra
open MoreAlgebra.Definitions
open MoreAlgebra.Consequences

-- 4.1  Algebraic structure of numbers
--
-- Fields have the property that nonzero numbers have a multiplicative inverse, or more precisely, that
--   (∀ x : F) x ≠ 0 ⇒ (∃ y : F) x · y = 1.
--
-- Remark 4.1.1.
-- If we require the collection of numbers to form a set in the sense of Definition 2.5.4, and satisfy the ring axioms, then multiplicative inverses are unique, so that the above is equivalent to the proposition
--   (Π x : F) x ≠ 0 ⇒ (Σ y : F) x · y = 1.
--
-- Definition 4.1.2.
-- A classical field is a set F with points 0, 1 : F, operations +, · : F → F → F, which is a commutative ring with unit, such that
--   (∀ x : F) x ≠ 0 ⇒ (∃ y : F) x · y = 1.

module ClassicalFieldModule where
  record IsClassicalField {F : Type ℓ}
                          (0f : F) (1f : F) (_+_ : F → F → F) (_·_ : F → F → F) (-_ : F → F) (_⁻¹ᶠ : (x : F) → {{¬(x ≡ 0f)}} → F) : Type ℓ where
    constructor isclassicalfield

    field
      isCommRing : IsCommRing 0f 1f _+_ _·_ -_
      ·-rinv : (x : F) → (p : ¬(x ≡ 0f)) → x · (_⁻¹ᶠ x {{p}}) ≡ 1f
      ·-linv : (x : F) → (p : ¬(x ≡ 0f)) → (_⁻¹ᶠ x {{p}}) · x ≡ 1f

    open IsCommRing {0r = 0f} {1r = 1f} isCommRing public

  record ClassicalField : Type (ℓ-suc ℓ) where
    field
      Carrier : Type ℓ
      0f   : Carrier
      1f   : Carrier
      _+_  : Carrier → Carrier → Carrier
      _·_  : Carrier → Carrier → Carrier
      -_   : Carrier → Carrier
      _⁻¹ᶠ : (x : Carrier) → {{¬(x ≡ 0f)}} → Carrier
      isClassicalField : IsClassicalField 0f 1f _+_ _·_ -_ _⁻¹ᶠ

    infix  9 _⁻¹ᶠ
    infix  8 -_
    infixl 7 _·_
    infixl 6 _+_

    open IsClassicalField isClassicalField public

-- Remark 4.1.3.
-- As in the classical case, by proving that additive and multiplicative inverses are unique, we also obtain the negation and division operations.
--
-- For the reals, the assumption x ≠ 0 does not give us any information allowing us to bound x away from 0, which we would like in order to compute multiplicative inverses.
-- Hence, we give a variation on the denition of fields in which the underlying set comes equipped with an apartness relation #, which satises x # y ⇒ x ≠ y, although the converse implication may not hold.
-- This apartness relation allows us to make appropriate error bounds and compute multiplicative inverses based on the assumption x # 0.
--

-- NOTE: there is also PropRel in Cubical.Relation.Binary.Base which
-- NOTE: one needs these "all-lowercase constructors" to make use of copatterns
-- NOTE: see also Relation.Binary.Indexed.Homogeneous.Definitions.html
-- NOTE: see also Algebra.Definitions.html

-- Definition 4.1.5.
-- A constructive field is a set F with points 0, 1 : F, binary operations +, · : F → F → F, and a binary relation # such that
-- 1. (F, 0, 1, +, ·) is a commutative ring with unit;
-- 2. x : F has a multiplicative inverse iff x # 0;
-- 3. + is #-extensional, that is, for all w, x, y, z : F
--    w + x # y + z ⇒ w # y ∨ x # z.

record IsConstructiveField {F : Type ℓ}
                           (0f : F) (1f : F) (_+_ : F → F → F) (_·_ : F → F → F) (-_ : F → F) (_#_ : hPropRel F F ℓ') (_⁻¹ᶠ : (x : F) → {{[ x # 0f ]}} → F) : Type (ℓ-max ℓ ℓ') where
  constructor isconstructivefield

  field
    isCommRing : IsCommRing 0f 1f _+_ _·_ -_
    ·-rinv     : ∀ x → (p : [ x # 0f ]) → x · (_⁻¹ᶠ x {{p}}) ≡ 1f
    ·-linv     : ∀ x → (p : [ x # 0f ]) → (_⁻¹ᶠ x {{p}}) · x ≡ 1f
    ·-inv-back : ∀ x y → (x · y ≡ 1f) → [ x # 0f ] × [ y # 0f ]
    #-tight    : ∀ x y → ¬([ x # y ]) → x ≡ y
    -- NOTE: the following ⊎ caused trouble two times with resolving ℓ or ℓ'
    +-#-extensional : ∀ w x y z → [ (w + x) # (y + z) ] → [ (w # y) ⊔ (x # z) ]
    isApartnessRel  : IsApartnessRelᵖ _#_

  open IsCommRing {0r = 0f} {1r = 1f} isCommRing public
  open IsApartnessRelᵖ isApartnessRel public
    renaming
      ( isIrrefl  to #-irrefl
      ; isSym     to #-sym
      ; isCotrans to #-cotrans )

record ConstructiveField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor constructivefield
  field
    Carrier : Type ℓ
    0f   : Carrier
    1f   : Carrier
    _+_  : Carrier → Carrier → Carrier
    _·_  : Carrier → Carrier → Carrier
    -_   : Carrier → Carrier
    _#_  : hPropRel Carrier Carrier ℓ'
    _⁻¹ᶠ : (x : Carrier) → {{[ x # 0f ]}} → Carrier
    isConstructiveField : IsConstructiveField 0f 1f _+_ _·_ -_ _#_ _⁻¹ᶠ

  infix  9 _⁻¹ᶠ
  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _#_

  open IsConstructiveField isConstructiveField public

-- Definition 4.1.8.
-- Let (A, ≤) be a partial order, and let min, max : A → A → A be binary operators on A. We say that (A, ≤, min, max) is a lattice if min computes greatest lower bounds in the sense that for every x, y, z : A, we have
--   z ≤ min(x,y) ⇔ z ≤ x ∧ z ≤ y,
-- and max computes least upper bounds in the sense that for every x, y, z : A, we have
--   max(x,y) ≤ z ⇔ x ≤ z ∧ y ≤ z.

record IsLattice {A : Type ℓ}
                 (_≤_ : Rel A A ℓ') (min max : A → A → A) : Type (ℓ-max ℓ ℓ') where
  constructor islattice
  field
    isPartialOrder : IsPartialOrder _≤_
    glb      : ∀ x y z → z ≤ min x y → z ≤ x × z ≤ y
    glb-back : ∀ x y z → z ≤ x × z ≤ y → z ≤ min x y
    lub      : ∀ x y z → max x y ≤ z → x ≤ z × y ≤ z
    lub-back : ∀ x y z → x ≤ z × y ≤ z → max x y ≤ z

  open IsPartialOrder isPartialOrder public
    renaming
      ( isRefl    to ≤-refl
      ; isAntisym to ≤-antisym
      ; isTrans   to ≤-trans )

record Lattice : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor lattice
  field
    Carrier : Type ℓ
    _≤_ : Rel Carrier Carrier ℓ'
    min max : Carrier → Carrier → Carrier
    isLattice : IsLattice _≤_ min max

  infixl 4 _≤_

  open IsLattice isLattice public

-- Remark 4.1.9.2
-- 1. From the fact that (A, ≤, min, max) is a lattice, it does not follow that for every x and y, min(x,y) = x ∨ min(x,y) = y. However, we can characterize min as
--   z < min(x,y) ⇔ z < x ∨ z < y
--   and similarly for max, see Lemma 6.7.1.
-- 2. In a partial order, for two fixed elements a and b, all joins and meets of a, b are equal, so that Lemma 2.6.20 the type of joins and the type of meets are propositions. Hence, providing the maps min and max as in the above definition is equivalent to the showing the existenceof all binary joins and meets.
--
-- The following definition is modified from on The Univalent Foundations Program [89, Definition 11.2.7].
--
-- Definition 4.1.10.
-- An ordered field is a set F together with constants 0, 1, operations +, ·, min, max, and a binary relation < such that:
-- 1. (F, 0, 1, +, ·) is a commutative ring with unit;
-- 2. < is a strict [partial] order;
-- 3. x : F has a multiplicative inverse iff x # 0, recalling that # is defined as in Lemma 4.1.7;
-- 4. ≤, as in Lemma 4.1.7, is antisymmetric, so that (F, ≤) is a partial order;
-- 5. (F, ≤, min, max) is a lattice.
-- 6. for all x, y, z, w : F:
--    x + y < z + w ⇒ x < z ∨ y < w, (†)
--    0 < z ∧ x < y ⇒ x z < y z.     (∗)
-- Our notion of ordered fields coincides with The Univalent Foundations Program [89, Definition 11.2.7].

-- NOTE: well, the HOTT book definition organizes things slightly different. Why prefer one approach over the other?

record IsAlmostOrderedField {F : Type ℓ}
                 (0f 1f : F) (_+_ : F → F → F) (-_ : F → F) (_·_ min max : F → F → F) (_<_ _#_ _≤_ : Rel F F ℓ') (_⁻¹ᶠ : (x : F) → {{x # 0f}} → F) : Type (ℓ-max ℓ ℓ') where
  field
    -- 1.
    isCommRing : IsCommRing 0f 1f _+_ _·_ -_
    -- 2.
    <-isStrictPartialOrder : IsStrictPartialOrder _<_
    -- 3.
    ·-rinv     : (x : F) → (p : x # 0f) → x · (_⁻¹ᶠ x {{p}}) ≡ 1f
    ·-linv     : (x : F) → (p : x # 0f) → (_⁻¹ᶠ x {{p}}) · x ≡ 1f
    ·-inv-back : (x y : F) → (x · y ≡ 1f) → x # 0f × y # 0f
    -- 4. NOTE: we already have ≤-isPartialOrder in <-isLattice
    -- ≤-isPartialOrder : IsPartialOrder _≤_
    -- 5.
    ≤-isLattice : IsLattice _≤_ min max

  open IsCommRing {0r = 0f} {1r = 1f} isCommRing public
  open IsStrictPartialOrder <-isStrictPartialOrder public
    renaming
      ( isIrrefl  to <-irrefl
      ; isTrans   to <-trans
      ; isCotrans to <-cotrans )
  open IsLattice ≤-isLattice public

record AlmostOrderedField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor orderedfield
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : Rel Carrier Carrier ℓ'
    <-isProp : ∀ x y → isProp (x < y)

  _#_ = _#'_ {_<_ = _<_}
  _≤_ = _≤'_ {_<_ = _<_}

  field
    _⁻¹ᶠ    : (x : Carrier) → {{x # 0f}} → Carrier
    isAlmostOrderedField : IsAlmostOrderedField 0f 1f _+_ -_ _·_ min max _<_ _#_ _≤_ _⁻¹ᶠ

  infix  9 _⁻¹ᶠ
  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _#_
  infixl 4 _≤_
  infixl 4 _<_

  open IsAlmostOrderedField isAlmostOrderedField public

  #-isProp : ∀ x y → isProp (x # y)
  #-isProp = #-from-<-isProp _<_ <-isStrictPartialOrder <-isProp

record IsOrderedField {F : Type ℓ}
                 (0f 1f : F) (_+_ : F → F → F) (-_ : F → F) (_·_ min max : F → F → F) (_<_ _#_ _≤_ : Rel F F ℓ') (_⁻¹ᶠ : (x : F) → {{x # 0f}} → F) : Type (ℓ-max ℓ ℓ') where
  constructor isorderedfield
  field
    -- 1. 2. 3. 4. 5.
    isAlmostOrderedField : IsAlmostOrderedField 0f 1f _+_ -_ _·_ min max _<_ _#_ _≤_ _⁻¹ᶠ
    -- 6. (†)
    -- NOTE: this is 'shifted' from the pevious definition of #-extensionality for + .. does the name still fit?
    +-<-extensional : ∀ w x y z → (x + y) < (z + w) → (x < z) ⊎ (y < w)
    -- 6. (∗)
    ·-preserves-< : ∀ x y z → 0f < z → x < y → (x · z) < (y · z)
  open IsAlmostOrderedField isAlmostOrderedField public

record OrderedField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor orderedfield
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : Rel Carrier Carrier ℓ'
    <-isProp : ∀ x y → isProp (x < y)

  _#_ = _#'_ {_<_ = _<_}
  _≤_ = _≤'_ {_<_ = _<_}

  field
    _⁻¹ᶠ    : (x : Carrier) → {{x # 0f}} → Carrier
    isOrderedField : IsOrderedField 0f 1f _+_ -_ _·_ min max _<_ _#_ _≤_ _⁻¹ᶠ

  infix  9 _⁻¹ᶠ
  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _#_
  infixl 4 _≤_
  infixl 4 _<_

  open IsOrderedField isOrderedField public

  abstract
    -- NOTE: there might be some reason not to "do" (or "open") all the theory of a record within that record
    +-preserves-< : ∀ a b x → a < b → a + x < b + x
    +-preserves-< a b x a<b = (
       a            <  b            ⇒⟨ transport (λ i → sym (fst (+-identity a)) i < sym (fst (+-identity b)) i) ⟩
       a +    0f    <  b +    0f    ⇒⟨ transport (λ i → a + sym (+-rinv x) i < b + sym (+-rinv x) i) ⟩
       a + (x  - x) <  b + (x  - x) ⇒⟨ transport (λ i → +-assoc a x (- x) i < +-assoc b x (- x) i) ⟩
      (a +  x) - x  < (b +  x) - x  ⇒⟨ +-<-extensional (- x) (a + x) (- x) (b + x) ⟩
      (a + x < b + x) ⊎ (- x < - x) ⇒⟨ (λ{ (inl a+x<b+x) → a+x<b+x -- somehow ⊥-elim needs a hint in the next line
                                         ; (inr  -x<-x ) → ⊥-elim {A = λ _ → (a + x < b + x)} (<-irrefl (- x) -x<-x) }) ⟩
       a + x < b + x ◼) a<b

    ≤-isPreorder : IsPreorder _≤_
    ≤-isPreorder = ≤-isPreorder' {_<_ = _<_} {<-isStrictPartialOrder}

-- Definition 4.3.1.
-- A morphism from an ordered field (F, 0F , 1F , +F , ·F , minF , maxF , <F )
--              to an ordered field (G, 0G , 1G , +G , ·G , minG , maxG , <G )
-- is a map f : F → G such that
-- 1. f is a morphism of rings,
-- 2. f reflects < in the sense that for every x, y : F
--    f (x) <G f (y) ⇒ x <F y.

-- NOTE: see Cubical.Structures.Group.Morphism
--       and Cubical.Structures.Group.MorphismProperties

-- open import Cubical.Structures.Group.Morphism

record IsRingMor
  {ℓ ℓ'}
  (F : Ring {ℓ}) (G : Ring {ℓ'})
  (f : (Ring.Carrier F) → (Ring.Carrier G)) : Type (ℓ-max ℓ ℓ')
  where
  module F = Ring F
  module G = Ring G
  field
    preserves-+ : ∀ a b → f (a F.+ b) ≡ f a G.+ f b
    preserves-· : ∀ a b → f (a F.· b) ≡ f a G.· f b
    perserves-1 : f F.1r ≡ G.1r

record IsOrderedFieldMor
  {ℓ ℓ' ℓₚ ℓₚ'} -- NOTE: this is a lot of levels. Can we get rid of some of these?
  (F : OrderedField {ℓ} {ℓₚ}) (G : OrderedField {ℓ'} {ℓₚ'})
  -- (let module F = OrderedField F) -- NOTE: `let` is not allowed in a telescope
  -- (let module G = OrderedField G)
  (f : (OrderedField.Carrier F) → (OrderedField.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  module F = OrderedField F
  module G = OrderedField G
  field
    isRingMor : IsRingMor (record {F}) (record {G}) f
    reflects-< : ∀ x y → f x G.< f y → x F.< y
  -- NOTE: for more properties, see https://en.wikipedia.org/wiki/Ring_homomorphism#Properties

record OrderedFieldMor {ℓ ℓ' ℓₚ ℓₚ'} (F : OrderedField {ℓ} {ℓₚ}) (G : OrderedField {ℓ'} {ℓₚ'}) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ')) where
  constructor orderedfieldmor
  module F = OrderedField F
  module G = OrderedField G
  field
    fun : F.Carrier → G.Carrier
    isOrderedFieldMor : IsOrderedFieldMor F G fun

-- NOTE: f preserves P: P A ⇒ P (f A)
--       f reflects  P: P (f A) ⇒ P A
-- Remark 4.3.2. The contrapositive of reflecting < means preserving ≤.

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- Soundness of normalization w.r.t. to declarative kinding of Fω with
-- interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Declarative.Normalization where

open import Data.Fin using (zero)
open import Data.Fin.Substitution
open import Data.Product using (_,_; proj₂; _×_)
open import Data.Vec using ([])
open import Relation.Binary.PropositionalEquality hiding ([_])

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Typing
open import FOmegaInt.Typing.Validity

open Syntax
open TermCtx
open Substitution hiding (subst)
open ContextConversions
open Typing
open TypedSubstitution

------------------------------------------------------------------------
-- Soundness of hereditary substitutions

-- NOTE. The following are corollaries of the corresponding soundness
-- lemmas using untyped β-reduction and the subject reduction property
-- for kinding (see the Syntax.HereditarySubstitution and
-- Typing.Validity modules for details).

-- Soundness of hereditary substitution: the results of ordinary and
-- hereditary substitutions in well-formed kinds resp. well-kinded
-- types are equal (w.r.t. type resp. kind equality).

kd-⌞⌟-[]-≅ : ∀ {n} {Γ : Ctx n} {j k a} →
             kd ⌞ j ⌟Kd ∷ Γ ⊢ ⌞ k ⌟Kd kd → Γ ⊢Tp ⌞ a ⌟ ∈ ⌞ j ⌟Kd →
             Γ ⊢ ⌞ k ⌟Kd Kind[ ⌞ a ⌟ ] ≅ ⌞ k Kind[ a ∈ ⌊ j ⌋ ] ⌟Kd
kd-⌞⌟-[]-≅ {k = k} ⌞k⌟-kd ⌞a⌟∈⌞j⌟ =
  kd-→β*-≅ (kd-[] ⌞k⌟-kd (∈-tp ⌞a⌟∈⌞j⌟)) (⌞⌟Kd-/⟨⟩-β k)

Tp∈-⌞⌟-[]-≃ : ∀ {n} {Γ : Ctx n} {j a k b} →
              kd ⌞ j ⌟Kd ∷ Γ ⊢Tp ⌞ a ⌟ ∈ ⌞ k ⌟Kd → Γ ⊢Tp ⌞ b ⌟ ∈ ⌞ j ⌟Kd →
              Γ ⊢ ⌞ a ⌟ [ ⌞ b ⌟ ] ≃ ⌞ a [ b ∈ ⌊ j ⌋ ] ⌟ ∈ ⌞ k ⌟Kd Kind[ ⌞ b ⌟ ]
Tp∈-⌞⌟-[]-≃ {a = a} ⌞a⌟∈⌞k⌟ ⌞b⌟∈⌞j⌟ =
  Tp∈-→β*-≃ (Tp∈-[] ⌞a⌟∈⌞k⌟ (∈-tp ⌞b⌟∈⌞j⌟)) (⌞⌟-/⟨⟩-β a)

-- Soundness of potentially reducing application: ordinary and
-- potentially reducing application of well-kinded types are equal
-- (w.r.t. type equality).
Tp∈-⌞⌟-·-≃ : ∀ {n} {Γ : Ctx n} {a b j k} →
             Γ ⊢Tp ⌞ a ⌟ ∈ Π j k → Γ ⊢Tp ⌞ b ⌟ ∈ j →
             Γ ⊢ ⌞ a ⌟ · ⌞ b ⌟ ≃ ⌞ a ↓⌜·⌝ b ⌟ ∈ k Kind[ ⌞ b ⌟ ]
Tp∈-⌞⌟-·-≃ {_} {_} {a} {b} {j} {k} ⌞a⌟∈Πjk ⌞b⌟∈j =
  Tp∈-→β*-≃ (∈-Π-e ⌞a⌟∈Πjk ⌞b⌟∈j) (⌞⌟-↓⌜·⌝-β a b)

------------------------------------------------------------------------
-- Soundness of η-expansion.

module TrackSimpleKindsDeclarativeEtaExp where
  open RenamingCommutes
  open SimpHSubstLemmas
  private
    module V   = VarSubst
    module TK  = TrackSimpleKindsEtaExp

  -- NOTE. The definition of the function Tp∈-⌞⌟-≃-η below is
  -- structurally recursive in the *shape* parameter k, but *not* in
  -- the kind j because we need to weaken the domain j₁ of the
  -- dependent kind (j = Π j₁ j₂) in the arrow case.  The additional
  -- hypothesis ⌊ j ⌋≡ k ensures that k is indeed the shape of the
  -- kind j.

  -- Well-kinded neutrals are equal to to their η-expansions.
  Tp∈-⌞⌟-≃-η : ∀ {n} {Γ : Ctx n} {x as j k} (hyp : ⌊ j ⌋≡ k) →
               Γ ⊢ ⌞ j ⌟Kd kd → Γ ⊢Tp ⌞ var x ∙ as ⌟ ∈ ⌞ j ⌟Kd →
               Γ ⊢ ⌞ var x ∙ as ⌟ ≃ ⌞ TK.η-exp j hyp (var x ∙ as) ⌟ ∈ ⌞ j ⌟Kd
  Tp∈-⌞⌟-≃-η is-★ ⌞b₂⋯c₂⌟-kd ⌞x∙as⌟∈⌞b₁⋯c₁⌟ = ≃-refl ⌞x∙as⌟∈⌞b₁⋯c₁⌟
  Tp∈-⌞⌟-≃-η {_} {Γ} {x} {as} (is-⇒ {j₁} {j₂} ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂)
             (kd-Π ⌞j₁⌟-kd ⌞j₂⌟-kd) ⌞x∙as⌟∈⌞Πj₁j₂⌟ =
    begin
      ⌞ var x ∙ as ⌟
    ≃⟨ ≃-sym (≃-η ⌞x∙as⌟∈⌞Πj₁j₂⌟) ⟩
      Λ ⌞ j₁ ⌟Kd (weaken ⌞ var x ∙ as ⌟ · var zero)
    ≃⟨ ≃-λ′ (≅-refl ⌞j₁⌟-kd) (begin
        weaken ⌞ var x ∙ as ⌟ · var zero
      ≃⟨ ⌞x∙as⌟·z≃⌞x∙as⌟·⌞η-z⌟∈⌞j₂⌟ ⟩
        weaken ⌞ var x ∙ as ⌟ ·
          ⌞ TK.η-exp (weakenKind′ _) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero) ⌟
      ≡⟨ ⌞x∙as⌟·⌞η-z⌟≡⌞x∙as⌜·⌝η-z⌟ ⟩
        ⌞ weakenElim (var x ∙ as) ⌜·⌝
          TK.η-exp (weakenKind′ _) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero) ⌟
      ≃⟨ Tp∈-⌞⌟-≃-η ⌊j₂⌋≡k₂ ⌞j₂⌟-kd
                    (subst (_ ⊢Tp_∈ _) ⌞x∙as⌟·⌞η-z⌟≡⌞x∙as⌜·⌝η-z⌟
                           ⌞x∙as⌟·⌞η-z⌟∈⌞j₂⌟) ⟩
        ⌞ TK.η-exp j₂ ⌊j₂⌋≡k₂ _ ⌟
      ∎) ⟩
      ⌞ TK.η-exp (Π j₁ j₂) (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) (var x ∙ as) ⌟
    ∎
    where
      ⌞j₁⌟-wf     = wf-kd ⌞j₁⌟-kd
      ⌞j₁⌟′-kd    = kd-weaken ⌞j₁⌟-wf ⌞j₁⌟-kd
      ⌞j₁⌟′≡⌞j₁′⌟ = sym (⌞⌟Kd-/Var j₁)
      ⌞j₁′⌟-kd    = subst (kd ⌞ j₁ ⌟Kd ∷ _ ⊢_kd) ⌞j₁⌟′≡⌞j₁′⌟ ⌞j₁⌟′-kd
      ⌞j₁⌟∷Γ-ctx  = ⌞j₁⌟-wf ∷ Tp∈-ctx ⌞x∙as⌟∈⌞Πj₁j₂⌟

      ⌞x∙as⌟′∈⌞Πj₁j₂′⌟ = subst (kd ⌞ j₁ ⌟Kd ∷ Γ ⊢Tp weaken ⌞ var x ∙ as ⌟ ∈_)
                               (sym (⌞⌟Kd-/Var (Π j₁ j₂)))
                               (Tp∈-weaken ⌞j₁⌟-wf ⌞x∙as⌟∈⌞Πj₁j₂⌟)

      z∈⌞j₁⌟      = ∈-var zero ⌞j₁⌟∷Γ-ctx (cong kd ⌞j₁⌟′≡⌞j₁′⌟ )
      z≃η-z∈⌞j₁⌟  = Tp∈-⌞⌟-≃-η (⌊⌋≡-weaken ⌊j₁⌋≡k₁) ⌞j₁′⌟-kd z∈⌞j₁⌟
      ⌞j₂′⌟[z]≡⌞j₂⌟ =
        begin
          ⌞ j₂ Kind′/Var V.wk V.↑ ⌟Kd Kind[ var zero ]
        ≡⟨ cong (_Kind[ var zero ]) (⌞⌟Kd-/Var j₂) ⟩
          (⌞ j₂ ⌟Kd Kind/Var V.wk V.↑) Kind[ var zero ]
        ≡⟨ Kind-wk↑-sub-zero-vanishes ⌞ j₂ ⌟Kd ⟩
          ⌞ j₂ ⌟Kd
        ∎
        where open ≡-Reasoning

      ⌞x∙as⌟·z≃⌞x∙as⌟·⌞η-z⌟∈⌞j₂⌟ =
        subst (_ ⊢ _ ≃ _ ∈_) ⌞j₂′⌟[z]≡⌞j₂⌟
              (≃-· (≃-refl (⌞x∙as⌟′∈⌞Πj₁j₂′⌟)) z≃η-z∈⌞j₁⌟)
      ⌞x∙as⌟·⌞η-z⌟∈⌞j₂⌟ = proj₂ (≃-valid ⌞x∙as⌟·z≃⌞x∙as⌟·⌞η-z⌟∈⌞j₂⌟)
      ⌞x∙as⌟·⌞η-z⌟≡⌞x∙as⌜·⌝η-z⌟ =
        begin
          weaken ⌞ var x ∙ as ⌟ ·
            ⌞ TK.η-exp (weakenKind′ _) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero) ⌟
        ≡⟨ cong (_· _) (sym (⌞⌟-/Var (var x ∙ as)))  ⟩
          ⌞ weakenElim (var x ∙ as) ⌟ ·
            ⌞ TK.η-exp (weakenKind′ _) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero) ⌟
        ≡⟨ sym (⌞⌟-· (weakenElim (var x ∙ as)) _) ⟩
          ⌞ weakenElim (var x ∙ as) ⌜·⌝
            TK.η-exp (weakenKind′ _) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero) ⌟
        ∎
        where open ≡-Reasoning

      open ≃-Reasoning

private module TK  = TrackSimpleKindsDeclarativeEtaExp

-- Soundness of η-expansion of neutrals: well-kinded neutral types are
-- equal to their η-expansions (w.r.t. to type equality).
Tp∈-⌞⌟-≃-η : ∀ {n} {Γ : Ctx n} {x as k} →
             Γ ⊢Tp ⌞ var x ∙ as ⌟ ∈ ⌞ k ⌟Kd →
             Γ ⊢ ⌞ var x ∙ as ⌟ ≃ ⌞ η-exp k (var x ∙ as) ⌟ ∈ ⌞ k ⌟Kd
Tp∈-⌞⌟-≃-η ⌞x∙as⌟∈⌞k⌟ =
  TK.Tp∈-⌞⌟-≃-η (⌊⌋-⌊⌋≡ _) (Tp∈-valid ⌞x∙as⌟∈⌞k⌟) ⌞x∙as⌟∈⌞k⌟

------------------------------------------------------------------------
-- Soundness of normalization

mutual

  -- Soundness of normalization: well-formed kinds and well-kinded
  -- types are equal to their normal forms (w.r.t. to kind resp. type
  -- equality).

  Tp∈-≃-⌞⌟-nf : ∀ {n} {Γ : Ctx n} {a k} →
                Γ ⊢Tp a ∈ k → Γ ⊢ a ≃ ⌞ nf (nfCtx Γ) a ⌟ ∈ k
  Tp∈-≃-⌞⌟-nf {_} {Γ} (∈-var {k} x Γ-ctx Γ[x]≡kd-k)
    with ElimCtx.lookup (nfCtx Γ) x | nfCtx-lookup-kd x Γ Γ[x]≡kd-k
  ... | kd ._ | refl =
    ≃-⇑ (Tp∈-⌞⌟-≃-η (∈-⇑ (∈-var x Γ-ctx Γ[x]≡kd-k) (≅⇒<∷ k≅⌞nf-k⌟)))
        (≅⇒<∷ (≅-sym k≅⌞nf-k⌟))
    where
      open ≡-Reasoning
      open CtxEqOps using (lookup-≃-kd)

      Γ≃⌞nf-Γ⌟         = ctx-≃-⌞⌟-nf Γ-ctx
      ⌞nf-Γ⌟[x]≡kd-⌞k⌟ = begin
          lookup ⌞ nfCtx Γ ⌟Ctx x
        ≡⟨ ⌞⌟Asc-lookup (nfCtx Γ) x ⟩
          ⌞ ElimCtx.lookup (nfCtx Γ) x ⌟Asc
        ≡⟨ cong ⌞_⌟Asc (nfCtx-lookup-kd x Γ Γ[x]≡kd-k) ⟩
          kd ⌞ nfKind (nfCtx Γ) k ⌟Kd
        ∎

      k≅⌞nf-k⌟ : Γ ⊢ k ≅ ⌞ nfKind (nfCtx Γ) k ⌟Kd
      k≅⌞nf-k⌟ = lookup-≃-kd x Γ≃⌞nf-Γ⌟ Γ[x]≡kd-k ⌞nf-Γ⌟[x]≡kd-⌞k⌟
  Tp∈-≃-⌞⌟-nf (∈-⊥-f Γ-ctx) = ≃-refl (∈-⊥-f Γ-ctx)
  Tp∈-≃-⌞⌟-nf (∈-⊤-f Γ-ctx) = ≃-refl (∈-⊤-f Γ-ctx)
  Tp∈-≃-⌞⌟-nf (∈-∀-f k-kd a∈*) = ≃-∀ (kd-≅-⌞⌟-nf k-kd) (Tp∈-≃-⌞⌟-nf a∈*)
  Tp∈-≃-⌞⌟-nf (∈-→-f a∈* b∈*)  = ≃-→ (Tp∈-≃-⌞⌟-nf a∈*) (Tp∈-≃-⌞⌟-nf b∈*)
  Tp∈-≃-⌞⌟-nf (∈-Π-i j-kd a∈k) = ≃-λ′ (kd-≅-⌞⌟-nf j-kd) (Tp∈-≃-⌞⌟-nf a∈k)
  Tp∈-≃-⌞⌟-nf {_} {Γ} (∈-Π-e {a} {b} {j} {k} a∈Πjk b∈j) with Tp∈-valid a∈Πjk
  ... | (kd-Π j-kd k-kd) =
    begin
      a · b
    ≃⟨ ≃-· a≃⌞nf-a⌟∈Πjk b≃⌞nf-b⌟∈j ⟩
      ⌞ nf (nfCtx Γ) a ⌟ · ⌞ nf (nfCtx Γ) b ⌟
    ≃⟨ ≃-⇑ (Tp∈-⌞⌟-·-≃ {a = nf (nfCtx Γ) a} {nf (nfCtx Γ) b}
                       ⌞nf-a⌟∈Πjk ⌞nf-b⌟∈j)
           (≅⇒<∷ (≅-sym (kd-[≃] k-kd b≃⌞nf-b⌟∈j))) ⟩
      ⌞ nf (nfCtx Γ) a ↓⌜·⌝ nf (nfCtx Γ) b ⌟
    ∎
    where
      open ≃-Reasoning

      a≃⌞nf-a⌟∈Πjk = Tp∈-≃-⌞⌟-nf a∈Πjk
      ⌞nf-a⌟∈Πjk   = proj₂ (≃-valid a≃⌞nf-a⌟∈Πjk)

      b≃⌞nf-b⌟∈j = Tp∈-≃-⌞⌟-nf b∈j
      ⌞nf-b⌟∈j   = proj₂ (≃-valid b≃⌞nf-b⌟∈j)
  Tp∈-≃-⌞⌟-nf (∈-s-i a∈b⋯c)  = ≃-s-i (Tp∈-≃-⌞⌟-nf a∈b⋯c)
  Tp∈-≃-⌞⌟-nf (∈-⇑ a∈j j<∷k) = ≃-⇑ (Tp∈-≃-⌞⌟-nf a∈j) j<∷k

  kd-≅-⌞⌟-nf : ∀ {n} {Γ : Ctx n} {k} →
               Γ ⊢ k kd → Γ ⊢ k ≅ ⌞ nfKind (nfCtx Γ) k ⌟Kd
  kd-≅-⌞⌟-nf (kd-⋯ a∈* b∈*)   = ≅-⋯ (Tp∈-≃-⌞⌟-nf a∈* ) (Tp∈-≃-⌞⌟-nf b∈*)
  kd-≅-⌞⌟-nf (kd-Π j-kd k-kd) = ≅-Π (kd-≅-⌞⌟-nf j-kd) (kd-≅-⌞⌟-nf k-kd)

  -- Well-formed ascriptions and contexts are equal to their normal
  -- forms.

  wf-≃-⌞⌟-nf : ∀ {n} {Γ : Ctx n} {a} →
               Γ ⊢ a wf → Γ ⊢ a ≃ ⌞ nfAsc (nfCtx Γ) a ⌟Asc wf
  wf-≃-⌞⌟-nf (wf-kd k-kd) = ≃wf-≅ (kd-≅-⌞⌟-nf k-kd)
  wf-≃-⌞⌟-nf (wf-tp a∈*)  = ≃wf-≃ (Tp∈-≃-⌞⌟-nf a∈*)

  ctx-≃-⌞⌟-nf : ∀ {n} {Γ : Ctx n} → Γ ctx → Γ ≃ ⌞ nfCtx Γ ⌟Ctx ctx
  ctx-≃-⌞⌟-nf []             = ≃-[]
  ctx-≃-⌞⌟-nf (a-wf ∷ Γ-ctx) = ≃-∷ (wf-≃-⌞⌟-nf a-wf) (ctx-≃-⌞⌟-nf Γ-ctx)

-- Some corollaries.

-- The domain and co-domain of universal types are equal to their
-- normal forms.
Tp∈-∀-≃-⌞⌟-nf : ∀ {n} {Γ : Ctx n} {k a} → Γ ⊢Tp Π k a ∈ * →
                Γ ⊢ k ≅ ⌞ nfKind (nfCtx Γ) k ⌟Kd ×
                  kd k ∷ Γ ⊢ a ≃ ⌞ nf (nfCtx (kd k ∷ Γ)) a ⌟ ∈ *
Tp∈-∀-≃-⌞⌟-nf ∀ka∈* with Tp∈-∀-inv ∀ka∈*
... | k-kd , a∈* = kd-≅-⌞⌟-nf k-kd , Tp∈-≃-⌞⌟-nf a∈*

-- The domain and co-domain of arrow types are equal to their normal
-- forms.
Tp∈-→-≃-⌞⌟-nf : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢Tp a ⇒ b ∈ * →
                Γ ⊢ a ≃ ⌞ nf (nfCtx Γ) a ⌟ ∈ * × Γ ⊢ b ≃ ⌞ nf (nfCtx Γ) b ⌟ ∈ *
Tp∈-→-≃-⌞⌟-nf a⇒b∈* with Tp∈-→-inv a⇒b∈*
... | a∈* , b∈* = Tp∈-≃-⌞⌟-nf a∈* , Tp∈-≃-⌞⌟-nf b∈*

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
-- Andreas, 2017-10-04, issue #2752, report and test case by nad
--
-- Problem was: instance does not distribute into mutual blocks.

open import Agda.Builtin.List
open import Agda.Builtin.Size

mutual

  data Rose (i : Size) (A : Set) : Set where
    node : List (Rose′ i A) → Rose i A

  data Rose′ (i : Size) (A : Set) : Set where
    delay : {j : Size< i} → Rose j A → Rose′ i A

record Map (F : Set → Set) : Set₁ where
  field
    map : {A B : Set} → (A → B) → F A → F B

open Map ⦃ … ⦄ public

instance

  Map-List : Map List
  Map.map Map-List = λ where
    f []       → []
    f (x ∷ xs) → f x ∷ map f xs

instance

  mutual

    Map-Rose : ∀ {i} → Map (Rose i)
    Map.map Map-Rose f (node xs) = node (map (map f) xs)

    Map-Rose′ : ∀ {i} → Map (Rose′ i)
    Map.map Map-Rose′ f (delay t) = delay (map f t)

-- Was: unresolved instance arguments.

-- Should succeed.


text:
module RecordDef where

data ⊤
  : Set
  where

  tt
    : ⊤

data ⊤'
  (x : ⊤)
  : Set
  where

  tt
    : ⊤' x

record R
  {y : ⊤}
  (y' : ⊤' y)
  : Set

record R {z} _ where

postulate

  r
    : R {tt} tt

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
------------------------------------------------------------------------
-- Extra definitions related to simultaneous substitutions
------------------------------------------------------------------------

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

module Data.Fin.Substitution.Extra where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Vec using (_∷_; map)
open import Level using (_⊔_) renaming (zero to lzero; suc to lsuc)
open import Relation.Unary using (Pred)

-- Extension of substitutions and iterated weakening.

record Extension {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  infixr 5 _/∷_

  field weaken : ∀ {n} → T n → T (suc n)  -- Weakens Ts.

  -- Iterated weakening of Ts.

  weaken⋆ : ∀ m {n} → T n → T (m + n)
  weaken⋆ zero    t = t
  weaken⋆ (suc m) t = weaken (weaken⋆ m t)

  -- Extension.
  --
  -- The extension operation t /∷ ρ takes a substitution ρ and extends
  -- it with a term t for an additional free variable.  It is a
  -- generalization of the lifting substitution ρ ↑ = var zero /∷ ρ
  -- where the term for the additional free variable may be something
  -- other than var zero.  Note that the term t must itself admit an
  -- additional free variable so that the resulting substitution t /∷
  -- ρ has an extended domain *and* codomain.  This is in contrast to
  -- t ∷ ρ where the codomain has no additional free variables.
  -- I.e. given (ρ : Sub T m n) we have
  --
  --   t  ∷ ρ : Sub T (1 + m) m         for   t : T m
  --   u /∷ ρ : Sub T (1 + m) (1 + m)   for   u : T (1 + m)

  _/∷_ : ∀ {m n} → T (suc n) → Sub T m n → Sub T (suc m) (suc n)
  t /∷ ρ = t ∷ map weaken ρ

-- A helper module for unpacking an instance of the Simple record
-- together with the extra operations from the Extension module (as if
-- Simple contained an instance of Extension).

module SimpleExt {ℓ} {T : Pred ℕ ℓ} (simple : Simple T) where
  open Simple simple public

  extension : Extension T
  extension = record { weaken = weaken }
  open Extension extension public hiding (weaken)

-- T₂-substitutions in term-like T₁

record TermLikeSubst {ℓ} (T₁ : Pred ℕ ℓ) (T₂ : ℕ → Set)
                     : Set (lsuc (ℓ ⊔ lzero)) where
  field
    app       : ∀ {T₃} → Lift T₃ T₂ → ∀ {m n} → T₁ m → Sub T₃ m n → T₁ n
    termSubst : TermSubst T₂

  open TermSubst termSubst public
    hiding (app; var; weaken; _/Var_; _/_; _/✶_)

  termApplication : Application T₁ T₂
  termApplication = record { _/_ = app termLift }

  varApplication : Application T₁ Fin
  varApplication = record { _/_ = app varLift }

  open Application termApplication public using (_/_; _/✶_)
  open Application varApplication  public using () renaming (_/_ to _/Var_)

  -- Weakening of T₁s.

  weaken : ∀ {n} → T₁ n → T₁ (suc n)
  weaken t = t /Var VarSubst.wk

max_stars_repo_name: sstucki/f-omega-int-agda

max_issues_repo_name: sstucki/f-omega-int-agda

max_forks_repo_name: sstucki/f-omega-int-agda


text:
module Prelude.Float where

open import Prelude.String

postulate
  Float : Set
  floatToString : Float  -> String
  stringToFloat : String -> Float

{-# BUILTIN FLOAT Float #-}
{-# COMPILED_EPIC floatToString (f : Float) -> String = frString(floatToStr(f)) #-}
{-# COMPILED_EPIC stringToFloat (s : Any) -> Float = strToFloat(mkString(s)) #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
module List.Order.Simple {A : Set}(_≤_ : A → A → Set) where

open import Data.List

data _*≤_ : List A → A → Set where
  lenx : {x : A}
                   → [] *≤ x
  lecx : {x y : A}{ys : List A}
                   → y ≤ x
                   → ys *≤ x
                   → (y ∷ ys) *≤ x

data _≤*_ : A → List A → Set where
  genx : {x : A}
                   → x ≤* []
  gecx : {x y : A}{ys : List A}
                   → x ≤ y
                   → x ≤* ys
                   → x ≤* (y ∷ ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --rewriting --confluence-check --double-check #-}

data _==_ {A : Set} : (x y : A) → Set where
  refl : {a : A} → a == a
{-# BUILTIN REWRITE _==_ #-}

postulate
  copy : ∀ {X : Set} → X → X
  A : Set
  a : A
  uip : (p : a == a) → p == refl

record S : Set where
  field
    x : A
    x-β : x == a
open S

module T (s : S) where
  dummy = x-β (copy s)
  {-# REWRITE dummy #-}

  y-β-is-refl : x-β (copy s) == refl
  y-β-is-refl = uip _ -- WAS: Double check complains about solution to meta.


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

module Definition.Typed.EqRelInstance where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Reduction
open import Definition.Typed.EqualityRelation

open import Tools.Function

-- Judgmental instance of the equality relation

instance eqRelInstance : EqRelSet
eqRelInstance = record {
  _⊢_≅_ = _⊢_≡_;
  _⊢_≅_∷_ = _⊢_≡_∷_;
  _⊢_~_∷_ = _⊢_≡_∷_;
  ~-to-≅ₜ = idᶠ;
  ≅-eq = idᶠ;
  ≅ₜ-eq = idᶠ;
  ≅-univ = univ;
  ≅-sym = sym;
  ≅ₜ-sym = sym;
  ~-sym = sym;
  ≅-trans = trans;
  ≅ₜ-trans = trans;
  ~-trans = trans;
  ≅-conv = conv;
  ~-conv = conv;
  ≅-wk = wkEq;
  ≅ₜ-wk = wkEqTerm;
  ~-wk = wkEqTerm;
  ≅-red = reduction;
  ≅ₜ-red = reductionₜ;
  ≅-Urefl = refl ∘ᶠ Uⱼ;
  ≅-ℕrefl = refl ∘ᶠ ℕⱼ;
  ≅ₜ-ℕrefl = refl ∘ᶠ ℕⱼ;
  ≅-Emptyrefl = refl ∘ᶠ Emptyⱼ;
  ≅ₜ-Emptyrefl = refl ∘ᶠ Emptyⱼ;
  ≅-Unitrefl = refl ∘ᶠ Unitⱼ;
  ≅ₜ-Unitrefl = refl ∘ᶠ Unitⱼ;
  ≅ₜ-η-unit = η-unit;
  ≅-Π-cong = Π-cong;
  ≅ₜ-Π-cong = Π-cong;
  ≅-Σ-cong = Σ-cong;
  ≅ₜ-Σ-cong = Σ-cong;
  ≅ₜ-zerorefl = refl ∘ᶠ zeroⱼ;
  ≅-suc-cong = suc-cong;
  ≅-η-eq = λ x x₁ x₂ x₃ x₄ x₅ → η-eq x x₁ x₂ x₅;
  ≅-Σ-η = λ ⊢F ⊢G ⊢p ⊢r pProd rProd fst≡ snd≡ → Σ-η ⊢F ⊢G ⊢p ⊢r fst≡ snd≡;
  ~-var = refl;
  ~-app = app-cong;
  ~-fst = fst-cong;
  ~-snd = snd-cong;
  ~-natrec = natrec-cong;
  ~-Emptyrec = Emptyrec-cong }


text:
-- A minor variant of code reported by Andreas Abel. The code below
-- should be rejected.

open import Agda.Builtin.Size

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  size : (j : Size< i) → SizeLt i

data D {i : Size} : SizeLt i → Set where
  c : ∀{i' : Size< i} → ((j : SizeLt i') → D j) → D (size i')

f : D (size ∞) → ⊥
f (c h) = f (h (size ∞))

d : ∀{i} s → D {i} s
d (size i) = c λ{ (size j) → d (size j) }

loop : ⊥
loop = f (d (size ∞))


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.Hash
open import Util.KVMap
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open EpochConfig

-- This module defines an abstract system state (represented by a value of type
-- 'IntermediateSystemState') for a given concrete state.  The culminaton of this
-- module is the 'intSystemState' "function" at the bottom, which is probably the
-- best place to start understanding this.  Longer term, we will also need
-- higher-level, cross-epoch properties.

open import Yasm.Base
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

module LibraBFT.Concrete.System where

 module PerEpoch (𝓔 : EpochConfig) where
   open WithEC
   open import LibraBFT.Abstract.Abstract     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs hiding (qcVotes; Vote)
   open import LibraBFT.Concrete.Intermediate                   𝓔 (ConcreteVoteEvidence 𝓔)
   open import LibraBFT.Concrete.Records as LCR
   open LCR.WithEC 𝓔

   module PerState (st : SystemState) where

     -- * Auxiliary definitions;
     -- Here we capture the idea that there exists a vote message that
     -- witnesses the existence of a given Abs.Vote
     record ∃VoteMsgFor (v : Abs.Vote) : Set where
       constructor mk∃VoteMsgFor
       field
         -- A message that was actually sent
         nm            : NetworkMsg
         cv            : Vote
         cv∈nm         : cv ⊂Msg nm
         -- And contained a valid vote that, once abstracted, yeilds v.
         vmsgMember    : EpochConfig.Member 𝓔
         vmsgSigned    : WithVerSig (getPubKey 𝓔 vmsgMember) cv
         vmsg≈v        : α-ValidVote 𝓔 cv vmsgMember ≡ v
         vmsgEpoch     : cv ^∙ vEpoch ≡ epoch 𝓔
     open ∃VoteMsgFor public

     record ∃VoteMsgSentFor (sm : SentMessages)(v : Abs.Vote) : Set where
       constructor mk∃VoteMsgSentFor
       field
         vmFor        : ∃VoteMsgFor v
         vmSender     : NodeId
         nmSentByAuth : (vmSender , (nm vmFor)) ∈ sm
     open ∃VoteMsgSentFor public

     ∈QC⇒sent : ∀{st : SystemState} {q α}
              → Abs.Q q α-Sent (msgPool st)
              → Meta-Honest-Member α
              → (vα : α Abs.∈QC q)
              → ∃VoteMsgSentFor (msgPool st) (Abs.∈QC-Vote q vα)
     ∈QC⇒sent vsent@(ws {sender} {nm} e≡ nm∈st (qc∈NM {cqc} .{nm} valid cqc∈nm)) ha va
       with All-reduce⁻ {vdq = Any-lookup va} (α-Vote cqc valid) All-self
                        (Any-lookup-correctP va)
     ...| as , as∈cqc , α≡
       with  α-Vote-evidence cqc valid  as∈cqc | inspect
            (α-Vote-evidence cqc valid) as∈cqc
     ...| ev | [ refl ]
        with vote∈qc {vs = as} as∈cqc refl cqc∈nm
     ...| v∈nm = mk∃VoteMsgSentFor
                   (mk∃VoteMsgFor nm (_cveVote ev) v∈nm
                                  (_ivvMember (_cveIsValidVote ev))
                                  (_ivvSigned (_cveIsValidVote ev)) (sym α≡)
                                  (_ivvEpoch  (_cveIsValidVote ev)))
                   sender
                   nm∈st

     -- Finally, we can define the abstract system state corresponding to the concrete state st
     intSystemState : IntermediateSystemState ℓ0
     intSystemState = record
       { InSys           = λ { r → r α-Sent (msgPool st) }
       ; HasBeenSent     = λ { v → ∃VoteMsgSentFor (msgPool st) v }
       ; ∈QC⇒HasBeenSent = ∈QC⇒sent {st = st}
       }

   module InSys (siah : SystemInitAndHandlers ℓ-RoundManager ConcSysParms) where
     open WithInitAndHandlers siah
     open All-InSys-props

     stable : ∀ {st0 st1 : SystemState} → Step st0 st1 → {r : Abs.Record}
              → IntermediateSystemState.InSys (PerState.intSystemState st0) r
              → IntermediateSystemState.InSys (PerState.intSystemState st1) r
     stable theStep (_α-Sent_.ws refl x₁ x₂) = _α-Sent_.ws refl (msgs-stable theStep x₁) x₂

     ais-stable : ∀ {st0 st1 : SystemState} → Step st0 st1 → {o r : Abs.Record} → (rc : RecordChainFrom o r)
                  → All-InSys (IntermediateSystemState.InSys (PerState.intSystemState st0)) rc
                  → All-InSys (IntermediateSystemState.InSys (PerState.intSystemState st1)) rc
     ais-stable theStep rc ais = λ x → stable theStep (ais x)


text:
------------------------------------------------------------------------
-- Empty type (in Set₁)
------------------------------------------------------------------------

module Data.Empty1 where

data ⊥₁ : Set₁ where

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module erase where

open import syntax-util
open import lib
open import cedille-types
open import general-util
open import constants
open import is-free

{-# TERMINATING #-}
erase : { ed : exprd } → ⟦ ed ⟧ → ⟦ ed ⟧
erase-term : term → term
erase-type : type → type
erase-kind : kind → kind
erase-lterms : term → lterms → term
erase-tk : tk → tk
erase-liftingType : liftingType → liftingType
erase-cases : cases → cases
erase-case : case → case
erase-caseArgs : caseArgs → caseArgs
erase-term-args : args → 𝕃 term

erase-if : 𝔹 → { ed : exprd } → ⟦ ed ⟧ → ⟦ ed ⟧
erase-if tt = erase
erase-if ff = id

erase-term (Parens _ t _) = erase-term t
erase-term (App t1 Erased t2) = erase-term t1
erase-term (App t1 NotErased t2) = App (erase-term t1) NotErased (erase-term t2)
erase-term (AppTp t tp) = erase-term t
erase-term (Lam _ Erased _ _ _ t) = erase-term t
erase-term (Lam _ NotErased _ x oc t) = Lam posinfo-gen NotErased posinfo-gen x NoClass (erase-term t)
erase-term (Let _ NotErased (DefTerm _ x _ t) t') =
  let body = erase-term t'
  in if is-free-in skip-erased x t'
     then Let posinfo-gen ff (DefTerm posinfo-gen x NoType (erase-term t)) body
     -- if x does not occur in an unerase position in t', then the binding is irrelevant in the erasure
     else body
erase-term (Let _ Erased (DefTerm _ x _ t) t') = erase-term t'
erase-term (Let _ _ (DefType _ _ _ _) t) = erase-term t
erase-term (Open _ _ _ _ t) = erase-term t
erase-term (Var _ x) = Var posinfo-gen x
erase-term (Beta _ _ NoTerm) = id-term
erase-term (Beta _ _ (SomeTerm t _)) = erase-term t
erase-term (IotaPair _ t1 t2 _ _) = erase-term t1
erase-term (IotaProj t n _) = erase-term t
erase-term (Epsilon _ lr _ t) = erase-term t
erase-term (Sigma _ t) = erase-term t
erase-term (Hole pi) = Hole pi -- Retain position, so jumping to hole works
erase-term (Phi _ t t₁ t₂ _) = erase-term t₂
erase-term (Rho _ _ _ t _ t') = erase-term t'
erase-term (Chi _ T t') = erase-term t'
erase-term (Delta _ T t) = id-term
erase-term (Theta _ u t ls) = erase-lterms (erase-term t) ls
erase-term (Mu _ _ x t ot _ c _) = Mu posinfo-gen posinfo-gen x (erase-term t) NoType posinfo-gen (erase-cases c) posinfo-gen
erase-term (Mu' _ _ t _ _ c _)  = Mu' posinfo-gen NoTerm (erase-term t) NoType posinfo-gen (erase-cases c) posinfo-gen

erase-cases = map erase-case

erase-case (Case _ x as t) = Case posinfo-gen x (erase-caseArgs as) (erase-term t)

erase-caseArgs [] = []
erase-caseArgs ((CaseTermArg pi NotErased t) :: as) = CaseTermArg posinfo-gen NotErased t :: erase-caseArgs as
erase-caseArgs (_ :: as) = erase-caseArgs as

erase-term-args [] = []
erase-term-args (TermArg NotErased t :: as) = erase t :: erase-term-args as
erase-term-args (_ :: as) = erase-term-args as

-- Only erases TERMS in types, leaving the structure of types the same
erase-type (Abs _ b _ v atk tp) = Abs posinfo-gen b posinfo-gen v (erase-tk atk) (erase-type tp)
erase-type (Iota _ _ v otp tp) = Iota posinfo-gen posinfo-gen v (erase-type otp) (erase-type tp)
erase-type (Lft _ _ v t lt) = Lft posinfo-gen posinfo-gen v (erase-term t) (erase-liftingType lt)
erase-type (NoSpans tp _) = NoSpans (erase-type tp) posinfo-gen
erase-type (TpApp tp tp') = TpApp (erase-type tp) (erase-type tp')
erase-type (TpAppt tp t) = TpAppt (erase-type tp) (erase-term t)
erase-type (TpArrow tp at tp') = TpArrow (erase-type tp) at (erase-type tp')
erase-type (TpEq _ t t' _) = TpEq posinfo-gen (erase-term t) (erase-term t') posinfo-gen
erase-type (TpLambda _ _ v atk tp) = TpLambda posinfo-gen posinfo-gen v (erase-tk atk) (erase-type tp)
erase-type (TpParens _ tp _) = erase-type tp
erase-type (TpHole pi) = TpHole pi -- Retain position, so jumping to hole works
erase-type (TpVar _ x) = TpVar posinfo-gen x
erase-type (TpLet _ (DefTerm _ x _ t) T) = TpLet posinfo-gen (DefTerm posinfo-gen x NoType (erase-term t)) (erase-type T)
erase-type (TpLet _ (DefType _ x k T) T') = TpLet posinfo-gen (DefType posinfo-gen x (erase-kind k) (erase-type T)) (erase-type T')

-- Only erases TERMS in types in kinds, leaving the structure of kinds and types in those kinds the same
erase-kind (KndArrow k k') = KndArrow (erase-kind k) (erase-kind k')
erase-kind (KndParens _ k _) = erase-kind k
erase-kind (KndPi _ _ v atk k) = KndPi posinfo-gen posinfo-gen v (erase-tk atk) (erase-kind k)
erase-kind (KndTpArrow tp k) = KndTpArrow (erase-type tp) (erase-kind k)
erase-kind (KndVar _ x ps) = KndVar posinfo-gen x ps
erase-kind (Star _) = Star posinfo-gen

erase{TERM} t = erase-term t
erase{TYPE} tp = erase-type tp
erase{KIND} k = erase-kind k
erase{LIFTINGTYPE} lt = erase-liftingType lt
erase{TK} atk = erase-tk atk
erase{ARG} a = a
erase{QUALIF} q = q

erase-tk (Tkt tp) = Tkt (erase-type tp)
erase-tk (Tkk k) = Tkk (erase-kind k)

erase-liftingType (LiftArrow lt lt') = LiftArrow (erase-liftingType lt) (erase-liftingType lt')
erase-liftingType (LiftParens _ lt _) = erase-liftingType lt
erase-liftingType (LiftPi _ v tp lt) = LiftPi posinfo-gen v (erase-type tp) (erase-liftingType lt)
erase-liftingType (LiftTpArrow tp lt) = LiftTpArrow (erase-type tp) (erase-liftingType lt)
erase-liftingType lt = lt

erase-lterms t [] = t
erase-lterms t ((Lterm Erased t') :: ls) = erase-lterms t ls
erase-lterms t ((Lterm NotErased t') :: ls) = erase-lterms (App t NotErased (erase-term t')) ls

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
{-# OPTIONS --allow-unsolved-metas #-}
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CS410 2017/18 Exercise 1  VECTORS AND FRIENDS (worth 25%)
------------------------------------------------------------------------------
------------------------------------------------------------------------------

-- NOTE (19/9/17) This file is currently incomplete: more will arrive on
-- GitHub.

-- MARK SCHEME (transcribed from paper): the (m) numbers add up to slightly
-- more than 25, so should be taken as the maximum number of marks losable on
-- the exercise. In fact, I did mark it negatively, but mostly because it was
-- done so well (with Agda's help) that it was easier to find the errors.

------------------------------------------------------------------------------
-- Dependencies
------------------------------------------------------------------------------

open import CS410-Prelude

------------------------------------------------------------------------------
-- Vectors
------------------------------------------------------------------------------

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_   -- the "cons" operator associates to the right

-- I like to use the asymmetric ,- to remind myself that the element is to
-- the left and the rest of the list is to the right.

-- Vectors are useful when there are important length-related safety
-- properties.

------------------------------------------------------------------------------
-- Heads and Tails
------------------------------------------------------------------------------

-- We can rule out nasty head and tail errors by insisting on nonemptiness!

--??--1.1-(2)-----------------------------------------------------------------

vHead : {X : Set}{n : Nat} -> Vec X (suc n) -> X
vHead (x ,- xs) = x

vTail : {X : Set}{n : Nat} -> Vec X (suc n) -> Vec X n
vTail (x ,- xs) = xs

vHeadTailFact :  {X : Set}{n : Nat}(xs : Vec X (suc n)) ->
                 (vHead xs ,- vTail xs) == xs
vHeadTailFact (x ,- xs) = refl (x ,- xs)

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Concatenation and its Inverse
------------------------------------------------------------------------------

--??--1.2-(2)-----------------------------------------------------------------

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V ys = ys
(x ,- xs) +V ys = x ,- xs +V ys
infixr 4 _+V_

vChop : {X : Set}(m : Nat){n : Nat} -> Vec X (m +N n) -> Vec X m * Vec X n
vChop zero xs = [] , xs
vChop (suc m) (x ,- xs) with vChop m xs
vChop (suc m) (x ,- xs) | fst₁ , snd₁ = (x ,- fst₁) , snd₁

vChopAppendFact : {X : Set}{m n : Nat}(xs : Vec X m)(ys : Vec X n) ->
                  vChop m (xs +V ys) == (xs , ys)
vChopAppendFact [] ys = refl ([] , ys)
vChopAppendFact (x ,- xs) ys rewrite vChopAppendFact xs ys = refl ((x ,- xs) , ys)

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Map, take I
------------------------------------------------------------------------------

-- Implement the higher-order function that takes an operation on
-- elements and does it to each element of a vector. Use recursion
-- on the vector.
-- Note that the type tells you the size remains the same.

-- Show that if the elementwise function "does nothing", neither does
-- its vMap. "map of identity is identity"

-- Show that two vMaps in a row can be collapsed to just one, or
-- "composition of maps is map of compositions"

--??--1.3-(2)-----------------------------------------------------------------

vMap : {X Y : Set} -> (X -> Y) -> {n : Nat} -> Vec X n -> Vec Y n
vMap f [] = []
vMap f (x ,- xs) = f x ,- vMap f xs

vMapIdFact : {X : Set}{f : X -> X}(feq : (x : X) -> f x == x) ->
             {n : Nat}(xs : Vec X n) -> vMap f xs == xs
vMapIdFact feq [] = refl []
vMapIdFact feq (x ,- xs) rewrite feq x | vMapIdFact feq xs = refl (x ,- xs)

vMapCpFact : (X Y Z : Set)(f : Y -> Z)(g : X -> Y)(h : X -> Z)
               (heq : (x : X) -> f (g x) == h x) ->
             {n : Nat}(xs : Vec X n) ->
               vMap f (vMap g xs) == vMap h xs
vMapCpFact _ _ _ _ _ _ heq [] = refl []
vMapCpFact X Y Z f g h heq (x ,- xs) rewrite heq x | vMapCpFact X Y Z f g h heq xs = refl (h x ,- vMap h xs)

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- vMap and +V
------------------------------------------------------------------------------

-- Show that if you've got two vectors of Xs and a function from X to Y,
-- and you want to concatenate and map, it doesn't matter which you do
-- first.

--??--1.4-(1)-----------------------------------------------------------------

vMap+VFact : {X Y : Set}(f : X -> Y) ->
             {m n : Nat}(xs : Vec X m)(xs' : Vec X n) ->
             vMap f (xs +V xs') == (vMap f xs +V vMap f xs')
vMap+VFact f [] xs' = refl (vMap f xs')
vMap+VFact f (x ,- xs) xs' rewrite vMap+VFact f xs xs' = refl _

--??--------------------------------------------------------------------------

-- Think about what you could prove, relating vMap with vHead, vTail, vChop...
-- Now google "Philip Wadler" "Theorems for Free"

------------------------------------------------------------------------------
-- Applicative Structure (giving mapping and zipping cheaply)
------------------------------------------------------------------------------

--??--1.5-(2)-----------------------------------------------------------------

-- HINT: you will need to override the default invisibility of n to do this.
vPure : {X : Set} -> X -> {n : Nat} -> Vec X n
vPure x {zero} = []
vPure x {suc n} = x ,- vPure x

_$V_ : {X Y : Set}{n : Nat} -> Vec (X -> Y) n -> Vec X n -> Vec Y n
[] $V [] = []
x ,- fs $V x₁ ,- xs = x x₁ ,- (fs $V xs)
infixl 3 _$V_  -- "Application associates to the left,
               --  rather as we all did in the sixties." (Roger Hindley)

-- Pattern matching and recursion are forbidden for the next two tasks.

-- implement vMap again, but as a one-liner
vec : {X Y : Set} -> (X -> Y) -> {n : Nat} -> Vec X n -> Vec Y n
vec f xs = vPure f $V xs

-- implement the operation which pairs up corresponding elements
vZip : {X Y : Set}{n : Nat} -> Vec X n -> Vec Y n -> Vec (X * Y) n
vZip [] [] = []
vZip (x ,- xs) (x₁ ,- ys) = (x , x₁) ,- vZip xs ys

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Applicative Laws
------------------------------------------------------------------------------

-- According to "Applicative programming with effects" by
--   Conor McBride and Ross Paterson
-- some laws should hold for applicative functors.
-- Check that this is the case.

--??--1.6-(2)-----------------------------------------------------------------

vIdentity : {X : Set}{f : X -> X}(feq : (x : X) -> f x == x) ->
            {n : Nat}(xs : Vec X n) -> (vPure f $V xs) == xs
vIdentity feq [] = refl []
vIdentity feq (x ,- xs) rewrite feq x | vIdentity feq xs = refl (x ,- xs)

vHomomorphism : {X Y : Set}(f : X -> Y)(x : X) ->
                {n : Nat} -> (vPure f $V vPure x) == vPure (f x) {n}
vHomomorphism f x {zero} = refl []
vHomomorphism f x {suc n} rewrite vHomomorphism f x {n} = refl (f x ,- vPure (f x))

vInterchange : {X Y : Set}{n : Nat}(fs : Vec (X -> Y) n)(x : X) ->
               (fs $V vPure x) == (vPure (_$ x) $V fs)
vInterchange [] x = refl []
vInterchange (x₁ ,- fs) x rewrite vInterchange fs x = refl _

vComposition : {X Y Z : Set}{n : Nat}
               (fs : Vec (Y -> Z) n)(gs : Vec (X -> Y) n)(xs : Vec X n) ->
               (vPure _<<_ $V fs $V gs $V xs) == (fs $V (gs $V xs))
vComposition [] [] [] = refl []
vComposition (x₁ ,- fs) (x₂ ,- gs) (x ,- xs) rewrite vComposition fs gs xs = refl _

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Order-Preserving Embeddings (also known in the business as "thinnings")
------------------------------------------------------------------------------

-- What have these to do with Pascal's Triangle?

data _<=_ : Nat -> Nat -> Set where
  oz :                          zero  <= zero
  os : {n m : Nat} -> n <= m -> suc n <= suc m
  o' : {n m : Nat} -> n <= m ->     n <= suc m

-- Find all the values in each of the following <= types.
-- This is a good opportunity to learn to use C-c C-a with the -l option
--   (a.k.a. "google the type" without "I feel lucky")
-- The -s n option also helps.

--??--1.7-(1)-----------------------------------------------------------------

all0<=4 : Vec (0 <= 4) 3
all0<=4 = o' (o' (o' (o' oz))) ,- o' (o' (o' (o' oz))) ,- o' (o' (o' (o' oz))) ,- []

all1<=4 : Vec (1 <= 4) 2
all1<=4 = os (o' (o' (o' oz))) ,- os (o' (o' (o' oz))) ,- []

all2<=4 : Vec (2 <= 4) _
all2<=4 = os (o' (o' (os oz))) ,- os (os (o' (o' oz))) ,- []

all3<=4 : Vec (3 <= 4) zero
all3<=4 = []

all4<=4 : Vec (4 <= 4) zero
all4<=4 = []

-- Prove the following. A massive case analysis "rant" is fine.

no5<=4 : 5 <= 4 -> Zero
no5<=4 (os (os (os (os ()))))
no5<=4 (os (os (os (o' ()))))
no5<=4 (os (os (o' (os ()))))
no5<=4 (os (os (o' (o' ()))))
no5<=4 (os (o' (os (os ()))))
no5<=4 (os (o' (os (o' ()))))
no5<=4 (os (o' (o' (os ()))))
no5<=4 (os (o' (o' (o' ()))))
no5<=4 (o' (os (os (os ()))))
no5<=4 (o' (os (os (o' ()))))
no5<=4 (o' (os (o' (os ()))))
no5<=4 (o' (os (o' (o' ()))))
no5<=4 (o' (o' (os (os ()))))
no5<=4 (o' (o' (os (o' ()))))
no5<=4 (o' (o' (o' (os ()))))
no5<=4 (o' (o' (o' (o' ()))))

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Order-Preserving Embeddings Select From Vectors
------------------------------------------------------------------------------

-- Use n <= m to encode the choice of n elements from an m-Vector.
-- The os constructor tells you to take the next element of the vector;
-- the o' constructor tells you to omit the next element of the vector.

--??--1.8-(2)-----------------------------------------------------------------

_<?=_ : {X : Set}{n m : Nat} -> n <= m -> Vec X m
                     -> Vec X n
oz <?= [] = []
os th <?= (x ,- xs) = x ,- (th <?= xs)
o' th <?= (x ,- xs) = th <?= xs

-- it shouldn't matter whether you map then select or select then map

vMap<?=Fact : {X Y : Set}(f : X -> Y)
              {n m : Nat}(th : n <= m)(xs : Vec X m) ->
              vMap f (th <?= xs) == (th <?= vMap f xs)
vMap<?=Fact f oz [] = refl []
vMap<?=Fact f (os th) (x ,- xs) rewrite vMap<?=Fact f th xs = refl _
vMap<?=Fact f (o' th) (x ,- xs) = vMap<?=Fact f th xs

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Our Favourite Thinnings
------------------------------------------------------------------------------

-- Construct the identity thinning and the empty thinning.

--??--1.9-(1)-----------------------------------------------------------------

oi : {n : Nat} -> n <= n
oi {zero} = oz
oi {suc n} = os oi

oe : {n : Nat} -> 0 <= n
oe {zero} = oz
oe {suc n} = o' oe

--??--------------------------------------------------------------------------

-- Show that all empty thinnings are equal to yours.

--??--1.10-(1)----------------------------------------------------------------

oeUnique : {n : Nat}(th : 0 <= n) -> th == oe
oeUnique oz = refl oz
oeUnique (o' i) rewrite oeUnique i = refl (o' oe)

--??--------------------------------------------------------------------------

-- Show that there are no thinnings of form big <= small  (TRICKY)
-- Then show that all the identity thinnings are equal to yours.
-- Note that you can try the second even if you haven't finished the first.
-- HINT: you WILL need to expose the invisible numbers.
-- HINT: check CS410-Prelude for a reminder of >=

--??--1.11-(3)----------------------------------------------------------------

thinMore : {n m : Nat} -> suc n <= m -> n <= m
thinMore (os n<=m) = o' n<=m
thinMore (o' n<=m) = o' (thinMore n<=m)

oTooBig : {n m : Nat} -> n >= m -> suc n <= m -> Zero
oTooBig {zero} {.(suc _)} n>=m (os th) = n>=m
oTooBig {zero} {.(suc _)} n>=m (o' th) = n>=m
oTooBig {suc n} {.(suc _)} n>=m (os th) = oTooBig n>=m th
oTooBig {suc n} {.(suc _)} n>=m (o' th) = oTooBig n>=m (thinMore th)

oiUnique : {n : Nat}(th : n <= n) -> th == oi
oiUnique oz = refl oz
oiUnique (os th) rewrite oiUnique th = refl (os oi)
oiUnique {m} (o' th) with oTooBig (refl->= m) th
oiUnique {.(suc _)} (o' th) | ()

--??--------------------------------------------------------------------------

-- Show that the identity thinning selects the whole vector

--??--1.12-(1)----------------------------------------------------------------

id-<?= : {X : Set}{n : Nat}(xs : Vec X n) -> (oi <?= xs) == xs
id-<?= [] = refl []
id-<?= (x ,- xs) rewrite id-<?= xs = refl (x ,- xs)

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Composition of Thinnings
------------------------------------------------------------------------------

-- Define the composition of thinnings and show that selecting by a
-- composite thinning is like selecting then selecting again.
-- A small bonus applies to minimizing the length of the proof.
-- To collect the bonus, you will need to think carefully about
-- how to make the composition as *lazy* as possible.

--??--1.13-(3)----------------------------------------------------------------

_o>>_ : {p n m : Nat} -> p <= n -> n <= m -> p <= m
th o>> oz = th
os th o>> os th' = os (th o>> th')
o' th o>> os th' = o' (th o>> th')
th o>> o' th' = o' (th o>> th')

cp-<?= : {p n m : Nat}(th : p <= n)(th' : n <= m) ->
         {X : Set}(xs : Vec X m) ->
         ((th o>> th') <?= xs) == (th <?= (th' <?= xs))
cp-<?= th oz [] = refl (th <?= [])
cp-<?= oz (o' th') (x ,- xs) = cp-<?= oz th' xs
cp-<?= (os th) (os th') (x ,- xs) rewrite cp-<?= th th' xs = refl (x ,- (th <?= (th' <?= xs)))
cp-<?= (os th) (o' th') (x ,- xs) = cp-<?= (os th) th' xs
cp-<?= (o' th) (os th') (x ,- xs) = cp-<?= th th' xs
cp-<?= (o' th) (o' th') (x ,- xs) = cp-<?= (o' th) th' xs

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Thinning Dominoes
------------------------------------------------------------------------------

--??--1.14-(3)----------------------------------------------------------------

idThen-o>> : {n m : Nat}(th : n <= m) -> (oi o>> th) == th
idThen-o>> oz = refl oz
idThen-o>> (os th) rewrite idThen-o>> th = refl (os th)
idThen-o>> (o' th) rewrite idThen-o>> th = refl (o' th)

idAfter-o>> : {n m : Nat}(th : n <= m) -> (th o>> oi) == th
idAfter-o>> oz = refl oz
idAfter-o>> (os th) rewrite idAfter-o>> th = refl (os th)
idAfter-o>> (o' th) rewrite idAfter-o>> th = refl (o' th)

assoc-o>> : {q p n m : Nat}(th0 : q <= p)(th1 : p <= n)(th2 : n <= m) ->
            ((th0 o>> th1) o>> th2) == (th0 o>> (th1 o>> th2))
assoc-o>> th0 th1 oz = refl (th0 o>> th1)
assoc-o>> th0 (o' th1) (os th2) rewrite assoc-o>> th0 th1 th2 = refl (o' (th0 o>> (th1 o>> th2)))
assoc-o>> (os th0) (os th1) (os th2) rewrite assoc-o>> th0 th1 th2 = refl (os (th0 o>> (th1 o>> th2)))
assoc-o>> (o' th0) (os th1) (os th2) rewrite assoc-o>> th0 th1 th2 = refl (o' (th0 o>> (th1 o>> th2)))
assoc-o>> th0 th1 (o' th2) rewrite assoc-o>> th0 th1 th2 = refl (o' (th0 o>> (th1 o>> th2)))

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Vectors as Arrays
------------------------------------------------------------------------------

-- We can use 1 <= n as the type of bounded indices into a vector and do
-- a kind of "array projection". First we select a 1-element vector from
-- the n-element vector, then we take its head to get the element out.

vProject : {n : Nat}{X : Set} -> Vec X n -> 1 <= n -> X
vProject xs i = vHead (i <?= xs)

-- Your (TRICKY) mission is to reverse the process, tabulating a function
-- from indices as a vector. Then show that these operations are inverses.

--??--1.15-(3)----------------------------------------------------------------

selectHead : (n : Nat) -> 1 <= (suc n)
selectHead n = os oe

-- HINT: composition of functions
vTabulate : {n : Nat}{X : Set} -> (1 <= n -> X) -> Vec X n
vTabulate {zero} f = []
vTabulate {suc n} f = (f (selectHead n)) ,- (vTabulate (\p -> f (o' p)))

-- This should be easy if vTabulate is correct.
vTabulateProjections : {n : Nat}{X : Set}(xs : Vec X n) ->
                       vTabulate (vProject xs) == xs
vTabulateProjections [] = refl []
vTabulateProjections (x ,- xs) rewrite vTabulateProjections xs = refl (x ,- xs)

-- HINT: oeUnique
vProjectFromTable : {n : Nat}{X : Set}(f : 1 <= n -> X)(i : 1 <= n) ->
                    vProject (vTabulate f) i == f i
vProjectFromTable {.(suc _)} {X} f (os i) with oeUnique i
vProjectFromTable {.(suc _)} {X} f (os .oe) | refl .oe = refl (f (os oe))
vProjectFromTable {.(suc _)} {X} f (o' i) = vProjectFromTable (λ z → f (o' z)) i

--??--------------------------------------------------------------------------


text:
------------------------------------------------------------------------
-- A general grammar and pretty-printer for binary operators of
-- various (not necessarily linearly ordered) precedences
------------------------------------------------------------------------

-- The code below uses a variant of the operator grammars described by
-- Ulf Norell and me in "Parsing Mixfix Operators". For simplicity the
-- code only handles binary infix operators.

{-# OPTIONS --guardedness #-}

module Examples.Precedence where

open import Codata.Musical.Notation
open import Data.Bool using (Bool; T)
import Data.Bool.Properties as Bool-prop
open import Data.Char as Char using (Char; _==_)
open import Data.Fin using (Fin; zero; suc; #_)
open import Data.Fin.Properties as Fin using () renaming (_≟_ to _≟F_)
open import Data.List as List
open import Data.List.Membership.Propositional
open import Data.List.NonEmpty as List⁺
import Data.List.Properties as List
open import Data.List.Relation.Unary.Any as Any
open import Data.Nat using (ℕ)
open import Data.Product as Prod
import Data.String as String
open import Data.Unit
import Data.Vec as Vec
open import Data.Vec.Membership.Propositional.Properties
open import Function using (id; _∘_; _∘′_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable as Decidable
open import Relation.Nullary.Product

open import Examples.Identifier
open import Grammar.Infinite as Grammar using (Grammar-for)
open import Pretty using (Pretty-printer-for)
open import Renderer
open import Utilities

------------------------------------------------------------------------
-- Binary operators

-- Associativities.

data Associativity : Set where
  -   -- Non-associative.
   ⇾  -- Right associative.
   ⇽  -- Left associative.
     : Associativity

-- Operator names.

is-operator-char : Char → Bool
is-operator-char t =
  List.any (_==_ t) (String.toList "+-*/.:^<>=!&|")

Operator-name : Set
Operator-name = List⁺ (∃ (T ∘ is-operator-char))

-- Operators (parametrised by their associativity).

record Operator (assoc : Associativity) : Set where
  constructor ⟪_⟫
  field name : Operator-name

-- Equality of operators can be decided.

_≟O_ : ∀ {assoc} → Decidable (_≡_ {A = Operator assoc})
⟪ n₁ ∷ ns₁ ⟫ ≟O ⟪ n₂ ∷ ns₂ ⟫ =
  Decidable.map′
    (P.cong ⟪_⟫ ∘ uncurry (P.cong₂ _∷_))
    (< P.cong List⁺.head , P.cong List⁺.tail > ∘′ P.cong Operator.name)
    ((n₁ ≟OC n₂)
       ×-dec
     List.≡-dec _≟OC_ ns₁ ns₂)
  where
  _≟OC_ : Decidable (_≡_ {A = ∃ (T ∘ is-operator-char)})
  (c₁ , _) ≟OC (c₂ , _) =
    Decidable.map′ lemma (P.cong proj₁) (c₁ Char.≟ c₂)
    where
    lemma : {p₁ p₂ : ∃ (T ∘ is-operator-char)} →
            proj₁ p₁ ≡ proj₁ p₂ → p₁ ≡ p₂
    lemma {p₁ = _ , _} {p₂ = ._ , _} P.refl =
      P.cong -,_ (Bool-prop.T-irrelevant _ _)

-- A grammar for a given operator name.

operator-name : Grammar-for Operator-name
operator-name n = list⁺ (tok-sat _) n
  where open Grammar

-- A pretty-printer for operator names.

operator-name-printer : Pretty-printer-for operator-name
operator-name-printer n = list⁺ tok-sat n
  where open Pretty

-- A grammar for a given operator.

operator : ∀ {assoc} → Grammar-for (Operator assoc)
operator op =
  Prod.map ⟪_⟫ (P.cong ⟪_⟫) <$> operator-name (Operator.name op)
  where open Grammar

-- A pretty-printer for operators.

operator-printer : ∀ {assoc} →
                   Pretty-printer-for (operator {assoc = assoc})
operator-printer op = <$> operator-name-printer (Operator.name op)
  where open Pretty

------------------------------------------------------------------------
-- Precedence graphs

-- Precedence graphs are represented by the number of precedence
-- levels, plus functions mapping node identifiers (precedences) to
-- node contents and successor precedences.

record Precedence-graph : Set where
  field

    -- The number of precedence levels.

    levels : ℕ

  -- Precedence levels.

  Precedence : Set
  Precedence = Fin levels

  field

    -- The precedence level's operators.

    ops : Precedence → (assoc : Associativity) → List (Operator assoc)

    -- The immediate successors of the precedence level.

    ↑ : Precedence → List Precedence

  -- All precedence levels.

  all-precedences : List Precedence
  all-precedences = Vec.toList (Vec.allFin levels)

  -- Every precedence level is a member of all-precedences.

  ∈-all-precedences : ∀ {p} → p ∈ all-precedences
  ∈-all-precedences {p} = ∈-toList⁺ (∈-allFin⁺ p)

  -- A membership test for precedences.

  _∈?_ : ∀ (p : Precedence) ps → Dec (p ∈ ps)
  p ∈? ps = Any.any? (_≟F_ p) ps

------------------------------------------------------------------------
-- Expressions

-- The code is parametrised by a precedence graph.

module Expr (g : Precedence-graph) where

  open Precedence-graph g

  -- Operators with a given precedence and associativity.

  Op : Precedence → Associativity → Set
  Op p assoc = ∃ λ op → op ∈ ops p assoc

  mutual

    -- Expressions.

    data Expr : Set where
      var : Identifier → Expr
      app : ∀ {p} → ∃ (App p) → Expr

    -- Binary operator applications where the operator has a given
    -- precedence and associativity.

    App : Precedence → Associativity → Set
    App p assoc = Expr × Op p assoc × Expr

  -- The following function can be convenient to use when constructing
  -- examples.

  _⟨_⟩_ :
    ∀ {assoc} → Expr → (op : Operator assoc) →
    {member : True (Fin.any? λ p →
                      Any.any? (_≟O_ op) (ops p assoc))} →
    Expr → Expr
  _⟨_⟩_ e₁ op {member} e₂ =
    app (_ , e₁ , (op , proj₂ (toWitness member)) , e₂)

  module _ where

    open Grammar

    mutual

      -- Expression grammar.

      expr : Grammar Expr
      expr = whitespace ⋆ ⊛> precs all-precedences <⊛ whitespace ⋆

      -- Grammar for a given list of precedence levels.

      precs : List Precedence → Grammar Expr
      precs ps = string′ "(" ⊛> ♯ expr <⊛ string′ ")"
               ∣ var <$> identifier
               ∣ precs′ ps

      precs′ : List Precedence → Grammar Expr
      precs′ []       = fail
      precs′ (p ∷ ps) = app <$> ♯ prec p
                      ∣ precs′ ps

      -- Grammar for a given precedence level.

      prec : (p : Precedence) → Grammar (∃ (App p))
      prec p = -,_ <$> non-assoc p
             ∣ -,_ <$> right⁺ p
             ∣ -,_ <$> left⁺ p

      -- Grammar for higher precedence levels.

      higher : Precedence → Grammar Expr
      higher p = precs (↑ p)

      -- Non-associative operators.

      non-assoc : (p : Precedence) → Grammar (App p -)
      non-assoc p = (λ e₁ op e₂ → e₁ , op , e₂) <$>
        higher p ⊛ operators (ops p -) ⊛ higher p

      -- Right-associative operators.

      right⁺ : (p : Precedence) → Grammar (App p ⇾)
      right⁺ p = (λ e₁ op e₂ → e₁ , op , e₂) <$>
        higher p ⊛ operators (ops p ⇾) ⊛ right⁺↑ p

      right⁺↑ : Precedence → Grammar Expr
      right⁺↑ p = (app ∘ -,_) <$> ♯ right⁺ p
                ∣ higher p

      -- Left-associative operators.

      left⁺ : (p : Precedence) → Grammar (App p ⇽)
      left⁺ p = (λ e₁ op e₂ → e₁ , op , e₂) <$>
        left⁺↑ p ⊛ operators (ops p ⇽) ⊛ higher p

      left⁺↑ : Precedence → Grammar Expr
      left⁺↑ p = (app ∘ -,_) <$> ♯ left⁺ p
               ∣ higher p

      -- An operator from a given list of operators.

      operators : ∀ {assoc} (os : List (Operator assoc)) →
                  Grammar (∃ λ op → op ∈ os)
      operators []         = fail
      operators (op ∷ ops) =    whitespace ⋆
                             ⊛> (Prod.map id here <$> operator op)
                             <⊛ whitespace ⋆
                           ∣ Prod.map id there <$> operators ops

  open Pretty

  mutual

    -- Pretty-printer. The produced layout could probably be improved,
    -- I have not tried very hard to make it pretty.

    expr-printer : Pretty-printer expr
    expr-printer e = nil-⋆ ⊛> precs-printer e <⊛ nil-⋆

    precs-printer : ∀ {ps} → Pretty-printer (precs ps)
    precs-printer e = group (precs-printer′ e)
      where
      precs-printer′ : ∀ {ps} → Pretty-printer (precs ps)
      precs-printer′ (var x) = left (right (<$> identifier-printer x))
      precs-printer′ {ps} (app {p = p} e)
        with p ∈? ps
      ... | yes p∈ps = right (precs′-printer p∈ps e)
      ... | no  _    =
        -- Incorrect precedence level: insert parentheses.
        left (left (text ⊛> nest 1 d <⊛ text))
        where
        d = nil-⋆                                       ⊛>
            right (precs′-printer ∈-all-precedences e) <⊛
            nil-⋆

    precs′-printer :
      ∀ {p ps} → p ∈ ps → (e : ∃ (App p)) → Doc (precs′ ps) (app e)
    precs′-printer (here P.refl) e = left  (<$> prec-printer e)
    precs′-printer (there p∈ps)  e = right (precs′-printer p∈ps e)

    prec-printer : ∀ {p} → Pretty-printer (prec p)
    prec-printer (- , e) = left (left (<$> non-assoc-printer e))
    prec-printer (⇾ , e) = left (right (<$> right⁺-printer e))
    prec-printer (⇽ , e) = right (<$> left⁺-printer e)

    non-assoc-printer : ∀ {p} → Pretty-printer (non-assoc p)
    non-assoc-printer (e₁ , op , e₂) =
      <$> higher-printer e₁ ⊛ operators-printer op ⊛ higher-printer e₂

    right⁺-printer : ∀ {p} → Pretty-printer (right⁺ p)
    right⁺-printer (e₁ , op , e₂) =
      <$> higher-printer e₁ ⊛ operators-printer op ⊛ right⁺↑-printer e₂

    right⁺↑-printer : ∀ {p} → Pretty-printer (right⁺↑ p)
    right⁺↑-printer {p₁} (app {p = p₂} (⇾ , e))
      with p₁ ≟F p₂ | higher-printer (app (⇾ , e))
    right⁺↑-printer (app (⇾ , e)) | yes P.refl | _ =
      -- Matching precedence and associativity.
      left (<$> right⁺-printer e)
    right⁺↑-printer (app (⇾ , e)) | no _ | d = right d
    right⁺↑-printer e = right (higher-printer e)

    left⁺-printer : ∀ {p} → Pretty-printer (left⁺ p)
    left⁺-printer (e₁ , op , e₂) =
      <$> left⁺↑-printer e₁ ⊛ operators-printer op ⊛ higher-printer e₂

    left⁺↑-printer : ∀ {p} → Pretty-printer (left⁺↑ p)
    left⁺↑-printer {p₁} (app {p = p₂} (⇽ , e))
      with p₁ ≟F p₂ | higher-printer (app (⇽ , e))
    left⁺↑-printer (app (⇽ , e)) | yes P.refl | _ =
      -- Matching precedence and associativity.
      left (<$> left⁺-printer e)
    left⁺↑-printer (app (⇽ , e)) | no _ | d = right d
    left⁺↑-printer e = right (higher-printer e)

    higher-printer : ∀ {p} → Pretty-printer (higher p)
    higher-printer e = nest 2 (precs-printer e)

    operators-printer : ∀ {assoc} {os : List (Operator assoc)} →
                        Pretty-printer (operators os)
    operators-printer {os = []}     (_  , ())
    operators-printer {os = ._ ∷ _} (op , here P.refl) =
      left (line⋆ tt-⊛> <$> operator-printer op <⊛ space)
    operators-printer {os =  _ ∷ _} (_  , there op∈os) =
      right (<$> operators-printer (_ , op∈os))

------------------------------------------------------------------------
-- An example

-- Some operators.

add : Operator ⇽
add = ⟪ str⁺ "+" ⟫

sub : Operator ⇽
sub = ⟪ str⁺ "-" ⟫

mul : Operator ⇽
mul = ⟪ str⁺ "*" ⟫

div : Operator ⇽
div = ⟪ str⁺ "/" ⟫

cons : Operator ⇾
cons = ⟪ str⁺ "<:" ⟫

snoc : Operator ⇽
snoc = ⟪ str⁺ ":>" ⟫

-- A precedence graph.

g : Precedence-graph
g = record { ops = ops; ↑ = ↑ }
  where
  ops : Fin 3 → (assoc : Associativity) → List (Operator assoc)
  ops zero             ⇽ = snoc ∷ []
  ops zero             ⇾ = cons ∷ []
  ops (suc zero)       ⇽ = add ∷ sub ∷ []
  ops (suc (suc zero)) ⇽ = mul ∷ div ∷ []
  ops _                _ = []

  ↑ : Fin 3 → List (Fin 3)
  ↑ zero          = # 1 ∷ # 2 ∷ []
  ↑ (suc zero)    = # 2 ∷ []
  ↑ (suc (suc p)) = []

open Precedence-graph g
open Expr g

-- An expression.

example : Expr
example =
  (((var (str⁺ "y") ⟨ add ⟩ var (str⁺ "k"))
      ⟨ cons ⟩
    (((var (str⁺ "i") ⟨ add ⟩ var (str⁺ "foo"))
        ⟨ add ⟩
      ((var (str⁺ "a")
          ⟨ div ⟩
        (var (str⁺ "b") ⟨ sub ⟩ var (str⁺ "c")))
         ⟨ mul ⟩
       var (str⁺ "c")))
       ⟨ cons ⟩
     (var (str⁺ "xs"))))
     ⟨ snoc ⟩
   (var (str⁺ "x")))
    ⟨ snoc ⟩
  (var (str⁺ "z") ⟨ mul ⟩ var (str⁺ "z"))

-- Some unit tests.

test₁ : render 80 (expr-printer example) ≡
        "(y + k <: i + foo + a / (b - c) * c <: xs) :> x :> z * z"
test₁ = P.refl

test₂ : render 50 (expr-printer example) ≡
        "(y + k <: i + foo + a / (b - c) * c <: xs)\n:> x\n:> z * z"
test₂ = P.refl

test₃ : render 40 (expr-printer example) ≡
        "(y + k\n   <: i + foo + a / (b - c) * c\n   <: xs)\n:> x\n:> z * z"
test₃ = P.refl

test₄ : render 30 (expr-printer example) ≡
        "(y + k\n   <: i\n     + foo\n     + a / (b - c) * c\n   <: xs)\n:> x\n:> z * z"
test₄ = P.refl

test₅ : render 20 (expr-printer example) ≡
        "(y + k\n   <: i\n     + foo\n     + a\n       / (b - c)\n       * c\n   <: xs)\n:> x\n:> z * z"
test₅ = P.refl

test₆ : render 6 (expr-printer example) ≡
        "(y + k\n   <: i\n     + foo\n     + a\n       / (b\n          - c)\n       * c\n   <: xs)\n:> x\n:> z\n  * z"
test₆ = P.refl

-- The rendering of "y + k" in the following test may seem strange: if
-- no newline had been inserted before +, then the total width of this
-- subexpression would have been smaller.
--
-- Wadler's pretty-printing algorithm is not always optimal for texts
-- that do not fit in the allotted width, if by "optimal" we mean
-- "with as little overflow as possible". To see what I mean, try
-- running the following Haskell code, where the functions are
-- implemented as in Wadler's paper:
--
--   pretty 1 (group (nest 20 (line <> text "x")))
--
-- The result is "\n                    x", which can be seen as much
-- worse than the alternative result " x". However, note that Wadler
-- uses a lexicographic definition of "better", in which
-- "\n                    x" is better than " x", because the first
-- line of "\n                    x" fits, but the first line of " x"
-- doesn't.

test₇ : render 5 (expr-printer example) ≡
        "(y\n     + k\n   <: i\n     + foo\n     + a\n       / (b\n          - c)\n       * c\n   <: xs)\n:> x\n:> z\n  * z"
test₇ = P.refl

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
module sets.fin.core where

open import decidable
open import equality.core
open import sets.empty
open import sets.unit public
open import sets.nat.core
  hiding (_≟_; pred)
open import sets.empty

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} → Fin n → Fin (suc n)

raise : ∀ {n} → Fin n → Fin (suc n)
raise zero = zero
raise (suc i) = suc (raise i)

fin-disj : ∀ {n}(i : Fin n) → ¬ (zero ≡ suc i)
fin-disj {n} i = J' P tt (suc i)
  where
    P : (i : Fin (suc n)) → zero ≡ i → Set
    P zero _ = ⊤
    P (suc _) _ = ⊥

fin-suc-inj : ∀ {n} {i j : Fin n} → Fin.suc i ≡ suc j → i ≡ j
fin-suc-inj {n}{i}{j} = J' P refl (suc j)
  where
    P : (j : Fin (suc n)) → Fin.suc i ≡ j → Set
    P zero _ = ⊤
    P (suc j) _ = i ≡ j

_≟_ : ∀ {n} → (i j : Fin n) → Dec (i ≡ j)
_≟_ zero zero = yes refl
_≟_ zero (suc i) = no (fin-disj i)
_≟_ (suc i) zero = no (λ p → fin-disj i (sym p))
_≟_ {suc n} (suc i) (suc j) with i ≟ j
... | yes p = yes (ap suc p)
... | no a = no (λ p → a (fin-suc-inj p))

last-fin : {n : ℕ} → Fin (suc n)
last-fin {zero} = zero
last-fin {suc n} = suc last-fin

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
open import Agda.Primitive.Cubical

data BadData : IUniv where

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda