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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat hiding (_+_ ; +-comm)
open import Cubical.Data.Vec
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary

open import Cubical.Structures.CommRing

private
  variable
    ℓ : Level
    A : Type ℓ

-- Equivalence between Vec matrix and Fin function matrix

FinMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
FinMatrix A m n = FinVec (FinVec A n) m

VecMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
VecMatrix A m n = Vec (Vec A n) m

FinMatrix→VecMatrix : {m n : ℕ} → FinMatrix A m n → VecMatrix A m n
FinMatrix→VecMatrix M = FinVec→Vec (λ fm → FinVec→Vec (λ fn → M fm fn))

VecMatrix→FinMatrix : {m n : ℕ} → VecMatrix A m n → FinMatrix A m n
VecMatrix→FinMatrix M fn fm = lookup fm (lookup fn M)

FinMatrix→VecMatrix→FinMatrix : {m n : ℕ} (M : FinMatrix A m n)
                              → VecMatrix→FinMatrix (FinMatrix→VecMatrix M) ≡ M
FinMatrix→VecMatrix→FinMatrix {m = zero} M = funExt λ f → ⊥.rec (¬Fin0 f)
FinMatrix→VecMatrix→FinMatrix {n = zero} M = funExt₂ λ _ f → ⊥.rec (¬Fin0 f)
FinMatrix→VecMatrix→FinMatrix {m = suc m} {n = suc n} M = funExt₂ goal
  where
  goal : (fm : Fin (suc m)) (fn : Fin (suc n)) →
         VecMatrix→FinMatrix (_ ∷ FinMatrix→VecMatrix (λ z → M (suc z))) fm fn ≡ M fm fn
  goal zero zero = refl
  goal zero (suc fn) i = FinVec→Vec→FinVec (λ z → M zero (suc z)) i fn
  goal (suc fm) fn i = FinMatrix→VecMatrix→FinMatrix (λ z → M (suc z)) i fm fn

VecMatrix→FinMatrix→VecMatrix : {m n : ℕ} (M : VecMatrix A m n)
                              → FinMatrix→VecMatrix (VecMatrix→FinMatrix M) ≡ M
VecMatrix→FinMatrix→VecMatrix {m = zero} [] = refl
VecMatrix→FinMatrix→VecMatrix {m = suc m} (M ∷ MS) i =
  Vec→FinVec→Vec M i ∷ VecMatrix→FinMatrix→VecMatrix MS i

FinMatrixIsoVecMatrix : (A : Type ℓ) (m n : ℕ) → Iso (FinMatrix A m n) (VecMatrix A m n)
FinMatrixIsoVecMatrix A m n =
  iso FinMatrix→VecMatrix VecMatrix→FinMatrix VecMatrix→FinMatrix→VecMatrix FinMatrix→VecMatrix→FinMatrix

FinMatrix≃VecMatrix : {m n : ℕ} → FinMatrix A m n ≃ VecMatrix A m n
FinMatrix≃VecMatrix {_} {A} {m} {n} = isoToEquiv (FinMatrixIsoVecMatrix A m n)

FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
FinMatrix≡VecMatrix _ _ _ = ua FinMatrix≃VecMatrix

-- We could have constructed the above Path as follows, but that
-- doesn't reduce as nicely as ua isn't on the toplevel:
--
-- FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
-- FinMatrix≡VecMatrix A m n i = FinVec≡Vec (FinVec≡Vec A n i) m i

-- Experiment using addition. Transport commutativity from one
-- representation to the the other and relate the transported
-- operation with a more direct definition.
module _ (R' : CommRing {ℓ}) where

  open CommRing R' renaming ( Carrier to R )

  addFinMatrix : ∀ {m n} → FinMatrix R m n → FinMatrix R m n → FinMatrix R m n
  addFinMatrix M N = λ k l → M k l + N k l

  addFinMatrixComm : ∀ {m n} → (M N : FinMatrix R m n) → addFinMatrix M N ≡ addFinMatrix N M
  addFinMatrixComm M N i k l = +-comm (M k l) (N k l) i

  addVecMatrix : ∀ {m n} → VecMatrix R m n → VecMatrix R m n → VecMatrix R m n
  addVecMatrix {m} {n} = transport (λ i → FinMatrix≡VecMatrix R m n i
                                        → FinMatrix≡VecMatrix R m n i
                                        → FinMatrix≡VecMatrix R m n i)
                                   addFinMatrix

  addMatrixPath : ∀ {m n} → PathP (λ i → FinMatrix≡VecMatrix R m n i
                                       → FinMatrix≡VecMatrix R m n i
                                       → FinMatrix≡VecMatrix R m n i)
                                  addFinMatrix addVecMatrix
  addMatrixPath {m} {n} i = transp (λ j → FinMatrix≡VecMatrix R m n (i ∧ j)
                                        → FinMatrix≡VecMatrix R m n (i ∧ j)
                                        → FinMatrix≡VecMatrix R m n (i ∧ j))
                                   (~ i) addFinMatrix

  addVecMatrixComm : ∀ {m n} → (M N : VecMatrix R m n) → addVecMatrix M N ≡ addVecMatrix N M
  addVecMatrixComm {m} {n} = transport (λ i → (M N : FinMatrix≡VecMatrix R m n i)
                                            → addMatrixPath i M N ≡ addMatrixPath i N M)
                                       addFinMatrixComm

  -- More direct definition of addition for VecMatrix:

  addVec : ∀ {m} → Vec R m → Vec R m → Vec R m
  addVec [] [] = []
  addVec (x ∷ xs) (y ∷ ys) = x + y ∷ addVec xs ys

  addVecLem : ∀ {m} → (M N : Vec R m)
            → FinVec→Vec (λ l → lookup l M + lookup l N) ≡ addVec M N
  addVecLem {zero} [] [] = refl
  addVecLem {suc m} (x ∷ xs) (y ∷ ys) = cong (λ zs → x + y ∷ zs) (addVecLem xs ys)

  addVecMatrix' : ∀ {m n} → VecMatrix R m n → VecMatrix R m n → VecMatrix R m n
  addVecMatrix' [] [] = []
  addVecMatrix' (M ∷ MS) (N ∷ NS) = addVec M N ∷ addVecMatrix' MS NS

  -- The key lemma relating addVecMatrix and addVecMatrix'
  addVecMatrixEq : ∀ {m n} → (M N : VecMatrix R m n) → addVecMatrix M N ≡ addVecMatrix' M N
  addVecMatrixEq {zero} {n} [] [] j = transp (λ i → Vec (Vec R n) 0) j []
  addVecMatrixEq {suc m} {n} (M ∷ MS) (N ∷ NS) =
    addVecMatrix (M ∷ MS) (N ∷ NS)
      ≡⟨ transportUAop₂ FinMatrix≃VecMatrix addFinMatrix (M ∷ MS) (N ∷ NS) ⟩
    FinVec→Vec (λ l → lookup l M + lookup l N) ∷ _
      ≡⟨ (λ i → addVecLem M N i ∷ FinMatrix→VecMatrix (λ k l → lookup l (lookup k MS) + lookup l (lookup k NS))) ⟩
    addVec M N ∷ _
      ≡⟨ cong (λ X → addVec M N ∷ X) (sym (transportUAop₂ FinMatrix≃VecMatrix addFinMatrix MS NS) ∙ addVecMatrixEq MS NS) ⟩
    addVec M N ∷ addVecMatrix' MS NS ∎

  -- By binary funext we get an equality as functions
  addVecMatrixEqFun : ∀ {m} {n} → addVecMatrix {m} {n} ≡ addVecMatrix'
  addVecMatrixEqFun i M N = addVecMatrixEq M N i

  -- We then directly get the properties about addVecMatrix'
  addVecMatrixComm' : ∀ {m n} → (M N : VecMatrix R m n) → addVecMatrix' M N ≡ addVecMatrix' N M
  addVecMatrixComm' M N = sym (addVecMatrixEq M N) ∙∙ addVecMatrixComm M N ∙∙ addVecMatrixEq N M

  -- TODO: prove more properties about addition of matrices for both
  -- FinMatrix and VecMatrix

-- TODO: define multiplication of matrices and do the same kind of
-- reasoning as we did for addition

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module OldBasicILP.UntypedSyntax.Common where

open import Common.UntypedContext public

-- Types parametrised by closed, untyped representations.

module ClosedSyntax
    (Proof : Set)
  where

  infixr 10 _⦂_
  infixl 9 _∧_
  infixr 7 _▻_
  data Ty : Set where
    α_  : Atom → Ty
    _▻_ : Ty → Ty → Ty
    _⦂_ : Proof → Ty → Ty
    _∧_ : Ty → Ty → Ty
    ⊤  : Ty

  -- Additional useful types.

  infixr 7 _▻⋯▻_
  _▻⋯▻_ : Cx Ty → Ty → Ty
  ∅       ▻⋯▻ B = B
  (Ξ , A) ▻⋯▻ B = Ξ ▻⋯▻ (A ▻ B)

ext: agda

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
open import Nat
open import Prelude
open import core
open import disjointness

module elaboration-generality where
  mutual
    elaboration-generality-synth : {Γ : tctx} {e : hexp} {τ : htyp} {d : ihexp} {Δ : hctx} →
                            Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                            Γ ⊢ e => τ
    elaboration-generality-synth ESConst = SConst
    elaboration-generality-synth (ESVar x₁) = SVar x₁
    elaboration-generality-synth (ESLam apt ex) with elaboration-generality-synth ex
    ... | ih = SLam apt ih
    elaboration-generality-synth (ESAp dis _ a x₁ x₂ x₃) = SAp dis a x₁ (elaboration-generality-ana x₃)
    elaboration-generality-synth ESEHole = SEHole
    elaboration-generality-synth (ESNEHole dis ex) = SNEHole (elab-disjoint-new-synth ex dis) (elaboration-generality-synth ex)
    elaboration-generality-synth (ESAsc x) = SAsc (elaboration-generality-ana x)

    elaboration-generality-ana : {Γ : tctx} {e : hexp} {τ τ' : htyp} {d : ihexp} {Δ : hctx} →
                          Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                          Γ ⊢ e <= τ
    elaboration-generality-ana (EALam apt m ex) = ALam apt m (elaboration-generality-ana ex)
    elaboration-generality-ana (EASubsume x x₁ x₂ x₃) = ASubsume (elaboration-generality-synth x₂) x₃
    elaboration-generality-ana EAEHole = ASubsume SEHole TCHole1
    elaboration-generality-ana (EANEHole dis x) = ASubsume (SNEHole (elab-disjoint-new-synth x dis) (elaboration-generality-synth x)) TCHole1

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
open import Functional using (id)
import      Structure.Logic.Constructive.NaturalDeduction

module Structure.Logic.Constructive.Functions.Properties {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ constructiveLogicSign : _ ⦄ where
open Structure.Logic.Constructive.NaturalDeduction.ConstructiveLogicSignature {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (constructiveLogicSign)

open import Structure.Logic.Constructive.Functions(Domain)
open import Syntax.Function

-- States whether the function f is defined on the element x.
-- Whether f(x) yields/returns an element in the domain.
-- In other words: Whether the logic can interpret f(x) as anything meaningful.
Defined : Function → Domain → Formula
Defined f(x) = ∃ₗ(y ↦ f(x) ≡ y)

-- States whether the function f can yield/return the element y.
Value : Function → Domain → Formula
Value f(y) = ∃ₗ(x ↦ f(x) ≡ y)

Injective : Function → Formula
Injective(f) = ∀ₗ(x ↦ ∀ₗ(y ↦ (f(x) ≡ f(y)) ⟶ (x ≡ y)))

Surjective : Function → Formula
Surjective(f) = ∀ₗ(y ↦ ∃ₗ(x ↦ f(x) ≡ y))

Bijective : Function → Formula
Bijective(f) =
  Injective(f)
  ∧ Surjective(f)

Preserving₁ : Function → Function → Function → Formula
Preserving₁(f)(g₁)(g₂) = ∀ₗ(x ↦ f(g₁(x)) ≡ g₂(f(x)))

Preserving₂ : Function → BinaryOperator → BinaryOperator → Formula
Preserving₂(f)(_▫₁_)(_▫₂_) = ∀ₗ(x ↦ ∀ₗ(y ↦ f(x ▫₁ y) ≡ (f(x) ▫₂ f(y))))

Fixpoint : Function → Domain → Formula
Fixpoint f(x) = (f(x) ≡ x)

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite maps with indexed keys and values, based on AVL trees
------------------------------------------------------------------------

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

open import Data.Product as Prod
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)
import Data.AVL.Value

module Data.AVL.IndexedMap
  {i k v ℓ}
  {Index : Set i} {Key : Index → Set k}  (Value : Index → Set v)
  {_<_ : Rel (∃ Key) ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

import Data.AVL
open import Data.Bool
open import Data.List.Base as List using (List)
open import Data.Maybe.Base as Maybe
open import Function
open import Level

-- Key/value pairs.

KV : Set (i ⊔ k ⊔ v)
KV = ∃ λ i → Key i × Value i

-- Conversions.

private

  fromKV : KV → Σ[ ik ∈ ∃ Key ] Value (proj₁ ik)
  fromKV (i , k , v) = ((i , k) , v)

  toKV : Σ[ ik ∈ ∃ Key ] Value (proj₁ ik) → KV
  toKV ((i , k) , v) = (i , k , v)

-- The map type.

private
  open module AVL =
    Data.AVL (record { isStrictTotalOrder = isStrictTotalOrder })
    using () renaming (Tree to Map')
  Map = Map' (AVL.MkValue (Value ∘ proj₁) (subst Value ∘′ cong proj₁))

-- Repackaged functions.

empty : Map
empty = AVL.empty

singleton : ∀ {i} → Key i → Value i → Map
singleton k v = AVL.singleton (-, k) v

insert : ∀ {i} → Key i → Value i → Map → Map
insert k v = AVL.insert (-, k) v

delete : ∀ {i} → Key i → Map → Map
delete k = AVL.delete (-, k)

lookup : ∀ {i} → Key i → Map → Maybe (Value i)
lookup k m = AVL.lookup (-, k) m

infix 4 _∈?_

_∈?_ : ∀ {i} → Key i → Map → Bool
_∈?_ k = AVL._∈?_ (-, k)

headTail : Map → Maybe (KV × Map)
headTail m = Maybe.map (Prod.map toKV id) (AVL.headTail m)

initLast : Map → Maybe (Map × KV)
initLast m = Maybe.map (Prod.map id toKV) (AVL.initLast m)

fromList : List KV → Map
fromList = AVL.fromList ∘ List.map fromKV

toList : Map → List KV
toList = List.map toKV ∘ AVL.toList


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Showing booleans
------------------------------------------------------------------------

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

module Data.Bool.Show where

open import Data.Bool.Base using (Bool; false; true)
open import Data.String.Base using (String)

show : Bool → String
show true  = "true"
show false = "false"


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

open import Algebra

module Algebra.SemiringLiterals {r} (rng : Semiring r) where

open Semiring rng

open import Literals.Number
open import Data.Nat.Literals
open import Data.Unit
import Data.Unit.UniversePolymorphic as Poly
open import Data.Nat.DivMod
open import Data.Nat using (ℕ; suc; zero)
open import Data.Nat.Properties
open import Data.Bool
open import Strict

2# : 𝑅
2# = 1# + 1#

sringFromNatRec : ℕ → ℕ → 𝑅
sringFromNatRec zero    _       = 0#
sringFromNatRec (suc 0) _       = 1#
sringFromNatRec (suc 1) _       = 2#
sringFromNatRec (suc 2) _       = 1# + 2#
sringFromNatRec (suc n) (suc w) =
  let! r =! sringFromNatRec (n ÷ 2) w in!
  if even n
    then 1# + (r * 2#)
    else (1# + r) * 2#
sringFromNatRec _ zero = 0# -- will not happen

sringFromNat : ℕ → 𝑅
sringFromNat n = sringFromNatRec n n

instance
  numberRng : Number 𝑅
  Number.Constraint numberRng _ = Poly.⊤
  Number.fromNat numberRng n = sringFromNat n

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --without-K --safe #-}
module Util.Relation.Binary.PropositionalEquality where

open import Relation.Binary.PropositionalEquality public

open import Data.Product using (uncurry)

open import Util.Prelude

private
  variable
    α β γ γ′ δ : Level
    A B C A′ B′ C′ : Set α

trans-unassoc : {a b c d : A} (p : a ≡ b) {q : b ≡ c} {r : c ≡ d}
  → trans p (trans q r) ≡ trans (trans p q) r
trans-unassoc p = sym (trans-assoc p)

Σ-≡⁻ : {A : Set α} {B : A → Set β} {x y : Σ A B}
  → x ≡ y
  → Σ[ p ∈ (proj₁ x ≡ proj₁ y) ] subst B p (proj₂ x) ≡ proj₂ y
Σ-≡⁻ refl = refl , refl

Σ-≡⁺ : {A : Set α} {B : A → Set β} {x y : Σ A B}
  → Σ[ p ∈ (proj₁ x ≡ proj₁ y) ] subst B p (proj₂ x) ≡ proj₂ y
  → x ≡ y
Σ-≡⁺ (refl , refl) = refl

Σ-≡⁺∘Σ-≡⁻ : {A : Set α} {B : A → Set β} {x y : Σ A B}
  → (p : x ≡ y)
  → Σ-≡⁺ (Σ-≡⁻ p) ≡ p
Σ-≡⁺∘Σ-≡⁻ refl = refl

Σ-≡⁻∘Σ-≡⁺ : {A : Set α} {B : A → Set β} {x y : Σ A B}
  → (p : Σ[ p ∈ (proj₁ x ≡ proj₁ y) ] subst B p (proj₂ x) ≡ proj₂ y)
  → Σ-≡⁻ (Σ-≡⁺ p) ≡ p
Σ-≡⁻∘Σ-≡⁺ (refl , refl) = refl

×-≡⁺ : {x y : A × B}
  → (proj₁ x ≡ proj₁ y) × (proj₂ x ≡ proj₂ y)
  → x ≡ y
×-≡⁺ (refl , refl) = refl

×-≡⁻ : {x y : A × B}
  → x ≡ y
  → (proj₁ x ≡ proj₁ y) × (proj₂ x ≡ proj₂ y)
×-≡⁻ refl = refl , refl

×-≡⁺∘×-≡⁻ : {x y : A × B} (p : x ≡ y)
  → ×-≡⁺ (×-≡⁻ p) ≡ p
×-≡⁺∘×-≡⁻ refl = refl

×-≡⁻∘×-≡⁺ : {x y : A × B} (p : (proj₁ x ≡ proj₁ y) × (proj₂ x ≡ proj₂ y))
  → ×-≡⁻ (×-≡⁺ p) ≡ p
×-≡⁻∘×-≡⁺ (refl , refl) = refl

cast : A ≡ B → A → B
cast = subst (λ x → x)

cast-refl : {x : A} → cast refl x ≡ x
cast-refl = refl

cast-trans : (B≡C : B ≡ C) (A≡B : A ≡ B) {x : A}
  → cast B≡C (cast A≡B x) ≡ cast (trans A≡B B≡C) x
cast-trans refl refl = refl

subst-trans : ∀ {P : A → Set β} {x y z : A} {p : P x}
  → (x≡y : x ≡ y) (y≡z : y ≡ z)
  → subst P y≡z (subst P x≡y p) ≡ subst P (trans x≡y y≡z) p
subst-trans refl refl = refl

subst₂-trans : (C : A → B → Set γ)
  → {a₀ a₁ a₂ : A} (p : a₀ ≡ a₁) (p′ : a₁ ≡ a₂)
  → {b₀ b₁ b₂ : B} (q : b₀ ≡ b₁) (q′ : b₁ ≡ b₂)
  → {x : C a₀ b₀}
  → subst₂ C p′ q′ (subst₂ C p q x) ≡ subst₂ C (trans p p′) (trans q q′) x
subst₂-trans C refl refl refl refl = refl

subst₂-subst₂-sym : (C : A → B → Set γ)
  → {a a′ : A} (p : a ≡ a′)
  → {b b′ : B} (q : b ≡ b′)
  → {x : C a′ b′}
  → subst₂ C p q (subst₂ C (sym p) (sym q) x) ≡ x
subst₂-subst₂-sym C refl refl = refl

subst₂-sym-subst₂ : (C : A → B → Set γ)
  → {a a′ : A} (p : a ≡ a′)
  → {b b′ : B} (q : b ≡ b′)
  → {x : C a b}
  → subst₂ C (sym p) (sym q) (subst₂ C p q x) ≡ x
subst₂-sym-subst₂ C refl refl = refl

subst₂-cong : (C : A′ → B′ → Set γ)
  → (f : A → A′) (g : B → B′)
  → {a a′ : A} (p : a ≡ a′)
  → {b b′ : B} (q : b ≡ b′)
  → {x : C (f a) (g b)}
  → subst₂ C (cong f p) (cong g q) x ≡ subst₂ (λ a b → C (f a) (g b)) p q x
subst₂-cong C f g refl refl = refl

subst₂≡subst : ∀ {la} {A : Set la} {lb} {B : Set lb} {lc} (C : A → B → Set lc)
  → ∀ {a a′} (p : a ≡ a′) {b b′} (q : b ≡ b′) {x : C a b}
  → subst₂ C p q x ≡ subst (uncurry C) (cong₂ _,_ p q) x
subst₂≡subst C refl refl = refl

subst₂-application : (C : A → B → Set γ) {C′ : A′ → B′ → Set γ′}
  → {fa : A′ → A} {fb : B′ → B}
  → {a a′ : A′} {b b′ : B′} {c : C (fa a) (fb b)}
  → (g : ∀ a b → C (fa a) (fb b) → C′ a b)
  → (eqa : a ≡ a′)
  → (eqb : b ≡ b′)
  → subst₂ C′ eqa eqb (g a b c)
  ≡ g a′ b′ (subst₂ C (cong fa eqa) (cong fb eqb) c)
subst₂-application _ _ refl refl = refl

subst₂-application′ : {C : A → B → Set γ} (C′ : A′ → B′ → Set γ′)
  → {fa : A → A′} {fb : B → B′}
  → {a a′ : A} {b b′ : B} {c : C a b}
  → (g : ∀ a b → C a b → C′ (fa a) (fb b))
  → (eqa : a ≡ a′)
  → (eqb : b ≡ b′)
  → subst₂ C′ (cong fa eqa) (cong fb eqb) (g a b c)
  ≡ g a′ b′ (subst₂ C eqa eqb c)
subst₂-application′ _ _ refl refl = refl

cong₂-dep : {A : Set α} {B : A → Set β} {C : Set γ}
  → (f : (a : A) → B a → C)
  → {x y : A} (p : x ≡ y)
  → {u : B x} {v : B y} (q : subst B p u ≡ v)
  → f x u ≡ f y v
cong₂-dep f refl refl = refl

cong₃-dep : {A : Set α} {B : A → Set β} {C : (a : A) → B a → Set γ}
  → {D : Set δ}
  → (f : (a : A) (b : B a) → C a b → D)
  → {x y : A} (p : x ≡ y)
  → {u : B x} {v : B y} (q : subst B p u ≡ v)
  → {w : C x u} {z : C y v} (r : subst (λ i → C (proj₁ i) (proj₂ i)) (Σ-≡⁺ (p , q)) w ≡ z)
  → f x u w ≡ f y v z
cong₃-dep f refl refl refl = refl

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

module MidiEvent where

open import Data.Fin     using (Fin; #_)
open import Data.List    using (List; _∷_; []; concat; map)
open import Data.Nat     using (ℕ; _+_; _⊔_)
open import Data.Product using (_×_; _,_; proj₁)
open import Data.String  using (String)
open import Data.Vec     using (toList)
open import Function     using (_∘_)

open import Music        using (Melody; melody; Counterpoint; cp; Harmony; melody→notes; harmony→counterpoint)
open import Note         using (Note; tone; rest; duration)
open import Pitch        using (Pitch)

-- General MIDI instrument numbers range from 1 to 128,
-- so this is the actual instrument number minus 1.
InstrumentNumber-1 : Set
InstrumentNumber-1 = Fin 128

Tick : Set
Tick = ℕ

Velocity : Set
Velocity  = Fin 128

defaultVelocity : Velocity
defaultVelocity = # 60

-- percussion is channel 10, so 9 as Channel-1
Channel-1 : Set
Channel-1 = Fin 16

-- in bpm
Tempo : Set
Tempo = ℕ

record MidiEvent : Set where
  constructor midiEvent
  field
    pitch            : Pitch -- Pitch was defined to correspond to MIDI pitch
    start            : Tick
    stop             : Tick
    velocity         : Velocity

record MidiTrack : Set where
  constructor track
  field
    trackName        : String
    instrumentNumber : InstrumentNumber-1
    channel          : Channel-1
    tempo            : Tempo -- initial tempo
    events           : List MidiEvent

notes→events : Velocity → List Note → List MidiEvent
notes→events v ns = me 0 ns where
  me : Tick → List Note → List MidiEvent
  me t [] = []
  me t (tone (duration d) p ∷ ns) = midiEvent p t (t + d) v ∷ me (t + d) ns
  me t (rest (duration d)   ∷ ns) = me (t + d) ns

melody→events : {n : ℕ} → Velocity → Melody n → List MidiEvent
melody→events v = notes→events v ∘ melody→notes

counterpoint→events : {v d : ℕ} → Velocity → Counterpoint v d → List MidiEvent
counterpoint→events v (cp ms) = concat (map (melody→events v) (toList ms))

harmony→events : {v d : ℕ} → Velocity → Harmony v d → List MidiEvent
harmony→events v = counterpoint→events v ∘ harmony→counterpoint

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


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

module TypeTheory.HoTT.Data.Empty.Properties where

-- agda-stdlib
open import Data.Empty

-- agda-misc
open import TypeTheory.HoTT.Base

isProp-⊥ : isProp ⊥
isProp-⊥ x = ⊥-elim x


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

module Math.Combinatorics.Function.Properties.Lemma where

open import Data.Unit using (tt)
open import Data.Product
open import Data.Sum
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Data.Nat.Solver using (module +-*-Solver)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Function
open import Algebra.FunctionProperties

open ≤-Reasoning

1≤n⇒n≢0 : ∀ {n} → 1 ≤ n → n ≢ 0
1≤n⇒n≢0 .{suc _} (s≤s z≤n) ()

-- TODO: use m<n⇒0<n∸m
m<n⇒n∸m≢0 : ∀ {m n} → m < n → n ∸ m ≢ 0
m<n⇒n∸m≢0 {m} {n} m<n n∸m≡0 = (λ x → x (sym n∸m≡0)) $ <⇒≢ $ +-cancelʳ-< 0 (n ∸ m) $ begin-strict
  m           <⟨ m<n ⟩
  n           ≡⟨ sym $ m∸n+n≡m (<⇒≤ m<n) ⟩
  (n ∸ m) + m ∎

≤⇒≡∨< : ∀ {m n} → m ≤ n → (m ≡ n) ⊎ (m < n)
≤⇒≡∨< {m} {n} m≤n with m ≟ n
... | yes m≡n = inj₁ m≡n
... | no  m≢n = inj₂ (≤∧≢⇒< m≤n m≢n)

^-monoˡ-≤ : ∀ n → (_^ n) Preserves _≤_ ⟶ _≤_
^-monoˡ-≤ 0       {m} {o} m≤o = ≤-refl
^-monoˡ-≤ (suc n) {m} {o} m≤o = begin
  m ^ suc n ≡⟨⟩
  m * m ^ n ≤⟨ *-mono-≤ m≤o (^-monoˡ-≤ n m≤o) ⟩
  o * o ^ n ≡⟨⟩
  o ^ suc n ∎

1≤[1+m]^n : ∀ m n → 1 ≤ (1 + m) ^ n
1≤[1+m]^n m zero = ≤-refl
1≤[1+m]^n m (suc n) = begin
  1 * 1             ≤⟨ *-mono-≤ (s≤s {0} {m} z≤n) (1≤[1+m]^n m n) ⟩
  suc m * suc m ^ n ∎

^-monoʳ-≤ : ∀ n → (suc n ^_) Preserves _≤_ ⟶ _≤_
^-monoʳ-≤ n {.0}       {o}        z≤n       = begin
  1         ≤⟨ 1≤[1+m]^n n o ⟩
  suc n ^ o ∎
^-monoʳ-≤ n {.(suc _)} {.(suc _)} (s≤s {m} {o} m≤o) = begin
  suc n ^ suc m     ≡⟨⟩
  suc n * suc n ^ m ≤⟨ *-monoʳ-≤ (suc n) (^-monoʳ-≤ n m≤o) ⟩
  suc n * suc n ^ o ≡⟨⟩
  suc n ^ suc o     ∎

^-mono-≤ : ∀ {m n o p} → m ≤ n → o ≤ p → suc m ^ o ≤ suc n ^ p
^-mono-≤ {m} {n} {o} {p} m≤n o≤p = begin
  suc m ^ o ≤⟨ ^-monoˡ-≤ o (s≤s m≤n) ⟩
  suc n ^ o ≤⟨ ^-monoʳ-≤ n o≤p ⟩
  suc n ^ p ∎

*-cancelʳ-≤′ : ∀ m n {o} → False (o ≟ 0) → m * o ≤ n * o → m ≤ n
*-cancelʳ-≤′ m n {suc o} tt = *-cancelʳ-≤ m n o

-- TODO upadte stdlib
*-cancelʳ-≡′ : ∀ m n {o} → False (o ≟ 0) → m * o ≡ n * o → m ≡ n
*-cancelʳ-≡′ m n {suc o} tt = *-cancelʳ-≡ m n

*-monoʳ-<′ : ∀ n → False (n ≟ 0) → (n *_) Preserves _<_ ⟶ _<_
*-monoʳ-<′ (suc n) tt gt = *-monoʳ-< n gt

*-monoˡ-<′ : ∀ n → False (n ≟ 0) → (_* n) Preserves _<_ ⟶ _<_
*-monoˡ-<′ (suc n) tt gt = *-monoˡ-< n gt

m≡n+o⇒m∸o≡n : ∀ m n o → m ≡ n + o → m ∸ o ≡ n
m≡n+o⇒m∸o≡n m n o m≡n+o = trans (cong (_∸ o) m≡n+o) (m+n∸n≡m n o)

lemma₃ : ∀ m n → (∃ λ o → (n ≡ o + m)) ⊎ (n < m)
lemma₃ m n with compare m n
lemma₃ m              .(suc (m + k)) | less    .m k = inj₁ (suc k , cong suc (+-comm m k))
lemma₃ m              .m             | equal   .m   = inj₁ (0 , +-identityˡ m)
lemma₃ .(suc (n + k)) n              | greater .n k = inj₂ (s≤s (≤-stepsʳ k ≤-refl))

m≡n*o⇒n≡m/o : ∀ m n o → (wit : False (o ≟ 0)) → m ≡ n * o → n ≡ _/_ m o {wit}
m≡n*o⇒n≡m/o m n o@(suc o-1) tt m≡n*o = sym $ begin-equality
  m / o       ≡⟨ cong (_/ o) $ m≡n*o ⟩
  (n * o) / o ≡⟨ m*n/n≡m n o ⟩
  n            ∎

m*n≡o⇒m≡o/n : ∀ m n o → (wit : False (n ≟ 0)) → m * n ≡ o → m ≡ _/_ o n {wit}
m*n≡o⇒m≡o/n m n o wit m*n≡o = m≡n*o⇒n≡m/o o m n wit (sym m*n≡o)

*-pres-≢0 : ∀ {a b} → a ≢ 0 → b ≢ 0 → a * b ≢ 0
*-pres-≢0 {0}     {b} a≢0 b≢0 a*b≡0 = a≢0 refl
*-pres-≢0 {suc a} {0} a≢0 b≢0 a*b≡0 = b≢0 refl

-- TODO numbering
lemma₅ : ∀ m n o p → (m + n) * (o * p) ≡ (o * (m * p)) + n * (o * p)
lemma₅ = solve 4 (λ m n o p →
  (m :+ n) :* (o :* p) := (o :* (m :* p)) :+ (n :* (o :* p))) refl
  where open +-*-Solver

lemma₇ : ∀ m n o → m * n * o ≡ m * o * n
lemma₇ = solve 3 (λ m n o → m :* n :* o := m :* o :* n) refl
  where open +-*-Solver

lemma₈ : ∀ m n o → m * (n * o) ≡ n * m * o
lemma₈ = solve 3 (λ m n o → m :* (n :* o) := n :* m :* o) refl
  where open +-*-Solver

lemma₉ : ∀ m n o p → m * n * (o * p) ≡ (m * o) * (n * p)
lemma₉ = solve 4 (λ m n o p → m :* n :* (o :* p) := (m :* o) :* (n :* p)) refl
  where open +-*-Solver

lemma₁₀ : ∀ m n o p → m * n * o * p ≡ (m * o) * (n * p)
lemma₁₀ = solve 4 (λ m n o p → m :* n :* o :* p := (m :* o) :* (n :* p)) refl
  where open +-*-Solver

lemma₁₁ : ∀ m n o p → (m * n) * (o * p) ≡ m * o * p * n
lemma₁₁ = solve 4 (λ m n o p → (m :* n) :* (o :* p) := m :* o :* p :* n) refl
  where open +-*-Solver

lemma₁₂ : ∀ m n o → m * n * o ≡ n * (m * o)
lemma₁₂ = solve 3 (λ m n o → m :* n :* o := n :* (m :* o)) refl
  where open +-*-Solver

lemma₁₃ : ∀ m n o → m * n * n * o ≡ o * m * n * n
lemma₁₃ = solve 3 (λ m n o → m :* n :* n :* o := o :* m :* n :* n) refl
  where open +-*-Solver

lemma₁₄ : ∀ m n o → m * n * (n * o * o) ≡ m * (n * o) * (n * o)
lemma₁₄ = solve 3 (λ m n o → m :* n :* (n :* o :* o) := m :* (n :* o) :* (n :* o)) refl
  where open +-*-Solver

lemma₁₅ : ∀ n → (2 + 2 * n) * (1 + 2 * n) ≡ 2 * (1 + 2 * n) * (1 + n)
lemma₁₅ = solve 1 (λ n →
  (con 2 :+ con 2 :* n) :* (con 1 :+ con 2 :* n) :=
  con 2 :* (con 1 :+ con 2 :* n) :* (con 1 :+ n)
  ) refl
  where open +-*-Solver

lemma₁₆ : ∀ m n o p → m * n * (o * p * p) ≡ m * o * (n * p * p)
lemma₁₆ = solve 4 (λ m n o p →
  m :* n :* (o :* p :* p) := m :* o :* (n :* p :* p)
  ) refl
  where open +-*-Solver

lemma₁₇ : ∀ m n o p → m * n * (o * p) ≡ o * m * (n * p)
lemma₁₇ = solve 4 (λ m n o p → m :* n :* (o :* p) := o :* m :* (n :* p)) refl
  where open +-*-Solver


text:
module Semantics where

open import Syntax public

-- Kripke models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    World     : Set
    _≤_       : World → World → Set
    refl≤     : ∀ {w} → w ≤ w
    trans≤    : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″
    idtrans≤  : ∀ {w w′} → (p : w ≤ w′) → trans≤ refl≤ p ≡ p
    _⊩ᵅ_     : World → Atom → Set
    mono⊩ᵅ   : ∀ {P w w′} → w ≤ w′ → w ⊩ᵅ P → w′ ⊩ᵅ P
    idmono⊩ᵅ : ∀ {P w} → (s : w ⊩ᵅ P) → mono⊩ᵅ {P} refl≤ s ≡ s

open Model {{…}} public

-- Forcing in a particular world.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World → Type → Set
  w ⊩ α P    = w ⊩ᵅ P
  w ⊩ A ⇒ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
  w ⊩ A ⩕ B  = w ⊩ A ∧ w ⊩ B
  w ⊩ ⫪     = ⊤

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Stack Type → Set
  w ⊩⋆ ∅     = ⊤
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ ∧ w ⊩ A

-- Function extensionality.

postulate
  funext  : ∀ {X : Set} {Y : X → Set} {f g : ∀ x → Y x} →
            (∀ x → f x ≡ g x) →
            (λ x → f x) ≡ (λ x → g x)

  ⟨funext⟩ : ∀ {X : Set} {Y : X → Set} {f g : ∀ {x} → Y x} →
             (∀ {x} → f {x} ≡ g {x}) →
             (λ {x} → f {x}) ≡ (λ {x} → g {x})

extfun : ∀ {X : Set} {Y : X → Set} {f g : ∀ x → Y x} →
         (λ x → f x) ≡ (λ x → g x) →
         (∀ x → f x ≡ g x)
extfun refl = λ x → refl

⟨extfun⟩ : ∀ {X : Set} {Y : X → Set} {f g : ∀ {x} → Y x} →
           (λ {x} → f {x}) ≡ (λ {x} → g {x}) →
           (∀ {x} → f {x} ≡ g {x})
⟨extfun⟩ refl = refl

-- Monotonicity of forcing with respect to constructive accessibility.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
  mono⊩ {α P}    p s = mono⊩ᵅ p s
  mono⊩ {A ⇒ B} p s = λ p′ → s (trans≤ p p′)
  mono⊩ {A ⩕ B}  p s = mono⊩ {A} p (π₁ s) , mono⊩ {B} p (π₂ s)
  mono⊩ {⫪}     p s = ∙

  mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     p ∙       = ∙
  mono⊩⋆ {Ξ , A} p (σ , s) = mono⊩⋆ {Ξ} p σ , mono⊩ {A} p s

-- TODO: Naming things.

module _ {{_ : Model}} where
  idmono⊩ : ∀ {A w} → (s : w ⊩ A) → mono⊩ {A} refl≤ s ≡ s
  idmono⊩ {α P}    s = idmono⊩ᵅ s
  idmono⊩ {A ⇒ B} s = ⟨funext⟩ λ {w′} → funext λ p → cong s (idtrans≤ p)
  idmono⊩ {A ⩕ B}  s = cong² _,_ (idmono⊩ {A} (π₁ s)) (idmono⊩ {B} (π₂ s))
  idmono⊩ {⫪}     s = refl

  idmono⊩⋆ : ∀ {Ξ w} → (γ : w ⊩⋆ Ξ) → mono⊩⋆ refl≤ γ ≡ γ
  idmono⊩⋆ {∅}     ∙       = refl
  idmono⊩⋆ {Ξ , A} (σ , s) = cong² _,_ (idmono⊩⋆ σ) (idmono⊩ {A} s)

-- TODO: Naming things.

module _ {{_ : Model}} where
  _⟪_⊫_⟫ : World → Context → Type → Set
  w ⟪ Γ ⊫ A ⟫ = w ⊩⋆ Γ → w ⊩ A

-- Evaluation equipment.

module _ {{_ : Model}} where
  ⟪var⟫ : ∀ {A Γ w} → A ∈ Γ → w ⟪ Γ ⊫ A ⟫
  ⟪var⟫ top     = λ { (γ , s) → s }
  ⟪var⟫ (pop i) = λ { (γ , s) → ⟪var⟫ i γ }

  ⟪lam⟫ : ∀ {A B Γ w} → (∀ {w′} → w′ ⟪ Γ , A ⊫ B ⟫) → w ⟪ Γ ⊫ A ⇒ B ⟫
  ⟪lam⟫ ⟪d⟫ = λ γ p s → ⟪d⟫ (mono⊩⋆ p γ , s)

  ⟪app⟫ : ∀ {A B Γ w} → w ⟪ Γ ⊫ A ⇒ B ⟫ → w ⟪ Γ ⊫ A ⟫ → w ⟪ Γ ⊫ B ⟫
  ⟪app⟫ ⟪d⟫ ⟪e⟫ = λ γ → ⟪d⟫ γ refl≤ (⟪e⟫ γ)

  ⟪pair⟫ : ∀ {A B Γ w} → w ⟪ Γ ⊫ A ⟫ → w ⟪ Γ ⊫ B ⟫ → w ⟪ Γ ⊫ A ⩕ B ⟫
  ⟪pair⟫ ⟪d⟫ ⟪e⟫ = λ γ → ⟪d⟫ γ , ⟪e⟫ γ

  ⟪fst⟫ : ∀ {A B Γ w} → w ⟪ Γ ⊫ A ⩕ B ⟫ → w ⟪ Γ ⊫ A ⟫
  ⟪fst⟫ ⟪d⟫ = λ γ → π₁ (⟪d⟫ γ)

  ⟪snd⟫ : ∀ {A B Γ w} → w ⟪ Γ ⊫ A ⩕ B ⟫ → w ⟪ Γ ⊫ B ⟫
  ⟪snd⟫ ⟪d⟫ = λ γ → π₂ (⟪d⟫ γ)

  ⟪unit⟫ : ∀ {Γ w} → w ⟪ Γ ⊫ ⫪ ⟫
  ⟪unit⟫ = λ γ → ∙

-- Shorthand for variables.

module _ {{_ : Model}} where
  ⟪v₀⟫ : ∀ {A Γ w} → w ⟪ Γ , A ⊫ A ⟫
  ⟪v₀⟫ {A} = ⟪var⟫ {A} i₀

-- Forcing in all worlds, or semantic entailment.

module _ {{_ : Model}} where
  infix 3 _⊨_
  _⊨_ : Context → Type → Set
  Γ ⊨ A = ∀ {w} → w ⟪ Γ ⊫ A ⟫

-- Evaluation, or soundness of the semantics with respect to the syntax.

module _ {{_ : Model}} where
  eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
  eval (var i)            = ⟪var⟫ i
  eval (lam {A} {B} d)    = ⟪lam⟫ {A} {B} (eval d)
  eval (app {A} {B} d e)  = ⟪app⟫ {A} {B} (eval d) (eval e)
  eval (pair {A} {B} d e) = ⟪pair⟫ {A} {B} (eval d) (eval e)
  eval (fst {A} {B} d)    = ⟪fst⟫ {A} {B} (eval d)
  eval (snd {A} {B} d)    = ⟪snd⟫ {A} {B} (eval d)
  eval unit               = ⟪unit⟫

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { World     = Context
      ; _≤_       = _⊆_
      ; refl≤     = refl⊆
      ; trans≤    = trans⊆
      ; idtrans≤  = idtrans⊆
      ; _⊩ᵅ_     = λ Γ P → Γ ⊢ⁿᵉ α P
      ; mono⊩ᵅ   = mono⊢ⁿᵉ
      ; idmono⊩ᵅ = idmono⊢ⁿᵉ
      }

-- Soundness and completeness of the canonical model with respect to the syntax.

mutual
  evalᶜ : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊩ A
  evalᶜ {α P}    d = d
  evalᶜ {A ⇒ B} d = λ p e → evalᶜ (appⁿᵉ (mono⊢ⁿᵉ p d) (quotᶜ e))
  evalᶜ {A ⩕ B}  d = evalᶜ (fstⁿᵉ d) , evalᶜ (sndⁿᵉ d)
  evalᶜ {⫪}     d = ∙

  quotᶜ : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ⁿᶠ A
  quotᶜ {α P}    s = neⁿᶠ s
  quotᶜ {A ⇒ B} s = lamⁿᶠ (quotᶜ (s weak⊆ (evalᶜ {A} v₀ⁿᵉ)))
  quotᶜ {A ⩕ B}  s = pairⁿᶠ (quotᶜ (π₁ s)) (quotᶜ (π₂ s))
  quotᶜ {⫪}     s = unitⁿᶠ

-- Reflexivity of simultaneous forcing.

refl⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
refl⊩⋆ {∅}     = ∙
refl⊩⋆ {Γ , A} = mono⊩⋆ weak⊆ refl⊩⋆ , evalᶜ {A} v₀ⁿᵉ

-- Quotation, or completeness of the semantics with respect to the syntax.

quot : ∀ {A Γ} → Γ ⊨ A → Γ ⊢ⁿᶠ A
quot s = quotᶜ (s refl⊩⋆)

-- Normalisation by evaluation.

nbe : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ⁿᶠ A
nbe = quot ∘ eval

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness


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 #-}

-- This module proves the two "VotesOnce" proof obligations for our fake handler

open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS

import      LibraBFT.Concrete.Properties.VotesOnce as VO
open import LibraBFT.Impl.Base.Types

open import LibraBFT.Impl.Consensus.Types hiding (EpochConfigFor)
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Consensus.ChainedBFT.EventProcessor.Properties  sha256 sha256-cr
open import LibraBFT.Impl.Handle                                          sha256 sha256-cr
open import LibraBFT.Impl.Handle.Properties                               sha256 sha256-cr
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Properties.Aux
open import LibraBFT.Impl.Util.Util
open import LibraBFT.Concrete.System impl-sps-avp
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK
open        Structural impl-sps-avp

-- In this module, we prove the two implementation obligations for the VotesOnce rule.  Note
-- that it is not yet 100% clear that the obligations are the best definitions to use.  See comments
-- in Concrete.VotesOnce.  We will want to prove these obligations for the fake/simple
-- implementation (or some variant on it) and streamline the proof before we proceed to tackle more
-- ambitious properties.

module LibraBFT.Impl.Properties.VotesOnce where

  -- TODO-1: It seems that vo₂ should be proved via a couple of invocations of this property;
  -- the proofs are quite similar.
  newVoteSameEpochGreaterRound : ∀ {e}{pre : SystemState e}{pid initd' s' outs v m pk}
                               → ReachableSystemState pre
                               → StepPeerState {e} pid (availEpochs pre) (msgPool pre) (initialised pre) (peerStates pre pid) initd' (s' , outs)
                               → v  ⊂Msg m → m ∈ outs → (sig : WithVerSig pk v)
                               → ¬ MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
                               → (v ^∙ vEpoch) ≡ (₋epEC (peerStates pre pid)) ^∙ epEpoch
                               × suc ((₋epEC (peerStates pre pid)) ^∙ epLastVotedRound) ≡ (v ^∙ vRound)  -- New vote for higher round than last voted
                               × (v ^∙ vRound) ≡ ((₋epEC s') ^∙ epLastVotedRound)     -- Last voted round is round of new vote
  newVoteSameEpochGreaterRound _ (step-init _) v⊂m m∈outs sig = ⊥-elim (¬Any[] m∈outs)
  newVoteSameEpochGreaterRound {pre = pre} {pid} {m = m} r (step-msg {(_ , nm)} msg∈pool pinit) v⊂m m∈outs sig vnew
     rewrite pinit
     with nm
  ...| P msg
    with msgsToSendWereSent {pid} {0} {P msg} {m} {peerStates pre pid} m∈outs
  ...| vm , refl , vmSent
    with msgsToSendWereSent1 {pid} {0} {msg} {vm} {peerStates pre pid} vmSent
  ...| _ , v∈outs
     rewrite SendVote-inj-v  (Any-singleton⁻ v∈outs)
           | SendVote-inj-si (Any-singleton⁻ v∈outs)
    with v⊂m
       -- Rebuilding keeps the same signature, and the SyncInfo included with the
       -- VoteMsg sent comprises QCs from the peer's state.  Votes represented in
       -- those QCS have signatures that have been sent before, contradicting the
       -- assumption that v's signature has not been sent before.
  ...| vote∈qc {vs = vs} {qc} vs∈qc v≈rbld (inV qc∈m)
                  rewrite cong ₋vSignature v≈rbld
                        | procPMCerts≡ {0} {msg} {peerStates pre pid} {vm} v∈outs
     = ⊥-elim (vnew (qcVotesSentB4 r pinit refl qc∈m refl vs∈qc))
  ...| vote∈vm {si} = refl , refl , refl

  -- Always true, so far, as no epoch changes.
  noEpochChangeYet : ∀ {e}{pre : SystemState e}{pid}{initd' ppre ppost msgs}
                   → ReachableSystemState pre
                   → ppre ≡ peerStates pre pid
                   → StepPeerState pid (availEpochs pre) (msgPool pre) (initialised pre) ppre initd' (ppost , msgs)
                   → (₋epEC ppre) ^∙ epEpoch ≡ (₋epEC ppost) ^∙ epEpoch
  noEpochChangeYet _ ppre≡ (step-init ix) = {!!}
  noEpochChangeYet _ ppre≡ (step-msg {(_ , m)} _ _)
     with m
  ...| P p = refl
  ...| V v = refl
  ...| C c = refl

  -- We resist the temptation to combine this with the noEpochChangeYet because in future there will be epoch changes
  lastVoteRound-mono : ∀ {e}{pre : SystemState e}{pid}{initd' ppre ppost msgs}
                     → ReachableSystemState pre
                     → ppre ≡ peerStates pre pid
                     → StepPeerState pid (availEpochs pre) (msgPool pre) (initialised pre) ppre initd' (ppost , msgs)
                     → (₋epEC ppre) ^∙ epEpoch ≡ (₋epEC ppost) ^∙ epEpoch
                     → (₋epEC ppre) ^∙ epLastVotedRound ≤ (₋epEC ppost) ^∙ epLastVotedRound
  lastVoteRound-mono _ ppre≡ (step-init ix) _ = {!!}
  lastVoteRound-mono _ ppre≡ (step-msg {(_ , m)} _ _)
     with m
  ...| P p = const (≤-step (≤-reflexive refl))
  ...| V v = const (≤-reflexive refl)
  ...| C c = const (≤-reflexive refl)

  -- This is the information we can establish about the state after the first time a signature is
  -- sent, and that we can carry forward to subsequent states, so we can use it to prove
  -- VO.ImplObligation₁.
  LvrProp : CarrierProp
  LvrProp v ep = (  v ^∙ vEpoch ≢ (₋epEC ep) ^∙ epEpoch
                 ⊎ (v ^∙ vEpoch ≡ (₋epEC ep) ^∙ epEpoch × v ^∙ vRound ≤ (₋epEC ep) ^∙ epLastVotedRound))

  LvrCarrier = PropCarrier LvrProp

  firstSendEstablishes : ∀ {e} → Vote → PK → (origSt : SystemState e) → SystemStateRel Step
  firstSendEstablishes _ _ _ (step-epoch _)               = Lift (ℓ+1 0ℓ) ⊥
  firstSendEstablishes _ _ _ (step-peer (step-cheat _ _)) = Lift (ℓ+1 0ℓ) ⊥
  firstSendEstablishes {e} v' pk origSt sysStep@(step-peer {e'} {pid'} {pre = pre} pstep@(step-honest _)) =
                         ( ReachableSystemState pre
                         × ¬ MsgWithSig∈ pk (signature v' unit) (msgPool pre)
                         × LvrCarrier pk (₋vSignature v') (StepPeer-post pstep)
                         )

  isValidNewPart⇒fSE : ∀ {e e' pk v'}{pre : SystemState e} {post : SystemState e'} {theStep : Step pre post}
                     → Meta-Honest-PK pk
                     → (ivnp : IsValidNewPart (₋vSignature v') pk theStep)
                     → firstSendEstablishes v' pk pre theStep
  isValidNewPart⇒fSE {pre = pre} {theStep = step-peer {pid = β} {outs = outs} pstep} hpk (_ , ¬sentb4 , mws , _)
     with Any-++⁻ (List-map (β ,_) outs) (msg∈pool mws)
     -- TODO-1 : Much of this proof is not specific to the particular property being proved, and could be
     -- refactored into Yasm.Properties.  See proof of unwind and refactor to avoid redundancy?
  ...| inj₂ furtherBack = ⊥-elim (¬sentb4 (MsgWithSig∈-transp mws furtherBack))
  ...| inj₁ thisStep
     with pstep
  ...| step-cheat fm isCheat
     with thisStep
  ...| here refl
     with isCheat (msg⊆ mws) (msgSigned mws)
  ...| inj₁ dis = ⊥-elim (hpk dis)
  ...| inj₂ sentb4 rewrite msgSameSig mws = ⊥-elim (¬sentb4 sentb4)

  isValidNewPart⇒fSE {e}{pk = pk}{pre = pre}{theStep = step-peer {.e} {β} {postst} {outs} {.pre} pstep} hpk (r , ¬sentb4 , mws , vpk)
     | inj₁ thisStep
     | step-honest {.β} {postst} {outs} {init'} hstep
     with Any-satisfied-∈ (Any-map⁻ thisStep)
  ...| nm , refl , nm∈outs
     with hstep
  ...| step-init _ = ⊥-elim (¬Any[] nm∈outs)
  ...| step-msg {m} m∈pool _
     with impl-sps-avp {m = msgWhole mws} r hpk hstep nm∈outs (msg⊆ mws) (msgSigned mws)
  ...| inj₂ sentb4 rewrite msgSameSig mws = ⊥-elim (¬sentb4 sentb4)
  ...| inj₁ (vpk' , _)
     with sameEpoch⇒sameEC vpk vpk' refl
  ...| refl
     with newVoteSameEpochGreaterRound r hstep (msg⊆ mws) nm∈outs (msgSigned mws)
                                       (subst (λ sig → ¬ MsgWithSig∈ pk sig (msgPool pre))
                                              (sym (msgSameSig mws))
                                              ¬sentb4)
  ...| refl , refl , newlvr
     with noEpochChangeYet {ppre = peerStates pre β} r refl hstep
  ...| eids≡
     with StepPeer-post-lemma pstep
  ...| post≡ = r , ¬sentb4 , mkCarrier (step-s r (step-peer pstep)) mws vpk
                                       (inj₂ ( trans  eids≡ (auxEid post≡)
                                             , ≤-reflexive (trans newlvr (auxLvr post≡))))
                                       where auxEid = cong (_^∙ epEpoch ∘ ₋epEC)
                                             auxLvr = cong (_^∙ epLastVotedRound ∘ ₋epEC)

  ImplPreservesLvr : PeerStepPreserves LvrProp
  -- We don't have a real model for the initial peer state, so we can't prove this case yet.
  -- Eventually, we'll prove something like a peer doesn't initialize to an epoch for which
  -- it has already sent votes.
  ImplPreservesLvr r _ (step-init ix) = {!!}
  ImplPreservesLvr {pre = pre} r prop (step-msg {m} m∈pool inited)
     with carrProp prop
  ...| preprop
     with noEpochChangeYet r refl (step-msg m∈pool inited)
  ...| stepDNMepoch
     with preprop
  ...| inj₁ diffEpoch = inj₁ λ x → diffEpoch (trans x (sym stepDNMepoch))
  ...| inj₂ (sameEpoch , rnd≤ppre)
     with (msgPart (carrSent prop)) ^∙ vEpoch ≟ (₋epEC (peerStates pre (msgSender (carrSent prop)))) ^∙ epEpoch
  ...| no neq = ⊥-elim (neq sameEpoch)
  ...| yes refl
     with lastVoteRound-mono r refl (step-msg m∈pool inited)
  ...| es≡⇒lvr≤
     = inj₂ (stepDNMepoch , ≤-trans rnd≤ppre (es≡⇒lvr≤ stepDNMepoch))

  LvrCarrier-transp* : ∀ {e e' pk sig} {start : SystemState e}{final : SystemState e'}
                     → LvrCarrier pk sig start
                     → (step* : Step* start final)
                     → LvrCarrier pk sig final
  LvrCarrier-transp* lvrc step-0 = lvrc
  LvrCarrier-transp* lvrc (step-s s* s) = Carrier-transp LvrProp ImplPreservesLvr s (LvrCarrier-transp* lvrc s*)

  fSE⇒rnd≤lvr : ∀ {v' pk e'}
              → {final : SystemState e'}
              → Meta-Honest-PK pk
              → ∀ {d d'}{pre : SystemState d}{post : SystemState d'}{theStep : Step pre post}
              → firstSendEstablishes v' pk post theStep
              → Step* post final
              → LvrCarrier pk (signature v' unit) final
  fSE⇒rnd≤lvr _ {theStep = step-epoch _} ()
  fSE⇒rnd≤lvr hpk {theStep = step-peer (step-honest _)} (_ , _ , lvrc) step* = LvrCarrier-transp* lvrc step*

  vo₁ : VO.ImplObligation₁
  -- Initialization doesn't send any messages at all so far.  In future it may send messages, but
  -- probably not containing Votes?
  vo₁ r (step-init _) _ _ m∈outs = ⊥-elim (¬Any[] m∈outs)
  vo₁ {e} {pid} {pk = pk} {pre = pre} r (step-msg m∈pool ps≡)
      {v' = v'} hpk v⊂m m∈outs sig ¬sentb4 vpb v'⊂m' m'∈pool sig' refl rnds≡
     with newVoteSameEpochGreaterRound {e} {pre} {pid = pid} r
                                       (step-msg m∈pool ps≡) v⊂m m∈outs sig ¬sentb4
  ...| eIds≡' , suclvr≡v'rnd , _
     -- Use unwind to find the step that first sent the signature for v', then Any-Step-elim to
     -- prove that going from the poststate of that step to pre results in a state in which the
     -- round of v' is at most the last voted round recorded in the peerState of the peer that
     -- sent v'
     with Any-Step-elim {Q = LvrCarrier pk (₋vSignature v') pre}
                        (fSE⇒rnd≤lvr {v'} hpk)
                        (Any-Step-⇒ (λ _ ivnp → isValidNewPart⇒fSE {v' = v'} hpk ivnp)
                                    (unwind r hpk v'⊂m' m'∈pool sig'))
  ...| mkCarrier r' mws vpf' preprop
     -- The fake/trivial handler always sends a vote for its current epoch, but for a
     -- round greater than its last voted round
     with sameHonestSig⇒sameVoteData hpk (msgSigned mws) sig' (msgSameSig mws)
  ...| inj₁ hb = ⊥-elim (PerState.meta-sha256-cr pre r hb)
  ...| inj₂ refl
     -- Both votes have the same epochID, therefore same EpochConfig
     with sameEpoch⇒sameEC vpb vpf' refl
                    -- Both peers are allowed to sign for the same PK, so they are the same peer
  ...| refl rewrite NodeId-PK-OK-injective (vp-ec vpb) (vp-sender-ok vpb) (vp-sender-ok vpf')
     with noEpochChangeYet r' refl (step-msg m∈pool ps≡)
  ...| stepDNMepoch
     with preprop
  ...| inj₁ diffEpoch = ⊥-elim (diffEpoch eIds≡')
  ...| inj₂ (sameEpoch , v'rnd≤lvr)
                    -- So we have proved both that the round of v' is ≤ the lastVotedRound of
                    -- the peer's state and that the round of v' is one greater than that value,
                    -- which leads to a contradiction
                    = ⊥-elim (1+n≰n (≤-trans (≤-reflexive suclvr≡v'rnd)
                                             (≤-trans (≤-reflexive rnds≡) v'rnd≤lvr)))

  -- TODO-1: This proof should be refactored to reduce redundant reasoning about the two votes.  The
  -- newVoteSameEpochGreaterRound property uses similar reasoning.
  vo₂ : VO.ImplObligation₂
  vo₂ _ (step-init _) _ _ m∈outs _ _ _ _ _ _ _ _ = ⊥-elim (¬Any[] m∈outs)
  vo₂ {pid = pid} {pre = pre} r (step-msg {_ , nm} _ pinit) {m = m} {m' = m'}
      hpk v⊂m m∈outs sig vnew vpk v'⊂m' m'∈outs sig' v'new vpk' es≡ rnds≡
    with nm
  ...| P msg
    with msgsToSendWereSent {pid} {0} {P msg} {m} {peerStates pre pid} m∈outs
  ...| vm , refl , vmSent
    with msgsToSendWereSent1 {pid} {0} {msg} {vm} {peerStates pre pid} vmSent
  ...| _ , v∈outs
    with v⊂m
       -- Rebuilding keeps the same signature, and the SyncInfo included with the
       -- VoteMsg sent comprises QCs from the peer's state.  Votes represented in
       -- those QCS have signatures that have been sent before, contradicting the
       -- assumption that v's signature has not been sent before.
  ...| vote∈qc {vs = vs} {qc} vs∈qc v≈rbld (inV qc∈m)
                  rewrite cong ₋vSignature v≈rbld
                        | procPMCerts≡ {0} {msg} {peerStates pre pid} {vm} v∈outs
                        | SendVote-inj-v (Any-singleton⁻ v∈outs)
     = ⊥-elim (vnew (qcVotesSentB4 r pinit refl qc∈m refl vs∈qc))
  ...| vote∈vm {si}
     with m'
  ...| P _ = ⊥-elim (P≢V (Any-singleton⁻ m'∈outs))
  ...| C _ = ⊥-elim (C≢V (Any-singleton⁻ m'∈outs))
  ...| V vm'
       -- Because the handler sends only one message, the two VoteMsgs vm and vm' are the same
     rewrite V-inj (trans (Any-singleton⁻ m'∈outs) (sym (Any-singleton⁻ m∈outs)))
     with v'⊂m'
       -- Both votes are the vote in the (single) VoteMsg, so their biIds must be the same
  ...| vote∈vm = refl
       -- Here we use the same reasoning as above to show that v' is not new
  ...| vote∈qc vs∈qc v≈rbld (inV qc∈m)
                  rewrite cong ₋vSignature v≈rbld
                        | procPMCerts≡ {0} {msg} {peerStates pre pid} {vm} v∈outs
     = ⊥-elim (v'new (qcVotesSentB4 r pinit refl qc∈m refl vs∈qc))

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
-- Andreas, 2017-01-26

-- A hopefully exhaustive list of reasons why a function cannot
-- be projection-like.  The correctness is ensured by triggering
-- a crash if any of the functions in this file is projection-like.

{-# OPTIONS -v tc.proj.like.crash:1000 #-}

data ⊥ : Set where
record ⊤ : Set where

data Bool : Set where
  true false : Bool

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

-- Not projection-like because recursive.
-- (Could be changed).

id' : ∀{A} (xs : List A) → List A
id' [] = []
id' (x ∷ xs) = x ∷ id' xs

-- Not projection-like because constructor-headed.
-- (Could this be changed?)

NonEmpty : ∀{A} (xs : List A) → Set
NonEmpty []       = ⊥
NonEmpty (x ∷ xs) = ⊤

-- Not projection-like because of absurd match.
-- Reason: we cannot infer the value of @A@ for stuck @head [] p@.

head : ∀{A} (xs : List A) (p : NonEmpty xs) → A
head []       ()
head (x ∷ xs) _ = x

-- Not projection-like because of matching on non-principal argument.
-- Reason: we cannot infer the value of @A@ for @dropHeadIf (x ∷ xs) b@.
-- (Constructor applications are not inferable in general.)

dropHeadIf : ∀{A} (xs : List A) (b : Bool) → List A
dropHeadIf (_ ∷ xs) true = xs
dropHeadIf xs _ = xs

-- Not projection-like because of deep matching.
-- Reason: we cannot infer @A@ for @drop2 (x ∷ xs)@.

drop2 : ∀{A} (xs : List A) → List A
drop2 (_ ∷ (_ ∷ xs)) = xs
drop2 xs = xs

-- Not projection-like because @abstract@.
-- Reason: @tail []@ is stuck outside of the abstract block.

abstract
  tail : ∀{A} (xs : List A) → List A
  tail [] = []
  tail (_ ∷ xs) = xs

-- Not projection-like because mutually defined.

mutual
  odds : ∀{A} (xs : List A) → List A
  odds []       = []
  odds (x ∷ xs) = evens xs

  postulate
    evens : ∀{A} (xs : List A) → List A
    -- evens [] = []
    -- evens (x ∷ xs) = x ∷ odds xs

-- Not projection-like because no parameters.

IsTrue : Bool → Set
IsTrue true  = ⊤
IsTrue false = ⊥

-- Not projection-like because type can reduce.

idTrue : (b : Bool) (p : IsTrue b) → Bool
idTrue b p = b

-- Not projection-like because it returns a paramter

par : {A : Set} (xs : List A) → Set
par {A} xs = A

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.KcompPrelims
open import Cubical.ZCohomology.Groups.Sn

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
  hiding (map)
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁)
  hiding (map)

open import Cubical.Data.Bool
open import Cubical.Data.Sigma
open import Cubical.Data.Int

open import Cubical.Algebra.Group

open GroupIso
open GroupHom
open BijectionIso

-- --------------------------H¹(S¹) -----------------------------------
{-
In order to apply Mayer-Vietoris, we need the following lemma.
Given the following diagram
  a ↦ (a , 0)   ψ         ϕ
 A -->  A × A -------> B --->  C
If ψ is an isomorphism and ϕ is surjective with ker ϕ ≡ {ψ (a , a) ∣ a ∈ A}, then C ≅ B
-}

diagonalIso : ∀ {ℓ ℓ' ℓ''} {A : Group {ℓ}} (B : Group {ℓ'}) {C : Group {ℓ''}}
               (ψ : GroupIso (dirProd A A) B) (ϕ : GroupHom B C)
             → isSurjective _ _ ϕ
             → ((x : ⟨ B ⟩) → isInKer B C ϕ x
                                    → ∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
             → ((x : ⟨ B ⟩) → (∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
                                    → isInKer B C ϕ x)
             → GroupIso A C
diagonalIso {A = A} B {C = C} ψ ϕ issurj ker→diag diag→ker = BijectionIsoToGroupIso bijIso
  where
  open GroupStr
  module A = GroupStr (snd A)
  module B = GroupStr (snd B)
  module C = GroupStr (snd C)
  module A×A = GroupStr (snd (dirProd A A))
  module ψ = GroupIso ψ
  module ϕ = GroupHom ϕ
  ψ⁻ = inv ψ

  fstProj : GroupHom A (dirProd A A)
  fun fstProj a = a , GroupStr.0g (snd A)
  isHom fstProj g0 g1 i = (g0 A.+ g1) , GroupStr.lid (snd A) (GroupStr.0g (snd A)) (~ i)

  bijIso : BijectionIso A C
  map' bijIso = compGroupHom fstProj (compGroupHom (map ψ) ϕ)
  inj bijIso a inker = pRec (isSetCarrier A _ _)
                             (λ {(a' , id) → (cong fst (sym (leftInv ψ (a , GroupStr.0g (snd A))) ∙∙ cong ψ⁻ id ∙∙ leftInv ψ (a' , a')))
                                           ∙ cong snd (sym (leftInv ψ (a' , a')) ∙∙ cong ψ⁻ (sym id) ∙∙ leftInv ψ (a , GroupStr.0g (snd A)))})
                             (ker→diag _ inker)
  surj bijIso c =
    pRec propTruncIsProp
         (λ { (b , id) → ∣ (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)))
                          , ((sym (GroupStr.rid (snd C) _)
                           ∙∙ cong ((fun ϕ) ((fun (map ψ)) (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)) , GroupStr.0g (snd A))) C.+_)
                                  (sym (diag→ker (fun (map ψ) ((snd (ψ⁻ b)) , (snd (ψ⁻ b))))
                                                  ∣ (snd (ψ⁻ b)) , refl ∣₁))
                           ∙∙ sym ((isHom ϕ) _ _))
                           ∙∙ cong (fun ϕ) (sym ((isHom (map ψ)) _ _)
                                        ∙∙ cong (fun (map ψ)) (ΣPathP (sym (GroupStr.assoc (snd A) _ _ _)
                                                                           ∙∙ cong (fst (ψ⁻ b) A.+_) (GroupStr.invl (snd A) _)
                                                                           ∙∙ GroupStr.rid (snd A) _
                                                                        , (GroupStr.lid (snd A) _)))
                                        ∙∙ rightInv ψ b)
                           ∙∙ id) ∣₁ })
         (issurj c)

H¹-S¹≅ℤ : GroupIso intGroup (coHomGr 1 (S₊ 1))
H¹-S¹≅ℤ =
    diagonalIso (coHomGr 0 (S₊ 0))
                (invGroupIso H⁰-S⁰≅ℤ×ℤ)
                (K.d 0)
                (λ x → K.Ker-i⊂Im-d 0 x
                                     (ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _
                                            , isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _)))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                        (λ x inker
                            → pRec propTruncIsProp
                                    (λ {((f , g) , id') → helper x f g id' inker})
                                    ((K.Ker-d⊂Im-Δ 0 ∣ x ∣₂ inker)))))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                         λ F surj
                           → pRec (setTruncIsSet _ _)
                                   (λ { (x , id) → K.Im-Δ⊂Ker-d 0 ∣ F ∣₂
                                                      ∣ (∣ (λ _ → x) ∣₂ , ∣ (λ _ → 0) ∣₂) ,
                                                       (cong ∣_∣₂ (funExt (surjHelper x))) ∙ sym id ∣₁ })
                                   surj) )
  □ invGroupIso (coHomPushout≅coHomSn 0 1)
  where
  module K = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)

  surjHelper :  (x : Int) (x₁ : S₊ 0) → x -[ 0 ]ₖ 0 ≡ S0→Int (x , x) x₁
  surjHelper x true = Iso.leftInv (Iso-Kn-ΩKn+1 0) x
  surjHelper x false = Iso.leftInv (Iso-Kn-ΩKn+1 0) x

  helper : (F : S₊ 0 → Int) (f g : ∥ (Unit → Int) ∥₂)
           (id : GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂)
         → isInKer (coHomGr 0 (S₊ 0))
                    (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
                    (K.d 0)
                    ∣ F ∣₂
         → ∃[ x ∈ Int ] ∣ F ∣₂ ≡ inv H⁰-S⁰≅ℤ×ℤ (x , x)
  helper F =
    sElim2 (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
           λ f g id inker
             → pRec propTruncIsProp
                     (λ ((a , b) , id2)
                        → sElim2 {C = λ f g → GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂ → _ }
                                  (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                                  (λ f g id → ∣ (helper2 f g .fst) , (sym id ∙ sym (helper2 f g .snd)) ∣₁)
                                  a b id2)
                     (MV.Ker-d⊂Im-Δ _ _ (S₊ 0) (λ _ → tt) (λ _ → tt) 0 ∣ F ∣₂ inker)
    where
    helper2 : (f g : Unit → Int)
            → Σ[ x ∈ Int ] (inv H⁰-S⁰≅ℤ×ℤ (x , x))
             ≡ GroupHom.fun (K.Δ 0) (∣ f ∣₂ , ∣ g ∣₂)
    helper2 f g = (f _ -[ 0 ]ₖ g _) , cong ∣_∣₂ (funExt λ {true → refl ; false → refl})

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module Sec2 where
open import Sec4
data Bool : Set where
  T : Bool
  F : Bool

_∣∣_ : Bool → Bool → Bool
_ ∣∣ F = F
_ ∣∣ T = T

_&_ : Bool → Bool → Bool
_ & F = F
F & T = F
T & T = T

_==>_ : Bool → Bool → Bool
F ==> _ = T
T ==> F = F
T ==> T = T

not : Bool -> Bool
not T = F
not F = T

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

_+_ : ∀ (m : ℕ) → ∀ (n : ℕ) → ℕ
Z + m = m
(S n) + m = S (n + m)

_*_ : ℕ → ℕ → ℕ
Z * m = Z
(S n) * m = (n * m) + m

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN BOOL Bool #-}

_≤_ : ℕ → ℕ → Bool
Z ≤ _ = T
(S n) ≤ Z = F
(S n) ≤ (S m) = n ≤ m

_<_ : ℕ → ℕ → Bool
Z < (S _) = T
Z < Z = F
(S n) < (S m) = n < m
(S n) < Z = F

_≥_ : ℕ → ℕ → Bool
m ≥ n = n ≤ m

_>_ : ℕ → ℕ → Bool
m > n = n < m

-- XXX: == on Nat
_==_ : ℕ → ℕ → Bool
x == y = (x ≥ y) & (x ≤ y)

_-_ : ℕ → ℕ → ℕ
Z - _ = Z
(S n) - Z = (S n)
(S n) - (S m) = n - m

K : {A B : Set} → A → B → A
K x _ = x

SC : {A B C : Set} → (A → B → C) → (A → B) → A → C
SC f g x = f x (g x)

-- XXX: The list type
data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

length : {A : Set} → List A → ℕ
length [] = Z
length (x ∷ m) = 1 + length m

test : List ℕ
test = 2 ∷ (3 ∷ [])

test1 : ℕ
test1 = length test

data So : Bool → Set where
  ok : So T

private head : {A : Set} → (x : List A) → So ((length x) ≥ 1) → A
head [] ()
head (x ∷ x₁) _ = x

private tail : {A : Set} → (x : List A) → So ((length x) ≥ 1) → List A
tail [] ()
tail (x ∷ x₁) _ = x₁

if_then_else_ : {A : Set} → Bool → A → A → A
if T then x else _ = x
if F then _ else y = y

private filter : {A : Set} → (A → Bool) → List A → List A
filter cmp [] = []
filter cmp (x ∷ x₁) = if (cmp x)
                      then x ∷ (filter cmp x₁)
                      else filter cmp x₁

_++_ : {A : Set} →  List A → List A → List A
[] ++ r = r
(x ∷ l) ++ r = x ∷ (l ++ r)

insert : (a : ℕ) → (List ℕ) → (List ℕ)
insert a [] = (a ∷ [])
insert a (x ∷ l) = if (a ≤ x)
                   then (a ∷ (x ∷ l))
                   else (x ∷ (insert a l))

tt2 : List ℕ
tt2 = insert 9 (0 ∷ (8 ∷ []))

private foldl : {A : Set} → (A → A → A) → List A → A → A
foldl _ [] y = y
foldl f (x ∷ x₁) y = foldl f x₁ (f x y)

-- XXX: injective tuple
data _+′_  (A B : Set) : Set where
  inl : (x : A) → A +′ B
  inr : (x : B) → A +′ B

case : {A B C : Set} → (A +′ B) → (f₁ : (A → C)) → (f₂ : (B → C)) → C
case (inl x) f₁ _ = f₁ x
case (inr x) _ f₂ = f₂ x

-- XXX: Proof of transitivity of >
T> : (a b c : ℕ) → So (a > b) → So (b > c) → So (a > c)
T> Z Z Z () y
T> Z Z (S c) () y
T> Z (S b) c () y
T> (S a) Z Z ok ()
T> (S a) Z (S c) ok ()
T> (S a) (S b) Z x y = ok
T> (S a) (S b) (S c) x y = T> a b c x y

-- XXX: Tuple type
data _Π_ (A B : Set) : Set where
  <_,_> : (x : A) → (y : B) → A Π B

private zip : {A B : Set} → (xs : List A) → (ys : List B) → So ((length xs) == (length ys)) → List (A Π B)
zip [] [] k = []
zip [] (x ∷ ys) ()
zip (x ∷ xs) [] ()
zip (x ∷ xs) (y ∷ ys) k = < x , y > ∷ zip xs ys k

-- TODO: Write unzip later on
-- unzip : {A B : Set} → List (A Π B) → (List A Π List B)
-- unzip xs = {!!}

test5 : List (ℕ Π ℕ)
test5 = zip ((1 ∷ [])) (2 ∷ []) ok

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

-- XXX: Transitivity of ℕ
ℕ-trans : ∀ {x y z : ℕ} → (x ≡ y) → (y ≡ z) → (x ≡ z)
ℕ-trans refl refl = refl

-- XXX: Symmetry of ℕ
sym : ∀ {x y : ℕ} → (x ≡ y) → (y ≡ x)
sym refl = refl

-- XXX: Congruence of ℕ
cong : ∀ {x y : ℕ} → (x ≡ y) → (1 + x) ≡ (1 + y)
cong refl = refl

plus-z : ∀ (y : ℕ) → ((y + Z) ≡ y)
plus-z Z = refl
plus-z (S y) = cong (plus-z y)

assoc-+ : ∀ (a b c : ℕ) → ((a + b) + c) ≡ (a + (b + c))
assoc-+ Z y z = refl
assoc-+ (S x) y z = cong (assoc-+ x y z)

t1 : ∀ (x y : ℕ) → (x + S y) ≡ S (x + y)
t1 Z y = refl
t1 (S x) y = cong (t1 x y)

-- See this: https://github.com/dvanhorn/play/blob/master/agda/Rewrite.agda
-- for examples of rewrite.
-- Also read: http://agda.readthedocs.io/en/latest/language/with-abstraction.html#generalisation
commute-+ : ∀ (x y : ℕ) → ((x + y) ≡ (y + x))
commute-+ Z y rewrite plus-z y = refl
commute-+ (S x) y rewrite t1 y x = cong (commute-+ x y)

mult-z : ∀ (y : ℕ) → ((y * Z) ≡ Z)
mult-z Z = refl
mult-z (S y) rewrite plus-z (y * Z) = mult-z y

lemma-1 : ∀ {a b : ℕ} → ∀ (n : ℕ) → (a ≡ b) → (n + a ≡ n + b)
lemma-1 _ refl = refl

c-* : ∀ (m n : ℕ) → (m * S n) ≡ (m * n) + m
c-* Z n rewrite commute-+ (n * Z) Z
                | mult-z n = refl
c-* (S m) n rewrite
            commute-+ (m * S n) (S n)
            | commute-+ ((m * n) + n) (S m)
            | commute-+ m ((m * n) + n)
            | assoc-+ (m * n) n m
            | commute-+  (m * n) (n + m)
            | assoc-+ n m (m * n)
            | commute-+ m (m * n)
            = cong (lemma-1 n (c-* m n))

commute-* : ∀ (m n : ℕ) → (m * n) ≡ (n * m)
commute-* m Z = mult-z m
commute-* m (S n) rewrite c-* m n
                          | commute-+ (m * n) m
                          | commute-+ (n * m) m = lemma-1 m (commute-* m n)

lemma-2 : ∀ (m n x : ℕ) → (m + n) * x ≡ ((m * x) + (n * x))
lemma-2 m n Z rewrite mult-z (m + n)
              | mult-z m
              | mult-z n = refl
lemma-2 m n (S x) rewrite c-* (m + n) x
                  | c-* m x
                  | c-* n x
                  | assoc-+ (m * x) m ((n * x) + n)
                  | commute-+ m ((n * x) + n)
                  | assoc-+ (n * x) n m
                  | commute-+ n m
                  | commute-+ (n * x) (m + n)
                  | commute-+ (m * x) ((m + n) + (n * x))
                  | assoc-+ (m + n) (n * x) (m * x)
                  | commute-+ (m + n) ((n * x) + (m * x))
                  | commute-+ (n * x) (m * x)
                  | commute-+ ((m * x) + (n * x)) (m + n)
                  | commute-+ ((m + n) * x) (m + n) = lemma-1 (m + n) (lemma-2 m n x)

assoc-* : ∀ (a b c : ℕ) → ((a * b) * c) ≡ (a * (b * c))
assoc-* Z b c = refl
assoc-* (S a) b c rewrite lemma-2 (a * b) b c
                  | commute-+ ((a * b) * c) (b * c)
                  | commute-+ (a * (b * c)) (b * c) = lemma-1 (b * c) (assoc-* a b c)

distributivity-+-* : ∀ (a b c : ℕ) → (a * (b + c)) ≡ ((a * b) + (a * c))
distributivity-+-* a b c rewrite commute-* a (b + c)
                         | commute-* a b
                         | commute-* a c
                         | lemma-2 b c a = refl

-- XXX: factorial function on naturals
fact : ∀ (x : ℕ) → ℕ
fact Z = (S Z)
fact (S Z) = (S Z)
fact (S x) = x * (fact x)

-- TODO: Relation on ℕ and >
_>⋆_ : ℕ → ℕ → Prop
Z >⋆ Z = ⊥
S x >⋆ Z = ⊤
Z >⋆ S y = ⊥
S x >⋆ S y = x >⋆ y

lem : (m n : ℕ) → (p : n >⋆ Z) → (m + n) >⋆ 0
lem Z n p = p
lem (S m) n p = ⋆

-- XXX: Theorem; factorial of any natural number is > 0
-- XXX: page-124, problem 4.35, Type Theory and functional programming
thm : ∀ (x : ℕ) → (fact x) >⋆ Z
thm Z = ⋆
thm (S Z) = ⋆
thm (S (S x)) = lem (x * fact (S x)) (fact (S x)) (thm (S x))

_<=_ : ∀ (m n : ℕ) → Prop
Z <= n = ⊤
S m <= Z = ⊥
S m <= S n = m <= n

-- symm : ∀ (m n : ℕ) → (p : m <= n) → (n <= m)
-- symm Z Z p = ⋆
-- symm Z (S n) p = {!!}
-- symm (S m) Z p = ⋆
-- symm (S m) (S n) p = symm m n p

transm : ∀ (m n p : ℕ) → (m <= n) → (n <= p) → (m <= p)
transm Z n p p1 p2 = ⋆
transm (S m) Z Z p1 p2 = p1
transm (S m) (S n) Z p1 p2 = p2
transm (S m) Z (S p) () p2
transm (S m) (S n) (S p) p1 p2 = transm m n p p1 p2

-- Show that 2 + 3 ≡ 3 + 2
eqq : 2 + 3 ≡ 3 + 2
eqq = refl


text:
{-# OPTIONS --without-K  #-}
module algebra.monoid where

open import algebra.monoid.core public
open import algebra.monoid.morphism public
open import algebra.monoid.mset public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --type-in-type --no-termination-check
  #-}

module Containers where

  record Sigma (A : Set) (B : A -> Set) : Set where
    field fst : A
          snd : B fst

  open Sigma

  _*_ : (A B : Set) -> Set
  A * B = Sigma A \_ -> B

  data Zero : Set where

  record One : Set where

  data PROP : Set where
    Absu : PROP
    Triv : PROP
    _/\_ : PROP -> PROP -> PROP
    All : (S : Set) -> (S -> PROP) -> PROP

  Prf : PROP -> Set
  Prf Absu = Zero
  Prf Triv = One
  Prf (P /\ Q) = Prf P * Prf Q
  Prf (All S P) = (x : S) -> Prf (P x)

  _,_ : forall {A B} -> (a : A) -> B a -> Sigma A B
  a , b = record { fst = a ; snd = b }

  split : ∀ {A B} {C : Sigma A B -> Set} ->
    (f : (a : A) -> (b : B a) -> C (a , b)) -> (ab : Sigma A B) -> C ab
  split f ab = f (fst ab) (snd ab)

  data _+_ (A B : Set) : Set where
    l : A -> A + B
    r : B -> A + B

  cases : ∀ {A B} {C : A + B -> Set} ->
            ((a : A) -> C (l a)) -> ((b : B) -> C (r b)) ->
            (ab : A + B) -> C ab
  cases f g (l a) = f a
  cases f g (r b) = g b

  rearrange : ∀ {A B X} (C : A → Set) (D : B → Set) (f : Sigma A C → X) →
              Sigma (A + B) (cases C D) → X + Sigma B D
  rearrange {A} {B} {X} C D f = split {A + B} (cases (\a c → l (f (a , c))) (\b d → r (b , d)))

  data CON (I : Set) : Set where
    ?? : I -> CON I
    PrfC : PROP -> CON I
    _*C_ : CON I -> CON I -> CON I
    PiC : (S : Set) -> (S -> CON I) -> CON I
    SiC : (S : Set) -> (S -> CON I) -> CON I
    MuC : (O : Set) -> (O -> CON (I + O)) -> O -> CON I

  mutual

    data Mu {I : Set} (O : Set) (D : O -> CON (I + O))
            (X : I -> Set) : O -> Set where
      inm : {o : O} -> [| D o |] (cases X (Mu O D X)) ->  Mu O D X o

    [|_|]_ : {I : Set} -> (CON I) -> (I -> Set) -> Set
    [| ?? i |] X = X i
    [| PrfC p |] X = Prf p
    [| C *C D |] X = [| C |] X * [| D |] X
    [| PiC S C |] X = (s : S) -> [| C s |] X
    [| SiC S C |] X = Sigma S \s -> [| C s |] X
    [| MuC O C o |] X = Mu O C X o

  outm : {I O : Set} {D : O -> CON (I + O)} {X : I -> Set} {o : O} ->
    Mu O D X o -> [| D o |]  (cases X (Mu O D X))
  outm (inm x) = x

  Everywhere : {I : Set} -> (D : CON I) -> (J : I -> Set) -> (X : Set) ->
               (Sigma I J -> X) ->  [| D |] J -> CON X
  Everywhere (?? i) J X c t = ?? (c (i , t))
  Everywhere (PrfC p) J X c t = PrfC Triv
  Everywhere (C *C D) J X c t =
    Everywhere C J X c (fst t) *C Everywhere D J X c (snd t)
  Everywhere (PiC S C) J X c t = PiC S (\s -> Everywhere (C s) J X c (t s))
  Everywhere (SiC S C) J X c t = Everywhere (C (fst t)) J X c (snd t)
  Everywhere (MuC O C o) J X c t = MuC (Sigma O (Mu O C J)) (\ot' ->
        Everywhere (C (fst ot'))
                   (cases J (Mu O C J))
                   (X + (Sigma O (Mu O C J)))
                   (split (cases(\i j -> l (c (i , j)))
                                (\o'' t'' -> r (o'' , t''))))
                   (outm (snd ot')))
     (o , t)

  everywhere : {I : Set} -> (D : CON I) -> (J : I -> Set) -> (X : Set) ->
               (c : Sigma I J -> X) -> (Y : X -> Set) ->
               (f : (ij : Sigma I J) -> Y (c ij)) -> (t : [| D |] J) ->
               [| Everywhere D J X c t |] Y
  everywhere (?? i) J X c Y f t = f (i , t)
  everywhere (PrfC p) J X c Y f t = _
  everywhere (C *C D) J X c Y f t =
    everywhere C J X c Y f (fst t) , everywhere D J X c Y f (snd t)
  everywhere (PiC S C) J X c Y f t = \s -> everywhere (C s) J X c Y f (t s)
  everywhere (SiC S C) J X c Y f t = everywhere (C (fst t)) J X c Y f (snd t)
  everywhere (MuC O C o) J X c Y f (inm t) =
    inm (everywhere (C o) (cases J (Mu O C J)) (X + Sigma O (Mu O C J)) (
        (split (cases (\i j -> l (c (i , j))) (\o t -> r (o , t)))))
        (cases Y (split \o'' t'' -> [| Everywhere (MuC O C o'') J X c t'' |] Y))
        (split (cases (\i j -> f (i , j))
                      (\o'' t'' -> everywhere (MuC O C o'') J X c Y f t'')))
        t)

  induction : {I O : Set} (D : O -> CON (I + O)) (J : I -> Set) (X : Set)
              (c : Sigma I J -> X) (Y : X -> Set) (f : (ij : Sigma I J) -> Y (c ij))
              (P : Sigma O (Mu O D J) -> Set) ->
              ({o : O} (v : [| D o |] cases J (Mu O D J)) ->
               [| Everywhere (D o) _ (X + Sigma O (Mu O D J))
                             (split (cases (\i j -> l (c (i , j)))
                             (\o v -> r (o , v)))) v |] cases Y P ->
               P (o , inm v)) ->
              (o : O) (v : Mu O D J o) -> P (o , v)
  induction {I} {O} D J X c Y f P p o (inm v) =
    p v (everywhere {I + O} (D o)
                    (λ x -> cases {I} {O} {\_ -> Set} J
                    (Mu O D J) x) ((X + Sigma O (Mu O D J)))
                    (rearrange J (Mu O D J) c) (cases Y P)
                    (split {I + O} (cases (\i j -> f (i , j))
                    (\o v -> induction D J X c Y f P p o v))) v)

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
module Everything where

-- basic utilities
open import Library
open import Isomorphism

-- basic category theory
open import Categories
open import Categories.Sets
open import Categories.Families
open import Categories.Initial
open import Categories.Terminal
open import Categories.CoProducts
open import Categories.PushOuts
open import Categories.Setoids -- should be replaced by standard libary def

open import Functors
open import Functors.Fin
open import Functors.FullyFaithful

open import Naturals

-- basic examples
open import Monoids
open import FunctorCat

-- ordinary monads
open import Monads
open import Monads.MonadMorphs
open import Adjunctions
open import Adjunctions.Adj2Mon
open import Monads.Kleisli
open import Monads.Kleisli.Functors
open import Monads.Kleisli.Adjunction
open import Monads.EM
open import Monads.EM.Functors
open import Monads.EM.Adjunction
open import Monads.CatofAdj
open import Monads.CatofAdj.InitAdj
open import Monads.CatofAdj.TermAdjObj
open import Monads.CatofAdj.TermAdjHom
open import Monads.CatofAdj.TermAdjUniq
open import Monads.CatofAdj.TermAdj

-- relative monads
open import RMonads
open import RMonads.RMonadMorphs
open import RAdjunctions
open import RAdjunctions.RAdj2RMon
open import RMonads.REM
open import RMonads.REM.Functors
open import RMonads.REM.Adjunction
open import RMonads.RKleisli
open import RMonads.RKleisli.Functors
open import RMonads.RKleisli.Adjunction
open import RMonads.Restriction
open import RMonads.SpecialCase
open import RMonads.CatofRAdj
open import RMonads.CatofRAdj.InitRAdj
open import RMonads.CatofRAdj.TermRAdjObj
open import RMonads.CatofRAdj.TermRAdjHom
open import RMonads.CatofRAdj.TermRAdj
open import RMonads.Modules

-- rmonad examples
open import WellScopedTerms
open import WellScopedTermsModel
open import WellTypedTerms
open import WellTypedTermsModel

open import Lawvere

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
open import Auto
open import Algebra
open import Data.List using (_∷_; [];_++_;List)
open import Data.Nat using (ℕ; suc; zero; _+_)
open import Data.Product using (_×_; ∃₂; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; sym)
open import Reflection

module Auto.Example.Even where

  private
    n+0≡n : ∀ n → n + 0 ≡ n
    n+0≡n zero    = refl
    n+0≡n (suc n) = cong suc (n+0≡n n)

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

  data Even  : ℕ →  Set where
    isEven0  : Even 0
    isEven+2 : ∀ {n} → Even n → Even (suc (suc n))

  even+ : ∀ {n m} → Even n → Even m → Even (n + m)
  even+  isEven0      e2 = e2
  even+ (isEven+2 e1) e2 = isEven+2 (even+ e1 e2)

  isEven-2 : ∀ {n} → Even (2 + n) → Even n
  isEven-2 (isEven+2 n) = n

  simple : ∀ {n} → Even n → Even (n + 2)
  simple e =  even+ e (isEven+2 isEven0)

  rules : HintDB
  rules = [] << quote isEven0
             << quote isEven+2
             << quote even+

  test₁ : Even 4
  test₁ = tactic (auto 5 rules)

  test₂ : ∀ {n} → Even n → Even (n + 2)
  test₂ = tactic (auto 5 rules)

  test₃ : ∀ {n} → Even n → Even (4 + n)
  test₃ = tactic (auto 5 rules)

  test₄ : ∀ {n} → Even n → Even (n + 2)
  test₄ = tactic (auto 5 rules)

  -- attempting to prove an impossible goal (e.g. evenness of n + 3
  -- for all n) will result in searchSpaceExhausted
  goal₁ = quoteTerm (∀ {n} → Even n → Even (n + 3))
  fail₁ : unquote (auto 5 rules goal₁) ≡ throw searchSpaceExhausted
  fail₁ = refl

  -- attempting to convert an unsupported expression (e.g. a lambda
  -- term) will result in unsupportedSyntax
  goal₂ = quoteTerm (∃₂ λ m n → Even (m + n))
  fail₂ : unquote (auto 5 rules goal₂) ≡ throw unsupportedSyntax
  fail₂ = refl

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda