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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert         as QuorumCert
import      LibraBFT.Impl.Consensus.ConsensusTypes.TimeoutCertificate as TimeoutCertificate
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.BlockInfo                             as BlockInfo
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.LBFT
open import Optics.All
open import Util.Hash
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                               using (String)

module LibraBFT.Impl.Consensus.ConsensusTypes.SyncInfo where

highestRound : SyncInfo → Round
highestRound self = max (self ^∙ siHighestCertifiedRound) (self ^∙ siHighestTimeoutRound)

verify : SyncInfo → ValidatorVerifier → Either ErrLog Unit

verifyM : SyncInfo → ValidatorVerifier → LBFT (Either ErrLog Unit)
verifyM self validator = pure (verify self validator)

module verify (self : SyncInfo) (validator : ValidatorVerifier) where
  step₀ step₁ step₂ step₃ step₄ step₅ step₆ : Either ErrLog Unit
  here' : List String → List String

  epoch = self ^∙ siHighestQuorumCert ∙ qcCertifiedBlock ∙ biEpoch

  step₀ = do
    lcheck (epoch == self ^∙ siHighestCommitCert ∙ qcCertifiedBlock ∙ biEpoch)
           (here' ("Multi epoch in SyncInfo - HCC and HQC" ∷ []))
    step₁

  step₁ = do
    lcheck (maybeS (self ^∙ siHighestTimeoutCert) true (λ tc -> epoch == tc ^∙ tcEpoch))
           (here' ("Multi epoch in SyncInfo - TC and HQC" ∷ []))
    step₂

  step₂ = do
    lcheck (   self ^∙ siHighestQuorumCert ∙ qcCertifiedBlock ∙ biRound
           ≥? self ^∙ siHighestCommitCert ∙ qcCertifiedBlock ∙ biRound)
           (here' ("HQC has lower round than HCC" ∷ []))
    step₃

  step₃ = do
    lcheck (self ^∙ siHighestCommitCert ∙ qcCommitInfo /= BlockInfo.empty)
           (here' ("HCC has no committed block" ∷ []))
    step₄

  step₄ = do
    QuorumCert.verify (self ^∙ siHighestQuorumCert) validator
    step₅

  step₅ = do
    -- Note: do not use (self ^∙ siHighestCommitCert) because it might be
    -- same as siHighestQuorumCert -- so no need to check again
    maybeS (self ^∙ sixxxHighestCommitCert) (pure unit) (` QuorumCert.verify ` validator)
    step₆

  step₆ = do
    maybeS (self ^∙ siHighestTimeoutCert)   (pure unit) (` TimeoutCertificate.verify ` validator)

  here' t = "SyncInfo" ∷ "verify" ∷ t

verify = verify.step₀

hasNewerCertificates : SyncInfo → SyncInfo → Bool
hasNewerCertificates self other
  = ⌊ self ^∙ siHighestCertifiedRound >? other ^∙ siHighestCertifiedRound ⌋
  ∨ ⌊ self ^∙ siHighestTimeoutRound   >? other ^∙ siHighestTimeoutRound   ⌋
  ∨ ⌊ self ^∙ siHighestCommitRound    >? other ^∙ siHighestCommitRound    ⌋


text:
-- Andrease, 2016-12-31, issue #1975 reported by nad.

-- {-# OPTIONS -v tc.lhs.split:40 #-}

data ⊥ : Set where

record ⊤ : Set where

data Bool : Set where
  true false : Bool

T : Bool → Set
T false = ⊥
T true  = ⊤

module M (b : Bool) where

  data D : Set where
    c : T b → D

open M true

-- The following definition is rejected:

-- rejected : M.D false → ⊥
-- rejected (c x) = x

data D₂ : Set where
  c : D₂

-- WAS: However, the following definition is accepted:

test : M.D false → ⊥
test (c x) = x

-- I think both definitions should be rejected.
-- NOW: Both are rejected.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This file contains:

- Equivalence with the pushout definition
  Written by: Loïc Pujet, September 2019

- Associativity of the join
  Written by: Loïc Pujet, September 2019

-}

{-# OPTIONS --cubical --safe #-}

module Cubical.HITs.Join.Properties where

open import Cubical.Core.Glue

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

open import Cubical.Data.Prod

open import Cubical.HITs.Join.Base
open import Cubical.HITs.Pushout

private
  variable
    ℓ ℓ' : Level

-- Alternative definition of the join using a pushout
joinPushout : (A : Type ℓ) → (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
joinPushout A B = Pushout {A = A × B} proj₁ proj₂

-- Proof that it is equal
joinPushout-iso-join : (A : Type ℓ) → (B : Type ℓ') → Iso (joinPushout A B) (join A B)
joinPushout-iso-join A B = iso joinPushout→join join→joinPushout join→joinPushout→join joinPushout→join→joinPushout
  where
    joinPushout→join : joinPushout A B → join A B
    joinPushout→join (inl x) = inl x
    joinPushout→join (inr x) = inr x
    joinPushout→join (push y i) = push (proj₁ y) (proj₂ y) i

    join→joinPushout : join A B → joinPushout A B
    join→joinPushout (inl x) = inl x
    join→joinPushout (inr x) = inr x
    join→joinPushout (push a b i) = push (a , b) i

    joinPushout→join→joinPushout : ∀ x → join→joinPushout (joinPushout→join x) ≡ x
    joinPushout→join→joinPushout (inl x) = refl
    joinPushout→join→joinPushout (inr x) = refl
    joinPushout→join→joinPushout (push (a , b) j) = refl

    join→joinPushout→join : ∀ x → joinPushout→join (join→joinPushout x) ≡ x
    join→joinPushout→join (inl x) = refl
    join→joinPushout→join (inr x) = refl
    join→joinPushout→join (push a b j) = refl

-- We will need both the equivalence and path version
joinPushout≃join : (A : Type ℓ) → (B : Type ℓ') → joinPushout A B ≃ join A B
joinPushout≃join A B = isoToEquiv (joinPushout-iso-join A B)

joinPushout≡join : (A : Type ℓ) → (B : Type ℓ') → joinPushout A B ≡ join A B
joinPushout≡join A B = isoToPath (joinPushout-iso-join A B)

{-
  Proof of associativity of the join
-}
join-assoc : (A B C : Type₀) → join (join A B) C ≡ join A (join B C)
join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
                   ∙ (spanEquivToPushoutPath sp3≃sp4) ⁻¹
                   ∙ (3x3-span.3x3-lemma span) ⁻¹
                   ∙ (spanEquivToPushoutPath sp1≃sp2)
                   ∙ (joinPushout≡join A (join B C))
  where
    -- the meat of the proof is handled by the 3x3 lemma applied to this diagram
    span : 3x3-span
    span = record {
      A00 = A;      A02 = A × B;      A04 = B;
      A20 = A × C;  A22 = A × B × C;  A24 = B × C;
      A40 = A × C;  A42 = A × C;      A44 = C;
      f10 = proj₁;   f12 = proj₁₂; f14 = proj₁;
      f30 = λ x → x; f32 = proj₁₃; f34 = proj₂;
      f01 = proj₁;   f21 = proj₁₃; f41 = λ x → x;
      f03 = proj₂;   f23 = proj₂;  f43 = proj₂;
      H11 = H11;    H13 = H13;    H31 = H31;    H33 = H33  }
      where
        proj₁₃ : A × B × C → A × C
        proj₁₃ (a , (b , c)) = a , c

        proj₁₂ : A × B × C → A × B
        proj₁₂ (a , (b , c)) = a , b

        H11 : (x : A × B × C) → proj₁ (proj₁₂ x) ≡ proj₁ (proj₁₃ x)
        H11 (a , (b , c)) = refl

        H13 : (x : A × B × C) → proj₂ (proj₁₂ x) ≡ proj₁ (proj₂ x)
        H13 (a , (b , c)) = refl

        H31 : (x : A × B × C) → proj₁₃ x ≡ proj₁₃ x
        H31 (a , (b , c)) = refl

        H33 : (x : A × B × C) → proj₂ (proj₁₃ x) ≡ proj₂ (proj₂ x)
        H33 (a , (b , c)) = refl

    -- the first pushout span appearing in the 3x3 lemma
    sp1 : 3-span
    sp1 = record {
      A0 = 3x3-span.A□0 span;
      A2 = 3x3-span.A□2 span;
      A4 = 3x3-span.A□4 span;
      f1 = 3x3-span.f□1 span;
      f3 = 3x3-span.f□3 span }

    -- the first span we are interested in
    sp2 : 3-span
    sp2 = record {
      A0 = A ;
      A2 = A × (join B C) ;
      A4 = join B C ;
      f1 = proj₁ ;
      f3 = proj₂ }

    -- proof that they are in fact equivalent
    sp1≃sp2 : 3-span-equiv sp1 sp2
    sp1≃sp2 = record {
      e0 = A□0≃A;
      e2 = A□2≃A×join;
      e4 = joinPushout≃join B C;
      H1 = H1;
      H3 = H2 }
      where
        A×join : Type₀
        A×join = A × (join B C)

        A□2→A×join : 3x3-span.A□2 span → A×join
        A□2→A×join (inl (a , b)) = a , inl b
        A□2→A×join (inr (a , c)) = a , inr c
        A□2→A×join (push (a , (b , c)) i) = a , push b c i

        A×join→A□2 : A×join → 3x3-span.A□2 span
        A×join→A□2 (a , inl b) = inl (a , b)
        A×join→A□2 (a , inr c) = inr (a , c)
        A×join→A□2 (a , push b c i) = push (a , (b , c)) i

        A×join→A□2→A×join : ∀ x → A×join→A□2 (A□2→A×join x) ≡ x
        A×join→A□2→A×join (inl (a , b)) = refl
        A×join→A□2→A×join (inr (a , c)) = refl
        A×join→A□2→A×join (push (a , (b , c)) i) = refl

        A□2→A×join→A□2 : ∀ x → A□2→A×join (A×join→A□2 x) ≡ x
        A□2→A×join→A□2 (a , inl b) = refl
        A□2→A×join→A□2 (a , inr c) = refl
        A□2→A×join→A□2 (a , push b c i) = refl

        A□2≃A×join : 3x3-span.A□2 span ≃ A×join
        A□2≃A×join = isoToEquiv (iso A□2→A×join A×join→A□2 A□2→A×join→A□2 A×join→A□2→A×join)

        A→A□0 : A → 3x3-span.A□0 span
        A→A□0 b = inl b

        A□0→A : 3x3-span.A□0 span → A
        A□0→A (inl b) = b
        A□0→A (inr a) = proj₁ a
        A□0→A (push a i) = proj₁ a

        A→A□0→A : ∀ x → A□0→A (A→A□0 x) ≡ x
        A→A□0→A x = refl

        A□0→A→A□0 : ∀ x → A→A□0 (A□0→A x) ≡ x
        A□0→A→A□0 (inl b) = refl
        A□0→A→A□0 (inr a) j = push a j
        A□0→A→A□0 (push a i) j = push a (j ∧ i)

        A□0≃A :  3x3-span.A□0 span ≃ A
        A□0≃A = isoToEquiv (iso A□0→A A→A□0 A→A□0→A A□0→A→A□0)

        H1 : (x : 3x3-span.A□2 span) → proj₁ (A□2→A×join x) ≡ A□0→A (3x3-span.f□1 span x)
        H1 (inl (a , b)) = refl
        H1 (inr (a , c)) = refl
        H1 (push (a , (b , c)) i) j = A□0→A (doubleCompPath-filler refl (λ i → push (a , c) i) refl i j)

        H2 : (x : 3x3-span.A□2 span) → proj₂ (A□2→A×join x) ≡ fst (joinPushout≃join _ _) (3x3-span.f□3 span x)
        H2 (inl (a , b)) = refl
        H2 (inr (a , c)) = refl
        H2 (push (a , (b , c)) i) j = fst (joinPushout≃join _ _) (doubleCompPath-filler refl (λ i → push (b , c) i) refl i j)

    -- the second span appearing in 3x3 lemma
    sp3 : 3-span
    sp3 = record {
      A0 = 3x3-span.A0□ span;
      A2 = 3x3-span.A2□ span;
      A4 = 3x3-span.A4□ span;
      f1 = 3x3-span.f1□ span;
      f3 = 3x3-span.f3□ span }

    -- the second span we are interested in
    sp4 : 3-span
    sp4 = record {
      A0 = join A B ;
      A2 = (join A B) × C ;
      A4 = C ;
      f1 = proj₁ ;
      f3 = proj₂ }

    -- proof that they are in fact equivalent
    sp3≃sp4 : 3-span-equiv sp3 sp4
    sp3≃sp4 = record {
      e0 = joinPushout≃join A B;
      e2 = A2□≃join×C;
      e4 = A4□≃C;
      H1 = H4;
      H3 = H3 }
      where
        join×C : Type₀
        join×C = (join A B) × C

        A2□→join×C : 3x3-span.A2□ span → join×C
        A2□→join×C (inl (a , c)) = (inl a) , c
        A2□→join×C (inr (b , c)) = (inr b) , c
        A2□→join×C (push (a , (b , c)) i) = push a b i , c

        join×C→A2□ : join×C → 3x3-span.A2□ span
        join×C→A2□ (inl a , c) = inl (a , c)
        join×C→A2□ (inr b , c) = inr (b , c)
        join×C→A2□ (push a b i , c) = push (a , (b , c)) i

        join×C→A2□→join×C : ∀ x → join×C→A2□ (A2□→join×C x) ≡ x
        join×C→A2□→join×C (inl (a , c)) = refl
        join×C→A2□→join×C (inr (b , c)) = refl
        join×C→A2□→join×C (push (a , (b , c)) j) = refl

        A2□→join×C→A2□ : ∀ x → A2□→join×C (join×C→A2□ x) ≡ x
        A2□→join×C→A2□ (inl a , c) = refl
        A2□→join×C→A2□ (inr b , c) = refl
        A2□→join×C→A2□ (push a b i , c) = refl

        A2□≃join×C : 3x3-span.A2□ span ≃ join×C
        A2□≃join×C = isoToEquiv (iso A2□→join×C join×C→A2□ A2□→join×C→A2□ join×C→A2□→join×C)

        C→A4□ : C → 3x3-span.A4□ span
        C→A4□ b = inr b

        A4□→C : 3x3-span.A4□ span → C
        A4□→C (inl x) = proj₂ x
        A4□→C (inr c) = c
        A4□→C (push x i) = proj₂ x

        C→A4□→C : ∀ x → A4□→C (C→A4□ x) ≡ x
        C→A4□→C x = refl

        A4□→C→A4□ : ∀ x → C→A4□ (A4□→C x) ≡ x
        A4□→C→A4□ (inl x) j = push x (~ j)
        A4□→C→A4□ (inr c) = refl
        A4□→C→A4□ (push x i) j = push x (~ j ∨ i)

        A4□≃C :  3x3-span.A4□ span ≃ C
        A4□≃C = isoToEquiv (iso A4□→C C→A4□ C→A4□→C A4□→C→A4□)

        H3 : (x : 3x3-span.A2□ span) → proj₂ (A2□→join×C x) ≡ A4□→C (3x3-span.f3□ span x)
        H3 (inl (a , c)) = refl
        H3 (inr (b , c)) = refl
        H3 (push (a , (b , c)) i) j = A4□→C (doubleCompPath-filler refl (λ i → push (a , c) i) refl i j)

        H4 : (x : 3x3-span.A2□ span) → proj₁ (A2□→join×C x) ≡ fst (joinPushout≃join _ _) (3x3-span.f1□ span x)
        H4 (inl (a , c)) = refl
        H4 (inr (b , c)) = refl
        H4 (push (a , (b , c)) i) j = fst (joinPushout≃join _ _) (doubleCompPath-filler refl (λ i → push (a , b) i) refl i j)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module plantsigma where

data Tree : Set where
  oak    : Tree
  pine   : Tree
  spruce : Tree

data Flower : Set where
  rose : Flower
  lily : Flower

data PlantGroup : Set where
  tree   : PlantGroup
  flower : PlantGroup

PlantsInGroup : PlantGroup -> Set
PlantsInGroup tree   = Tree
PlantsInGroup flower = Flower

data Plant : Set where
  plant : (g : PlantGroup) -> PlantsInGroup g -> Plant

f : Plant -> PlantGroup
f (plant g pg) = g

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


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

module TNT.Base where

open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Divisibility
open import Data.Nat.Properties
open import Agda.Builtin.Equality
open import Relation.Nullary.Decidable
open import Data.Empty

-- defination of congruence modulo

_≡_⟨mod_⟩ : ℕ → ℕ → (n : ℕ) → {≢0 : False (n ≟ 0)} → Set
(a ≡ b ⟨mod 0 ⟩){}
a ≡ b ⟨mod suc n ⟩ = a % suc n ≡ b % suc n

-- commutative

≡-comm : ∀ {ℓ} {A : Set ℓ} {a b : A} → a ≡ b → b ≡ a
≡-comm refl = refl

≡-mod-comm : ∀ {a b n : ℕ} → a ≡ b ⟨mod suc n ⟩ → b ≡ a ⟨mod suc n ⟩
≡-mod-comm refl₁ = ≡-comm refl₁

-- divisibility

a≡b⟨modn⟩⇒a%n-b%n≡0 : ∀ {a b n : ℕ} → a ≡ b ⟨mod suc n ⟩ → ∣ a % suc n - b % suc n ∣ ≡ 0
a≡b⟨modn⟩⇒a%n-b%n≡0 refl₁ = n≡m⇒∣n-m∣≡0 refl₁

a%n-b%n≡0⇒⟨a-b⟩%n≡0 : ∀ {a b n : ℕ} → ∣ a % suc n - b % suc n ∣ ≡ 0 → ∣ a - b ∣ % suc n ≡ 0
a%n-b%n≡0⇒⟨a-b⟩%n≡0 = {!!}

≡-mod-div : ∀ {a b n : ℕ} → a ≡ b ⟨mod suc n ⟩ → suc n ∣ ∣ a - b ∣
≡-mod-div {a} {b} {n} refl₁ = m%n≡0⇒n∣m ∣ a - b ∣ n (a%n-b%n≡0⇒⟨a-b⟩%n≡0 {a} {b} {n} (a≡b⟨modn⟩⇒a%n-b%n≡0 {a} {b} {n} refl₁))

-- transitivity

≡-trans : ∀ {ℓ} {A : Set ℓ} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
≡-trans refl refl = refl

≡-mod-trans : ∀ {a b c n : ℕ} → a ≡ b ⟨mod suc n ⟩ → b ≡ c ⟨mod suc n ⟩ → a ≡ c ⟨mod suc n ⟩
≡-mod-trans refl₁ refl₂ = ≡-trans refl₁ refl₂

max_stars_repo_name: PragmaTwice/TNT

max_issues_repo_name: PragmaTwice/TNT

max_forks_repo_name: PragmaTwice/TNT


text:
module x01-842Naturals-hc where

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

one : ℕ
one = suc zero

two : ℕ
two = suc (suc zero)

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

{-# BUILTIN NATURAL ℕ #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq             using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

_ : 2 + 3 ≡ 5
_ = refl

_ : 2 + 3 ≡ 5
_ =
  begin
    2                + 3                      ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero))) ≡⟨⟩    -- many steps condensed
    5
  ∎

_*_ : ℕ → ℕ → ℕ
zero  * n = 0
suc m * n = n + (m * n)

_ =
  begin
    2 * 3 ≡⟨⟩    -- many steps condensed
    6
  ∎

_^_ : ℕ → ℕ → ℕ
m ^  zero = 1
m ^ suc n = m * (m ^ n)

_ : 2 ^ 3 ≡ 8
_ = refl
_ : 2 ^ 4 ≡ 16
_ = refl
_ : 3 ^ 3 ≡ 27
_ = refl
_ : 3 ^ 10 ≡ 59049
_ = refl

-- Monus (subtraction for naturals, bottoms out at zero).

_∸_ : ℕ → ℕ → ℕ
zero  ∸     n = zero
m     ∸  zero = m
suc m ∸ suc n = m ∸ n

_ =
  begin
     3 ∸ 2
  ≡⟨⟩ -- many steps condensed
     1
  ∎

_ =
  begin
     2 ∸ 3
  ≡⟨⟩ -- many steps condensed
     0
  ∎

_ = begin 5 ∸ 3 ≡⟨⟩ 2 ∎
_ = begin 3 ∸ 5 ≡⟨⟩ 0 ∎

infixl 6  _+_  _∸_
infixl 7  _*_

-- {-# BUILTIN NATPLUS  _+_ #-}
-- {-# BUILTIN NATTIMES _*_ #-}
-- {-# BUILTIN NATMINUS _∸_ #-}

-- Binary representation.
-- Modified from PLFA exercise (thanks to David Darais).

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ

-- Our representation of zero is different from PLFA.
-- We use the empty sequence of bits (more consistent).

bin-zero : Bin-ℕ
bin-zero = bits

bin-one : Bin-ℕ
bin-one = bits x1     -- 1 in binary

bin-two : Bin-ℕ
bin-two = bits x1 x0  -- 10 in binary

-- 842 exercise: Increment (1 point)

inc : Bin-ℕ → Bin-ℕ
inc  bits  =  bits x1
inc (m x0) =     m x1
inc (m x1) = inc m x0

_ : inc (bits x1 x0 x1 x0) ≡    bits x1 x0 x1 x1
_ = refl
_ : inc (bits x1 x0 x1 x1) ≡    bits x1 x1 x0 x0
_ = refl
_ : inc (bits x1 x1 x1 x1) ≡ bits x1 x0 x0 x0 x0
_ = refl

-- 842 exercise: To/From (2 points)
-- Hint: avoid addition and multiplication. Use the provided dbl.

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc m) = suc (suc (dbl m))

tob : ℕ → Bin-ℕ
tob   zero   = bits
tob (suc m)  = inc (tob m)

fromb : Bin-ℕ → ℕ
fromb  bits  = 0
fromb (n x0) =      dbl (fromb n)
fromb (n x1) = suc (dbl (fromb n))

_ : tob 6 ≡    bits x1 x1 x0
_ = refl
_ : tob 7 ≡    bits x1 x1 x1
_ = refl
_ : tob 8 ≡ bits x1 x0 x0 x0
_ = refl

_ : fromb    (bits x1 x1 x0) ≡ 6
_ = refl
_ : fromb    (bits x1 x1 x1) ≡ 7
_ = refl
_ : fromb (bits x1 x0 x0 x0) ≡ 8
_ = refl

-- 842 exercise: BinAdd (2 points)
-- Write the addition function for binary notation.
-- Do NOT use 'to' and 'from'. Work with Bin-ℕ as if ℕ did not exist.
-- Hint: use recursion on both m and n.

_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
m      bin-+ bits   =       m
bits   bin-+  n     =               n
(m x0) bin-+ (n x0) =      (m bin-+ n) x0
(m x0) bin-+ (n x1) =      (m bin-+ n) x1
(m x1) bin-+ (n x0) =      (m bin-+ n) x1
(m x1) bin-+ (n x1) = inc ((m bin-+ n) x1)

-- Tests can use to/from, or write out binary constants as below.
-- Again: write more tests!

_ : (bits x1 x0) bin-+ (bits x1 x1) ≡ (bits x1 x0 x1)
_ = refl

_ : tob 0 bin-+ tob 0 ≡ tob 0
_ = refl

_ : tob 7 bin-+ tob 7 ≡ tob 14
_ = refl

_ : tob 3 bin-+ tob 4 ≡ tob 7
_ = refl

{-
-- Many definitions from above are also in the standard library.
-- open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

-- Unicode used in this chapter:

    ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
    →  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
    ∸  U+2238  DOT MINUS (\.-)
    ≡  U+2261  IDENTICAL TO (\==)
    ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
    ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
    ∎  U+220E  END OF PROOF (\qed)
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
import cedille-options
open import general-util
module spans (options : cedille-options.options) {mF : Set → Set} {{_ : monad mF}} where

open import lib
open import functions

open import cedille-types
open import constants
open import conversion
open import ctxt
open import is-free
open import syntax-util
open import to-string options
open import subst

--------------------------------------------------
-- span datatype
--------------------------------------------------

err-m : Set
err-m = maybe string

data span : Set where
  mk-span : string → posinfo → posinfo → 𝕃 tagged-val {- extra information for the span -} → err-m → span

span-to-rope : span → rope
span-to-rope (mk-span name start end extra nothing) =
  [[ "[\"" ^ name ^ "\"," ^ start ^ "," ^ end ^ ",{" ]] ⊹⊹ tagged-vals-to-rope 0 extra ⊹⊹ [[ "}]" ]]
span-to-rope (mk-span name start end extra (just err)) =
  [[ "[\"" ^ name ^ "\"," ^ start ^ "," ^ end ^ ",{" ]] ⊹⊹ tagged-vals-to-rope 0 (("error" , [[ err ]] , []) :: extra) ⊹⊹ [[ "}]" ]]

data error-span : Set where
  mk-error-span : string → posinfo → posinfo → 𝕃 tagged-val → string → error-span

data spans : Set where
  regular-spans : maybe error-span → 𝕃 span → spans
  global-error : string {- error message -} → maybe span → spans

is-error-span : span → 𝔹
is-error-span (mk-span _ _ _ _ err) = isJust err

get-span-error : span → err-m
get-span-error (mk-span _ _ _ _ err) = err

get-tagged-vals : span → 𝕃 tagged-val
get-tagged-vals (mk-span _ _ _ tvs _) = tvs

spans-have-error : spans → 𝔹
spans-have-error (regular-spans es ss) = isJust es
spans-have-error (global-error _ _) = tt

empty-spans : spans
empty-spans = regular-spans nothing []

𝕃span-to-rope : 𝕃 span → rope
𝕃span-to-rope (s :: []) = span-to-rope s
𝕃span-to-rope (s :: ss) = span-to-rope s ⊹⊹ [[ "," ]] ⊹⊹ 𝕃span-to-rope ss
𝕃span-to-rope [] = [[]]

spans-to-rope : spans → rope
spans-to-rope (regular-spans _ ss) = [[ "{\"spans\":["]] ⊹⊹ 𝕃span-to-rope ss ⊹⊹ [[ "]}" ]] where
spans-to-rope (global-error e s) =
  [[ global-error-string e ]] ⊹⊹ maybe-else [[]] (λ s → [[", \"global-error\":"]] ⊹⊹ span-to-rope s) s

print-file-id-table : ctxt → 𝕃 tagged-val
print-file-id-table (mk-ctxt mod (syms , mn-fn , mn-ps , fn-ids , id , id-fns) is os _) =
  h [] id-fns where
  h : ∀ {i} → 𝕃 tagged-val → 𝕍 string i → 𝕃 tagged-val
  h ts [] = ts
  h {i} ts (fn :: fns) = h (("fileid" , [[ fn ]] , []) :: ts) fns

add-span : span → spans → spans
add-span s@(mk-span dsc pi pi' tv nothing) (regular-spans es ss) =
  regular-spans es (s :: ss)
add-span s@(mk-span dsc pi pi' tv (just err)) (regular-spans es ss) =
  regular-spans (just (mk-error-span dsc pi pi' tv err)) (s :: ss)
add-span s (global-error e e') =
  global-error e e'

--------------------------------------------------
-- spanM, a state monad for spans
--------------------------------------------------

spanM : Set → Set
spanM A = ctxt → spans → mF (A × ctxt × spans)

-- return for the spanM monad
spanMr : ∀{A : Set} → A → spanM A
spanMr a Γ ss = returnM (a , Γ , ss)

spanMok : spanM ⊤
spanMok = spanMr triv

get-ctxt : ∀{A : Set} → (ctxt → spanM A) → spanM A
get-ctxt m Γ ss = m Γ Γ ss

set-ctxt : ctxt → spanM ⊤
set-ctxt Γ _ ss = returnM (triv , Γ , ss)

get-error : ∀ {A : Set} → (maybe error-span → spanM A) → spanM A
get-error m Γ ss@(global-error _ _) = m nothing Γ ss
get-error m Γ ss@(regular-spans nothing _) = m nothing Γ ss
get-error m Γ ss@(regular-spans (just es) _) = m (just es) Γ ss

set-error : maybe (error-span) → spanM ⊤
set-error es Γ ss@(global-error _ _) = returnM (triv , Γ , ss)
set-error es Γ (regular-spans _ ss) = returnM (triv , Γ , regular-spans es ss)

restore-def : Set
restore-def = maybe qualif-info × maybe sym-info

spanM-set-params : params → spanM ⊤
spanM-set-params ps Γ ss = returnM (triv , (ctxt-params-def ps Γ) , ss)

-- this returns the previous ctxt-info, if any, for the given variable
spanM-push-term-decl : posinfo → var → type → spanM restore-def
spanM-push-term-decl pi x t Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-term-decl pi x t Γ , ss)

-- let bindings currently cannot be made opaque, so this is OpacTrans. -tony
spanM-push-term-def : posinfo → var → term → type → spanM restore-def
spanM-push-term-def pi x t T Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-term-def pi localScope OpacTrans x t T Γ , ss)

spanM-push-term-udef : posinfo → var → term → spanM restore-def
spanM-push-term-udef pi x t Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-term-udef pi localScope OpacTrans x t Γ , ss)

 -- return previous ctxt-info, if any
spanM-push-type-decl : posinfo → var → kind → spanM restore-def
spanM-push-type-decl pi x k Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-type-decl pi x k Γ , ss)

spanM-push-type-def : posinfo → var → type → kind → spanM restore-def
spanM-push-type-def pi x t T Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-type-def pi localScope OpacTrans x t T Γ , ss)

-- returns the original sym-info.
-- clarification is idempotent: if the definition was already clarified,
-- then the operation succeeds, and returns (just sym-info).
-- this only returns nothing in the case that the opening didnt make sense:
-- you tried to open a term def, you tried to open an unknown def, etc...
-- basically any situation where the def wasnt a "proper" type def
spanM-clarify-def : var → spanM (maybe sym-info)
spanM-clarify-def x Γ ss = returnM (result (ctxt-clarify-def Γ x))
  where
  result : maybe (sym-info × ctxt) → (maybe sym-info × ctxt × spans)
  result (just (si , Γ')) = ( just si , Γ' , ss )
  result nothing = ( nothing , Γ , ss )

spanM-restore-clarified-def : var → sym-info → spanM ⊤
spanM-restore-clarified-def x si Γ ss = returnM (triv , ctxt-set-sym-info Γ x si , ss)

-- restore ctxt-info for the variable with given posinfo
spanM-restore-info : var → restore-def → spanM ⊤
spanM-restore-info v rd Γ ss = returnM (triv , ctxt-restore-info Γ v (fst rd) (snd rd) , ss)

_≫=span_ : ∀{A B : Set} → spanM A → (A → spanM B) → spanM B
(m₁ ≫=span m₂) ss Γ = m₁ ss Γ ≫=monad λ where (v , Γ , ss) → m₂ v Γ ss

_≫span_ : ∀{A B : Set} → spanM A → spanM B → spanM B
(m₁ ≫span m₂) = m₁ ≫=span (λ _ → m₂)

spanM-restore-info* : 𝕃 (var × restore-def) → spanM ⊤
spanM-restore-info* [] = spanMok
spanM-restore-info* ((v , qi , m) :: s) = spanM-restore-info v (qi , m) ≫span spanM-restore-info* s

infixl 2 _≫span_ _≫=span_ _≫=spanj_ _≫=spanm_ _≫=spanm'_ _≫=spanc_ _≫=spanc'_ _≫spanc_ _≫spanc'_

_≫=spanj_ : ∀{A : Set} → spanM (maybe A) → (A → spanM ⊤) → spanM ⊤
_≫=spanj_{A} m m' = m ≫=span cont
  where cont : maybe A → spanM ⊤
        cont nothing = spanMok
        cont (just x) = m' x

-- discard changes made by the first computation
_≫=spand_ : ∀{A B : Set} → spanM A → (A → spanM B) → spanM B
_≫=spand_{A} m m' Γ ss = m Γ ss ≫=monad λ where (v , _ , _) → m' v Γ ss

-- discard *spans* generated by first computation
_≫=spands_ : ∀ {A B : Set} → spanM A → (A → spanM B) → spanM B
_≫=spands_ m f Γ ss = m Γ ss ≫=monad λ where (v , Γ , _ ) → f v Γ ss

_≫=spanm_ : ∀{A : Set} → spanM (maybe A) → (A → spanM (maybe A)) → spanM (maybe A)
_≫=spanm_{A} m m' = m ≫=span cont
  where cont : maybe A → spanM (maybe A)
        cont nothing = spanMr nothing
        cont (just a) = m' a

_≫=spans'_ : ∀ {A B E : Set} → spanM (E ∨ A) → (A → spanM (E ∨ B)) → spanM (E ∨ B)
_≫=spans'_ m f = m ≫=span λ where
  (inj₁ e) → spanMr (inj₁ e)
  (inj₂ a) → f a

_≫=spanm'_ : ∀{A B : Set} → spanM (maybe A) → (A → spanM (maybe B)) → spanM (maybe B)
_≫=spanm'_{A}{B} m m' = m ≫=span cont
  where cont : maybe A → spanM (maybe B)
        cont nothing = spanMr nothing
        cont (just a) = m' a

-- Currying/uncurry span binding
_≫=spanc_ : ∀{A B C} → spanM (A × B) → (A → B → spanM C) → spanM C
(m ≫=spanc m') Γ ss = m Γ ss ≫=monad λ where
  ((a , b) , Γ' , ss') → m' a b Γ' ss'

_≫=spanc'_ : ∀{A B C} → spanM (A × B) → (B → spanM C) → spanM C
(m ≫=spanc' m') Γ ss = m Γ ss ≫=monad λ where
  ((a , b) , Γ' , ss') → m' b Γ' ss'

_≫spanc'_ : ∀{A B} → spanM A → B → spanM (A × B)
(m ≫spanc' b) = m ≫=span λ a → spanMr (a , b)

_≫spanc_ : ∀{A B} → spanM A → spanM B → spanM (A × B)
(ma ≫spanc mb) = ma ≫=span λ a → mb ≫=span λ b → spanMr (a , b)

spanMok' : ∀{A} → A → spanM (⊤ × A)
spanMok' a = spanMr (triv , a)

_on-fail_≫=spanm'_ : ∀ {A B} → spanM (maybe A) → spanM B
                            → (A → spanM B) → spanM B
_on-fail_≫=spanm'_ {A}{B} m fail f = m ≫=span cont
  where cont : maybe A → spanM B
        cont nothing  = fail
        cont (just x) = f x

_on-fail_≫=spans'_ : ∀ {A B E} → spanM (E ∨ A) → (E → spanM B) → (A → spanM B) → spanM B
_on-fail_≫=spans'_ {A}{B}{E} m fail f = m ≫=span cont
  where cont : E ∨ A → spanM B
        cont (inj₁ err) = fail err
        cont (inj₂ a) = f a

_exit-early_≫=spans'_ = _on-fail_≫=spans'_

with-ctxt : ∀ {A} → ctxt → spanM A → spanM A
with-ctxt Γ sm
  =   get-ctxt λ Γ' → set-ctxt Γ
    ≫span  sm
    ≫=span λ a → set-ctxt Γ'
    ≫span  spanMr a

sequence-spanM : ∀ {A} → 𝕃 (spanM A) → spanM (𝕃 A)
sequence-spanM [] = spanMr []
sequence-spanM (sp :: sps)
  =   sp
    ≫=span λ x → sequence-spanM sps
    ≫=span λ xs → spanMr (x :: xs)

foldr-spanM : ∀ {A B} → (A → spanM B → spanM B) → spanM B → 𝕃 (spanM A) → spanM B
foldr-spanM f n [] = n
foldr-spanM f n (m :: ms)
  = m ≫=span λ a → f a (foldr-spanM f n ms)

foldl-spanM : ∀ {A B} → (spanM B → A → spanM B) → spanM B → 𝕃 (spanM A) → spanM B
foldl-spanM f m [] = m
foldl-spanM f m (m' :: ms) =
  m' ≫=span λ a → foldl-spanM f (f m a) ms

spanM-for_init_use_ : ∀ {A B} → 𝕃 (spanM A) → spanM B → (A → spanM B → spanM B) → spanM B
spanM-for xs init acc use f = foldr-spanM f acc xs

spanM-add : span → spanM ⊤
spanM-add s Γ ss = returnM (triv , Γ , add-span s ss)

spanM-addl : 𝕃 span → spanM ⊤
spanM-addl [] = spanMok
spanM-addl (s :: ss) = spanM-add s ≫span spanM-addl ss

debug-span : posinfo → posinfo → 𝕃 tagged-val → span
debug-span pi pi' tvs = mk-span "Debug" pi pi' tvs nothing

spanM-debug : posinfo → posinfo → 𝕃 tagged-val → spanM ⊤
--spanM-debug pi pi' tvs = spanM-add (debug-span pi pi' tvs)
spanM-debug pi pi' tvs = spanMok

to-string-tag-tk : (tag : string) → ctxt → tk → tagged-val
to-string-tag-tk t Γ (Tkt T) = to-string-tag t Γ T
to-string-tag-tk t Γ (Tkk k) = to-string-tag t Γ k

--------------------------------------------------
-- tagged-val constants
--------------------------------------------------

location-data : location → tagged-val
location-data (file-name , pi) = "location" , [[ file-name ]] ⊹⊹ [[ " - " ]] ⊹⊹ [[ pi ]] , []

var-location-data : ctxt → var → tagged-val
var-location-data Γ @ (mk-ctxt _ _ i _ _) x =
  location-data (maybe-else ("missing" , "missing") snd
    (trie-lookup i x maybe-or trie-lookup i (qualif-var Γ x)))
{-
{-# TERMINATING #-}
var-location-data : ctxt → var → maybe language-level → tagged-val
var-location-data Γ x (just ll-term) with ctxt-var-location Γ x | qualif-term Γ (Var posinfo-gen x)
...| ("missing" , "missing") | (Var pi x') = location-data (ctxt-var-location Γ x')
...| loc | _ = location-data loc
var-location-data Γ x (just ll-type) with ctxt-var-location Γ x | qualif-type Γ (TpVar posinfo-gen x)
...| ("missing" , "missing") | (TpVar pi x') = location-data (ctxt-var-location Γ x')
...| loc | _ = location-data loc
var-location-data Γ x (just ll-kind) with ctxt-var-location Γ x | qualif-kind Γ (KndVar posinfo-gen x ArgsNil)
...| ("missing" , "missing") | (KndVar pi x' as) = location-data (ctxt-var-location Γ x')
...| loc | _ = location-data loc
var-location-data Γ x nothing with ctxt-lookup-term-var Γ x | ctxt-lookup-type-var Γ x | ctxt-lookup-kind-var-def Γ x
...| just _ | _ | _ = var-location-data Γ x (just ll-term)
...| _ | just _ | _ = var-location-data Γ x (just ll-type)
...| _ | _ | just _ = var-location-data Γ x (just ll-kind)
...| _ | _ | _ = location-data ("missing" , "missing")
-}
explain : string → tagged-val
explain s = "explanation" , [[ s ]] , []

reason : string → tagged-val
reason s = "reason" , [[ s ]] , []

expected-type : ctxt → type → tagged-val
expected-type = to-string-tag "expected-type"

expected-type-subterm : ctxt → type → tagged-val
expected-type-subterm = to-string-tag "expected-type of the subterm"

missing-expected-type : tagged-val
missing-expected-type = "expected-type" , [[ "[missing]" ]] , []

-- hnf-type : ctxt → type → tagged-val
-- hnf-type Γ tp = to-string-tag "hnf of type" Γ (hnf-term-type Γ ff tp)

-- hnf-expected-type : ctxt → type → tagged-val
-- hnf-expected-type Γ tp = to-string-tag "hnf of expected type" Γ (hnf-term-type Γ ff tp)

expected-kind : ctxt → kind → tagged-val
expected-kind = to-string-tag "expected kind"

expected-kind-if : ctxt → maybe kind → 𝕃 tagged-val
expected-kind-if _ nothing = []
expected-kind-if Γ (just k) = [ expected-kind Γ k ]

expected-type-if : ctxt → maybe type → 𝕃 tagged-val
expected-type-if _ nothing = []
expected-type-if Γ (just tp) = [ expected-type Γ tp ]

-- hnf-expected-type-if : ctxt → maybe type → 𝕃 tagged-val
-- hnf-expected-type-if Γ nothing = []
-- hnf-expected-type-if Γ (just tp) = [ hnf-expected-type Γ tp ]

type-data : ctxt → type → tagged-val
type-data = to-string-tag "type"

missing-type : tagged-val
missing-type = "type" , [[ "[undeclared]" ]] , []

warning-data : string → tagged-val
warning-data s = "warning" , [[ s ]] , []

check-for-type-mismatch : ctxt → string → type → type → 𝕃 tagged-val × err-m
check-for-type-mismatch Γ s tp tp' =
  let tp'' = hnf Γ unfold-head tp' tt in
  expected-type Γ tp :: [ type-data Γ tp' ] ,
  if conv-type Γ tp tp'' then nothing else just ("The expected type does not match the " ^ s ^ " type.")

check-for-type-mismatch-if : ctxt → string → maybe type → type → 𝕃 tagged-val × err-m
check-for-type-mismatch-if Γ s (just tp) = check-for-type-mismatch Γ s tp
check-for-type-mismatch-if Γ s nothing tp = [ type-data Γ tp ] , nothing

summary-data : {ed : exprd} → (name : string) → ctxt → ⟦ ed ⟧ → tagged-val
summary-data name Γ t = strRunTag "summary" Γ (strVar name ≫str strAdd " : " ≫str to-stringh t)

missing-kind : tagged-val
missing-kind = "kind" , [[ "[undeclared]" ]] , []

head-kind : ctxt → kind → tagged-val
head-kind = to-string-tag "the kind of the head"

head-type : ctxt → type → tagged-val
head-type = to-string-tag "the type of the head"

arg-type : ctxt → type → tagged-val
arg-type = to-string-tag "computed arg type"

arg-exp-type : ctxt → type → tagged-val
arg-exp-type = to-string-tag "expected arg type"

type-app-head : ctxt → type → tagged-val
type-app-head = to-string-tag "the head"

term-app-head : ctxt → term → tagged-val
term-app-head = to-string-tag "the head"

term-argument : ctxt → term → tagged-val
term-argument = to-string-tag "the argument"

type-argument : ctxt → type → tagged-val
type-argument = to-string-tag "the argument"

contextual-type-argument : ctxt → type → tagged-val
contextual-type-argument = to-string-tag "contextual type arg"

arg-argument : ctxt → arg → tagged-val
arg-argument Γ (TermArg me x) = term-argument Γ x
arg-argument Γ (TypeArg x) = type-argument Γ x

kind-data : ctxt → kind → tagged-val
kind-data = to-string-tag "kind"

liftingType-data : ctxt → liftingType → tagged-val
liftingType-data = to-string-tag "lifting type"

kind-data-if : ctxt → maybe kind → 𝕃 tagged-val
kind-data-if Γ (just k) = [ kind-data Γ k ]
kind-data-if _ nothing = []

super-kind-data : tagged-val
super-kind-data = "superkind" , [[ "□" ]] , []

symbol-data : string → tagged-val
symbol-data x = "symbol" , [[ x ]] , []

tk-data : ctxt → tk → tagged-val
tk-data Γ (Tkk k) = kind-data Γ k
tk-data Γ (Tkt t) = type-data Γ t

checking-to-string : checking-mode → string
checking-to-string checking = "checking"
checking-to-string synthesizing = "synthesizing"
checking-to-string untyped = "untyped"

checking-data : checking-mode → tagged-val
checking-data cm = "checking-mode" , [[ checking-to-string cm ]] , []

checked-meta-var : var → tagged-val
checked-meta-var x = "checked meta-var" , [[ x ]] , []

ll-data : language-level → tagged-val
ll-data x = "language-level" , [[ ll-to-string x ]] , []

ll-data-term = ll-data ll-term
ll-data-type = ll-data ll-type
ll-data-kind = ll-data ll-kind

binder-data : ℕ → tagged-val
binder-data n = "binder" , [[ ℕ-to-string n ]] , []

-- this is the subterm position in the parse tree (as determined by
-- spans) for the bound variable of a binder
binder-data-const : tagged-val
binder-data-const = binder-data 0

bound-data : defTermOrType → ctxt → tagged-val
bound-data (DefTerm pi v mtp t) Γ = to-string-tag "bound-value" Γ t
bound-data (DefType pi v k tp) Γ = to-string-tag "bound-value" Γ tp

punctuation-data : tagged-val
punctuation-data = "punctuation" , [[ "true" ]] , []

not-for-navigation : tagged-val
not-for-navigation = "not-for-navigation" , [[ "true" ]] , []

is-erased : type → 𝔹
is-erased (TpVar _ _ ) = tt
is-erased _ = ff

erased? = 𝔹

keywords = "keywords"
keyword-erased = "erased"
keyword-noterased = "noterased"
keyword-application = "application"
keyword-locale = "meta-var-locale"

noterased : tagged-val
noterased = keywords , [[ keyword-noterased ]] , []

keywords-data : 𝕃 string → tagged-val
keywords-data kws = keywords , h kws , [] where
  h : 𝕃 string → rope
  h [] = [[]]
  h (k :: []) = [[ k ]]
  h (k :: ks) = [[ k ]] ⊹⊹ [[ " " ]] ⊹⊹ h ks

keywords-data-var : erased? → tagged-val
keywords-data-var e =
  keywords ,  [[ if e then keyword-erased else keyword-noterased ]] , []

keywords-app : (is-locale : 𝔹) → tagged-val
keywords-app l = keywords-data ([ keyword-application ] ++ (if l then [ keyword-locale ] else []))

keywords-app-if-typed : checking-mode → (is-locale : 𝔹) → 𝕃 tagged-val
keywords-app-if-typed untyped l = []
keywords-app-if-typed _ l = [ keywords-app l ]

error-if-not-eq : ctxt → type → 𝕃 tagged-val → 𝕃 tagged-val × err-m
error-if-not-eq Γ (TpEq pi t1 t2 pi') tvs = expected-type Γ (TpEq pi t1 t2 pi') :: tvs , nothing
error-if-not-eq Γ tp tvs = expected-type Γ tp :: tvs , just "This term is being checked against the following type, but an equality type was expected"

error-if-not-eq-maybe : ctxt → maybe type → 𝕃 tagged-val → 𝕃 tagged-val × err-m
error-if-not-eq-maybe Γ (just tp) = error-if-not-eq Γ tp
error-if-not-eq-maybe _ _ tvs = tvs , nothing

params-data : ctxt → params → 𝕃 tagged-val
params-data _ ParamsNil = []
params-data Γ ps = [ params-to-string-tag "parameters" Γ ps ]

--------------------------------------------------
-- span-creating functions
--------------------------------------------------

Star-name : string
Star-name = "Star"

parens-span : posinfo → posinfo → span
parens-span pi pi' = mk-span "parentheses" pi pi' [] nothing

data decl-class : Set where
  param : decl-class
  index : decl-class

decl-class-name : decl-class → string
decl-class-name param = "parameter"
decl-class-name index = "index"

Decl-span : decl-class → posinfo → var → tk → posinfo → span
Decl-span dc pi v atk pi' = mk-span ((if tk-is-type atk then "Term " else "Type ") ^ (decl-class-name dc))
                                      pi pi' [ binder-data-const ] nothing

TpVar-span : ctxt → posinfo → string → checking-mode → 𝕃 tagged-val → err-m → span
TpVar-span Γ pi v check tvs = mk-span "Type variable" pi (posinfo-plus-str pi (unqual-local v)) (checking-data check :: ll-data-type :: var-location-data Γ v :: symbol-data (unqual-local v) :: tvs)

Var-span : ctxt → posinfo → string → checking-mode → 𝕃 tagged-val → err-m → span
Var-span Γ pi v check tvs = mk-span "Term variable" pi (posinfo-plus-str pi (unqual-local v)) (checking-data check :: ll-data-term :: var-location-data Γ v :: symbol-data (unqual-local v) :: tvs)

KndVar-span : ctxt → (posinfo × var) → (end-pi : posinfo) → params → checking-mode → 𝕃 tagged-val → err-m → span
KndVar-span Γ (pi , v) pi' ps check tvs =
  mk-span "Kind variable" pi pi'
    (checking-data check :: ll-data-kind :: var-location-data Γ v :: symbol-data (unqual-local v) :: super-kind-data :: (params-data Γ ps ++ tvs))

var-span :  erased? → ctxt → posinfo → string → checking-mode → tk → err-m → span
var-span _ Γ pi x check (Tkk k) = TpVar-span Γ pi x check (keywords-data-var ff :: [ kind-data Γ k ])
var-span e Γ pi x check (Tkt t) = Var-span Γ pi x check (keywords-data-var e :: [ type-data Γ t ])

redefined-var-span : ctxt → posinfo → var → span
redefined-var-span Γ pi x = mk-span "Variable definition" pi (posinfo-plus-str pi x)
                             [ var-location-data Γ x ] (just "This symbol was defined already.")

TpAppt-span : type → term → checking-mode → 𝕃 tagged-val → err-m → span
TpAppt-span tp t check tvs = mk-span "Application of a type to a term" (type-start-pos tp) (term-end-pos t) (checking-data check :: ll-data-type :: tvs)

TpApp-span : type → type → checking-mode → 𝕃 tagged-val → err-m → span
TpApp-span tp tp' check tvs = mk-span "Application of a type to a type" (type-start-pos tp) (type-end-pos tp') (checking-data check :: ll-data-type :: tvs)

App-span : (is-locale : 𝔹) → term → term → checking-mode → 𝕃 tagged-val → err-m → span
App-span l t t' check tvs = mk-span "Application of a term to a term" (term-start-pos t) (term-end-pos t') (checking-data check :: ll-data-term :: keywords-app-if-typed check l ++ tvs)

AppTp-span : term → type → checking-mode → 𝕃 tagged-val → err-m → span
AppTp-span t tp check tvs = mk-span "Application of a term to a type" (term-start-pos t) (type-end-pos tp) (checking-data check :: ll-data-term :: keywords-app-if-typed check ff ++ tvs)

TpQuant-e = 𝔹

is-pi : TpQuant-e
is-pi = tt

TpQuant-span : TpQuant-e → posinfo → var → tk → type → checking-mode → 𝕃 tagged-val → err-m → span
TpQuant-span is-pi pi x atk body check tvs err =
  let err-if-type-pi = if ~ tk-is-type atk && is-pi then just "Π-types must bind a term, not a type (use ∀ instead)" else nothing in
  mk-span (if is-pi then "Dependent function type" else "Implicit dependent function type")
       pi (type-end-pos body) (checking-data check :: ll-data-type :: binder-data-const :: tvs) (if isJust err-if-type-pi then err-if-type-pi else err)

TpLambda-span : posinfo → var → tk → type → checking-mode → 𝕃 tagged-val → err-m → span
TpLambda-span pi x atk body check tvs =
  mk-span "Type-level lambda abstraction" pi (type-end-pos body)
    (checking-data check :: ll-data-type :: binder-data-const :: tvs)

Iota-span : posinfo → type → checking-mode → 𝕃 tagged-val → err-m → span
Iota-span pi t2 check tvs = mk-span "Iota-abstraction" pi (type-end-pos t2) (explain "A dependent intersection type" :: checking-data check :: binder-data-const :: ll-data-type :: tvs)

TpArrow-span : type → type → checking-mode → 𝕃 tagged-val → err-m → span
TpArrow-span t1 t2 check tvs = mk-span "Arrow type" (type-start-pos t1) (type-end-pos t2) (checking-data check :: ll-data-type :: tvs)

TpEq-span : posinfo → term → term → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
TpEq-span pi t1 t2 pi' check tvs = mk-span "Equation" pi pi'
                             (explain "Equation between terms" :: checking-data check :: ll-data-type :: tvs)

Star-span : posinfo → checking-mode → err-m → span
Star-span pi check = mk-span Star-name pi (posinfo-plus pi 1) (checking-data check :: [ ll-data-kind ])

KndPi-span : posinfo → var → tk → kind → checking-mode → err-m → span
KndPi-span pi x atk k check =
  mk-span "Pi kind" pi (kind-end-pos k)
    (checking-data check :: ll-data-kind :: binder-data-const :: [ super-kind-data ])

KndArrow-span : kind → kind → checking-mode → err-m → span
KndArrow-span k k' check = mk-span "Arrow kind" (kind-start-pos k) (kind-end-pos k') (checking-data check :: ll-data-kind :: [ super-kind-data ])

KndTpArrow-span : type → kind → checking-mode → err-m → span
KndTpArrow-span t k check = mk-span "Arrow kind" (type-start-pos t) (kind-end-pos k) (checking-data check :: ll-data-kind :: [ super-kind-data ])

{- [[file:../cedille-mode.el::(defun%20cedille-mode-filter-out-special(data)][Frontend]]  -}
special-tags : 𝕃 string
special-tags =
  "symbol" :: "location" :: "language-level" :: "checking-mode" :: "summary"
  :: "binder" :: "bound-value" :: "keywords" :: "erasure" :: []

error-span-filter-special : error-span → error-span
error-span-filter-special (mk-error-span dsc pi pi' tvs msg) =
  mk-error-span dsc pi pi' tvs' msg
  where tvs' = (flip filter) tvs λ tag → list-any (_=string (fst tag)) special-tags

erasure : ctxt → term → tagged-val
erasure Γ t = to-string-tag "erasure" Γ (erase-term t)

erased-marg-span : ctxt → term → maybe type → span
erased-marg-span Γ t mtp = mk-span "Erased module parameter" (term-start-pos t) (term-end-pos t)
  (maybe-else [] (λ tp → [ type-data Γ tp ]) mtp)
  (just "An implicit module parameter variable occurs free in the erasure of the term.")

Lam-span-erased : maybeErased → string
Lam-span-erased Erased = "Erased lambda abstraction (term-level)"
Lam-span-erased NotErased = "Lambda abstraction (term-level)"

Lam-span : ctxt → checking-mode → posinfo → maybeErased → var → optClass → term → 𝕃 tagged-val → err-m → span
Lam-span Γ c pi NotErased x (SomeClass (Tkk k)) t tvs e =
  mk-span (Lam-span-erased NotErased) pi (term-end-pos t) (ll-data-term :: binder-data-const :: checking-data c :: tvs) (e maybe-or just "λ-terms must bind a term, not a type (use Λ instead)")
Lam-span _ c pi l x NoClass t tvs = mk-span (Lam-span-erased l) pi (term-end-pos t) (ll-data-term :: binder-data-const :: checking-data c :: tvs)
Lam-span Γ c pi l x (SomeClass atk) t tvs = mk-span (Lam-span-erased l) pi (term-end-pos t)
                                           ((ll-data-term :: binder-data-const :: checking-data c :: tvs)
                                           ++ [ to-string-tag-tk "type of bound variable" Γ atk ])

compileFail-in : ctxt → term → 𝕃 tagged-val × err-m
compileFail-in Γ t with is-free-in check-erased compileFail-qual | qualif-term Γ t
...| is-free | tₒ with erase-term tₒ | hnf Γ unfold-all tₒ ff
...| tₑ | tₙ with is-free tₒ
...| ff = [] , nothing
...| tt with is-free tₙ | is-free tₑ
...| tt | _ = [ to-string-tag "normalized term" Γ tₙ ] , just "compileFail occurs in the normalized term"
...| ff | ff = [ to-string-tag "the term" Γ tₒ ] , just "compileFail occurs in an erased position"
...| ff | tt = [] , nothing

DefTerm-span : ctxt → posinfo → var → (checked : checking-mode) → maybe type → term → posinfo → 𝕃 tagged-val → span
DefTerm-span Γ pi x checked tp t pi' tvs =
  h ((h-summary tp) ++ (erasure Γ t :: tvs)) pi x checked tp pi'
  where h : 𝕃 tagged-val → posinfo → var → (checked : checking-mode) → maybe type → posinfo → span
        h tvs pi x checking _ pi' =
          mk-span "Term-level definition (checking)" pi pi' tvs nothing
        h tvs pi x _ (just tp) pi' =
          mk-span "Term-level definition (synthesizing)" pi pi' (to-string-tag "synthesized type" Γ tp :: tvs) nothing
        h tvs pi x _ nothing pi' =
          mk-span "Term-level definition (synthesizing)" pi pi' (("synthesized type" , [[ "[nothing]" ]] , []) :: tvs) nothing
        h-summary : maybe type → 𝕃 tagged-val
        h-summary nothing = [(checking-data synthesizing)]
        h-summary (just tp) = (checking-data checking :: [ summary-data x Γ tp ])

CheckTerm-span : ctxt → (checked : checking-mode) → maybe type → term → posinfo → 𝕃 tagged-val → span
CheckTerm-span Γ checked tp t pi' tvs =
  h (erasure Γ t :: tvs) checked tp (term-start-pos t) pi'
  where h : 𝕃 tagged-val → (checked : checking-mode) → maybe type → posinfo → posinfo → span
        h tvs checking _ pi pi' =
          mk-span "Checking a term" pi pi' (checking-data checking :: tvs) nothing
        h tvs _ (just tp) pi pi' =
          mk-span "Synthesizing a type for a term" pi pi' (checking-data synthesizing :: to-string-tag "synthesized type" Γ tp :: tvs) nothing
        h tvs _ nothing pi pi' =
          mk-span "Synthesizing a type for a term" pi pi' (checking-data synthesizing :: ("synthesized type" , [[ "[nothing]" ]] , []) :: tvs) nothing

normalized-type : ctxt → type → tagged-val
normalized-type = to-string-tag "normalized type"

DefType-span : ctxt → posinfo → var → (checked : checking-mode) → maybe kind → type → posinfo → 𝕃 tagged-val → span
DefType-span Γ pi x checked mk tp pi' tvs =
  h ((h-summary mk) ++ tvs) checked mk
  where h : 𝕃 tagged-val → checking-mode → maybe kind → span
        h tvs checking _ = mk-span "Type-level definition (checking)" pi pi' tvs nothing
        h tvs _ (just k) =
          mk-span "Type-level definition (synthesizing)" pi pi' (to-string-tag "synthesized kind" Γ k :: tvs) nothing
        h tvs _ nothing =
          mk-span "Type-level definition (synthesizing)" pi pi' ( ("synthesized kind" , [[ "[nothing]" ]] , []) :: tvs) nothing
        h-summary : maybe kind → 𝕃 tagged-val
        h-summary nothing = [(checking-data synthesizing)]
        h-summary (just k) = (checking-data checking :: [ summary-data x Γ k ])

DefKind-span : ctxt → posinfo → var → kind → posinfo → span
DefKind-span Γ pi x k pi' = mk-span "Kind-level definition" pi pi' (kind-data Γ k :: [ summary-data x Γ (Var pi "□") ]) nothing

{-unchecked-term-span : term → span
unchecked-term-span t = mk-span "Unchecked term" (term-start-pos t) (term-end-pos t)
                           (ll-data-term :: not-for-navigation :: [ explain "This term has not been type-checked."]) nothing-}

Beta-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Beta-span pi pi' check tvs = mk-span "Beta axiom" pi pi'
                     (checking-data check :: ll-data-term :: explain "A term constant whose type states that β-equal terms are provably equal" :: tvs)

hole-span : ctxt → posinfo → maybe type → 𝕃 tagged-val → span
hole-span Γ pi tp tvs =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (ll-data-term :: expected-type-if Γ tp ++ tvs)
    (just "This hole remains to be filled in")

tp-hole-span : ctxt → posinfo → maybe kind → 𝕃 tagged-val → span
tp-hole-span Γ pi k tvs =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (ll-data-term :: expected-kind-if Γ k ++ tvs)
    (just "This hole remains to be filled in")

expected-to-string : checking-mode → string
expected-to-string checking = "expected"
expected-to-string synthesizing = "synthesized"
expected-to-string untyped = "untyped"

Epsilon-span : posinfo → leftRight → maybeMinus → term → checking-mode → 𝕃 tagged-val → err-m → span
Epsilon-span pi lr m t check tvs = mk-span "Epsilon" pi (term-end-pos t)
                                         (checking-data check :: ll-data-term :: tvs ++
                                         [ explain ("Normalize " ^ side lr ^ " of the "
                                                   ^ expected-to-string check ^ " equation, using " ^ maybeMinus-description m
                                                   ^ " reduction." ) ])
  where side : leftRight → string
        side Left = "the left-hand side"
        side Right = "the right-hand side"
        side Both = "both sides"
        maybeMinus-description : maybeMinus → string
        maybeMinus-description EpsHnf = "head"
        maybeMinus-description EpsHanf = "head-applicative"

optGuide-spans : optGuide → checking-mode → spanM ⊤
optGuide-spans NoGuide _ = spanMok
optGuide-spans (Guide pi x tp) expected =
  get-ctxt λ Γ → spanM-add (Var-span Γ pi x expected [] nothing)

Rho-span : posinfo → term → term → checking-mode → optPlus → ℕ ⊎ var → 𝕃 tagged-val → err-m → span
Rho-span pi t t' expected r (inj₂ x) tvs =
  mk-span "Rho" pi (term-end-pos t')
    (checking-data expected :: ll-data-term :: explain ("Rewrite all places where " ^ x ^ " occurs in the " ^ expected-to-string expected ^ " type, using an equation. ") :: tvs)
Rho-span pi t t' expected r (inj₁ numrewrites) tvs err =
  mk-span "Rho" pi (term-end-pos t')
    (checking-data expected :: ll-data-term :: tvs ++
    (explain ("Rewrite terms in the "
      ^ expected-to-string expected ^ " type, using an equation. "
      ^ (if (is-rho-plus r) then "" else "Do not ") ^ "Beta-reduce the type as we look for matches.") :: fst h)) (snd h)
  where h : 𝕃 tagged-val × err-m
        h = if isJust err
              then [] , err
              else if numrewrites =ℕ 0
                then [] , just "No rewrites could be performed."
                else [ "Number of rewrites", [[ ℕ-to-string numrewrites ]] , [] ] , err

Phi-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Phi-span pi pi' expected tvs = mk-span "Phi" pi pi' (checking-data expected :: ll-data-term :: tvs)

Chi-span : ctxt → posinfo → optType → term → checking-mode → 𝕃 tagged-val → err-m → span
Chi-span Γ pi m t' check tvs = mk-span "Chi" pi (term-end-pos t')  (ll-data-term :: checking-data check :: tvs ++ helper m)
  where helper : optType → 𝕃 tagged-val
        helper (SomeType T) =  explain ("Check a term against an asserted type") :: [ to-string-tag "the asserted type" Γ T ]
        helper NoType = [ explain ("Change from checking mode (outside the term) to synthesizing (inside)") ]

Sigma-span : posinfo → term → checking-mode → 𝕃 tagged-val → err-m → span
Sigma-span pi t check tvs =
  mk-span "Sigma" pi (term-end-pos t)
     (ll-data-term :: checking-data check :: explain "Swap the sides of the equation synthesized for the body of this term" :: tvs)

Delta-span : ctxt → posinfo → optType → term → checking-mode → 𝕃 tagged-val → err-m → span
Delta-span Γ pi T t check tvs =
  mk-span "Delta" pi (term-end-pos t)
    (ll-data-term :: explain "Prove anything you want from a contradiction" :: checking-data check :: tvs)

motive-label : string
motive-label = "the motive"

the-motive : ctxt → type → tagged-val
the-motive = to-string-tag motive-label

Theta-span : ctxt → posinfo → theta → term → lterms → checking-mode → 𝕃 tagged-val → err-m → span
Theta-span Γ pi u t ls check tvs = mk-span "Theta" pi (lterms-end-pos ls) (ll-data-term :: checking-data check :: tvs ++ do-explain u)
  where do-explain : theta → 𝕃 tagged-val
        do-explain Abstract = [ explain ("Perform an elimination with the first term, after abstracting it from the expected type.") ]
        do-explain (AbstractVars vs) = [ strRunTag "explanation" Γ (strAdd "Perform an elimination with the first term, after abstracting the listed variables (" ≫str vars-to-string vs ≫str strAdd ") from the expected type.") ]
        do-explain AbstractEq = [ explain ("Perform an elimination with the first term, after abstracting it with an equation "
                                         ^ "from the expected type.") ]

Lft-span : posinfo → var → term → checking-mode → 𝕃 tagged-val → err-m → span
Lft-span pi X t check tvs = mk-span "Lift type" pi (term-end-pos t) (checking-data check :: ll-data-type :: binder-data-const :: tvs)

File-span : ctxt → posinfo → posinfo → string → span
File-span Γ pi pi' filename = mk-span ("Cedille source file (" ^ filename ^ ")") pi pi' (print-file-id-table Γ) nothing

Module-span : posinfo → posinfo → span
Module-span pi pi' = mk-span "Module declaration" pi pi' [ not-for-navigation ] nothing

Module-header-span : posinfo → posinfo → span
Module-header-span pi pi' = mk-span "Module header" pi pi' [ not-for-navigation ] nothing

Import-span : posinfo → string → posinfo → 𝕃 tagged-val → err-m → span
Import-span pi file pi' tvs = mk-span ("Import of another source file") pi pi' (location-data (file , first-position) :: tvs)

Import-module-span : ctxt → (posinfo × var) → params → 𝕃 tagged-val → err-m → span
Import-module-span Γ (pi , mn) ps tvs = mk-span "Imported module" pi (posinfo-plus-str pi mn) (params-data Γ ps ++ tvs)

punctuation-span : string → posinfo → posinfo → span
punctuation-span name pi pi'  = mk-span name pi pi' ( punctuation-data ::  not-for-navigation :: [] ) nothing

whitespace-span : posinfo → posinfo → span
whitespace-span pi pi'  = mk-span "Whitespace" pi pi' [ not-for-navigation ] nothing

comment-span : posinfo → posinfo → span
comment-span pi pi'  = mk-span "Comment" pi pi' [ not-for-navigation ] nothing

IotaPair-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
IotaPair-span pi pi' c tvs =
  mk-span "Iota pair" pi pi' (explain "Inhabit a iota-type (dependent intersection type)." :: checking-data c :: ll-data-term :: tvs)

IotaProj-span : term → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
IotaProj-span t pi' c tvs = mk-span "Iota projection" (term-start-pos t) pi' (checking-data c :: ll-data-term :: tvs)

Let-span : ctxt → checking-mode → posinfo → defTermOrType → term → 𝕃 tagged-val → err-m → span
Let-span Γ c pi d t' tvs = mk-span "Term Let" pi (term-end-pos t') (binder-data-const :: bound-data d Γ :: ll-data-term :: checking-data c :: tvs)

TpLet-span : ctxt → checking-mode → posinfo → defTermOrType → type → 𝕃 tagged-val → err-m → span
TpLet-span Γ c pi d t' tvs = mk-span "Type Let" pi (type-end-pos t') (binder-data-const :: bound-data d Γ :: ll-data-type :: checking-data c :: tvs)

Mu'-span : term → 𝕃 tagged-val → err-m → span
Mu'-span t tvs = mk-span "Mu' cases" (term-start-pos t) (term-end-pos t) tvs

Mu-span : term → 𝕃 tagged-val → err-m → span
Mu-span t tvs = mk-span "Mu fixpoint" (term-start-pos t) (term-end-pos t) tvs

DefDatatype-span : posinfo → posinfo → var → posinfo → span
DefDatatype-span pi _ x pi' = mk-span "Datatype definition" pi pi' [] nothing

DefDataConst-span : posinfo → var → span
DefDataConst-span pi c = mk-span "Datatype constructor" pi (posinfo-plus-str pi c) [] nothing

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Sets.CantorBijection.Order
open import Orders.Total.Definition
open import Orders.WellFounded.Induction

module Sets.CantorBijection.Proofs where

open Sets.CantorBijection.Order using (order ; totalOrder ; orderWellfounded)

cantorInverseLemma : (ℕ && ℕ) → (ℕ && ℕ)
cantorInverseLemma (0 ,, s) = (succ s) ,, 0
cantorInverseLemma (succ r ,, 0) = r ,, 1
cantorInverseLemma (succ r ,, succ s) = (r ,, succ (succ s))

cantorInverse : ℕ → (ℕ && ℕ)
cantorInverse zero = (0 ,, 0)
cantorInverse (succ z) = cantorInverseLemma (cantorInverse z)

cantorInverseLemmaInjective : (a b : ℕ && ℕ) → cantorInverseLemma a ≡ cantorInverseLemma b → a ≡ b
cantorInverseLemmaInjective (zero ,, b) (zero ,, .b) refl = refl
cantorInverseLemmaInjective (zero ,, b) (succ c ,, zero) ()
cantorInverseLemmaInjective (zero ,, b) (succ c ,, succ d) ()
cantorInverseLemmaInjective (succ a ,, zero) (zero ,, d) ()
cantorInverseLemmaInjective (succ a ,, succ b) (zero ,, d) ()
cantorInverseLemmaInjective (succ a ,, zero) (succ .a ,, zero) refl = refl
cantorInverseLemmaInjective (succ a ,, succ b) (succ .a ,, succ .b) refl = refl

cantorInverseLemmaSurjective : (a : ℕ && ℕ) → (a ≡ (0 ,, 0)) || (Sg (ℕ && ℕ) (λ b → cantorInverseLemma b ≡ a))
cantorInverseLemmaSurjective (zero ,, zero) = inl refl
cantorInverseLemmaSurjective (zero ,, succ zero) = inr ((1 ,, 0) , refl)
cantorInverseLemmaSurjective (zero ,, succ (succ b)) = inr ((1 ,, succ b) , refl)
cantorInverseLemmaSurjective (succ a ,, zero) = inr ((0 ,, a) , refl)
cantorInverseLemmaSurjective (succ a ,, succ zero) = inr ((succ (succ a) ,, 0) , refl)
cantorInverseLemmaSurjective (succ a ,, succ (succ b)) = inr ((succ (succ a) ,, succ b) , refl)

cantorInverseLemmaNotZero : (a : ℕ && ℕ) → (cantorInverseLemma a ≡ (0 ,, 0)) → False
cantorInverseLemmaNotZero (succ a ,, zero) ()
cantorInverseLemmaNotZero (succ a ,, succ b) ()

cantorInverseLemmaIncreases : (x : ℕ && ℕ) → order x (cantorInverseLemma x)
cantorInverseLemmaIncreases (zero ,, b) = inl (identityOfIndiscernablesRight _<N_ (a<SuccA b) (applyEquality succ (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))))
cantorInverseLemmaIncreases (succ a ,, zero) = inr (transitivity (applyEquality succ (Semiring.sumZeroRight ℕSemiring a)) (Semiring.commutative ℕSemiring 1 a) ,, (le 0 refl))
cantorInverseLemmaIncreases (succ a ,, succ b) = inr (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a (succ b))) (Semiring.commutative ℕSemiring (succ (succ b)) a) ,, (le 0 refl))

cantorInverseOrderPreserving : (x y : ℕ) → (x <N y) → order (cantorInverse x) (cantorInverse y)
cantorInverseOrderPreserving zero (succ y) x<y with TotalOrder.totality totalOrder (0 ,, 0) (cantorInverseLemma (cantorInverse y))
cantorInverseOrderPreserving zero (succ y) x<y | inl (inl bl) = bl
cantorInverseOrderPreserving zero (succ y) x<y | inl (inr bl) = exFalso (leastElement bl)
cantorInverseOrderPreserving zero (succ y) x<y | inr x = exFalso (leastElement {cantorInverse y} (identityOfIndiscernablesRight order (cantorInverseLemmaIncreases (cantorInverse y)) (equalityCommutative x)))
cantorInverseOrderPreserving (succ x) (succ y) x<y with cantorInverseOrderPreserving x y (canRemoveSuccFrom<N x<y)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr with cantorInverse x
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | x1 ,, x2 with cantorInverse y
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | zero ,, succ y2 = inl (succPreservesInequality (succIsPositive (y2 +N 0)))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, zero with TotalOrder.totality ℕTotalOrder 1 (y1 +N 1)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, zero | inl (inl pr1) = inl pr1
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, zero | inl (inr pr1) rewrite Semiring.commutative ℕSemiring y1 1 = exFalso (zeroNeverGreater (canRemoveSuccFrom<N pr1))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, zero | inr pr1 = inr (pr1 ,, le 0 refl)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring y1 (succ (succ y2)) = inl (succPreservesInequality (succIsPositive (y2 +N y1)))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | zero ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring y2 | Semiring.sumZeroRight ℕSemiring x1 = inl (TotalOrder.<Transitive ℕTotalOrder pr (a<SuccA _))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | succ y1 ,, zero rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.commutative ℕSemiring y1 1 | Semiring.sumZeroRight ℕSemiring x1 | Semiring.sumZeroRight ℕSemiring y1 = inl pr
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring x1 = inl (identityOfIndiscernablesRight _<N_ pr (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y1 (succ y2))) (Semiring.commutative ℕSemiring (succ (succ y2)) y1)))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring x2 | Semiring.sumZeroRight ℕSemiring y2 = inl (succPreservesInequality pr)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, succ x2 | succ y1 ,, zero rewrite Semiring.commutative ℕSemiring y1 1 | Semiring.sumZeroRight ℕSemiring y1 | Semiring.sumZeroRight ℕSemiring x2 = ans
  where
    ans : (succ (succ x2) <N succ y1) || (succ (succ x2) ≡ succ y1) && (zero <N 1)
    ans with TotalOrder.totality ℕTotalOrder (succ (succ x2)) (succ y1)
    ans | inl (inl x) = inl x
    ans | inl (inr x) = exFalso (noIntegersBetweenXAndSuccX (succ x2) pr x)
    ans | inr x = inr (x ,, le zero refl)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, succ x2 | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring y1 1 | Semiring.sumZeroRight ℕSemiring y1 | Semiring.sumZeroRight ℕSemiring x2 = ans
  where
    ans : (succ (succ x2) <N y1 +N succ (succ y2)) || (succ (succ x2) ≡ y1 +N succ (succ y2)) && (zero <N succ (succ y2))
    ans with TotalOrder.totality ℕTotalOrder (succ (succ x2)) (y1 +N succ (succ y2))
    ans | inl (inl x) = inl x
    ans | inl (inr x) = exFalso (noIntegersBetweenXAndSuccX (succ x2) pr (identityOfIndiscernablesLeft _<N_ x (transitivity (Semiring.commutative ℕSemiring y1 (succ (succ y2))) (applyEquality succ (Semiring.commutative ℕSemiring (succ y2) y1)))))
    ans | inr x = inr (x ,, succIsPositive (succ y2))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring y2 = inl (TotalOrder.<Transitive ℕTotalOrder (identityOfIndiscernablesLeft _<N_ pr (transitivity (applyEquality succ (Semiring.commutative ℕSemiring x1 (succ x2))) (Semiring.commutative ℕSemiring (succ (succ x2)) x1))) (a<SuccA (succ y2)))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | succ y1 ,, zero rewrite Semiring.commutative ℕSemiring y1 1 | Semiring.sumZeroRight ℕSemiring y1 | Semiring.commutative ℕSemiring x1 (succ x2) | Semiring.commutative ℕSemiring x1 (succ (succ x2)) = inl pr
cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 (succ x2) | Semiring.commutative ℕSemiring y1 (succ y2) | Semiring.commutative ℕSemiring x1 (succ (succ x2)) | Semiring.commutative ℕSemiring y1 (succ (succ y2)) = inl pr
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) with cantorInverse x
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | x1 ,, x2 with cantorInverse y
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, ()) | zero ,, zero | zero ,, zero
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (() ,, snd) | zero ,, zero | zero ,, succ y2
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (refl ,, snd) | zero ,, succ .y2 | zero ,, succ y2 = exFalso (TotalOrder.irreflexive ℕTotalOrder snd)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (refl ,, snd) | zero ,, succ .(y1 +N succ y2) | succ y1 ,, succ y2 = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder snd (identityOfIndiscernablesRight _<N_ (addingIncreases (succ y2) y1) (Semiring.commutative ℕSemiring (succ y2) (succ y1)))))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, zero | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring x1 | succInjective fst | Semiring.commutative ℕSemiring y2 1 | Semiring.sumZeroRight ℕSemiring y2 = inl (le zero refl)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, zero | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring x1 = inr (transitivity fst (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y1 (succ y2))) (Semiring.commutative ℕSemiring (succ (succ y2)) y1)) ,, succPreservesInequality snd)
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring y2 | Semiring.commutative ℕSemiring x1 (succ x2) | Semiring.commutative ℕSemiring (succ (succ x2)) x1 | fst = inl (succPreservesInequality (le zero refl))
cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, succ x2 | succ y1 ,, succ y2 = inr (transitivity (transitivity (Semiring.commutative ℕSemiring x1 (succ (succ x2))) (applyEquality succ (Semiring.commutative ℕSemiring (succ x2) x1))) (transitivity fst (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y1 (succ y2))) (Semiring.commutative ℕSemiring (succ (succ y2)) y1))) ,, succPreservesInequality snd)

cantorInverseInjective : (a b : ℕ) → cantorInverse a ≡ cantorInverse b → a ≡ b
cantorInverseInjective zero zero pr = refl
cantorInverseInjective zero (succ b) pr = exFalso (cantorInverseLemmaNotZero _ (equalityCommutative pr))
cantorInverseInjective (succ a) zero pr = exFalso (cantorInverseLemmaNotZero _ pr)
cantorInverseInjective (succ a) (succ b) pr = applyEquality succ (cantorInverseInjective a b (cantorInverseLemmaInjective (cantorInverse a) (cantorInverse b) pr))

-- Some unnecessary things on the way to the final proof
cantorInverseDiscrete : (a : ℕ) → (c : ℕ && ℕ) → order (cantorInverse a) c → order c (cantorInverse (succ a)) → False
cantorInverseDiscrete zero (zero ,, zero) (inl ()) c<sa
cantorInverseDiscrete zero (zero ,, zero) (inr ()) c<sa
cantorInverseDiscrete zero (zero ,, succ c) a<c (inl x) = zeroNeverGreater (canRemoveSuccFrom<N x)
cantorInverseDiscrete zero (succ b ,, zero) a<c (inl x) = zeroNeverGreater (canRemoveSuccFrom<N x)
cantorInverseDiscrete zero (succ b ,, succ c) a<c (inl x) = zeroNeverGreater (canRemoveSuccFrom<N x)
cantorInverseDiscrete (succ a) (b ,, c) a<c c<sa with cantorInverse a
cantorInverseDiscrete (succ a) (zero ,, zero) (inl ()) (inl x) | zero ,, zero
cantorInverseDiscrete (succ a) (zero ,, zero) (inr ()) (inl x) | zero ,, zero
cantorInverseDiscrete (succ a) (zero ,, succ zero) a<c (inl x) | zero ,, zero = TotalOrder.irreflexive ℕTotalOrder x
cantorInverseDiscrete (succ a) (zero ,, succ (succ c)) a<c (inl x) | zero ,, zero = zeroNeverGreater (canRemoveSuccFrom<N x)
cantorInverseDiscrete (succ a) (succ b ,, c) a<c (inl x) | zero ,, zero = zeroNeverGreater (canRemoveSuccFrom<N x)
cantorInverseDiscrete (succ a) (b ,, zero) (inl x) (inr (fst ,, snd)) | zero ,, zero = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x fst)
cantorInverseDiscrete (succ a) (b ,, succ c) a<c (inr (fst ,, snd)) | zero ,, zero = zeroNeverGreater (canRemoveSuccFrom<N snd)
cantorInverseDiscrete (succ a) (b ,, c) (inl y) (inl x) | zero ,, succ snd rewrite Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x y)
cantorInverseDiscrete (succ a) (b ,, succ c) (inr (fst ,, _)) (inl x) | zero ,, succ snd rewrite Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd | fst = TotalOrder.irreflexive ℕTotalOrder x
cantorInverseDiscrete (succ a) (b ,, zero) (inl x) (inr (fst ,, snd₁)) | zero ,, succ snd rewrite fst | Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd = TotalOrder.irreflexive ℕTotalOrder x
cantorInverseDiscrete (succ a) (b ,, succ c) (inl x) (inr (fst ,, snd1)) | zero ,, succ snd = zeroNeverGreater (canRemoveSuccFrom<N snd1)
cantorInverseDiscrete (succ a) (b ,, succ zero) (inr (fst ,, _)) (inr (fst₁ ,, bad)) | zero ,, succ snd = TotalOrder.irreflexive ℕTotalOrder bad
cantorInverseDiscrete (succ a) (b ,, succ (succ c)) (inr (fst ,, _)) (inr (fst₁ ,, bad)) | zero ,, succ snd = zeroNeverGreater (canRemoveSuccFrom<N bad)
cantorInverseDiscrete (succ a) (b ,, c) (inl x1) (inl x) | succ zero ,, zero = noIntegersBetweenXAndSuccX 1 x1 x
cantorInverseDiscrete (succ a) (zero ,, succ zero) (inr (fst ,, snd)) (inl x) | succ zero ,, zero = TotalOrder.irreflexive ℕTotalOrder snd
cantorInverseDiscrete (succ a) (succ b ,, succ c) (inr (fst ,, snd)) (inl x) | succ zero ,, zero rewrite Semiring.commutative ℕSemiring b (succ c) = bad fst
  where
    bad : {a : ℕ} → 1 ≡ succ (succ a) → False
    bad ()
cantorInverseDiscrete (succ a) (b ,, c) (inl y) (inl x) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder y x)
cantorInverseDiscrete (succ a) (b ,, c) (inr (bad ,, _)) (inl x) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x bad)
cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inr (bad ,, snd)) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x bad)
cantorInverseDiscrete (succ a) (b ,, c) (inr (_ ,, bad)) (inr (fst₁ ,, snd)) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = noIntegersBetweenXAndSuccX 1 bad snd
cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd = noIntegersBetweenXAndSuccX (succ (succ snd)) x y
cantorInverseDiscrete (succ a) (zero ,, c) (inr (fst ,, snd1)) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd = noIntegersBetweenXAndSuccX (succ (succ snd)) snd1 y
cantorInverseDiscrete (succ a) (succ b ,, c) (inr (fst ,, bad)) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd | fst = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder bad (identityOfIndiscernablesRight _<N_ (addingIncreases c b) (Semiring.commutative ℕSemiring c (succ b))))
cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inl y) | succ (succ fst) ,, succ snd rewrite Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder y x)
cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inr (y ,, z)) | succ (succ fst) ,, succ snd rewrite y | Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder x
cantorInverseDiscrete (succ a) (b ,, c) (inr (x ,, y)) (inl z) | succ (succ fst) ,, succ snd rewrite equalityCommutative x | Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder z
cantorInverseDiscrete (succ a) (b ,, c) (inr (x ,, y)) (inr (m ,, n)) | succ (succ fst) ,, succ snd = noIntegersBetweenXAndSuccX (succ (succ snd)) y n

boundedInversesExist : (a : ℕ && ℕ) (s : ℕ) → order a (cantorInverse s) → Sg ℕ (λ i → cantorInverse i ≡ a)
boundedInversesExist a zero a<s = exFalso (leastElement a<s)
boundedInversesExist a (succ s) a<s with TotalOrder.totality totalOrder a (cantorInverse s)
boundedInversesExist a (succ s) _ | inl (inl a<s) = boundedInversesExist a s a<s
boundedInversesExist a (succ s) a<s | inl (inr s<a) = exFalso (cantorInverseDiscrete s a s<a a<s)
boundedInversesExist a (succ s) a<s | inr a=s = s , equalityCommutative a=s

cantorInverseSurjective : (x : ℕ && ℕ) → Sg ℕ (λ i → (cantorInverse i) ≡ x)
cantorInverseSurjective = rec orderWellfounded (λ z → Sg ℕ (λ z₁ → (cantorInverse z₁) ≡ z)) go
  where
    go : (a : ℕ && ℕ) → (pr : (x : ℕ && ℕ) (x₁ : order x a) → Sg ℕ (λ z → (cantorInverse z) ≡ x)) → Sg ℕ (λ i → (cantorInverse i) ≡ a)
    go a pr with cantorInverseLemmaSurjective a
    go .(0 ,, 0) pr | inl refl = 0 , refl
    go a ind | inr (decr , proof) with ind decr (identityOfIndiscernablesRight order (cantorInverseLemmaIncreases decr) proof)
    go a ind | inr (decr , proof) | boundForDecr , boundIsBound = succ boundForDecr , transitivity (applyEquality cantorInverseLemma boundIsBound) proof


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable semi-heterogeneous vector equality over setoids
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.Vec.Relation.Binary.Equality.DecSetoid
  {a ℓ} (DS : DecSetoid a ℓ) where

open import Data.Nat using (ℕ)
import Data.Vec.Relation.Binary.Equality.Setoid as Equality
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
open import Level using (_⊔_)
open import Relation.Binary using (Decidable)

open DecSetoid DS

------------------------------------------------------------------------
-- Make all definitions from equality available

open Equality setoid public

------------------------------------------------------------------------
-- Additional properties

infix 4 _≋?_

_≋?_ : ∀ {m n} → Decidable (_≋_ {m} {n})
_≋?_ = PW.decidable _≟_

≋-isDecEquivalence : ∀ n → IsDecEquivalence (_≋_ {n})
≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence

≋-decSetoid : ℕ → DecSetoid a (a ⊔ ℓ)
≋-decSetoid = PW.decSetoid DS


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

open import Data.Nat
open import Data.Fin

module Examples.Lambda.Lambda where

  {- Terms & Values -}
  data Term (n : ℕ) : Set where
    var : Fin n → Term n
    lambda : Term (suc n) → Term n
    app : Term n → Term n → Term n

  data Value : Set where
    lambda : Term 1 → Value

  term : Value → Term 0
  term (lambda x) = lambda x

  {- Substitution -}
  ext : ∀{n m} → (Fin n → Fin m) → (Fin (suc n) → Fin (suc m))
  ext f zero = zero
  ext f (suc n) = suc (f n)

  rename : ∀{n m} → (Fin n → Fin m) → (Term n → Term m)
  rename f (var x) = var (f x)
  rename f (lambda t) = lambda (rename (ext f) t)
  rename f (app t t₁) = app (rename f t) (rename f t₁)

  exts : ∀{n m} → (Fin n → Term m) → (Fin (suc n) → Term (suc m))
  exts _ zero = var zero
  exts f (suc n) = rename suc (f n)

  subst : ∀{n m} → (Fin n → Term m) → (Term n → Term m)
  subst f (var x) = f x
  subst f (lambda t) = lambda (subst (exts f) t)
  subst f (app t t₁) = app (subst f t) (subst f t₁)

  subst-0 : ∀{n} → Term (suc n) → Term n → Term n
  subst-0 {n} t t₁ = subst {suc n}{n} f t where
    f : Fin (suc n) → Term n
    f zero = t₁
    f (suc n) = var n

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
module Spire.Type where

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

data ⊥ : Set where
record ⊤ : Set where constructor tt
data Bool : Set where true false : Bool

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ    #-}

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁
open Σ public

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

const : {A : Set₁} {B : Set} → A → B → A
const a _ = a

uncurry : {A : Set} {B : A → Set} {C : Σ A B → Set} →
  ((a : A) → (b : B a) → C (a , b)) →
  ((p : Σ A B) → C p)
uncurry f (a , b) = f a b

_∘_ : {A B C : Set₁} → (B → C) → (A → B) → A → C
_∘_ g f x = g (f x)

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

elim⊥ : {A : Set} → ⊥ → A
elim⊥ ()

elimBool : (P : Bool → Set)
  (pt : P true)
  (pf : P false)
  (b : Bool) → P b
elimBool P pt pf true = pt
elimBool P pt pf false = pf

if_then_else_ : {C : Set} → Bool → C → C → C
if b then c₁ else c₂ = elimBool _ c₁ c₂ b

elimℕ : (P : ℕ → Set)
  (pz : P zero)
  (ps : (n : ℕ) → P n → P (suc n))
  (n : ℕ) → P n
elimℕ P pz ps zero = pz
elimℕ P pz ps (suc n) = ps n (elimℕ P pz ps n)

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

record Universe : Set₁ where
  field
    Codes : Set
    Meaning : Codes → Set

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

data DescForm (U : Universe) : Set where
  `⊤ `X : DescForm U
  `Π `Σ : (A : Universe.Codes U)
    (D : Universe.Meaning U A → DescForm U)
    → DescForm U

⟦_/_⟧ᵈ : (U : Universe) → DescForm U → Set → Set
⟦ U / `⊤ ⟧ᵈ X = ⊤
⟦ U / `X ⟧ᵈ X = X
⟦ U / `Π A D ⟧ᵈ X =
  (a : Universe.Meaning U A) → ⟦ U / D a ⟧ᵈ X
⟦ U / `Σ A D ⟧ᵈ X =
  Σ (Universe.Meaning U A) (λ a → ⟦ U / D a ⟧ᵈ X)

data μ {U : Universe} (D : DescForm U) : Set where
  con : ⟦ U / D ⟧ᵈ (μ D) → μ D

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

data TypeForm (U : Universe) : Set
⟦_/_⟧ : (U : Universe) → TypeForm U → Set

data TypeForm U where
  `⊥ `⊤ `Bool `ℕ `Desc `Type : TypeForm U
  `Π `Σ : (A : TypeForm U)
    (B : ⟦ U / A ⟧ → TypeForm U)
    → TypeForm U
  `⟦_⟧ : Universe.Codes U → TypeForm U
  `⟦_⟧ᵈ : DescForm U → TypeForm U → TypeForm U
  `μ : DescForm U → TypeForm U

⟦ U / `⊥ ⟧ = ⊥
⟦ U / `⊤ ⟧ = ⊤
⟦ U / `Bool ⟧ = Bool
⟦ U / `ℕ ⟧ = ℕ
⟦ U / `Π A B ⟧ = (a : ⟦ U / A ⟧) → ⟦ U / B a ⟧
⟦ U / `Σ A B ⟧ = Σ ⟦ U / A ⟧ (λ a → ⟦ U / B a ⟧)
⟦ U / `Type ⟧ = Universe.Codes U
⟦ U / `⟦ A ⟧ ⟧ = Universe.Meaning U A
⟦ U / `Desc ⟧ = DescForm U
⟦ U / `⟦ D ⟧ᵈ X ⟧ = ⟦ U / D ⟧ᵈ ⟦ U / X ⟧
⟦ U / `μ D ⟧ = μ D

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

_`→_ : ∀{U} (A B : TypeForm U) → TypeForm U
A `→ B = `Π A (λ _ → B)

Level : (ℓ : ℕ) → Universe
Level zero = record { Codes = ⊥ ; Meaning = λ() }
Level (suc ℓ) = record { Codes = TypeForm (Level ℓ)
                       ; Meaning = ⟦_/_⟧ (Level ℓ) }

Type : ℕ → Set
Type ℓ = TypeForm (Level ℓ)

Desc : ℕ → Set
Desc ℓ = DescForm (Level ℓ)

infix 0 ⟦_∣_⟧
⟦_∣_⟧ : (ℓ : ℕ) → Type ℓ → Set
⟦ ℓ ∣ A ⟧ = ⟦ Level ℓ / A ⟧

⟦_∣_⟧ᵈ : (ℓ : ℕ) → Desc ℓ → Set → Set
⟦ ℓ ∣ D ⟧ᵈ X = ⟦ Level ℓ / D ⟧ᵈ X

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

elimDesc : (P : (ℓ : ℕ) → Desc ℓ → Set)
  → ((ℓ : ℕ) → P ℓ `⊤)
  → ((ℓ : ℕ) → P ℓ `X)
  → ((ℓ : ℕ) (A : Type ℓ) (D : ⟦ ℓ ∣ A ⟧ → Desc (suc ℓ))
    (rec : (a : ⟦ ℓ ∣ A ⟧) → P (suc ℓ) (D a))
    → P (suc ℓ) (`Π A D))
  → ((ℓ : ℕ) (A : Type ℓ) (D : ⟦ ℓ ∣ A ⟧ → Desc (suc ℓ))
    (rec : (a : ⟦ ℓ ∣ A ⟧) → P (suc ℓ) (D a))
    → P (suc ℓ) (`Σ A D))
  → (ℓ : ℕ) (D : Desc ℓ) → P ℓ D
elimDesc P p⊤ pX pΠ pΣ ℓ `⊤ = p⊤ ℓ
elimDesc P p⊤ pX pΠ pΣ ℓ `X = pX ℓ
elimDesc P p⊤ pX pΠ pΣ zero (`Π () D)
elimDesc P p⊤ pX pΠ pΣ (suc ℓ) (`Π A D) =
  let f = elimDesc P p⊤ pX pΠ pΣ (suc ℓ)
  in pΠ ℓ A D (λ a → f (D a))
elimDesc P p⊤ pX pΠ pΣ zero (`Σ () D)
elimDesc P p⊤ pX pΠ pΣ (suc ℓ) (`Σ A D) =
  let f = elimDesc P p⊤ pX pΠ pΣ (suc ℓ)
  in pΣ ℓ A D (λ a → f (D a))

des : ∀{ℓ} {D : Desc ℓ} → μ D → ⟦ ℓ ∣ D ⟧ᵈ (μ D)
des (con x) = x

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

elimType : (P : (ℓ : ℕ) → Type ℓ → Set)
  → ((ℓ : ℕ) → P ℓ `⊥)
  → ((ℓ : ℕ) → P ℓ `⊤)
  → ((ℓ : ℕ) → P ℓ `Bool)
  → ((ℓ : ℕ) → P ℓ `ℕ)
  → ((ℓ : ℕ) (A : Type ℓ) (B : ⟦ ℓ ∣ A ⟧ → Type ℓ)
    (rec₁ : P ℓ A)
    (rec₂ : (a : ⟦ ℓ ∣ A ⟧) → P ℓ (B a))
    → P ℓ (`Π A B))
  → ((ℓ : ℕ) (A : Type ℓ) (B : ⟦ ℓ ∣ A ⟧ → Type ℓ)
    (rec₁ : P ℓ A)
    (rec₂ : (a : ⟦ ℓ ∣ A ⟧) → P ℓ (B a))
    → P ℓ (`Σ A B))
  → ((ℓ : ℕ) → P ℓ `Desc)
  → ((ℓ : ℕ) (D : Desc ℓ) (X : Type ℓ) (rec : P ℓ X) → P ℓ (`⟦ D ⟧ᵈ X))
  → ((ℓ : ℕ) (D : Desc ℓ) → P ℓ (`μ D))
  → ((ℓ : ℕ) → P ℓ `Type)
  → ((ℓ : ℕ) (A : Type ℓ) (rec : P ℓ A) → P (suc ℓ) `⟦ A ⟧)
  → (ℓ : ℕ) (A : Type ℓ) → P ℓ A

elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ `⊥ = p⊥ ℓ
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ `⊤ = p⊤ ℓ
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ `Bool = pBool ℓ
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ `ℕ = pℕ ℓ
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ (`Π A B) =
  let f = elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧ ℓ
  in pΠ ℓ A B (f A) (λ a → f (B a))
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ (`Σ A B) =
  let f = elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧ ℓ
  in pΣ ℓ A B (f A) (λ a → f (B a))
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ `Type = pType ℓ
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ `Desc = pDesc ℓ
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ (`⟦ D ⟧ᵈ X) =
  let f = elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧ ℓ
  in p⟦D⟧ᵈ ℓ D X (f X)
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  ℓ (`μ D) = pμ ℓ D
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  zero `⟦ () ⟧
elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧
  (suc ℓ) `⟦ A ⟧ =
  let f = elimType P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧ ℓ
  in p⟦A⟧ ℓ A (f A)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
module Thesis.Changes where

open import Data.Product
open import Data.Sum
open import Data.Unit
open import Relation.Binary.PropositionalEquality

record IsChangeStructure (A : Set) (ChA : Set) (ch_from_to_ : (dv : ChA) → (v1 v2 : A) → Set) : Set₁ where
  infixl 6 _⊕_ _⊝_
  field
    _⊕_ : A → ChA → A
    fromto→⊕ : ∀ dv v1 v2 →
      ch dv from v1 to v2 →
      v1 ⊕ dv ≡ v2
    _⊝_ : A → A → ChA
    ⊝-fromto : ∀ (a b : A) → ch (b ⊝ a) from a to b

  update-diff : (b a : A) → a ⊕ (b ⊝ a) ≡ b
  update-diff b a = fromto→⊕ (b ⊝ a) a b (⊝-fromto a b)
  nil : A → ChA
  nil a = a ⊝ a
  nil-fromto : (a : A) → ch (nil a) from a to a
  nil-fromto a = ⊝-fromto a a
  update-nil : (a : A) → a ⊕ nil a ≡ a
  update-nil a = update-diff a a

  valid : ∀ (a : A) (da : ChA) → Set
  valid a da = ch da from a to (a ⊕ da)
  Δ₁ : (a : A) → Set
  Δ₁ a = Σ[ da ∈ ChA ] valid a da
  Δ₂ : (a1 : A) (a2 : A) → Set
  Δ₂ a1 a2 = Σ[ da ∈ ChA ] ch da from a1 to a2

  _⊕'_ : (a1 : A) -> {a2 : A} -> (da : Δ₂ a1 a2) -> A
  a1 ⊕' (da , daa) = a1 ⊕ da

record IsCompChangeStructure (A : Set) (ChA : Set) (ch_from_to_ : (dv : ChA) → (v1 v2 : A) → Set) : Set₁ where
  field
    isChangeStructure : IsChangeStructure A ChA ch_from_to_
    _⊚_ : ChA → ChA → ChA
    ⊚-fromto : ∀ (a1 a2 a3 : A) (da1 da2 : ChA) →
      ch da1 from a1 to a2 → ch da2 from a2 to a3 → ch da1 ⊚ da2 from a1 to a3

  open IsChangeStructure isChangeStructure public
  ⊚-correct : ∀ (a1 a2 a3 : A) (da1 da2 : ChA) →
    ch da1 from a1 to a2 → ch da2 from a2 to a3 →
    a1 ⊕ (da1 ⊚ da2) ≡ a3
  ⊚-correct a1 a2 a3 da1 da2 daa1 daa2 = fromto→⊕ _ _ _ (⊚-fromto _ _ _ da1 da2 daa1 daa2)

record ChangeStructure (A : Set) : Set₁ where
  field
    Ch : Set
    ch_from_to_ : (dv : Ch) → (v1 v2 : A) → Set
    isCompChangeStructure : IsCompChangeStructure A Ch ch_from_to_
  open IsCompChangeStructure isCompChangeStructure public

open ChangeStructure {{...}} public hiding (Ch)
Ch : ∀ (A : Set) → {{CA : ChangeStructure A}} → Set
Ch A {{CA}} = ChangeStructure.Ch CA

-- infix 2 Σ-syntax

-- Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
-- Σ-syntax = Σ

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

⊚-syntax : ∀ (A : Set) → {{CA : ChangeStructure A}} → Ch A → Ch A → Ch A
⊚-syntax A {{CA}} da1 da2 = _⊚_ {{CA}} da1 da2
syntax ⊚-syntax A da1 da2 = da1 ⊚[ A ] da2

{-# DISPLAY IsChangeStructure._⊕_ x = _⊕_ #-}
{-# DISPLAY ChangeStructure._⊕_ x = _⊕_ #-}
{-# DISPLAY IsChangeStructure._⊝_ x = _⊝_ #-}
{-# DISPLAY ChangeStructure._⊝_ x = _⊝_ #-}
{-# DISPLAY IsChangeStructure.nil x = nil #-}
{-# DISPLAY ChangeStructure.nil x = nil #-}
{-# DISPLAY IsCompChangeStructure._⊚_ x = _⊚_ #-}
{-# DISPLAY ChangeStructure._⊚_ x = _⊚_ #-}
{-# DISPLAY ChangeStructure.ch_from_to_ x = ch_from_to_ #-}

module _ {A B : Set} {{CA : ChangeStructure A}} {{CB : ChangeStructure B}} where

  -- In this module, given change structures CA and CB for A and B, we define
  -- change structures for A → B, A × B and A ⊎ B.

  open import Postulate.Extensionality

  -- Functions
  instance
    funCS : ChangeStructure (A → B)

  infixl 6 _f⊕_ _f⊝_
  private
    fCh = A → Ch A → Ch B

    fCh_from_to_ : (df : fCh) → (f1 f2 : A → B) → Set
    fCh_from_to_ =
      λ df f1 f2 → ∀ da (a1 a2 : A) (daa : ch da from a1 to a2) →
        ch df a1 da from f1 a1 to f2 a2

    _f⊕_ : (A → B) → fCh → A → B
    _f⊕_ = λ f df a → f a ⊕ df a (nil a)

    _f⊝_ : (g f : A → B) → fCh
    _f⊝_ = λ g f a da → g (a ⊕ da) ⊝ f a

    f⊝-fromto : ∀ (f1 f2 : A → B) → fCh (f2 f⊝ f1) from f1 to f2
    f⊝-fromto f1 f2 da a1 a2 daa
      rewrite sym (fromto→⊕ da a1 a2 daa) = ⊝-fromto (f1 a1) (f2 (a1 ⊕ da))

    _f⊚_ : fCh → fCh → fCh
    _f⊚_ df1 df2 = λ a da → df1 a (nil a) ⊚[ B ] df2 a da

    _f2⊚_ : fCh → fCh → fCh
    _f2⊚_ df1 df2 = λ a da → df1 a da ⊚[ B ] df2 (a ⊕ da) (nil (a ⊕ da))

    f⊚-fromto : ∀ (f1 f2 f3 : A → B) (df1 df2 : fCh) → fCh df1 from f1 to f2 → fCh df2 from f2 to f3 →
      fCh df1 f⊚ df2 from f1 to f3
    f⊚-fromto f1 f2 f3 df1 df2 dff1 dff2 da a1 a2 daa =
      ⊚-fromto (f1 a1) (f2 a1) (f3 a2)
        (df1 a1 (nil a1))
        (df2 a1 da)
        (dff1 (nil a1) a1 a1 (nil-fromto a1))
        (dff2 da a1 a2 daa)

    f⊚2-fromto : ∀ (f1 f2 f3 : A → B) (df1 df2 : fCh) → fCh df1 from f1 to f2 → fCh df2 from f2 to f3 →
      fCh df1 f2⊚ df2 from f1 to f3
    f⊚2-fromto f1 f2 f3 df1 df2 dff1 dff2 da a1 a2 daa rewrite fromto→⊕ da a1 a2 daa =
      ⊚-fromto (f1 a1) (f2 a2) (f3 a2)
        (df1 a1 da)
        (df2 a2 (nil a2))
        (dff1 da a1 a2 daa)
        (dff2 (nil a2) a2 a2 (nil-fromto a2))

  funCS = record
    { Ch = fCh
    ; ch_from_to_ =
      λ df f1 f2 → ∀ da (a1 a2 : A) (daa : ch da from a1 to a2) →
        ch df a1 da from f1 a1 to f2 a2
    ; isCompChangeStructure = record
      { isChangeStructure = record
        { _⊕_ = _f⊕_
        ; fromto→⊕ = λ df f1 f2 dff →
          ext (λ v →
            fromto→⊕ (df v (nil v)) (f1 v) (f2 v) (dff (nil v) v v (nil-fromto v)))
        ; _⊝_ = _f⊝_
        ; ⊝-fromto = f⊝-fromto
        }
      ; _⊚_ = _f⊚_
      ; ⊚-fromto = f⊚-fromto
      }
    }

  -- Products
  private
    pCh = Ch A × Ch B
    _p⊕_ : A × B → Ch A × Ch B → A × B
    _p⊕_ (a , b) (da , db) = a ⊕ da , b ⊕ db
    _p⊝_ : A × B → A × B → pCh
    _p⊝_ (a2 , b2) (a1 , b1) = a2 ⊝ a1 , b2 ⊝ b1
    pch_from_to_ : pCh → A × B → A × B → Set
    pch (da , db) from (a1 , b1) to (a2 , b2) = ch da from a1 to a2 × ch db from b1 to b2
    _p⊚_ : pCh → pCh → pCh
    (da1 , db1) p⊚ (da2 , db2) = da1 ⊚[ A ] da2 , db1 ⊚[ B ] db2
    pfromto→⊕ : ∀ dp p1 p2 →
      pch dp from p1 to p2 → p1 p⊕ dp ≡ p2
    pfromto→⊕ (da , db) (a1 , b1) (a2 , b2) (daa , dbb) =
      cong₂ _,_ (fromto→⊕ _ _ _ daa) (fromto→⊕ _ _ _ dbb)
    p⊝-fromto : ∀ (p1 p2 : A × B) → pch p2 p⊝ p1 from p1 to p2
    p⊝-fromto (a1 , b1) (a2 , b2) = ⊝-fromto a1 a2 , ⊝-fromto b1 b2
    p⊚-fromto : ∀ p1 p2 p3 dp1 dp2 →
      pch dp1 from p1 to p2 → (pch dp2 from p2 to p3) → pch dp1 p⊚ dp2 from p1 to p3
    p⊚-fromto (a1 , b1) (a2 , b2) (a3 , b3) (da1 , db1) (da2 , db2)
      (daa1 , dbb1) (daa2 , dbb2) =
        ⊚-fromto a1 a2 a3 da1 da2 daa1 daa2 , ⊚-fromto b1 b2 b3 db1 db2 dbb1 dbb2

  instance
    pairCS : ChangeStructure (A × B)
  pairCS = record
    { Ch = pCh
    ; ch_from_to_ = pch_from_to_
    ; isCompChangeStructure = record
      { isChangeStructure = record
        { _⊕_ = _p⊕_
        ; fromto→⊕ = pfromto→⊕
        ; _⊝_ = _p⊝_
        ; ⊝-fromto = p⊝-fromto
        }
      ; _⊚_ = _p⊚_
      ; ⊚-fromto = p⊚-fromto
      }
    }

  -- Sums
  private
    SumChange = (Ch A ⊎ Ch B) ⊎ (A ⊎ B)

  data SumChange2 : Set where
    ch₁ : (da : Ch A) → SumChange2
    ch₂ : (db : Ch B) → SumChange2
    rp : (s : A ⊎ B) → SumChange2

  convert : SumChange → SumChange2
  convert (inj₁ (inj₁ da)) = ch₁ da
  convert (inj₁ (inj₂ db)) = ch₂ db
  convert (inj₂ s) = rp s
  convert₁ : SumChange2 → SumChange
  convert₁ (ch₁ da) = inj₁ (inj₁ da)
  convert₁ (ch₂ db) = inj₁ (inj₂ db)
  convert₁ (rp s) = inj₂ s

  inv1 : ∀ ds → convert₁ (convert ds) ≡ ds
  inv1 (inj₁ (inj₁ da)) = refl
  inv1 (inj₁ (inj₂ db)) = refl
  inv1 (inj₂ s) = refl
  inv2 : ∀ ds → convert (convert₁ ds) ≡ ds
  inv2 (ch₁ da) = refl
  inv2 (ch₂ db) = refl
  inv2 (rp s) = refl

  private
    _s⊕2_ : A ⊎ B → SumChange2 → A ⊎ B
    _s⊕2_ s (rp s₁) = s₁
    _s⊕2_ (inj₁ a) (ch₁ da) = inj₁ (a ⊕ da)
    _s⊕2_ (inj₂ b) (ch₂ db) = inj₂ (b ⊕ db)
    _s⊕2_ (inj₂ b) (ch₁ da) = inj₂ b -- invalid
    _s⊕2_ (inj₁ a) (ch₂ db) = inj₁ a -- invalid

    _s⊕_ : A ⊎ B → SumChange → A ⊎ B
    s s⊕ ds = s s⊕2 (convert ds)

    _s⊝2_ : A ⊎ B → A ⊎ B → SumChange2
    _s⊝2_ (inj₁ x2) (inj₁ x1) = ch₁ (x2 ⊝ x1)
    _s⊝2_ (inj₂ y2) (inj₂ y1) = ch₂ (y2 ⊝ y1)
    _s⊝2_ s2 s1 = rp s2

    _s⊝_ : A ⊎ B → A ⊎ B → SumChange
    s2 s⊝ s1 = convert₁ (s2 s⊝2 s1)

  data sch_from_to_ : SumChange → A ⊎ B → A ⊎ B → Set where
    -- sft = Sum From To
    sft₁ : ∀ {da a1 a2} (daa : ch da from a1 to a2) → sch (convert₁ (ch₁ da)) from (inj₁ a1) to (inj₁ a2)
    sft₂ : ∀ {db b1 b2} (dbb : ch db from b1 to b2) → sch (convert₁ (ch₂ db)) from (inj₂ b1) to (inj₂ b2)
    sftrp : ∀ s1 s2 → sch (convert₁ (rp s2)) from s1 to s2

  sfromto→⊕2 : (ds : SumChange2) (s1 s2 : A ⊎ B) →
    sch convert₁ ds from s1 to s2 → s1 s⊕2 ds ≡ s2
  sfromto→⊕2 (ch₁ da) (inj₁ a1) (inj₁ a2) (sft₁ daa) = cong inj₁ (fromto→⊕ _ _ _ daa)
  sfromto→⊕2 (ch₂ db) (inj₂ b1) (inj₂ b2) (sft₂ dbb) = cong inj₂ (fromto→⊕ _ _ _ dbb)
  sfromto→⊕2 (rp .s2) .s1 .s2 (sftrp s1 s2) = refl

  sfromto→⊕ : (ds : SumChange) (s1 s2 : A ⊎ B) →
    sch ds from s1 to s2 → s1 s⊕ ds ≡ s2
  sfromto→⊕ ds s1 s2 dss =
    sfromto→⊕2 (convert ds) s1 s2
      (subst (sch_from s1 to s2) (sym (inv1 ds))
        dss)
  s⊝-fromto : (s1 s2 : A ⊎ B) → sch s2 s⊝ s1 from s1 to s2
  s⊝-fromto (inj₁ a1) (inj₁ a2) = sft₁ (⊝-fromto a1 a2)
  s⊝-fromto (inj₂ b1) (inj₂ b2) = sft₂ (⊝-fromto b1 b2)
  s⊝-fromto s1@(inj₁ a1) s2@(inj₂ b2) = sftrp s1 s2
  s⊝-fromto s1@(inj₂ b1) s2@(inj₁ a2) = sftrp s1 s2

  _s⊚2_ : SumChange2 → SumChange2 → SumChange2
  ds1 s⊚2 rp s3 = rp s3
  ch₁ da1 s⊚2 ch₁ da2 = ch₁ (da1 ⊚[ A ] da2)
  rp (inj₁ a2) s⊚2 ch₁ da2 = rp (inj₁ (a2 ⊕ da2))
  ch₂ db1 s⊚2 ch₂ db2 = ch₂ (db1 ⊚[ B ] db2)
  rp (inj₂ b2) s⊚2 ch₂ db2 = rp (inj₂ (b2 ⊕ db2))
  -- Cases for invalid combinations of input changes.
  --
  -- That is, whenever ds2 is a non-replacement change for outputs that ds1
  -- can't produce.
  --
  -- We can prove validity preservation *without* filling this in.
  ds1 s⊚2 ds2 = ds1

  _s⊚_ : SumChange → SumChange → SumChange
  ds1 s⊚ ds2 = convert₁ (convert ds1 s⊚2 convert ds2)

  s⊚-fromto : (s1 s2 s3 : A ⊎ B) (ds1 ds2 : SumChange) →
      sch ds1 from s1 to s2 →
      sch ds2 from s2 to s3 → sch ds1 s⊚ ds2 from s1 to s3

  s⊚-fromto (inj₁ a1) (inj₁ a2) (inj₁ a3) (inj₁ (inj₁ da1)) (inj₁ (inj₁ da2)) (sft₁ daa1) (sft₁ daa2) = sft₁ (⊚-fromto a1 a2 a3 _ _ daa1 daa2)
  s⊚-fromto (inj₂ b1) (inj₂ b2) (inj₂ b3) (inj₁ (inj₂ db1)) (inj₁ (inj₂ db2)) (sft₂ dbb1) (sft₂ dbb2) = sft₂ (⊚-fromto b1 b2 b3 _ _ dbb1 dbb2)
  s⊚-fromto s1 (inj₁ a2) (inj₁ a3) .(inj₂ (inj₁ _)) .(inj₁ (inj₁ _)) (sftrp .s1 .(inj₁ _)) (sft₁ daa) rewrite fromto→⊕ _ a2 a3 daa = sftrp _ _
  s⊚-fromto s1 (inj₂ b2) (inj₂ b3) .(inj₂ (inj₂ _)) .(inj₁ (inj₂ _)) (sftrp .s1 .(inj₂ _)) (sft₂ dbb) rewrite fromto→⊕ _ b2 b3 dbb = sftrp _ _
  s⊚-fromto s1 s2 s3 _ _ _ (sftrp .s2 .s3) = sftrp s1 s3

  -- s⊚-fromto .(inj₂ b1) .(inj₁ a2) (inj₁ a3) .(inj₂ (inj₁ a2)) (inj₁ (inj₁ da2)) (sftrp (inj₂ b1) (inj₁ a2)) (sft₁ daa2) with sfromto→⊕ (inj₁ (inj₁ da2)) _ _ (sft₁ daa2)
  -- s⊚-fromto .(inj₂ b1) .(inj₁ a2) (inj₁ .(a2 ⊕ da2)) .(inj₂ (inj₁ a2)) (inj₁ (inj₁ da2)) (sftrp (inj₂ b1) (inj₁ a2)) (sft₁ daa2) | refl = sftrp (inj₂ b1) (inj₁ (a2 ⊕ da2))
  -- s⊚-fromto .(inj₁ a1) .(inj₂ b2) (inj₂ b3) .(inj₂ (inj₂ b2)) (inj₁ (inj₂ db2)) (sftrp (inj₁ a1) (inj₂ b2)) (sft₂ dbb2) with sfromto→⊕ (inj₁ (inj₂ db2)) _ _ (sft₂ dbb2)
  -- s⊚-fromto .(inj₁ a1) .(inj₂ b2) (inj₂ .(b2 ⊕ db2)) .(inj₂ (inj₂ b2)) (inj₁ (inj₂ db2)) (sftrp (inj₁ a1) (inj₂ b2)) (sft₂ dbb2) | refl = sftrp (inj₁ a1) (inj₂ (b2 ⊕ db2))

  instance
    sumCS : ChangeStructure (A ⊎ B)
  sumCS = record
    { Ch = SumChange
    ; ch_from_to_ = sch_from_to_
    ; isCompChangeStructure = record
      { isChangeStructure = record
      { _⊕_ = _s⊕_
      ; fromto→⊕ = sfromto→⊕
      ; _⊝_ = _s⊝_
      ; ⊝-fromto = s⊝-fromto
      }
      ; _⊚_ = _s⊚_
      ; ⊚-fromto = s⊚-fromto
      }
    }

instance
  unitCS : ChangeStructure ⊤

  unitCS = record
    { Ch = ⊤
    ; ch_from_to_ = λ dv v1 v2 → ⊤
    ; isCompChangeStructure = record
      { isChangeStructure = record
      { _⊕_ = λ _ _ → tt
      ; fromto→⊕ = λ { _ _ tt _ → refl }
      ; _⊝_ = λ _ _ → tt
      ; ⊝-fromto = λ a b → tt
      }
      ; _⊚_ = λ da1 da2 → tt
      ; ⊚-fromto = λ a1 a2 a3 da1 da2 daa1 daa2 → tt
      }
    }

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import LogicalFormulae

module Monoids.Definition where

record Monoid {a : _} {A : Set a} (Zero : A) (_+_ : A → A → A) : Set a where
  field
    associative : (a b c : A) → a + (b + c) ≡ (a + b) + c
    idLeft : (a : A) → Zero + a ≡ a
    idRight : (a : A) → a + Zero ≡ a