text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Kripke-style semantics with abstract worlds.
-- Gödel embedding.

module BasicIPC.Semantics.KripkeGodel where

open import BasicIPC.Syntax.Common public

-- Kripke models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    World : Set

    -- Intuitionistic accessibility; preorder.
    _≤_    : World → World → Set
    refl≤  : ∀ {w} → w ≤ w
    trans≤ : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″

    -- Forcing for atomic propositions.
    _⊩ᵅ_ : World → Atom → Set

open Model {{…}} public

-- Forcing in a particular world of a particular model, based on the Gödel embedding of IPC in S4.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World → Ty → Set
  w ⊩ α P   = ∀ {w′} → w ≤ w′ → w′ ⊩ᵅ P
  w ⊩ A ▻ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
  w ⊩ A ∧ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A × w′ ⊩ B
  w ⊩ ⊤    = ∀ {w′} → w ≤ w′ → 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Cx Ty → Set
  w ⊩⋆ ∅     = 𝟙
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w ⊩ A

-- Monotonicity with respect to intuitionistic accessibility.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
  mono⊩ {α P}   ξ s = λ ξ′ → s (trans≤ ξ ξ′)
  mono⊩ {A ▻ B} ξ s = λ ξ′ → s (trans≤ ξ ξ′)
  mono⊩ {A ∧ B} ξ s = λ ξ′ → s (trans≤ ξ ξ′)
  mono⊩ {⊤}    ξ s = λ ξ′ → ∙

  mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     ξ ∙       = ∙
  mono⊩⋆ {Ξ , A} ξ (γ , a) = mono⊩⋆ {Ξ} ξ γ , mono⊩ {A} ξ a

-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ : ∀ {A B w} → w ⊩ A ▻ B → w ⊩ A → w ⊩ B
  s ⟪$⟫ a = s refl≤ a

  ⟪K⟫ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A
  ⟪K⟫ {A} a ξ = K (mono⊩ {A} ξ a)

  ⟪S⟫ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ A ▻ B → w ⊩ A → w ⊩ C
  ⟪S⟫ {A} {B} {C} s₁ s₂ a = _⟪$⟫_ {B} {C} (_⟪$⟫_ {A} {B ▻ C} s₁ a) (_⟪$⟫_ {A} {B} s₂ a)

  ⟪S⟫′ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ ξ s₂ ξ′ a = let s₁′ = mono⊩ {A ▻ B ▻ C} (trans≤ ξ ξ′) s₁
                                      s₂′ = mono⊩ {A ▻ B} ξ′ s₂
                                  in  ⟪S⟫ {A} {B} {C} s₁′ s₂′ a

  _⟪,⟫_ : ∀ {A B w} → w ⊩ A → w ⊩ B → w ⊩ A ∧ B
  _⟪,⟫_ {A} {B} a b ξ = mono⊩ {A} ξ a , mono⊩ {B} ξ b

  _⟪,⟫′_ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} {B} a ξ = _⟪,⟫_ {A} {B} (mono⊩ {A} ξ a)

  ⟪π₁⟫ : ∀ {A B w} → w ⊩ A ∧ B → w ⊩ A
  ⟪π₁⟫ s = π₁ (s refl≤)

  ⟪π₂⟫ : ∀ {A B w} → w ⊩ A ∧ B → w ⊩ B
  ⟪π₂⟫ s = π₂ (s refl≤)

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : World → Cx Ty → Ty → Set
  w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : World → Cx Ty → Cx Ty → Set
  w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

  ⟦λ⟧ : ∀ {A B Γ w} → (∀ {w′} → w′ ⊩ Γ , A ⇒ B) → w ⊩ Γ ⇒ A ▻ B
  ⟦λ⟧ s γ = λ ξ a → s (mono⊩⋆ ξ γ , a)

  _⟦$⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B
  _⟦$⟧_ {A} {B} s₁ s₂ γ = _⟪$⟫_ {A} {B} (s₁ γ) (s₂ γ)

  ⟦K⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B ▻ A
  ⟦K⟧ {A} {B} a γ = ⟪K⟫ {A} {B} (a γ)

  ⟦S⟧ : ∀ {A B C Γ w} → w ⊩ Γ ⇒ A ▻ B ▻ C → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ C
  ⟦S⟧ {A} {B} {C} s₁ s₂ a γ = ⟪S⟫ {A} {B} {C} (s₁ γ) (s₂ γ) (a γ)

  _⟦,⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B → w ⊩ Γ ⇒ A ∧ B
  _⟦,⟧_ {A} {B} a b γ = _⟪,⟫_ {A} {B} (a γ) (b γ)

  ⟦π₁⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ A
  ⟦π₁⟧ {A} {B} s γ = ⟪π₁⟫ {A} {B} (s γ)

  ⟦π₂⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ B
  ⟦π₂⟧ {A} {B} s γ = ⟪π₂⟫ {A} {B} (s γ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

open import Cubical.HITs.Cost.Base

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K #-}
-- Constructions on top of exploration functions

open import Level.NP
open import Type hiding (★)
open import Type.Identities
open import Function.NP
open import Function.Extensionality
open import Algebra.FunctionProperties.NP
open import Data.Two.Base
open import Data.Indexed
open import Data.Nat.NP hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Fin using (Fin) renaming (zero to fzero)
open import Data.Maybe.NP
open import Algebra
open import Data.Product.NP renaming (map to ×-map) hiding (first)
open import Data.Sum.NP renaming (map to ⊎-map)
open import Data.Zero using (𝟘)
open import Data.One using (𝟙)
open import Data.Tree.Binary
import Data.List as List
open List using (List; _++_)
open import Relation.Nullary.Decidable
open import Relation.Nullary.NP
open import Relation.Binary
open import Relation.Binary.Sum using (_⊎-cong_)
open import Relation.Binary.Product.Pointwise using (_×-cong_)
import Function.Related as FR
import Relation.Binary.PropositionalEquality.NP as ≡
open import HoTT
open Equivalences
open ≡ using (_≡_)

open import Explore.Core
open import Explore.Properties
import Explore.Monad as EM

module Explore.Explorable where

module _ {m a} {A : ★ a} where
  open EM {a} m
  gfilter-explore : ∀ {B} → (A →? B) → Explore m A → Explore m B
  gfilter-explore f eᴬ = eᴬ >>= λ x → maybe (λ η → point-explore η) empty-explore (f x)

  filter-explore : (A → 𝟚) → Explore m A → Explore m A
  filter-explore p = gfilter-explore λ x → [0: nothing 1: just x ] (p x)

  -- monoidal exploration: explore A with a monoid M
  explore-monoid : ∀ {ℓ} → Explore m A → ExploreMon m ℓ A
  explore-monoid eᴬ M = eᴬ ε _·_ where open Mon M renaming (_∙_ to _·_)

  explore-endo : Explore m A → Explore m A
  explore-endo eᴬ ε op f = eᴬ id _∘′_ (op ∘ f) ε

  explore-endo-monoid : ∀ {ℓ} → Explore m A → ExploreMon m ℓ A
  explore-endo-monoid = explore-monoid ∘ explore-endo

  explore-backward : Explore m A → Explore m A
  explore-backward eᴬ ε _∙_ f = eᴬ ε (flip _∙_) f

  -- explore-backward ∘ explore-backward = id
  -- (m : a comm monoid) → explore-backward m = explore m

private
  module FindForward {a} {A : ★ a} (explore : Explore a A) where
    find? : Find? A
    find? = explore nothing (M?._∣_ _)

    first : Maybe A
    first = find? just

    findKey : FindKey A
    findKey pred = find? (λ x → [0: nothing 1: just x ] (pred x))

module ExplorePlug {ℓ a} {A : ★ a} where
  record ExploreIndKit p (P : Explore ℓ A → ★ p) : ★ (a ⊔ ₛ ℓ ⊔ p) where
    constructor mk
    field
      Pε : P empty-explore
      P∙ : ∀ {e₀ e₁ : Explore ℓ A} → P e₀ → P e₁ → P (merge-explore e₀ e₁)
      Pf : ∀ x → P (point-explore x)

  _$kit_ : ∀ {p} {P : Explore ℓ A → ★ p} {e : Explore ℓ A}
           → ExploreInd p e → ExploreIndKit p P → P e
  _$kit_ {P = P} ind (mk Pε P∙ Pf) = ind P Pε P∙ Pf

  _,-kit_ : ∀ {p} {P : Explore ℓ A → ★ p}{Q : Explore ℓ A → ★ p}
            → ExploreIndKit p P → ExploreIndKit p Q → ExploreIndKit p (P ×° Q)
  Pk ,-kit Qk = mk (Pε Pk , Pε Qk)
                   (λ x y → P∙ Pk (fst x) (fst y) , P∙ Qk (snd x) (snd y))
                   (λ x → Pf Pk x , Pf Qk x)
               where open ExploreIndKit

  ExploreInd-Extra : ∀ p → Explore ℓ A → ★ _
  ExploreInd-Extra p exp =
    ∀ (Q     : Explore ℓ A → ★ p)
      (Q-kit : ExploreIndKit p Q)
      (P     : Explore ℓ A → ★ p)
      (Pε    : P empty-explore)
      (P∙    : ∀ {e₀ e₁ : Explore ℓ A} → Q e₀ → Q e₁ → P e₀ → P e₁
               → P (merge-explore e₀ e₁))
      (Pf    : ∀ x → P (point-explore x))
    → P exp

  to-extra : ∀ {p} {e : Explore ℓ A} → ExploreInd p e → ExploreInd-Extra p e
  to-extra e-ind Q Q-kit P Pε P∙ Pf =
   snd (e-ind (Q ×° P)
           (Qε , Pε)
           (λ { (a , b) (c , d) → Q∙ a c , P∙ a c b d })
           (λ x → Qf x , Pf x))
   where open ExploreIndKit Q-kit renaming (Pε to Qε; P∙ to Q∙; Pf to Qf)

  ExplorePlug : ∀ {m} (M : Monoid ℓ m) (e : Explore _ A) → ★ _
  ExplorePlug M e = ∀ f x → e∘ ε _∙_ f ∙ x ≈ e∘ x _∙_ f
     where open Mon M
           e∘ = explore-endo e

  plugKit : ∀ {m} (M : Monoid ℓ m) → ExploreIndKit _ (ExplorePlug M)
  plugKit M = mk (λ _ → fst identity)
                 (λ Ps Ps' f x →
                    trans (∙-cong (! Ps _ _) refl)
                          (trans (assoc _ _ _)
                                 (trans (∙-cong refl (Ps' _ x)) (Ps _ _))))
                 (λ x f _ → ∙-cong (snd identity (f x)) refl)
       where open Mon M

module FromExplore
    {a} {A : ★ a}
    (explore : ∀ {ℓ} → Explore ℓ A) where

  module _ {ℓ} where
    with-monoid : ∀ {m} → ExploreMon ℓ m A
    with-monoid = explore-monoid explore

    with∘ : Explore ℓ A
    with∘ = explore-endo explore

    with-endo-monoid : ∀ {m} → ExploreMon ℓ m A
    with-endo-monoid = explore-endo-monoid explore

    backward : Explore ℓ A
    backward = explore-backward explore

    gfilter : ∀ {B} → (A →? B) → Explore ℓ B
    gfilter f = gfilter-explore f explore

    filter : (A → 𝟚) → Explore ℓ A
    filter p = filter-explore p explore

  sum : Sum A
  sum = explore 0 _+_

  Card : ℕ
  Card = sum (const 1)

  count : Count A
  count f = sum (𝟚▹ℕ ∘ f)

  product : (A → ℕ) → ℕ
  product = explore 1 _*_

  big-∧ big-∨ big-xor : (A → 𝟚) → 𝟚

  big-∧ = explore 1₂ _∧_
  and   = big-∧
  all   = big-∧

  big-∨ = explore 0₂ _∨_
  or    = big-∨
  any   = big-∨

  big-xor = explore 0₂ _xor_

  big-lift∧ big-lift∨ : Level → (A → 𝟚) → 𝟚
  big-lift∧ ℓ f = lower (explore {ℓ} (lift 1₂) (lift-op₂ _∧_) (lift ∘ f))
  big-lift∨ ℓ f = lower (explore {ℓ} (lift 0₂) (lift-op₂ _∨_) (lift ∘ f))

  bin-tree : BinTree A
  bin-tree = explore empty fork leaf

  list : List A
  list = explore List.[] _++_ List.[_]

  module FindBackward = FindForward backward

  findLast? : Find? A
  findLast? = FindBackward.find?

  last : Maybe A
  last = FindBackward.first

  findLastKey : FindKey A
  findLastKey = FindBackward.findKey

  open FindForward explore public

module FromLookup
    {a} {A : ★ a}
    {explore : ∀ {ℓ} → Explore ℓ A}
    (lookup : ∀ {ℓ} → Lookup {ℓ} explore)
    where

  module CheckDec! {ℓ}{P : A → ★ ℓ}(decP : ∀ x → Dec (P x)) where
    CheckDec! : ★ _
    CheckDec! = explore (Lift 𝟙) _×_ λ x → ✓ ⌊ decP x ⌋

    checkDec! : {p✓ : CheckDec!} → ∀ x → P x
    checkDec! {p✓} x = toWitness (lookup p✓ x)

module FromExploreInd
    {a} {A : ★ a}
    {explore : ∀ {ℓ} → Explore ℓ A}
    (explore-ind : ∀ {p ℓ} → ExploreInd {ℓ} p explore)
    where

  open FromExplore explore public

  module _ {ℓ p} where
    explore-mon-ext : ExploreMonExt {ℓ} p explore
    explore-mon-ext m {f} {g} f≈°g = explore-ind (λ s → s _ _ f ≈ s _ _ g) refl ∙-cong f≈°g
      where open Mon m

    explore-mono : ExploreMono {ℓ} p explore
    explore-mono _⊆_ z⊆ _∙-mono_ {f} {g} f⊆°g =
      explore-ind (λ e → e _ _ f ⊆ e _ _ g) z⊆ _∙-mono_ f⊆°g

    open ExplorePlug {ℓ} {a} {A}

    explore∘-plug : (M : Monoid ℓ ℓ) → ExplorePlug M explore
    explore∘-plug M = explore-ind $kit plugKit M

    module _ (M : Monoid ℓ ℓ)
             (open Mon M)
             (f : A → C)
             where
        explore-endo-monoid-spec′ : ∀ z → explore ε _∙_ f ∙ z ≈ explore-endo explore z _∙_ f
        explore-endo-monoid-spec′ = explore-ind (λ e → ∀ z → e ε _∙_ f ∙ z ≈ explore-endo e z _∙_ f)
                                                (fst identity) (λ P₀ P₁ z → trans (assoc _ _ _) (trans (∙-cong refl (P₁ z)) (P₀ _))) (λ _ _ → refl)

        explore-endo-monoid-spec : with-monoid M f ≈ with-endo-monoid M f
        explore-endo-monoid-spec = trans (! snd identity _) (explore-endo-monoid-spec′ ε)

    explore∘-ind : ∀ (M : Monoid ℓ ℓ) → BigOpMonInd ℓ M (with-endo-monoid M)
    explore∘-ind M P Pε P∙ Pf P≈ =
      snd (explore-ind (λ e → ExplorePlug M e × P (λ f → e id _∘′_ (_∙_ ∘ f) ε))
                 (const (fst identity) , Pε)
                 (λ {e} {s'} Ps Ps' → ExploreIndKit.P∙ (plugKit M) {e} {s'} (fst Ps) (fst Ps')
                                    , P≈ (λ f → fst Ps f _) (P∙ (snd Ps) (snd Ps')))
                 (λ x → ExploreIndKit.Pf (plugKit M) x
                      , P≈ (λ f → ! snd identity _) (Pf x)))
      where open Mon M

    explore-swap : ∀ {b} → ExploreSwap {ℓ} p explore {b}
    explore-swap mon {eᴮ} eᴮ-ε pf f =
      explore-ind (λ e → e _ _ (eᴮ ∘ f) ≈ eᴮ (e _ _ ∘ flip f))
                  (! eᴮ-ε)
                  (λ p q → trans (∙-cong p q) (! pf _ _))
                  (λ _ → refl)
      where open Mon mon

    explore-ε : Exploreε {ℓ} p explore
    explore-ε M = explore-ind (λ e → e ε _ (const ε) ≈ ε)
                              refl
                              (λ x≈ε y≈ε → trans (∙-cong x≈ε y≈ε) (fst identity ε))
                              (λ _ → refl)
      where open Mon M

    explore-hom : ExploreHom {ℓ} p explore
    explore-hom cm f g = explore-ind (λ e → e _ _ (f ∙° g) ≈ e _ _ f ∙ e _ _ g)
                                     (! fst identity ε)
                                     (λ p₀ p₁ → trans (∙-cong p₀ p₁) (∙-interchange _ _ _ _))
                                     (λ _ → refl)
      where open CMon cm

    explore-linˡ : ExploreLinˡ {ℓ} p explore
    explore-linˡ m _◎_ f k ide dist = explore-ind (λ e → e ε _∙_ (λ x → k ◎ f x) ≈ k ◎ e ε _∙_ f) (! ide) (λ x x₁ → trans (∙-cong x x₁) (! dist k _ _)) (λ x → refl)
      where open Mon m

    explore-linʳ : ExploreLinʳ {ℓ} p explore
    explore-linʳ m _◎_ f k ide dist = explore-ind (λ e → e ε _∙_ (λ x → f x ◎ k) ≈ e ε _∙_ f ◎ k) (! ide) (λ x x₁ → trans (∙-cong x x₁) (! dist k _ _)) (λ x → refl)
      where open Mon m

    module ProductMonoid
        {M : ★₀} (εₘ : M) (_⊕ₘ_ : Op₂ M)
        {N : ★₀} (εₙ : N) (_⊕ₙ_ : Op₂ N)
        where
        ε = (εₘ , εₙ)
        _⊕_ : Op₂ (M × N)
        (xₘ , xₙ) ⊕ (yₘ , yₙ) = (xₘ ⊕ₘ yₘ , xₙ ⊕ₙ yₙ)

        explore-product-monoid :
          ∀ fₘ fₙ → explore ε _⊕_ < fₘ , fₙ > ≡ (explore εₘ _⊕ₘ_ fₘ , explore εₙ _⊕ₙ_ fₙ)
        explore-product-monoid fₘ fₙ =
          explore-ind (λ e → e ε _⊕_ < fₘ , fₙ > ≡ (e εₘ _⊕ₘ_ fₘ , e εₙ _⊕ₙ_ fₙ)) ≡.refl (≡.ap₂ _⊕_) (λ _ → ≡.refl)
  {-
  empty-explore:
    ε ≡ (εₘ , εₙ) ✓
  point-explore (x , y):
    < fₘ , fₙ > (x , y) ≡ (fₘ x , fₙ y) ✓
  merge-explore e₀ e₁:
    e₀ ε _⊕_ < fₘ , fₙ > ⊕ e₁ ε _⊕_ < fₘ , fₙ >
    ≡
    (e₀ εₘ _⊕ₘ_ fₘ , e₀ εₙ _⊕ₙ_ fₙ) ⊕ (e₁ εₘ _⊕ₘ_ fₘ , e₁ εₙ _⊕ₙ_ fₙ)
    ≡
    (e₀ εₘ _⊕ₘ_ fₘ ⊕ e₁ εₘ _⊕ₘ_ fₘ , e₀ εₙ _⊕ₙ_ fₙ ⊕ e₁ εₙ _⊕ₙ_ fₙ)
  -}

  module _ {ℓ} where
    reify : Reify {ℓ} explore
    reify = explore-ind (λ eᴬ → Πᵉ eᴬ _) _ _,_

    unfocus : Unfocus {ℓ} explore
    unfocus = explore-ind Unfocus (λ{ (lift ()) }) (λ P Q → [ P , Q ]) (λ η → _,_ η)

    module _ {ℓᵣ aᵣ} {Aᵣ : A → A → ★ aᵣ}
             (Aᵣ-refl : Reflexive Aᵣ) where
      ⟦explore⟧ : ⟦Explore⟧ ℓᵣ Aᵣ (explore {ℓ}) (explore {ℓ})
      ⟦explore⟧ Mᵣ zᵣ ∙ᵣ fᵣ = explore-ind (λ e → Mᵣ (e _ _ _) (e _ _ _)) zᵣ (λ η → ∙ᵣ η) (λ η → fᵣ Aᵣ-refl)

    explore-ext : ExploreExt {ℓ} explore
    explore-ext ε op = explore-ind (λ e → e _ _ _ ≡ e _ _ _) ≡.refl (≡.ap₂ op)

  module LiftHom
       {m p}
       {S T : ★ m}
       (_≈_ : T → T → ★ p)
       (≈-refl : Reflexive _≈_)
       (≈-trans : Transitive _≈_)
       (zero : S)
       (_+_  : Op₂ S)
       (one  : T)
       (_*_  : Op₂ T)
       (≈-cong-* : _*_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_)
       (f   : S → T)
       (g   : A → S)
       (hom-0-1 : f zero ≈ one)
       (hom-+-* : ∀ {x y} → (f (x + y)) ≈ (f x * f y))
       where

        lift-hom : f (explore zero _+_ g) ≈ explore one _*_ (f ∘ g)
        lift-hom = explore-ind (λ e → f (e zero _+_ g) ≈ e one _*_ (f ∘ g))
                               hom-0-1
                               (λ p q → ≈-trans hom-+-* (≈-cong-* p q))
                               (λ _ → ≈-refl)

  module _ {ℓ} {P : A → ★_ ℓ} where
    open LiftHom {S = ★_ ℓ} {★_ ℓ} (λ A B → B → A) id _∘′_
                 (Lift 𝟘) _⊎_ (Lift 𝟙) _×_
                 (λ f g → ×-map f g) Dec P (const (no (λ{ (lift ()) })))
                 (uncurry Dec-⊎)
                 public renaming (lift-hom to lift-Dec)

  module FromFocus {p} (focus : Focus {p} explore) where
    Dec-Σ : ∀ {P} → Π A (Dec ∘ P) → Dec (Σ A P)
    Dec-Σ = map-Dec unfocus focus ∘ lift-Dec ∘ reify

  lift-hom-≡ :
      ∀ {m} {S T : ★ m}
        (zero : S)
        (_+_  : Op₂ S)
        (one  : T)
        (_*_  : Op₂ T)
        (f    : S → T)
        (g    : A → S)
        (hom-0-1 : f zero ≡ one)
        (hom-+-* : ∀ {x y} → f (x + y) ≡ f x * f y)
      → f (explore zero _+_ g) ≡ explore one _*_ (f ∘ g)
  lift-hom-≡ z _+_ o _*_ = LiftHom.lift-hom _≡_ ≡.refl ≡.trans z _+_ o _*_ (≡.ap₂ _*_)

  -- Since so far S and T should have the same level, we get this mess of resizing
  -- There is a later version based on ⟦explore⟧.
  module _ (f : A → 𝟚) {{_ : UA}} where
    lift-✓all-Πᵉ : ✓ (big-lift∧ ₁ f) ≡ Πᵉ explore (✓ ∘ f)
    lift-✓all-Πᵉ = lift-hom-≡ (lift 1₂) (lift-op₂ _∧_) (Lift 𝟙) _×_ (✓ ∘ lower) (lift ∘ f) (≡.! Lift≡id) (✓-∧-× _ _)

  module _ (f : A → 𝟚) where
    lift-✓any↔Σᵉ : ✓ (big-lift∨ ₁ f) ↔ Σᵉ explore (✓ ∘ f)
    lift-✓any↔Σᵉ = LiftHom.lift-hom _↔_ (id , id) (zip (flip _∘′_) _∘′_)
                     (lift 0₂) (lift-op₂ _∨_) (Lift 𝟘) _⊎_
                     (zip ⊎-map ⊎-map) (✓ ∘ lower) (lift ∘ f)
                     ((λ()) , λ{(lift())}) (✓∨-⊎ , ⊎-✓∨)

  sum-ind : SumInd sum
  sum-ind P P0 P+ Pf = explore-ind (λ e → P (e 0 _+_)) P0 P+ Pf

  sum-ext : SumExt sum
  sum-ext = explore-ext 0 _+_

  sum-zero : SumZero sum
  sum-zero = explore-ε ℕ+.monoid

  sum-hom : SumHom sum
  sum-hom = explore-hom ℕ°.+-commutativeMonoid

  sum-mono : SumMono sum
  sum-mono = explore-mono _≤_ z≤n _+-mono_

  sum-swap' : SumSwap sum
  sum-swap' {sumᴮ = sᴮ} sᴮ-0 hom f =
    sum-ind (λ s → s (sᴮ ∘ f) ≡ sᴮ (s ∘ flip f))
            (! sᴮ-0)
            (λ p q → (ap₂ _+_ p q) ∙ (! hom _ _)) (λ _ → refl)
    where open ≡

  sum-lin : SumLin sum
  sum-lin f zero    = sum-zero
  sum-lin f (suc k) = ≡.trans (sum-hom f (λ x → k * f x)) (≡.ap₂ _+_ (≡.refl {x = sum f}) (sum-lin f k))

  sum-const : SumConst sum
  sum-const x = sum-ext (λ _ → ! snd ℕ°.*-identity x) ∙ sum-lin (const 1) x ∙ ℕ°.*-comm x Card
    where open ≡

  exploreStableUnder→sumStableUnder : ∀ {p} → StableUnder explore p → SumStableUnder sum p
  exploreStableUnder→sumStableUnder SU-p = SU-p 0 _+_

  count-ext : CountExt count
  count-ext f≗g = sum-ext (≡.cong 𝟚▹ℕ ∘ f≗g)

  sumStableUnder→countStableUnder : ∀ {p} → SumStableUnder sum p → CountStableUnder count p
  sumStableUnder→countStableUnder sumSU-p f = sumSU-p (𝟚▹ℕ ∘ f)

  diff-list = with-endo-monoid (List.monoid A) List.[_]

  {-
  list≡diff-list : list ≡ diff-list
  list≡diff-list = {!explore-endo-monoid-spec (List.monoid A) List.[_]!}
  -}

  lift-sum : ∀ ℓ → Sum A
  lift-sum ℓ f = lower {₀} {ℓ} (explore (lift 0) (lift-op₂ _+_) (lift ∘ f))

  Fin-lower-sum≡Σᵉ-Fin : ∀ {{_ : UA}}(f : A → ℕ) → Fin (lift-sum _ f) ≡ Σᵉ explore (Fin ∘ f)
  Fin-lower-sum≡Σᵉ-Fin f = lift-hom-≡ (lift 0) (lift-op₂ _+_) (Lift 𝟘) _⊎_ (Fin ∘ lower) (lift ∘ f) (Fin0≡𝟘 ∙ ! Lift≡id) (! Fin-⊎-+)
    where open ≡

module FromTwoExploreInd
    {a} {A : ★ a}
    {eᴬ : ∀ {ℓ} → Explore ℓ A}
    (eᴬ-ind : ∀ {p ℓ} → ExploreInd {ℓ} p eᴬ)
    {b} {B : ★ b}
    {eᴮ : ∀ {ℓ} → Explore ℓ B}
    (eᴮ-ind : ∀ {p ℓ} → ExploreInd {ℓ} p eᴮ)
    where

    module A = FromExploreInd eᴬ-ind
    module B = FromExploreInd eᴮ-ind

    module _ {c ℓ}(cm : CommutativeMonoid c ℓ) where
        open CMon cm

        opᴬ = eᴬ ε _∙_
        opᴮ = eᴮ ε _∙_

        -- TODO use lift-hom
        explore-swap' : ∀ f → opᴬ (opᴮ ∘ f) ≈ opᴮ (opᴬ ∘ flip f)
        explore-swap' = A.explore-swap m (B.explore-ε m) (B.explore-hom cm)

    sum-swap : ∀ f → A.sum (B.sum ∘ f) ≡ B.sum (A.sum ∘ flip f)
    sum-swap = explore-swap' ℕ°.+-commutativeMonoid

module FromTwoAdequate-sum
  {{_ : UA}}{{_ : FunExt}}
  {A}{B}
  {sumᴬ : Sum A}{sumᴮ : Sum B}
  (open Adequacy _≡_)
  (sumᴬ-adq : Adequate-sum sumᴬ)
  (sumᴮ-adq : Adequate-sum sumᴮ) where

  open ≡
  sumStableUnder : (p : A ≃ B)(f : B → ℕ)
                 → sumᴬ (f ∘ ·→ p) ≡ sumᴮ f
  sumStableUnder p f = Fin-injective (sumᴬ-adq (f ∘ ·→ p)
                                      ∙ Σ-fst≃ p _
                                      ∙ ! sumᴮ-adq f)

  sumStableUnder′ : (p : A ≃ B)(f : A → ℕ)
                 → sumᴬ f ≡ sumᴮ (f ∘ <– p)
  sumStableUnder′ p f = Fin-injective (sumᴬ-adq f
                                      ∙ Σ-fst≃′ p _
                                      ∙ ! sumᴮ-adq (f ∘ <– p))

module FromAdequate-sum
  {A}
  {sum : Sum A}
  (open Adequacy _≡_)
  (sum-adq : Adequate-sum sum)
  {{_ : UA}}{{_ : FunExt}}
  where

  open FromTwoAdequate-sum sum-adq sum-adq public
  open ≡

  sum-ext : SumExt sum
  sum-ext = ap sum ∘ λ=

  private
    count : Count A
    count f = sum (𝟚▹ℕ ∘ f)

  private
    module M {p q : A → 𝟚}(same-count : count p ≡ count q) where
      private

        P = λ x → p x ≡ 1₂
        Q = λ x → q x ≡ 1₂
        ¬P = λ x → p x ≡ 0₂
        ¬Q = λ x → q x ≡ 0₂

        π : Σ A P ≡ Σ A Q
        π = ! Σ=′ _ (count-≡ p)
            ∙ ! (sum-adq (𝟚▹ℕ ∘ p))
            ∙ ap Fin same-count
            ∙ sum-adq (𝟚▹ℕ ∘ q)
            ∙ Σ=′ _ (count-≡ q)

        lem1 : ∀ px qx → 𝟚▹ℕ qx ≡ (𝟚▹ℕ (px ∧ qx)) + 𝟚▹ℕ (not px) * 𝟚▹ℕ qx
        lem1 1₂ 1₂ = ≡.refl
        lem1 1₂ 0₂ = ≡.refl
        lem1 0₂ 1₂ = ≡.refl
        lem1 0₂ 0₂ = ≡.refl

        lem2 : ∀ px qx → 𝟚▹ℕ px ≡ (𝟚▹ℕ (px ∧ qx)) + 𝟚▹ℕ px * 𝟚▹ℕ (not qx)
        lem2 1₂ 1₂ = ≡.refl
        lem2 1₂ 0₂ = ≡.refl
        lem2 0₂ 1₂ = ≡.refl
        lem2 0₂ 0₂ = ≡.refl

        lemma1 : ∀ px qx → (qx ≡ 1₂) ≡ (Fin (𝟚▹ℕ (px ∧ qx)) ⊎ (px ≡ 0₂ × qx ≡ 1₂))
        lemma1 px qx = ! Fin-≡-≡1₂ qx
                     ∙ ap Fin (lem1 px qx)
                     ∙ ! Fin-⊎-+
                     ∙ ⊎= refl (! Fin-×-* ∙ ×= (Fin-≡-≡0₂ px) (Fin-≡-≡1₂ qx))

        lemma2 : ∀ px qx → (Fin (𝟚▹ℕ (px ∧ qx)) ⊎ (px ≡ 1₂ × qx ≡ 0₂)) ≡ (px ≡ 1₂)
        lemma2 px qx = ! ⊎= refl (! Fin-×-* ∙ ×= (Fin-≡-≡1₂ px) (Fin-≡-≡0₂ qx)) ∙ Fin-⊎-+ ∙ ap Fin (! lem2 px qx) ∙ Fin-≡-≡1₂ px

        π' : (Fin (sum (λ x → 𝟚▹ℕ (p x ∧ q x))) ⊎ Σ A (λ x →  P x × ¬Q x))
           ≡ (Fin (sum (λ x → 𝟚▹ℕ (p x ∧ q x))) ⊎ Σ A (λ x → ¬P x ×  Q x))
        π' = ⊎= (sum-adq (λ x → 𝟚▹ℕ (p x ∧ q x))) refl
           ∙ ! Σ⊎-split
           ∙ Σ=′ _ (λ x → lemma2 (p x) (q x))
           ∙ π
           ∙ Σ=′ _ (λ x → lemma1 (p x) (q x))
           ∙ Σ⊎-split
           ∙ ! ⊎= (sum-adq (λ x → 𝟚▹ℕ (p x ∧ q x))) refl

        π'' : Σ A (P ×° ¬Q) ≡ Σ A (¬P ×° Q)
        π'' = Fin⊎-injective (sum (λ x → 𝟚▹ℕ (p x ∧ q x))) π'

      open EquivalentSubsets π'' public

  same-count→iso : ∀{p q : A → 𝟚}(same-count : count p ≡ count q) → p ≡ q ∘ M.π {p} {q} same-count
  same-count→iso {p} {q} sc = M.prop {p} {q} sc

module From⟦Explore⟧
    {-a-} {A : ★₀ {- a-}}
    {explore   : ∀ {ℓ} → Explore ℓ A}
    (⟦explore⟧ : ∀ {ℓ₀ ℓ₁} ℓᵣ → ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ _≡_ explore explore)
    {{_ : UA}}
    where
  open FromExplore explore

  module AlsoInFromExploreInd
          {ℓ}(M : Monoid ℓ ℓ)
             (open Mon M)
             (f : A → C)
             where
        explore-endo-monoid-spec′ : ∀ z → explore ε _∙_ f ∙ z ≈ explore-endo explore z _∙_ f
        explore-endo-monoid-spec′ = ⟦explore⟧ ₀ {C} {C → C}
                                              (λ r s → ∀ z → r ∙ z ≈ s z)
                                              (fst identity)
                                              (λ P₀ P₁ z → trans (assoc _ _ _) (trans (∙-cong refl (P₁ z)) (P₀ _)))
                                              (λ xᵣ _ → ∙-cong (reflexive (≡.ap f xᵣ)) refl)

        explore-endo-monoid-spec : with-monoid M f ≈ with-endo-monoid M f
        explore-endo-monoid-spec = trans (! snd identity _) (explore-endo-monoid-spec′ ε)

  open ≡
  module _ (f : A → ℕ) where
    sum⇒Σᵉ : Fin (explore 0 _+_ f) ≡ explore (Lift 𝟘) _⊎_ (Fin ∘ f)
    sum⇒Σᵉ = ⟦explore⟧ {₀} {₁} ₁
                (λ n X → Fin n ≡ X)
                (Fin0≡𝟘 ∙ ! Lift≡id)
                (λ p q → ! Fin-⊎-+ ∙ ⊎= p q)
                (ap (Fin ∘ f))

    product⇒Πᵉ : Fin (explore 1 _*_ f) ≡ explore (Lift 𝟙) _×_ (Fin ∘ f)
    product⇒Πᵉ = ⟦explore⟧ {₀} {₁} ₁
                    (λ n X → Fin n ≡ X)
                    (Fin1≡𝟙 ∙ ! Lift≡id)
                    (λ p q → ! Fin-×-* ∙ ×= p q)
                    (ap (Fin ∘ f))

  module _ (f : A → 𝟚) where
    ✓all-Πᵉ : ✓ (all f) ≡ Πᵉ explore (✓ ∘ f)
    ✓all-Πᵉ = ⟦explore⟧ {₀} {₁} ₁
                (λ b X → ✓ b ≡ X)
                (! Lift≡id)
                (λ p q → ✓-∧-× _ _ ∙ ×= p q)
                (ap (✓ ∘ f))

    ✓any→Σᵉ : ✓ (any f) → Σᵉ explore (✓ ∘ f)
    ✓any→Σᵉ p = ⟦explore⟧ {₀} {ₛ ₀} ₁
                         (λ b (X : ★₀) → Lift (✓ b) → X)
                         (λ x → lift (lower x))
                         (λ { {0₂} {x₁} xᵣ {y₀} {y₁} yᵣ zᵣ → inr (yᵣ zᵣ)
                            ; {1₂} {x₁} xᵣ {y₀} {y₁} yᵣ zᵣ → inl (xᵣ _) })
                         (λ xᵣ x → tr (✓ ∘ f) xᵣ (lower x)) (lift p)

  module FromAdequate-Σᵉ
           (adequate-Σᵉ : ∀ {ℓ} → Adequate-Σ {ℓ} (Σᵉ explore))
          where
    open Adequacy

    adequate-sum : Adequate-sum _≡_ sum
    adequate-sum f = sum⇒Σᵉ f ∙ adequate-Σᵉ (Fin ∘ f)

    open FromAdequate-sum adequate-sum public

    adequate-any : Adequate-any -→- any
    adequate-any f e = coe (adequate-Σᵉ (✓ ∘ f)) (✓any→Σᵉ f e)

  module FromAdequate-Πᵉ
           (adequate-Πᵉ : ∀ {ℓ} → Adequate-Π {ℓ} (Πᵉ explore))
          where
    open Adequacy

    adequate-product : Adequate-product _≡_ product
    adequate-product f = product⇒Πᵉ f ∙ adequate-Πᵉ (Fin ∘ f)

    adequate-all : Adequate-all _≡_ all
    adequate-all f = ✓all-Πᵉ f ∙ adequate-Πᵉ _

    check! : (f : A → 𝟚) {pf : ✓ (all f)} → (∀ x → ✓ (f x))
    check! f {pf} = coe (adequate-all f) pf

{-
module ExplorableRecord where
    record Explorable A : ★₁ where
      constructor mk
      field
        explore     : Explore₀ A
        explore-ind : ExploreInd₀ explore

      open FromExploreInd explore-ind
      field
        adequate-sum     : Adequate-sum sum
    --  adequate-product : AdequateProduct product

      open FromExploreInd explore-ind public

    open Explorable public

    ExploreForFun : ★₀ → ★₁
    ExploreForFun A = ∀ {X} → Explorable X → Explorable (A → X)

    record Funable A : ★₂ where
      constructor _,_
      field
        explorable : Explorable A
        negative   : ExploreForFun A

    module DistFun {A} (μA : Explorable A)
                       (μA→ : ExploreForFun A)
                       {B} (μB : Explorable B){X}
                       (_≈_ : X → X → ★ ₀)
                       (0′  : X)
                       (_+_ : X → X → X)
                       (_*_ : X → X → X) where

      Σᴮ = explore μB 0′ _+_
      Π' = explore μA 0′ _*_
      Σ' = explore (μA→ μB) 0′ _+_

      DistFun = ∀ f → Π' (Σᴮ ∘ f) ≈ Σ' (Π' ∘ _ˢ_ f)

    DistFun : ∀ {A} → Explorable A → ExploreForFun A → ★₁
    DistFun μA μA→ = ∀ {B} (μB : Explorable B) c → let open CMon {₀}{₀} c in
                       ∀ _*_ → Zero _≈_ ε _*_ → _DistributesOver_ _≈_ _*_ _∙_ → _*_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
                       → DistFun.DistFun μA μA→ μB _≈_ ε _∙_ _*_

    DistFunable : ∀ {A} → Funable A → ★₁
    DistFunable (μA , μA→) = DistFun μA μA→

    module _ {{_ : UA}}{{_ : FunExt}} where
        μ-iso : ∀ {A B} → (A ≃ B) → Explorable A → Explorable B
        μ-iso {A}{B} A≃B μA = mk (EM.map _ A→B (explore μA)) (EM.map-ind _ A→B (explore-ind μA)) ade
          where
            open ≡
            A→B = –> A≃B
            ade = λ f → adequate-sum μA (f ∘ A→B) ∙ Σ-fst≃ A≃B _

        -- I guess this could be more general
        μ-iso-preserve : ∀ {A B} (A≃B : A ≃ B) f (μA : Explorable A) → sum μA f ≡ sum (μ-iso A≃B μA) (f ∘ <– A≃B)
        μ-iso-preserve A≃B f μA = sum-ext μA (λ x → ap f (! (<–-inv-l A≃B x)))
          where open ≡

          {-
        μLift : ∀ {A} → Explorable A → Explorable (Lift A)
        μLift = μ-iso {!(! Lift↔id)!}
          where open ≡
          -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Data.Num.Bijective.Properties where

open import Data.Num.Bijective

open import Data.Nat
open import Data.Nat.DM
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)
open import Data.Fin.Extra
open import Data.Fin.Properties         as FinP hiding (_≟_)
    renaming (toℕ-injective to Fin-toℕ-injective)
open import Data.Fin.Properties.Extra   as FinPX
    renaming (cancel-suc to Fin-cancel-suc)

open import Data.Product
open import Function
open import Function.Injection hiding (_∘_)
open import Relation.Nullary
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality as PropEq
open ≡-Reasoning

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

------------------------------------------------------------------------
-- Various ≡-related lemmata
------------------------------------------------------------------------

1+-never-∙ : ∀ {b} xs → 1+ {b} xs ≢ ∙
1+-never-∙     ∙        ()
1+-never-∙ {b} (x ∷ xs) +1xs≡∙ with full x
1+-never-∙     (x ∷ xs) () | yes p
1+-never-∙     (x ∷ xs) () | no ¬p

fromℕ-∙-0 : ∀ {b} n → fromℕ {b} n ≡ ∙ → n ≡ 0
fromℕ-∙-0 zero    p = refl
fromℕ-∙-0 (suc n) p = contradiction p (1+-never-∙ (fromℕ n))

toℕ-∙-0 : ∀ {b} xs → toℕ {suc b} xs ≡ 0 → xs ≡ ∙
toℕ-∙-0 ∙ p = refl
toℕ-∙-0 (x ∷ xs) ()

digit+1-never-0 : ∀ {b} (x : Fin (suc b)) → (¬p : Fin.toℕ x ≢ b) → digit+1 x ¬p ≢ Fin.zero
digit+1-never-0 {b}     x            ¬p eq with Fin.toℕ x ≟ b
digit+1-never-0 {b}     x            ¬p eq | yes q = contradiction q ¬p
digit+1-never-0 {zero}  Fin.zero     ¬p eq | no ¬q = contradiction refl ¬p
digit+1-never-0 {suc b} Fin.zero     ¬p eq | no ¬q = contradiction eq (λ ())
digit+1-never-0 {zero}  (Fin.suc ()) ¬p eq | no ¬q
digit+1-never-0 {suc b} (Fin.suc x)  ¬p () | no ¬q

Fin⇒ℕ-digit+1 : ∀ {b}
    → (x : Fin (suc b))
    → (¬p : Fin.toℕ x ≢ b)
    → Fin.toℕ (digit+1 x ¬p) ≡ suc (Fin.toℕ x)
Fin⇒ℕ-digit+1 {b} x ¬p = toℕ-fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ x) b (bounded x) ¬p))

------------------------------------------------------------------------
-- injectivity
------------------------------------------------------------------------

∷-injective : ∀ {b}
    → {x y : Fin (suc b)}
    → {xs ys : Bij (suc b)}
    → x ∷ xs ≡ y ∷ ys
    → x ≡ y × xs ≡ ys
∷-injective refl = refl , refl

digit+1-injective :  ∀ {b} (x y : Fin (suc b))
    → (¬p : Fin.toℕ x ≢ b)
    → (¬q : Fin.toℕ y ≢ b)
    → digit+1 x ¬p ≡ digit+1 y ¬q
    → x ≡ y
digit+1-injective         Fin.zero     Fin.zero     ¬p ¬q eq = refl
digit+1-injective {zero}  Fin.zero     (Fin.suc ()) ¬p ¬q eq
digit+1-injective {suc b} Fin.zero     (Fin.suc y)  ¬p ¬q eq = Fin-toℕ-injective (cancel-suc eq')
    where   eq' : Fin.toℕ {suc (suc b)} (digit+1 Fin.zero ¬p) ≡ suc (Fin.toℕ {suc (suc b)} (Fin.suc y))
            eq' = begin
                    Fin.toℕ {suc (suc b)} (Fin.suc Fin.zero)
                ≡⟨ cong Fin.toℕ eq ⟩
                    suc (Fin.toℕ (Fin.fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ y) b (bounded y) (¬q ∘ cong suc)))))
                ≡⟨ cong suc (toℕ-fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ y) b (bounded y) (¬q ∘ cong suc)))) ⟩
                    suc (Fin.toℕ {suc (suc b)} (Fin.suc y))
                ∎
digit+1-injective {zero}  (Fin.suc ()) Fin.zero    ¬p ¬q eq
digit+1-injective {suc b} (Fin.suc x)  Fin.zero    ¬p ¬q eq = Fin-toℕ-injective (cancel-suc eq')
    where   eq' : suc (Fin.toℕ {suc (suc b)} (Fin.suc x)) ≡ Fin.toℕ {suc (suc b)} (digit+1 Fin.zero ¬q)
            eq' = begin
                    suc (Fin.toℕ {suc (suc b)} (Fin.suc x))
                ≡⟨ cong suc (sym (toℕ-fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ x) b (bounded x) (¬p ∘ cong suc))))) ⟩
                    suc (Fin.toℕ (Fin.fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ x) b (bounded x) (¬p ∘ cong suc)))))
                ≡⟨ cong Fin.toℕ eq ⟩
                    Fin.toℕ {suc (suc b)} (Fin.suc Fin.zero)
                ∎
digit+1-injective {zero}  (Fin.suc ()) (Fin.suc y) ¬p ¬q eq
digit+1-injective {suc b} (Fin.suc x)  (Fin.suc y) ¬p ¬q eq = cong Fin.suc (digit+1-injective x y (¬p ∘ cong suc) (¬q ∘ cong suc) (Fin-cancel-suc eq))
    where   open import Data.Fin.Properties.Extra

1+-injective : ∀ b → (xs ys : Bij (suc b)) → 1+ xs ≡ 1+ ys → xs ≡ ys
1+-injective b ∙        ∙        eq = refl
1+-injective b ∙        (y ∷ ys) eq with full y
1+-injective b ∙        (y ∷ ys) eq | yes p = contradiction (proj₂ (∷-injective (sym eq))) (1+-never-∙ ys)
1+-injective b ∙        (y ∷ ys) eq | no ¬p = contradiction (proj₁ (∷-injective (sym eq))) (digit+1-never-0 y ¬p)
1+-injective b (x ∷ xs) ∙        eq with full x
1+-injective b (x ∷ xs) ∙        eq | yes p = contradiction (proj₂ (∷-injective eq)) (1+-never-∙ xs)
1+-injective b (x ∷ xs) ∙        eq | no ¬p = contradiction (proj₁ (∷-injective eq)) (digit+1-never-0 x ¬p)
1+-injective b (x ∷ xs) (y ∷ ys) eq with full x | full y
1+-injective b (x ∷ xs) (y ∷ ys) eq | yes p | yes q = cong₂ _∷_ x≡y xs≡ys
    where
            x≡y : x ≡ y
            x≡y = Fin-toℕ-injective (trans p (sym q))
            xs≡ys : xs ≡ ys
            xs≡ys = 1+-injective b xs ys (proj₂ (∷-injective eq))
1+-injective b (x ∷ xs) (y ∷ ys) eq | yes p | no ¬q = contradiction (sym (proj₁ (∷-injective eq))) (digit+1-never-0 y ¬q)
1+-injective b (x ∷ xs) (y ∷ ys) eq | no ¬p | yes q = contradiction (proj₁ (∷-injective eq))       (digit+1-never-0 x ¬p)
1+-injective b (x ∷ xs) (y ∷ ys) eq | no ¬p | no ¬q = cong₂ _∷_ (digit+1-injective x y ¬p ¬q (proj₁ (∷-injective eq))) (proj₂ (∷-injective eq))

toℕ-injective : ∀ {b} → (xs ys : Bij (suc b)) → toℕ xs ≡ toℕ ys → xs ≡ ys
toℕ-injective ∙        ∙        eq = refl
toℕ-injective ∙        (y ∷ ys) ()
toℕ-injective (x ∷ xs) ∙        ()
toℕ-injective (x ∷ xs) (y ∷ ys) eq =
    cong₂ _∷_ (proj₁ ind) (toℕ-injective xs ys (proj₂ ?))
    where
            ind : x ≡ y × toℕ xs ≡ toℕ ys
            ind = some-lemma x y (toℕ xs) (toℕ ys) (cancel-suc eq)

fromℕ-injective : ∀ b m n → fromℕ {b} m ≡ fromℕ {b} n → m ≡ n
fromℕ-injective b zero    zero    eq = refl
fromℕ-injective b zero    (suc n) eq = contradiction (sym eq) (1+-never-∙ (fromℕ n))
fromℕ-injective b (suc m) zero    eq = contradiction eq       (1+-never-∙ (fromℕ m))
fromℕ-injective b (suc m) (suc n) eq = cong suc (fromℕ-injective b m n (1+-injective b (fromℕ m) (fromℕ n) eq))

--
--      xs ─── 1+ ──➞ 1+ xs
--      |                |
--     toℕ              toℕ
--      ↓                ↓
--      n ─── suc ──➞ suc n
--
toℕ-1+ : ∀ b xs → toℕ {suc b} (1+ xs) ≡ suc (toℕ xs)
toℕ-1+ b ∙        = refl
toℕ-1+ b (x ∷ xs) with full x
toℕ-1+ b (x ∷ xs) | yes p =
    begin
        toℕ (Fin.zero ∷ 1+ xs)
    ≡⟨ cong (λ w → suc (w * suc b)) (toℕ-1+ b xs) ⟩
        suc (suc (b + toℕ xs * suc b))
    ≡⟨ cong (λ w → suc (suc (w + toℕ xs * suc b))) (sym p) ⟩
        suc (toℕ (x ∷ xs))
    ∎
toℕ-1+ b (x ∷ xs) | no ¬p =
    cong (λ w → suc w + toℕ xs * suc b) (toℕ-fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ x) b (bounded x) ¬p)))

--
--      xs ── n+ n ──➞ n+ n xs
--      |                  |
--     toℕ               toℕ
--      ↓                  ↓
--      m ──   n + ──➞ n + m
--

toℕ-n+ : ∀ b n xs → toℕ {suc b} (n+ n xs) ≡ n + (toℕ xs)
toℕ-n+ b zero xs = refl
toℕ-n+ b (suc n) xs = begin
        toℕ (1+ (n+ n xs))
    ≡⟨ toℕ-1+ b (n+ n xs) ⟩
        suc (toℕ (n+ n xs))
    ≡⟨ cong suc (toℕ-n+ b n xs) ⟩
        suc (n + toℕ xs)
    ∎

toℕ-fromℕ : ∀ b n → toℕ {suc b} (fromℕ {b} n) ≡ n
toℕ-fromℕ b zero    = refl
toℕ-fromℕ b (suc n) with fromℕ {b} n | inspect (fromℕ {b}) n
toℕ-fromℕ b (suc n) | ∙      | [ eq ] = cong suc (sym (fromℕ-∙-0 n eq))
toℕ-fromℕ b (suc n) | x ∷ xs | [ eq ] with full x
toℕ-fromℕ b (suc n) | x ∷ xs | [ eq ] | yes p =
    begin
        toℕ (Fin.zero ∷ 1+ xs)
    ≡⟨ refl ⟩
        suc (toℕ (1+ xs) * suc b)
    ≡⟨ cong (λ w → suc (w * suc b)) (toℕ-1+ b xs) ⟩
        suc (suc (b + toℕ xs * suc b))
    ≡⟨ cong (λ w → suc (suc (w + toℕ xs * suc b))) (sym p) ⟩
        suc (suc (Fin.toℕ x) + toℕ xs * suc b)
    ≡⟨ cong (λ w → suc (toℕ w)) (sym eq) ⟩
        suc (toℕ (fromℕ n))
    ≡⟨ cong suc (toℕ-fromℕ b n) ⟩
        suc n
    ∎
toℕ-fromℕ b (suc n) | x ∷ xs | [ eq ] | no ¬p =
    begin
        toℕ (digit+1 x ¬p ∷ xs)
    ≡⟨ cong (λ w → suc (w + toℕ xs * suc b)) (toℕ-fromℕ≤ (s≤s (digit+1-lemma (Fin.toℕ x) b (bounded x) ¬p))) ⟩
        suc (suc (Fin.toℕ x + toℕ xs * suc b))
    ≡⟨ cong (λ w → suc (toℕ w)) (sym eq) ⟩
        suc (toℕ (fromℕ n))
    ≡⟨ cong suc (toℕ-fromℕ b n) ⟩
        suc n
    ∎

fromℕ-toℕ : ∀ {b} xs → fromℕ {b} (toℕ {suc b} xs) ≡ xs
fromℕ-toℕ {b} xs = toℕ-injective (fromℕ (toℕ xs)) xs (toℕ-fromℕ b (toℕ xs))

toℕ-fromℕ-reverse : ∀ b {m} {n} → toℕ (fromℕ {b} m) ≡ n → m ≡ n
toℕ-fromℕ-reverse b {m} {n} eq = begin
        m
    ≡⟨ sym (toℕ-fromℕ b m) ⟩
        toℕ (fromℕ m)
    ≡⟨ eq ⟩
        n
    ∎

fromℕ-toℕ-reverse : ∀ b {xs} {ys} → fromℕ {b} (toℕ {suc b} xs) ≡ ys → xs ≡ ys
fromℕ-toℕ-reverse b {xs} {ys} eq = begin
        xs
    ≡⟨ sym (fromℕ-toℕ xs) ⟩
        fromℕ (toℕ xs)
    ≡⟨ eq ⟩
        ys
    ∎

------------------------------------------------------------------------
-- surjectivity
------------------------------------------------------------------------

toℕ-surjective : ∀ b n → Σ[ xs ∈ Bij (suc b) ] toℕ xs ≡ n
toℕ-surjective b zero    = ∙               , refl
toℕ-surjective b (suc n) = (fromℕ (suc n)) , toℕ-fromℕ b (suc n)

fromℕ-surjective : ∀ {b} (xs : Bij (suc b)) → Σ[ n ∈ ℕ ] fromℕ n ≡ xs
fromℕ-surjective ∙ = zero , refl
fromℕ-surjective (x ∷ xs) = toℕ (x ∷ xs) , fromℕ-toℕ (x ∷ xs)

------------------------------------------------------------------------
-- _⊹_
------------------------------------------------------------------------

toℕ-⊹-homo : ∀ {b} (xs ys : Bij (suc b)) → toℕ (xs ⊹ ys) ≡ toℕ xs + toℕ ys
toℕ-⊹-homo {b} ∙        ys       = refl
toℕ-⊹-homo {b} (x ∷ xs) ∙        = sym (+-right-identity (suc (Fin.toℕ x + toℕ xs * suc b)))
toℕ-⊹-homo {b} (x ∷ xs) (y ∷ ys) with suc (Fin.toℕ x + Fin.toℕ y) divMod (suc b)
toℕ-⊹-homo {b} (x ∷ xs) (y ∷ ys) | result quotient remainder property div-eq mod-eq
    rewrite div-eq | mod-eq
    = begin
            suc (Fin.toℕ remainder + toℕ (n+ quotient (xs ⊹ ys)) * suc b)
        -- apply "toℕ-n+" to remove "n+"
        ≡⟨ cong (λ w → suc (Fin.toℕ remainder + w * suc b)) (toℕ-n+ b quotient (xs ⊹ ys)) ⟩
            suc (Fin.toℕ remainder + (quotient + toℕ (xs ⊹ ys)) * suc b)
        -- the induction hypothesis
        ≡⟨ cong (λ w → suc (Fin.toℕ remainder + (quotient + w) * suc b)) (toℕ-⊹-homo xs ys) ⟩
            suc (Fin.toℕ remainder + (quotient + (toℕ xs + toℕ ys)) * suc b)
        ≡⟨ cong (λ w → suc (Fin.toℕ remainder) + w) (distribʳ-*-+ (suc b) quotient (toℕ xs + toℕ ys)) ⟩
            suc (Fin.toℕ remainder + (quotient * suc b + (toℕ xs + toℕ ys) * suc b))
        ≡⟨ cong suc (sym (+-assoc (Fin.toℕ remainder) (quotient * suc b) ((toℕ xs + toℕ ys) * suc b))) ⟩
            suc (Fin.toℕ remainder + quotient * suc b + (toℕ xs + toℕ ys) * suc b)
        -- apply "property"
        ≡⟨ cong (λ w → suc (w + (toℕ xs + toℕ ys) * suc b)) (sym property) ⟩
            suc (suc (Fin.toℕ x + Fin.toℕ y + (toℕ xs + toℕ ys) * suc b))
        ≡⟨ cong (λ w → suc (suc (Fin.toℕ x + Fin.toℕ y + w))) (distribʳ-*-+ (suc b) (toℕ xs) (toℕ ys)) ⟩
            suc (suc (Fin.toℕ x + Fin.toℕ y + (toℕ xs * suc b + toℕ ys * suc b)))
        ≡⟨ cong (λ w → suc (suc w)) (+-assoc (Fin.toℕ x) (Fin.toℕ y) (toℕ xs * suc b + toℕ ys * suc b)) ⟩
            suc (suc (Fin.toℕ x + (Fin.toℕ y + (toℕ xs * suc b + toℕ ys * suc b))))
        ≡⟨ cong (λ w → suc (suc (Fin.toℕ x + w))) (sym (+-assoc (Fin.toℕ y) (toℕ xs * suc b) (toℕ ys * suc b))) ⟩
            suc (suc (Fin.toℕ x + (Fin.toℕ y + toℕ xs * suc b + toℕ ys * suc b)))
        ≡⟨ cong (λ w → suc (suc (Fin.toℕ x + (w + toℕ ys * suc b)))) (+-comm (Fin.toℕ y) (toℕ xs * suc b)) ⟩
            suc (suc (Fin.toℕ x + (toℕ xs * suc b + Fin.toℕ y + toℕ ys * suc b)))
        ≡⟨ cong (λ w → suc (suc (Fin.toℕ x + w))) (+-assoc (toℕ xs * suc b) (Fin.toℕ y) (toℕ ys * suc b)) ⟩
            suc (suc (Fin.toℕ x + (toℕ xs * suc b + (Fin.toℕ y + toℕ ys * suc b))))
        ≡⟨ cong (λ w → suc (suc w)) (sym (+-assoc (Fin.toℕ x) (toℕ xs * suc b) (Fin.toℕ y + toℕ ys * suc b))) ⟩
            suc (suc ((Fin.toℕ x + toℕ xs * suc b) + (Fin.toℕ y + toℕ ys * suc b)))
        ≡⟨ cong suc (sym (+-suc (Fin.toℕ x + toℕ xs * suc b) (Fin.toℕ y + toℕ ys * suc b))) ⟩
            suc (Fin.toℕ x + toℕ xs * suc b + suc (Fin.toℕ y + toℕ ys * suc b))
        ≡⟨ refl ⟩
            toℕ (x ∷ xs) + toℕ (y ∷ ys)
        ∎

fromℕ-⊹-homo : ∀ {b} (m n : ℕ) → fromℕ {b} (m + n) ≡ fromℕ m ⊹ fromℕ n
fromℕ-⊹-homo {b} m n = toℕ-injective (fromℕ (m + n)) (fromℕ m ⊹ fromℕ n) $
    begin
        toℕ (fromℕ (m + n))
    ≡⟨ toℕ-fromℕ b (m + n) ⟩
        m + n
    ≡⟨ sym (cong₂ _+_ (toℕ-fromℕ b m) (toℕ-fromℕ b n)) ⟩
        toℕ (fromℕ m) + toℕ (fromℕ n)
    ≡⟨ sym (toℕ-⊹-homo (fromℕ m) (fromℕ n)) ⟩
        toℕ (fromℕ m ⊹ fromℕ n)
    ∎

⊹-1+ : ∀ {b} (xs ys : Bij (suc b)) → (1+ xs) ⊹ ys ≡ 1+ (xs ⊹ ys)
⊹-1+ {b} xs ys = toℕ-injective (1+ xs ⊹ ys) (1+ (xs ⊹ ys)) $
    begin
        toℕ (1+ xs ⊹ ys)
    ≡⟨ toℕ-⊹-homo (1+ xs) ys ⟩
        toℕ (1+ xs) + toℕ ys
    ≡⟨ cong (λ w → w + toℕ ys) (toℕ-1+ b xs) ⟩
        suc (toℕ xs + toℕ ys)
    ≡⟨ cong suc (sym (toℕ-⊹-homo xs ys)) ⟩
        suc (toℕ (xs ⊹ ys))
    ≡⟨ sym (toℕ-1+ b (xs ⊹ ys)) ⟩
        toℕ (1+ (xs ⊹ ys))
    ∎

⊹-assoc : ∀ {b} (xs ys zs : Bij (suc b)) → (xs ⊹ ys) ⊹ zs ≡ xs ⊹ (ys ⊹ zs)
⊹-assoc xs ys zs = toℕ-injective (xs ⊹ ys ⊹ zs) (xs ⊹ (ys ⊹ zs)) $
    begin
        toℕ (xs ⊹ ys ⊹ zs)
    ≡⟨ toℕ-⊹-homo (xs ⊹ ys) zs ⟩
        toℕ (xs ⊹ ys) + toℕ zs
    ≡⟨ cong (λ w → w + toℕ zs) (toℕ-⊹-homo xs ys) ⟩
        toℕ xs + toℕ ys + toℕ zs
    ≡⟨ +-assoc (toℕ xs) (toℕ ys) (toℕ zs) ⟩
        toℕ xs + (toℕ ys + toℕ zs)
    ≡⟨ cong (λ w → toℕ xs + w) (sym (toℕ-⊹-homo ys zs)) ⟩
        toℕ xs + toℕ (ys ⊹ zs)
    ≡⟨ sym (toℕ-⊹-homo xs (ys ⊹ zs)) ⟩
        toℕ (xs ⊹ (ys ⊹ zs))
    ∎

⊹-comm : ∀ {b} (xs ys : Bij (suc b)) → xs ⊹ ys ≡ ys ⊹ xs
⊹-comm xs ys = toℕ-injective (xs ⊹ ys) (ys ⊹ xs) $
    begin
        toℕ (xs ⊹ ys)
    ≡⟨ toℕ-⊹-homo xs ys ⟩
        toℕ xs + toℕ ys
    ≡⟨ +-comm (toℕ xs) (toℕ ys) ⟩
        toℕ ys + toℕ xs
    ≡⟨ sym (toℕ-⊹-homo ys xs) ⟩
        toℕ (ys ⊹ xs)
    ∎

increase-base-lemma : ∀ b
    → (xs : Bij (suc b))
    → toℕ (increase-base xs) ≡ toℕ xs
increase-base-lemma b ∙ = refl
increase-base-lemma b (x ∷ xs) with fromℕ {suc b} (toℕ (increase-base xs) * suc b) | inspect (λ ws → fromℕ {suc b} (toℕ ws * suc b)) (increase-base xs)
increase-base-lemma b (x ∷ xs) | ∙      | [ eq ] = cong suc $
    begin
        Fin.toℕ (Fin.inject₁ x) + 0
    ≡⟨ cong (λ w → w + 0) (FinP.inject₁-lemma x) ⟩
        Fin.toℕ x + 0
    ≡⟨ cong (λ w → Fin.toℕ x + w) $
            begin
                zero
            ≡⟨ cong toℕ (sym eq) ⟩
                toℕ (fromℕ (toℕ (increase-base xs) * suc b))
            ≡⟨ toℕ-fromℕ (suc b) (toℕ (increase-base xs) * suc b) ⟩
                toℕ (increase-base xs) * suc b
            ∎ ⟩
        Fin.toℕ x + toℕ (increase-base xs) * suc b
    ≡⟨ cong (λ w → Fin.toℕ x + w * suc b) (increase-base-lemma b xs) ⟩
        Fin.toℕ x + toℕ xs * suc b
    ∎
increase-base-lemma b (x ∷ xs) | y ∷ ys | [ eq ] with (suc (Fin.toℕ x + Fin.toℕ y)) divMod (suc (suc b))
increase-base-lemma b (x ∷ xs) | y ∷ ys | [ eq ] | result quotient remainder property div-eq mod-eq
    rewrite div-eq | mod-eq
    = cong suc $ begin
            Fin.toℕ remainder + toℕ (n+ quotient ys) * suc (suc b)
        ≡⟨ cong (λ w → Fin.toℕ remainder + w * suc (suc b)) (toℕ-n+ (suc b) quotient ys) ⟩
            Fin.toℕ remainder + (quotient + toℕ ys) * suc (suc b)
        ≡⟨ cong (λ w → Fin.toℕ remainder + w) (distribʳ-*-+ (suc (suc b)) quotient (toℕ ys)) ⟩
            Fin.toℕ remainder + (quotient * suc (suc b) + toℕ ys * suc (suc b))
        ≡⟨ sym (+-assoc (Fin.toℕ remainder) (quotient * suc (suc b)) (toℕ ys * suc (suc b))) ⟩
            Fin.toℕ remainder + quotient * suc (suc b) + toℕ ys * suc (suc b)
        ≡⟨ cong (λ w → w + toℕ ys * suc (suc b)) (sym property) ⟩
            suc (Fin.toℕ x + Fin.toℕ y + toℕ ys * suc (suc b))
        ≡⟨ cong suc (+-assoc (Fin.toℕ x) (Fin.toℕ y) (toℕ ys * suc (suc b))) ⟩
            suc (Fin.toℕ x + (Fin.toℕ y + toℕ ys * suc (suc b)))
        ≡⟨ sym (+-suc (Fin.toℕ x) (Fin.toℕ y + toℕ ys * suc (suc b))) ⟩
            Fin.toℕ x + suc (Fin.toℕ y + toℕ ys * suc (suc b))
        ≡⟨ cong (λ w → Fin.toℕ x + toℕ w) (sym eq) ⟩
            Fin.toℕ x + toℕ (fromℕ (toℕ (increase-base xs) * suc b))
        ≡⟨ cong (λ w → Fin.toℕ x + w) (toℕ-fromℕ (suc b) (toℕ (increase-base xs) * suc b)) ⟩
            Fin.toℕ x + toℕ (increase-base xs) * suc b
        ≡⟨ cong (λ w → Fin.toℕ x + w * suc b) (increase-base-lemma b xs) ⟩
            Fin.toℕ x + toℕ xs * suc b
        ∎

decrease-base-lemma : ∀ b → (xs : Bij (suc (suc b))) → toℕ (decrease-base xs) ≡ toℕ xs
decrease-base-lemma b ∙ = refl
decrease-base-lemma b (x ∷ xs) with fromℕ {b} (toℕ (decrease-base xs) * suc (suc b))
              | inspect (λ ws → fromℕ {b} (toℕ ws * suc (suc b))) (decrease-base xs)
decrease-base-lemma b (x ∷ xs) | ∙ | [ eq ] with full x
decrease-base-lemma b (x ∷ xs) | ∙ | [ eq ] | yes p = cong suc $
    begin
        suc (b + 0)
    ≡⟨ cong (λ w → w + 0) (sym p)⟩
        Fin.toℕ x + zero
    ≡⟨ cong (λ w → Fin.toℕ x + w) $
            begin
                zero
            ≡⟨ cong toℕ (sym eq) ⟩
                toℕ (fromℕ (toℕ (decrease-base xs) * suc (suc b)))
            ≡⟨ toℕ-fromℕ b (toℕ (decrease-base xs) * suc (suc b)) ⟩
                toℕ (decrease-base xs) * suc (suc b)
            ∎ ⟩
        Fin.toℕ x + toℕ (decrease-base xs) * suc (suc b)
    ≡⟨ cong (λ w → Fin.toℕ x + w * suc (suc b)) (decrease-base-lemma b xs) ⟩
        Fin.toℕ x + toℕ xs * suc (suc b)
    ∎
decrease-base-lemma b (x ∷ xs) | ∙ | [ eq ] | no ¬p = cong suc $
    begin
        Fin.toℕ (inject-1 x ¬p) + 0
    ≡⟨ cong (λ w → w + 0) (inject-1-lemma x ¬p) ⟩
        Fin.toℕ x + 0
    ≡⟨ cong (λ w → Fin.toℕ x + w) $
            begin
                zero
            ≡⟨ cong toℕ (sym eq) ⟩
                toℕ (fromℕ (toℕ (decrease-base xs) * suc (suc b)))
            ≡⟨ toℕ-fromℕ b (toℕ (decrease-base xs) * suc (suc b)) ⟩
                toℕ (decrease-base xs) * suc (suc b)
            ∎ ⟩
        Fin.toℕ x + toℕ (decrease-base xs) * suc (suc b)
    ≡⟨ cong (λ w → Fin.toℕ x + w * suc (suc b)) (decrease-base-lemma b xs) ⟩
        Fin.toℕ x + toℕ xs * suc (suc b)
    ∎
decrease-base-lemma b (x ∷ xs) | y ∷ ys | [ eq ] with (suc (Fin.toℕ x + Fin.toℕ y)) divMod (suc b)
decrease-base-lemma b (x ∷ xs) | y ∷ ys | [ eq ] | result quotient remainder property div-eq mod-eq
    rewrite div-eq | mod-eq = cong suc $ begin
            Fin.toℕ remainder + toℕ (n+ quotient ys) * suc b
        ≡⟨ cong (λ w → Fin.toℕ remainder + w * suc b) (toℕ-n+ b quotient ys) ⟩
            Fin.toℕ remainder + (quotient + toℕ ys) * suc b
        ≡⟨ cong (λ w → Fin.toℕ remainder + w) (distribʳ-*-+ (suc b) quotient (toℕ ys)) ⟩
            Fin.toℕ remainder + (quotient * suc b + toℕ ys * suc b)
        ≡⟨ sym (+-assoc (Fin.toℕ remainder) (quotient * suc b) (toℕ ys * suc b)) ⟩
            Fin.toℕ remainder + quotient * suc b + toℕ ys * suc b
        ≡⟨ cong (λ w → w + toℕ ys * suc b) (sym property) ⟩
            suc (Fin.toℕ x + Fin.toℕ y + toℕ ys * suc b)
        ≡⟨ cong suc (+-assoc (Fin.toℕ x) (Fin.toℕ y) (toℕ ys * suc b)) ⟩
            suc (Fin.toℕ x + (Fin.toℕ y + toℕ ys * suc b))
        ≡⟨ sym (+-suc (Fin.toℕ x) (Fin.toℕ y + toℕ ys * suc b)) ⟩
            Fin.toℕ x + suc (Fin.toℕ y + toℕ ys * suc b)
        ≡⟨ cong (λ w → Fin.toℕ x + toℕ w) (sym eq) ⟩
            Fin.toℕ x + toℕ (fromℕ (toℕ (decrease-base xs) * suc (suc b)))
        ≡⟨ cong (λ w → Fin.toℕ x + w) (toℕ-fromℕ b (toℕ (decrease-base xs) * suc (suc b))) ⟩
            Fin.toℕ x + toℕ (decrease-base xs) * suc (suc b)
        ≡⟨ cong (λ w → Fin.toℕ x + w * suc (suc b)) (decrease-base-lemma b xs) ⟩
            Fin.toℕ x + toℕ xs * suc (suc b)
        ∎

    -- begin
    --     {!   !}
    -- ≡⟨ {!   !} ⟩
    --     {!   !}
    -- ≡⟨ {!   !} ⟩
    --     {!   !}
    -- ≡⟨ {!   !} ⟩
    --     {!   !}
    -- ≡⟨ {!   !} ⟩
    --     {!   !}
    -- ∎

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Andreas, 2011-04-11 adapted from Data.Nat.Properties

module FrozenMVar2 where

open import Common.Level
open import Common.Equality

Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Rel A ℓ = A → A → Set ℓ

Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
Op₂ A = A → A → A

module FunctionProperties
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

  Associative : Op₂ A → Set _
  Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

open FunctionProperties _≡_  -- THIS produces frozen metas

data ℕ : Set where
  zℕ : ℕ
  sℕ : (n : ℕ) → ℕ

infixl 6 _+_

_+_ : ℕ → ℕ → ℕ
zℕ   + n = n
sℕ m + n = sℕ (m + n)

+-assoc : Associative _+_
-- +-assoc : ∀ x y z -> ((x + y) + z) ≡ (x + (y + z)) -- this works
+-assoc zℕ     _ _ = refl
+-assoc (sℕ m) n o = cong sℕ (+-assoc m n o)
-- Due to a frozen meta we get:
-- Type mismatch when checking that the pattern zℕ has type _95

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Primitive

Type : (i : Level) → Set (lsuc i)
Type i = Set i

postulate
  T : (i : Level) (A : Type i) → Set

-- Give 'T lzero ?', then give '? → ?'.
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Rules/Term.hs:178
Bug : Set
Bug = {!T lzero ?!}

-- Now: Failed to give (? → ?)
-- Ideally, this should succeed.


text:
{-# OPTIONS --without-K #-}
module pointed where

open import pointed.core public
open import pointed.equality public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- List-related properties
------------------------------------------------------------------------

-- Note that the lemmas below could be generalised to work with other
-- equalities than _≡_.

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

module Data.List.Properties where

open import Algebra
import Algebra.Structures as Structures
import Algebra.FunctionProperties as FunctionProperties
open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
open import Data.Fin using (Fin; zero; suc; cast; toℕ)
open import Data.List as List
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod hiding (map; zip)
open import Data.These as These using (These; this; that; these)
open import Function
import Relation.Binary as B
import Relation.Binary.Reasoning.Setoid as EqR
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; _≗_; refl ; sym ; cong)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Unary using (Pred; Decidable; ∁)
open import Relation.Unary.Properties using (∁?)

------------------------------------------------------------------------
-- _∷_

module _ {a} {A : Set a} {x y : A} {xs ys : List A} where

 ∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
 ∷-injective refl = (refl , refl)

 ∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y
 ∷-injectiveˡ refl = refl

 ∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys
 ∷-injectiveʳ refl = refl

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

  ≡-dec : B.Decidable _≡_ → B.Decidable {A = List A} _≡_
  ≡-dec _≟_ []       []       = yes refl
  ≡-dec _≟_ (x ∷ xs) []       = no λ()
  ≡-dec _≟_ []       (y ∷ ys) = no λ()
  ≡-dec _≟_ (x ∷ xs) (y ∷ ys) with x ≟ y | ≡-dec _≟_ xs ys
  ... | no  x≢y  | _        = no (x≢y   ∘ ∷-injectiveˡ)
  ... | yes _    | no xs≢ys = no (xs≢ys ∘ ∷-injectiveʳ)
  ... | yes refl | yes refl = yes refl

------------------------------------------------------------------------
-- map

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

  map-id : map id ≗ id {A = List A}
  map-id []       = refl
  map-id (x ∷ xs) = P.cong (x ∷_) (map-id xs)

  map-id₂ : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
  map-id₂ []         = refl
  map-id₂ (fx≡x ∷ pxs) = P.cong₂ _∷_ fx≡x (map-id₂ pxs)

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

  map-++-commute : ∀ (f : A → B) xs ys →
                   map f (xs ++ ys) ≡ map f xs ++ map f ys
  map-++-commute f []       ys = refl
  map-++-commute f (x ∷ xs) ys = P.cong (f x ∷_) (map-++-commute f xs ys)

  map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
  map-cong f≗g []       = refl
  map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

  map-cong₂ : ∀ {f g : A → B} {xs} →
              All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
  map-cong₂ []                = refl
  map-cong₂ (fx≡gx ∷ fxs≡gxs) = P.cong₂ _∷_ fx≡gx (map-cong₂ fxs≡gxs)

  length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs
  length-map f []       = refl
  length-map f (x ∷ xs) = P.cong suc (length-map f xs)

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

  map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
  map-compose []       = refl
  map-compose (x ∷ xs) = P.cong (_ ∷_) (map-compose xs)

------------------------------------------------------------------------
-- mapMaybe

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

  mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
  mapMaybe-just []       = refl
  mapMaybe-just (x ∷ xs) = P.cong (x ∷_) (mapMaybe-just xs)

  mapMaybe-nothing : (xs : List A) →
                     mapMaybe {B = A} (λ _ → nothing) xs ≡ []
  mapMaybe-nothing []       = refl
  mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs

module _ {a b} {A : Set a} {B : Set b} (f : A → Maybe B) where

  mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
  mapMaybe-concatMap [] = refl
  mapMaybe-concatMap (x ∷ xs) with f x
  ... | just y  = P.cong (y ∷_) (mapMaybe-concatMap xs)
  ... | nothing = mapMaybe-concatMap xs

  length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
  length-mapMaybe []       = z≤n
  length-mapMaybe (x ∷ xs) with f x
  ... | just y  = s≤s (length-mapMaybe xs)
  ... | nothing = ≤-step (length-mapMaybe xs)

------------------------------------------------------------------------
-- _++_

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

  length-++ : ∀ (xs : List A) {ys} → length (xs ++ ys) ≡ length xs + length ys
  length-++ []       = refl
  length-++ (x ∷ xs) = P.cong suc (length-++ xs)

  open FunctionProperties {A = List A} _≡_

  ++-assoc : Associative _++_
  ++-assoc []       ys zs = refl
  ++-assoc (x ∷ xs) ys zs = P.cong (x ∷_) (++-assoc xs ys zs)

  ++-identityˡ : LeftIdentity [] _++_
  ++-identityˡ xs = refl

  ++-identityʳ : RightIdentity [] _++_
  ++-identityʳ []       = refl
  ++-identityʳ (x ∷ xs) = P.cong (x ∷_) (++-identityʳ xs)

  ++-identity : Identity [] _++_
  ++-identity = ++-identityˡ , ++-identityʳ

  ++-identityʳ-unique : ∀ (xs : List A) {ys} → xs ≡ xs ++ ys → ys ≡ []
  ++-identityʳ-unique []       refl = refl
  ++-identityʳ-unique (x ∷ xs) eq   =
    ++-identityʳ-unique xs (proj₂ (∷-injective eq))

  ++-identityˡ-unique : ∀ {xs} (ys : List A) → xs ≡ ys ++ xs → ys ≡ []
  ++-identityˡ-unique               []       _  = refl
  ++-identityˡ-unique {xs = []}     (y ∷ ys) ()
  ++-identityˡ-unique {xs = x ∷ xs} (y ∷ ys) eq
    with ++-identityˡ-unique (ys ++ [ x ]) (begin
         xs                  ≡⟨ proj₂ (∷-injective eq) ⟩
         ys ++ x ∷ xs        ≡⟨ P.sym (++-assoc ys [ x ] xs) ⟩
         (ys ++ [ x ]) ++ xs ∎)
    where open P.≡-Reasoning
  ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
  ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()

  ++-cancelˡ : ∀ xs {ys zs : List A} → xs ++ ys ≡ xs ++ zs → ys ≡ zs
  ++-cancelˡ []       ys≡zs             = ys≡zs
  ++-cancelˡ (x ∷ xs) x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)

  ++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≡ zs ++ xs → ys ≡ zs
  ++-cancelʳ []       []       _             = refl
  ++-cancelʳ {xs} []           (z ∷ zs) eq =
    contradiction (P.trans (cong length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
  ++-cancelʳ {xs} (y ∷ ys) []       eq =
    contradiction (P.trans (P.sym (length-++ (y ∷ ys))) (cong length eq)) (m≢1+n+m (length xs) ∘ sym)
  ++-cancelʳ (y ∷ ys) (z ∷ zs) eq =
    P.cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ ys zs (∷-injectiveʳ eq))

  ++-cancel : Cancellative _++_
  ++-cancel = ++-cancelˡ , ++-cancelʳ

  ++-conicalˡ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → xs ≡ []
  ++-conicalˡ []       _ refl = refl
  ++-conicalˡ (x ∷ xs) _ ()

  ++-conicalʳ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → ys ≡ []
  ++-conicalʳ []       _ refl = refl
  ++-conicalʳ (x ∷ xs) _ ()

  ++-conical : Conical [] _++_
  ++-conical = ++-conicalˡ , ++-conicalʳ

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

  open Structures {A = List A} _≡_

  ++-isMagma : IsMagma _++_
  ++-isMagma = record
    { isEquivalence = P.isEquivalence
    ; ∙-cong        = P.cong₂ _++_
    }

  ++-isSemigroup : IsSemigroup _++_
  ++-isSemigroup = record
    { isMagma = ++-isMagma
    ; assoc   = ++-assoc
    }

  ++-isMonoid : IsMonoid _++_ []
  ++-isMonoid = record
    { isSemigroup = ++-isSemigroup
    ; identity    = ++-identity
    }

module _ {a} (A : Set a) where

  ++-semigroup : Semigroup a a
  ++-semigroup = record
    { Carrier     = List A
    ; isSemigroup = ++-isSemigroup
    }

  ++-monoid : Monoid a a
  ++-monoid = record
    { Carrier  = List A
    ; isMonoid = ++-isMonoid
    }

------------------------------------------------------------------------
-- alignWith

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         {f g : These A B → C} where

  alignWith-cong : f ≗ g → ∀ as → alignWith f as ≗ alignWith g as
  alignWith-cong f≗g []         bs       = map-cong (f≗g ∘ that) bs
  alignWith-cong f≗g as@(_ ∷ _) []       = map-cong (f≗g ∘ this) as
  alignWith-cong f≗g (a ∷ as)   (b ∷ bs) =
    P.cong₂ _∷_ (f≗g (these a b)) (alignWith-cong f≗g as bs)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         (f : These A B → C) where

  length-alignWith : ∀ xs ys →
                   length (alignWith f xs ys) ≡ length xs ⊔ length ys
  length-alignWith []         ys       = length-map (f ∘′ that) ys
  length-alignWith xs@(_ ∷ _) []       = length-map (f ∘′ this) xs
  length-alignWith (x ∷ xs)   (y ∷ ys) = P.cong suc (length-alignWith xs ys)

  alignWith-map : ∀ {d e} {D : Set d} {E : Set e} (g : D → A) (h : E → B) →
                ∀ xs ys → alignWith f (map g xs) (map h ys) ≡
                          alignWith (f ∘′ These.map g h) xs ys
  alignWith-map g h []         ys     = sym (map-compose ys)
  alignWith-map g h xs@(_ ∷ _) []     = sym (map-compose xs)
  alignWith-map g h (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ refl (alignWith-map g h xs ys)

  map-alignWith : ∀ {d} {D : Set d} (g : C → D) → ∀ xs ys →
                map g (alignWith f xs ys) ≡
                alignWith (g ∘′ f) xs ys
  map-alignWith g []         ys     = sym (map-compose ys)
  map-alignWith g xs@(_ ∷ _) []     = sym (map-compose xs)
  map-alignWith g (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ refl (map-alignWith g xs ys)

------------------------------------------------------------------------
-- zipWith

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

  zipWith-comm : (∀ x y → f x y ≡ f y x) →
                 ∀ xs ys → zipWith f xs ys ≡ zipWith f ys xs
  zipWith-comm f-comm []       []       = refl
  zipWith-comm f-comm []       (x ∷ ys) = refl
  zipWith-comm f-comm (x ∷ xs) []       = refl
  zipWith-comm f-comm (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ (f-comm x y) (zipWith-comm f-comm xs ys)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         (f : A → B → C) where

  zipWith-identityˡ : ∀ xs → zipWith f [] xs ≡ []
  zipWith-identityˡ []       = refl
  zipWith-identityˡ (x ∷ xs) = refl

  zipWith-identityʳ : ∀ xs → zipWith f xs [] ≡ []
  zipWith-identityʳ []       = refl
  zipWith-identityʳ (x ∷ xs) = refl

  length-zipWith : ∀ xs ys →
                   length (zipWith f xs ys) ≡ length xs ⊓ length ys
  length-zipWith []       []       = refl
  length-zipWith []       (y ∷ ys) = refl
  length-zipWith (x ∷ xs) []       = refl
  length-zipWith (x ∷ xs) (y ∷ ys) = P.cong suc (length-zipWith xs ys)

  zipWith-map : ∀ {d e} {D : Set d} {E : Set e} (g : D → A) (h : E → B) →
                ∀ xs ys → zipWith f (map g xs) (map h ys) ≡
                          zipWith (λ x y → f (g x) (h y)) xs ys
  zipWith-map g h []       []       = refl
  zipWith-map g h []       (y ∷ ys) = refl
  zipWith-map g h (x ∷ xs) []       = refl
  zipWith-map g h (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ refl (zipWith-map g h xs ys)

  map-zipWith : ∀ {d} {D : Set d} (g : C → D) → ∀ xs ys →
                map g (zipWith f xs ys) ≡
                zipWith (λ x y → g (f x y)) xs ys
  map-zipWith g []       []       = refl
  map-zipWith g []       (y ∷ ys) = refl
  map-zipWith g (x ∷ xs) []       = refl
  map-zipWith g (x ∷ xs) (y ∷ ys) =
    P.cong₂ _∷_ refl (map-zipWith g xs ys)

------------------------------------------------------------------------
-- unalignWith

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

  unalignWith-this : unalignWith ((A → These A B) ∋ this) ≗ (_, [])
  unalignWith-this []       = refl
  unalignWith-this (a ∷ as) = P.cong (Prod.map₁ (a ∷_)) (unalignWith-this as)

  unalignWith-that : unalignWith ((B → These A B) ∋ that) ≗ ([] ,_)
  unalignWith-that []       = refl
  unalignWith-that (b ∷ bs) = P.cong (Prod.map₂ (b ∷_)) (unalignWith-that bs)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         {f g : C → These A B} where

  unalignWith-cong : f ≗ g → unalignWith f ≗ unalignWith g
  unalignWith-cong f≗g []       = refl
  unalignWith-cong f≗g (c ∷ cs) with f c | g c | f≗g c
  ... | this a    | ._ | refl = P.cong (Prod.map₁ (a ∷_)) (unalignWith-cong f≗g cs)
  ... | that b    | ._ | refl = P.cong (Prod.map₂ (b ∷_)) (unalignWith-cong f≗g cs)
  ... | these a b | ._ | refl = P.cong (Prod.map (a ∷_) (b ∷_)) (unalignWith-cong f≗g cs)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         (f : C → These A B) where

  unalignWith-map : ∀ {d} {D : Set d} (g : D → C) →
    ∀ ds → unalignWith f (map g ds) ≡ unalignWith (f ∘′ g) ds
  unalignWith-map g []       = refl
  unalignWith-map g (d ∷ ds) with f (g d)
  ... | this a    = P.cong (Prod.map₁ (a ∷_)) (unalignWith-map g ds)
  ... | that b    = P.cong (Prod.map₂ (b ∷_)) (unalignWith-map g ds)
  ... | these a b = P.cong (Prod.map (a ∷_) (b ∷_)) (unalignWith-map g ds)

  map-unalignWith : ∀ {d e} {D : Set d} {E : Set e} (g : A → D) (h : B → E) →
    Prod.map (map g) (map h) ∘′ unalignWith f ≗ unalignWith (These.map g h ∘′ f)
  map-unalignWith g h []       = refl
  map-unalignWith g h (c ∷ cs) with f c
  ... | this a    = P.cong (Prod.map₁ (g a ∷_)) (map-unalignWith g h cs)
  ... | that b    = P.cong (Prod.map₂ (h b ∷_)) (map-unalignWith g h cs)
  ... | these a b = P.cong (Prod.map (g a ∷_) (h b ∷_)) (map-unalignWith g h cs)

  unalignWith-alignWith : (g : These A B → C) → f ∘′ g ≗ id →
                      ∀ as bs → unalignWith f (alignWith g as bs) ≡ (as , bs)
  unalignWith-alignWith g g∘f≗id []         bs = begin
    unalignWith f (map (g ∘′ that) bs) ≡⟨ unalignWith-map (g ∘′ that) bs ⟩
    unalignWith (f ∘′ g ∘′ that) bs    ≡⟨ unalignWith-cong (g∘f≗id ∘ that) bs ⟩
    unalignWith that bs                ≡⟨ unalignWith-that bs ⟩
    [] , bs ∎ where open P.≡-Reasoning
  unalignWith-alignWith g g∘f≗id as@(_ ∷ _) [] = begin
    unalignWith f (map (g ∘′ this) as) ≡⟨ unalignWith-map (g ∘′ this) as ⟩
    unalignWith (f ∘′ g ∘′ this) as    ≡⟨ unalignWith-cong (g∘f≗id ∘ this) as ⟩
    unalignWith this as                ≡⟨ unalignWith-this as ⟩
    as , [] ∎ where open P.≡-Reasoning
  unalignWith-alignWith g g∘f≗id (a ∷ as)   (b ∷ bs)
    rewrite g∘f≗id (these a b) = let ih = unalignWith-alignWith g g∘f≗id as bs in
                                 P.cong (Prod.map (a ∷_) (b ∷_)) ih

------------------------------------------------------------------------
-- unzipWith

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         (f : A → B × C) where

  length-unzipWith₁ : ∀ xys →
                     length (proj₁ (unzipWith f xys)) ≡ length xys
  length-unzipWith₁ []        = refl
  length-unzipWith₁ (x ∷ xys) = P.cong suc (length-unzipWith₁ xys)

  length-unzipWith₂ : ∀ xys →
                     length (proj₂ (unzipWith f xys)) ≡ length xys
  length-unzipWith₂ []        = refl
  length-unzipWith₂ (x ∷ xys) = P.cong suc (length-unzipWith₂ xys)

  zipWith-unzipWith : (g : B → C → A) → uncurry′ g ∘ f ≗ id →
                      uncurry′ (zipWith g) ∘ (unzipWith f)  ≗ id
  zipWith-unzipWith g f∘g≗id []       = refl
  zipWith-unzipWith g f∘g≗id (x ∷ xs) =
    P.cong₂ _∷_ (f∘g≗id x) (zipWith-unzipWith g f∘g≗id xs)

------------------------------------------------------------------------
-- foldr

foldr-universal : ∀ {a b} {A : Set a} {B : Set b}
                  (h : List A → B) f e → (h [] ≡ e) →
                  (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                  h ≗ foldr f e
foldr-universal h f e base step []       = base
foldr-universal h f e base step (x ∷ xs) = begin
    h (x ∷ xs)
  ≡⟨ step x xs ⟩
    f x (h xs)
  ≡⟨ P.cong (f x) (foldr-universal h f e base step xs) ⟩
    f x (foldr f e xs)
  ∎
  where open P.≡-Reasoning

foldr-cong : ∀ {a b} {A : Set a} {B : Set b}
             {f g : A → B → B} {d e : B} →
             (∀ x y → f x y ≡ g x y) → d ≡ e →
             foldr f d ≗ foldr g e
foldr-cong f≗g refl []      = refl
foldr-cong f≗g d≡e (x ∷ xs) rewrite foldr-cong f≗g d≡e xs = f≗g x _

foldr-fusion : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
               (h : B → C) {f : A → B → B} {g : A → C → C} (e : B) →
               (∀ x y → h (f x y) ≡ g x (h y)) →
               h ∘ foldr f e ≗ foldr g (h e)
foldr-fusion h {f} {g} e fuse =
  foldr-universal (h ∘ foldr f e) g (h e) refl
                  (λ x xs → fuse x (foldr f e xs))

id-is-foldr : ∀ {a} {A : Set a} → id {A = List A} ≗ foldr _∷_ []
id-is-foldr = foldr-universal id _∷_ [] refl (λ _ _ → refl)

++-is-foldr : ∀ {a} {A : Set a} (xs ys : List A) →
           xs ++ ys ≡ foldr _∷_ ys xs
++-is-foldr xs ys =
  begin
    xs ++ ys
  ≡⟨ P.cong (_++ ys) (id-is-foldr xs) ⟩
    foldr _∷_ [] xs ++ ys
  ≡⟨ foldr-fusion (_++ ys) [] (λ _ _ → refl) xs ⟩
    foldr _∷_ ([] ++ ys) xs
  ≡⟨⟩
    foldr _∷_ ys xs
  ∎
  where open P.≡-Reasoning

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

  foldr-++ : ∀ (f : A → B → B) x ys zs →
             foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys
  foldr-++ f x []       zs = refl
  foldr-++ f x (y ∷ ys) zs = P.cong (f y) (foldr-++ f x ys zs)

  map-is-foldr : {f : A → B} → map f ≗ foldr (λ x ys → f x ∷ ys) []
  map-is-foldr {f = f} =
    begin
      map f
    ≈⟨ P.cong (map f) ∘ id-is-foldr ⟩
      map f ∘ foldr _∷_ []
    ≈⟨ foldr-fusion (map f) [] (λ _ _ → refl) ⟩
      foldr (λ x ys → f x ∷ ys) []
    ∎  where open EqR (P._→-setoid_ _ _)

  foldr-∷ʳ : ∀ (f : A → B → B) x y ys →
             foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys
  foldr-∷ʳ f x y []       = refl
  foldr-∷ʳ f x y (z ∷ ys) = P.cong (f z) (foldr-∷ʳ f x y ys)

------------------------------------------------------------------------
-- foldl

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

  foldl-++ : ∀ (f : A → B → A) x ys zs →
             foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
  foldl-++ f x []       zs = refl
  foldl-++ f x (y ∷ ys) zs = foldl-++ f (f x y) ys zs

  foldl-∷ʳ : ∀ (f : A → B → A) x y ys →
             foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y
  foldl-∷ʳ f x y []       = refl
  foldl-∷ʳ f x y (z ∷ ys) = foldl-∷ʳ f (f x z) y ys

------------------------------------------------------------------------
-- concat

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

  concat-map : ∀ {f : A → B} → concat ∘ map (map f) ≗ map f ∘ concat
  concat-map {f = f} =
    begin
      concat ∘ map (map f)
    ≈⟨ P.cong concat ∘ map-is-foldr ⟩
      concat ∘ foldr (λ xs → map f xs ∷_) []
    ≈⟨ foldr-fusion concat [] (λ _ _ → refl) ⟩
      foldr (λ ys → map f ys ++_) []
    ≈⟨ P.sym ∘ foldr-fusion (map f) [] (map-++-commute f) ⟩
      map f ∘ concat
    ∎
    where open EqR (P._→-setoid_ _ _)

------------------------------------------------------------------------
-- sum

sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []       ys = refl
sum-++-commute (x ∷ xs) ys = begin
  x + sum (xs ++ ys)     ≡⟨ P.cong (x +_) (sum-++-commute xs ys) ⟩
  x + (sum xs + sum ys)  ≡⟨ P.sym (+-assoc x _ _) ⟩
  (x + sum xs) + sum ys  ∎
  where open P.≡-Reasoning

------------------------------------------------------------------------
-- replicate

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

  length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
  length-replicate zero    = refl
  length-replicate (suc n) = P.cong suc (length-replicate n)

------------------------------------------------------------------------
-- scanr

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

  scanr-defn : ∀ (f : A → B → B) (e : B) →
               scanr f e ≗ map (foldr f e) ∘ tails
  scanr-defn f e []             = refl
  scanr-defn f e (x ∷ [])       = refl
  scanr-defn f e (x ∷ y ∷ xs)
    with scanr f e (y ∷ xs) | scanr-defn f e (y ∷ xs)
  ... | []     | ()
  ... | z ∷ zs | eq with ∷-injective eq
  ...   | z≡fy⦇f⦈xs , _ = P.cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq

------------------------------------------------------------------------
-- scanl

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

  scanl-defn : ∀ (f : A → B → A) (e : A) →
               scanl f e ≗ map (foldl f e) ∘ inits
  scanl-defn f e []       = refl
  scanl-defn f e (x ∷ xs) = P.cong (e ∷_) (begin
     scanl f (f e x) xs
   ≡⟨ scanl-defn f (f e x) xs ⟩
     map (foldl f (f e x)) (inits xs)
   ≡⟨ refl ⟩
     map (foldl f e ∘ (x ∷_)) (inits xs)
   ≡⟨ map-compose (inits xs) ⟩
     map (foldl f e) (map (x ∷_) (inits xs))
   ∎)
   where open P.≡-Reasoning

------------------------------------------------------------------------
-- applyUpTo

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

  length-applyUpTo : ∀ (f : ℕ → A) n → length (applyUpTo f n) ≡ n
  length-applyUpTo f zero    = refl
  length-applyUpTo f (suc n) = P.cong suc (length-applyUpTo (f ∘ suc) n)

  lookup-applyUpTo : ∀ (f : ℕ → A) n i → lookup (applyUpTo f n) i ≡ f (toℕ i)
  lookup-applyUpTo f zero  ()
  lookup-applyUpTo f (suc n) zero    = refl
  lookup-applyUpTo f (suc n) (suc i) = lookup-applyUpTo (f ∘ suc) n i

------------------------------------------------------------------------
-- applyUpTo

module _ {a} {A : Set a} (f : ℕ → A) where

  length-applyDownFrom : ∀ n → length (applyDownFrom f n) ≡ n
  length-applyDownFrom zero    = refl
  length-applyDownFrom (suc n) = P.cong suc (length-applyDownFrom n)

  lookup-applyDownFrom : ∀ n i → lookup (applyDownFrom f n) i ≡ f (n ∸ (suc (toℕ i)))
  lookup-applyDownFrom zero  ()
  lookup-applyDownFrom (suc n) zero    = refl
  lookup-applyDownFrom (suc n) (suc i) = lookup-applyDownFrom n i

------------------------------------------------------------------------
-- upTo

length-upTo : ∀ n → length (upTo n) ≡ n
length-upTo = length-applyUpTo id

lookup-upTo : ∀ n i → lookup (upTo n) i ≡ toℕ i
lookup-upTo = lookup-applyUpTo id

------------------------------------------------------------------------
-- downFrom

length-downFrom : ∀ n → length (downFrom n) ≡ n
length-downFrom = length-applyDownFrom id

lookup-downFrom : ∀ n i → lookup (downFrom n) i ≡ n ∸ (suc (toℕ i))
lookup-downFrom = lookup-applyDownFrom id

------------------------------------------------------------------------
-- tabulate

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

  tabulate-cong : ∀ {n} {f g : Fin n → A} →
                  f ≗ g → tabulate f ≡ tabulate g
  tabulate-cong {zero}  p = P.refl
  tabulate-cong {suc n} p = P.cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))

  tabulate-lookup : ∀ (xs : List A) → tabulate (lookup xs) ≡ xs
  tabulate-lookup []       = refl
  tabulate-lookup (x ∷ xs) = P.cong (_ ∷_) (tabulate-lookup xs)

  length-tabulate : ∀ {n} → (f : Fin n → A) →
                 length (tabulate f) ≡ n
  length-tabulate {zero} f = refl
  length-tabulate {suc n} f = P.cong suc (length-tabulate (λ z → f (suc z)))

  lookup-tabulate : ∀{n} → (f : Fin n → A) →
                    ∀ i → let i′ = cast (sym (length-tabulate f)) i
                          in lookup (tabulate f) i′ ≡ f i
  lookup-tabulate f zero    = refl
  lookup-tabulate f (suc i) = lookup-tabulate (f ∘ suc) i

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

  map-tabulate : ∀ {n} (g : Fin n → A) (f : A → B) →
                 map f (tabulate g) ≡ tabulate (f ∘ g)
  map-tabulate {zero}  g f = refl
  map-tabulate {suc n} g f = P.cong (_ ∷_) (map-tabulate (g ∘ suc) f)

------------------------------------------------------------------------
-- _[_]%=_

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

  length-%= : ∀ xs k (f : A → A) → length (xs [ k ]%= f) ≡ length xs
  length-%= []       ()      f
  length-%= (x ∷ xs) zero    f = refl
  length-%= (x ∷ xs) (suc k) f = P.cong suc (length-%= xs k f)

------------------------------------------------------------------------
-- _[_]∷=_

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

  length-∷= : ∀ xs k (v : A) → length (xs [ k ]∷= v) ≡ length xs
  length-∷= xs k v = length-%= xs k (const v)

  map-∷= : ∀ {b} {B : Set b} xs k (v : A) (f : A → B) →
           let eq = P.sym (length-map f xs) in
           map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
  map-∷= []       ()      v f
  map-∷= (x ∷ xs) zero    v f = refl
  map-∷= (x ∷ xs) (suc k) v f = P.cong (f x ∷_) (map-∷= xs k v f)

------------------------------------------------------------------------
-- _─_

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

  length-─ : ∀ (xs : List A) k → length (xs ─ k) ≡ pred (length xs)
  length-─ []       ()
  length-─ (x ∷ xs) zero        = refl
  length-─ (x ∷ []) (suc ())
  length-─ (x ∷ y ∷ xs) (suc k) = P.cong suc (length-─ (y ∷ xs) k)

  map-─ : ∀ {b} {B : Set b} xs k (f : A → B) →
          let eq = P.sym (length-map f xs) in
          map f (xs ─ k) ≡ map f xs ─ cast eq k
  map-─ []       ()      f
  map-─ (x ∷ xs) zero    f = refl
  map-─ (x ∷ xs) (suc k) f = P.cong (f x ∷_) (map-─ xs k f)

------------------------------------------------------------------------
-- take

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

  length-take : ∀ n (xs : List A) → length (take n xs) ≡ n ⊓ (length xs)
  length-take zero    xs       = refl
  length-take (suc n) []       = refl
  length-take (suc n) (x ∷ xs) = P.cong suc (length-take n xs)

------------------------------------------------------------------------
-- drop

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

  length-drop : ∀ n (xs : List A) → length (drop n xs) ≡ length xs ∸ n
  length-drop zero    xs       = refl
  length-drop (suc n) []       = refl
  length-drop (suc n) (x ∷ xs) = length-drop n xs

  take++drop : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
  take++drop zero    xs       = refl
  take++drop (suc n) []       = refl
  take++drop (suc n) (x ∷ xs) = P.cong (x ∷_) (take++drop n xs)

------------------------------------------------------------------------
-- splitAt

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

  splitAt-defn : ∀ n → splitAt {A = A} n ≗ < take n , drop n >
  splitAt-defn zero    xs       = refl
  splitAt-defn (suc n) []       = refl
  splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
  ... | (ys , zs) | ih = P.cong (Prod.map (x ∷_) id) ih

------------------------------------------------------------------------
-- takeWhile, dropWhile, and span

module _ {a p} {A : Set a} {P : Pred A p} (P? : Decidable P) where

  takeWhile++dropWhile : ∀ xs → takeWhile P? xs ++ dropWhile P? xs ≡ xs
  takeWhile++dropWhile []       = refl
  takeWhile++dropWhile (x ∷ xs) with P? x
  ... | yes _ = P.cong (x ∷_) (takeWhile++dropWhile xs)
  ... | no  _ = refl

  span-defn : span P? ≗ < takeWhile P? , dropWhile P? >
  span-defn []       = refl
  span-defn (x ∷ xs) with P? x
  ... | yes _ = P.cong (Prod.map (x ∷_) id) (span-defn xs)
  ... | no  _ = refl

------------------------------------------------------------------------
-- filter

module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where

  length-filter : ∀ xs → length (filter P? xs) ≤ length xs
  length-filter []       = z≤n
  length-filter (x ∷ xs) with P? x
  ... | no  _ = ≤-step (length-filter xs)
  ... | yes _ = s≤s (length-filter xs)

  filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
  filter-all {[]}     []         = refl
  filter-all {x ∷ xs} (px ∷ pxs) with P? x
  ... | no  ¬px = contradiction px ¬px
  ... | yes _   = P.cong (x ∷_) (filter-all pxs)

  filter-notAll : ∀ xs → Any (∁ P) xs → length (filter P? xs) < length xs
  filter-notAll [] ()
  filter-notAll (x ∷ xs) (here ¬px) with P? x
  ... | no  _  = s≤s (length-filter xs)
  ... | yes px = contradiction px ¬px
  filter-notAll (x ∷ xs) (there any) with P? x
  ... | no  _ = ≤-step (filter-notAll xs any)
  ... | yes _ = s≤s (filter-notAll xs any)

  filter-some : ∀ {xs} → Any P xs → 0 < length (filter P? xs)
  filter-some {x ∷ xs} (here px)   with P? x
  ... | yes _  = s≤s z≤n
  ... | no ¬px = contradiction px ¬px
  filter-some {x ∷ xs} (there pxs) with P? x
  ... | yes _ = ≤-step (filter-some pxs)
  ... | no  _ = filter-some pxs

  filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
  filter-none {[]}     []           = refl
  filter-none {x ∷ xs} (¬px ∷ ¬pxs) with P? x
  ... | no  _  = filter-none ¬pxs
  ... | yes px = contradiction px ¬px

  filter-complete : ∀ {xs} → length (filter P? xs) ≡ length xs →
                    filter P? xs ≡ xs
  filter-complete {[]}     eq = refl
  filter-complete {x ∷ xs} eq with P? x
  ... | no ¬px = contradiction eq (<⇒≢ (s≤s (length-filter xs)))
  ... | yes px = P.cong (x ∷_) (filter-complete (suc-injective eq))

------------------------------------------------------------------------
-- partition

module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where

  partition-defn : partition P? ≗ < filter P? , filter (∁? P?) >
  partition-defn []       = refl
  partition-defn (x ∷ xs) with P? x
  ...  | yes Px = P.cong (Prod.map (x ∷_) id) (partition-defn xs)
  ...  | no ¬Px = P.cong (Prod.map id (x ∷_)) (partition-defn xs)

------------------------------------------------------------------------
-- reverse

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

  open FunctionProperties {A = List A} _≡_

  unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
  unfold-reverse x xs = helper [ x ] xs
    where
    open P.≡-Reasoning
    helper : (xs ys : List A) → foldl (flip _∷_) xs ys ≡ reverse ys ++ xs
    helper xs []       = refl
    helper xs (y ∷ ys) = begin
      foldl (flip _∷_) (y ∷ xs) ys  ≡⟨ helper (y ∷ xs) ys ⟩
      reverse ys ++ y ∷ xs          ≡⟨ P.sym (++-assoc (reverse ys) _ _) ⟩
      (reverse ys ∷ʳ y) ++ xs       ≡⟨ P.sym $ P.cong (_++ xs) (unfold-reverse y ys) ⟩
      reverse (y ∷ ys) ++ xs        ∎

  reverse-++-commute : (xs ys : List A) →
                       reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
  reverse-++-commute []       ys = P.sym (++-identityʳ _)
  reverse-++-commute (x ∷ xs) ys = begin
    reverse (x ∷ xs ++ ys)               ≡⟨ unfold-reverse x (xs ++ ys) ⟩
    reverse (xs ++ ys) ++ [ x ]          ≡⟨ P.cong (_++ [ x ]) (reverse-++-commute xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]  ≡⟨ ++-assoc (reverse ys) _ _ ⟩
    reverse ys ++ (reverse xs ++ [ x ])  ≡⟨ P.sym $ P.cong (reverse ys ++_) (unfold-reverse x xs) ⟩
    reverse ys ++ reverse (x ∷ xs)       ∎
    where open P.≡-Reasoning

  reverse-involutive : Involutive reverse
  reverse-involutive [] = refl
  reverse-involutive (x ∷ xs) = begin
    reverse (reverse (x ∷ xs))   ≡⟨ P.cong reverse $ unfold-reverse x xs ⟩
    reverse (reverse xs ∷ʳ x)    ≡⟨ reverse-++-commute (reverse xs) ([ x ]) ⟩
    x ∷ reverse (reverse (xs))   ≡⟨ P.cong (x ∷_) $ reverse-involutive xs ⟩
    x ∷ xs                       ∎
    where open P.≡-Reasoning

  length-reverse : (xs : List A) → length (reverse xs) ≡ length xs
  length-reverse []       = refl
  length-reverse (x ∷ xs) = begin
    length (reverse (x ∷ xs))   ≡⟨ P.cong length $ unfold-reverse x xs ⟩
    length (reverse xs ∷ʳ x)    ≡⟨ length-++ (reverse xs) ⟩
    length (reverse xs) + 1     ≡⟨ P.cong (_+ 1) (length-reverse xs) ⟩
    length xs + 1               ≡⟨ +-comm _ 1 ⟩
    suc (length xs)             ∎
    where open P.≡-Reasoning

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

  reverse-map-commute : (f : A → B) (xs : List A) →
                        map f (reverse xs) ≡ reverse (map f xs)
  reverse-map-commute f []       = refl
  reverse-map-commute f (x ∷ xs) = begin
    map f (reverse (x ∷ xs))   ≡⟨ P.cong (map f) $ unfold-reverse x xs ⟩
    map f (reverse xs ∷ʳ x)    ≡⟨ map-++-commute f (reverse xs) ([ x ]) ⟩
    map f (reverse xs) ∷ʳ f x  ≡⟨ P.cong (_∷ʳ f x) $ reverse-map-commute f xs ⟩
    reverse (map f xs) ∷ʳ f x  ≡⟨ P.sym $ unfold-reverse (f x) (map f xs) ⟩
    reverse (map f (x ∷ xs))   ∎
    where open P.≡-Reasoning

  reverse-foldr : ∀ (f : A → B → B) x ys →
                  foldr f x (reverse ys) ≡ foldl (flip f) x ys
  reverse-foldr f x []       = refl
  reverse-foldr f x (y ∷ ys) = begin
    foldr f x (reverse (y ∷ ys)) ≡⟨ P.cong (foldr f x) (unfold-reverse y ys) ⟩
    foldr f x ((reverse ys) ∷ʳ y) ≡⟨ foldr-∷ʳ f x y (reverse ys) ⟩
    foldr f (f y x) (reverse ys)  ≡⟨ reverse-foldr f (f y x) ys ⟩
    foldl (flip f) (f y x) ys     ∎
    where open P.≡-Reasoning

  reverse-foldl : ∀ (f : A → B → A) x ys →
                  foldl f x (reverse ys) ≡ foldr (flip f) x ys
  reverse-foldl f x []       = refl
  reverse-foldl f x (y ∷ ys) = begin
    foldl f x (reverse (y ∷ ys)) ≡⟨ P.cong (foldl f x) (unfold-reverse y ys) ⟩
    foldl f x ((reverse ys) ∷ʳ y) ≡⟨ foldl-∷ʳ f x y (reverse ys) ⟩
    f (foldl f x (reverse ys)) y ≡⟨ P.cong (flip f y) (reverse-foldl f x ys) ⟩
    f (foldr (flip f) x ys) y    ∎
    where open P.≡-Reasoning

------------------------------------------------------------------------
-- _∷ʳ_

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

  ∷ʳ-injective : ∀ {x y : A} xs ys →
                 xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
  ∷ʳ-injective []          []          refl = (refl , refl)
  ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with ∷-injective eq
  ... | refl , eq′ = Prod.map (P.cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
  ∷ʳ-injective []          (_ ∷ [])    ()
  ∷ʳ-injective []          (_ ∷ _ ∷ _) ()
  ∷ʳ-injective (_ ∷ [])    []          ()
  ∷ʳ-injective (_ ∷ _ ∷ _) []          ()

  ∷ʳ-injectiveˡ : ∀ {x y : A} (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
  ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)

  ∷ʳ-injectiveʳ : ∀ {x y : A} (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
  ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

gfilter-just      = mapMaybe-just
{-# WARNING_ON_USAGE gfilter-just
"Warning: gfilter-just was deprecated in v0.15.
Please use mapMaybe-just instead."
#-}
gfilter-nothing   = mapMaybe-nothing
{-# WARNING_ON_USAGE gfilter-nothing
"Warning: gfilter-nothing was deprecated in v0.15.
Please use mapMaybe-nothing instead."
#-}
gfilter-concatMap = mapMaybe-concatMap
{-# WARNING_ON_USAGE gfilter-concatMap
"Warning: gfilter-concatMap was deprecated in v0.15.
Please use mapMaybe-concatMap instead."
#-}
length-gfilter    = length-mapMaybe
{-# WARNING_ON_USAGE length-gfilter
"Warning: length-gfilter was deprecated in v0.15.
Please use length-mapMaybe instead."
#-}
right-identity-unique = ++-identityʳ-unique
{-# WARNING_ON_USAGE right-identity-unique
"Warning: right-identity-unique was deprecated in v0.15.
Please use ++-identityʳ-unique instead."
#-}
left-identity-unique  = ++-identityˡ-unique
{-# WARNING_ON_USAGE left-identity-unique
"Warning: left-identity-unique was deprecated in v0.15.
Please use ++-identityˡ-unique instead."
#-}

-- Version 0.16

module _ {a} {A : Set a} (p : A → Bool) where

  boolTakeWhile++boolDropWhile : ∀ xs → boolTakeWhile p xs ++ boolDropWhile p xs ≡ xs
  boolTakeWhile++boolDropWhile []       = refl
  boolTakeWhile++boolDropWhile (x ∷ xs) with p x
  ... | true  = P.cong (x ∷_) (boolTakeWhile++boolDropWhile xs)
  ... | false = refl
  {-# WARNING_ON_USAGE boolTakeWhile++boolDropWhile
  "Warning: boolTakeWhile and boolDropWhile were deprecated in v0.16.
  Please use takeWhile and dropWhile instead."
  #-}
  boolSpan-defn : boolSpan p ≗ < boolTakeWhile p , boolDropWhile p >
  boolSpan-defn []       = refl
  boolSpan-defn (x ∷ xs) with p x
  ... | true  = P.cong (Prod.map (x ∷_) id) (boolSpan-defn xs)
  ... | false = refl
  {-# WARNING_ON_USAGE boolSpan-defn
  "Warning: boolSpan, boolTakeWhile and boolDropWhile were deprecated in v0.16.
  Please use span, takeWhile and dropWhile instead."
  #-}
  length-boolFilter : ∀ xs → length (boolFilter p xs) ≤ length xs
  length-boolFilter xs =
    length-mapMaybe (λ x → if p x then just x else nothing) xs
  {-# WARNING_ON_USAGE length-boolFilter
  "Warning: boolFilter was deprecated in v0.16.
  Please use filter instead."
  #-}
  boolPartition-defn : boolPartition p ≗ < boolFilter p , boolFilter (not ∘ p) >
  boolPartition-defn []       = refl
  boolPartition-defn (x ∷ xs) with p x
  ...  | true  = P.cong (Prod.map (x ∷_) id) (boolPartition-defn xs)
  ...  | false = P.cong (Prod.map id (x ∷_)) (boolPartition-defn xs)
  {-# WARNING_ON_USAGE boolPartition-defn
  "Warning: boolPartition and boolFilter were deprecated in v0.16.
  Please use partition and filter instead."
  #-}

module _ {a p} {A : Set a} (P : A → Set p) (P? : Decidable P) where

  boolFilter-filters : ∀ xs → All P (boolFilter (⌊_⌋ ∘ P?) xs)
  boolFilter-filters []       = []
  boolFilter-filters (x ∷ xs) with P? x
  ... | yes px = px ∷ boolFilter-filters xs
  ... | no ¬px = boolFilter-filters xs
  {-# WARNING_ON_USAGE boolFilter-filters
  "Warning: boolFilter was deprecated in v0.16.
  Please use filter instead."
  #-}

-- Version 0.17

idIsFold  = id-is-foldr
{-# WARNING_ON_USAGE idIsFold
"Warning: idIsFold was deprecated in v0.17.
Please use id-is-foldr instead."
#-}
++IsFold  = ++-is-foldr
{-# WARNING_ON_USAGE ++IsFold
"Warning: ++IsFold was deprecated in v0.17.
Please use ++-is-foldr instead."
#-}
mapIsFold = map-is-foldr
{-# WARNING_ON_USAGE mapIsFold
"Warning: mapIsFold was deprecated in v0.17.
Please use map-is-foldr instead."
#-}


text:
-- Andreas, 2018-09-03, issue #3200 reported by gallais
--
-- Record let pattern bindings trigger spurious irrelevance
-- marker, probably due to confusion of Prop with dummy type.

-- {-# OPTIONS -v tc.term.let.pattern:100 #-}
-- {-# OPTIONS -v tc.lhs.top:30 #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Unit

record R : Set where
  field
    fld : Bool

data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

solve2 : Maybe (Bool → Bool)
solve2 =
  let record { fld = bla } = record { fld = true } in
  case true of λ where
    true → just (λ x → true)
    false → nothing

From-just : {A : Set} → Maybe A → Set
From-just {A} (just _) = A
From-just nothing  = ⊤

from-just : {A : Set} (x : Maybe A) → From-just x
from-just (just x) = x
from-just nothing  = _

test : Bool
test = from-just solve2 true

-- Error was:
--
-- From-just .((just (λ x → true))) should be a function type, but it isn't
-- when checking that true is a valid argument to a function of type
-- From-just solve2

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import leibniz public
open import equalities public
open import leibniz-equality public

max_stars_repo_name: guilhermehas/Equality

max_issues_repo_name: guilhermehas/Equality

max_forks_repo_name: guilhermehas/Equality


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Lift
open import lib.groups.Homomorphisms

module lib.groups.Lift where

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

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

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

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

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

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

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --show-implicit #-}
open import Relation.Binary.PropositionalEquality

module Experiments.Ref (funext : ∀ {a b} → Extensionality a b) where

open import Level
open import Data.Nat
import Data.Unit as Unit
open import Data.List
open import Data.List.Most
open import Data.Product hiding (swap)
open import Data.Maybe as Maybe hiding (All)
open import Function as Fun using (case_of_)
import Relation.Binary.PropositionalEquality as PEq
open PEq.≡-Reasoning

data Ty : Set where
  unit : Ty
  ref  : Ty → Ty

open import Experiments.Category (⊑-preorder {A = Ty})
open Product

data Expr : Ty → Set where
  unit  : Expr unit
  ref   : ∀ {t} → Expr t → Expr (ref t)
  !_    : ∀ {t} → Expr (ref t) → Expr t
  _≔_   : ∀ {t} → Expr (ref t) → Expr t → Expr unit

Val : Ty → MP₀
Val t = mp (Val' t) (record {
    monotone = λ{ c~c' unit → unit ; c~c' (ref x) → ref (∈-⊒ x c~c') };
    monotone-refl = λ{ unit → refl ; (ref x) → cong ref ∈-⊒-refl };
    monotone-trans = λ p c~c' c'~c'' → {!!}
  })
  module Values where
    data Val' : Ty → List Ty → Set where
      unit   : ∀ {Σ} → Val' unit Σ
      ref    : ∀ {Σ t} → t ∈ Σ → Val' (ref t) Σ

open import Experiments.StrongMonad Ty Val funext
open Strong

mkunit : ⊤ ⇒ Val unit
mkunit = mk⇒ (λ _ → Values.unit) λ c~c' → refl

alloc : ∀ {a} → Val a ⇒ M (Val (ref a))
alloc {a} = mk⇒
  (λ v Σ₁ ext μ₁ →
    let ext' = ∷ʳ-⊒ a Σ₁ in
      (Σ₁ ∷ʳ a) ,
      ext' ,
      ((map-all (MP.monotone (Val _) ext') μ₁) all-∷ʳ MP.monotone (Val _) (⊑-trans ext ext') v) ,
      Values.ref (∈-∷ʳ Σ₁ a))
  (λ c~c' → {!!})

load : ∀ {a} → Val (ref a) ⇒ M (Val a)
load  {a} = mk⇒
  (λ v Σ₁ ext μ₁ → case v of λ{
    (Values.ref x) → Σ₁ , ⊑-refl , μ₁ , (∈-all (∈-⊒ x ext) μ₁)
  })
  (λ c~c' → {!!})

store : ∀ {a} → (Val (ref a) ⊗ Val a) ⇒ M ⊤
store = mk⇒
  (λ x Σ₁ ext μ₁ → case x of λ{
    (Values.ref l , v) → Σ₁ , ⊑-refl , (μ₁ All[ ∈-⊒ l ext ]≔' MP.monotone (Val _) ext v) , Unit.tt
  })
  (λ c~c' → {!!})

eval : ∀ {a} → Expr a → ⊤ ⇒ M (Val a)
eval unit = η (Val _) ∘ mkunit
eval (ref e) = μ (Val _) ∘ fmap alloc ∘ eval e
eval (! e) = μ (Val _) ∘ fmap load ∘ eval e
eval (e₁ ≔ e₂) =
    fmap mkunit
  ∘ μ ⊤
  ∘ fmap store
  ∘ μ ((Val _) ⊗ (Val _))
  ∘ fmap (ts' (Val _)(Val _))
  ∘ ts (M (Val _))(Val _)
  ∘ ⟨ eval e₁ , eval e₂ ⟩


text:
------------------------------------------------------------------------
-- Strings
------------------------------------------------------------------------

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

module String where

open import Prelude

------------------------------------------------------------------------
-- Helper code used below

private

  -- A variant of Maybe that matches the Haskell Maybe type.

  data HMaybe (A : Type) : Type where
    Nothing : HMaybe A
    Just    : A → HMaybe A

  {-# COMPILE GHC HMaybe = data Maybe (Nothing | Just) #-}

  -- A conversion function.

  hmaybe-to-maybe : ∀ {A} → HMaybe A → Maybe A
  hmaybe-to-maybe Nothing  = nothing
  hmaybe-to-maybe (Just x) = just x

------------------------------------------------------------------------
-- Operations on strings

-- Implemented using the FFI. These operations do not compute at
-- compile-time, and are only supported by the GHC backend.

{-# FOREIGN GHC
  import qualified Data.Text
  #-}

mutual

  -- Tries to parse the given string as a natural number. Accepts
  -- whatever the Haskell Read instance for Integer accepts, except
  -- for negative numbers.

  parseℕ : String → Maybe ℕ
  parseℕ = hmaybe-to-maybe ∘ parseℕ′

  private
    postulate
      parseℕ′ : String → HMaybe ℕ

{-# COMPILE GHC parseℕ′ =
  \s -> case reads (Data.Text.unpack s) of
          { [(x, "")] | x >= 0 -> Just (x :: Integer)
          ; _                  -> Nothing
          }
  #-}

-- Turns natural numbers into strings.

postulate
  prettyℕ : ℕ → String

{-# COMPILE GHC prettyℕ =
  \n -> Data.Text.pack (show (n :: Integer))
  #-}

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
module Data.QuadTree.FunctorProofs.Valid-QuadTreeFunctor where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.QuadTree.FunctorProofs.FunctorLaws
open import Data.QuadTree.FunctorProofs.Valid-QuadrantFunctor
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.Functors
open import Data.QuadTree.Implementation.QuadrantLenses

ValidFunctor-QuadTree-IdentityLaw : (dep : Nat) -> IdentityLaw (λ y -> VQuadTree y {dep}) {{quadtreeFunctor dep}}
ValidFunctor-QuadTree-IdentityLaw dep (CVQuadTree (Wrapper (w , h) qd) {p}) =
    begin
        toQt dep w h _ (fmapₑ (quadrantFunctor dep) id (CVQuadrant qd))
    =⟨ cong (toQt dep w h _) (ValidFunctor-Quadrant-IdentityLaw dep (CVQuadrant qd)) ⟩
        toQt dep w h _ (CVQuadrant qd)
    end

toQt-fmap : {a b : Set} {{eqA : Eq a}} {{eqB : Eq b}} (dep w h : Nat) (g : a -> b) (v : VQuadrant a {dep}) .(q : IsTrue (dep == log2up (if w < h then h else w)))
    -> toQt dep w h q (fmapₑ (quadrantFunctor dep) g v)
    ≡ fmapₑ (quadtreeFunctor dep) g (toQt dep w h q v)
toQt-fmap dep w h g (CVQuadrant (Leaf x)) q = refl
toQt-fmap dep w h g (CVQuadrant (Node qd qd₁ qd₂ qd₃)) q = refl

ValidFunctor-QuadTree-CompositionLaw : (dep : Nat) -> CompositionLaw (λ y -> VQuadTree y {dep}) {{quadtreeFunctor dep}}
ValidFunctor-QuadTree-CompositionLaw dep (CVQuadTree (Wrapper (w , h) qd) {p} {q}) f g =
    begin
        toQt dep w h _ (fmapₑ (quadrantFunctor dep) (g ∘ f) (CVQuadrant qd))
    =⟨ cong (toQt dep w h _) (ValidFunctor-Quadrant-CompositionLaw dep (CVQuadrant qd) f g) ⟩
        toQt dep w h _ (fmapₑ (quadrantFunctor dep) g (fmapₑ (quadrantFunctor dep) f (CVQuadrant qd)))
    =⟨ toQt-fmap dep w h g (fmapₑ (quadrantFunctor dep) f (CVQuadrant qd)) q ⟩
        fmapₑ (quadtreeFunctor dep) g (toQt dep w h _ (fmapₑ (quadrantFunctor dep) f (CVQuadrant qd)))
    end where

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project