text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Object.BinaryProducts

module Categories.Object.BinaryProducts.N-ary {o ℓ e}
  (C : Category o ℓ e)
  (BP : BinaryProducts C)
  where

open Category C
open BinaryProducts BP
open Equiv

import Categories.Object.Product
open Categories.Object.Product C

open import Data.Nat using (ℕ; zero; suc)
open import Data.Vec
open import Data.Product.N-ary hiding ([])

Prod : {n : ℕ} → Vec Obj (suc n) → Obj
Prod { zero} (A ∷ []) = A
Prod {suc n} (A ∷ As) = A × Prod {n} As

πˡ : {n m : ℕ}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → Prod (As ++ Bs) ⇒ Prod As
πˡ { zero} (A ∷ []) Bs = π₁
πˡ {suc n} (A ∷ As) Bs = ⟨ π₁ , πˡ {n} As Bs ∘ π₂ ⟩

πʳ : {n m : ℕ}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → Prod (As ++ Bs) ⇒ Prod Bs
πʳ { zero} (A ∷ []) Bs = π₂
πʳ {suc n} (A ∷ As) Bs = πʳ {n} As Bs ∘ π₂

glue : {n m : ℕ}{X : Obj}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → (f : X ⇒ Prod As)
  → (g : X ⇒ Prod Bs)
  → X ⇒ Prod (As ++ Bs)
glue { zero}{m} (A ∷ []) Bs f g = ⟨ f , g ⟩
glue {suc n}{m} (A ∷ As) Bs f g = ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩

open HomReasoning

.commuteˡ : {n m : ℕ}{X : Obj}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → {f : X ⇒ Prod As}
  → {g : X ⇒ Prod Bs}
  → πˡ As Bs ∘ glue As Bs f g ≡ f
commuteˡ { zero} (A ∷ []) Bs {f}{g} = commute₁
commuteˡ {suc n} (A ∷ As) Bs {f}{g} =
  begin
    ⟨ π₁ , πˡ As Bs ∘ π₂ ⟩ ∘ ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
  ↓⟨ ⟨⟩∘ ⟩
    ⟨ π₁              ∘ ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
    , (πˡ As Bs ∘ π₂) ∘ ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
    ⟩
  ↓⟨ ⟨⟩-cong₂ commute₁ assoc ⟩
    ⟨ π₁ ∘ f
    , πˡ As Bs ∘ π₂ ∘ ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
    ⟩
  ↓⟨ ⟨⟩-congʳ (refl ⟩∘⟨ commute₂) ⟩
    ⟨ π₁ ∘ f , πˡ As Bs ∘ glue As Bs (π₂ ∘ f) g ⟩
  ↓⟨ ⟨⟩-congʳ (commuteˡ As Bs) ⟩
    ⟨ π₁ ∘ f , π₂ ∘ f ⟩
  ↓⟨ g-η ⟩
    f
  ∎

.commuteʳ : {n m : ℕ}{X : Obj}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → {f : X ⇒ Prod As}
  → {g : X ⇒ Prod Bs}
  → πʳ As Bs ∘ glue As Bs f g ≡ g
commuteʳ { zero} (A ∷ []) Bs {f}{g} = commute₂
commuteʳ {suc n} (A ∷ As) Bs {f}{g} =
  begin
    (πʳ As Bs ∘ π₂) ∘ ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
  ↓⟨ assoc ⟩
    πʳ As Bs ∘ π₂ ∘ ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
  ↓⟨ refl ⟩∘⟨ commute₂ ⟩
    πʳ As Bs ∘ glue As Bs (π₂ ∘ f) g
  ↓⟨ commuteʳ As Bs ⟩
    g
  ∎

.N-universal : {n m : ℕ}{X : Obj}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → {f : X ⇒ Prod As}
  → {g : X ⇒ Prod Bs}
  → {h : X ⇒ Prod (As ++ Bs) }
  → πˡ As Bs ∘ h ≡ f
  → πʳ As Bs ∘ h ≡ g
  → glue As Bs f g ≡ h
N-universal { zero} (A ∷ []) Bs {f}{g}{h} h-commuteˡ h-commuteʳ = universal h-commuteˡ h-commuteʳ
N-universal {suc n} (A ∷ As) Bs {f}{g}{h} h-commuteˡ h-commuteʳ =
  begin
    ⟨ π₁ ∘ f , glue As Bs (π₂ ∘ f) g ⟩
  ↓⟨ ⟨⟩-congʳ (N-universal As Bs π₂∘h-commuteˡ π₂∘h-commuteʳ) ⟩
    ⟨ π₁ ∘ f , π₂ ∘ h ⟩
  ↑⟨ ⟨⟩-congˡ π₁∘h-commuteˡ ⟩
    ⟨ π₁ ∘ h , π₂ ∘ h ⟩
  ↓⟨ g-η ⟩
    h
  ∎
  where
    -- h-commuteˡ : ⟨ π₁ , πˡ As Bs ∘ π₂ ⟩ ∘ h ≡ f
    -- h-commuteʳ : (πʳ As Bs ∘ π₂) ∘ h ≡ g

    π₁∘h-commuteˡ : π₁ ∘ h ≡ π₁ ∘ f
    π₁∘h-commuteˡ =
      begin
        π₁ ∘ h
      ↑⟨ commute₁ ⟩∘⟨ refl ⟩
        (π₁ ∘ ⟨ π₁ , πˡ As Bs ∘ π₂ ⟩) ∘ h
      ↓⟨ assoc ⟩
        π₁ ∘ ⟨ π₁ , πˡ As Bs ∘ π₂ ⟩ ∘ h
      ↓⟨ refl ⟩∘⟨ h-commuteˡ ⟩
        π₁ ∘ f
      ∎

    π₂∘h-commuteˡ :  πˡ As Bs ∘ π₂ ∘ h ≡ π₂ ∘ f
    π₂∘h-commuteˡ =
      begin
        πˡ As Bs ∘ π₂ ∘ h
      ↑⟨ assoc ⟩
        (πˡ As Bs ∘ π₂) ∘ h
      ↑⟨ commute₂ ⟩∘⟨ refl ⟩
        (π₂ ∘ ⟨ π₁ , πˡ As Bs ∘ π₂ ⟩) ∘ h
      ↓⟨ assoc ⟩
        π₂ ∘ ⟨ π₁ , πˡ As Bs ∘ π₂ ⟩ ∘ h
      ↓⟨ refl ⟩∘⟨ h-commuteˡ ⟩
        π₂ ∘ f
      ∎

    π₂∘h-commuteʳ : πʳ As Bs ∘ π₂ ∘ h ≡ g
    π₂∘h-commuteʳ = trans (sym assoc) h-commuteʳ

isProduct : {n m : ℕ}
  → (As : Vec Obj (suc n))
  → (Bs : Vec Obj (suc m))
  → Product (Prod As) (Prod Bs)
isProduct {n}{m} As Bs = record
  { A×B   = Prod (As ++ Bs)
  ; π₁    = πˡ As Bs
  ; π₂    = πʳ As Bs
  ; ⟨_,_⟩ = glue As Bs
  ; commute₁ = commuteˡ As Bs
  ; commute₂ = commuteʳ As Bs
  ; universal = N-universal As Bs
  }

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --cubical --no-import-sorts #-}
module Cubical.Codata.Stream where

open import Cubical.Codata.Stream.Base public

open import Cubical.Codata.Stream.Properties public

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:
module Structure.Operator.Ring.Proofs where

import      Data.Tuple as Tuple
open import Functional
open import Logic.IntroInstances
open import Logic.Propositional
import      Lvl
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Operator.Ring
open import Structure.Operator
open import Structure.Operator.Proofs
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Implication
open import Syntax.Transitivity
open import Type.Properties.MereProposition
open import Type.Properties.Singleton
open import Type.Properties.Singleton.Proofs
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}
private variable _+_ _⋅_ : T → T → T

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ rng : Rng{T = T}(_+_)(_⋅_) ⦄ where
  open Rng(rng)

  instance
    [+]-cancellationₗ : Cancellationₗ(_+_)
    [+]-cancellationₗ = One.cancellationₗ-by-associativity-inverse

  instance
    [+]-cancellationᵣ : Cancellationᵣ(_+_)
    [+]-cancellationᵣ = One.cancellationᵣ-by-associativity-inverse

  instance
    [⋅]-absorberₗ : Absorberₗ(_⋅_)(𝟎)
    Absorberₗ.proof [⋅]-absorberₗ {x} = One.zero-when-redundant-addition $
      𝟎 ⋅ x             🝖-[ congruence₂ₗ(_⋅_)(x) (identityₗ(_+_)(𝟎)) ]-sym
      (𝟎 + 𝟎) ⋅ x       🝖-[ distributivityᵣ(_⋅_)(_+_) ]
      (𝟎 ⋅ x) + (𝟎 ⋅ x) 🝖-end

  instance
    [⋅]-absorberᵣ : Absorberᵣ(_⋅_)(𝟎)
    Absorberᵣ.proof [⋅]-absorberᵣ {x} = One.zero-when-redundant-addition $
      x ⋅ 𝟎             🝖-[ congruence₂ᵣ(_⋅_)(x) (identityₗ(_+_)(𝟎)) ]-sym
      x ⋅ (𝟎 + 𝟎)       🝖-[ distributivityₗ(_⋅_)(_+_) ]
      (x ⋅ 𝟎) + (x ⋅ 𝟎) 🝖-end

  -- TODO: Stuff provable in groups
  [−]-binaryOperator : BinaryOperator(_−_)
  BinaryOperator.congruence [−]-binaryOperator {x₁}{y₁}{x₂}{y₂} xy1 xy2 =
    (x₁ − x₂)     🝖[ _≡_ ]-[]
    (x₁ + (− x₂)) 🝖[ _≡_ ]-[ congruence₂(_+_) xy1 (congruence₁(−_) xy2) ]
    (y₁ + (− y₂)) 🝖[ _≡_ ]-[]
    (y₁ − y₂)     🝖-end

  postulate [⋅][−]-distributivityₗ : Distributivityₗ(_⋅_)(_−_)
  postulate [⋅][−]-distributivityᵣ : Distributivityᵣ(_⋅_)(_−_)

  instance
    [−]-involution : Involution(−_)
    [−]-involution = intro One.double-inverse

  [+]-negation-distribution : ∀{x y} → (−(x + y) ≡ (− x) + (− y))
  [+]-negation-distribution = One.inverse-distribution 🝖 commutativity(_+_)

  [−]-negation-distribution : ∀{x y} → (−(x − y) ≡ y − x)
  [−]-negation-distribution = One.inverse-distribution 🝖 congruence₂ₗ(_−_) ⦃ [−]-binaryOperator ⦄ (_) (involution(−_))

  -- TODO: See abs-of-negation for a similiar proof
  postulate zero-when-equal-negation : ∀{x} → (− x ≡ x) → (x ≡ 𝟎)

  instance
    [+]-inversePropₗ : InversePropertyₗ(_+_)(−_)
    [+]-inversePropₗ = One.inverse-propertyₗ-by-groupₗ

  instance
    [+]-inversePropᵣ : InversePropertyᵣ(_+_)(−_)
    [+]-inversePropᵣ = One.inverse-propertyᵣ-by-groupᵣ

  [+][−]-inverseOperᵣ : InverseOperatorᵣ(_+_)(_−_)
  [+][−]-inverseOperᵣ = One.standard-inverse-inverse-operatorᵣ-by-inverse-propᵣ ⦃ inverPropᵣ = [+]-inversePropᵣ ⦄

  [−][+]-inverseOperᵣ : InverseOperatorᵣ(_−_)(_+_)
  [−][+]-inverseOperᵣ = One.standard-inverse-operatorᵣ-by-involuting-inverse-propᵣ ⦃ inverPropᵣ = [+]-inversePropᵣ ⦄

  -- TODO: Defined set subset of natural numbers and integers by using summation ∑. That is: (x ∈ ℕ) = ∃{Obj = ℕ}(n ↦ ∑(0 ‥ n) (const 𝟏))

  [−]-of-𝟎 : ((− 𝟎) ≡ 𝟎)
  [−]-of-𝟎 =
    − 𝟎       🝖-[ symmetry(_≡_) (identityₗ(_+_)(𝟎)) ]
    𝟎 + (− 𝟎) 🝖-[ inverseFunctionᵣ(_+_)(−_) ]
    𝟎         🝖-end

  [−]-is-𝟎 : ∀{x} → ((− x) ≡ 𝟎) ↔ (x ≡ 𝟎)
  [−]-is-𝟎 = [↔]-intro (p ↦ congruence₁(−_) p 🝖 [−]-of-𝟎) (p ↦ symmetry(_≡_) (involution(−_)) 🝖 congruence₁(−_) p 🝖 [−]-of-𝟎)

  [−]-difference-is-𝟎 : ∀{x y} → ((x − y) ≡ 𝟎) ↔ (x ≡ y)
  [−]-difference-is-𝟎 {x}{y} = [↔]-intro l r where
    l =
      (x     ≡ y    ) ⇒-[ congruence₂ᵣ(_−_) ⦃ [−]-binaryOperator ⦄ (x) ]
      (x − x ≡ x − y) ⇒-[ symmetry(_≡_) ]
      (x − y ≡ x − x) ⇒-[ _🝖 inverseFunctionᵣ(_+_)(−_) ]
      (x − y ≡ 𝟎    ) ⇒-end

    r =
      (x − y           ≡ 𝟎    ) ⇒-[]
      (x + (− y)       ≡ 𝟎    ) ⇒-[ congruence₂ₗ(_+_)(y) ]
      ((x + (− y)) + y ≡ 𝟎 + y) ⇒-[ symmetry(_≡_) (associativity(_+_)) 🝖_ ]
      (x + ((− y) + y) ≡ 𝟎 + y) ⇒-[ congruence₂ᵣ(_+_)(x) (symmetry(_≡_) (inverseFunctionₗ(_+_)(−_))) 🝖_ ]
      (x + 𝟎           ≡ 𝟎 + y) ⇒-[ (\p → symmetry(_≡_) (identityᵣ(_+_)(𝟎)) 🝖 p 🝖 identityₗ(_+_)(𝟎)) ]
      (x               ≡ y    ) ⇒-end

  module _ ⦃ unity : Unity(_+_)(_⋅_) ⦄ where
    open import Type.Properties.MereProposition
    open import Type.Properties.Singleton
    open import Type.Properties.Singleton.Proofs

    open Unity(unity)

    singleton-when-identities-equal : (𝟎 ≡ 𝟏) ↔ IsUnit(T)
    singleton-when-identities-equal = [↔]-intro l r where
      l : (𝟎 ≡ 𝟏) ← IsUnit(T)
      l p = uniqueness(_) ⦃ inst = unit-is-prop ⦃ proof = p ⦄ ⦄

      r : (𝟎 ≡ 𝟏) → IsUnit(T)
      IsUnit.unit       (r oi)     = 𝟎
      IsUnit.uniqueness (r oi) {x} =
        x     🝖[ _≡_ ]-[ identityᵣ(_⋅_)(𝟏) ]-sym
        x ⋅ 𝟏 🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅_)(x) oi ]-sym
        x ⋅ 𝟎 🝖[ _≡_ ]-[ absorberᵣ(_⋅_)(𝟎) ]
        𝟎     🝖-end

    [⋅]ₗ-of-[−1] : ∀{x} → ((− 𝟏) ⋅ x ≡ − x)
    [⋅]ₗ-of-[−1] {x} = One.unique-inverseᵣ-by-id $
      x + ((− 𝟏) ⋅ x)       🝖-[ congruence₂ₗ(_+_)(_) (identityₗ(_⋅_)(𝟏)) ]-sym
      (𝟏 ⋅ x) + ((− 𝟏) ⋅ x) 🝖-[ distributivityᵣ(_⋅_)(_+_) ]-sym
      (𝟏 + (− 𝟏)) ⋅ x       🝖-[ congruence₂ₗ(_⋅_)(x) (inverseFunctionᵣ(_+_)(−_)) ]
      𝟎 ⋅ x                 🝖-[ absorberₗ(_⋅_)(𝟎) ]
      𝟎                     🝖-end

    [⋅]ᵣ-of-[−1] : ∀{x} → (x ⋅ (− 𝟏) ≡ − x)
    [⋅]ᵣ-of-[−1] {x} = One.unique-inverseₗ-by-id $
      (x ⋅ (− 𝟏)) + x       🝖-[ congruence₂ᵣ(_+_)(_) (identityᵣ(_⋅_)(𝟏)) ]-sym
      (x ⋅ (− 𝟏)) + (x ⋅ 𝟏) 🝖-[ distributivityₗ(_⋅_)(_+_) ]-sym
      x ⋅ ((− 𝟏) + 𝟏)       🝖-[ congruence₂ᵣ(_⋅_)(x) (inverseFunctionₗ(_+_)(−_)) ]
      x ⋅ 𝟎                 🝖-[ absorberᵣ(_⋅_)(𝟎) ]
      𝟎                     🝖-end

    [⋅]ₗ-of-[−] : ∀{x y} → ((− x) ⋅ y ≡ −(x ⋅ y))
    [⋅]ₗ-of-[−] {x}{y} =
      ((− x) ⋅ y)       🝖-[ congruence₂ₗ(_⋅_)(y) [⋅]ₗ-of-[−1] ]-sym
      (((− 𝟏) ⋅ x) ⋅ y) 🝖-[ associativity(_⋅_) ]
      ((− 𝟏) ⋅ (x ⋅ y)) 🝖-[ [⋅]ₗ-of-[−1] ]
      (−(x ⋅ y))        🝖-end

    [⋅]ᵣ-of-[−] : ∀{x y} → (x ⋅ (− y) ≡ −(x ⋅ y))
    [⋅]ᵣ-of-[−] {x}{y} =
      (x ⋅ (− y))       🝖-[ congruence₂ᵣ(_⋅_)(x) [⋅]ᵣ-of-[−1] ]-sym
      (x ⋅ (y ⋅ (− 𝟏))) 🝖-[ associativity(_⋅_) ]-sym
      ((x ⋅ y) ⋅ (− 𝟏)) 🝖-[ [⋅]ᵣ-of-[−1] ]
      (−(x ⋅ y))        🝖-end

    [⋅]-of-[−] : ∀{x y} → ((− x) ⋅ (− y) ≡ x ⋅ y)
    [⋅]-of-[−] {x}{y} =
      ((− x) ⋅ (− y)) 🝖[ _≡_ ]-[ [⋅]ᵣ-of-[−] ]
      −((− x) ⋅ y)    🝖[ _≡_ ]-[ congruence₁(−_) [⋅]ₗ-of-[−] ]
      −(−(x ⋅ y))     🝖[ _≡_ ]-[ involution(−_) ]
      (x ⋅ y)         🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Lambda where

