text:
{-
  Day 2, 2nd part
-}
module a2b where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String; primShowNat; primStringAppend)
open import Agda.Builtin.Equality

open import Data.Nat
open import Data.Bool using (if_then_else_)
open import Data.List
open import Data.Maybe renaming (map to maybeMap)

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

-- helper
shopMaybeNat : Maybe ℕ → String
shopMaybeNat (just n) = primShowNat n
shopMaybeNat nothing = "nothing"

data Command : Set where
  forward : ℕ → Command
  up      : ℕ → Command
  down    : ℕ → Command

record Position : Set where
  constructor pos
  field
    h : ℕ
    d : ℕ

{- Alignment of the submarine, i.e. position and aim -}
record Alignment : Set where
  constructor state
  field
    h : ℕ
    d : ℕ
    aim : ℕ

open Position

apply : Command → Alignment → Maybe Alignment

apply (forward x) (state h d aim) = just (state (h + x) (d + (x * aim)) aim)

apply (up x)      (state h d aim) = if aim <ᵇ x
                                    then nothing
                                    else just (state h d ∣ aim - x ∣)

apply (down x) (state h d aim) = just (state h d (aim + x))

iterate : List Command → Alignment → Maybe Alignment
iterate [] a = just a
iterate (command ∷ list) a with apply command a
...                           | just a'  = iterate list a'
...                           | nothing = nothing

doTask : List Command → Maybe ℕ
doTask list = let maybeResult = iterate list (state 0 0 0)
              in maybeMap multiplyComponents maybeResult
  where multiplyComponents : Alignment → ℕ
        multiplyComponents (state h d aim) = h * d

input : List Command
input =
  forward 2 ∷
  forward 3 ∷
  forward 5 ∷
  forward 6 ∷
  down 7 ∷
  forward 8 ∷
  forward 4 ∷
  forward 7 ∷
  forward 5 ∷
  forward 5 ∷
  down 4 ∷
  down 9 ∷
  forward 8 ∷
  forward 5 ∷
  up 5 ∷
  down 5 ∷
  forward 3 ∷
  down 4 ∷
  down 8 ∷
  forward 9 ∷
  down 1 ∷
  up 9 ∷
  down 7 ∷
  up 7 ∷
  up 1 ∷
  forward 1 ∷
  down 1 ∷
  down 4 ∷
  down 4 ∷
  down 8 ∷
  down 4 ∷
  up 3 ∷
  down 1 ∷
  down 3 ∷
  forward 7 ∷
  down 6 ∷
  forward 3 ∷
  forward 5 ∷
  forward 2 ∷
  up 9 ∷
  forward 7 ∷
  up 5 ∷
  down 3 ∷
  forward 1 ∷
  forward 2 ∷
  down 3 ∷
  down 8 ∷
  down 3 ∷
  forward 8 ∷
  up 5 ∷
  down 5 ∷
  forward 3 ∷
  down 5 ∷
  forward 9 ∷
  down 3 ∷
  down 4 ∷
  down 9 ∷
  down 7 ∷
  up 3 ∷
  down 9 ∷
  up 9 ∷
  up 1 ∷
  forward 3 ∷
  up 4 ∷
  down 3 ∷
  forward 7 ∷
  forward 7 ∷
  up 7 ∷
  forward 6 ∷
  down 7 ∷
  down 6 ∷
  forward 2 ∷
  forward 9 ∷
  down 5 ∷
  forward 4 ∷
  up 6 ∷
  down 1 ∷
  down 9 ∷
  down 9 ∷
  forward 4 ∷
  down 1 ∷
  forward 6 ∷
  down 1 ∷
  down 5 ∷
  down 4 ∷
  down 4 ∷
  forward 4 ∷
  forward 9 ∷
  up 1 ∷
  down 2 ∷
  down 8 ∷
  down 5 ∷
  down 8 ∷
  down 8 ∷
  up 2 ∷
  forward 8 ∷
  up 1 ∷
  forward 4 ∷
  down 5 ∷
  down 1 ∷
  up 2 ∷
  forward 6 ∷
  forward 9 ∷
  forward 2 ∷
  forward 6 ∷
  forward 9 ∷
  up 6 ∷
  forward 9 ∷
  up 4 ∷
  down 7 ∷
  up 6 ∷
  forward 2 ∷
  down 1 ∷
  up 3 ∷
  forward 1 ∷
  forward 8 ∷
  down 6 ∷
  down 8 ∷
  down 8 ∷
  forward 8 ∷
  forward 2 ∷
  forward 2 ∷
  down 2 ∷
  up 1 ∷
  down 9 ∷
  up 9 ∷
  down 9 ∷
  up 3 ∷
  forward 9 ∷
  up 4 ∷
  up 7 ∷
  up 6 ∷
  down 9 ∷
  forward 1 ∷
  down 3 ∷
  down 4 ∷
  forward 8 ∷
  down 3 ∷
  down 9 ∷
  up 3 ∷
  forward 2 ∷
  up 5 ∷
  down 3 ∷
  forward 8 ∷
  up 3 ∷
  down 3 ∷
  forward 2 ∷
  forward 9 ∷
  down 1 ∷
  down 9 ∷
  down 4 ∷
  up 7 ∷
  down 4 ∷
  up 6 ∷
  forward 5 ∷
  down 6 ∷
  forward 3 ∷
  down 2 ∷
  forward 1 ∷
  forward 8 ∷
  down 4 ∷
  forward 1 ∷
  up 7 ∷
  forward 6 ∷
  up 9 ∷
  forward 6 ∷
  down 3 ∷
  forward 2 ∷
  down 4 ∷
  forward 6 ∷
  down 3 ∷
  down 6 ∷
  down 1 ∷
  down 1 ∷
  down 5 ∷
  forward 3 ∷
  forward 9 ∷
  forward 8 ∷
  down 3 ∷
  forward 7 ∷
  up 9 ∷
  forward 9 ∷
  up 2 ∷
  forward 4 ∷
  up 3 ∷
  forward 1 ∷
  up 6 ∷
  up 8 ∷
  down 5 ∷
  down 6 ∷
  up 9 ∷
  down 6 ∷
  down 9 ∷
  up 9 ∷
  down 4 ∷
  forward 5 ∷
  up 2 ∷
  down 3 ∷
  up 3 ∷
  down 1 ∷
  forward 3 ∷
  down 5 ∷
  forward 7 ∷
  down 6 ∷
  down 7 ∷
  down 5 ∷
  forward 2 ∷
  up 6 ∷
  down 9 ∷
  down 4 ∷
  down 3 ∷
  forward 9 ∷
  up 8 ∷
  forward 2 ∷
  down 2 ∷
  forward 4 ∷
  up 6 ∷
  down 4 ∷
  up 8 ∷
  down 7 ∷
  down 2 ∷
  up 6 ∷
  up 4 ∷
  down 2 ∷
  forward 5 ∷
  up 4 ∷
  down 8 ∷
  forward 3 ∷
  forward 1 ∷
  down 7 ∷
  forward 8 ∷
  forward 7 ∷
  down 7 ∷
  up 4 ∷
  forward 8 ∷
  down 5 ∷
  up 9 ∷
  forward 1 ∷
  forward 4 ∷
  forward 9 ∷
  forward 7 ∷
  down 9 ∷
  up 9 ∷
  down 1 ∷
  down 7 ∷
  forward 7 ∷
  down 7 ∷
  down 7 ∷
  down 3 ∷
  down 5 ∷
  forward 3 ∷
  down 2 ∷
  forward 6 ∷
  down 9 ∷
  up 5 ∷
  up 3 ∷
  forward 5 ∷
  down 6 ∷
  down 1 ∷
  forward 4 ∷
  down 3 ∷
  forward 8 ∷
  down 7 ∷
  forward 7 ∷
  forward 7 ∷
  up 7 ∷
  up 2 ∷
  up 3 ∷
  forward 9 ∷
  down 5 ∷
  up 2 ∷
  forward 5 ∷
  up 5 ∷
  forward 2 ∷
  forward 2 ∷
  down 8 ∷
  forward 2 ∷
  up 4 ∷
  forward 1 ∷
  forward 3 ∷
  up 8 ∷
  up 9 ∷
  forward 5 ∷
  down 1 ∷
  up 8 ∷
  down 4 ∷
  down 8 ∷
  up 4 ∷
  forward 9 ∷
  down 6 ∷
  down 8 ∷
  up 2 ∷
  up 3 ∷
  down 7 ∷
  down 4 ∷
  forward 5 ∷
  down 6 ∷
  forward 3 ∷
  forward 3 ∷
  forward 8 ∷
  down 1 ∷
  down 7 ∷
  down 9 ∷
  down 2 ∷
  down 7 ∷
  forward 7 ∷
  down 7 ∷
  down 6 ∷
  up 6 ∷
  forward 8 ∷
  forward 5 ∷
  up 5 ∷
  down 2 ∷
  up 8 ∷
  up 4 ∷
  down 9 ∷
  up 2 ∷
  forward 5 ∷
  up 2 ∷
  down 4 ∷
  up 4 ∷
  forward 2 ∷
  forward 4 ∷
  forward 9 ∷
  forward 9 ∷
  up 4 ∷
  up 5 ∷
  down 1 ∷
  down 6 ∷
  down 1 ∷
  down 4 ∷
  down 5 ∷
  down 3 ∷
  forward 3 ∷
  down 9 ∷
  forward 6 ∷
  down 3 ∷
  down 9 ∷
  down 2 ∷
  up 2 ∷
  down 2 ∷
  down 7 ∷
  forward 9 ∷
  down 3 ∷
  down 3 ∷
  down 2 ∷
  down 3 ∷
  forward 2 ∷
  down 9 ∷
  down 9 ∷
  up 5 ∷
  up 3 ∷
  forward 4 ∷
  up 7 ∷
  forward 8 ∷
  up 6 ∷
  forward 7 ∷
  down 7 ∷
  down 1 ∷
  forward 5 ∷
  down 2 ∷
  up 1 ∷
  down 8 ∷
  up 3 ∷
  forward 2 ∷
  up 9 ∷
  down 1 ∷
  down 3 ∷
  down 6 ∷
  down 2 ∷
  down 7 ∷
  up 2 ∷
  forward 5 ∷
  forward 7 ∷
  down 2 ∷
  forward 5 ∷
  forward 4 ∷
  forward 5 ∷
  down 3 ∷
  forward 7 ∷
  down 7 ∷
  forward 8 ∷
  down 3 ∷
  down 2 ∷
  up 1 ∷
  forward 6 ∷
  down 4 ∷
  down 2 ∷
  forward 7 ∷
  up 3 ∷
  down 4 ∷
  forward 2 ∷
  up 6 ∷
  down 3 ∷
  up 6 ∷
  up 8 ∷
  down 9 ∷
  up 6 ∷
  forward 8 ∷
  forward 9 ∷
  forward 4 ∷
  forward 7 ∷
  down 2 ∷
  forward 9 ∷
  down 7 ∷
  up 9 ∷
  down 5 ∷
  down 6 ∷
  up 5 ∷
  down 4 ∷
  forward 8 ∷
  forward 4 ∷
  forward 4 ∷
  down 6 ∷
  forward 3 ∷
  forward 6 ∷
  down 9 ∷
  down 9 ∷
  up 2 ∷
  forward 7 ∷
  down 8 ∷
  down 9 ∷
  down 9 ∷
  forward 7 ∷
  forward 3 ∷
  down 7 ∷
  down 8 ∷
  forward 8 ∷
  down 6 ∷
  down 5 ∷
  down 9 ∷
  down 3 ∷
  forward 1 ∷
  down 5 ∷
  forward 2 ∷
  forward 8 ∷
  down 2 ∷
  forward 6 ∷
  forward 3 ∷
  down 7 ∷
  down 4 ∷
  forward 8 ∷
  forward 1 ∷
  down 6 ∷
  forward 9 ∷
  forward 6 ∷
  up 1 ∷
  up 3 ∷
  down 8 ∷
  forward 1 ∷
  up 5 ∷
  down 4 ∷
  forward 7 ∷
  up 3 ∷
  down 2 ∷
  forward 1 ∷
  forward 9 ∷
  down 9 ∷
  down 7 ∷
  forward 8 ∷
  down 4 ∷
  up 3 ∷
  down 4 ∷
  forward 2 ∷
  forward 6 ∷
  down 7 ∷
  forward 6 ∷
  down 6 ∷
  down 4 ∷
  down 1 ∷
  up 9 ∷
  down 4 ∷
  down 7 ∷
  up 4 ∷
  down 9 ∷
  forward 6 ∷
  down 3 ∷
  forward 2 ∷
  down 4 ∷
  forward 3 ∷
  down 5 ∷
  up 9 ∷
  forward 8 ∷
  up 7 ∷
  up 6 ∷
  up 4 ∷
  forward 1 ∷
  down 1 ∷
  forward 4 ∷
  up 6 ∷
  forward 5 ∷
  forward 4 ∷
  forward 5 ∷
  up 6 ∷
  down 1 ∷
  forward 3 ∷
  up 7 ∷
  down 9 ∷
  up 9 ∷
  down 5 ∷
  forward 6 ∷
  forward 4 ∷
  up 1 ∷
  down 4 ∷
  up 1 ∷
  forward 3 ∷
  forward 1 ∷
  down 3 ∷
  forward 7 ∷
  down 2 ∷
  forward 3 ∷
  up 2 ∷
  forward 8 ∷
  down 3 ∷
  up 9 ∷
  down 5 ∷
  forward 6 ∷
  down 1 ∷
  down 8 ∷
  down 5 ∷
  forward 1 ∷
  down 6 ∷
  up 2 ∷
  forward 6 ∷
  down 2 ∷
  down 1 ∷
  up 6 ∷
  up 7 ∷
  down 5 ∷
  forward 7 ∷
  forward 6 ∷
  forward 6 ∷
  down 7 ∷
  forward 4 ∷
  down 5 ∷
  up 5 ∷
  down 1 ∷
  up 8 ∷
  down 8 ∷
  down 2 ∷
  down 2 ∷
  down 9 ∷
  up 9 ∷
  forward 2 ∷
  forward 7 ∷
  down 7 ∷
  down 4 ∷
  down 4 ∷
  down 8 ∷
  forward 5 ∷
  forward 2 ∷
  up 9 ∷
  down 9 ∷
  forward 7 ∷
  up 9 ∷
  down 2 ∷
  down 7 ∷
  up 2 ∷
  up 8 ∷
  forward 8 ∷
  down 4 ∷
  forward 3 ∷
  forward 4 ∷
  forward 6 ∷
  forward 2 ∷
  down 1 ∷
  down 2 ∷
  forward 2 ∷
  up 1 ∷
  down 1 ∷
  forward 5 ∷
  up 3 ∷
  up 3 ∷
  down 3 ∷
  down 1 ∷
  down 4 ∷
  up 5 ∷
  up 6 ∷
  forward 5 ∷
  up 7 ∷
  forward 6 ∷
  down 4 ∷
  down 7 ∷
  up 8 ∷
  forward 1 ∷
  down 5 ∷
  up 4 ∷
  up 3 ∷
  up 5 ∷
  down 1 ∷
  up 5 ∷
  forward 3 ∷
  up 5 ∷
  forward 2 ∷
  forward 2 ∷
  forward 5 ∷
  forward 2 ∷
  up 9 ∷
  forward 4 ∷
  down 1 ∷
  down 3 ∷
  down 5 ∷
  up 2 ∷
  down 8 ∷
  forward 8 ∷
  forward 9 ∷
  down 1 ∷
  down 3 ∷
  forward 8 ∷
  forward 2 ∷
  down 2 ∷
  down 1 ∷
  up 7 ∷
  forward 2 ∷
  forward 8 ∷
  down 9 ∷
  forward 1 ∷
  forward 4 ∷
  down 7 ∷
  down 4 ∷
  up 7 ∷
  down 3 ∷
  down 1 ∷
  down 4 ∷
  up 7 ∷
  down 6 ∷
  forward 7 ∷
  down 8 ∷
  up 2 ∷
  up 4 ∷
  up 6 ∷
  down 9 ∷
  down 9 ∷
  down 8 ∷
  forward 6 ∷
  up 3 ∷
  up 1 ∷
  forward 9 ∷
  forward 6 ∷
  up 4 ∷
  up 2 ∷
  up 7 ∷
  forward 5 ∷
  up 9 ∷
  up 9 ∷
  forward 9 ∷
  up 6 ∷
  down 1 ∷
  down 3 ∷
  forward 3 ∷
  down 2 ∷
  down 2 ∷
  down 6 ∷
  down 9 ∷
  forward 3 ∷
  forward 7 ∷
  up 3 ∷
  forward 3 ∷
  down 5 ∷
  forward 9 ∷
  up 6 ∷
  down 2 ∷
  forward 8 ∷
  down 3 ∷
  up 5 ∷
  down 6 ∷
  forward 9 ∷
  down 5 ∷
  down 2 ∷
  down 6 ∷
  forward 8 ∷
  forward 6 ∷
  down 1 ∷
  forward 6 ∷
  up 1 ∷
  up 7 ∷
  down 4 ∷
  down 7 ∷
  forward 4 ∷
  forward 7 ∷
  down 4 ∷
  forward 8 ∷
  down 8 ∷
  down 7 ∷
  forward 9 ∷
  down 1 ∷
  down 3 ∷
  down 6 ∷
  forward 7 ∷
  forward 6 ∷
  forward 3 ∷
  forward 8 ∷
  down 5 ∷
  down 3 ∷
  up 1 ∷
  down 9 ∷
  down 8 ∷
  forward 3 ∷
  down 6 ∷
  down 1 ∷
  forward 5 ∷
  forward 5 ∷
  forward 9 ∷
  up 5 ∷
  down 6 ∷
  up 9 ∷
  down 7 ∷
  down 6 ∷
  up 1 ∷
  forward 5 ∷
  forward 7 ∷
  forward 8 ∷
  forward 7 ∷
  forward 6 ∷
  forward 3 ∷
  forward 1 ∷
  forward 2 ∷
  up 4 ∷
  forward 3 ∷
  forward 4 ∷
  forward 5 ∷
  up 2 ∷
  up 3 ∷
  forward 4 ∷
  down 9 ∷
  up 4 ∷
  forward 7 ∷
  down 6 ∷
  down 6 ∷
  down 1 ∷
  forward 2 ∷
  down 2 ∷
  forward 2 ∷
  down 3 ∷
  forward 7 ∷
  forward 8 ∷
  down 4 ∷
  up 7 ∷
  forward 7 ∷
  down 7 ∷
  forward 7 ∷
  forward 9 ∷
  down 7 ∷
  up 2 ∷
  down 3 ∷
  forward 7 ∷
  down 1 ∷
  forward 8 ∷
  forward 2 ∷
  up 9 ∷
  down 3 ∷
  forward 2 ∷
  up 4 ∷
  forward 9 ∷
  down 4 ∷
  down 4 ∷
  forward 4 ∷
  down 2 ∷
  down 9 ∷
  forward 4 ∷
  down 2 ∷
  down 6 ∷
  forward 9 ∷
  forward 2 ∷
  up 1 ∷
  forward 2 ∷
  forward 3 ∷
  down 5 ∷
  up 8 ∷
  down 4 ∷
  down 4 ∷
  forward 7 ∷
  down 2 ∷
  up 6 ∷
  down 9 ∷
  forward 9 ∷
  up 1 ∷
  forward 3 ∷
  down 5 ∷
  forward 3 ∷
  down 3 ∷
  forward 4 ∷
  up 3 ∷
  down 6 ∷
  down 7 ∷
  down 4 ∷
  down 8 ∷
  down 4 ∷
  down 5 ∷
  up 9 ∷
  up 1 ∷
  down 7 ∷
  up 3 ∷
  up 3 ∷
  down 3 ∷
  up 4 ∷
  up 6 ∷
  forward 8 ∷
  down 1 ∷
  forward 7 ∷
  forward 4 ∷
  down 9 ∷
  down 1 ∷
  forward 7 ∷
  forward 9 ∷
  forward 1 ∷
  down 3 ∷
  down 2 ∷
  forward 3 ∷
  forward 2 ∷
  down 7 ∷
  forward 9 ∷
  forward 6 ∷
  up 9 ∷
  down 2 ∷
  forward 9 ∷
  up 6 ∷
  forward 8 ∷
  up 1 ∷
  down 5 ∷
  down 8 ∷
  forward 1 ∷
  down 1 ∷
  forward 9 ∷
  up 1 ∷
  forward 9 ∷
  forward 1 ∷
  forward 1 ∷
  down 7 ∷
  forward 3 ∷
  forward 6 ∷
  down 5 ∷
  forward 7 ∷
  forward 1 ∷
  down 7 ∷
  down 6 ∷
  down 6 ∷
  forward 5 ∷
  up 6 ∷
  down 6 ∷
  forward 8 ∷
  up 2 ∷
  down 8 ∷
  down 3 ∷
  up 5 ∷
  up 8 ∷
  down 6 ∷
  forward 4 ∷
  forward 2 ∷
  up 3 ∷
  forward 5 ∷
  forward 3 ∷
  up 8 ∷
  forward 6 ∷
  up 8 ∷
  forward 1 ∷
  up 8 ∷
  up 7 ∷
  up 6 ∷
  forward 2 ∷
  down 9 ∷
  down 9 ∷
  forward 3 ∷
  down 7 ∷
  forward 3 ∷
  down 6 ∷
  forward 9 ∷
  up 5 ∷
  down 1 ∷
  forward 7 ∷
  down 1 ∷
  down 5 ∷
  down 9 ∷
  forward 8 ∷
  forward 9 ∷
  forward 7 ∷
  down 9 ∷
  up 4 ∷
  forward 5 ∷
  down 5 ∷
  forward 5 ∷
  down 9 ∷
  forward 9 ∷
  forward 3 ∷
  up 5 ∷
  forward 8 ∷
  up 5 ∷
  down 1 ∷
  forward 8 ∷
  down 3 ∷
  forward 6 ∷
  up 9 ∷
  forward 8 ∷
  down 4 ∷
  forward 3 ∷
  down 5 ∷
  forward 8 ∷
  forward 9 ∷
  forward 2 ∷
  down 1 ∷
  down 6 ∷
  down 4 ∷
  forward 9 ∷
  up 2 ∷
  down 3 ∷
  down 6 ∷
  down 3 ∷
  down 9 ∷
  down 1 ∷
  up 6 ∷
  down 2 ∷
  down 7 ∷
  up 5 ∷
  forward 5 ∷
  up 1 ∷
  down 7 ∷
  forward 6 ∷
  up 6 ∷
  down 2 ∷
  down 3 ∷
  forward 3 ∷
  down 5 ∷
  forward 8 ∷
  down 9 ∷
  down 7 ∷
  down 8 ∷
  up 7 ∷
  down 1 ∷
  forward 1 ∷
  forward 1 ∷
  down 2 ∷
  up 4 ∷
  forward 2 ∷
  down 3 ∷
  up 2 ∷
  down 3 ∷
  down 2 ∷
  forward 7 ∷
  down 1 ∷
  up 7 ∷
  down 2 ∷
  down 1 ∷
  forward 6 ∷
  down 9 ∷
  up 9 ∷
  down 4 ∷
  down 6 ∷
  up 9 ∷
  forward 7 ∷
  forward 9 ∷
  forward 7 ∷
  down 4 ∷
  down 1 ∷
  forward 7 ∷
  down 4 ∷
  down 7 ∷
  down 3 ∷
  down 5 ∷
  forward 3 ∷
  down 8 ∷
  forward 8 ∷
  forward 7 ∷
  forward 8 ∷
  down 4 ∷
  down 9 ∷
  forward 2 ∷
  forward 7 ∷
  up 8 ∷
  forward 4 ∷
  down 6 ∷
  up 8 ∷
  down 2 ∷
  forward 3 ∷
  down 6 ∷
  down 8 ∷
  forward 8 ∷
  forward 2 ∷
  forward 9 ∷
  up 6 ∷
  forward 7 ∷
  down 3 ∷
  down 5 ∷
  forward 8 ∷
  forward 9 ∷
  down 3 ∷
  forward 3 ∷
  forward 2 ∷
  forward 3 ∷
  down 8 ∷
  up 9 ∷
  up 5 ∷
  up 2 ∷
  up 6 ∷
  up 1 ∷
  up 1 ∷
  up 5 ∷
  forward 3 ∷
  forward 2 ∷
  down 3 ∷
  forward 4 ∷
  []

main : IO ⊤
main = putStrLn (shopMaybeNat (doTask input))

private
  -- checks from the exercise text
  _ : apply (forward 5) (state 0 0 0) ≡ just (state 5 0 0)
  _ = refl

  _ : apply (down 5) (state 5 0 0) ≡ just (state 5 0 5)
  _ = refl

  _ : apply (forward 8) (state 5 0 5) ≡ just (state 13 (8 * 5) 5)
  _ = refl

  _ : apply (up 3) (state 13 40 5) ≡ just (state 13 40 2)
  _ = refl

  _ : apply (down 8) (state 13 40 2) ≡ just (state 13 40 10)
  _ = refl

  _ : apply (forward 2) (state 13 40 10) ≡ just (state 15 60 10)
  _ = refl

  -- submarine does not 'fly'
  _ : apply (up 7) (state 13 2 2) ≡ nothing
  _ = refl

max_stars_repo_name: felixwellen/adventOfCode

max_issues_repo_name: felixwellen/adventOfCode

max_forks_repo_name: felixwellen/adventOfCode


text:
module Oscar.Class.Injectivity where

open import Oscar.Level

record Injectivity {a} {A : Set a} {b} {B : Set b} {ℓ₁} (_≋₁_ : A → B → Set ℓ₁)
                   {i} {I : Set i} {ℓ₂} (_≋₂_ : I → I → Set ℓ₂)
                   (f : I → A)
                   (g : I → B)
       : Set (a ⊔ b ⊔ ℓ₁ ⊔ i ⊔ ℓ₂) where
  field
    injectivity : ∀ {x y} → f x ≋₁ g y → x ≋₂ y

open Injectivity ⦃ … ⦄ public

record Injectivityoid a b ℓ₁ i ℓ₂ : Set (lsuc (a ⊔ b ⊔ ℓ₁ ⊔ i ⊔ ℓ₂)) where
  field
    {A} : Set a
    {B} : Set b
    _≋₁_ : A → B → Set ℓ₁
    I : Set i
    _≋₂_ : I → I → Set ℓ₂
    μₗ : I → A
    μᵣ : I → B
    `injectivity : ∀ {x y} → μₗ x ≋₁ μᵣ y → x ≋₂ y

ext: agda


text:
-- {-# OPTIONS -v tc.lhs:100 #-}

module IrrelevantData where

data T (A : Set) : Set where
  c : .A → T A

d : ∀ {A} → T A → A
d (c x) = x
-- needs to fail since x is irrelevant under c

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --prop --allow-unsolved-metas #-}

{-# TERMINATING #-}
makeloop : {P : Prop} → P → P
makeloop p = makeloop p

postulate
  A : Set
  B : A → Prop

record AB : Set where
  constructor _,_
  field
    a : A
    b : B a
open AB public

id : AB → AB
id ab = a ab , makeloop (b ab)

postulate
  f : (id* : AB → AB) → A → Set

C : A → Set
C = f id

postulate
  D : (C : A → Set) (a : A) (c : C a) → Set

-- Works if you either give the type of v (C u) or the second argument of D (u)
loops : (u : A) (v : _) → D C _ v
loops = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Issue2799 where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

record Stream (A : Set) : Set where
  coinductive
  constructor _,_
  field
    head : A
    tail : Stream A

open Stream

mapS : ∀ {A B} → (A → B) → Stream A → Stream B
head (mapS f xs) = f (head xs)
tail (mapS f xs) = mapS f (tail xs)

mapS-id : ∀ {A} {xs : Stream A} → mapS (λ x → x) xs ≡ xs
head (mapS-id {xs = xs} i) = head xs
tail (mapS-id {xs = xs} i) = mapS-id {xs = tail xs} i

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module half where

open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Size

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

half : ℕ → ℕ
half zero = zero
half (suc zero) = zero
half (suc (suc i)) = suc (half i)

_ : half 5 ≡ 2
_ = refl

data ℕₛ (n : Size) : Set where
  zero : ℕₛ n
  suc : (m : Size< n) → ℕₛ m → ℕₛ n

_ : ∀ {n} → ℕₛ n
_ = zero

_ : ∀ {n} (m : Size< n) → ℕₛ m → ℕₛ n
_ = suc

halfₛ : ∀ n → ℕₛ n → ℕₛ n
halfₛ n zero = zero
halfₛ n (suc m zero) = zero
halfₛ n (suc m (suc k i)) = suc k (halfₛ k i)

max_stars_repo_name: JLimperg/msc-thesis

max_issues_repo_name: JLimperg/msc-thesis

max_forks_repo_name: JLimperg/msc-thesis


text:
module UnquoteDecl where

open import Common.Prelude
open import Common.Reflection
open import Common.Equality
open import Agda.Builtin.Sigma

infixr 3 _`⇒_
pattern _`⇒_ a b = pi (vArg a) (abs "_" b)
pattern `Nat = def (quote Nat) []

unquoteDecl x =
  define (vArg x) (funDef `Nat (clause [] [] (quoteTerm 15) ∷ []))

y = x + 4

-- unquoteDecl loop = define loop (funDef `Nat (clause [] (def (quote loop) []) ∷ []))

pattern `zero  = con (quote zero) []
pattern `suc n = con (quote suc) (vArg n ∷ [])

-- Note that in the body of the unquote, 'plus' really means 'quote plus'.
unquoteDecl plus =
  define (vArg plus) (
  funDef (`Nat `⇒ `Nat `⇒ `Nat)
         ( clause (("y" , vArg unknown) ∷ []) (vArg (con (quote zero) []) ∷ vArg (var 0) ∷ []) (var 0 [])
         ∷ clause (("y" , vArg unknown) ∷ ("x" , vArg unknown) ∷ [])
                  (vArg (con (quote suc) (vArg (var 1) ∷ [])) ∷ vArg (var 0) ∷ [])
                  (`suc (def plus (vArg (var 1 []) ∷ vArg (var 0 []) ∷ [])))
         ∷ []))

prf : plus 1 1 ≡ 2
prf = refl

magicDef : FunDef
magicDef =
  funDef (def (quote ⊥) [] `⇒ `Nat)
         (absurdClause (("()" , vArg unknown) ∷ []) (vArg absurd ∷ []) ∷ [])

unquoteDecl magic = define (vArg magic) magicDef

max_forks_repo_name: shlevy/agda


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Congruity
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Transassociativity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.IsPrecategory
open import Oscar.Class.IsCategory
open import Oscar.Class.Precategory
open import Oscar.Class.Category
open import Oscar.Data.¶
open import Oscar.Data.Descender
open import Oscar.Data.Proposequality
import Oscar.Property.Setoid.Proposequality
import Oscar.Class.Congruity.Proposequality
import Oscar.Class.Transextensionality.Proposequality
import Oscar.Data.Constraint

module Oscar.Property.Category.AListProposequality where

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

  private AList = Descender⟨ A ⟩

  instance

    𝓡eflexivityAList : Reflexivity.class AList
    𝓡eflexivityAList .⋆ = ∅

    𝓣ransitivityAList : Transitivity.class AList
    𝓣ransitivityAList .⋆ f ∅ = f
    𝓣ransitivityAList .⋆ f (x , g) =
      let _∙'_ = λ g f → 𝓣ransitivityAList .⋆ f g in -- FIXME needed to help Agda prove termination
      x , g ∙' f

    𝓣ransitivityAList' : Transitivity.class (flip AList)
    𝓣ransitivityAList' .⋆ f g = transitivity g f

    HasEquivalenceAList : ∀ {m n} → HasEquivalence (AList m n) _
    HasEquivalenceAList = ∁ Proposequality

    𝓣ransassociativityAList : Transassociativity.class AList Proposequality transitivity
    𝓣ransassociativityAList .⋆ f g ∅ = ∅
    𝓣ransassociativityAList .⋆ f g (x , h) = congruity (x ,_) $ 𝓣ransassociativityAList .⋆ _ _ h -- h ⟨∙ _ ⟨∙ _

    𝓣ransassociativityAList' : Transassociativity.class (flip AList) Proposequality transitivity
    𝓣ransassociativityAList' .⋆ f g h = symmetry (transassociativity h g f) -- Sym.[] {!!}

    IsPrecategoryAList : IsPrecategory AList Proposequality transitivity
    IsPrecategoryAList = ∁

    IsPrecategoryAList' : IsPrecategory (flip AList) Proposequality transitivity
    IsPrecategoryAList' = ∁

    𝓣ransleftidentityAList : Transleftidentity.class AList Proposequality ε transitivity
    𝓣ransleftidentityAList .⋆ = ∅

    𝓣ransrightidentityAList : Transrightidentity.class AList Proposequality ε transitivity
    𝓣ransrightidentityAList .⋆ {f = ∅} = ∅
    𝓣ransrightidentityAList .⋆ {f = x , f} rewrite 𝓣ransrightidentityAList .⋆ {f = f} = ∅
    -- 𝓣ransrightidentityAList .⋆ {f = x , f} = congruity (x ,_) (transrightidentity {_∼_ = AList} {_∼̇_ = Proposequality})
    -- 𝓣ransrightidentityAList .⋆ {f = x , f} rewrite (f ∙ ε[ AList ] ≡ f) ∋ transrightidentity {_∼_ = AList} = ∅

    𝓣ransleftidentityAList' : Transleftidentity.class (flip AList) Proposequality ε transitivity
    𝓣ransleftidentityAList' .⋆ = transrightidentity {_∼_ = AList}

    𝓣ransrightidentityAList' : Transrightidentity.class (flip AList) Proposequality ε transitivity
    𝓣ransrightidentityAList' .⋆ = transleftidentity {_∼_ = AList}

    IsCategoryAList : IsCategory AList Proposequality ε transitivity
    IsCategoryAList = ∁

    IsCategoryAList' : IsCategory (flip AList) Proposequality ε transitivity
    IsCategoryAList' = ∁

module _ {a} (A : ¶ → Ø a) where

  private AList = Descender⟨ A ⟩

  PrecategoryAListProposequality : Precategory _ _ _
  PrecategoryAListProposequality = ∁ AList Proposequality transitivity

  CategoryAListProposequality : Category _ _ _
  CategoryAListProposequality = ∁ AList Proposequality ε transitivity

  PrecategoryAList'Proposequality : Precategory _ _ _
  PrecategoryAList'Proposequality = ∁ (flip AList) Proposequality transitivity

  CategoryAList'Proposequality : Category _ _ _
  CategoryAList'Proposequality = ∁ (flip AList) Proposequality ε transitivity


text:
-- Andreas, 2017-10-06, issue #2751
-- Highlighting for unsolved constraints

module _ where

open import Agda.Builtin.Size

module UnsolvedSizeConstraints where

  mutual

    data D (i : Size) (A : Set) : Set where
      c : D′ i A → D i A

    record D′ (i : Size) (A : Set) : Set where
      inductive
      field
        size  : Size< i
        force : D size A

  open D′

  Map : (F : Set → Set) → Set₁
  Map F = {A B : Set} → F A → F B

  mutual

      map-D : ∀ {i} → Map (D i)
      map-D (c xs) = c (map-D′ xs)

      map-D′ : ∀ {i} → Map (D′ i)
      size  (map-D′ {i} t) = foo where postulate foo : {!Size< i!}
      force (map-D′ {i} t) = map-D {i = i} (force t)  -- correct is  i = foo

  -- Produces an unsolved size constraint.
  -- Problem WAS: no highlighting for unsolved constraints.
  -- Now: yellow highlighting in last rhs.

-- Test also highlighting for unsolved level constraints:

module UnsolvedLevelConstraints where

mutual
  l = _

  data D {a} (A : Set a) : Set l where
    c : A → D A  -- highlighted

  data E (A : Set l) : Set1 where
    c : A → E A  -- highlighted


text:
open import Prelude
open import Data.Vec
open import Data.List.Properties
open import Data.List.Any hiding (map)
open import Data.List.All as All using ()
open import Extensions.Vec
open import Data.Product hiding (map)

module Implicits.Resolution.Ambiguous.Semantics where

open import Implicits.Syntax
open import Implicits.Resolution.Ambiguous.Resolution
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Semantics
open import Implicits.Semantics.Lemmas

open import SystemF.Everything as F using ()

module DerivationSemantics where

  ⟦_,_⟧r : ∀ {ν n} {Δ} {Γ : Ctx ν n} {a} → Δ ⊢ᵣ a → Γ # Δ →
           ∃ λ t → ⟦ Γ ⟧ctx→ F.⊢ t ∈ ⟦ a ⟧tp→
  ⟦_,_⟧r (r-tabs {r = r} p) m with ⟦ p , #tvar m ⟧r
  ⟦_,_⟧r {Γ = Γ} (r-tabs {r = r} p) m | _ , x =
    , F.Λ (subst (λ u → u F.⊢ _ ∈ ⟦ r ⟧tp→) (⟦weaken⟧ctx→ Γ) x)
  ⟦_,_⟧r (r-tapp a p) m with ⟦ p , m ⟧r
  ⟦_,_⟧r {Γ = Γ} (r-tapp {r = a} b p) m | _ , x =
    , subst
      (λ u → ⟦ Γ ⟧ctx→ F.⊢ _ ∈ u)
      (sym $ ⟦a/sub⟧tp→ a b)
      (x F.[ ⟦ b ⟧tp→ ])
  ⟦_,_⟧r {Γ = Γ} {a = a} (r-ivar x) m with ∈⟶index (All.lookup m x)
  ⟦_,_⟧r {Γ = Γ} {a = a} (r-ivar x) m | i , lookup-i≡r =
    , subst (λ u → _ F.⊢ F.var i ∈ u) eq (F.var i)
    where
      eq = begin
        lookup i ⟦ Γ ⟧ctx→
          ≡⟨ sym $ lookup-⟦⟧ctx→ Γ i ⟩
        ⟦ lookup i Γ ⟧tp→
            ≡⟨ cong ⟦_⟧tp→ lookup-i≡r ⟩
        ⟦ a ⟧tp→ ∎
  ⟦_,_⟧r (r-iabs {a = a} p) m = , F.λ' ⟦ a ⟧tp→ (proj₂ ⟦ p , #ivar a m ⟧r)
  ⟦_,_⟧r (r-iapp p p₁) m = , (proj₂ ⟦ p , m ⟧r) F.· (proj₂ ⟦ p₁ , m ⟧r)

open Semantics _⊢ᵣ_ DerivationSemantics.⟦_,_⟧r public


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Gentzen-style formalisation of labelled syntax, after Basin-Matthews-Viganò.

module BasicIS4.Syntax.LabelledGentzen where

open import BasicIS4.Syntax.Common public

-- Labels, as in Gabbay’s labelled deductive systems.

postulate
  Label : Set

-- Label pairs, or relational access tokens.
-- x ↝ y means the world labelled y is accessible from the world labelled x.

infix 6 _↝_
record Token : Set where
  constructor _↝_
  field
    x : Label
    y : Label

-- Labelled types.
-- A ◎ x means the type A is inhabited at the world labelled x.

infix 6 _◎_
record LabelledTy : Set where
  constructor _◎_
  field
    A : Ty
    x : Label

infix 6 _◎⋆_
_◎⋆_ : Cx Ty → Label → Cx LabelledTy
∅       ◎⋆ x = ∅
(Ξ , A) ◎⋆ x = Ξ ◎⋆ x , A ◎ x

-- Derivations.

infix 3 _⊢ᴿ_
data _⊢ᴿ_ (Λ : Cx Token) : Token → Set where
  rvar   : ∀ {x y}   → x ↝ y ∈ Λ → Λ ⊢ᴿ x ↝ y
  rrefl  : ∀ {x}     → Λ ⊢ᴿ x ↝ x
  rtrans : ∀ {x y z} → Λ ⊢ᴿ x ↝ y → Λ ⊢ᴿ y ↝ z → Λ ⊢ᴿ x ↝ z

infix 3 _⊢_
data _⊢_ : Cx² Ty Token → LabelledTy → Set where
  var  : ∀ {x A Γ Λ}   → A ∈ Γ → Γ ⁏ Λ ⊢ A ◎ x
  lam  : ∀ {x A B Γ Λ} → Γ , A ⁏ Λ ⊢ B ◎ x → Γ ⁏ Λ ⊢ A ▻ B ◎ x
  app  : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ▻ B ◎ x → Γ ⁏ Λ ⊢ A ◎ x → Γ ⁏ Λ ⊢ B ◎ x
  scan : ∀ {x A Γ Λ}   → (∀ {y} → Γ ⁏ Λ , x ↝ y ⊢ A ◎ y) → Γ ⁏ Λ ⊢ □ A ◎ x
  move : ∀ {x y A Γ Λ} → Γ ⁏ Λ ⊢ □ A ◎ x → Λ ⊢ᴿ x ↝ y → Γ ⁏ Λ ⊢ A ◎ y
  pair : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ◎ x → Γ ⁏ Λ ⊢ B ◎ x → Γ ⁏ Λ ⊢ A ∧ B ◎ x
  fst  : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ∧ B ◎ x → Γ ⁏ Λ ⊢ A ◎ x
  snd  : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ∧ B ◎ x → Γ ⁏ Λ ⊢ B ◎ x
  unit : ∀ {x Γ Λ}     → Γ ⁏ Λ ⊢ ⊤ ◎ x

infix 3 _⊢⋆_
_⊢⋆_ : Cx² Ty Token → Cx LabelledTy → Set
Γ ⁏ Λ ⊢⋆ ∅     = 𝟙
Γ ⁏ Λ ⊢⋆ Ξ , A = Γ ⁏ Λ ⊢⋆ Ξ × Γ ⁏ Λ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {x A Γ Γ′ Λ} → Γ ⊆ Γ′ → Γ ⁏ Λ ⊢ A ◎ x → Γ′ ⁏ Λ ⊢ A ◎ x
mono⊢ η (var i)    = var (mono∈ η i)
mono⊢ η (lam t)    = lam (mono⊢ (keep η) t)
mono⊢ η (app t u)  = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η (scan t)   = scan (mono⊢ η t)
mono⊢ η (move t u) = move (mono⊢ η t) u
mono⊢ η (pair t u) = pair (mono⊢ η t) (mono⊢ η u)
mono⊢ η (fst t)    = fst (mono⊢ η t)
mono⊢ η (snd t)    = snd (mono⊢ η t)
mono⊢ η unit       = unit

mono⊢⋆ : ∀ {Ξ x Γ Γ′ Λ} → Γ ⊆ Γ′ → Γ ⁏ Λ ⊢⋆ Ξ ◎⋆ x → Γ′ ⁏ Λ ⊢⋆ Ξ ◎⋆ x
mono⊢⋆ {∅}     η ∙        = ∙
mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Monotonicity with respect to relational context inclusion.

rmono⊢ᴿ : ∀ {x y Λ Λ′} → Λ ⊆ Λ′ → Λ ⊢ᴿ x ↝ y → Λ′ ⊢ᴿ x ↝ y
rmono⊢ᴿ ρ (rvar i)     = rvar (mono∈ ρ i)
rmono⊢ᴿ ρ rrefl        = rrefl
rmono⊢ᴿ ρ (rtrans t u) = rtrans (rmono⊢ᴿ ρ t) (rmono⊢ᴿ ρ u)

rmono⊢ : ∀ {x A Γ Λ Λ′} → Λ ⊆ Λ′ → Γ ⁏ Λ ⊢ A ◎ x → Γ ⁏ Λ′ ⊢ A ◎ x
rmono⊢ ρ (var i)    = var i
rmono⊢ ρ (lam t)    = lam (rmono⊢ ρ t)
rmono⊢ ρ (app t u)  = app (rmono⊢ ρ t) (rmono⊢ ρ u)
rmono⊢ ρ (scan t)   = scan (rmono⊢ (keep ρ) t)
rmono⊢ ρ (move t u) = move (rmono⊢ ρ t) (rmono⊢ᴿ ρ u)
rmono⊢ ρ (pair t u) = pair (rmono⊢ ρ t) (rmono⊢ ρ u)
rmono⊢ ρ (fst t)    = fst (rmono⊢ ρ t)
rmono⊢ ρ (snd t)    = snd (rmono⊢ ρ t)
rmono⊢ ρ unit       = unit

rmono⊢⋆ : ∀ {Ξ x Γ Λ Λ′} → Λ ⊆ Λ′ → Γ ⁏ Λ ⊢⋆ Ξ ◎⋆ x → Γ ⁏ Λ′ ⊢⋆ Ξ ◎⋆ x
rmono⊢⋆ {∅}     ρ ∙        = ∙
rmono⊢⋆ {Ξ , A} ρ (ts , t) = rmono⊢⋆ ρ ts , rmono⊢ ρ t

-- Monotonicity using context pairs.

mono²⊢ : ∀ {x A Π Π′} → Π ⊆² Π′ → Π ⊢ A ◎ x → Π′ ⊢ A ◎ x
mono²⊢ (η , ρ) = mono⊢ η ∘ rmono⊢ ρ

-- Shorthand for variables.

v₀ : ∀ {x A Γ Λ} → Γ , A ⁏ Λ ⊢ A ◎ x
v₀ = var i₀

v₁ : ∀ {x A B Γ Λ} → Γ , A , B ⁏ Λ ⊢ A ◎ x
v₁ = var i₁

v₂ : ∀ {x A B C Γ Λ} → Γ , A , B , C ⁏ Λ ⊢ A ◎ x
v₂ = var i₂

rv₀ : ∀ {x y Λ} → Λ , x ↝ y ⊢ᴿ x ↝ y
rv₀ = rvar i₀

rv₁ : ∀ {x y x′ y′ Λ} → Λ , x ↝ y , x′ ↝ y′ ⊢ᴿ x ↝ y
rv₁ = rvar i₁

rv₂ : ∀ {x y x′ y′ x″ y″ Λ} → Λ , x ↝ y , x′ ↝ y′ , x″ ↝ y″ ⊢ᴿ x ↝ y
rv₂ = rvar i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ x Λ} → Γ ⁏ Λ ⊢⋆ Γ ◎⋆ x
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem is built-in.

lam⋆ : ∀ {Ξ x A Γ Λ} → Γ ⧺ Ξ ⁏ Λ ⊢ A ◎ x → Γ ⁏ Λ ⊢ Ξ ▻⋯▻ A ◎ x
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ x A Λ} → Γ ⁏ Λ ⊢ A ◎ x → ∅ ⁏ Λ ⊢ Γ ▻⋯▻ A ◎ x
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Detachment theorem.

det : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ▻ B ◎ x → Γ , A ⁏ Λ ⊢ B ◎ x
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ x A Γ Λ} → Γ ⁏ Λ ⊢ Ξ ▻⋯▻ A ◎ x → Γ ⧺ Ξ ⁏ Λ ⊢ A ◎ x
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ x A Λ} → ∅ ⁏ Λ ⊢ Γ ▻⋯▻ A ◎ x → Γ ⁏ Λ ⊢ A ◎ x
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

-- Cut and multicut.

cut : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ◎ x → Γ , A ⁏ Λ ⊢ B ◎ x → Γ ⁏ Λ ⊢ B ◎ x
cut t u = app (lam u) t

multicut : ∀ {Ξ x A Γ Λ} → Γ ⁏ Λ ⊢⋆ Ξ ◎⋆ x → Ξ ⁏ Λ ⊢ A ◎ x → Γ ⁏ Λ ⊢ A ◎ x
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ x Γ′ Γ Λ} → Γ ⁏ Λ ⊢⋆ Γ′ ◎⋆ x → Γ′ ⁏ Λ ⊢⋆ Γ″ ◎⋆ x → Γ ⁏ Λ ⊢⋆ Γ″ ◎⋆ x
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

ccont : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ (A ▻ A ▻ B) ▻ A ▻ B ◎ x
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {x A B Γ Λ} → Γ , A , A ⁏ Λ ⊢ B ◎ x → Γ , A ⁏ Λ ⊢ B ◎ x
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {x A B C Γ Λ} → Γ ⁏ Λ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C ◎ x
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {x A B C Γ Λ} → Γ , A , B ⁏ Λ ⊢ C ◎ x → Γ , B , A  ⁏ Λ ⊢ C ◎ x
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {x A B C Γ Λ} → Γ ⁏ Λ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C ◎ x
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {x A B C Γ Λ} → Γ , B ⁏ Λ ⊢ C ◎ x → Γ , A ⁏ Λ ⊢ B ◎ x → Γ , A ⁏ Λ ⊢ C ◎ x
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

dist : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (A ▻ B) ◎ x → Γ ⁏ Λ ⊢ □ A ◎ x → Γ ⁏ Λ ⊢ □ B ◎ x
dist t u = scan (app (move (rmono⊢ weak⊆ t) rv₀) (move (rmono⊢ weak⊆ u) rv₀))

up : ∀ {x A Γ Λ} → Γ ⁏ Λ ⊢ □ A ◎ x → Γ ⁏ Λ ⊢ □ □ A ◎ x
up t = scan (scan (move (rmono⊢ (trans⊆ weak⊆ weak⊆) t) (rtrans rv₁ rv₀)))

down : ∀ {x A Γ Λ} → Γ ⁏ Λ ⊢ □ A ◎ x → Γ ⁏ Λ ⊢ A ◎ x
down t = move t rrefl

distup : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (□ A ▻ B) ◎ x → Γ ⁏ Λ ⊢ □ A ◎ x → Γ ⁏ Λ ⊢ □ B ◎ x
distup t u = dist t (up u)

box : ∀ {x A Γ Λ} → (∀ {y} → ∅ ⁏ Λ , x ↝ y ⊢ A ◎ y) → Γ ⁏ Λ ⊢ □ A ◎ x
box t = scan (mono⊢ bot⊆ t)

unbox : ∀ {x A C Γ Λ} → Γ ⁏ Λ ⊢ □ A ◎ x → Γ , □ A ⁏ Λ ⊢ C ◎ x → Γ ⁏ Λ ⊢ C ◎ x
unbox t u = app (lam u) t

-- Useful theorems in combinatory form.

ci : ∀ {x A Γ Λ} → Γ ⁏ Λ ⊢ A ▻ A ◎ x
ci = lam v₀

ck : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ▻ B ▻ A ◎ x
ck = lam (lam v₁)

cs : ∀ {x A B C Γ Λ} → Γ ⁏ Λ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C ◎ x
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cdist : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (A ▻ B) ▻ □ A ▻ □ B ◎ x
cdist = lam (lam (scan (app (move v₁ rv₀) (move v₀ rv₀))))

cup : ∀ {x A Γ Λ} → Γ ⁏ Λ ⊢ □ A ▻ □ □ A ◎ x
cup = lam (scan (scan (move v₀ (rtrans rv₁ rv₀))))

cdown : ∀ {x A Γ Λ} → Γ ⁏ Λ ⊢ □ A ▻ A ◎ x
cdown = lam (move v₀ rrefl)

cdistup : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (□ A ▻ B) ▻ □ A ▻ □ B ◎ x
cdistup = lam (lam (app (app cdist v₁) (app cup v₀)))

cunbox : ∀ {x A C Γ Λ} → Γ ⁏ Λ ⊢ □ A ▻ (□ A ▻ C) ▻ C ◎ x
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ▻ B ▻ A ∧ B ◎ x
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ∧ B ▻ A ◎ x
cfst = lam (fst v₀)

csnd : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ∧ B ▻ B ◎ x
csnd = lam (snd v₀)

-- Internalisation, or lifting, and additional theorems.

lift : ∀ {Γ x A Λ} → (∀ {y} → Γ ⁏ Λ , x ↝ y ⊢ A ◎ y) → □⋆ Γ ⁏ Λ ⊢ □ A ◎ x
lift {∅}     t = box t
lift {Γ , B} t = det (app cdist (lift (lam t)))

hypup : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ A ▻ B ◎ x → Γ ⁏ Λ ⊢ □ A ▻ B ◎ x
hypup t = lam (app (mono⊢ weak⊆ t) (down v₀))

hypdown : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ □ A ▻ B ◎ x → Γ ⁏ Λ ⊢ □ A ▻ B ◎ x
hypdown t = lam (app (mono⊢ weak⊆ t) (up v₀))

cxup : ∀ {Γ x A Λ} → Γ ⁏ Λ ⊢ A ◎ x → □⋆ Γ ⁏ Λ ⊢ A ◎ x
cxup {∅}     t = t
cxup {Γ , B} t = det (hypup (cxup (lam t)))

cxdown : ∀ {Γ x A Λ} → □⋆ □⋆ Γ ⁏ Λ ⊢ A ◎ x → □⋆ Γ ⁏ Λ ⊢ A ◎ x
cxdown {∅}     t = t
cxdown {Γ , B} t = det (hypdown (cxdown (lam t)))

box⋆ : ∀ {Ξ x Γ Λ} → (∀ {y} → ∅ ⁏ Λ , x ↝ y ⊢⋆ Ξ ◎⋆ y) → Γ ⁏ Λ ⊢⋆ □⋆ Ξ ◎⋆ x
box⋆ {∅}     f = ∙
box⋆ {Ξ , A} f = box⋆ (π₁ f) , box (π₂ f)

lift⋆ : ∀ {Ξ x Γ Λ} → (∀ {y} → Γ ⁏ Λ , x ↝ y ⊢⋆ Ξ ◎⋆ y) → □⋆ Γ ⁏ Λ ⊢⋆ □⋆ Ξ ◎⋆ x
lift⋆ {∅}     f = ∙
lift⋆ {Ξ , A} f = lift⋆ (π₁ f) , lift (π₂ f)

up⋆ : ∀ {Ξ x Γ Λ} → Γ ⁏ Λ ⊢⋆ □⋆ Ξ ◎⋆ x → Γ ⁏ Λ ⊢⋆ □⋆ □⋆ Ξ ◎⋆ x
up⋆ {∅}     f = ∙
up⋆ {Ξ , A} f = up⋆ (π₁ f) , up (π₂ f)

down⋆ : ∀ {Ξ x Γ Λ} → Γ ⁏ Λ ⊢⋆ □⋆ Ξ ◎⋆ x → Γ ⁏ Λ ⊢⋆ Ξ ◎⋆ x
down⋆ {∅}     f = ∙
down⋆ {Ξ , A} f = down⋆ (π₁ f) , down (π₂ f)

multibox : ∀ {Ξ x A Γ Λ} → Γ ⁏ Λ ⊢⋆ □⋆ Ξ ◎⋆ x → (∀ {y} → □⋆ Ξ ⁏ ∅ , x ↝ y ⊢ A ◎ y) → Γ ⁏ Λ ⊢ □ A ◎ x
multibox ts u = multicut (up⋆ ts) (rmono⊢ bot⊆ (lift u))

dist′ : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (A ▻ B) ◎ x → Γ ⁏ Λ ⊢ □ A ▻ □ B ◎ x
dist′ t = lam (dist (mono⊢ weak⊆ t) v₀)

mpair : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ A ◎ x → Γ ⁏ Λ ⊢ □ B ◎ x → Γ ⁏ Λ ⊢ □ (A ∧ B) ◎ x
mpair t u = scan (pair (move (rmono⊢ weak⊆ t) rv₀) (move (rmono⊢ weak⊆ u) rv₀))

mfst : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (A ∧ B) ◎ x → Γ ⁏ Λ ⊢ □ A ◎ x
mfst t = scan (fst (move (rmono⊢ weak⊆ t) rv₀))

msnd : ∀ {x A B Γ Λ} → Γ ⁏ Λ ⊢ □ (A ∧ B) ◎ x → Γ ⁏ Λ ⊢ □ B ◎ x
msnd t = scan (snd (move (rmono⊢ weak⊆ t) rv₀))

-- Closure under context concatenation.

concat : ∀ {x A B Γ} Γ′ {Λ} → Γ , A ⁏ Λ ⊢ B ◎ x → Γ′ ⁏ Λ ⊢ A ◎ x → Γ ⧺ Γ′ ⁏ Λ ⊢ B ◎ x
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- TODO: Substitution.

-- [_≔_]_ : ∀ {x A B Γ Λ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Λ ⊢ A ◎ x → Γ ⁏ Λ ⊢ B ◎ x → Γ ∖ i ⁏ Λ ⊢ B ◎ x
-- [ i ≔ s ] var j    with i ≟∈ j
-- [ i ≔ s ] var .i   | same   = s
-- [ i ≔ s ] var ._   | diff j = var j
-- [ i ≔ s ] lam t    = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
-- [ i ≔ s ] app t u  = app ([ i ≔ s ] t) ([ i ≔ s ] u)
-- [ i ≔ s ] scan t   = scan {![ i ≔ rmono⊢ weak⊆ s ] t!}
-- [ i ≔ s ] move t u = move {![ i ≔ s ] t!} u
-- [ i ≔ s ] pair t u = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
-- [ i ≔ s ] fst t    = fst ([ i ≔ s ] t)
-- [ i ≔ s ] snd t    = snd ([ i ≔ s ] t)
-- [ i ≔ s ] unit     = unit

-- TODO: Convertibility.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
A : {!!}
A a = Set

-- Display constraints (C-c C-=):
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Interaction/BasicOps.hs:457


text:
open import Common.Product
open import Agda.Builtin.Equality

data ⊥ : Set where

record Empty : Set where
  field absurdity : ⊥

magic₁ : Empty → ⊥
magic₁ ()

record EmptyIrr : Set where
  field .absurdity : ⊥

magic₂ : EmptyIrr → ⊥
magic₂ ()

test : ∀ x y → magic₂ x ≡ magic₂ y
test x y = refl

postulate whatever : Set

magic₃ : Σ ⊥ (λ _ → whatever) → ⊥
magic₃ ()

magic₄ : Σ whatever (λ _ → ⊥) → ⊥
magic₄ ()

data D : whatever → Set where

magic₅ : Σ whatever D → ⊥
magic₅ ()


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Lift
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism

module lib.groups.Lift where

Lift-group-structure : ∀ {i j} {A : Type i}
  → GroupStructure A → GroupStructure (Lift {j = j} A)
Lift-group-structure GS = record
  { ident = lift ident
  ; inv = λ {(lift x) → lift (inv x)}
  ; comp = λ {(lift x) (lift y) → lift (comp x y)}
  ; unit-l = λ {(lift y) → ap lift (unit-l y)}
  ; assoc = λ {(lift x) (lift y) (lift z) → ap lift (assoc x y z)}
  ; inv-l = λ {(lift x) → ap lift (inv-l x)}
  }
  where open GroupStructure GS

Lift-group : ∀ {i j} → Group i → Group (lmax i j)
Lift-group {j = j} G = group (Lift {j = j} El) (Lift-level El-level)
                             (Lift-group-structure group-struct)
  where open Group G

lift-hom : ∀ {i j} {G : Group i} → (G →ᴳ Lift-group {j = j} G)
lift-hom = group-hom lift (λ _ _ → idp)

lower-hom : ∀ {i j} {G : Group i} → (Lift-group {j = j} G →ᴳ G)
lower-hom = group-hom lower (λ _ _ → idp)

lift-iso : ∀ {i j} {G : Group i} → (G ≃ᴳ Lift-group {j = j} G)
lift-iso = lift-hom , snd lift-equiv

lower-iso : ∀ {i j} {G : Group i} → (Lift-group {j = j} G ≃ᴳ G)
lower-iso = lower-hom , snd lower-equiv

Lift-group-is-abelian : ∀ {i j} (G : Group i) → is-abelian G → is-abelian (Lift-group {j = j} G)
Lift-group-is-abelian G comm (lift g₁) (lift g₂) = ap lift (comm g₁ g₂)

Lift-abgroup : ∀ {i j} (G : AbGroup i) → AbGroup (lmax i j)
Lift-abgroup {j = j} G = Lift-group {j = j} (AbGroup.grp G)
  , Lift-group-is-abelian (AbGroup.grp G) (AbGroup.comm G)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Andreas, 2019-04-10, issue #3689, reported by andrejtokarcik

-- Regression introduced by #3533 (dropping trivially impossible clauses
-- during case-splitting).

-- {-# OPTIONS -v interaction.case:100 #-}
-- {-# OPTIONS -v tc.cover:100 #-}

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

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

record R (A : Set) : Set where
  field π : A

fun : {A : Set} (xyz : Σ (R A) λ r → Σ (R.π r ≡ R.π r) λ _ → R.π r ≡ R.π r) → Set
fun (x , y) = {!y !} -- C-c C-c

-- WAS: internal error.

-- Should succeed.


text:
-- Andreas, 2020-05-19, issue #4157, reported by nad

-- In old-style mutual blocks, it should be possible to have
-- several anonymous definitions.

open import Agda.Builtin.Equality

mutual

  _ : Set₁
  _ = Set

  _ : Set → Set
  _ = λ A → A

mutual

  F : Set → Set
  F = _

  _ : F ≡ λ A → A
  _ = refl

  G : Set → Set
  G = _

  _ : G ≡ λ A → A → A
  _ = refl

-- Should pass


text:
module LocalOpenImplicit where

record Id (a : Set) : Set where
  field id : a -> a

foo : {a b : Set} -> Id a -> Id b -> (a -> b) -> a -> b
foo id1 id2 f x = id id2 (f (id id1 x))
  where open Id


text:
module _ where

postulate
  C : Set → Set
  A : Set
  i : C A
  foo : {X : Set} {{_ : C X}} → X

-- Let bindings need to be declared 'instance' to be eligible.
bar : A
bar = let z = i in foo


text:
--------------------------------------------------------------------------------
-- Author : Bradley Hardy
--------------------------------------------------------------------------------
-- The first exercise from the ACS Algebraic Path Problems course, taught by
-- Timothy Griffin
--
-- Final proofs of 'fun fun facts' are at the bottom of the file; the rest
-- consists of definitions and supplementary proofs.
--------------------------------------------------------------------------------

module MLib.Lattices {ℓ} {S : Set ℓ} where

open import Matrix.Prelude

open import Function using (flip)

open Algebra.FunctionProperties (_≡_ {A = S}) using (Associative; Idempotent; Commutative)

module OperatorProperties (_∙_ : S → S → S) where
  _≤L_ = λ a b → a ≡ a ∙ b
  _≤R_ = λ a b → b ≡ a ∙ b

-- open OperatorProperties using (Associative; Idempotent; Commutative)

--------------------------------------------------------------------------------
--  Semigroups
--------------------------------------------------------------------------------

record IsCISemigroup (_∙_ : S → S → S) : Set ℓ where
  field
    isAssociative : Associative _∙_
    isIdempotent : Idempotent _∙_
    isCommutative : Commutative _∙_

  open OperatorProperties _∙_ public

  ≤L→flip≤R : ∀ {x y} → x ≤L y → y ≤R x
  ≤L→flip≤R p = ≡.trans p (isCommutative _ _)

  ≤R→flip≤L : ∀ {x y} → x ≤R y → y ≤L x
  ≤R→flip≤L p = ≡.trans p (isCommutative _ _)

  ≤L-isPartialOrder : IsPartialOrder _≡_ _≤L_
  ≤L-isPartialOrder =
    record
    { isPreorder =
      record
      { isEquivalence = ≡.isEquivalence
      ; reflexive = λ {i j} p →
        begin
          i           ≡⟨ ≡.sym (isIdempotent _) ⟩
          i ∙ i       ≡⟨ ≡.cong₂ _∙_ ≡.refl p ⟩
          i ∙ j       ∎
      ; trans = λ {i j k} p q →
        begin
          i             ≡⟨ p ⟩
          i ∙ j         ≡⟨ ≡.cong₂ _∙_ ≡.refl q ⟩
          i ∙ (j ∙ k)   ≡⟨ ≡.sym (isAssociative _ _ _) ⟩
          (i ∙ j) ∙ k   ≡⟨ ≡.cong₂ _∙_ (≡.sym p) ≡.refl ⟩
          i ∙ k         ∎
      }
    ; antisym = λ {x y} p q →
      begin
         x        ≡⟨ p ⟩
         x ∙ y    ≡⟨ isCommutative _ _ ⟩
         y ∙ x    ≡⟨ ≡.sym q ⟩
         y        ∎
    }
    where open ≡.≡-Reasoning

  -- Prove this by deferring to ≤L-isPartialOrder and taking advantage of the
  -- fact that _≤L_ and _≤R_ are dual.
  ≤R-isPartialOrder : IsPartialOrder _≡_ _≤R_
  ≤R-isPartialOrder =
    record
    { isPreorder =
      record
      { isEquivalence = ≡.isEquivalence
      ; reflexive = λ p → fromL (≤L.reflexive (≡.sym p))
      ; trans = λ {i j k} p q → fromL (≤L.trans (toL q) (toL p))
      }
    ; antisym = λ {x y} p q → ≤L.antisym (toL q) (toL p)
    }
    where module ≤L = IsPartialOrder ≤L-isPartialOrder
          fromL = ≤L→flip≤R
          toL = ≤R→flip≤L

--------------------------------------------------------------------------------
--  (Greatest) lower and (least) upper bounds
--------------------------------------------------------------------------------

record IsLowerBound (_≤_ : S → S → Set ℓ) (c a b : S) : Set ℓ where
  field
    ≤L : c ≤ a
    ≤R : c ≤ b

record IsGlb (_≤_ : S → S → Set ℓ) (c a b : S) : Set ℓ where
  field
    isLowerBound : IsLowerBound _≤_ c a b
    isGreatest : ∀ {d} → d ≤ a → d ≤ b → d ≤ c

  open IsLowerBound isLowerBound public

record IsUpperBound (_≤_ : S → S → Set ℓ) (c a b : S) : Set ℓ where
  field
    L≤ : a ≤ c
    R≤ : b ≤ c

record IsLub (_≤_ : S → S → Set ℓ) (c a b : S) : Set ℓ where
  field
    isUpperBound : IsUpperBound _≤_ c a b
    isLeast : ∀ {d} → a ≤ d → b ≤ d → c ≤ d

  open IsUpperBound isUpperBound public

  -- A least upper bound is a greatest lower bound with respect to the reversed
  -- order.
  flipGlb : IsGlb (flip _≤_) c a b
  flipGlb = record
    { isLowerBound = record { ≤L = L≤ ; ≤R = R≤ }
    ; isGreatest = isLeast
    }

module IsGlbProperties {≤ c a b} (isGlb : IsGlb ≤ c a b) where
  open IsGlb isGlb public

  sym : IsGlb ≤ c b a
  sym = record
    { isLowerBound = record { ≤L = ≤R ; ≤R = ≤L }
    ; isGreatest = λ x y → isGreatest y x
    }

  -- A greatest lower bound is a least upper bound with respect to the reversed
  -- order.
  flipLub : IsLub (flip ≤) c a b
  flipLub = record
    { isUpperBound = record { L≤ = ≤L ; R≤ = ≤R }
    ; isLeast = isGreatest
    }

module PartialOrderProperties (_≤_ : S → S → Set ℓ)
                              (isPartialOrder : IsPartialOrder _≡_ _≤_)
                              where
  module ≤ = IsPartialOrder isPartialOrder

  IsGlb-self : ∀ {a} → IsGlb _≤_ a a a
  IsGlb-self = record
    { isLowerBound = record { ≤L = ≤.refl ; ≤R = ≤.refl }
    ; isGreatest = λ x y → x
    }

  -- In a partial order, there is at most one greatest lower bound for any given
  -- pair of values.
  IsGlb-unique : ∀ {a b c} → IsGlb _≤_ c a b → ∀ {d} → IsGlb _≤_ d a b → c ≡ d
  IsGlb-unique p q =
    ≤.antisym
    (IsGlb.isGreatest q (IsGlb.≤L p) (IsGlb.≤R p))
    (IsGlb.isGreatest p (IsGlb.≤L q) (IsGlb.≤R q))

  flipIsPartialOrder : IsPartialOrder _≡_ (flip _≤_)
  flipIsPartialOrder = record
    { isPreorder = record
      { isEquivalence = ≡.isEquivalence
      ; reflexive = λ p → ≤.reflexive (≡.sym p)
      ; trans = flip ≤.trans
      }
      ; antisym = flip ≤.antisym
    }

--------------------------------------------------------------------------------
--  Semilattices
--------------------------------------------------------------------------------

record IsMeetSemilattice (_≤_ : S → S → Set ℓ) (_⊓_ : S → S → S) : Set ℓ where
  field
    isPartialOrder : IsPartialOrder _≡_ _≤_
    isGlb : ∀ {a b} → IsGlb _≤_ (a ⊓ b) a b

  open PartialOrderProperties _≤_ isPartialOrder public
  module This {a b} = IsGlbProperties (isGlb {a} {b})
  open This public

  -- In a meet semilattice, the only greatest lower bound of any pair 'a' and
  -- 'b' is 'a ⊓ b'.
  glb-intro : ∀ {c a b} → IsGlb _≤_ c a b → c ≡ a ⊓ b
  glb-intro p = IsGlb-unique p isGlb

  module CISemigroup where
    isCommutative : Commutative _⊓_
    isCommutative _ _ = glb-intro (IsGlbProperties.sym isGlb)

    isIdempotent : Idempotent _⊓_
    isIdempotent _ = ≡.sym (glb-intro IsGlb-self)

    isAssociative : Associative _⊓_
    isAssociative a b c =
      let d = (a ⊓ b) ⊓ c

          d≤a : d ≤ a
          d≤a = ≤.trans ≤L ≤L

          d≤b : d ≤ b
          d≤b = ≤.trans ≤L ≤R

          d≤c : d ≤ c
          d≤c = ≤R

          d≤b⊓c : d ≤ (b ⊓ c)
          d≤b⊓c = isGreatest d≤b d≤c

          d-greatest : ∀ {d′} → d′ ≤ a → d′ ≤ b → d′ ≤ c → d′ ≤ d
          d-greatest p q r = isGreatest (isGreatest p q) r
      in glb-intro (
         record
         { isLowerBound = record { ≤L = ≤.trans ≤L ≤L ; ≤R = d≤b⊓c}
         ; isGreatest = λ p q → d-greatest p (≤.trans q ≤L) (≤.trans q ≤R)
         })

  -- A meet semilattic is also a commutative idempotent semigroup
  isCISemigroup : IsCISemigroup _⊓_
  isCISemigroup = record { CISemigroup }

record IsJoinSemilattice (≤ : S → S → Set ℓ) (_⊔_ : S → S → S) : Set ℓ where
  field
    isPartialOrder : IsPartialOrder _≡_ ≤
    isLub : ∀ {a b} → IsLub ≤ (a ⊔ b) a b

  open PartialOrderProperties ≤ isPartialOrder public
  module This {a b} = IsLub (isLub {a} {b})
  open This

  -- A join semilattice is a meet semilattice with respect to the reversed order
  flipIsMeetSemilattice : IsMeetSemilattice (flip ≤) _⊔_
  flipIsMeetSemilattice = record
    { isPartialOrder = flipIsPartialOrder
    ; isGlb = flipGlb
    }

  -- A join semilattice is also a commutative idempotent semigroup
  open IsMeetSemilattice flipIsMeetSemilattice using (isCISemigroup) public

module MeetSemilatticeProperties {≤ ⊓}
                                 (isMeetSemilattice : IsMeetSemilattice ≤ ⊓)
                                 where

  open IsMeetSemilattice isMeetSemilattice

  -- A meet semilattice is a join semilattice with respect to the reversed order
  flipIsJoinSemilattice : IsJoinSemilattice (flip ≤) ⊓
  flipIsJoinSemilattice = record
    { isPartialOrder = flipIsPartialOrder
    ; isLub = flipLub
    }

--------------------------------------------------------------------------------
--  Proofs of fun fun facts
--------------------------------------------------------------------------------

-- Commutative idempotent semigroups create meet and join semilattices from
-- their left and right natural orders respectively.
module FunFunFact1 {_∙_ : S → S → S} (isCISemigroup : IsCISemigroup _∙_) where
  open IsCISemigroup isCISemigroup

  funFunFact1Meet : IsMeetSemilattice _≤L_ _∙_
  funFunFact1Meet =
    record
    { isPartialOrder = ≤L-isPartialOrder
    ; isGlb = λ {a b} → record
      { isLowerBound = record
        { ≤L =
          begin
            a ∙ b          ≡⟨ ≡.cong₂ _∙_ (≡.sym (isIdempotent _)) ≡.refl ⟩
            (a ∙ a) ∙ b    ≡⟨ isAssociative _ _ _ ⟩
            a ∙ (a ∙ b)    ≡⟨ isCommutative _ _ ⟩
            (a ∙ b) ∙ a    ∎
        ; ≤R =
          begin
            a ∙ b         ≡⟨ ≡.cong₂ _∙_ ≡.refl (≡.sym (isIdempotent _)) ⟩
            a ∙ (b ∙ b)   ≡⟨ ≡.sym (isAssociative _ _ _) ⟩
            (a ∙ b) ∙ b   ∎
        }
      ; isGreatest = λ {d} p q →
        begin
          d                 ≡⟨ ≡.sym (isIdempotent _) ⟩
          d ∙ d             ≡⟨ ≡.cong₂ _∙_ p q ⟩
          (d ∙ a) ∙ (d ∙ b) ≡⟨ isAssociative _ _ _ ⟩
          d ∙ (a ∙ (d ∙ b)) ≡⟨ ≡.cong₂ _∙_ ≡.refl (≡.sym (isAssociative _ _ _)) ⟩
          d ∙ ((a ∙ d) ∙ b) ≡⟨ ≡.cong₂ _∙_ ≡.refl
                               (≡.cong₂ _∙_ (isCommutative _ _) ≡.refl) ⟩
          d ∙ ((d ∙ a) ∙ b) ≡⟨ ≡.cong₂ _∙_ ≡.refl (isAssociative _ _ _) ⟩
          d ∙ (d ∙ (a ∙ b)) ≡⟨ ≡.sym (isAssociative _ _ _) ⟩
          (d ∙ d) ∙ (a ∙ b) ≡⟨ ≡.cong₂ _∙_ (isIdempotent _) ≡.refl ⟩
          d ∙ (a ∙ b)       ∎
      }
    }
    where open ≡.≡-Reasoning

  -- Prove for join by symmetry with meet
  funFunFact1Join : IsJoinSemilattice _≤R_ _∙_
  funFunFact1Join =
    record
    { isPartialOrder = ≤R-isPartialOrder
    ; isLub = λ {a b} → record
      { isUpperBound = record
        { L≤ = fromL Meet.≤L
        ; R≤ = fromL Meet.≤R
        }
      ; isLeast =
        λ {d} p q →
        fromL (Meet.isGreatest (toL p) (toL q))
      }
    }
    where
      open ≡.≡-Reasoning
      module Meet = IsMeetSemilattice funFunFact1Meet
      toL = ≤R→flip≤L
      fromL = ≤L→flip≤R

-- Semilattices are commutative idempotent semigroups
module FunFunFact2 {≤ : S → S → Set ℓ} where
  funFunFact2Meet : ∀ {⊓} → IsMeetSemilattice ≤ ⊓ → IsCISemigroup ⊓
  funFunFact2Meet ijs = isCISemigroup
    where open IsMeetSemilattice ijs

  -- Note this is using 'isCISemigroup' from the flipped /meet/ semilattice.
  funFunFact2Join : ∀ {⊔} → IsJoinSemilattice ≤ ⊔ → IsCISemigroup ⊔
  funFunFact2Join ijs = isCISemigroup
    where open IsJoinSemilattice ijs


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

module Luau.OpSem where

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.String using (primStringEquality; primStringAppend)
open import Utility.Bool using (not; _or_; _and_)
open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; ··; number; bool; string)
open import Luau.RuntimeType using (RuntimeType; valueType)
open import Properties.Product using (_×_; _,_)

evalEqOp : Value → Value → Bool
evalEqOp Value.nil Value.nil = true
evalEqOp (addr x) (addr y) = (x ==ᴬ y)
evalEqOp (number x) (number y) = primFloatEquality x y
evalEqOp (bool true) (bool y) = y
evalEqOp (bool false) (bool y) = not y
evalEqOp _ _ = false

evalNeqOp : Value → Value → Bool
evalNeqOp (number x) (number y) = primFloatInequality x y
evalNeqOp x y = not (evalEqOp x y)

data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
  + : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n)
  - : ∀ m n → (number m) ⟦ - ⟧ (number n) ⟶ number (primFloatMinus m n)
  / : ∀ m n → (number m) ⟦ / ⟧ (number n) ⟶ number (primFloatTimes m n)
  * : ∀ m n → (number m) ⟦ * ⟧ (number n) ⟶ number (primFloatDiv m n)
  < : ∀ m n → (number m) ⟦ < ⟧ (number n) ⟶ bool (primFloatLess m n)
  > : ∀ m n → (number m) ⟦ > ⟧ (number n) ⟶ bool (primFloatLess n m)
  <= : ∀ m n → (number m) ⟦ <= ⟧ (number n) ⟶ bool ((primFloatLess m n) or (primFloatEquality m n))
  >= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n))
  == : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w)
  ~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w)
  ·· : ∀ x y → (string x) ⟦ ·· ⟧ (string y) ⟶ string (primStringAppend x y)

data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set

data _⊢_⟶ᴱ_⊣_  where

  function : ∀ a {H H′ F B} →

    H′ ≡ H ⊕ a ↦ (function F is B end) →
    -------------------------------------------
    H ⊢ (function F is B end) ⟶ᴱ val(addr a) ⊣ H′

  app₁ : ∀ {H H′ M M′ N} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    -----------------------------
    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′

  app₂ : ∀ v {H H′ N N′} →

    H ⊢ N ⟶ᴱ N′ ⊣ H′ →
    -----------------------------
    H ⊢ (val v $ N) ⟶ᴱ (val v $ N′) ⊣ H′

  beta : ∀ O v {H a F B} →

    (O ≡ function F is B end) →
    H [ a ] ≡ just(O) →
    -----------------------------------------------------------------------------
    H ⊢ (val (addr a) $ val v) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) ⊣ H

  block : ∀ {H H′ B B′ b} →

    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
    ----------------------------------------------------
    H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′

  return : ∀ v {H B b} →

    --------------------------------------------------------
    H ⊢ (block b is return (val v) ∙ B end) ⟶ᴱ val v ⊣ H

  done : ∀ {H b} →

    --------------------------------------------
    H ⊢ (block b is done end) ⟶ᴱ (val nil) ⊣ H

  binOp₀ : ∀ {H op v₁ v₂ w} →

    v₁ ⟦ op ⟧ v₂ ⟶ w →
    --------------------------------------------------
    H ⊢ (binexp (val v₁) op (val v₂)) ⟶ᴱ (val w) ⊣ H

  binOp₁ : ∀ {H H′ x x′ op y} →

    H ⊢ x ⟶ᴱ x′ ⊣ H′ →
    ---------------------------------------------
    H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′

  binOp₂ : ∀ {H H′ x op y y′} →

    H ⊢ y ⟶ᴱ y′ ⊣ H′ →
    ---------------------------------------------
    H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′

data _⊢_⟶ᴮ_⊣_  where

  local : ∀ {H H′ x M M′ B} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    -------------------------------------------------
    H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′

  subst : ∀ v {H x B} →

    ------------------------------------------------------
    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H

  function : ∀ a {H H′ F B C} →

    H′ ≡ H ⊕ a ↦ (function F is C end) →
    --------------------------------------------------------------
    H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / name(fun F) ]ᴮ) ⊣ H′

  return : ∀ {H H′ M M′ B} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    --------------------------------------------
    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′

data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set where

  refl : ∀ {H B} →

    ----------------
    H ⊢ B ⟶* B ⊣ H

  step : ∀ {H H′ H″ B B′ B″} →
    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
    H′ ⊢ B′ ⟶* B″ ⊣ H″ →
    ------------------
    H ⊢ B ⟶* B″ ⊣ H″

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module Numeric.Nat.Prime where

open import Prelude hiding (less-antirefl)
open import Numeric.Nat.GCD
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.DivMod
open import Numeric.Nat.Sqrt
open import Numeric.Nat.Properties
open import Tactic.Nat

data Prime (n : Nat) : Set where
  prime : n > 1 → (∀ k → k Divides n → Either (k ≡ 1) (k ≡ n)) → Prime n

private
  lem : (a b : Nat) → b > 1 → suc a < suc a * b
  lem a .(suc (k + 1)) (diff! k) = auto

data Composite (n : Nat) : Set where
  composite : ∀ a b → a > 1 → b > 1 → a * b ≡ n → Composite n

pattern composite! a b 1<a 1<b = composite a b 1<a 1<b refl

composite-not-prime : ∀ {n} → Composite n → Prime n → ⊥
composite-not-prime (composite! 0 b (diff _ ()) _)
composite-not-prime (composite! (suc a) b sa>1 b>1) (prime _ f) =
  case f (suc a) (divides-mul-l b divides-refl) of λ
  { (left  sa=1)   → less-antirefl sa>1 (sym sa=1)
  ; (right sa=sab) → less-antirefl (lem a b b>1) sa=sab
  }

data Prime? n : Set where
  yes  : Prime n     → Prime? n
  no   : Composite n → Prime? n
  tiny : LessNat n 2 → Prime? n

private
  less-inv : ∀ {a b} → ¬ LessNat a b → LessNat b (suc a)
  less-inv {a} {b} a≮b with compare a b
  less-inv a≮b | less a<b    = ⊥-elim (a≮b a<b)
  less-inv a≮b | equal refl  = diff! 0
  less-inv a≮b | greater a>b = by a>b

data _∈[_,_] (n a b : Nat) : Set where
  in-range : a ≤ n → n ≤ b → n ∈[ a , b ]

empty-range : ∀ {n a b} → a > b → ¬ (n ∈[ a , b ])
empty-range a>b (in-range a≤n n≤b) = less-not-geq a>b (a≤n ⟨≤⟩ n≤b)

below-range : ∀ {n a b} → n < a → ¬ (n ∈[ a , b ])
below-range n<a (in-range a≤n _) = less-not-geq n<a a≤n

range-lower-bound : ∀ {n a b} → n ∈[ a , b ] → a ≤ n
range-lower-bound (in-range a<n _) = a<n

range-upper-bound : ∀ {n a b} → n ∈[ a , b ] → n ≤ b
range-upper-bound (in-range _ n<b) = n<b

singleton-range : ∀ {n a} → n ∈[ a , a ] → a ≡ n
singleton-range (in-range a<n n<a) = leq-antisym a<n n<a

suc-range-r : ∀ {n a b} → n ∈[ a , b ] → n ∈[ a , suc b ]
suc-range-r (in-range a<n n<b) = in-range a<n (by n<b)

suc-range-l : ∀ {n a b} → n ∈[ suc a , b ] → n ∈[ a , b ]
suc-range-l (in-range a<n n<b) = in-range (by a<n) n<b

in-range-l :  ∀ {a b} → a ≤ b → a ∈[ a , b ]
in-range-l a<b = in-range (diff! 0) a<b

in-range-r :  ∀ {a b} → a ≤ b → b ∈[ a , b ]
in-range-r a<b = in-range a<b (diff! 0)

non-zero-range : ∀ {n a b} → n ∈[ suc a , b ] → NonZero n
non-zero-range {zero} {a} (in-range (diff k eq) _) = refute eq
non-zero-range {suc _} _ = _

erase-in-range : ∀ {n a b} → n ∈[ a , b ] → n ∈[ a , b ]
erase-in-range r = in-range (fast-diff (range-lower-bound r))
                            (fast-diff (range-upper-bound r))

data _∈[_,_]? k a b : Set where
  inside : k ∈[ a , b ] → k ∈[ a , b ]?
  below  : k < a → k ∈[ a , b ]?
  above  : k > b → k ∈[ a , b ]?

cmp-leq : (a b : Nat) → Either (a < b) (b ≤ a)
cmp-leq a b with compare a b
cmp-leq a b | less    a<b = left a<b
cmp-leq a b | equal   a=b = right (diff 0 (cong suc a=b))
cmp-leq a b | greater a>b = right (by a>b)

in-range? : ∀ k a b → k ∈[ a , b ]?
in-range? k a b with cmp-leq k a
in-range? k a b | left  k<a = below k<a
in-range? k a b | right k≥a with cmp-leq b k
in-range? k a b | right k≥a | left k>b = above k>b
in-range? k a b | right k≥a | right k≤b = inside (in-range k≥a k≤b)

data FindInRange {ℓ} a b (P : Nat → Set ℓ) : Set ℓ where
  here :  ∀ k → k ∈[ a , b ] →   P k  → FindInRange a b P
  none : (∀ k → k ∈[ a , b ] → ¬ P k) → FindInRange a b P

-- Version with less evidence. Faster to compute.
data FindInRange! {ℓ} (P : Nat → Set ℓ) : Set ℓ where
  here :  ∀ k → P k → FindInRange! P
  none : FindInRange! P

private
  not-first : ∀ {ℓ} {P : Nat → Set ℓ} {a b} →
              ¬ P a → (∀ k → k ∈[ suc a , b ] → ¬ P k) →
              ∀ k → k ∈[ a , b ] → ¬ P k
  not-first {a = a} !pa !pa+ k k∈r pk with compare k a
  not-first !pa !pa+ k k∈r              pk | less    k<a  = below-range k<a k∈r
  not-first !pa !pa+ k k∈r              pk | equal   refl = !pa pk
  not-first !pa !pa+ k (in-range _ k≤b) pk | greater k>a  = !pa+ k (in-range (by k>a) k≤b) pk

  find! : ∀ {ℓ} {P : Nat → Set ℓ} (a d : Nat) → (∀ k → Dec (P k)) → FindInRange! P
  find! a  zero   check = none
  find! a (suc d) check with check a
  find! a (suc d) check | yes pa = here a pa
  find! a (suc d) check | no _ = force a λ a → find! (suc a) d check

  found-in-range : ∀ {ℓ} {P : Nat → Set ℓ} a b d (eq : d + a ≡ suc b) (check : ∀ k → Dec (P k)) →
                     ∀ k (pk : P k) → find! a d check ≡ here k pk → k ∈[ a , b ]
  found-in-range a b zero eq check k pk ()
  found-in-range a b (suc d) eq check k pk feq with check a
  found-in-range a b (suc d) eq check .a pa refl | yes .pa = in-range-l (by eq)
  found-in-range  0      b (suc d) eq check  k pk feq | no !pa
    with find! 1 d check | found-in-range 1 b d (by eq) check
  found-in-range  0      b (suc d) eq check k pk refl | no !pa | here .k .pk | rec = suc-range-l (rec _ _ refl)
  found-in-range  0      b (suc d) eq check k pk ()   | no !pa | none        | rec
  found-in-range (suc a) b (suc d) eq check k pk feq  | no !pa
    with find! (2 + a) d check | found-in-range (2 + a) b d (by eq) check
  found-in-range (suc a) b (suc d) eq check k pk refl | no !pa | here .k .pk | rec = suc-range-l (rec _ _ refl)
  found-in-range (suc a) b (suc d) eq check k pk ()   | no !pa | none        | rec

  not-found-in-range : ∀ {ℓ} {P : Nat → Set ℓ} a b d (eq : d + a ≡ suc b) (check : ∀ k → Dec (P k)) →
                         find! a d check ≡ none → ∀ k → k ∈[ a , b ] → ¬ P k
  not-found-in-range 0       b zero eq check prf k k∈ab pk = empty-range (diff 0 eq) k∈ab
  not-found-in-range (suc _) b zero eq check prf k k∈ab pk = empty-range (diff 0 eq) k∈ab
  not-found-in-range a b (suc d) eq check prf k (in-range a<k k<b) pk with check a
  not-found-in-range a b (suc d) eq check ()  k (in-range a<k k<b) pk | yes pa
  not-found-in-range 0 b (suc d) eq check prf k (in-range a<k k<b) pk | no !pa
    with find! 1 d check | not-found-in-range 1 b d (by eq) check
  not-found-in-range 0 b (suc d) eq check ()  k (in-range a<k k<b) pk | no !pa | here _ _ | rec
  not-found-in-range 0 b (suc d) eq check prf k (in-range a<k k<b) pk | no !pa | none     | rec =
    not-first !pa (rec refl) k (in-range a<k k<b) pk
  not-found-in-range (suc a) b (suc d) eq check prf k (in-range a<k k<b) pk | no !pa
    with find! (suc (suc a)) d check | not-found-in-range (suc (suc a)) b d (by eq) check
  not-found-in-range (suc a) b (suc d) eq check ()  k (in-range a<k k<b) pk | no !pa | here _ _ | rec
  not-found-in-range (suc a) b (suc d) eq check prf k (in-range a<k k<b) pk | no !pa | none     | rec =
    not-first !pa (rec refl) k (in-range a<k k<b) pk

  find : ∀ {ℓ} {P : Nat → Set ℓ} a b d → d + a ≡ suc b → (∀ k → Dec (P k)) → FindInRange a b P
  find a b d eq check with inspect (find! a d check)
  ... | here k pk with≡ prf = here k (erase-in-range (found-in-range a b d eq check k pk prf)) pk
  ... | none with≡ prf      = none (not-found-in-range a b d eq check prf)

findInRange : ∀ {ℓ} {P : Nat → Set ℓ} a b → (∀ k → Dec (P k)) → FindInRange a b P
findInRange a  b check with compare a b
findInRange a ._ check | less (diff! k) = find a _ (2 + k) refl check
findInRange a .a check | equal   refl   = find a _ 1 refl check
findInRange a  b check | greater gt     = none (λ k k∈ab _ → empty-range gt k∈ab)

--- Reducing the required search space to 2..√a ---

private
  lem-less : {n r d q : Nat} → r ^ 2 ≥ n →
        q * d ≡ n → r < d → suc r ≤ q → ⊥
  lem-less (diff k eq) refl (diff j refl) (diff! i) = refute eq

  non-zero-less : ∀ {a} {{_ : NonZero a}} → 0 < a
  non-zero-less {0} {{}}
  non-zero-less {suc a} = diff a auto

  div-unique : ∀ q {a b} {{_ : NonZero b}} → q * b ≡ a → a div b ≡ q
  div-unique q {a} {b} eq = quot-unique (qr (a div b) (a mod b) (mod-less b a) (divmod-sound b a))
                                        (qr q 0 non-zero-less (by eq))

  divide-smaller : ∀ n r d {{_ : NonZero d}} → n ≤ r ^ 2 → d Divides n → d > r → n div d ≤ r
  divide-smaller n r d n<r² (factor q eq) d>r =
    let n/d=q : n div d ≡ q
        n/d=q = div-unique q eq
    in less-raa (lem-less n<r² (cong (_* d) n/d=q ⟨≡⟩ eq) d>r)

  divide-bigger : ∀ n k {{_ : NonZero k}} → k < n → k Divides n → n div k ≥ 2
  divide-bigger ._ k (diff! k₁) (factor zero eq) = refute eq
  divide-bigger n  k k<n (factor 1 eq) = ⊥-elim (less-antirefl k<n (by eq))
  divide-bigger n  k k<n (factor (suc (suc q)) eq) = by (sym (div-unique (2 + q) {b = k} eq))

  up-to-root : ∀ r n → r ≤ n → r ^ 2 ≥ suc n → FindInRange 2 r (_Divides suc n) → FindInRange 2 n (_Divides suc n)
  up-to-root r n r<n r²>n (none k∤sn) =
    none λ k k∈2n k|sn → erase-⊥ $
    case in-range? k 2 r of λ
    { (inside k∈2r) → k∤sn k k∈2r k|sn
    ; (below  k<2)  → less-not-geq k<2 (range-lower-bound k∈2n)
    ; (above  k>r)  →
      let instance k≠0 : NonZero k
                   k≠0 = non-zero-range k∈2n
          hi : suc n div k ≤ r
          hi = divide-smaller (suc n) r k r²>n k|sn k>r
          lo : suc n div k ≥ 2
          lo = divide-bigger (suc n) k (range-upper-bound k∈2n) k|sn
      in k∤sn (suc n div k) (in-range lo hi) (factor k (by (div-divides k|sn)))
    }
  up-to-root 0 _ _ _ (here k k∈⊥ _) = ⊥-elim (empty-range (diff! 1) k∈⊥)
  up-to-root (suc r) n r<n r²>n (here k (in-range 2<k k<r) pk) =
    here k (in-range 2<k (k<r ⟨≤⟩ r<n)) pk

private
  is-1-or-n : ∀ {n} → (∀ k → k ∈[ 2 , n ] → k Divides suc n → ⊥) →
                  ∀ k → k Divides suc n → Either (k ≡ 1) (k ≡ suc n)
  is-1-or-n {n} no-div  k (factor q kq=n) with in-range? k 2 n
  is-1-or-n     no-div  k (factor q kq=n) | inside inr = ⊥-elim (no-div k inr (factor q kq=n))
  is-1-or-n     no-div .1 (factor q kq=n) | below (diff! zero) = left refl
  is-1-or-n {n} no-div  k (factor q kq=n) | below (diff (suc k₁) eq) =
    refute (divides-zero (transport (_Divides suc n) (by eq) (factor q kq=n)))
  is-1-or-n {n} no-div  k (factor q kq=n) | above  k>n =
    right (leq-antisym {A = Nat} (divides-less (factor q kq=n)) (by k>n))

  lem₂ : ∀ {n d : Nat} q → q * d ≡ suc n → d < suc n → q > 1
  lem₂ 0 eq d≤n = refute eq
  lem₂ 1 eq d≤n = ⊥-elim (less-antirefl d≤n (by eq))
  lem₂ (suc (suc q)) eq d≤n = auto

  two-is-prime : ∀ k → k Divides 2 → Either (k ≡ 1) (k ≡ 2)
  two-is-prime k k|2 with divides-less k|2
  two-is-prime 0 (factor q eq) | k≤2 = refute eq
  two-is-prime 1 k|2 | k≤2 = left refl
  two-is-prime 2 k|2 | k≤2 = right refl
  two-is-prime (suc (suc (suc k))) k|2 | lt = refute lt

  lem-sqrt : (n r : Nat) → r ^ 2 < 4 + n → ¬ (suc n < r)
  lem-sqrt n ._ lt (diff! c) = refute lt

  sqrt-less : (n : Nat) → n > 2 → suc (sqrt! n) < n
  sqrt-less 0 (diff k ())
  sqrt-less 1 (diff k eq) = refute eq
  sqrt-less 2 (diff k eq) = refute eq
  sqrt-less (suc (suc (suc n))) _ with sqrt (3 + n)
  sqrt-less (suc (suc (suc n))) _ | root r lt _ =
    less-raa λ n<r → lem-sqrt n r lt (by n<r)

  isPrimeAux : ∀ n → Comparison _<_ 2 n → Prime? n
  isPrimeAux 0 _ = tiny (diff! 1)
  isPrimeAux 1 _ = tiny (diff! 0)
  isPrimeAux 2 _ = yes (prime (diff! 0) two-is-prime)
  isPrimeAux (suc (suc (suc n))) (greater (diff k eq)) = refute eq
  isPrimeAux (suc (suc (suc _))) (equal ())
  isPrimeAux (suc n) (less n>2) with sqrt (suc n) | sqrt-less _ n>2
  ... | root r r²<n sr²>n | r<n with up-to-root (suc r) n r<n (by sr²>n) $
                                     findInRange 2 (suc r) (λ k → k divides? suc n)
  ...   | none p = yes (prime (by n>2) (is-1-or-n p))
  ...   | here d (in-range 2≤d d≤n) (factor q eq) =
    no (composite d q (by 2≤d) (lem₂ q eq d≤n) (by eq))

isPrime : ∀ n → Prime? n
isPrime n = isPrimeAux n (compare 2 n)

isPrime! : Nat → Bool
isPrime! n with isPrime n
... | yes  _ = true
... | no   _ = false
... | tiny _ = false

decPrime : ∀ p → Dec (Prime p)
decPrime p =
  case isPrime p of λ where
    (yes isp)  → yes isp
    (no comp)  → no (composite-not-prime comp)
    (tiny p<2) → no λ where (prime p>1 dp) → less-not-geq p>1 p<2

-- Benchmarking

-- Todo: test only odd numbers

--   Composite
--       5.0s    + isPrime 1927   (41 * 47)
--        40ms   recurse from below
--       5.2s    + isPrime (1021 * 1021)
--       0.2s    remove range argument from check
--       0.8s    + isPrime (3581 * 3581)
--       0.3s    don't compute in-range proof in find!

--   Prime (no proof)
--       2.3s    + isPrime! 1021
--       5.0s    recurse from below
--       0.1s    remove range argument from check
--       0.7s    + isPrime! 3581

--   Prime (run proof: cheap because we're not actually running the (negative) function computed by find)
--       0.7s    + testPrimeProof 3581

--   Prime (print proof)
--       1.8s    + isPrime 83
--       3.4s    recurse from below
--       2.6s    remove range argument from check
--       0.1s    split negative proof into separate function
--       0.6s    + isPrime 3581
--       0.2s    only check up to sqrt
--       0.7s    + isPrime 12823607
--       2.3s    + isPrime 234576373
--       1.4s    don't compute in-range proof in find!

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
open import Oscar.Prelude
open import Oscar.Data.¶
open import Oscar.Data.Fin
open import Oscar.Data.Vec

module Oscar.Data.Term where

module Term {𝔭} (𝔓 : Ø 𝔭) where

  mutual

    Terms : ¶ → ¶ → Ø 𝔭
    Terms N n = ⟨ Term n ∞ ⟩¶⟨≤ N ⟩

    data Term (n : ¶) : Ø 𝔭 where
      i : (x : ¶⟨< n ⟩) → Term n
      leaf : Term n
      _fork_ : (s t : Term n) → Term n
      function : 𝔓 → ∀ {N} → Terms N n → Term n


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.QuotientAlgebra where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Powerset using (_∈_; _⊆_)
open import Cubical.Foundations.Structure

open import Cubical.HITs.SetQuotients hiding (_/_)
open import Cubical.Data.Unit
open import Cubical.Data.Sigma.Properties using (Σ≡Prop)

open import Cubical.Algebra.CommRing
import Cubical.Algebra.CommRing.QuotientRing as CommRing
import Cubical.Algebra.Ring.QuotientRing as Ring
open import Cubical.Algebra.CommRing.Ideal hiding (IdealsIn)
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Ideal
open import Cubical.Algebra.CommAlgebra.Kernel
open import Cubical.Algebra.CommAlgebra.Instances.Unit
open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom; isPropIsAlgebraHom)
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Ideal using (isIdeal)
open import Cubical.Algebra.CommRingSolver.Reflection
open import Cubical.Algebra.Algebra.Properties
open AlgebraHoms using (compAlgebraHom)

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
  open CommRingStr {{...}} hiding (_-_; -_; dist; ·Lid; ·Rdist+) renaming (_·_ to _·R_; _+_ to _+R_)
  open CommAlgebraStr {{...}}
  open RingTheory (CommRing→Ring (CommAlgebra→CommRing A)) using (-DistR·)
  instance
    _ : CommRingStr _
    _ = snd R
    _ : CommAlgebraStr _ _
    _ = snd A

  _/_ : CommAlgebra R ℓ
  _/_ = commAlgebraFromCommRing
           ((CommAlgebra→CommRing A) CommRing./ I)
           (λ r → elim (λ _ → squash/) (λ x → [ r ⋆ x ]) (eq r))
           (λ r s → elimProp (λ _ → squash/ _ _)
                             λ x i → [ ((r ·R s) ⋆ x ≡⟨ ⋆-assoc r s x ⟩
                                         r ⋆ (s ⋆ x) ∎) i ])
           (λ r s → elimProp (λ _ → squash/ _ _)
                             λ x i → [ ((r +R s) ⋆ x ≡⟨ ⋆-ldist r s x ⟩
                                       r ⋆ x + s ⋆ x ∎) i ])
           (λ r → elimProp2 (λ _ _ → squash/ _ _)
                            λ x y i → [ (r ⋆ (x + y)  ≡⟨ ⋆-rdist r x y ⟩
                                        r ⋆ x + r ⋆ y ∎) i ])
           (elimProp (λ _ → squash/ _ _)
                     (λ x i →  [ (1r ⋆ x ≡⟨ ⋆-lid x ⟩ x ∎) i ]))
           λ r → elimProp2 (λ _ _ → squash/ _ _)
                           λ x y i → [ ((r ⋆ x) · y ≡⟨ ⋆-lassoc r x y ⟩
                                       r ⋆ (x · y) ∎) i ]

          where
                open CommIdeal using (isCommIdeal)
                eq : (r : fst R) (x y : fst A) → x - y ∈ (fst I) →  [ r ⋆ x ] ≡ [ r ⋆ y ]
                eq r x y x-y∈I = eq/ _ _
                  (subst (λ u → u ∈ fst I)
                  ((r ⋆ 1a) · (x - y)               ≡⟨ ·Rdist+ (r ⋆ 1a) x (- y) ⟩
                    (r ⋆ 1a) · x + (r ⋆ 1a) · (- y) ≡[ i ]⟨ (r ⋆ 1a) · x + -DistR· (r ⋆ 1a) y i ⟩
                    (r ⋆ 1a) · x - (r ⋆ 1a) · y     ≡[ i ]⟨ ⋆-lassoc r 1a x i
                                                            - ⋆-lassoc r 1a y i ⟩
                    r ⋆ (1a · x) - r ⋆ (1a · y)     ≡[ i ]⟨ r ⋆ (·Lid x i) - r ⋆ (·Lid y i) ⟩
                    r ⋆ x - r ⋆ y ∎ )
                  (isCommIdeal.·Closed (snd I) _ x-y∈I))

  quotientHom : CommAlgebraHom A (_/_)
  fst quotientHom x = [ x ]
  IsAlgebraHom.pres0 (snd quotientHom) = refl
  IsAlgebraHom.pres1 (snd quotientHom) = refl
  IsAlgebraHom.pres+ (snd quotientHom) _ _ = refl
  IsAlgebraHom.pres· (snd quotientHom) _ _ = refl
  IsAlgebraHom.pres- (snd quotientHom) _ = refl
  IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
  open CommRingStr {{...}} hiding (_-_; -_; dist; ·Lid; ·Rdist+) renaming (_·_ to _·R_; _+_ to _+R_)
  open CommAlgebraStr ⦃...⦄

  instance
    _ : CommRingStr _
    _ = snd R
    _ : CommAlgebraStr _ _
    _ = snd A

  private
    LRing = CommAlgebra→Ring (A / I)
    RRing = (CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I)

  -- sanity check / maybe a helper function some day
  CommForget/ : RingEquiv (CommAlgebra→Ring (A / I)) ((CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I))
  fst CommForget/ =
    isoToEquiv
      (iso
        (rec (isSetRing LRing) (λ a → [ a ]) λ a b a-b∈I → eq/ a b a-b∈I)
        (rec (isSetRing RRing) (λ a → [ a ]) (λ a b a-b∈I → eq/ a b a-b∈I))
        (elimProp (λ _ → isSetRing LRing _ _) λ _ → refl)
        (elimProp (λ _ → isSetRing RRing _ _) (λ _ → refl)))
  IsRingHom.pres0 (snd CommForget/) = refl
  IsRingHom.pres1 (snd CommForget/) = refl
  IsRingHom.pres+ (snd CommForget/) = elimProp2 (λ _ _ → isSetRing RRing _ _) (λ _ _ → refl)
  IsRingHom.pres· (snd CommForget/) = elimProp2 (λ _ _ → isSetRing RRing _ _) (λ _ _ → refl)
  IsRingHom.pres- (snd CommForget/) = elimProp (λ _ → isSetRing RRing _ _) (λ _ → refl)

  open IsAlgebraHom
  inducedHom : (B : CommAlgebra R ℓ) (ϕ : CommAlgebraHom A B)
               → (fst I) ⊆ (fst (kernel A B ϕ))
               → CommAlgebraHom (A / I) B
  fst (inducedHom B ϕ I⊆kernel) =
    let open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
        instance
          _ : CommAlgebraStr R _
          _ = snd B
          _ : CommRingStr _
          _ = snd (CommAlgebra→CommRing B)
    in rec (isSetCommAlgebra B) (λ x → fst ϕ x)
        λ a b a-b∈I →
          equalByDifference
            (fst ϕ a) (fst ϕ b)
            ((fst ϕ a) - (fst ϕ b)     ≡⟨ cong (λ u → (fst ϕ a) + u) (sym (IsAlgebraHom.pres- (snd ϕ) _)) ⟩
             (fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
             fst ϕ (a - b)             ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
             0r ∎)
  pres0 (snd (inducedHom B ϕ kernel⊆I)) = pres0 (snd ϕ)
  pres1 (snd (inducedHom B ϕ kernel⊆I)) = pres1 (snd ϕ)
  pres+ (snd (inducedHom B ϕ kernel⊆I)) = elimProp2 (λ _ _ → isSetCommAlgebra B _ _) (pres+ (snd ϕ))
  pres· (snd (inducedHom B ϕ kernel⊆I)) = elimProp2 (λ _ _ → isSetCommAlgebra B _ _) (pres· (snd ϕ))
  pres- (snd (inducedHom B ϕ kernel⊆I)) = elimProp (λ _ → isSetCommAlgebra B _ _) (pres- (snd ϕ))
  pres⋆ (snd (inducedHom B ϕ kernel⊆I)) = λ r → elimProp (λ _ → isSetCommAlgebra B _ _) (pres⋆ (snd ϕ) r)

  injectivePrecomp : (B : CommAlgebra R ℓ) (f g : CommAlgebraHom (A / I) B)
                     → f ∘a (quotientHom A I) ≡ g ∘a (quotientHom A I)
                     → f ≡ g
  injectivePrecomp B f g p =
    Σ≡Prop
      (λ h → isPropIsAlgebraHom (CommRing→Ring R) (snd (CommAlgebra→Algebra (A / I))) h (snd (CommAlgebra→Algebra B)))
      (descendMapPath (fst f) (fst g) (isSetCommAlgebra B)
                      λ x → λ i → fst (p i) x)

{- trivial quotient -}
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
  open CommAlgebraStr (snd A)

  oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal A)) (UnitCommAlgebra R)
  fst oneIdealQuotient =
    isoToEquiv (iso (fst (terminalMap R (A / (1Ideal A))))
                    (λ _ → [ 0a ])
                    (λ _ → isPropUnit* _ _)
                    (elimProp (λ _ → squash/ _ _)
                              λ a → eq/ 0a a tt*))
  snd oneIdealQuotient = snd (terminalMap R (A / (1Ideal A)))

  zeroIdealQuotient : CommAlgebraEquiv A (A / (0Ideal A))
  fst zeroIdealQuotient =
    let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
    in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
                    (rec (isSetCommAlgebra A) (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
                    (elimProp (λ _ → squash/ _ _) λ _ → refl)
                    λ _ → refl)
  snd zeroIdealQuotient = snd (quotientHom A (0Ideal A))

[_]/ : {R : CommRing ℓ} {A : CommAlgebra R ℓ} {I : IdealsIn A}
       → (a : fst A) → fst (A / I)
[ a ]/ = [ a ]

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
  open CommIdeal using (isPropIsCommIdeal)

  private
    π = quotientHom A I

  kernel≡I : kernel A (A / I) π ≡ I
  kernel≡I =
    kernel A (A / I) π ≡⟨ Σ≡Prop
                            (isPropIsCommIdeal (CommAlgebra→CommRing A))
                            refl ⟩
    _                  ≡⟨  CommRing.kernel≡I {R = CommAlgebra→CommRing A} I ⟩
    I ∎

private
  module _ (R : CommRing ℓ) where
    open CommRingStr (snd R)
    lemma : (y : (fst R)) → y ≡ y - 0r
    lemma = solve R

isZeroFromIdeal : {R : CommRing ℓ} {A : CommAlgebra R ℓ} {I : IdealsIn A}
                  → (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
isZeroFromIdeal {A = A} {I = I} x x∈I = eq/ x 0a (subst (λ y → y ∈ (fst I)) step x∈I )
  where
    open CommAlgebraStr (snd A)
    step : x ≡ x - 0a
    step = lemma (CommAlgebra→CommRing A) x
    0' : ⟨ A / I ⟩
    0' = fst (quotientHom A I) 0a

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Fst {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as Wk hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Introductions.Pi

open import Tools.Product
import Tools.PropositionalEquality as PE

fst-subst* : ∀ {Γ F G t t′} → Γ ⊢ F → Γ ∙ F ⊢ G
             → Γ ⊢ t ⇒* t′ ∷ Σ F ▹ G → Γ ⊢ fst t ⇒* fst t′ ∷ F
fst-subst* ⊢F ⊢G (id x) = id (fstⱼ ⊢F ⊢G x)
fst-subst* ⊢F ⊢G (x ⇨ t⇒t′) = fst-subst ⊢F ⊢G x ⇨ fst-subst* ⊢F ⊢G t⇒t′

-- Reducibility of fst with a specific typing derivation
fst′ : ∀ {F G t Γ l l′}
       ([F] : Γ ⊩⟨ l′ ⟩ F)
       ([ΣFG] : Γ ⊩⟨ l ⟩B⟨ BΣ ⟩ Σ F ▹ G)
       ([t] : Γ ⊩⟨ l ⟩ t ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
       → Γ ⊩⟨ l′ ⟩ fst t ∷ F / [F]
fst′ {F = F} {t = t} {Γ = Γ} [F] (noemb (Bᵣ F' G' D ⊢F ⊢G A≡A [F'] [G'] G-ext))
     (Σₜ p d pProd p≅p [fstp] [sndp]) with
       B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let [fstp] : Γ ⊩⟨ _ ⟩ fst p ∷ F / [F]
      [fstp] = irrelevanceTerm′ (wk-id F)
                                ([F'] id (wf ⊢F)) [F]
                                [fstp]
  in  proj₁ (redSubst*Term (fst-subst* ⊢F ⊢G (redₜ d))
                           [F] [fstp])
fst′ {t = t} {Γ = Γ} {l = l} [F] (emb 0<1 x) [t] = fst′ [F] x [t]

-- Reducibility of fst with a general typing derivation
fst″ : ∀ {F G t Γ l l′}
       ([F] : Γ ⊩⟨ l′ ⟩ F)
       ([ΣFG] : Γ ⊩⟨ l ⟩ Σ F ▹ G)
       ([t] : Γ ⊩⟨ l ⟩ t ∷ Σ F ▹ G / [ΣFG])
       → Γ ⊩⟨ l′ ⟩ fst t ∷ F / [F]
fst″ {t = t} {Γ = Γ} {l = l} [F] [ΣFG] [t] =
  let [t]′ = irrelevanceTerm [ΣFG] (B-intr BΣ (Σ-elim [ΣFG])) [t]
  in  fst′ [F] (Σ-elim [ΣFG]) [t]′

fst-cong′ : ∀ {F G t t′ Γ l l′}
            ([F] : Γ ⊩⟨ l′ ⟩ F)
            ([ΣFG] : Γ ⊩⟨ l ⟩B⟨ BΣ ⟩ Σ F ▹ G)
            ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
            → Γ ⊩⟨ l′ ⟩ fst t ≡ fst t′ ∷ F / [F]
fst-cong′ {F = F} {G = G} {Γ = Γ} [F]
          [ΣFG]@(noemb (Bᵣ F' G' D ⊢F ⊢G A≡A [F'] [G'] G-ext))
          [t≡t′]@(Σₜ₌ p p′ d d′ pProd pProd′ p≅p′ [t] [t′] [fstp] [fstp′] [fst≡] [snd≡]) with
            B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let ⊢Γ = wf ⊢F
      [fstp]₁ = irrelevanceTerm′ (wk-id F) ([F'] id ⊢Γ) [F] [fstp]
      [fstp′]₁ = irrelevanceTerm′ (wk-id F) ([F'] id ⊢Γ) [F] [fstp′]
      [fst≡]₁ = irrelevanceEqTerm′ (wk-id F) ([F'] id ⊢Γ) [F] [fst≡]
      [fstt≡fstp] = proj₂ (redSubst*Term (fst-subst* ⊢F ⊢G (redₜ d)) [F] [fstp]₁)
      [fstt′≡fstp′] = proj₂ (redSubst*Term (fst-subst* ⊢F ⊢G (redₜ d′)) [F] [fstp′]₁)
  in  transEqTerm [F] [fstt≡fstp] (transEqTerm [F] [fst≡]₁ (symEqTerm [F] [fstt′≡fstp′]))
fst-cong′ [F] (emb 0<1 x) = fst-cong′ [F] x

-- Reducibility of congruence of fst
fst-cong″ : ∀ {F G t t′ Γ l l′}
            ([F] : Γ ⊩⟨ l′ ⟩ F)
            ([ΣFG] : Γ ⊩⟨ l ⟩ Σ F ▹ G)
            ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Σ F ▹ G / [ΣFG])
            → Γ ⊩⟨ l′ ⟩ fst t ≡ fst t′ ∷ F / [F]
fst-cong″ {F} {G} [F] [ΣFG] [t≡t′] =
  let [t≡t′] = irrelevanceEqTerm [ΣFG] (B-intr BΣ (Σ-elim [ΣFG])) [t≡t′]
  in  fst-cong′ [F] (Σ-elim [ΣFG]) [t≡t′]

fst-congᵛ : ∀ {F G t t′ Γ l}
            ([Γ] : ⊩ᵛ Γ)
            ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
            ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
            ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
            ([t′] : Γ ⊩ᵛ⟨ l ⟩ t′ ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
            ([t≡t′] : Γ ⊩ᵛ⟨ l ⟩ t ≡ t′ ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
          → Γ ⊩ᵛ⟨ l ⟩ fst t ≡ fst t′ ∷ F / [Γ] / [F]
fst-congᵛ {F} {G} [Γ] [F] [G] [t] [t′] [t≡t′] ⊢Δ [σ] =
  let [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G]
      ⊩σF = proj₁ ([F] ⊢Δ [σ])
      ⊩σΣFG = proj₁ ([ΣFG] ⊢Δ [σ])
      ⊩σt≡t′ = [t≡t′] ⊢Δ [σ]
  in  fst-cong″ ⊩σF ⊩σΣFG ⊩σt≡t′

-- Validity of first projection
fstᵛ : ∀ {F G t Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
       ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
       ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
       → Γ ⊩ᵛ⟨ l ⟩ fst t ∷ F / [Γ] / [F]
fstᵛ {F} {G} {t} {Γ} {l} [Γ] [F] [G] [t] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G]
      σfst : ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
           → Δ ⊩⟨ l ⟩ subst σ (fst t) ∷ subst σ F / proj₁ ([F] ⊢Δ [σ])
      σfst {Δ} {σ} ⊢Δ [σ] =
        let ⊩σF = proj₁ ([F] ⊢Δ [σ])
            ⊩σΣFG = proj₁ ([ΣFG] ⊢Δ [σ])
            ⊩σt = proj₁ ([t] ⊢Δ [σ])
        in  fst″ ⊩σF ⊩σΣFG ⊩σt

  in  σfst ⊢Δ [σ] ,
      (λ {σ′} [σ′] [σ≡σ′] →
        let [σF] = proj₁ ([F] ⊢Δ [σ])
            [σΣFG] = proj₁ ([ΣFG] ⊢Δ [σ])
            [σt≡σ′t] = proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]
        in  fst-cong″ [σF] [σΣFG] [σt≡σ′t])


text:
------------------------------------------------------------------------------
-- The LTC-PCF natural numbers type
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Type where

open import LTC-PCF.Base

------------------------------------------------------------------------------
-- The inductive predicate 'N' represents the type of the natural
-- numbers. They are a subset of 'D'.

-- The LTC-PCF natural numbers type (inductive predicate for total
-- natural numbers).
data N : D → Set where
  nzero :               N zero
  nsucc : ∀ {n} → N n → N (succ₁ n)

-- Induction principle for N (elimination rule).
N-ind : (A : D → Set) →
       A zero →
       (∀ {n} → A n → A (succ₁ n)) →
       ∀ {n} → N n → A n
N-ind A A0 h nzero      = A0
N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Data.Product using ( _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import FRP.LTL.ISet.Core using
  ( ISet ; I⟦_⟧ ; M⟦_⟧ ; ⟦_⟧ ; ⌈_⌉ ; splitM⟦_⟧ ; subsumM⟦_⟧ ; i→m ; m→i ) renaming
  ( [_] to [_]′ )
open import FRP.LTL.ISet.Stateless using ( _⇒_ ; _$_ )
open import FRP.LTL.Time.Bound using ( fin ; +∞ ; +∞-top ; ≼-refl ; _≼-trans_ ; _≼-total_ ; _≼-asym_ ; ≺-impl-⋡ )
open import FRP.LTL.Time.Interval using ( ↑ ; [_⟩; _⊑_ ; lb≺ub ; lb≼ ; _,_ ; Int )
open import FRP.LTL.Util using ( ≡-relevant ; ⊥-elim )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Unary using ( _∈_ )

module FRP.LTL.ISet.Globally where

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

□ : ISet → ISet
□ A = ⌈( λ t → M⟦ A ⟧ (↑ t) )⌉

-- Comonad structure of □

extend : ∀ {A B} → ⟦ A ⇒ B ⟧ → ⟦ □ A ⇒ □ B ⟧
extend {A} {B} f [ [ σ ]′ ]′ =
  [ (λ t t∈i → i→m (λ j j⊑↑t → f [ subsumM⟦ A ⟧ j (↑ t) j⊑↑t (σ t t∈i) ]′)) ]′

extract : ∀ {A} → ⟦ □ A ⇒ A ⟧
extract {A} {[_⟩ {fin s} {t} s≺t} [ [ σ ]′ ]′ =
  m→i (subsumM⟦ A ⟧ [ s≺t ⟩ (↑ s) (≼-refl , +∞-top) (σ s (≼-refl , s≺t)))
extract {A} {[_⟩ {+∞}    {t} ∞≺t} [ [ σ ]′ ]′ =
  ⊥-elim (≺-impl-⋡ ∞≺t +∞-top)

duplicate : ∀ {A} → ⟦ □ A ⇒ □ (□ A) ⟧
duplicate {A} [ [ σ ]′ ]′ =
  [ (λ t t∈i → [ (λ u u∈↑t → subsumM⟦ A ⟧ (↑ u) (↑ t) (lb≼ u∈↑t , ≼-refl) (σ t t∈i)) ]′) ]′

-- Applicative structure of □

[_] : ∀ {A} → ⟦ A ⟧ → ⟦ □ A ⟧
[ σ ] = [ (λ t t∈i → i→m (λ j j⊑↑t → σ)) ]′

_⟨*⟩_ : ∀ {A B} → ⟦ □ (A ⇒ B) ⇒ □ A ⇒ □ B ⟧
[ [ f ]′ ]′ ⟨*⟩ [ [ σ ]′ ]′ =
  [ (λ t t∈i → (f t t∈i) $ (σ t t∈i)) ]′

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
{- NEW TRANSLATION STUFF: same thing but interpret source nat as ♭nat-}

open import Preliminaries
open import Source
open import Complexity

module Translation where

  mutual
    ⟨⟨_⟩⟩ : Tp → CTp
    ⟨⟨ unit ⟩⟩ = unit
    ⟨⟨ nat ⟩⟩ = nat
    ⟨⟨ susp A ⟩⟩ = || A ||
    ⟨⟨ A ->s B ⟩⟩ = ⟨⟨ A ⟩⟩ ->c || B ||
    ⟨⟨ A ×s B ⟩⟩ = ⟨⟨ A ⟩⟩ ×c ⟨⟨ B ⟩⟩
    ⟨⟨ list A ⟩⟩ = list ⟨⟨ A ⟩⟩
    ⟨⟨ bool ⟩⟩ = bool

    ||_|| : Tp → CTp
    || τ || = C ×c ⟨⟨ τ ⟩⟩

  ⟨⟨_⟩⟩c : Source.Ctx → Complexity.Ctx
  ⟨⟨ [] ⟩⟩c = []
  ⟨⟨ x :: Γ ⟩⟩c = ⟨⟨ x ⟩⟩ :: ⟨⟨ Γ ⟩⟩c

  interp-Cost : ∀{Γ} → Cost → Γ Complexity.|- C
  interp-Cost 0c = 0C
  interp-Cost 1c = 1C
  interp-Cost (m +c n) = plusC (interp-Cost m) (interp-Cost n)

  lookup : ∀{Γ τ} → τ Source.∈ Γ → ⟨⟨ τ ⟩⟩ Complexity.∈ ⟨⟨ Γ ⟩⟩c
  lookup i0 = i0
  lookup (iS x) = iS (lookup x)

  _+C_ : ∀ {Γ τ} → Γ Complexity.|- C  → Γ Complexity.|- (C ×c τ)→ Γ Complexity.|- (C ×c τ)
  c +C e = prod (plusC c (l-proj e)) (r-proj e)

  -- translation from source expressions to complexity expressions
  ||_||e : ∀{Γ τ} → Γ Source.|- τ → ⟨⟨ Γ ⟩⟩c Complexity.|- || τ ||
  || unit ||e = prod 0C unit
  || var x ||e = prod 0C (var (lookup x))
  || z ||e = prod 0C z
  || suc e ||e = prod (l-proj (|| e ||e)) (s (r-proj (|| e ||e)))
  || rec e e0 e1 ||e = (l-proj (|| e ||e)) +C (rec (r-proj || e ||e) (1C +C || e0 ||e) (1C +C || e1 ||e))
  || lam e ||e = prod 0C (lam || e ||e)
  || app e1 e2 ||e =
    prod (plusC (plusC (plusC 1C (l-proj || e1 ||e)) (l-proj || e2 ||e)) (l-proj (app (r-proj || e1 ||e) (r-proj || e2 ||e))))
    (r-proj (app (r-proj || e1 ||e) (r-proj || e2 ||e)))
  || prod e1 e2 ||e = prod (plusC (l-proj (|| e1 ||e)) (l-proj (|| e2 ||e))) (prod (r-proj (|| e1 ||e)) (r-proj (|| e2 ||e)))
  || delay e ||e = prod 0C (|| e ||e)
  || force e ||e = prod (plusC (l-proj (|| e ||e)) (l-proj (r-proj || e ||e))) (r-proj (r-proj (|| e ||e)))
  || split e0 e1 ||e = prod (plusC (l-proj (|| e0 ||e)) (l-proj E1)) (r-proj E1)
    where E1 = (Complexity.subst || e1 ||e (Complexity.lem4 (l-proj (r-proj || e0 ||e)) (r-proj (r-proj || e0 ||e))))
  || nil ||e = prod 0C nil
  || e ::s e₁ ||e = prod (plusC (l-proj || e ||e) (l-proj || e₁ ||e)) ((r-proj || e ||e) ::c (r-proj || e₁ ||e))
  || listrec e e₁ e₂ ||e = l-proj || e ||e +C listrec (r-proj || e ||e) (1C +C || e₁ ||e) (1C +C || e₂ ||e)
  || true ||e = prod 0C true
  || false ||e = prod 0C false

  -- new translation with let bindings to reduce exponential increase in term size

  throw-s : ∀ {Γ Γ' τ} → Complexity.sctx Γ (τ :: Γ') → Complexity.sctx Γ Γ'
  throw-s Θ x = Θ (iS x)

  _+C'_ : ∀ {Γ τ} → Γ Complexity.|- C  → Γ Complexity.|- (C ×c τ)→ Γ Complexity.|- (C ×c τ)
  c +C' e = letc (prod (plusC (Complexity.wkn c) (l-proj (var i0))) (r-proj (var i0))) e

  ||_||e' : ∀{Γ τ} → Γ Source.|- τ → ⟨⟨ Γ ⟩⟩c Complexity.|- || τ ||
  || unit ||e' = prod 0C unit
  || var x ||e' = prod 0C (var (lookup x))
  || z ||e' = prod 0C z
  || suc e ||e' = (letc (prod (l-proj (var i0)) (s (r-proj (var i0)))) || e ||e')
--  || rec e e0 e1 ||e = (l-proj (|| e ||e)) +C (rec (r-proj || e ||e) (1C +C || e0 ||e) (1C +C || e1 ||e))
  || rec e e0 e1 ||e' =
      letc (l-proj (var i0) +C' rec (r-proj (var i0))
                   (Complexity.wkn (1C +C' || e0 ||e'))
                   (Complexity.subst (1C +C' || e1 ||e') (Complexity.s-extend (Complexity.s-extend (throw-s Complexity.ids)))))
           || e ||e'
  || lam e ||e' = prod 0C (lam || e ||e')
  || app e1 e2 ||e' = letc (letc (prod (plusC (plusC (plusC 1C (l-proj (var (iS i0)))) (l-proj (var i0))) (l-proj (app (r-proj (var (iS i0))) (r-proj (var i0)))))
                            (r-proj (app (r-proj (var (iS i0))) (r-proj (var i0))))) (Complexity.wkn || e2 ||e')) || e1 ||e'
  || prod e1 e2 ||e' = letc (letc (prod (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (prod (r-proj (var (iS i0))) (r-proj (var i0)))) (Complexity.wkn || e2 ||e')) || e1 ||e'
  || delay e ||e' = prod 0C || e ||e'
  || force e ||e' = letc (prod (plusC (l-proj (var i0)) (l-proj (r-proj (var i0)))) (r-proj (r-proj (var i0)))) || e ||e'
  || split e0 e1 ||e' = letc (prod (plusC (Complexity.wkn (l-proj || e0 ||e')) (l-proj (var i0))) (r-proj (var i0))) E1
       where E1 = letc (Complexity.subst || e1 ||e' (Complexity.lem4 (l-proj (r-proj (var i0))) (r-proj (r-proj (var i0))) Complexity.ss Complexity.s-extend (Complexity.s-extend (throw-s Complexity.ids)))) || e0 ||e'
  || nil ||e' = prod 0C nil
  || e ::s e₁ ||e' = letc (letc (prod (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (r-proj (var (iS i0)) ::c r-proj (var i0))) (Complexity.wkn || e₁ ||e')) || e ||e'
  || listrec e e₁ e₂ ||e' =
      letc (l-proj (var i0) +C' listrec (r-proj (var i0))
        (Complexity.wkn (1C +C' || e₁ ||e')) (Complexity.subst (1C +C' || e₂ ||e') (Complexity.s-extend (Complexity.s-extend (Complexity.s-extend (throw-s Complexity.ids)))))) || e ||e'
  || true ||e' = prod 0C true
  || false ||e' = prod 0C false

{- try prove ||.||old <=/=> ||.||new

  trans-eq-l : ∀ {Γ τ} → (e : Γ Source.|- τ) → || e ||e ≤s || e ||e'
  trans-eq-l unit = refl-s
  trans-eq-l (var x) = refl-s
  trans-eq-l z = refl-s
  trans-eq-l (suc e) = (cong-prod (cong-lproj (trans-eq-l e)) (cong-suc (cong-rproj (trans-eq-l e))) trans lam-s) trans letc-app-r
  trans-eq-l (rec e e₁ e₂) = {!!}
  trans-eq-l (lam e) = cong-prod refl-s (cong-lam (trans-eq-l e))
  trans-eq-l (app e e₁) = {!!}
  trans-eq-l (prod e e₁) = (((cong-prod (cong-+ (cong-lproj {!!}) (cong-lproj {!!})) {!!} trans lam-s) trans letc-app-r) trans lam-s) trans letc-app-r
  trans-eq-l (delay e) = {!!}
  trans-eq-l (force e) = {!!}
  trans-eq-l (split e e₁) = {!!}
  trans-eq-l nil = {!!}
  trans-eq-l (e ::s e₁) = {!!}
  trans-eq-l (listrec e e₁ e₂) = {!!}
  trans-eq-l true = refl-s
  trans-eq-l false = refl-s
-}

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

data U : ∀ t → Set
data T t : Set


text:
module Quantifiers where

-- Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
-- open import plfa.part1.Isomorphism using (_≃_; extensionality)

-- 同型 (isomorphism)
infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- Universals

-- 全称量化子の除去則
∀-elim : ∀ {A : Set} {B : A → Set}
  → (L : ∀ (x : A) → B x)
  → (M : A)
    ---------------------
  → B M
∀-elim L M = L M

-- Existentials

-- 依存和型 (dependent sum type)
data Σ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩ : (x : A) → B x → Σ A B

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

record Σ′ (A : Set) (B : A → Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B proj₁′

-- 存在量化子 (existential quantifier)
∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

-- 存在量化子の除去則
∃-elim : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ x → B x → C)
  → ∃[ x ] B x
    ---------------
  → C
∃-elim f ⟨ x , y ⟩ = f x y

∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ x → B x → C) ≃ (∃[ x ] B x → C)
∀∃-currying =
  record
    { to      = λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
    ; from    = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
    ; from∘to = λ{ f → refl }
    ; to∘from = λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }}
    }

-- An existential example

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    m * 2 ≡ n)
odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + m * 2 ≡ n)

even-∃ even-zero                      = ⟨ zero , refl ⟩
even-∃ (even-suc o) with odd-∃ o
...                    | ⟨ m , refl ⟩ = ⟨ suc m , refl ⟩

odd-∃  (odd-suc e)  with even-∃ e
...                    | ⟨ m , refl ⟩ = ⟨ m , refl ⟩

∃-even : ∀ {n : ℕ} → ∃[ m ] (    m * 2 ≡ n) → even n
∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) →  odd n

∃-even ⟨  zero , refl ⟩ = even-zero
∃-even ⟨ suc m , refl ⟩ = even-suc (∃-odd ⟨ m , refl ⟩)

∃-odd  ⟨     m , refl ⟩ = odd-suc (∃-even ⟨ m , refl ⟩)

-- Existentials, Universals, and Negation

-- B(x)が成り立たないxが存在することと、任意のxについてB(x)が成り立たないことは同型
¬∃≃∀¬ : ∀ {A : Set} {B : A → Set}
  → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x
¬∃≃∀¬ =
  record
    { to      = λ{ ¬∃xy x y → ¬∃xy ⟨ x , y ⟩ }
    ; from    = λ{ ∀¬xy ⟨ x , y ⟩ → ∀¬xy x y }
    ; from∘to = λ{ ¬∃xy → extensionality λ{ ⟨ x , y ⟩ → refl } }
    ; to∘from = λ{ ∀¬xy → refl }
    }

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
infixr 2 _×_
infixr 2 _,_
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

data W (A : Set) (B : A → Set) : Set where
  sup : (x : A) → ((p : B x) → W A B) → W A B

-- Should be able to get φ (λ x → (k x) , rec φ (k x)))
-- just using refine.
rec : ∀ {S P}{X : Set} → (Σ[ s ∶ S ] (P s → W S P × X) → X) → W S P → X
rec φ (sup s k) = {!!}

postulate
  A : Set
  a : A

-- Refine hole as far as possible.
-- Should get: (? , ?) , (λ x → ?) , λ x → ?
test-refine : (A × A) × (A → A) × (A → A)
test-refine = {!!}