text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Naturals.Order.WellFounded
open import KeyValue.KeyValue
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Vectors
open import Maybe
open import Semirings.Definition
open import Numbers.Naturals.EuclideanAlgorithm

module Numbers.Primes.PrimeNumbers where

open TotalOrder ℕTotalOrder
open Semiring ℕSemiring
open import Decidable.Lemmas ℕDecideEquality

dividesEqualityLemma'' : {a b : ℕ} → (quot1 quot2 : ℕ) → .(quot1 ≡ quot2) → (rem : ℕ) → .(pr1 : (quot1 +N a *N quot1) +N rem ≡ b) → .(pr2 : (quot2 +N a *N quot2) +N rem ≡ b) → (y : rem <N' succ a) → (x1 : zero <N' succ a) → _≡_ {A = divisionAlgResult' _ _} record { quot = quot1 ; rem = rem ; pr = pr1 ; remIsSmall = inl y ; quotSmall = inl x1 } record { quot = quot2 ; rem = rem ; pr = pr2 ; remIsSmall = inl y ; quotSmall = inl x1}
dividesEqualityLemma'' {a} {b} q1 q2 pr rem pr1 pr2 y x1 with squashN record { eq = pr }
... | refl = refl

dividesEqualityLemma' : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem : ℕ) → .(pr1 : (quot1 +N a *N quot1) +N rem ≡ b) → .(pr2 : (quot2 +N a *N quot2) +N rem ≡ b) → (y : rem <N' succ a) → (y2 : rem <N' succ a) → (x1 : zero <N' succ a) → _≡_ {A = divisionAlgResult' _ _} record { quot = quot1 ; rem = rem ; pr = pr1 ; remIsSmall = inl y ; quotSmall = inl x1 } record { quot = quot2 ; rem = rem ; pr = pr2 ; remIsSmall = inl y2 ; quotSmall = inl x1}
dividesEqualityLemma' {a} {b} quot1 quot2 rem pr1 pr2 y y2 x1 with productCancelsLeft (succ a) quot2 quot1 (succIsPositive a) (canSubtractFromEqualityRight (transitivity (squashN record { eq = pr2 }) (equalityCommutative (squashN record { eq = pr1 }))))
... | refl with <N'Refl y y2
... | refl = refl

dividesEqualityLemma : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem1 rem2 : ℕ) → .(pr1 : (quot1 +N a *N quot1) +N rem1 ≡ b) → .(pr2 : (quot2 +N a *N quot2) +N rem2 ≡ b) → .(rem1 ≡ rem2) → (y : rem1 <N' succ a) → (y2 : rem2 <N' succ a) → (x1 : zero <N' succ a) → _≡_ {A = divisionAlgResult' _ _} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = inl y ; quotSmall = inl x1 } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = inl y2 ; quotSmall = inl x1}
dividesEqualityLemma {a} {b} quot1 quot2 rem1 rem2 pr1 pr2 remEq y y2 x1 with squashN record { eq = remEq }
... | refl = dividesEqualityLemma' quot1 quot2 rem1 pr1 pr2 y y2 x1

dividesEqualityLemma1 : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem1 rem2 : ℕ) → .(pr1 : (quot1 +N a *N quot1) +N rem1 ≡ b) → .(pr2 : (quot2 +N a *N quot2) +N rem2 ≡ b) → .(rem1 ≡ rem2) → (y : (rem1 <N' succ a) || (succ a =N' zero)) → (y2 : (rem2 <N' succ a) || (succ a =N' zero)) → (x1 : zero <N' succ a) → _≡_ {A = divisionAlgResult' _ _} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = y ; quotSmall = inl x1 } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = y2 ; quotSmall = inl x1}
dividesEqualityLemma1 {a} {b} quot1 quot2 rem1 rem2 pr1 pr2 remEq (inl x) (inl y) x1 = dividesEqualityLemma quot1 quot2 rem1 rem2 pr1 pr2 remEq x y x1

dividesEqualityLemma2 : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem1 rem2 : ℕ) → .(pr1 : (quot1 +N a *N quot1) +N rem1 ≡ b) → .(pr2 : (quot2 +N a *N quot2) +N rem2 ≡ b) → .(rem1 ≡ rem2) → (y : (rem1 <N' succ a) || (succ a =N' zero)) → (y2 : (rem2 <N' succ a) || (succ a =N' zero)) → (x1 : zero <N' succ a) (x2 : zero <N' succ a) → _≡_ {A = divisionAlgResult' _ _} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = y ; quotSmall = inl x1 } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = y2 ; quotSmall = inl x2 }
dividesEqualityLemma2 {a} {b} quot1 quot2 rem1 rem2 pr1 pr2 remEq x y x1 x2 with <N'Refl x1 x2
... | refl = dividesEqualityLemma1 quot1 quot2 rem1 rem2 pr1 pr2 remEq x y x1

dividesEqualityLemma3 : {a b : ℕ} → (quot1 quot2 : ℕ) → (rem1 rem2 : ℕ) → .(pr1 : (succ a *N quot1) +N rem1 ≡ b) → .(pr2 : (succ a *N quot2) +N rem2 ≡ b) → .(rem1 ≡ rem2) → (y : (rem1 <N' succ a) || (succ a =N' zero)) → (y2 : (rem2 <N' succ a) || (succ a =N' zero)) → (x1 : (zero <N' succ a) || (zero =N' succ a) && (quot1 =N' zero)) (x2 : (zero <N' succ a) || (zero =N' succ a) && (quot2 =N' zero)) → _≡_ {A = divisionAlgResult' _ _} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = y ; quotSmall = x1 } record { quot = quot2 ; rem = rem2 ; pr = pr2 ; remIsSmall = y2 ; quotSmall = x2 }
dividesEqualityLemma3 {a} {b} quot1 quot2 rem1 rem2 pr1 pr2 remEq x y (inl x1) (inl x2) = dividesEqualityLemma2 quot1 quot2 rem1 rem2 pr1 pr2 remEq x y x1 x2

dividesEqualityPr' : {a b : ℕ} → (res1 res2 : divisionAlgResult' a b) → res1 ≡ res2
dividesEqualityPr' {zero} {zero} record { quot = quot₁ ; rem = rem₁ ; pr = pr1 ; remIsSmall = (inr f2) ; quotSmall = (inr (f4 ,, quot1=0)) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr f1) ; quotSmall = (inr (f3 ,, quot=0)) } with squashN quot1=0
... | refl with squashN quot=0
... | refl with =N'Refl f1 f2
... | refl with =N'Refl f3 f4
... | refl with =N'Refl quot1=0 quot=0
... | refl with transitivity (squashN record { eq = pr }) (equalityCommutative (squashN record { eq = pr1 }))
... | refl = refl
dividesEqualityPr' {zero} {succ b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inr rSm) ; quotSmall = (inr (f ,, quot1=0)) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr rSm2) ; quotSmall = (inr (f2 ,, quot=0)) } with squashN quot=0
... | refl with squashN quot1=0
... | refl with =N'Refl rSm rSm2
... | refl with =N'Refl quot1=0 quot=0
... | refl with =N'Refl f f2
... | refl with transitivity (squashN record { eq = pr }) (equalityCommutative (squashN record { eq = pr1 }))
... | refl = refl
dividesEqualityPr' {succ a} {zero} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inl remSm) ; quotSmall = (inl qSm) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl remSm2) ; quotSmall = (inl qSm2) } with sumZeroImpliesSummandsZero {quot +N a *N quot} {rem} (squashN record { eq = pr })
... | fst ,, refl with sumZeroImpliesSummandsZero {quot} {_} fst
... | refl ,, _ with sumZeroImpliesSummandsZero {_} {rem1} (squashN record { eq = pr1 })
... | fst2 ,, refl with sumZeroImpliesSummandsZero {quot1} {_} fst2
... | refl ,, _ with <N'Refl remSm remSm2
... | refl with <N'Refl qSm qSm2
... | refl = refl
dividesEqualityPr' {succ a} {succ b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = inl remIsSmall1 ; quotSmall = inl (quotSmall1) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = (inl quotSmall) } = dividesEqualityLemma3 quot1 quot rem1 rem pr1 pr t (inl remIsSmall1) (inl remIsSmall) (inl quotSmall1) (inl quotSmall)
  where
    t : rem1 ≡ rem
    t = modIsUnique record { quot = quot1 ; rem = rem1 ; pr = squash pr1 ; remIsSmall = inl (<N'To<N remIsSmall1) ; quotSmall = inl (<N'To<N quotSmall) } record { quot = quot ; rem = rem ; pr = squash pr ; remIsSmall = inl (<N'To<N remIsSmall) ; quotSmall = inl (<N'To<N quotSmall1) }

dividesEquality : {a b : ℕ} → (res1 res2 : a ∣' b) → res1 ≡ res2
dividesEquality (divides' res1 x1) (divides' res2 x2) with dividesEqualityPr' res1 res2
... | refl = refl

data notDiv : ℕ → ℕ → Set where
  doesNotDivide : {a b : ℕ} → (res : divisionAlgResult a b) → 0 <N divisionAlgResult.rem res → notDiv a b

twoDividesFour : succ (succ zero) ∣ succ (succ (succ (succ zero)))
twoDividesFour = divides {(succ (succ zero))} {succ (succ (succ (succ zero)))} (record { quot = succ (succ zero) ; rem = zero ; pr = refl ; remIsSmall = inl (succIsPositive 1) ; quotSmall = inl (succIsPositive 1) }) refl

record Prime (p : ℕ) : Set where
  field
    p>1 : 1 <N p
    pr : forall {i : ℕ} → i ∣ p → i <N p → zero <N i → i ≡ (succ zero)

record Composite (n : ℕ) : Set where
  field
    n>1 : 1 <N n
    divisor : ℕ
    dividesN : divisor ∣ n
    divisorLessN : divisor <N n
    divisorNot1 : 1 <N divisor
    divisorPrime : Prime divisor
    noSmallerDivisors : ∀ i → i <N divisor → 1 <N i → i ∣ n → False

notBothPrimeAndComposite : {n : ℕ} → Composite n → Prime n → False
notBothPrimeAndComposite {n} record { n>1 = n>1 ; divisor = divisor ; dividesN = dividesN ; divisorLessN = divisorLessN ; divisorNot1 = divisorNot1 } record { p>1 = p>1 ; pr = pr } = lessImpliesNotEqual divisorNot1 (equalityCommutative div=1)
  where
    div=1 : divisor ≡ 1
    div=1 = pr {divisor} dividesN divisorLessN (TotalOrder.<Transitive ℕTotalOrder (succIsPositive 0) divisorNot1)

zeroIsNotPrime : Prime 0 → False
zeroIsNotPrime record { p>1 = p>1 ; pr = pr } = zeroNeverGreater p>1

oneIsNotPrime : Prime 1 → False
oneIsNotPrime record { p>1 = (le x proof) ; pr = pr } = naughtE (equalityCommutative absurd')
  where
    absurd : x +N 1 ≡ 0
    absurd = succInjective proof
    absurd' : succ x ≡ 0
    absurd' rewrite Semiring.commutative ℕSemiring 1 x = absurd

twoIsPrime : Prime 2
Prime.p>1 twoIsPrime = succPreservesInequality (succIsPositive 0)
Prime.pr twoIsPrime {i} i|2 i<2 0<i with totality i (succ (succ zero))
Prime.pr twoIsPrime {zero} i|2 i<2 (le x ()) | order
Prime.pr twoIsPrime {succ zero} i|2 i<2 0<i | order = refl
Prime.pr twoIsPrime {succ (succ zero)} i|2 i<2 0<i | order = exFalso (lessImpliesNotEqual {2} i<2 refl)
Prime.pr twoIsPrime {succ (succ (succ i))} i|2 i<2 0<i | inl (inl x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder i<2 (succPreservesInequality (succPreservesInequality (succIsPositive i)))))
Prime.pr twoIsPrime {succ (succ (succ i))} i|2 i<2 0<i | inl (inr twoLessThree) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder twoLessThree i<2))
Prime.pr twoIsPrime {succ (succ (succ i))} i|2 i<2 0<i | inr ()

threeIsPrime : Prime 3
Prime.p>1 threeIsPrime = le 1 refl
Prime.pr threeIsPrime {succ zero} i|3 i<3 _ = refl
Prime.pr threeIsPrime {succ (succ zero)} (divides record { quot = (succ (succ (succ zero))) ; rem = zero ; pr = () ; remIsSmall = remIsSmall ; quotSmall = quotSmall } x) i<3 _
Prime.pr threeIsPrime {succ (succ zero)} (divides record { quot = (succ (succ (succ (succ quot)))) ; rem = zero ; pr = () ; remIsSmall = remIsSmall ; quotSmall = quotSmall } x) i<3 _
Prime.pr threeIsPrime {succ (succ (succ i))} i|3 (le (succ (succ zero)) ()) _
Prime.pr threeIsPrime {succ (succ (succ i))} i|3 (le (succ (succ (succ x))) ()) _

compositeImpliesNotPrime : (m p : ℕ) → (succ zero <N m) → (m <N p) → (m ∣ p) → Prime p → False
compositeImpliesNotPrime zero p (le x ()) _ mDivP pPrime
compositeImpliesNotPrime (succ zero) p mLarge _ mDivP pPrime = lessImpliesNotEqual {succ zero} {succ zero} mLarge refl
compositeImpliesNotPrime (succ (succ m)) zero _ _ mDivP ()
compositeImpliesNotPrime (succ (succ m)) (succ zero) _ _ mDivP primeP = exFalso (oneIsNotPrime primeP)
compositeImpliesNotPrime (succ (succ m)) (succ (succ p)) _ mLessP mDivP pPrime = false
  where
    r = succ (succ m)
    q = succ (succ p)
    rEqOne : r ≡ succ zero
    rEqOne = (Prime.pr pPrime) {r} mDivP mLessP (succIsPositive (succ m))
    false : False
    false = succIsNonzero (succInjective rEqOne)

fourIsNotPrime : Prime 4 → False
fourIsNotPrime = compositeImpliesNotPrime (succ (succ zero)) (succ (succ (succ (succ zero)))) (le zero refl) (le (succ zero) refl) twoDividesFour

record Coprime (a : ℕ) (b : ℕ) : Set where
  field
    hcf : hcfData a b
    hcfNot1 : 1 <N hcfData.c hcf

record numberLessThan (n : ℕ) : Set where
  field
    a : ℕ
    a<n : a <N' n
  upper : ℕ
  upper = n

numberLessThanEquality : {n : ℕ} → (a b : numberLessThan n) → (numberLessThan.a a ≡ numberLessThan.a b) → a ≡ b
numberLessThanEquality record { a = a ; a<n = a<n } record { a = b ; a<n = b<n } pr rewrite pr | <N'Refl a<n b<n = refl

numberLessThanOrder : (n : ℕ) → TotalOrder (numberLessThan n)
PartialOrder._<_ (TotalOrder.order (numberLessThanOrder n)) = λ a b → (numberLessThan.a a) <N numberLessThan.a b
PartialOrder.irreflexive (TotalOrder.order (numberLessThanOrder n)) pr = TotalOrder.irreflexive ℕTotalOrder pr
PartialOrder.<Transitive (TotalOrder.order (numberLessThanOrder n)) pr1 pr2 = TotalOrder.<Transitive ℕTotalOrder pr1 pr2
TotalOrder.totality (numberLessThanOrder n) a b with totality (numberLessThan.a a) (numberLessThan.a b)
TotalOrder.totality (numberLessThanOrder n) a b | inl (inl x) = inl (inl x)
TotalOrder.totality (numberLessThanOrder n) a b | inl (inr x) = inl (inr x)
TotalOrder.totality (numberLessThanOrder n) a b | inr x rewrite x = inr (numberLessThanEquality a b x)

numberLessThanInject : {newMax : ℕ} → (max : ℕ) → (n : numberLessThan max) → (max <N newMax) → (numberLessThan newMax)
numberLessThanInject max record { a = n ; a<n = n<max } max<newMax = record { a = n ; a<n = <NTo<N' (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (<N'To<N n<max) max<newMax) }

numberLessThanInjectComp : {max : ℕ} (a b : ℕ) → (i : numberLessThan b) → (pr : b <N a) → (pr2 : a <N max) → numberLessThanInject {max} a (numberLessThanInject {a} b i pr) pr2 ≡ numberLessThanInject {max} b i (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) pr pr2)
numberLessThanInjectComp {max} a b record { a = i ; a<n = i<max } b<a a<max = numberLessThanEquality _ _ refl

allNumbersLessThanDescending : (n : ℕ) → Vec (numberLessThan n) n
allNumbersLessThanDescending zero = []
allNumbersLessThanDescending (succ n) = record { a = n ; a<n = <NTo<N' (le zero refl) } ,- vecMap (λ i → numberLessThanInject {succ n} (numberLessThan.upper i) i (le zero refl)) (allNumbersLessThanDescending n)

allNumbersLessThan : (n : ℕ) → Vec (numberLessThan n) n
allNumbersLessThan n = vecRev (allNumbersLessThanDescending n)

maxDivides : (a b : ℕ) → ((TotalOrder.max ℕTotalOrder a b) ∣ a) → (TotalOrder.max ℕTotalOrder a b) ∣ b → (((a ≡ 0) && (0 <N b)) || ((b ≡ 0) && (0 <N a))) || (a ≡ b)
maxDivides a b max|a max|b with totality a b
maxDivides a b max|a max|b | inl (inl a<b) = inl (inl (record { fst = gg ; snd = identityOfIndiscernablesLeft _<N_ a<b gg}))
  where
    gg : a ≡ 0
    gg = biggerThanCantDivideLemma {a} {b} a<b max|a
maxDivides a b max|a max|b | inl (inr b<a) = inl (inr (record { fst = gg ; snd = identityOfIndiscernablesLeft _<N_ b<a gg }))
  where
    gg : b ≡ 0
    gg = biggerThanCantDivideLemma b<a max|b
maxDivides a .a a|max b|max | inr refl = inr refl

{-
hcfsEquivalent' : {a b : ℕ} → extensionalHCF a b → hcfData a b
hcfData.c (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) = c
hcfData.c|a (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) = c|a
hcfData.c|b (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) = c|b
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcfExtension = hcfExtension }) x x|a x|b with totality ℕTotalOrder x c
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = zeroCase ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = hIRL }) x x|a x|b | inl (inl x<c) = {!!}
  where
    xLess : numberLessThan c
    xLess = record { a = x ; a<n = x<c }
    pair : Set
    pair = Sg (numberLessThan c) (λ i → (notDiv (numberLessThan.a i) a || notDiv (numberLessThan.a i) b) || (numberLessThan.a i ∣ a) & numberLessThan.a i ∣ b & (numberLessThan.a i ∣ c))
    pr : Sg pair λ p → (lookup (MapWithDomain.map hcfExtension) xLess ≡ {!!})
    pr = MapWithDomain.lookup' hcfExtension xLess (hcfsContains {a} {b} {x} (record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = zeroCase ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = hIRL }) x<c)
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = _ ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = _ }) x x|a x|b | inl (inr c<x) = {!!}
hcfData.hcf (hcfsEquivalent' {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; zeroCase = _ ; hcfExtension = hcfExtension ; hcfExtensionIsRightLength = _ }) x x|a x|b | inr x=c rewrite x=c = aDivA c

extensionalHCFEquality : {a b : ℕ} → {h1 h2 : extensionalHCF a b} → (extensionalHCF.c h1 ≡ extensionalHCF.c h2) → h1 ≡ h2
extensionalHCFEquality {a} {b} {record { c = c1 ; c|a = c|a1 ; c|b = c|b1 ; hcfExtension = hcfExtension1 }} {record { c = c2 ; c|a = c|a2 ; c|b = c|b2 ; hcfExtension = hcfExtension2 }} pr rewrite pr = {!!}
-}

divisorIsSmaller : {a b : ℕ} → a ∣ succ b → succ b <N a → False
divisorIsSmaller {a} {b} (divides record { quot = zero ; rem = .0 ; pr = pr } refl) sb<a rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) = go
  where
    go : False
    go rewrite Semiring.productZeroRight ℕSemiring a = naughtE pr
divisorIsSmaller {a} {b} (divides record { quot = (succ quot) ; rem = .0 ; pr = pr } refl) sb<a rewrite Semiring.sumZeroRight ℕSemiring (a *N succ quot) = go
  where
    go : False
    go rewrite equalityCommutative pr = go'
      where
        go' : False
        go' rewrite multiplicationNIsCommutative a (succ quot) = cannotAddAndEnlarge' sb<a

primeDivisorIs1OrP : {a p : ℕ} → (prime : Prime p) → (a ∣ p) → (a ≡ 1) || (a ≡ p)
primeDivisorIs1OrP {zero} {zero} prime a|p = inr refl
primeDivisorIs1OrP {zero} {succ p} prime a|p = exFalso (zeroDividesNothing p a|p)
primeDivisorIs1OrP {succ zero} {p} prime a|p = inl refl
primeDivisorIs1OrP {succ (succ a)} {p} prime a|p with totality (succ (succ a)) p
primeDivisorIs1OrP {succ (succ a)} {p} prime a|p | inl (inl ssa<p) = go p prime a|p ssa<p
  where
    go : (n : ℕ) → Prime n → succ (succ a) ∣ n → succ (succ a) <N n → (succ (succ a) ≡ 1) || (succ (succ a) ≡ p)
    go zero pr x|n n<n = exFalso (zeroIsNotPrime pr)
    go (succ zero) pr x|n n<n = exFalso (oneIsNotPrime pr)
    go (succ (succ n)) pr x|n n<n = inl ((Prime.pr pr) {succ (succ a)} x|n n<n (succIsPositive (succ a)))
primeDivisorIs1OrP {succ (succ a)} {zero} prime a|p | inl (inr x) = exFalso (zeroIsNotPrime prime)
primeDivisorIs1OrP {succ (succ a)} {succ p} prime a|p | inl (inr x) = exFalso (divisorIsSmaller {succ (succ a)} {p} a|p x)
primeDivisorIs1OrP {succ (succ a)} {p} prime a|p | inr x = inr x

hcfPrimeIsOne' : {p : ℕ} → {a : ℕ} → (Prime p) → (0 <N divisionAlgResult.rem (divisionAlg p a)) → (extendedHcf.c (euclid a p) ≡ 1) || (extendedHcf.c (euclid a p) ≡ p)
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA with euclid a p
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } with divisionAlg p a
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } | record { quot = quot ; rem = rem ; pr = prPDivA } with primeDivisorIs1OrP pPrime hcf|p
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } | record { quot = quot ; rem = rem ; pr = prPDivA } | inl x = inl x
hcfPrimeIsOne' {p} {a} pPrime pCoprimeA | record { hcf = record { c = hcf ; c|a = hcf|a ; c|b = hcf|p ; hcf = hcfPr } } | record { quot = quot ; rem = rem ; pr = prPDivA } | inr x = inr x

divisionDecidable : (a b : ℕ) → (a ∣ b) || ((a ∣ b) → False)
divisionDecidable zero zero = inl (aDivA zero)
divisionDecidable zero (succ b) = inr f
  where
    f : zero ∣ succ b → False
    f (divides record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall } x) rewrite x = naughtE pr
divisionDecidable (succ a) b with divisionAlg (succ a) b
divisionDecidable (succ a) b | record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remSmall } = inl (divides (record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remSmall ; quotSmall = inl (succIsPositive a) }) refl)
divisionDecidable (succ a) b | record { quot = b/a ; rem = succ rem ; pr = prANotDivB ; remIsSmall = inr p } = exFalso (naughtE (equalityCommutative p))
divisionDecidable (succ a) b | record { quot = b/a ; rem = succ rem ; pr = prANotDivB ; remIsSmall = inl p } = inr f
  where
    f : (succ a) ∣ b → False
    f (divides record { quot = b/a' ; rem = .0 ; pr = pr } refl) rewrite Semiring.sumZeroRight ℕSemiring ((succ a) *N b/a') = naughtE (modUniqueLemma {zero} {succ rem} {succ a} b/a' b/a (succIsPositive a) p comp')
      where
        comp : (succ a) *N b/a' ≡ (succ a) *N b/a +N succ rem
        comp = transitivity pr (equalityCommutative prANotDivB)
        comp' : (succ a) *N b/a' +N zero ≡ (succ a) *N b/a +N succ rem
        comp' rewrite Semiring.sumZeroRight ℕSemiring (succ a *N b/a') = comp

doesNotDivideImpliesNonzeroRem : (a b : ℕ) → ((a ∣ b) → False) → 0 <N divisionAlgResult.rem (divisionAlg a b)
doesNotDivideImpliesNonzeroRem a b pr with divisionAlg a b
doesNotDivideImpliesNonzeroRem a b pr | record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall } with zeroIsValidRem rem
doesNotDivideImpliesNonzeroRem a b pr | record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall } | inl x = x
doesNotDivideImpliesNonzeroRem a b pr | record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } | inr x = exFalso (pr aDivB)
  where
    aDivB : a ∣ b
    aDivB = divides (record { quot = quot ; rem = rem ; pr = divAlgPr ; remIsSmall = remIsSmall ; quotSmall = quotSmall }) x

hcfPrimeIsOne : {p : ℕ} → {a : ℕ} → (Prime p) → ((p ∣ a) → False) → extendedHcf.c (euclid a p) ≡ 1
hcfPrimeIsOne {p} {a} pPrime pr with hcfPrimeIsOne' {p} {a} pPrime (doesNotDivideImpliesNonzeroRem p a pr)
hcfPrimeIsOne {p} {a} pPrime pr | inl x = x
hcfPrimeIsOne {p} {a} pPrime pr | inr x with euclid a p
hcfPrimeIsOne {p} {a} pPrime pr | inr x | record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = extendedProof } rewrite x = exFalso (pr c|a)

reduceEquationMod : {a b c : ℕ} → (d : ℕ) → (a ∣ b) → (a ∣ c) → b ≡ c +N d → a ∣ d
reduceEquationMod {a} {b} {c} 0 a|b a|c pr = aDivZero a
reduceEquationMod {a} {b} {c} (succ d) (divides record { quot = b/a ; rem = .0 ; pr = prb/a ; remIsSmall = r1 ; quotSmall = qSm1 } refl) (divides record { quot = c/a ; rem = .0 ; pr = prc/a ; remIsSmall = r2 ; quotSmall = qSm2 } refl) b=c+d = identityOfIndiscernablesRight _∣_ a|b-c ex
  where
    c<b : c <N b
    c<b rewrite succExtracts c d | Semiring.commutative ℕSemiring c d = le d (equalityCommutative b=c+d)
    a|b-c : a ∣ subtractionNResult.result (-N (inl c<b))
    a|b-c = dividesBothImpliesDividesDifference (divides record { quot = b/a ; rem = 0 ; pr = prb/a ; remIsSmall = r1 ; quotSmall = qSm1 } refl) (divides record { quot = c/a ; rem = 0 ; pr = prc/a ; remIsSmall = r2 ; quotSmall = qSm2 } refl) c<b
    ex : subtractionNResult.result (-N {c} {b} (inl c<b)) ≡ subtractionNResult.result (-N {0} {succ d} (inl (succIsPositive d)))
    ex = equivalentSubtraction c (succ d) b 0 (c<b) (succIsPositive d) (equalityCommutative (identityOfIndiscernablesLeft _≡_ b=c+d (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))))

primesArePrime : {p : ℕ} → {a b : ℕ} → (Prime p) → p ∣ (a *N b) → (p ∣ a) || (p ∣ b)
primesArePrime {p} {a} {b} pPrime pr with divisionDecidable p a
primesArePrime {p} {a} {b} pPrime pr | inl p|a = inl p|a
primesArePrime {p} {a} {b} pPrime (divides record {quot = ab/p ; rem = .0 ; pr = p|ab ; remIsSmall = _ ; quotSmall = quotSmall } refl) | inr notp|a = inr (answer ex'')
  where
    euc : extendedHcf a p
    euc = euclid a p
    h : extendedHcf.c euc ≡ 1
    h = hcfPrimeIsOne {p} {a} pPrime notp|a
    x = extendedHcf.extended1 euc
    y = extendedHcf.extended2 euc
    extended : ((a *N x) ≡ p *N y +N extendedHcf.c euc) || (a *N x +N extendedHcf.c euc ≡ p *N y)
    extended = extendedHcf.extendedProof euc
    extended' : (a *N x ≡ p *N y +N 1) || (a *N x +N 1 ≡ p *N y)
    extended' rewrite equalityCommutative h = extended
    extended'' : ((a *N x ≡ p *N y +N 1) || (a *N x +N 1 ≡ p *N y)) → (b *N (a *N x) ≡ b *N (p *N y +N 1)) || (b *N (a *N x +N 1) ≡ b *N (p *N y))
    extended'' (inl z) = inl (applyEquality (λ t → b *N t) z)
    extended'' (inr z) = inr (applyEquality (λ t → b *N t) z)
    ex : (b *N (a *N x) ≡ b *N (p *N y +N 1)) || (b *N (a *N x +N 1) ≡ b *N (p *N y)) → ((b *N a) *N x ≡ (b *N (p *N y) +N b)) || (((b *N a) *N x +N b) ≡ b *N (p *N y))
    ex (inl z) rewrite Semiring.*Associative ℕSemiring b a x | Semiring.+DistributesOver* ℕSemiring b (p *N y) 1 | Semiring.productOneRight ℕSemiring b = inl z
    ex (inr z) rewrite Semiring.+DistributesOver* ℕSemiring b (a *N x) 1 | Semiring.*Associative ℕSemiring b a x | Semiring.productOneRight ℕSemiring b = inr z
    ex' : ((a *N b) *N x ≡ ((p *N y) *N b +N b)) || (((a *N b) *N x +N b) ≡ (p *N y) *N b)
    ex' rewrite multiplicationNIsCommutative a b | multiplicationNIsCommutative (p *N y) b = ex (extended'' extended')
    ex'' : ((a *N b) *N x ≡ (p *N (y *N b) +N b)) || (((a *N b) *N x +N b) ≡ p *N (y *N b))
    ex'' rewrite Semiring.*Associative ℕSemiring (p) y b = ex'
    inter1 : p ∣ (a *N b) *N x
    inter1 = divides (record {quot = ab/p *N x ; rem = 0 ; pr = g ; remIsSmall = zeroIsValidRem p ; quotSmall = qsm quotSmall}) refl
      where
        g' : p *N ab/p ≡ a *N b
        g' rewrite Semiring.sumZeroRight ℕSemiring (p *N ab/p) = p|ab
        g'' : p *N (ab/p *N x) ≡ (a *N b) *N x
        g'' rewrite Semiring.*Associative ℕSemiring (p) ab/p x = applyEquality (λ t → t *N x) g'
        g : p *N (ab/p *N x) +N 0 ≡ (a *N b) *N x
        g rewrite Semiring.sumZeroRight ℕSemiring (p *N (ab/p *N x)) = g''
        qsm : ((0 <N p) || ((0 ≡ p) && (ab/p ≡ 0))) → (0 <N p) || ((0 ≡ p) && (ab/p *N x ≡ 0))
        qsm (inl pr) = inl pr
        qsm (inr (pr1 ,, pr2)) = inr (pr1 ,, blah)
          where
            blah : ab/p *N x ≡ 0
            blah rewrite pr2 = refl
    inter2 : ((0 <N p) || ((0 ≡ p) && (ab/p ≡ 0))) → p ∣ (p *N (y *N b))
    inter2 (inl 0<p) = divides (record {quot = y *N b ; rem = 0 ; pr = Semiring.sumZeroRight ℕSemiring (p *N (y *N b)) ; remIsSmall = zeroIsValidRem p ; quotSmall = inl 0<p }) refl
    inter2 (inr (0=p ,, ab/p=0)) = divides (record {quot = y *N b ; rem = 0 ; pr = Semiring.sumZeroRight ℕSemiring (p *N (y *N b)) ; remIsSmall = zeroIsValidRem p ; quotSmall = inr (0=p ,, blah) }) refl
      where
        oneZero : (a ≡ 0) || (b ≡ 0)
        oneZero rewrite Semiring.commutative ℕSemiring (p *N ab/p) 0 | ab/p=0 | equalityCommutative 0=p = productZeroImpliesOperandZero (equalityCommutative p|ab)
        blah : y *N b ≡ 0
        blah with oneZero
        blah | inl x1 = exFalso (notp|a p|a)
          where
            p|a : p ∣ a
            p|a rewrite x1 = aDivZero p
        blah | inr x1 rewrite x1 = Semiring.productZeroRight ℕSemiring y
    answer : ((a *N b) *N x ≡ (p *N (y *N b) +N b)) || (((a *N b) *N x +N b) ≡ p *N (y *N b)) → (p ∣ b)
    answer (inl z) = reduceEquationMod {p} b inter1 (inter2 quotSmall) z
    answer (inr z) = reduceEquationMod {p} b (inter2 quotSmall) inter1 (equalityCommutative z)

primesAreBiggerThanOne : {p : ℕ} → Prime p → (1 <N p)
primesAreBiggerThanOne {zero} record { p>1 = (le x ()) ; pr = pr }
primesAreBiggerThanOne {succ zero} pr = exFalso (oneIsNotPrime pr)
primesAreBiggerThanOne {succ (succ p)} pr = succPreservesInequality (succIsPositive p)

primesAreBiggerThanZero : {p : ℕ} → Prime p → 0 <N p
primesAreBiggerThanZero {p} pr = TotalOrder.<Transitive ℕTotalOrder (succIsPositive 0) (primesAreBiggerThanOne pr)

record notDividedByLessThan (a : ℕ) (firstPossibleDivisor : ℕ) : Set where
  field
    previousDoNotDivide : ∀ x → 1 <N x → x <N firstPossibleDivisor → x ∣ a → False

alternativePrime : {a : ℕ} → 1 <N a → notDividedByLessThan a a → Prime a
alternativePrime {a} 1<a record { previousDoNotDivide = previousDoNotDivide } = record { pr = pr ; p>1 = 1<a}
  where
    pr : {x : ℕ} → (x|a : x ∣ a) (x<a : x <N a) (0<x : zero <N x) → x ≡ 1
    pr {zero} _ _ (le x ())
    pr {succ zero} _ _ _ = refl
    pr {succ (succ x)} x|a x<a 0<x = exFalso (previousDoNotDivide (succ (succ x)) (succPreservesInequality (succIsPositive x)) x<a x|a)

divisibilityTransitive : {a b c : ℕ} → a ∣ b → b ∣ c → a ∣ c
divisibilityTransitive {a} {b} {c} (divides record { quot = b/a ; rem = .0 ; pr = prDivAB ; remIsSmall = remIsSmallAB ; quotSmall = quotSmall } refl) (divides record { quot = c/b ; rem = .0 ; pr = prDivBC ; remIsSmall = remIsSmallBC } refl) = divides record { quot = b/a *N c/b ; rem = 0 ; pr = p ; remIsSmall = zeroIsValidRem a ; quotSmall = qsm quotSmall } refl
  where
    p : a *N (b/a *N c/b) +N 0 ≡ c
    p rewrite Semiring.sumZeroRight ℕSemiring (a *N (b/a *N c/b)) | Semiring.sumZeroRight ℕSemiring (b *N c/b) | Semiring.sumZeroRight ℕSemiring (a *N b/a) | Semiring.*Associative ℕSemiring a b/a c/b | prDivAB | prDivBC = refl
    qsm : ((0 <N a) || (0 ≡ a) && (b/a ≡ 0)) → ((0 <N a) || (0 ≡ a) && (b/a *N c/b ≡ 0))
    qsm (inl x) = inl x
    qsm (inr (p1 ,, p2)) = inr (p1 ,, blah)
      where
        blah : b/a *N c/b ≡ 0
        blah rewrite p2 = refl

compositeOrPrimeLemma : {a b : ℕ} → notDividedByLessThan b a → a ∣ b → {i : ℕ} → (i ∣ a) → (i <N a) → (0 <N i) → i ≡ 1
compositeOrPrimeLemma {a} {b} record { previousDoNotDivide = previousDoNotDivide } a|b {zero} i|a i<a 0<i = exFalso (lessIrreflexive 0<i)
compositeOrPrimeLemma {a} {b} record { previousDoNotDivide = previousDoNotDivide } a|b {succ zero} i|a i<a 0<i = refl
compositeOrPrimeLemma {a} {b} record { previousDoNotDivide = previousDoNotDivide } a|b {succ (succ i)} i|a i<a 0<i = exFalso (previousDoNotDivide (succ (succ i)) (succPreservesInequality (succIsPositive i)) i<a (divisibilityTransitive i|a a|b) )

compositeOrPrime : (a : ℕ) → (1 <N a) → (Composite a) || (Prime a)
compositeOrPrime a pr = go''' go''
  where
    base : notDividedByLessThan a 2
    base = record { previousDoNotDivide = λ x 1<x x<2 _ → noIntegersBetweenXAndSuccX 1 1<x x<2 }
    go : {firstPoss : ℕ} → notDividedByLessThan a firstPoss → ((notDividedByLessThan a (succ firstPoss)) || ((firstPoss ∣ a) && (firstPoss <N a))) || (firstPoss ≡ a)
    go' : (firstPoss : ℕ) → (((notDividedByLessThan a firstPoss) || (Composite a))) || (notDividedByLessThan a a)
    go'' : (notDividedByLessThan a a) || (Composite a)
    go'' with go' a
    ... | inr x = inl x
    ... | inl x = x
    go''' : ((notDividedByLessThan a a) || (Composite a)) → ((Composite a) || (Prime a))
    go''' (inl x) = inr (alternativePrime pr x)
    go''' (inr x) = inl x
    go' (zero) = inl (inl (record { previousDoNotDivide = λ x 1<x x<0 _ → zeroNeverGreater x<0 }))
    go' (succ 0) = inl (inl (record { previousDoNotDivide = λ x 1<x x<1 _ → TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x<1 1<x) }))
    go' (succ (succ zero)) = inl (inl base)
    go' (succ (succ (succ firstPoss))) with go' (succ (succ firstPoss))
    go' (succ (succ (succ firstPoss))) | inl (inl x) with go {succ (succ firstPoss)} x
    go' (succ (succ (succ firstPoss))) | inl (inl x) | inl (inl x1) = inl (inl x1)
    go' (succ (succ (succ firstPoss))) | inl (inl x) | inl (inr x1) = inl (inr record { noSmallerDivisors = λ i i<ssFP 1<i i|a → notDividedByLessThan.previousDoNotDivide x i 1<i i<ssFP i|a ; n>1 = pr ; divisor = succ (succ firstPoss) ; dividesN = _&&_.fst x1 ; divisorLessN = _&&_.snd x1 ; divisorNot1 = succPreservesInequality (succIsPositive firstPoss) ; divisorPrime = record { p>1 = succPreservesInequality (succIsPositive firstPoss) ; pr = compositeOrPrimeLemma {succ (succ firstPoss)} {a} x (_&&_.fst x1) } })
    go' (succ (succ (succ firstPoss))) | inl (inl x) | inr y rewrite y = inr x
    go' (succ (succ (succ firstPoss))) | inl (inr x) = inl (inr x)
    go' (succ (succ (succ firstPoss))) | inr x = inr x

    go {zero} pr = inl (inl (record { previousDoNotDivide = λ x 1<x x<1 _ → irreflexive (<Transitive x<1 1<x)}))
    go {succ firstPoss} knownCoprime with totality (succ firstPoss) a
    go {succ firstPoss} knownCoprime | inr x = inr x
    go {succ firstPoss} knownCoprime | inl (inl sFP<a) with divisionAlg (succ firstPoss) a
    go {succ firstPoss} knownCoprime | inl (inl sFP<a) | record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall } = inl (inr record { fst = (divides (record { quot = quot ; rem = zero ; remIsSmall = remIsSmall ; pr = pr ; quotSmall = inl (succIsPositive firstPoss) }) refl) ; snd = sFP<a })
    go {succ firstPoss} knownCoprime | inl (inl sFP<a) | record { quot = quot ; rem = succ rem ; pr = pr ; remIsSmall = remIsSmall } = inl next
      where
        previous : ∀ x → 1 <N x → x <N succ firstPoss → x ∣ a → False
        previous = notDividedByLessThan.previousDoNotDivide knownCoprime
        next : notDividedByLessThan a (succ (succ firstPoss)) || (((succ firstPoss) ∣ a) && (succ firstPoss <N a))
        next with divisionAlg (succ firstPoss) a
        next | record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall } = inr (record { fst = divides record { quot = quot ; rem = zero ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = inl (succIsPositive firstPoss) } refl ; snd = sFP<a } )
        next | record { quot = quot ; rem = succ rem ; pr = pr ; remIsSmall = remIsSmall } = inl record { previousDoNotDivide = (next' record { quot = quot ; rem = succ rem ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = inl (succIsPositive firstPoss)  } (succIsPositive rem)) }
          where
            next' : (res : divisionAlgResult (succ firstPoss) a) → (pr : 0 <N divisionAlgResult.rem res) → (x : ℕ) → 1 <N x → x <N succ (succ firstPoss) → x ∣ a → False
            next' (res) (prDiv) x 1<x x<ssFirstposs x|a with totality x (succ firstPoss)
            next' (res) (prDiv) x 1<x x<ssFirstposs x|a | inl (inl x<sFirstPoss) = previous x 1<x x<sFirstPoss x|a
            next' (res) (prDiv) x 1<x x<ssFirstposs x|a | inl (inr sFirstPoss<x) = noIntegersBetweenXAndSuccX (succ firstPoss) sFirstPoss<x x<ssFirstposs
            next' res prDiv x 1<x x<ssFirstposs (divides res1 x1) | inr x=sFirstPoss rewrite equalityCommutative x=sFirstPoss = g
              where
                g : False
                g with modIsUnique res res1
                ... | r rewrite r = lessImpliesNotEqual prDiv (equalityCommutative x1)
    go {succ firstPoss} record { previousDoNotDivide = previousDoNotDivide } | inl (inr a<sFP) = exFalso (previousDoNotDivide a pr a<sFP (aDivA a))

primeDivPrimeImpliesEqual : {p1 p2 : ℕ} → Prime p1 → Prime p2 → p1 ∣ p2 → p1 ≡ p2
primeDivPrimeImpliesEqual {p1} {p2} pr1 pr2 p1|p2 with totality p1 p2
primeDivPrimeImpliesEqual {p1} {p2} pr1 record { p>1 = p>1 ; pr = pr } p1|p2 | inl (inl p1<p2) with pr p1|p2 p1<p2 (primesAreBiggerThanZero {p1} pr1)
... | p1=1 = exFalso (oneIsNotPrime contr)
  where
    contr : Prime 1
    contr rewrite p1=1 = pr1
primeDivPrimeImpliesEqual {p1} {zero} pr1 pr2 p1|p2 | inl (inr p1>p2) = exFalso (zeroIsNotPrime pr2)
primeDivPrimeImpliesEqual {p1} {succ p2} pr1 pr2 p1|p2 | inl (inr p1>p2) = exFalso (divisorIsSmaller p1|p2 p1>p2)
primeDivPrimeImpliesEqual {p1} {p2} pr1 pr2 p1|p2 | inr p1=p2 = p1=p2

mult1Lemma : {a b : ℕ} → a *N succ b ≡ 1 → (a ≡ 1) && (b ≡ 0)
mult1Lemma {a} {b} pr = record { fst = _&&_.fst p ; snd = q}
  where
    p : (a ≡ 1) && (succ b ≡ 1)
    p = productOneImpliesOperandsOne pr
    q : b ≡ zero
    q = succInjective (_&&_.snd p)

oneHasNoDivisors : {a : ℕ} → a ∣ 1 → a ≡ 1
oneHasNoDivisors {a} (divides record { quot = zero ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall } refl) rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | multiplicationNIsCommutative a zero | Semiring.sumZeroRight ℕSemiring a = exFalso (naughtE pr)
oneHasNoDivisors {a} (divides record { quot = (succ quot) ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall } refl) rewrite Semiring.sumZeroRight ℕSemiring (a *N succ quot) = _&&_.fst (mult1Lemma pr)

notSmallerMeansGE : {a b : ℕ} → (a <N b → False) → b ≤N a
notSmallerMeansGE {a} {b} notA<b with totality a b
notSmallerMeansGE {a} {b} notA<b | inl (inl x) = exFalso (notA<b x)
notSmallerMeansGE {a} {b} notA<b | inl (inr x) = inl x
notSmallerMeansGE {a} {b} notA<b | inr x = inr (equalityCommutative x)


text:
------------------------------------------------------------------------
-- Functional semantics for a non-deterministic untyped λ-calculus
-- with constants
------------------------------------------------------------------------

{-# OPTIONS --no-termination-check #-}

module Lambda.Closure.Functional.Non-deterministic.No-workarounds where

open import Category.Monad.Partiality as Pa using (_⊥; now; later)
open import Codata.Musical.Notation
open import Data.Fin using (Fin; zero; suc; #_)
open import Data.List hiding (lookup)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Data.Vec using ([]; _∷_; lookup)
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable

open import Lambda.Syntax using (Ty; Ctxt)
open Lambda.Syntax.Closure using (con; ƛ)
open Lambda.Syntax.Ty
open import Lambda.VirtualMachine
  hiding (comp; comp-val; comp-env; lookup-hom)
open Functional
private
  module VM = Lambda.Syntax.Closure Code

------------------------------------------------------------------------
-- A monad with partiality, failure and non-determinism

-- This is basically the maybe monad transformer applied to the
-- partiality monad transformer applied to the non-determinism monad
-- N A = μX. A ⊎ X × X. Unfortunately it is somewhat awkward to
-- implement the partiality monad transformer in Agda: the definition
--
--   data Partiality′ (M : Set → Set) (A : Set) : Set where
--     now-or-later : M (A ⊎ Partiality′ M A) → Partiality′ M A
--
-- is rejected, because M might use its argument negatively.

infixr 6 _∣_

data D (A : Set) : Set where
  fail   : D A
  return : (x : A) → D A
  _∣_    : (x y : D A) → D A
  later  : (x : ∞ (D A)) → D A

-- The function force n removes (up to) n layers of later
-- constructors.

force : {A : Set} → ℕ → D A → D A
force (suc n) (later x) = force n (♭ x)
force n       (x₁ ∣ x₂) = force n x₁ ∣ force n x₂
force _       x         = x

-- Bind.

infixl 5 _>>=_

_>>=_ : {A B : Set} → D A → (A → D B) → D B
fail      >>= f = fail
return x  >>= f = f x
(x₁ ∣ x₂) >>= f = (x₁ >>= f) ∣ (x₂ >>= f)
later x   >>= f = later (♯ (♭ x >>= f))

-- A deterministic non-terminating computation.

never : {A : Set} → D A
never = later (♯ never)

-- Strong bisimilarity.

infix 4 _≅_

data _≅_ {A : Set} : D A → D A → Set where
  fail   : fail ≅ fail
  return : ∀ {x} → return x ≅ return x
  _∣_    : ∀ {x₁ x₂ y₁ y₂}
           (x₁≅y₁ : x₁ ≅ y₁) (x₂≅y₂ : x₂ ≅ y₂) → x₁ ∣ x₂ ≅ y₁ ∣ y₂
  later  : ∀ {x y} (x≅y : ∞ (♭ x ≅ ♭ y)) → later x ≅ later y

-- Strong bisimilarity is reflexive.

infixr 3 _∎

_∎ : {A : Set} (x : D A) → x ≅ x
fail     ∎ = fail
return x ∎ = return
x₁ ∣ x₂  ∎ = (x₁ ∎) ∣ (x₂ ∎)
later x  ∎ = later (♯ (♭ x ∎))

-- Strong bisimilarity is symmetric.

sym : {A : Set} {x y : D A} → x ≅ y → y ≅ x
sym fail            = fail
sym return          = return
sym (x₁≅y₁ ∣ x₂≅y₂) = sym x₁≅y₁ ∣ sym x₂≅y₂
sym (later x≅y)     = later (♯ sym (♭ x≅y))

-- Strong bisimilarity is transitive.

infixr 2 _≅⟨_⟩_

_≅⟨_⟩_ : ∀ {A : Set} (x : D A) {y z} → x ≅ y → y ≅ z → x ≅ z
._ ≅⟨ fail          ⟩ fail          = fail
._ ≅⟨ return        ⟩ return        = return
._ ≅⟨ x₁≅y₁ ∣ x₂≅y₂ ⟩ y₁≅z₁ ∣ y₂≅z₂ = (_ ≅⟨ x₁≅y₁ ⟩ y₁≅z₁) ∣ (_ ≅⟨ x₂≅y₂ ⟩ y₂≅z₂)
._ ≅⟨ later x≅y     ⟩ later y≅z     = later (♯ (_ ≅⟨ ♭ x≅y ⟩ ♭ y≅z))

-- The monad laws hold up to strong bisimilarity.

left-identity : {A B : Set} {x : A} {f : A → D B} →
                return x >>= f ≅ f x
left-identity {x = x} {f} = f x ∎

right-identity : {A : Set} (x : D A) → x >>= return ≅ x
right-identity fail       = fail
right-identity (return x) = return
right-identity (x₁ ∣ x₂)  = right-identity x₁ ∣ right-identity x₂
right-identity (later x)  = later (♯ right-identity (♭ x))

associative : {A B C : Set} (x : D A) {f : A → D B} {g : B → D C} →
              x >>= f >>= g ≅ x >>= λ y → f y >>= g
associative fail               = fail
associative (return x) {f} {g} = f x >>= g ∎
associative (x₁ ∣ x₂)          = associative x₁ ∣ associative x₂
associative (later x)          = later (♯ associative (♭ x))

-- Bind respects strong bisimilarity.

infixl 5 _>>=-cong_

_>>=-cong_ : {A B : Set} {x₁ x₂ : D A} {f₁ f₂ : A → D B} →
             x₁ ≅ x₂ → (∀ y → f₁ y ≅ f₂ y) → x₁ >>= f₁ ≅ x₂ >>= f₂
fail          >>=-cong f₁≅f₂ = fail
return        >>=-cong f₁≅f₂ = f₁≅f₂ _
later x≅y     >>=-cong f₁≅f₂ = later (♯ (♭ x≅y >>=-cong f₁≅f₂))
x₁≅x₂ ∣ y₁≅y₂ >>=-cong f₁≅f₂ =
  (x₁≅x₂ >>=-cong f₁≅f₂) ∣ (y₁≅y₂ >>=-cong f₁≅f₂)

-- More laws.

never-left-zero : {A B : Set} {f : A → D B} → never >>= f ≅ never
never-left-zero = later (♯ never-left-zero)

fail-left-zero : {A B : Set} {f : A → D B} → fail >>= f ≅ fail
fail-left-zero = fail ∎

------------------------------------------------------------------------
-- Syntax

infixl 9 _·_

data Tm (n : ℕ) : Set where
  con : (i : ℕ) → Tm n
  var : (x : Fin n) → Tm n
  ƛ   : (t : Tm (suc n)) → Tm n
  _·_ : (t₁ t₂ : Tm n) → Tm n
  _∣_ : (t₁ t₂ : Tm n) → Tm n

-- Convenient helper.

vr : ∀ m {n} {m<n : True (suc m ≤? n)} → Tm n
vr _ {m<n = m<n} = var (#_ _ {m<n = m<n})

open Lambda.Syntax.Closure Tm hiding (con; ƛ)

------------------------------------------------------------------------
-- Semantics

infix 9 _∙_

mutual

  ⟦_⟧ : ∀ {n} → Tm n → Env n → D Value
  ⟦ con i ⟧   ρ = return (con i)
  ⟦ var x ⟧   ρ = return (lookup ρ x)
  ⟦ ƛ t ⟧     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ >>= λ v₁ →
                  ⟦ t₂ ⟧ ρ >>= λ v₂ →
                  v₁ ∙ v₂
  ⟦ t₁ ∣ t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ ∣ ⟦ t₂ ⟧ ρ

  _∙_ : Value → Value → D Value
  con i  ∙ v₂ = fail
  ƛ t₁ ρ ∙ v₂ = later (♯ (⟦ t₁ ⟧ (v₂ ∷ ρ)))

-- An abbreviation.

infix 9 _⟦·⟧_

_⟦·⟧_ : D Value → D Value → D Value
v₁ ⟦·⟧ v₂ = v₁ >>= λ v₁ → v₂ >>= λ v₂ → v₁ ∙ v₂

------------------------------------------------------------------------
-- Compiler

-- The compiler takes a code continuation.
--
-- Non-determinism is resolved by always picking the left choice.

comp : ∀ {n} → Tm n → Code n → Code n
comp (con i)   c = con i ∷ c
comp (var x)   c = var x ∷ c
comp (ƛ t)     c = clo (comp t [ ret ]) ∷ c
comp (t₁ · t₂) c = comp t₁ (comp t₂ (app ∷ c))
comp (t₁ ∣ t₂) c = comp t₁ c

-- Environments and values can also be compiled.

mutual

  comp-env : ∀ {n} → Env n → VM.Env n
  comp-env []      = []
  comp-env (v ∷ ρ) = comp-val v ∷ comp-env ρ

  comp-val : Value → VM.Value
  comp-val (con i) = con i
  comp-val (ƛ t ρ) = ƛ (comp t [ ret ]) (comp-env ρ)

-- lookup x is homomorphic with respect to comp-env/comp-val.

lookup-hom : ∀ {n} (x : Fin n) ρ →
             lookup (comp-env ρ) x ≡ comp-val (lookup ρ x)
lookup-hom zero    (v ∷ ρ) = P.refl
lookup-hom (suc x) (v ∷ ρ) = lookup-hom x ρ

------------------------------------------------------------------------
-- Examples

-- A non-terminating term.

Ω : Tm 0
Ω = ω · ω
  where ω = ƛ (vr 0 · vr 0)

Ω-loops : ⟦ Ω ⟧ [] ≅ never
Ω-loops = later (♯ Ω-loops)

-- A call-by-value fix-point combinator.

Z : {n : ℕ} → Tm n
Z = ƛ (t · t)
  where t = ƛ (vr 1 · ƛ (vr 1 · vr 1 · vr 0))

-- A non-deterministically non-terminating term.

! : Tm 0
! = Z · ƛ (ƛ (vr 1 · vr 0 ∣ vr 1 · vr 0)) · con 0

-- Its semantics.

!-sem : D Value
!-sem = later (♯ later (♯ later (♯ later (♯ (!-sem ∣ !-sem)))))

⟦!⟧≅!-sem : ⟦ ! ⟧ [] ≅ !-sem
⟦!⟧≅!-sem = later (♯ lem)
  where
  lem : force 1 (⟦ ! ⟧ []) ≅ force 1 !-sem
  lem = later (♯ later (♯ later (♯ (later (♯ lem) ∣ later (♯ lem)))))

-- How did I come up with this proof term? Through a manual
-- calculation...
--
-- Let us first define some abbreviations:
--
--   t₀ = vr 1 · vr 1 · vr 0
--   t₁ = ƛ t₀
--   t₂ = vr 1 · t₁
--   t₃ = ƛ t₂
--
--   u₀ = vr 1 · vr 0
--   u₁ = u₀ ∣ u₀
--   u₂ = ƛ u₁
--   u₃ = ƛ u₂
--
--   c₀ = ƛ u₂ []
--   c₁ = ƛ t₂ (c₀ ∷ [])
--   c₂ = ƛ t₀ (c₁ ∷ c₀ ∷ [])
--
-- Now we can calculate as follows (ignoring ♯):
--
--   ⟦ Z · u₃ · con 0 ⟧ []
-- = ⟦ Z · u₃ ⟧ [] ⟦·⟧ return (con 0)
-- = ƛ (t₃ · t₃) [] ∙ c₀ ⟦·⟧ return (con 0)
-- = later (⟦ t₃ · t₃ ⟧ (c₀ ∷ []) ⟦·⟧ return (con 0))
-- = later (c₁ ∙ c₁ ⟦·⟧ return (con 0))
--
-- = c₁ ∙ c₁ ⟦·⟧ return (con 0)
-- = later (⟦ t₂ ⟧ (c₁ ∷ c₀ ∷ []) ⟦·⟧ return (con 0))
-- = later (c₀ ∙ c₂ ⟦·⟧ return (con 0))
-- = later (later (⟦ u₂ ⟧ (c₂ ∷ []) ⟦·⟧ return (con 0)))
-- = later (later (ƛ u₁ (c₂ ∷ []) ∙ con 0))
-- = later (later (later (⟦ u₁ ⟧ (con 0 ∷ c₂ ∷ []))))
-- = later (later (later (⟦ u₀ ⟧ (con 0 ∷ c₂ ∷ []) ∣
--                        ⟦ u₀ ⟧ (con 0 ∷ c₂ ∷ []))))
-- = later (later (later (c₂ ∙ con 0 ∣ c₂ ∙ con 0)))
-- = later (later (later (⟦ t₀ ⟧ (con 0 ∷ c₁ ∷ c₀ ∷ []) ∣
--                        ⟦ t₀ ⟧ (con 0 ∷ c₁ ∷ c₀ ∷ []))))
-- = later (later (later (later (c₁ ∙ c₁ ⟦·⟧ return (con 0)) ∣
--                        later (c₁ ∙ c₁ ⟦·⟧ return (con 0)))))

------------------------------------------------------------------------
-- A relation relating deterministic and non-deterministic
-- computations

-- x ≈∈ y means that x implements /one/ possible semantics of y (up to
-- weak bisimilarity).

infix 4 _≈∈_

data _≈∈_ {A : Set} : Maybe A ⊥ → D A → Set where
  fail   : now nothing ≈∈ fail

  return : ∀ {x} → now (just x) ≈∈ return x

  ∣ˡ     : ∀ {x y₁ y₂} (x≈∈y₁ : x ≈∈ y₁) → x ≈∈ y₁ ∣ y₂
  ∣ʳ     : ∀ {x y₁ y₂} (x≈∈y₂ : x ≈∈ y₂) → x ≈∈ y₁ ∣ y₂

  later  : ∀ {x y} (x≈∈y : ∞ (♭ x ≈∈ ♭ y)) → later x ≈∈ later y
  laterˡ : ∀ {x y} (x≈∈y :    ♭ x ≈∈   y ) → later x ≈∈       y
  laterʳ : ∀ {x y} (x≈∈y :      x ≈∈ ♭ y ) →       x ≈∈ later y

-- A transitivity-like result for _≡_ and _≈∈_.

infixr 2 _≡⟨_⟩_

_≡⟨_⟩_ : ∀ {A : Set} (x : Maybe A ⊥) {y z} → x ≡ y → y ≈∈ z → x ≈∈ z
_ ≡⟨ P.refl ⟩ y≈z = y≈z

-- A transitivity-like result for _≈∈_ and _≅_.

infixr 2 _≈∈⟨_⟩_

_≈∈⟨_⟩_ : ∀ {A : Set} (x : Maybe A ⊥) {y z} → x ≈∈ y → y ≅ z → x ≈∈ z
._ ≈∈⟨ fail        ⟩ fail          = fail
._ ≈∈⟨ return      ⟩ return        = return
_  ≈∈⟨ ∣ˡ x₁≈∈y₁   ⟩ y₁≅z₁ ∣ y₂≅z₂ = ∣ˡ (_ ≈∈⟨ x₁≈∈y₁ ⟩ y₁≅z₁)
_  ≈∈⟨ ∣ʳ x₂≈∈y₂   ⟩ y₁≅z₁ ∣ y₂≅z₂ = ∣ʳ (_ ≈∈⟨ x₂≈∈y₂ ⟩ y₂≅z₂)
._ ≈∈⟨ later  x≈∈y ⟩ later y≅z     = later (♯ (_ ≈∈⟨ ♭ x≈∈y ⟩ ♭ y≅z))
._ ≈∈⟨ laterˡ x≈∈y ⟩       y≅z     = laterˡ   (_ ≈∈⟨   x≈∈y ⟩   y≅z)
_  ≈∈⟨ laterʳ x≈∈y ⟩ later y≅z     = laterʳ   (_ ≈∈⟨   x≈∈y ⟩ ♭ y≅z)

-- An example.

lemma : Pa.never ≈∈ !-sem
lemma = later (♯ later (♯ later (♯ later (♯ ∣ˡ lemma))))

------------------------------------------------------------------------
-- Compiler correctness

module Correctness where

  mutual

    correct :
      ∀ {n} t {ρ : Env n} {c s} {k : Value → D VM.Value} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈∈ k v) →
      exec ⟨ comp t c , s , comp-env ρ ⟩ ≈∈ (⟦ t ⟧ ρ >>= k)
    correct (con i) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (con i) ∷ s , comp-env ρ ⟩  ≈∈⟨ hyp (con i) ⟩
      k (con i)                                  ∎)
    correct (var x) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (lookup (comp-env ρ) x) ∷ s , comp-env ρ ⟩  ≡⟨ P.cong (λ v → exec ⟨ c , val v ∷ s , comp-env ρ ⟩) (lookup-hom x ρ) ⟩
      exec ⟨ c , val (comp-val (lookup ρ x)) ∷ s , comp-env ρ ⟩  ≈∈⟨ hyp (lookup ρ x) ⟩
      k (lookup ρ x)                                             ∎)
    correct (ƛ t) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (comp-val (ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≈∈⟨ hyp (ƛ t ρ) ⟩
      k (ƛ t ρ)                                             ∎)
    correct (t₁ · t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩      ≈∈⟨ correct t₁ (λ v₁ → correct t₂ (λ v₂ → ∙-correct v₁ v₂ hyp)) ⟩
      (⟦ t₁ ⟧ ρ >>= λ v₁ →  ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂  >>= k)  ≅⟨ ((⟦ t₁ ⟧ ρ ∎) >>=-cong λ _ → sym $ associative (⟦ t₂ ⟧ ρ)) ⟩
      (⟦ t₁ ⟧ ρ >>= λ v₁ → (⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂) >>= k)  ≅⟨ sym $ associative (⟦ t₁ ⟧ ρ) ⟩
      (⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ >>= k)                              ≅⟨ _ ∎ ⟩
      (⟦ t₁ · t₂ ⟧ ρ >>= k)                                      ∎
    correct (t₁ ∣ t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ c , s , comp-env ρ ⟩  ≈∈⟨ ∣ˡ (correct t₁ hyp) ⟩
      (⟦ t₁ ⟧ ρ >>= k) ∣ (⟦ t₂ ⟧ ρ >>= k)  ∎

    ∙-correct :
      ∀ {n} v₁ v₂ {ρ : Env n} {c s} {k : Value → D VM.Value} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈∈ k v) →
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s , comp-env ρ ⟩ ≈∈
      v₁ ∙ v₂ >>= k
    ∙-correct (con i)   v₂                 _   = fail
    ∙-correct (ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val (ƛ t₁ ρ₁)) ∷ s , comp-env ρ ⟩  ≈∈⟨ later (♯ (

        exec ⟨ comp t₁ [ ret ] , ret c (comp-env ρ) ∷ s , comp-env (v₂ ∷ ρ₁) ⟩                ≈∈⟨ correct t₁ (λ v → laterˡ (hyp v)) ⟩
        (⟦ t₁ ⟧ (v₂ ∷ ρ₁) >>= k)                                                              ∎)) ⟩

      (ƛ t₁ ρ₁ ∙ v₂ >>= k)                                                              ∎

correct : ∀ t →
          exec ⟨ comp t [] , [] , [] ⟩ ≈∈
          ⟦ t ⟧ [] >>= λ v → return (comp-val v)
correct t = Correctness.correct t (λ _ → return)

------------------------------------------------------------------------
-- Type system (following Leroy and Grall)

infix 4 _⊢_∈_

data _⊢_∈_ {n} (Γ : Ctxt n) : Tm n → Ty → Set where
  con : ∀ {i} → Γ ⊢ con i ∈ nat
  var : ∀ {x} → Γ ⊢ var x ∈ lookup Γ x
  ƛ   : ∀ {t σ τ} (t∈ : ♭ σ ∷ Γ ⊢ t ∈ ♭ τ) → Γ ⊢ ƛ t ∈ σ ⇾ τ
  _·_ : ∀ {t₁ t₂ σ τ} (t₁∈ : Γ ⊢ t₁ ∈ σ ⇾ τ) (t₂∈ : Γ ⊢ t₂ ∈ ♭ σ) →
        Γ ⊢ t₁ · t₂ ∈ ♭ τ
  _∣_ : ∀ {t₁ t₂ σ} (t₁∈ : Γ ⊢ t₁ ∈ σ) (t₂∈ : Γ ⊢ t₂ ∈ σ) →
        Γ ⊢ t₁ ∣ t₂ ∈ σ

-- Ω is well-typed.

Ω-well-typed : (τ : Ty) → [] ⊢ Ω ∈ τ
Ω-well-typed τ =
  _·_ {σ = ♯ σ} {τ = ♯ τ} (ƛ (var · var)) (ƛ (var · var))
  where σ = ♯ σ ⇾ ♯ τ

-- The call-by-value fix-point combinator is also well-typed.

fix-well-typed :
  ∀ {σ τ} → [] ⊢ Z ∈ ♯ (♯ (σ ⇾ τ) ⇾ ♯ (σ ⇾ τ)) ⇾ ♯ (σ ⇾ τ)
fix-well-typed =
  ƛ (_·_ {σ = υ} {τ = ♯ _}
         (ƛ (var · ƛ (var · var · var)))
         (ƛ (var · ƛ (var · var · var))))
  where
  υ : ∞ Ty
  υ = ♯ (υ ⇾ ♯ _)

------------------------------------------------------------------------
-- Type soundness

-- WF-Value, WF-Env and WF-DV specify when a
-- value/environment/computation is well-formed with respect to a
-- given context (and type).

mutual

  data WF-Value : Ty → Value → Set where
    con : ∀ {i} → WF-Value nat (con i)
    ƛ   : ∀ {n Γ σ τ} {t : Tm (1 + n)} {ρ}
          (t∈ : ♭ σ ∷ Γ ⊢ t ∈ ♭ τ) (ρ-wf : WF-Env Γ ρ) →
          WF-Value (σ ⇾ τ) (ƛ t ρ)

  infixr 5 _∷_

  data WF-Env : ∀ {n} → Ctxt n → Env n → Set where
    []  : WF-Env [] []
    _∷_ : ∀ {n} {Γ : Ctxt n} {ρ σ v}
          (v-wf : WF-Value σ v) (ρ-wf : WF-Env Γ ρ) →
          WF-Env (σ ∷ Γ) (v ∷ ρ)

data WF-DV (σ : Ty) : D Value → Set where
  return : ∀ {v} (v-wf : WF-Value σ v) → WF-DV σ (return v)
  _∣_    : ∀ {x y}
           (x-wf : WF-DV σ x) (y-wf : WF-DV σ y) → WF-DV σ (x ∣ y)
  later  : ∀ {x} (x-wf : ∞ (WF-DV σ (♭ x))) → WF-DV σ (later x)

-- Variables pointing into a well-formed environment refer to
-- well-formed values.

lookup-wf : ∀ {n Γ ρ} (x : Fin n) → WF-Env Γ ρ →
            WF-Value (lookup Γ x) (lookup ρ x)
lookup-wf zero    (v-wf ∷ ρ-wf) = v-wf
lookup-wf (suc x) (v-wf ∷ ρ-wf) = lookup-wf x ρ-wf

-- If we can prove WF-DV σ x, then x does not "go wrong".

does-not-go-wrong : ∀ {σ x} → WF-DV σ x → ¬ now nothing ≈∈ x
does-not-go-wrong (return v-wf) ()
does-not-go-wrong (x-wf ∣ y-wf) (∣ˡ x↯)     = does-not-go-wrong x-wf x↯
does-not-go-wrong (x-wf ∣ y-wf) (∣ʳ y↯)     = does-not-go-wrong y-wf y↯
does-not-go-wrong (later x-wf)  (laterʳ x↯) =
  does-not-go-wrong (♭ x-wf) x↯

-- Bind preserves WF-DV in the following way:

_>>=-cong-WF_ :
  ∀ {σ τ x f} →
  WF-DV σ x → (∀ {v} → WF-Value σ v → WF-DV τ (f v)) →
  WF-DV τ (x >>= f)
return v-wf   >>=-cong-WF f-wf = f-wf v-wf
(x-wf ∣ y-wf) >>=-cong-WF f-wf = (x-wf >>=-cong-WF f-wf)
                               ∣ (y-wf >>=-cong-WF f-wf)
later x-wf    >>=-cong-WF f-wf = later (♯ (♭ x-wf >>=-cong-WF f-wf))

-- Well-typed programs do not "go wrong".

mutual

  ⟦⟧-wf : ∀ {n Γ} (t : Tm n) {σ} → Γ ⊢ t ∈ σ →
          ∀ {ρ} → WF-Env Γ ρ → WF-DV σ (⟦ t ⟧ ρ)
  ⟦⟧-wf (con i)   con             ρ-wf = return con
  ⟦⟧-wf (var x)   var             ρ-wf = return (lookup-wf x ρ-wf)
  ⟦⟧-wf (ƛ t)     (ƛ t∈)          ρ-wf = return (ƛ t∈ ρ-wf)
  ⟦⟧-wf (t₁ ∣ t₂) (t₁∈ ∣ t₂∈)     ρ-wf = ⟦⟧-wf t₁ t₁∈ ρ-wf
                                       ∣ ⟦⟧-wf t₂ t₂∈ ρ-wf
  ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf =
    ⟦⟧-wf t₁ t₁∈ ρ-wf >>=-cong-WF λ f-wf →
    ⟦⟧-wf t₂ t₂∈ ρ-wf >>=-cong-WF λ v-wf →
    ∙-wf f-wf v-wf

  ∙-wf : ∀ {σ τ f v} →
         WF-Value (σ ⇾ τ) f → WF-Value (♭ σ) v →
         WF-DV (♭ τ) (f ∙ v)
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf = later (♯ ⟦⟧-wf _ t₁∈ (v₂-wf ∷ ρ₁-wf))

type-soundness : ∀ {t : Tm 0} {σ} →
                 [] ⊢ t ∈ σ → ¬ now nothing ≈∈ ⟦ t ⟧ []
type-soundness t∈ = does-not-go-wrong (⟦⟧-wf _ t∈ [])

ext: agda

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module CoinductiveConstructorsAndLet where

open import Common.Coinduction

data D : Set where

foo : D → ∞ D
foo x = let y = x in ♯ y

-- CoinductiveConstructorsAndLet.agda:9,24-25
-- Panic: thing out of context ([CtxId 1] is not a sub context of
-- [CtxId 3])
-- when checking that the expression y has type D

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module SystemF.NormalForm where

open import Prelude

open import SystemF.Syntax
open import SystemF.WellTyped
open import SystemF.Substitutions

open import Data.Vec hiding ([_])
open import Data.List hiding ([_])

mutual

  -- The eta-long beta-normal form described by Andreas Abel in:
  -- Abel, A., 2008, November.
  -- Weak βη-normalization and normalization by evaluation for System F.
  -- In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 497-511).
  -- Springer Berlin Heidelberg.

  infix 4 _⊢_⇓_ _⊢_⇑_

  data _⊢_⇓_ {ν n} (Γ : Ctx ν n) : Term ν n → Type ν → Set where
    nvar   : ∀ n → Γ ⊢ (var n) ⇓ (lookup n Γ)
    napp  : ∀ {a b f e} → Γ ⊢ f ⇓ (a →' b) → Γ ⊢ e ⇑ a → Γ ⊢ (f · e) ⇓ b
    ntapp : ∀ {a f} b → Γ ⊢ f ⇓ (∀' a) → Γ ⊢ (f [ b ]) ⇓ a tp[/tp b ]

  data _⊢_⇑_ {ν n} (Γ : Ctx ν n) : Term ν n → Type ν → Set where
    nbase : ∀ {t a} → Base a → Γ ⊢ t ⇓ a → Γ ⊢ t ⇑ a
    nabs  : ∀ {a b e} → (a ∷ Γ) ⊢ e ⇑ b → Γ ⊢ (λ' a e) ⇑ (a →' b)
    ntabs : ∀ {a e} → (ctx-weaken Γ) ⊢ e ⇑ a → Γ ⊢ (Λ e) ⇑ (∀' a)

mutual

  ⇓-sound : ∀ {ν n} {Γ : Ctx ν n} {t a} → Γ ⊢ t ⇓ a → Γ ⊢ t ∈ a
  ⇓-sound (nvar n₁) = var n₁
  ⇓-sound (napp p x) = (⇓-sound p) · ⇑-sound x
  ⇓-sound (ntapp b p) = ⇓-sound p [ b ]

  ⇑-sound : ∀ {ν n} {Γ : Ctx ν n} {t a} → Γ ⊢ t ⇑ a → Γ ⊢ t ∈ a
  ⇑-sound (nbase a p) = ⇓-sound p
  ⇑-sound (nabs x) = λ' _ (⇑-sound x)
  ⇑-sound (ntabs x) = Λ (⇑-sound x)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on M-types
------------------------------------------------------------------------

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

module Codata.M.Properties where

open import Level
open import Size
open import Codata.Thunk using (Thunk; force)
open import Codata.M
open import Codata.M.Bisimilarity
open import Data.Container.Core as C hiding (map)
import Data.Container.Morphism as Mp
open import Data.Product as Prod using (_,_)
open import Data.Product.Properties
open import Function
import Relation.Binary.PropositionalEquality as P

open import Data.Container.Relation.Binary.Pointwise using (_,_)
import Data.Container.Relation.Binary.Equality.Setoid as EqSetoid

private module Eq {a} (A : Set a) = EqSetoid (P.setoid A)
open Eq using (Eq)

module _ {s p} {C : Container s p} where

  map-id : ∀ {i} c → Bisim C i (map (Mp.id C) c) c
  map-id (inf (s , f)) = inf (P.refl , λ where p .force → map-id (f p .force))

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} where

  map-cong : ∀ {i} {f g : C₁ ⇒ C₂} →
             (∀ {X} t → Eq X C₂ (⟪ f ⟫ t) (⟪ g ⟫ t)) →
             ∀ c₁ → Bisim C₂ i (map f c₁) (map g c₁)
  map-cong {f = f} {g} f≗g (inf t@(s , n)) with f≗g t
  ... | eqs , eqf = inf (eqs , λ where
     p .force {j} → P.subst (λ t → Bisim C₂ j (map f (n (position f p) .force))
                                              (map g (t .force)))
                    (eqf p)
                    (map-cong f≗g (n (position f p) .force)))

module _ {s₁ s₂ s₃ p₁ p₂ p₃} {C₁ : Container s₁ p₁}
         {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃} where

  map-compose : ∀ {i} {g : C₂ ⇒ C₃} {f : C₁ ⇒ C₂} c₁ →
                Bisim C₃ i (map (g Mp.∘ f) c₁) (map g $′ map f c₁)
  map-compose (inf (s , f)) = inf (P.refl , λ where p .force → map-compose (f _ .force))

module _ {s₁ s₂ p₁ p₂ s} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         {S : Set s} {alg : S → ⟦ C₁ ⟧ S} {f : C₁ ⇒ C₂} where

  map-unfold : ∀ {i} s → Bisim C₂ i (map f (unfold alg s))
                                    (unfold (⟪ f ⟫ ∘′ alg) s)
  map-unfold s = inf (P.refl , λ where p .force → map-unfold _)


text:
-- Andreas, 2012-01-17
-- {-# OPTIONS -v tc.proj.like:50 #-}
-- {-# OPTIONS -v tc.conv.atom:50 #-}
module Issue553c where

postulate
  A : Set
  a : A

data Bool : Set where
  true false : Bool

data WrapBool (C : Set) : Set where
  wrap : Bool -> WrapBool C

-- a projection-like function (must not be constructor-headed!)
-- the dummy C is to make Agda accept f as projection like
f : {C : Set} -> WrapBool C -> A
f (wrap true)  = a
f (wrap false) = a

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

-- it is important that f does not reduce, in order to enter compareAtom
test : (b : Bool) -> f {C = A} (wrap b) ≡ f (wrap b)
test b = refl
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:335

-- the problem is fixed now, since f is no longer projection-like
-- because of deep matching

max_stars_repo_name: asr/agda-kanso


text:
module STLC1.Kovacs.Substitution where

open import STLC1.Kovacs.Embedding public
open import Category

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

-- Substitutions (Sub ; ∙ ; _,_)
infix 3 _⊢⋆_
data _⊢⋆_ : 𝒞 → 𝒞 → Set
  where
    ∅   : ∀ {Γ} → Γ ⊢⋆ ∅

    _,_ : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ) (M : Γ ⊢ A)
                    → Γ ⊢⋆ Ξ , A

-- (_ₛ∘ₑ_)
-- NOTE: _◐_ = ren⋆
_◐_ : ∀ {Γ Γ′ Ξ} → Γ ⊢⋆ Ξ → Γ′ ⊇ Γ → Γ′ ⊢⋆ Ξ
∅       ◐ η = ∅
(σ , M) ◐ η = σ ◐ η , ren η M

-- (_ₑ∘ₛ_)
_◑_ : ∀ {Γ Ξ Ξ′} → Ξ′ ⊇ Ξ → Γ ⊢⋆ Ξ′ → Γ ⊢⋆ Ξ
done    ◑ σ       = σ
wkₑ η   ◑ (σ , M) = η ◑ σ
liftₑ η ◑ (σ , M) = η ◑ σ , M

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

-- (dropₛ)
wkₛ : ∀ {A Γ Ξ} → Γ ⊢⋆ Ξ → Γ , A ⊢⋆ Ξ
wkₛ σ = σ ◐ wkₑ idₑ

-- (keepₛ)
liftₛ : ∀ {A Γ Ξ} → Γ ⊢⋆ Ξ → Γ , A ⊢⋆ Ξ , A
liftₛ σ = wkₛ σ , 0

-- (⌜_⌝ᵒᵖᵉ)
⌊_⌋ : ∀ {Γ Γ′} → Γ′ ⊇ Γ → Γ′ ⊢⋆ Γ
⌊ done ⌋    = ∅
⌊ wkₑ η ⌋   = wkₛ ⌊ η ⌋
⌊ liftₑ η ⌋ = liftₛ ⌊ η ⌋

-- (∈ₛ)
getₛ : ∀ {Γ Ξ A} → Γ ⊢⋆ Ξ → Ξ ∋ A → Γ ⊢ A
getₛ (σ , M) zero    = M
getₛ (σ , M) (suc i) = getₛ σ i

-- (Tmₛ)
sub : ∀ {Γ Ξ A} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
sub σ (𝓋 i)   = getₛ σ i
sub σ (ƛ M)   = ƛ (sub (liftₛ σ) M)
sub σ (M ∙ N) = sub σ M ∙ sub σ N
sub σ (M , N) = sub σ M , sub σ N
sub σ (π₁ M)  = π₁ (sub σ M)
sub σ (π₂ M)  = π₂ (sub σ M)
sub σ τ       = τ

-- (idₛ)
idₛ : ∀ {Γ} → Γ ⊢⋆ Γ
idₛ {∅}     = ∅
idₛ {Γ , A} = liftₛ idₛ

cut : ∀ {Γ A B} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut M N = sub (idₛ , M) N

-- (_∘ₛ_)
-- NOTE: _●_ = sub⋆
_●_ : ∀ {Γ Ξ Φ} → Ξ ⊢⋆ Φ → Γ ⊢⋆ Ξ → Γ ⊢⋆ Φ
∅        ● σ₁ = ∅
(σ₂ , M) ● σ₁ = σ₂ ● σ₁ , sub σ₁ M

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

-- (assₛₑₑ)
comp◐○ : ∀ {Γ Γ′ Γ″ Ξ} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (σ : Γ ⊢⋆ Ξ)
                       → (σ ◐ η₂) ◐ η₁ ≡ σ ◐ (η₂ ○ η₁)
comp◐○ η₁ η₂ ∅       = refl
comp◐○ η₁ η₂ (σ , M) = _,_ & comp◐○ η₁ η₂ σ
                           ⊗ (ren○ η₁ η₂ M ⁻¹)

-- (assₑₛₑ)
comp◑◐ : ∀ {Γ Γ′ Ξ Ξ′} → (η₁ : Γ′ ⊇ Γ) (σ : Γ ⊢⋆ Ξ′) (η₂ : Ξ′ ⊇ Ξ)
                       → (η₂ ◑ σ) ◐ η₁ ≡ η₂ ◑ (σ ◐ η₁)
comp◑◐ η₁ ∅       done       = refl
comp◑◐ η₁ (σ , M) (wkₑ η₂)   = comp◑◐ η₁ σ η₂
comp◑◐ η₁ (σ , M) (liftₑ η₂) = (_, ren η₁ M) & comp◑◐ η₁ σ η₂

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

-- (idlₑₛ)
lid◑ : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → idₑ ◑ σ ≡ σ
lid◑ ∅       = refl
lid◑ (σ , M) = (_, M) & lid◑ σ

-- (idlₛₑ)
lid◐ : ∀ {Γ Γ′} → (η : Γ′ ⊇ Γ)
                → idₛ ◐ η ≡ ⌊ η ⌋
lid◐ done      = refl
lid◐ (wkₑ η)   = ((idₛ ◐_) ∘ wkₑ) & rid○ η ⁻¹
               ⦙ comp◐○ (wkₑ idₑ) η idₛ ⁻¹
               ⦙ wkₛ & lid◐ η
lid◐ (liftₑ η) = (_, 0) & ( comp◐○ (liftₑ η) (wkₑ idₑ) idₛ
                          ⦙ ((idₛ ◐_) ∘ wkₑ) & ( lid○ η
                                               ⦙ rid○ η ⁻¹
                                               )
                          ⦙ comp◐○ (wkₑ idₑ) η idₛ ⁻¹
                          ⦙ (_◐ wkₑ idₑ) & lid◐ η
                          )

-- (idrₑₛ)
rid◑ : ∀ {Γ Γ′} → (η : Γ′ ⊇ Γ)
                → η ◑ idₛ ≡ ⌊ η ⌋
rid◑ done      = refl
rid◑ (wkₑ η)   = comp◑◐ (wkₑ idₑ) idₛ η ⁻¹
               ⦙ wkₛ & rid◑ η
rid◑ (liftₑ η) = (_, 0) & ( comp◑◐ (wkₑ idₑ) idₛ η ⁻¹
                          ⦙ (_◐ wkₑ idₑ) & rid◑ η
                          )

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

-- (∈-ₑ∘ₛ)
get◑ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (i : Ξ ∋ A)
                    → getₛ (η ◑ σ) i ≡ (getₛ σ ∘ getₑ η) i
get◑ σ       done      i       = refl
get◑ (σ , M) (wkₑ η)   i       = get◑ σ η i
get◑ (σ , M) (liftₑ η) zero    = refl
get◑ (σ , M) (liftₑ η) (suc i) = get◑ σ η i

-- (Tm-ₑ∘ₛ)
mutual
  sub◑ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (M : Ξ ⊢ A)
                      → sub (η ◑ σ) M ≡ (sub σ ∘ ren η) M
  sub◑ σ η (𝓋 i)   = get◑ σ η i
  sub◑ σ η (ƛ M)   = ƛ & sublift◑ σ η M
  sub◑ σ η (M ∙ N) = _∙_ & sub◑ σ η M
                         ⊗ sub◑ σ η N
  sub◑ σ η (M , N) = _,_ & sub◑ σ η M
                         ⊗ sub◑ σ η N
  sub◑ σ η (π₁ M)  = π₁ & sub◑ σ η M
  sub◑ σ η (π₂ M)  = π₂ & sub◑ σ η M
  sub◑ σ η τ       = refl

  sublift◑ : ∀ {Γ Ξ Ξ′ A B} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (M : Ξ , B ⊢ A)
                            → sub (liftₛ {B} (η ◑ σ)) M ≡
                               (sub (liftₛ σ) ∘ ren (liftₑ η)) M
  sublift◑ σ η M = (λ σ′ → sub (σ′ , 0) M)
                   & comp◑◐ (wkₑ idₑ) σ η
                 ⦙ sub◑ (liftₛ σ) (liftₑ η) M

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

-- (∈-ₛ∘ₑ)
get◐ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ⊇ Γ) (σ : Γ ⊢⋆ Ξ) (i : Ξ ∋ A)
                    → getₛ (σ ◐ η) i ≡ (ren η ∘ getₛ σ) i
get◐ η (σ , M) zero    = refl
get◐ η (σ , M) (suc i) = get◐ η σ i

-- (Tm-ₛ∘ₑ)
mutual
  sub◐ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ⊇ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
                      → sub (σ ◐ η) M ≡ (ren η ∘ sub σ) M
  sub◐ η σ (𝓋 i)   = get◐ η σ i
  sub◐ η σ (ƛ M)   = ƛ & sublift◐ η σ M
  sub◐ η σ (M ∙ N) = _∙_ & sub◐ η σ M
                         ⊗ sub◐ η σ N
  sub◐ η σ (M , N) = _,_ & sub◐ η σ M
                         ⊗ sub◐ η σ N
  sub◐ η σ (π₁ M)  = π₁ & sub◐ η σ M
  sub◐ η σ (π₂ M)  = π₂ & sub◐ η σ M
  sub◐ η σ τ       = refl

  sublift◐ : ∀ {Γ Γ′ Ξ A B} → (η : Γ′ ⊇ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ , B ⊢ A)
                            → sub (liftₛ {B} (σ ◐ η)) M ≡
                               (ren (liftₑ η) ∘ sub (liftₛ σ)) M
  sublift◐ η σ M = (λ σ′ → sub (σ′ , 0) M)
                   & ( comp◐○ (wkₑ idₑ) η σ
                     ⦙ (σ ◐_) & (wkₑ & ( rid○ η
                                       ⦙ lid○ η ⁻¹
                                       ))
                     ⦙ comp◐○ (liftₑ η) (wkₑ idₑ) σ ⁻¹
                     )
                 ⦙ sub◐ (liftₑ η) (liftₛ σ) M

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

-- (assₛₑₛ)
comp●◑ : ∀ {Γ Ξ Ξ′ Φ} → (σ₁ : Γ ⊢⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (σ₂ : Ξ ⊢⋆ Φ)
                      → (σ₂ ◐ η) ● σ₁ ≡ σ₂ ● (η ◑ σ₁)
comp●◑ σ₁ η ∅        = refl
comp●◑ σ₁ η (σ₂ , M) = _,_ & comp●◑ σ₁ η σ₂
                           ⊗ (sub◑ σ₁ η M ⁻¹)

-- (assₛₛₑ)
comp●◐ : ∀ {Γ Γ′ Ξ Φ} → (η : Γ′ ⊇ Γ) (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ)
                      → (σ₂ ● σ₁) ◐ η ≡ σ₂ ● (σ₁ ◐ η)
comp●◐ η σ₁ ∅        = refl
comp●◐ η σ₁ (σ₂ , M) = _,_ & comp●◐ η σ₁ σ₂
                           ⊗ (sub◐ η σ₁ M ⁻¹)

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

-- (∈-∘ₛ)
get● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (i : Φ ∋ A)
                   → getₛ (σ₂ ● σ₁) i ≡ (sub σ₁ ∘ getₛ σ₂) i
get● σ₁ (σ₂ , M) zero    = refl
get● σ₁ (σ₂ , M) (suc i) = get● σ₁ σ₂ i

-- (Tm-∘ₛ)
mutual
  sub● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Φ ⊢ A)
                     → sub (σ₂ ● σ₁) M ≡ (sub σ₁ ∘ sub σ₂) M
  sub● σ₁ σ₂ (𝓋 i)   = get● σ₁ σ₂ i
  sub● σ₁ σ₂ (ƛ M)   = ƛ & sublift● σ₁ σ₂ M
  sub● σ₁ σ₂ (M ∙ N) = _∙_ & sub● σ₁ σ₂ M
                           ⊗ sub● σ₁ σ₂ N
  sub● σ₁ σ₂ (M , N) = _,_ & sub● σ₁ σ₂ M
                           ⊗ sub● σ₁ σ₂ N
  sub● σ₁ σ₂ (π₁ M)  = π₁ & sub● σ₁ σ₂ M
  sub● σ₁ σ₂ (π₂ M)  = π₂ & sub● σ₁ σ₂ M
  sub● σ₁ σ₂ τ       = refl

  sublift● : ∀ {Γ Ξ Φ A B} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Φ , B ⊢ A)
                           → sub (liftₛ {B} (σ₂ ● σ₁)) M ≡
                              (sub (liftₛ σ₁) ∘ sub (liftₛ σ₂)) M
  sublift● σ₁ σ₂ M = (λ σ′ → sub (σ′ , 0) M)
                     & ( comp●◐ (wkₑ idₑ) σ₁ σ₂
                       ⦙ (σ₂ ●_) & (lid◑ (wkₛ σ₁) ⁻¹)
                       ⦙ comp●◑ (liftₛ σ₁) (wkₑ idₑ) σ₂ ⁻¹
                       )
                   ⦙ sub● (liftₛ σ₁) (liftₛ σ₂) M

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

-- (∈-idₛ)
idgetₛ : ∀ {Γ A} → (i : Γ ∋ A)
                 → getₛ idₛ i ≡ 𝓋 i
idgetₛ zero    = refl
idgetₛ (suc i) = get◐ (wkₑ idₑ) idₛ i
               ⦙ wk & idgetₛ i
               ⦙ 𝓋 ∘ suc & idgetₑ i

-- (Tm-idₛ)
idsub : ∀ {Γ A} → (M : Γ ⊢ A)
                → sub idₛ M ≡ M
idsub (𝓋 i)   = idgetₛ i
idsub (ƛ M)   = ƛ & idsub M
idsub (M ∙ N) = _∙_ & idsub M
                    ⊗ idsub N
idsub (M , N) = _,_ & idsub M
                    ⊗ idsub N
idsub (π₁ M)  = π₁ & idsub M
idsub (π₂ M)  = π₂ & idsub M
idsub τ       = refl

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

-- (idrₛ)
rid● : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → σ ● idₛ ≡ σ
rid● ∅       = refl
rid● (σ , M) = _,_ & rid● σ
                   ⊗ idsub M

-- (idlₛ)
lid● : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → idₛ ● σ ≡ σ
lid● ∅       = refl
lid● (σ , M) = (_, M) & ( comp●◑ (σ , M) (wkₑ idₑ) idₛ
                        ⦙ lid● (idₑ ◑ σ)
                        ⦙ lid◑ σ
                        )

-- (assₛ)
assoc● : ∀ {Γ Ξ Φ Ψ} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (σ₃ : Φ ⊢⋆ Ψ)
                     → (σ₃ ● σ₂) ● σ₁ ≡ σ₃ ● (σ₂ ● σ₁)
assoc● σ₁ σ₂ ∅        = refl
assoc● σ₁ σ₂ (σ₃ , M) = _,_ & assoc● σ₁ σ₂ σ₃
                            ⊗ (sub● σ₁ σ₂ M ⁻¹)

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

𝗦𝗧𝗟𝗖 : Category 𝒞 _⊢⋆_
𝗦𝗧𝗟𝗖 =
  record
    { idₓ    = idₛ
    ; _⋄_    = _●_
    ; lid⋄   = lid●
    ; rid⋄   = rid●
    ; assoc⋄ = assoc●
    }

subPsh : 𝒯 → Presheaf₀ 𝗦𝗧𝗟𝗖
subPsh A =
  record
    { Fₓ  = _⊢ A
    ; F   = sub
    ; idF = fext! idsub
    ; F⋄  = λ σ₁ σ₂ → fext! (sub● σ₂ σ₁)
    }

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties, related to products, that rely on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Product.Properties.WithK where

open import Data.Product
open import Data.Product.Properties
open import Function
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- Equality

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

  ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
  ,-injective refl = refl , refl

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

  ,-injectiveʳ : ∀ {a} {b c : B a} → (Σ A B ∋ (a , b)) ≡ (a , c) → b ≡ c
  ,-injectiveʳ refl = refl

  ≡-dec : Decidable _≡_ → (∀ {a} → Decidable {A = B a} _≡_) →
          Decidable {A = Σ A B} _≡_
  ≡-dec dec₁ dec₂ (a , x) (b , y) with dec₁ a b
  ... | no  a≢b  = no (a≢b ∘ ,-injectiveˡ)
  ... | yes refl with dec₂ x y
  ...   | no x≢y   = no (x≢y ∘ ,-injectiveʳ)
  ...   | yes refl = yes refl


text:
module Oscar.Object {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Category.Category
open import Oscar.Category.Functor
open import Oscar.Category.Morphism
open import Oscar.Category.Semifunctor
open import Oscar.Category.Semigroupoid
open import Oscar.Category.Setoid
open import Oscar.Data.Nat
{-
open import Oscar.Data.AList FunctionName
open import Oscar.Data.Equality
open import Oscar.Data.Equality.properties
open import Oscar.Data.Fin
open import Oscar.Data.List
open import Oscar.Data.Nat
open import Oscar.Data.Product
open import Oscar.Data.Step FunctionName
open import Oscar.Data.Term FunctionName
open import Oscar.Data.Term.internal.SubstituteAndSubstitution FunctionName
open import Oscar.Data.Unit
-}
open import Oscar.Function
open import Oscar.Level

{-
List : Set
ListNatAction : Nat → Set
ListNatMorphism : Nat → Nat → Set

Nat : Set
NatNatAction : Nat → Set
NatNatMorphism : Nat → Nat → Set
-}

{-
data ⋆ : Set where
  ∅ : ⋆
  ↧ : ⋆ → ⋆

data ⟱ {a} {A : Set a} : Set a where

data Nat[_↦_] (m : Nat) : Nat → Set where
  zero : Nat[ m ↦ m ]
  suc : ∀ {n} → Nat[ m ↦ n ] → Nat[ m ↦ suc n ]

_+²_ : ∀ {i₂ i₃} → Nat[ i₂ ↦ i₃ ] → ∀ {i₁} → Nat[ i₁ ↦ i₂ ] → Nat[ i₁ ↦ i₃ ]
zero +² y = y
suc x +² y = suc (x +² y)

data

Nat↥ = Fin

bar = Nat[ 0 ↦ 3 ]
br = Nat
br2 = Nat↥ 3
-}

open import Oscar.Data5

data Indexed : Set (lsuc ℓ) where
  iset₀ : (⟦⟧ → Set) → Indexed
  isetℓ : (⟦⟧ → Set ℓ) → Indexed
  vec : ⟦⟧ → Indexed → Indexed
  list : Indexed → Indexed
  function : Indexed → Indexed → Indexed

data IsMonoid : Indexed → Set where
  list : ∀ i → IsMonoid (list i)
  function : ∀ i j → IsMonoid (function i j)
  vec : ∀ n i → IsMonoid

open import Level

test-l : ∀ {ℓ} {ℓ'} → (⟦⟧ → Lift {ℓ = ℓ} Set) → (⟦⟧ → Lift {ℓ = ℓ'} Set)
test-l f n = lift (lower (f n))

data Categorical : Set (lsuc ℓ) where
  set₀ : (⟦⟧ → ⟦⟧ → Set) → Categorical
  setℓ : (⟦⟧ → ⟦⟧ → Set ℓ) → Categorical
  function : Indexed → Indexed → Categorical {- e.g. Fin m → Term n -}
  monoidal-function : Indexed → Indexed → Categorical {- e.g. Fin n → Term n -}

alist = setℓ AList

ifin = iset₀ Fin
iterm = isetℓ Term
iterms = λ N → isetℓ (Terms N)
istep = isetℓ Step
iliststep = list (istep)

finterm = relational-function ifin iterm
termterm = relational-function iterm iterm
termsterms = λ N → relational-function (iterms N) (iterms N)
stepstep = relational-function istep istep

data Functorial : Categorical → Categorical → Set (lsuc ℓ) where
  unpack : Functorial alist finterm
  substitute : Functorial finterm termterm
  substitutes : (N : ⟦⟧) → Functorial finterm (termsterms N)
  stepify : Functorial termterm stepstep
  collapse : (n : Nat) → Arrow (listStepN n) (termtermN n)
  reduce : (n : Nat) → Arrow (termtermN n) termterm
  COMPOSE : ∀ {o₂ o₃} → Functorial o₂ o₃ → ∀ {o₁} → Functorial o₁ o₂ → Functorial o₁ o₃

data Cat : Set where
  identity : Cat
  cat : Category → Cat
  compose :

--  sustitute : Functorial

--   unpack : Arrow alist finterm
--   substitute : Arrow finterm termterm
--   substitutes : (N : Nat) → Arrow finterm (termsterms N)
--   stepify : Arrow termterm stepstep
--   collapse : (n : Nat) → Arrow (listStepN n) (termtermN n)
--   reduce : (n : Nat) → Arrow (termtermN n) termterm
--   COMPOSE : ∀ {o₂ o₃} → Arrow o₂ o₃ → ∀ {o₁} → Arrow o₁ o₂ → Arrow o₁ o₃

--   finterm : Object
--   termterm : Object
--   termsterms : Nat → Object
--   stepstep : Object
--   listStepN : Nat → Object
--   termtermN : Nat → Object
--   list∘ : Object → Object

-- {-
-- object⋆ : Object → Set _
-- object⋆ alist = Nat
-- object⋆ finterm = Nat
-- object⋆ termterm = Nat
-- object⋆ (termsterms N) = Nat
-- object⋆ stepstep = Nat
-- object⋆ (listStepN _) = ⊤
-- object⋆ (termtermN _) = ⊤

-- objectMorphism : (o : Object) → Morphism (object⋆ o) 𝔣 𝔣
-- objectMorphism alist = ⇧ AList
-- objectMorphism finterm = Fin ⇨ Term
-- objectMorphism termterm = Term ⇨ Term
-- objectMorphism (termsterms N) = Terms N ⇨ Terms N
-- objectMorphism stepstep = Step ⇨ Step
-- Setoid.⋆ ((objectMorphism (listStepN n) Morphism.⇒ _) _) = List (Step n)
-- IsSetoid._≋_ (Setoid.isSetoid ((objectMorphism (listStepN N) Morphism.⇒ _) _)) = _≡_
-- Setoid.⋆ ((objectMorphism (termtermN n) Morphism.⇒ _) _) = Term n → Term n
-- IsSetoid._≋_ (Setoid.isSetoid ((objectMorphism (termtermN N) Morphism.⇒ _) _)) = _≡̇_
-- IsSetoid._≋_ (Morphism.isSetoid (objectMorphism (termtermN N))) = _≡̇_
-- -}

-- objectCategory : Object → Category lzero 𝔣 𝔣
-- objectCategory alist = {!!}
-- objectCategory finterm = 𝔾₁
-- objectCategory termterm = 𝔾₂
-- objectCategory (termsterms N) = 𝔾₂ₛ N
-- objectCategory stepstep = {!!}
-- objectCategory (listStepN x) = {!!}
-- objectCategory (termtermN x) = {!!}
-- Semigroupoid.⋆ (Category.semigroupoid (objectCategory (list∘ G))) = List (Category.⋆ (objectCategory G))
-- Morphism._⇒_ (Semigroupoid.𝔐 (Category.semigroupoid (objectCategory (list∘ G)))) = {!!}
-- Morphism.isSetoid (Semigroupoid.𝔐 (Category.semigroupoid (objectCategory (list∘ G)))) = {!!}
-- Semigroupoid._∙_ (Category.semigroupoid (objectCategory (list∘ G))) = {!!}
-- Semigroupoid.isSemigroupoid (Category.semigroupoid (objectCategory (list∘ G))) = {!!}
-- Category.ε (objectCategory (list∘ G)) = {!!}
-- Category.isCategory (objectCategory (list∘ G)) = {!!}

-- data Arrow : Object → Object → Set where
--   unpack : Arrow alist finterm
--   substitute : Arrow finterm termterm
--   substitutes : (N : Nat) → Arrow finterm (termsterms N)
--   stepify : Arrow termterm stepstep
--   collapse : (n : Nat) → Arrow (listStepN n) (termtermN n)
--   reduce : (n : Nat) → Arrow (termtermN n) termterm
--   COMPOSE : ∀ {o₂ o₃} → Arrow o₂ o₃ → ∀ {o₁} → Arrow o₁ o₂ → Arrow o₁ o₃

-- data SimpleArrow : ∀ {o1 o2} → Arrow o1 o2 → Set where
--   unpack : SimpleArrow unpack
--   substitute : SimpleArrow substitute
--   substitutes : (N : Nat) → SimpleArrow (substitutes N)
--   stepify : SimpleArrow stepify
--   collapse : (n : Nat) → SimpleArrow (collapse n)
--   reduce : (n : Nat) → SimpleArrow (reduce n)

-- import Data.List as LIST
-- open import Algebra using (Monoid)

-- serialiseArrow : ∀ {o1 o2} → Arrow o1 o2 → List (∃ λ o1 → ∃ λ o2 → ∃ λ (a : Arrow o1 o2) → SimpleArrow a)
-- serialiseArrow unpack = (_ , _ , _ , unpack) ∷ []
-- serialiseArrow substitute = {!!}
-- serialiseArrow (substitutes N) = {!!}
-- serialiseArrow stepify = {!!}
-- serialiseArrow (collapse n) = {!!}
-- serialiseArrow (reduce n) = {!!}
-- serialiseArrow (COMPOSE g f) =
--   let g' = serialiseArrow g
--       f' = serialiseArrow f
--   in Monoid._∙_ (LIST.monoid (∃ (λ o1 → ∃ (λ o2 → ∃ SimpleArrow)))) g' f'

-- open import Data.Empty

-- eqArrow : ∀ {o1 o2} → Arrow o1 o2 → Arrow o1 o2 → Set
-- eqArrow x y = serialiseArrow x ≡ serialiseArrow y

-- open IsSemifunctor ⦃ … ⦄ using () renaming (extensionality to ext; distributivity to dist)

-- module _
--   {𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ 𝔬₃ 𝔪₃ 𝔮₃}
--   (c₁ : Semigroupoid 𝔬₁ 𝔪₁ 𝔮₁)
--   (c₂ : Semigroupoid 𝔬₂ 𝔪₂ 𝔮₂)
--   (c₃ : Semigroupoid 𝔬₃ 𝔪₃ 𝔮₃)
--   where
--   private
--     module 𝔊₁ = Semigroupoid c₁
--     module 𝔊₂ = Semigroupoid c₂
--     module 𝔊₃ = Semigroupoid c₃
--   composeS : ∀
--     {μ₁₂ : 𝔊₁.⋆ → 𝔊₂.⋆}
--     (𝔣₁₂ : ∀ {x y} → x 𝔊₁.↦ y → μ₁₂ x 𝔊₂.↦ μ₁₂ y)
--     {μ₂₃ : 𝔊₂.⋆ → 𝔊₃.⋆}
--     (𝔣₂₃ : ∀ {x y} → x 𝔊₂.↦ y → μ₂₃ x 𝔊₃.↦ μ₂₃ y)
--     ⦃ _ : IsSemifunctor (c₁ , c₂) 𝔣₁₂ ⦄
--     ⦃ _ : IsSemifunctor (c₂ , c₃) 𝔣₂₃ ⦄
--     → IsSemifunctor (c₁ , c₃) (𝔣₂₃ ∘ 𝔣₁₂)
--   IsSemifunctor.extensionality (composeS 𝔣₁₂ 𝔣₂₃ ⦃ isS₁ ⦄ ⦃ isS₂ ⦄) f₁≋f₂ = ext ⦃ isS₂ ⦄ (ext ⦃ isS₁ ⦄ f₁≋f₂)
--   IsSemifunctor.distributivity (composeS {μ₁₂} 𝔣₁₂ {μ₂₃} 𝔣₂₃ ⦃ isS₁ ⦄ ⦃ isS₂ ⦄) {x} {y} f {z} g =
--     let eq₁ = ext ⦃ isS₂ ⦄ (dist ⦃ isS₁ ⦄ f g)
--         eq₂ = dist ⦃ isS₂ ⦄ (𝔣₁₂ f) (𝔣₁₂ g)
--         instance _ = IsSetoid.isEquivalence 𝔊₃.isSetoid
--     in transitivity eq₁ eq₂

-- module _
--   {𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ 𝔬₃ 𝔪₃ 𝔮₃}
--   (c₁ : Category 𝔬₁ 𝔪₁ 𝔮₁)
--   (c₂ : Category 𝔬₂ 𝔪₂ 𝔮₂)
--   (c₃ : Category 𝔬₃ 𝔪₃ 𝔮₃)
--   where
--   private
--     module 𝔊₁ = Category c₁
--     module 𝔊₂ = Category c₂
--     module 𝔊₃ = Category c₃
--   composeF : ∀
--     {μ₁₂ : 𝔊₁.⋆ → 𝔊₂.⋆}
--     (𝔣₁₂ : ∀ {x y} → x 𝔊₁.↦ y → μ₁₂ x 𝔊₂.↦ μ₁₂ y)
--     {μ₂₃ : 𝔊₂.⋆ → 𝔊₃.⋆}
--     (𝔣₂₃ : ∀ {x y} → x 𝔊₂.↦ y → μ₂₃ x 𝔊₃.↦ μ₂₃ y)
--     ⦃ _ : IsFunctor (c₁ , c₂) 𝔣₁₂ ⦄
--     ⦃ _ : IsFunctor (c₂ , c₃) 𝔣₂₃ ⦄
--     → IsFunctor (c₁ , c₃) (𝔣₂₃ ∘ 𝔣₁₂)
--   IsFunctor.isSemifunctor (composeF 𝔣₁₂ 𝔣₂₃ ⦃ isF₁ ⦄ ⦃ isF₂ ⦄) = composeS _ _ _ _ _ ⦃ (IsFunctor.isSemifunctor isF₁) ⦄ ⦃ (IsFunctor.isSemifunctor isF₂) ⦄
--   IsFunctor.identity (composeF {μ₁₂} 𝔣₁₂ 𝔣₂₃ ⦃ isF₁ ⦄ ⦃ isF₂ ⦄) x =
--     let f₁₂ε≋ε = identity ⦃ isF₁ ⦄ x
--         f₂₃f₁₂ε≋f₂₃ε = ext ⦃ IsFunctor.isSemifunctor isF₂ ⦄ f₁₂ε≋ε
--         f₂₃ε≋ε = identity ⦃ isF₂ ⦄ (μ₁₂ x)
--         instance _ = IsSetoid.isEquivalence 𝔊₃.isSetoid
--     in transitivity f₂₃f₁₂ε≋f₂₃ε f₂₃ε≋ε

-- --𝔬₁ 𝔪₁ 𝔮₁ 𝔬₃ 𝔪₃ 𝔮₃
-- --composeF 𝔣₁₂ 𝔣₂₃ = (c₁ , c₃) , (𝔣₂₃ ∘ 𝔣₁₂)

-- arrowIsFunctor : ∀ {o₁ o₂} → Arrow o₁ o₂
--   → ∃ λ μ
--   → (let c1 = objectCategory o₁)
--     (let c2 = objectCategory o₂)
--     (let module 𝔊₁ = Category c1)
--     (let module 𝔊₂ = Category c2)
--   → ∃ λ (f : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y)
--   → (IsFunctor (objectCategory o₁ , objectCategory o₂) {μ} f)
-- arrowIsFunctor unpack = {!!}
-- arrowIsFunctor substitute = _ , _ , IsFunctor𝔾₁,₂◂
-- arrowIsFunctor (substitutes N) = _ , _ , IsFunctor𝔾₁,₂ₛ◂ {N}
-- arrowIsFunctor stepify = {!!}
-- arrowIsFunctor (collapse n) = {!!}
-- arrowIsFunctor (reduce n) = {!!}
-- arrowIsFunctor (COMPOSE a1 a2) =
--   let _ , _ , isF1 = arrowIsFunctor a1
--       _ , _ , isF2 = arrowIsFunctor a2
--   in _ , _ , composeF _ _ _ _ _ ⦃ isF2 ⦄ ⦃ isF1 ⦄

-- arrowFunctor : ∀ {o₁ o₂} → Arrow o₁ o₂ → Functor _ _ _ _ _ _
-- arrowFunctor {o₁} {o₂} a =
--   let cs , f , IF = arrowIsFunctor a
--       instance _ = IF
--   in (objectCategory o₁ , objectCategory o₂) , f

-- category : Category _ _ _
-- Semigroupoid.⋆ (Category.semigroupoid category) = Object
-- Setoid.⋆ ((Semigroupoid.𝔐 (Category.semigroupoid category) Morphism.⇒ o1) o2) = Arrow o1 o2
-- IsSetoid._≋_ (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid category) Morphism.⇒ x) x₁)) = {!!}
-- IsSetoid.isEquivalence (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid category) Morphism.⇒ x) x₁)) = {!!}
-- IsSetoid._≋_ (Morphism.isSetoid (Semigroupoid.𝔐 (Category.semigroupoid category))) = eqArrow
-- IsSetoid.isEquivalence (Morphism.isSetoid (Semigroupoid.𝔐 (Category.semigroupoid category))) = {!!}
-- Semigroupoid._∙_ (Category.semigroupoid category) g f = COMPOSE g f
-- IsSemigroupoid.extensionality (Semigroupoid.isSemigroupoid (Category.semigroupoid category)) = {!!}
-- IsSemigroupoid.associativity (Semigroupoid.isSemigroupoid (Category.semigroupoid category)) = {!!}
-- Category.ε category = {!!}
-- IsCategory.left-identity (Category.isCategory category) = {!!}
-- IsCategory.right-identity (Category.isCategory category) = {!!}


text:
module Syntax where

open import Stack public

-- Abstract symbols, or atoms.

abstract
  Atom : Set
  Atom = Nat

-- Types, or propositions in constructive logic.

infixl 9 _⩕_
infixr 7 _⇒_
data Type : Set where
  α_   : Atom → Type
  _⇒_ : Type → Type → Type
  _⩕_  : Type → Type → Type
  ⫪   : Type

-- Contexts, or stacks of types.

Context : Set
Context = Stack Type

-- Derivations, or syntactic entailment.

infix 3 _⊢_
data _⊢_ : Context → Type → Set where
  var   : ∀ {A Γ}   → A ∈ Γ → Γ ⊢ A
  lam   : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
  app   : ∀ {A B Γ} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  pair  : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ⩕ B
  fst   : ∀ {A B Γ} → Γ ⊢ A ⩕ B → Γ ⊢ A
  snd   : ∀ {A B Γ} → Γ ⊢ A ⩕ B → Γ ⊢ B
  unit  : ∀ {Γ}     → Γ ⊢ ⫪

-- Shorthand for variables.

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → Γ , A , B ⊢ A
v₁ = var i₁

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

-- Stacks of derivations, or simultaneous syntactic entailment.

infix 3 _⊢⋆_
_⊢⋆_ : Context → Stack Type → Set
Γ ⊢⋆ ∅     = ⊤
Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ ∧ Γ ⊢ A

-- Monotonicity of syntactic entailment with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ p (var i)      = var (mono∈ p i)
mono⊢ p (lam d)      = lam (mono⊢ (keep p) d)
mono⊢ p (app d e)    = app (mono⊢ p d) (mono⊢ p e)
mono⊢ p (pair d e)   = pair (mono⊢ p d) (mono⊢ p e)
mono⊢ p (fst d)      = fst (mono⊢ p d)
mono⊢ p (snd d)      = snd (mono⊢ p d)
mono⊢ p unit         = unit

mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
mono⊢⋆ {∅}     p ∙       = ∙
mono⊢⋆ {Ξ , A} p (ζ , d) = mono⊢⋆ p ζ , mono⊢ p d

-- TODO: Naming things.

idmono⊢ : ∀ {A Γ} → (d : Γ ⊢ A) → mono⊢ refl⊆ d ≡ d
idmono⊢ (var {A} i) = cong var (idmono∈ i)
idmono⊢ (lam d)     = cong lam (idmono⊢ d)
idmono⊢ (app d e)   = cong² app (idmono⊢ d) (idmono⊢ e)
idmono⊢ (pair d e)  = cong² pair (idmono⊢ d) (idmono⊢ e)
idmono⊢ (fst d)     = cong fst (idmono⊢ d)
idmono⊢ (snd d)     = cong snd (idmono⊢ d)
idmono⊢ unit        = refl

idmono⊢⋆ : ∀ {Ξ Γ} → (ζ : Γ ⊢⋆ Ξ) → mono⊢⋆ refl⊆ ζ ≡ ζ
idmono⊢⋆ {∅}     ∙       = refl
idmono⊢⋆ {Ξ , A} (ζ , d) = cong² _,_ (idmono⊢⋆ ζ) (idmono⊢ d)

-- Reflexivity of simultaneous syntactic entailment.

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

-- Substitution.

[_≔_]∈_ : ∀ {A C Γ} → (i : C ∈ Γ) → Γ ∖ i ⊢ C → A ∈ Γ → Γ ∖ i ⊢ A
[ i ≔ c ]∈  j      with i ≟∈ j
[ i ≔ c ]∈ .i      | same   = c
[ i ≔ c ]∈ ._      | diff j = var j

[_≔_]_ : ∀ {A C Γ} → (i : C ∈ Γ) → Γ ∖ i ⊢ C → Γ ⊢ A → Γ ∖ i ⊢ A
[ i ≔ c ] var j    = [ i ≔ c ]∈ j
[ i ≔ c ] lam d    = lam ([ pop i ≔ mono⊢ weak⊆ c ] d)
[ i ≔ c ] app d e  = app ([ i ≔ c ] d) ([ i ≔ c ] e)
[ i ≔ c ] pair d e = pair ([ i ≔ c ] d) ([ i ≔ c ] e)
[ i ≔ c ] fst d    = fst ([ i ≔ c ] d)
[ i ≔ c ] snd d    = snd ([ i ≔ c ] d)
[ i ≔ c ] unit     = unit

-- Grafting of derivation trees, or simultaneous substitution, or cut.

graft∈ : ∀ {A Ξ Γ} → Γ ⊢⋆ Ξ → A ∈ Ξ → Γ ⊢ A
graft∈ (ζ , d) top     = d
graft∈ (ζ , d) (pop i) = graft∈ ζ i

graft⊢ : ∀ {A Ξ Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
graft⊢ ζ (var i)      = graft∈ ζ i
graft⊢ ζ (lam d)      = lam (graft⊢ (mono⊢⋆ weak⊆ ζ , v₀) d)
graft⊢ ζ (app d e)    = app (graft⊢ ζ d) (graft⊢ ζ e)
graft⊢ ζ (pair d e)   = pair (graft⊢ ζ d) (graft⊢ ζ e)
graft⊢ ζ (fst d)      = fst (graft⊢ ζ d)
graft⊢ ζ (snd d)      = snd (graft⊢ ζ d)
graft⊢ ζ unit         = unit

-- Derivations, or syntactic entailment, in normal form.

mutual
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ : Context → Type → Set where
    neⁿᶠ   : ∀ {A Γ}   → Γ ⊢ⁿᵉ A → Γ ⊢ⁿᶠ A
    lamⁿᶠ  : ∀ {A B Γ} → Γ , A ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ⇒ B
    pairⁿᶠ : ∀ {A B Γ} → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ⩕ B
    unitⁿᶠ : ∀ {Γ}     → Γ ⊢ⁿᶠ ⫪

  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ : Context → Type → Set where
    varⁿᵉ  : ∀ {A Γ}   → A ∈ Γ → Γ ⊢ⁿᵉ A
    appⁿᵉ  : ∀ {A B Γ} → Γ ⊢ⁿᵉ A ⇒ B → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᵉ B
    fstⁿᵉ  : ∀ {A B Γ} → Γ ⊢ⁿᵉ A ⩕ B → Γ ⊢ⁿᵉ A
    sndⁿᵉ  : ∀ {A B Γ} → Γ ⊢ⁿᵉ A ⩕ B → Γ ⊢ⁿᵉ B

-- Shorthand for variables.

v₀ⁿᵉ : ∀ {A Γ} → Γ , A ⊢ⁿᵉ A
v₀ⁿᵉ = varⁿᵉ top

-- Stacks of derivations, or simultaneous syntactic entailment, in normal form.

infix 3 _⊢⋆ⁿᵉ_
_⊢⋆ⁿᵉ_ : Context → Stack Type → Set
Γ ⊢⋆ⁿᵉ ∅     = ⊤
Γ ⊢⋆ⁿᵉ Ξ , A = Γ ⊢⋆ⁿᵉ Ξ ∧ Γ ⊢ⁿᵉ A

-- Translation from normal form to arbitrary form.

mutual
  nf→af : ∀ {A Γ} → Γ ⊢ⁿᶠ A → Γ ⊢ A
  nf→af (neⁿᶠ d)     = ne→af d
  nf→af (lamⁿᶠ d)    = lam (nf→af d)
  nf→af (pairⁿᶠ d e) = pair (nf→af d) (nf→af e)
  nf→af unitⁿᶠ       = unit

  ne→af : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊢ A
  ne→af (varⁿᵉ i)    = var i
  ne→af (appⁿᵉ d e)  = app (ne→af d) (nf→af e)
  ne→af (fstⁿᵉ d)    = fst (ne→af d)
  ne→af (sndⁿᵉ d)    = snd (ne→af d)

-- Monotonicity of syntactic entailment with respect to context inclusion, in normal form.

mutual
  mono⊢ⁿᶠ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ⁿᶠ A → Γ′ ⊢ⁿᶠ A
  mono⊢ⁿᶠ p (neⁿᶠ d)     = neⁿᶠ (mono⊢ⁿᵉ p d)
  mono⊢ⁿᶠ p (lamⁿᶠ d)    = lamⁿᶠ (mono⊢ⁿᶠ (keep p) d)
  mono⊢ⁿᶠ p (pairⁿᶠ d e) = pairⁿᶠ (mono⊢ⁿᶠ p d) (mono⊢ⁿᶠ p e)
  mono⊢ⁿᶠ p unitⁿᶠ       = unitⁿᶠ

  mono⊢ⁿᵉ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ⁿᵉ A → Γ′ ⊢ⁿᵉ A
  mono⊢ⁿᵉ p (varⁿᵉ i)    = varⁿᵉ (mono∈ p i)
  mono⊢ⁿᵉ p (appⁿᵉ d e)  = appⁿᵉ (mono⊢ⁿᵉ p d) (mono⊢ⁿᶠ p e)
  mono⊢ⁿᵉ p (fstⁿᵉ d)    = fstⁿᵉ (mono⊢ⁿᵉ p d)
  mono⊢ⁿᵉ p (sndⁿᵉ d)    = sndⁿᵉ (mono⊢ⁿᵉ p d)

mono⊢⋆ⁿᵉ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ⁿᵉ Ξ → Γ′ ⊢⋆ⁿᵉ Ξ
mono⊢⋆ⁿᵉ {∅}     p ∙       = ∙
mono⊢⋆ⁿᵉ {Ξ , A} p (ζ , d) = mono⊢⋆ⁿᵉ p ζ , mono⊢ⁿᵉ p d

-- TODO: Naming things.

mutual
  idmono⊢ⁿᶠ : ∀ {A Γ} → (d : Γ ⊢ⁿᶠ A) → mono⊢ⁿᶠ refl⊆ d ≡ d
  idmono⊢ⁿᶠ (neⁿᶠ d)     = cong neⁿᶠ (idmono⊢ⁿᵉ d)
  idmono⊢ⁿᶠ (lamⁿᶠ d)    = cong lamⁿᶠ (idmono⊢ⁿᶠ d)
  idmono⊢ⁿᶠ (pairⁿᶠ d e) = cong² pairⁿᶠ (idmono⊢ⁿᶠ d) (idmono⊢ⁿᶠ e)
  idmono⊢ⁿᶠ unitⁿᶠ       = refl

  idmono⊢ⁿᵉ : ∀ {A Γ} → (d : Γ ⊢ⁿᵉ A) → mono⊢ⁿᵉ refl⊆ d ≡ d
  idmono⊢ⁿᵉ (varⁿᵉ i)    = cong varⁿᵉ (idmono∈ i)
  idmono⊢ⁿᵉ (appⁿᵉ d e)  = cong² appⁿᵉ (idmono⊢ⁿᵉ d) (idmono⊢ⁿᶠ e)
  idmono⊢ⁿᵉ (fstⁿᵉ d)    = cong fstⁿᵉ (idmono⊢ⁿᵉ d)
  idmono⊢ⁿᵉ (sndⁿᵉ d)    = cong sndⁿᵉ (idmono⊢ⁿᵉ d)

idmono⊢⋆ⁿᵉ : ∀ {Ξ Γ} → (ζ : Γ ⊢⋆ⁿᵉ Ξ) → mono⊢⋆ⁿᵉ refl⊆ ζ ≡ ζ
idmono⊢⋆ⁿᵉ {∅}     ∙       = refl
idmono⊢⋆ⁿᵉ {Ξ , A} (ζ , d) = cong² _,_ (idmono⊢⋆ⁿᵉ ζ) (idmono⊢ⁿᵉ d)

-- Reflexivity of simultaneous syntactic entailment, in normal form.

refl⊢⋆ⁿᵉ : ∀ {Γ} → Γ ⊢⋆ⁿᵉ Γ
refl⊢⋆ⁿᵉ {∅}     = ∙
refl⊢⋆ⁿᵉ {Γ , A} = mono⊢⋆ⁿᵉ weak⊆ refl⊢⋆ⁿᵉ , v₀ⁿᵉ

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness


text:
------------------------------------------------------------------------
-- Encoder and decoder instances
------------------------------------------------------------------------

open import Atom

module Coding.Instances (atoms : χ-atoms) where

open import Prelude

open import Chi            atoms
open import Free-variables atoms
open import Values         atoms

open χ-atoms atoms

open import Coding atoms as Coding using (Rep; module Code)

instance

  rep-Consts-Exp : ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ →
                   Rep A Exp
  rep-Consts-Exp = Coding.rep-Consts-Exp

  rep-Consts-Closed-exp :
    ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ → Rep A Closed-exp
  rep-Consts-Closed-exp = Coding.rep-Consts-Closed-exp

  rep-Bool : Rep Bool Consts
  rep-Bool = Code.rep Coding.code-Bool

  rep-ℕ : Rep ℕ Consts
  rep-ℕ = Code.rep Coding.code-ℕ

  rep-Var : Rep Var Consts
  rep-Var = Code.rep Coding.code-Var

  rep-Const : Rep Const Consts
  rep-Const = Code.rep Coding.code-Const

  rep-× : ∀ {a b} {A : Type a} {B : Type b}
            ⦃ c : Rep A Consts ⦄ ⦃ d : Rep B Consts ⦄ →
          Rep (A × B) Consts
  rep-× = Coding.rep-×

  rep-Var⋆ : Rep (List Var) Consts
  rep-Var⋆ = Code.rep Coding.code-Var⋆

  rep-Exp : Rep Exp Consts
  rep-Exp = Code.rep Coding.code-Exp

  rep-Br : Rep Br Consts
  rep-Br = Code.rep Coding.code-Br

  rep-Exps : Rep (List Exp) Consts
  rep-Exps = Code.rep Coding.code-Exps

  rep-Brs : Rep (List Br) Consts
  rep-Brs = Code.rep Coding.code-Brs

  rep-Closed : Rep Closed-exp Consts
  rep-Closed = Code.rep Coding.code-Closed

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
module Nat where

import Bool
open Bool

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

infixr 25 _+_

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

infix 10 _==_ _<_

_==_ : Nat -> Nat -> Bool
zero  == zero  = true
suc n == zero  = false
zero  == suc m = false
suc n == suc m = n == m

_<_ : Nat -> Nat -> Bool
n     < zero  = false
zero  < suc m = true
suc n < suc m = n < m

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
-- {-# BUILTIN NATPLUS _+_ #-}
-- {-# BUILTIN NATEQUALS _==_ #-}
-- {-# BUILTIN NATLESS _<_ #-}

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module #1 where

open import Level
open import Relation.Binary.PropositionalEquality

{-
Exercise 1.1. Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C.
Show that we have h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f .
-}

-- Function composition
_∘_ : ∀ {a b c}{A : Set a}{B : Set b}{C : Set c} → (B → C) → (A → B) → A → C
f ∘ g = λ x → f (g x)

-- Proof of associativity of composition
∘-assoc : ∀ {a b c d}{A : Set a}{B : Set b}{C : Set c}{D : Set d} →
            (h : C → D) → (g : B → C) → (f : A → B) →
            h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
∘-assoc _ _ _ = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Miscellaneous.InstanceLoop where

open import Type

postulate A : TYPE
postulate B : TYPE
postulate C : TYPE

instance
  postulate ab : ⦃ A ⦄ → B

instance
  postulate ba : ⦃ B ⦄ → A

postulate a : A

test-a : B
test-a = ab

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Lemmachine.Resource.Universe where
open import Lemmachine.Request
open import Lemmachine.Response
open import Data.Maybe
open import Data.List
open import Data.Product
open import Data.Bool
open import Data.String

AuthHead = Bool
MediaType = String
Handler = String
Charset = String
CharsetConverter = String
Encoding = String
Encoder = String
MovedURI = String
DateTime = String
ETag = String

data Code : Set where
  resourceExists serviceAvailable isAuthorized : Code
  forbidden allowMissingPost malformedRequest : Code
  uriTooLong knownContentType validContentHeaders : Code
  validEntityLength options allowedMethods : Code
  knownMethods deleteResource deleteCompleted : Code
  postIsCreate createPath processPost : Code
  contentTypesProvided languageAvailable contentTypesAccepted : Code
  charsetsProvided encodingsProvided variances : Code
  isConflict multipleChoices previouslyExisted : Code
  movedPermanently movedTemporarily lastModified : Code
  expires generateETag finishRequest body : Code

El : Code → Set
El resourceExists = Request → Bool
El serviceAvailable = Request → Bool
El isAuthorized = Request → AuthHead
El forbidden = Request → Bool
El allowMissingPost = Request → Bool
El malformedRequest = Request → Bool
El uriTooLong = Request → Bool
El knownContentType = Request → Bool
El validContentHeaders = Request → Bool
El validEntityLength = Request → Bool
El options = Request → List ResponseHeader
El allowedMethods = Request → List Method
El knownMethods = Request → List Method
El deleteResource = Request → Bool
El deleteCompleted = Request → Bool
El postIsCreate = Request → Bool
El createPath = Request → Maybe Path
El processPost = Request → Bool
El contentTypesProvided = Request → List MediaType
El languageAvailable = Request → Bool
El contentTypesAccepted = Request → List (MediaType × Handler)
El charsetsProvided = Request → List (Charset × CharsetConverter)
El encodingsProvided = Request → List (Encoding × Encoder)
El variances = Request → List RequestHeader
El isConflict = Request → Bool
El multipleChoices = Request → Bool
El previouslyExisted = Request → Bool
El movedPermanently = Request → Maybe MovedURI
El movedTemporarily = Request → Maybe MovedURI
El lastModified = Request → Maybe DateTime
El expires = Request → Maybe DateTime
El generateETag = Request → Maybe ETag
El finishRequest = Request → Bool
El body = Status → String

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------------
-- FOTC list terms properties
------------------------------------------------------------------------------

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

module FOTC.Base.List.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- Congruence properties

∷-leftCong : ∀ {x y xs} → x ≡ y → x ∷ xs ≡ y ∷ xs
∷-leftCong refl = refl

∷-rightCong : ∀ {x xs ys} → xs ≡ ys → x ∷ xs ≡ x ∷ ys
∷-rightCong refl = refl

∷-cong : ∀ {x y xs ys} → x ≡ y → xs ≡ ys → x ∷ xs ≡ y ∷ ys
∷-cong refl refl = refl

headCong : ∀ {xs ys} → xs ≡ ys → head₁ xs ≡ head₁ ys
headCong refl = refl

tailCong : ∀ {xs ys} → xs ≡ ys → tail₁ xs ≡ tail₁ ys
tailCong refl = refl

------------------------------------------------------------------------------
-- Injective properties

∷-injective : ∀ {x y xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y ∧ xs ≡ ys
∷-injective {x} {y} {xs} {ys} h = x≡y , xs≡ys
  where
  x≡y : x ≡ y
  x≡y = x              ≡⟨ sym (head-∷ x xs) ⟩
        head₁ (x ∷ xs) ≡⟨ headCong h ⟩
        head₁ (y ∷ ys) ≡⟨ head-∷ y ys ⟩
        y              ∎

  xs≡ys : xs ≡ ys
  xs≡ys = xs             ≡⟨ sym (tail-∷ x xs) ⟩
          tail₁ (x ∷ xs) ≡⟨ tailCong h ⟩
          tail₁ (y ∷ ys) ≡⟨ tail-∷ y ys ⟩
          ys             ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Equivalence.Empty where

open variables

𝟎-equiv : {A : 𝒰 i} → ¬ A → 𝟎 {i} ≃ A
𝟎-equiv ¬a = 𝟎-rec , qinv→isequiv (𝟎-rec ∘ ¬a , 𝟎-ind , 𝟎-rec ∘ ¬a)

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
-- 2014-05-27 Jesper and Andreas

postulate
  A : Set

{-# BUILTIN REWRITE A #-}

-- Expected error:
-- A  does not have the right type for a rewriting relation
-- because it should accept at least two arguments
-- when checking the pragma BUILTIN REWRITE A