open import Data.Bool   using    (true; false)
open import Data.Nat    renaming (_≟_ to _≟N_)
import      Data.Stream as S
open import Data.Vec    using    ([]; _∷_)
open import Relation.Binary.PropositionalEquality

open import Check
open import Eval
open import Operations.Combinatorial
open import Operations.Stateful
open import Types
open import Utils

ex₀ : S.take 5 ([] ⟦ alternator bitO ⟧) ≡ false ∷ true ∷ false ∷ true ∷ false ∷ []
ex₀ = refl

ex₁ : S.take 5 ([] ⟦ constant bitI ⟧) ≡ true ∷ true ∷ true ∷ true ∷ true ∷ []
ex₁ = refl

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc


text:
-- Andreas, 2012-06-05 let for record patterns

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

module LetPair where

import Common.Level
-- open import Common.Equality

data _×_ (A B : Set) : Set where
  _,_ : (fst : A)(snd : B) → A × B

swap : {A B : Set} → A × B → B × A
swap p =
  let (a , b) = p  -- works only for record patterns
  in  (b , a)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Unit where

open import Light.Level using (Level ; Setω)

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓ : Level
            Unit : Set ℓ
            unit : Unit
open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

module RepresPerm where

open import Enumeration using (Enum)
open import Equiv
  using (_≃_; id≃; sym≃; trans≃; mkqinv; module qinv; _⋆_; path⊎)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin; zero)
open import Data.Product using (_,_)
open import FinEquiv
open import Data.Unit using (⊤)
open import Data.Sum using (_⊎_)
open import LeftCancellation

-- A Representable Permutation consists of
-- 1. an Enumeration of A
-- 2. an Enumeration of B
-- 3. an isomorphism between A and B

record RPerm (A : Set) (n : ℕ) (B : Set) (m : ℕ) : Set where
  constructor rp
  field
    #A : Enum A n
    #B : Enum B m
    iso : A ≃ B

open RPerm

-- first theorem about these: same size!
thm1 : ∀ {n m} {A B} → (X : RPerm A n B m) → n ≡ m
thm1 {0} {0 } (rp _ _ _ ) = refl
thm1 {0} {suc m} (rp (fA , isoA) (fB , mkqinv g α β) (f , iso)) with fA (I.g (g zero))
  where module I = qinv iso
... | ()
thm1 {suc n} {0} (rp (fA , isoA) B≃Fm (f , iso)) with B≃Fm ⋆ f (IA.g zero)
  where module IA = qinv isoA
... | ()
thm1 {suc n} {suc m} {A} {B} (rp A≃Fsn B≃Fsm A≃B) =
  cong suc (thm1 {n} {m} {Fin n} {Fin m} (rp id≃ id≃ Fn≃Fm))
  where
    Fsn≃Fsm : Fin (suc n) ≃ Fin (suc m)
    Fsn≃Fsm = trans≃ (trans≃ (sym≃ A≃Fsn) A≃B) B≃Fsm
    1+n≃1+m : (Fin 1 ⊎ Fin n) ≃ (Fin 1 ⊎ Fin m)
    1+n≃1+m = trans≃ (trans≃ (Plus.fwd-iso {suc 0} {n}) Fsn≃Fsm)
                                                    (sym≃ (Plus.fwd-iso {suc 0} {m}))
    ⊤⊎n≃⊤⊎m : (⊤ ⊎ Fin n) ≃ (⊤ ⊎ Fin m)
    ⊤⊎n≃⊤⊎m = trans≃ (trans≃ (path⊎ (sym≃ Fin1≃⊤) id≃) 1+n≃1+m)
                                                    (path⊎ Fin1≃⊤ id≃)
    Fn≃Fm = left-cancel-⊤ ⊤⊎n≃⊤⊎m

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; ≲-trans ; _**_ ; _≋_ )
open import Web.Semantic.DL.KB using ( KB ; _,_ ; tbox )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( _,_ )
open import Web.Semantic.Util using ( _⊕_⊕_ ; inode ; enode )

module Web.Semantic.DL.Integrity {Σ : Signature} {X V Y : Set} where

-- A variant of the notion of OWL integrity in:

--   Boris Motik, Ian Horrocks, and Ulrike Sattler. Bridging the gap between OWL and
--   relational databases. In Proc. Conf. World Wide Web (WWW2007), pp 807–816, 2007.

-- They propose defining that an integrity constraint S (given as a T-Box) is valid
-- for a knowlege base K whenever S is valid in every minimal Herbrand model.
-- We strengthen this requirement to say that there is a minimal model of K,
-- which validtes S.

infixr 4 _>>_ _,_
infix 2 _⊕_⊨_

-- J ∈ Initial I K whenever J is the initial extension of I
-- satisfying K, that is there is I≲J s.t. I ⊨ K
-- and for any other such I≲K, there is a unique
-- J≲K which commutes with I≲J and I≲K.

_>>_ : ∀ {I : Interp Σ X} {J K : Interp Σ (X ⊕ V ⊕ Y)} →
  (I ≲ inode * J) → (J ≲ K) → (I ≲ inode * K)
I≲J >> J≲K = ≲-trans I≲J (inode ** J≲K)

Unique : ∀ (I : Interp Σ X) → (J K : Interp Σ (X ⊕ V ⊕ Y)) →
  (I ≲ inode * J) → (I ≲ inode * K) → Set
Unique I J K I≲J I≲K = ∀ (J≲₁K J≲₂K : J ≲ K) →
  (I≲K ≋ I≲J >> J≲₁K) → (I≲K ≋ I≲J >> J≲₂K) → (J≲₁K ≋ J≲₂K)

data Mediated (I : Interp Σ X) (J K : Interp Σ (X ⊕ V ⊕ Y))
  (I≲J : I ≲ inode * J) (I≲K : I ≲ inode * K) : Set where
    _,_ : (J≲K : J ≲ K) → (I≲K ≋ I≲J >> J≲K) × (Unique I J K I≲J I≲K)
      → Mediated I J K I≲J I≲K

med-≲ : ∀ {I} {J K : Interp Σ (X ⊕ V ⊕ Y)} {I≲J I≲K} →
  (Mediated I J K I≲J I≲K) → (J ≲ K)
med-≲ (J≲K , I≲K≋I≲J≲K , J≲K-uniq) = J≲K

med-≋ : ∀ {I} {J K : Interp Σ (X ⊕ V ⊕ Y)} {I≲J I≲K} →
  (m : Mediated I J K I≲J I≲K) → (I≲K ≋ I≲J >> med-≲ m)
med-≋ (J≲K , I≲K≋I≲J≲K , J≲K-uniq) = I≲K≋I≲J≲K

med-uniq : ∀ {I} {J K : Interp Σ (X ⊕ V ⊕ Y)} {I≲J I≲K} →
  (Mediated I J K I≲J I≲K) → Unique I J K I≲J I≲K
med-uniq (J≲K , I≲K≋I≲J≲K , J≲K-uniq) = J≲K-uniq

Mediator : ∀ (I : Interp Σ X) → (J : Interp Σ (X ⊕ V ⊕ Y)) →
  (I ≲ inode * J) → (KB Σ (X ⊕ V ⊕ Y)) → Set₁
Mediator I J I≲J KB =
  ∀ K (I≲K : I ≲ inode * K) → (K ⊨ KB) → Mediated I J K I≲J I≲K

data Initial I KB (J : Interp Σ (X ⊕ V ⊕ Y)) : Set₁ where
  _,_ : ∀ (I≲J : I ≲ inode * J) → (J ⊨ KB) × (Mediator I J I≲J KB) →
    (J ∈ Initial I KB)

init-≲ : ∀ {I KB} {J : Interp Σ (X ⊕ V ⊕ Y)} →
  (J ∈ Initial I KB) → (I ≲ inode * J)
init-≲ (I≲J , J⊨KB , J-med) = I≲J

init-⊨ : ∀ {I KB} {J : Interp Σ (X ⊕ V ⊕ Y)} →
  (J ∈ Initial I KB) → (J ⊨ KB)
init-⊨ (I≲J , J⊨KB , J-med) = J⊨KB

init-med : ∀ {I KB} {J : Interp Σ (X ⊕ V ⊕ Y)} →
  (J-init : J ∈ Initial I KB) → Mediator I J (init-≲ J-init) KB
init-med (I≲J , J⊨KB , J-med) = J-med

-- I ⊕ KB₁ ⊨ KB₂ whenever the initial extension of I satisfying
-- KB₁ exists, and has exports satisfying KB₂.

data _⊕_⊨_ I (KB₁ : KB Σ (X ⊕ V ⊕ Y)) KB₂ : Set₁ where
    _,_ : ∀ J → ((J ∈ Initial I KB₁) × (enode * J ⊨ KB₂)) → (I ⊕ KB₁ ⊨ KB₂)

extension : ∀ {I KB₁ KB₂} → (I ⊕ KB₁ ⊨ KB₂) → (Interp Σ (X ⊕ V ⊕ Y))
extension (J , J-init , J⊨KB₂) = J

ext-init : ∀ {I} {KB₁ : KB Σ (X ⊕ V ⊕ Y)} {KB₂} →
  (I⊕KB₁⊨KB₂ : I ⊕ KB₁ ⊨ KB₂) → (extension I⊕KB₁⊨KB₂ ∈ Initial I KB₁)
ext-init (J , J-init , J⊨KB₂) = J-init

ext-⊨ : ∀ {I} {KB₁ : KB Σ (X ⊕ V ⊕ Y)} {KB₂} →
  (I⊕KB₁⊨KB₂ : I ⊕ KB₁ ⊨ KB₂) → (enode * (extension I⊕KB₁⊨KB₂) ⊨ KB₂)
ext-⊨ (J , J-init , J⊨KB₂) = J⊨KB₂

ext✓ : ∀ {I S T} {F : ABox Σ (X ⊕ V ⊕ Y)} {B} →
  (I⊕SF⊨TB : I ⊕ S , F ⊨ T , B) →
    (enode * (extension I⊕SF⊨TB) ⊨ (S , T) , B)
ext✓ I⊕SF⊨TB =
  ( ( proj₁ (init-⊨ (ext-init I⊕SF⊨TB))
    , proj₁ (ext-⊨ I⊕SF⊨TB) )
  , proj₂ (ext-⊨ I⊕SF⊨TB) )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Sort where
  open import Sec4
  import Sec2
  postulate _≤_ : {A : Set} →  A → A → Prop
  postulate tot-list : {A : Set} → (a b : A) → (a ≤ b) ∨ (b ≤ a)
  postulate trans-list :  {A : Set} → (a b c : A) → (a ≤ b) → (b ≤ c) → (a ≤ c)

-- XXX: Definition of a list
  data List (A : Set) : Set where
    Nil : List A
    _∷_ : A → List A → List A

-- XXX: definition of an ordered list
  all-ordered-list : {A : Set} → (a : A)
                     → (l : List A)
                     → Prop
  all-ordered-list a Nil = ⊤
  all-ordered-list a (x ∷ l) = (a ≤ x) ∧ all-ordered-list a l

  ordered-list : {A : Set} → List A → Prop
  ordered-list Nil = ⊤
  ordered-list (x ∷ l) = all-ordered-list x l ∧ (ordered-list l)

-- XXX: Inserting elements in the list
  insert-list : {A : Set} → (a : A) → (l : List A) → List A
  insert-list a Nil = a ∷ Nil
  insert-list a (x ∷ l) with (tot-list a x)
  insert-list a (x ∷ l) | ora h = a ∷ (x ∷ l)
  insert-list a (x ∷ l) | orb h = x ∷ (insert-list a l)

  lem1 : {A : Set}
         → (a x : A)
         → (l : List A)
         → (p : all-ordered-list x l)
         → (p1 : a ≤ x)
         → (all-ordered-list a l)
  lem1 a x Nil p p1 = ⋆
  lem1 a x (x₁ ∷ l) (and x₂ x₃) p1 = and (trans-list a x x₁ p1 x₂) (lem1 a x l x₃ p1)

  lem2 : {A : Set} → (x a : A) → (l : List A) → (h : x ≤ a)
         → (p1 : all-ordered-list x l) → (p2 : ordered-list l)
         → (v : ordered-list (insert-list a l))
         → all-ordered-list x (insert-list a l)
  lem2 x a Nil h p1 p3 v = and h ⋆
  lem2 x a (x₁ ∷ l) h p1 p3 v with (tot-list a x₁)
  lem2 x₂ a (x₁ ∷ l) h p1 p3 v | ora x = and h p1
  lem2 x₂ a (x₁ ∷ l) h (and x₃ x₄) (and x₅ x₆) (and x₇ x₈) | orb x = and x₃ (lem2 x₂ a l h x₄ x₆ x₈)

  thm2 : {A : Set}
         → ∀ (a : A)
         → ∀ (l : List A)
         → (p : ordered-list l)
         → (ordered-list (insert-list a l))
  thm2 a Nil p = and ⋆ ⋆
  thm2 a (x ∷ l) p with (tot-list a x)
  thm2 a (x ∷ l) (and x₁ x₂) | ora h = and (and h (lem1 a x l x₁ h)) (and x₁ x₂)
  thm2 a (x ∷ l) (and x₁ x₂) | orb h =
                                   let v = (thm2 a l x₂)
                                   in
                                   and (lem2 x a l h x₁ x₂ v) v

-- XXX: append lists
  _++_ : {A : Set} → (l : List A) → (m : List A) → List A
  Nil ++ m = m
  (x ∷ l) ++ m = x ∷ (l ++ m)

-- XXX: Length of a list
  length : {A : Set} → (l : List A) → Sec2.ℕ
  length Nil = Sec2.Z
  length (x ∷ l) = Sec2.S (length l)

-- XXX: reverse of a list
  rev : {A : Set} → (List A) → (List A)
  rev Nil = Nil
  rev (x ∷ l) = (rev l) ++ (x ∷ Nil)

-- XXX: Theorem on length of lists
  thm : {A : Set} → (l : List A) → (m : List A) → ((length l) Sec2.+ (length m) Sec2.≡ length (l ++ m))
  thm Nil m = Sec2.refl
  thm (x ∷ l) m =
                let
                  xx = thm l m
                in
                Sec2.cong xx

  cong : {A : Set} → (x : A) → (l m : List A) → (l Sec2.≡ m)
         → (x ∷ l) Sec2.≡ (x ∷ m)
  cong x l .l Sec2.refl = Sec2.refl

  cong2 : {A : Set} → (l m q : List A) → (l Sec2.≡ m)
          → (l ++ q) Sec2.≡ (m ++ q)
  cong2 l .l q Sec2.refl = Sec2.refl

  ++-lem : {A : Set} → (l : List A) → ((l ++ Nil) Sec2.≡ l)
  ++-lem Nil = Sec2.refl
  ++-lem (x ∷ l) = cong x (l ++ Nil) l (++-lem l)

  assoc : {A : Set} → (l m q : List A)
          → l ++ (m ++ q) Sec2.≡ (l ++ m) ++ q
  assoc Nil m q = Sec2.refl
  assoc (x ∷ l) m q = cong x (l ++ (m ++ q)) ((l ++ m) ++ q) (assoc l m q)

  rev-lem : {A : Set} → ∀ (l m : List A)
            → rev (l ++ m) Sec2.≡ (rev m) ++ (rev l)
  rev-lem Nil m rewrite
                ++-lem (rev m) = Sec2.refl
  rev-lem (x ∷ l) m rewrite
                    assoc (rev m) (rev l) (x ∷ Nil)
                    = let p = rev-lem l m in
                      cong2 (rev (l ++ m)) (rev m ++ rev l) (x ∷ Nil) p

-- XXX: Involution of reversal of lists
  rev-involute : {A : Set} → (l : List A) → l Sec2.≡ (rev (rev l))
  rev-involute Nil = Sec2.refl
  rev-involute (x ∷ l) rewrite
                       rev-lem (rev l) (x ∷ Nil)
                       = cong x l (rev (rev l)) (rev-involute l)


text:
open import Coinduction using ( ♭ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong ; cong₂ )
open import System.IO.Transducers using ( _⇒_ ; inp ; out ; done ; out*' ; _⟫_ ; _⟨&⟩_ ; _⟨&⟩[_]_ ; discard ; π₁ ; π₂ ; ⟦_⟧ ; _≃_ )
open import System.IO.Transducers.Session using ( [] ; _∷_ ; _&_ )
open import System.IO.Transducers.Trace using ( _≤_ ; Trace ; [] ; _∷_ )
open import System.IO.Transducers.Properties.Lemmas using ( cong₃ ; revApp ; out*'-semantics )
open import System.IO.Transducers.Properties.BraidedMonoidal using ( _++_ )
open import System.IO.Transducers.Properties.Category using ( _⟦⟫⟧_ ; ⟫-semantics )

module System.IO.Transducers.Properties.LaxProduct where

open Relation.Binary.PropositionalEquality.≡-Reasoning

_⟦⟨&⟩⟧_ : ∀ {S T U} →
  (f : Trace S → Trace T) → (g : Trace S → Trace U) →
    (Trace S) → (Trace (T & U))
(f ⟦⟨&⟩⟧ g) as = f as ++ g as

_⟦⟨&⟩[_]⟧_ : ∀ {S T U V} →
  (Trace S → Trace T) → (U ≤ V) → (Trace S → Trace U) →
    (Trace S → Trace (T & V))
(f ⟦⟨&⟩[ cs ]⟧ g) as = f as ++ (revApp cs (g as))

⟨&⟩[]-semantics : ∀ {S T U V} →
  (P : S ⇒ T) → (cs : U ≤ V) →  (Q : S ⇒ U) →
    (⟦ P ⟨&⟩[ cs ] Q ⟧ ≃ ⟦ P ⟧ ⟦⟨&⟩[ cs ]⟧ ⟦ Q ⟧)
⟨&⟩[]-semantics (inp {T = []}     F) cs Q         as with ⟦ inp F ⟧ as
⟨&⟩[]-semantics (inp {T = []}     F) cs Q         as    | [] = out*'-semantics cs Q as
⟨&⟩[]-semantics (inp {T = W ∷ Ts} F) cs (inp G)   []         = refl
⟨&⟩[]-semantics (inp {T = W ∷ Ts} F) cs (inp G)   (a ∷ as)   = ⟨&⟩[]-semantics (♭ F a) cs (♭ G a) as
⟨&⟩[]-semantics (inp {T = W ∷ Ts} F) cs (out c Q) as         = ⟨&⟩[]-semantics (inp F) (c ∷ cs) Q as
⟨&⟩[]-semantics (inp {T = W ∷ Ts} F) cs done      []         = refl
⟨&⟩[]-semantics (inp {T = W ∷ Ts} F) cs done      (a ∷ as)   = ⟨&⟩[]-semantics (♭ F a) (a ∷ cs) done as
⟨&⟩[]-semantics (out b P)            cs Q         as         = cong (_∷_ b) (⟨&⟩[]-semantics P cs Q as)
⟨&⟩[]-semantics (done {[]})          cs Q         []         = out*'-semantics cs Q []
⟨&⟩[]-semantics (done {W ∷ Ts})      cs (inp F)   []         = refl
⟨&⟩[]-semantics (done {W ∷ Ts})      cs (inp F)   (a ∷ as)   = cong (_∷_ a) (⟨&⟩[]-semantics done cs (♭ F a) as)
⟨&⟩[]-semantics (done {W ∷ Ts})      cs (out c Q) as         = ⟨&⟩[]-semantics done (c ∷ cs) Q as
⟨&⟩[]-semantics (done {W ∷ Ts})      cs done      []         = refl
⟨&⟩[]-semantics (done {W ∷ Ts})      cs done      (a ∷ as)   = cong (_∷_ a) (⟨&⟩[]-semantics done (a ∷ cs) done as)

⟨&⟩-semantics : ∀ {S T U} →
  (P : S ⇒ T) → (Q : S ⇒ U) →
    (⟦ P ⟨&⟩ Q ⟧ ≃ ⟦ P ⟧ ⟦⟨&⟩⟧ ⟦ Q ⟧)
⟨&⟩-semantics P Q = ⟨&⟩[]-semantics P [] Q

⟫-dist-⟨&⟩ : ∀ {S T U V} →
  (P : T ⇒ U) → (Q : T ⇒ V) → (R : S ⇒ T) →
    (⟦ R ⟫ (P ⟨&⟩ Q) ⟧ ≃ ⟦ (R ⟫ P) ⟨&⟩ (R ⟫ Q) ⟧)
⟫-dist-⟨&⟩ P Q R as =
  begin
    ⟦ R ⟫ P ⟨&⟩ Q ⟧ as
  ≡⟨ ⟫-semantics R (P ⟨&⟩ Q) as ⟩
    ⟦ P ⟨&⟩ Q ⟧ (⟦ R ⟧ as)
  ≡⟨ ⟨&⟩-semantics P Q (⟦ R ⟧ as) ⟩
    ⟦ P ⟧ (⟦ R ⟧ as) ++ ⟦ Q ⟧ (⟦ R ⟧ as)
  ≡⟨ cong₂ _++_ (sym (⟫-semantics R P as)) (sym (⟫-semantics R Q as)) ⟩
    ⟦ R ⟫ P ⟧ as ++ ⟦ R ⟫ Q ⟧ as
  ≡⟨ sym (⟨&⟩-semantics (R ⟫ P) (R ⟫ Q) as) ⟩
    ⟦ (R ⟫ P) ⟨&⟩ (R ⟫ Q) ⟧ as
  ∎

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module fold-Tree where

open import map-Tree using (Tree; leaf; node)

fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
fold-Tree f _ (leaf a)             = f a
fold-Tree f g (node treeˡ b treeʳ) = g (fold-Tree f g treeˡ) b (fold-Tree f g treeʳ)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module moveArg where
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool

stuff : ( number : Nat) -> Bool -> Bool
stuff number bool = {!   !}

stuff2 : Nat -> Bool -> Bool
stuff2 number bool = bool

nonsense : Bool
nonsense = stuff 0 true

dep : (A : Set) -> (B : A) -> Bool -> Bool
dep a b c = c

unnamedDep : (A : Set) -> A -> Bool -> Bool
unnamedDep a b c = c

sameName : (A : Set) -> {A : Set} -> A -> A
sameName set a = a

nonDep : (A : Set) -> (B : Set) -> B -> B
nonDep set1 set2 b = b

data List (A : Set) : Nat -> Set where
    nil : List A 0
    cons : {n : Nat} -> A -> List A n -> List A (suc n)

map : {n : Nat} -> {A : Set} -> {B : Set} -> (A -> B) -> List A n -> List B n
map f nil = nil
map f (cons x xs) = cons (f x) (map f xs)

map2 : {A : Set} -> {n : Nat} -> {B : Set} -> (A -> B) -> List A n -> List B n
map2 f nil = nil
map2 f (cons x xs) = cons (f x) (map2 f xs)


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

-- This module defines an intermediate calculus that is set up in the D<: universe
-- which bridges F<:- and D<:. The goal here is purely technical - to simply reduce
-- duplication.
module DsubReduced where

open import Data.List as List
open import Data.List.All as All
open import Data.Nat as ℕ
open import Data.Maybe as Maybe
open import Data.Product
open import Function

open import Data.Maybe.Properties as Maybeₚ
open import Data.Nat.Properties as ℕₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as ≡

open import DsubDef
open import FsubMinus
open import FsubMinus2
open import Utils

-- D<: Reduced
--
-- This judgment for contexts and types in D<: defines a corresponding calculus after
-- interpreting F<:⁻ into D<:. That is, D<: reduced is the image derivation of
-- interpreting F<:⁻ in D<:.
infix 4 _⊢ᵣ_<:_
data _⊢ᵣ_<:_ : Env → Typ → Typ → Set where
  drtop   : ∀ {Γ T} → Covar T → Γ ⊢ᵣ T <: ⊤
  drrefl  : ∀ {Γ T} → Covar T → Γ ⊢ᵣ T <: T
  drall   : ∀ {Γ S U S′ U′} →
              Covar S → Covar U → Covar S′ → Covar U′ →
              (S′<:S : Γ ⊢ᵣ S′ <: S) →
              (U<:U′ : ⟨A: ⊥ ⋯ S′ ⟩ ∷ Γ ⊢ᵣ U <: U′) →
              Γ ⊢ᵣ Π ⟨A: ⊥ ⋯ S ⟩ ∙ U <: Π ⟨A: ⊥ ⋯ S′ ⟩ ∙ U′
  drsel   : ∀ {Γ n U U′} →
              (T∈Γ : env-lookup Γ n ≡ just ⟨A: ⊥ ⋯ U ⟩) →
              Covar U →
              Γ ⊢ᵣ U <: U′ →
              Γ ⊢ᵣ n ∙A <: U′

module FsubMinusToDsubR where
  open FsubMinus.FsubMinus renaming (Env to Env′ ; _↑_ to _⇑_) hiding (env-lookup)

  infix 5 ⟦_⟧ ⟪_⟫
  ⟦_⟧ : Ftyp → Typ
  ⟦ ⊤ ⟧         = ⊤
  ⟦ var x ⟧     = x ∙A
  ⟦ Π<: S ∙ U ⟧ = Π ⟨A: ⊥ ⋯ ⟦ S ⟧ ⟩ ∙ ⟦ U ⟧

  ⟪_⟫ : Env′ → Env
  ⟪ [] ⟫    = []
  ⟪ T ∷ Γ ⟫ = ⟨A: ⊥ ⋯ ⟦ T ⟧ ⟩ ∷ ⟪ Γ ⟫

  module ⟦⟧-Bijective where
    open import Function.Bijection
    open import Function.Surjection
    open import Function.Equality

    CovTyp : Set
    CovTyp = ∃ λ T → Covar T

    ⟦⟧-covar : ∀ T → Covar ⟦ T ⟧
    ⟦⟧-covar ⊤           = cv⊤
    ⟦⟧-covar (var x)     = cv∙A _
    ⟦⟧-covar (Π<: S ∙ U) = cvΠ (⟦⟧-covar S) (⟦⟧-covar U)

    ⟦⟧-func : ≡.setoid Ftyp ⟶ ≡.setoid CovTyp
    ⟦⟧-func   = record
      { _⟨$⟩_ = < ⟦_⟧ , ⟦⟧-covar >
      ; cong  = ≡.cong < ⟦_⟧ , ⟦⟧-covar >
      }

    ⟦⟧-injective : ∀ {S U} → ⟦ S ⟧ ≡ ⟦ U ⟧ → S ≡ U
    ⟦⟧-injective {⊤} {⊤} eq            = refl
    ⟦⟧-injective {⊤} {var x} ()
    ⟦⟧-injective {⊤} {Π<: _ ∙ _} ()
    ⟦⟧-injective {var x} {⊤} ()
    ⟦⟧-injective {var x} {var .x} refl = refl
    ⟦⟧-injective {var x} {Π<: _ ∙ _} ()
    ⟦⟧-injective {Π<: _ ∙ _} {⊤} ()
    ⟦⟧-injective {Π<: _ ∙ _} {var x} ()
    ⟦⟧-injective {Π<: S₁ ∙ U₁} {Π<: S₂ ∙ U₂} eq
      with ⟦ S₁ ⟧ | ⟦ S₂ ⟧ | ⟦ U₁ ⟧ | ⟦ U₂ ⟧
         | ⟦⟧-injective {S₁} {S₂} | ⟦⟧-injective {U₁} {U₂}
    ⟦⟧-injective {Π<: S₁ ∙ U₁} {Π<: S₂ ∙ U₂} refl
         | _ | _ | _ | _ | rec₁ | rec₂ = ≡.cong₂ Π<:_∙_ (rec₁ refl) (rec₂ refl)

    ⟦⟧-func-injective : ∀ {S U} → (CovTyp ∋ (⟦ S ⟧ , ⟦⟧-covar S)) ≡ (⟦ U ⟧ , ⟦⟧-covar U) → S ≡ U
    ⟦⟧-func-injective {S} {U} eq
      with ⟦ S ⟧ | ⟦⟧-covar S | ⟦ U ⟧ | ⟦⟧-covar U
         | ⟦⟧-injective {S} {U}
    ⟦⟧-func-injective {S} {U} refl
         | _ | _ | _ | _ | inj = inj refl

    infix 5 ⟦_⟧⁻¹
    ⟦_⟧⁻¹ : CovTyp → Ftyp
    ⟦ _ , cv⊤ ⟧⁻¹     = ⊤
    ⟦ _ , cv∙A x ⟧⁻¹  = var x
    ⟦ _ , cvΠ S U ⟧⁻¹ = Π<: ⟦ -, S ⟧⁻¹ ∙ ⟦ -, U ⟧⁻¹

    ⟦⟧-func-inv : ≡.setoid CovTyp ⟶ ≡.setoid Ftyp
    ⟦⟧-func-inv = record
      { _⟨$⟩_   = ⟦_⟧⁻¹
      ; cong    = ≡.cong ⟦_⟧⁻¹
      }

    ⟦⟧-left-inverse-⟦⟧⁻¹ : ∀ {T} (cT : Covar T) → (⟦ ⟦ -, cT ⟧⁻¹ ⟧ , ⟦⟧-covar ⟦ -, cT ⟧⁻¹) ≡ (CovTyp ∋ (-, cT))
    ⟦⟧-left-inverse-⟦⟧⁻¹ cv⊤           = refl
    ⟦⟧-left-inverse-⟦⟧⁻¹ (cv∙A n)      = refl
    ⟦⟧-left-inverse-⟦⟧⁻¹ (cvΠ S U)
      with ⟦ ⟦ -, S ⟧⁻¹ ⟧         | ⟦ ⟦ -, U ⟧⁻¹ ⟧
         | ⟦⟧-covar ⟦ -, S ⟧⁻¹    | ⟦⟧-covar ⟦ -, U ⟧⁻¹
         | ⟦⟧-left-inverse-⟦⟧⁻¹ S | ⟦⟧-left-inverse-⟦⟧⁻¹ U
    ...  | _ | _ | _ | _ | refl | refl = refl

    ⟦⟧-bijective : Bijective ⟦⟧-func
    ⟦⟧-bijective   = record
      { injective  = ⟦⟧-func-injective
      ; surjective = record
        { from             = ⟦⟧-func-inv
        ; right-inverse-of = λ { (_ , T) → ⟦⟧-left-inverse-⟦⟧⁻¹ T }
        }
      }

  open ⟦⟧-Bijective using (⟦⟧-covar ; ⟦⟧-injective) public

  ⟪⟫-contraEnv : ∀ Γ → ContraEnv ⟪ Γ ⟫
  ⟪⟫-contraEnv []      = []
  ⟪⟫-contraEnv (T ∷ Γ) = ctt (⟦⟧-covar T) ∷ ⟪⟫-contraEnv Γ

  ⟦⟧-↑-comm : ∀ T n → ⟦ T ⟧ ↑ n ≡ ⟦ T ⇑ n ⟧
  ⟦⟧-↑-comm ⊤ n = refl
  ⟦⟧-↑-comm (var x) n with n ≤? x
  ... | yes n≤x = refl
  ... | no n>x  = refl
  ⟦⟧-↑-comm (Π<: S ∙ U) n
    rewrite ⟦⟧-↑-comm S n | ⟦⟧-↑-comm U (suc n)
                = refl

  <:∈⇒env-lookup : ∀ {n T Γ} → n <: T ∈ Γ → env-lookup ⟪ Γ ⟫ n ≡ just ⟨A: ⊥ ⋯ ⟦ T ⟧ ⟩
  <:∈⇒env-lookup {_} {_} {T ∷ ._} hd
    rewrite ⟦⟧-↑-comm T 0       = refl
  <:∈⇒env-lookup {suc n} {_} {._ ∷ Γ} (tl {_} {T} T∈Γ)
    with lookupOpt ⟪ Γ ⟫ n | <:∈⇒env-lookup T∈Γ
  ...  | nothing           | ()
  ...  | just _            | eq
    rewrite sym $ ⟦⟧-↑-comm T 0 = cong (just ∘ (_↑ 0)) (just-injective eq)

  F<:⇒D<:ᵣ : ∀ {Γ S U} → Γ ⊢F S <: U → ⟪ Γ ⟫ ⊢ᵣ ⟦ S ⟧ <: ⟦ U ⟧
  F<:⇒D<:ᵣ ftop               = drtop (⟦⟧-covar _)
  F<:⇒D<:ᵣ fvrefl             = drrefl (cv∙A _)
  F<:⇒D<:ᵣ (fbinds T∈Γ T<:U)  = drsel (<:∈⇒env-lookup T∈Γ) (⟦⟧-covar _) (F<:⇒D<:ᵣ T<:U)
  F<:⇒D<:ᵣ (fall S′<:S U<:U′) = drall (⟦⟧-covar _) (⟦⟧-covar _) (⟦⟧-covar _) (⟦⟧-covar _)
                                      (F<:⇒D<:ᵣ S′<:S) (F<:⇒D<:ᵣ U<:U′)

  env-lookup⇒<:∈ : ∀ {n T Γ} → env-lookup Γ n ≡ just ⟨A: ⊥ ⋯ T ⟩ →
                   ∀ {Γ′} → Γ ≡ ⟪ Γ′ ⟫ →
                   ∃ λ T′ → T ≡ ⟦ T′ ⟧ × n <: T′ ∈ Γ′
  env-lookup⇒<:∈ T∈Γ eqΓ = aux (lookup⇒↦∈ T∈Γ) refl eqΓ
    where aux : ∀ {n T Γ} → n ↦ T ∈ Γ →
                   ∀ {U Γ′} → T ≡ ⟨A: ⊥ ⋯ U ⟩ → Γ ≡ ⟪ Γ′ ⟫ →
                   ∃ λ U′ → U ≡ ⟦ U′ ⟧ × n <: U′ ∈ Γ′
          aux hd {_} {[]} eqT ()
          aux hd {_} {T ∷ Γ′} refl refl
            rewrite ⟦⟧-↑-comm T 0 = T ⇑ zero , refl , hd
          aux (tl T∈Γ) {_} {[]} eqT ()
          aux (tl {T = ⊤} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = ⊥} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = n ∙A} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = Π S ∙ U} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = ⟨A: ⊤ ⋯ U ⟩} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = ⟨A: ⊥ ⋯ U ⟩} T∈Γ) {_} {_ ∷ Γ′} refl refl
            with aux T∈Γ refl refl
          ...  | U′ , refl , U′∈Γ′
            rewrite ⟦⟧-↑-comm U′ 0 = U′ ⇑ zero , refl , tl U′∈Γ′
          aux (tl {T = ⟨A: _ ∙A ⋯ U ⟩} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = ⟨A: Π _ ∙ _ ⋯ U ⟩} T∈Γ) {_} {_ ∷ Γ′} () refl
          aux (tl {T = ⟨A: ⟨A: _ ⋯ _ ⟩ ⋯ U ⟩} T∈Γ) {_} {_ ∷ Γ′} () refl

  D<:ᵣ⇒F<: : ∀ {Γ′ S′ U′} → Γ′ ⊢ᵣ S′ <: U′ →
            ∀ {Γ S U} →
              Γ′ ≡ ⟪ Γ ⟫ → S′ ≡ ⟦ S ⟧ → U′ ≡ ⟦ U ⟧ →
              Γ ⊢F S <: U
  D<:ᵣ⇒F<: (drtop S′) {Γ} {S} {⊤} eqΓ eqS refl   = ftop
  D<:ᵣ⇒F<: (drtop S′) {Γ} {S} {var x} eqΓ eqS ()
  D<:ᵣ⇒F<: (drtop S′) {Γ} {S} {Π<: U ∙ U₁} eqΓ eqS ()
  D<:ᵣ⇒F<: (drrefl S′) {Γ} {S} {U} eqΓ eqS eqU
    rewrite ⟦⟧-injective (≡.trans (sym eqS) eqU) = <:-refl Γ U
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {⊤} {⊤} eqΓ () eqU
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {⊤} {var x} eqΓ () eqU
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {⊤} {Π<: U ∙ U₁} eqΓ () eqU
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {var _} {⊤} eqΓ () eqU
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {var _} {var _} eqΓ () eqU
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {var _} {Π<: _ ∙ _} eqΓ () eqU
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {Π<: _ ∙ _} {⊤} eqΓ refl ()
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {Π<: _ ∙ _} {var _} eqΓ refl ()
  D<:ᵣ⇒F<: (drall cS cU cS′ cU′ S′<:S U<:U′) {Γ} {Π<: S ∙ U} {Π<: S′ ∙ U′} eqΓ refl refl
    = fall (D<:ᵣ⇒F<: S′<:S eqΓ refl refl)
           (D<:ᵣ⇒F<: U<:U′ (cong (⟨A: ⊥ ⋯ ⟦ S′ ⟧ ⟩ ∷_) eqΓ) refl refl)
  D<:ᵣ⇒F<: (drsel T∈Γ cT S<:U) {Γ} {⊤} {U} eqΓ () eqU
  D<:ᵣ⇒F<: (drsel T∈Γ cT S<:U) {Γ} {var x} {U} eqΓ refl eqU
    with env-lookup⇒<:∈ T∈Γ eqΓ
  ...  | U′ , eqU′ , T′∈Γ = fbinds T′∈Γ (D<:ᵣ⇒F<: S<:U eqΓ eqU′ eqU)
  D<:ᵣ⇒F<: (drsel T∈Γ cT S<:U) {Γ} {Π<: _ ∙ _} {U} eqΓ () eqU


text:
{-# OPTIONS --safe #-}
module Cubical.Data.List.FinData where

open import Cubical.Foundations.Prelude
open import Cubical.Data.List
open import Cubical.Data.FinData

variable
  ℓ : Level
  A : Type ℓ

-- copy-paste from agda-stdlib
lookup : ∀ (xs : List A) → Fin (length xs) → A
lookup (x ∷ xs) zero    = x
lookup (x ∷ xs) (suc i) = lookup xs i

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Minimal implicational modal logic, PHOAS approach, final encoding

module Pf.BoxMp where

open import Lib using (Nat; suc)

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty
  BOX  : Ty       -> Ty

-- Context and truth judgement with modal depth

Cx : Set1
Cx = Ty -> Nat -> Set

isTrue : Ty -> Nat -> Cx -> Set
isTrue a d tc = tc a d

-- Terms

TmRepr : Set1
TmRepr = Nat -> Cx -> Ty -> Set

module ArrMp where
  record Tm (tr : TmRepr) : Set1 where
    infixl 1 _$_
    field
      var  : forall {d tc a}   -> isTrue a d tc                 -> tr d tc a
      lam' : forall {d tc a b} -> (isTrue a d tc -> tr d tc b)  -> tr d tc (a => b)
      _$_  : forall {d tc a b} -> tr d tc (a => b) -> tr d tc a -> tr d tc b

    lam'' : forall {d tc a b} -> (tr d tc a -> tr d tc b) -> tr d tc (a => b)
    lam'' f = lam' \x -> f (var x)

    syntax lam'' (\a -> b) = lam a => b
  open Tm {{...}} public

module BoxMp where
  record Tm (tr : TmRepr) : Set1 where
    field
      box    : forall {d tc a}      -> tr (suc d) tc a          -> tr d tc (BOX a)
      unbox' : forall {d >d tc a b} -> tr d tc (BOX a) -> (isTrue a >d tc -> tr d tc b) -> tr d tc b

      isArrMp : ArrMp.Tm tr
    open ArrMp.Tm isArrMp public

    unbox'' : forall {d >d tc a b} -> tr d tc (BOX a) -> (tr >d tc a -> tr d tc b) -> tr d tc b
    unbox'' x' f = unbox' x' \x -> f (var x)

    syntax unbox'' x' (\x -> y) = unbox x' as x => y
  open Tm {{...}} public

  Thm : Ty -> Set1
  Thm a = forall {tr d tc} {{_ : Tm tr}} -> tr d tc a
open BoxMp public

-- Example theorems

rNec : forall {a} -> Thm a -> Thm (BOX a)
rNec x =
  box x

aK : forall {a b} -> Thm (BOX (a => b) => BOX a => BOX b)
aK =
  lam f' =>
    lam x' =>
      unbox f' as f =>
        unbox x' as x =>
          box (f $ x)

aT : forall {a} -> Thm (BOX a => a)
aT =
  lam x' =>
    unbox x' as x => x

a4 : forall {a} -> Thm (BOX a => BOX (BOX a))
a4 =
  lam x' =>
    unbox x' as x => box (box x)

t1 : forall {a} -> Thm (a => BOX (a => a))
t1 =
  lam _ => box (lam y => y)

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Equivalence closures of binary relations
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.Equivalence module directly.
------------------------------------------------------------------------

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

module Relation.Binary.EquivalenceClosure where

open import Relation.Binary.Construct.Closure.Equivalence public


text:
module Examples where

open import Prelude
open import T

---- some example programs
-- boy, de bruijn indexes are unreadable
w = weaken-closed

one : TNat
one = suc zero
two = suc one
three = suc two
t-plus : TCExp (nat ⇒ nat ⇒ nat)
t-plus = Λ (Λ (rec (var (S Z)) (var Z) (suc (var Z))))
t-compose : ∀{A B C} → TCExp ((A ⇒ B) ⇒ (C ⇒ A) ⇒ (C ⇒ B))
t-compose = Λ (Λ (Λ (var (S (S Z)) $ ((var (S Z)) $ (var Z)))))
t-id : ∀{A} → TCExp (A ⇒ A)
t-id = Λ (var Z)
t-iterate : ∀{A} → TCExp (nat ⇒ (A ⇒ A) ⇒ (A ⇒ A))
t-iterate = Λ (Λ (rec (var (S Z)) (w t-id)
                   (w t-compose $ var (S Z) $ var Z)))
t-ack : TCExp (nat ⇒ nat ⇒ nat)
t-ack = Λ (rec (var Z) (Λ (suc (var Z)))
            (Λ (w t-iterate $ var Z $ var (S Z) $ (var (S Z) $ w one))))
ack-test : TNat
ack-test = t-ack $ two $ two
plus-test : TNat
plus-test = t-plus $ two $ two

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
open import Prelude
open import Nat
open import List

module contexts where
  -- helper function
  diff-1 : ∀{n m} → n < m → Nat
  diff-1 n<m = difference (n<m→1+n≤m n<m)

  ---- the core declarations ----
  -- TODO move definitions

  _ctx : Set → Set
  A ctx = List (Nat ∧ A)

  -- nil context
  ∅ : {A : Set} → A ctx
  ∅ = []

  -- singleton context
  ■_ : {A : Set} → (Nat ∧ A) → A ctx
  ■_ (x , a) = (x , a) :: []

  infixr 100 ■_

  -- context extension/insertion - never use _::_
  _,,_ : ∀{A} → A ctx → (Nat ∧ A) → A ctx
  [] ,, (x , a) = ■ (x , a)
  ((hx , ha) :: t) ,, (x , a) with <dec x hx
  ... | Inl x<hx       = (x , a) :: ((diff-1 x<hx , ha) :: t)
  ... | Inr (Inl refl) = (x , a) :: t
  ... | Inr (Inr hx<x) = (hx , ha) :: (t ,, (diff-1 hx<x , a))

  infixl 10 _,,_

  -- membership, or presence, in a context
  data _∈_ : {A : Set} (p : Nat ∧ A) → (Γ : A ctx) → Set where
    InH : {A : Set} {Γ : A ctx} {x : Nat} {a : A} →
           (x , a) ∈ ((x , a) :: Γ)
    InT : {A : Set} {Γ : A ctx} {x s : Nat} {a a' : A} →
           (x , a) ∈ Γ →
           ((x + 1+ s , a)) ∈ ((s , a') :: Γ)

  -- the domain of a context
  dom : {A : Set} → A ctx → Nat → Set
  dom {A} Γ x = Σ[ a ∈ A ] ((x , a) ∈ Γ)

  -- apartness for contexts
  _#_ : {A : Set} (n : Nat) → (Γ : A ctx) → Set
  x # Γ = dom Γ x → ⊥

  _##_ : {A : Set} → A ctx → A ctx → Set
  Γ1 ## Γ2 = (x : Nat) → dom Γ1 x → x # Γ2

  _≈_ : {A : Set} → A ctx → A ctx → Set
  _≈_ {A} Γ1 Γ2 = (x : Nat) (a1 a2 : A) →
                   (x , a1) ∈ Γ1 ∧ (x , a2) ∈ Γ2 →
                   a1 == a2

  -- TODO theorems and explanation
  ctxmap : {A B : Set} → (A → B) → A ctx → B ctx
  ctxmap f Γ = map (λ {(hx , ha) → (hx , f ha)}) Γ

  -- TODO theorems
  -- returns a list of the values stored in the context
  ctx⇒values : {A : Set} → A ctx → List A

  -- TODO theorems
  -- converts a list of key-value pairs into a context, with later pairs in the list
  -- overriding bindings definend by previous pairs
  list⇒ctx : {A : Set} → List (Nat ∧ A) → A ctx

  -- TODO theorems
  -- converts a list of key-value pairs into a multi-context, where each value of
  -- the result is the sublist of values from the former that were mapped to by the
  -- corresponding key
  list⇒list-ctx : {A : Set} → List (Nat ∧ A) → (List A) ctx

  -- union merge A B is the union of A and B,
  -- with (merge a b) being invoked to handle the mappings they have in common
  union : {A : Set} → (A → A → A) → A ctx → A ctx → A ctx

  -- The primary way to test membership is to use _∈_,
  -- but this can be used in cases where using _∈_
  -- would be too verbose or awkward.
  -- The lookup theorems prove that they are compatible
  _⦃⦃_⦄⦄ : {A : Set} → A ctx → Nat → Maybe A
  [] ⦃⦃ x ⦄⦄ = None
  ((hx , ha) :: t) ⦃⦃ x ⦄⦄ with <dec x hx
  ... | Inl x<hx       = None
  ... | Inr (Inl refl) = Some ha
  ... | Inr (Inr hx<x) = t ⦃⦃ diff-1 hx<x ⦄⦄

  ---- lemmas ----

  undiff-1 : (x s : Nat) → (x<s+1+x : x < s + 1+ x) → s == diff-1 x<s+1+x
  undiff-1 x s x<s+1+x
    rewrite n+1+m==1+n+m {s} {x} | ! (m-n==1+m-1+n n≤m+n (n<m→1+n≤m x<s+1+x)) | +comm {s} {x}
      = ! (n+m-n==m n≤n+m)

  too-small : {A : Set} {Γ : A ctx} {xl xb : Nat} {a : A} →
               xl < xb →
               dom ((xb , a) :: Γ) xl →
               ⊥
  too-small (_ , ne) (_ , InH) = ne refl
  too-small (x+1+xb≤xb , x+1+xb==xb) (_ , InT _) =
    x+1+xb==xb (≤antisym x+1+xb≤xb (≤trans (≤1+ ≤refl) n≤m+n))

  all-not-none : {A : Set} {Γ : A ctx} {x : Nat} {a : A} →
                  None ≠ (((x , a) :: Γ) ⦃⦃ x ⦄⦄)
  all-not-none {x = x} rewrite <dec-refl x = λ ()

  all-bindings-==-rec-eq : {A : Set} {Γ1 Γ2 : A ctx} {x : Nat} {a : A} →
                            ((x' : Nat) → ((x , a) :: Γ1) ⦃⦃ x' ⦄⦄ == ((x , a) :: Γ2) ⦃⦃ x' ⦄⦄) →
                            ((x' : Nat) → Γ1 ⦃⦃ x' ⦄⦄ == Γ2 ⦃⦃ x' ⦄⦄)
  all-bindings-==-rec-eq {x = x} h x'
    with h (x' + 1+ x)
  ... | eq
    with <dec (x' + 1+ x) x
  ... | Inl x'+1+x<x
          = abort (<antisym x'+1+x<x (n<m→n<s+m n<1+n))
  ... | Inr (Inl x'+1+x==x)
          = abort ((flip n≠n+1+m) (n+1+m==1+n+m · (+comm {1+ x} · x'+1+x==x)))
  ... | Inr (Inr x<x'+1+x)
          rewrite ! (undiff-1 x x' x<x'+1+x) = eq

  all-bindings-==-rec : {A : Set} {Γ1 Γ2 : A ctx} {x1 x2 : Nat} {a1 a2 : A} →
                         ((x : Nat) → ((x1 , a1) :: Γ1) ⦃⦃ x ⦄⦄ == ((x2 , a2) :: Γ2) ⦃⦃ x ⦄⦄) →
                         ((x : Nat) → Γ1 ⦃⦃ x ⦄⦄ == Γ2 ⦃⦃ x ⦄⦄)
  all-bindings-==-rec {x1 = x1} {x2} h x
    with h x1 | h x2
  ... | eq1 | eq2
    rewrite <dec-refl x1 | <dec-refl x2
    with <dec x1 x2 | <dec x2 x1
  ... | Inl _ | _
          = abort (somenotnone eq1)
  ... | Inr _ | Inl _
          = abort (somenotnone (! eq2))
  ... | Inr (Inl refl) | Inr (Inl refl)
          rewrite someinj eq1 | someinj eq2
            = all-bindings-==-rec-eq h x
  ... | Inr (Inl refl) | Inr (Inr x2<x2)
          = abort (<antirefl x2<x2)
  ... | Inr (Inr x2<x2) | Inr (Inl refl)
          = abort (<antirefl x2<x2)
  ... | Inr (Inr x2<x1) | Inr (Inr x1<x2)
          = abort (<antisym x1<x2 x2<x1)

  ---- core theorems ----

  -- lookup is decidable
  lookup-dec : {A : Set} (Γ : A ctx) (x : Nat) →
                Σ[ a ∈ A ] (Γ ⦃⦃ x ⦄⦄ == Some a) ∨ Γ ⦃⦃ x ⦄⦄ == None
  lookup-dec Γ x
    with Γ ⦃⦃ x ⦄⦄
  ... | Some a = Inl (a , refl)
  ... | None   = Inr refl

  -- The next two theorems show that lookup (_⦃⦃_⦄⦄) is consistent with membership (_∈_)
  lookup-cons-1 : {A : Set} {Γ : A ctx} {x : Nat} {a : A} →
                   Γ ⦃⦃ x ⦄⦄ == Some a →
                   (x , a) ∈ Γ
  lookup-cons-1 {Γ = []} ()
  lookup-cons-1 {Γ = (hx , ha) :: t} {x} h
    with <dec x hx
  lookup-cons-1 {_} {(hx , ha) :: t} {x} ()        | Inl _
  lookup-cons-1 {_} {(hx , ha) :: t} {.hx} refl    | Inr (Inl refl) = InH
  lookup-cons-1 {_} {(hx , ha) :: t} {x} {a = a} h | Inr (Inr hx<x)
    = tr
        (λ y → (y , a) ∈ ((hx , ha) :: t))
        (m-n+n==m (n<m→1+n≤m hx<x))
        (InT (lookup-cons-1 {Γ = t} h))

  lookup-cons-2 : {A : Set} {Γ : A ctx} {x : Nat} {a : A} →
                   (x , a) ∈ Γ →
                   Γ ⦃⦃ x ⦄⦄ == Some a
  lookup-cons-2 {x = x} InH rewrite <dec-refl x = refl
  lookup-cons-2 (InT {Γ = Γ} {x = x} {s} {a} x∈Γ)
    with <dec (x + 1+ s) s
  ... | Inl x+1+s<s        = abort (<antisym x+1+s<s (n<m→n<s+m n<1+n))
  ... | Inr (Inl x+1+s==s) = abort ((flip n≠n+1+m) (n+1+m==1+n+m · (+comm {1+ s} · x+1+s==s)))
  ... | Inr (Inr s<x+1+s)
    with lookup-cons-2 x∈Γ
  ... | h rewrite ! (undiff-1 s x s<x+1+s) = h

  -- membership (_∈_) respects insertion (_,,_)
  x,a∈Γ,,x,a : {A : Set} {Γ : A ctx} {x : Nat} {a : A} →
                (x , a) ∈ (Γ ,, (x , a))
  x,a∈Γ,,x,a {Γ = []} {x} {a} = InH
  x,a∈Γ,,x,a {_} {(hx , ha) :: t} {x} {a}
    with <dec x hx
  ... | Inl _          = InH
  ... | Inr (Inl refl) = InH
  ... | Inr (Inr hx<x) =
          tr
            (λ y → (y , a) ∈ ((hx , ha) :: (t ,, (diff-1 hx<x , a))))
            (m-n+n==m (n<m→1+n≤m hx<x))
            (InT (x,a∈Γ,,x,a {Γ = t} {diff-1 hx<x} {a}))

  -- insertion can't generate spurious membership
  x∈Γ+→x∈Γ : {A : Set} {Γ : A ctx} {x x' : Nat} {a a' : A} →
                x ≠ x' →
                (x , a) ∈ (Γ ,, (x' , a')) →
                (x , a) ∈ Γ
  x∈Γ+→x∈Γ {Γ = []} x≠x' InH = abort (x≠x' refl)
  x∈Γ+→x∈Γ {Γ = []} x≠x' (InT ())
  x∈Γ+→x∈Γ {Γ = (hx , ha) :: t} {x' = x'} x≠x' x∈Γ+
    with <dec x' hx
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = x'} x≠x' InH | Inl x'<hx = abort (x≠x' refl)
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = x'} x≠x' (InT InH) | Inl x'<hx
    rewrite m-n+n==m (n<m→1+n≤m x'<hx) = InH
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = x'} x≠x' (InT (InT {x = x} x∈Γ+)) | Inl x'<hx
    rewrite +assc {x} {1+ (diff-1 x'<hx)} {1+ x'} | m-n+n==m (n<m→1+n≤m x'<hx)
      = InT x∈Γ+
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = .hx} x≠x' InH | Inr (Inl refl) = abort (x≠x' refl)
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = .hx} x≠x' (InT x∈Γ+) | Inr (Inl refl) = InT x∈Γ+
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = x'} x≠x' InH | Inr (Inr hx<x') = InH
  x∈Γ+→x∈Γ {_} {(hx , ha) :: t} {x' = x'} x≠x' (InT x∈Γ+) | Inr (Inr hx<x')
    = InT (x∈Γ+→x∈Γ (λ where refl → x≠x' (m-n+n==m (n<m→1+n≤m hx<x'))) x∈Γ+)

  -- insertion respects membership
  x∈Γ→x∈Γ+ : {A : Set} {Γ : A ctx} {x x' : Nat} {a a' : A} →
                x ≠ x' →
                (x , a) ∈ Γ →
                (x , a) ∈ (Γ ,, (x' , a'))
  x∈Γ→x∈Γ+ {x = x} {x'} {a} {a'} x≠x' (InH {Γ = Γ'})
    with <dec x' x
  ... | Inl x'<x
          = tr
              (λ y → (y , a) ∈ ((x' , a') :: ((diff-1 x'<x , a) :: Γ')))
              (m-n+n==m (n<m→1+n≤m x'<x))
              (InT InH)
  ... | Inr (Inl refl) = abort (x≠x' refl)
  ... | Inr (Inr x<x') = InH
  x∈Γ→x∈Γ+ {x = .(_ + 1+ _)} {x'} {a} {a'} x≠x' (InT {Γ = Γ} {x} {s} {a' = a''} x∈Γ)
    with <dec x' s
  ... | Inl x'<s
          = tr
              (λ y → (y , a) ∈ ((x' , a') :: ((diff-1 x'<s , a'') :: Γ)))
              ((+assc {b = 1+ (diff-1 x'<s)}) · (ap1 (_+_ x) (1+ap (m-n+n==m (n<m→1+n≤m x'<s)))))
              (InT (InT x∈Γ))
  ... | Inr (Inl refl) = InT x∈Γ
  ... | Inr (Inr s<x') =
          InT (x∈Γ→x∈Γ+ (λ where refl → x≠x' (m-n+n==m (n<m→1+n≤m s<x'))) x∈Γ)

  -- Decidability of membership
  -- This also packages up an appeal to context membership into a form that
  -- lets us retain more information
  ctxindirect : {A : Set} (Γ : A ctx) (x : Nat) → dom Γ x ∨ x # Γ
  ctxindirect [] x = Inr (λ ())
  ctxindirect ((hx , ha) :: t) x
    with <dec x hx
  ... | Inl x<hx       = Inr (too-small x<hx)
  ... | Inr (Inl refl) = Inl (ha , InH)
  ... | Inr (Inr hx<x)
    with ctxindirect t (diff-1 hx<x)
  ctxindirect ((hx , ha) :: t) x | Inr (Inr hx<x) | Inl (a , rec) =
    Inl (a , tr
               (λ y → (y , a) ∈ ((hx , ha) :: t))
               (m-n+n==m (n<m→1+n≤m hx<x))
               (InT rec))
  ctxindirect {A} ((hx , ha) :: t) x | Inr (Inr hx<x) | Inr dne =
    Inr x∉Γ
    where
      x∉Γ : Σ[ a ∈ A ] ((x , a) ∈ ((hx , ha) :: t)) → ⊥
      x∉Γ (_ , x∈Γ) with x∈Γ
      ... | InH = (π2 hx<x) refl
      ... | InT {x = s} x-hx-1∈t
        rewrite ! (undiff-1 hx s hx<x) = dne (_ , x-hx-1∈t)

  -- contexts give at most one binding for each variable
  ctxunicity : {A : Set} {Γ : A ctx} {x : Nat} {a a' : A} →
                 (x , a) ∈ Γ →
                 (x , a') ∈ Γ →
                 a == a'
  ctxunicity ah a'h
    with lookup-cons-2 ah | lookup-cons-2 a'h
  ... | ah' | a'h' = someinj (! ah' · a'h')

  -- everything is apart from the nil context
  x#∅ : {A : Set} {x : Nat} → _#_ {A} x ∅
  x#∅ (_ , ())

  -- if an index is in the domain of a singleton context, it's the only
  -- index in the context
  lem-dom-eq : {A : Set} {a : A} {n m : Nat} →
                 dom (■ (m , a)) n →
                 n == m
  lem-dom-eq (_ , InH) = refl
  lem-dom-eq (_ , InT ())

  -- If two contexts are semantically equivalent
  -- (i.e. they represent the same mapping from ids to values),
  -- then they are physically equal as judged by _==_
  ctx-==-eqv : {A : Set} {Γ1 Γ2 : A ctx} →
                ((x : Nat) → Γ1 ⦃⦃ x ⦄⦄ == Γ2 ⦃⦃ x ⦄⦄) →
                Γ1 == Γ2
  ctx-==-eqv {Γ1 = []} {[]} all-bindings-== = refl
  ctx-==-eqv {Γ1 = []} {(hx2 , ha2) :: t2} all-bindings-==
    = abort (all-not-none {Γ = t2} {x = hx2} (all-bindings-== hx2))
  ctx-==-eqv {Γ1 = (hx1 , ha1) :: t1} {[]} all-bindings-==
    = abort (all-not-none {Γ = t1} {x = hx1} (! (all-bindings-== hx1)))
  ctx-==-eqv {Γ1 = (hx1 , ha1) :: t1} {(hx2 , ha2) :: t2} all-bindings-==
    rewrite ctx-==-eqv {Γ1 = t1} {t2} (all-bindings-==-rec all-bindings-==)
    with all-bindings-== hx1 | all-bindings-== hx2
  ... | ha1== | ha2== rewrite <dec-refl hx1 | <dec-refl hx2
    with <dec hx1 hx2 | <dec hx2 hx1
  ... | Inl hx1<hx2 | _
          = abort (somenotnone ha1==)
  ... | Inr (Inl refl) | Inl hx2<hx1
          = abort (somenotnone (! ha2==))
  ... | Inr (Inr hx2<hx1) | Inl hx2<'hx1
          = abort (somenotnone (! ha2==))
  ... | Inr (Inl refl) | Inr _
          rewrite someinj ha1== = refl
  ... | Inr (Inr hx2<hx1) | Inr (Inl refl)
          rewrite someinj ha2== = refl
  ... | Inr (Inr hx2<hx1) | Inr (Inr hx1<hx2)
          = abort (<antisym hx1<hx2 hx2<hx1)

  -- equality of contexts is decidable
  ctx-==-dec : {A : Set}
                (Γ1 Γ2 : A ctx) →
                ((a1 a2 : A) → a1 == a2 ∨ a1 ≠ a2) →
                Γ1 == Γ2 ∨ Γ1 ≠ Γ2
  ctx-==-dec [] [] _ = Inl refl
  ctx-==-dec [] (_ :: _) _ = Inr (λ ())
  ctx-==-dec (_ :: _) [] _ = Inr (λ ())
  ctx-==-dec ((hx1 , ha1) :: t1) ((hx2 , ha2) :: t2) A==dec
    with natEQ hx1 hx2 | A==dec ha1 ha2 | ctx-==-dec t1 t2 A==dec
  ... | Inl refl | Inl refl | Inl refl = Inl refl
  ... | Inl refl | Inl refl | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl | Inr ne   | _        = Inr λ where refl → ne refl
  ... | Inr ne   | _        | _        = Inr λ where refl → ne refl

  -- A useful way to destruct context membership. Never destruct a context via _::_
  ctx-split : {A : Set} {Γ : A ctx} {n m : Nat} {an am : A} →
                (n , an) ∈ (Γ ,, (m , am)) →
                (n ≠ m ∧ (n , an) ∈ Γ) ∨ (n == m ∧ an == am)
  ctx-split {Γ = Γ} {n} {m} {an} {am} n∈Γ+
    with natEQ n m
  ... | Inl refl = Inr (refl , ctxunicity n∈Γ+ (x,a∈Γ,,x,a {Γ = Γ}))
  ... | Inr n≠m  = Inl (n≠m , x∈Γ+→x∈Γ n≠m n∈Γ+)

  -- I'd say "God dammit agda" but AFAICT Coq is terrible about this as well
  lemma-bullshit : {A : Set} (Γ' : A ctx) (a : A) (n m : Nat) →
                    Σ[ Γ ∈ A ctx ] (Γ == (n + 1+ m , a) :: Γ')
  lemma-bullshit Γ' a n m = ((n + 1+ m , a) :: Γ') , refl

  -- Allows the elimination of contexts. Never destruct a context via _::_
  ctx-elim : {A : Set} {Γ : A ctx} →
              Γ == ∅
                ∨
              Σ[ n ∈ Nat ] Σ[ a ∈ A ] Σ[ Γ' ∈ A ctx ]
                 (Γ == Γ' ,, (n , a) ∧ n # Γ')
  ctx-elim {Γ = []}            = Inl refl
  ctx-elim {Γ = (n , a) :: []} = Inr (_ , _ , _ , refl , x#∅)
  ctx-elim {Γ = (n , a) :: ((m , a2) :: Γ'')}
    with lemma-bullshit Γ'' a2 m n
  ... | Γ' , eq
    = Inr (n , a , Γ' , eqP , not-dom)
      where
        eqP : (n , a) :: ((m , a2) :: Γ'') == Γ' ,, (n , a)
        eqP rewrite eq with <dec n (m + 1+ n)
        ... | Inl n<m+1+n
          rewrite ! (undiff-1 n m n<m+1+n) = refl
        ... | Inr (Inl n==m+1+n)
          = abort (n≠n+1+m (n==m+1+n · (n+1+m==1+n+m · +comm {1+ m})))
        ... | Inr (Inr m+1+n<n)
          = abort (<antisym m+1+n<n (n<m→n<s+m n<1+n))
        not-dom : dom Γ' n → ⊥
        not-dom rewrite eq = λ n∈Γ' →
          too-small (n<m→n<s+m n<1+n) n∈Γ'

  -- When using ctx-elim, this theorem is useful for establishing termination
  ctx-decreasing : {A : Set} {Γ : A ctx} {n : Nat} {a : A} →
                    n # Γ →
                    ∥ Γ ,, (n , a) ∥ == 1+ ∥ Γ ∥
  ctx-decreasing {Γ = []} n#Γ = refl
  ctx-decreasing {Γ = (n' , a') :: Γ} {n} n#Γ
    with <dec n n'
  ... | Inl n<n'       = refl
  ... | Inr (Inl refl) = abort (n#Γ (_ , InH))
  ... | Inr (Inr n'<n)
    = 1+ap (ctx-decreasing λ {(a , diff∈Γ) →
        n#Γ (a , tr
                   (λ y → (y , a) ∈ ((n' , a') :: Γ))
                   (m-n+n==m (n<m→1+n≤m n'<n))
                   (InT diff∈Γ))})

  ---- contrapositives of some previous theorems ----

  lem-neq-apart : {A : Set} {a : A} {n m : Nat} →
                    n ≠ m →
                    n # (■ (m , a))
  lem-neq-apart n≠m h = n≠m (lem-dom-eq h)

  x#Γ→x#Γ+ : {A : Set} {Γ : A ctx} {x x' : Nat} {a' : A} →
               x ≠ x' →
               x # Γ →
               x # (Γ ,, (x' , a'))
  x#Γ→x#Γ+ {Γ = Γ} {x} {x'} {a'} x≠x' x#Γ
    with ctxindirect (Γ ,, (x' , a')) x
  ... | Inl (_ , x∈Γ+) = abort (x#Γ (_ , x∈Γ+→x∈Γ x≠x' x∈Γ+))
  ... | Inr x#Γ+       = x#Γ+

  x#Γ+→x#Γ : {A : Set} {Γ : A ctx} {x x' : Nat} {a' : A} →
               x # (Γ ,, (x' , a')) →
               x # Γ
  x#Γ+→x#Γ {Γ = Γ} {x} {x'} {a'} x#Γ+
    with ctxindirect Γ x
  ... | Inr x#Γ       = x#Γ
  ... | Inl (_ , x∈Γ)
    with natEQ x x'
  ... | Inl refl = abort (x#Γ+ (_ , x,a∈Γ,,x,a {Γ = Γ}))
  ... | Inr x≠x' = abort (x#Γ+ (_ , x∈Γ→x∈Γ+ x≠x' x∈Γ))

  lookup-cp-1 : {A : Set} {Γ : A ctx} {x : Nat} →
                 x # Γ →
                 Γ ⦃⦃ x ⦄⦄ == None
  lookup-cp-1 {Γ = Γ} {x} x#Γ
    with lookup-dec Γ x
  ... | Inl (_ , x∈Γ) = abort (x#Γ (_ , (lookup-cons-1 x∈Γ)))
  ... | Inr x#'Γ      = x#'Γ

  lookup-cp-2 : {A : Set} {Γ : A ctx} {x : Nat} →
                 Γ ⦃⦃ x ⦄⦄ == None →
                 x # Γ
  lookup-cp-2 {Γ = Γ} {x} x#Γ
    with ctxindirect Γ x
  ... | Inl (_ , x∈Γ) = abort (somenotnone ((! (lookup-cons-2 x∈Γ)) · x#Γ))
  ... | Inr x#'Γ      = x#'Γ

  ---- some definitions ----

  merge' : {A : Set} → (A → A → A) → Maybe A → A → A
  merge' merge ma1 a2
    with ma1
  ... | None    = a2
  ... | Some a1 = merge a1 a2

  union' : {A : Set} → (A → A → A) → A ctx → A ctx → Nat → A ctx
  union' merge Γ1 [] _ = Γ1
  union' merge Γ1 ((hx , ha) :: Γ2) offset
    = union' merge (Γ1 ,, (hx + offset , merge' merge (Γ1 ⦃⦃ hx + offset ⦄⦄) ha)) Γ2 (1+ hx + offset)

  union merge Γ1 Γ2 = union' merge Γ1 Γ2 0

  ---- union theorems ----

  lemma-math' : ∀{x x1 n} → x ≠ x1 + (n + 1+ x)
  lemma-math' {x} {x1} {n}
    rewrite ! (+assc {x1} {n} {1+ x})
          | n+1+m==1+n+m {x1 + n} {x}
          | +comm {1+ x1 + n} {x}
      = n≠n+1+m

  lemma-union'-0 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x n : Nat} {a : A} →
                    (x , a) ∈ Γ1 →
                    (x , a) ∈ union' m Γ1 Γ2 (n + 1+ x)
  lemma-union'-0 {Γ2 = []} x∈Γ1 = x∈Γ1
  lemma-union'-0 {Γ2 = (x1 , a1) :: Γ2} {x} {n} x∈Γ1
    rewrite ! (+assc {1+ x1} {n} {1+ x})
      = lemma-union'-0 {Γ2 = Γ2} {n = 1+ x1 + n} (x∈Γ→x∈Γ+ (lemma-math' {x1 = x1} {n}) x∈Γ1)

  lemma-union'-1 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x n : Nat} {a : A} →
                    (x , a) ∈ Γ1 →
                    (n≤x : n ≤ x) →
                    (difference n≤x) # Γ2 →
                    (x , a) ∈ union' m Γ1 Γ2 n
  lemma-union'-1 {Γ2 = []} {x} x∈Γ1 n≤x x-n#Γ2 = x∈Γ1
  lemma-union'-1 {m = m} {Γ1} {(x1 , a1) :: Γ2} {x} {n} {a} x∈Γ1 n≤x x-n#Γ2
    with <dec x (x1 + n)
  lemma-union'-1 {m = m} {Γ1} {(x1 , a1) :: Γ2} {x} {n} {a} x∈Γ1 n≤x x-n#Γ2 | Inl x<x1+n
    with Γ1 ⦃⦃ x1 + n ⦄⦄
  lemma-union'-1 {m = m} {Γ1} {(x1 , a1) :: Γ2} {x} {n} {a} x∈Γ1 n≤x x-n#Γ2 | Inl x<x1+n | Some a'
    = tr
         (λ y → (x , a) ∈ union' m (Γ1 ,, (x1 + n , m a' a1)) Γ2 y)
         (n+1+m==1+n+m {difference (π1 x<x1+n)} · 1+ap (m-n+n==m (π1 x<x1+n)))
         (lemma-union'-0 {Γ2 = Γ2} (x∈Γ→x∈Γ+ (π2 x<x1+n) x∈Γ1))
  lemma-union'-1 {m = m} {Γ1} {(x1 , a1) :: Γ2} {x} {n} {a} x∈Γ1 n≤x x-n#Γ2 | Inl x<x1+n | None
    = tr
         (λ y → (x , a) ∈ union' m (Γ1 ,, (x1 + n , a1)) Γ2 y)
         (n+1+m==1+n+m {difference (π1 x<x1+n)} · 1+ap (m-n+n==m (π1 x<x1+n)))
         (lemma-union'-0 {Γ2 = Γ2} (x∈Γ→x∈Γ+ (π2 x<x1+n) x∈Γ1))
  lemma-union'-1 {m = m} {Γ1} {(x1 , a1) :: Γ2} {x} {n} {a} x∈Γ1 n≤x x-n#Γ2 | Inr (Inl refl)
    rewrite +comm {x1} {n} | n+m-n==m n≤x
      = abort (x-n#Γ2 (_ , InH))
  lemma-union'-1 {m = m} {Γ1} {(x1 , a1) :: Γ2} {x} {n} {a} x∈Γ1 n≤x x-n#Γ2 | Inr (Inr x1+n<x)
    rewrite (! (a+b==c→a==c-b (+assc {diff-1 x1+n<x} · m-n+n==m (n<m→1+n≤m x1+n<x)) n≤x))
      = lemma-union'-1
          (x∈Γ→x∈Γ+ (flip (π2 x1+n<x)) x∈Γ1)
          (n<m→1+n≤m x1+n<x)
          λ {(_ , x-x1-n∈Γ2) → x-n#Γ2 (_ , InT x-x1-n∈Γ2)}

  lemma-union'-2 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x n : Nat} {a : A} →
                    (x + n) # Γ1 →
                    (x , a) ∈ Γ2 →
                    (x + n , a) ∈ union' m Γ1 Γ2 n
  lemma-union'-2 {Γ1 = Γ1} x+n#Γ1 (InH {Γ = Γ2})
    rewrite lookup-cp-1 x+n#Γ1
      = lemma-union'-0 {Γ2 = Γ2} {n = Z} (x,a∈Γ,,x,a {Γ = Γ1})
  lemma-union'-2 {Γ1 = Γ1} {n = n} x+n#Γ1 (InT {Γ = Γ2} {x = x} {s} x∈Γ2)
    rewrite +assc {x} {1+ s} {n}
    with Γ1 ⦃⦃ s + n ⦄⦄
  ... | Some a'
    = lemma-union'-2
        (λ {(_ , x∈Γ1+) →
             x+n#Γ1 (_ , x∈Γ+→x∈Γ (flip (lemma-math' {x1 = Z})) x∈Γ1+)})
        x∈Γ2
  ... | None
    = lemma-union'-2
        (λ {(_ , x∈Γ1+) →
             x+n#Γ1 (_ , x∈Γ+→x∈Γ (flip (lemma-math' {x1 = Z})) x∈Γ1+)})
        x∈Γ2

  lemma-union'-3 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x n : Nat} {a1 a2 : A} →
                    (x + n , a1) ∈ Γ1 →
                    (x , a2) ∈ Γ2 →
                    (x + n , m a1 a2) ∈ union' m Γ1 Γ2 n
  lemma-union'-3 {Γ1 = Γ1} x+n∈Γ1 (InH {Γ = Γ2})
    rewrite lookup-cons-2 x+n∈Γ1
      = lemma-union'-0 {Γ2 = Γ2} {n = Z} (x,a∈Γ,,x,a {Γ = Γ1})
  lemma-union'-3 {Γ1 = Γ1} {n = n} x+n∈Γ1 (InT {Γ = Γ2} {x = x} {s} x∈Γ2)
    rewrite +assc {x} {1+ s} {n}
    with Γ1 ⦃⦃ s + n ⦄⦄
  ... | Some a'
    = lemma-union'-3 (x∈Γ→x∈Γ+ (flip (lemma-math' {x1 = Z})) x+n∈Γ1) x∈Γ2
  ... | None
    = lemma-union'-3 (x∈Γ→x∈Γ+ (flip (lemma-math' {x1 = Z})) x+n∈Γ1) x∈Γ2

  lemma-union'-4 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x n : Nat} →
                    dom (union' m Γ1 Γ2 n) x →
                    dom Γ1 x ∨ (Σ[ s ∈ Nat ] (x == n + s ∧ dom Γ2 s))
  lemma-union'-4 {Γ2 = []} x∈un = Inl x∈un
  lemma-union'-4 {Γ1 = Γ1} {(x1 , a1) :: Γ2} {x} {n} x∈un
    with lemma-union'-4 {Γ2 = Γ2} x∈un
  ... | Inr (s , refl , _ , s∈Γ2)
    rewrite +comm {x1} {n}
          | ! (n+1+m==1+n+m {n + x1} {s})
          | +assc {n} {x1} {1+ s}
          | +comm {x1} {1+ s}
          | ! (n+1+m==1+n+m {s} {x1})
      = Inr (_ , refl , _ , InT s∈Γ2)
  ... | Inl (_ , x∈Γ1+)
    with natEQ x (n + x1)
  ... | Inl refl   = Inr (_ , refl , _ , InH)
  ... | Inr x≠n+x1
    rewrite +comm {x1} {n}
      = Inl (_ , x∈Γ+→x∈Γ x≠n+x1 x∈Γ1+)

  x,a∈Γ1→x∉Γ2→x,a∈Γ1∪Γ2 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x : Nat} {a : A} →
                              (x , a) ∈ Γ1 →
                              x # Γ2 →
                              (x , a) ∈ union m Γ1 Γ2
  x,a∈Γ1→x∉Γ2→x,a∈Γ1∪Γ2 {Γ2 = Γ2} x∈Γ1 x#Γ2
    = lemma-union'-1 x∈Γ1 0≤n (tr (λ y → y # Γ2) (! (n+m-n==m 0≤n)) x#Γ2)

  x∉Γ1→x,a∈Γ2→x,a∈Γ1∪Γ2 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x : Nat} {a : A} →
                              x # Γ1 →
                              (x , a) ∈ Γ2 →
                              (x , a) ∈ union m Γ1 Γ2
  x∉Γ1→x,a∈Γ2→x,a∈Γ1∪Γ2 {Γ1 = Γ1} {x = x} x#Γ1 x∈Γ2
    with lemma-union'-2 {n = Z} (tr (λ y → y # Γ1) (! n+Z==n) x#Γ1) x∈Γ2
  ... | rslt
    rewrite n+Z==n {x}
      = rslt

  x∈Γ1→x∈Γ2→x∈Γ1∪Γ2 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x : Nat} {a1 a2 : A} →
                              (x , a1) ∈ Γ1 →
                              (x , a2) ∈ Γ2 →
                              (x , m a1 a2) ∈ union m Γ1 Γ2
  x∈Γ1→x∈Γ2→x∈Γ1∪Γ2 {Γ1 = Γ1} {Γ2} {x} {a1} x∈Γ1 x∈Γ2
    with lemma-union'-3 (tr (λ y → (y , a1) ∈ Γ1) (! n+Z==n) x∈Γ1) x∈Γ2
  ... | rslt
    rewrite n+Z==n {x}
      = rslt

  x∈Γ1∪Γ2→x∈Γ1∨x∈Γ2 : {A : Set} {m : A → A → A} {Γ1 Γ2 : A ctx} {x : Nat} →
                          dom (union m Γ1 Γ2) x →
                          dom Γ1 x ∨ dom Γ2 x
  x∈Γ1∪Γ2→x∈Γ1∨x∈Γ2 x∈Γ1∪Γ2
    with lemma-union'-4 {n = Z} x∈Γ1∪Γ2
  x∈Γ1∪Γ2→x∈Γ1∨x∈Γ2 x∈Γ1∪Γ2 | Inl x'∈Γ1 = Inl x'∈Γ1
  x∈Γ1∪Γ2→x∈Γ1∨x∈Γ2 x∈Γ1∪Γ2 | Inr (_ , refl , x'∈Γ2) = Inr x'∈Γ2

  ---- contraction and exchange ----

  -- TODO these proofs could use refactoring -
  -- contraction should probably make use of ctx-==-dec and
  -- exchange is way too long and repetitive

  contraction : {A : Set} {Γ : A ctx} {x : Nat} {a a' : A} →
                 Γ ,, (x , a') ,, (x , a) == Γ ,, (x , a)
  contraction {Γ = []} {x} rewrite <dec-refl x = refl
  contraction {Γ = (hx , ha) :: t} {x} {a} {a'}
    with <dec x hx
  ... | Inl _          rewrite <dec-refl x  = refl
  ... | Inr (Inl refl) rewrite <dec-refl hx = refl
  ... | Inr (Inr hx<x)
    with <dec x hx
  ... | Inl x<hx        = abort (<antisym x<hx hx<x)
  ... | Inr (Inl refl)  = abort (<antirefl hx<x)
  ... | Inr (Inr hx<'x)
    rewrite diff-proof-irrelevance (n<m→1+n≤m hx<x) (n<m→1+n≤m hx<'x)
          | contraction {Γ = t} {diff-1 hx<'x} {a} {a'}
    = refl

  exchange : {A : Set} {Γ : A ctx} {x1 x2 : Nat} {a1 a2 : A} →
              x1 ≠ x2 →
              Γ ,, (x1 , a1) ,, (x2 , a2) == Γ ,, (x2 , a2) ,, (x1 , a1)
  exchange {A} {Γ} {x1} {x2} {a1} {a2} x1≠x2
    = ctx-==-eqv fun
      where
        fun : (x : Nat) →
               (Γ ,, (x1 , a1) ,, (x2 , a2)) ⦃⦃ x ⦄⦄ ==
               (Γ ,, (x2 , a2) ,, (x1 , a1)) ⦃⦃ x ⦄⦄
        fun x
          with natEQ x x1 | natEQ x x2 | ctxindirect Γ x
        fun x  | Inl refl | Inl refl | _
          = abort (x1≠x2 refl)
        fun x1 | Inl refl | Inr x≠x2 | Inl (_ , x1∈Γ)
          with x,a∈Γ,,x,a {Γ = Γ} {x1} {a1}
        ... | x∈Γ+1
          with x∈Γ→x∈Γ+ {a' = a2} x≠x2 x∈Γ+1 | x,a∈Γ,,x,a {Γ = Γ ,, (x2 , a2)} {x1} {a1}
        ... | x∈Γ++1 | x∈Γ++2
          rewrite lookup-cons-2 x∈Γ++1 | lookup-cons-2 x∈Γ++2 = refl
        fun x1 | Inl refl | Inr x≠x2 | Inr x1#Γ
          with x,a∈Γ,,x,a {Γ = Γ} {x1} {a1}
        ... | x∈Γ+1
          with x∈Γ→x∈Γ+ {a' = a2} x≠x2 x∈Γ+1 | x,a∈Γ,,x,a {Γ = Γ ,, (x2 , a2)} {x1} {a1}
        ... | x∈Γ++1 | x∈Γ++2
          rewrite lookup-cons-2 x∈Γ++1 | lookup-cons-2 x∈Γ++2 = refl
        fun x2 | Inr x≠x1 | Inl refl | Inl (_ , x2∈Γ)
          with x,a∈Γ,,x,a {Γ = Γ} {x2} {a2}
        ... | x∈Γ+2
          with x∈Γ→x∈Γ+ {a' = a1} x≠x1 x∈Γ+2 | x,a∈Γ,,x,a {Γ = Γ ,, (x1 , a1)} {x2} {a2}
        ... | x∈Γ++1 | x∈Γ++2
          rewrite lookup-cons-2 x∈Γ++1 | lookup-cons-2 x∈Γ++2 = refl
        fun x2 | Inr x≠x1 | Inl refl | Inr x2#Γ
          with x,a∈Γ,,x,a {Γ = Γ} {x2} {a2}
        ... | x∈Γ+2
          with x∈Γ→x∈Γ+ {a' = a1} x≠x1 x∈Γ+2 | x,a∈Γ,,x,a {Γ = Γ ,, (x1 , a1)} {x2} {a2}
        ... | x∈Γ++1 | x∈Γ++2
          rewrite lookup-cons-2 x∈Γ++1 | lookup-cons-2 x∈Γ++2 = refl
        fun x  | Inr x≠x1 | Inr x≠x2 | Inl (_ , x∈Γ)
          with x∈Γ→x∈Γ+ {a' = a1} x≠x1 x∈Γ   | x∈Γ→x∈Γ+ {a' = a2} x≠x2 x∈Γ
        ... | x∈Γ+1  | x∈Γ+2
          with x∈Γ→x∈Γ+ {a' = a2} x≠x2 x∈Γ+1 | x∈Γ→x∈Γ+ {a' = a1} x≠x1 x∈Γ+2
        ... | x∈Γ++1 | x∈Γ++2
          rewrite lookup-cons-2 x∈Γ++1 | lookup-cons-2 x∈Γ++2 = refl
        fun x  | Inr x≠x1 | Inr x≠x2 | Inr x#Γ
          with x#Γ→x#Γ+ {a' = a1} x≠x1 x#Γ   | x#Γ→x#Γ+ {a' = a2} x≠x2 x#Γ
        ... | x#Γ+1  | x#Γ+2
          with x#Γ→x#Γ+ {a' = a2} x≠x2 x#Γ+1 | x#Γ→x#Γ+ {a' = a1} x≠x1 x#Γ+2
        ... | x#Γ++1 | x#Γ++2
          rewrite lookup-cp-1 x#Γ++1 | lookup-cp-1 x#Γ++2 = refl

  ---- remaining function definitions ----

  list⇒ctx = foldl _,,_ ∅

  list⇒list-ctx {A} l
    = foldl f ∅ (reverse l)
      where
        f : (List A) ctx → Nat ∧ A → (List A) ctx
        f Γ (n , a)
          with ctxindirect Γ n
        ... | Inl (as , n∈Γ)
          = Γ ,, (n , a :: as)
        ... | Inr n#Γ
          = Γ ,, (n , a :: [])

  ctx⇒values = map π2

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Empty.Base where

open import Cubical.Core.Everything

data ⊥ : Type₀ where

rec : ∀ {ℓ} {A : Type ℓ} → ⊥ → A
rec ()

elim : ∀ {ℓ} {A : ⊥ → Type ℓ} → (x : ⊥) → A x
elim ()

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
open import Stlc hiding (⟹*-Preorder; _⟹*⟪_⟫_; example₀; example₁)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
open import Relation.Binary using (Preorder)
import Relation.Binary.PreorderReasoning as PreorderReasoning

⟹*-Preorder : Preorder _ _ _
⟹*-Preorder = record
  { Carrier    = Term
  ; _≈_        = _≡_
  ; _∼_        = _⟹*_
  ; isPreorder = record
    { isEquivalence = P.isEquivalence
    ; reflexive     = λ {refl → ⟨⟩}
    ; trans         = _>>_
    }
  }

open PreorderReasoning ⟹*-Preorder
     using (_IsRelatedTo_; begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_)

infixr 2 _⟹*⟪_⟫_

_⟹*⟪_⟫_ : ∀ x {y z} → x ⟹ y → y IsRelatedTo z → x IsRelatedTo z
x ⟹*⟪ x⟹y ⟫ yz  =  x ⟹*⟨ ⟨ x⟹y ⟩ ⟩ yz

example₀ : not · true ⟹* false
example₀ =
  begin
    not · true
  ⟹*⟪ β⇒ value-true ⟫
    if true then false else true
  ⟹*⟪ β𝔹₁ ⟫
    false
  ∎

example₁ : I² · I · (not · false) ⟹* true
example₁ =
  begin
    I² · I · (not · false)
  ⟹*⟪ γ⇒₁ (β⇒ value-λ) ⟫
    (λ[ x ∶ 𝔹 ] I · var x) · (not · false)
  ⟹*⟪ γ⇒₂ value-λ (β⇒ value-false) ⟫
    (λ[ x ∶ 𝔹 ] I · var x) · (if false then false else true)
  ⟹*⟪ γ⇒₂ value-λ β𝔹₂ ⟫
    (λ[ x ∶ 𝔹 ] I · var x) · true
  ⟹*⟪ β⇒ value-true ⟫
    I · true
  ⟹*⟪ β⇒ value-true ⟫
    true
  ∎


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

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

open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import Util.Prelude

module LibraBFT.Impl.OBM.Util where

-- To tolerate f failures, cluster must contain at least n ≥ 3f + 1 nodes,
-- where n − f nodes form a quorum, assuming 1 vote per node.
-- Note: our Haskell implementation and our model of it support non-uniform voting power,
-- that is NOT reflected in these functions, but is reflected in functions in ValidatorVerifier.

numNodesNeededForNFailures : U64 -> U64
numNodesNeededForNFailures numFaultsAllowed = 3 * numFaultsAllowed + 1

checkBftAndRun : ∀ {names : Set} {b : Set}
               → U64 → List names → (U64 → List names → b)
               → Either ErrLog b
checkBftAndRun numFailures authors f =
  if-dec length authors <? numNodesNeededForNFailures numFailures
  then Left fakeErr --(ErrL [ "checkBftAndRun: not enough authors for given number of failures"
                    --      , show numFailures, show (length authors) ])
  else pure (f numFailures authors)


text:
module Problem1 where

{-
If we list all the natural numbers below 10 that are multiples of 3 or
5, we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.
-}

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Data.List
open import Data.Sum

open import Function.Nary.NonDependent using (congₙ)

open import Relation.Unary.Properties
open import Relation.Binary.PropositionalEquality

problem′ : ℕ → ℕ
problem′ n = sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo n))

example : ℕ
example = problem′ 10

example-correct : example ≡ 23
example-correct = refl

-- this is actually quick enough but I'm sure we can do better
problem : ℕ
problem = problem′ 1000

module Lemmas where
  import Agda.Builtin.Nat

  open import Algebra.Definitions

  open import Data.Bool using (true; false)
  open import Data.Empty
  open import Data.List.Properties
  open import Data.Nat.LCM

  open import Relation.Nullary
  open import Relation.Unary

  -- first definition of triangle numbers. This is easiest to work with
  triangle : ℕ → ℕ
  triangle zero = zero
  triangle n@(suc x) = n + triangle x

  -- second definition of triangle numbers. This looks pretty but sadly ⌊_/2⌋
  -- is O(n) so this works out pretty slow in practice
  triangle′ : ℕ → ℕ
  triangle′ n = ⌊ n * suc n /2⌋

  -- Identity to do with adding to half something
  +-⌊n/2⌋ : ∀ m n → m + ⌊ n /2⌋ ≡ ⌊ 2 * m + n /2⌋
  +-⌊n/2⌋ zero n = refl
  +-⌊n/2⌋ (suc m) n = begin
    suc (m + ⌊ n /2⌋)         ≡⟨ cong suc (+-⌊n/2⌋ m n) ⟩
    suc ⌊ 2 * m + n /2⌋       ≡⟨ cong (λ x → suc ⌊ m + x + n /2⌋) (+-identityʳ m) ⟩
    ⌊ suc (suc m + m) + n /2⌋ ≡˘⟨ cong (λ x → ⌊ suc x + n /2⌋) (+-suc m m) ⟩
    ⌊ suc (m + suc m + n) /2⌋ ≡˘⟨ cong (λ x → ⌊ suc (m + suc x + n) /2⌋) (+-identityʳ m) ⟩
    ⌊ 2 * suc m + n /2⌋       ∎
    where
      open ≡-Reasoning

  -- The first two definitions of triangle numbers match!
  triangle≗triangle′ : triangle ≗ triangle′
  triangle≗triangle′ zero = refl
  triangle≗triangle′ (suc x) = begin
    triangle (suc x)            ≡⟨ cong (suc x +_) (triangle≗triangle′ x) ⟩
    suc x + ⌊ x * suc x /2⌋     ≡⟨ +-⌊n/2⌋ (suc x) (x * suc x) ⟩
    ⌊ 2 * suc x + x * suc x /2⌋ ≡˘⟨ cong ⌊_/2⌋ (*-distribʳ-+ (suc x) 2 x) ⟩
    ⌊ (2 + x) * suc x /2⌋       ≡⟨ cong ⌊_/2⌋ (*-comm (2 + x) _) ⟩
    triangle′ (suc x)           ∎
    where
      open ≡-Reasoning

  -- the third and final definition of triangle numbers
  -- This uses builtin division under the hood which gets compiled to proper
  -- division operators (I think ultimately GMP integer division) so it's fast
  triangle″ : ℕ → ℕ
  triangle″ n = n * suc n / 2

  -- halfing is the same as dividing by 2, as you might expect
  //2 : ∀ n → ⌊ n /2⌋ ≡ n / 2
  //2 zero = refl
  //2 (suc zero) = refl
  //2 (suc (suc n)) = begin
    suc ⌊ n /2⌋ ≡⟨ cong suc (//2 n) ⟩
    suc (n / 2) ≡˘⟨ +-distrib-/ 2 n (m%n<n n 1)  ⟩
    suc (suc n) / 2 ∎
    where
      open ≡-Reasoning

  -- the second and third definitions of triangle numbers also match!
  triangle′≗triangle″ : triangle′ ≗ triangle″
  triangle′≗triangle″ n = //2 _

  -- and so the first and thirdd definitions match
  triangle≗triangle″ : triangle ≗ triangle″
  triangle≗triangle″ x = trans (triangle≗triangle′ x) (triangle′≗triangle″ x)

  -- if we're almost done dividing, we're not going to change the answer
  foo : ∀ {k m n j} → n ≤ j → Agda.Builtin.Nat.div-helper k m n j ≡ k
  foo z≤n = refl
  foo (s≤s p) = foo p

  -- dividing a small number by a big one gets 0
  m<n⇒m/n≡0 : ∀ {m n n≢0} → m < n → (m / n) {n≢0} ≡ 0
  m<n⇒m/n≡0 (s≤s p) = foo p

  -- if i divides both m and n then it divides their difference
  ∣m∣n⇒∣m∸n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m ∸ n
  ∣m∣n⇒∣m∸n (divides p refl) (divides q refl) = divides (p ∸ q) (sym (*-distribʳ-∸ _ p q))

  lemma : {x d : ℕ} → suc d ∣ suc x → suc x / suc d ≡ suc (x / suc d)
  lemma {x} {zero} p = begin
    suc x / 1   ≡⟨ n/1≡n (suc x) ⟩
    suc x       ≡˘⟨ cong suc (n/1≡n x) ⟩
    suc (x / 1) ∎
    where
      open ≡-Reasoning
  lemma {x} {suc d} (divides (suc q) p) = begin
    suc x / suc (suc d)                                         ≡⟨ cong (_/ suc (suc d)) p ⟩
    suc q * suc (suc d) / suc (suc d)                           ≡⟨ m*n/n≡m (suc q) (suc (suc d)) ⟩
    suc q                                                       ≡˘⟨ cong suc (m*n/n≡m q (suc (suc d))) ⟩
    suc (q * suc (suc d) / suc (suc d))                         ≡⟨⟩
    suc ((suc q ∸ 1) * suc (suc d) / suc (suc d))               ≡⟨ cong (λ x → suc (x / suc (suc d))) (*-distribʳ-∸ (suc (suc d)) (suc q) 1) ⟩
    suc ((suc q * suc (suc d) ∸ 1 * suc (suc d)) / suc (suc d)) ≡⟨ cong (λ x → suc ((suc q * suc (suc d) ∸ x) / suc (suc d))) (*-identityˡ (suc (suc d))) ⟩
    suc ((suc q * suc (suc d) ∸ suc (suc d)) / suc (suc d))     ≡˘⟨ cong (λ x → suc ((x ∸ suc (suc d)) / suc (suc d))) p ⟩
    suc (0 + (x ∸ suc d) / suc (suc d))                         ≡˘⟨ cong (λ n → suc (n + (x ∸ suc d) / suc (suc d))) (m<n⇒m/n≡0 (n<1+n (suc d))) ⟩
    suc (suc d / suc (suc d) + (x ∸ suc d) / suc (suc d))       ≡˘⟨ cong suc (+-distrib-/-∣ʳ {suc d} (x ∸ suc d) (∣m∣n⇒∣m∸n (divides (suc q) p) ∣-refl)) ⟩
    suc ((suc d + (x ∸ suc d)) / suc (suc d))                   ≡˘⟨ cong (λ x → suc (x / suc (suc d))) (+-∸-assoc (suc d) (+-cancelˡ-≤ 1 (≤-trans (≤-trans (≤-reflexive (sym (*-identityˡ (suc (suc d))))) (*-monoˡ-≤ (suc (suc d)) (s≤s {n = q} z≤n))) (≤-reflexive (sym p)))))⟩
    suc (((suc d + x) ∸ suc d) / suc (suc d))                   ≡⟨ cong (λ x → suc (x / suc (suc d))) (m+n∸m≡n (suc d) x) ⟩
    suc (x / suc (suc d)) ∎
    where
      open ≡-Reasoning

  bar : ∀ {x d} → ¬ (suc (suc d) ∣ suc x) → x % suc (suc d) ≤ d
  bar {x} {d} ¬p with suc x % suc (suc d) | inspect (λ a → a % suc (suc d)) (suc x)
  ... | zero  | [ p ] = ⊥-elim (¬p (m%n≡0⇒n∣m (suc x) (suc d) p))
  ... | suc n | [ p ] = [1+m%d]≤1+n⇒[m%d]≤n x d (suc (suc d)) (≤-trans (s≤s z≤n) (≤-reflexive (sym p))) (+-cancelˡ-≤ 1 (m%n<n (suc x) (suc d)))

  lemma₂ : {x d : ℕ} → ¬ (suc d ∣ suc x) → suc x / suc d ≡ x / suc d
  lemma₂ {x} {zero} ¬p = ⊥-elim (¬p (1∣ suc x))
  lemma₂ {x} {suc d} ¬p with suc x % suc (suc d) | inspect (λ a → a % suc (suc d)) (suc x)
  ... | zero  | [ p ] = ⊥-elim (¬p (m%n≡0⇒n∣m _ _ p))
  ... | suc n | [ p ] = +-distrib-/ 1 x (+-monoʳ-≤ 2 (bar ¬p))

  prop : ∀ d l → suc d * triangle (l / suc d) ≡ sum (filter (suc d ∣?_) (downFrom (suc l)))
  prop d zero = *-zeroʳ d
  prop d (suc l) with suc d ∣? suc l
  ... | true because ofʸ p = begin
    suc d * triangle (suc l / suc d)                         ≡⟨ cong (λ x → suc d * triangle x) (lemma p) ⟩
    suc d * triangle (suc (l / suc d))                       ≡⟨ *-distribˡ-+ (suc d) (suc (l / suc d)) (triangle (l / suc d)) ⟩
    suc d * (suc (l / suc d)) + suc d * triangle (l / suc d) ≡˘⟨ cong (λ x → suc d * x + suc d * triangle (l / suc d)) (lemma p) ⟩
    suc d * (suc l / suc d) + suc d * triangle (l / suc d)   ≡⟨ cong (_+ suc d * triangle (l / suc d)) (m*[n/m]≡n p) ⟩
    suc l + suc d * triangle (l / suc d)                     ≡⟨ cong (suc l +_) (prop d l) ⟩
    sum (suc l ∷ filter (suc d ∣?_) (downFrom (suc l)))      ≡˘⟨ cong sum (filter-accept (suc d ∣?_) p) ⟩
    sum (filter (suc d ∣?_) (suc l ∷ downFrom (suc l)))      ∎
    where
      open ≡-Reasoning
  ... | false because ofⁿ ¬p = begin
    suc d * triangle (suc l / suc d) ≡⟨ cong (λ n → suc d * triangle n) (lemma₂ ¬p) ⟩
    suc d * triangle (l / suc d) ≡⟨ prop d l ⟩
    sum (filter (suc d ∣?_) (downFrom (suc l))) ≡˘⟨ cong sum (filter-reject (suc d ∣?_) ¬p) ⟩
    sum (filter (suc d ∣?_) (suc l ∷ downFrom (suc l))) ∎
    where
      open ≡-Reasoning

  notLemmaAux : ∀ {A : Set} (∙ : A → A → A) (ε : A) (comm : Commutative _≡_ ∙) (assoc : Associative _≡_ ∙) (n : A) (ns : List A) → foldr ∙ ε (n ∷ ns) ≡ foldr ∙ (∙ n ε) ns
  notLemmaAux _∙_ ε comm assoc n [] = refl
  notLemmaAux _∙_ ε comm assoc n (m ∷ ns) = begin
    n ∙ (m ∙ foldr _∙_ ε ns) ≡˘⟨ assoc n m _ ⟩
    (n ∙ m) ∙ foldr _∙_ ε ns ≡⟨ cong (_∙ foldr _∙_ ε ns) (comm n m) ⟩
    (m ∙ n) ∙ foldr _∙_ ε ns ≡⟨ assoc m n _ ⟩
    m ∙ (n ∙ foldr _∙_ ε ns) ≡⟨ cong (m ∙_) (notLemmaAux _∙_ ε comm assoc n ns) ⟩
    m ∙ foldr _∙_ (n ∙ ε) ns ∎
    where
      open ≡-Reasoning

  foldr-downFrom-insert : ∀ {A : Set} (_∙_ : A → A → A) (ε : A) (f : ℕ → A) (n : ℕ) → foldr _∙_ (f zero ∙ ε) (applyDownFrom (λ x → f (suc x)) n) ≡ foldr _∙_ ε (applyDownFrom f (suc n))
  foldr-downFrom-insert _∙_ ε f zero = refl
  foldr-downFrom-insert _∙_ ε f (suc n) = cong (f (suc n) ∙_) (foldr-downFrom-insert _∙_ ε f n)

  notLemmaFilterAuxⁿ : ∀ {A : Set} (∙ : A → A → A) (ε : A) {p} {P : Pred A p} (P? : Decidable P) (f : ℕ → A) (n : ℕ) → ¬ P (f 0) → foldr ∙ ε (filter P? (applyDownFrom (λ x → f (suc x)) n)) ≡ foldr ∙ ε (filter P? (applyDownFrom f (suc n)))
  notLemmaFilterAuxⁿ ∙ ε P? f zero ¬p = cong (foldr ∙ ε) (sym (filter-reject P? ¬p))
  notLemmaFilterAuxⁿ ∙ ε P? f (suc n) ¬p with does (P? (f (suc n)))
  ... | false = notLemmaFilterAuxⁿ ∙ ε P? f n ¬p
  ... | true  = cong (∙ (f (suc n))) (notLemmaFilterAuxⁿ ∙ ε P? f n ¬p)

  foldr-filter-downFrom-insert : ∀ {A : Set} (_∙_ : A → A → A) (ε : A) {p} {P : Pred A p} (P? : Decidable P) (f : ℕ → A) (n : ℕ) → P (f zero) → foldr _∙_ (f zero ∙ ε) (filter P? (applyDownFrom (λ x → f (suc x)) n)) ≡ foldr _∙_ ε (filter P? (applyDownFrom f (suc n)))
  foldr-filter-downFrom-insert _∙_ ε P? f zero p = begin
    f zero ∙ ε ≡˘⟨ cong (foldr _∙_ ε) (filter-accept P? p) ⟩
    foldr _∙_ ε (filter P? (f zero ∷ [])) ∎
    where
      open ≡-Reasoning
  foldr-filter-downFrom-insert _∙_ ε P? f (suc n) p with does (P? (f (suc n)))
  ... | true = cong (f (suc n) ∙_) (foldr-filter-downFrom-insert _∙_ ε P? f n p)
  ... | false = foldr-filter-downFrom-insert _∙_ ε P? f n p

  notLemmaFilter : ∀ {A : Set} (∙ : A → A → A) (ε : A) (comm : Commutative _≡_ ∙) (assoc : Associative _≡_ ∙) {p} {P : Pred A p} (P? : Decidable P) (f : ℕ → A) (n : ℕ) → foldr ∙ ε (filter P? (applyUpTo f n)) ≡ foldr ∙ ε (filter P? (applyDownFrom f n))
  notLemmaFilter ∙ ε comm assoc P? f zero = refl
  notLemmaFilter ∙ ε comm assoc P? f (suc n) with P? (f zero)
  ... | false because ofⁿ ¬p = begin
    foldr ∙ ε (filter P? (applyUpTo (λ x → f (suc x)) n)) ≡⟨ notLemmaFilter ∙ ε comm assoc P? (λ x → f (suc x)) n ⟩
    foldr ∙ ε (filter P? (applyDownFrom (λ x → f (suc x)) n)) ≡⟨ notLemmaFilterAuxⁿ ∙ ε P? f n ¬p ⟩
    foldr ∙ ε (filter P? (applyDownFrom f (suc n))) ∎
    where
      open ≡-Reasoning
  ... | true because ofʸ p  = begin
    ∙ (f zero) (foldr ∙ ε (filter P? (applyUpTo (λ x → f (suc x)) n))) ≡⟨ notLemmaAux ∙ ε comm assoc (f zero) (filter P? (applyUpTo (λ x → f (suc x)) n)) ⟩
    foldr ∙ (∙ (f zero) (ε)) (filter P? (applyUpTo (λ x → f (suc x)) n)) ≡⟨ notLemmaFilter ∙ (∙ (f zero) ε) comm assoc P? (λ x → f (suc x)) n ⟩
    foldr ∙ (∙ (f zero) (ε)) (filter P? (applyDownFrom (λ x → f (suc x)) n)) ≡⟨ foldr-filter-downFrom-insert ∙ ε P? f n p ⟩
    foldr ∙ ε (filter P? (applyDownFrom f (suc n))) ∎
    where
      open ≡-Reasoning

  prop′ : ∀ d l → suc d * triangle″ (l / suc d) ≡ sum (filter (suc d ∣?_) (upTo (suc l)))
  prop′ d l = begin
    suc d * triangle″ (l / suc d)               ≡˘⟨ cong (λ x → suc d * x) (triangle≗triangle″ (l / suc d)) ⟩
    suc d * triangle (l / suc d)                ≡⟨ prop d l ⟩
    sum (filter (suc d ∣?_) (downFrom (suc l))) ≡˘⟨ notLemmaFilter _+_ 0 +-comm +-assoc (suc d ∣?_) (λ x → x) (suc l) ⟩
    sum (filter (suc d ∣?_) (upTo (suc l)))     ∎
    where
      open ≡-Reasoning

  recombine-divisors : ∀ d d′ xs → sum (filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs) ≡ sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)
  recombine-divisors d d′ [] = refl
  recombine-divisors d d′ (x ∷ xs) with suc d ∣? x | suc d′ ∣? x
  ... | .true because ofʸ p | .true because ofʸ q = begin
    sum (filter (suc d ∣?_) (x ∷ xs)) + sum (filter (suc d′ ∣?_) (x ∷ xs)) ≡⟨ cong₂ (λ x y → sum x + sum y) (filter-accept (suc d ∣?_) p) (filter-accept (suc d′ ∣?_) q) ⟩
    sum (x ∷ filter (suc d ∣?_) xs) + sum (x ∷ filter (suc d′ ∣?_) xs) ≡⟨⟩
    (x + sum (filter (suc d ∣?_) xs)) + (x + sum (filter (suc d′ ∣?_) xs)) ≡⟨ +-assoc x (sum (filter (suc d ∣?_) xs)) _ ⟩
    x + (sum (filter (suc d ∣?_) xs) + (x + sum (filter (suc d′ ∣?_) xs))) ≡˘⟨ cong (x +_) (+-assoc (sum (filter (suc d ∣?_) xs)) x _) ⟩
    x + ((sum (filter (suc d ∣?_) xs) + x) + sum (filter (suc d′ ∣?_) xs)) ≡⟨ cong (λ n → x + (n + sum (filter (suc d′ ∣?_) xs))) (+-comm _ x) ⟩
    x + ((x + sum (filter (suc d ∣?_) xs)) + sum (filter (suc d′ ∣?_) xs)) ≡⟨ cong (x +_) (+-assoc x (sum (filter (suc d ∣?_) xs)) _) ⟩
    x + (x + (sum (filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs))) ≡˘⟨ +-assoc x x _ ⟩
    (x + x) + (sum (filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs)) ≡⟨ cong ((x + x) +_) (recombine-divisors d d′ xs) ⟩
    (x + x) + (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)) ≡⟨ +-assoc x x _ ⟩
    x + (x + (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs))) ≡˘⟨ cong (x +_) (+-assoc x (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) _) ⟩
    x + ((x + sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)) ≡⟨ cong (λ n → x + (n + sum (filter (lcm (suc d) (suc d′) ∣?_) xs))) (+-comm x _) ⟩
    x + ((sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + x) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)) ≡⟨ cong (x +_) (+-assoc (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) x _) ⟩
    x + (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + (x + sum (filter (lcm (suc d) (suc d′) ∣?_) xs))) ≡˘⟨ +-assoc x (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) _ ⟩
    (x + sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) + (x + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)) ≡⟨⟩
    sum (x ∷ filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (x ∷ filter (lcm (suc d) (suc d′) ∣?_) xs) ≡˘⟨ cong₂ (λ x y → sum x + sum y) (filter-accept ((suc d ∣?_) ∪? (suc d′ ∣?_)) (inj₁ p)) (filter-accept (lcm (suc d) (suc d′) ∣?_) (lcm-least p q))⟩
    sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) (x ∷ xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) (x ∷ xs)) ∎
    where
      open ≡-Reasoning
  ... | .true because ofʸ p | .false because ofⁿ ¬q = begin
    sum (filter (suc d ∣?_) (x ∷ xs)) + sum (filter (suc d′ ∣?_) (x ∷ xs)) ≡⟨ cong₂ (λ x y → sum x + sum y) (filter-accept (suc d ∣?_) p) (filter-reject (suc d′ ∣?_) ¬q) ⟩
    sum (x ∷ filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs) ≡⟨ +-assoc x (sum (filter (suc d ∣?_) xs)) _ ⟩
    x + (sum (filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs)) ≡⟨ cong (x +_) (recombine-divisors d d′ xs) ⟩
    x + (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)) ≡˘⟨ +-assoc x (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) _ ⟩
    (x + sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs) ≡˘⟨ cong₂ (λ x y → sum x + sum y) (filter-accept ((suc d ∣?_) ∪? (suc d′ ∣?_)) (inj₁ p)) (filter-reject (lcm (suc d) (suc d′) ∣?_) (λ r → ¬q (∣-trans (n∣lcm[m,n] (suc d) (suc d′)) r))) ⟩
    sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) (x ∷ xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) (x ∷ xs)) ∎
    where
      open ≡-Reasoning
  ... | .false because ofⁿ ¬p | .true because ofʸ q = begin
    sum (filter (suc d ∣?_) (x ∷ xs)) + sum (filter (suc d′ ∣?_) (x ∷ xs)) ≡⟨ cong₂ (λ x y → sum x + sum y) (filter-reject (suc d ∣?_) ¬p) (filter-accept (suc d′ ∣?_) q) ⟩
    sum (filter (suc d ∣?_) xs) + sum (x ∷ filter (suc d′ ∣?_) xs) ≡˘⟨ +-assoc (sum (filter (suc d ∣?_) xs)) x _ ⟩
    (sum (filter (suc d ∣?_) xs) + x) + sum (filter (suc d′ ∣?_) xs) ≡⟨ cong (_+ sum (filter (suc d′ ∣?_) xs)) (+-comm _ x) ⟩
    (x + sum (filter (suc d ∣?_) xs)) + sum (filter (suc d′ ∣?_) xs) ≡⟨ +-assoc x (sum (filter (suc d ∣?_) xs)) _ ⟩
    x + (sum (filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs)) ≡⟨ cong (x +_) (recombine-divisors d d′ xs) ⟩
    x + (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs)) ≡˘⟨ +-assoc x (sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) _ ⟩
    (x + sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs) ≡˘⟨ cong₂ (λ x y → sum x + sum y) (filter-accept ((suc d ∣?_) ∪? (suc d′ ∣?_)) (inj₂ q)) (filter-reject (lcm (suc d) (suc d′) ∣?_) λ r → ¬p (∣-trans (m∣lcm[m,n] (suc d) (suc d′)) r)) ⟩
    sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) (x ∷ xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) (x ∷ xs)) ∎
    where
      open ≡-Reasoning
  ... | .false because ofⁿ ¬p | .false because ofⁿ ¬q = begin
    sum (filter (suc d ∣?_) (x ∷ xs)) + sum (filter (suc d′ ∣?_) (x ∷ xs)) ≡⟨ cong₂ (λ x y → sum x + sum y) (filter-reject (suc d ∣?_) ¬p) (filter-reject (suc d′ ∣?_) ¬q) ⟩
    sum (filter (suc d ∣?_) xs) + sum (filter (suc d′ ∣?_) xs) ≡⟨ recombine-divisors d d′ xs ⟩
    sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) xs) + sum (filter (lcm (suc d) (suc d′) ∣?_) xs) ≡˘⟨ cong₂ (λ x y → sum x + sum y) (filter-reject ((suc d ∣?_) ∪? (suc d′ ∣?_)) [ ¬p , ¬q ]) (filter-reject (lcm (suc d) (suc d′) ∣?_) (λ r → ¬p (∣-trans (m∣lcm[m,n] (suc d) (suc d′)) r))) ⟩
    sum (filter ((suc d ∣?_) ∪? (suc d′ ∣?_)) (x ∷ xs)) + sum (filter (lcm (suc d) (suc d′) ∣?_) (x ∷ xs)) ∎
    where
      open ≡-Reasoning

solution′ : ℕ → ℕ
solution′ zero = zero
solution′ (suc n) = 3 * Lemmas.triangle″ (n / 3) + 5 * Lemmas.triangle″ (n / 5) ∸ 15 * Lemmas.triangle″ (n / 15)

solution-correct : problem′ ≗ solution′
solution-correct zero = refl
solution-correct (suc n) = begin
  sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo (suc n))) ≡˘⟨ +-identityʳ _ ⟩
  sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo (suc n))) + 0 ≡˘⟨ cong (sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo (suc n))) +_) (n∸n≡0 (sum (filter (15 ∣?_) (upTo (suc n))))) ⟩
  sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo (suc n))) + (sum (filter (15 ∣?_) (upTo (suc n))) ∸ sum (filter (15 ∣?_) (upTo (suc n)))) ≡˘⟨ +-∸-assoc (sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo (suc n)))) {sum (filter (15 ∣?_) (upTo (suc n)))} ≤-refl ⟩
  (sum (filter ((3 ∣?_) ∪? (5 ∣?_)) (upTo (suc n))) + sum (filter (15 ∣?_) (upTo (suc n)))) ∸ sum (filter (15 ∣?_) (upTo (suc n))) ≡˘⟨ cong (_∸ sum (filter (15 ∣?_) (upTo (suc n)))) (Lemmas.recombine-divisors 2 4 (upTo (suc n))) ⟩
  (sum (filter (3 ∣?_) (upTo (suc n))) + sum (filter (5 ∣?_) (upTo (suc n)))) ∸ sum (filter (15 ∣?_) (upTo (suc n))) ≡˘⟨ congₙ 3 (λ x y z → x + y ∸ z) (Lemmas.prop′ 2 n) (Lemmas.prop′ 4 n) (Lemmas.prop′ 14 n) ⟩
  (3 * Lemmas.triangle″ (n / 3) + 5 * Lemmas.triangle″ (n / 5)) ∸ 15 * Lemmas.triangle″ (n / 15) ∎
  where
    open ≡-Reasoning

solution : ℕ
solution = solution′ 1000

-- output the solution
open import Data.Nat.Show
open import IO
import IO.Primitive as Prim

main : Prim.IO _
main = run (putStrLn (show solution))

max_stars_repo_name: Taneb/project-euler

max_issues_repo_name: Taneb/project-euler

max_forks_repo_name: Taneb/project-euler


text:
-- {-# OPTIONS -v tc.cover.splittree:10 -v tc.cc:30 #-}
module Issue829 where

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

postulate
  P : ⊥ → Set

data D : (A : Set) → A → Set where
  c : ⊥ → (x : ⊤) → D ⊤ x

f : {A : Set} {x : A} → D A x → ⊥
f (c () .tt)

g : (x : ⊥) → P x
g ()

h : (A : Set) (x : A) (d : D A x) → P (f d)
h .⊤ tt (c x .tt) = g x

-- Bug.agda:21,21-24
-- Incomplete pattern matching when applying Bug.f
-- when checking that the expression g x has type P (f (c x tt))

-- Agda 2.3.2 gives the following more reasonable error message:
--
-- Bug.agda:21,21-24
-- x != f (c x tt) of type ⊥
-- when checking that the expression g x has type P (f (c x tt))

-- This regression is caused by the patch "Fixed  issue 827 : incomplete
-- case tree caused by record pattern translation".

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2019-05-15
-- one-linear-layout
-- Author: ice10
--

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

import Relation.Binary
variable A : Set
private variable B : Set

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


text:
module Data.Num.Continuous where

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

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

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

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

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

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

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

Continuous : ∀ b d o → Set
Continuous b d o = (xs : Numeral b d o) → Incrementable xs

Bounded⇒¬Continuous : ∀ {b d o}
    → Bounded b d o
    → ¬ (Continuous b d o)
Bounded⇒¬Continuous (xs , max) claim = contradiction (claim xs) (Maximum⇒¬Incrementable xs max)

first-endpoint : ∀ b d o → Numeral (suc b) (suc d) o
first-endpoint b d o = greatest-digit d ∙

first-endpoint-¬Incrementable : ∀ {b d o}
    → (proper : 2 ≤ suc (d + o))
    → (gapped : Gapped#0 b d o)
    → ¬ (Incrementable (first-endpoint b d o))
first-endpoint-¬Incrementable {b} {d} {o} proper gapped with nextView (first-endpoint b d o) proper
first-endpoint-¬Incrementable proper gapped | Interval b d o ¬greatest
    = contradiction (greatest-digit-is-the-Greatest d) ¬greatest
first-endpoint-¬Incrementable proper gapped | GappedEndpoint b d o greatest _
    = GappedEndpoint⇒¬Incrementable (first-endpoint b d o) greatest proper gapped
first-endpoint-¬Incrementable proper gapped | UngappedEndpoint b d o greatest ¬gapped
    = contradiction gapped ¬gapped

Gapped#0⇒¬Continuous : ∀ {b d o}
    → (proper : 2 ≤ suc (d + o))
    → (gapped : Gapped#0 b d o)
    → ¬ (Continuous (suc b) (suc d) o)
Gapped#0⇒¬Continuous {b} {d} {o} proper gapped#0 cont
    = contradiction
        (cont (first-endpoint b d o))
        (first-endpoint-¬Incrementable proper gapped#0)

¬Gapped#0⇒Continuous : ∀ {b d o}
    → (proper : 2 ≤ suc (d + o))
    → (¬gapped : ¬ (Gapped#0 b d o))
    → Continuous (suc b) (suc d) o
¬Gapped#0⇒Continuous proper ¬gapped#0 xs with Incrementable? xs
¬Gapped#0⇒Continuous proper ¬gapped#0 xs | yes incr = incr
¬Gapped#0⇒Continuous proper ¬gapped#0 xs | no ¬incr = contradiction
    (¬Gapped⇒Incrementable xs proper (¬Gapped#0⇒¬Gapped xs proper ¬gapped#0))
    ¬incr

Continuous-Proper : ∀ b d o
    → (proper : 2 ≤ suc (d + o))
    → Dec (Continuous (suc b) (suc d) o)
Continuous-Proper b d o proper with Gapped#0? b d o
Continuous-Proper b d o proper | yes gapped#0 = no  (Gapped#0⇒¬Continuous proper gapped#0)
Continuous-Proper b d o proper | no ¬gapped#0 = yes (¬Gapped#0⇒Continuous proper ¬gapped#0)

Continuous? : ∀ b d o → Dec (Continuous b d o)
Continuous? b d o with numView b d o
Continuous? _ _ _ | NullBase d o = no (Bounded⇒¬Continuous (Bounded-NullBase d o))
Continuous? _ _ _ | NoDigits b o = yes (λ xs → NoDigits-explode xs)
Continuous? _ _ _ | AllZeros b = no (Bounded⇒¬Continuous (Bounded-AllZeros b))
Continuous? _ _ _ | Proper b d o proper = Continuous-Proper b d o proper

-- Continuous⇒¬Gapped#0 : ∀ {b d o}
--     → (cont : True (Continuous? (suc b) (suc d) o))
--     → (proper : suc d + o ≥ 2)
--     → ¬ (Gapped#0 b d o)
-- Continuous⇒¬Gapped#0 cont proper gapped#0 = contradiction (toWitness cont) (Gapped#0⇒¬Continuous proper gapped#0)

-- -- a partial function that only maps ℕ to Continuous Nums
-- fromℕ : ∀ {b d o}
--     → (True (Continuous? b (suc d) o))
--     → (val : ℕ)
--     → (True (o ≤? val))
--     → Numeral b (suc d) o
-- fromℕ {o = zero} cont zero o≤n = z ∙
-- fromℕ {o = zero} cont (suc n) o≤n = 1+ cont (fromℕ cont n tt)
-- fromℕ {o = suc o} cont zero ()
-- fromℕ {o = suc o} cont (suc n) o≤n with o ≟ n
-- fromℕ {b} {d} {suc o} cont (suc n) o≤n | yes o≡n = z ∙
-- fromℕ {b} {d} {suc o} cont (suc n) o≤n | no  o≢n = 1+ cont (fromℕ cont n (fromWitness o<n))
--     where
--         o<n : o < n
--         o<n = ≤∧≢⇒< (≤-pred (toWitness o≤n)) o≢n

1+ : ∀ {b d o}
    → {cont : True (Continuous? b d o)}
    → (xs : Numeral b d o)
    → Numeral b d o
1+ {cont = cont} xs = proj₁ (toWitness cont xs)

1+-toℕ : ∀ {b d o}
    → {cont : True (Continuous? b d o)}
    → (xs : Numeral b d o)
    → ⟦ 1+ {cont = cont} xs ⟧ ≡ suc ⟦ xs ⟧
1+-toℕ {cont = cont} xs = proj₂ (toWitness cont xs)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module FFI.Data.HaskellString where

open import Agda.Builtin.String using (String)

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

postulate HaskellString : Set
{-# COMPILE GHC HaskellString = type Data.String.String #-}

postulate pack : HaskellString → String
{-# COMPILE GHC pack = Data.Text.pack #-}

postulate unpack : String → HaskellString
{-# COMPILE GHC unpack = Data.Text.unpack #-}

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau