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

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

open import LibraBFT.Impl.OBM.Crypto              hiding (verify)
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.ValidatorVerifier as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.KVMap                            as Map
open import Util.PKCS                             hiding (verify)
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.TimeoutCertificate where

verify : TimeoutCertificate → ValidatorVerifier → Either ErrLog Unit
verify self validator =
  withErrCtx' ("TimeoutCertificate" ∷ "verify" ∷ "failed" ∷ [])
  (ValidatorVerifier.verifyAggregatedStructSignature
    validator (self ^∙ tcTimeout) (self ^∙ tcSignatures))

verify' : Maybe TimeoutCertificate → ValidatorVerifier → Either ErrLog Unit
verify' mtc validator = maybeSMP (pure mtc) unit (` verify ` validator)

-- HC-TODO : refactor this and LedgerInfoWithSignatures
addSignature : Author → Signature → TimeoutCertificate → TimeoutCertificate
addSignature a s tc =
  case Map.lookup a (tc ^∙ tcSignatures) of λ where
    (just _) → tc
    nothing  → tc & tcSignatures ∙~ Map.kvm-insert-Haskell a s (tc ^∙ tcSignatures)


text:
module Mystuff where

-- open import Axiom.Extensionality.Propositional as AEP
open import Categories.Category.Cartesian.Bundle
open import Categories.Category.CartesianClosed.Canonical
open import Categories.Category.Core
open import Categories.Category.Slice
-- open import Categories.Functor
open import Categories.Category.BinaryProducts
-- open import Categories.Morphism
open import Categories.Object.Exponential -- 𝒞 hiding (repack)
open import Data.Product
open import Function using (const)
open import Level
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

private
  variable
    a b c d e : Level

-- so painful
_⋆_ : ∀ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ⋆ g = λ x → f (g x)

simple : Category (suc zero) zero zero
simple =
 record
  -- structure
  { Obj = Set × Set
  ; _⇒_ = _⇒_
  ; _≈_ = _≡_
  ; id  = (λ z → z) , proj₁
  ; _∘_ = _∘_
  -- properties
  ; assoc     = refl
  ; sym-assoc = refl
  ; identityˡ  = refl
  ; identityʳ  = refl
  ; identity² = refl
  -- whew, they're all trivial!
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = ∘-resp
  }
  where
  _⇒_ : Rel (Set × Set) zero
  (i , x) ⇒ (j , y) = (i → j) × (x × i → y)
  _∘_ : {A B C : Set × Set} → B ⇒ C → A ⇒ B → A ⇒ C
  _∘_ {i , x} {j , y} {_} (u , f) (v , g) =
   (λ t → u (v t)) , λ t → f (g t , v (proj₂ t))
  ∘-resp :
    {A B C : Set × Set} {f h : B ⇒ C} {g i : A ⇒ B} →
    --------------------------------------------------
    f ≡ h → g ≡ i → (f ∘ g) ≡ (h ∘ i)
  ∘-resp {A} {B} {C} {f} {h} {g} {i} x y =
   trans (cong (λ t → t ∘ g) x) (cong (λ t → h ∘ t) y)

data t : Set where
 ⊤ : t

!-unique-lemma : ∀ (x : t) → ⊤ ≡ x
!-unique-lemma ⊤ = refl

postulate
 -- I'm lazy.
 respSetC : {A B C : Set} {f h : B → C} {g i : A → B} →
  f ≡ h →
  g ≡ i →
  (λ a → f (g a)) ≡ (λ a → h (i a))
 extensionality : ∀ {A B : Set} {f g : A → B} →
  (∀ (x : A) → f x ≡ g x) →
  f ≡ g

-- I need the category of Sets...
SetC : Category (suc zero) zero zero
SetC =
 record
  { Obj = Set
  ; _⇒_ = λ x y → x → y
  ; _≈_ = _≡_
  ; id = λ x → x
  ; _∘_ = λ f g a → f (g a)
  ; assoc = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = respSetC
  }

_·_ : {I : Set} {A B C : Set} → (B × I → C) → (A × I → B) → A × I → C
_·_ {I} f g (x , i) = f (g(x , i) , i)

fiber-of-simple : {I : Set} → Category (suc zero) zero zero
fiber-of-simple {I} =
 record
  { Obj = Set
  ; _⇒_ = λ X Y → X × I → Y
  ; _≈_ = _≡_
  ; id  = proj₁
  ; _∘_ = _·_ -- this is the Kleisli composition
  ; assoc     = refl
  ; sym-assoc = refl
  ; identityˡ  = refl
  ; identityʳ  = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = rresp
  }
  where
  rresp : {A B C : Set} {f h : B × I → C} {g i : A × I → B} → f ≡ h → g ≡ i → (f · g) ≡ (h · i)
  rresp {A} {B} {C} {f} {h} {g} {i} x y = trans (cong (λ t → t · g) x) (cong (_·_ h) y)

-- each fiber of a simple fibration is cartesian
fiber-of-simple-cart : ∀ {I : Set} → CartesianCategory (suc zero) zero zero
fiber-of-simple-cart {I} =
 record
  { U = fiber-of-simple {I}
  ; cartesian =
    record
     { terminal =
       record { ⊤ = t
           ; ⊤-is-terminal =
             record
              { ! = const ⊤
              ; !-unique =
                λ f → extensionality (λ x → !-unique-lemma (f x))
              }
           }
     ; products =
       record
        { product = λ {A} {B} →
          record
           { A×B = A × B
           ; π₁ = λ x → proj₁ (proj₁ x)
           ; π₂ = λ x → proj₂ (proj₁ x)
           ; ⟨_,_⟩ = λ f g t → f t , g t
           ; project₁ = refl
           ; project₂ = refl
           ; unique = λ {refl refl → refl}
           } } } }

-- but also the total category is cartesian.
simple-cart : CartesianCategory (suc zero) zero zero
simple-cart = record
 { U = simple
 ; cartesian = record
   { terminal = record { ⊤ = t , t
                       ; ⊤-is-terminal =
                         record { ! = const ⊤ , const ⊤
                                ; !-unique = bang-uniq
                                } }
   ; products = record { product = λ {A} {B} → record
              { A×B = (proj₁ A × proj₁ B) , (proj₂ A × proj₂ B)
              ; π₁ = proj₁ , λ x → proj₁ (proj₁ x)
              ; π₂ = proj₂ , (λ x → proj₂ (proj₁ x))
              ; ⟨_,_⟩ = ⟨_,_⟩
              ; project₁ = refl
              ; project₂ = refl
              ; unique = λ {refl refl → refl}
              } } } }
              where
               bang-uniq :
                {A : Category.Obj simple}
                -------------------------
                (f : (simple Category.⇒ A) (t , t)) →
                --------------------------------------
                (simple Category.≈ (const ⊤ , const ⊤)) f
               bang-uniq {I , X} (u , k) =
                cong₂ Data.Product._,_
                 (extensionality (λ x → !-unique-lemma (u x)))
                 (extensionality (λ x → !-unique-lemma (k x)))
               ⟨_,_⟩ :
                {A B C : Set × Set} →
                (simple Category.⇒ C) A →
                (simple Category.⇒ C) B →
                (simple Category.⇒ C) ((proj₁ A × proj₁ B) , (proj₂ A × proj₂ B))
               ⟨_,_⟩ {A0 , A1} {B0 , B1} {C0 , C1} (u , h) (v , k) =
                (λ x → (u x) , (v x)) , λ x → (h x) , (k x)

fib-of-simple-ccc : {I : Set} → CartesianClosed (fiber-of-simple {I})
fib-of-simple-ccc {I} =
 record
  { ⊤ = t
  ; _×_ = _×_
  ; ! = λ x → ⊤
  ; π₁ = proj₁ ⋆ proj₁
  ; π₂ = proj₂ ⋆ proj₁
  ; ⟨_,_⟩ = λ f g ci → (f ci) , (g ci)
  ; !-unique = λ f → extensionality λ x → !-unique-lemma (f x)
  ; π₁-comp = refl
  ; π₂-comp = refl
  ; ⟨,⟩-unique = λ {refl refl → refl}
  ; _^_ = λ A B → B → A
  ; eval = evev
  ; curry = λ f ci a → f (((proj₁ ci) , a) , (proj₂ ci))
  ; eval-comp = refl
  ; curry-resp-≈ = λ {refl → refl}
  ; curry-unique = λ {refl → refl}
  }
  where
  evev : {B A : Category.Obj (fiber-of-simple {I})} → (fiber-of-simple {I} Category.⇒ ((A → B) × A)) B
  evev ((f , a) , i) = f a

{-
the arrow category has objects the morphisms of `Set` and
morphisms the commutative squares

A → B
↓   ↓
C → D
-}
arrow : Category (suc zero) zero zero
arrow = record
  { Obj = Σ (Set × Set) (λ x → proj₁ x → proj₂ x)
  ; _⇒_ = arr
  ; _≈_ = _≡_
  ; id = (λ z → z) , λ z → z
  ; _∘_ = λ {A} {B} {C} f g → comp {A} {B} {C} f g
  ; assoc = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = λ {refl refl → refl}
  }
  where
  arr : Rel (Σ (Set × Set) (λ x → proj₁ x → proj₂ x)) zero
  arr ((a , b) , x1) ((c , d) , y1) = (a → c) × (b → d)
  comp : {A B C : Σ (Set × Set) (λ x → proj₁ x → proj₂ x)} → arr B C → arr A B → arr A C
  comp {A} {B} {C} (f0 , f1) (g0 , g1) = (λ x → f0 (g0 x)) , λ x → f1 (g1 x)

arrow-ccc : CartesianClosed arrow
arrow-ccc = record
 { ⊤ = (t , t) , (λ _ → ⊤)
 ; _×_ = prod
 ; ! = (λ _ → ⊤) , (λ _ → ⊤)
 ; π₁ = proj₁ , proj₁
 ; π₂ = proj₂ , proj₂
 ; ⟨_,_⟩ = λ {A} {B} {C} f g → pair {A} {B} {C} f g
 ; !-unique = λ {A} → bang-uniq {A}
 ; π₁-comp = refl
 ; π₂-comp = refl
 ; ⟨,⟩-unique = λ {refl refl → refl}
 ; _^_ = to-the
 ; eval = λ {B} {A} → ev {B} {A}
 ; curry = λ {C} {A} {B} x → cur {C} {A} {B} x
 ; eval-comp = refl
 ; curry-resp-≈ = λ {refl → refl}
 ; curry-unique = {!   !}
 }
 where
 prod : Category.Obj arrow → Category.Obj arrow → Category.Obj arrow
 prod ((X , Y) , u) ((A , B) , v) =
  ((X × A) , (Y × B)) , λ x → (u (proj₁ x)) , (v (proj₂ x))
 pair : {C A B : Category.Obj arrow} →
  (arrow Category.⇒ C) A →
  (arrow Category.⇒ C) B →
  (arrow Category.⇒ C) (prod A B)
 pair {(X , Y) , u} {(A , B) , v} {(E , F) , w} (f0 , f1) (g0 , g1) =
  (λ x → (f0 x) , (g0 x)) , (λ x → (f1 x) , (g1 x))
 bang-uniq : {A : Category.Obj arrow} →
  (f : (arrow Category.⇒ A) ((t , t) , (λ _ → ⊤))) →
  ((λ _ → ⊤) , (λ _ → ⊤)) ≡ f
 bang-uniq (f0 , f1) =
  cong₂ _,_
   (extensionality λ x → !-unique-lemma (f0 x))
   (extensionality (λ x → !-unique-lemma (f1 x)))
 to-the : Category.Obj arrow →
  Category.Obj arrow →
  Category.Obj arrow
 to-the ((B0 , B1) , u) ((A0 , A1) , v) =
  (p , (A1 → B1)) , (λ x a1 → proj₂ (proj₁ x) a1)
   where
   p : Set
   p = Σ ((A0 → B0) × (A1 → B1)) (λ r → (λ x → u ((proj₁ r) x)) ≡ (λ x → (proj₂ r) (v x)))
 -- ^ it's the pullback-hom
 -- λ x → u (s x) ≡ λ x → t (v x)
 ev : {B A : Category.Obj arrow} → (arrow Category.⇒ prod (to-the B A) A) B
 ev {(B0 , B1) , u} {(A0 , A1)  , v} = dis , dat
  where
  dis : proj₁ (proj₁ (prod (to-the ((B0 , B1) , u) ((A0 , A1) , v)) ((A0 , A1) , v))) → B0
  dis ((d , p) , a0) = (proj₁ d) a0
  dat : proj₂ (proj₁ (prod (to-the ((B0 , B1) , u) ((A0 , A1) , v)) ((A0 , A1) , v))) → B1
  dat (fst , snd) = fst snd
 cur : {C A B : Category.Obj arrow} →
  (arrow Category.⇒ (prod C A)) B →
  (arrow Category.⇒ C) (to-the B A)
 cur {(C0 , C1) , u} {(A0 , A1) , v} {(B0 , B1) , w} (fst , snd) =
  (λ x → ((λ t → fst (x , t)) , λ t → snd (u x , t)) , extensionality (λ a0 → {!   !})) , (λ z z₁ → snd (z , z₁))

ext: agda

max_stars_repo_name: tetrapharmakon/agda-categories

max_issues_repo_name: tetrapharmakon/agda-categories

max_forks_repo_name: tetrapharmakon/agda-categories


text:
{-

Definition of the integers as a HIT inspired by slide 10 of (original
idea due to Paolo Capriotti):

http://www.cs.nott.ac.uk/~psztxa/talks/bonn18.pdf

Disclaimer: this definition is very hard to work with and I have not
been able to prove that it is equivalent to nat + nat or that it is a
set.

For a variation that relies on a different notion of equivalence
(without any 2-cell) and which seems easier to work with see:

https://github.com/RedPRL/redtt/blob/master/library/cool/biinv-int.red

It might be interesting to port that example one day.

-}
{-# OPTIONS --cubical --no-import-sorts #-}
module Cubical.Experiments.HInt where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Int
open import Cubical.Data.Nat

data ℤ : Type₀ where
  zero : ℤ
  suc  : ℤ → ℤ
  pred : ℤ → ℤ
  sucpred : (n : ℤ) → suc (pred n) ≡ n
  predsuc : (n : ℤ) → pred (suc n) ≡ n
  -- Coherence: could also be written "sucpred (suc n) ≡ cong (suc (predsuc n))"
  coh     : (n : ℤ) → Path (suc (pred (suc n)) ≡ suc n)
                           (sucpred (suc n))
                           (λ i → suc (predsuc n i))

-- This is equivalent to Int:
coherence : (n : Int) → Path (Path Int (sucInt (predInt (sucInt n))) (sucInt n))
                             (sucPred (sucInt n))
                             (cong sucInt (predSuc n))
coherence (pos zero) = refl
coherence (pos (suc n)) = refl
coherence (negsuc zero) = refl
coherence (negsuc (suc zero)) = refl
coherence (negsuc (suc (suc n))) = refl

ℤ→Int : ℤ → Int
ℤ→Int zero = pos 0
ℤ→Int (suc n) = sucInt (ℤ→Int n)
ℤ→Int (pred n) = predInt (ℤ→Int n)
ℤ→Int (sucpred n i) = sucPred (ℤ→Int n) i
ℤ→Int (predsuc n i) = predSuc (ℤ→Int n) i
ℤ→Int (coh n i j) = coherence (ℤ→Int n) i j

ℕ→ℤ : ℕ → ℤ
ℕ→ℤ zero = zero
ℕ→ℤ (suc n) = suc (ℕ→ℤ n)

negsucℕ→ℤ : ℕ → ℤ
negsucℕ→ℤ zero = pred zero
negsucℕ→ℤ (suc n) = pred (negsucℕ→ℤ n)

Int→ℤ : Int → ℤ
Int→ℤ (pos n) = ℕ→ℤ n
Int→ℤ (negsuc n) = negsucℕ→ℤ n

lem1 : ∀ n → Int→ℤ (sucInt n) ≡ suc (Int→ℤ n)
lem1 (pos n) = refl
lem1 (negsuc zero) = sym (sucpred zero)
lem1 (negsuc (suc n)) = sym (sucpred (negsucℕ→ℤ n))

lem2 : ∀ n → Int→ℤ (predInt n) ≡ pred (Int→ℤ n)
lem2 (pos zero) = refl
lem2 (pos (suc n)) = sym (predsuc (ℕ→ℤ n))
lem2 (negsuc n) = refl

-- I don't see how to fill these holes, especially the last one
ℤ→Int→ℤ : ∀ (n : ℤ) → Int→ℤ (ℤ→Int n) ≡ n
ℤ→Int→ℤ zero = refl
ℤ→Int→ℤ (suc n) = (lem1 (ℤ→Int n)) ∙ (cong suc (ℤ→Int→ℤ n))
ℤ→Int→ℤ (pred n) = (lem2 (ℤ→Int n)) ∙ (cong pred (ℤ→Int→ℤ n))
ℤ→Int→ℤ (sucpred n i) = {!!}
ℤ→Int→ℤ (predsuc n i) = {!!}
ℤ→Int→ℤ (coh n i j) = {!!}

Int→ℤ→Int : ∀ n → ℤ→Int (Int→ℤ n) ≡ n
Int→ℤ→Int (pos zero) = refl
Int→ℤ→Int (pos (suc n)) = cong sucInt (Int→ℤ→Int (pos n))
Int→ℤ→Int (negsuc zero) = refl
Int→ℤ→Int (negsuc (suc n)) = cong predInt (Int→ℤ→Int (negsuc n))

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

isSetℤ : isSet ℤ
isSetℤ = subst isSet Int≡ℤ isSetInt

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Bool
open import lib.types.Nat
open import lib.types.Fin

module lib.types.Vec where

infixr 5 _∷_

data Vec {i} (A : Type i) : ℕ → Type i where
  []  : Vec A 0
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (S n)

infix 4 _[_]=_

data _[_]=_ {i} {A : Type i} : ∀ {n} → Vec A n → ℕ → A → Type i where
  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ 0 ]= x
  there : ∀ {n} {m} {x y} {xs : Vec A n}
          (xs[m]=x : xs [ m ]= x) → y ∷ xs [ S m ]= x

module _ {i} {A : Type i} where

  length : ∀ {n} → Vec A n → ℕ
  length {n = n} _ = n

  head : ∀ {n} → Vec A (S n) → A
  head (x ∷ xs) = x

  vtail : ∀ {n} → Vec A (S n) → Vec A n
  vtail (x ∷ xs) = xs

  lookup : ∀ {n} → Vec A n → Fin n → A
  lookup [] ()
  lookup (x ∷ xs) (O , _) = x
  lookup (x ∷ xs) (S n , p) = lookup xs (n , <-cancel-S p)

  updateAt : ∀ {n} → Fin n → (A → A) → Vec A n → Vec A n
  updateAt (_ , _) _ [] = []
  updateAt (O , _) f (x ∷ xs) = (f x) ∷ xs
  updateAt (S n , p) f (x ∷ xs) = x ∷ (updateAt (n , <-cancel-S p) f xs)

max_stars_repo_name: maxdore/hott-morse

max_issues_repo_name: maxdore/hott-morse

max_forks_repo_name: maxdore/hott-morse


text:
module Data.Iterator where

import      Lvl
open import Data hiding (empty)
open import Data.Boolean
open import Functional
open import Numeral.Natural
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable a x init : T
private variable f : A → B
private variable n : ℕ

-- TODO: Is this useful when not lazy? It cannot store data and I am not sure if the whole list is evaluated in listIterator or not (strictness)
record Iterator (T : Type{ℓ}) : Type{ℓ} where
  coinductive
  field
    isEmpty : Bool
    current : if isEmpty then Unit else T -- TODO: These are essentially `Option`s but instead of storing its state, they depend on a boolean defined somewhere else
    step    : if isEmpty then Unit else Iterator(T)

open Iterator

{- TODO: This is a generalization of an iterator. It could be used to define iterators for any number of dimensions or to define double-ended iterators.
-- TODO: decidable-all-step may also be ∃{Obj = (Step → Bool) → Bool}(dec ↦ ∀{P} → (IsTrue(dec(P)) ↔ ∀ₗ(IsTrue ∘ P))). Not sure if it captures that (∀{s} → atEnd s) always is decidable by the smallest amount of assumptions. An example of this is when Step is finitely enumerable.
record Stepper (Step : Type{ℓₛ}) ⦃ decidable-all-step : ∀{P : Step → Bool} → Decidable(∀ₗ(IsTrue ∘ P)) ⦄ (T : Type{ℓ}) : Type{ℓ} where
  coinductive
  field
    atEnd : Step → Bool
    current : if decide(∀ₗ(IsTrue ∘ atEnd)) then Unit else T
    step    : (step : Step) → if(atEnd step) then Unit else Stepper(Step)(T)
-}

open import Data.Option
open import Data.Boolean.Operators
open        Data.Boolean.Operators.Programming

skip : ℕ → Iterator(T) → Iterator(T)
skip 𝟎 iter = iter
skip (𝐒 n) iter with isEmpty iter | step iter
... | 𝑇 | <>    = iter
... | 𝐹 | sIter = skip n sIter

skipExact : ℕ → Iterator(T) → Option(Iterator(T))
skipExact 𝟎 iter = Some iter
skipExact (𝐒 n) iter with isEmpty iter | step iter
... | 𝑇 | <>    = None
... | 𝐹 | sIter = skipExact n sIter

{- TODO: Not sure if I did not get the semantics of how codata works or whether the termination checker is wrong
{-# TERMINATING #-}
_++_ : Iterator(T) → Iterator(T) → Iterator(T)
isEmpty (a ++ b) with isEmpty a
... | 𝑇 = isEmpty b
... | 𝐹 = 𝐹
current (a ++ b) with isEmpty a | current a
... | 𝐹 | ca = ca
... | 𝑇 | <> with isEmpty b | current b
...     | 𝐹 | cb = cb
...     | 𝑇 | <> = <>
step (a ++ b) with isEmpty a | step a
... | 𝐹 | sa = sa ++ b
... | 𝑇 | <> with isEmpty b | step b
...     | 𝐹 | sb = sb
...     | 𝑇 | <> = <>

{-# TERMINATING #-}
map : (A → B) → (Iterator(A) → Iterator(B))
isEmpty (map f iter) = isEmpty iter
current (map f iter) with isEmpty iter | current iter
... | 𝑇 | <> = <>
... | 𝐹 | a = f(a)
step    (map f iter) with isEmpty iter | step iter
... | 𝑇 | <>    = <>
... | 𝐹 | sIter = map f sIter
-}

empty : Iterator(T)
isEmpty empty = 𝑇
current empty = <>
step    empty = <>

prepend : T → Iterator(T) → Iterator(T)
isEmpty (prepend x l) = 𝐹
current (prepend x l) = x
step    (prepend x l) = l

open import Data.List

listIterator : List(T) → Iterator(T)
listIterator ∅ = empty
listIterator (x ⊰ l) = prepend x (listIterator l)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Andreas, 2016-05-04, issue 1960 reported by Nisse

-- {-# OPTIONS -v tc.proj.amb:100 #-}

postulate
  A : Set

module M (_ : Set₁) where

  record R₁ : Set where
    field
      f : A

  open R₁ public

open M Set

record R₂ : Set where
  field
    f : A

open R₂ public

postulate
  P     : A → Set
  x     : R₁
  works : P (R₁.f x)
  test  : P   (f x)

-- should succeed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Delta-observational equivalence
------------------------------------------------------------------------
module Base.Change.Equivalence where

open import Relation.Binary.PropositionalEquality
open import Base.Change.Algebra
open import Level
open import Data.Unit
open import Data.Product
open import Function

open import Base.Change.Equivalence.Base public
open import Base.Change.Equivalence.EqReasoning public

module _
  {a} {A : Set a} {{CA : ChangeAlgebra A}}
  {x : A}
  where
  -- By update-nil, if dx = nil x, then x ⊞ dx ≡ x.
  -- As a consequence, if dx ≙ nil x, then x ⊞ dx ≡ x
  nil-is-⊞-unit : ∀ (dx : Δ x) → dx ≙ nil x → x ⊞ dx ≡ x
  nil-is-⊞-unit dx dx≙nil-x =
    begin
      x ⊞ dx
    ≡⟨ proof dx≙nil-x ⟩
      x ⊞ (nil x)
    ≡⟨ update-nil x ⟩
      x
    ∎
    where
      open ≡-Reasoning

  -- Here we prove the inverse:
  ⊞-unit-is-nil : ∀ (dx : Δ x) → x ⊞ dx ≡ x → dx ≙ (nil x)
  ⊞-unit-is-nil dx x⊞dx≡x = doe $
    begin
      x ⊞ dx
    ≡⟨ x⊞dx≡x ⟩
      x
    ≡⟨ sym (update-nil x) ⟩
      x ⊞ nil x
    ∎
    where
      open ≡-Reasoning

  -- Let's show that nil x is d.o.e. to x ⊟ x
  nil-x-is-x⊟x : nil x ≙ x ⊟ x
  nil-x-is-x⊟x = ≙-sym (⊞-unit-is-nil (x ⊟ x) (update-diff x x))

  -- TODO: we want to show that all functions of interest respect
  -- delta-observational equivalence, so that two d.o.e. changes can be
  -- substituted for each other freely.
  --
  -- * That should be be true for
  --   functions using changes parametrically.
  --
  -- * Moreover, d.o.e. should be respected by contexts [ ] x dx and df x [ ];
  --   this is proved below on both contexts at once by
  --   equiv-fun-changes-respect, and its corollaries fun-change-respects and
  --   equiv-fun-changes-funs.
  --
  -- * Finally, change algebra operations should respect d.o.e. But ⊞ respects
  --   it by definition, and ⊟ doesn't take change arguments - we will only
  --   need a proof for compose, when we define it.
  --
  -- Stating the general result, though, seems hard, we should
  -- rather have lemmas proving that certain classes of functions respect this
  -- equivalence.

  -- This results pairs with update-diff.
  diff-update : ∀ {dx : Δ x} → (x ⊞ dx) ⊟ x ≙ dx
  diff-update {dx} = doe lemma
    where
      lemma : x ⊞ (x ⊞ dx ⊟ x) ≡ x ⊞ dx
      lemma = update-diff (x ⊞ dx) x

  -- \begin{lemma}[Equivalence cancellation]
  --   |v2 `ominus` v1 `doe` dv| holds if and only if |v2 = v1 `oplus`
  --   dv|, for any |v1, v2 `elem` V| and |dv `elem` Dt ^ v1|.
  -- \end{lemma}

  equiv-cancel-1 : ∀ x' dx → (x' ⊟ x) ≙ dx → x' ≡ x ⊞ dx
  equiv-cancel-1 x' dx (doe x'⊟x≙dx) = trans (sym (update-diff x' x)) x'⊟x≙dx
  equiv-cancel-2 : ∀ x' dx → x' ≡ x ⊞ dx → x' ⊟ x ≙ dx
  equiv-cancel-2 _ dx refl = diff-update

module _
  {a} {A : Set a} {{CA : ChangeAlgebra A}}
  {b} {B : Set b} {{CB : ChangeAlgebra B}}
  where

  ≙-cong₂ : ∀ {c} {C : Set c} {x y}
       (f : A → B → C) {dx1 dx2 dy1 dy2} → dx1 ≙ dx2 → dy1 ≙ dy2 → f (x ⊞ dx1) (y ⊞ dy1) ≡ f (x ⊞ dx2) (y ⊞ dy2)
  ≙-cong₂ f dx1≙dx2 dy1≙dy2 = cong₂ f (proof dx1≙dx2) (proof dy1≙dy2)

  ≙-incrementalization : ∀ (f : A → B) (df : Δ f) x dx → (f ⊞ df) (x ⊞ dx) ⊟ f x ≙ apply df x dx
  ≙-incrementalization f df x dx = equiv-cancel-2 _ _ (incrementalization f df x dx)

  equiv-fun-changes-respect : ∀ {x : A} {dx₁ dx₂ : Δ x} {f : A → B} {df₁ df₂ : Δ f} →
    df₁ ≙₍ f ₎ df₂ → dx₁ ≙ dx₂ → apply df₁ x dx₁ ≙ apply df₂ x dx₂
  equiv-fun-changes-respect {x} {dx₁} {dx₂} {f} {df₁} {df₂} df₁≙df₂ dx₁≙dx₂ = doe lemma
    where
      open ≡-Reasoning
      -- This type signature just expands the goal manually a bit.
      lemma : f x ⊞ apply df₁ x dx₁ ≡ f x ⊞ apply df₂ x dx₂
      -- Informally: use incrementalization on both sides and then apply
      -- congruence.
      lemma =
        begin
          f x ⊞ apply df₁ x dx₁
        ≡⟨ sym (incrementalization f df₁ x dx₁) ⟩
          (f ⊞ df₁) (x ⊞ dx₁)
        ≡⟨ ≙-cong (f ⊞ df₁) dx₁≙dx₂ ⟩
          (f ⊞ df₁) (x ⊞ dx₂)
        ≡⟨ ≙-cong (λ f → f (x ⊞ dx₂)) df₁≙df₂ ⟩
          (f ⊞ df₂) (x ⊞ dx₂)
        ≡⟨ incrementalization f df₂ x dx₂ ⟩
          f x ⊞ apply df₂ x dx₂
        ∎

  fun-change-respects : ∀ {x : A} {dx₁ dx₂} {f : A → B} (df : Δ f) →
    dx₁ ≙ dx₂ → apply df x dx₁ ≙ apply df x dx₂
  fun-change-respects df dx₁≙dx₂ = equiv-fun-changes-respect (≙-refl {dx = df}) dx₁≙dx₂

  -- D.o.e. function changes behave like the same function (up to d.o.e.).
  equiv-fun-changes-funs : ∀ {x : A} {dx} {f : A → B} {df₁ df₂} →
    df₁ ≙₍ f ₎ df₂ → apply df₁ x dx ≙ apply df₂ x dx
  equiv-fun-changes-funs {dx = dx} df₁≙df₂ = equiv-fun-changes-respect df₁≙df₂ (≙-refl {dx = dx})

  derivative-doe-characterization : ∀ {a : A} {da : Δ a}
    {f : A → B} {df : RawChange f} (is-derivative : IsDerivative f df) →
    df a da ≙ f (a ⊞ da) ⊟ f a
  derivative-doe-characterization {a} {da} {f} {df} is-derivative = doe lemma
    where
      open ≡-Reasoning
      lemma : f a ⊞ df a da ≡ f a ⊞ (f (a ⊞ da) ⊟ f a)
      lemma =
        begin
          (f a ⊞ df a da)
        ≡⟨ is-derivative a da ⟩
          (f (a ⊞ da))
        ≡⟨ sym (update-diff (f (a ⊞ da)) (f a)) ⟩
          (f a ⊞ (f (a ⊞ da) ⊟ f a))
        ∎

  derivative-respects-doe : ∀ {x : A} {dx₁ dx₂ : Δ x}
    {f : A → B} {df : RawChange f} (is-derivative : IsDerivative f df) →
    dx₁ ≙ dx₂ → df x dx₁ ≙ df x dx₂
  derivative-respects-doe {x} {dx₁} {dx₂} {f} {df} is-derivative dx₁≙dx₂ =
    begin
      df x dx₁
    ≙⟨ derivative-doe-characterization is-derivative ⟩
      f (x ⊞ dx₁) ⊟ f x
    ≡⟨ cong (λ v → f v  ⊟ f x) (proof dx₁≙dx₂) ⟩
      f (x ⊞ dx₂) ⊟ f x
    ≙⟨ ≙-sym (derivative-doe-characterization is-derivative) ⟩
      df x dx₂
    ∎
    where
      open ≙-Reasoning

  -- This is also a corollary of fun-changes-respect
  derivative-respects-doe-alt : ∀ {x : A} {dx₁ dx₂ : Δ x}
    {f : A → B} {df : RawChange f} (is-derivative : IsDerivative f df) →
    dx₁ ≙ dx₂ → df x dx₁ ≙ df x dx₂
  derivative-respects-doe-alt {x} {dx₁} {dx₂} {f} {df} is-derivative dx₁≙dx₂ =
    fun-change-respects (DerivativeAsChange is-derivative) dx₁≙dx₂

  open import Postulate.Extensionality

  -- An extensionality principle for delta-observational equivalence: if
  -- applying two function changes to the same base value and input change gives
  -- a d.o.e. result, then the two function changes are d.o.e. themselves.

  delta-ext : ∀ {f : A → B} → ∀ {df dg : Δ f} → (∀ x dx → apply df x dx ≙ apply dg x dx) → df ≙ dg
  delta-ext {f} {df} {dg} df-x-dx≙dg-x-dx = doe lemma₂
    where
      open ≡-Reasoning
      -- This type signature just expands the goal manually a bit.
      lemma₁ : ∀ x dx → f x ⊞ apply df x dx ≡ f x ⊞ apply dg x dx
      lemma₁ x dx = proof $ df-x-dx≙dg-x-dx x dx
      lemma₂ : f ⊞ df ≡ f ⊞ dg
      lemma₂ = ext (λ x → lemma₁ x (nil x))

  -- You could think that the function should relate equivalent changes, but
  -- that's a stronger hypothesis, which doesn't give you extra guarantees. But
  -- here's the statement and proof, for completeness:

  delta-ext₂ : ∀ {f : A → B} → ∀ {df dg : Δ f} → (∀ x (dx₁ dx₂ : Δ x) → dx₁ ≙₍ x ₎ dx₂ → apply df x dx₁ ≙ apply dg x dx₂) → df ≙ dg
  delta-ext₂ {f} {df} {dg} df-x-dx≙dg-x-dx = delta-ext (λ x dx → df-x-dx≙dg-x-dx x dx dx ≙-refl)

  -- We know that IsDerivative f (apply (nil f)) (by nil-is-derivative).
  -- That is, df = nil f -> IsDerivative f (apply df).
  -- Now, we try to prove that if IsDerivative f (apply df) -> df = nil f.
  -- But first, we prove that f ⊞ df = f.
  derivative-is-⊞-unit : ∀ {f : A → B} df →
    IsDerivative f (apply df) → f ⊞ df ≡ f
  derivative-is-⊞-unit {f} df fdf =
    begin
      f ⊞ df
    ≡⟨⟩
      (λ x → f x ⊞ apply df x (nil x))
    ≡⟨ ext (λ x → fdf x (nil x)) ⟩
      (λ x → f (x ⊞ nil x))
    ≡⟨ ext (λ x → cong f (update-nil x)) ⟩
      (λ x → f x)
    ≡⟨⟩
      f
    ∎
    where
      open ≡-Reasoning

  -- We can restate the above as "df is a nil change".

  derivative-is-nil : ∀ {f : A → B} df →
    IsDerivative f (apply df) → df ≙ nil f
  derivative-is-nil df fdf = ⊞-unit-is-nil df (derivative-is-⊞-unit df fdf)

  derivative-is-nil-alternative : ∀ {f : A → B} df →
    (IsDerivative-f-df : IsDerivative f df) → DerivativeAsChange IsDerivative-f-df ≙ nil f
  derivative-is-nil-alternative df IsDerivative-f-df = derivative-is-nil (DerivativeAsChange IsDerivative-f-df) IsDerivative-f-df

  -- Theorem 2.10, appears in Base.Change.Algebra.
  -- nil-is-derivative : ∀ (f : A → B) → IsDerivative f (apply (nil f))

  -- If we have two derivatives, they're both nil, hence they're equivalent.
  derivative-unique : ∀ {f : A → B} {df dg : Δ f} → IsDerivative f (apply df) → IsDerivative f (apply dg) → df ≙ dg
  derivative-unique {f} {df} {dg} fdf fdg =
    begin
      df
    ≙⟨ derivative-is-nil df fdf ⟩
      nil f
    ≙⟨ ≙-sym (derivative-is-nil dg fdg) ⟩
      dg
    ∎
    where
      open ≙-Reasoning

  equiv-derivative-is-derivative : ∀ {f : A → B} df₁ df₂ → IsDerivative f (apply df₁) → df₁ ≙₍ f ₎ df₂ → IsDerivative f (apply df₂)
  equiv-derivative-is-derivative {f} df₁ df₂ IsDerivative-f-df₁ df₁≙df₂ a da =
    begin
      f a ⊞ apply df₂ a da
    ≡⟨ sym (incrementalization f df₂ a da) ⟩
      (f ⊞ df₂) (a ⊞ da)
    ≡⟨ cong (λ □ → □ (a ⊞ da)) lemma ⟩
      f (a ⊞ da)
    ∎
    where
      open ≡-Reasoning
      lemma : f ⊞ df₂ ≡ f
      lemma =
        begin
          f ⊞ df₂
        ≡⟨ proof (≙-sym df₁≙df₂) ⟩
          f ⊞ df₁
        ≡⟨ derivative-is-⊞-unit df₁ IsDerivative-f-df₁ ⟩
          f
        ∎
  equiv-nil-is-derivative : ∀ {f : A → B} df → nil f ≙₍ f ₎ df → IsDerivative f (apply df)
  equiv-nil-is-derivative {f} df = equiv-derivative-is-derivative (nil f) df (nil-is-derivative f)

  -- This is Lemma 2.5 in the paper. Note that the statement in the paper uses
  -- (incorrectly) normal equality instead of delta-observational equivalence.
  deriv-zero :
    ∀ (f : A → B) df → IsDerivative f df →
    ∀ v → df v (nil v) ≙ nil (f v)
  deriv-zero f df proof v = doe lemma
    where
      open ≡-Reasoning
      lemma : f v ⊞ df v (nil v) ≡ f v ⊞ nil (f v)
      lemma =
        begin
          f v ⊞ df v (nil v)
        ≡⟨ proof v (nil v) ⟩
          f (v ⊞ (nil v))
        ≡⟨ cong f (update-nil v) ⟩
          f v
        ≡⟨ sym (update-nil (f v)) ⟩
          f v ⊞ nil (f v)
        ∎

module _
  {a} {A : Set a} {{CA : ChangeAlgebra A}}
  {b} {B : Set b} {{CB : ChangeAlgebra B}}
  {c} {C : Set c} {{CC : ChangeAlgebra C}}
  where
  ≙-cong₃ : ∀ {d} {D : Set d} {x y z}
       (f : A → B → C → D) {dx1 dx2 dy1 dy2 dz1 dz2} →
       dx1 ≙ dx2 → dy1 ≙ dy2 → dz1 ≙ dz2 →
       f (x ⊞ dx1) (y ⊞ dy1) (z ⊞ dz1) ≡ f (x ⊞ dx2) (y ⊞ dy2) (z ⊞ dz2)
  ≙-cong₃ f dx1≙dx2 dy1≙dy2 dz1≙dz2 = cong₂ (λ x y → x y) (cong₂ f (proof dx1≙dx2) (proof dy1≙dy2)) (proof dz1≙dz2)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda