text:
-- {-# OPTIONS -v tc.pos:100 #-}
-- Records are allowed in mutual blocks.
module RecordInMutual where

import Common.Level
open import Common.Equality

mutual
  record A : Set where
    field p : D
  record B : Set where
    field q : A
  data D : Set where
    c : B -> D

open A
open B

-- A and B are guarded via D, so we have eta for A and for B:

etaA : {a : A} → a ≡ record { p = p a }
etaA = refl

etaB : {b : B} → b ≡ record { q = q b }
etaB = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Definition.Conversion.Weakening where

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Consequences.Syntactic
open import Definition.Conversion
open import Definition.Conversion.Soundness

import Tools.PropositionalEquality as PE
open import Tools.Product

mutual
  -- Weakening of algorithmic equality of neutrals.
  wk~↑ : ∀ {ρ t u A Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
      → Γ ⊢ t ~ u ↑ A
      → Δ ⊢ U.wk ρ t ~ U.wk ρ u ↑ U.wk ρ A
  wk~↑ {ρ} [ρ] ⊢Δ (var-refl x₁ x≡y) = var-refl (wkTerm [ρ] ⊢Δ x₁) (PE.cong (wkVar ρ) x≡y)
  wk~↑ ρ ⊢Δ (app-cong {G = G} t~u x) =
    PE.subst (λ x → _ ⊢ _ ~ _ ↑ x) (PE.sym (wk-β G))
             (app-cong (wk~↓ ρ ⊢Δ t~u) (wkConv↑Term ρ ⊢Δ x))
  wk~↑ ρ ⊢Δ (fst-cong p~r) =
    fst-cong (wk~↓ ρ ⊢Δ p~r)
  wk~↑ ρ ⊢Δ (snd-cong {G = G} p~r) =
    PE.subst (λ x → _ ⊢ _ ~ _ ↑ x)
             (PE.sym (wk-β G))
             (snd-cong (wk~↓ ρ ⊢Δ p~r))
  wk~↑ {ρ} {Δ = Δ} [ρ] ⊢Δ (natrec-cong {k} {l} {h} {g} {a₀} {b₀} {F} {G} x x₁ x₂ t~u) =
    PE.subst (λ x → _ ⊢ U.wk ρ (natrec F a₀ h k) ~ _ ↑ x) (PE.sym (wk-β F))
             (natrec-cong (wkConv↑ (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) x)
                          (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x) (wk-β F)
                                    (wkConv↑Term [ρ] ⊢Δ x₁))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ h [conv↑] U.wk ρ g ∷ x)
                                    (wk-β-natrec _ F) (wkConv↑Term [ρ] ⊢Δ x₂))
                          (wk~↓ [ρ] ⊢Δ t~u))
  wk~↑ {ρ} {Δ = Δ} [ρ] ⊢Δ (Emptyrec-cong {k} {l} {F} {G} x t~u) =
    Emptyrec-cong (wkConv↑ [ρ] ⊢Δ x) (wk~↓ [ρ] ⊢Δ t~u)

  -- Weakening of algorithmic equality of neutrals in WHNF.
  wk~↓ : ∀ {ρ t u A Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
      → Γ ⊢ t ~ u ↓ A
      → Δ ⊢ U.wk ρ t ~ U.wk ρ u ↓ U.wk ρ A
  wk~↓ {ρ} [ρ] ⊢Δ ([~] A₁ D whnfA k~l) =
    [~] (U.wk ρ A₁) (wkRed* [ρ] ⊢Δ D) (wkWhnf ρ whnfA) (wk~↑ [ρ] ⊢Δ k~l)

  -- Weakening of algorithmic equality of types.
  wkConv↑ : ∀ {ρ A B Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
          → Γ ⊢ A [conv↑] B
          → Δ ⊢ U.wk ρ A [conv↑] U.wk ρ B
  wkConv↑ {ρ} [ρ] ⊢Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    [↑] (U.wk ρ A′) (U.wk ρ B′) (wkRed* [ρ] ⊢Δ D) (wkRed* [ρ] ⊢Δ D′)
        (wkWhnf ρ whnfA′) (wkWhnf ρ whnfB′) (wkConv↓ [ρ] ⊢Δ A′<>B′)

  -- Weakening of algorithmic equality of types in WHNF.
  wkConv↓ : ∀ {ρ A B Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
         → Γ ⊢ A [conv↓] B
         → Δ ⊢ U.wk ρ A [conv↓] U.wk ρ B
  wkConv↓ ρ ⊢Δ (U-refl x) = U-refl ⊢Δ
  wkConv↓ ρ ⊢Δ (ℕ-refl x) = ℕ-refl ⊢Δ
  wkConv↓ ρ ⊢Δ (Empty-refl x) = Empty-refl ⊢Δ
  wkConv↓ ρ ⊢Δ (Unit-refl x) = Unit-refl ⊢Δ
  wkConv↓ ρ ⊢Δ (ne x) = ne (wk~↓ ρ ⊢Δ x)
  wkConv↓ ρ ⊢Δ (Π-cong x A<>B A<>B₁) =
    let ⊢ρF = wk ρ ⊢Δ x
    in  Π-cong ⊢ρF (wkConv↑ ρ ⊢Δ A<>B) (wkConv↑ (lift ρ) (⊢Δ ∙ ⊢ρF) A<>B₁)
  wkConv↓ ρ ⊢Δ (Σ-cong x A<>B A<>B₁) =
    let ⊢ρF = wk ρ ⊢Δ x
    in  Σ-cong ⊢ρF (wkConv↑ ρ ⊢Δ A<>B) (wkConv↑ (lift ρ) (⊢Δ ∙ ⊢ρF) A<>B₁)

  -- Weakening of algorithmic equality of terms.
  wkConv↑Term : ∀ {ρ t u A Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
             → Γ ⊢ t [conv↑] u ∷ A
             → Δ ⊢ U.wk ρ t [conv↑] U.wk ρ u ∷ U.wk ρ A
  wkConv↑Term {ρ} [ρ] ⊢Δ ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    [↑]ₜ (U.wk ρ B) (U.wk ρ t′) (U.wk ρ u′)
         (wkRed* [ρ] ⊢Δ D) (wkRed*Term [ρ] ⊢Δ d) (wkRed*Term [ρ] ⊢Δ d′)
         (wkWhnf ρ whnfB) (wkWhnf ρ whnft′) (wkWhnf ρ whnfu′)
         (wkConv↓Term [ρ] ⊢Δ t<>u)

  -- Weakening of algorithmic equality of terms in WHNF.
  wkConv↓Term : ∀ {ρ t u A Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
             → Γ ⊢ t [conv↓] u ∷ A
             → Δ ⊢ U.wk ρ t [conv↓] U.wk ρ u ∷ U.wk ρ A
  wkConv↓Term ρ ⊢Δ (ℕ-ins x) =
    ℕ-ins (wk~↓ ρ ⊢Δ x)
  wkConv↓Term ρ ⊢Δ (Empty-ins x) =
    Empty-ins (wk~↓ ρ ⊢Δ x)
  wkConv↓Term ρ ⊢Δ (Unit-ins x) =
    Unit-ins (wk~↓ ρ ⊢Δ x)
  wkConv↓Term {ρ} [ρ] ⊢Δ (ne-ins t u x x₁) =
    ne-ins (wkTerm [ρ] ⊢Δ t) (wkTerm [ρ] ⊢Δ u) (wkNeutral ρ x) (wk~↓ [ρ] ⊢Δ x₁)
  wkConv↓Term ρ ⊢Δ (univ x x₁ x₂) =
    univ (wkTerm ρ ⊢Δ x) (wkTerm ρ ⊢Δ x₁) (wkConv↓ ρ ⊢Δ x₂)
  wkConv↓Term ρ ⊢Δ (zero-refl x) = zero-refl ⊢Δ
  wkConv↓Term ρ ⊢Δ (suc-cong t<>u) = suc-cong (wkConv↑Term ρ ⊢Δ t<>u)
  wkConv↓Term {ρ} {Δ = Δ} [ρ] ⊢Δ (η-eq {F = F} {G = G} x₁ x₂ y y₁ t<>u) =
    let ⊢F , _ = syntacticΠ (syntacticTerm x₁)
        ⊢ρF = wk [ρ] ⊢Δ ⊢F
    in  η-eq (wkTerm [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂)
             (wkFunction ρ y) (wkFunction ρ y₁)
             (PE.subst₃ (λ x y z → Δ ∙ U.wk ρ F ⊢ x [conv↑] y ∷ z)
                        (PE.cong₂ _∘_ (PE.sym (wk1-wk≡lift-wk1 _ _)) PE.refl)
                        (PE.cong₂ _∘_ (PE.sym (wk1-wk≡lift-wk1 _ _)) PE.refl)
                        PE.refl
                        (wkConv↑Term (lift [ρ]) (⊢Δ ∙ ⊢ρF) t<>u))
  wkConv↓Term {ρ} [ρ] ⊢Δ (Σ-η {G = G} ⊢p ⊢r pProd rProd fstConv sndConv) =
    Σ-η (wkTerm [ρ] ⊢Δ ⊢p)
        (wkTerm [ρ] ⊢Δ ⊢r)
        (wkProduct ρ pProd)
        (wkProduct ρ rProd)
        (wkConv↑Term [ρ] ⊢Δ fstConv)
        (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x)
                  (wk-β G)
                  (wkConv↑Term [ρ] ⊢Δ sndConv))
  wkConv↓Term {ρ} [ρ] ⊢Δ (η-unit [t] [u] tWhnf uWhnf) =
    η-unit (wkTerm [ρ] ⊢Δ [t]) (wkTerm [ρ] ⊢Δ [u])
           (wkWhnf ρ tWhnf) (wkWhnf ρ uWhnf)

ext: agda


text:
-- Instances of Gaussian integers.

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

module GauInt.Instances where

open import Data.Integer using (+_ ; -[1+_] ; +[1+_])
open import Data.Nat using (suc )

open import Instances
open import GauInt.Base renaming (-_ to -𝔾_ ; _-_ to _-𝔾_ ; _+_ to _+𝔾_ ; _*_ to _*𝔾_ ; NonZero to NonZero𝔾 ; rank to rank𝔾)

-- Instances to overload operations.
instance
  sr𝔾 : SemiRing 𝔾
  _+_ {{sr𝔾}} = _+𝔾_
  _*_ {{sr𝔾}} = _*𝔾_
  0# {{sr𝔾}} = 0𝔾
  1# {{sr𝔾}} = 1𝔾

instance
  ring𝔾 : Ring 𝔾
  ring𝔾 .sra = sr𝔾
  ring𝔾 .-_ = -𝔾_

instance
  Rank𝔾 : Rank 𝔾
  Rank𝔾 .rank = rank𝔾

-- This depends on how the boolean equality on 𝔾 is defined. To be
-- precise, it depends on the order of comparing the components.
instance
  nzp : ∀ {n} {y} -> NonZero𝔾 (+ suc n + y i)
  nzp = _

  nzn : ∀ {n} {y} -> NonZero𝔾 (-[1+ n ] + y i)
  nzn = _

  nzpi : ∀ {n} -> NonZero𝔾 (0# + (+ suc n) i)
  nzpi = _

  nzni : ∀ {n} -> NonZero𝔾 (0# + (-[1+ n ]) i)
  nzni = _

instance
  NZT𝔾 : NonZeroTypeclass 𝔾
  NZT𝔾 .NonZero = NonZero𝔾

{-

-- Translation from NonZero predicate to non-equality.
test-t : ∀ (x : 𝔾) -> .{{NonZero x}} -> ¬ x ≡ 0#
test-t (+_ zero + +[1+ n ] i) = λ {()}
test-t (+_ zero + -[1+_] n i) = λ {()}
test-t (+[1+ n ] + x₁ i) = λ {()}
test-t (-[1+_] n + x₁ i) = λ {()}

open import Relation.Binary.Structures
open IsDecEquivalence {{...}}
open IsDecTotalOrder {{...}}
open import Data.Nat.Instances
open import Data.Integer.Instances
test : {!!}
test = 0ℤ ≤? 0ℤ

-}

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sum
open import Cubical.Data.Unit

module Coequalizers where

record Graph {ℓ ℓ' : Level} (E : Type ℓ) (V : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    π₀ : E → V
    π₁ : E → V

open Graph ⦃...⦄

data Coeq {ℓ ℓ' : Level} {V : Type ℓ} {E : Type ℓ'} (ev : Graph E V) :
          Type (ℓ-max ℓ ℓ')  where
  c[_] : V → (Coeq ev)
  quot : (e : E) → c[ (Graph.π₀ ev e) ] ≡ c[ (Graph.π₁ ev e) ]

_/_ : {ℓ ℓ' : Level} (V : Type ℓ) (E : Type ℓ') ⦃ ev : Graph E V ⦄ →
         Type (ℓ-max ℓ ℓ')
_/_ V E ⦃ ev ⦄ = Coeq ev

infix 25 _/_

module CoprodCoeq {ℓ ℓ' ℓ'' : Level} (E₀ : Type ℓ) (E₁ : Type ℓ') (V : Type ℓ'')
  ⦃ ev : Graph (E₀ ⊎ E₁) V ⦄ where
  instance
    evE₀ : Graph E₀ V
    evE₀ = record { π₀ = π₀ ∘ inl ; π₁ = π₁ ∘ inl }

    ev-snd : Graph E₁ (V / E₀)
    ev-snd = record { π₀ = c[_] ∘ π₀ ∘ inr ; π₁ = c[_] ∘ π₁ ∘ inr }

  coeq-coprod-equiv : V / (E₀ ⊎ E₁) ≃ (V / E₀) / E₁
  coeq-coprod-equiv = isoToEquiv (iso f g f-g g-f)
    where
      f : V / (E₀ ⊎ E₁) → (V / E₀) / E₁
      f c[ x ] = c[ c[ x ] ]
      f (quot (inl e) i) = c[ quot e i ]
      f (quot (inr e) i) = quot e i

      g : (V / E₀) / E₁ →  V / (E₀ ⊎ E₁)
      g c[ c[ x ] ] = c[ x ]
      g c[ quot e i ] = quot (inl e) i
      g (quot e i) = quot (inr e) i

      f-g : (z : (V / E₀) / E₁) → (f (g z) ≡ z)
      f-g c[ c[ x ] ] = refl
      f-g c[ quot e i ] = refl
      f-g (quot e i) = refl

      g-f : (z : V / (E₀ ⊎ E₁)) → (g (f z) ≡ z)
      g-f c[ x ] = refl
      g-f (quot (inl e) i) = refl
      g-f (quot (inr e) i) = refl

module TrivialExtension {ℓ ℓ' : Level} (V : Type ℓ) (v : V) where
  instance
    evt-l : Graph Unit (V ⊎ Unit)
    evt-l = record { π₀ = λ x → inl v ; π₁ = inr }

    evt-r : Graph Unit (Unit ⊎ V)
    evt-r = record { π₀ = inl ; π₁ = λ _ → inr v }

  te-equiv-l : V ≃ (V ⊎ Unit) / Unit
  te-equiv-l = isoToEquiv (iso (c[_] ∘ inl) g f-g (λ _ → refl))
    where
      g : (V ⊎ Unit) / Unit → V
      g c[ inl x ] = x
      g c[ inr x ] = v
      g (quot e i) = v

      f-g : (z : (V ⊎ Unit) / Unit) → c[ inl (g z) ] ≡ z
      f-g c[ inl x ] = refl
      f-g c[ inr x ] = quot x
      f-g (quot e i) j = quot e (i ∧ j)

  te-equiv-r : V ≃ (Unit ⊎ V) / Unit
  te-equiv-r = isoToEquiv (iso (c[_] ∘ inr) g f-g λ _ → refl)
    where
      g : (Unit ⊎ V) / Unit → V
      g c[ inl x ] = v
      g c[ inr x ] = x
      g (quot e i) = v

      f-g : (z : (Unit ⊎ V) / Unit) → c[ inr (g z) ] ≡ z
      f-g c[ inl x ] i = quot x (~ i)
      f-g c[ inr x ] = refl
      f-g (quot e i) j = quot e (i ∨ ~ j)

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

open import Level

open import Axiom.ExcludedMiddle
open import Axiom.Extensionality.Propositional

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

module Common where

postulate
  excluded-middle : ExcludedMiddle Level.zero
  extensionality : Extensionality Level.zero (Level.suc Level.zero)

record Message (ℙ : Set) : Set where
  infix 4 _?=_
  field
    _?=_ : (x y : ℙ) -> Dec (x ≡ y)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module _ where

module M where

  data D : Set where
    d : D

  private
    instance
      x : D
      x = d

! : ⦃ _ : M.D ⦄ → M.D
! ⦃ x ⦄ = x

y : M.D
y = !

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Constructive.SequentCalculus (𝔏 : Signature) where
open Signature(𝔏)

open import Data.Option
open import Data.List
open import Data.List.Functions using (map) renaming (singleton to · ; _++_ to _∪_)
open import Data.List.Relation.Permutation
import      Data.ListSized as S
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Formalization.PredicateLogic.Syntax.Substitution(𝔏)
open import Functional as Fn using ()
import      Lvl
open import Numeral.Natural
open import Type

private variable ℓ : Lvl.Level
private variable args n vars vars₁ vars₂ : ℕ
private variable Γ Γ₁ Γ₂ Γ₃ : List(Formula(vars))
private variable Δ Δ₁ Δ₂ Δ₃ : Option(Formula(vars))
private variable φ φ₁ φ₂ ψ A B C : Formula(vars)
private variable p : Prop(n)
private variable f : Prop(args)
private variable x : S.List(Term(vars))(args)

_∪·_ : ∀{T : Type{ℓ}} → List(T) → T → List(T)
_∪·_ = Fn.swap(_⊰_)
infixl 1000 _∪·_

module Variant1 where
  data _⇒_ : List(Formula(vars)) → Option(Formula(vars)) → Type{Lvl.𝐒(ℓₚ Lvl.⊔ ℓₒ)} where
    axiom : ((· φ) ⇒ Some(φ))

    weakenₗ : (Γ ⇒ Δ) → ((Γ ∪· A) ⇒ Δ)
    permuteₗ : (Γ₁ permutes Γ₂) → (Γ₁ ⇒ Δ) → (Γ₂ ⇒ Δ)
    contractₗ : ((Γ ∪· A ∪· A) ⇒ Δ) → ((Γ ∪· A) ⇒ Δ)
    ⊥ₗ : (Γ ∪· ⊥) ⇒ None
    ∧ₗₗ : ((Γ ∪· A) ⇒ Δ) → ((Γ ∪· (A ∧ B)) ⇒ Δ)
    ∧ₗᵣ : ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ∧ B)) ⇒ Δ)
    ∨ₗ : ((Γ ∪· A) ⇒ Δ) → ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ∨ B)) ⇒ Δ)
    ⟶ₗ : (Γ ⇒ Some(A)) → ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ⟶ B)) ⇒ Δ)
    Ɐₗ : ∀{t} → ((Γ ∪· (substitute0 t A)) ⇒ Δ) → ((Γ ∪· (Ɐ A)) ⇒ Δ)
    ∃ₗ : ∀{v}{n} → ((Γ ∪· (substituteN n (var v) A)) ⇒ Δ) → ((Γ ∪· (∃ A)) ⇒ Δ)

    weakenᵣ : (Γ ⇒ None) → (Γ ⇒ Some(A))
    ⊤ᵣ : ∅ ⇒ Some(⊤ {vars})
    ∧ᵣ : (Γ ⇒ Some(A)) → (Γ ⇒ Some(B)) → (Γ ⇒ Some(A ∧ B))
    ∨ᵣₗ : (Γ ⇒ Some(A)) → (Γ ⇒ Some(A ∨ B))
    ∨ᵣᵣ : (Γ ⇒ Some(B)) → (Γ ⇒ Some(A ∨ B))
    ⟶ᵣ : ((Γ ∪· A) ⇒ Some(B)) → (Γ ⇒ Some(A ⟶ B))
    Ɐᵣ : ∀{v}{n} → (Γ ⇒ Some((substituteN n (var v) A))) → (Γ ⇒ Some(Ɐ A))
    ∃ᵣ : ∀{t} → (Γ ⇒ Some((substitute0 t A))) → (Γ ⇒ Some(∃ A))

  import Logic.Propositional as Meta

  no-empty-refl : Meta.¬(∅ ⇒ None{T = Formula vars})
  no-empty-refl (permuteₗ perm p) rewrite Proofs.permutes-on-empty perm = no-empty-refl p

  {-
  no-callCC : Meta.¬(∅ ⇒ Some(((A ⟶ B) ⟶ A) ⟶ A))
  no-callCC (permuteₗ perm p) rewrite permutes-on-empty perm = no-callCC p
  no-callCC (weakenᵣ (permuteₗ perm p)) rewrite permutes-on-empty perm = no-empty-refl p
  no-callCC (⟶ᵣ p) = no-callCC {!!}
  {-no-callCC (⟶ᵣ (weakenₗ p)) = {!!}
  no-callCC (⟶ᵣ (permuteₗ x p)) = {!!}
  no-callCC (⟶ᵣ (contractₗ p)) = {!!}
  no-callCC (⟶ᵣ (⟶ₗ p p₁)) = {!!}
  no-callCC (⟶ᵣ (weakenᵣ p)) = {!!}
  no-callCC (⟶ᵣ (∧ᵣ p p₁)) = {!!}
  no-callCC (⟶ᵣ (∨ᵣₗ p)) = {!!}
  no-callCC (⟶ᵣ (∨ᵣᵣ p)) = {!!}
  no-callCC (⟶ᵣ (⟶ᵣ p)) = {!!}
  no-callCC (⟶ᵣ (Ɐᵣ p)) = {!!}
  no-callCC (⟶ᵣ (∃ᵣ p)) = {!!}
  -}
  -}

module Variant3 where
  -- Note: Because this formalization is non-standard, a problem arises for Formula(𝟎): It it missing some of the quantification rules because it has no variables.
  data _⇒_ : List(Formula(vars)) → Formula(vars) → Type{Lvl.𝐒(ℓₚ Lvl.⊔ ℓₒ)} where
    axiom : ((Γ ∪· (f $ x)) ⇒ (f $ x))

    permuteₗ : (Γ₁ permutes Γ₂) → (Γ₁ ⇒ C) → (Γ₂ ⇒ C)
    ⊥ₗ : (Γ ∪· ⊥) ⇒ A
    ∧ₗ : ((Γ ∪· A ∪· B) ⇒ C) → ((Γ ∪· (A ∧ B)) ⇒ C)
    ∨ₗ : ((Γ ∪· A) ⇒ C) → ((Γ ∪· B) ⇒ C) → ((Γ ∪· (A ∨ B)) ⇒ C)
    ⟶ₗ : ((Γ ∪· (A ⟶ B)) ⇒ A) → ((Γ ∪· B) ⇒ C) → ((Γ ∪· (A ⟶ B)) ⇒ C)
    Ɐₗ : ∀{t} → ((Γ ∪· (substitute0 t A) ∪· (Ɐ A)) ⇒ C) → ((Γ ∪· (Ɐ A)) ⇒ C)
    ∃ₗ : ∀{n}{v} → ((Γ ∪· (substituteN n (var v) A)) ⇒ C) → ((Γ ∪· (∃ A)) ⇒ C)

    ⊤ᵣ : Γ ⇒ (⊤ {vars})
    ∧ᵣ : (Γ ⇒ A) → (Γ ⇒ B) → (Γ ⇒ (A ∧ B))
    ∨ᵣₗ : (Γ ⇒ A) → (Γ ⇒ (A ∨ B))
    ∨ᵣᵣ : (Γ ⇒ B) → (Γ ⇒ (A ∨ B))
    ⟶ᵣ : ((Γ ∪· A) ⇒ B) → (Γ ⇒ (A ⟶ B))
    Ɐᵣ : ∀{n}{v} → (Γ ⇒ (substituteN n (var v) A)) → (Γ ⇒ (Ɐ A))
    ∃ᵣ : ∀{t} → (Γ ⇒ (substitute0 t A)) → (Γ ⇒ (∃ A))

  import      Logic.Propositional as Meta
  open import Numeral.Finite
  open import Type.Properties.Inhabited

  weakenₗ : (Γ ⇒ ψ) → ((Γ ∪· φ) ⇒ ψ)
  weakenₗ axiom          = permuteₗ swap axiom
  weakenₗ (permuteₗ x p) = permuteₗ (prepend x) (weakenₗ p)
  weakenₗ ⊥ₗ             = permuteₗ swap ⊥ₗ
  weakenₗ (∧ₗ p)         = permuteₗ swap (∧ₗ(permuteₗ (trans swap (prepend swap)) (weakenₗ p)))
  weakenₗ (∨ₗ p q)       = permuteₗ swap (∨ₗ (permuteₗ swap (weakenₗ p)) (permuteₗ swap (weakenₗ q)))
  weakenₗ (⟶ₗ p q)       = permuteₗ swap (⟶ₗ (permuteₗ swap (weakenₗ p)) (permuteₗ swap (weakenₗ q)))
  weakenₗ (Ɐₗ p)         = permuteₗ swap (Ɐₗ (permuteₗ (trans swap (prepend swap)) (weakenₗ p)))
  weakenₗ (∃ₗ{n = n} p)  = permuteₗ swap (∃ₗ{n = n} (permuteₗ swap (weakenₗ p)))
  weakenₗ ⊤ᵣ             = ⊤ᵣ
  weakenₗ (∧ᵣ  p q)      = ∧ᵣ (weakenₗ p) (weakenₗ q)
  weakenₗ (∨ᵣₗ p)        = ∨ᵣₗ (weakenₗ p)
  weakenₗ (∨ᵣᵣ p)        = ∨ᵣᵣ (weakenₗ p)
  weakenₗ (⟶ᵣ  p)        = ⟶ᵣ (permuteₗ swap (weakenₗ p))
  weakenₗ (Ɐᵣ{n = n} p)  = Ɐᵣ{n = n} (weakenₗ p)
  weakenₗ (∃ᵣ  p)        = ∃ᵣ (weakenₗ p)

  weaken-union : (Γ₂ ⇒ φ) → ((Γ₁ ∪ Γ₂) ⇒ φ)
  weaken-union {Γ₁ = ∅}      p = p
  weaken-union {Γ₁ = φ ⊰ Γ₁} p = weakenₗ (weaken-union {Γ₁ = Γ₁} p)

  open import Formalization.PredicateLogic.Syntax.Tree(𝔏)
  open import Numeral.Natural.Relation.Order
  open import Numeral.Natural.Relation.Order.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Structure.Function
  open import Structure.Relator.Properties
  open import Syntax.Function

  direct₊ : ∀{φ : Formula(𝐒(vars))} → ((Γ ∪· φ) ⇒ φ)
  direct₊{Γ = Γ}{φ = φ} = induction-on-height(P) (\{vars}{φ} → proof{vars}{φ}) \() where
    P = \{vars} (φ : Formula(vars)) → (vars ≢ 𝟎) → ∀{Γ} → (Γ ∪· φ) ⇒ φ
    proof : ∀{φ : Formula(vars)} → (∀{vars}{ψ : Formula(vars)} → (height ψ < height φ) → P(ψ)) → P(φ)
    proof {𝟎}               _    nz with () ← nz [≡]-intro
    proof {𝐒 _} {φ = f $ x} prev _  = axiom
    proof {𝐒 _} {φ = ⊤}     prev _  = weakenₗ ⊤ᵣ
    proof {𝐒 _} {φ = ⊥}     prev _  = ⊥ₗ
    proof {𝐒 _} {φ = φ ∧ ψ} prev nz = ∧ᵣ (∧ₗ (permuteₗ swap (prev (∧-height-orderₗ{φ = φ}{ψ = ψ}) nz))) (∧ₗ (prev (∧-height-orderᵣ{ψ = ψ}{φ = φ}) nz))
    proof {𝐒 _} {φ = φ ∨ ψ} prev nz = ∨ₗ (∨ᵣₗ (prev (∨-height-orderₗ{φ = φ}{ψ = ψ}) nz)) (∨ᵣᵣ (prev (∨-height-orderᵣ{ψ = ψ}{φ = φ}) nz))
    proof {𝐒 _} {φ = φ ⟶ ψ} prev nz = ⟶ᵣ (permuteₗ swap (⟶ₗ (permuteₗ swap (prev (⟶-height-orderₗ{φ = φ}{ψ = ψ}) nz)) (prev (⟶-height-orderᵣ{ψ = ψ}{φ = φ}) nz)))
    proof {𝐒 v} {φ = Ɐ φ}   prev nz = Ɐᵣ{n = 𝟎}{v = 𝟎} (Ɐₗ{t = var 𝟎} (weakenₗ (prev (subtransitivityₗ(_≤_)(_≡_) (congruence₁(𝐒) (substitute-height{φ = φ})) (Ɐ-height-order{φ = φ})) nz)))
    proof {𝐒 v} {φ = ∃ φ}   prev nz = ∃ᵣ{t = var 𝟎} (∃ₗ{n = 𝟎}{v = 𝟎} (prev (subtransitivityₗ(_≤_)(_≡_) (congruence₁(𝐒) (substitute-height{φ = φ})) (Ɐ-height-order{φ = φ})) nz))

  no-empty-refl : Meta.¬(∅ ⇒ (⊥ {vars}))
  no-empty-refl (permuteₗ perm p) rewrite Proofs.permutes-on-empty perm = no-empty-refl p

  no-empty-axiomₗ : Meta.¬(·(p $ x) ⇒ ⊥)
  no-empty-axiomₗ (permuteₗ perm p) rewrite Proofs.permutes-on-singleton perm = no-empty-axiomₗ p

  no-empty-axiomᵣ : Meta.¬(∅ ⇒ (p $ x))
  no-empty-axiomᵣ (permuteₗ perm p) rewrite Proofs.permutes-on-empty perm = no-empty-axiomᵣ p

  no-negated-axiomᵣ : Meta.¬(∅ ⇒ (¬(p $ x)))
  no-negated-axiomᵣ (permuteₗ perm p) rewrite Proofs.permutes-on-empty perm = no-negated-axiomᵣ p
  no-negated-axiomᵣ (⟶ᵣ p) = no-empty-axiomₗ p

  -- 3.5.2
  substitute-proof : ∀{t : 𝕟(vars₁) → Term(vars₂)} → (Γ ⇒ φ) → ((map(substitute t) Γ) ⇒ (substitute t φ))
  substitute-proof p = {!!}

  module _ ⦃ pos-prop : ◊(Prop(0)) ⦄ where
    no-excludedMiddle : Meta.¬(∀{A : Formula(vars)} → (∅ ⇒ (A ∨ (¬ A))))
    no-excludedMiddle as = proof(as{[◊]-existence $ S.∅}) where
      proof : Meta.¬(∅ ⇒ ((p $ x) ∨ ¬(p $ x)))
      proof (permuteₗ perm q)            rewrite Proofs.permutes-on-empty perm = proof q
      proof (∨ᵣₗ (permuteₗ perm q))      rewrite Proofs.permutes-on-empty perm = no-empty-axiomᵣ q
      proof (∨ᵣᵣ (permuteₗ perm q))      rewrite Proofs.permutes-on-empty perm = no-negated-axiomᵣ q
      proof (∨ᵣᵣ (permuteₗ perm (⟶ᵣ q))) rewrite Proofs.permutes-on-empty perm = no-empty-axiomₗ q
      proof (∨ᵣᵣ (⟶ᵣ (permuteₗ perm q))) rewrite Proofs.permutes-on-singleton perm = no-empty-axiomₗ q

    no-doubleNegation : Meta.¬(∀{A : Formula(vars)} → (∅ ⇒ ((¬ ¬ A) ⟶ A)))
    no-doubleNegation as = proof(as{[◊]-existence $ S.∅}) where
      proof : Meta.¬(∅ ⇒ ((¬ ¬(p $ x)) ⟶ (p $ x)))
      proof (permuteₗ perm q) rewrite Proofs.permutes-on-empty perm = proof q
      proof (⟶ᵣ (permuteₗ perm q)) = {!!}
      proof (⟶ᵣ (⟶ₗ q (permuteₗ perm q₁))) = {!!}
      proof (⟶ᵣ (⟶ₗ (permuteₗ perm q) ⊥ₗ)) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ₗ q q₁) ⊥ₗ)) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ᵣ q) ⊥ₗ)) = {!!}

    test : ∀{T : Type{ℓ}} → (Γ₁ permutes Γ₂) → ((Γ₁ ⇒ φ) → T) → ((Γ₂ ⇒ φ) → T)
    test perm p1 p2 = p1 (permuteₗ (symmetry(_permutes_) perm) p2)
    {-# INLINE test #-}

    no-callCC : Meta.¬(∀{A B : Formula(vars)} → (∅ ⇒ ((A ⟶ B) ⟶ A) ⟶ A))
    no-callCC as = proof(as{[◊]-existence $ S.∅}{⊥}) where
      proof2 : Meta.¬((∅ ∪· ((p $ x ⟶ ⊥) ⟶ p $ x) ∪· p $ x) ⇒ ⊥)
      proof2 (permuteₗ x t) = {!t!}

      proof3 : Meta.¬((∅ ∪· p $ x ∪· ((p $ x ⟶ ⊥) ⟶ p $ x)) ⇒ ⊥)
      proof3 (permuteₗ perm p) = {!!}
      proof3 (⟶ₗ p q) = {!!}

      proof : Meta.¬(∅ ⇒ (((p $ x) ⟶ ⊥) ⟶ (p $ x)) ⟶ (p $ x))
      proof (permuteₗ perm q) rewrite Proofs.permutes-on-empty perm = proof q
      proof (⟶ᵣ (permuteₗ perm q)) rewrite Proofs.permutes-on-singleton perm = {!!}
      proof (⟶ᵣ (⟶ₗ (permuteₗ perm q) q₁)) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ₗ q (permuteₗ x r)) s)) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ₗ q (⟶ᵣ r)) s)) = no-empty-axiomₗ (contract-axiom-bottom r) where
        contract-axiom-bottom : ((·(p $ x) ∪· (p $ x)) ⇒ ⊥) → (·(p $ x) ⇒ ⊥)
        contract-axiom-bottom (permuteₗ x p) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ perm q)) r)) = proof2 (permuteₗ perm q)

      -- proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ perm q)) r)) = test (trans swap (symmetry(_permutes_) perm)) (proof ↦ {!⟶ᵣ proof!}) q
      {-proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ perm q)) r)) = test (symmetry(_permutes_) perm) proof2 q where
        proof2 : Meta.¬((∅ ∪· ((p $ x ⟶ ⊥) ⟶ p $ x) ∪· p $ x) ⇒ ⊥)
        proof2 (permuteₗ perm p) = test (symmetry(_permutes_) perm) proof2 p-}

      {-proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ (prepend perm) q)) r)) rewrite permutes-on-singleton perm = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ swap (permuteₗ perm q))) r)) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ swap (⟶ₗ q₁ (permuteₗ perm q₂)))) r)) = {!!}
      proof (⟶ᵣ (⟶ₗ (⟶ᵣ (permuteₗ (trans perm₁ perm₂) q)) r)) = {!!}-}

     --⟶ₗ : ((Γ ∪· (A ⟶ B)) ⇒ A) → ((Γ ∪· B) ⇒ A) → ((Γ ∪· (A ⟶ B)) ⇒ A)

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:
-- Andreas, 2020-09-26, issue #4946.
-- More liberal type signatures for constructors of sized types.

-- {-# OPTIONS -v tc.polarity:20 #-}

open import Agda.Builtin.Size

variable
  i : Size
  A : Set

data T : Size → Set → Set where
  c : A → T i A → T (↑ i) A

-- The type of the constructor c is elaborated to
--
--   c : {A : Set} {i : Set} → A → T i A → T (↑ i) A
--
-- Thus, the size argument i is not the first.
-- Nevertheless, Agda recognize the first argument of T
-- as covariant.

test : T i A → T ∞ A
test x = x

-- Should pass.

max_forks_repo_name: shlevy/agda


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

open import Cubical.Relation.Nullary.Base public
open import Cubical.Relation.Nullary.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Pullback where

open import Logic.Equivalence
open import Logic.Relations
open import Logic.Base
open import Category
open import Unique

module Pull (ℂ : Cat) where

  private open module CC = Category.Category ℂ
  private open module U = Uniq ℂ

  record isPull {A B C D A' : Obj}(f : A ─→ B)(g : A ─→ C)(f' : C ─→ D)(g' : B ─→ D)(h₁ : A' ─→ C)(h₂ : A' ─→ B)(commut : f' ∘ h₁ == g' ∘ h₂) : Set1 where
    field unique  : ∃! \(h : A' ─→ A) -> (g ∘ h == h₁) /\ (f ∘ h == h₂)

  record pullback {B C D : Obj}(g' : B ─→ D)(f' : C ─→ D) : Set1 where
    field
      A    : Obj
      f    : A ─→ B
      g    : A ─→ C
      comm : g' ∘ f == f' ∘ g
      pull : (forall {A' : Obj}(h₁ : A' ─→ C)(h₂ : A' ─→ B)(commut : f' ∘ h₁ == g' ∘ h₂) -> isPull f g f' g' h₁ h₂ commut)

  record PullCat : Set2 where
    field pull : {B C D : Obj}(g' : B ─→ D)(f' : C ─→ D) -> pullback g' f'


text:
------------------------------------------------------------------------------
-- Co-inductive natural numbers
------------------------------------------------------------------------------

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

module GFPs.Conat where

open import FOTC.Base
open import FOTC.Base.PropertiesI

------------------------------------------------------------------------------
-- Conat is a greatest fixed-point of a functor

-- The functor.
NatF : (D → Set) → D → Set
NatF A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')

-- The co-natural numbers are the greatest fixed-point of NatF.
postulate
  Conat : D → Set

  -- Conat is a post-fixed point of NatF, i.e.
  --
  -- Conat ≤ NatF Conat.
  Conat-out : ∀ {n} → Conat n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')

  -- The higher-order version.
  Conat-out-ho : ∀ {n} → Conat n → NatF Conat n

  -- Conat is the greatest post-fixed point of NatF, i.e.
  --
  -- ∀ A. A ≤ NatF A ⇒ A ≤ Conat.
  Conat-coind :
    (A : D → Set) →
    -- A is post-fixed point of ConatF.
    (∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
    -- Conat is greater than A.
    ∀ {n} → A n → Conat n

  -- The higher-order version.
  Conat-coind-ho :
    (A : D → Set) → (∀ {n} → A n → NatF A n) → ∀ {n} → A n → Conat n

  -- 22 December 2013. This is a stronger induction principle. If we
  -- use it, we can use the trivial predicate A = λ x → x ≡ x in the
  -- proofs. Unfortunately, we don't have a justification/proof for
  -- this principle.
  Conat-stronger-coind₁ :
    ∀ (A : D → Set) {n} →
    (A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
    A n → Conat n

  -- Other stronger co-induction principle
  --
  -- Adapted from (Paulson, 1997. p. 16).
  Conat-stronger-coind₂ :
    (A : D → Set) →
    (∀ {n} → A n → (n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) ∨ Conat n) →
    ∀ {n} → A n → Conat n

------------------------------------------------------------------------------
-- Conat-out and Conat-out-ho are equivalents

Conat-out-fo : ∀ {n} → Conat n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')
Conat-out-fo = Conat-out-ho

Conat-out-ho' : ∀ {n} → Conat n → NatF Conat n
Conat-out-ho' = Conat-out

------------------------------------------------------------------------------
-- Conat-coind and Conat-coind-ho are equivalents

Conat-coind-fo :
  (A : D → Set) →
  (∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
  ∀ {n} → A n → Conat n
Conat-coind-fo = Conat-coind-ho

Conat-coind-ho' :
  (A : D → Set) → (∀ {n} → A n → NatF A n) → ∀ {n} → A n → Conat n
Conat-coind-ho' = Conat-coind

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Conat predicate is also a pre-fixed point of the functional NatF,
-- i.e.
--
-- NatF Conat ≤ Conat.
Conat-in : ∀ {n} →
           n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n') →
           Conat n
Conat-in h = Conat-coind A h' h
  where
  A : D → Set
  A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')

  h' : ∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')
  h' (inj₁ n≡0)              = inj₁ n≡0
  h' (inj₂ (n' , prf , Cn')) = inj₂ (n' , prf , Conat-out Cn')

-- The higher-order version.
Conat-in-ho : ∀ {n} → NatF Conat n → Conat n
Conat-in-ho = Conat-in

-- A different definition.
Conat-in' : (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')) →
            ∀ {n} → Conat n
Conat-in' h = Conat-coind (λ m → m ≡ m) (h' h) refl
  where
  h' : (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')) →
       ∀ {m} → m ≡ m → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ m' ≡ m')
  h' h'' {m} _ with (h'' {m})
  ... | inj₁ m≡0            = inj₁ m≡0
  ... | inj₂ (m' , prf , _) = inj₂ (m' , prf , refl)

Conat-in-ho' : (∀ {n} → NatF Conat n) → ∀ {n} → Conat n
Conat-in-ho' = Conat-in'

------------------------------------------------------------------------------
-- From Conat-coind/Conat-stronger-coind₁ to Conat-stronger-coind₁/Conat-coind

Conat-coind'' :
  (A : D → Set) →
  (∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
  ∀ {n} → A n → Conat n
Conat-coind'' A h An = Conat-stronger-coind₁ A h An

-- 22 December 2013: We couln't prove Conat-stronger-coind₁ using
-- Conat-coind.
Conat-stronger-coind₁' :
  ∀ (A : D → Set) {n} →
  (A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
  A n → Conat n
Conat-stronger-coind₁' A {n} h An = Conat-in (case prf₁ prf₂ (h An))
  where
  prf₁ : n ≡ zero → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')
  prf₁ n≡0 = inj₁ n≡0

  prf₂ : ∃[ n' ] n ≡ succ₁ n' ∧ A n' →
         n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')
  prf₂ (n' , prf , An') = inj₂ (n' , prf , {!!})

------------------------------------------------------------------------------
-- From Conat-stronger-coind₂ to Conat-stronger-coind₁

-- 13 January 2014: We couln't prove Conat-stronger-coind₁ using
-- Conat-stronger-coind₂.
Conat-stronger-coind₁'' :
  ∀ (A : D → Set) {n} →
  (A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
  A n → Conat n
Conat-stronger-coind₁'' A h An = Conat-stronger-coind₂ A {!!} An

------------------------------------------------------------------------------
-- References
--
-- Paulson, L. C. (1997). Mechanizing Coinduction and Corecursion in
-- Higher-order Logic. Journal of Logic and Computation 7.2,
-- pp. 175–204.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Initial {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

record Initial : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊥ : Obj
    ! : ∀ {A} → (⊥ ⇒ A)
    .!-unique : ∀ {A} → (f : ⊥ ⇒ A) → ! ≡ f

  .!-unique₂ : ∀ {A} → (f g : ⊥ ⇒ A) → f ≡ g
  !-unique₂ f g =
      begin
        f
      ↑⟨ !-unique f ⟩
        !
      ↓⟨ !-unique g ⟩
        g
      ∎
    where
    open HomReasoning

  .⊥-id : (f : ⊥ ⇒ ⊥) → f ≡ id
  ⊥-id f = !-unique₂ f id

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Data.Graph

module Data.Graph.Path.Cut {ℓᵥ ℓₑ} (g : FiniteGraph ℓᵥ ℓₑ) where

open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.Fin.Properties as Fin-Props using (pigeonhole)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Any as Any using (Any; here; there)
open import Data.List.Membership.Propositional as ∈L renaming (_∈_ to _∈L_)
open import Data.Nat as ℕ
open import Data.Nat.Properties as ℕ-Props
open import Data.Product as Σ
open import Data.Sum as ⊎
open import Finite
import Finite.Pigeonhole
open import Function
open import Induction.Nat
open import Induction.WellFounded
import Level as ℓ
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PreorderReasoning ≤-preorder
open import Relation.Nullary hiding (module Dec)
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation

open FiniteGraph g
open IsFinite

infix 3 _∈_
data _∈_ x : ∀ {a b n} → Path a b n → Set where
  here : ∀ {b c n} {e : Edge x b} {p : Path b c n} → x ∈ e ∷ p
  there : ∀ {a b c n} {e : Edge a b} {p : Path b c n} → x ∈ p → x ∈ e ∷ p

infix 3 _∈?_
_∈?_ : ∀ {a b n} x (p : Path a b n) → Dec (x ∈ p)
x ∈? [] = no λ ()
_∈?_ {a} x (e ∷ p) =
  case decEqVertex a x of λ where
    (yes refl) → yes here
    (no a≢x) →
      case x ∈? p of λ where
        (yes i) → yes (there i)
        (no ¬i) →
          no λ where
            here → contradiction refl a≢x
            (there i) → contradiction i ¬i

index : ∀ {a b x n} {p : Path a b n} → x ∈ p → Fin n
index here = zero
index (there i) = suc (index i)

lookup : ∀ {a b n} → Path a b n → Fin n → Vertex
lookup {a} (e ∷ p) zero = a
lookup (e ∷ p) (suc i) = lookup p i

∈-lookup : ∀ {a b n} {p : Path a b n} (i : Fin n) → lookup p i ∈ p
∈-lookup {p = []} ()
∈-lookup {p = e ∷ p} zero = here
∈-lookup {p = e ∷ p} (suc i) = there (∈-lookup i)

finiteIndex : ∀ {a b n} (p : Path a b n) → Fin n → Fin (size vertexFinite)
finiteIndex p = Any.index ∘ membership vertexFinite ∘ lookup p

prefixLength : ∀ {a b x n} {p : Path a b n} → x ∈ p → ℕ
prefixLength here = zero
prefixLength (there i) = suc (prefixLength i)

suffixLength : ∀ {a b x n} {p : Path a b n} → x ∈ p → ℕ
suffixLength {n = n} here = n
suffixLength (there i) = suffixLength i

split : ∀ {a b x n} {p : Path a b n}
  (i : x ∈ p) →
  Path a x (prefixLength i) × Path x b (suffixLength i)
split {p = p} here = [] , p
split {p = e ∷ p} (there i) = Σ.map₁ (e ∷_) (split i)

prefix : ∀ {a b x n} {p : Path a b n} (i : x ∈ p) → Path a x (prefixLength i)
prefix = proj₁ ∘ split

suffix : ∀ {a b x n} {p : Path a b n} (i : x ∈ p) → Path x b (suffixLength i)
suffix = proj₂ ∘ split

splitLengthsAddUp : ∀ {a b x n} {p : Path a b n}
  (i : x ∈ p) →
  n ≡ prefixLength i + suffixLength i
splitLengthsAddUp here = refl
splitLengthsAddUp (there i) = cong suc (splitLengthsAddUp i)

data Repeats : ∀ {a b n} → Path a b n → Set where
  here : ∀ {a b c n} {e : Edge a b} {p : Path b c n} → a ∈ p → Repeats (e ∷ p)
  there : ∀ {a b c n} {e : Edge a b} {p : Path b c n} → Repeats p → Repeats (e ∷ p)

repeats? : ∀ {a b n} (p : Path a b n) → Dec (Repeats p)
repeats? [] = no λ ()
repeats? {a} (e ∷ p) =
  case a ∈? p of λ where
    (yes i) → yes (here i)
    (no ¬i) →
      case repeats? p of λ where
        (yes r) → yes (there r)
        (no ¬r) →
          no λ where
            (here i) → contradiction i ¬i
            (there r) → contradiction r ¬r

Acyclic : ∀ {a b n} → Path a b n → Set
Acyclic p = ¬ Repeats p

acyclic? : ∀ {a b n} (p : Path a b n) → Dec (Acyclic p)
acyclic? = ¬? ∘ repeats?

data Segmented a b : ℕ → Set (ℓᵥ ℓ.⊔ ℓₑ) where
  _◄_◄_ : ∀ {x m n l} →
    Path a x m →
    Path x x (suc n) →
    Path x b l →
    Segmented a b (m + suc n + l)

segment : ∀ {a b n} {p : Path a b n} → Repeats p → Segmented a b n
segment {p = []} ()
segment {p = e ∷ p} (here i) rewrite splitLengthsAddUp i = [] ◄ e ∷ prefix i ◄ suffix i
segment {p = e ∷ p} (there r) =
  case segment r of λ where
    (p₁ ◄ p₂ ◄ p₃) → (e ∷ p₁) ◄ p₂ ◄ p₃

cutLoop< : ∀ {a b n} {p : Path a b n} → Repeats p → Path< a b n
cutLoop< r = case segment r of λ where (_◄_◄_ {m = m} p₁ p₂ p₃) → -, lengthLem m , p₁ ++ p₃
  where
    lengthLem : ∀ x {y z} → suc (x + z) ≤ x + suc y + z
    lengthLem zero = s≤s (n≤m+n _ _)
    lengthLem (suc x) = s≤s (lengthLem x)

indicesLoop : ∀ {a b n i j} {p : Path a b n} → i ≢ j → lookup p i ≡ lookup p j → Repeats p
indicesLoop {i = zero} {zero} {e ∷ p} z≢z eq = contradiction refl z≢z
indicesLoop {i = zero} {suc j} {e ∷ p} _ refl = here (∈-lookup j)
indicesLoop {i = suc i} {zero} {e ∷ p} _ refl = here (∈-lookup i)
indicesLoop {i = suc i} {suc j} {e ∷ p} si≢sj eq = there (indicesLoop (si≢sj ∘ cong suc) eq)

findLoop : ∀ {a b n} (p : Path a b n) → n > size vertexFinite → Repeats p
findLoop p gt =
  let i , j , i≢j , eq = pigeonhole gt (finiteIndex p) in
    indicesLoop i≢j (indexOf-injective vertexFinite eq)

acyclic-length-≤ : ∀ {a b n} (p : Path a b n) → Acyclic p → n ≤ size vertexFinite
acyclic-length-≤ {n = n} p ¬r =
  case n ≤? size vertexFinite of λ where
    (yes le) → le
    (no ¬le) → contradiction (findLoop p (≰⇒> ¬le)) ¬r

shortenPath : ∀ {a b n} → Path a b n → n > size vertexFinite → Path< a b n
shortenPath p = cutLoop< ∘ findLoop p

shortenPathEnough : ∀ {a b n}
  (p : Path a b n) →
  n > size vertexFinite →
  Path≤ a b (size vertexFinite)
shortenPathEnough = <-rec _ wfRec _
  where
    wfRec =
      λ n rec p gt →
        let n′ , le , p′ = shortenPath p gt in
          case size vertexFinite <? n′ of λ where
            (yes n′>v) → rec _ le p′ n′>v
            (no n′≯v) → -, ≮⇒≥ n′≯v , p′

shortEnoughPath : ∀ {a b n} (p : Path a b n) → Path≤ a b (size vertexFinite)
shortEnoughPath {n = n} p =
  case size vertexFinite <? n of λ where
    (yes n>v) → shortenPathEnough p n>v
    (no n≯v) → -, ≮⇒≥ n≯v , p

cutAllLoops : ∀ {a b n} →
  (p : Path a b n) →
  Repeats p →
  ∃ λ (p : Path≤ a b n) → ¬ Repeats (proj₂ (proj₂ p))
cutAllLoops = <-rec _ wfRec _
  where
    wfRec = λ x rec p r →
      case cutLoop< r of λ where
        (n′ , lt , p′) →
          case repeats? p′ of λ where
            (yes r) →
              case rec _ lt p′ r of λ where
                ((n′′ , le′′ , p′′) , ¬r′′) →
                  (n′′ , ≤-trans le′′ (<⇒≤ lt) , p′′) , ¬r′′
            (no ¬r) → (n′ , <⇒≤ lt , p′) , ¬r

acyclicPath : ∀ {a b n} →
  (p : Path a b n) →
  ∃ λ (p : Path≤ a b n) → ¬ Repeats (proj₂ (proj₂ p))
acyclicPath p =
  case repeats? p of λ where
    (yes r) → cutAllLoops p r
    (no ¬r) → (-, ≤-refl , p) , ¬r

minimalPath : ∀ {a b n} →
  Path a b n →
  ∃ λ (p : Path≤ a b (size vertexFinite)) → ¬ Repeats (proj₂ (proj₂ p))
minimalPath p =
  let
    x , x≤max , p′ = shortEnoughPath p
    (y , y≤x , p′′) , ¬r = acyclicPath p′
  in
    (y , ≤-trans y≤x x≤max , p′′) , ¬r


text:
open import Type
open import Structure.Relator
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)

-- TODO: Organize this module
module Structure.Sets.ZFC.Inductive {ℓₛ ℓₗ ℓₑ} {S : Type{ℓₛ}} ⦃ equiv : Equiv{ℓₑ}(S) ⦄ (_∈_ : S → S → Type{ℓₗ}) ⦃ [∈]-binaryRelator : BinaryRelator(_∈_) ⦄ where

open import Functional using (id)
open import Functional.Dependent
import      Lvl
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Structure.Relator.Proofs renaming ([≡]-binaryRelator to [≡ₑ]-binaryRelator)
open import Structure.Sets.ZFC(_∈_) ⦃ [∈]-binaryRelator ⦄
open import Structure.Sets.ZFC.Oper(_∈_)
import      Structure.Sets.Names
open        Structure.Sets.Names.From-[∈] (_∈_)
open import Structure.Sets.Quantifiers (_∈_)
open import Syntax.Function

private variable ℓ : Lvl.Level
private variable A B C D E N a b c d e x y z As : S
private variable P : S → Type{ℓ}

module _ ⦃ zfc : ZFC ⦄ where
  open ZFC(zfc)

  -- minSubset P(A) is the intersection of all subsets of A satisfying P.
  -- Semantically, minSubset P(A) is the minimal subset of A satisfying P when A satisfies P and big intersection of a set containing A preserves P.
  minSubset : (P : S → Type{ℓ}) → ⦃ rel : UnaryRelator(P) ⦄ → S → S
  minSubset P(A) = ⋂(filter P(℘(A)))

  -- The minimal subset is a subset of the given set when the given set satisfies the given property.
  minSubset-subset : ⦃ rel : UnaryRelator(P) ⦄ → P(A) → (minSubset P(A) ⊆ A)
  minSubset-subset {P = P}{A = A} pa xM = [∧]-elimᵣ([↔]-to-[→] intersection xM) filt where
    filt : (A ∈ filter P(℘(A)))
    filt = [↔]-to-[←] restricted-comprehension ([∧]-intro ℘-self pa)

  -- A subset of the minimal subset is equal to the minimal subset if it and the given set satisfies the given property.
  minSubset-subsets : ⦃ rel : UnaryRelator(P) ⦄ → P(A) → P(B) → (B ⊆ minSubset P(A)) → (B ⊇ minSubset P(A))
  minSubset-subsets {P = P}{A = A} pa pb sub cont = [∧]-elimᵣ([↔]-to-[→] (restricted-comprehension ⦃ _ ⦄) cont) (filt-pow ([∧]-intro (minSubset-subset pa ∘ sub) pb)) where
    filt-pow : ((B ⊆ A) ∧ P(B)) → (B ∈ filter P(℘(A)))
    filt-pow ([∧]-intro sub pb) = [↔]-to-[←] restricted-comprehension ([∧]-intro ([↔]-to-[←] power sub) pb)

  minSubset-satisfaction3 : ⦃ rel : UnaryRelator(P) ⦄ → (∀ₛ(℘(℘(A))) (As ↦ ((∀ₛ(As) P) → P(⋂ As)))) → P(A) → P(minSubset P(A))
  minSubset-satisfaction3 preserv p = preserv ([↔]-to-[←] power ([∧]-elimₗ ∘ [↔]-to-[→] restricted-comprehension)) ([∧]-elimᵣ ∘ [↔]-to-[→] restricted-comprehension)

  -- When the big intersection of a set containing A preserves P and A satisfies P, then the minimal subset satisfies P.
  minSubset-satisfaction : ⦃ rel : UnaryRelator(P) ⦄ → (∀{As} → (A ∈ As) → (∀ₛ(As) P) → P(⋂ As)) → P(A) → P(minSubset P(A))
  minSubset-satisfaction preserv p = preserv ([↔]-to-[←] restricted-comprehension ([∧]-intro ℘-self p)) ([∧]-elimᵣ ∘ [↔]-to-[→] restricted-comprehension)

  -- The "smallest" inductive set is the set of natural numbers.
  -- All elements which can be expressed using only 𝟎 and 𝐒.
  ℕ : S
  ℕ = ⋂(filter Inductive (℘(ω₀))) -- TODO: This pattern seems useful. See the module Inductive

  -- The relation "lesser than" in this model of ℕ.
  -- This works for all elements in ℕ by the definition of 𝟎 and 𝐒.
  _<_ : S → S → Type
  a < b = a ∈ b

  _≤_ : S → S → Type
  a ≤ b = (a < b) ∨ (a ≡ b)

  _>_ : S → S → Type
  a > b = b < a

  _≥_ : S → S → Type
  a ≥ b = b ≤ a

  infixl 2000 _<_ _≤_ _>_ _≥_

  𝕟 : S → S
  𝕟(n) = filter(_< n) ⦃ binary-unaryRelatorᵣ ⦄ (ℕ)

  -- The set ℕ contains zero and all successors.
  ℕ-inductive : Inductive(ℕ)
  ℕ-inductive = minSubset-satisfaction p infinity where
    p :  ∀{S} → (ω₀ ∈ S) → (∀ₛ(S) Inductive) → Inductive(⋂ S)
    p {S} omega ind = [∧]-intro base step where
      base : 𝟎 ∈ (⋂ S)
      base = [↔]-to-[←] intersection ([∧]-intro ([∃]-intro ω₀ ⦃ [∧]-intro omega ([∧]-elimₗ infinity) ⦄) ([∧]-elimₗ ∘ ind))
      step : (x ∈ (⋂ S)) → (𝐒(x) ∈ (⋂ S))
      step xint = [↔]-to-[←] intersection ([∧]-intro ([∃]-intro ω₀ ⦃ [∧]-intro omega ([∧]-elimᵣ infinity ([∧]-elimᵣ([↔]-to-[→] intersection xint) omega)) ⦄) (\as → [∧]-elimᵣ(ind as) ([∧]-elimᵣ([↔]-to-[→] intersection xint) as)))

  {-
    ℕ-inclusionᵣ : (x ∈ ℕ) → ∃(A ↦ ((A ⊆ ω₀) ∧ Inductive(A)) ∧ (x ∈ A)) ∧ ∀ₗ(A ↦ (((A ⊆ ω₀) ∧ Inductive(A)) → (x ∈ A)))
    ℕ-inclusionᵣ xℕ = [∧]-map ([∃]-map-proof ([∧]-map ([∧]-map ([↔]-to-[→] power) id ∘ [↔]-to-[→] restricted-comprehension) id) ∘ [↔]-to-[→] union) (\p q → p ([↔]-to-[←] restricted-comprehension ([∧]-map ([↔]-to-[←] power) id q))) ([↔]-to-[→] intersection xℕ)
  -}

  -- The natural numbers' set induction principle.
  ℕ-set-induction : Inductive(N) → (N ⊆ ℕ) → (N ⊇ ℕ)
  ℕ-set-induction = minSubset-subsets infinity

  -- The induction principle of the natural numbers for the elements in the set ℕ.
  ℕ-induction : ⦃ rel : UnaryRelator(P) ⦄ → P(𝟎) → (∀ₛ(ℕ) (n ↦ (P(n) → P(𝐒(n))))) → (∀ₛ(ℕ) P)
  ℕ-induction {P = P} pz ps = [∧]-elimᵣ ∘ [↔]-to-[→] restricted-comprehension ∘ Pset-super where
    Pset : S
    Pset = filter P(ℕ)

    Pset-𝟎 : (𝟎 ∈ Pset)
    Pset-𝟎 = [↔]-to-[←] restricted-comprehension ([∧]-intro ([∧]-elimₗ ℕ-inductive) pz)

    Pset-𝐒 : ∀ₛ(Pset) (n ↦ (𝐒(n) ∈ Pset))
    Pset-𝐒 {n} nPset =
      let Pn : P(n)
          Pn = [∧]-elimᵣ([↔]-to-[→] restricted-comprehension nPset)

          nℕ : (n ∈ ℕ)
          nℕ = [∧]-elimₗ([↔]-to-[→] restricted-comprehension nPset)

      in  [↔]-to-[←] restricted-comprehension ([∧]-intro ([∧]-elimᵣ ℕ-inductive nℕ) (ps nℕ Pn))

    Pset-super : ℕ ⊆ Pset
    Pset-super = ℕ-set-induction ([∧]-intro Pset-𝟎 Pset-𝐒) ([∧]-elimₗ ∘ [↔]-to-[→] restricted-comprehension)


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Impl.Consensus.BlockStorage.BlockStore
open import LibraBFT.Impl.Consensus.BlockStorage.BlockTree
open import LibraBFT.Impl.Consensus.ConsensusTypes.ExecutedBlock as ExecutedBlock
open import LibraBFT.Impl.Consensus.ConsensusTypes.Vote as Vote
open import LibraBFT.Impl.OBM.Prelude
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Hash
open import Util.KVMap                                           as Map
open import Util.PKCS
open import Util.Prelude

open QCProps
open Invariants

module LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockTree where

module insertBlockESpec (eb0 : ExecutedBlock) (bt : BlockTree) where
  eb0Id = eb0 ^∙ ebId

  open Reqs (eb0 ^∙ ebBlock) bt

  -- This is not quite right.  It does not yet account for the updating of the parent Block
  -- Is it needed (see below)?
  record Updated (hv : HashValue) (pre post : BlockTree) (eb : ExecutedBlock) : Set where
    field
      ≢hv¬Upd : ∀ {hv'} → hv' ≢ hv → btGetBlock hv' post ≡ btGetBlock hv' pre

  record ContractOk (bt“ : BlockTree) (eb : ExecutedBlock) : Set where
    constructor mkContractOk
    field
      bt≡x    : bt ≡ (bt“ & btIdToBlock ∙~ (bt ^∙ btIdToBlock))
      -- The following two fields are not used, but something like this will be useful in proving
      -- btiPres and may provide value in their own right
      ¬upd    : ∀ {eb'} → btGetBlock eb0Id bt ≡ just eb' → bt ≡ bt“
      upd     :           btGetBlock eb0Id bt ≡ nothing  →  Updated eb0Id bt bt“ eb
      blocks≈ : NoHC1 → eb [ _≈Block_ ]L eb0 at ebBlock
      btiPres : ∀ {eci} → Preserves BlockTreeInv (bt , eci) (bt“ , eci)

  Contract : Either ErrLog (BlockTree × ExecutedBlock) → Set
  Contract (Left _) = ⊤
  Contract (Right (bt' , b)) = ContractOk bt' b

  open insertBlockE

  postulate -- TODO-1: prove; note that the contract is stronger than we need because insertBlockE
            -- is called only when btGetBlock eb0Id bt ≡ nothing in LibraBFT
    contract' : EitherD-weakestPre (step₀ eb0 bt) Contract

  contract : Contract (insertBlockE.E eb0 bt)
  contract = EitherD-contract (step₀ eb0 bt) Contract contract'

module insertQuorumCertESpec
  (qc : QuorumCert) (bt0  : BlockTree) where
  open insertQuorumCertE qc bt0

  Ok : Set
  Ok = ∃₂ λ bt1 il → insertQuorumCertE qc bt0 ≡ Right (bt1 , il)

  private
    Ok' : BlockTree → List InfoLog → Either ErrLog (BlockTree × List InfoLog) → Set
    Ok' bt il m = m ≡ Right (bt , il)

  record ContractOk (btPre btPost : BlockTree) (ilPre ilPost : List InfoLog) : Set where
    constructor mkContractOk
    field
      noNewQCs : ∈Post⇒∈PreOrBT (_≡ qc) btPre btPost

  ContractOk-trans : ∀ {btPre btInt btPost ilPre ilInt ilPost}
                   → ContractOk btPre btInt  ilPre ilInt
                   → ContractOk btInt btPost ilInt ilPost
                   → ContractOk btPre btPost ilPre ilPost
  ContractOk-trans (mkContractOk noNewQCs) (mkContractOk noNewQCs₁) =
                    mkContractOk (∈Post⇒∈PreOr'-trans _∈BlockTree_ (_≡ qc) noNewQCs noNewQCs₁)

  Contract : EitherD-Post ErrLog (BlockTree × List InfoLog)
  Contract (Left _) = ⊤
  Contract (Right (bt1 , il)) = ContractOk bt0 bt1 [] il

  contract' : EitherD-weakestPre step₀ Contract
  contract'
     with safetyInvariant
  ...| Left e     = tt
  ...| Right unit = contract-step₁'
    where
    contract-step₁' : EitherD-weakestPre (step₁ blockId) Contract
    proj₁ contract-step₁' _ = tt
    proj₂ contract-step₁' block _ = contract-step₂'
      where
      contract-step₂' : EitherD-weakestPre (step₂ blockId block) Contract
      proj₁ contract-step₂' _ = tt
      proj₂ contract-step₂' hcb _ =
        contract-step₃'
        where
        contract-cont2' : ∀ (bt : BlockTree) (info : List InfoLog)
                         → let (bt' , info') = continue2 bt info
                           in ContractOk bt bt' info info'
        contract-cont2' bt info
           with (bt ^∙ btHighestCommitCert ∙ qcCommitInfo ∙ biRound) <? (qc ^∙ qcCommitInfo ∙ biRound)
        ...| yes hqcR<qcR = mkContractOk (∈BlockTree-upd-hcc refl refl)
        ...| no  hqcR≥qcR = mkContractOk (λ _ x → inj₁ x)

        cont1-update-bt : BlockTree → BlockTree
        cont1-update-bt bt = bt & btIdToQuorumCert ∙~ Map.insert blockId qc (bt ^∙ btIdToQuorumCert)

        info' : List InfoLog → Bool → List InfoLog
        info' il b = (fakeInfo ∷ il) ++ (if b then (fakeInfo ∷ []) else [])

        contract-cont1' : ∀ (btPre : BlockTree) (infoPre : List InfoLog)
                        → let (btPost , infoPost) = continue1 btPre blockId block infoPre
                          in  ContractOk btPre btPost infoPre infoPost
        contract-cont1' btPre infoPre
           with Map.kvm-member blockId (btPre ^∙ btIdToQuorumCert)
        ...| true  = mkContractOk (ContractOk.noNewQCs (contract-cont2' btPre (info' infoPre $ ExecutedBlock.isNilBlock block )))
        ...| false = ContractOk-trans {btInt = cont1-update-bt btPre} {ilInt = info' infoPre $ ExecutedBlock.isNilBlock block }
                               (mkContractOk (∈Post⇒∈PreOrBT-QCs≡ _ refl refl))
                               (mkContractOk (ContractOk.noNewQCs (contract-cont2'
                                                                     (cont1-update-bt btPre)
                                                                     (info' infoPre $ ExecutedBlock.isNilBlock block))))

        bt' = bt0 & btHighestCertifiedBlockId ∙~ block ^∙ ebId
                  & btHighestQuorumCert       ∙~ qc

        contract-step₃' : EitherD-weakestPre (step₃ blockId block hcb) Contract
        proj₁ contract-step₃' _ = ContractOk-trans
                                    (mkContractOk (∈BlockTree-upd-hqc refl refl))
                                    (contract-cont1' bt' (fakeInfo ∷ []))
        proj₂ contract-step₃' _ = ContractOk-trans
                                    (mkContractOk (∈Post⇒∈PreOr'-refl _∈BlockTree_ _))
                                    (contract-cont1' bt0 [])


text:
open import Prelude

module Nat where

  -- definitions

  data Nat : Set where
    Z : Nat
    1+ : Nat → Nat

  {-# BUILTIN NATURAL Nat #-}

  _+_ : Nat → Nat → Nat
  Z + m = m
  1+ n + m = 1+ (n + m)

  infixl 60 _+_

  data _≤_ : Nat → Nat → Set where
    ≤refl  : ∀{n} → n ≤ n
    ≤1+    : ∀{n m} → n ≤ m → n ≤ 1+ m

  infix 40 _≤_

  _<_ : Nat → Nat → Set
  n < m = n ≤ m ∧ n ≠ m
  infix 40 _<_

  -- The `difference` operation accepts two numbers n and m and a proof that n ≤ m.
  -- Alternative definitions could return an option, returning None if n > m,
  -- or truncation, returning 0 if n > m. The latter may make some of the work easier,
  -- if it allows us to avoid issues with proof relevance. Even so, many proofs would
  -- still need to make use of the proof that n ≤ m to establish that the difference is
  -- not arbitrarily 0. As such, we believe that refactoring to use the perhaps more
  -- conventional truncation approach would not necessarily go far enough in cleaning up
  -- proofs as to be worth the refactoring effort.
  difference : ∀{n m} → n ≤ m → Nat
  difference {n} {.n} ≤refl = Z
  difference {n} {.(1+ _)} (≤1+ n≤m-1) = 1+ (difference n≤m-1)

  -- basic theorems

  -- the succ operation is injective
  1+inj : ∀{n m} → 1+ n == 1+ m → n == m
  1+inj refl = refl

  1+ap : ∀{n m} → n == m → 1+ n == 1+ m
  1+ap {n} {.n} refl = refl

  1+ap-cp : ∀{n m} → 1+ n ≠ 1+ m → n ≠ m
  1+ap-cp h1 h2 = h1 (1+ap h2)

  1+inj-cp : ∀{n m} → n ≠ m → 1+ n ≠ 1+ m
  1+inj-cp h1 h2 = h1 (1+inj h2)

  -- equality of naturals is decidable. we represent this as computing a
  -- choice of units, with inl <> meaning that the naturals are indeed the
  -- same and inr <> that they are not.
  natEQ : (x y : Nat) → ((x == y) ∨ ((x == y) → ⊥))
  natEQ Z Z = Inl refl
  natEQ Z (1+ y) = Inr (λ ())
  natEQ (1+ x) Z = Inr (λ ())
  natEQ (1+ x) (1+ y) with natEQ x y
  natEQ (1+ x) (1+ .x) | Inl refl = Inl refl
  ... | Inr b = Inr (λ x₁ → b (1+inj x₁))

  0≠1+n : ∀{n} → 0 ≠ 1+ n
  0≠1+n = λ ()

  -- _+_ theorems

  n+Z==n : ∀{n} → n + Z == n
  n+Z==n {Z} = refl
  n+Z==n {1+ n} = 1+ap n+Z==n

  n+1+m==1+n+m : ∀{n m} → n + 1+ m == 1+ (n + m)
  n+1+m==1+n+m {Z} = refl
  n+1+m==1+n+m {1+ n} = 1+ap n+1+m==1+n+m

  n≠n+1+m : ∀{n m} → n ≠ n + 1+ m
  n≠n+1+m {Z} {m} ()
  n≠n+1+m {1+ n} {m} h = 1+inj-cp n≠n+1+m h

  +comm : ∀{a b} → a + b == b + a
  +comm {Z} {b} = ! n+Z==n
  +comm {1+ a} {Z} = 1+ap n+Z==n
  +comm {1+ a} {1+ b} with a + 1+ b | b + 1+ a | n+1+m==1+n+m {a} {b} | n+1+m==1+n+m {b} {a}
  +comm {1+ a} {1+ b} | _ | _ | refl | refl = 1+ap (1+ap (+comm {a}))

  +assc : ∀{a b c} → (a + b) + c == a + (b + c)
  +assc {Z} = refl
  +assc {1+ a} = 1+ap (+assc {a})

  a+n==a+m→n==m : ∀{a n m} → a + n == a + m → n == m
  a+n==a+m→n==m {Z} refl = refl
  a+n==a+m→n==m {1+ a} a+n==a+m = a+n==a+m→n==m (1+inj a+n==a+m)

  n+a==m+a→n==m : ∀{n m a} → n + a == m + a → n == m
  n+a==m+a→n==m {n} {m} {a} n+a==m+a rewrite +comm {n} {a} | +comm {m} {a} = a+n==a+m→n==m n+a==m+a

  +inj : ∀{a1 a2 b} → a1 + b == a2 + b → a1 == a2
  +inj {a1} {a2} {Z} h
    rewrite (n+Z==n {a1}) | (n+Z==n {a2}) = h
  +inj {a1} {a2} {1+ b} h
    rewrite n+1+m==1+n+m {a1} {b} | n+1+m==1+n+m {a2} {b} = +inj (1+inj h)

  +inj-cp : ∀{a1 a2 b} → a1 ≠ a2 → a1 + b ≠ a2 + b
  +inj-cp ne f = ne (+inj f)

  -- even/odd theorems

  even-inj : ∀{m n} → m + m == n + n → m == n
  even-inj {Z} {Z} eq = refl
  even-inj {1+ m} {1+ n} eq rewrite (n+1+m==1+n+m {n} {n}) | (n+1+m==1+n+m {m} {m})
    = 1+ap (even-inj (1+inj (1+inj eq)))

  even-not-odd : ∀{m n} → 1+ (m + m) ≠ (n + n)
  even-not-odd {Z} {1+ n} eq rewrite (n+1+m==1+n+m {n} {n}) = 0≠1+n (1+inj eq)
  even-not-odd {1+ m} {1+ n} eq rewrite (n+1+m==1+n+m {n} {n}) | (n+1+m==1+n+m {m} {m})
    = even-not-odd {m} {n} (1+inj (1+inj eq))

  -- _≤_ theorems

  0≤n : ∀{n} → Z ≤ n
  0≤n {Z} = ≤refl
  0≤n {1+ n} = ≤1+ 0≤n

  1+n≰0 : ∀{n} → 1+ n ≤ Z → ⊥
  1+n≰0 = λ ()

  n≤m→1+n≤1+m : ∀{n m} → n ≤ m → 1+ n ≤ 1+ m
  n≤m→1+n≤1+m {n} {.n} ≤refl = ≤refl
  n≤m→1+n≤1+m {n} {.(1+ _)} (≤1+ h) = ≤1+ (n≤m→1+n≤1+m h)

  n≤m→s+n=m : ∀{n m} → n ≤ m → Σ[ s ∈ Nat ] (s + n == m)
  n≤m→s+n=m ≤refl = Z , refl
  n≤m→s+n=m (≤1+ n≤m)
    with n≤m→s+n=m n≤m
  ... | _ , refl = _ , refl

  1+n≤1+m→n≤m : ∀{n m} → 1+ n ≤ 1+ m → n ≤ m
  1+n≤1+m→n≤m {n} {.n} ≤refl = ≤refl
  1+n≤1+m→n≤m {n} {Z} (≤1+ h) = abort (1+n≰0 h)
  1+n≤1+m→n≤m {n} {1+ m} (≤1+ h) = ≤1+ (1+n≤1+m→n≤m h)

  n+s≤m+s→n≤m : ∀{n m s} → n + s ≤ m + s → n ≤ m
  n+s≤m+s→n≤m {n} {m} {s = Z} n+s≤m+s
    rewrite n+Z==n {n} | n+Z==n {m} = n+s≤m+s
  n+s≤m+s→n≤m {n} {m} {s = 1+ s} n+s≤m+s
    rewrite n+1+m==1+n+m {n} {s} | n+1+m==1+n+m {m} {s}
      = n+s≤m+s→n≤m (1+n≤1+m→n≤m n+s≤m+s)

  1+n≰n : ∀{n} → 1+ n ≤ n → ⊥
  1+n≰n {Z} h = abort (1+n≰0 h)
  1+n≰n {1+ n} h = 1+n≰n (1+n≤1+m→n≤m h)

  ≤total : ∀{n m} → n ≤ m ∨ m ≤ n
  ≤total {Z} {m} = Inl 0≤n
  ≤total {1+ n} {Z} = Inr (≤1+ 0≤n)
  ≤total {1+ n} {1+ m} with ≤total {n} {m}
  ≤total {1+ n} {1+ m} | Inl h = Inl (n≤m→1+n≤1+m h)
  ≤total {1+ n} {1+ m} | Inr h = Inr (n≤m→1+n≤1+m h)

  ≤trans : ∀{a b c} → a ≤ b → b ≤ c → a ≤ c
  ≤trans ≤refl b≤c = b≤c
  ≤trans (≤1+ a≤b) ≤refl = ≤1+ a≤b
  ≤trans (≤1+ a≤b) (≤1+ b≤c) = ≤1+ (≤trans (≤1+ a≤b) b≤c)

  ≤antisym : ∀{n m} → n ≤ m → m ≤ n → n == m
  ≤antisym {n} {.n} ≤refl m≤n = refl
  ≤antisym {n} {.(1+ _)} (≤1+ h1) h2 = abort (1+n≰n (≤trans h2 h1))

  n≤n+m : ∀{n m} → n ≤ n + m
  n≤n+m {n} {Z} with n + Z | n+Z==n {n}
  n≤n+m {_} {Z} | _ | refl = ≤refl
  n≤n+m {n} {1+ m} with n + 1+ m | ! (n+1+m==1+n+m {n} {m})
  n≤n+m {n} {1+ m} | _ | refl = ≤trans n≤n+m (≤1+ ≤refl)

  n≤m+n : ∀{n m} → n ≤ m + n
  n≤m+n {n} {m} rewrite +comm {m} {n} = n≤n+m

  -- _<_ theorems

  n≮0 : ∀{n} → n < Z → ⊥
  n≮0 {Z} (π3 , π4) = π4 refl
  n≮0 {1+ n} (π3 , π4) = 1+n≰0 π3

  n<1+n : ∀{n} → n < 1+ n
  π1 n<1+n = ≤1+ ≤refl
  π2 n<1+n ()

  1+n<1+m→n<m : ∀{n m} → 1+ n < 1+ m → n < m
  π1 (1+n<1+m→n<m (π3 , π4)) = 1+n≤1+m→n≤m π3
  π2 (1+n<1+m→n<m (π3 , π4)) = 1+ap-cp π4

  <trans : ∀{a b c} → a < b → b < c → a < c
  π1 (<trans (π3 , π4) (π5 , π6)) = ≤trans π3 π5
  π2 (<trans (π3 , π4) (≤refl , π6)) = abort (π6 refl)
  π2 (<trans (π3 , π4) (≤1+ π5 , π6)) refl = 1+n≰n (≤trans π3 π5)

  <antisym : ∀{n m} → n < m → m < n → ⊥
  <antisym (n≤m , n≠m) (m≤n , _) = n≠m (≤antisym n≤m m≤n)

  <antirefl : ∀{n} → n < n → ⊥
  <antirefl (_ , ne) = abort (ne refl)

  n<m→n<s+m : ∀{n m s} → n < m → n < s + m
  n<m→n<s+m {s = Z} n<m = n<m
  n<m→n<s+m {s = 1+ s} n<m =
    <trans (n<m→n<s+m {s = s} n<m) n<1+n

  n<m→1+n<1+m : ∀{n m} → n < m → 1+ n < 1+ m
  n<m→1+n<1+m (π3 , π4) = n≤m→1+n≤1+m π3 , 1+inj-cp π4

  n<m→s+1+n=m : ∀{n m} → n < m → Σ[ s ∈ Nat ] (s + 1+ n == m)
  n<m→s+1+n=m (≤refl , ne) = abort (ne refl)
  n<m→s+1+n=m {n = n} (≤1+ n≤m , _)
    with n≤m→s+n=m n≤m
  ... | _ , refl = _ , (n+1+m==1+n+m {m = n})

  0<1+n : ∀{n} → 0 < 1+ n
  0<1+n {Z} = ≤1+ ≤refl , (λ ())
  0<1+n {1+ n} = 0≤n , (λ ())

  1+n≤m→n<m : ∀{n m} → 1+ n ≤ m → n < m
  1+n≤m→n<m ≤refl = n<1+n
  1+n≤m→n<m (≤1+ 1+n≤m) = <trans (1+n≤m→n<m 1+n≤m) n<1+n

  n≤m→n<1+m : ∀{n m} → n ≤ m → n < 1+ m
  n≤m→n<1+m {Z} n≤m = 0<1+n
  n≤m→n<1+m {1+ n} n≤m = n<m→1+n<1+m (1+n≤m→n<m n≤m)

  n<m→1+n≤m : ∀{n m} → n < m → 1+ n ≤ m
  n<m→1+n≤m (≤refl , ne) = abort (ne refl)
  n<m→1+n≤m (≤1+ n≤m , _) = n≤m→1+n≤1+m n≤m

  n<m→n≤m : ∀{n m} → n < m → n ≤ m
  n<m→n≤m n<m = 1+n≤1+m→n≤m (≤1+ (n<m→1+n≤m n<m))

  <dec : (n m : Nat) → n < m ∨ n == m ∨ m < n
  <dec n m with natEQ n m
  ... | Inl refl = Inr (Inl refl)
  ... | Inr ne   with ≤total {n} {m}
  ... | Inl ≤refl     = abort (ne refl)
  ... | Inl (≤1+ n≤m) = Inl (n≤m→n<1+m n≤m)
  ... | Inr ≤refl     = abort (ne refl)
  ... | Inr (≤1+ m≤n) = Inr (Inr (n≤m→n<1+m m≤n))

  <dec-refl : (n : Nat) → <dec n n == Inr (Inl refl)
  <dec-refl n with <dec n n
  <dec-refl n | Inl (_ , ne)       = abort (ne refl)
  <dec-refl n | Inr (Inl refl)     = refl
  <dec-refl n | Inr (Inr (_ , ne)) = abort (ne refl)

  -- difference theorems

  m-n+n==m : ∀{n m} → (n≤m : n ≤ m) → difference n≤m + n == m
  m-n+n==m ≤refl = refl
  m-n+n==m (≤1+ n≤m) = 1+ap (m-n+n==m n≤m)

  n+m-n==m : ∀{n m} → (n≤n+m : n ≤ n + m) → difference n≤n+m == m
  n+m-n==m {n} n≤n+m =
    n+a==m+a→n==m (m-n+n==m n≤n+m · +comm {n})

  a+b==c→a==c-b : ∀{a b c} → a + b == c → (b≤c : b ≤ c) → a == difference b≤c
  a+b==c→a==c-b a+b==c b≤c
    = n+a==m+a→n==m (a+b==c · ! (m-n+n==m b≤c))

  diff-proof-irrelevance : ∀{n m} →
                             (n≤m1 n≤m2 : n ≤ m) →
                             difference n≤m1 == difference n≤m2
  diff-proof-irrelevance ≤refl ≤refl = refl
  diff-proof-irrelevance ≤refl (≤1+ n≤m2) = abort (1+n≰n n≤m2)
  diff-proof-irrelevance (≤1+ n≤m1) ≤refl = abort (1+n≰n n≤m1)
  diff-proof-irrelevance (≤1+ n≤m1) (≤1+ n≤m2) = 1+ap (diff-proof-irrelevance n≤m1 n≤m2)

  m-n==1+m-1+n : ∀{n m} →
                   (n≤m : n ≤ m) →
                   (1+n≤1+m : 1+ n ≤ 1+ m) →
                   difference n≤m == difference 1+n≤1+m
  m-n==1+m-1+n {n} {.n} ≤refl ≤refl = refl
  m-n==1+m-1+n {n} {.n} ≤refl (≤1+ 1+n≤n) = abort (1+n≰n 1+n≤n)
  m-n==1+m-1+n {.(1+ _)} {.(1+ _)} (≤1+ 1+m≤m) ≤refl = abort (1+n≰n 1+m≤m)
  m-n==1+m-1+n {n} {.(1+ _)} (≤1+ n≤m) (≤1+ 1+n≤1+m) = 1+ap (m-n==1+m-1+n n≤m 1+n≤1+m)

  m-n==m+s-n+s : ∀{n m s} →
                   (n≤m : n ≤ m) →
                   (n+s≤m+s : n + s ≤ m + s) →
                   difference n≤m == difference n+s≤m+s
  m-n==m+s-n+s {n} {m} {s = Z} n≤m n+s≤m+s
    rewrite n+Z==n {n} | n+Z==n {m}
      = diff-proof-irrelevance n≤m n+s≤m+s
  m-n==m+s-n+s {n} {m} {s = 1+ s} n≤m n+s≤m+s
    rewrite n+1+m==1+n+m {n} {s} | n+1+m==1+n+m {m} {s}
      = (m-n==m+s-n+s n≤m (1+n≤1+m→n≤m n+s≤m+s)) · (m-n==1+m-1+n (1+n≤1+m→n≤m n+s≤m+s) n+s≤m+s)

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module Prelude where
  open import Agda.Primitive using (Level; lzero; lsuc) renaming (_⊔_ to lmax)

  -- empty type
  data ⊥ : Set where

  -- from false, derive whatever
  abort : ∀ {C : Set} → ⊥ → C
  abort ()

  -- unit
  data ⊤ : Set where
    <> : ⊤

  -- sums
  data _+_ (A B : Set) : Set where
    Inl : A → A + B
    Inr : B → A + B

  -- pairs
  infixr 1 _,_
  record Σ {l1 l2 : Level} (A : Set l1) (B : A → Set l2) : Set (lmax l1 l2) where
    constructor _,_
    field
      π1 : A
      π2 : B π1
  open Σ public

  -- Sigma types, or dependent pairs, with nice notation.
  syntax Σ A (\ x -> B) = Σ[ x ∈ A ] B

  _×_ : {l1 : Level} {l2 : Level} → (Set l1) → (Set l2) → Set (lmax l1 l2)
  A × B = Σ A λ _ → B

  infixr 1 _×_
  infixr 1 _+_

  -- equality
  data _==_ {l : Level} {A : Set l} (M : A) : A → Set l where
    refl : M == M

  infixr 9 _==_

  -- disequality
  _≠_ : {l : Level} {A : Set l} → (a b : A) → Set l
  a ≠ b = (a == b) → ⊥

  {-# BUILTIN EQUALITY _==_ #-}

  -- transitivity of equality
  _·_ : {l : Level} {α : Set l} {x y z : α} → x == y → y == z → x == z
  refl · refl = refl

  -- symmetry of equality
  ! : {l : Level} {α : Set l} {x y : α} → x == y → y == x
  ! refl = refl

  -- ap, in the sense of HoTT, that all functions respect equality in their
  -- arguments. named in a slightly non-standard way to avoid naming
  -- clashes with hazelnut constructors.
  ap1 : {l1 l2 : Level} {α : Set l1} {β : Set l2} {x y : α} (F : α → β)
          → x == y → F x == F y
  ap1 F refl = refl

  -- transport, in the sense of HoTT, that fibrations respect equality
  tr : {l1 l2 : Level} {α : Set l1} {x y : α}
                    (B : α → Set l2)
                    → x == y
                    → B x
                    → B y
  tr B refl x₁ = x₁

  -- options
  data Maybe (A : Set) : Set where
    Some : A → Maybe A
    None : Maybe A

  -- the some constructor is injective. perhaps unsurprisingly.
  someinj : {A : Set} {x y : A} → Some x == Some y → x == y
  someinj refl = refl

  --  some isn't none.
  somenotnone : {A : Set} {x : A} → Some x == None → ⊥
  somenotnone ()

  -- function extensionality, used to reason about contexts as finite
  -- functions.
  postulate
     funext : {A : Set} {B : A → Set} {f g : (x : A) → (B x)} →
              ((x : A) → f x == g x) → f == g

  -- non-equality is commutative
  flip : {A : Set} {x y : A} → (x == y → ⊥) → (y == x → ⊥)
  flip neq eq = neq (! eq)

  -- two types are said to be equivalent, or isomorphic, if there is a pair
  -- of functions between them where both round-trips are stable up to ==
  _≃_ : Set → Set → Set
  _≃_ A B = Σ[ f ∈ (A → B) ] Σ[ g ∈ (B → A) ]
             (((a : A) → g (f a) == a) × (((b : B) → f (g b) == b)))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
----------------------------------------------------------------------
-- Functional big-step evaluation of terms in the partiality monad
----------------------------------------------------------------------

module SystemF.Eval where

open import Codata.Musical.Notation
open import Category.Monad
open import Category.Monad.Partiality.All as All using (All; now; later)
open import Data.Fin using (Fin; zero; suc)
open import Data.Maybe as Maybe using (just; nothing)
open import Data.Maybe.Relation.Unary.Any as MaybeAny using (just)
open import Data.Nat using (_+_)
open import Data.Vec using ([])
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open import PartialityAndFailure as PF hiding (fail)
open PF.Equality hiding (fail)
open PF.Equivalence
private module M {f} = RawMonad (PF.monad {f})

open import SystemF.Type
open import SystemF.Term
open import SystemF.WtTerm

open TypeSubst       using () renaming (_[/_]  to _[/tp_])
open TermTypeSubst   using () renaming (_[/_]  to _[/tmTp_])
open TermTermSubst   using () renaming (_[/_]  to _[/tmTm_])
open WtTermTypeSubst using () renaming (_[/_]′ to _[/⊢tmTp_])
open WtTermTermSubst using () renaming (_[/_]  to _[/⊢tmTm_])

----------------------------------------------------------------------
-- Functional call-by-value big-step semantics

-- The functional presentation of the big-step semantics below is
-- heavily inspired by Danielsson's ICFP'12 paper "Operational
-- Semantics Using the Partiality Monad".  While the paper describes a
-- closure-based semantics, the semantics given below is
-- substitution-based.  This simplifies the evaluation of recursive
-- terms, i.e those involving fixpoint combinators, which would
-- otherwise have to be evaluated in a cyclic evironment, i.e. one
-- already containing the value of the recursive term being evaluated.
--
-- NB: while it is not described in detail in the paper, Danielsson
-- actually provides an alternative, substitution-based implementation
-- in the accompanying code, which can be found at
--
--   http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.tgz
--
-- As pointed out in Danielsson's paper, the functional presentation
-- of the big-step semantics feels rather natural in that it follows
-- the form of an interpreter, and it has the added advantage of
-- proving that the semantics are deterministic and computable "for
-- free".
--
-- For more information about Danielson's paper see
--
--   http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.html

----------------------------------------------------------------------
-- Semantic domain and evaluation

-- Computations with potential failure and partiality effects.
Comp : ∀ m n → Set
Comp m n = (Val m n) ?⊥

-- Following Danielsson's approach, we formulate the evaluation
-- function _⇓′ in an "embedded language" to work around the
-- limitations of Agda's guarded coinduction.  The function _⇓′
-- returns "programs", i.e. instances of the type _?⊥P which
-- internalizes the monadic bind operation as a constructor.  In a
-- second step, these programs are interpreted in the
-- partiality-and-failure monad by the function _⇓.
--
-- For details about this technique, see e.g. Danielsson's PAR'10
-- paper "Beating the Productivity Checker Using Embedded Languages".
--
-- SystemF.Eval.NoWorkarounds contains an alternative version of the
-- semantics which does not use the above-mentioned workaround.  The
-- alternative definition, while (provably) equivalent to the one
-- given below, is more verbose and arguably less readable.  However
-- the associated type soundness proof is simpler in that it requires
-- no additional compositionality lemmas.
module _ where
  open PF.Workaround

  -- Computation "programs".
  CompP : ∀ m n → Set₁
  CompP m n = (Val m n) ?⊥P

  mutual

    infix 7 _⇓′ _[_]′ _·′_

    -- Evaluation of untyped (open) terms in _?⊥P.
    _⇓′ : ∀ {m n} → Term m n → CompP m n
    var x ⇓′      = fail
    Λ t ⇓′        = return (Λ t)
    λ' a t ⇓′     = return (λ' a t)
    μ a t ⇓′      = later (♯ (t [/tmTm μ a t ] ⇓′))
    (t [ a ]) ⇓′  = t ⇓′ >>= λ v → v [ a ]′
    (s · t) ⇓′    = s ⇓′ >>= λ f → t ⇓′ >>= λ v → f ·′ v
    fold a t ⇓′   = t ⇓′ >>= λ v → return (fold a v)
    unfold a t ⇓′ = t ⇓′ >>= λ v → unfold′ a v

    -- Call-by-value evaluation of type application in _?⊥P.
    _[_]′ : ∀ {m n} → Val m n → Type n → CompP m n
    (Λ t) [ a ]′ = later (♯ (t [/tmTp a ] ⇓′))
    _     [ _ ]′ = fail

    -- Call-by-value Evaluation of term application in _?⊥P.
    _·′_ : ∀ {m n} → Val m n → Val m n → CompP m n
    (λ' _ t) ·′ v = later (♯ (t [/tmTm ⌜ v ⌝ ] ⇓′))
    _        ·′ _ = fail

    -- Evaluation of recursive type unfolding in _?⊥P.
    unfold′ : ∀ {m n} → Type (1 + n) → Val m n → CompP m n
    unfold′ _ (fold _ v) = return v
    unfold′ a _          = fail

  infix 7 _⇓

  -- Evaluation of untyped (open) terms in the partiality monad.
  _⇓ : ∀ {m n} → Term m n → Comp m n
  t ⇓ = ⟦ t ⇓′ ⟧P

----------------------------------------------------------------------
-- The semantics _⇓ is compositional

module _ where
  open M
  open PF.Reasoning
  open PF.Workaround using (⟦_⟧P) renaming (_>>=_ to _>>=P_)
  open PF.Workaround.Correct

  infix 7 _[_]⇓ _·⇓_

  -- Short hands for relating the semantics of composite terms to the
  -- semantics of their subterms.

  _[_]⇓ : ∀ {m n} → Comp m n → Type n → Comp m n
  c [ a ]⇓ = c >>= λ v → ⟦ v [ a ]′ ⟧P

  _·⇓_ : ∀ {m n} → Comp m n → Comp m n → Comp m n
  c ·⇓ d = c >>= λ f → d >>= λ v → ⟦ f ·′ v ⟧P

  fold⇓ : ∀ {m n} → Type (1 + n) → Comp m n → Comp m n
  fold⇓ a c = c >>= λ v → return (fold a v)

  unfold⇓ : ∀ {m n} → Type (1 + n) → Comp m n → Comp m n
  unfold⇓ a c = c >>= λ v → ⟦ unfold′ a v ⟧P

  -- The semantics of type application is compositional.
  []-comp : ∀ {m n} (t : Term m n) (a : Type n) → t [ a ] ⇓ ≅ (t ⇓) [ a ]⇓
  []-comp t a = >>=-hom (t ⇓′) _

  -- The semantics of term application is compositional.
  ·-comp : ∀ {m n} (s t : Term m n) → s · t ⇓ ≅ (s ⇓) ·⇓ (t ⇓)
  ·-comp s t =
      s · t ⇓
    ≅⟨ >>=-hom (s ⇓′) _ ⟩
      (s ⇓ >>= λ f → ⟦ t ⇓′ >>=P (λ v → f ·′ v) ⟧P)
    ≅⟨ (s ⇓ ∎ >>=-cong λ _ → >>=-hom (t ⇓′) _) ⟩
      (s ⇓) ·⇓ (t ⇓)
    ∎

  -- The semantics of recursive type folding is compositional.
  fold-comp : ∀ {m n} (a : Type (1 + n)) (t : Term m n) →
              fold a t ⇓ ≅ fold⇓ a (t ⇓)
  fold-comp a t = >>=-hom (t ⇓′) _

  -- The semantics of recursive type unfolding is compositional.
  unfold-comp : ∀ {m n} (a : Type (1 + n)) (t : Term m n) →
                unfold a t ⇓ ≅ unfold⇓ a (t ⇓)
  unfold-comp a t = >>=-hom (t ⇓′) _

----------------------------------------------------------------------
-- Type soundness

open PF using (fail)

infix 4 _⊢comp_∈_

-- A computation is well-typed if it is a well-typed value or it takes
-- a step towards a well-typed computation.  Note that we exclude the
-- case of failing well-typed computations through the use of
-- Maybe.Any.
_⊢comp_∈_ : ∀ {m n} → Ctx m n → Comp m n → Type n → Set
Γ ⊢comp c ∈ a = All (MaybeAny.Any (λ v → Γ ⊢val v ∈ a)) c

-- Well-typed computations do not fail.
does-not-fail : ∀ {m n} {Γ : Ctx m n} {c a} → Γ ⊢comp c ∈ a → ¬ c ≈ fail
does-not-fail (now (MaybeAny.just _)) (now ())
does-not-fail (later ⊢c)     (laterˡ c-fails) = does-not-fail (♭ ⊢c) c-fails

-- It remains to prove that well-typed terms evaluate to well-typed
-- computations.  The proof ⊢_⇓ follows the same structure as _⇓ and
-- uses an analogous workaround to deal with guarded coinduction.  It
-- is formulated in the language AllP of of Partiality.All "programs"
-- defined in All.Alternative.
open All.Alternative
open PF.Workaround using (⟦_⟧P)

infix 4 ⊢compP_∈_ ⊢val_∈_

-- Closed well-typed computation "programs".
⊢compP_∈_ : Comp 0 0 → Type 0 → Set₁
⊢compP c ∈ a = AllP (MaybeAny.Any (λ v → [] ⊢val v ∈ a)) c

-- A short hand for closed well-typed values.
⊢val_∈_ : Val 0 0 → Type 0 → Set
⊢val v ∈ a = [] ⊢val v ∈ a

mutual

  infix 7 ⊢_⇓′ ⊢_[_]′ ⊢_·′_

  -- Evaluation of closed terms preserves well-typedness in AllP.
  ⊢_⇓′ : ∀ {t a} → [] ⊢ t ∈ a → ⊢compP t ⇓ ∈ a
  ⊢ var ()      ⇓′
  ⊢ Λ ⊢t        ⇓′   = now (just (Λ ⊢t))
  ⊢ λ' a ⊢t     ⇓′   = now (just (λ' a ⊢t))
  ⊢ μ a ⊢t      ⇓′   = later (♯ ⊢ ⊢t [/⊢tmTm μ a ⊢t ] ⇓′)
  ⊢_⇓′ {t [ a ]} (⊢t [ .a ] ) =
    t [ a ] ⇓        ≅⟨ []-comp t a ⟩P
    (t ⇓) [ a ]⇓      ⟨  ⊢ ⊢t ⇓′ >>=-congP (λ { .{_} (just ⊢v) →
                         ⊢ ⊢v [ a ]′ }) ⟩P
  ⊢_⇓′ {s · t} (⊢s · ⊢t) =
    s · t ⇓          ≅⟨ ·-comp s t ⟩P
    (s ⇓) ·⇓ (t ⇓)    ⟨ (⊢ ⊢s ⇓′ >>=-congP λ { .{_} (just ⊢f) →
                         ⊢ ⊢t ⇓′ >>=-congP λ { .{_} (just ⊢v) →
                         ⊢ ⊢f ·′ ⊢v }}) ⟩P
  ⊢_⇓′ {fold a t} (fold .a ⊢t) =
    fold a t ⇓       ≅⟨ fold-comp a t ⟩P
    fold⇓ a (t ⇓)     ⟨ (⊢ ⊢t ⇓′ >>=-congP λ { .{_} (just ⊢v) →
                         now (just (fold a ⊢v)) }) ⟩P
  ⊢_⇓′ {unfold a t} (unfold .a ⊢t) =
    unfold a t ⇓     ≅⟨ unfold-comp a t ⟩P
    unfold⇓ a (t ⇓)   ⟨ (⊢ ⊢t ⇓′ >>=-congP λ { .{_} (just ⊢v) →
                         ⊢unfold′ a ⊢v }) ⟩P

  -- Evaluation of type application preserves well-typedness in AllP.
  ⊢_[_]′ : ∀ {v a} → ⊢val v ∈ ∀' a → ∀ b → ⊢compP ⟦ v [ b ]′ ⟧P ∈ a [/tp b ]
  ⊢ Λ ⊢t [ a ]′ = later (♯ ⊢ ⊢t [/⊢tmTp a ] ⇓′)

  -- Evaluation of term application preserves well-typedness in AllP.
  ⊢_·′_ : ∀ {f v a b} → ⊢val f ∈ a →' b → ⊢val v ∈ a → ⊢compP ⟦ f ·′ v ⟧P ∈ b
  ⊢ λ' a ⊢t ·′ ⊢v = later (♯ ⊢ ⊢t [/⊢tmTm ⊢⌜ ⊢v ⌝ ] ⇓′)

  -- Evaluation of recursive type unfolding preserves well-typedness in AllP.
  ⊢unfold′ : ∀ {v} a → ⊢val v ∈ μ a → ⊢compP ⟦ unfold′ a v ⟧P ∈ a [/tp μ a ]
  ⊢unfold′ _ (fold ._ ⊢v) = now (just ⊢v)

infix 7 ⊢_⇓

-- Evaluation of closed terms preserves well-typedness.
⊢_⇓ : ∀ {t a} → [] ⊢ t ∈ a → [] ⊢comp t ⇓ ∈ a
⊢_⇓ = sound ∘ ⊢_⇓′

-- Type soundness: evaluation of well-typed terms does not fail.
type-soundness : ∀ {t a} → [] ⊢ t ∈ a → ¬ t ⇓ ≈ fail
type-soundness ⊢t = does-not-fail ⊢ ⊢t ⇓

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


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

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

module GroupTheory.PropertiesI where

open import GroupTheory.Base

open import Common.FOL.Relation.Binary.EqReasoning

------------------------------------------------------------------------------
-- Congruence properties

-- The propositional equality is compatible with the binary operation.

·-leftCong : ∀ {a b c} → a ≡ b → a · c ≡ b · c
·-leftCong refl = refl

·-rightCong : ∀ {a b c} → b ≡ c → a · b ≡ a · c
·-rightCong refl = refl

-- The propositional equality is compatible with the inverse function.
⁻¹-cong : ∀ {a b} → a ≡ b → a ⁻¹ ≡ b ⁻¹
⁻¹-cong refl = refl

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

leftCancellation : ∀ {a b c} → a · b ≡ a · c → b ≡ c
leftCancellation {a} {b} {c} h =
  b              ≡⟨ sym (leftIdentity b) ⟩
  ε · b          ≡⟨ ·-leftCong (sym (leftInverse a)) ⟩
  a ⁻¹ · a · b   ≡⟨ assoc (a ⁻¹) a b ⟩
  a ⁻¹ · (a · b) ≡⟨ ·-rightCong h ⟩
  a ⁻¹ · (a · c) ≡⟨ sym (assoc (a ⁻¹) a c) ⟩
  a ⁻¹ · a · c   ≡⟨ ·-leftCong (leftInverse a) ⟩
  ε · c          ≡⟨ leftIdentity c ⟩
  c              ∎

-- A different proof without using congruence.
leftCancellation' : ∀ {a b c} → a · b ≡ a · c → b ≡ c
-- Paper proof (Mac Lane and Garret Birkhoff 1999. p. 48):
--
-- 1. a⁻¹(ab) = a⁻¹(ac)  (hypothesis ab = ac)
-- 2. a⁻¹a(b) = a⁻¹a(c)  (associative axiom)
-- 3. εb      = εc       (left-inverse axiom for a⁻¹)
-- 4. b       = c        (left-identity axiom)
leftCancellation' {a} {b} {c} h =
  b              ≡⟨ sym (leftIdentity b) ⟩
  ε · b          ≡⟨ subst (λ t → ε · b ≡ t · b) (sym (leftInverse a)) refl ⟩
  a ⁻¹ · a · b   ≡⟨ assoc (a ⁻¹) a b ⟩
  a ⁻¹ · (a · b) ≡⟨ subst (λ t → a ⁻¹ · (a · b) ≡ a ⁻¹ · t) h refl ⟩
  a ⁻¹ · (a · c) ≡⟨ sym (assoc (a ⁻¹) a c) ⟩
  a ⁻¹ · a · c   ≡⟨ subst (λ t → a ⁻¹ · a · c ≡ t · c) (leftInverse a) refl ⟩
  ε · c          ≡⟨ leftIdentity c ⟩
  c              ∎

-- Mac Lane and Garret Birkhoff (1999) p. 50, exercise 6.
rightIdentity : ∀ a → a · ε ≡ a
rightIdentity a = leftCancellation prf
  where
  prf : a ⁻¹ · (a · ε) ≡ a ⁻¹ · a
  prf = a ⁻¹ · (a · ε) ≡⟨ sym (assoc (a ⁻¹) a ε) ⟩
        a ⁻¹ · a · ε   ≡⟨ ·-leftCong (leftInverse a) ⟩
        ε · ε          ≡⟨ leftIdentity ε ⟩
        ε              ≡⟨ sym (leftInverse a) ⟩
        a ⁻¹ · a       ∎

-- Mac Lane and Garret Birkhoff (1999) p. 50, exercise 6.
rightInverse : ∀ a → a · a ⁻¹ ≡ ε
rightInverse a = leftCancellation prf
  where
  prf : a ⁻¹ · (a · a ⁻¹) ≡ a ⁻¹ · ε
  prf = a ⁻¹ · (a · a ⁻¹) ≡⟨ sym (assoc (a ⁻¹) a (a ⁻¹)) ⟩
        a ⁻¹ · a · a ⁻¹   ≡⟨ ·-leftCong (leftInverse a) ⟩
        ε · a ⁻¹          ≡⟨ leftIdentity (a ⁻¹)  ⟩
        a ⁻¹              ≡⟨ sym (rightIdentity (a ⁻¹)) ⟩
        a ⁻¹ · ε          ∎

rightCancellation : ∀ {a b c} → b · a ≡ c · a → b ≡ c
rightCancellation {a} {b} {c} h =
-- Paper proof:
--
-- 1. (ba)a⁻¹ = (ca)a⁻¹  (hypothesis ab = ac)
-- 2. (b)aa⁻¹ = (c)aa⁻¹  (associative axiom)
-- 3. bε      = cε       (right-inverse axiom for a⁻¹)
-- 4. b       = c        (right-identity axiom)
  b              ≡⟨ sym (rightIdentity b) ⟩
  b · ε          ≡⟨ ·-rightCong (sym (rightInverse a)) ⟩
  b · (a · a ⁻¹) ≡⟨ sym (assoc b a (a ⁻¹)) ⟩
  b · a · a ⁻¹   ≡⟨ ·-leftCong h ⟩
  c · a · a ⁻¹   ≡⟨ assoc c a (a ⁻¹) ⟩
  c · (a · a ⁻¹) ≡⟨ ·-rightCong (rightInverse a) ⟩
  c · ε          ≡⟨ rightIdentity c ⟩
  c              ∎

-- Adapted from the Agda standard library 0.8.1 (see
-- Algebra.Properties.Group.right-helper).
y≡x⁻¹[xy] : ∀ a b → b ≡ a ⁻¹ · (a · b)
y≡x⁻¹[xy] a b = b              ≡⟨ sym (leftIdentity b) ⟩
                ε · b          ≡⟨ ·-leftCong (sym (leftInverse a)) ⟩
                a ⁻¹ · a · b   ≡⟨ assoc (a ⁻¹) a b ⟩
                a ⁻¹ · (a · b) ∎

-- Adapted from the Agda standard library 0.8.1 (see
-- Algebra.Properties.Group.left-helper).
x≡[xy]y⁻¹ : ∀ a b → a ≡ (a · b) · b ⁻¹
x≡[xy]y⁻¹ a b = a              ≡⟨ sym (rightIdentity a) ⟩
                a · ε          ≡⟨ ·-rightCong (sym (rightInverse b)) ⟩
                a · (b · b ⁻¹) ≡⟨ sym (assoc a b (b ⁻¹)) ⟩
                a · b · b ⁻¹   ∎

rightIdentityUnique : ∀ r → (∀ a → a · r ≡ a) → r ≡ ε
-- Paper proof (Mac Lane and Garret 1999. p. 48):
--
-- 1. r  = εr (ε is an identity)
-- 2. εr = r  (hypothesis)
-- 3. r  = ε  (transitivity)
rightIdentityUnique r h = trans (sym (leftIdentity r)) (h ε)

-- A more appropiate version to be used in the proofs. Adapted from
-- the Agda standard library 0.8.1 (see
-- Algebra.Properties.Group.right-identity-unique).
rightIdentityUnique' : ∀ a r → a · r ≡ a → r ≡ ε
rightIdentityUnique' a r h = r              ≡⟨ y≡x⁻¹[xy] a r ⟩
                             a ⁻¹ · (a · r) ≡⟨ ·-rightCong h ⟩
                             a ⁻¹ · a       ≡⟨ leftInverse a ⟩
                             ε              ∎

leftIdentityUnique : ∀ l → (∀ a → l · a ≡ a) → l ≡ ε
-- Paper proof:
-- 1. l  = le (ε is an identity)
-- 2. le = e  (hypothesis)
-- 3. l  = e  (transitivity)
leftIdentityUnique l h = trans (sym (rightIdentity l)) (h ε)

-- A more appropiate version to be used in the proofs. Adapted from
-- the Agda standard library 0.8.1 (see
-- Algebra.Properties.Group.left-identity-unique).
leftIdentityUnique' : ∀ a l → l · a ≡ a → l ≡ ε
leftIdentityUnique' a l h = l            ≡⟨ x≡[xy]y⁻¹ l a ⟩
                            l · a · a ⁻¹ ≡⟨ ·-leftCong h ⟩
                            a · a ⁻¹     ≡⟨ rightInverse a ⟩
                            ε            ∎

rightInverseUnique : ∀ {a} → ∃[ r ] (a · r ≡ ε) ∧
                                    (∀ r' → a · r' ≡ ε → r ≡ r')
rightInverseUnique {a} =
-- Paper proof:
--
-- 1.   We know that (a⁻¹) is a right inverse for a.
-- 2.   Let's suppose there is other right inverse r for a, i.e. ar ≡ ε, then
-- 2.1. aa⁻¹ = ε  (right-inverse axiom)
-- 2.2. ar   = ε  (hypothesis)
-- 2.3. aa⁻¹ = ar (transitivity)
-- 2.4  a⁻¹  = a  (left-cancellation)
  _ , rightInverse a , prf
    where
    prf : ∀ r' → a · r' ≡ ε → a ⁻¹ ≡ r'
    prf r' ar'≡ε = leftCancellation aa⁻¹≡ar'
      where
      aa⁻¹≡ar' : a · a ⁻¹ ≡ a · r'
      aa⁻¹≡ar' = a · a ⁻¹ ≡⟨ rightInverse a ⟩
                 ε        ≡⟨ sym ar'≡ε ⟩
                 a · r'   ∎

-- A more appropiate version to be used in the proofs.
rightInverseUnique' : ∀ {a r} → a · r ≡ ε → a ⁻¹ ≡ r
rightInverseUnique' {a} {r} ar≡ε = leftCancellation aa⁻¹≡ar
  where
  aa⁻¹≡ar : a · a ⁻¹ ≡ a · r
  aa⁻¹≡ar = a · a ⁻¹ ≡⟨ rightInverse a ⟩
            ε        ≡⟨ sym ar≡ε ⟩
            a · r    ∎

leftInverseUnique : ∀ {a} → ∃[ l ] (l · a ≡ ε) ∧
                                   (∀ l' → l' · a ≡ ε → l ≡ l')
leftInverseUnique {a} =
-- Paper proof:
--
-- 1.   We know that (a⁻¹) is a left inverse for a.
-- 2.   Let's suppose there is other right inverse l for a, i.e. la ≡ ε, then
-- 2.1. a⁻¹a = ε  (left-inverse axiom)
-- 2.2. la   = ε  (hypothesis)
-- 2.3. a⁻¹a = la (transitivity)
-- 2.4  a⁻¹  = l  (right-cancellation)
  _ , leftInverse a , prf
    where
    prf : ∀ l' → l' · a ≡ ε → a ⁻¹ ≡ l'
    prf l' l'a≡ε = rightCancellation a⁻¹a≡l'a
      where
      a⁻¹a≡l'a : a ⁻¹ · a ≡ l' · a
      a⁻¹a≡l'a = a ⁻¹ · a ≡⟨ leftInverse a ⟩
                 ε        ≡⟨ sym l'a≡ε ⟩
                 l' · a   ∎

-- A more appropiate version to be used in the proofs.
leftInverseUnique' : ∀ {a l} → l · a ≡ ε → a ⁻¹ ≡ l
leftInverseUnique' {a} {l} la≡ε = rightCancellation a⁻¹a≡la
  where
  a⁻¹a≡la : a ⁻¹ · a ≡ l · a
  a⁻¹a≡la = a ⁻¹ · a ≡⟨ leftInverse a ⟩
            ε        ≡⟨ sym la≡ε ⟩
            l · a    ∎

⁻¹-involutive : ∀ a → a ⁻¹ ⁻¹ ≡ a
-- Paper proof:
--
-- 1. a⁻¹a = ε  (left-inverse axiom)
-- 2. The previous equation states that a is the unique right
-- inverse (a⁻¹)⁻¹ of a⁻¹.
⁻¹-involutive a = rightInverseUnique' (leftInverse a)

identityInverse : ε ⁻¹ ≡ ε
-- Paper proof:
--
-- 1. εε = ε  (left/right-identity axiom)
-- 2. The previous equation states that ε is the unique left/right
-- inverse ε⁻¹ of ε.
identityInverse = rightInverseUnique' (leftIdentity ε)

inverseDistribution : ∀ a b → (a · b) ⁻¹ ≡ b ⁻¹ · a ⁻¹
-- Paper proof:
--
-- (b⁻¹a⁻¹)(ab) = b⁻¹(a⁻¹(ab)) (associative axiom)
--              = b⁻¹(a⁻¹a)b   (associative axiom)
--              = b⁻¹(εb)      (left-inverse axiom)
--              = b⁻¹b         (left-identity axiom)
--              = ε            (left-inverse axiom)
-- Therefore, b⁻¹a⁻¹ is the unique left inverse of ab.
inverseDistribution a b = leftInverseUnique' b⁻¹a⁻¹[ab]≡ε
  where
  b⁻¹a⁻¹[ab]≡ε : b ⁻¹ · a ⁻¹ · (a · b) ≡ ε
  b⁻¹a⁻¹[ab]≡ε =
    b ⁻¹ · a ⁻¹ · (a · b)
      ≡⟨ assoc (b ⁻¹) (a ⁻¹) (a · b) ⟩
    b ⁻¹ · (a ⁻¹ · (a · b))
      ≡⟨ ·-rightCong (sym (assoc (a ⁻¹) a b)) ⟩
    b ⁻¹ · (a ⁻¹ · a · b)
      ≡⟨ ·-rightCong (·-leftCong (leftInverse a)) ⟩
    b ⁻¹ · (ε · b)
      ≡⟨ ·-rightCong (leftIdentity b) ⟩
    b ⁻¹ · b
      ≡⟨ leftInverse b ⟩
    ε ∎

-- If the square of every element is the identity, the system is
-- commutative. From: TPTP 6.4.0 problem GRP/GRP001-2.p.
x²≡ε→comm : (∀ a → a · a ≡ ε) → ∀ {b c d} → b · c ≡ d → c · b ≡ d
-- Paper proof:
--
-- 1. d(bc)  = dd  (hypothesis bc = d)
-- 2. d(bc)  = ε   (hypothesis dd = ε)
-- 3. d(bc)c = c   (by 2)
-- 4. db(cc) = c   (associativity axiom)
-- 5. db     = c   (hypothesis cc = ε)
-- 6. (db)b  = cb  (by 5)
-- 7. d(bb)  = cb  (associativity axiom)
-- 6. d      = cb  (hypothesis bb = ε)
x²≡ε→comm h {b} {c} {d} bc≡d = sym d≡cb
  where
  db≡c : d · b ≡ c
  db≡c =
    d · b
      ≡⟨ sym (rightIdentity (d · b)) ⟩
    d · b · ε
      ≡⟨ ·-rightCong (sym (h c)) ⟩
    d · b · (c · c)
      ≡⟨ assoc d b (c · c) ⟩
    d · (b · (c · c))
      ≡⟨ ·-rightCong (sym (assoc b c c)) ⟩
    d · ((b · c) · c)
      ≡⟨ ·-rightCong (·-leftCong bc≡d) ⟩
    d · (d · c)
      ≡⟨ sym (assoc d d c) ⟩
    d · d · c
      ≡⟨ ·-leftCong (h d) ⟩
    ε · c
      ≡⟨ leftIdentity c ⟩
    c ∎

  d≡cb : d ≡ c · b
  d≡cb = d           ≡⟨ sym (rightIdentity d) ⟩
         d · ε       ≡⟨ ·-rightCong (sym (h b)) ⟩
         d · (b · b) ≡⟨ sym (assoc d b b) ⟩
         d · b · b   ≡⟨ ·-leftCong db≡c ⟩
         c · b       ∎

------------------------------------------------------------------------------
-- References
--
-- Mac Lane, S. and Birkhof, G. (1999). Algebra. 3rd ed. AMS Chelsea
-- Publishing.


text:
-- intrinsically-typed λ-calculus

module IntrinsicallyTypedLC where

open import Data.List
open import Data.List.Relation.Unary.All
open import Data.Unit
open import Data.Nat

-- definitions

data Ty : Set where
  Tunit : Ty
  Tfun : Ty → Ty → Ty

TEnv = List Ty

data _∈_ : Ty → TEnv → Set where
  here : ∀ {t Φ} → t ∈ (t ∷ Φ)
  there : ∀ {t t' Φ} → t ∈ Φ → t ∈ (t' ∷ Φ)

data Exp : TEnv → Ty → Set where
  Var : ∀ {Φ t} → (x : t ∈ Φ) → Exp Φ t
  Abs : ∀ {Φ t t'} → Exp (t ∷ Φ) t' → Exp Φ (Tfun t t')
  App : ∀ {Φ t t'} → Exp Φ (Tfun t t') → Exp Φ t → Exp Φ t'

-- big-step semantics

Val : Ty → Set
Val Tunit = ⊤
Val (Tfun t t₁) = Val t → Val t₁

access : ∀ {t Φ} → t ∈ Φ → All Val Φ → Val t
access here (px ∷ ρ) = px
access (there x) (px ∷ ρ) = access x ρ

eval : ∀ {Φ t} → Exp Φ t → All Val Φ → Val t
eval (Var x) ρ = access x ρ
eval (Abs e) ρ = λ x → eval e (x ∷ ρ)
eval (App e e₁) ρ = (eval e ρ) (eval e₁ ρ)

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous equality
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary.HeterogeneousEquality.

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.HeterogeneousEquality.Core where

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

------------------------------------------------------------------------
-- Heterogeneous equality

infix 4 _≅_

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

------------------------------------------------------------------------
-- Conversion

≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
≅-to-≡ refl = refl

≡-to-≅ : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≅ y
≡-to-≅ refl = refl


text:
module Problem4 where

infixr 40 _::_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

-- 4.1

map : {A B : Set} -> (A -> B) -> List A -> List B
map f []        = []
map f (x :: xs) = f x :: map f xs

infixr 40 _++_

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

-- 4.2

infixr 40 _▹_

data All {A : Set}(P : A -> Set) : List A -> Set where
  ∅   : All P []
  _▹_ : {x : A} -> P x -> {xs : List A} -> All P xs -> All P (x :: xs)

-- 4.3

data Some {A : Set}(P : A -> Set) : List A -> Set where
  hd : {x : A} -> P x -> {xs : List A}   -> Some P (x :: xs)
  tl : {x : A}{xs : List A} -> Some P xs -> Some P (x :: xs)

-- 4.4

-- We need composition at a higher universe here.

_∘¹_ : {A B : Set}{C : B -> Set1}(f : (x : B) -> C x)
       (g : A -> B)(x : A) -> C (g x)
(f ∘¹ g) x = f (g x)

-- You might have to give f explictly when applying this theorem.

all-map : {A B : Set}{P : A -> Set}{Q : B -> Set}{f : A -> B}{xs : List A} ->
          ({x : A} -> P x -> Q (f x)) ->
          All P xs -> All Q (map f xs)
all-map h ∅        = ∅
all-map h (p ▹ ps) = h p ▹ all-map h ps

all-++ : {A : Set}{P : A -> Set}{xs ys : List A} ->
         All P xs -> All P ys -> All P (xs ++ ys)
all-++ ∅        qs = qs
all-++ (p ▹ ps) qs = p ▹ (all-++ ps qs)

some-map : {A B : Set}{P : A -> Set}{Q : B -> Set}{f : A -> B}{xs : List A} ->
           ({x : A} -> P x -> Q (f x)) ->
           Some P xs -> Some Q (map f xs)
some-map h (hd p)  = hd (h p)
some-map h (tl ps) = tl (some-map h ps)

some-++-left : {A : Set}{P : A -> Set}{xs ys : List A} ->
               Some P xs -> Some P (xs ++ ys)
some-++-left (hd p)  = hd p
some-++-left (tl ps) = tl (some-++-left ps)

-- Here we can't expect to infer xs, so we make it explicit

some-++-right : {A : Set}{P : A -> Set}(xs : List A){ys : List A} ->
               Some P ys -> Some P (xs ++ ys)
some-++-right []        p = p
some-++-right (x :: xs) p = tl (some-++-right xs p)

-- 4.5

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

_∈_ : {A : Set} -> A -> List A -> Set
x ∈ xs = Some (_==_ x) xs

-- 4.6

record True : Set where

tt : True
tt = record {}

Nat  = List True

zero : Nat
zero = []

suc : Nat -> Nat
suc n = tt :: n

Vec : Set -> Nat -> Set
Vec A n = All (\_ -> A) n

Fin : Nat -> Set
Fin n = Some (\_ -> True) n

-- 4.7

infixr 5 _,_

data _×_ (A : Set)(B : A -> Set) : Set where
  _,_ : (x : A) -> B x -> A × B

_∧_ : Set -> Set -> Set
A ∧ B = A × (\_ -> B)

_!_ : {A : Set}{P : A -> Set}{Q : A -> Set}{xs : List A} ->
      All P xs -> Some Q xs -> A × (\z -> P z ∧ Q z)
∅ ! ()
(p ▹ ps) ! hd q = (_ , p , q)
(p ▹ ps) ! tl q = ps ! q

-- 4.8

data False : Set where

¬_ : Set -> Set
¬ A = A -> False

data _∨_ (A B : Set) : Set where
  inl : A -> A ∨ B
  inr : B -> A ∨ B

data Bool : Set where
  true  : Bool
  false : Bool

data IsTrue : Bool -> Set where
  isTrue : IsTrue true

Holds : {A : Set} -> (A -> Bool) -> A -> Set
Holds p x = IsTrue (p x)

false-isn't-true : ¬ IsTrue false
false-isn't-true ()

decide : {A : Set}(p : A -> Bool)(x : A) ->
         Holds p x ∨ ¬ Holds p x
decide p x with p x
...        | true  = inl isTrue
...        | false = inr false-isn't-true

all : {A : Set}(p : A -> Bool)(xs : List A) ->
      All (Holds p) xs ∨ Some (\x -> ¬ Holds p x) xs
all p [] = inl ∅
all p (x :: xs) with decide p x
... | inr npx = inr (hd npx)
... | inl px  with all p xs
...   | inr npxs = inr (tl npxs)
...   | inl pxs  = inl (px ▹ pxs)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.RingStructure.CupProduct where

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed

open import Cubical.Data.Nat
open import Cubical.Data.Int hiding (_+'_ ; +'≡+ ; _+_)

open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.Truncation as T
open import Cubical.HITs.S1 hiding (_·_)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties

infixl 30 _·₀_
infixr 35 _⌣ₖ_
infixr 35 _⌣_

--- This definition of ℕ-addition removes some unnecessary transports.
open PlusBis

-- Cup product with one integer (K₀) argument
_·₀_ : {n : ℕ} (m : ℤ) → coHomK n → coHomK n
_·₀_ {n = n} (pos zero) x = 0ₖ _
_·₀_ {n = n} (pos (suc m)) x = x +ₖ (pos m ·₀ x)
_·₀_ {n = n} (negsuc zero) x = -ₖ x
_·₀_ {n = n} (negsuc (suc m)) x = (negsuc m ·₀ x) -ₖ x

·₀-0ₖ : {n : ℕ} (m : ℤ) → _·₀_ m (0ₖ n) ≡ 0ₖ n
·₀-0ₖ (pos zero) = refl
·₀-0ₖ (pos (suc n)) = cong (0ₖ _ +ₖ_) (·₀-0ₖ (pos n)) ∙ rUnitₖ _ (0ₖ _)
·₀-0ₖ (negsuc zero) = -0ₖ
·₀-0ₖ (negsuc (suc n)) = cong (λ x → x -ₖ (0ₖ _)) (·₀-0ₖ (negsuc n)) ∙ rCancelₖ _ (0ₖ _)

-- Pointed version first (enables truncation elimination)
⌣ₖ∙ : (n m : ℕ) → coHomK n → coHomK-ptd m →∙ coHomK-ptd (n +' m)
fst (⌣ₖ∙ zero m a) b = a ·₀ b
snd (⌣ₖ∙ zero m a) = ·₀-0ₖ a
fst (⌣ₖ∙ (suc n) zero a) b = b ·₀ a
snd (⌣ₖ∙ (suc n) zero a) = refl
⌣ₖ∙ (suc n) (suc m) = T.rec (isOfHLevel↑∙ (suc n) m) (cup n m)
  where
  cup : (n m : ℕ) → S₊ (suc n) → coHomK-ptd (suc m) →∙ coHomK-ptd (suc (suc (n + m)))
  fst (cup zero m base) _ = 0ₖ _
  fst (cup zero m (loop i)) x = Kn→ΩKn+1 _ x i
  fst (cup (suc n) m north) _ = 0ₖ _
  fst (cup (suc n) m south) _ = 0ₖ _
  fst (cup (suc n) m (merid a i)) x = Kn→ΩKn+1 _ (fst (cup n m a) x) i
  snd (cup zero m base) = refl
  snd (cup zero m (loop i)) k = Kn→ΩKn+10ₖ _ k i
  snd (cup (suc n) m north) = refl
  snd (cup (suc n) m south) = refl
  snd (cup (suc n) m (merid a i)) k = (cong (Kn→ΩKn+1 _) (snd (cup n m a)) ∙ Kn→ΩKn+10ₖ _) k i

-- Non pointed version
_⌣ₖ_ : {n m : ℕ} → coHomK n → coHomK m → coHomK (n +' m)
_⌣ₖ_ {n = n} {m = m} x y = fst (⌣ₖ∙ n m x) y

-- Doubly pointed version
⌣ₖ∙∙ : (n m : ℕ) → coHomK-ptd n →∙ (coHomK-ptd m →∙ coHomK-ptd (n +' m) ∙)
fst (⌣ₖ∙∙ n m) = ⌣ₖ∙ n m
fst (snd (⌣ₖ∙∙ zero zero) i) x = 0
fst (snd (⌣ₖ∙∙ zero (suc m)) i) x = 0ₖ _
fst (snd (⌣ₖ∙∙ (suc n) zero) i) x = ·₀-0ₖ x i
fst (snd (⌣ₖ∙∙ (suc zero) (suc m)) i) x = 0ₖ _
fst (snd (⌣ₖ∙∙ (suc (suc n)) (suc m)) i) x = 0ₖ _
snd (snd (⌣ₖ∙∙ zero zero) i) = refl
snd (snd (⌣ₖ∙∙ zero (suc m)) i) = refl
snd (snd (⌣ₖ∙∙ (suc n) zero) i) = refl
snd (snd (⌣ₖ∙∙ (suc zero) (suc m)) i) = refl
snd (snd (⌣ₖ∙∙ (suc (suc n)) (suc m)) i) = refl

-- Cup product
_⌣_ : ∀ {ℓ} {A : Type ℓ} {n m : ℕ} → coHom n A → coHom m A → coHom (n +' m) A
_⌣_ = ST.rec2 squash₂ λ f g → ∣ (λ x → f x ⌣ₖ g x) ∣₂

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- https://stackoverflow.com/questions/61037572/how-to-define-the-range-function-on-a-relation-in-agda-set-theory

module range where

open import Data.Unit
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum
open import Function

Subset : Set → Set₁
Subset A = A → Set

_∈_ : ∀ {A} → A → Subset A → Set
a ∈ P = P a

Relation : ∀ A B → Set₁
Relation A B = Subset (A × B)

Range : ∀ {A B} → Relation A B → Subset B
Range R b = ∃ (R ∘ ⟨_, b ⟩)  -- equivalent to ∃ \a → R ⟨ a , b ⟩

_⊆_ : ∀ {A} → Subset A → Subset A → Set
A ⊆ B = ∀ x → x ∈ A → x ∈ B

wholeSet : ∀ A → Subset A
wholeSet _ _ = ⊤

∀subset⊆set : ∀ {A sub} → sub ⊆ wholeSet A
∀subset⊆set _ _ = tt

_∩_ : ∀ {A} → Subset A → Subset A → Subset A
(A ∩ B) x = x ∈ A × x ∈ B

open import Data.Nat

x : Set₁
x = Subset ℕ

y : Set₁
y = Relation ℕ ℕ

z : Subset ℕ
z = Range {ℕ} λ { ⟨ n1 , n2 ⟩ → (x₁ : Σ ℕ (λ _ → ℕ)) → {!!} ∈ {!!}}

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

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

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


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- A compilation of theorems in Propositional Logic
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems ( n : ℕ ) where

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

open import Data.PropFormula.Theorems.Biimplication n public
open import Data.PropFormula.Theorems.Classical n     public
open import Data.PropFormula.Theorems.Conjunction n   public
open import Data.PropFormula.Theorems.Disjunction n   public
open import Data.PropFormula.Theorems.Implication n   public
open import Data.PropFormula.Theorems.Mixies n        public
open import Data.PropFormula.Theorems.Negation n      public
open import Data.PropFormula.Theorems.Weakening n     public

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

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition08 where

open import Common.FOL

postulate
  P  : D → Set
  op : D → D

-- In this case the proof term `Pb` is referenced in the types of the
-- definitions of `c` and `d` via the `where` clause. Therefore in the
-- translation of `c` and `d`, we need to erase this proof term.

-- TODO (2016-04-02): This test case is invalid after fixing #22.

-- foo : D → ∀ {b} → P b → D
-- foo a Pb = a
--   where
--   c : D
--   c = a
--   {-# ATP definition c #-}

--   d : D
--   d = op c
--   {-# ATP definition d #-}

--   postulate bar : d ≡ op a
--   {-# ATP prove bar #-}

-- We need to have at least one conjecture to generate a TPTP file.
postulate bar : ∀ d → d ≡ d
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary using (yes)
open import Cubical.Relation.Binary.Raw using (Decidable)

import Cubical.Data.Unit.Base as ⊤

⊤ : {ℓ : Level} → Type ℓ
⊤ = Lift ⊤.⊤

pattern tt = lift ⊤.tt

infix 4 _≟_

_≟_ : {ℓ : Level} → Decidable {A = ⊤ {ℓ}} _≡_
_ ≟ _ = yes refl

isContr⊤ : {ℓ : Level} → isContr (⊤ {ℓ})
isContr⊤ = tt , λ {tt → refl}

isProp⊤ : {ℓ : Level} → isProp (⊤ {ℓ})
isProp⊤ _ _ i = tt