text:
module UniDB.Subst.Star where

open import UniDB.Subst.Core
open import UniDB.Morph.Star

module _
  {T : STX} {{vrT : Vr T}} {{apTT : Ap T T}}
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
  where

  instance
    iLkStar : Lk T (Star Ξ)
    lk {{iLkStar}} ε        i = vr i
    lk {{iLkStar}} (ξs ▻ ξ) i = ap {T} ξ (lk ξs i)

    iLkIdmStar : LkIdm T (Star Ξ)
    lk-idm {{iLkIdmStar}} i = refl

    -- iLkCompApStar : {{apIdmT : ApIdm T T}} → LkCompAp T (Star Ξ)
    -- lk-⊙-ap {{iLkCompApStar}} ξs ε        i = sym (ap-idm T T (Star Ξ) (lk T (Star Ξ) ξs i))
    -- lk-⊙-ap {{iLkCompApStar}} ξs (ζs ▻ ζ) i =
    --   begin
    --     ap T T Ξ ζ (lk T (Star Ξ) (ξs ⊙ ζs) i)
    --   ≡⟨ cong (ap T T Ξ ζ) (lk-⊙-ap T (Star Ξ) ξs ζs i) ⟩
    --     ap T T Ξ ζ (ap T T (Star Ξ) ζs (lk T (Star Ξ) ξs i))
    --   ≡⟨ {!!} ⟩
    --     ap T T (Star Ξ) (ζs ▻ ζ) (lk T (Star Ξ) ξs i)
    --   ∎

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
module Formalization.RecursiveFunction where

import      Lvl
open import Data
open import Data.ListSized
open import Numeral.Finite
open import Numeral.Natural
open import Syntax.Number
open import Type{Lvl.𝟎}

-- Function(n) is a syntactic representation of recursive functions of type (ℕⁿ → ℕ).
-- The syntax
data Function : ℕ → Type where
  -- Base cases
  Base        : Function(0)
  Successor   : Function(1)
  Projection  : ∀{n : ℕ} → (i : 𝕟(n)) → Function(n)

  -- Inductive cases
  Composition : ∀{m n : ℕ} → Function(n) → List(Function(m))(n) → Function(m)
  Recursion   : ∀{n : ℕ} → Function(n) → Function(𝐒(𝐒(n))) → Function(𝐒(n))
  Minimization : ∀{n : ℕ} → Function(𝐒(n)) → Function(n)

Primitive : Type
Primitive = ℕ

module _ where
  open import Data.ListSized.Functions
  open import Functional
  open import Logic.Predicate
  open import Numeral.Natural.Relation.Order

  private variable m n   : ℕ
  private variable i     : 𝕟(n)
  private variable x v   : Primitive
  private variable xs vs : List(Primitive)(n)
  private variable f g   : Function(m)
  private variable fs gs : List(Function(m))(n)

  -- The operational semantics.
  data _$_⟹_ : ∀{m n} → List(Function(m))(n) → List(Primitive)(m) → List(Primitive)(n) → Type
  data _$_⟶_ : ∀{n} → Function(n) → List(Primitive)(n) → ℕ → Type where
    zero : (Base $ ∅ ⟶ 𝟎)
    succ : (Successor $ singleton(n) ⟶ 𝐒(n))
    proj : (Projection{n}(i) $ xs ⟶ index(i)(xs))
    comp : (f $ vs ⟶ v) → (gs $ xs ⟹ vs) → (Composition{m}{n} f gs $ xs ⟶ v)
    rec𝟎 : (f $ xs ⟶ v) → (Recursion f g $ (𝟎 ⊰ xs) ⟶ v)
    rec𝐒 : (Recursion f g $ (n ⊰ xs) ⟶ x) → (g $ (n ⊰ x ⊰ xs) ⟶ v) → (Recursion f g $ (𝐒(n) ⊰ xs) ⟶ v)
    min  : (f $ (n ⊰ xs) ⟶ 𝟎) → ∃{Obj = ℕ → ℕ}(k ↦ ∀{m} → (m < n) → (f $ (m ⊰ xs) ⟶ 𝐒(k(m)))) → (Minimization f $ xs ⟶ n)
  data _$_⟹_ where
    base : (∅ $ xs ⟹ ∅)
    step : (f $ xs ⟶ v) → (fs $ xs ⟹ vs) → ((f ⊰ fs) $ xs ⟹ (v ⊰ vs))

  -- TODO: The denotational semantics should use partial functions, but even if that was used, one needs to decide whether there is a 0 in an arbitrary function's range. This is not possible, I guess?

  open import Logic.Propositional
  open import Numeral.Natural.Relation.Order.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Structure.Operator
  open import Structure.Setoid.Uniqueness

  [$⟹]-deterministic : Unique(fs $ xs ⟹_)

  [$⟶]-deterministic : Unique(f $ xs ⟶_)
  [$⟶]-deterministic zero         zero = [≡]-intro
  [$⟶]-deterministic succ         succ = [≡]-intro
  [$⟶]-deterministic proj         proj = [≡]-intro
  [$⟶]-deterministic (comp p₁ p₂) (comp q₁ q₂) rewrite [$⟹]-deterministic p₂ q₂ = [$⟶]-deterministic p₁ q₁
  [$⟶]-deterministic (rec𝟎 p)     (rec𝟎 q) = [$⟶]-deterministic p q
  [$⟶]-deterministic (rec𝐒 p₁ p₂) (rec𝐒 q₁ q₂) rewrite [$⟶]-deterministic p₁ q₁ = [$⟶]-deterministic p₂ q₂
  [$⟶]-deterministic {x = x}{y = y} (min p₁ ([∃]-intro k₁ ⦃ p₂ ⦄)) (min q₁ ([∃]-intro k₂ ⦃ q₂ ⦄)) with [<]-trichotomy {x}{y}
  ... | [∨]-introₗ ([∨]-introₗ lt) with () ← [$⟶]-deterministic p₁ (q₂ lt)
  ... | [∨]-introₗ ([∨]-introᵣ eq) = eq
  ... | [∨]-introᵣ             gt  with () ← [$⟶]-deterministic q₁ (p₂ gt)

  [$⟹]-deterministic base base = [≡]-intro
  [$⟹]-deterministic (step p pl) (step q ql) = congruence₂(_⊰_) ([$⟶]-deterministic p q) ([$⟹]-deterministic pl ql)

  [$⟶]-not-total : ∃{Obj = Function(n)}(f ↦ ∀{xs} → ¬ ∃(f $ xs ⟶_))
  ∃.witness [$⟶]-not-total = Minimization (Composition Successor (singleton (Projection 0)))
  ∃.proof   [$⟶]-not-total ([∃]-intro _ ⦃ min (comp () _) _ ⦄)

ext: agda

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:
{-# OPTIONS --without-K #-}

module FinEquiv where

-- The goal is to establish that finite sets and equivalences form a
-- commutative semiring.

import Level using (zero)

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_,_; _×_; proj₁; proj₂)

open import Data.Nat
  using (ℕ; zero; suc; _+_; _*_; ≤-pred; _<_; _≤_; _≥_; _≤?_;
         module ≤-Reasoning)
open import Data.Nat.DivMod using (_divMod_; result)
open import Data.Nat.Properties using (≰⇒>; 1+n≰n; m≤m+n; ¬i+1+j≤i)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-assoc; +-suc; +-comm; *-right-zero)

open import Data.Fin
  using (Fin; zero; suc; inject+; raise; toℕ; fromℕ≤; reduce≥)
open import Data.Fin.Properties
  using (bounded; inject+-lemma; toℕ-raise; toℕ-injective; toℕ-fromℕ≤)

open import Algebra using (CommutativeSemiring)
open import Algebra.Structures
  using (IsSemigroup; IsCommutativeMonoid; IsCommutativeSemiring)

open import Function using (_∘_; id; case_of_)
open import Relation.Nullary using (yes; no)
open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; subst;
         module ≡-Reasoning; inspect; [_])

--

open import Equiv
  using (_∼_; _≃_; id≃; sym≃; trans≃; _●_;
         qinv; module isqinv; _⊎≃_; _×≃_)
open import TypeEquiv
  using (assocl₊equiv; unite₊′equiv;
    unite₊equiv; swap₊equiv;
    unite⋆equiv; unite⋆′equiv; swap⋆equiv; assocl⋆equiv;
    distzequiv; distzrequiv; distequiv; distlequiv)

open import Proofs using (
  -- LeqLemmas
  _<?_; cong+r≤; cong+l≤; cong*r≤;
  -- FinNatLemmas
  inj₁-≡; inj₂-≡; inject+-injective; raise-injective; addMul-lemma
  )

------------------------------------------------------------------------------
-- This is the relation we are interested in showing is a commutative
-- semiring.

_fin≃_ : (m n : ℕ) → Set
m fin≃ n = Fin m ≃ Fin n

-- Additive unit and multiplicative unit are Fin 0 and Fin 1 which are
-- equivalent to ⊥ and ⊤

abstract

  Fin0-⊥ : Fin 0 → ⊥
  Fin0-⊥ ()

  F0≃⊥ : Fin 0 ≃ ⊥
  F0≃⊥ = f , qinv g α β
    where
      f : Fin 0 → ⊥
      f ()
      g : ⊥ → Fin 0
      g ()
      α : f ∘ g ∼ id
      α ()
      β : g ∘ f ∼ id
      β ()

  Fin1≃⊤ : Fin 1 ≃ ⊤
  Fin1≃⊤ = f , qinv g α β
    where
      f : Fin 1 → ⊤
      f zero = tt
      f (suc ())
      g : ⊤ → Fin 1
      g tt = zero
      α : f ∘ g ∼ id
      α tt = refl
      β : g ∘ f ∼ id
      β zero = refl
      β (suc ())

------------------------------------------------------------------------------
-- Additive monoid

module Plus where
  infix 9 _+F_

  -- Main goal is to show (Fin m ⊎ Fin n) ≃ Fin (m + n) It is then
  -- fairly easy to show that ⊎ satisfies the commutative monoid
  -- axioms

  fwd : {m n : ℕ} → (Fin m ⊎ Fin n) → Fin (m + n)
  fwd {m} {n} (inj₁ x) = inject+ n x
  fwd {m} {n} (inj₂ y) = raise m y

  bwd : {m n : ℕ} → Fin (m + n) → (Fin m ⊎ Fin n)
  bwd {m} {n} = λ i → case (toℕ i <? m) of λ
    { (yes p) → inj₁ (fromℕ≤ p)
     ; (no ¬p) → inj₂ (reduce≥ i (≤-pred (≰⇒> ¬p)))
     }

  fwd∘bwd~id : {m n : ℕ} → fwd {m} {n} ∘ bwd ∼ id
  fwd∘bwd~id {m} i with toℕ i <? m
  fwd∘bwd~id i | yes p = sym (inj₁-≡ i p)
  fwd∘bwd~id i | no ¬p = sym (inj₂-≡ i (≤-pred (≰⇒> ¬p)))

  bwd∘fwd~id : {m n : ℕ} → bwd {m} {n} ∘ fwd ∼ id
  bwd∘fwd~id {m} {n} (inj₁ x) with toℕ (inject+ n x) <? m
  bwd∘fwd~id {n = n} (inj₁ x) | yes p =
     cong inj₁
       (inject+-injective (fromℕ≤ p) x (sym (inj₁-≡ (inject+ n x) p)))
  bwd∘fwd~id {m} {n} (inj₁ x) | no ¬p = ⊥-elim (1+n≰n pf)
   where
     open ≤-Reasoning
     pf : suc (toℕ x) ≤ toℕ x
     pf = let q =  (≤-pred (≰⇒> ¬p)) in
            begin (
              suc (toℕ x)
                ≤⟨ bounded x ⟩
              m
                ≤⟨ q ⟩
              toℕ (inject+ n x)
                ≡⟨ sym (inject+-lemma n x) ⟩
              toℕ x ∎ )
  bwd∘fwd~id {m} {n} (inj₂ y) with toℕ (raise m y) <? m
  bwd∘fwd~id {m} {n} (inj₂ y) | yes p = ⊥-elim (1+n≰n pf)
   where
     open ≤-Reasoning
     pf : suc m ≤ m
     pf = begin (
             suc m
                 ≤⟨ m≤m+n (suc m) (toℕ y) ⟩
             suc (m + toℕ y)
                 ≡⟨ cong suc (sym (toℕ-raise m y)) ⟩
             suc (toℕ (raise m y))
                 ≤⟨ p ⟩
             m ∎)
  bwd∘fwd~id {m} {n} (inj₂ y) | no ¬p =
     cong inj₂
       (raise-injective {m}
         (reduce≥ (raise m y) (≤-pred (≰⇒> ¬p)))
         y
         (sym (inj₂-≡ (raise m y) (≤-pred (≰⇒> ¬p)))))

  -- the main equivalence

  fwd-iso : {m n : ℕ} → (Fin m ⊎ Fin n) ≃ Fin (m + n)
  fwd-iso {m} {n} = fwd , qinv bwd (fwd∘bwd~id {m}) (bwd∘fwd~id {m})

  -- aliases for the above which are more convenient
  ⊎≃+ : {m n : ℕ} → (Fin m ⊎ Fin n) ≃ Fin (m + n)
  ⊎≃+ = fwd-iso

  +≃⊎ : {m n : ℕ} → Fin (m + n) ≃ (Fin m ⊎ Fin n)
  +≃⊎ = sym≃ fwd-iso

  -- additive monoid equivalences

  -- unite+

  unite+ : {m : ℕ} → Fin (0 + m) ≃ Fin m
  unite+ = unite₊equiv ● F0≃⊥ ⊎≃ id≃ ● +≃⊎

  -- and on the other side as well

  unite+r : {m : ℕ} → Fin (m + 0) ≃ Fin m
  unite+r = unite₊′equiv ● id≃ ⊎≃ F0≃⊥ ● +≃⊎

-- uniti+

  uniti+ : {m : ℕ} → Fin m ≃ Fin (0 + m)
  uniti+ = sym≃ unite+

  uniti+r : {m : ℕ} → Fin m ≃ Fin (m + 0)
  uniti+r = sym≃ unite+r

  -- swap₊

  swap+ : {m n : ℕ} → Fin (m + n) ≃ Fin (n + m)
  swap+ {m} = ⊎≃+ ● swap₊equiv ● +≃⊎ {m}

  -- associativity

  assocl+ : {m n o : ℕ} → Fin (m + (n + o)) ≃ Fin ((m + n) + o)
  assocl+ {m} = ⊎≃+ ● ⊎≃+ ⊎≃ id≃ ● assocl₊equiv ● id≃ ⊎≃ +≃⊎ ● +≃⊎ {m}

  assocr+ : {m n o : ℕ} → Fin ((m + n) + o) ≃ Fin (m + (n + o))
  assocr+ {m} = sym≃ (assocl+ {m})

  -- congruence

  _+F_ : {m n o p : ℕ} → (Fin m ≃ Fin n) → (Fin o ≃ Fin p) →
              Fin (m + o) ≃ Fin (n + p)
  Fm≃Fn +F Fo≃Fp = ⊎≃+ ● Fm≃Fn ⊎≃ Fo≃Fp ● +≃⊎

-----------------------------------------------------------------------------
-- Multiplicative monoid

module Times where
  infixl 7 _*F_

  -- main goal is to show (Fin m × Fin n) ≃ Fin (m * n) It is then
  -- fairly easy to show that × satisfies the commutative monoid
  -- axioms

  fwd : {m n : ℕ} → (Fin m × Fin n) → Fin (m * n)
  fwd {suc m} {n} (zero , k) = inject+ (m * n) k
  fwd {n = n} (suc i , k) = raise n (fwd (i , k))

  private
    soundness : ∀ {m n} (i : Fin m) (j : Fin n) →
                toℕ (fwd (i , j)) ≡ toℕ i * n + toℕ j
    soundness {suc m} {n} zero     j = sym (inject+-lemma (m * n) j)
    soundness {n = n} (suc i) j
      rewrite toℕ-raise n (fwd (i , j)) | soundness i j
      = sym (+-assoc n (toℕ i * n) (toℕ j))

    absurd-quotient : (m n q : ℕ) (r : Fin (suc n)) (k : Fin (m * suc n))
         (k≡r+q*sn : toℕ k ≡ toℕ r + q * suc n) (p : m ≤ q) → ⊥
    absurd-quotient m n q r k k≡r+q*sn p = ¬i+1+j≤i (toℕ k) {toℕ r} k≥k+sr
      where k≥k+sr : toℕ k ≥ toℕ k + suc (toℕ r)
            k≥k+sr = begin (toℕ k + suc (toℕ r)
                       ≡⟨ +-suc (toℕ k) (toℕ r) ⟩
                     suc (toℕ k) + toℕ r
                       ≤⟨ cong+r≤ (bounded k) (toℕ r) ⟩
                     (m * suc n) + toℕ r
                       ≡⟨ +-comm (m * suc n) (toℕ r) ⟩
                     toℕ r + (m * suc n)
                       ≡⟨ refl ⟩
                     toℕ r + m * suc n
                       ≤⟨ cong+l≤ (cong*r≤ p (suc n)) (toℕ r) ⟩
                     toℕ r + q * suc n
                       ≡⟨ sym k≡r+q*sn ⟩
                     toℕ k ∎)
                      where open ≤-Reasoning

  elim-right-zero : ∀ {ℓ} {Whatever : Set ℓ}
                    (m : ℕ) → Fin (m * 0) → Whatever
  elim-right-zero m i = ⊥-elim (Fin0-⊥ (subst Fin (*-right-zero m) i))

  bwd : {m n : ℕ} → Fin (m * n) → (Fin m × Fin n)
  bwd {m} {0} k = elim-right-zero m k
  bwd {m} {suc n} k with (toℕ k) divMod (suc n)
  ... | result q r k≡r+q*sn = (fromℕ≤ {q} {m} (q<m) , r)
    where
          q<m : q < m
          q<m with suc q ≤? m
          ... | no ¬p = ⊥-elim
                          (absurd-quotient m n q r k k≡r+q*sn
                            (≤-pred (≰⇒> ¬p)))
          ... | yes p = p

  fwd∘bwd~id : {m n : ℕ} → fwd {m} {n} ∘ bwd ∼ id
  fwd∘bwd~id {m} {zero} i = elim-right-zero m i
  fwd∘bwd~id {m} {suc n} i with (toℕ i) divMod (suc n)
  ... | result q r k≡r+q*sn with suc q ≤? m
  ... | yes p = toℕ-injective (
      begin (
        toℕ (fwd (fromℕ≤ p , r))
          ≡⟨ soundness (fromℕ≤ p) r ⟩
        toℕ (fromℕ≤ p) * (suc n) + toℕ r
          ≡⟨ cong (λ x → x * (suc n) + toℕ r) (toℕ-fromℕ≤ p) ⟩
        q * (suc n) + toℕ r
          ≡⟨ +-comm _ (toℕ r) ⟩
        toℕ r  + q * (suc n)
          ≡⟨ sym (k≡r+q*sn) ⟩
        toℕ i ∎))
      where open ≡-Reasoning
  ... | no ¬p = ⊥-elim (absurd-quotient m n q r i k≡r+q*sn (≤-pred (≰⇒> ¬p)))

  bwd∘fwd~id : {m n : ℕ} → bwd {m} {n} ∘ fwd ∼ id
  bwd∘fwd~id {n = zero} (b , ())
  bwd∘fwd~id {m} {suc n} (b , d) with fwd (b , d) | inspect fwd (b , d)
  ... | k | [ eq ] with (toℕ k) divMod (suc n)
  ... | result q r pf with q <? m
  ... | no ¬p = ⊥-elim (absurd-quotient m n q r k pf (≤-pred (≰⇒> ¬p)))
  ... | yes p = cong₂ _,_  pf₁ (proj₁ same-quot)
    where
      open ≡-Reasoning
      eq' : toℕ d + toℕ b * suc n ≡ toℕ r + q * suc n
      eq' = begin (
        toℕ d + toℕ b * suc n
          ≡⟨ +-comm (toℕ d) _ ⟩
        toℕ b * suc n + toℕ d
          ≡⟨ trans (sym (soundness b d)) (cong toℕ eq) ⟩
        toℕ k
          ≡⟨ pf ⟩
        toℕ r + q * suc n ∎ )
      same-quot : (r ≡ d) × (q ≡ toℕ b)
      same-quot = addMul-lemma q (toℕ b) n r d ( sym eq' )
      pf₁ = (toℕ-injective (trans (toℕ-fromℕ≤ p) (proj₂ same-quot)))

  fwd-iso : {m n : ℕ} → (Fin m × Fin n) ≃ Fin (m * n)
  fwd-iso {m} {n} = fwd , qinv bwd (fwd∘bwd~id {m}) (bwd∘fwd~id {m})

  -- convenient aliases
  ×≃* : {m n : ℕ} → (Fin m × Fin n) ≃ Fin (m * n)
  ×≃* = fwd-iso

  *≃× : {m n : ℕ} → Fin (m * n) ≃ (Fin m × Fin n)
  *≃× = sym≃ ×≃*

  -- multiplicative monoid equivalences

  -- unite*

  unite* : {m : ℕ} → Fin (1 * m) ≃ Fin m
  unite* {m} = unite⋆equiv ● Fin1≃⊤ ×≃ id≃ ● *≃×

  -- uniti*

  uniti* : {m : ℕ} → Fin m ≃ Fin (1 * m)
  uniti* = sym≃ unite*

  -- unite*r

  unite*r : {m : ℕ} → Fin (m * 1) ≃ Fin m
  unite*r {m} = unite⋆′equiv ● id≃ ×≃ Fin1≃⊤ ● *≃×

  -- uniti*r
  uniti*r : {m : ℕ} → Fin m ≃ Fin (m * 1)
  uniti*r = sym≃ unite*r

  -- swap*

  swap* : {m n : ℕ} → Fin (m * n) ≃ Fin (n * m)
  swap* {m} {n} = ×≃* ● swap⋆equiv ● *≃× {m}

  -- associativity

  assocl* : {m n o : ℕ} → Fin (m * (n * o)) ≃ Fin ((m * n) * o)
  assocl* {m} {n} {o} = ×≃* ● ×≃* ×≃ id≃ ● assocl⋆equiv ● id≃ ×≃ *≃× ● *≃× {m}

  assocr* : {m n o : ℕ} → Fin ((m * n) * o) ≃ Fin (m * (n * o))
  assocr* {m} {n} {o} = sym≃ (assocl* {m})

  -- congruence

  _*F_ : {m n o p : ℕ} → Fin m ≃ Fin n → Fin o ≃ Fin p →
              Fin (m * o) ≃ Fin (n * p)
  Fm≃Fn *F Fo≃Fp = ×≃* ● Fm≃Fn ×≃ Fo≃Fp ● *≃×

------------------------------------------------------------------------------
-- Distributivity of multiplication over addition

module PlusTimes where

  -- now that we have two monoids, we need to check distributivity

  -- note that the sequence below is "logically right", *but* could be
  -- replaced by id≃ !
  distz : {m : ℕ} → Fin (0 * m) ≃ Fin 0
  distz {m} = sym≃ F0≃⊥ ● distzequiv ● F0≃⊥ ×≃ id≃ ● *≃× {0} {m}
    where open Times

  factorz : {m : ℕ} → Fin 0 ≃ Fin (0 * m)
  factorz {m} = sym≃ (distz {m})

  distzr : {m : ℕ} → Fin (m * 0) ≃ Fin 0
  distzr {m} = sym≃ F0≃⊥ ● distzrequiv ● id≃ ×≃ F0≃⊥ ● *≃× {m} {0}
    where open Times

  factorzr : {n : ℕ} → Fin 0 ≃ Fin (n * 0)
  factorzr {n} = sym≃ (distzr {n})

  dist : {m n o : ℕ} → Fin ((m + n) * o) ≃ Fin ((m * o) + (n * o))
  dist {m} {n} {o} = ⊎≃+ {m * o} {n * o} ● ×≃* {m} ⊎≃ ×≃* ● distequiv ● +≃⊎ ×≃ id≃ ● *≃×
    where open Times
          open Plus

  factor : {m n o : ℕ} → Fin ((m * o) + (n * o)) ≃ Fin ((m + n) * o)
  factor {m} = sym≃ (dist {m})

  distl : {m n o : ℕ} → Fin (m * (n + o)) ≃ Fin ((m * n) + (m * o))
  distl {m} {n} {o} = ⊎≃+ {m * n} {m * o} ● ×≃* {m} ⊎≃ ×≃* ● distlequiv ● id≃ ×≃ +≃⊎ ● *≃×
    where open Plus
          open Times

  factorl : {m n o : ℕ} → Fin ((m * n) + (m * o)) ≃ Fin (m * (n + o))
  factorl {m} = sym≃ (distl {m})

------------------------------------------------------------------------------
-- Summarizing... we have a commutative semiring structure

fin≃IsEquiv : IsEquivalence _fin≃_
fin≃IsEquiv = record {
  refl = id≃ ;
  sym = sym≃ ;
  trans = trans≃
  }

finPlusIsSG : IsSemigroup _fin≃_ _+_
finPlusIsSG = record {
  isEquivalence = fin≃IsEquiv ;
  assoc = λ m n o → Plus.assocr+ {m} {n} {o} ;
  ∙-cong = Plus._+F_
  }

finTimesIsSG : IsSemigroup _fin≃_ _*_
finTimesIsSG = record {
  isEquivalence = fin≃IsEquiv ;
  assoc = λ m n o → Times.assocr* {m} {n} {o} ;
  ∙-cong = Times._*F_
  }

finPlusIsCM : IsCommutativeMonoid _fin≃_ _+_ 0
finPlusIsCM = record {
  isSemigroup = finPlusIsSG ;
  identityˡ = λ m → id≃ ;
  comm = λ m n → Plus.swap+ {m} {n}
  }

finTimesIsCM : IsCommutativeMonoid _fin≃_ _*_ 1
finTimesIsCM = record {
  isSemigroup = finTimesIsSG ;
  identityˡ = λ m → Times.unite* {m} ;
  comm = λ m n → Times.swap* {m} {n}
  }

finIsCSR : IsCommutativeSemiring _fin≃_ _+_ _*_ 0 1
finIsCSR = record {
  +-isCommutativeMonoid = finPlusIsCM ;
  *-isCommutativeMonoid = finTimesIsCM ;
  distribʳ = λ o m n → PlusTimes.dist {m} {n} {o} ;
  zeroˡ = λ m → PlusTimes.distz {m}
  }

finCSR : CommutativeSemiring Level.zero Level.zero
finCSR = record {
  Carrier = ℕ ;
  _≈_ = _fin≃_ ;
  _+_ = _+_ ;
  _*_ = _*_ ;
  0# = 0 ;
  1# = 1 ;
  isCommutativeSemiring = finIsCSR
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- {-# OPTIONS -v tc.meta:30 --show-irrelevant #-}
-- Andreas, 2013-10-29 submitted by sanzhiyan
-- Documents need for different treating of DontCare in
-- linearity analysis of Miller unification.
-- Now, there can be DontCares stemming from irrelevant projections.

module Issue927 where

import Common.Level

module Fails where

  postulate
    Σ : (B : Set) (C : B → Set) → Set

    <_,_> : {A : Set} {B : A → Set} {C : ∀ x → B x → Set}
          (f : (x : A) → B x) →
          (g : (x : A) → C x (f x)) →
          ((x : A) → Σ (B x) (C x))

  record _⟶_ (A B : Set) : Set  where
    field
      .app : A → B

  open _⟶_ public

  .⟪_,_⟫ : ∀ (A B C : Set) → (A ⟶ B) → (A ⟶ C) → A → Σ B (\ _ → C)
  ⟪_,_⟫ A B C f₁ f₂ = < app f₁ , app f₂ >

-- Using darcs Agda, the following code triggers an
-- internal error at src/full/Agda/TypeChecking/MetaVars.hs:897

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Issue630 where

Test = (A : Set) → A → A

g : Test
g = λ _ x → {!!}

-- the goal should be displayed as ?1 : A
-- not ?1 : _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Here is a smaller test case. The error message is produced using
-- the latest (at the time of writing) development version of Agda.

module Issue183 where

postulate A : Set

T : Set
T = A → A

data L (A : Set) : Set where

data E (x : T) : T → Set where
  e : E x x

foo : (f : A → A) → L (E f (λ x → f x))
foo = λ _ → e

-- Previously:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Translation/AbstractToConcrete.hs:705
-- Should now give a proper error message.

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --cubical --postfix-projections --safe #-}

open import Relation.Binary
open import Prelude hiding (tt)

module Data.List.Sort.Sorted {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open import Relation.Binary.Construct.LowerBound totalOrder

open TotalOrder totalOrder renaming (refl to refl-≤)
open TotalOrder lb-ord renaming (≤-trans to ⌊trans⌋) using ()

open import Data.List
open import Data.Unit.UniversePolymorphic as Poly using (tt)
open import Data.List.Relation.Binary.Permutation
open import Function.Isomorphism
open import Data.Fin
open import Data.List.Membership

private variable lb : ⌊∙⌋

Sorted-cons : E → (⌊∙⌋ → Type (r₁ ℓ⊔ r₂)) → ⌊∙⌋ → Type (r₁ ℓ⊔ r₂)
Sorted-cons x xs lb = (lb ⌊≤⌋ ⌊ x ⌋) × xs ⌊ x ⌋

SortedFrom : ⌊∙⌋ → List E → Type _
SortedFrom = flip (foldr Sorted-cons (const Poly.⊤))

Sorted : List E → Type _
Sorted = SortedFrom ⌊⊥⌋

ord-in : ∀ x xs → SortedFrom lb xs → x ∈ xs → lb ⌊≤⌋ ⌊ x ⌋
ord-in {lb = lb} x (x₁ ∷ xs) p (f0 , x∈xs) = subst (λ z → lb ⌊≤⌋ ⌊ z ⌋) x∈xs (p .fst)
ord-in {lb} x (y ∷ xs) p (fs n , x∈xs) = ⌊trans⌋ {lb} (p .fst) (ord-in x xs (p .snd) (n , x∈xs))

perm-head : ∀ {lbˣ lbʸ} x xs y ys → SortedFrom lbˣ (x ∷ xs) → SortedFrom lbʸ (y ∷ ys) → (x ∷ xs ↭ y ∷ ys) → x ≡ y
perm-head x xs y ys Sxs Sys xs⇔ys with xs⇔ys _ .inv (f0 , refl)
... | f0  , y∈xs = y∈xs
... | fs n , y∈xs with xs⇔ys _ .fun (f0 , refl)
... | f0  , x∈ys = sym x∈ys
... | fs m , x∈ys = antisym (ord-in y xs (Sxs .snd) (n , y∈xs)) (ord-in x ys (Sys .snd) (m , x∈ys))

perm-same : ∀ {lbˣ lbʸ} xs ys → SortedFrom lbˣ xs → SortedFrom lbʸ ys → xs ↭ ys → xs ≡ ys
perm-same [] [] Sxs Sys xs⇔ys = refl
perm-same [] (y ∷ ys) Sxs Sys xs⇔ys = ⊥-elim (xs⇔ys _ .inv (f0 , refl) .fst)
perm-same (x ∷ xs) [] Sxs Sys xs⇔ys = ⊥-elim (xs⇔ys _ .fun (f0 , refl) .fst)
perm-same {lbˣ} {lbʸ} (x ∷ xs) (y ∷ ys) Sxs Sys xs⇔ys =
  let h = perm-head {lbˣ} {lbʸ} x xs y ys Sxs Sys xs⇔ys
  in cong₂ _∷_ h
      (perm-same xs ys (Sxs .snd) (Sys .snd) (tailₚ x xs ys (subst (λ y′ → x ∷ xs ↭ y′ ∷ ys) (sym h) xs⇔ys)))

sorted-perm-eq : ∀ xs ys → Sorted xs → Sorted ys → xs ↭ ys → xs ≡ ys
sorted-perm-eq = perm-same

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Holey where

open import Basics
open import Ix
open import All
open import Cutting
open import Interior
open import Recutter
open import Mask

module HOLEY {I}(C : I |> I) where

  open _|>_ C
  open INTERIOR C
  open RECUTTER C
  open MASK C

  data Holey {I : Set}(P : I -> Set)(i : I) : Set where
    hole : Holey P i
    fill : P i -> Holey P i

  module SUPERIMPOSE {P}(pc : CutKit P)(rec : Recutter) where

    cutHole : CutKit (Holey P)
    cutHole i c hole      = allPu (\ i -> hole) (inners c)
    cutHole i c (fill p)  = all (\ _ -> fill) (inners c) (pc i c p)

    open CHOP cutHole rec

    superimpose : [ Interior (Holey P) -:> Interior (Holey P) -:> Interior (Holey P) ]
    superimpose = mask \
      { i hole     y -> y
      ; i (fill x) y -> tile (fill x)
      }

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
-- Andreas, 2019-10-13, issue 4125
-- Avoid unnecessary normalization in type checker.
-- Print to the user what they wrote, not its expanded form.

-- {-# OPTIONS -v tc:25 #-}

postulate
  We-do-not-want-to : Set → Set
  see-this-in-the-output : Set

A = We-do-not-want-to see-this-in-the-output

postulate
  P : A → Set

test : ∀{a} → P a → P a
test p = {!!} -- C-c C-,

-- Expected to see
--   a : A
-- in the context, not the expanded monster of A.

-- Testing that the etaExpandVar strategy of the unifier
-- does not reduce the context.

record ⊤ : Set where
data D : ⊤ → Set where
  c : ∀{x} → D x

etaExp : ∀{a} → D record{} → P a
etaExp c = {!!}  -- C-c C-,

-- WAS (2.5.x-2.6.0):
--   a : We-do-not-want-to see-this-in-the-output  (not in scope)
-- EXPECTED
--   a : A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Numeric.Rational.Properties where

open import Prelude
open import Numeric.Rational
open import Numeric.Nat.Properties
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.Prime
open import Numeric.Nat.Prime.Properties
open import Numeric.Nat.GCD
open import Numeric.Nat.GCD.Properties
open import Tactic.Nat
open import Tactic.Nat.Coprime

-- Correctness proofs for the efficient arithmetic operations -------

private
  lem-coprime : ∀ n₁ n₂ s′ d₁′ d₂′ g g₁ →
                  s′ * g₁ ≡ n₁ * d₂′ + n₂ * d₁′ →
                  Coprime n₁ (d₁′ * g) →
                  Coprime d₁′ d₂′ →
                  Coprime s′ d₁′
  lem-coprime n₁ n₂ s′ d₁′ d₂′ g g₁ s′g₁=s n₁⊥d₁ d₁′⊥d₂′ =
    coprimeByPrimes s′ d₁′ λ p isP p|s′ p|d₁′ →

      let s  = n₁ * d₂′ + n₂ * d₁′
          d₁ = d₁′ * g

          p|d₁ : p Divides d₁
          p|d₁ = divides-mul-l g p|d₁′

          p|s : p Divides s
          p|s = transport (p Divides_) s′g₁=s (divides-mul-l g₁ p|s′)

          p|n₁d₂′ : p Divides (n₁ * d₂′)
          p|n₁d₂′ = divides-sub-r p|s (divides-mul-r n₂ p|d₁′)

          p∤n₁ : ¬ (p Divides n₁)
          p∤n₁ p|n₁ = prime-divide-coprime p n₁ d₁ isP n₁⊥d₁ p|n₁ p|d₁

          p|d₂′ : p Divides d₂′
          p|d₂′ = case prime-split n₁ d₂′ isP p|n₁d₂′ of λ where
                    (left p|n₁)   → ⊥-elim (p∤n₁ p|n₁)
                    (right p|d₂′) → p|d₂′

      in divide-coprime p d₁′ d₂′ d₁′⊥d₂′ p|d₁′ p|d₂′

addQ-sound : ∀ x y → x + y ≡ slowAddQ x y
addQ-sound (ratio n₁ d₁ n₁⊥d₁) (ratio n₂ d₂ n₂⊥d₂)
  with gcd (n₁ * d₂ + n₂ * d₁) (d₁ * d₂) | gcd d₁ d₂
...  | gcd-res g₀ g₀-gcd@(is-gcd (factor p pg₀=n₀) (factor q qg₀=d₀) _)
     | gcd-res g isgcd-dd@(is-gcd (factor! d₁′) (factor! d₂′) _)
  with gcd (n₁ * d₂′ + n₂ * d₁′) g
...  | gcd-res g₁ isgcd-sg@(is-gcd (factor s′ s′g₁=s) (factor! g′) _) =

  let n₀ = n₁ * d₂ + n₂ * d₁
      d₀ = d₁ * d₂
      s  = n₁ * d₂′ + n₂ * d₁′

      instance
        nz-g₀  = nonzero-is-gcd-r ⦃ mul-nonzero d₁ d₂ ⦄ g₀-gcd
        nz-g   = nonzero-is-gcd-l isgcd-dd
        nz-g₁  = nonzero-is-gcd-r isgcd-sg
        nz-gg₁ = mul-nonzero g g₁

      s′gg₁=n₀ : s′ * (g * g₁) ≡ n₀
      s′gg₁=n₀ =
        s′ * (g * g₁)
          ≡⟨ auto ⟩
        s′ * g₁ * g
          ≡⟨ _* g $≡ s′g₁=s ⟩
        (n₁ * d₂′ + n₂ * d₁′) * g
          ≡⟨ auto ⟩
        n₀ ∎

      ddg′gg₁=d₀ : d₁′ * d₂′ * g′ * (g * g₁) ≡ d₀
      ddg′gg₁=d₀ = auto

      s′⊥ddg : Coprime s′ (d₁′ * d₂′ * g′)
      s′⊥ddg =
        let[ _ := is-gcd-factors-coprime isgcd-dd ]
        let[ _ := lem-coprime n₁ n₂ s′ d₁′ d₂′ g g₁ s′g₁=s n₁⊥d₁ auto-coprime ]
        let[ _ := lem-coprime n₂ n₁ s′ d₂′ d₁′ g g₁ (s′g₁=s ⟨≡⟩ auto) n₂⊥d₂ auto-coprime ]
        let[ _ := is-gcd-factors-coprime isgcd-sg ]
        auto-coprime

      gg₁-gcd : IsGCD (g * g₁) n₀ d₀
      gg₁-gcd = is-gcd-by-coprime-factors (g * g₁) n₀ d₀
                  (factor s′ s′gg₁=n₀) (factor (d₁′ * d₂′ * g′) ddg′gg₁=d₀)
                  s′⊥ddg

      gg₁=g₀ : g * g₁ ≡ g₀
      gg₁=g₀ = is-gcd-unique (g * g₁) g₀ gg₁-gcd g₀-gcd

      s′g₀=n₀ : s′ * g₀ ≡ n₀
      s′g₀=n₀ = s′ *_ $≡ sym gg₁=g₀ ⟨≡⟩ s′gg₁=n₀

      ddgg₀=d₀ : d₁′ * d₂′ * g′ * g₀ ≡ d₀
      ddgg₀=d₀ = d₁′ * d₂′ * g′ *_ $≡ sym gg₁=g₀ ⟨≡⟩ ddg′gg₁=d₀

      s′=p : s′ ≡ p
      s′=p = mul-inj₁ s′ p g₀ (s′g₀=n₀ ⟨≡⟩ʳ pg₀=n₀)

      ddg=q : d₁′ * d₂′ * g′ ≡ q
      ddg=q = mul-inj₁ _ q g₀ (ddgg₀=d₀ ⟨≡⟩ʳ qg₀=d₀)

    in cong-ratio s′=p ddg=q

mulQ-sound : ∀ x y → x * y ≡ slowMulQ x y
mulQ-sound (ratio n₁ d₁ n₁⊥d₁) (ratio n₂ d₂ n₂⊥d₂)
  with gcd n₁ d₂ | gcd n₂ d₁ | gcd (n₁ * n₂) (d₁ * d₂)
... | gcd-res g₁ gcd₁₂@(is-gcd (factor! n₁′) (factor! d₂′) _)
    | gcd-res g₂ gcd₂₁@(is-gcd (factor! n₂′) (factor! d₁′) _)
    | gcd-res g  gcdnd@(is-gcd (factor n′ n′g=n) (factor d′ d′g=d) _) =
  let instance _ = nonzero-is-gcd-r gcd₁₂
               _ = nonzero-is-gcd-r gcd₂₁
               _ = mul-nonzero g₁ g₂
      g=gg : g ≡ g₁ * g₂
      g=gg = is-gcd-unique _ _ gcdnd $
               is-gcd-by-coprime-factors _ _ _ (factor (n₁′ * n₂′) auto)
                                               (factor (d₁′ * d₂′) auto) $
                 let[ _ := is-gcd-factors-coprime gcd₁₂ ]
                 let[ _ := is-gcd-factors-coprime gcd₂₁ ]
                 auto-coprime
      neq : n₁′ * n₂′ ≡ n′
      neq = case g=gg of λ where
              refl → mul-inj₁ (n₁′ * n₂′) n′ (g₁ * g₂) (by n′g=n)
      deq : d₁′ * d₂′ ≡ d′
      deq = case g=gg of λ where
              refl → mul-inj₁ (d₁′ * d₂′) d′ (g₁ * g₂) (by d′g=d)
  in cong-ratio neq deq

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
-- BEGIN prelude.agda

-- the Haskell $ and .

($) (A::Set) (B::Set) (f :: A -> B) (a :: A) :: B
  = f a

compose (B,C,A::Set)(f :: B -> C)(g :: A -> B) :: A -> C
  = \ (x::A) -> f (g x)

{- hardwired into Agda

Integer :: Set
  = ?

Bool :: Set
  = data True | False

-}

not (b::Bool) :: Bool
  = case b of {
      (True) -> False;  -- Agda does not require @_ for built-in constructors
      (False) -> True;}

(||) (b1::Bool)(b2::Bool) :: Bool
  = case b1 of {
      (True) -> True@_;
      (False) ->
        case b2 of {
          (True) -> True@_;
          (False) -> False@_;};}

(&&) (b1::Bool)(b2::Bool) :: Bool
  = case b1 of {
      (True) ->
        case b2 of {
          (True) -> False@_;
          (False) -> True@_;};
      (False) -> False@_;}

Pair (a::Set)(b::Set) :: Set
  = data Pair (x::a) (y::b)

Triple (a::Set)(b::Set)(c::Set) :: Set
  = data Triple (x::a) (y::b) (z::c)

flip (a::Set)(b::Set)(c::Set)(f::a -> b -> c)(x::b)(y::a) :: c
  = f y x

{- hardwired into Agda:

List (a::Set) :: Set
  = data Nil | (:) (x::a) (xs::List a)

-}

foldl (a::Set)(b::Set)(f::a -> b -> a)(acc::a)(l::List b) :: a
  = case l of {
      (Nil) -> acc;
      (x:xs) -> foldl a b f (f acc x) xs;}

reverse (a::Set)(l::List a) :: List a
  = foldl (List a) a
      (flip a (List a) (List a) (\(h::a) -> \(h'::List a) -> (:)@_ h h'))
      Nil@_
      l

append (a::Set)(l1::List a)(l2::List a) :: List a
  = case l1 of {
      (Nil) -> l2;
      (x:xs) -> x : (append a xs l2);}

null (a::Set)(l::List a) :: Bool
  = case l of {
      (Nil) -> True@_;
      (x:xs) -> False@_;}

map (a,b::Set)(f::a -> b)(l::List a) :: List b
  = case l of
       (Nil)  -> Nil
       (x:xs) -> f x : map a b f xs

Maybe (a::Set) :: Set
  = data Nothing | Just (x::a)

-- Should not be here - temporary addition to provide an "interesting" type
-- data Simple = A | B | C  -gone

-- Properties
-- naive implementation of Property.hs

-- from SET.alfa
Rel (X::Set) :: Type
  = X -> X -> Set
Id (X::Set) :: Rel X
  = idata ref (x::X) :: _ x x
Zero :: Set
  = data
whenZero (X::Set)(z::Zero) :: X
  = case z of { }
Unit :: Set
  = data tt
Sum (X::Set)(Y::X -> Set) :: Set
  = sig{fst :: X;
        snd :: Y fst;}
Plus (X::Set)(Y::Set) :: Set
  = data inl (x::X) | inr (y::Y)

package Property where

  Prop :: Type
    = Set

  (===) (A :: Set) (a :: A) (b :: A) :: Prop
    = Id A a b

  -- translate forAll into a dependent function type
  forAll (A :: Set) (f :: A -> Prop) :: Prop
    = (x :: A) -> f x

  exists (A :: Set) (f :: A -> Prop) :: Prop
    = sig { witness :: A;
            prop    :: f witness; }

  (/\) (A,B :: Prop) :: Prop
    = Sum A (\(a::A) -> B)

  (\/) (A,B :: Prop) :: Prop
    = Plus A B

  (<=>) (A,B :: Prop) :: Prop
    =  (A -> B) /\ (B -> A)

  (==>) (A,B :: Prop) :: Prop
    =  (A -> B)

  true :: Prop
    = Unit

  false :: Prop
    = Zero

  nt (A :: Prop) :: Prop
    =  A -> false

  -- cannot do the naive using because of universe conflict
  -- List cannot have a parameter which is not a set, and Prop is a type
  --using (L :: List Prop) (A :: Prop) :: Prop
  --  = A

  holds (b::Bool) :: Prop
    = if b then true else false

  holdsNot (b::Bool) :: Prop
    = if b then false else true

-- Class of inhabited types

class Inhabited (a::Set) :: Set exports
  arbitrary :: a

error (a::Set)(|ia::Inhabited a)(msg::String) :: a
  = arbitrary

-- Prelude types are inhabited

instance iBool :: Inhabited Bool where
  arbitrary = True

instance iString :: Inhabited String where
  arbitrary = "I AM ARBITRARY"

instance iInteger :: Inhabited Integer where
  arbitrary = 123456789

{- Syntax error:
instance iRational :: Inhabited Rational where
  arbitrary = 0.123456789
-}

instance iList (|a::Set) :: Inhabited (List a) where
  arbitrary = Nil
-- instance iList (a::Set)(ia::Inhabited a)  :: Inhabited (List a) where

-- END prelude.agda

max_issues_repo_name: siddharthist/CoverTranslator


text:
------------------------------------------------------------------------------
-- Addition as a function constant
------------------------------------------------------------------------------

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

module FOTC.AddConstant where

------------------------------------------------------------------------------
-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Algebra.agda and Relation/Binary/Core.agda).
infixl 9 _·_
infix  7 _≡_

postulate
  D                      : Set
  _·_                    : D → D → D
  true false if          : D
  zero succ pred iszero  : D
  _≡_                    : D → D → Set

postulate
  if-true  : ∀ t {t'} → if · true  · t · t' ≡ t
  if-false : ∀ {t} t' → if · false · t · t' ≡ t'
  pred-0   : pred · zero ≡ zero
  pred-S   : ∀ n → pred · (succ · n) ≡ n
  iszero-0 : iszero · zero ≡ true
  iszero-S : ∀ n → iszero · (succ · n) ≡ false
{-# ATP axioms if-true if-false pred-0 pred-S iszero-0 iszero-S #-}

postulate
  +    : D
  +-eq : ∀ m n → + · m · n ≡
         if · (iszero · m) · n · (succ · (+ · (pred · m) · n))
{-# ATP axiom +-eq #-}

postulate
  +-0x : ∀ n → + · zero · n ≡ n
  +-Sx : ∀ m n → + · (succ · m) · n ≡ succ · (+ · m · n)
{-# ATP prove +-0x #-}
{-# ATP prove +-Sx #-}

-- $ cd fotc/notes/thesis
-- $ agda -i. -i ~/fot FOTC/AddConstant.agda
-- $ apia -i. -i ~/fot FOTC/AddConstant.agda
-- Proving the conjecture in /tmp/FOTC/AddConstant/37-43-0x.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture
-- Proving the conjecture in /tmp/FOTC/AddConstant/38-43-Sx.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module sv20.assign2.SetTheory.Algebra where

open import sv20.assign2.SetTheory.Subset
open import sv20.assign2.SetTheory.Logic
open import sv20.assign2.SetTheory.ZAxioms

infix 6 _∪_
infix 6 _-_
infix 6 _∩_

-- Properties involving operations between sets, algebra of sets.

-- In this module some properties involving union, difference
-- and intersection of set are proved.

-- First, some properties of the union between sets, justified by the
-- union axiom.

_∪_ : 𝓢 → 𝓢 → 𝓢
x ∪ y = proj₁ (union x y)
-- {-# ATP definition _∪_ #-}

-- Theorem 20, p. 27 (Suppes 1960)
∪-d : (x y : 𝓢) → ∀ {z} → z ∈ x ∪ y ⇔ z ∈ x ∨ z ∈ y
∪-d x y = proj₂ _ (union x y)

-- ∧-projections of past theorem for convenience.
∪-d₁ : (A B : 𝓢) → ∀ {x} → x ∈ (A ∪ B) → x ∈ A ∨ x ∈ B
∪-d₁ A B = ∧-proj₁ (∪-d A B)

∪-d₂ : (A B : 𝓢) → ∀ {x} → x ∈ A ∨ x ∈ B → x ∈ (A ∪ B)
∪-d₂ A B = ∧-proj₂ (∪-d A B)

-- Theorem 21, p. 27 (Suppes 1960)
A∪B≡B∪A : (A B : 𝓢) → A ∪ B ≡ B ∪ A
A∪B≡B∪A A B = equalitySubset (A ∪ B) (B ∪ A) (p₁ , p₂)
  where
  p₁ : (x : 𝓢) → x ∈ (A ∪ B) → x ∈ (B ∪ A)
  p₁ x x₁ = ∪-d₂ B A (∨-sym _ _ (∪-d₁ A B x₁))

  p₂ : (x : 𝓢) → x ∈ (B ∪ A) → x ∈ (A ∪ B)
  p₂ x x₁ = ∪-d₂ A B (∨-sym _ _ (∪-d₁ B A x₁))

-- Theorem 23, p. 27 (Suppes 1960)
A∪A≡A : (A : 𝓢) → A ∪ A ≡ A
A∪A≡A A = equalitySubset (A ∪ A) A (p₁ , p₂)
  where
  p₁ : (x :  𝓢) → x ∈ (A ∪ A) → x ∈ A
  p₁ x x₁ = ∨-idem _ (∪-d₁ A A x₁)

  p₂ : (x : 𝓢) → x ∈ A → x ∈ (A ∪ A)
  p₂ x x₁ = ∪-d₂ A A (inj₁ x₁)

-- Theorem 25, p. 27 (Suppes 1960)
∪-prop : (A B : 𝓢) → A ⊆ A ∪ B
∪-prop A B t x = ∪-d₂ _ _ (inj₁ x)

⊆∪ : (x A B : 𝓢) → x ⊆ A ∧ x ⊆ B → x ⊆ A ∪ B
⊆∪ x A B (x₁ , x₂) t x₃ = trans-⊆ _ _ _ (x₁ , (∪-prop _ _)) _ x₃

∪-prop₂ : (x A B : 𝓢) → x ⊆ A ∨ x ⊆ B → x ⊆ A ∪ B
∪-prop₂ x A B (inj₁ x₁) t x₂ = ∪-d₂ _ _ (inj₁ (x₁ _ x₂))
∪-prop₂ x A B (inj₂ x₁) t x₂ = ∪-d₂ _ _ (inj₂ (x₁ _ x₂))

∪-prop₃ : (A B : 𝓢) → B ⊆ A ∪ B
∪-prop₃ A B t x = ∪-d₂ _ _ (inj₂ x)

-- Theorem 27, p. 27 (Suppes 1960)
∪-prop₄ : (x y A : 𝓢) → x ⊆ A → y ⊆ A → x ∪ y ⊆ A
∪-prop₄ x y A x⊆A y⊆A t t∈x∪y = ∨-idem _ p₂
  where
  p₁ : t ∈ x ∨ t ∈ y
  p₁ = ∪-d₁ _ _ t∈x∪y

  p₂ : t ∈ A ∨ t ∈ A
  p₂ = ∨-prop₅ p₁ (x⊆A _) (y⊆A _)

-- Properties about the intersection opertaion. Its existence is justified
-- as an axiom derived from the sub axiom schema.

_∩_ : 𝓢 → 𝓢 → 𝓢
x ∩ y = proj₁ (sub (λ z → z ∈ y) x)

-- Instantiation of the subset axiom schema needed for justifiying
-- the operation.
sub₂ : (x y : 𝓢) → ∃ (λ B → {z : 𝓢} → (z ∈ B ⇔ z ∈ x ∧ z ∈ y))
sub₂ x y = sub (λ z → z ∈ y) x

-- Theorem 12, p.25 (Suppes 1960)
∩-def : (x y : 𝓢) → ∀ {z} → z ∈ x ∩ y ⇔ z ∈ x ∧ z ∈ y
∩-def x y = proj₂ _ (sub₂ x y)

-- Projections of ∩-def, useful for avoiding repeating this
-- projections later.
∩-d₁ : (x A B : 𝓢)  → x ∈ (A ∩ B) → x ∈ A ∧ x ∈ B
∩-d₁ x A B = ∧-proj₁ (∩-def A B)

∩-d₂ : (x A B : 𝓢) → x ∈ A ∧ x ∈ B → x ∈ (A ∩ B)
∩-d₂ x A B = ∧-proj₂ (∩-def A B)

-- Theorem 13, p.26 (Suppes 1960)
∩-sym : (A B : 𝓢) → A ∩ B ≡ B ∩ A
∩-sym A B = equalitySubset (A ∩ B) (B ∩ A) (p₁ , p₂)
  where
  p₁ : (x : 𝓢) → x ∈ A ∩ B → x ∈ B ∩ A
  p₁ x x∈A∩B = ∩-d₂ x B A (x∈B , x∈A)
    where
    x∈A : x ∈ A
    x∈A = ∧-proj₁ (∩-d₁ x A B x∈A∩B)

    x∈B : x ∈ B
    x∈B = ∧-proj₂ (∩-d₁ x A B x∈A∩B)
  p₂ : (x :  𝓢) → x ∈ B ∩ A → x ∈ A ∩ B
  p₂ x x∈B∩A = ∩-d₂ x A B (x∈A , x∈B)
    where
    x∈A : x ∈ A
    x∈A = ∧-proj₂ (∩-d₁ x B A x∈B∩A)

    x∈B : x ∈ B
    x∈B = ∧-proj₁ (∩-d₁ x B A x∈B∩A)

-- Theorem 14, p. 26 (Suppes 1960).
∩-dist : (A B C : 𝓢) → (A ∩ B) ∩ C ≡ A ∩ (B ∩ C)
∩-dist A B C = equalitySubset ((A ∩ B) ∩ C) (A ∩ (B ∩ C)) (p₁ , p₂)
  where
  p₁ : (x : 𝓢) → x ∈ (A ∩ B) ∩ C → x ∈ A ∩ (B ∩ C)
  p₁ x x₁ = ∩-d₂ x A (B ∩ C) (x∈A , x∈B∩C)
    where
    x∈B∩C : x ∈ B ∩ C
    x∈B∩C = ∩-d₂ x B C (x∈B , x∈C)
      where
      x∈A∩B : x ∈ A ∩ B
      x∈A∩B = ∧-proj₁ (∩-d₁ x (A ∩ B) _ x₁)

      x∈B : x ∈ B
      x∈B = ∧-proj₂ (∩-d₁ x _ B x∈A∩B)

      x∈C : x ∈ C
      x∈C = ∧-proj₂ (∩-d₁ x _ C x₁)
    x∈A : x ∈ A
    x∈A = ∧-proj₁ (∩-d₁ x A _ x∈A∩B)
      where
      x∈A∩B : x ∈ A ∩ B
      x∈A∩B = ∧-proj₁ (∩-d₁ x (A ∩ B) _ x₁)
  p₂ : (x : 𝓢) → x ∈ A ∩ (B ∩ C) → x ∈ (A ∩ B) ∩ C
  p₂ x x₁ = ∩-d₂ x (A ∩ B) C (x∈A∩B , x∈C)
    where
    x∈A∩B : x ∈ A ∩ B
    x∈A∩B = ∩-d₂ x A B (x∈A , x∈B)
      where
      x∈A : x ∈ A
      x∈A = ∧-proj₁ (∩-d₁ x A _ x₁)

      x∈B∩C : x ∈ B ∩ C
      x∈B∩C = ∧-proj₂ (∩-d₁ x _ (B ∩ C) x₁)

      x∈B : x ∈ B
      x∈B = ∧-proj₁ (∩-d₁ x B _ x∈B∩C)
    x∈C : x ∈ C
    x∈C = ∧-proj₂ (∩-d₁ x _ C x∈B∩C)
      where
      x∈B∩C : x ∈ B ∩ C
      x∈B∩C = ∧-proj₂ (∩-d₁ x _ (B ∩ C) x₁)

-- Theorem 15, p. 26 (Suppes).
∩-itself : (A : 𝓢) → A ∩ A ≡ A
∩-itself A = equalitySubset (A ∩ A) A (p₁ , p₂)
  where
  p₁ : (x : 𝓢) → x ∈ A ∩ A → x ∈ A
  p₁ x x₁ = ∧-proj₁ (∩-d₁ _ A _ x₁)

  p₂ : (x :  𝓢) → x ∈ A → x ∈ A ∩ A
  p₂ x x₁ = ∩-d₂ _ A A (x₁ , x₁)

-- Theorem 17, p. 26 (Suppes 1960).
A∩B⊆A : (A B : 𝓢) → A ∩ B ⊆ A
A∩B⊆A A B _ p = ∧-proj₁ (∩-d₁ _ A _ p)

-- Properties involving the difference between sets. The existence of this
-- sets is also justified as an instance of the subset axiom schema.

-- Instantiation of the subset schema that will justify the operation
-- of difference between sets.
sub₃ : (x y : 𝓢) → ∃ (λ B → {z : 𝓢} → (z ∈ B ⇔ z ∈ x ∧ z ∉ y))
sub₃ x y = sub (λ z → z ∉ y) x

_-_ : 𝓢 → 𝓢 → 𝓢
x - y = proj₁ (sub₃ x y)

-- Theorem 31, p.28 (Suppes 1960).
dif-def : (x y : 𝓢) → ∀ {z} → z ∈ (x - y) ⇔ z ∈ x ∧ z ∉ y
dif-def x y = proj₂ _ (sub₃ x y)

-- Again both ∧-projections of the past theorem.
dif-d₁ : (A B z : 𝓢) → z ∈ A - B → z ∈ A ∧ z ∉ B
dif-d₁ A B z = ∧-proj₁ (dif-def A B)

dif-d₂ : (A B z : 𝓢) → z ∈ A ∧ z ∉ B → z ∈ A - B
dif-d₂ A B z = ∧-proj₂ (dif-def A B)

-- Theorem 33, p. 29 (Suppes 1960).
∩- : (A B : 𝓢) → A ∩ (A - B) ≡ A - B
∩- A B = equalitySubset (A ∩ (A - B)) (A - B) (p₁ , p₂)
  where
  p₁ : (x : 𝓢) → x ∈ A ∩ (A - B) → x ∈ A - B
  p₁ x x∈∩- = dif-d₂ A B x (x∈A , x∉B)
    where
    x∈A : x ∈ A
    x∈A = ∧-proj₁ (∩-d₁ x A _ x∈∩-)

    x∈A-B : x ∈ A - B
    x∈A-B = ∧-proj₂ (∩-d₁ x _ (A - B) x∈∩-)

    x∉B : x ∉ B
    x∉B = ∧-proj₂ (dif-d₁ A B x x∈A-B)
  p₂ : (x : 𝓢) → x ∈ A - B → x ∈ A ∩ (A - B)
  p₂ x x∈A-B = ∩-d₂ x A (A - B) ((∧-proj₁ (dif-d₁ A B x x∈A-B)) , x∈A-B)

-- References
--
-- Suppes, Patrick (1960). Axiomatic Set Theory.
-- The University Series in Undergraduate Mathematics.
-- D. Van Nostrand Company, inc.
--
-- Enderton, Herbert B. (1977). Elements of Set Theory.
-- Academic Press Inc.


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

open import Level
  using (_⊔_; Lift; lift; lower)
  public

infix  1 _≡_
infixr 1 _⊎_
infixr 2 _×_
infix  3 ¬_
infixr 4 _,_
infixr 9 _∘_

-- The negative fragment.
Π : ∀ {a b} (A : Set a) → (A → Set b) → Set _
Π A B = (x : A) → B x

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁

open Σ public
-- Projections are defined automatically.

_×_ : ∀ {a b} → Set a → Set b → Set _
A × B = Σ A λ _ → B

-- Unit type with definitional η.
record ⊤ : Set where
  constructor tt

id : ∀ {a} {A : Set a} → A → A
id x = x

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

-- The positive fragment.
data ⊥ : Set where

-- Ex falso quodlibet.
0-elim : ∀ {p} {P : Set p} → ⊥ → P
0-elim ()

¬_ : ∀ {a} → Set a → Set a
¬ A = A → ⊥

-- Unit type without definitional η.
data Unit : Set where
  tt : Unit

1-elim : ∀ {p} (P : Unit → Set p) → P tt →
  ∀ z → P z
1-elim P c tt = c

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

-- Case analysis.
case : ∀ {a b p} {A : Set a} {B : Set b} (P : A ⊎ B → Set p)
  (f : ∀ a → P (inl a)) (g : ∀ b → P (inr b)) → ∀ z → P z
case P f g (inl a) = f a
case P f g (inr b) = g b

-- Simga as a positive type.
data Σ′ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  _,_ : (a : A) → B a → Σ′ A B

split : ∀ {a b p} {A : Set a} {B : A → Set b} (P : Σ′ A B → Set p)
  (f : (a : A) (b : B a) → P (a , b)) → ∀ z → P z
split P f (a , b) = f a b

-- Natural numbers.
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

ind : ∀ {p} (P : ℕ → Set p)
  (s : ∀ n → P n → P (suc n))
  (z : P zero) →
  ∀ z → P z
ind P s z zero    = z
ind P s z (suc n) = s n (ind P s z n)

-- Identity type.
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

-- When the type cannot be infered.
Id : ∀ {a} (A : Set a) (x y : A) → Set _
Id _ x y = x ≡ y

-- Path induction.
J : ∀ {a p} {A : Set a} (P : ∀ (x : A) y → x ≡ y → Set p)
  (f : ∀ x → P x x refl) → ∀ x y → (p : x ≡ y) → P x y p
J P f x .x refl = f x

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
-- notes-04-thursday.agda

open import mylib

{-
  Infinite datastructure
  - streams, Stream A
  0 ,1 , 2 ,3 ,4, ... : Stream ℕ
  1, 1 , 2, 3 ,5 ,..
  2, 3, 5, 7, 11,..

  duality, categorical mirror
  _×_ (products) and _⊎_ (coproducts, sums)

  Inductive datatypes: finite datastructures
  Coinductive datatypes: Streams, ℕ∞ (conatural numbers)
-}

record Stream (A : Set) : Set where
  constructor _∷_
  coinductive
  field
    head : A
    tail : Stream A

open Stream

{-
  _∷S_ : A → Stream A → Stream A
  head (a ∷S as) = a
  tail (a ∷S as) = as
-}

from : ℕ → Stream ℕ
head (from n) = n
tail (from n) = from (suc n)

-- from is productive because it is guarded

mapS : (A → B) → Stream A → Stream B
head (mapS f as) = f (head as)
tail (mapS f as) = mapS f (tail as)

{-
  filterS : (A → Bool) → Stream A → Stream A
  head (filterS f as) = if f (head as) then (head as) else {!!}
  tail (filterS f as) = {!!} -- no guarded definition of filter
-}

-- Conatural numbers

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

-- Maybe A = 1 ⊎ A

pred : ℕ → Maybe ℕ
pred zero = nothing
pred (suc n) = just n

zero-suc : Maybe ℕ → ℕ
zero-suc nothing = zero
zero-suc (just n) = suc n
-- Lambek's lemma, initial algebras

record ℕ∞ : Set where
  coinductive
  field
    pred∞ : Maybe ℕ∞
-- terminal coalgebra

-- emb : ℕ → ℕ∞ -- 2 ways
-- f : ℕ∞ → ℕ -- no way, cons local continuity

open ℕ∞

zero∞ : ℕ∞
pred∞ zero∞ = nothing

suc∞ : ℕ∞ → ℕ∞
pred∞ (suc∞ n) = just n

∞ : ℕ∞
pred∞ ∞ = just ∞

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

_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
pred∞ (m +∞ n) with pred∞ m
... | nothing = pred∞ n
... | just m' = just (m' +∞ n)

{-
  Dependent types (families)
  A dependent type is a function whose codomain is Set.
  List : Set → Set
  Not proper?

  Vec : Set → ℕ → Set
  Vec A n = tuple of n as
  { as | length as = n} -- type theoretic of comprehension

  Fin : ℕ → Set
  Fin n = a set with n elements
  {0 , 1, .. , n-1}

  Function type
  A B : Set
  A → B : Set

  Dependent function type (Π-type)
  A : Set
  B : A → Set

  (x : A) → B x
  {x : A} → B x -- hidden arguments

  zeros : (n : ℕ) → Vec ℕ n

-}

data Vec (A : Set) : ℕ → Set where
  [] : Vec A 0
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

zeros : (n : ℕ) → Vec ℕ n
zeros zero = []
zeros (suc n) = 0 ∷ zeros n

{-
_++_ : List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
-}

_++v_ : {m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
[] ++v ys = ys
(x ∷ xs) ++v ys = x ∷ (xs ++v ys)

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} → Fin n → Fin (suc n)

{-
  Fin 0 = {}
  Fin 1 = { zero{0} }
  Fin 2 = { zero{1} , suc{1} (zero{0}) }
  ...
-}

_!!_ : {n : ℕ} → Vec A n → Fin n → A -- safe lookup function
(a ∷ as) !! zero = a
(a ∷ as) !! suc n = as !! n

max_stars_repo_path: Type Theory/notes-04-thursday.agda

max_issues_repo_path: Type Theory/notes-04-thursday.agda

max_forks_repo_path: Type Theory/notes-04-thursday.agda


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Pointed

module lib.types.Span where

record Span {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor span
  field
    A : Type i
    B : Type j
    C : Type k
    f : C → A
    g : C → B

private
  span=-raw : ∀ {i j k} {A A' : Type i} (p : A == A')
    {B B' : Type j} (q : B == B') {C C' : Type k} (r : C == C')
    {f : C → A} {f' : C' → A'}
    (s : f == f' [ (λ CA → fst CA → snd CA) ↓ pair×= r p ])
    {g : C → B} {g' : C' → B'}
    (t : g == g' [ (λ CB → fst CB → snd CB) ↓ pair×= r q ])
    → (span A B C f g) == (span A' B' C' f' g')
  span=-raw idp idp idp idp idp = idp

abstract
  span= : ∀ {i j k} {A A' : Type i} (p : A ≃ A')
    {B B' : Type j} (q : B ≃ B') {C C' : Type k} (r : C ≃ C')
    {f : C → A} {f' : C' → A'} (s : (a : C) → (–> p) (f a) == f' (–> r a))
    {g : C → B} {g' : C' → B'} (t : (b : C) → (–> q) (g b) == g' (–> r b))
    → (span A B C f g) == (span A' B' C' f' g')
  span= p q r {f} {f'} s {g} {g'} t = span=-raw
    (ua p)
    (ua q)
    (ua r)
    (↓-→-in (λ α → ↓-snd×-in (ua r) (ua p) (↓-idf-ua-in p (
                   s _
                   ∙ ap f' (↓-idf-ua-out r (↓-fst×-out (ua r) (ua p) α))))))
    (↓-→-in (λ β → ↓-snd×-in (ua r) (ua q) (↓-idf-ua-in q (
                   t _
                   ∙ ap g' (↓-idf-ua-out r (↓-fst×-out (ua r) (ua q) β))))))

record ⊙Span {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor ⊙span
  field
    X : Ptd i
    Y : Ptd j
    Z : Ptd k
    f : fst (Z ⊙→ X)
    g : fst (Z ⊙→ Y)

⊙span-out : ∀ {i j k} → ⊙Span {i} {j} {k} → Span {i} {j} {k}
⊙span-out (⊙span X Y Z f g) = span (fst X) (fst Y) (fst Z) (fst f) (fst g)

{- Helper for path induction on pointed spans -}
⊙span-J : ∀ {i j k l} (P : ⊙Span {i} {j} {k} → Type l)
  → ({A : Type i} {B : Type j} {Z : Ptd k} (f : fst Z → A) (g : fst Z → B)
     → P (⊙span (A , f (snd Z)) (B , g (snd Z)) Z (f , idp) (g , idp)))
  → Π ⊙Span P
⊙span-J P t (⊙span (A , ._) (B , ._) Z (f , idp) (g , idp)) = t f g

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Data.Real.Order where

open import Assume
open import Data.Real.Base
open import Data.Bool using (T; T?)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Binary

open import Level using (0ℓ)

-- TODO
-- should this move to Data.Real.Equality?
_≉_ : Rel ℝ 0ℓ
x ≉ y = ¬ x ≈ y

≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_
≉-isApartnessRelation = assume

≉-apartnessRelation : ApartnessRelation 0ℓ 0ℓ 0ℓ
≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }

_≤_ : ℝ → ℝ → Set
x ≤ y = T (x ≤ᵇ y)

open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ public
  using (_<_; <-isStrictTotalOrder₁)

_≤?_ : ∀ x y → Dec (x ≤ y)
x ≤? y = T? (x ≤ᵇ y)

≤-isTotalOrder : IsTotalOrder _≈_ _≤_
≤-isTotalOrder = assume

≤-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_
≤-isDecTotalOrder = record { isTotalOrder = ≤-isTotalOrder ; _≟_ = _≈?_ ; _≤?_ = _≤?_ }

≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record { isDecTotalOrder = ≤-isDecTotalOrder }

<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder = <-isStrictTotalOrder₁ _≈?_ ≤-isTotalOrder

abs : ℝ → ℝ
abs x = if does (0.0 ≤? x) then x else - x
  where
    open import Data.Bool using (if_then_else_)
    open import Relation.Nullary using (does)

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
------------------------------------------------------------------------
-- Various definitions of "true infinitely often", and some proofs
-- showing that this property commutes with binary sums (in the
-- double-negation monad, and sometimes with extra assumptions)
------------------------------------------------------------------------

module InfinitelyOften where

open import Algebra
open import Axiom.ExcludedMiddle
open import Category.Monad
open import Codata.Musical.Notation
open import Data.Empty
open import Data.Nat
import Data.Nat.Properties as NatProp
open import Data.Product as Prod hiding (map)
open import Data.Sum hiding (map)
open import Data.Unit using (tt)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
import Function.Related as Related
open import Level using (Lift; lift; lower)
open import Relation.Binary hiding (_⇒_; _⇔_)
open import Relation.Nullary
open import Relation.Nullary.Negation
import Relation.Nullary.Universe as Univ
open import Relation.Unary hiding (_⇒_)
private
  open module M {f} = RawMonad {f = f} ¬¬-Monad
  module NatOrder   = DecTotalOrder NatProp.≤-decTotalOrder
  module NatLattice = DistributiveLattice
                        NatProp.⊓-⊔-distributiveLattice

------------------------------------------------------------------------
-- Above

module Above where

  -- P Above i holds if P holds somewhere above i (perhaps at i
  -- itself).

  infix 4 _Above_

  _Above_ : (ℕ → Set) → (ℕ → Set)
  P Above i = ∃ λ j → i ≤ j × P j

  -- Conversion lemma.

  move-suc : ∀ {P i} → P Above suc i ⇔ (P ∘ suc) Above i
  move-suc {P} {i} = equivalence ⇒ ⇐
    where
    ⇒ : P Above suc i → (P ∘ suc) Above i
    ⇒ (.(1 + j) , s≤s {n = j} i≤j , P[1+j]) = (j , i≤j , P[1+j])

    ⇐ : (P ∘ suc) Above i → P Above suc i
    ⇐ (j , i≤j , P[1+j]) = (1 + j , s≤s i≤j , P[1+j])

  -- A closure lemma.

  stable-up :
    ∀ {P} →
    (∀ i → Stable (P Above i)) → (∀ i → Stable ((P ∘ suc) Above i))
  stable-up stable i ¬¬P∘suc⇑i =
    Equivalence.to move-suc ⟨$⟩
      stable (1 + i) (_⟨$⟩_ (Equivalence.from move-suc) <$> ¬¬P∘suc⇑i)

------------------------------------------------------------------------
-- Has upper bound

module Has-upper-bound where

  open Above using (_Above_)

  -- P Has-upper-bound i means that P does not hold for any j ≥ i.

  infix 4 _Has-upper-bound_

  _Has-upper-bound_ : (ℕ → Set) → (ℕ → Set)
  P Has-upper-bound i = ∀ j → i ≤ j → ¬ P j

  -- A closure lemma.

  up : ∀ {P i} → P Has-upper-bound i → (P ∘ suc) Has-upper-bound i
  up ¬p = λ j i≤j → ¬p (suc j) (NatProp.≤-step i≤j)

  -- A conversion lemma.

  move-suc : ∀ {P i} →
             P Has-upper-bound suc i ⇔ (P ∘ suc) Has-upper-bound i
  move-suc {P} {i} = equivalence ⇒ ⇐
    where
    ⇒ : P Has-upper-bound suc i → (P ∘ suc) Has-upper-bound i
    ⇒ P↯[1+i] j i≤j P[1+j] = P↯[1+i] (1 + j) (s≤s i≤j) P[1+j]

    ⇐ : (P ∘ suc) Has-upper-bound i → P Has-upper-bound suc i
    ⇐ P∘suc↯i .(1 + j) (s≤s {n = j} i≤j) Pj = P∘suc↯i j i≤j Pj

  -- _Has-upper-bound_ and _Above_ are mutually inconsistent.

  mutually-inconsistent :
    ∀ {P i} → P Has-upper-bound i ⇔ (¬ (P Above i))
  mutually-inconsistent {P} {i} = equivalence ⇒ ⇐
    where
    ⇒ : P Has-upper-bound i → ¬ (P Above i)
    ⇒ P↯i (j , i≤j , Pj) = P↯i j i≤j Pj

    ⇐ : ¬ (P Above i) → P Has-upper-bound i
    ⇐ ¬P⇑i j i≤j Pj = ¬P⇑i (j , i≤j , Pj)

------------------------------------------------------------------------
-- Below

module Below where

  open Above using (_Above_)

  -- P Below i holds if P holds everywhere below i (including at i).

  infix 4 _Below_

  _Below_ : (ℕ → Set) → (ℕ → Set)
  P Below i = ∀ j → j ≤ i → P j

  -- _Below_ P has a comonadic structure (at least if morphism
  -- equality is trivial).

  map : ∀ {P Q} → P ⊆ Q → _Below_ P ⊆ _Below_ Q
  map P⊆Q P⇓i j j≤i = P⊆Q (P⇓i j j≤i)

  counit : ∀ {P} → _Below_ P ⊆ P
  counit P⇓i = P⇓i _ NatOrder.refl

  cojoin : ∀ {P} → _Below_ P ⊆ _Below_ (_Below_ P)
  cojoin P⇓i = λ j j≤i k k≤j → P⇓i _ (NatOrder.trans k≤j j≤i)

  -- _Above_ (_Below_ P) is pointwise equivalent to _Below_ P.

  ⇑⇓⇔⇓ : ∀ {P} i → (_Below_ P) Above i ⇔ P Below i
  ⇑⇓⇔⇓ {P} i = equivalence ⇒ ⇐
    where
    ⇒ : (_Below_ P) Above i → P Below i
    ⇒ (j , i≤j , P⇓j) k k≤i = P⇓j k (NatOrder.trans k≤i i≤j)

    ⇐ : P Below i → (_Below_ P) Above i
    ⇐ P⇓i = (i , NatOrder.refl , P⇓i)

------------------------------------------------------------------------
-- Mixed inductive/coinductive definition of "true infinitely often"

module Mixed where

  open Above using (_Above_)

  -- Inf P means that P is true for infinitely many natural numbers.

  data Inf (P : ℕ → Set) : Set where
    now  : (p : P 0) (inf : ∞ (Inf (P ∘ suc))) → Inf P
    skip :           (inf :    Inf (P ∘ suc) ) → Inf P

  -- Inf commutes with binary sums in the double-negation monad if one
  -- of the predicates satisfies a certain stability condition.

  up : ∀ {P} → Inf P → Inf (P ∘ suc)
  up (now p inf) = ♭ inf
  up (skip  inf) = inf

  filter₁ : ∀ {P Q} → Inf (P ∪ Q) → ¬ ∃ Q → Inf P
  filter₁ (now (inj₁ p) inf) ¬q = now p (♯ filter₁ (♭ inf) (¬q ∘ Prod.map suc id))
  filter₁ (now (inj₂ q) inf) ¬q = ⊥-elim (¬q (0 , q))
  filter₁ (skip         inf) ¬q = skip (filter₁ inf (¬q ∘ Prod.map suc id))

  filter₂ : ∀ {P Q} → (∀ i → Stable (Q Above i)) →
            Inf (P ∪ Q) → ¬ Inf P → Inf Q
  filter₂ {P} {Q} stable p∪q ¬p = helper witness stable p∪q ¬p
    where
    open Related.EquationalReasoning

    witness : ∃ Q
    witness = Prod.map id proj₂ $ stable 0 (
      ¬ (Q Above 0)  ∼⟨ contraposition (Prod.map id (_,_ z≤n)) ⟩
      ¬ ∃ Q          ∼⟨ filter₁ p∪q ⟩
      Inf P          ∼⟨ ¬p ⟩
      ⊥              ∎)

    helper : ∀ {P Q} →
             ∃ Q → (∀ i → Stable (Q Above i)) →
             Inf (P ∪ Q) → ¬ Inf P → Inf Q
    helper (zero  , q) stable p∪q ¬p = now q (♯ filter₂     (Above.stable-up stable) (up p∪q) (¬p ∘ skip))
    helper (suc i , q) stable p∪q ¬p = skip (helper (i , q) (Above.stable-up stable) (up p∪q) (¬p ∘ skip))

  commutes : ∀ {P Q} → (∀ i → Stable (Q Above i)) →
             Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
  commutes stable p∪q =
    call/cc λ ¬[p⊎q] →
    return $ inj₂ $ filter₂ stable p∪q (¬[p⊎q] ∘ inj₁)

------------------------------------------------------------------------
-- Alternative inductive/coinductive definition of "true infinitely
-- often"

module Alternative where

  open Mixed using (now; skip)

  -- Always P means that P holds for every natural number.

  data Always (P : ℕ → Set) : Set where
    now : (p : P 0) (next : ∞ (Always (P ∘ suc))) → Always P

  -- Eventually P means that P holds for some natural number.

  data Eventually (P : ℕ → Set) : Set where
    now   : (p : P 0) → Eventually P
    later : (p : Eventually (P ∘ suc)) → Eventually P

  -- Inf P means that P is true for infinitely many natural numbers.

  Inf : (ℕ → Set) → Set
  Inf P = Always (λ n → Eventually (P ∘ _+_ n))

  -- This definition is equivalent to the previous one.

  up : ∀ P → Inf P → Inf (P ∘ suc)
  up _ (now _ inf) = ♭ inf

  equivalent : ∀ {P} → Inf P ⇔ Mixed.Inf P
  equivalent = equivalence ⇒ ⇐
    where
    ⇒ : ∀ {P} → Inf P → Mixed.Inf P
    ⇒ (now p inf) = ⇒′ p (♭ inf)
      where
      ⇒′ : ∀ {P} → Eventually P → Inf (P ∘ suc) → Mixed.Inf P
      ⇒′     (now   p) inf = now p (♯ ⇒ inf)
      ⇒′ {P} (later p) inf = skip (⇒′ p (up (P ∘ suc) inf))

    ⇐ : ∀ {P} → Mixed.Inf P → Inf P
    ⇐ inf = now (eventually inf) (♯ ⇐ (Mixed.up inf))
      where
      eventually : ∀ {P} → Mixed.Inf P → Eventually P
      eventually (now p _)  = now p
      eventually (skip inf) = later (eventually inf)

------------------------------------------------------------------------
-- Functional/inductive definition of "true infinitely often"

module Functional where

  open Mixed using (now; skip)
  open Above using (_Above_)

  -- Inf P means that P is true for infinitely many natural numbers.

  Inf : (ℕ → Set) → Set
  Inf P = ∀ i → P Above i

  -- This definition is equivalent to the ones above.

  up : ∀ {P} → Inf P → Inf (P ∘ suc)
  up ∀iP⇑i i = Equivalence.to Above.move-suc ⟨$⟩ ∀iP⇑i (suc i)

  equivalent : ∀ {P} → Inf P ⇔ Mixed.Inf P
  equivalent = equivalence ⇒ ⇐
    where
    ⇒ : ∀ {P} → Inf P → Mixed.Inf P
    ⇒ {P} inf with inf 0
    ... | (j , _ , p) = helper inf j p
      where
      helper : ∀ {P} → Inf P → ∀ j → P j → Mixed.Inf P
      helper inf zero    p = now p (♯ ⇒ (up inf))
      helper inf (suc n) p = skip (helper (up inf) n p)

    ⇐ : ∀ {P} → Mixed.Inf P → Inf P
    ⇐ (now p inf) zero    = (0 , z≤n , p)
    ⇐ (skip  inf) zero    = Prod.map suc (Prod.map (const z≤n) id) $ ⇐ inf zero
    ⇐ inf         (suc i) = Prod.map suc (Prod.map s≤s         id) $
                              ⇐ (Mixed.up inf) i

  -- Inf is a functor (at least if morphism equality is trivial).

  map : ∀ {P₁ P₂} → P₁ ⊆ P₂ → Inf P₁ → Inf P₂
  map P₁⊆P₂ inf = λ i → Prod.map id (Prod.map id P₁⊆P₂) (inf i)

------------------------------------------------------------------------
-- Definition of "only true finitely often"

module Fin where

  open Mixed using (now; skip)
  open Has-upper-bound using (_Has-upper-bound_)

  -- Fin P means that P is only true for finitely many natural
  -- numbers.

  Fin : (ℕ → Set) → Set
  Fin P = ∃ λ i → P Has-upper-bound i

  -- Fin implies the negation of Mixed.Inf.

  ⇐ : ∀ {P} → Fin P → ¬ Mixed.Inf P
  ⇐ = uncurry ⇐′
    where
    ⇐′ : ∀ {P} i → P Has-upper-bound i → ¬ Mixed.Inf P
    ⇐′ zero    fin (now p inf) = fin 0 z≤n p
    ⇐′ zero    fin (skip  inf) = ⇐′ zero (λ j i≤j → fin (suc j) z≤n) inf
    ⇐′ (suc i) fin inf         =
      ⇐′ i (Equivalence.to Has-upper-bound.move-suc ⟨$⟩ fin)
         (Mixed.up inf)

  -- The other direction (with a double-negated conclusion) implies
  -- that Mixed.Inf commutes with binary sums (in the double-negation
  -- monad).

  filter : ∀ {P Q} → Mixed.Inf (P ∪ Q) → Fin P → Mixed.Inf Q
  filter inf (i , fin) = filter′ inf i fin
    where
    filter′ : ∀ {P Q} →
              Mixed.Inf (P ∪ Q) →
              ∀ i → P Has-upper-bound i → Mixed.Inf Q
    filter′ (now (inj₁ p) inf) 0       fin = ⊥-elim (fin 0 z≤n p)
    filter′ (now (inj₁ p) inf) (suc i) fin = skip (filter′ (♭ inf) i (Equivalence.to Has-upper-bound.move-suc ⟨$⟩ fin))
    filter′ (now (inj₂ q) inf) i       fin = now q (♯ filter′ (♭ inf) i (Has-upper-bound.up fin))
    filter′ (skip         inf) i       fin = skip (filter′ inf i (Has-upper-bound.up fin))

  commutes : ∀ {P Q} → (¬ Mixed.Inf P → ¬ ¬ Fin P) →
             Mixed.Inf (P ∪ Q) → ¬ ¬ (Mixed.Inf P ⊎ Mixed.Inf Q)
  commutes ⇒ p∪q =
    call/cc               λ ¬[p⊎q] →
    ⇒ (¬[p⊎q] ∘ inj₁) >>= λ fin →
    return $ inj₂ (filter p∪q fin)

  -- Fin is preserved by binary sums.

  ∪-preserves : ∀ {P Q} → Fin P → Fin Q → Fin (P ∪ Q)
  ∪-preserves {P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
    where
    open NatProp.≤-Reasoning

    helper : ∀ k → i ⊔ j ≤ k → ¬ (P ∪ Q) k
    helper k i⊔j≤k (inj₁ p) = ¬p k (begin
      i      ≤⟨ NatProp.m≤m⊔n i j ⟩
      i ⊔ j  ≤⟨ i⊔j≤k ⟩
      k      ∎) p
    helper k i⊔j≤k (inj₂ q) = ¬q k (begin
      j      ≤⟨ NatProp.m≤m⊔n j i ⟩
      j ⊔ i  ≡⟨ NatLattice.∧-comm j i ⟩
      i ⊔ j  ≤⟨ i⊔j≤k ⟩
      k      ∎) q

------------------------------------------------------------------------
-- Double-negation shift lemmas

module Double-negation-shift where

  open Below using (_Below_)

  -- General double-negation shift property.

  DNS : (ℕ → Set) → Set
  DNS P = (∀ i → ¬ ¬ P i) → ¬ ¬ (∀ i → P i)

  -- DNS holds for stable predicates.

  Stable⇒DNS : ∀ {P} → (∀ i → Stable (P i)) → DNS P
  Stable⇒DNS stable ∀¬¬P = λ ¬∀P → ¬∀P (λ i → stable i (∀¬¬P i))

  -- DNS follows from excluded middle.

  EM⇒DNS : ∀ {P} → ExcludedMiddle Level.zero → DNS P
  EM⇒DNS {P} em hyp = return hyp′
    where
    hyp′ : ∀ i → P i
    hyp′ i = decidable-stable em (hyp i)

  -- DNS follows from the double-negation of excluded middle.

  ¬¬EM⇒DNS : ∀ {P} → ¬ ¬ ExcludedMiddle Level.zero → DNS P
  ¬¬EM⇒DNS em hyp =
    ¬¬-map lower (em >>= λ em → ¬¬-map lift (EM⇒DNS em hyp))

  -- DNS respects predicate equivalence.

  respects : ∀ {P₁ P₂} → (∀ i → P₁ i ⇔ P₂ i) → DNS P₁ → DNS P₂
  respects P₁⇔P₂ dns ∀i¬¬P₂i ¬∀iP₂i =
    dns (λ i ¬P₁i → ∀i¬¬P₂i i (λ P₂i →
                      ¬P₁i (Equivalence.from (P₁⇔P₂ i) ⟨$⟩ P₂i)))
        (λ ∀iP₁i → ¬∀iP₂i (λ i → Equivalence.to (P₁⇔P₂ i) ⟨$⟩ ∀iP₁i i))

  -- Double-negation shift property restricted to predicates which are
  -- downwards closed.

  DNS⇓ : (ℕ → Set) → Set
  DNS⇓ P =
    (∀ {i j} → i ≥ j → P i → P j) →
    (∀ i → ¬ ¬ P i) → ¬ ¬ (∀ i → P i)

  -- Certain instances of DNS imply other instances of DNS⇓, and vice
  -- versa.

  DNS⇒DNS⇓ : ∀ {P} → DNS (_Below_ P) → DNS⇓ P
  DNS⇒DNS⇓ {P} shift downwards-closed ∀i¬¬Pi =
    _∘_ Below.counit <$> shift (λ i → unit <$> ∀i¬¬Pi i)
    where
    unit : P ⊆ _Below_ P
    unit Pi j j≤i = downwards-closed j≤i Pi

  -- The following lemma is due to Thierry Coquand (but the proof,
  -- including any inelegance, is due to me).

  DNS⇓⇒DNS : ∀ {P} → DNS⇓ (_Below_ P) → DNS P
  DNS⇓⇒DNS {P} shift ∀¬¬P = _∘_ Below.counit <$> ¬¬∀P⇓
    where
    P⇓-downwards-closed : ∀ {i j} → i ≥ j → P Below i → P Below j
    P⇓-downwards-closed i≥j P⇓i = λ j′ j′≤j →
      P⇓i j′ (NatOrder.trans j′≤j i≥j)

    Q : ℕ → Set
    Q i = ∀ {j} → j ≤′ i → P j

    q-zero : P 0 → Q 0
    q-zero P0 ≤′-refl = P0

    q-suc : ∀ {i} → P (suc i) → Q i → Q (suc i)
    q-suc P1+i Qi ≤′-refl       = P1+i
    q-suc P1+i Qi (≤′-step j≤i) = Qi j≤i

    ∀¬¬Q : ∀ i → ¬ ¬ Q i
    ∀¬¬Q zero    = q-zero <$> ∀¬¬P zero
    ∀¬¬Q (suc i) = q-suc  <$> ∀¬¬P (suc i) ⊛ ∀¬¬Q i

    ∀¬¬P⇓ : ∀ i → ¬ ¬ (P Below i)
    ∀¬¬P⇓ i = (λ Qi j j≤i → Qi (NatProp.≤⇒≤′ j≤i)) <$> ∀¬¬Q i

    ¬¬∀P⇓ : ¬ ¬ (∀ i → P Below i)
    ¬¬∀P⇓ = shift P⇓-downwards-closed ∀¬¬P⇓

------------------------------------------------------------------------
-- "Non-constructive" definition of "true infinitely often"

module NonConstructive where

  open Fin using (Fin)
  open Above using (_Above_)
  open Below using (_Below_)
  open Has-upper-bound using (_Has-upper-bound_)
  open Double-negation-shift using (DNS; DNS⇓)

  -- Inf P means that P is true for infinitely many natural numbers.

  Inf : (ℕ → Set) → Set
  Inf P = ¬ Fin P

  -- Inf commutes with binary sums (in the double-negation monad).

  commutes : ∀ {P Q} → Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
  commutes p∪q =
    call/cc λ ¬[p⊎q] →
    (λ ¬p ¬q → ⊥-elim (p∪q $ Fin.∪-preserves ¬p ¬q))
      <$> ¬[p⊎q] ∘ inj₁ ⊛ ¬[p⊎q] ∘ inj₂

  -- Inf is a functor (at least if morphism equality is trivial).

  map : ∀ {P₁ P₂} → P₁ ⊆ P₂ → Inf P₁ → Inf P₂
  map P₁⊆P₂ ¬fin = λ fin →
    ¬fin (Prod.map id (λ never j i≤j P₁j → never j i≤j (P₁⊆P₂ P₁j)) fin)

  -- If we have a constructive proof of "true infinitely often", then
  -- we get a "non-constructive" proof as well.

  ⇒ : ∀ {P} → Functional.Inf P → Inf P
  ⇒ inf (i , fin) with inf i
  ... | (j , i≤j , p) = fin j i≤j p

  -- The other direction can be proved iff we have a double-negation
  -- shift lemma.

  Other-direction : (ℕ → Set) → Set
  Other-direction P = Inf P → ¬ ¬ Functional.Inf P

  equivalent₁ : ∀ {P} → Other-direction P ⇔ DNS (_Above_ P)
  equivalent₁ = equivalence ⇒shift shift⇒
    where
    shift⇒ : ∀ {P} → DNS (_Above_ P) → Other-direction P
    shift⇒ shift ¬fin =
      shift (λ i ¬p →
        ¬fin (i , Equivalence.from
                    Has-upper-bound.mutually-inconsistent ⟨$⟩ ¬p))

    ⇒shift : ∀ {P} → Other-direction P → DNS (_Above_ P)
    ⇒shift hyp p =
      hyp (uncurry (λ i fin →
        p i (Equivalence.to
               Has-upper-bound.mutually-inconsistent ⟨$⟩ fin)))

  equivalent₂ : ∀ {P} → Other-direction (_Below_ P) ⇔ DNS P
  equivalent₂ {P} = equivalence ⇒shift shift⇒
    where
    shift⇒ : DNS P → Other-direction (_Below_ P)
    shift⇒ shift inf ¬inf =
      shift (λ i ¬Pi →
               inf (i , λ j i≤j ∀k≤j[Pk] → ¬Pi (∀k≤j[Pk] i i≤j)))
            (λ ∀iPi → ¬inf (λ i → i , NatOrder.refl , λ j j≤i → ∀iPi j))

    ⇒shift : ∀ {P} → Other-direction (_Below_ P) → DNS P
    ⇒shift {P} =
      Other-direction (_Below_ P)                   ∼⟨ (λ other₁ →
        Inf (_Below_ (_Below_ P))                         ∼⟨ map Below.counit ⟩
        Inf (_Below_ P)                                   ∼⟨ other₁ ⟩
        ¬ ¬ Functional.Inf (_Below_ P)                    ∼⟨ _<$>_ (Functional.map Below.cojoin) ⟩
        (¬ ¬ Functional.Inf (_Below_ (_Below_ P)))        ∎) ⟩
      Other-direction (_Below_ (_Below_ P))         ∼⟨ _⟨$⟩_ (Equivalence.to equivalent₁) ⟩
      DNS (_Above_ (_Below_ (_Below_ P)))           ∼⟨ Double-negation-shift.respects Below.⇑⇓⇔⇓ ⟩
      DNS (_Below_ (_Below_ P))                     ∼⟨ Double-negation-shift.DNS⇒DNS⇓ ⟩
      DNS⇓ (_Below_ P)                              ∼⟨ Double-negation-shift.DNS⇓⇒DNS ⟩
      DNS P                                         ∎
      where open Related.EquationalReasoning

  equivalent : (∀ P → Other-direction P) ⇔ (∀ P → DNS P)
  equivalent =
    equivalence (λ other P → _⟨$⟩_ (Equivalence.to   equivalent₂)
                                   (other (_Below_ P)))
                (λ shift P → _⟨$⟩_ (Equivalence.from equivalent₁)
                                   (shift (_Above_ P)))

  -- Some lemmas used below.

  up : ∀ {P} → Inf P → Inf (P ∘ suc)
  up =
    contraposition
      (Prod.map suc (_⟨$⟩_ (Equivalence.from Has-upper-bound.move-suc)))

  witness : ∀ {P} → Inf P → ¬ ¬ ∃ P
  witness ¬fin ¬p = ¬fin (0 , λ i _ Pi → ¬p (i , Pi))

------------------------------------------------------------------------
-- Definition of "true infinitely often" which uses double-negation

module DoubleNegated where

  open Fin using (Fin)
  open Has-upper-bound using (_Has-upper-bound_)

  infixl 4 _⟪$⟫_

  mutual

    -- Inf P means that P is true for infinitely many natural numbers.

    data Inf (P : ℕ → Set) : Set₁ where
      now  : (p : P 0) (inf : ∞ (¬¬Inf (P ∘ suc))) → Inf P
      skip :           (inf :      Inf (P ∘ suc) ) → Inf P

    data ¬¬Inf (P : ℕ → Set) : Set₁ where
      _⟪$⟫_ : {A : Set} (f : A → Inf P) (m : ¬ ¬ A) → ¬¬Inf P

  -- ¬¬Inf is equivalent to the non-constructive definition given
  -- above.

  expand : ∀ {P} → ¬¬Inf P → ¬ ¬ Inf P
  expand (f ⟪$⟫ m) = λ ¬inf → m (¬inf ∘ f)

  ¬¬equivalent : ∀ {P} → NonConstructive.Inf P ⇔ ¬¬Inf P
  ¬¬equivalent = equivalence ⇒ ⇐
    where
    ⇒ : ∀ {P} → NonConstructive.Inf P → ¬¬Inf P
    ⇒ ¬fin = helper ¬fin ⟪$⟫ NonConstructive.witness ¬fin
      where
      helper : ∀ {P} → NonConstructive.Inf P → ∃ P → Inf P
      helper ¬fin (zero  , p) = now p (♯ ⇒ (NonConstructive.up ¬fin))
      helper ¬fin (suc i , p) =
        skip (helper (NonConstructive.up ¬fin) (i , p))

    ⇐ : ∀ {P} → ¬¬Inf P → NonConstructive.Inf P
    ⇐ ¬¬inf (i , fin) = ⇐′ ¬¬inf i fin
      where
      mutual
        ⇐′ : ∀ {P} → ¬¬Inf P → ∀ i → ¬ P Has-upper-bound i
        ⇐′ ¬¬inf i fin = ¬¬-map (helper i fin) (expand ¬¬inf) id

        helper : ∀ {P} → ∀ i → P Has-upper-bound i → ¬ Inf P
        helper i       ¬p (skip  inf)   = helper i (Has-upper-bound.up ¬p) inf
        helper zero    ¬p (now p inf)   = ¬p 0 z≤n p
        helper (suc i) ¬p (now p ¬¬inf) =
          ⇐′ (♭ ¬¬inf) i (λ j i≤j → ¬p (suc j) (s≤s i≤j))

  -- Inf is equivalent to the non-constructive definition given above
  -- (in the double-negation monad).

  ⇐ : ∀ {P} → Inf P → NonConstructive.Inf P
  ⇐ {P} =
    Inf P                  ∼⟨ (λ inf → const inf ⟪$⟫ return tt) ⟩
    ¬¬Inf P                ∼⟨ _⟨$⟩_ (Equivalence.from ¬¬equivalent) ⟩
    NonConstructive.Inf P  ∎
    where open Related.EquationalReasoning

  ⇒ : ∀ {P} → NonConstructive.Inf P → ¬ ¬ Inf P
  ⇒ {P} =
    NonConstructive.Inf P  ∼⟨ _⟨$⟩_ (Equivalence.to ¬¬equivalent) ⟩
    ¬¬Inf P                ∼⟨ expand ⟩
    (¬ ¬ Inf P)            ∎
    where open Related.EquationalReasoning

  equivalent : ∀ {P} → ¬ ¬ (NonConstructive.Inf P ⇔ Inf P)
  equivalent {P} =
    (λ ⇒′ → equivalence (⇒′ ∘ lift) ⇐) <$>
      Univ.¬¬-pull (Univ._⇒_ _ Univ.Id) (λ inf → ⇒ (lower inf))

  -- Inf commutes with binary sums (in the double-negation monad).

  commutes : ∀ {P Q} → Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
  commutes {P} {Q} p∪q =
    negated-stable $ ¬¬-map helper $ NonConstructive.commutes (⇐ p∪q)
    where
    helper : NonConstructive.Inf P ⊎ NonConstructive.Inf Q →
             ¬ ¬ (Inf P ⊎ Inf Q)
    helper (inj₁ p) = λ ¬p∪q → ⇒ p (¬p∪q ∘ inj₁)
    helper (inj₂ q) = λ ¬p∪q → ⇒ q (¬p∪q ∘ inj₂)

-- You may wonder why double-negation is introduced in a roundabout
-- way in ¬¬Inf above. The reason is that the more direct definition,
-- used in DoubleNegated₂ below, is not strictly positive. Furthermore
-- DoubleNegated₂.equivalent is not accepted by the termination
-- checker.

{-
module DoubleNegated₂ where

  open DoubleNegated using (now; skip; _⟪$⟫_)

  data Inf (P : ℕ → Set) : Set where
    now  : (p : P 0) (inf : ∞ (¬ ¬ Inf (P ∘ suc))) → Inf P
    skip :           (inf :        Inf (P ∘ suc) ) → Inf P

  equivalent : ∀ {P} → DoubleNegated.Inf P ⇔ Inf P
  equivalent = equivalence ⇒ ⇐
    where
    ⇐ : ∀ {P} → Inf P → DoubleNegated.Inf P
    ⇐ (now p inf) = now p (♯ (⇐ ⟪$⟫ ♭ inf))
    ⇐ (skip  inf) = skip (⇐ inf)

    ⇒ : ∀ {P} → DoubleNegated.Inf P → Inf P
    ⇒ (now p inf) with ♭ inf
    ... | f ⟪$⟫ m = now p (♯ λ ¬inf → m (λ x → ¬inf (⇒ (f x))))
    ⇒ (skip  inf) = skip (⇒ inf)
-}

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; subst₂; cong)
open import Data.Nat.Base
open import Data.Fin hiding (_+_; #_)
open import Data.Product using (∃; _×_; _,_; ∃-syntax)

open import DeBruijn
open import Substitution using (rename-subst-commute; subst-commute)
open import Beta

infix 3 _⇉_

data _⇉_ : ∀ {n} → Term n → Term n → Set where

  ⇉-c : ∀ {n} {x : Fin n}
      ---------
    → # x ⇉ # x

  ⇉-ƛ : ∀ {n} {M M′ : Term (suc n)}
    → M ⇉ M′
      ----------
    → ƛ M ⇉ ƛ M′

  ⇉-ξ : ∀ {n} {M M′ N N′ : Term n}
    → M ⇉ M′
    → N ⇉ N′
      ---------------
    → M · N ⇉ M′ · N′

  ⇉-β : ∀ {n} {M M′ : Term (suc n)} {N N′ : Term n}
    → M ⇉ M′
    → N ⇉ N′
      ---------------------
    → (ƛ M) · N ⇉ M′ [ N′ ]

par-subst : ∀ {n m} → Subst n m → Subst n m → Set
par-subst σ σ′ = ∀ {x} → σ x ⇉ σ′ x

par-rename : ∀ {n m} {ρ : Rename n m} {M M′ : Term n}
  → M ⇉ M′
    ------------------------
  → rename ρ M ⇉ rename ρ M′
par-rename ⇉-c         = ⇉-c
par-rename (⇉-ƛ p)     = ⇉-ƛ (par-rename p)
par-rename (⇉-ξ p₁ p₂) = ⇉-ξ (par-rename p₁) (par-rename p₂)
par-rename {n}{m}{ρ} (⇉-β {n}{N}{N′}{M}{M′} p₁ p₂)
    with ⇉-β (par-rename {ρ = ext ρ} p₁) (par-rename {ρ = ρ} p₂)
... | G rewrite rename-subst-commute {n}{m}{N′}{M′}{ρ} = G

par-subst-exts : ∀ {n m} {σ σ′ : Subst n m}
  → par-subst σ σ′
    ---------------------------
  → par-subst (exts σ) (exts σ′)
par-subst-exts s {x = zero} = ⇉-c
par-subst-exts s {x = suc x} = par-rename s

subst-par : ∀ {n m} {σ σ′ : Subst n m} {M M′ : Term n}
  → par-subst σ σ′
  → M ⇉ M′
    ----------------------
  → subst σ M ⇉ subst σ′ M′
subst-par {M = # x} s ⇉-c = s
subst-par {n}{m}{σ}{σ′} {ƛ N} s (⇉-ƛ p) =
  ⇉-ƛ (subst-par {σ = exts σ}{σ′ = exts σ′}
         (λ {x} → par-subst-exts s {x = x}) p)
subst-par {M = L · M} s (⇉-ξ p₁ p₂) =
  ⇉-ξ (subst-par s p₁) (subst-par s p₂)
subst-par {n}{m}{σ}{σ′} {(ƛ N) · M} s (⇉-β {M′ = M′}{N′ = N′} p₁ p₂)
    with ⇉-β (subst-par {σ = exts σ}{σ′ = exts σ′}{M = N}
                        (λ {x} → par-subst-exts s {x = x}) p₁)
             (subst-par {σ = σ} s p₂)
... | G rewrite subst-commute {N = M′}{M = N′}{σ = σ′} = G

par-subst-zero : ∀ {n} {M M′ : Term n}
  → M ⇉ M′
    ----------------------------------------
  → par-subst (subst-zero M) (subst-zero M′)
par-subst-zero M⇉M′ {zero} = M⇉M′
par-subst-zero M⇉M′ {suc x} = ⇉-c

sub-par : ∀ {n} {M M′ : Term (suc n)} {N N′ : Term n}
  → M ⇉ M′
  → N ⇉ N′
    -------------------
  → M [ N ] ⇉ M′ [ N′ ]
sub-par M⇉M′ N⇉N′ = subst-par (par-subst-zero N⇉N′) M⇉M′

par-refl : ∀ {n} {M : Term n}
    -----
  → M ⇉ M
par-refl {M = # x}   = ⇉-c
par-refl {M = ƛ N}   = ⇉-ƛ par-refl
par-refl {M = L · M} = ⇉-ξ par-refl par-refl

beta-par : ∀ {n} {M N : Term n}
  → M —→ N
    ------
  → M ⇉ N
beta-par {M = L · M} (—→-ξₗ r) = ⇉-ξ (beta-par {M = L} r) par-refl
beta-par {M = L · M} (—→-ξᵣ r) = ⇉-ξ par-refl (beta-par {M = M} r)
beta-par {M = ƛ N} (—→-ƛ r) = ⇉-ƛ (beta-par r)
beta-par {M = (ƛ N) · M} —→-β = ⇉-β par-refl par-refl

par-betas : ∀ {n} {M N : Term n}
  → M ⇉ N
    ------
  → M —↠ N
par-betas {M = # _} (⇉-c {x = x}) = # x ∎
par-betas {M = ƛ M} (⇉-ƛ p) = —↠-cong-ƛ (par-betas p)
par-betas {M = M · N} (⇉-ξ p₁ p₂) = —↠-cong (par-betas p₁) (par-betas p₂)
par-betas {M = (ƛ M) · N} (⇉-β {M′ = M′}{N′ = N′} p₁ p₂) =
  let a : (ƛ M) · N —↠ (ƛ M′) · N
      a = —↠-congₗ (—↠-cong-ƛ (par-betas p₁))
      b : (ƛ M′) · N —↠ (ƛ M′) · N′
      b = —↠-congᵣ (par-betas p₂)
      c = (ƛ M′) · N′ —→⟨ —→-β ⟩ M′ [ N′ ] ∎ in
  —↠-trans (—↠-trans a b) c

infix  3 _⇉*_
infixr 3 _⇉⟨_⟩_
infix  4 _∎

data _⇉*_ : ∀ {n} → Term n → Term n → Set where

  _∎ : ∀ {n} (M : Term n)
      ------
    → M ⇉* M

  _⇉⟨_⟩_ : ∀ {n} {L N : Term n} (M : Term n)
    → M ⇉  L
    → L ⇉* N
      ------
    → M ⇉* N

betas-pars : ∀ {n} {M N : Term n}
  → M —↠ N
    ------
  → M ⇉* N
betas-pars (M ∎) = M ∎
betas-pars (M —→⟨ b ⟩ bs) = M ⇉⟨ beta-par b ⟩ betas-pars bs

pars-betas : ∀ {n} {M N : Term n}
  → M ⇉* N
    ------
  → M —↠ N
pars-betas (M ∎) = M ∎
pars-betas (M ⇉⟨ p ⟩ ps) = —↠-trans (par-betas p) (pars-betas ps)

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Hilbert-style formalisation of closed syntax.
-- Sequences of terms.

module BasicIPC.Syntax.ClosedHilbertSequential where

open import BasicIPC.Syntax.Common public

-- Derivations.

infix 3 ⊦⊢_
data ⊦⊢_ : Cx Ty → Set where
  nil   : ⊦⊢ ∅
  mp    : ∀ {Ξ A B}   → A ▻ B ∈ Ξ → A ∈ Ξ → ⊦⊢ Ξ → ⊦⊢ Ξ , B
  ci    : ∀ {Ξ A}     → ⊦⊢ Ξ → ⊦⊢ Ξ , A ▻ A
  ck    : ∀ {Ξ A B}   → ⊦⊢ Ξ → ⊦⊢ Ξ , A ▻ B ▻ A
  cs    : ∀ {Ξ A B C} → ⊦⊢ Ξ → ⊦⊢ Ξ , (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  cpair : ∀ {Ξ A B}   → ⊦⊢ Ξ → ⊦⊢ Ξ , A ▻ B ▻ A ∧ B
  cfst  : ∀ {Ξ A B}   → ⊦⊢ Ξ → ⊦⊢ Ξ , A ∧ B ▻ A
  csnd  : ∀ {Ξ A B}   → ⊦⊢ Ξ → ⊦⊢ Ξ , A ∧ B ▻ B
  unit  : ∀ {Ξ}       → ⊦⊢ Ξ → ⊦⊢ Ξ , ⊤

infix 3 ⊢_
⊢_ : Ty → Set
⊢ A = ∃ (λ Ξ → ⊦⊢ Ξ , A)

-- Concatenation of derivations.

_⧺⊦_ : ∀ {Ξ Ξ′} → ⊦⊢ Ξ → ⊦⊢ Ξ′ → ⊦⊢ Ξ ⧺ Ξ′
us ⧺⊦ nil       = us
us ⧺⊦ mp i j ts = mp (mono∈ weak⊆⧺₂ i) (mono∈ weak⊆⧺₂ j) (us ⧺⊦ ts)
us ⧺⊦ ci ts     = ci (us ⧺⊦ ts)
us ⧺⊦ ck ts     = ck (us ⧺⊦ ts)
us ⧺⊦ cs ts     = cs (us ⧺⊦ ts)
us ⧺⊦ cpair ts  = cpair (us ⧺⊦ ts)
us ⧺⊦ cfst ts   = cfst (us ⧺⊦ ts)
us ⧺⊦ csnd ts   = csnd (us ⧺⊦ ts)
us ⧺⊦ unit ts   = unit (us ⧺⊦ ts)

-- Modus ponens in expanded form.

app : ∀ {A B} → ⊢ A ▻ B → ⊢ A → ⊢ B
app {A} {B} (Ξ , ts) (Ξ′ , us) = Ξ″ , vs
  where Ξ″ = (Ξ′ , A) ⧺ (Ξ , A ▻ B)
        vs = mp top (mono∈ (weak⊆⧺₁ (Ξ , A ▻ B)) top) (us ⧺⊦ ts)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Semigroup.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Reflection.RecordEquiv

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open Iso

private
  variable
    ℓ : Level

-- Semigroups as a record, inspired by the Agda standard library:
--
--  https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Bundles.agda#L48
--  https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L50
--
-- Note that as we are using Path for all equations the IsMagma record
-- would only contain isSet A if we had it.
record IsSemigroup {A : Type ℓ} (_·_ : A → A → A) : Type ℓ where
  no-eta-equality
  constructor issemigroup

  field
    is-set : isSet A
    ·Assoc  : (x y z : A) → x · (y · z) ≡ (x · y) · z

unquoteDecl IsSemigroupIsoΣ = declareRecordIsoΣ IsSemigroupIsoΣ (quote IsSemigroup)

record SemigroupStr (A : Type ℓ) : Type ℓ where

  constructor semigroupstr

  field
    _·_         : A → A → A
    isSemigroup : IsSemigroup _·_

  infixl 7 _·_

  open IsSemigroup isSemigroup public

Semigroup : ∀ ℓ → Type (ℓ-suc ℓ)
Semigroup ℓ = TypeWithStr ℓ SemigroupStr

module _ (A : Type ℓ) (_·_ : A → A → A) (h : IsSemigroup _·_) where
  semigroup : Semigroup ℓ
  semigroup .fst = A
  semigroup .snd .SemigroupStr._·_ = _·_
  semigroup .snd .SemigroupStr.isSemigroup = h

record IsSemigroupEquiv {A : Type ℓ} {B : Type ℓ}
  (M : SemigroupStr A) (e : A ≃ B) (N : SemigroupStr B)
  : Type ℓ
  where

  -- Shorter qualified names
  private
    module M = SemigroupStr M
    module N = SemigroupStr N

  field
    isHom : (x y : A) → equivFun e (x M.· y) ≡ equivFun e x N.· equivFun e y

open SemigroupStr
open IsSemigroup
open IsSemigroupEquiv

SemigroupEquiv : (M N : Semigroup ℓ) → Type ℓ
SemigroupEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsSemigroupEquiv (M .snd) e (N .snd)

isPropIsSemigroup : {A : Type ℓ} (_·_ : A → A → A) → isProp (IsSemigroup _·_)
isPropIsSemigroup _·_ =
  isOfHLevelRetractFromIso 1 IsSemigroupIsoΣ
    (isPropΣ
      isPropIsSet
      (λ isSetA → isPropΠ3 λ _ _ _ → isSetA _ _))

𝒮ᴰ-Semigroup : DUARel (𝒮-Univ ℓ) SemigroupStr ℓ
𝒮ᴰ-Semigroup =
  𝒮ᴰ-Record (𝒮-Univ _) IsSemigroupEquiv
    (fields:
      data[ _·_ ∣ autoDUARel _ _ ∣ isHom ]
      prop[ isSemigroup ∣ (λ _ _ → isPropIsSemigroup _) ])

SemigroupPath : (M N : Semigroup ℓ) → SemigroupEquiv M N ≃ (M ≡ N)
SemigroupPath = ∫ 𝒮ᴰ-Semigroup .UARel.ua

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --copatterns --show-implicit #-}

module Issue940 where

module _ (A : Set) where

  record Box : Set where
    constructor box
    field
      unbox : A

  open Box

  postulate x : A

  ex : Box
  ex = box x -- works

  ex' : Box
  unbox ex' = x

  -- Error WAS:
  -- An internal error has occurred. Please report this as a bug.
  -- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:326

postulate
  A : Set

ok : Box A
Box.unbox ok = x A -- works


text:
module Issue558b where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

data _≡_ {A : Set} (a : A) : A → Set where
  Refl : a ≡ a

plus : Nat → Nat → Nat
plus Z n = n
plus (S n) m = S (plus n m)

data Addable (τ : Set) : Set where
  addable : (τ → τ → τ) → Addable τ

plus' : {τ : Set} → Addable τ → τ → τ → τ
plus' (addable p) = p

record ⊤ : Set where

module AddableM {τ : Set} {a : ⊤} (a : Addable τ) where
  _+_ : τ → τ → τ
  _+_ = plus' a

-- record Addable (τ : Set) : Set where
--  constructor addable
--  field
--   _+_ : τ → τ → τ

open module AddableIFS {t : Set} {a : ⊤} {{r : Addable t}} = AddableM {t} r

data CommAddable (τ : Set) {a : ⊤} : Set where
 commAddable : (addable : Addable τ) → ((a b : τ) → (a + b) ≡ (b + a)) → CommAddable τ

private
  addableCA' : {τ : Set} (ca : CommAddable τ) → Addable τ
  addableCA' (commAddable a _) = a

  comm' : {τ : Set} (ca : CommAddable τ) →
          let a = addableCA' ca in (a b : τ) → (a + b) ≡ (b + a)
  comm' (commAddable _ c) = c

module CommAddableM {τ : Set} {a : ⊤} (ca : CommAddable τ) where
  addableCA : Addable τ
  addableCA = addableCA' ca

  comm : (a b : τ) → (a + b) ≡ (b + a)
  comm = comm' ca

natAdd : Addable Nat
natAdd = addable plus

postulate commPlus : (a b : Nat) → plus a b ≡ plus b a

commNatAdd : CommAddable Nat
commNatAdd = commAddable natAdd commPlus

open CommAddableM {{...}}

test : (Z + Z) ≡ Z
test = comm Z Z

a : {x y : Nat} → (S (S Z) + (x + y)) ≡ ((x + y) + S (S Z))
a {x}{y} = comm (S (S Z)) (x + y)


text:
-- Andreas, 2017-01-01, issue 2372, reported by m0davis

-- This file is imported by Issue2372ImportInst.

module Issue2372Inst where

postulate D : Set

record R : Set₁ where
  field
    r : Set

open R {{ ... }} public

instance iR = record { r = D }


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

module Examples.Run where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Luau.Syntax using (nil; var; _$_; function_⟨_⟩_end; return; _∙_; done)
open import Luau.Value using (nil)
open import Luau.Run using (run; return)
open import Luau.Heap using (emp; lookup-next; next-emp; lookup-next-emp)

import Agda.Builtin.Equality.Rewrite
{-# REWRITE lookup-next next-emp lookup-next-emp #-}

x = var "x"
id = var "id"

ex1 : (run (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _)
ex1 = refl

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
module Issue5563 where

F : (@0 A : Set) → A → A
F A x =
  let
    y : A
    y = x
  in y


text:
module Cats.Category.Fun.Facts where

open import Cats.Category
open import Cats.Category.Cat using (_≈_)
open import Cats.Category.Fun using (Trans ; Fun ; ≈-intro ; ≈-elim)
open import Cats.Functor using (Functor)
open import Cats.Trans.Iso using (NatIso ; iso ; forth-natural ; back-natural)

open import Level using (_⊔_)

open Functor
open Trans
open Category._≅_

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  {F G : Functor C D}
  where

  private
    module C = Category C
    module D = Category D
    open D.≈-Reasoning
    open Category (Fun C D) using (_≅_)

  NatIso→≅ : NatIso F G → F ≅ G
  NatIso→≅ i = record
      { forth = Forth i
      ; back = Back i
      ; back-forth = ≈-intro (back-forth (iso i))
      ; forth-back = ≈-intro (forth-back (iso i))
      }
    where
      open NatIso

  ≅→NatIso : F ≅ G → NatIso F G
  ≅→NatIso i = record
      { iso = λ {c} → record
          { forth = component (forth i) c
          ; back = component (back i) c
          ; back-forth = ≈-elim (back-forth i)
          ; forth-back = ≈-elim (forth-back i)
          }
      ; forth-natural = natural (forth i)
      }

  ≈→≅ : F ≈ G → F ≅ G
  ≈→≅ eq = NatIso→≅ eq

  ≅→≈ : F ≅ G → F ≈ G
  ≅→≈ i = ≅→NatIso i

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

module Classifying where
  open import Basics

  open import Flat
  open import lib.types.Sigma
  open import lib.Equivalence2
  open import lib.types.Truncation

  BAut : ∀ {i} {X : Type i} (x : X) → Type i
  BAut {X = X} x = Σ X $ (\y → ∥ x == y ∥)

  ♭-commutes-with-BAut : {@♭ i : ULevel } (@♭ X : Type i) (@♭ x : X)
                         → (♭ (BAut x)) ≃ BAut (x ^♭)
  ♭-commutes-with-BAut X x =  ♭ (BAut x)
                           ≃⟨ ♭-commutes-with-Σ ⟩
                              Σ (♭ X) (\u → let♭ y ^♭:= u in♭ (♭ ∥ x == y ∥))
                           ≃⟨ Σ-emap-r lemma₂ ⟩
                               Σ (♭ X) (\u → let♭ y ^♭:= u in♭ ∥ ♭ (x == y) ∥)
                           ≃⟨ Σ-emap-r lemma₁ ⟩
                              BAut (x ^♭)
                           ≃∎
     where
       lemma₁ : (z : ♭ X) → (let♭ y ^♭:= z in♭ ∥ ♭ (x == y) ∥) ≃ ∥ (x ^♭) == z ∥
       lemma₁ (z ^♭) = Trunc-emap (♭-identity-eq x z)

       lemma₂ : (z : ♭ X) → (let♭ y ^♭:= z in♭ (♭ ∥ x == y ∥)) ≃ (let♭ y ^♭:= z in♭ ∥ ♭ (x == y) ∥)
       lemma₂ (z ^♭) = (♭-Trunc-eq (x == z)) ⁻¹

  _is-locally-crisply-discrete : {@♭ i : ULevel} (@♭ X : Type i) → Type i
  _is-locally-crisply-discrete X = (@♭ x y : X) → (x == y) is-discrete

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
module Section8 where

open import Section7 public

-- 8. Correctness of conversion between terms
-- ==========================================
--
-- The conversion rules for terms are sound:

-- Theorem 9.
postulate
  thm₉ : ∀ {Γ A t₀ t₁} →
           (M N : Γ ⊢ A) → t₀ 𝒟 M → t₁ 𝒟 N → Γ ⊢ t₀ ≊ t₁ ∷ A →
           M ≅ N

-- Proof: The proof is by induction on the proof of `Γ ⊢ t₀ ≊ t₁ ∷ A`.  We illustrate the proof
-- with the reflexivity case.  In this case we have that `t₀` and `t₁` are the same, hence by Corollary 3
-- we get `M ≅ N`.
--
-- To prove that the conversion rules are complete
-- is straightforward by induction on the proof of `M ≅ N`.

-- Theorem 10.
postulate
  thm₁₀ : ∀ {Γ A} →
            (M N : Γ ⊢ A) → M ≅ N →
            Γ ⊢ M ⁻ ≊ N ⁻ ∷ A

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.Renaming
import SecondOrder.Term

module SecondOrder.Theory
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Metavariable Σ public
  open SecondOrder.Term Σ public
  open SecondOrder.Signature.Signature Σ public
  open SecondOrder.Renaming Σ

  record Axiom : Set ℓ where
    constructor make-ax
    field
      ax-mv-ctx : MContext -- metavariable context of an equation
      ax-sort : sort -- sort of an equation
      ax-lhs : Term ax-mv-ctx ctx-empty ax-sort -- left-hand side
      ax-rhs : Term ax-mv-ctx ctx-empty ax-sort -- right-hand side

  record Theory ℓa : Set (lsuc (ℓ ⊔ ℓa)) where
    field
      ax : Set ℓa -- the axioms
      ax-eq : ax → Axiom -- each axiom has a corresponding Axiom

    ax-mv-ctx : ax → MContext -- the meta-context of each axiom
    ax-mv-ctx ε = Axiom.ax-mv-ctx (ax-eq ε)

    ax-sort : ax → sort -- the sort of each axiom
    ax-sort ε = Axiom.ax-sort (ax-eq ε)

    -- the left- and right-hand side of each axiom s ≈ t, promoted to any context
    ax-lhs : ∀ (ε : ax) {Γ} → Term (ax-mv-ctx ε) Γ (ax-sort ε)
    ax-lhs ε =  [ inʳ ]ʳ Axiom.ax-lhs (ax-eq ε)

    ax-rhs : ∀ (ε : ax) {Γ} → Term (ax-mv-ctx ε) Γ (ax-sort ε)
    ax-rhs ε = [ inʳ ]ʳ Axiom.ax-rhs (ax-eq ε)

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------------
-- Properties for the bisimilarity relation
------------------------------------------------------------------------------

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

module FOT.FOTC.Relation.Binary.Bisimilarity.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Relation.Binary.Bisimilarity.Type

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

{-# TERMINATING #-}
≈→≡ : ∀ {xs ys} → xs ≈ ys → xs ≡ ys
≈→≡ {xs} {ys} h with ≈-out h
... | x' , xs' , ys' , prf₁ , prf₂ , prf₃ =
  xs       ≡⟨ prf₁ ⟩
  x' ∷ xs' ≡⟨ ∷-rightCong (≈→≡ prf₃) ⟩
  x' ∷ ys' ≡⟨ sym prf₂ ⟩
  ys       ∎


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

module Data.Binary.PerformanceTests.Multiplication where

open import Prelude
open import Data.Binary.Definition
open import Data.Binary.Addition using (_+_)
open import Data.Binary.Multiplication using (_*_)
open import Data.Binary.Increment using (inc)

one-thousand : 𝔹
one-thousand = 2ᵇ 1ᵇ 1ᵇ 2ᵇ 1ᵇ 2ᵇ 2ᵇ 2ᵇ 2ᵇ 0ᵇ

pow-r : 𝔹 → ℕ → 𝔹
pow-r x zero    = 1ᵇ 0ᵇ
pow-r x (suc n) = x * pow-r (inc x) n

pow-l : 𝔹 → ℕ → 𝔹
pow-l x zero    = 1ᵇ 0ᵇ
pow-l x (suc n) = pow-l (inc x) n * x

n : ℕ
n = 6

f : 𝔹
f = one-thousand

-- The actual performance test (uncomment and time how long it takes to type-check)
-- _ : pow-r f n ≡ pow-l f n
-- _ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Data.Tuple.Base where

open import Level using (_⊔_)

-- non-dependent pair; failed to reuse _×_
record Pair {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B
{-# FOREIGN GHC type AgdaPair a b c d = (c , d) #-}
-- {-# COMPILE GHC Pair = type MAlonzo.Code.Data.Tuple.AgdaPair #-}
{-# COMPILE GHC Pair = data MAlonzo.Code.Data.Tuple.AgdaPair ((,)) #-}

infixl 5 _∥_

_∥_ = Pair

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
------------------------------------------------------------------------------
-- Group theory
------------------------------------------------------------------------------

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

module GroupTheory.README where

------------------------------------------------------------------------------
-- Description

-- Theory of groups using Agda postulates for the group axioms.

------------------------------------------------------------------------------
-- The axioms
open import GroupTheory.Base

-- Basic properties
open import GroupTheory.PropertiesATP
open import GroupTheory.PropertiesI

-- Commutator properties
open import GroupTheory.Commutator.PropertiesATP
open import GroupTheory.Commutator.PropertiesI

-- Abelian groups
open import GroupTheory.AbelianGroup.PropertiesATP


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

open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Sets.Cardinality.Finite.Definition
open import Groups.Definition

module Groups.FiniteGroups.Definition where

record FiniteGroup {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_·_ : A → A → A} (G : Group S _·_) {c : _} (quotientSet : Set c) : Set (a ⊔ b ⊔ c) where
  field
    toSet : SetoidToSet S quotientSet
    finite : FiniteSet quotientSet

groupOrder : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_·_ : A → A → A} {underG : Group S _·_} {c : _} {quotientSet : Set c} (G : FiniteGroup underG quotientSet) → ℕ
groupOrder record { toSet = toSet ; finite = record { size = size ; mapping = mapping ; bij = bij } } = size


text:
------------------------------------------------------------------------
-- A tiny library of derived combinators
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.Lib (Tok : Set) where

open import Codata.Musical.Notation
open import Data.Bool hiding (_∧_; _≤_)
open import Data.Bool.Properties
open import Function hiding (_∋_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (module Equivalence)
open import Data.List
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product as Prod
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary.Decidable

import TotalRecognisers.LeftRecursion
open TotalRecognisers.LeftRecursion Tok

------------------------------------------------------------------------
-- Kleene star

-- The intended semantics of the Kleene star.

infixr 5 _∷_
infix  4 _∈[_]⋆

data _∈[_]⋆ {n} : List Tok → P n → Set where
  []  : ∀ {p}       → [] ∈[ p ]⋆
  _∷_ : ∀ {s₁ s₂ p} → s₁ ∈ p → s₂ ∈[ p ]⋆ → s₁ ++ s₂ ∈[ p ]⋆

module KleeneStar₁ where

  infix 15 _⋆ _+

  -- This definition requires that the argument recognisers are not
  -- nullable.

  mutual

    _⋆ : P false → P true
    p ⋆ = empty ∣ p +

    _+ : P false → P false
    p + = p · ♯ (p ⋆)

  -- The definition of _⋆ above is correct.

  ⋆-sound : ∀ {s p} → s ∈ p ⋆ → s ∈[ p ]⋆
  ⋆-sound (∣-left  empty)       = []
  ⋆-sound (∣-right (pr₁ · pr₂)) = pr₁ ∷ ⋆-sound pr₂

  ⋆-complete : ∀ {s p} → s ∈[ p ]⋆ → s ∈ p ⋆
  ⋆-complete []                    = ∣-left empty
  ⋆-complete (_∷_ {[]}    pr₁ pr₂) = ⋆-complete pr₂
  ⋆-complete (_∷_ {_ ∷ _} pr₁ pr₂) =
    ∣-right {n₁ = true} (pr₁ · ⋆-complete pr₂)

module KleeneStar₂ where

  infix 15 _⋆

  -- This definition works for any argument recogniser.

  _⋆ : ∀ {n} → P n → P true
  _⋆ = KleeneStar₁._⋆ ∘ nonempty

  -- The definition of _⋆ above is correct.

  ⋆-sound : ∀ {s n} {p : P n} → s ∈ p ⋆ → s ∈[ p ]⋆
  ⋆-sound (∣-left  empty)                = []
  ⋆-sound (∣-right (nonempty pr₁ · pr₂)) = pr₁ ∷ ⋆-sound pr₂

  ⋆-complete : ∀ {s n} {p : P n} → s ∈[ p ]⋆ → s ∈ p ⋆
  ⋆-complete []                    = ∣-left empty
  ⋆-complete (_∷_ {[]}    pr₁ pr₂) = ⋆-complete pr₂
  ⋆-complete (_∷_ {_ ∷ _} pr₁ pr₂) =
    ∣-right {n₁ = true} (nonempty pr₁ · ⋆-complete pr₂)

  -- Note, however, that for actual parsing the corresponding
  -- definition would not be correct. The reason is that p would give
  -- a result also when the empty string was accepted, and these
  -- results are ignored by the definition above. In the case of
  -- actual parsing the result of p ⋆, when p is nullable, should be a
  -- stream and not a finite list.

------------------------------------------------------------------------
-- A simplified sequencing operator

infixl 10 _⊙_

_⊙_ : ∀ {n₁ n₂} → P n₁ → P n₂ → P (n₁ ∧ n₂)
_⊙_ {n₁ = n₁} p₁ p₂ = ♯? p₁ · ♯? {b = n₁} p₂

module ⊙ where

  complete : ∀ {n₁ n₂ s₁ s₂} {p₁ : P n₁} {p₂ : P n₂} →
             s₁ ∈ p₁ → s₂ ∈ p₂ → s₁ ++ s₂ ∈ p₁ ⊙ p₂
  complete {n₁} {n₂} s₁∈p₁ s₂∈p₂ = add-♭♯ n₂ s₁∈p₁ · add-♭♯ n₁ s₂∈p₂

  infixl 10 _⊙′_
  infix   4 _⊙_∋_

  data _⊙_∋_ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) : List Tok → Set where
    _⊙′_ : ∀ {s₁ s₂} (s₁∈p₁ : s₁ ∈ p₁) (s₂∈p₂ : s₂ ∈ p₂) →
           p₁ ⊙ p₂ ∋ s₁ ++ s₂

  sound : ∀ {n₁} n₂ {s} {p₁ : P n₁} {p₂ : P n₂} →
          s ∈ p₁ ⊙ p₂ → p₁ ⊙ p₂ ∋ s
  sound {n₁} n₂ (s₁∈p₁ · s₂∈p₂) = drop-♭♯ n₂ s₁∈p₁ ⊙′ drop-♭♯ n₁ s₂∈p₂

------------------------------------------------------------------------
-- A combinator which repeats a recogniser a fixed number of times

⟨_^_⟩-nullable : Bool → ℕ → Bool
⟨ n ^ zero  ⟩-nullable = true
⟨ n ^ suc i ⟩-nullable = n ∧ ⟨ n ^ i ⟩-nullable

infixl 15 _^_

_^_ : ∀ {n} → P n → (i : ℕ) → P ⟨ n ^ i ⟩-nullable
p ^ 0     = empty
p ^ suc i = p ⊙ p ^ i

-- Some lemmas relating _^_ to _⋆.

open KleeneStar₂

^≤⋆ : ∀ {n} {p : P n} i → p ^ i ≤ p ⋆
^≤⋆ {n} {p} i s∈ = ⋆-complete $ helper i s∈
  where
  helper : ∀ i {s} → s ∈ p ^ i → s ∈[ p ]⋆
  helper zero    empty          = []
  helper (suc i) (s₁∈p · s₂∈pⁱ) =
    drop-♭♯ ⟨ n ^ i ⟩-nullable s₁∈p ∷ helper i (drop-♭♯ n s₂∈pⁱ)

⋆≤^ : ∀ {n} {p : P n} {s} → s ∈ p ⋆ → ∃ λ i → s ∈ p ^ i
⋆≤^ {n} {p} s∈p⋆ = helper (⋆-sound s∈p⋆)
  where
  helper : ∀ {s} → s ∈[ p ]⋆ → ∃ λ i → s ∈ p ^ i
  helper []             = (0 , empty)
  helper (s₁∈p ∷ s₂∈p⋆) =
    Prod.map suc (λ {i} s₂∈pⁱ → add-♭♯ ⟨ n ^ i ⟩-nullable s₁∈p ·
                                add-♭♯ n                  s₂∈pⁱ)
             (helper s₂∈p⋆)

------------------------------------------------------------------------
-- A recogniser which only accepts a given token

module Tok (dec : Decidable (_≡_ {A = Tok})) where

  tok : Tok → P false
  tok t = sat (⌊_⌋ ∘ dec t)

  sound : ∀ {s t} → s ∈ tok t → s ≡ [ t ]
  sound (sat ok) = cong [_] $ sym $ toWitness ok

  complete : ∀ {t} → [ t ] ∈ tok t
  complete = sat (fromWitness refl)

------------------------------------------------------------------------
-- A recogniser which accepts the empty string iff the argument is
-- true (and never accepts non-empty strings)

accept-if-true : ∀ b → P b
accept-if-true true  = empty
accept-if-true false = fail

module AcceptIfTrue where

  sound : ∀ b {s} → s ∈ accept-if-true b → s ≡ [] × T b
  sound true  empty = (refl , _)
  sound false ()

  complete : ∀ {b} → T b → [] ∈ accept-if-true b
  complete ok with Equivalence.to T-≡ ⟨$⟩ ok
  ... | refl = empty

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Andreas, 2016-06-08 issue #2006 (actually #289)

open import Common.Reflection
open import Common.Prelude

bla : Term → Term
bla = {!!}  -- Splitting here should be fine

macro
  comp : Term → Term → TC ⊤
  comp x t = bindTC (quoteTC (bla x)) (λ y → unify t y)

foo : Term
foo = comp Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda