text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility
------------------------------------------------------------------------

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

module Data.Nat.Divisibility where

open import Algebra
open import Data.Nat.Base
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Data.Product
open import Function.Base
open import Function.Equivalence using (_⇔_; equivalence)
open import Level using (0ℓ)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable as Dec using (False)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst)

------------------------------------------------------------------------
-- Definition

open import Data.Nat.Divisibility.Core public

------------------------------------------------------------------------
-- Relationship with _%_

m%n≡0⇒n∣m : ∀ m n → m % suc n ≡ 0 → suc n ∣ m
m%n≡0⇒n∣m m n eq = divides (m / suc n) (begin-equality
  m                               ≡⟨ m≡m%n+[m/n]*n m n ⟩
  m % suc n + m / suc n * (suc n) ≡⟨ cong₂ _+_ eq refl ⟩
  m / suc n * (suc n)             ∎)
  where open ≤-Reasoning

n∣m⇒m%n≡0 : ∀ m n → suc n ∣ m → m % suc n ≡ 0
n∣m⇒m%n≡0 m n (divides v eq) = begin-equality
  m           % suc n  ≡⟨ cong (_% suc n) eq ⟩
  (v * suc n) % suc n  ≡⟨ m*n%n≡0 v n ⟩
  0                    ∎
  where open ≤-Reasoning

m%n≡0⇔n∣m : ∀ m n → m % suc n ≡ 0 ⇔ suc n ∣ m
m%n≡0⇔n∣m m n = equivalence (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)

------------------------------------------------------------------------
-- Properties of _∣_ and _≤_

∣⇒≤ : ∀ {m n} → m ∣ suc n → m ≤ suc n
∣⇒≤ {m} {n} (divides (suc q) eq) = begin
  m          ≤⟨ m≤m+n m (q * m) ⟩
  suc q * m  ≡⟨ sym eq ⟩
  suc n      ∎
  where open ≤-Reasoning

>⇒∤ : ∀ {m n} → m > suc n → m ∤ suc n
>⇒∤ (s≤s m>n) m∣n = contradiction (∣⇒≤ m∣n) (≤⇒≯ m>n)

------------------------------------------------------------------------
-- _∣_ is a partial order

∣-reflexive : _≡_ ⇒ _∣_
∣-reflexive {n} refl = divides 1 (sym (*-identityˡ n))

∣-refl : Reflexive _∣_
∣-refl = ∣-reflexive refl

∣-trans : Transitive _∣_
∣-trans (divides p refl) (divides q refl) =
  divides (q * p) (sym (*-assoc q p _))

∣-antisym : Antisymmetric _≡_ _∣_
∣-antisym {m}     {zero}  _ (divides q refl) = *-zeroʳ q
∣-antisym {zero}  {n}     (divides p eq) _   = sym (trans eq (*-comm p 0))
∣-antisym {suc m} {suc n} p∣q           q∣p  = ≤-antisym (∣⇒≤ p∣q) (∣⇒≤ q∣p)

infix 4 _∣?_

_∣?_ : Decidable _∣_
zero  ∣? zero   = yes (divides 0 refl)
zero  ∣? suc m  = no ((λ()) ∘′ ∣-antisym (divides 0 refl))
suc n ∣? m      = Dec.map (m%n≡0⇔n∣m m n) (m % suc n ≟ 0)

∣-isPreorder : IsPreorder _≡_ _∣_
∣-isPreorder = record
  { isEquivalence = PropEq.isEquivalence
  ; reflexive     = ∣-reflexive
  ; trans         = ∣-trans
  }

∣-isPartialOrder : IsPartialOrder _≡_ _∣_
∣-isPartialOrder = record
  { isPreorder = ∣-isPreorder
  ; antisym    = ∣-antisym
  }

∣-preorder : Preorder 0ℓ 0ℓ 0ℓ
∣-preorder = record
  { isPreorder = ∣-isPreorder
  }

∣-poset : Poset 0ℓ 0ℓ 0ℓ
∣-poset = record
  { isPartialOrder = ∣-isPartialOrder
  }

------------------------------------------------------------------------
-- A reasoning module for the _∣_ relation

module ∣-Reasoning where
  private
    module Base = PreorderReasoning ∣-preorder

  open Base public
    hiding (step-≈; step-≈˘; step-∼)

  infixr 2 step-∣
  step-∣ = Base.step-∼
  syntax step-∣ x y∣z x∣y = x ∣⟨ x∣y ⟩ y∣z

------------------------------------------------------------------------
-- Simple properties of _∣_

infix 10 1∣_ _∣0

1∣_ : ∀ n → 1 ∣ n
1∣ n = divides n (sym (*-identityʳ n))

_∣0 : ∀ n → n ∣ 0
n ∣0 = divides 0 refl

0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
0∣⇒≡0 {n} 0∣n = ∣-antisym (n ∣0) 0∣n

∣1⇒≡1 : ∀ {n} → n ∣ 1 → n ≡ 1
∣1⇒≡1 {n} n∣1 = ∣-antisym n∣1 (1∣ n)

n∣n : ∀ {n} → n ∣ n
n∣n {n} = ∣-refl

------------------------------------------------------------------------
-- Properties of _∣_ and _+_

∣m∣n⇒∣m+n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
∣m∣n⇒∣m+n (divides p refl) (divides q refl) =
  divides (p + q) (sym (*-distribʳ-+ _ p q))

∣m+n∣m⇒∣n : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
∣m+n∣m⇒∣n {i} {m} {n} (divides p m+n≡p*i) (divides q m≡q*i) =
  divides (p ∸ q) $ begin-equality
    n             ≡⟨ sym (m+n∸n≡m n m) ⟩
    n + m ∸ m     ≡⟨ cong (_∸ m) (+-comm n m) ⟩
    m + n ∸ m     ≡⟨ cong₂ _∸_ m+n≡p*i m≡q*i ⟩
    p * i ∸ q * i ≡⟨ sym (*-distribʳ-∸ i p q) ⟩
    (p ∸ q) * i   ∎
  where open ∣-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and _*_

n∣m*n : ∀ m {n} → n ∣ m * n
n∣m*n m = divides m refl

m∣m*n : ∀ {m} n → m ∣ m * n
m∣m*n n = divides n (*-comm _ n)

∣m⇒∣m*n : ∀ {i m} n → i ∣ m → i ∣ m * n
∣m⇒∣m*n {i} {m} n (divides q refl) = ∣-trans (n∣m*n q) (m∣m*n n)

∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
∣n⇒∣m*n {i} m {n} i∣n = subst (i ∣_) (*-comm n m) (∣m⇒∣m*n m i∣n)

*-monoʳ-∣ : ∀ {i j} k → i ∣ j → k * i ∣ k * j
*-monoʳ-∣ {i} {j} k (divides q refl) = divides q $ begin-equality
  k * (q * i)  ≡⟨ sym (*-assoc k q i) ⟩
  (k * q) * i  ≡⟨ cong (_* i) (*-comm k q) ⟩
  (q * k) * i  ≡⟨ *-assoc q k i ⟩
  q * (k * i)  ∎
  where open ≤-Reasoning

*-monoˡ-∣ : ∀ {i j} k → i ∣ j → i * k ∣ j * k
*-monoˡ-∣ {i} {j} k rewrite *-comm i k | *-comm j k = *-monoʳ-∣ k

*-cancelˡ-∣ : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j
*-cancelˡ-∣ {i} {j} k (divides q eq) =
  divides q $ *-cancelʳ-≡ j (q * i) $ begin-equality
    j * (suc k)      ≡⟨ *-comm j (suc k) ⟩
    suc k * j        ≡⟨ eq ⟩
    q * (suc k * i)  ≡⟨ cong (q *_) (*-comm (suc k) i) ⟩
    q * (i * suc k)  ≡⟨ sym (*-assoc q i (suc k)) ⟩
    (q * i) * suc k  ∎
    where open ≤-Reasoning

*-cancelʳ-∣ : ∀ {i j} k {k≢0 : False (k ≟ 0)} → i * k ∣ j * k → i ∣ j
*-cancelʳ-∣ {i} {j} k@(suc k-1) rewrite *-comm i k | *-comm j k = *-cancelˡ-∣ k-1

------------------------------------------------------------------------
-- Properties of _∣_ and _∸_

∣m∸n∣n⇒∣m : ∀ i {m n} → n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
∣m∸n∣n⇒∣m i {m} {n} n≤m (divides p m∸n≡p*i) (divides q n≡q*o) =
  divides (p + q) $ begin-equality
    m             ≡⟨ sym (m+[n∸m]≡n n≤m) ⟩
    n + (m ∸ n)   ≡⟨ +-comm n (m ∸ n) ⟩
    m ∸ n + n     ≡⟨ cong₂ _+_ m∸n≡p*i n≡q*o ⟩
    p * i + q * i ≡⟨ sym (*-distribʳ-+ i p q)  ⟩
    (p + q) * i   ∎
  where open ≤-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and _/_

m/n∣m : ∀ {m n n≢0} → n ∣ m → (m / n) {n≢0} ∣ m
m/n∣m {m} {n} (divides p refl) = begin
  p * n / n ≡⟨ m*n/n≡m p n ⟩
  p         ∣⟨ m∣m*n n ⟩
  p * n     ∎
  where open ∣-Reasoning

m*n∣o⇒m∣o/n : ∀ m n {o n≢0} → m * n ∣ o → m ∣ (o / n) {n≢0}
m*n∣o⇒m∣o/n m n {_} {≢0} (divides p refl) = begin
  m               ∣⟨ n∣m*n p ⟩
  p * m           ≡⟨ sym (*-identityʳ (p * m)) ⟩
  p * m * 1       ≡⟨ sym (cong (p * m *_) (n/n≡1 n)) ⟩
  p * m * (n / n) ≡⟨ sym (*-/-assoc (p * m) {≢0 = ≢0} (n∣n {n})) ⟩
  p * m * n / n   ≡⟨ cong (λ v → (v / n) {≢0}) (*-assoc p m n) ⟩
  p * (m * n) / n ∎
  where open ∣-Reasoning

m*n∣o⇒n∣o/m : ∀ m n {o n≢0} → m * n ∣ o → n ∣ (o / m) {n≢0}
m*n∣o⇒n∣o/m m n {o} {≢0} rewrite *-comm m n = m*n∣o⇒m∣o/n n m {o} {≢0}

m∣n/o⇒m*o∣n : ∀ {m n o n≢0} → o ∣ n → m ∣ (n / o) {n≢0} → m * o ∣ n
m∣n/o⇒m*o∣n {m} {n} {o} (divides p refl) m∣p*o/o = begin
  m * o ∣⟨ *-monoˡ-∣ o (subst (m ∣_) (m*n/n≡m p o) m∣p*o/o) ⟩
  p * o ∎
  where open ∣-Reasoning

m∣n/o⇒o*m∣n : ∀ {m n o o≢0} → o ∣ n → m ∣ (n / o) {o≢0} → o * m ∣ n
m∣n/o⇒o*m∣n {m} {_} {o} {≢0} rewrite *-comm o m = m∣n/o⇒m*o∣n {n≢0 = ≢0}

m/n∣o⇒m∣o*n : ∀ {m n o n≢0} → n ∣ m → (m / n) {n≢0} ∣ o → m ∣ o * n
m/n∣o⇒m∣o*n {_} {n} {o} (divides p refl) p*n/n∣o = begin
  p * n ∣⟨ *-monoˡ-∣ n (subst (_∣ o) (m*n/n≡m p n) p*n/n∣o) ⟩
  o * n ∎
  where open ∣-Reasoning

m∣n*o⇒m/n∣o : ∀ {m n o n≢0} → n ∣ m → m ∣ o * n → (m / n) {n≢0} ∣ o
m∣n*o⇒m/n∣o {_} {n@(suc _)} {o} (divides p refl) pn∣on = begin
  p * n / n ≡⟨ m*n/n≡m p n ⟩
  p         ∣⟨ *-cancelʳ-∣ n pn∣on ⟩
  o         ∎
  where open ∣-Reasoning

------------------------------------------------------------------------
-- Properties of _∣_ and _%_

∣n∣m%n⇒∣m : ∀ {m n d ≢0} → d ∣ n → d ∣ (m % n) {≢0} → d ∣ m
∣n∣m%n⇒∣m {m} {n@(suc n-1)} {d} (divides a n≡ad) (divides b m%n≡bd) =
  divides (b + (m / n) * a) (begin-equality
    m                         ≡⟨ m≡m%n+[m/n]*n m n-1 ⟩
    m % n + (m / n) * n       ≡⟨ cong₂ _+_ m%n≡bd (cong (m / n *_) n≡ad) ⟩
    b * d + (m / n) * (a * d) ≡⟨ sym (cong (b * d +_) (*-assoc (m / n) a d)) ⟩
    b * d + ((m / n) * a) * d ≡⟨ sym (*-distribʳ-+ d b _) ⟩
    (b + (m / n) * a) * d     ∎)
    where open ≤-Reasoning

%-presˡ-∣ : ∀ {m n d ≢0} → d ∣ m → d ∣ n → d ∣ (m % n) {≢0}
%-presˡ-∣ {m} {n@(suc n-1)} {d} (divides a refl) (divides b 1+n≡bd) =
  divides (a ∸ ad/n * b) $ begin-equality
    a * d % n              ≡⟨ m%n≡m∸m/n*n (a * d) n-1 ⟩
    a * d ∸ ad/n * n       ≡⟨ cong (λ v → a * d ∸ ad/n * v) 1+n≡bd ⟩
    a * d ∸ ad/n * (b * d) ≡⟨ sym (cong (a * d ∸_) (*-assoc ad/n b d)) ⟩
    a * d ∸ (ad/n * b) * d ≡⟨ sym (*-distribʳ-∸ d a (ad/n * b)) ⟩
    (a ∸ ad/n * b) * d     ∎
  where open ≤-Reasoning; ad/n = a * d / n

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

-- Version 0.14

∣-+ = ∣m∣n⇒∣m+n
{-# WARNING_ON_USAGE ∣-+
"Warning: ∣-+ was deprecated in v0.14.
Please use ∣m∣n⇒∣m+n instead."
#-}
∣-∸ = ∣m+n∣m⇒∣n
{-# WARNING_ON_USAGE ∣-∸
"Warning: ∣-∸ was deprecated in v0.14.
Please use ∣m+n∣m⇒∣n instead."
#-}
∣-* = n∣m*n
{-# WARNING_ON_USAGE ∣-*
"Warning: ∣-* was deprecated in v0.14.
Please use n∣m*n instead."
#-}

-- Version 0.17

open import Data.Fin.Base using (Fin; zero; suc; toℕ)
import Data.Fin.Properties as FP
open import Data.Nat.Solver
open +-*-Solver

nonZeroDivisor-lemma : ∀ m q (r : Fin (1 + m)) → toℕ r ≢ 0 →
                       1 + m ∤ toℕ r + q * (1 + m)
nonZeroDivisor-lemma m zero r r≢zero (divides zero eq) = r≢zero $ begin-equality
  toℕ r      ≡⟨ sym (*-identityˡ (toℕ r)) ⟩
  1 * toℕ r  ≡⟨ eq ⟩
  0          ∎
  where open ≤-Reasoning
nonZeroDivisor-lemma m zero r r≢zero (divides (suc q) eq) =
  m+1+n≰m m $ begin
    m + suc (q * suc m) ≡⟨ +-suc m (q * suc m) ⟩
    suc (m + q * suc m) ≡⟨ sym eq ⟩
    1 * toℕ r           ≡⟨ *-identityˡ (toℕ r) ⟩
    toℕ r               ≤⟨ FP.toℕ≤pred[n] r ⟩
    m                   ∎
    where open ≤-Reasoning
nonZeroDivisor-lemma m (suc q) r r≢zero d =
  nonZeroDivisor-lemma m q r r≢zero (∣m+n∣m⇒∣n d' ∣-refl)
  where
  lem = solve 3 (λ m r q → r :+ (m :+ q)  :=  m :+ (r :+ q))
                refl (suc m) (toℕ r) (q * suc m)
  d' = subst (1 + m ∣_) lem d
{-# WARNING_ON_USAGE nonZeroDivisor-lemma
"Warning: nonZeroDivisor-lemma was deprecated in v0.17."
#-}

-- Version 1.1

poset = ∣-poset
{-# WARNING_ON_USAGE poset
"Warning: poset was deprecated in v1.1.
Please use ∣-poset instead."
#-}
*-cong = *-monoʳ-∣
{-# WARNING_ON_USAGE *-cong
"Warning: *-cong was deprecated in v1.1.
Please use *-monoʳ-∣ instead."
#-}
/-cong = *-cancelˡ-∣
{-# WARNING_ON_USAGE /-cong
"Warning: /-cong was deprecated in v1.1.
Please use *-cancelˡ-∣ instead."
#-}


text:
import Relation.Unary.Monotone as Mono

open import Data.List.Prefix
open import Data.List as List

module Category.Monad.Monotone.Heap.HList
  (T : Set)
  (V : T → List T → Set)⦃ wkV : ∀ {a} → Mono.Monotone ⊑-preorder (V a) ⦄ where

open import Level
open import Data.List.All as All
open import Data.List.All.Properties.Extra
open import Data.List.Any
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Properties.Extra
open import Data.Product
open import Data.Unit

open import Relation.Binary using (Preorder)
open import Relation.Unary hiding (_∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Unary.Monotone.Prefix {T = T}

private
  HeapT : Set
  HeapT = List T

  Heap : Pred HeapT _
  Heap = λ W → All (λ a → V a W) W

open Mono (⊑-preorder {A = T})
open import Category.Monad.Monotone (⊑-preorder {A = T})
open import Category.Monad.Monotone.State ⊑-preorder Heap
open import Category.Monad.Monotone.Heap ⊑-preorder T V Heap _∈_
open import Category.Monad using (RawMonad)

module _ {M : Set → Set}⦃ Mon : RawMonad M ⦄ where
  private module M = RawMonad Mon

  hlist-heap-monad : HeapMonad (MST M)
  HeapMonad.store hlist-heap-monad {a}{i} sv μ =
    let ext = ∷ʳ-⊒ a i in M.return (_ , ext , (wk ext μ all-∷ʳ wk ext sv) , ∈-∷ʳ i a )
  HeapMonad.modify hlist-heap-monad ptr v μ =
    M.return (_ , ⊑-refl , μ All[ ptr ]≔' v , lift tt)
  HeapMonad.deref hlist-heap-monad ptr μ =
    M.return (_ , ⊑-refl , μ , ∈-all ptr μ)

ext: agda


text:
import Relation.Binary.PropositionalEquality
module Data.Bin.Multiplication where
  private module PropEq = Relation.Binary.PropositionalEquality

  module ℕ-lemmas where
    open import Data.Nat
    open import Data.Nat.Properties
    open import Relation.Binary.PropositionalEquality
    open SemiringSolver

    *-2-3-comm : ∀ x y z → x * y * z ≡ x * z * y
    *-2-3-comm x y z = solve 3 (λ x y z → x :* y :* z := x :* z :* y) refl x y z

    n+x≡0→n≡0 : ∀ {n x} → n + x ≡ 0 → n ≡ 0
    n+x≡0→n≡0 {zero} = λ _ → refl
    n+x≡0→n≡0 {suc _} = λ ()

    distribʳ : ∀ a b c → (a + b) * c ≡ a * c + b * c
    distribʳ a b c = solve 3 (λ a b c → (a :+ b) :* c := a :* c :+ b :* c) refl a b c

  open PropEq using (_≡_; cong; cong₂; trans; sym; [_]; inspect)
  open import Data.Bin using (_*2; toℕ; 0#; _1#; Bin; pred; _*_; _+_)
  open import Data.Nat using (ℕ; zero; suc)
                     renaming (_*_ to _ℕ*_; _+_ to _ℕ+_)
  open import Data.Nat.Properties using (isCommutativeSemiring)
  open import Algebra.Structures
     using (module IsCommutativeSemiring;
            module IsCommutativeMonoid)
  open IsCommutativeSemiring isCommutativeSemiring
     using (+-isCommutativeMonoid; *-isCommutativeMonoid)

  open import Data.Product

  open import Relation.Nullary
  open import Data.Fin using (zero; suc) renaming (toℕ to bitToℕ)
  open import Data.Digit using (Bit)
  open import Data.List using (List; _∷_; [])
  open import Data.Bin.Utils

  open import Data.Bin.Bijection using (fromℕ-bijection; toℕ-inj)
  import Relation.Binary.PropositionalEquality
  open Relation.Binary.PropositionalEquality.≡-Reasoning

  import Data.Bin.Addition
  open Data.Bin.Addition using (+-is-addition)
  module B+ICM = IsCommutativeMonoid Data.Bin.Addition.is-commutativeMonoid
  open B+ICM using () renaming (identity to +-identity; ∙-cong to +-cong)

  *2-is-*2 : ∀ x → toℕ (x *2) ≡ toℕ x ℕ* 2
  *2-is-*2 0# = PropEq.refl
  *2-is-*2 (bs 1#) = PropEq.refl

  bitToX-≡ : ∀ x → bitToℕ x ≡ toℕ (bitToBin x)
  bitToX-≡ zero = PropEq.refl
  bitToX-≡ (suc zero) = PropEq.refl
  bitToX-≡ (suc (suc ()))

  ∷1#-interpretation : ∀ (b : Bit) (bs : List Bit) → ((b ∷ bs) 1#) ≡ bitToBin b + (bs 1#) *2
  ∷1#-interpretation b bs = toℕ-inj (
   begin
    toℕ ((b ∷ bs) 1#)
     ≡⟨ PropEq.refl ⟩
    bitToℕ b ℕ+ toℕ (bs 1#) ℕ* 2
     ≡⟨ cong₂ _ℕ+_ (bitToX-≡ b) (sym (*2-is-*2 (bs 1#))) ⟩
    toℕ (bitToBin b) ℕ+ toℕ ((bs 1#) *2)
     ≡⟨ sym (+-is-addition (bitToBin b) ((bs 1#) *2)) ⟩
    toℕ (bitToBin b + (bs 1#) *2)
   ∎)

  open import Function using (_⟨_⟩_)

  multBit : Bit → Bin → Bin
  multBit zero _ = 0#
  multBit (suc zero) n = n
  multBit (suc (suc ())) _

  n+x≡0→n≡0 : ∀ {n x} → n + x ≡ 0# → n ≡ 0#
  n+x≡0→n≡0 {n} {x} n+x≡0 = toℕ-inj (ℕ-lemmas.n+x≡0→n≡0 ((sym (+-is-addition n x)) ⟨ trans ⟩ cong toℕ n+x≡0))

  1+*n≡0→n≡0 : ∀ {l} n → l 1# * n ≡ 0# → n ≡ 0#
  1+*n≡0→n≡0 {[]} n eq = eq
  1+*n≡0→n≡0 {h ∷ t} n eq with t 1# * n | PropEq.inspect (λ n → (t 1# * n)) n
  1+*n≡0→n≡0 {h ∷ t} n _ | 0# | [ eq ] = 1+*n≡0→n≡0 {t} n eq
  1+*n≡0→n≡0 {zero ∷ t} n eq | (l 1#) | [ eq2 ] rewrite eq2 with eq
  ... | ()
  1+*n≡0→n≡0 {suc zero ∷ t} n eq | (l 1#) | [ eq2 ] rewrite eq2 = n+x≡0→n≡0 {n} {(zero ∷ l) 1#} eq
  1+*n≡0→n≡0 {suc (suc ()) ∷ t} n eq | _ | _

  simplify-mult : ∀ x xs n → (x ∷ xs) 1# * n ≡ multBit x n + (xs 1# * n) *2
  simplify-mult x xs n with (xs 1# * n) | inspect (λ n → (xs 1# * n)) n
  simplify-mult zero xs n | 0# | [ ≡ ] rewrite ≡ = PropEq.refl
  simplify-mult (suc zero) xs n | 0# | [ ≡ ] rewrite ≡ | 1+*n≡0→n≡0 {xs} n ≡ = PropEq.refl
  simplify-mult zero xs n | (xs' 1#)  | [ ≡ ] rewrite ≡ =
    begin
      (zero ∷ xs') 1#
        ≡⟨ PropEq.refl ⟩
      (xs' 1#) *2
        ≡⟨ B+ICM.sym ( B+ICM.identityˡ ((xs' 1#) *2)) ⟩
      0# + (xs' 1#) *2
        ≡⟨ PropEq.refl ⟩
      multBit zero n + (xs' 1#) *2
    ∎
  simplify-mult (suc zero) xs n | (xs' 1#)  | [ ≡ ] rewrite ≡ =
    begin
      n + (zero ∷ xs') 1#
        ≡⟨ PropEq.refl ⟩
      multBit (suc zero) n + (xs' 1#) *2
    ∎
  simplify-mult (suc (suc ())) xs n | _ | _

  _*-def'_ : ℕ → Bin → Bin
  zero *-def' y = 0#
  (suc x) *-def' y = y + (x *-def' y)

  _*-def_ : Bin → Bin → Bin
  x *-def y = (toℕ x) *-def' y
  infixl 7 _*-def_

  *-def'-is-* : ∀ m n → toℕ (m *-def' n) ≡ m ℕ* toℕ n
  *-def'-is-* zero n = PropEq.refl
  *-def'-is-* (suc m) n = +-is-addition  n ( m *-def' n) ⟨ trans ⟩ cong (_ℕ+_ (toℕ n)) (*-def'-is-* m n)

  *-def-is-* : ∀ m n → toℕ (m *-def n) ≡ toℕ m ℕ* toℕ n
  *-def-is-* m = *-def'-is-* (toℕ m)

  *-def-*2-comm : ∀ x y → (x *-def y) *2 ≡ x *2 *-def y
  *-def-*2-comm x y = toℕ-inj (
    begin
     toℕ ((x *-def y) *2)
      ≡⟨ *2-is-*2 (x *-def y) ⟩
     toℕ (x *-def y) ℕ* 2
      ≡⟨ cong (λ x → x ℕ* 2) (*-def-is-* x y) ⟩
     toℕ x ℕ* toℕ y ℕ* 2
      ≡⟨ ℕ-lemmas.*-2-3-comm (toℕ x) (toℕ y) 2 ⟩
     toℕ x ℕ* 2 ℕ* toℕ y
      ≡⟨ cong (λ x → x ℕ* toℕ y) (sym (*2-is-*2 x)) ⟩
     toℕ (x *2) ℕ* toℕ y
      ≡⟨ sym (*-def-is-* (x *2) y) ⟩
     toℕ (x *2 *-def y)
    ∎)

  multbit-is-*-def : ∀ c x → multBit c x ≡ bitToBin c *-def x
  multbit-is-*-def zero x = PropEq.refl
  multbit-is-*-def (suc zero) x = sym (proj₂ +-identity x)
  multbit-is-*-def (suc (suc ())) x

  *-def-distribʳ : ∀ a b c → (a + b) *-def c ≡ a *-def c + b *-def c
  *-def-distribʳ a b c = toℕ-inj (
    begin
     toℕ ((a + b) *-def c)
      ≡⟨ *-def-is-* (a + b) c ⟩
     toℕ (a + b) ℕ* toℕ c
      ≡⟨ cong (λ x → x ℕ* toℕ c) (+-is-addition a b) ⟩
     (toℕ a ℕ+ toℕ b) ℕ* toℕ c
      ≡⟨ ℕ-lemmas.distribʳ (toℕ a) (toℕ b) (toℕ c) ⟩
     toℕ a ℕ* toℕ c ℕ+ toℕ b ℕ* toℕ c
      ≡⟨ cong₂ _ℕ+_ (kojo a) (kojo b) ⟩
     toℕ (a *-def c) ℕ+ toℕ (b *-def c)
      ≡⟨ sym (+-is-addition (a *-def c) (b *-def c)) ⟩
     toℕ (a *-def c + b *-def c)
    ∎
    ) where
     kojo : ∀ x → toℕ x ℕ* toℕ c ≡ toℕ (x *-def c)
     kojo x = sym (*-def-is-* x c)

  mutual
    *-is-*-def : ∀ m n → m * n ≡ m *-def n
    *-is-*-def 0# n = PropEq.refl
    *-is-*-def (l 1#) n = *-is-*-def-1# l n

    *-is-*-def-1# : ∀ l n → l 1# * n ≡ l 1# *-def n
    *-is-*-def-1# [] n = sym (proj₂ +-identity n)
    *-is-*-def-1# (x ∷ xs) n = *-is-*-def-∷ x xs n

    *-is-*-def-∷ : ∀ h t n → (h ∷ t) 1# * n ≡ ((h ∷ t) 1#) *-def n
    *-is-*-def-∷ h t n =
     begin
      (h ∷ t) 1# * n
       ≡⟨ simplify-mult h t n  ⟩
      multBit h n + (t 1# * n) *2
       ≡⟨ +-cong (multbit-is-*-def h n) (cong (λ x → x *2) (*-is-*-def-1# t n) ⟨ trans ⟩ *-def-*2-comm (t 1#) n) ⟩
      bitToBin h *-def n + t 1# *2 *-def n
       ≡⟨ sym (*-def-distribʳ (bitToBin h) (t 1# *2) n) ⟩
      (bitToBin h + t 1# *2) *-def n
       ≡⟨ cong (λ x → x *-def n) (sym (∷1#-interpretation h t)) ⟩
      ((h ∷ t) 1#) *-def n
     ∎

  *-*2-comm : ∀ x y → (x * y) *2 ≡ x *2 * y
  *-*2-comm x y = cong _*2 (*-is-*-def x y) ⟨ trans ⟩ *-def-*2-comm x y ⟨ trans ⟩ sym (*-is-*-def (x *2) y)

  *-distribʳ : ∀ a b c → (a + b) * c ≡ a * c + b * c
  *-distribʳ a b c =
                     *-is-*-def (a + b) c
           ⟨ trans ⟩ *-def-distribʳ a b c
           ⟨ trans ⟩ sym (cong₂ _+_ (*-is-*-def a c) (*-is-*-def b c))

  *-is-multiplication : ∀ a b → toℕ (a * b) ≡ toℕ a ℕ* toℕ b
  *-is-multiplication a b = cong toℕ (*-is-*-def a b) ⟨ trans ⟩ *-def-is-* a b

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


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

module Base where

open import Types public
open import Functions public
open import Paths public
open import HLevel public
open import Equivalences public
open import Univalence public
open import Funext public
open import EquivalenceLemmas public
open import HLevelBis public
open import FiberEquivalences public

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, 2013-11-07
-- Need to drop parameters not only from constructors found by
-- instance search, but also from projection(like) functions.
module Issue670b where

open import Common.Prelude
open import Common.Equality

record Wrap (A : Set) : Set where
  constructor wrap
  field
    unwrap : A
open Wrap

module _ {A : Set} where

  g : {{i : Wrap A → A}} → Wrap A → A
  g {{i}} = i

test : g (wrap true) ≡ true
test = refl

-- Error WAS:
-- unwrap Bool (wrap true) != true of type Bool
-- when checking that the expression refl has type
-- g (wrap true) ≡ true

-- Should work now.

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Alter: An unguarded co-recursive function
------------------------------------------------------------------------------

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

module FOT.FOTC.UnguardedCorecursion.Alter.Alter where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.List

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

postulate
  alter    : D
  alter-eq : alter ≡ true ∷ false ∷ alter
{-# ATP axiom alter-eq #-}

postulate
  not₀    : D
  not₀-eq : ∀ b → not₀ · b ≡ not b
{-# ATP axiom not₀-eq #-}

postulate
  alter' : D
  alter'-eq : alter' ≡ true ∷ map not₀ alter'
{-# ATP axiom alter'-eq #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --allow-unsolved-metas #-}

-- Andreas, 2014-11-25, issue found by Christopher Jenkins
-- {-# OPTIONS -v tc.with:40 #-}

open import Common.Prelude
open import Common.Equality

infixr 5 _∷_

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)

+-suc : ∀ (n m : Nat) → n + suc m ≡ suc (n + m)
+-suc zero m    = refl
+-suc (suc n) m = cong suc (+-suc n m)

swap : ∀ {A : Set} n → Vec A (n + n) → Vec A (n + n)
swap zero [] = []
swap (suc n) (x ∷ xs) with n + suc n | +-suc n n
swap (suc n) (x ∷ y ∷ xs) | .(suc (n + n)) | refl = y ∷ x ∷ swap n xs

swap-involutive : ∀ {A : Set} n → (xs : Vec A (n + n)) →
                  swap n (swap n xs) ≡ xs
swap-involutive zero [] = refl
swap-involutive {A = A} (suc n) (x ∷ xs) with swap {A = A} (suc n)
...  | f = {!!}
-- Goal before with is:
-- swap (suc n) (swap (suc n) (x ∷ xs) | n + suc n | +-suc n n) ≡ x ∷ xs

{- ERROR WAS:
A !=< ℕ of type Set
when checking that the type
{A : Set}
(n : ℕ)
(w : Vec A (suc (n + suc n)) → Vec A (suc (n + suc n)))
(x : A)
(xs : Vec A (n + suc n)) →
w (swap (suc x) (xs ∷ w) | x + suc x | +-suc x x) ≡ x ∷ xs
of the generated with function is well-formed
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-

Basic properties about Σ-types

- Characterization of equality in Σ-types using transport ([pathSigma≡sigmaPath])

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sigma.Properties where

open import Cubical.Data.Sigma.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

open import Cubical.Data.Nat.Base

private
  variable
    ℓ : Level
    A : Type ℓ
    B : (a : A) → Type ℓ

ΣPathP : ∀ {x y}
  → Σ (fst x ≡ fst y) (λ a≡ → PathP (λ i → B (a≡ i)) (snd x) (snd y))
  → x ≡ y
ΣPathP eq = λ i → (fst eq i) , (snd eq i)

Σ≡ : {x y : Σ A B}  →
     Σ (fst x ≡ fst y) (λ a≡ → PathP (λ i → B (a≡ i)) (snd x) (snd y)) ≃
     (x ≡ y)
Σ≡ {A = A} {B = B} {x} {y} = isoToEquiv (iso intro elim intro-elim elim-intro)
  where
    intro = ΣPathP

    elim : x ≡ y → Σ (fst x ≡ fst y) (λ a≡ → PathP (λ i → B (a≡ i)) (snd x) (snd y ))
    elim eq = (λ i → fst (eq i)) , λ i → snd (eq i)

    intro-elim : ∀ eq → intro (elim eq) ≡ eq
    intro-elim eq = refl

    elim-intro : ∀ eq → elim (intro eq) ≡ eq
    elim-intro eq = refl

-- Alternative version for path in Σ-types, as in the HoTT book

sigmaPathTransport : (a b : Σ A B) → Type _
sigmaPathTransport {B = B} a b =
  Σ (fst a ≡ fst b) (λ p → transport (λ i → B (p i)) (snd a) ≡ snd b)

_Σ≡T_ : (a b : Σ A B) → Type _
a Σ≡T b = sigmaPathTransport a b

-- now we prove that the alternative path space a Σ≡ b is equal to the usual path space a ≡ b

-- forward direction

private
  pathSigma-π1 : {a b : Σ A B} → a ≡ b → fst a ≡ fst b
  pathSigma-π1 p i = fst (p i)

  filler-π2 : {a b : Σ A B} → (p : a ≡ b) → I → (i : I) → B (fst (p i))
  filler-π2 {B = B} {a = a} p i =
    fill (λ i → B (fst (p i)))
         (λ t → λ { (i = i0) → coe0→i (λ j → B (fst (p j))) t (snd a)
                  ; (i = i1) → snd (p t) })
         (inS (snd a))

  pathSigma-π2 : {a b : Σ A B} → (p : a ≡ b) →
    subst B (pathSigma-π1 p) (snd a) ≡ snd b
  pathSigma-π2 p i = filler-π2 p i i1

pathSigma→sigmaPath : (a b : Σ A B) → a ≡ b → a Σ≡T b
pathSigma→sigmaPath _ _ p = (pathSigma-π1 p , pathSigma-π2 p)

-- backward direction

private
  filler-comp : (a b : Σ A B) → a Σ≡T b → I → I → Σ A B
  filler-comp {B = B} a b (p , q) i =
    hfill (λ t → λ { (i = i0) → a
                   ; (i = i1) → (p i1 , q t) })
          (inS (p i , coe0→i (λ j → B (p j)) i (snd a)))

sigmaPath→pathSigma : (a b : Σ A B) → a Σ≡T b → (a ≡ b)
sigmaPath→pathSigma a b x i = filler-comp a b x i i1

-- first homotopy

private
  homotopy-π1 : (a b : Σ A B) →
    ∀ (x : a Σ≡T b) → pathSigma-π1 (sigmaPath→pathSigma a b x) ≡ fst x
  homotopy-π1 a b x i j = fst (filler-comp a b x j (~ i))

  homotopy-π2 : (a b : Σ A B) → (p : a Σ≡T b) → (i : I) →
             (transport (λ j → B (fst (filler-comp a b p j i))) (snd a) ≡ snd b)
  homotopy-π2 {B = B} a b p i j =
    comp (λ t → B (fst (filler-comp a b p t (i ∨ j))))
         (λ t → λ { (j = i0) → coe0→i (λ t → B (fst (filler-comp a b p t i)))
                                      t (snd a)
                  ; (j = i1) → snd (sigmaPath→pathSigma a b p t)
                  ; (i = i0) → snd (filler-comp a b p t j)
                  ; (i = i1) → filler-π2 (sigmaPath→pathSigma a b p) j t })
         (snd a)

pathSigma→sigmaPath→pathSigma : {a b : Σ A B} →
  ∀ (x : a Σ≡T b) → pathSigma→sigmaPath _ _ (sigmaPath→pathSigma a b x) ≡ x
pathSigma→sigmaPath→pathSigma {a = a} p i =
  (homotopy-π1 a _ p i , homotopy-π2 a _ p (~ i))

-- second homotopy

sigmaPath→pathSigma→sigmaPath : {a b : Σ A B} →
  ∀ (x : a ≡ b) → sigmaPath→pathSigma a b (pathSigma→sigmaPath _ _ x) ≡ x
sigmaPath→pathSigma→sigmaPath {B = B} {a = a} {b = b} p i j =
  hcomp (λ t → λ { (i = i1) → (fst (p j) , filler-π2 p t j)
                 ; (i = i0) → filler-comp a b (pathSigma→sigmaPath _ _ p) j t
                 ; (j = i0) → (fst a , snd a)
                 ; (j = i1) → (fst b , filler-π2 p t i1) })
        (fst (p j) , coe0→i (λ k → B (fst (p k))) j (snd a))

pathSigma≡sigmaPath : (a b : Σ A B) → (a ≡ b) ≡ (a Σ≡T b)
pathSigma≡sigmaPath a b =
  isoToPath (iso (pathSigma→sigmaPath a b)
                 (sigmaPath→pathSigma a b)
                 (pathSigma→sigmaPath→pathSigma {a = a})
                 sigmaPath→pathSigma→sigmaPath)

discreteΣ : Discrete A → ((a : A) → Discrete (B a)) → Discrete (Σ A B)
discreteΣ {B = B} Adis Bdis (a0 , b0) (a1 , b1) = discreteΣ' (Adis a0 a1)
  where
    discreteΣ' : Dec (a0 ≡ a1) → Dec ((a0 , b0) ≡ (a1 , b1))
    discreteΣ' (yes p) = J (λ a1 p → ∀ b1 → Dec ((a0 , b0) ≡ (a1 , b1))) (discreteΣ'') p b1
      where
        discreteΣ'' : (b1 : B a0) → Dec ((a0 , b0) ≡ (a0 , b1))
        discreteΣ'' b1 with Bdis a0 b0 b1
        ... | (yes q) = yes (transport (ua Σ≡) (refl , q))
        ... | (no ¬q) = no (λ r → ¬q (subst (λ X → PathP (λ i → B (X i)) b0 b1) (Discrete→isSet Adis a0 a0 (cong fst r) refl) (cong snd r)))
    discreteΣ' (no ¬p) = no (λ r → ¬p (cong fst r))

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap as KVMap
open import LibraBFT.Base.Types
open import Data.String using (String)

-- This module defines types for an out-of-date implementation, based
-- on a previous version of LibraBFT.  It will be updated to model a
-- more recent version in future.
--
-- One important trick here is that the RoundManager type separayes
-- types that /define/ the EpochConfig and types that /use/ the
-- /EpochConfig/. The advantage of doing this separation can be seen
-- in Util.Util.liftEC, where we define a lifting of a function that
-- does not change the bits that define the EpochConfig into the whole
-- state.  This enables a more elegant approach for reasoning about
-- functions that do not change parts of the state responsible for
-- defining the epoch config.  However, the separation is not perfect,
-- so sometimes fields may be modified in EpochIndep even though there
-- is no epoch change.

module LibraBFT.Impl.Consensus.Types where
  open import LibraBFT.Impl.Base.Types                       public
  open import LibraBFT.Impl.NetworkMsg                       public
  open import LibraBFT.Abstract.Types.EpochConfig UID NodeId public
  open import LibraBFT.Impl.Consensus.Types.EpochIndep       public
  open import LibraBFT.Impl.Consensus.Types.EpochDep         public

  record EpochState : Set where
    constructor EpochState∙new
    field
      ₋esEpoch    : Epoch
      ₋esVerifier : ValidatorVerifier
  open EpochState public
  unquoteDecl esEpoch esVerifier = mkLens (quote EpochState)
    (esEpoch ∷ esVerifier ∷ [])

  -- The parts of the state of a peer that are used to
  -- define the EpochConfig are the SafetyRules and ValidatorVerifier:
  record RoundManagerEC : Set where
    constructor RoundManagerEC∙new
    field
      ₋rmEpochState   : EpochState
      ₋rmSafetyRules  : SafetyRules
  open RoundManagerEC public
  unquoteDecl rmEpochState rmSafetyRules = mkLens (quote RoundManagerEC)
    (rmEpochState ∷ rmSafetyRules ∷ [])

  rmEpoch : Lens RoundManagerEC Epoch
  rmEpoch = rmEpochState ∙ esEpoch

  rmLastVotedRound : Lens RoundManagerEC Round
  rmLastVotedRound = rmSafetyRules ∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVotedRound

  -- We need enough authors to withstand the desired number of
  -- byzantine failures.  We enforce this with a predicate over
  -- 'RoundManagerEC'.
  RoundManagerEC-correct : RoundManagerEC → Set
  RoundManagerEC-correct rmec =
    let numAuthors = kvm-size (rmec ^∙ rmEpochState ∙ esVerifier ∙ vvAddressToValidatorInfo)
        qsize      = rmec ^∙ rmEpochState ∙ esVerifier ∙ vvQuorumVotingPower
        bizF       = numAuthors ∸ qsize
     in suc (3 * bizF) ≤ numAuthors

  RoundManagerEC-correct-≡ : (rmec1 : RoundManagerEC)
                             → (rmec2 : RoundManagerEC)
                             → (rmec1 ^∙ rmEpochState ∙ esVerifier) ≡ (rmec2 ^∙ rmEpochState ∙ esVerifier)
                             → RoundManagerEC-correct rmec1
                             → RoundManagerEC-correct rmec2
  RoundManagerEC-correct-≡ rmec1 rmec2 refl = id

  -- Given a well-formed set of definitions that defines an EpochConfig,
  -- α-EC will compute this EpochConfig by abstracting away the unecessary
  -- pieces from RoundManagerEC.
  -- TODO-2: update and complete when definitions are updated to more recent version
  α-EC : Σ RoundManagerEC RoundManagerEC-correct → EpochConfig
  α-EC (rmec , ok) =
    let numAuthors = kvm-size (rmec ^∙ rmEpochState ∙ esVerifier ∙ vvAddressToValidatorInfo)
        qsize      = rmec ^∙ rmEpochState ∙ esVerifier ∙ vvQuorumVotingPower
        bizF       = numAuthors ∸ qsize
     in (EpochConfig∙new {! someHash?!}
                (rmec ^∙ rmEpoch) numAuthors {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!})

  postulate
    α-EC-≡ : (rmec1  : RoundManagerEC)
           → (rmec2  : RoundManagerEC)
           → (vals≡  : rmec1 ^∙ rmEpochState ∙ esVerifier ≡ rmec2 ^∙ rmEpochState ∙ esVerifier)
           →           rmec1 ^∙ rmEpoch      ≡ rmec2 ^∙ rmEpoch
           → (rmec1-corr : RoundManagerEC-correct rmec1)
           → α-EC (rmec1 , rmec1-corr) ≡ α-EC (rmec2 , RoundManagerEC-correct-≡ rmec1 rmec2 vals≡ rmec1-corr)
  {-
  α-EC-≡ rmec1 rmec2 refl refl rmec1-corr = refl
  -}

  -- Just in case RoundManager is at a higher level in future
  ℓ-RoundManager : Level
  ℓ-RoundManager = 0ℓ

  -- Finally, the RoundManager is split in two pieces: those that are used to make an EpochConfig
  -- versus those that use an EpochConfig.  The reason is that the *abstract* EpochConfig is a
  -- function of some parts of the RoundManager (₋rmEC), and some parts depend on the abstract
  -- EpochConfig.  For example, ₋btIdToQuorumCert carries a proof that the QuorumCert is valid (for
  -- the abstract EpochConfig).
  record RoundManager : Set ℓ-RoundManager where
    constructor RoundManager∙new
    field
      ₋rmEC           : RoundManagerEC
      ₋rmEC-correct   : RoundManagerEC-correct ₋rmEC
      ₋rmWithEC       : RoundManagerWithEC (α-EC (₋rmEC , ₋rmEC-correct))
     -- If we want to add pieces that neither contribute to the
     -- construction of the EC nor need one, they should be defined in
     -- RoundManager directly
  open RoundManager public

  α-EC-RM : RoundManager → EpochConfig
  α-EC-RM rm = α-EC ((₋rmEC rm) , (₋rmEC-correct rm))

  ₋rmHighestQC : (rm : RoundManager) → QuorumCert
  ₋rmHighestQC rm = ₋btHighestQuorumCert ((₋rmWithEC rm) ^∙ (lBlockTree (α-EC-RM rm)))

  rmHighestQC : Lens RoundManager QuorumCert
  rmHighestQC = mkLens' ₋rmHighestQC
                        (λ (RoundManager∙new ec ecc (RoundManagerWithEC∙new (BlockStore∙new bsInner))) qc
                          → RoundManager∙new ec ecc (RoundManagerWithEC∙new (BlockStore∙new (record bsInner {₋btHighestQuorumCert = qc}))))

  ₋rmHighestCommitQC : (rm : RoundManager) → QuorumCert
  ₋rmHighestCommitQC rm = ₋btHighestCommitCert ((₋rmWithEC rm) ^∙ (lBlockTree (α-EC-RM rm)))

  rmHighestCommitQC : Lens RoundManager QuorumCert
  rmHighestCommitQC = mkLens' ₋rmHighestCommitQC
                        (λ (RoundManager∙new ec ecc (RoundManagerWithEC∙new (BlockStore∙new bsInner))) qc
                          → RoundManager∙new ec ecc (RoundManagerWithEC∙new (BlockStore∙new (record bsInner {₋btHighestCommitCert = qc}))))

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Integer where

open import Agda.Builtin.Int public renaming (Int to Integer)


text:
-- Andreas, 2012-03-30
module Issue593 where

import Common.Level
open import Common.Equality
open import Common.Irrelevance

record Unit : Set where
  constructor unit

bla6 : (F : Unit -> Set) ->
  let X : Unit -> Unit -> Set
      X = _
  in (z : Unit) -> X z z ≡ F z
bla6 F z = refl
-- non-linearity for singleton types should not matter

bla7 : (F : Unit -> Set) ->
  let X : Set
      X = _
  in (z : Unit) -> X ≡ F z
bla7 F z = refl
-- should eta expand z to unit

-- * a more involved singleton type:

record R (A : Set) : Set where
  constructor r
  field
    f1 : A -> Unit
    f2 : A

Sing : Set1
Sing = (A : Set) -> A -> R (A -> Unit)

test : (F : Sing -> Set) ->
  let X : Set
      X = _
  in (z : Sing) -> X ≡ F z
test F z = refl

-- * something with irrelevance

Sing' : Set1
Sing' = (A : Set) -> A -> R (Squash A)

test' : (F : Sing' -> Set) ->
  let X : Sing' -> Sing' -> Set
      X = _
  in (z : Sing') -> X z z ≡ F z
test' F z = refl
-- non-linearity should not matter

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Hilbert-style formalisation of closed syntax.
-- Sequences of terms.

module BasicIS4.Syntax.ClosedHilbertSequential where

open import BasicIS4.Syntax.Common public

-- Derivations.

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

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

-- Concatenation of derivations.

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

-- Modus ponens and necessitation in expanded form.

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

box : ∀ {A} → ⊢ A → ⊢ □ A
box (Ξ , ts) = ∅ , nec ts nil

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

import Data.Product as Product
import Data.Product.Properties as Productₚ
import Data.Nat as Nat
import Data.Vec as Vec
import Data.Vec.Properties as Vecₚ
import Data.Fin as Fin
import Data.Vec.Relation.Unary.All as All

open Nat using (ℕ; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Product using (_,_)

import PiCalculus.Syntax
open PiCalculus.Syntax.Scoped
open import PiCalculus.Semantics
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Weakening (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω
open import PiCalculus.LinearTypeSystem Ω

private
  variable
    n : ℕ
    i j : Fin n
    idx idx' : Idx
    idxs : Idxs n
    P Q : Scoped n

∋-weaken : {γ : PreCtx n} {Γ Θ : Ctx idxs} {t t' : Type} {xs : Usage idx ²} {xs' : Usage idx' ²}
         → (j : Fin (suc n))
         → γ                ； Γ                 ∋[ i               ] t' ； xs' ▹ Θ
         → Vec.insert γ j t ； ctx-insert j xs Γ ∋[ Fin.punchIn j i ] t' ； xs' ▹ ctx-insert j xs Θ
∋-weaken zero x = there x
∋-weaken (suc i) (zero , zero xyz) = zero , zero xyz
∋-weaken (suc i) (suc t , suc x) = there (∋-weaken i (t , x))

⊢-weaken : {P : Scoped n} {γ : PreCtx n} {Γ Θ : Ctx idxs} {t : Type} {xs : Usage idx ²}
         → (j : Fin (suc n))
         → γ ； Γ ⊢ P ▹ Θ
         → Vec.insert γ j t ； ctx-insert j xs Γ ⊢ lift j P ▹ ctx-insert j xs Θ
⊢-weaken j 𝟘 = 𝟘
⊢-weaken j (ν t m μ ⊢P) = ν t m μ (⊢-weaken (suc j) ⊢P)
⊢-weaken j (⊢P ∥ ⊢Q) = ⊢-weaken j ⊢P ∥ ⊢-weaken j ⊢Q
⊢-weaken j (x ⦅⦆ ⊢P) = ∋-weaken j x ⦅⦆ ⊢-weaken (suc j) ⊢P
⊢-weaken j (x ⟨ y ⟩ ⊢P) = ∋-weaken j x ⟨ ∋-weaken j y ⟩ ⊢-weaken j ⊢P

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Equivalence where

-- A 'strict' equality relation for Functors.

open import Level
open import Data.Product using (Σ; curry) renaming (_,_ to _,,_)
open import Relation.Binary.PropositionalEquality as ≡
open import Relation.Binary using (IsEquivalence)
open import Function using (_$_) renaming (_∘_ to _⊚_)

open import Categories.Category using (Category; _[_,_]; _[_≈_])
open import Categories.Category.Product
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Properties using ([_]-resp-square)
open import Categories.NaturalTransformation using (ntHelper)
import Categories.Morphism as Morphism
import Categories.Morphism.HeterogeneousIdentity as HId
import Categories.Morphism.HeterogeneousIdentity.Properties as HIdProps
import Categories.Morphism.IsoEquiv as IsoEquiv
import Categories.Morphism.Reasoning as MorphismReasoning
import Categories.NaturalTransformation.NaturalIsomorphism as NatIso

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ : Level

-- "Strict" equality of Functors.
--
-- It's helpful to think of a functor equality (P : F ≡F G) as a
-- special natural isomorphism where every component (hid $ eq₀ P X)
-- is a 'heterogeneous' identity.

infix  4 _≡F_

record _≡F_ {C : Category o ℓ e}
            {D : Category o′ ℓ′ e′}
            (F G : Functor C D) : Set (ℓ ⊔ o ⊔ o′ ⊔ e′) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
  open F using (F₀; F₁)
  open G using () renaming (F₀ to G₀; F₁ to G₁)
  open HId D

  field
    eq₀ : ∀ X → F₀ X ≡ G₀ X

    eq₁ : ∀ {X Y} (f : C [ X , Y ]) →
          D.CommutativeSquare (F₁ f) (hid $ eq₀ X) (hid $ eq₀ Y) (G₁ f)

  eq₀⁻¹ : ∀ X → G₀ X ≡ F₀ X
  eq₀⁻¹ X = sym $ eq₀ X

  eq₁⁻¹ : ∀ {X Y} (f : C [ X , Y ]) →
          D.CommutativeSquare (G₁ f) (hid $ eq₀⁻¹ X) (hid $ eq₀⁻¹ Y) (F₁ f)
  eq₁⁻¹ {X} {Y} f = begin
      τ⁻¹ Y ∘   G₁ f                      ≈˘⟨ identityʳ ⟩
     (τ⁻¹ Y ∘   G₁ f) ∘  id               ≈˘⟨ ∘-resp-≈ʳ $ hid-symʳ _ ⟩
     (τ⁻¹ Y ∘   G₁ f) ∘ (τ X   ∘ τ⁻¹ X)   ≈⟨ assoc ⟩
      τ⁻¹ Y ∘  (G₁ f  ∘ (τ X   ∘ τ⁻¹ X))  ≈˘⟨ ∘-resp-≈ʳ assoc ⟩
      τ⁻¹ Y ∘ ((G₁ f  ∘  τ X)  ∘ τ⁻¹ X)   ≈˘⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ eq₁ f ⟩
      τ⁻¹ Y ∘ ((τ Y   ∘ F₁ f)  ∘ τ⁻¹ X)   ≈˘⟨ assoc ⟩
     (τ⁻¹ Y ∘  (τ Y   ∘ F₁ f)) ∘ τ⁻¹ X    ≈˘⟨ ∘-resp-≈ˡ assoc ⟩
    ((τ⁻¹ Y ∘   τ Y)  ∘ F₁ f)  ∘ τ⁻¹ X    ≈⟨ ∘-resp-≈ˡ $ ∘-resp-≈ˡ $ hid-symˡ _ ⟩
    (id               ∘ F₁ f)  ∘ τ⁻¹ X    ≈⟨ ∘-resp-≈ˡ identityˡ ⟩
    F₁ f                       ∘ τ⁻¹ X    ∎
    where
      τ   = λ X → hid $ eq₀   X
      τ⁻¹ = λ X → hid $ eq₀⁻¹ X
      open D
      open HomReasoning

  open NatIso using (_≃_)

  -- the family (hid eq₀) is a natural isomorphism

  natIso : F ≃ G
  natIso = record
    { F⇒G = ntHelper record { η = hid ⊚ eq₀   ; commute = eq₁   }
    ; F⇐G = ntHelper record { η = hid ⊚ eq₀⁻¹ ; commute = eq₁⁻¹ }
    ; iso = λ X → hid-iso $ eq₀ X
    }

module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} where

  open Functor
  open Category D
  open HomReasoning hiding (refl; trans)
  open MorphismReasoning D
  open HId D
  open _≡F_

  -- Strict functor equality is an equivalence.

  ≡F-equiv : IsEquivalence (_≡F_ {C = C} {D})
  ≡F-equiv = record
    { refl  = record { eq₀ = λ _ → refl ; eq₁ = λ _ → id-comm-sym }
    ; sym   = λ F≡G → record { eq₀ = eq₀⁻¹ F≡G ; eq₁ = eq₁⁻¹ F≡G }
    ; trans = λ {F G H} F≡G G≡H → record
      { eq₀ = λ X → trans (eq₀ F≡G X) (eq₀ G≡H X)
      ; eq₁ = λ {X} {Y} f → begin
          hid (trans (eq₀ F≡G Y) (eq₀ G≡H Y)) ∘ F₁ F f
        ≈˘⟨ ∘-resp-≈ˡ (hid-trans _ _) ⟩
          (hid (eq₀ G≡H Y) ∘ hid (eq₀ F≡G Y)) ∘ F₁ F f
        ≈⟨ glue (eq₁ G≡H f) (eq₁ F≡G f) ⟩
          F₁ H f ∘ (hid (eq₀ G≡H X) ∘ hid (eq₀ F≡G X))
        ≈⟨ ∘-resp-≈ʳ (hid-trans _ _) ⟩
          F₁ H f ∘ hid (trans (eq₀ F≡G X) (eq₀ G≡H X))
        ∎
      }
    }

  ≡F-identityˡ : {F : Functor C D} → idF ∘F F ≡F F
  ≡F-identityˡ = record { eq₀ = λ _ → refl ; eq₁ = λ _ → id-comm-sym }

  ≡F-identityʳ : {F : Functor C D} → F ∘F idF ≡F F
  ≡F-identityʳ = record { eq₀ = λ _ → refl ; eq₁ = λ _ → id-comm-sym }

module _ {C : Category o ℓ e} where
  open MorphismReasoning C

  ≡F-identity² : idF ∘F idF ≡F idF {C = C}
  ≡F-identity² = record { eq₀ = λ _ → refl ; eq₁ = λ _ → id-comm-sym }

module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
         {E : Category o″ ℓ″ e″}
         where

  open Functor
  open Category E
  open HomReasoning hiding (refl; trans)
  open MorphismReasoning E
  open HId
  open HIdProps
  open _≡F_

  ∘F-resp-≡F : {H I : Functor D E} {F G : Functor C D} →
               H ≡F I → F ≡F G → H ∘F F ≡F I ∘F G
  ∘F-resp-≡F {H} {I} {F} {G} H≡I F≡G = record
    { eq₀ = λ X → trans (HF≡HG X) (HG≡IG X)
    ; eq₁ = λ {X Y} f → begin
        hid E (trans (HF≡HG Y) (HG≡IG Y)) ∘ F₁ H (F₁ F f)
      ≈˘⟨ ∘-resp-≈ˡ (hid-trans E _ _) ⟩
        (hid E (HG≡IG Y) ∘ hid E (HF≡HG Y)) ∘ F₁ H (F₁ F f)
      ≈˘⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ (F-hid H (eq₀ F≡G Y)) ⟩
        (hid E (HG≡IG Y) ∘ F₁ H (hid D (eq₀ F≡G Y))) ∘ F₁ H (F₁ F f)
      ≈⟨ glue (eq₁ H≡I (F₁ G f)) ([ H ]-resp-square (eq₁ F≡G f)) ⟩
        F₁ I (F₁ G f) ∘ (hid E (HG≡IG X) ∘ F₁ H (hid D (eq₀ F≡G X)))
      ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ʳ (F-hid H (eq₀ F≡G X)) ⟩
        F₁ I (F₁ G f) ∘ (hid E (HG≡IG X) ∘ hid E (HF≡HG X))
      ≈⟨ ∘-resp-≈ʳ (hid-trans E _ _) ⟩
        F₁ I (F₁ G f) ∘ hid E (trans (HF≡HG X) (HG≡IG X))
      ∎
    }
    where
      HF≡HG = λ X → cong (F₀ H) (eq₀ F≡G X)
      HG≡IG = λ X → eq₀ H≡I (F₀ G X)

module _ {B : Category o ℓ e} {C : Category o′ ℓ′ e′}
         {D : Category o″ ℓ″ e″} {E : Category o‴ ℓ‴ e‴}
         where

  open Functor
  open Category E
  open MorphismReasoning E
  open _≡F_

  ≡F-assoc : {F : Functor B C} {G : Functor C D} {H : Functor D E} →
             (H ∘F G) ∘F F  ≡F  H ∘F (G ∘F F)
  ≡F-assoc = record { eq₀ = λ _ → refl ; eq₁ = λ _ → id-comm-sym }

  ≡F-sym-assoc : {F : Functor B C} {G : Functor C D} {H : Functor D E} →
                 H ∘F (G ∘F F)  ≡F  (H ∘F G) ∘F F
  ≡F-sym-assoc = record { eq₀ = λ _ → refl ; eq₁ = λ _ → id-comm-sym }

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------------
-- Common properties for the alternating bit protocol
------------------------------------------------------------------------------

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

module FOTC.Program.ABP.PropertiesI where

open import FOTC.Base
open import FOTC.Program.ABP.ABP

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

awaitCong₄ : ∀ {b i is ds₁ ds₂} → ds₁ ≡ ds₂ →
             await b i is ds₁ ≡ await b i is ds₂
awaitCong₄ refl = refl

corruptCong : ∀ {os₁ os₂} → os₁ ≡ os₂ → corrupt os₁ ≡ corrupt os₂
corruptCong refl = refl