text:
module Data.Num.Next where

open import Data.Num.Core
open import Data.Num.Maximum
open import Data.Num.Bounded

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)

open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product

open import Function
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

--------------------------------------------------------------------------------
-- next-numeral: NullBase
--------------------------------------------------------------------------------

next-numeral-NullBase : ∀ {d o}
    → (xs : Numeral 0 (suc d) o)
    → ¬ (Maximum xs)
    → Numeral 0 (suc d) o
next-numeral-NullBase xs       ¬max with Greatest? (lsd xs)
next-numeral-NullBase xs       ¬max | yes greatest =
    contradiction (Maximum-NullBase-Greatest xs greatest) ¬max
next-numeral-NullBase (x ∙)    ¬max | no ¬greatest = digit+1 x ¬greatest ∙
next-numeral-NullBase (x ∷ xs) ¬max | no ¬greatest = digit+1 x ¬greatest ∷ xs

next-numeral-NullBase-lemma : ∀ {d o}
    → (xs : Numeral 0 (suc d) o)
    → (¬max : ¬ (Maximum xs))
    → ⟦ next-numeral-NullBase xs ¬max ⟧ ≡ suc ⟦ xs ⟧
next-numeral-NullBase-lemma {d} {o} xs    ¬max with Greatest? (lsd xs)
next-numeral-NullBase-lemma {d} {o} xs    ¬max | yes greatest =
    contradiction (Maximum-NullBase-Greatest xs greatest) ¬max
next-numeral-NullBase-lemma {d} {o} (x ∙) ¬max | no ¬greatest =
    begin
        Digit-toℕ (digit+1 x ¬greatest) o
    ≡⟨ digit+1-toℕ x ¬greatest ⟩
        suc (Fin.toℕ x + o)
    ∎
next-numeral-NullBase-lemma {d} {o} (x ∷ xs) ¬max | no ¬greatest =
    begin
        ⟦ digit+1 x ¬greatest ∷ xs ⟧
    ≡⟨ refl ⟩
        Digit-toℕ (digit+1 x ¬greatest) o + ⟦ xs ⟧ * zero
    ≡⟨ cong (λ w → w + ⟦ xs ⟧ * zero) (digit+1-toℕ x ¬greatest) ⟩
        suc (Fin.toℕ x + o + ⟦ xs ⟧ * zero)
    ≡⟨ refl ⟩
        suc ⟦ x ∷ xs ⟧
    ∎

next-numeral-is-greater-NullBase : ∀ {d o}
    → (xs : Numeral 0 (suc d) o)
    → (¬max : ¬ (Maximum xs))
    → ⟦ next-numeral-NullBase xs ¬max ⟧ > ⟦ xs ⟧
next-numeral-is-greater-NullBase xs ¬max =
    start
        suc ⟦ xs ⟧
    ≈⟨ sym (next-numeral-NullBase-lemma xs ¬max) ⟩
        ⟦ next-numeral-NullBase xs ¬max ⟧
    □

next-numeral-is-immediate-NullBase : ∀ {d o}
    → (xs : Numeral 0 (suc d) o)
    → (ys : Numeral 0 (suc d) o)
    → (¬max : ¬ (Maximum xs))
    → ⟦ ys ⟧ > ⟦ xs ⟧
    → ⟦ ys ⟧ ≥ ⟦ next-numeral-NullBase xs ¬max ⟧
next-numeral-is-immediate-NullBase xs ys ¬max prop =
    start
        ⟦ next-numeral-NullBase xs ¬max ⟧
    ≈⟨ next-numeral-NullBase-lemma xs ¬max ⟩
        suc ⟦ xs ⟧
    ≤⟨ prop ⟩
        ⟦ ys ⟧
    □

--------------------------------------------------------------------------------
-- next-numeral: Proper
--------------------------------------------------------------------------------

mutual
    Gapped#0 : ∀ b d o → Set
    Gapped#0 b d o = suc d < carry o * suc b

    Gapped#N : ∀ b d o
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → Set
    Gapped#N b d o xs proper = suc d < (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
        where
            next-xs : Numeral (suc b) (suc d) o
            next-xs = next-numeral-Proper xs proper

    Gapped#0? :  ∀ b d o → Dec (Gapped#0 b d o)
    Gapped#0? b d o = suc (suc d) ≤? carry o * suc b

    Gapped#N? :  ∀ b d o
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → Dec (Gapped#N b d o xs proper)
    Gapped#N? b d o xs proper = suc (suc d) ≤? (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
        where
            next-xs : Numeral (suc b) (suc d) o
            next-xs = next-numeral-Proper xs proper

    -- Gap#N
    Gapped : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → Set
    Gapped {b} {d} {o} (x ∙)    proper = Gapped#0 b d o
    Gapped {b} {d} {o} (x ∷ xs) proper = Gapped#N b d o xs proper

    Gapped? : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → Dec (Gapped {b} {d} {o} xs proper)
    Gapped? {b} {d} {o} (x ∙)    proper = Gapped#0? b d o
    Gapped? {b} {d} {o} (x ∷ xs) proper = Gapped#N? b d o xs proper

    data NextView : (b d o : ℕ) (xs : Numeral b d o) (proper : 2 ≤ d + o) → Set where
        Interval : ∀ b d o
            → {xs : Numeral (suc b) (suc d) o}
            → {proper : 2 ≤ suc (d + o)}
            → (¬greatest : ¬ (Greatest (lsd xs)))
            → NextView (suc b) (suc d) o xs proper
        GappedEndpoint : ∀ b d o
            → {xs : Numeral (suc b) (suc d) o}
            → {proper : 2 ≤ suc (d + o)}
            → (greatest : Greatest (lsd xs))
            → (gapped : Gapped xs proper)
            → NextView (suc b) (suc d) o xs proper
        UngappedEndpoint : ∀ b d o
            → {xs : Numeral (suc b) (suc d) o}
            → {proper : 2 ≤ suc (d + o)}
            → (greatest : Greatest (lsd xs))
            → (¬gapped : ¬ (Gapped xs proper))
            → NextView (suc b) (suc d) o xs proper

    nextView : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → NextView (suc b) (suc d) o xs proper
    nextView {b} {d} {o} xs proper with Greatest? (lsd xs)
    nextView {b} {d} {o} xs proper | yes greatest with Gapped? xs proper
    nextView {b} {d} {o} xs proper | yes greatest | yes gapped = GappedEndpoint  b d o greatest gapped
    nextView {b} {d} {o} xs proper | yes greatest | no ¬gapped = UngappedEndpoint b d o greatest ¬gapped
    nextView {b} {d} {o} xs proper | no ¬greatest = Interval b d o ¬greatest

    next-numeral-Proper-Interval : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (¬greatest : ¬ (Greatest (lsd xs)))
        → (proper : 2 ≤ suc (d + o))
        → Numeral (suc b) (suc d) o
    next-numeral-Proper-Interval (x ∙)    ¬greatest proper = digit+1 x ¬greatest ∙
    next-numeral-Proper-Interval (x ∷ xs) ¬greatest proper = digit+1 x ¬greatest ∷ xs

    next-numeral-Proper-GappedEndpoint : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → (gapped : Gapped xs proper)
        → Numeral (suc b) (suc d) o
    next-numeral-Proper-GappedEndpoint {b} {d} {o} (x ∙)    proper gapped = z ∷ carry-digit d o proper ∙
    next-numeral-Proper-GappedEndpoint {b} {d} {o} (x ∷ xs) proper gapped = z ∷ next-numeral-Proper xs proper

    next-numeral-Proper-UngappedEndpoint : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (greatest : Greatest (lsd xs))
        → (proper : 2 ≤ suc (d + o))
        → (¬gapped : ¬ (Gapped xs proper))
        → Numeral (suc b) (suc d) o
    next-numeral-Proper-UngappedEndpoint {b} {d} {o} (x ∙) greatest proper gapped
        = digit+1-n x greatest (carry o * suc b) lower-bound ∷ carry-digit d o proper ∙
        where
            lower-bound : carry o * suc b > 0
            lower-bound =
                start
                    1
                ≤⟨ m≤m*1+n 1 b ⟩
                    1 * suc b
                ≤⟨ *n-mono (suc b) (m≤m⊔n 1 o) ⟩
                    carry o * suc b
                □

    next-numeral-Proper-UngappedEndpoint {b} {d} {o} (x ∷ xs) greatest proper gapped
        = digit+1-n x greatest gap lower-bound ∷ next-xs
        where
            next-xs : Numeral (suc b) (suc d) o
            next-xs = next-numeral-Proper xs proper

            gap : ℕ
            gap = (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b

            lower-bound : gap > 0
            lower-bound =
                start
                    1
                ≤⟨ m≤m*1+n 1 b ⟩
                    1 * suc b
                ≤⟨ *n-mono (suc b) (m≥n+o⇒m∸o≥n ⟦ next-xs ⟧ 1 ⟦ xs ⟧ (next-numeral-is-greater-Proper xs proper)) ⟩
                    (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
                □

    next-numeral-Proper : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → Numeral (suc b) (suc d) o
    next-numeral-Proper xs proper with nextView xs proper
    next-numeral-Proper xs proper | Interval b d o ¬greatest
        = next-numeral-Proper-Interval xs ¬greatest proper
    next-numeral-Proper xs proper | GappedEndpoint b d o greatest gapped
        = next-numeral-Proper-GappedEndpoint xs proper gapped
    next-numeral-Proper xs proper | UngappedEndpoint b d o greatest ¬gapped
        = next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped

    next-numeral-Proper-Interval-lemma : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (¬greatest : ¬ (Greatest (lsd xs)))
        → (proper : 2 ≤ suc (d + o))
        → ⟦ next-numeral-Proper-Interval xs ¬greatest proper ⟧ ≡ suc ⟦ xs ⟧
    next-numeral-Proper-Interval-lemma {b} {d} {o} (x ∙) ¬greatest proper =
        -- ⟦ digit+1 x ¬greatest ∙ ⟧ ≡ suc ⟦ x ∙ ⟧
        begin
            Digit-toℕ (digit+1 x ¬greatest) o
        ≡⟨ digit+1-toℕ x ¬greatest ⟩
            suc (Digit-toℕ x o)
        ∎
    next-numeral-Proper-Interval-lemma {b} {d} {o} (x ∷ xs) ¬greatest proper =
    -- ⟦ digit+1 x ¬greatest ∷ xs ⟧ ≡ suc ⟦ x ∷ xs ⟧
        begin
            Digit-toℕ (digit+1 x ¬greatest) o + ⟦ xs ⟧ * suc b
        ≡⟨ cong (λ w → w + ⟦ xs ⟧ * suc b) (digit+1-toℕ x ¬greatest) ⟩
            suc (Digit-toℕ x o) + ⟦ xs ⟧ * suc b
        ∎

    next-numeral-Proper-GappedEndpoint-lemma : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (greatest : Greatest (lsd xs))
        → (proper : 2 ≤ suc (d + o))
        → (gapped : Gapped xs proper)
        → ⟦ next-numeral-Proper-GappedEndpoint xs proper gapped ⟧ > suc ⟦ xs ⟧
    next-numeral-Proper-GappedEndpoint-lemma {b} {d} {o} (x ∙) greatest proper gapped =
        -- ⟦ z ∷ carry-digit d o proper ∙ ⟧ > suc ⟦ x ∙ ⟧
        start
            suc (suc (Fin.toℕ x + o))
        ≈⟨ cong (λ w → suc w + o) greatest ⟩
            suc (suc d) + o
        ≈⟨ +-comm (suc (suc d)) o ⟩
            o + suc (suc d)
        ≤⟨ n+-mono o gapped ⟩
            o + carry o * suc b
        ≈⟨ cong (λ w → o + w * suc b) (sym (carry-digit-toℕ d o proper)) ⟩
            o + (Digit-toℕ (carry-digit d o proper) o) * suc b
        □
    next-numeral-Proper-GappedEndpoint-lemma {b} {d} {o} (x ∷ xs) greatest proper gapped
        = proof
        where
            next-xs : Numeral (suc b) (suc d) o
            next-xs = next-numeral-Proper xs proper

            next-xs>xs : ⟦ next-xs ⟧ > ⟦ xs ⟧
            next-xs>xs = next-numeral-is-greater-Proper xs proper

            next : Numeral (suc b) (suc d) o
            next = z ∷ next-xs

            -- ⟦ z ∷ next-numeral-Proper xs (Maximum-Proper xs proper) proper ⟧ > suc ⟦ x ∷ xs ⟧
            proof : ⟦ next ⟧ > suc ⟦ x ∷ xs ⟧
            proof = start
                    suc (suc (Digit-toℕ x o)) + ⟦ xs ⟧ * suc b
                ≈⟨ cong (λ w → suc (suc w) + ⟦ xs ⟧ * suc b) (greatest-digit-toℕ x greatest) ⟩
                    suc (suc d) + o + ⟦ xs ⟧ * suc b
                ≈⟨ +-assoc (suc (suc d)) o (⟦ xs ⟧ * suc b) ⟩
                    suc (suc d) + (o + ⟦ xs ⟧ * suc b)
                ≈⟨ a+[b+c]≡b+[a+c] (suc (suc d)) o (⟦ xs ⟧ * suc b) ⟩
                    o + (suc (suc d) + ⟦ xs ⟧ * suc b)
                ≤⟨ n+-mono o (+n-mono (⟦ xs ⟧ * suc b) gapped) ⟩
                    o + ((⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b + ⟦ xs ⟧ * suc b)
                ≈⟨ cong (λ w → o + w) (sym (distribʳ-*-+ (suc b) (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) ⟦ xs ⟧)) ⟩
                    o + (⟦ next-xs ⟧ ∸ ⟦ xs ⟧ + ⟦ xs ⟧) * suc b
                ≈⟨ cong (λ w → o + w * suc b) (m∸n+n≡m (<⇒≤ next-xs>xs)) ⟩
                    o + ⟦ next-xs ⟧ * suc b
                ≈⟨ refl ⟩
                    ⟦ z ∷ next-xs ⟧
                □

    next-numeral-Proper-UngappedEndpoint-lemma : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (greatest : Greatest (lsd xs))
        → (proper : 2 ≤ suc (d + o))
        → (¬gapped : ¬ (Gapped xs proper))
        → ⟦ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped ⟧ ≡ suc ⟦ xs ⟧
    next-numeral-Proper-UngappedEndpoint-lemma {b} {d} {o} (x ∙) greatest proper ¬gapped = proof
        -- ⟦ digit+1-n x greatest (carry o * suc b) lower-bound ∷ carry-digit d o proper ∙ ⟧ ≡ suc ⟦ x ∙ ⟧
        where
            lower-bound : carry o * suc b > 0
            lower-bound =
                start
                    1
                ≤⟨ m≤m*1+n 1 b ⟩
                    1 * suc b
                ≤⟨ *n-mono (suc b) (m≤m⊔n 1 o) ⟩
                    carry o * suc b
                □

            upper-bound : carry o * suc b ≤ suc d
            upper-bound = ≤-pred $ ≰⇒> ¬gapped

            upper-bound' : carry o * suc b ≤ suc (Fin.toℕ x + o)
            upper-bound' = start
                    carry o * suc b
                ≤⟨ upper-bound ⟩
                    suc d
                ≈⟨ sym greatest ⟩
                    suc (Fin.toℕ x)
                ≤⟨ m≤m+n (suc (Fin.toℕ x)) o ⟩
                    suc (Fin.toℕ x + o)
                □

            next : Numeral (suc b) (suc d) o
            next = digit+1-n x greatest (carry o * suc b) lower-bound ∷ carry-digit d o proper ∙

            proof : ⟦ next ⟧ ≡ suc (Digit-toℕ x o)
            proof =
                begin
                    Digit-toℕ (digit+1-n x greatest (carry o * suc b) lower-bound) o + Digit-toℕ (carry-digit d o proper) o * suc b
                ≡⟨ cong (λ w → Digit-toℕ (digit+1-n x greatest (carry o * suc b) lower-bound) o + w * suc b) (carry-digit-toℕ d o proper) ⟩
                    Digit-toℕ (digit+1-n x greatest (carry o * suc b) lower-bound) o + carry o * suc b
                ≡⟨ cong (λ w → w + carry o * suc b) (digit+1-n-toℕ x greatest (carry o * suc b) lower-bound upper-bound) ⟩
                    suc (Fin.toℕ x + o) ∸ carry o * suc b + carry o * suc b
                ≡⟨ m∸n+n≡m upper-bound' ⟩
                    suc (Digit-toℕ x o)
                ∎
    next-numeral-Proper-UngappedEndpoint-lemma {b} {d} {o} (x ∷ xs) greatest proper ¬gapped = proof
        -- ⟦ digit+1-n x greatest gap gap>0 ∷ next ∙ ⟧ ≡ suc ⟦ x ∷ xs ⟧
        where
            ¬max-xs : ¬ (Maximum xs)
            ¬max-xs = Maximum-Proper xs proper

            next-xs : Numeral (suc b) (suc d) o
            next-xs = next-numeral-Proper xs proper

            lower-bound : (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b > 0
            lower-bound =
                start
                    1
                ≤⟨ m≤m*1+n 1 b ⟩
                    1 * suc b
                ≤⟨ *n-mono (suc b) (m≥n+o⇒m∸o≥n ⟦ next-xs ⟧ 1 ⟦ xs ⟧ (next-numeral-is-greater-Proper xs proper)) ⟩
                    (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
                □

            upper-bound : (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b ≤ suc d
            upper-bound = ≤-pred $ ≰⇒> ¬gapped

            next : Numeral (suc b) (suc d) o
            next = digit+1-n x greatest ((⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b) lower-bound ∷ next-xs

            ⟦next-xs⟧>⟦xs⟧ : ⟦ next-xs ⟧ > ⟦ xs ⟧
            ⟦next-xs⟧>⟦xs⟧ = next-numeral-is-greater-Proper xs proper

            upper-bound' : ⟦ next-xs ⟧ * suc b ∸ ⟦ xs ⟧ * suc b ≤ suc (Digit-toℕ x o)
            upper-bound' =
                start
                    ⟦ next-xs ⟧ * suc b ∸ ⟦ xs ⟧ * suc b
                ≈⟨ sym (*-distrib-∸ʳ (suc b) ⟦ next-xs ⟧ ⟦ xs ⟧) ⟩
                    (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
                ≤⟨ upper-bound ⟩
                    suc d
                ≤⟨ m≤m+n (suc d) o ⟩
                    suc d + o
                ≈⟨ cong (λ w → w + o) (sym greatest) ⟩
                    suc (Digit-toℕ x o)
                □

            proof : ⟦ next ⟧ ≡ suc ⟦ x ∷ xs ⟧
            proof =
                begin
                    ⟦ next ⟧
                ≡⟨ cong (λ w → w + ⟦ next-xs ⟧ * suc b) (digit+1-n-toℕ x greatest ((⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b) lower-bound upper-bound) ⟩
                    suc (Digit-toℕ x o) ∸ (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b + ⟦ next-xs ⟧ * suc b
                ≡⟨ cong (λ w → suc (Digit-toℕ x o) ∸ w + ⟦ next-xs ⟧ * suc b) (*-distrib-∸ʳ (suc b) ⟦ next-xs ⟧ ⟦ xs ⟧) ⟩
                    suc (Digit-toℕ x o) ∸ (⟦ next-xs ⟧ * suc b ∸ ⟦ xs ⟧ * suc b) + ⟦ next-xs ⟧ * suc b
                ≡⟨ m∸[o∸n]+o≡m+n (suc (Digit-toℕ x o)) (⟦ xs ⟧ * suc b) (⟦ next-xs ⟧ * suc b) (*n-mono (suc b) (<⇒≤ ⟦next-xs⟧>⟦xs⟧)) upper-bound' ⟩
                    suc ⟦ x ∷ xs ⟧
                ∎

    next-numeral-is-greater-Proper : ∀ {b d o}
        → (xs : Numeral (suc b) (suc d) o)
        → (proper : 2 ≤ suc (d + o))
        → ⟦ next-numeral-Proper xs proper ⟧ > ⟦ xs ⟧
    next-numeral-is-greater-Proper xs proper with nextView xs proper
    next-numeral-is-greater-Proper xs proper | Interval b d o ¬greatest =
        start
            suc ⟦ xs ⟧
        ≈⟨ sym (next-numeral-Proper-Interval-lemma xs ¬greatest proper) ⟩
            ⟦ next-numeral-Proper-Interval xs ¬greatest proper ⟧
        □
    next-numeral-is-greater-Proper xs proper | GappedEndpoint b d o greatest gapped =
        start
            suc ⟦ xs ⟧
        ≤⟨ n≤1+n (suc ⟦ xs ⟧) ⟩
            suc (suc ⟦ xs ⟧)
        ≤⟨ next-numeral-Proper-GappedEndpoint-lemma xs greatest proper gapped ⟩
            ⟦ next-numeral-Proper-GappedEndpoint xs proper gapped ⟧
        □
    next-numeral-is-greater-Proper xs proper | UngappedEndpoint b d o greatest ¬gapped =
        start
            suc ⟦ xs ⟧
        ≈⟨ sym (next-numeral-Proper-UngappedEndpoint-lemma xs greatest proper ¬gapped) ⟩
            ⟦ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped ⟧
        □

-- gap : ∀ {b d o}
--     → (xs : Numeral (suc b) (suc d) o)
--     → (proper : 2 ≤ suc (d + o))
--     → ℕ
-- gap {b} {d} {o} (x ∙)    proper = carry o                * suc b
-- gap {b} {d} {o} (x ∷ xs) proper = (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
--     where
--         next-xs : Numeral (suc b) (suc d) o
--         next-xs = next-numeral-Proper xs proper
--
-- gap>0 : ∀ {b d o}
--     → (xs : Numeral (suc b) (suc d) o)
--     → (proper : 2 ≤ suc (d + o))
--     → gap xs proper > 0
-- gap>0 {b} {d} {o} (x ∙)    proper =
--     start
--         1
--     ≤⟨ m≤m*1+n 1 b ⟩
--         1 * suc b
--     ≤⟨ *n-mono (suc b) (m≤m⊔n 1 o) ⟩
--         carry o * suc b
--     □
-- gap>0 {b} {d} {o} (x ∷ xs) proper =
--     start
--         1
--     ≤⟨ m≤m*1+n 1 b ⟩
--         1 * suc b
--     ≤⟨ *n-mono (suc b) (m≥n+o⇒m∸o≥n ⟦ next-xs ⟧ 1 ⟦ xs ⟧ (next-numeral-is-greater-Proper xs proper)) ⟩
--         (⟦ next-xs ⟧ ∸ ⟦ xs ⟧) * suc b
--     □
--     where
--         next-xs : Numeral (suc b) (suc d) o
--         next-xs = next-numeral-Proper xs proper
--------------------------------------------------------------------------------
-- Properties of next-numeral on Proper Numbers
--------------------------------------------------------------------------------

next-numeral-Proper-refine-target : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → NextView (suc b) (suc d) o xs proper
    → Set
next-numeral-Proper-refine-target xs proper (Interval b d o ¬greatest) = next-numeral-Proper xs proper ≡ next-numeral-Proper-Interval xs ¬greatest proper
next-numeral-Proper-refine-target xs proper (GappedEndpoint b d o greatest gapped) = next-numeral-Proper xs proper ≡ next-numeral-Proper-GappedEndpoint xs proper gapped
next-numeral-Proper-refine-target xs proper (UngappedEndpoint b d o greatest ¬gapped) = next-numeral-Proper xs proper ≡ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped

next-numeral-Proper-refine : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → (view : NextView (suc b) (suc d) o xs proper)
    → next-numeral-Proper-refine-target xs proper view
next-numeral-Proper-refine xs proper (Interval b d o ¬greatest) with nextView xs proper
next-numeral-Proper-refine xs proper (Interval b d o ¬greatest) | Interval _ _ _ _ = refl
next-numeral-Proper-refine xs proper (Interval b d o ¬greatest) | GappedEndpoint _ _ _ greatest _ = contradiction greatest ¬greatest
next-numeral-Proper-refine xs proper (Interval b d o ¬greatest) | UngappedEndpoint _ _ _ greatest _ = contradiction greatest ¬greatest
next-numeral-Proper-refine xs proper (GappedEndpoint b d o greatest gapped) with nextView xs proper
next-numeral-Proper-refine xs proper (GappedEndpoint b d o greatest gapped) | Interval _ _ _ ¬greatest = contradiction greatest ¬greatest
next-numeral-Proper-refine xs proper (GappedEndpoint b d o greatest gapped) | GappedEndpoint _ _ _ _ _ = refl
next-numeral-Proper-refine xs proper (GappedEndpoint b d o greatest gapped) | UngappedEndpoint _ _ _ _ ¬gapped = contradiction gapped ¬gapped
next-numeral-Proper-refine xs proper (UngappedEndpoint b d o greatest ¬gapped) with nextView xs proper
next-numeral-Proper-refine xs proper (UngappedEndpoint b d o greatest ¬gapped) | Interval _ _ _ ¬greatest = contradiction greatest ¬greatest
next-numeral-Proper-refine xs proper (UngappedEndpoint b d o greatest ¬gapped) | GappedEndpoint _ _ _ _ gapped = contradiction gapped ¬gapped
next-numeral-Proper-refine xs proper (UngappedEndpoint b d o greatest ¬gapped) | UngappedEndpoint _ _ _ _ _ = refl

--------------------------------------------------------------------------------
-- next-numeral-is-immediate-Proper
--------------------------------------------------------------------------------

next-numeral-is-immediate-Proper : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (ys : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → ⟦ ys ⟧ > ⟦ xs ⟧
    → ⟦ ys ⟧ ≥ ⟦ next-numeral-Proper xs proper ⟧
next-numeral-is-immediate-Proper xs ys proper prop with nextView xs proper
next-numeral-is-immediate-Proper xs ys proper prop | Interval b d o ¬greatest =
    start
        ⟦ next-numeral-Proper-Interval xs ¬greatest proper ⟧
    ≈⟨ next-numeral-Proper-Interval-lemma xs ¬greatest proper ⟩
        suc ⟦ xs ⟧
    ≤⟨ prop ⟩
        ⟦ ys ⟧
    □
next-numeral-is-immediate-Proper xs (y ∙) proper prop | GappedEndpoint b d o greatest gapped
    = contradiction prop $ >⇒≰ $
        start
            suc (Digit-toℕ y o)
        ≤⟨ s≤s (greatest-of-all o (lsd xs) y greatest) ⟩
            suc (Digit-toℕ (lsd xs) o)
        ≤⟨ s≤s (lsd-toℕ xs) ⟩
            suc ⟦ xs ⟧
        □
next-numeral-is-immediate-Proper (x ∙) (y ∷ ys) proper prop | GappedEndpoint b d o greatest gapped =
    start
        o + (Digit-toℕ (carry-digit d o proper) o) * suc b
    ≈⟨ cong (λ w → o + w * suc b) (carry-digit-toℕ d o proper) ⟩
        o + carry o * suc b
    ≤⟨ n+-mono o (*n-mono (suc b) ys-lower-bound) ⟩
        o + ⟦ ys ⟧ * suc b
    ≤⟨ +n-mono (⟦ ys ⟧ * suc b) (n≤m+n (Fin.toℕ y) o) ⟩
        Digit-toℕ y o + ⟦ ys ⟧ * suc b
    □
    where
        ≥carry : ∀ {b d o}
            → (xs : Numeral (suc b) (suc d) o)
            → (proper : 2 ≤ suc (d + o))
            → ⟦ xs ⟧ > 0
            → ⟦ xs ⟧ ≥ carry o
        ≥carry {_} {_} {zero}  xs proper prop = prop
        ≥carry {_} {_} {suc o} (x ∙) proper prop = n≤m+n (Fin.toℕ x) (suc o)
        ≥carry {b} {_} {suc o} (x ∷ xs) proper prop =
            start
                suc o
            ≤⟨ n≤m+n (Fin.toℕ x) (suc o) ⟩
                Fin.toℕ x + suc o
            ≤⟨ m≤m+n (Fin.toℕ x + suc o) (⟦ xs ⟧ * suc b) ⟩
                Fin.toℕ x + suc o + ⟦ xs ⟧ * suc b
            □

        ys-lower-bound : ⟦ ys ⟧ ≥ carry o
        ys-lower-bound = ≥carry ys proper (tail-mono-strict-Null x y ys greatest prop)

next-numeral-is-immediate-Proper (x ∷ xs) (y ∷ ys) proper prop | GappedEndpoint b d o greatest gapped =
    start
        o + ⟦ next-xs ⟧ * suc b
    ≤⟨ n+-mono o (*n-mono (suc b) ⟦next-xs⟧≤⟦ys⟧) ⟩
        o + ⟦ ys ⟧ * suc b
    ≤⟨ +n-mono (⟦ ys ⟧ * suc b) (n≤m+n (Fin.toℕ y) o) ⟩
        Digit-toℕ y o + ⟦ ys ⟧ * suc b
    □
    where
        next-xs : Numeral (suc b) (suc d) o
        next-xs = next-numeral-Proper xs proper

        ⟦xs⟧<⟦ys⟧ : ⟦ xs ⟧ < ⟦ ys ⟧
        ⟦xs⟧<⟦ys⟧ = tail-mono-strict x xs y ys greatest prop

        ⟦next-xs⟧≤⟦ys⟧ : ⟦ next-xs ⟧ ≤ ⟦ ys ⟧
        ⟦next-xs⟧≤⟦ys⟧ = next-numeral-is-immediate-Proper xs ys proper ⟦xs⟧<⟦ys⟧

next-numeral-is-immediate-Proper xs ys proper prop | UngappedEndpoint b d o greatest ¬gapped =
    start
        ⟦ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped ⟧
    ≈⟨ next-numeral-Proper-UngappedEndpoint-lemma xs greatest proper ¬gapped ⟩
        suc ⟦ xs ⟧
    ≤⟨ prop ⟩
        ⟦ ys ⟧
    □

--------------------------------------------------------------------------------
-- next-numeral
--------------------------------------------------------------------------------

next-numeral : ∀ {b d o}
    → (xs : Numeral b d o)
    → ¬ (Maximum xs)
    → Numeral b d o
next-numeral {b} {d} {o} xs ¬max with numView b d o
next-numeral xs ¬max | NullBase d o = next-numeral-NullBase xs ¬max
next-numeral xs ¬max | NoDigits b o = NoDigits-explode xs
next-numeral xs ¬max | AllZeros b   = contradiction (Maximum-AllZeros xs) ¬max
next-numeral xs ¬max | Proper b d o proper = next-numeral-Proper xs proper

--------------------------------------------------------------------------------
-- next-numeral-is-greater
--------------------------------------------------------------------------------

next-numeral-is-greater : ∀ {b d o}
    → (xs : Numeral b d o)
    → (¬max : ¬ (Maximum xs))
    → ⟦ next-numeral xs ¬max ⟧ > ⟦ xs ⟧
next-numeral-is-greater {b} {d} {o} xs ¬max with numView b d o
next-numeral-is-greater xs ¬max | NullBase d o = next-numeral-is-greater-NullBase xs ¬max
next-numeral-is-greater xs ¬max | NoDigits b o = NoDigits-explode xs
next-numeral-is-greater xs ¬max | AllZeros b   = contradiction (Maximum-AllZeros xs) ¬max
next-numeral-is-greater xs ¬max | Proper b d o proper = next-numeral-is-greater-Proper xs proper

--------------------------------------------------------------------------------
-- next-numeral-is-immediate
--------------------------------------------------------------------------------

next-numeral-is-immediate : ∀ {b d o}
    → (xs : Numeral b d o)
    → (ys : Numeral b d o)
    → (¬max : ¬ (Maximum xs))
    → ⟦ ys ⟧ > ⟦ xs ⟧
    → ⟦ ys ⟧ ≥ ⟦ next-numeral xs ¬max ⟧
next-numeral-is-immediate {b} {d} {o} xs ys ¬max prop with numView b d o
next-numeral-is-immediate xs ys ¬max prop | NullBase d o = next-numeral-is-immediate-NullBase xs ys ¬max prop
next-numeral-is-immediate xs ys ¬max prop | NoDigits b o = NoDigits-explode xs
next-numeral-is-immediate xs ys ¬max prop | AllZeros b = contradiction (Maximum-AllZeros xs) ¬max
next-numeral-is-immediate xs ys ¬max prop | Proper b d o proper = next-numeral-is-immediate-Proper xs ys proper prop

--------------------------------------------------------------------------------
-- properties of the gaps
--------------------------------------------------------------------------------

Gapped#N⇒Gapped#0 : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → Gapped#N b d o xs proper
    → Gapped#0 b d o
Gapped#N⇒Gapped#0 xs proper gapped#N with nextView xs proper
Gapped#N⇒Gapped#0 xs proper gapped#N | Interval b d o ¬greatest =
    start
        suc (suc d)
    ≤⟨ gapped#N ⟩
        (⟦ next-numeral-Proper-Interval xs ¬greatest proper ⟧ ∸ ⟦ xs ⟧) * suc b
    ≤⟨ *n-mono (suc b) $
        start
            ⟦ next-numeral-Proper-Interval xs ¬greatest proper ⟧ ∸ ⟦ xs ⟧
        ≈⟨ cong (λ w → w ∸ ⟦ xs ⟧) (next-numeral-Proper-Interval-lemma xs ¬greatest proper) ⟩
            suc ⟦ xs ⟧ ∸ ⟦ xs ⟧
        ≈⟨ m+n∸n≡m (suc zero) ⟦ xs ⟧ ⟩
            suc zero
        ≤⟨ m≤m⊔n 1 o ⟩
            suc zero ⊔ o
        □
     ⟩
        (suc zero ⊔ o) * suc b
    □
Gapped#N⇒Gapped#0 (x ∙)    proper gapped#N | GappedEndpoint b d o greatest gapped#0 = gapped#0
Gapped#N⇒Gapped#0 (x ∷ xs) proper _        | GappedEndpoint b d o greatest gapped#N = Gapped#N⇒Gapped#0 xs proper gapped#N
Gapped#N⇒Gapped#0 xs proper gapped#N | UngappedEndpoint b d o greatest ¬gapped =
        start
            suc (suc d)
        ≤⟨ gapped#N ⟩
            (⟦ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped ⟧ ∸ ⟦ xs ⟧) * suc b
        ≤⟨ *n-mono (suc b) $
            start
                ⟦ next-numeral-Proper-UngappedEndpoint xs greatest proper ¬gapped ⟧ ∸ ⟦ xs ⟧
            ≈⟨ cong (λ w → w ∸ ⟦ xs ⟧) (next-numeral-Proper-UngappedEndpoint-lemma xs greatest proper ¬gapped) ⟩
                suc ⟦ xs ⟧ ∸ ⟦ xs ⟧
            ≈⟨ m+n∸n≡m (suc zero) ⟦ xs ⟧ ⟩
                suc zero
            ≤⟨ m≤m⊔n 1 o ⟩
                suc zero ⊔ o
            □
         ⟩
            (suc zero ⊔ o) * suc b
        □

-- ¬Gapped#0⇒¬Gapped#N : ∀ {b d o}
--     → (xs : Numeral (suc b) (suc d) o)
--     → (proper : 2 ≤ suc (d + o))
--     → ¬ (Gapped#0 b d o)
--     → ¬ (Gapped#N b d o xs proper)
-- ¬Gapped#0⇒¬Gapped#N xs proper ¬Gapped#0 = contraposition (Gapped#N⇒Gapped#0 xs proper) ¬Gapped#0

¬Gapped#0⇒¬Gapped : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → ¬ (Gapped#0 b d o)
    → ¬ (Gapped xs proper)
¬Gapped#0⇒¬Gapped (x ∙)    proper ¬Gapped#0 = ¬Gapped#0
¬Gapped#0⇒¬Gapped (x ∷ xs) proper ¬Gapped#0 = contraposition
    (Gapped#N⇒Gapped#0 xs proper)
    ¬Gapped#0

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module #14 where

{-
  Why do the induction principles for identity types not allow us to construct a
  function f : ∏(x:A) ∏(p:x=x) (p = refl[x]) with the defining equation
              f(x,refl[x]) :≡ refl[refl[x]]   ?
-}

{-
  To use induction here we need proof that refl x ≡ p then use refl as a relation to prove
  that refl x ≡ p again.  It's a circular construction.
-}

open import Relation.Binary.PropositionalEquality

{- Closest I could get this into Agda.  Does not compile.
f : {A : Set} → (x : A) → (p : x ≡ x) → p ≡ refl x
f x (refl x) = refl (refl x)
-}

ext: agda

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Generic.Test where

import Generic.Test.Data
import Generic.Test.DeriveEq
import Generic.Test.Elim
import Generic.Test.Eq
import Generic.Test.Experiment
import Generic.Test.ReadData
import Generic.Test.Reify

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Pi-.Category where
open import Relation.Binary.PropositionalEquality
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided
open import Categories.Category.Monoidal.Symmetric
open import Categories.Category.Monoidal.Rigid
open import Categories.Category.Monoidal.CompactClosed
open import Categories.Functor.Bifunctor
open import Categories.Category
open import Categories.Category.Inverse
open import Categories.Category.Product
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Relation.Nullary
open import Base
open import Pi-.Syntax
open import Pi-.Opsem
open import Pi-.Eval
open import Pi-.NoRepeat
open import Pi-.Interp
open import Pi-.Properties
open import Pi-.Invariants
open import Pi-.Examples

Pi- : Category _ _ _
Pi- = record {
      Obj = 𝕌
    ; _⇒_ = _↔_
    ; _≈_ = λ c₁ c₂ → eval c₁ ∼ eval c₂
    ; id = id↔
    ; _∘_ = λ f g → g ⨾ f

    ; assoc = assoc
    ; sym-assoc = λ x → sym (assoc x)
    ; identityˡ = identityˡ _
    ; identityʳ = identityʳ _
    ; identity² = λ {(v ⃗) → refl ; (v ⃖) → refl}
    ; equiv = record { refl = λ a → refl
                     ; sym = λ f~g a → sym (f~g a)
                     ; trans = λ f~g g~h a → trans (f~g a) (g~h a) }
    ; ∘-resp-≈ = ∘-resp-≈
    }
  where
  identityˡ : ∀ {A B} (c : A ↔ B) (v : Val A B) → eval (c ⨾ id↔) v ≡ eval c v
  identityˡ c v rewrite eval≡interp (c ⨾ id↔) v | eval≡interp c v = lem c v
    where
    lem : ∀ {A B} (c : A ↔ B) (v : Val A B) → interp (c ⨾ id↔) v ≡ interp c v
    lem c (x ⃗) with interp c (x ⃗)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl
    lem c (x ⃖) with interp c (x ⃖)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl

  identityʳ : ∀ {A B} (c : A ↔ B) (v : Val A B) → eval (id↔ ⨾ c) v ≡ eval c v
  identityʳ c v rewrite eval≡interp (id↔ ⨾ c) v | eval≡interp c v = lem c v
    where
    lem : ∀ {A B} (c : A ↔ B) (v : Val A B) → interp (id↔ ⨾ c) v ≡ interp c v
    lem c (x ⃗) with interp c (x ⃗)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl
    lem c (x ⃖) with interp c (x ⃖)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl

Pi-Monoidal : Monoidal Pi-
Pi-Monoidal = record {
              ⊗ = record { F₀ = λ {(A , B) → A +ᵤ B}
                         ; F₁ = λ {(c₁ , c₂) → c₁ ⊕ c₂ }
                         ; identity = λ { (inj₁ v ⃗) → refl
                                        ; (inj₂ v ⃗) → refl
                                        ; (inj₁ v ⃖) → refl
                                        ; (inj₂ v ⃖) → refl}
                         ; homomorphism = homomorphism
                         ; F-resp-≈ = λ {(A , B)} {(C , D)} {(f , g)} {(f' , g')} (f~f' , g~g')
                                        → F-resp-≈ f f' g g' f~f' g~g'}
            ; unit = 𝟘
            ; unitorˡ = record { from = unite₊l
                               ; to = uniti₊l
                               ; iso = record { isoˡ = λ { (inj₂ v ⃗) → refl
                                                         ; (inj₂ v ⃖) → refl}
                                              ; isoʳ = λ { (v ⃗) → refl
                                                         ; (v ⃖) → refl}}}
            ; unitorʳ = record { from = unite₊r
                               ; to = uniti₊r
                               ; iso = record { isoˡ = λ { (inj₁ v ⃗) → refl
                                                         ; (inj₁ v ⃖) → refl}
                                              ; isoʳ = λ { (v ⃗) → refl
                                                         ; (v ⃖) → refl}}}
            ; associator = record { from = assocr₊
                                  ; to = assocl₊
                                  ; iso = record { isoˡ = λ { (inj₁ (inj₁ v) ⃗) → refl
                                                            ; (inj₁ (inj₂ v) ⃗) → refl
                                                            ; (inj₂ v ⃗) → refl
                                                            ; (inj₁ (inj₁ v) ⃖) → refl
                                                            ; (inj₁ (inj₂ v) ⃖) → refl
                                                            ; (inj₂ v ⃖) → refl}
                                                 ; isoʳ = λ { (inj₁ v ⃗) → refl
                                                            ; (inj₂ (inj₁ v) ⃗) → refl
                                                            ; (inj₂ (inj₂ v) ⃗) → refl
                                                            ; (inj₁ v ⃖) → refl
                                                            ; (inj₂ (inj₁ v) ⃖) → refl
                                                            ; (inj₂ (inj₂ v) ⃖) → refl}}}
            ; unitorˡ-commute-from = unitorˡ-commute-from _
            ; unitorˡ-commute-to = unitorˡ-commute-to _
            ; unitorʳ-commute-from = unitorʳ-commute-from _
            ; unitorʳ-commute-to = unitorʳ-commute-to _
            ; assoc-commute-from = assoc-commute-from _ _ _
            ; assoc-commute-to = assoc-commute-to _ _ _
            ; triangle = λ { (inj₁ (inj₁ v) ⃗) → refl
                           ; (inj₂ v ⃗) → refl
                           ; (inj₁ v ⃖) → refl
                           ; (inj₂ v ⃖) → refl}
            ; pentagon = λ { (inj₁ (inj₁ (inj₁ v)) ⃗) → refl
                           ; (inj₁ (inj₁ (inj₂ v)) ⃗) → refl
                           ; (inj₁ (inj₂ v) ⃗) → refl
                           ; (inj₂ v ⃗) → refl
                           ; (inj₁ v ⃖) → refl
                           ; (inj₂ (inj₁ v) ⃖) → refl
                           ; (inj₂ (inj₂ (inj₁ v)) ⃖) → refl
                           ; (inj₂ (inj₂ (inj₂ v)) ⃖) → refl}
            }
  where
  F-resp-≈ : ∀ {A B C D} (f f' : A ↔ B) (g g' : C ↔ D) → (eval f ∼ eval f') → (eval g ∼ eval g')
           → (eval (f ⊕ g) ∼ eval (f' ⊕ g'))
  F-resp-≈ f f' g g' f~f' g~g' x rewrite eval≡interp (f ⊕ g) x | eval≡interp (f' ⊕ g') x =
    lem f f' g g' (λ x → trans (sym (eval≡interp f x)) (trans (f~f' x) (eval≡interp f' x)))
                  (λ x → trans (sym (eval≡interp g x)) (trans (g~g' x) (eval≡interp g' x))) x
    where
    lem : ∀ {A B C D} (f f' : A ↔ B) (g g' : C ↔ D) → (interp f ∼ interp f') → (interp g ∼ interp g')
        → (interp (f ⊕ g) ∼ interp (f' ⊕ g'))
    lem f f' g g' f~f' g~g' (inj₁ x ⃗) with f~f' (x ⃗) | interp f' (x ⃗) | inspect (interp f') (x ⃗)
    ... | eq | x' ⃗ | [ eq' ] rewrite eq | eq' = refl
    ... | eq | x' ⃖ | [ eq' ] rewrite eq | eq' = refl
    lem f f' g g' f~f' g~g' (inj₂ y ⃗) with g~g' (y ⃗) | interp g' (y ⃗) | inspect (interp g') (y ⃗)
    ... | eq | y' ⃗ | [ eq' ] rewrite eq | eq' = refl
    ... | eq | y' ⃖ | [ eq' ] rewrite eq | eq' = refl
    lem f f' g g' f~f' g~g' (inj₁ x ⃖) with f~f' (x ⃖) | interp f' (x ⃖) | inspect (interp f') (x ⃖)
    ... | eq | x' ⃗ | [ eq' ] rewrite eq | eq' = refl
    ... | eq | x' ⃖ | [ eq' ] rewrite eq | eq' = refl
    lem f f' g g' f~f' g~g' (inj₂ y ⃖) with g~g' (y ⃖) | interp g' (y ⃖) | inspect (interp g') (y ⃖)
    ... | eq | y' ⃗ | [ eq' ] rewrite eq | eq' = refl
    ... | eq | y' ⃖ | [ eq' ] rewrite eq | eq' = refl

  unitorˡ-commute-from : ∀ {A B} (f : A ↔ B) (x : _) → eval ((id↔ ⊕ f) ⨾ unite₊l) x ≡ eval (unite₊l ⨾ f) x
  unitorˡ-commute-from f x rewrite eval≡interp ((id↔ ⊕ f) ⨾ unite₊l) x | eval≡interp (unite₊l ⨾ f) x = lem f x
    where
    lem : ∀ {A B} (f : A ↔ B) (x : _) → interp ((id↔ ⊕ f) ⨾ unite₊l) x ≡ interp (unite₊l ⨾ f) x
    lem f (inj₂ y ⃗) with interp f (y ⃗)
    ... | x ⃗ = refl
    ... | x ⃖ = refl
    lem f (x ⃖) with interp f (x ⃖)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl

  unitorˡ-commute-to : ∀ {A B} (f : A ↔ B) (x : _) → eval (f ⨾ uniti₊l) x ≡ eval (uniti₊l ⨾ (id↔ ⊕ f)) x
  unitorˡ-commute-to f x rewrite eval≡interp (f ⨾ uniti₊l) x | eval≡interp (uniti₊l ⨾ (id↔ ⊕ f)) x = lem f x
    where
    lem : ∀ {A B} (f : A ↔ B) (x : _) → interp (f ⨾ uniti₊l) x ≡ interp (uniti₊l ⨾ (id↔ ⊕ f)) x
    lem f (x ⃗) with interp f (x ⃗)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl
    lem f (inj₂ y ⃖) with interp f (y ⃖)
    ... | x ⃗ = refl
    ... | x ⃖ = refl

  unitorʳ-commute-from : ∀ {A B} (f : A ↔ B) (x : _) → eval ((f ⊕ id↔) ⨾ swap₊ ⨾ unite₊l) x ≡ eval ((swap₊ ⨾ unite₊l) ⨾ f) x
  unitorʳ-commute-from f x rewrite eval≡interp ((f ⊕ id↔) ⨾ swap₊ ⨾ unite₊l) x | eval≡interp ((swap₊ ⨾ unite₊l) ⨾ f) x = lem f x
    where
    lem : ∀ {A B} (f : A ↔ B) (x : _) → interp ((f ⊕ id↔) ⨾ swap₊ ⨾ unite₊l) x ≡ interp ((swap₊ ⨾ unite₊l) ⨾ f) x
    lem f (inj₁ x ⃗) with interp f (x ⃗)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl
    lem f (x ⃖) with interp f (x ⃖)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl

  unitorʳ-commute-to : ∀ {A B} (f : A ↔ B) (x : _) → eval (f ⨾ uniti₊l ⨾ swap₊) x ≡ eval ((uniti₊l ⨾ swap₊) ⨾ (f ⊕ id↔)) x
  unitorʳ-commute-to f x rewrite eval≡interp (f ⨾ uniti₊l ⨾ swap₊) x | eval≡interp ((uniti₊l ⨾ swap₊) ⨾ (f ⊕ id↔)) x = lem f x
    where
    lem : ∀ {A B} (f : A ↔ B) (x : _) → interp (f ⨾ uniti₊l ⨾ swap₊) x ≡ interp ((uniti₊l ⨾ swap₊) ⨾ (f ⊕ id↔)) x
    lem f (x ⃗) with interp f (x ⃗)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl
    lem f (inj₁ x ⃖) with interp f (x ⃖)
    ... | x₁ ⃗ = refl
    ... | x₁ ⃖ = refl

  assoc-commute-from : ∀ {A B C D E F} (f : A ↔ B) (g : C ↔ D) (h : E ↔ F) (x : _) → eval (((f ⊕ g) ⊕ h) ⨾ assocr₊) x ≡ eval (assocr₊ ⨾ (f ⊕ (g ⊕ h))) x
  assoc-commute-from f g h x rewrite eval≡interp (((f ⊕ g) ⊕ h) ⨾ assocr₊) x | eval≡interp (assocr₊ ⨾ (f ⊕ (g ⊕ h))) x = lem f g h x
    where
    lem : ∀ {A B C D E F} (f : A ↔ B) (g : C ↔ D) (h : E ↔ F) (x : _) → interp (((f ⊕ g) ⊕ h) ⨾ assocr₊) x ≡ interp (assocr₊ ⨾ (f ⊕ (g ⊕ h))) x
    lem f g h (inj₁ (inj₁ x) ⃗) with interp f (x ⃗)
    ... | x' ⃗ = refl
    ... | x' ⃖ = refl
    lem f g h (inj₁ (inj₂ y) ⃗) with interp g (y ⃗)
    ... | y' ⃗ = refl
    ... | y' ⃖ = refl
    lem f g h (inj₂ z ⃗) with interp h (z ⃗)
    ... | z' ⃗ = refl
    ... | z' ⃖ = refl
    lem f g h (inj₁ x ⃖) with interp f (x ⃖)
    ... | x' ⃗ = refl
    ... | x' ⃖ = refl
    lem f g h (inj₂ (inj₁ y) ⃖) with interp g (y ⃖)
    ... | y' ⃗ = refl
    ... | y' ⃖ = refl
    lem f g h (inj₂ (inj₂ z) ⃖) with interp h (z ⃖)
    ... | z' ⃗ = refl
    ... | z' ⃖ = refl

  assoc-commute-to : ∀ {A B C D E F} (f : A ↔ B) (g : C ↔ D) (h : E ↔ F) (x : _) → eval ((f ⊕ (g ⊕ h)) ⨾ assocl₊) x ≡ eval (assocl₊ ⨾ ((f ⊕ g) ⊕ h)) x
  assoc-commute-to f g h x rewrite eval≡interp ((f ⊕ (g ⊕ h)) ⨾ assocl₊) x | eval≡interp (assocl₊ ⨾ ((f ⊕ g) ⊕ h)) x = lem f g h x
    where
    lem : ∀ {A B C D E F} (f : A ↔ B) (g : C ↔ D) (h : E ↔ F) (x : _) → interp ((f ⊕ (g ⊕ h)) ⨾ assocl₊) x ≡ interp (assocl₊ ⨾ ((f ⊕ g) ⊕ h)) x
    lem f g h (inj₁ x ⃗) with interp f (x ⃗)
    ... | x' ⃗ = refl
    ... | x' ⃖ = refl
    lem f g h (inj₂ (inj₁ y) ⃗) with interp g (y ⃗)
    ... | y' ⃗ = refl
    ... | y' ⃖ = refl
    lem f g h (inj₂ (inj₂ z) ⃗) with interp h (z ⃗)
    ... | z' ⃗ = refl
    ... | z' ⃖ = refl
    lem f g h (inj₁ (inj₁ x) ⃖) with interp f (x ⃖)
    ... | x' ⃗ = refl
    ... | x' ⃖ = refl
    lem f g h (inj₁ (inj₂ y) ⃖) with interp g (y ⃖)
    ... | y' ⃗ = refl
    ... | y' ⃖ = refl
    lem f g h (inj₂ z ⃖) with interp h (z ⃖)
    ... | z' ⃗ = refl
    ... | z' ⃖ = refl

Pi-Braided : Braided Pi-Monoidal
Pi-Braided = record { braiding = record { F⇒G = record { η = λ _ → swap₊
                                                       ; commute = λ {(f , g) x → commute f g x}
                                                       ; sym-commute = λ {(f , g) x → sym (commute f g x)}}
                                        ; F⇐G = record { η = λ _ → swap₊
                                                       ; commute = λ { (f , g) x → commute g f x}
                                                       ; sym-commute = λ {(f , g) x → sym (commute g f x)}}
                                        ; iso = λ _ → record { isoˡ = λ { (inj₁ v ⃗) → refl
                                                                        ; (inj₂ v ⃗) → refl
                                                                        ; (inj₁ v ⃖) → refl
                                                                        ; (inj₂ v ⃖) → refl}
                                                             ; isoʳ = λ { (inj₁ v ⃗) → refl
                                                                        ; (inj₂ v ⃗) → refl
                                                                        ; (inj₁ v ⃖) → refl
                                                                        ; (inj₂ v ⃖) → refl} } }
                    ; hexagon₁ = λ { (inj₁ (inj₁ v) ⃗) → refl
                                   ; (inj₁ (inj₂ v) ⃗) → refl
                                   ; (inj₂ v ⃗) → refl
                                   ; (inj₁ v ⃖) → refl
                                   ; (inj₂ (inj₁ v) ⃖) → refl
                                   ; (inj₂ (inj₂ v) ⃖) → refl}
                    ; hexagon₂ = λ { (inj₁ (inj₁ v) ⃖) → refl
                                   ; (inj₁ (inj₂ v) ⃖) → refl
                                   ; (inj₂ v ⃖) → refl
                                   ; (inj₁ v ⃗) → refl
                                   ; (inj₂ (inj₁ v) ⃗) → refl
                                   ; (inj₂ (inj₂ v) ⃗) → refl}}
  where
  commute : ∀ {A B C D} (f : A ↔ C) (g : B ↔ D) (x : _)
          → eval ((f ⊕ g) ⨾ swap₊) x ≡ eval (swap₊ ⨾ (g ⊕ f)) x
  commute f g x rewrite eval≡interp ((f ⊕ g) ⨾ swap₊) x | eval≡interp (swap₊ ⨾ (g ⊕ f)) x = lem f g x
    where
    lem : ∀ {A B C D} (f : A ↔ C) (g : B ↔ D) (x : _)
        → interp ((f ⊕ g) ⨾ swap₊) x ≡ interp (swap₊ ⨾ (g ⊕ f)) x
    lem f g (inj₁ x ⃗) with interp f (x ⃗)
    ... | _ ⃗ = refl
    ... | _ ⃖ = refl
    lem f g (inj₂ y ⃗) with interp g (y ⃗)
    ... | _ ⃗ = refl
    ... | _ ⃖ = refl
    lem f g (inj₁ y ⃖) with interp g (y ⃖)
    ... | _ ⃗ = refl
    ... | _ ⃖ = refl
    lem f g (inj₂ x ⃖) with interp f (x ⃖)
    ... | _ ⃗ = refl
    ... | _ ⃖ = refl

Pi-Symmetric : Symmetric Pi-Monoidal
Pi-Symmetric = record { braided = Pi-Braided
                      ; commutative = λ { (inj₁ v ⃗) → refl
                                        ; (inj₂ v ⃗) → refl
                                        ; (inj₁ v ⃖) → refl
                                        ; (inj₂ v ⃖) → refl}}

Pi-Rigid : LeftRigid Pi-Monoidal
Pi-Rigid = record { _⁻¹ = -_
                  ; η = η₊
                  ; ε = swap₊ ⨾ ε₊
                  ; snake₁ = λ { (v ⃗) → refl
                               ; (v ⃖) → refl}
                  ; snake₂ = λ { ((- v) ⃗) → refl
                               ; ((- v) ⃖) → refl}}

Pi-CompactClosed : CompactClosed Pi-Monoidal
Pi-CompactClosed = record { symmetric = Pi-Symmetric
                          ; rigid     = inj₁ Pi-Rigid}

¬Pi-Inverse : ¬(Inverse Pi-)
¬Pi-Inverse record { _⁻¹ = _⁻¹ } with (ε₊ {𝟙} ⊕ id↔ {𝟙}) ⁻¹
... | c , (_ , _) , uniq = contr
  where
  c₁ c₂ : 𝟘 +ᵤ 𝟙 ↔ (𝟙 +ᵤ - 𝟙) +ᵤ 𝟙
  c₁ = η₊ ⊕ id↔
  c₂ = (η₊ ⊕ id↔) ⨾ swap₊ ⨾ (id↔ ⊕ swap₊) ⨾ assocl₊

  c₁pinv : (eval (((ε₊ {𝟙} ⊕ id↔) ⨾ c₁) ⨾ (ε₊ ⊕ id↔)) ∼ eval (ε₊ ⊕ id↔))
         × (eval ((c₁ ⨾ (ε₊ ⊕ id↔)) ⨾ c₁) ∼ eval c₁)
  c₁pinv = p₁ , p₂
    where
    p₁ : eval (((ε₊ {𝟙} ⊕ id↔) ⨾ c₁) ⨾ (ε₊ ⊕ id↔)) ∼ eval (ε₊ ⊕ id↔)
    p₁ (inj₁ (inj₁ tt) ⃗) = refl
    p₁ (inj₁ (inj₂ (- tt)) ⃗) = refl
    p₁ (inj₂ tt ⃗) = refl
    p₁ (inj₂ tt ⃖) = refl

    p₂ : eval ((c₁ ⨾ (ε₊ ⊕ id↔)) ⨾ c₁) ∼ eval c₁
    p₂ (inj₂ tt ⃗) = refl
    p₂ (inj₁ (inj₁ tt) ⃖) = refl
    p₂ (inj₁ (inj₂ (- tt)) ⃖) = refl
    p₂ (inj₂ tt ⃖) = refl

  c₂pinv : (eval (((ε₊ {𝟙} ⊕ id↔) ⨾ c₂) ⨾ (ε₊ ⊕ id↔)) ∼ eval (ε₊ ⊕ id↔))
         × (eval ((c₂ ⨾ (ε₊ ⊕ id↔)) ⨾ c₂) ∼ eval c₂)
  c₂pinv = p₁ , p₂
    where
    p₁ : eval (((ε₊ {𝟙} ⊕ id↔) ⨾ c₂) ⨾ (ε₊ ⊕ id↔)) ∼ eval (ε₊ ⊕ id↔)
    p₁ (inj₁ (inj₁ tt) ⃗) = refl
    p₁ (inj₁ (inj₂ (- tt)) ⃗) = refl
    p₁ (inj₂ tt ⃗) = refl
    p₁ (inj₂ tt ⃖) = refl

    p₂ : eval ((c₂ ⨾ (ε₊ ⊕ id↔)) ⨾ c₂) ∼ eval c₂
    p₂ (inj₂ tt ⃗) = refl
    p₂ (inj₁ (inj₁ tt) ⃖) = refl
    p₂ (inj₁ (inj₂ (- tt)) ⃖) = refl
    p₂ (inj₂ tt ⃖) = refl

  c∼c₁ : eval c ∼ eval c₁
  c∼c₁ = uniq c₁pinv

  c∼c₂ : eval c ∼ eval c₂
  c∼c₂ = uniq c₂pinv

  contr : ⊥
  contr with trans (sym (c∼c₁ (inj₂ _ ⃗))) (c∼c₂ (inj₂ _ ⃗))
  ... | ()

IHom : ∀ {A B C} → C ↔ (- A +ᵤ B) → (C +ᵤ A) ↔ B
IHom f = (f ⊕ id↔) ⨾ [A+B]+C=[A+C]+B ⨾ (swap₊ ⊕ id↔) ⨾ (ε₊ ⊕ id↔) ⨾ unite₊l

IHom' : ∀ {A B C} → C +ᵤ A ↔ B → C ↔ - A +ᵤ B
IHom' f = uniti₊l ⨾ (η₊ ⊕ id↔) ⨾ (swap₊ ⊕ id↔) ⨾ (assocr₊ ⨾ id↔ ⊕ swap₊) ⨾ id↔ ⊕ f

IHom'∘IHom : ∀ {A B C} → (f : C ↔ (- A +ᵤ B)) → interp f ∼ interp (IHom' (IHom f))
IHom'∘IHom f (c ⃗) with interp f (c ⃗)
IHom'∘IHom f (c ⃗) | inj₁ (- a) ⃗ = refl
IHom'∘IHom f (c ⃗) | inj₂ b ⃗ = refl
IHom'∘IHom f (c ⃗) | (c' ⃖) = refl
IHom'∘IHom f (inj₁ (- a) ⃖) with interp f (inj₁ (- a) ⃖)
IHom'∘IHom f (inj₁ (- a) ⃖) | inj₁ (- a') ⃗ = refl
IHom'∘IHom f (inj₁ (- a) ⃖) | inj₂ b ⃗ = refl
IHom'∘IHom f (inj₁ (- a) ⃖) | c ⃖ = refl
IHom'∘IHom f (inj₂ b ⃖) with interp f (inj₂ b ⃖)
IHom'∘IHom f (inj₂ b ⃖) | inj₁ (- a) ⃗ = refl
IHom'∘IHom f (inj₂ b ⃖) | inj₂ b' ⃗ = refl
IHom'∘IHom f (inj₂ b ⃖) | c ⃖ = refl

IHom∘IHom' : ∀ {A B C} → (f : (C +ᵤ A) ↔ B) → interp f ∼ interp (IHom (IHom' f))
IHom∘IHom' f (inj₁ c ⃗) with interp f (inj₁ c ⃗)
IHom∘IHom' f (inj₁ c ⃗) | b ⃗ = refl
IHom∘IHom' f (inj₁ c ⃗) | inj₁ c' ⃖ = refl
IHom∘IHom' f (inj₁ c ⃗) | inj₂ a ⃖ = refl
IHom∘IHom' f (inj₂ a ⃗) with interp f (inj₂ a ⃗)
IHom∘IHom' f (inj₂ a ⃗) | b ⃗ = refl
IHom∘IHom' f (inj₂ a ⃗) | inj₁ c ⃖ = refl
IHom∘IHom' f (inj₂ a ⃗) | inj₂ a' ⃖ = refl
IHom∘IHom' f (b ⃖) with interp f (b ⃖)
IHom∘IHom' f (b ⃖) | b' ⃗ = refl
IHom∘IHom' f (b ⃖) | inj₁ c ⃖ = refl
IHom∘IHom' f (b ⃖) | inj₂ a ⃖ = refl

Ev : ∀ {A B} → (- A +ᵤ B) +ᵤ A ↔ B
Ev = [A+B]+C=[A+C]+B ⨾ ((swap₊ ⨾ ε₊) ⊕ id↔) ⨾ unite₊l

hof : ∀ {A B} → (𝟘 ↔ (- A +ᵤ B)) → (A ↔ B)
hof f = uniti₊l ⨾ (f ⊕ id↔) ⨾ [A+B]+C=[A+C]+B ⨾ (swap₊ ⨾ ε₊) ⊕ id↔ ⨾ unite₊l

hof' : ∀ {A B} → (A ↔ B) → (𝟘 ↔ (- A +ᵤ B))
hof' f = η₊ ⨾ (f ⊕ id↔) ⨾ swap₊

hof'∘hof : ∀ {A B} → (f : 𝟘 ↔ (- A +ᵤ B)) → interp f ∼ interp (hof' (hof f))
hof'∘hof f (inj₁ (- a) ⃖) with interp f (inj₁ (- a) ⃖)
hof'∘hof f (inj₁ (- a) ⃖) | inj₁ (- a') ⃗ = refl
hof'∘hof f (inj₁ (- a) ⃖) | inj₂ b ⃗ = refl
hof'∘hof f (inj₂ b ⃖) with interp f (inj₂ b ⃖)
hof'∘hof f (inj₂ b ⃖) | inj₁ (- a) ⃗ = refl
hof'∘hof f (inj₂ b ⃖) | inj₂ b' ⃗ = refl

hof∘hof' : ∀ {A B} → (f : A ↔ B) → interp f ∼ interp (hof (hof' f))
hof∘hof' f (a ⃗) with interp f (a ⃗)
hof∘hof' f (a ⃗) | b ⃗ = refl
hof∘hof' f (a ⃗) | a' ⃖ = refl
hof∘hof' f (b ⃖) with interp f (b ⃖)
hof∘hof' f (b ⃖) | b' ⃗ = refl
hof∘hof' f (b ⃖) | a ⃖ = refl


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

open import LogicalFormulae
open import Groups.Definition
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations

module Fields.FieldOfFractions.Group {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open import Fields.FieldOfFractions.Setoid I
open import Fields.FieldOfFractions.Addition I

fieldOfFractionsGroup : Group fieldOfFractionsSetoid fieldOfFractionsPlus
Group.+WellDefined fieldOfFractionsGroup {record { num = a ; denom = b ; denomNonzero = b!=0 }} {record { num = c ; denom = d ; denomNonzero = d!=0 }} {record { num = e ; denom = f ; denomNonzero = f!=0 }} {record { num = g ; denom = h ; denomNonzero = h!=0 }} af=be ch=dg = need
  where
    open Setoid S
    open Ring R
    open Equivalence eq
    have1 : (c * h) ∼ (d * g)
    have1 = ch=dg
    have2 : (a * f) ∼ (b * e)
    have2 = af=be
    need : (((a * d) + (b * c)) * (f * h)) ∼ ((b * d) * (((e * h) + (f * g))))
    need = transitive (transitive (Ring.*Commutative R) (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) (transitive *Associative (transitive (*WellDefined (*Commutative) reflexive) (transitive (*WellDefined *Associative reflexive) (transitive (*WellDefined (*WellDefined have2 reflexive) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) reflexive) (symmetric *Associative))))))))) (transitive *Commutative (transitive (transitive (symmetric *Associative) (*WellDefined reflexive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined have1 reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))))))) *Associative))))) (symmetric (Ring.*DistributesOver+ R))
Group.0G fieldOfFractionsGroup = record { num = Ring.0R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }
Group.inverse fieldOfFractionsGroup record { num = a ; denom = b ; denomNonzero = p } = record { num = Group.inverse (Ring.additiveGroup R) a ; denom = b ; denomNonzero = p }
Group.+Associative fieldOfFractionsGroup {record { num = a ; denom = b ; denomNonzero = b!=0 }} {record { num = c ; denom = d ; denomNonzero = d!=0 }} {record { num = e ; denom = f ; denomNonzero = f!=0 }} = need
  where
    open Setoid S
    open Equivalence eq
    need : (((a * (d * f)) + (b * ((c * f) + (d * e)))) * ((b * d) * f)) ∼ ((b * (d * f)) * ((((a * d) + (b * c)) * f) + ((b * d) * e)))
    need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (symmetric (Ring.*Associative R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.*DistributesOver+ R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Associative R) (Ring.*Associative R))) (transitive (Group.+Associative (Ring.additiveGroup R)) (Group.+WellDefined (Ring.additiveGroup R) (transitive (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Associative R) (Ring.*Commutative R)) (Ring.*Commutative R)) (symmetric (Ring.*DistributesOver+ R))) (Ring.*Commutative R)) reflexive)))))
Group.identRight fieldOfFractionsGroup {record { num = a ; denom = b ; denomNonzero = b!=0 }} = need
  where
    open Setoid S
    open Equivalence eq
    need : (((a * Ring.1R R) + (b * Group.0G (Ring.additiveGroup R))) * b) ∼ ((b * Ring.1R R) * a)
    need = transitive (transitive (Ring.*WellDefined R (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) reflexive) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.timesZero R)) (Group.identRight (Ring.additiveGroup R)))) reflexive) (Ring.*Commutative R)) (symmetric (Ring.*WellDefined R (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) reflexive))
Group.identLeft fieldOfFractionsGroup {record { num = a ; denom = b }} = need
  where
    open Setoid S
    open Equivalence eq
    need : (((Group.0G (Ring.additiveGroup R) * b) + (Ring.1R R * a)) * b) ∼ ((Ring.1R R * b) * a)
    need = transitive (transitive (Ring.*WellDefined R (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Commutative R) (Ring.timesZero R)) reflexive) (Group.identLeft (Ring.additiveGroup R)))) reflexive) (Ring.*Commutative R)) (Ring.*WellDefined R (symmetric (Ring.identIsIdent R)) reflexive)
Group.invLeft fieldOfFractionsGroup {record { num = a ; denom = b }} = need
  where
    open Setoid S
    open Equivalence eq
    need : (((Group.inverse (Ring.additiveGroup R) a * b) + (b * a)) * Ring.1R R) ∼ ((b * b) * Group.0G (Ring.additiveGroup R))
    need = transitive (transitive (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) reflexive) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invLeft (Ring.additiveGroup R))) (Ring.timesZero R))))) (symmetric (Ring.timesZero R))
Group.invRight fieldOfFractionsGroup {record { num = a ; denom = b }} = need
  where
    open Setoid S
    open Equivalence eq
    need : (((a * b) + (b * Group.inverse (Ring.additiveGroup R) a)) * Ring.1R R) ∼ ((b * b) * Group.0G (Ring.additiveGroup R))
    need = transitive (transitive (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) reflexive) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invRight (Ring.additiveGroup R))) (Ring.timesZero R))))) (symmetric (Ring.timesZero R))


text:
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin; _≟_)
open import Data.Nat using (suc; zero)
open import Data.Nat.Properties using (suc-injective; 0≢1+n)
open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Data.Vec using (lookup; _[_]≔_)
open import Data.Vec.Properties using (lookup∘update; lookup∘update′)
open import Relation.Binary.PropositionalEquality using (refl; sym; cong; trans; _≡_; _≢_; module ≡-Reasoning)
open import Relation.Nullary using (yes; no)
open ≡-Reasoning

open import Common
open import Global
open import Local
open import Projection

completeness :
  ∀{ n } { act : Action n } { c c′ g g-size }
  -> { g-size-is-size-g : g-size ≡ size-g g }
  -> g ↔ c
  -> c - act →c c′
  -> ∃[ g′ ] g - act →g g′ × g′ ↔ c′
completeness assoc (→c-comm c p≢q lp≡c[p] lq≡c[q] c→c′ (→l-send p _ _) (→l-send .p _ _))
  = ⊥-elim (p≢q refl)
completeness assoc (→c-comm c p≢q lp≡c[p] lq≡c[q] c→c′ (→l-recv p _ _) (→l-send .p _ _))
  = ⊥-elim (p≢q refl)
completeness assoc (→c-comm c p≢q lp≡c[p] lq≡c[q] c→c′ (→l-recv p _ _) (→l-recv .p _ _))
  = ⊥-elim (p≢q refl)
completeness
  {n}
  {act}
  {c′ = c′}
  {g = g}
  {g-size = g-size}
  {g-size-is-size-g = g-size-is-size-g}
  assoc
  (→c-comm {p} {q} {l} c p≢q lp≡c[p] lq≡c[q] refl
    lpReduce@(→l-send {lp = lp} {lpSub = lp′} .p refl p≢q-p)
    lqReduce@(→l-recv {lp = lq} {lpSub = lq′} .q refl p≢q-q)
  )
  with proj-inv-send-recv {g = g}
    (trans (sym (_↔_.isProj assoc p)) (sym lp≡c[p]))
    (trans (sym (_↔_.isProj assoc q)) (sym lq≡c[q]))
... | inj₁ (p≢q , g′ , refl , refl , refl)
    = g′ , →g-prefix , record { isProj = isProj-g′ }
    where
      isProj-g′ : (r : Fin n) -> lookup c′ r ≡ project g′ r
      isProj-g′ r with r ≟ p | r ≟ q
      ...   | yes refl | yes refl = ⊥-elim (p≢q refl)
      ...   | no r≢p   | yes refl
        rewrite lookup∘update q (c [ p ]≔ lp′) lq′
        = refl
      ...   | yes refl | no r≢q
        rewrite lookup∘update′ p≢q (c [ p ]≔ lp′) lq′
        rewrite lookup∘update p c lp′
        = refl
      ...    | no r≢p  | no r≢q
        rewrite lookup∘update′ r≢q (c [ p ]≔ lp′) lq′
        rewrite lookup∘update′ r≢p c lp′
        rewrite sym (proj-prefix-other {l = l} p q r {p≢q} g′ (¬≡-flip r≢p) (¬≡-flip r≢q))
        rewrite _↔_.isProj assoc r
        = refl
... | inj₂ (r , s , r≢s , l′ , gSub , refl , r≢p , s≢p , r≢q , s≢q , gSub-proj-p , gSub-proj-q)
    with g-size
...   | zero
      = ⊥-elim (0≢1+n g-size-is-size-g)
...   | suc gSub-size
      = g′ , gReduce , record { isProj = isProj-g′ }
        where
          lrSub = project gSub r
          lsSub = project gSub s
          remove-prefix-g : ∃[ cSub ] cSub ≡ (c [ r ]≔ lrSub) [ s ]≔ lsSub × gSub ↔ cSub
          remove-prefix-g = config-gt-remove-prefix g c assoc refl
          completeness-gSub : ∃[ gSub′ ] gSub - act →g gSub′ × gSub′ ↔ ((((c [ r ]≔ lrSub) [ s ]≔ lsSub) [ p ]≔ lp′) [ q ]≔ lq′)
          completeness-gSub with remove-prefix-g
          ... | cSub , refl , gSub↔cSub
            = completeness {g = gSub} {g-size = gSub-size} {gSub-size-is-size-gSub} gSub↔cSub cSub→cSub′
            where
              gSub-size-is-size-gSub : gSub-size ≡ size-g gSub
              gSub-size-is-size-gSub = suc-injective g-size-is-size-g
              cSub′ = (cSub [ p ]≔ lp′) [ q ]≔ lq′
              cSub→cSub′ : cSub - act →c cSub′
              cSub→cSub′
                with remove-prefix-g
              ... | cSub , refl , gSub↔cSub = →c-comm cSub p≢q lp≡cSub[p] lq≡cSub[q] refl lpReduce lqReduce
                where
                  lp≡cSub[p] : lp ≡ lookup cSub p
                  lp≡cSub[p]
                    rewrite lp≡c[p]
                    rewrite sym (lookup∘update′ (¬≡-flip r≢p) c lrSub)
                    rewrite sym (lookup∘update′ (¬≡-flip s≢p) (c [ r ]≔ lrSub) lsSub)
                    = refl
                  lq≡cSub[q] : lq ≡ lookup cSub q
                  lq≡cSub[q]
                    rewrite lq≡c[q]
                    rewrite sym (lookup∘update′ (¬≡-flip r≢q) c lrSub)
                    rewrite sym (lookup∘update′ (¬≡-flip s≢q) (c [ r ]≔ lrSub) lsSub)
                    = refl
          g′ : Global n
          g′ with completeness-gSub
          ... | gSub′ , _ , _ = msgSingle r s r≢s l′ gSub′
          gReduce : g - act →g g′
          gReduce with completeness-gSub
          ... | gSub′ , gSubReduce , gSub′↔cSub′
            = →g-cont gSubReduce (¬≡-flip r≢p) (¬≡-flip r≢q) (¬≡-flip s≢p) (¬≡-flip s≢q)
          isProj-g′ : (t : Fin n) -> lookup c′ t ≡ project g′ t
          isProj-g′ t with remove-prefix-g | completeness-gSub
          ... | cSub , un-c′ , g′↔c′ | gSub′ , gSubReduce , gSub′↔cSub′
              with r ≟ t  | s ≟ t
          ... | yes refl | yes refl = ⊥-elim (r≢s refl)
          ... | no r≢t   | yes refl
              rewrite sym (_↔_.isProj gSub′↔cSub′ s)
              rewrite lookup∘update′ s≢q (c [ p ]≔ lp′) lq′
              rewrite lookup∘update′ s≢p c lp′
              rewrite _↔_.isProj assoc s
              rewrite proj-prefix-recv {l = l′} r s gSub r≢s
              rewrite lookup∘update′ s≢q (((c [ r ]≔ lrSub) [ s ]≔ lsSub) [ p ]≔ lp′) lq′
              rewrite lookup∘update′ s≢p ((c [ r ]≔ lrSub) [ s ]≔ lsSub) lp′
              rewrite lookup∘update s (c [ r ]≔ lrSub) lsSub
              = refl
          ... | yes refl | no s≢t
              rewrite sym (_↔_.isProj gSub′↔cSub′ r)
              rewrite lookup∘update′ r≢q (c [ p ]≔ lp′) lq′
              rewrite lookup∘update′ r≢p c lp′
              rewrite _↔_.isProj assoc r
              rewrite proj-prefix-send {l = l′} r s gSub r≢s
              rewrite lookup∘update′ r≢q (((c [ r ]≔ lrSub) [ s ]≔ lsSub) [ p ]≔ lp′) lq′
              rewrite lookup∘update′ r≢p ((c [ r ]≔ lrSub) [ s ]≔ lsSub) lp′
              rewrite lookup∘update′ r≢s (c [ r ]≔ lrSub) lsSub
              rewrite lookup∘update r c lrSub
              = refl
          ... | no r≢t  | no s≢t
              rewrite proj-prefix-other {l = l′} r s t {r≢s} gSub′ r≢t s≢t
              with p ≟ t  | q ≟ t
          ...   | yes refl | yes refl = ⊥-elim (p≢q refl)
          ...   | yes refl | no  q≢t
                  rewrite lookup∘update′ p≢q (c [ p ]≔ lp′) lq′
                  rewrite lookup∘update p c lp′
                  rewrite sym (_↔_.isProj gSub′↔cSub′ p)
                  rewrite lookup∘update′ p≢q (((c [ r ]≔ lrSub) [ s ]≔ lsSub) [ p ]≔ lp′) lq′
                  rewrite lookup∘update p ((c [ r ]≔ lrSub) [ s ]≔ lsSub) lp′
                  = refl
          ...   | no  p≢t  | yes refl
                  rewrite lookup∘update q (c [ p ]≔ lp′) lq′
                  rewrite sym (_↔_.isProj gSub′↔cSub′ q)
                  rewrite lookup∘update q (((c [ r ]≔ lrSub) [ s ]≔ lsSub) [ p ]≔ lp′) lq′
                  = refl
          ...   | no  p≢t  | no  q≢t
                  rewrite lookup∘update′ (¬≡-flip q≢t) (c [ p ]≔ lp′) lq′
                  rewrite lookup∘update′ (¬≡-flip p≢t) c lp′
                  rewrite sym (_↔_.isProj gSub′↔cSub′ t)
                  rewrite lookup∘update′ (¬≡-flip q≢t) (((c [ r ]≔ lrSub) [ s ]≔ lsSub) [ p ]≔ lp′) lq′
                  rewrite lookup∘update′ (¬≡-flip p≢t) ((c [ r ]≔ lrSub) [ s ]≔ lsSub) lp′
                  rewrite lookup∘update′ (¬≡-flip s≢t) (c [ r ]≔ lrSub) lsSub
                  rewrite lookup∘update′ (¬≡-flip r≢t) c lrSub
                  = refl

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


text:
-- Andreas, 2019-08-20, issue #4016

-- Debug printing should not crash Agda even if there are
-- __IMPOSSIBLE__s buried inside values that get printed.

{-# OPTIONS -v scope.decl.trace:80 #-}  -- KEEP!

-- The following is some random code (see issue #4010)
-- that happened to trigger an internal error with verbosity 80.

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List

data D : Set where
  c : D

module M where

  private

    unquoteDecl g = do
      ty ← quoteTC D
      _  ← declareDef (arg (arg-info visible relevant) g) ty
      qc ← quoteTC c
      defineFun g (clause [] [] qc ∷ [])

-- Should print lots of debug stuff and succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- Andreas, 2018-10-18, issue #3285, reported by ice1000
-- Testcase by Frederik NF

f : Set → Set
f x = x

syntax f a = a

-- WAS: internal error
--
-- Now: parse error: Malformed syntax declaration

max_forks_repo_name: Agda-zh/agda


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

open import HoTT
open import homotopy.Freudenthal

module homotopy.IterSuspensionStable where

{- π (S k) (Ptd-Susp^ (S n) X) == π k (Ptd-Susp^ n X), where k = S k'
   Susp^Stable below assumes k ≠ O instead of taking k' as the argument -}
module Susp^StableSucc {i} (k n : ℕ) (Skle : S k ≤ n *2)
  (X : Ptd i) {{_ : is-connected ⟨ n ⟩ (de⊙ X)}} where

  {- some numeric computations -}
  private
    Skle' : ⟨ S k ⟩ ≤T ⟨ n ⟩₋₁ +2+ ⟨ n ⟩₋₁
    Skle' = ≤T-trans (⟨⟩-monotone-≤ Skle) (inl (lemma n))
      where lemma : (n : ℕ) → ⟨ n *2 ⟩ == ⟨ n ⟩₋₁ +2+ ⟨ n ⟩₋₁
            lemma O = idp
            lemma (S n') = ap S (ap S (lemma n')
                                 ∙ ! (+2+-βr ⟨ S n' ⟩₋₂ ⟨ S n' ⟩₋₂))

  private
    module F = FreudenthalIso
      ⟨ n ⟩₋₂ k Skle' X

  stable : πS (S k) (⊙Susp X) ≃ᴳ πS k X
  stable =
    πS (S k) (⊙Susp X)
      ≃ᴳ⟨ πS-Ω-split-iso k (⊙Susp X) ⟩
    πS k (⊙Ω (⊙Susp X))
      ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso k (⊙Ω (⊙Susp X)) ⁻¹ᴳ ⟩
    Ω^S-group k (⊙Trunc ⟨ S k ⟩ (⊙Ω (⊙Susp X)))
      ≃ᴳ⟨ F.iso ⁻¹ᴳ ⟩
    Ω^S-group k (⊙Trunc ⟨ S k ⟩ X)
      ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso k X ⟩
    πS k X ≃ᴳ∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module eq where

open import level

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

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

{-# BUILTIN EQUALITY _≡_ #-}

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 4 _≡_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

sym : ∀ {ℓ}{A : Set ℓ}{x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {ℓ}{A : Set ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(p : A → B) {x y : A} → x ≡ y → p x ≡ p y
cong p refl = refl

congf : ∀{l l' : Level}{A : Set l}{B : Set l'}{f f' : A → B}{b c : A} → f ≡ f' → b ≡ c → (f b) ≡ (f' c)
congf refl refl = refl

congf2 : ∀{l l' l'' : Level}{A : Set l}{B : Set l'}{C : Set l''}{f f' : A → B → C}{b c : A}{d e : B} → f ≡ f' → b ≡ c → d ≡ e → (f b d) ≡ (f' c e)
congf2 refl refl refl = refl

cong2 : ∀{i j k}{A : Set i}{B : Set j}{C : Set k}{a a' : A}{b b' : B}
  → (f : A → B → C)
  → a ≡ a'
  → b ≡ b'
  → f a b ≡ f a' b'
cong2 f refl refl = refl

cong3 : ∀{i j k l}{A : Set i}{B : Set j}{C : Set k}{D : Set l}{a a' : A}{b b' : B}{c c' : C}
  → (f : A → B → C → D)
  → a ≡ a'
  → b ≡ b'
  → c ≡ c'
  → f a b c ≡ f a' b' c'
cong3 f refl refl refl = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
import      LibraBFT.Impl.Consensus.ConsensusTypes.Properties.QuorumCert as QC
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert            as QuorumCert
open import LibraBFT.Impl.Consensus.ConsensusTypes.SyncInfo as SI
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.Impl.Types.BlockInfo as BI
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open Invariants
open RoundManagerTransProps

module LibraBFT.Impl.Consensus.ConsensusTypes.Properties.SyncInfo where

module verifyMSpec (self : SyncInfo) (validator : ValidatorVerifier) where

  epoch = self ^∙ siHighestQuorumCert ∙ qcCertifiedBlock ∙ biEpoch

  record SIVerifyProps (pre : RoundManager) : Set where
    field
      sivpEp≡       : epoch ≡ self ^∙ siHighestCommitCert ∙ qcCertifiedBlock ∙ biEpoch
      sivpTcEp≡     : maybeS (self ^∙ siHighestTimeoutCert) Unit $ λ tc -> epoch ≡ tc ^∙ tcEpoch
      sivpHqc≥Hcc   : (self ^∙ siHighestQuorumCert) [ _≥_ ]L self ^∙ siHighestCommitCert at qcCertifiedBlock ∙ biRound
      sivpHqc≢empty : self ^∙ siHighestCommitCert ∙ qcCommitInfo ≢ BI.empty
      sivpHqcVer    : QC.Contract (self ^∙ siHighestQuorumCert) validator
      sivpHccVer    : maybeS (self ^∙ sixxxHighestCommitCert) Unit $ λ qc → QC.Contract qc validator
      -- Waiting on TimeoutCertificate Contract : sivpHtcVer    : maybeS (self ^∙ siHighestTimeoutCert  ) Unit $ λ tc → {!!}

  module _ (pre : RoundManager) where

   record Contract (r : Either ErrLog Unit) (post : RoundManager) (outs : List Output) : Set where
     constructor mkContract
     field
       -- General properties / invariants
       rmInv         : Preserves RoundManagerInv pre post
       noStateChange : pre ≡ post
       -- Output
       noMsgOuts     : OutputProps.NoMsgs outs
       -- Syncing
       syncResCorr   : r ≡ Right unit → SIVerifyProps pre
       -- NOTE: Since the output contains no messages and the state does not
       -- change, nothing needs to be said about the quorum certificats in the
       -- output and post state

   verifyCorrect : SI.verify self validator ≡ Right unit → SIVerifyProps pre
   verifyCorrect verify≡
      with epoch ≟ self ^∙ siHighestCommitCert ∙ qcCertifiedBlock ∙ biEpoch
   ...| no  ep≢ = absurd (Left _ ≡ Right _) case verify≡ of λ ()
   ...| yes sivpEp≡
      with sivpTcEp≡ verify≡
      where
      sivpTcEp≡ : SI.verify.step₁ self validator ≡ Right unit
                  → maybeS (self ^∙ siHighestTimeoutCert) Unit (\tc -> epoch ≡ tc ^∙ tcEpoch)
                    × SI.verify.step₂ self validator ≡ Right unit
      sivpTcEp≡ verify≡₁
         with self ^∙ siHighestTimeoutCert
      ...| nothing = unit , verify≡₁
      ...| just tc
         with epoch ≟ tc ^∙ tcEpoch
      ...| yes tce≡ = tce≡ , verify≡₁
      ...| no  tce≢ = absurd (Left _ ≡ Right _) case verify≡₁ of λ ()
   ...| sivpTcEp≡ , verify≡₂
      with sivpHqc≥Hcc verify≡₂
      where
      sivpHqc≥Hcc : (SI.verify.step₂ self validator ≡ Right unit)
                    → (self ^∙ siHighestQuorumCert) [ _≥_ ]L self ^∙ siHighestCommitCert at qcCertifiedBlock ∙ biRound
                      × SI.verify.step₃ self validator ≡ Right unit
      sivpHqc≥Hcc verify≡₂
         with    self ^∙ siHighestQuorumCert ∙ qcCertifiedBlock ∙ biRound
              ≥? self ^∙ siHighestCommitCert ∙ qcCertifiedBlock ∙ biRound
      ...| yes hqc≥hcc = hqc≥hcc , verify≡₂
      ...| no  hqc<hcc = absurd Left _ ≡ Right _ case verify≡₂ of λ ()
   ...| sivpHqc≥Hcc , verify≡₃
      with sivpHqc≢empty verify≡₃
      where
      sivpHqc≢empty : (SI.verify.step₃ self validator ≡ Right unit)
                      → self ^∙ siHighestCommitCert ∙ qcCommitInfo ≢ BI.empty
                        × SI.verify.step₄ self validator ≡ Right unit
      sivpHqc≢empty verify≡₃
         with self ^∙ siHighestCommitCert ∙ qcCommitInfo ≟ BI.empty
      ...| no  ≢empty = ≢empty , verify≡₃
      ...| yes ≡empty = absurd Left _ ≡ Right _ case verify≡₃ of λ ()
   ...| sivpHqc≢empty , verify≡₄
      with sivpHqcVer verify≡₄
      where
      sivpHqcVer : (SI.verify.step₄ self validator ≡ Right unit)
                   → QC.Contract (self ^∙ siHighestQuorumCert) validator
                     × SI.verify.step₅ self validator ≡ Right unit
      sivpHqcVer verify≡₄
         with  QuorumCert.verify (self ^∙ siHighestQuorumCert)  validator | inspect
              (QuorumCert.verify (self ^∙ siHighestQuorumCert)) validator
      ...| Left  _    | _ = absurd Left _ ≡ Right _ case verify≡₄ of λ ()
      ...| Right unit | [ R ]
         with QC.contract (self ^∙ siHighestQuorumCert) validator (Right unit) refl R
      ...| qcCon = qcCon , verify≡₄
   ...| sivpHqcVer , verify≡₅
      with sivpHccVer verify≡₅
      where
      sivpHccVer : (SI.verify.step₅ self validator ≡ Right unit)
                   → (maybeS (self ^∙ sixxxHighestCommitCert) Unit $ λ qc → QC.Contract qc validator)
                     × SI.verify.step₆ self validator ≡ Right unit
      sivpHccVer verify≡₅
         with self ^∙ sixxxHighestCommitCert
      ...| nothing = unit , verify≡₅
      ...| just qc
         with QuorumCert.verify  qc  validator | inspect
              (QuorumCert.verify qc) validator
      ...| Left _ | _ = absurd Left _ ≡ Right _ case verify≡₅ of λ ()
      ...| Right unit | [ R ] = QC.contract qc validator (Right unit) refl R , verify≡₅
   ...| sivpHccVer , verify≡₆ =
   -- TODO: continue case analysis for remaining fields
     record
     { sivpEp≡       = sivpEp≡
     ; sivpTcEp≡     = sivpTcEp≡
     ; sivpHqc≥Hcc   = sivpHqc≥Hcc
     ; sivpHqc≢empty = sivpHqc≢empty
     ; sivpHqcVer    = sivpHqcVer
     ; sivpHccVer    = sivpHccVer
     -- ; sivpHtcVer =
     }

   contract : ∀ Q → (RWS-Post-⇒ Contract Q) → LBFT-weakestPre (SI.verifyM self validator) Q pre
   contract Q pf = LBFT-⇒ (SI.verifyM self validator) pre (mkContract id refl refl verifyCorrect) pf


text:
module Rationals.Add.Assoc where

open import Equality
open import Function

open import Nats using (zero; ℕ)
                 renaming (suc to s; _+_ to _:+:_; _*_ to _:*:_)
open import Rationals
open import Rationals.Properties
open import Nats.Add.Comm
open import Nats.Add.Assoc
open import Nats.Multiply.Distrib
open import Nats.Multiply.Assoc
open import Nats.Multiply.Comm

------------------------------------------------------------------------
-- internal stuffs

private

  a+b+c=a+/b+c/ : ∀ a b c → a + (b + c) ≡ (a + b) + c
  a+b+c=a+/b+c/ (ax ÷ ay) (bx ÷ by) (cx ÷ cy)
    rewrite ax ÷ ay ↑ (by :*: cy)
          | bx ÷ by ↑ (ay :*: cy)
          | cx ÷ cy ↑ (ay :*: by)
          | nat-multiply-assoc ay by cy
          | sym $ nat-multiply-distrib (bx :*: cy) (cx :*: by) ay
          | sym $ nat-multiply-distrib (ax :*: by) (bx :*: ay) cy
          | sym $ nat-add-assoc (ax :*: (by :*: cy))
                                (bx :*: cy :*: ay) (cx :*: by :*: ay)
          | nat-multiply-assoc ax by cy
          | nat-multiply-comm ay by
          | nat-multiply-assoc cx by ay
          | nat-multiply-assoc bx cy ay
          | nat-multiply-assoc bx ay cy
          | nat-multiply-comm cy ay
            = refl

rational-add-assoc : ∀ a b c → a + (b + c) ≡ (a + b) + c
rational-add-assoc = a+b+c=a+/b+c/


text:
-- Intuitionistic propositional calculus.
-- Gentzen-style formalisation of syntax.
-- Normal forms and neutrals.

module IPC.Syntax.GentzenNormalForm where

open import IPC.Syntax.Gentzen public

-- Derivations.

mutual
  -- Normal forms, or introductions.
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ (Γ : Cx Ty) : Ty → Set where
    neⁿᶠ   : ∀ {A}   → Γ ⊢ⁿᵉ A → Γ ⊢ⁿᶠ A
    lamⁿᶠ  : ∀ {A B} → Γ , A ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ▻ B
    pairⁿᶠ : ∀ {A B} → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ∧ B
    unitⁿᶠ : Γ ⊢ⁿᶠ ⊤
    inlⁿᶠ  : ∀ {A B} → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᶠ A ∨ B
    inrⁿᶠ  : ∀ {A B} → Γ ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ∨ B

  -- Neutrals, or eliminations.
  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ (Γ : Cx Ty) : Ty → Set where
    varⁿᵉ  : ∀ {A}     → A ∈ Γ → Γ ⊢ⁿᵉ A
    appⁿᵉ  : ∀ {A B}   → Γ ⊢ⁿᵉ A ▻ B → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᵉ B
    fstⁿᵉ  : ∀ {A B}   → Γ ⊢ⁿᵉ A ∧ B → Γ ⊢ⁿᵉ A
    sndⁿᵉ  : ∀ {A B}   → Γ ⊢ⁿᵉ A ∧ B → Γ ⊢ⁿᵉ B
    boomⁿᵉ : ∀ {C}     → Γ ⊢ⁿᵉ ⊥ → Γ ⊢ⁿᵉ C
    caseⁿᵉ : ∀ {A B C} → Γ ⊢ⁿᵉ A ∨ B → Γ , A ⊢ⁿᶠ C → Γ , B ⊢ⁿᶠ C → Γ ⊢ⁿᵉ C

infix 3 _⊢⋆ⁿᶠ_
_⊢⋆ⁿᶠ_ : Cx Ty → Cx Ty → Set
Γ ⊢⋆ⁿᶠ ∅     = 𝟙
Γ ⊢⋆ⁿᶠ Ξ , A = Γ ⊢⋆ⁿᶠ Ξ × Γ ⊢ⁿᶠ A

infix 3 _⊢⋆ⁿᵉ_
_⊢⋆ⁿᵉ_ : Cx Ty → Cx Ty → Set
Γ ⊢⋆ⁿᵉ ∅     = 𝟙
Γ ⊢⋆ⁿᵉ Ξ , A = Γ ⊢⋆ⁿᵉ Ξ × Γ ⊢ⁿᵉ A

-- Translation to simple terms.

mutual
  nf→tm : ∀ {A Γ} → Γ ⊢ⁿᶠ A → Γ ⊢ A
  nf→tm (neⁿᶠ t)     = ne→tm t
  nf→tm (lamⁿᶠ t)    = lam (nf→tm t)
  nf→tm (pairⁿᶠ t u) = pair (nf→tm t) (nf→tm u)
  nf→tm unitⁿᶠ       = unit
  nf→tm (inlⁿᶠ t)    = inl (nf→tm t)
  nf→tm (inrⁿᶠ t)    = inr (nf→tm t)

  ne→tm : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊢ A
  ne→tm (varⁿᵉ i)      = var i
  ne→tm (appⁿᵉ t u)    = app (ne→tm t) (nf→tm u)
  ne→tm (fstⁿᵉ t)      = fst (ne→tm t)
  ne→tm (sndⁿᵉ t)      = snd (ne→tm t)
  ne→tm (boomⁿᵉ t)     = boom (ne→tm t)
  ne→tm (caseⁿᵉ t u v) = case (ne→tm t) (nf→tm u) (nf→tm v)

nf→tm⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ⁿᶠ Ξ → Γ ⊢⋆ Ξ
nf→tm⋆ {∅}     ∙        = ∙
nf→tm⋆ {Ξ , A} (ts , t) = nf→tm⋆ ts , nf→tm t

ne→tm⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ⁿᵉ Ξ → Γ ⊢⋆ Ξ
ne→tm⋆ {∅}     ∙        = ∙
ne→tm⋆ {Ξ , A} (ts , t) = ne→tm⋆ ts , ne→tm t

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ⁿᶠ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ⁿᶠ A → Γ′ ⊢ⁿᶠ A
  mono⊢ⁿᶠ η (neⁿᶠ t)     = neⁿᶠ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᶠ η (lamⁿᶠ t)    = lamⁿᶠ (mono⊢ⁿᶠ (keep η) t)
  mono⊢ⁿᶠ η (pairⁿᶠ t u) = pairⁿᶠ (mono⊢ⁿᶠ η t) (mono⊢ⁿᶠ η u)
  mono⊢ⁿᶠ η unitⁿᶠ       = unitⁿᶠ
  mono⊢ⁿᶠ η (inlⁿᶠ t)    = inlⁿᶠ (mono⊢ⁿᶠ η t)
  mono⊢ⁿᶠ η (inrⁿᶠ t)    = inrⁿᶠ (mono⊢ⁿᶠ η t)

  mono⊢ⁿᵉ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ⁿᵉ A → Γ′ ⊢ⁿᵉ A
  mono⊢ⁿᵉ η (varⁿᵉ i)      = varⁿᵉ (mono∈ η i)
  mono⊢ⁿᵉ η (appⁿᵉ t u)    = appⁿᵉ (mono⊢ⁿᵉ η t) (mono⊢ⁿᶠ η u)
  mono⊢ⁿᵉ η (fstⁿᵉ t)      = fstⁿᵉ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᵉ η (sndⁿᵉ t)      = sndⁿᵉ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᵉ η (boomⁿᵉ t)     = boomⁿᵉ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᵉ η (caseⁿᵉ t u v) = caseⁿᵉ (mono⊢ⁿᵉ η t) (mono⊢ⁿᶠ (keep η) u) (mono⊢ⁿᶠ (keep η) v)

mono⊢⋆ⁿᶠ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ⁿᶠ Ξ → Γ′ ⊢⋆ⁿᶠ Ξ
mono⊢⋆ⁿᶠ {∅}     η ∙        = ∙
mono⊢⋆ⁿᶠ {Ξ , A} η (ts , t) = mono⊢⋆ⁿᶠ η ts , mono⊢ⁿᶠ η t

mono⊢⋆ⁿᵉ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ⁿᵉ Ξ → Γ′ ⊢⋆ⁿᵉ Ξ
mono⊢⋆ⁿᵉ {∅}     η ∙        = ∙
mono⊢⋆ⁿᵉ {Ξ , A} η (ts , t) = mono⊢⋆ⁿᵉ η ts , mono⊢ⁿᵉ η t

-- Reflexivity.

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

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Issue1296.SolvedMeta where

open import Common.Prelude
open import Common.Equality

test : zero ≡ {!!}
test = refl


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.Semilattice where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.Semilattice

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Poset

open Category

module _ {ℓ} (L : Semilattice ℓ) where
  open JoinSemilattice L

  JoinSemilatticeCategory : Category ℓ ℓ
  JoinSemilatticeCategory = PosetCategory IndPoset

module _ {ℓ} (L : Semilattice ℓ) where
  open MeetSemilattice L

  MeetSemilatticeCategory : Category ℓ ℓ
  MeetSemilatticeCategory = PosetCategory IndPoset

max_stars_repo_name: FernandoLarrain/cubical


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

module Definition.Typed.Decidable where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Decidable
open import Definition.Conversion.Soundness
open import Definition.Conversion.Stability
open import Definition.Conversion.Consequences.Completeness

open import Tools.Nullary

-- Decidability of conversion of well-formed types
dec : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ B → Dec (Γ ⊢ A ≡ B)
dec ⊢A ⊢B = map soundnessConv↑ completeEq
                (decConv↑ (completeEq (refl ⊢A))
                          (completeEq (refl ⊢B)))

-- Decidability of conversion of well-formed terms
decTerm : ∀ {t u A Γ} → Γ ⊢ t ∷ A → Γ ⊢ u ∷ A → Dec (Γ ⊢ t ≡ u ∷ A)
decTerm ⊢t ⊢u = map soundnessConv↑Term completeEqTerm
                    (decConv↑Term (completeEqTerm (refl ⊢t))
                                  (completeEqTerm (refl ⊢u)))


text:
test : Set → Set
test record{} = record{}

-- Record pattern at non-record type  Set
-- when checking that the clause test record {} = record {} has
-- type Set → Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Ideal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Logic using ([_]; _∈_)

open import Cubical.Algebra.Ring

private
  variable
    ℓ : Level

module _ (R' : Ring {ℓ}) where

  open Ring R' renaming (Carrier to R)

  {- by default, 'ideal' means two-sided ideal -}
  record isIdeal (I : R → hProp ℓ) : Type ℓ where
    field
      +-closed : {x y : R} → x ∈ I → y ∈ I → (x + y) ∈ I
      -closed : {x : R} → x ∈ I → - x ∈ I
      0r-closed : 0r ∈ I
      ·-closedLeft : {x : R} → (r : R) → x ∈ I → r · x ∈ I
      ·-closedRight : {x : R} → (r : R) → x ∈ I → x · r ∈ I

  Ideal : Type _
  Ideal = Σ[ I ∈ (R → hProp ℓ) ] isIdeal I

  record isLeftIdeal (I : R → hProp ℓ) : Type ℓ where
    field
      +-closed : {x y : R} → x ∈ I → y ∈ I → (x + y) ∈ I
      -closed : {x : R} → x ∈ I → - x ∈ I
      0r-closed : 0r ∈ I
      ·-closedLeft : {x : R} → (r : R) → x ∈ I → r · x ∈ I

  record isRightIdeal (I : R → hProp ℓ) : Type ℓ where
    field
      +-closed : {x y : R} → x ∈ I → y ∈ I → (x + y) ∈ I
      -closed : {x : R} → x ∈ I → - x ∈ I
      0r-closed : 0r ∈ I
      ·-closedRight : {x : R} → (r : R) → x ∈ I → x · r ∈ I

  {- Examples of ideals -}
  zeroSubset : (x : R) → hProp ℓ
  zeroSubset x = (x ≡ 0r) , isSetRing R' _ _

  open Theory R'

  isIdealZeroIdeal : isIdeal zeroSubset
  isIdealZeroIdeal = record
                       { +-closed = λ x≡0 y≡0 → _ + _    ≡⟨ cong (λ u → u + _) x≡0 ⟩
                                                0r + _   ≡⟨ +-lid _ ⟩
                                                _        ≡⟨ y≡0 ⟩
                                                0r        ∎
                       ; -closed = λ x≡0 → - _ ≡⟨ cong (λ u → - u) x≡0 ⟩
                                           - 0r ≡⟨ 0-selfinverse ⟩
                                           0r ∎
                       ; 0r-closed = refl
                       ; ·-closedLeft = λ r x≡0 → r · _ ≡⟨ cong (λ u → r · u) x≡0 ⟩
                                                  r · 0r ≡⟨ 0-rightNullifies r  ⟩
                                                  0r ∎
                       ; ·-closedRight = λ r x≡0 → _ · r ≡⟨ cong (λ u → u · r) x≡0 ⟩
                                                   0r · r ≡⟨ 0-leftNullifies r ⟩
                                                   0r ∎
                       }

  zeroIdeal : Ideal
  zeroIdeal = zeroSubset , isIdealZeroIdeal

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Lemmachine.Utils where
open import Lemmachine.Request
open import Lemmachine.Response
open import Data.Maybe
open import Data.Bool hiding (_≟_)
open import Data.String
open import Data.Function
open import Data.Product
open import Relation.Nullary
open import Data.List hiding (any)
open import Data.List.Any
open Membership-≡

Application = Request → Response
Middleware = Application → Application

fetch : String → List (String × String) → Maybe String
fetch x xs with any (_≟_ x ∘ proj₁) xs
... | yes p = just (proj₂ (proj₁ (find p)))
... | no _ = nothing

private
  fromHeaders : RequestHeaders → List (String × String)
  fromHeaders xs = Data.List.map f xs where
    f : RequestHeader → String × String
    f (k , v) = k , v

fetchHeader : String → RequestHeaders → Maybe String
fetchHeader x xs with any (_≟_ x ∘ headerKey) xs
... | yes p = just (headerValue (proj₁ (find p)))
... | no _ = nothing

fetchContentType : String → List String → Maybe String
fetchContentType _ [] = nothing
fetchContentType "*" (y ∷ _) = just y
fetchContentType "*/*" (y ∷ _) = just y
fetchContentType x (y ∷ ys) with x == y
... | true = just y
... | false = fetchContentType x ys

fetchAccept : RequestHeaders → List String → Maybe String
fetchAccept hs cs with fetchHeader "Accept" hs
fetchAccept hs _ | nothing = nothing
fetchAccept _ [] | just _ = nothing
fetchAccept _ xss | just y = fetchContentType y xss

postulate
  isDate : String → Bool
  isModified : String → String → Bool
  now : String

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Agda.Builtin.Bool

data ⊥ : Set where

record ⊤ : Set where

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

record Squash {ℓ} (A : Set ℓ) : Set ℓ where
  field
    .unsquash : A
open Squash

f : .Bool → Squash Set₁
f b .unsquash = Set
  module M where
    IsTrue' : Set
    IsTrue' = IsTrue b

g : Squash Set₁
g .unsquash = Set
  module N where
    open M

    h : IsTrue' true → Set₁
    h p = Set


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Boolean.Definition

module Boolean.Lemmas where

notNot : (x : Bool) → not (not x) ≡ x
notNot BoolTrue = refl
notNot BoolFalse = refl

notXor : (x y : Bool) → not (xor x y) ≡ xor (not x) y
notXor BoolTrue BoolTrue = refl
notXor BoolTrue BoolFalse = refl
notXor BoolFalse BoolTrue = refl
notXor BoolFalse BoolFalse = refl


text:
module Module where

record R
  : Set
  where

module M where

module N where

module O where

  postulate

    A
      : Set

x
  : R
x
  = record {M}

module P
  = N

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
-- Andreas, 2018-08-14, issue #3176, reported by identicalsnowflake
--
-- Absurd lambdas should be equal.
-- In this case, they were only considered equal during give, but not upon reload.

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

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

open Σ public

∃ : ∀ {A : Set} → (A → Set) → Set
∃ = Σ _

_×_ : ∀ _ _ → _
_×_ a b = ∃ λ (_ : a) → b

record Fin (n : ℕ) : Set where
  field
    m : ℕ
    .p : ∃ λ k → (ℕ.suc k + m) ≡ n

module _ (n : ℕ) where

  data S : Set where
    V : S
    K : Fin n → S
    _X_ : S → S → S

[_] : ∀ {n} → S n → (Fin n → Set) → Set → Set
[ V       ] k t = t
[ K i     ] k _ = k i
[ s₁ X s₂ ] k t = [ s₁ ] k t × [ s₂ ] k t

postulate
  ignore : ∀ {t : Set} → t

_<*>_ : ∀ {s : S 0} {t₁ t₂}
  → [ s ] (λ ()) (t₁ → t₂)
  → [ s ] (λ ()) t₁
  → [ s ] (λ ()) t₂
_<*>_ {s₁ X s₂} {t₁} {t₂} (f , _) (x , _) =
  let v : [ s₁ ] (λ ()) t₂
      v = _<*>_ {s = s₁} {t₁ = t₁} {t₂ = t₂} f x
  in
  ignore
_<*>_ f x = ignore

-- Should succeed.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module Hello where

-- Oh, you made it! Well done! This line is a comment.

-- In the beginning, Agda knows nothing, but we can teach it about numbers.

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

-- data Nat = Zero | Suc Nat -- in Haskell

-- Now we can say how to add numbers.

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

-- Now we can try adding some numbers.

four : Nat
four = (suc (suc zero)) +N (suc (suc zero))

-- To make it go, select "Evaluate term to normal form" from the
-- Agda menu, then type "four", without the quotes, and press return.

-- Hopefully, you should get a response
--   suc (suc (suc (suc zero)))

-- Done?

-- Now you can start Ex1.agda

-- WARNING Ex1.agda requires you to give a definition of addition.
-- There are lots of ways to define addition, and by the end of the
-- exercise, it will matter which you choose. If you start just by
-- copying the above definition, you will reach a point where you
-- may wish to reconsider it, and hopefully learn something useful
-- about the way Agda works.


text:
module Terms where

import Level
open import Data.Unit as Unit
open import Data.List as List
open import Data.Product as Product
open import Categories.Category using (Category)

data Type : Set where
  Nat : Type
  _ˢ : Type → Type
  _⇒_ : Type → Type → Type

infixr 5 _⇒_

open import Common.Context Type
  using (Ctx; Var; zero; ctx-cat; ctx-bin-coproducts)
  renaming (succ to succ)
open Categories.Category.Category ctx-cat
  renaming ( _⇒_ to _▹_
           ; _≡_ to _≈_
           ; _∘_ to _●_
           ; id  to ctx-id
           )
open import Categories.Object.BinaryCoproducts ctx-cat
open BinaryCoproducts ctx-bin-coproducts

data Term (Γ : Ctx) : (σ : Type) → Set where
  var  : ∀{σ : Type}       (x : Var Γ σ)          → Term Γ σ
  abs  : ∀{σ τ : Type}     (t : Term (σ ∷ Γ) τ)   → Term Γ (σ ⇒ τ)
  app  : ∀{σ τ : Type}     (t : Term Γ (σ ⇒ τ))
                           (s : Term Γ σ)         → Term Γ τ
  -- Constants for recursion over ℕ
  𝟘    : Term Γ Nat
  s⁺   : Term Γ (Nat ⇒ Nat)
  R    : ∀{σ : Type} → Term Γ (σ ⇒ (Nat ⇒ σ ⇒ σ) ⇒ Nat ⇒ σ)
  -- Constants for corecursion over streams
  hd   : ∀{σ : Type} → Term Γ (σ ˢ ⇒ σ)
  tl   : ∀{σ : Type} → Term Γ (σ ˢ ⇒ σ ˢ)
  C    : ∀{σ τ : Type} → Term Γ ((σ ⇒ τ) ⇒ (σ ⇒ σ) ⇒ σ ⇒ τ ˢ)

-- Improve readability
_⟨$⟩_ : ∀{Γ σ τ} (t : Term Γ (σ ⇒ τ)) (s : Term Γ σ) → Term Γ τ
t ⟨$⟩ s = app t s

infixl 0 _⟨$⟩_

hd′ : ∀{Γ σ} → Term Γ (σ ˢ) → Term Γ σ
hd′ s = hd ⟨$⟩ s

tl′ : ∀{Γ σ} → Term Γ (σ ˢ) → Term Γ (σ ˢ)
tl′ s = tl ⟨$⟩ s

C′ : ∀{Γ σ τ} → Term Γ (σ ⇒ τ) → Term Γ (σ ⇒ σ) → Term Γ (σ ⇒ τ ˢ)
C′ h t = (C ⟨$⟩ h) ⟨$⟩ t

R′ : ∀{Γ σ} → Term Γ σ → Term Γ (Nat ⇒ σ ⇒ σ) → Term Γ (Nat ⇒ σ)
R′ x f = R ⟨$⟩ x ⟨$⟩ f

ƛ : ∀{Γ σ τ} → (Var (σ ∷ Γ) σ → Term (σ ∷ Γ) τ) → Term Γ (σ ⇒ τ)
ƛ f = abs (f zero)

abs₁ : ∀{Γ τ σ} →
       (Term (τ ∷ Γ) τ → Term (τ ∷ Γ) σ)
       → Term Γ (τ ⇒ σ)
abs₁ f = abs (f (var zero))

abs₂ : ∀{Γ τ₁ τ₂ σ} →
       (Term (τ₂ ∷ τ₁ ∷ Γ) τ₁ →
         Term (τ₂ ∷ τ₁ ∷ Γ) τ₂ →
         Term (τ₂ ∷ τ₁ ∷ Γ) σ) →
       Term Γ (τ₁ ⇒ τ₂ ⇒ σ)
abs₂ {Γ} {τ₁} f = abs (abs (f x₁ x₂))
  where
    x₁ = var (succ τ₁ zero)
    x₂ = var zero

abs₃ : ∀{Γ τ₁ τ₂ τ₃ σ} →
       (Term (τ₃ ∷ τ₂ ∷ τ₁ ∷ Γ) τ₁ →
         Term (τ₃ ∷ τ₂ ∷ τ₁ ∷ Γ) τ₂ →
         Term (τ₃ ∷ τ₂ ∷ τ₁ ∷ Γ) τ₃ →
         Term (τ₃ ∷ τ₂ ∷ τ₁ ∷ Γ) σ) →
       Term Γ (τ₁ ⇒ τ₂ ⇒ τ₃ ⇒ σ)
abs₃ {Γ} {τ₁} {τ₂} f = abs (abs (abs (f x₁ x₂ x₃)))
  where
    x₁ = var (succ τ₁ (succ τ₁ zero))
    x₂ = var (succ τ₂ zero)
    x₃ = var zero

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

π₁ :  ∀{Γ σ τ} → Term Γ (σ ⇒ τ ⇒ σ)
π₁ = abs₂ (λ x₁ x₂ → x₁)

π₂ :  ∀{Γ σ τ} → Term Γ (σ ⇒ τ ⇒ τ)
π₂ = abs₂ (λ x₁ x₂ → x₂)

-- | Prepend element to a stream
-- hd (cons x s) = x
-- tl (cons x s) = s
-- This needs to use continuations.
conc : ∀{Γ σ} → Term Γ (σ ⇒ σ ˢ ⇒ σ ˢ)
conc {Γ} {σ} = abs (abs (C′ f g ⟨$⟩ i))
  where
    -- | State space
    S = (σ ⇒ σ ˢ ⇒ σ) ⇒ σ
    -- | local context
    Γ′ = σ ˢ ∷ σ ∷ Γ

    f : Term Γ′ (S ⇒ σ)
    f = abs₁ (λ v → v ⟨$⟩ π₁)

    g : Term Γ′ (S ⇒ S)
    g = abs₂ (λ v _h →
             v ⟨$⟩ (abs₂ (λ _ s →
               h ⟨$⟩ (hd′ s) ⟨$⟩ (tl′ s))
             )
        )
      where
        Γ′′ = σ ˢ ∷ σ ∷ (σ ⇒ σ ˢ ⇒ σ) ∷ S ∷ Γ′
        h : Term Γ′′ (σ ⇒ σ ˢ ⇒ σ)
        h = var (succ (σ ⇒ σ ˢ ⇒ σ) (succ (σ ⇒ σ ˢ ⇒ σ) zero))

    i : Term Γ′ S
    i = abs₁ (λ h → h ⟨$⟩ x ⟨$⟩ s)
      where
        s : Term ((σ ⇒ σ ˢ ⇒ σ) ∷ Γ′) (σ ˢ)
        s = var (succ (σ ˢ) zero)
        x : Term ((σ ⇒ σ ˢ ⇒ σ) ∷ Γ′) σ
        x = var (succ σ (succ σ zero))

_∺_ : ∀{Γ σ} → Term Γ σ → Term Γ (σ ˢ) → Term Γ (σ ˢ)
x ∺ s = conc ⟨$⟩ x ⟨$⟩ s

id′ : ∀{Γ σ} → Term Γ (σ ⇒ σ)
id′ = abs₁ (λ x → x)

repeat : ∀{Γ σ} → Term Γ (σ ⇒ σ ˢ)
repeat = C′ id′ id′

-- | Extend a stream that is defined up to n by an element on the right, i.e.,
--     ext x 0     s  = repeat x
-- hd (ext x (n+1) s) = hd s
-- tl (ext x (n+1) s) = ext x n (tl s)
-- Thus ext is given by a recursion, followed by a corecursion:
-- ext x = R (λ_. repeat x) f
-- f _ h s = hd s ∷ (h (tl s))
ext : ∀{Γ σ} → Term Γ (σ ⇒ Nat ⇒ σ ˢ ⇒ σ ˢ)
ext {Γ} {σ} = abs (R′ (abs (repeat ⟨$⟩ x)) f)
  where
    Γ′ = σ ∷ Γ
    x : Term (σ ˢ ∷ Γ′) σ
    x = var (succ σ zero)

    f : Term Γ′ (Nat ⇒ (σ ˢ ⇒ σ ˢ) ⇒ σ ˢ ⇒ σ ˢ)
    f = abs₃ (λ _ h s → (hd′ s) ∺ (h ⟨$⟩ (tl′ s)))

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

open import Categories.Category

-- this module characterizes a category of all equalizer indexed by I.
-- this notion formalizes a category with all equalizer up to certain cardinal.
module Categories.Diagram.Equalizer.Indexed {o ℓ e} (C : Category o ℓ e) where

open import Level

open Category C

record IndexedEqualizerOf {i} {I : Set i} {A B : Obj} (M : I → A ⇒ B) : Set (i ⊔ o ⊔ e ⊔ ℓ) where
  field
    E   : Obj
    arr : E ⇒ A

    -- a reference morphism
    ref : E ⇒ B
    equality  : ∀ i → M i ∘ arr ≈ ref
    equalize  : ∀ {X} (h : X ⇒ A) (r : X ⇒ B) → (∀ i → M i ∘ h ≈ r) → X ⇒ E
    universal : ∀ {X} (h : X ⇒ A) (r : X ⇒ B) (eq : ∀ i → M i ∘ h ≈ r) → h ≈ arr ∘ equalize h r eq
    unique    : ∀ {X} {l : X ⇒ E} (h : X ⇒ A) (r : X ⇒ B) (eq : ∀ i → M i ∘ h ≈ r) → h ≈ arr ∘ l → l ≈ equalize h r eq

record IndexedEqualizer {i} (I : Set i) : Set (i ⊔ o ⊔ e ⊔ ℓ) where
  field
    A B         : Obj
    M           : I → A ⇒ B
    equalizerOf : IndexedEqualizerOf M

  open IndexedEqualizerOf equalizerOf public

AllEqualizers : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
AllEqualizers i = (I : Set i) → IndexedEqualizer I

AllEqualizersOf : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
AllEqualizersOf i = ∀ {I : Set i} {A B : Obj} (M : I → A ⇒ B) → IndexedEqualizerOf M

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2016-11-19 issue #2309
-- No-eta-equality needs to be respected in pattern matching
-- also before the clause compiler.

record Unit : Set where
  constructor unit
  no-eta-equality

record R : Set₁ where
  field Fst : Unit → Set
        Snd : (x : Unit) → Fst x
open R

Test : (A : Set) (a : A) → R
Fst (Test A a) unit = A
Snd (Test A a) x    = a  -- should not be accepted


text:
{- functions related to lift types.  The main function is do-lift, which
   is called from hnf -}
module lift where

open import lib
open import cedille-types
open import ctxt
open import syntax-util
open import subst

liftingType-to-kind : liftingType → kind
liftingType-to-kind (LiftArrow l1 l2) = KndArrow (liftingType-to-kind l1) (liftingType-to-kind l2)
liftingType-to-kind (LiftStar _) = star
liftingType-to-kind (LiftParens _ l _) = liftingType-to-kind l
liftingType-to-kind (LiftTpArrow tp l) = KndTpArrow tp (liftingType-to-kind l)
liftingType-to-kind (LiftPi _ x tp l) = KndPi posinfo-gen posinfo-gen x (Tkt tp) (liftingType-to-kind l)

liftingType-to-type : var → liftingType → type
liftingType-to-type X (LiftArrow l1 l2) = TpArrow (liftingType-to-type X l1) NotErased (liftingType-to-type X l2)
liftingType-to-type X (LiftTpArrow tp l) = TpArrow tp NotErased (liftingType-to-type X l)
liftingType-to-type X (LiftStar _) = TpVar posinfo-gen X
liftingType-to-type X (LiftParens _ l _) = liftingType-to-type X l
liftingType-to-type X (LiftPi _ x tp l) = Abs posinfo-gen Pi posinfo-gen x (Tkt tp) (liftingType-to-type X l)

{- create a type-level redex of the form

   (↑ X . (λ xs . t) : ls → l) xs

   where xs and ls are packaged as the input list of tuples, l is the
   input liftingType, and t is the input term. -}
lift-freeze : var → 𝕃 (var × liftingType) → liftingType → term → type
lift-freeze X tobind l t =
  let xs = map fst tobind in
    TpApp* (Lft posinfo-gen posinfo-gen X (Lam* xs t) (LiftArrow* (map snd tobind) l))
      (map (λ p → TpVar posinfo-gen (fst p)) tobind)

do-liftargs : ctxt → type → liftingType → 𝕃 term → var → 𝕃 (var × liftingType) → type
do-liftargs Γ tp (LiftArrow l1 l2) (arg :: args) X tobind =
  do-liftargs Γ (TpApp tp (lift-freeze X tobind l1 arg)) l2 args X tobind
do-liftargs Γ tp (LiftTpArrow l1 l2) (arg :: args) X tobind =
  do-liftargs Γ (TpAppt tp arg) l2 args X tobind
do-liftargs Γ tp (LiftPi _ x _ l) (arg :: args) X tobind =
  do-liftargs Γ (TpAppt tp arg) (subst Γ arg x l) args X tobind
do-liftargs Γ tp (LiftParens _ l _) args X tobind = do-liftargs Γ tp l args X tobind
do-liftargs Γ tp _ _ _ _ = tp

-- tobind are the variables we have seen going through the lifting type (they are also mapped by the trie)
do-lifth : ctxt → trie liftingType →
           𝕃 (var × liftingType) → type → var → liftingType →
           (term → term) → -- function to put terms in hnf
           term →
           type
do-lifth Γ m tobind origtp X (LiftParens _ l _) hnf t = do-lifth Γ m tobind origtp X l hnf t
do-lifth Γ m tobind origtp X (LiftArrow l1 l2) hnf (Lam _ _ _ x _ t) =
  do-lifth Γ (trie-insert m x l1) ((x , l1) :: tobind) origtp X l2 hnf t
do-lifth Γ m tobind origtp X (LiftTpArrow tp l2) hnf (Lam _ _ _ x _ t) =
  TpLambda posinfo-gen posinfo-gen x (Tkt tp) (do-lifth Γ m tobind origtp X l2 hnf t)
do-lifth Γ m tobind origtp X l hnf t with decompose-apps (hnf t)
do-lifth Γ m tobind origtp X l hnf t | (Var _ x) , args with trie-lookup m x
do-lifth Γ m tobind origtp X l hnf t | (Var _ x) , args | nothing = origtp -- the term being lifted is not headed by one of the bound vars
do-lifth Γ m tobind origtp X l hnf t | (Var _ x) , args | just l' =
  rebind tobind (do-liftargs Γ (TpVar posinfo-gen x) l' (reverse args) X tobind)
  where rebind : 𝕃 (var × liftingType) → type → type
        rebind ((x , l'):: xs) tp = rebind xs (TpLambda posinfo-gen posinfo-gen x (Tkk (liftingType-to-kind l')) tp)
        rebind [] tp = tp
do-lifth Γ m tobind origtp X l hnf t | _ , args = origtp

-- lift a term to a type at the given liftingType, if possible.
do-lift : ctxt → type → var → liftingType → (term → term) {- hnf -} → term → type
do-lift Γ origtp X l hnf t = do-lifth Γ empty-trie [] origtp X l hnf t

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille