text:
-- Shrunk version of examples/TT.agda
-- Bug introduced by fix of issue 1560

{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS --no-termination-check #-}
-- {-# OPTIONS --no-positivity-check #-}

-- {-# OPTIONS -v tc.pos:10 #-}
-- {-# OPTIONS -v tc.polarity:30 #-}

data True : Set where
  tt : True

data ⊥ : Set where

infix 3 _/\_

data _/\_ (P Q : Set) : Set where
  andI : P -> Q -> P /\ Q

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- Finite sets ------------------------------------------------------------

data Suc (A : Set) : Set where
  fzero' : Suc A
  fsuc'  : A -> Suc A

mutual
  data Fin (n : Nat) : Set where
    finI : Fin' n -> Fin n

  Fin' : Nat -> Set
  Fin'  zero   = ⊥
  Fin' (suc n) = Suc (Fin n)

fsuc : {n : Nat} -> Fin n -> Fin (suc n)
fsuc i = finI (fsuc' i)

module FinEq where

  infix 5 _==_

  _==_ : {n : Nat} -> Fin n -> Fin n -> Set
  _==_ {suc _} (finI  fzero'  ) (finI  fzero'  ) = True
  _==_ {suc _} (finI (fsuc' i)) (finI (fsuc' j)) = i == j
  _==_          _                _               = ⊥

  -- Needed
  rewriteEq : {n : Nat}(C : Fin n -> Set){i j : Fin n} -> i == j -> C j -> C i
  rewriteEq {suc _} C {finI  fzero'  } {finI  fzero'  } eq x = x
  rewriteEq {suc _} C {finI (fsuc' i)} {finI (fsuc' j)} eq x = rewriteEq (\z -> C (fsuc z)) eq x
  rewriteEq {suc _} C {finI (fsuc' _)} {finI fzero'   } () _
  rewriteEq {suc _} C {finI fzero'   } {finI (fsuc' _)} () _
  rewriteEq {zero}  C {finI ()}        {_}              _  _

data Expr (n : Nat) : Set where
  eVar : Fin n -> Expr n
  eApp : Expr n -> Expr n -> Expr n

module ExprEq where

  infix 5 _==_

  _==_ : {n : Nat} -> Expr n -> Expr n -> Set
  eVar i     == eVar j     = FinEq._==_ i j
  eApp e1 e2 == eApp e3 e4 = e1 == e3 /\ e2 == e4
  _          == _          = ⊥

  rewriteEq : {n : Nat}(C : Expr n -> Set){r s : Expr n} -> r == s -> C s -> C r
  rewriteEq C {eVar i    } {eVar j    } eq x = FinEq.rewriteEq (\z -> C (eVar z)) eq x
  rewriteEq C {eApp e1 e2} {eApp e3 e4} (andI eq13 eq24) x =
    rewriteEq (\z -> C (eApp z e2)) eq13 (
      rewriteEq (\z -> C (eApp e3 z)) eq24 x
    )
  rewriteEq C {eVar _} {eApp _ _} () _
  rewriteEq C {eApp _ _} {eVar _  } () _

-- checking args of rewriteEq
-- args of rewriteEq =
--   [Mixed, Unused, Mixed, Mixed, Unused, StrictPos]
-- Computing polarity of Polarity.ExprEq.rewriteEq
-- Polarity of Polarity.ExprEq.rewriteEq from positivity:
--   [Invariant,Nonvariant,Invariant,Invariant,Nonvariant,Covariant]
-- Refining polarity with type  {n : Nat} (C : Expr n → Set)
--                              {r s : Expr n} →
--                              r == s → C s → C r
-- Polarity of Polarity.ExprEq.rewriteEq: [Invariant,Invariant,Invariant,Invariant,Nonvariant,Covariant]

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Polarity.hs:235

-- -}
-- -}


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Emptyrec {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
import Definition.Typed.Weakening as T
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.Introductions.Empty
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

open import Tools.Product
open import Tools.Unit
open import Tools.Empty
open import Tools.Nat

import Tools.PropositionalEquality as PE

-- Reducibility of natural recursion under a valid substitution.
EmptyrecTerm : ∀ {F rF lF lEmpty n Γ Δ σ l}
             ([Γ]  : ⊩ᵛ Γ)
             ([F]  : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
             (⊢Δ   : ⊢ Δ)
             ([σ]  : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
             ([σn] : Δ ⊩⟨ l ⟩ n ∷ Empty lEmpty  ^ [ % , ι lEmpty ] / Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ))))
           → Δ ⊩⟨ l ⟩ Emptyrec lF lEmpty (subst σ F) n
               ∷ subst σ F ^ [ rF , ι lF ]
               / proj₁ ([F] ⊢Δ [σ])
EmptyrecTerm {F} {rF = !} {lF} {lEmpty} {n} {Γ} {Δ} {σ} {l} [Γ] [F] ⊢Δ [σ]
           (Emptyₜ (ne d)) =
  let [Empty] = Emptyᵛ {ll = lEmpty} {l = l} [Γ]
      [σEmpty] = proj₁ ([Empty] ⊢Δ [σ])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
  in neuTerm [σF] (Emptyrecₙ) (Emptyrecⱼ ⊢F d)
                  (~-Emptyrec ⊢F≡F d d)
EmptyrecTerm {F} {rF = %} {lF} {lEmpty} {n} {Γ} {Δ} {σ} {l} [Γ] [F] ⊢Δ [σ]
           (Emptyₜ (ne d)) =
  let [Empty] = Emptyᵛ {ll = lEmpty} {l = l} [Γ]
      [σEmpty] = proj₁ ([Empty] ⊢Δ [σ])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
  in logRelIrr [σF] (Emptyrecⱼ ⊢F d)

-- Reducibility of natural recursion congurence under a valid substitution equality.
Emptyrec-congTerm : ∀ {F F′ rF lF lEmpty n m Γ Δ σ σ′ l}
                  ([Γ]      : ⊩ᵛ Γ)
                  ([F]      : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
                  ([F′]     : Γ ⊩ᵛ⟨ l ⟩ F′ ^ [ rF , ι lF ] / [Γ])
                  ([F≡F′]   : Γ ⊩ᵛ⟨ l ⟩ F ≡ F′ ^ [ rF , ι lF ] / [Γ] / [F])
                  (⊢Δ       : ⊢ Δ)
                  ([σ]      : Δ ⊩ˢ σ  ∷ Γ / [Γ] / ⊢Δ)
                  ([σ′]     : Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ)
                  ([σ≡σ′]   : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
                  ([σn]     : Δ ⊩⟨ l ⟩ n ∷ Empty lEmpty ^ [ % , ι lEmpty ] / Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ))))
                  ([σm]     : Δ ⊩⟨ l ⟩ m ∷ Empty lEmpty  ^ [ % , ι lEmpty ] / Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ))))
                → Δ ⊩⟨ l ⟩ Emptyrec lF lEmpty (subst σ F) n
                    ≡ Emptyrec lF lEmpty (subst σ′ F′) m
                    ∷ subst σ F ^ [ rF , ι lF ]
                    / proj₁ ([F] ⊢Δ [σ])
Emptyrec-congTerm {F} {F′} {rF = !} {lF} {lEmpty} {n} {m} {Γ} {Δ} {σ} {σ′} {l}
                [Γ] [F] [F′] [F≡F′]
                ⊢Δ [σ] [σ′] [σ≡σ′]
                (Emptyₜ (ne ⊢n′))
                (Emptyₜ (ne ⊢m′)) =
  let [Empty] = Emptyᵛ {ll = lEmpty} {l = l} [Γ]
      [σEmpty] = proj₁ ([Empty] ⊢Δ [σ])
      [σ′Empty] = proj₁ ([Empty] ⊢Δ [σ′])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [σ′F] = proj₁ ([F] ⊢Δ [σ′])
      [σ′F′] = proj₁ ([F′] ⊢Δ [σ′])
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      ⊢F′ = escape [σ′F′]
      ⊢F′≡F′ = escapeEq [σ′F′] (reflEq [σ′F′])
      ⊢σF≡σ′F = escapeEq [σF] (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′])
      ⊢σ′F≡σ′F′ = escapeEq [σ′F] ([F≡F′] ⊢Δ [σ′])
      ⊢F≡F′ = ≅-trans ⊢σF≡σ′F ⊢σ′F≡σ′F′
      [σF≡σ′F] = proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′]
      [σ′F≡σ′F′] = [F≡F′] ⊢Δ [σ′]
      [σF≡σ′F′] = transEq [σF] [σ′F] [σ′F′] [σF≡σ′F] [σ′F≡σ′F′]
      EmptyrecN = neuTerm [σF] (Emptyrecₙ) (Emptyrecⱼ ⊢F ⊢n′)
                           (~-Emptyrec ⊢F≡F ⊢n′ ⊢n′)
      EmptyrecM = neuTerm [σ′F′] (Emptyrecₙ) (Emptyrecⱼ ⊢F′ ⊢m′)
                           (~-Emptyrec ⊢F′≡F′ ⊢m′ ⊢m′)
      EmptyrecN≡M =
          neuEqTerm [σF] Emptyrecₙ Emptyrecₙ
                     (Emptyrecⱼ ⊢F ⊢n′)
                     (conv (Emptyrecⱼ ⊢F′ ⊢m′)
                            (sym (≅-eq (escapeEq [σF]
                              (transEq [σF] [σ′F] [σ′F′] [σF≡σ′F] [σ′F≡σ′F′])))))
                     (~-Emptyrec ⊢F≡F′ ⊢n′ ⊢m′)
  in EmptyrecN≡M

Emptyrec-congTerm {F} {F′} {rF = %} {lF} {lEmpty} {n} {m} {Γ} {Δ} {σ} {σ′} {l}
                [Γ] [F] [F′] [F≡F′]
                ⊢Δ [σ] [σ′] [σ≡σ′]
                (Emptyₜ (ne ⊢n′))
                (Emptyₜ (ne ⊢m′)) =
  let [Empty] = Emptyᵛ {ll = lEmpty} {l = l} [Γ]
      [σEmpty] = proj₁ ([Empty] ⊢Δ [σ])
      [σ′Empty] = proj₁ ([Empty] ⊢Δ [σ′])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [σ′F] = proj₁ ([F] ⊢Δ [σ′])
      [σ′F′] = proj₁ ([F′] ⊢Δ [σ′])
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      ⊢F′ = escape [σ′F′]
      ⊢F′≡F′ = escapeEq [σ′F′] (reflEq [σ′F′])
      ⊢σF≡σ′F = escapeEq [σF] (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′])
      ⊢σ′F≡σ′F′ = escapeEq [σ′F] ([F≡F′] ⊢Δ [σ′])
      ⊢F≡F′ = ≅-trans ⊢σF≡σ′F ⊢σ′F≡σ′F′
      [σF≡σ′F] = proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′]
      [σ′F≡σ′F′] = [F≡F′] ⊢Δ [σ′]
      [σF≡σ′F′] = transEq [σF] [σ′F] [σ′F′] [σF≡σ′F] [σ′F≡σ′F′]
  in logRelIrrEq [σF] (Emptyrecⱼ ⊢F ⊢n′) (conv (Emptyrecⱼ ⊢F′ ⊢m′)
                            (sym (≅-eq (escapeEq [σF]
                              (transEq [σF] [σ′F] [σ′F′] [σF≡σ′F] [σ′F≡σ′F′])))))

-- Validity of empty recursion.
Emptyrecᵛ : ∀ {F rF lF lEmpty  n Γ l} ([Γ] : ⊩ᵛ Γ)
          ([Empty]  : Γ ⊩ᵛ⟨ l ⟩ Empty lEmpty ^ [ % , ι lEmpty ] / [Γ])
          ([F]  : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
        → ([n] : Γ ⊩ᵛ⟨ l ⟩ n ∷ Empty lEmpty ^ [ % , ι lEmpty ] / [Γ] / [Empty])
        → Γ ⊩ᵛ⟨ l ⟩ Emptyrec lF lEmpty F n ∷ F ^ [ rF , ι lF ] / [Γ] / [F]
Emptyrecᵛ {F} {rF} {lF} {lEmpty} {n} {l = l} [Γ] [Empty] [F] [n]
        {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [σn] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                             (Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ)))) (proj₁ ([n] ⊢Δ [σ]))
  in EmptyrecTerm {F = F} [Γ] [F] ⊢Δ [σ] [σn]
    , λ {σ'} [σ′] [σ≡σ′] →
      let [σ′n] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ′]))
                                  (Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ)))) (proj₁ ([n] ⊢Δ [σ′]))
          [σn≡σ′n] = irrelevanceEqTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                                       (Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ))))
                                       (proj₂ ([n] ⊢Δ [σ]) [σ′] [σ≡σ′])
          congTerm = Emptyrec-congTerm {F = F} {F′ = F} [Γ] [F] [F] (reflᵛ {F} {l = l} [Γ] [F])
                                       ⊢Δ [σ] [σ′] [σ≡σ′] [σn] [σ′n]
      in congTerm

-- Validity of natural recursion congurence.
Emptyrec-congᵛ : ∀ {F F′ rF lF lEmpty n n′ Γ l} ([Γ] : ⊩ᵛ Γ)
          ([Empty]  : Γ ⊩ᵛ⟨ l ⟩ Empty lEmpty ^ [ % , ι lEmpty ] / [Γ])
          ([F]  : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
          ([F′]  : Γ ⊩ᵛ⟨ l ⟩ F′ ^ [ rF , ι lF ] / [Γ])
          ([F≡F′]  : Γ ⊩ᵛ⟨ l ⟩ F ≡ F′ ^ [ rF , ι lF ] / [Γ] / [F])
          ([n] : Γ ⊩ᵛ⟨ l ⟩ n ∷ Empty lEmpty ^ [ % , ι lEmpty ] / [Γ] / [Empty])
          ([n′] : Γ ⊩ᵛ⟨ l ⟩ n′ ∷ Empty lEmpty ^ [ % , ι lEmpty ] / [Γ] / [Empty])
        → Γ ⊩ᵛ⟨ l ⟩ Emptyrec lF lEmpty F n ≡ Emptyrec lF lEmpty F′ n′ ∷ F ^ [ rF , ι lF ] / [Γ] / [F]
Emptyrec-congᵛ {F} {F′} {rF} {lF} {lEmpty} {n} {n′} {l = l}
             [Γ] [Empty] [F] [F′] [F≡F′]
             [n] [n′] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [σn] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                             (Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ)))) (proj₁ ([n] ⊢Δ [σ]))
      [σn′] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                             (Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ)))) (proj₁ ([n′] ⊢Δ [σ]))
      congTerm = Emptyrec-congTerm {F} {F′} [Γ] [F] [F′] [F≡F′]
                                   ⊢Δ [σ] [σ] (reflSubst [Γ] ⊢Δ [σ]) [σn] [σn′]
  in congTerm

ext: agda

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
-- Non-deterministic insert and permutation with choose oracle
-- The module abstracts over the choice structure by importing it.

open import bool

module perm-keep-length
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
 where

open import eq
open import bool-thms
open import nat
open import nat-thms
open import list

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

-- Non-deterministic insert:
ndinsert : {a : Set} → Choice → a → 𝕃 a  → 𝕃 a
ndinsert _  n []        = n :: []
ndinsert ch n (x :: xs) =
  if choose ch then n :: x :: xs
               else x :: ndinsert (lchoice ch) n xs

perm : {a : Set} → Choice → 𝕃 a  → 𝕃 a
perm _  []        = []
perm ch (x :: xs) = ndinsert (lchoice ch) x (perm (rchoice ch) xs)

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

-- Non-deterministic insertion increases the list length by one:
insert-inc-length : ∀ {a : Set} → (ch : Choice) (x : a) (xs : 𝕃 a)
                 → length (ndinsert ch x xs) ≡ suc (length xs)
insert-inc-length ch x [] = refl
insert-inc-length ch x (y :: ys) with choose ch
... | tt = refl
... | ff rewrite insert-inc-length (lchoice ch) x ys = refl

-- The length of a permuted list is identical to the length of the list:
perm-length : ∀ {a : Set} → (ch : Choice) (xs : 𝕃 a)
           → length (perm ch xs) =ℕ length xs ≡ tt
perm-length ch [] = refl
perm-length ch (x :: xs)
  rewrite insert-inc-length (lchoice ch) x (perm (rchoice ch) xs)
        | perm-length (rchoice ch) xs
  = refl

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

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


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

postulate
  C  : Set

  D  : Set → Set
  d₁ : (A : Set) → D A
  d₂ : (A : Set) → (C → D A) → D A

  E  : (A : Set) → A → A → Set
  e₁ : (A : Set) (j₁ j₂ : C → D A) →
       ((c : C) → E (D A) (j₁ c) (j₂ c)) →
       (y : D A) →
       E (D A) (d₂ A j₁) y

  f  : (A B : Set) → D A → D B
  f₁ : (A B : Set) → E (D B) (f A B (d₁ A)) (d₁ B)
  f₂ : (A B : Set) (j : C → D A) →
       E (D B) (f A B (d₂ A j)) (d₂ B (λ c → f A B (j c)))

  g  : (A : Set) (Q : D A → Set) →
       Q (d₁ A) →
       ((j : C → D A) → ((c : C) → Q (j c)) → Q (d₂ A j)) →
       (c : D A) → Q c

{-# BUILTIN REWRITE E #-}
{-# REWRITE f₁        #-}
{-# REWRITE f₂        #-}

h : (A B : Set)
    (i : D A → D B) →
    E (D B) (d₁ B) (i (d₁ A)) →
    (d : D A) → E (D B) (f A B d) (i d)
h A B i e₂ = g
  A
  (λ (d : D A) → E (D B) {!f A B d!} (i d))
  e₂
  (λ j q → e₁ B (λ c → f A B (j c)) (λ c → i (j c)) q (i (d₂ A j)))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2017-11-14, issue #2849, reported by laMudri

-- Internal error, regression introduced by new pattern Internal.AbsurdP

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

-- {-# OPTIONS -v tc.with.strip:30 #-}

open import Agda.Builtin.Equality

data ⊥ : Set where

data Bool : Set where
  true false : Bool

data P : Bool → Set where
  pt : P true

postulate
  b : Bool
  eq : b ≡ false

works : P b → ⊥
works p with b | eq
works () | .false | refl

test : P b → ⊥
test () rewrite eq

-- WAS (2.5.3): Internal error

-- OK error:
-- Failed to solve the following constraints:
--   Is empty: P b

-- This could also succeed, but somehow the rewrite does not
-- apply to the IsEmpty constraint generated by the absurd pattern.
-- The rewrite should be happening before the absurd pattern split.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Proj where
open import AlonzoPrelude

showTrue : True -> String
showTrue _ = "tt"

-- data True : Set where
--   tt : True

data T4 : Set where
  C : True -> True -> True -> True -> T4

g : True -> True -> True
g x y = tt

f14 : T4 -> True -> True
f14 (C x y z t) = \w -> g x t

mainS : String
mainS = showTrue $ (id ○ f14) (C tt tt tt tt) tt

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- {-# OPTIONS -v tc.polarity:10 -v tc.pos.args:10 #-}
module UnsolvableLevelConstraintsInDataDef where

open import Common.Equality

data D : Set1 where
  abs : ∀ E → D ≡ E → (E → D) → D


text:
module sn-calculus-compatconf.split where

open import sn-calculus-compatconf.base

open import sn-calculus
open import utility renaming (_U̬_ to _∪_)
open import context-properties
  using (unwrap-rho ; wrap-rho ; ->E-view ; plugc ; unplugc)

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
  using (Can ; Canₛ ; Canₛₕ ; Canₖ ; module CodeSet)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning)
open import Data.Bool
  using (Bool ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _∷_ ; [] ; _++_)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂ ; map)
open import Function using (_∘_ ; id ; _∋_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ->E-view

open EvaluationContext1
open _≐_⟦_⟧e
open Context1
open _≐_⟦_⟧c

open ListSet Data.Nat._≟_

{-
Base case where (E, C) = ([], _∷_).

  Simply switch the reductions. Note that since E = [], the rmerge rule
  at LHS is actually  ρθ.ρθ'.qin sn⟶₁ ρ(θ←θ').qin.  Since C = _∷_, the
  reduction at RHS must go inside ρθ' so it's easy to handle.

     p
  ρθ. E⟦ qin ⟧   -- sn⟶₁ ->    ρθq. E⟦ qo ⟧
 (ρθ) E⟦C⟦rin⟧⟧   -- sn⟶₁ ->   (ρθ) E⟦C⟦ro⟧⟧
-}
1-steplρ-E-view-ecsplit : ∀{E C p qin q qo rin r ro θ θq BV FV A Aq} →
  {ρθ·psn⟶₁ρθq·q  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θq , Aq ⟩· q} →
  CorrectBinding p BV FV →
  two-roads-diverged E C →

  (p≐E⟦qin⟧  :  p ≐ E ⟦ qin ⟧e) →
  (q≐E⟦qo⟧   :  q ≐ E ⟦ qo ⟧e) →
  ->E-view  ρθ·psn⟶₁ρθq·q  p≐E⟦qin⟧  q≐E⟦qo⟧ →

  (p≐E⟦rin⟧  :  p ≐ C ⟦ rin ⟧c) →
  (r≐E⟦ro⟧   :  r ≐ C ⟦ ro ⟧c) →
  (rinsn⟶₁ro  :  rin sn⟶₁ ro) →

  ∃ λ po →
    -- LHS: 0 or 1 step (ρθ) C⟦qo⟧ sn⟶* (ρθ) C⟦poq⟧ reduction inside ρθ [ ]
    (q ≡ po ⊎ q sn⟶ po)
    ×
    -- RHS: ρθ. E'⟦ro'⟧ sn⟶₁ ρθq. E'⟦por⟧
    Σ (EvaluationContext × Term × Term) λ { (E' , ro' , por) →
      Σ[ r≐E'⟦ro'⟧      ∈  r  ≐ E' ⟦ ro' ⟧e ]
      Σ[ po≐E'⟦por⟧     ∈  po ≐ E' ⟦ por ⟧e ]
      Σ[ ρθ·rsn⟶₁ρθq·po  ∈  ρ⟨ θ , A ⟩· r sn⟶₁ ρ⟨ θq , Aq ⟩· po ]
        ->E-view  ρθ·rsn⟶₁ρθq·po  r≐E'⟦ro'⟧  po≐E'⟦por⟧
      }

1-steplρ-E-view-ecsplit cb divout-disjoint dehole dehole
  vemit () r≐C⟦ro⟧ rinsn⟶₁ro
1-steplρ-E-view-ecsplit cb divout-disjoint dehole dehole
  vset-shared-value-old () r≐C⟦ro⟧ rinsn⟶₁ro
1-steplρ-E-view-ecsplit cb divout-disjoint dehole dehole
  vset-shared-value-new () r≐C⟦ro⟧ rinsn⟶₁ro
1-steplρ-E-view-ecsplit cb divout-disjoint dehole dehole
  vset-var () r≐C⟦ro⟧ rinsn⟶₁ro

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  divout-disjoint dehole dehole vmerge
  ρθp≐C⟦rin⟧ ρθr≐C⟦ro⟧ rinsn⟶₁ro
  with ρθp≐C⟦rin⟧ | ρθr≐C⟦ro⟧
... | dcenv p≐C⟦rin⟧ | dcenv r≐C⟦ro⟧  with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ p≐C⟦rin⟧ rinsn⟶₁ro) ,′
   _ , dehole , dehole , rmerge dehole , vmerge

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ris-present {_} {S} S∈ θS≡present dehole} cb
  divout-disjoint dehole dehole vis-present
  (dcpresent₁ p≐C⟦rin⟧) (dcpresent₁ r≐C⟦ro⟧) rinsn⟶₁ro with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ p≐C⟦rin⟧ rinsn⟶₁ro) ,′
   _ , dehole , dehole , ris-present {_} {S} S∈ θS≡present dehole , vis-present

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ris-present {_} {S} S∈ θS≡present dehole} cb
  divout-disjoint dehole dehole vis-present
  (dcpresent₂ p≐C⟦rin⟧) (dcpresent₂ r≐C⟦ro⟧) rinsn⟶₁ro =
  _ , inj₁ refl ,′
  _ , dehole , dehole , ris-present {_} {S} S∈ θS≡present dehole , vis-present

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ris-absent {_} {S} S∈ θS≡absent dehole} cb
  divout-disjoint dehole dehole vis-absent
  (dcpresent₁ p≐C⟦rin⟧) (dcpresent₁ r≐C⟦ro⟧) rinsn⟶₁ro =
  _ , inj₁ refl ,′
  _ , dehole , dehole , ris-absent {_} {S} S∈ θS≡absent dehole , vis-absent

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ris-absent {_} {S} S∈ θS≡absent dehole} cb
  divout-disjoint dehole dehole vis-absent
  (dcpresent₂ p≐C⟦rin⟧) (dcpresent₂ r≐C⟦ro⟧) rinsn⟶₁ro with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ p≐C⟦rin⟧ rinsn⟶₁ro) ,′
   _ , dehole , dehole , ris-absent {_} {S} S∈ θS≡absent dehole , vis-absent

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = rraise-shared {_} {_} {s} _ _} cb
  divout-disjoint dehole dehole vraise-shared
  (dcshared p≐C⟦rin⟧) (dcshared r≐C⟦ro⟧) rinsn⟶₁ro with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ (dcenv p≐C⟦rin⟧) rinsn⟶₁ro) ,′
   _ , dehole , dehole , rraise-shared {_} {_} {s} _ _ , vraise-shared

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = rraise-var {_} {_} {x} _ _} cb
  divout-disjoint dehole dehole vraise-var
  (dcvar p≐C⟦rin⟧) (dcvar r≐C⟦ro⟧) rinsn⟶₁ro with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ (dcenv p≐C⟦rin⟧) rinsn⟶₁ro) ,′
   _ , dehole , dehole , rraise-var {_} {_} {x} _ _ , vraise-var

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = rif-false {x = x} x∈ θx≡zero dehole} cb
  divout-disjoint dehole dehole vif-false
  (dcif₁ p≐C⟦rin⟧) (dcif₁ r≐C⟦ro⟧) rinsn⟶₁ro =
  _ , inj₁ refl ,′
  _ , dehole , dehole , rif-false {x = x} x∈ θx≡zero dehole , vif-false

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = rif-false {x = x} x∈ θx≡zero dehole} cb
  divout-disjoint dehole dehole vif-false
  (dcif₂ p≐C⟦rin⟧) (dcif₂ r≐C⟦ro⟧) rinsn⟶₁ro with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ p≐C⟦rin⟧ rinsn⟶₁ro) ,′
   _ , dehole , dehole , rif-false {x = x} x∈ θx≡zero dehole , vif-false

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = rif-true {θ} {x = x} x∈ θx≡suc dehole} cb
  divout-disjoint dehole dehole vif-true
  (dcif₁ p≐C⟦rin⟧) (dcif₁ r≐C⟦ro⟧) rinsn⟶₁ro with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ p≐C⟦rin⟧ rinsn⟶₁ro) ,′
   _ , dehole , dehole , rif-true {x = x} x∈ θx≡suc dehole , vif-true

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = rif-true {x = x} x∈ θx≡suc dehole} cb
  divout-disjoint dehole dehole vif-true
  (dcif₂ p≐C⟦rin⟧) (dcif₂ r≐C⟦ro⟧) rinsn⟶₁ro =
  _ , inj₁ refl ,′
  _ , dehole , dehole , rif-true {x = x} x∈ θx≡suc dehole , vif-true

1-steplρ-E-view-ecsplit cb divpar-split₁
  (depar₁ p₁≐E⟦qin⟧) (depar₁ q≐E⟦qo⟧) e-view
  (dcpar₂ p≐C⟦rin⟧) (dcpar₂ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho _ _ _ p₁≐E⟦qin⟧ q≐E⟦qo⟧ e-view
... | ρθ·p₁sn⟶₁ρθq·q , e-view' with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ (dcpar₂ p≐C⟦rin⟧) rinsn⟶₁ro) ,′
   _ , _ , _ , wrap-rho ρθ·p₁sn⟶₁ρθq·q _ _ e-view' _ (depar₁ p₁≐E⟦qin⟧) (depar₁ q≐E⟦qo⟧)

1-steplρ-E-view-ecsplit cb divpar-split₂
  (depar₂ p₂≐E⟦qin⟧) (depar₂ q≐E⟦qo⟧) e-view
  (dcpar₁ p≐C⟦rin⟧) (dcpar₁ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho _ _ _ p₂≐E⟦qin⟧ q≐E⟦qo⟧ e-view
... | ρθ·p₂sn⟶₁ρθq·q , e-view' with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ (dcpar₁ p≐C⟦rin⟧) rinsn⟶₁ro) ,′
   _ , _ , _ , wrap-rho ρθ·p₂sn⟶₁ρθq·q _ _ e-view' _ (depar₂ p₂≐E⟦qin⟧) (depar₂ q≐E⟦qo⟧)

1-steplρ-E-view-ecsplit cb divseq-split
  (deseq p₁≐E⟦qin⟧) (deseq q≐E⟦qo⟧) e-view
  (dcseq₂ p≐C⟦rin⟧) (dcseq₂ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho _ _ _ p₁≐E⟦qin⟧ q≐E⟦qo⟧ e-view
... | ρθ·p₁sn⟶₁ρθq·q , e-view' with sym (unplugc r≐C⟦ro⟧)
... | refl
  = _ , inj₂ (rcontext _ (dcseq₂ p≐C⟦rin⟧) rinsn⟶₁ro) ,′
    _ , _ , _ , wrap-rho ρθ·p₁sn⟶₁ρθq·q _ _ e-view' _ (deseq p₁≐E⟦qin⟧) (deseq q≐E⟦qo⟧)

1-steplρ-E-view-ecsplit cb divloopˢ-split
  (deloopˢ p₁≐E⟦qin⟧) (deloopˢ q≐E⟦qo⟧) e-view
  (dcloopˢ₂ p≐C⟦rin⟧) (dcloopˢ₂ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho _ _ _ p₁≐E⟦qin⟧ q≐E⟦qo⟧ e-view
... | ρθ·p₁sn⟶₁ρθq·q , e-view' with sym (unplugc r≐C⟦ro⟧)
... | refl
 = _ , inj₂ (rcontext _ (dcloopˢ₂ p≐C⟦rin⟧) rinsn⟶₁ro) ,′
   _ , _ , _ , wrap-rho ρθ·p₁sn⟶₁ρθq·q _ _ e-view' _ (deloopˢ p₁≐E⟦qin⟧) (deloopˢ q≐E⟦qo⟧)

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBpar cbp cbq _ _ _ _) (divin div)
  (depar₁ p≐E⟦qin⟧) (depar₁ q≐E⟦qo⟧) e-view-E₁
  (dcpar₁ p≐C⟦rin⟧) (dcpar₁ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (depar₁ p≐E⟦qin⟧) (depar₁ q≐E⟦qo⟧) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view)
  with 1-steplρ-E-view-ecsplit cbp div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
... | _ , qsn⟶po? , _ , r≐E'⟦qin⟧ , po≐E'⟦qo⟧ , _ , e-view' =
  _ , map (cong _) (Context1-sn⟶ (ceval (epar₁ _))) qsn⟶po? ,′
  _ , depar₁ r≐E'⟦qin⟧ , depar₁ po≐E'⟦qo⟧ , wrap-rho _ _ _ e-view' _ _ _

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBpar cbp cbq _ _ _ _) (divin div)
  (depar₂ p≐E⟦qin⟧) (depar₂ q≐E⟦qo⟧) e-view-E₁
  (dcpar₂ p≐C⟦rin⟧) (dcpar₂ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (depar₂ p≐E⟦qin⟧) (depar₂ q≐E⟦qo⟧) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view)
  with 1-steplρ-E-view-ecsplit cbq div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
... | _ , qsn⟶po? , _ , r≐E'⟦qin⟧ , po≐E'⟦qo⟧ , _ , e-view' =
  _ , map (cong _) (Context1-sn⟶ (ceval (epar₂ _))) qsn⟶po? ,′
  _ , depar₂ r≐E'⟦qin⟧ , depar₂ po≐E'⟦qo⟧ , wrap-rho _ _ _ e-view' _ _ _

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBseq cbp cbq _) (divin div)
  (deseq p≐E⟦qin⟧) (deseq q≐E⟦qo⟧) e-view-E₁
  (dcseq₁ p≐C⟦rin⟧) (dcseq₁ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (deseq p≐E⟦qin⟧) (deseq q≐E⟦qo⟧) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view)
  with 1-steplρ-E-view-ecsplit cbp div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
... | _ , qsn⟶po? , _ , r≐E'⟦qin⟧ , po≐E'⟦qo⟧ , _ , e-view' =
  _ , map (cong _) (Context1-sn⟶ (ceval (eseq _))) qsn⟶po? ,′
  _ , deseq r≐E'⟦qin⟧ , deseq po≐E'⟦qo⟧ , wrap-rho _ _ _ e-view' _ _ _

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBloopˢ cbp cbq _ _) (divin div)
  (deloopˢ p≐E⟦qin⟧) (deloopˢ q≐E⟦qo⟧) e-view-E₁
  (dcloopˢ₁ p≐C⟦rin⟧) (dcloopˢ₁ r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (deloopˢ p≐E⟦qin⟧) (deloopˢ q≐E⟦qo⟧) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view)
  with 1-steplρ-E-view-ecsplit cbp div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
... | _ , qsn⟶po? , _ , r≐E'⟦qin⟧ , po≐E'⟦qo⟧ , _ , e-view' =
  _ , map (cong _) (Context1-sn⟶ (ceval (eloopˢ _))) qsn⟶po? ,′
  _ , deloopˢ r≐E'⟦qin⟧ , deloopˢ po≐E'⟦qo⟧ , wrap-rho _ _ _ e-view' _ _ _

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBsusp cb' _) (divin div)
  (desuspend p≐E⟦qin⟧) (desuspend q≐E⟦qo⟧) e-view-E₁
  (dcsuspend p≐C⟦rin⟧) (dcsuspend r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (desuspend p≐E⟦qin⟧) (desuspend q≐E⟦qo⟧) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view)
  with 1-steplρ-E-view-ecsplit cb' div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
... | _ , qsn⟶po? , _ , r≐E'⟦qin⟧ , po≐E'⟦qo⟧ , _ , e-view' =
  _ , map (cong _) (Context1-sn⟶ (ceval (esuspend _))) qsn⟶po? ,′
  _ , desuspend r≐E'⟦qin⟧ , desuspend po≐E'⟦qo⟧ , wrap-rho _ _ _ e-view' _ _ _

1-steplρ-E-view-ecsplit {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBtrap cb') (divin div)
  (detrap p≐E⟦qin⟧) (detrap q≐E⟦qo⟧) e-view-E₁
  (dctrap p≐C⟦rin⟧) (dctrap r≐C⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (detrap p≐E⟦qin⟧) (detrap q≐E⟦qo⟧) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view)
  with 1-steplρ-E-view-ecsplit cb' div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
... | _ , qsn⟶po? , _ , r≐E'⟦qin⟧ , po≐E'⟦qo⟧ , _ , e-view' =
  _ , map (cong _) (Context1-sn⟶ (ceval etrap)) qsn⟶po? ,′
  _ , detrap r≐E'⟦qin⟧ , detrap po≐E'⟦qo⟧ , wrap-rho _ _ _ e-view' _ _ _

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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

open import HoTT
open import homotopy.PtdMapSequence
open import homotopy.CofiberSequence
open import groups.Exactness
open import groups.ExactSequence
open import groups.HomSequence
open import cohomology.Theory

module cohomology.Sigma {i} (CT : CohomologyTheory i)
  (n : ℤ) (X : Ptd i) (Y : de⊙ X → Ptd i) where

open CohomologyTheory CT
open import cohomology.PtdMapSequence CT

{- Cⁿ(Σx:X.Y) = Cⁿ(⋁x:X.Y) × Cⁿ(X). The proof is by constructing a
 - splitting exact sequence

       0 → Cⁿ(⋁x:X.Y) → Cⁿ(Σx:X.Y) → Cⁿ(X)

 - by observing that the map [select : x ↦ (x, pt Yₓ)] has a left inverse
 - and satisfies [Cofiber select == ⋁x:X.Y. -}

⊙select : X ⊙→ ⊙Σ X Y
⊙select = (bigwedge-f Y , idp)

⊙Σbwin : ⊙Σ X Y ⊙→ ⊙BigWedge Y
⊙Σbwin = ⊙cfcod' ⊙select

private
  abstract
    cst-C-Σbwin-is-exact : is-exact (cst-hom {G = C n (⊙Susp X)}) (C-fmap n ⊙Σbwin)
    cst-C-Σbwin-is-exact = equiv-preserves-exact
      {φ₁ = cst-hom {G = C n (⊙Susp X)}}
      {ξG = C-fmap n (⊙Susp-to-⊙Cof² ⊙select)} {ξH = idhom _} {ξK = idhom _}
      (comm-sqrᴳ λ x →
        CEl-fmap n (⊙cfcod²' ⊙select) x
          =⟨ ! $ CEl-fmap-idf n $ CEl-fmap n (⊙cfcod²' ⊙select) x ⟩
        CEl-fmap n (⊙idf _) (CEl-fmap n (⊙cfcod²' ⊙select) x)
          =⟨ C-comm-square n (extract-glue-cod²-comm-sqr ⊙select) □$ᴳ x ⟩
        CEl-fmap n ⊙extract-glue (CEl-fmap n (⊙Susp-to-⊙Cof² ⊙select) x)
          =⟨ CEl-fmap-const n (extract-glue-from-BigWedge-is-const Y) _ ⟩
        Cident n _
          =∎)
      (comm-sqrᴳ λ _ → idp)
      (C-isemap n (⊙Susp-to-⊙Cof² ⊙select) (snd (Cof²-equiv-Susp ⊙select ⁻¹)))
      (idf-is-equiv _)
      (idf-is-equiv _)
      (C-exact n ⊙Σbwin)

  χ : C n X →ᴳ C n (⊙Σ X Y)
  χ = C-fmap n (⊙fstᵈ Y)

  abstract
    select-χ-is-idf : ∀ s → CEl-fmap n ⊙select (GroupHom.f χ s) == s
    select-χ-is-idf = CEl-fmap-inverse n ⊙select (⊙fstᵈ Y) λ _ → idp

C-Σ : C n (⊙Σ X Y) ≃ᴳ C n (⊙BigWedge Y) ×ᴳ C n X
C-Σ = Exact.φ-inj-and-ψ-has-rinv-split
  (C-exact n ⊙select) (C-is-abelian n _)
  (Exact.φ-const-implies-ψ-is-inj cst-C-Σbwin-is-exact (λ _ → idp))
  χ select-χ-is-idf

{-
  ⊙Σbwin-over : CF-hom n ⊙Σbwin == ×ᴳ-inl
                [ (λ G → GroupHom (C n (⊙BigWedge Y)) G) ↓ path ]
  ⊙Σbwin-over = SER.φ-over-iso

  ⊙select-over : CF-hom n ⊙select == ×ᴳ-snd {G = C n (⊙BigWedge Y)}
                 [ (λ G → GroupHom G (C n X)) ↓ path ]
  ⊙select-over = SER.ψ-over-iso

  open CofSelect public using (select; ⊙select; ⊙Σbwin)
-}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module _ where

open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection

data D (B : Set) {{b : B}} : Set where
  c : D B

postulate
  B : Set
  instance b : B
  T : D B → Set

macro
  this : Term → Term → TC ⊤
  this thing hole = unify hole thing

test₁ : _
test₁ = c {_} {{b}}

test₂ : D B
test₂ = c {_} {{b}}

test₃ : D B
test₃ = this (c {{b}})


text:
-- {-# OPTIONS -v tc:10 -v tc.inj:100 #-}
-- 2013-02-18 reported by rotsor

module Issue796o where

data U : Set where
  a b : U

data A : Set where
data B : Set where

abstract
  A' B' : Set

  A' = A
  B' = B  -- fails if changed to A.  Should always fail.

[_] : U → Set
[_] a = A'
[_] b = B'

f : ∀ u → [ u ] → U
f u _ = u

postulate x : A'

zzz = f _ x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Categories.Functor.Instance.01-Truncation where

-- (0,1)-trucation of categories as a functor from Cats to Posets.
--
-- This is the right-adjoint of the inclusion functor from Posets to
-- Cats (see Categories.Functor.Adjoint.Instance.01-Truncation)

open import Level using (_⊔_)
open import Function using (flip)
open import Data.Product as Prod using (_,_; _×_)
open import Relation.Binary.OrderMorphism using (_⇒-Poset_)
open import Relation.Binary using (Poset)

open import Categories.Category using (Category; _[_≈_])
open import Categories.Functor hiding (id)
open import Categories.Category using (Category)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.Posets using (Posets)
import Categories.Morphism as Morphism
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; _≃_)

Trunc : ∀ {o ℓ e} → Functor (Cats o ℓ e) (Posets o ℓ ℓ)
Trunc {o} {ℓ} {e} = record
   { F₀           = Trunc₀
   ; F₁           = Trunc₁
   ; identity     = λ {C} → id C , id C
   ; homomorphism = λ {_ _ C} → id C , id C
   ; F-resp-≈     = TruncRespNI
   }
   where
     open Functor

     -- The choice of _≈_ below may seem a bit arbitrary.  The
     -- rationale is as follows:
     --
     -- Since we are defining an Agda stdlib-style poset, we have to
     -- pick an equality on the carrier set, i.e. on objects.  But
     -- objects do not come with an equality in this library (that's
     -- considered evil), so we pick isomorphism.  In a poset, any
     -- pair of morphisms f : X ⇒ Y and g : Y ⇒ X constitute an
     -- isomorphism between X and Y.  Hence the definition of _≈_.

     Trunc₀ : Category o ℓ e → Poset o ℓ ℓ
     Trunc₀ C = record
       { Carrier           = Obj
       ; _≈_               = λ x y → x ⇒ y × y ⇒ x
       ; _≤_               = _⇒_
       ; isPartialOrder    = record
         { isPreorder      = record
           { isEquivalence = record
             { refl        = id , id
             ; sym         = Prod.swap
             ; trans       = Prod.zip (flip _∘_) _∘_
             }
           ; reflexive     = Prod.proj₁
           ; trans         = flip _∘_
           }
         ; antisym         = _,_
         }
       }
       where open Category C

     Trunc₁ : ∀ {C D} → Functor C D → Trunc₀ C ⇒-Poset Trunc₀ D
     Trunc₁ F = record { fun = F₀ F ; monotone = F₁ F }

     TruncRespNI : ∀ {C D : Category o ℓ e} {F G : Functor C D} →
                   F ≃ G → Posets o ℓ ℓ [ Trunc₁ F ≈ Trunc₁ G ]
     TruncRespNI μ {X} = ⇒.η X , ⇐.η X
       where open NaturalIsomorphism μ

     open Category

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Oscar.Level where

open import Agda.Primitive public
  using ()
  renaming (Level to Ł̂; lzero to Ø̂; lsuc to ↑̂_; _⊔_ to _+̂_)

open import Agda.Primitive public
  using ()
  renaming (Level to Ł̂; lzero to lzero; lsuc to lsuc; _⊔_ to _⊔_)

𝑶 : ∀ a → Set (lsuc a)
𝑶 a = Set a

open import Agda.Primitive public
  using ()
  renaming ( Level to Ł
           ; lzero to ∅̂
           ; lsuc to ↑̂_
           ; _⊔_ to _∙̂_ )

infix 0 Ø_
Ø_ : ∀ 𝔬 → Set (↑̂ 𝔬)
Ø_ 𝔬 = Set 𝔬

Ø₀ = Ø ∅̂


text:
module pushdown where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
-- open import Data.Bool using ( Bool ; true ; false )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Level renaming ( suc to succ ; zero to Zero )
-- open import Data.Product
open import logic
open import automaton

data PushDown   (  Γ : Set  ) : Set  where
   pop    : PushDown  Γ
   push   :  Γ → PushDown  Γ
   none   :  PushDown  Γ

record PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
       : Set  where
    field
        pδ : Q → Σ →  Γ → Q ∧ ( PushDown  Γ )
        pok : Q → Bool
        pempty : Γ
    pmoves :  Q → List  Γ  → Σ → ( Q ∧ List  Γ )
    pmoves q [] i with pδ q i pempty
    pmoves q [] i | ⟪ qn , pop ⟫ =  ⟪  qn , [] ⟫
    pmoves q [] i | ⟪ qn , push x ⟫ =  ⟪ qn , ( x ∷  [] )  ⟫
    pmoves q [] i | ⟪ qn , none ⟫ =  ⟪ qn ,  [] ⟫
    pmoves q (  H  ∷ T  ) i with pδ q i H
    pmoves q (H ∷ T) i | ⟪ qn , pop ⟫ =  ⟪ qn , T  ⟫
    pmoves q (H ∷ T) i | ⟪ qn , none ⟫ =  ⟪ qn , (H ∷ T)  ⟫
    pmoves q (H ∷ T) i | ⟪ qn , push x ⟫ =  ⟪ qn ,  x ∷ H ∷ T  ⟫

    paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
    paccept q [] [] = pok q
    paccept q ( H  ∷ T) [] with pδ q H pempty
    paccept q (H ∷ T) [] | ⟪ qn , pop ⟫ = paccept qn T []
    paccept q (H ∷ T) [] | ⟪ qn , none ⟫ = paccept qn T []
    paccept q (H ∷ T) [] | ⟪ qn , push x ⟫ = paccept qn T (x  ∷ [] )
    paccept q [] (_ ∷ _ ) = false
    paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
    ... | ⟪ nq , pop ⟫     = paccept nq T ST
    ... | ⟪ nq , none ⟫    = paccept nq T (SH ∷ ST)
    ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns  ∷  SH ∷ ST )

record PDA ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
       : Set  where
    field
        automaton : Automaton Q Σ
        pδ : Q →  PushDown  Γ
    open Automaton
    paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
    paccept q [] [] = aend automaton q
    paccept q (H  ∷ T) [] with pδ  (δ automaton q H)
    paccept q (H ∷ T) [] | pop     = paccept (δ automaton q H) T []
    paccept q (H ∷ T) [] | none    = paccept (δ automaton q H) T []
    paccept q (H ∷ T) [] | push x  = paccept (δ automaton q H) T (x  ∷ [] )
    paccept q [] (_ ∷ _ ) = false
    paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ (δ automaton q H)
    ... | pop      = paccept (δ automaton q H) T ST
    ... | none     = paccept (δ automaton q H) T (SH ∷ ST)
    ... | push ns  = paccept (δ automaton q H) T ( ns  ∷  SH ∷ ST )

data  States0   : Set  where
   sr : States0

data  In2   : Set  where
   i0 : In2
   i1 : In2

pnn : PushDownAutomaton States0 In2 States0
pnn = record {
         pδ  = pδ
      ;  pempty = sr
      ;  pok = λ q → true
   } where
        pδ  : States0 → In2 → States0 → States0 ∧ PushDown States0
        pδ sr i0 _ = ⟪ sr , push sr ⟫
        pδ sr i1 _ = ⟪ sr , pop  ⟫

data  States2   : Set  where
   ph1 : States2
   ph2 : States2
   phf : States2

pnnp : PDA States2 In2 States2
pnnp = record {
         automaton = record { aend = aend ; δ = δ }
       ; pδ  = pδ
   } where
        δ : States2 → In2 → States2
        δ ph1 i0 = ph1
        δ ph1 i1 = ph2
        δ ph2 i1 = ph2
        δ _ _ = phf
        aend : States2 → Bool
        aend ph2 = true
        aend _ = false
        pδ  : States2 → PushDown States2
        pδ ph1 = push ph1
        pδ ph2 = pop
        pδ phf = none

data  States1   : Set  where
   ss : States1
   st : States1
pn1 : PushDownAutomaton States1 In2 States1
pn1 = record {
         pδ  = pδ
      ;  pempty = ss
      ;  pok = pok1
   } where
        pok1 :  States1 → Bool
        pok1 ss = false
        pok1 st = true
        pδ  : States1 → In2 → States1 → States1 ∧ PushDown States1
        pδ ss i0 _ = ⟪ ss , push ss ⟫
        pδ ss i1 _ = ⟪ st , pop ⟫
        pδ st i0 _ = ⟪ st , push ss ⟫
        pδ st i1 _ = ⟪ st , pop  ⟫

test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
test2 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) []
test3 = PushDownAutomaton.pmoves pnn sr [] i0
test4 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []

test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
-- Compiled things must have a Haskell type given by a COMPILED_TYPE pragma

module CompiledMustHaveHaskellType where

postulate
  N : Set
  foo : N

-- It is necessary add something like
-- {-# COMPILED_TYPE N Int #-}

{-# COMPILED foo bar #-}


text:
module FFI.IO where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String)

open import FFI.Data.HaskellString using (HaskellString; pack ; unpack)

infixl 1 _>>=_
infixl 1 _>>_

postulate
  return : ∀ {a} {A : Set a} → A → IO A
  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
  fmap : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B

{-# COMPILE GHC return = \_ _ -> return    #-}
{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
{-# COMPILE GHC fmap  = \_ _ _ _ -> fmap #-}

postulate getHContents : IO HaskellString
{-# COMPILE GHC getHContents = getContents #-}

postulate putHStrLn : HaskellString → IO ⊤
{-# COMPILE GHC putHStrLn = putStrLn #-}

getContents : IO String
getContents = fmap pack getHContents

putStrLn : String → IO ⊤
putStrLn txt = putHStrLn (unpack txt)

_>>_ : ∀ {a} {A : Set a} → IO ⊤ → IO A → IO A
a >> b = a >>= (λ _ → b )

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by posets
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.Poset
         {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open Relation.Binary.Poset P hiding (trans)
open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
open import Relation.Binary.Properties.Preorder preorder
open import Function using (flip)

-- The inverse relation is also a poset.

invIsPartialOrder : IsPartialOrder _≈_ (flip _≤_)
invIsPartialOrder = record
  { isPreorder   = invIsPreorder
  ; antisym      = flip antisym
  }

invPoset : Poset p₁ p₂ p₃
invPoset = record { isPartialOrder = invIsPartialOrder }

------------------------------------------------------------------------
-- Posets can be turned into strict partial orders

strictPartialOrder : StrictPartialOrder _ _ _
strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
  }

open StrictPartialOrder strictPartialOrder


text:
------------------------------------------------------------------------------
-- The division result is correct
------------------------------------------------------------------------------

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

module FOTC.Program.Division.ResultI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Program.Division.ConversionRulesI
open import FOTC.Program.Division.Division
open import FOTC.Program.Division.Specification

------------------------------------------------------------------------------
-- The division result is correct when the dividend is less than
-- the divisor.

div-x<y-helper : ∀ {i j} → N i → N j → i < j → i ≡ j * div i j + i
div-x<y-helper {i} {j} Ni Nj i<j = sym prf
  where
  prf : j * div i j + i ≡ i
  prf = j * div i j + i ≡⟨ +-leftCong (*-rightCong (div-x<y i<j)) ⟩
        j * zero + i    ≡⟨ +-leftCong (*-rightZero Nj) ⟩
        zero + i        ≡⟨ +-leftIdentity i ⟩
        i               ∎

div-x<y-resultCorrect : ∀ {i j} → N i → N j → i < j →
                        ∃[ r ] N r ∧ r < j ∧ i ≡ j * div i j + r
div-x<y-resultCorrect Ni Nj i<j = _ , Ni , i<j , div-x<y-helper Ni Nj i<j

-- The division result is correct when the dividend is greater or equal
-- than the divisor.
-- Using the inductive hypothesis ih we know that
--
-- i ∸ j = j * (div (i ∸ j) j) + r.

-- From that we get
--
-- i = j * (succ (div (i ∸ j) j)) + r and we know
--
-- div i j = succ (div (i ∸ j) j) therefore we get
--
-- i = j * div i j + r.
postulate helper : ∀ {i j r} → N i → N j → N r →
                   i ∸ j ≡ j * div (i ∸ j) j + r →
                   i ≡ j * succ₁ (div (i ∸ j) j) + r

div-x≮y-helper : ∀ {i j r} → N i → N j → N r →
                 i ≮ j →
                 i ∸ j ≡ j * div (i ∸ j) j + r →
                 i ≡ j * div i j + r
div-x≮y-helper {i} {j} {r} Ni Nj Nr i≮j helperH =
  i                             ≡⟨ helper Ni Nj Nr helperH ⟩
  j * succ₁ (div (i ∸ j) j) + r ≡⟨ prf ⟩
  j * div i j + r               ∎
  where
  prf : j * succ₁ (div (i ∸ j) j) + r ≡ j * div i j + r
  prf = subst (λ x → j * x + r ≡ j * div i j + r)
              (div-x≮y i≮j)
              refl

-- 2012-02-29: We are using the existential witness only for
-- documenting the types in the where clause. They could be removed.
div-x≮y-resultCorrect : ∀ {i j} → N i → N j →
                        (divSpec (i ∸ j) j (div (i ∸ j) j)) →
                        i ≮ j →
                        ∃[ r ] N r ∧ r < j ∧ i ≡ j * div i j + r
div-x≮y-resultCorrect {i} {j} Ni Nj (h₁ , r , r-correct) i≮j =
  r , Nr , r<j , div-x≮y-helper Ni Nj Nr i≮j helperH
  where
  Nr : N r
  Nr = ∧-proj₁ r-correct

  r<j : r < j
  r<j = ∧-proj₁ (∧-proj₂ r-correct)

  helperH : i ∸ j ≡ j * div (i ∸ j) j + r
  helperH = ∧-proj₂ (∧-proj₂ r-correct)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.Definition

module Groups.Abelian.Definition where

record AbelianGroup {a} {b} {A : Set a} {S : Setoid {a} {b} A} {_·_ : A → A → A} (G : Group S _·_) : Set (lsuc a ⊔ b) where
  open Setoid S
  field
    commutative : {a b : A} → (a · b) ∼ (b · a)


text:
{-# OPTIONS --allow-unsolved-metas #-}
-- The option is supplied to force a real error to pass the regression test.
module StronglyRigidOccurrence where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

test : let X : Nat; X = _ in X ≡ suc X
test = refl
-- this gives an error in the occurs checker

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universal lifting of predicates over Vectors
------------------------------------------------------------------------

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

module Data.Vec.Functional.Relation.Unary.All where

open import Data.Fin.Base
open import Data.Fin.Properties
open import Data.Nat.Base
open import Data.Product using (_,_)
open import Data.Vec.Functional as VF hiding (map)
open import Level using (Level)
open import Relation.Unary

private
  variable
    a p q ℓ : Level
    A : Set a

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

All : Pred A ℓ → ∀ {n} → Vector A n → Set ℓ
All P xs = ∀ i → P (xs i)

------------------------------------------------------------------------
-- Operations

module _ {P : Pred A p} {Q : Pred A q} where

  map : P ⊆ Q → ∀ {n} → All P {n = n} ⊆ All Q
  map p⊆q ps i = p⊆q (ps i)

------------------------------------------------------------------------
-- Properties of predicates preserved by All

module _ {P : Pred A p} where

  all : Decidable P → ∀ {n} → Decidable (All P {n = n})
  all p? xs = all? λ i → p? (xs i)

  universal : Universal P → ∀ {n} → Universal (All P {n = n})
  universal uni xs i = uni (xs i)

  satisfiable : Satisfiable P → ∀ {n} → Satisfiable (All P {n = n})
  satisfiable (x , px) = (λ _ → x) , (λ _ → px)


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

open import Calf.CostMonoid
open import Data.Nat using (ℕ)
open import Examples.Sorting.Comparable

module Examples.Sorting.Core
  (costMonoid : CostMonoid) (fromℕ : ℕ → CostMonoid.ℂ costMonoid)
  (M : Comparable costMonoid fromℕ)
  where

open Comparable M

open import Calf costMonoid
open import Calf.Types.List

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s; _+_; _*_; _^_; ⌊_/2⌋; ⌈_/2⌉)
import Data.Nat.Properties as N

open import Data.List.Properties using (++-assoc; length-++) public

open import Data.List.Relation.Binary.Permutation.Propositional public
open import Data.List.Relation.Binary.Permutation.Propositional.Properties
  using (↭-length; ¬x∷xs↭[]; All-resp-↭; Any-resp-↭; drop-∷; ++-identityʳ)
  renaming (++-comm to ++-comm-↭; ++⁺ˡ to ++⁺ˡ-↭; ++⁺ʳ to ++⁺ʳ-↭; ++⁺ to ++⁺-↭) public

open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup) public
open import Data.List.Relation.Unary.All.Properties as AllP using () renaming (++⁺ to ++⁺-All) public
open import Data.List.Relation.Unary.Any using (Any; here; there)

_≥_ : val A → val A → Set
x ≥ y = y ≤ x

_≰_ : val A → val A → Set
x ≰ y = ¬ x ≤ y

≰⇒≥ : _≰_ ⇒ _≥_
≰⇒≥ {x} {y} h with ≤-total x y
... | inj₁ h₁ = contradiction h₁ h
... | inj₂ h₂ = h₂

_≤*_ : val A → val (list A) → Set
_≤*_ x = All (x ≤_)

≤-≤* : ∀ {x₁ x₂ l} → x₁ ≤ x₂ → x₂ ≤* l → x₁ ≤* l
≤-≤* x₁≤x₂ = map (≤-trans x₁≤x₂)

data Sorted : val (list A) → Set where
  [] : Sorted []
  _∷_ : ∀ {y ys} → y ≤* ys → Sorted ys → Sorted (y ∷ ys)

short-sorted : {l : val (list A)} → length l Nat.≤ 1 → Sorted l
short-sorted {[]} _ = []
short-sorted {_ ∷ []} _ = [] ∷ []
short-sorted {_ ∷ _ ∷ _} (s≤s ())

unique-sorted : ∀ {l'₁ l'₂} → Sorted l'₁ → Sorted l'₂ → l'₁ ↭ l'₂ → l'₁ ≡ l'₂
unique-sorted []             []             ↭ = refl
unique-sorted []             (h₂ ∷ sorted₂) ↭ = contradiction (↭-sym ↭) ¬x∷xs↭[]
unique-sorted (h₁ ∷ sorted₁) []             ↭ = contradiction (↭) ¬x∷xs↭[]
unique-sorted (h₁ ∷ sorted₁) (h₂ ∷ sorted₂) ↭ with
  ≤-antisym
    (lookup (≤-refl ∷ h₁) (Any-resp-↭ (↭-sym ↭) (here refl)))
    (lookup (≤-refl ∷ h₂) (Any-resp-↭ (↭) (here refl)))
... | refl = Eq.cong (_ ∷_) (unique-sorted sorted₁ sorted₂ (drop-∷ ↭))

join-sorted : ∀ {l₁ mid l₂} → Sorted l₁ → Sorted l₂ → All (_≤ mid) l₁ → All (mid ≤_) l₂ → Sorted (l₁ ++ [ mid ] ++ l₂)
join-sorted []            sorted₂ all₁        all₂ = all₂ ∷ sorted₂
join-sorted (h ∷ sorted₁) sorted₂ (h' ∷ all₁) all₂ =
  ++⁺-All h (h' ∷ ≤-≤* h' all₂) ∷ (join-sorted sorted₁ sorted₂ all₁ all₂)

++⁻ˡ : ∀ xs {ys} → Sorted (xs ++ ys) → Sorted xs
++⁻ˡ []       sorted       = []
++⁻ˡ (x ∷ xs) (h ∷ sorted) = AllP.++⁻ˡ xs h ∷ (++⁻ˡ xs sorted)

++⁻ʳ : ∀ xs {ys} → Sorted (xs ++ ys) → Sorted ys
++⁻ʳ []       sorted       = sorted
++⁻ʳ (x ∷ xs) (h ∷ sorted) = ++⁻ʳ xs sorted

split-sorted₁ : ∀ xs {x} → Sorted (xs ∷ʳ x) → All (_≤ x) xs
split-sorted₁ []       sorted       = []
split-sorted₁ (x ∷ xs) (h ∷ sorted) = proj₂ (AllP.∷ʳ⁻ h) ∷ split-sorted₁ xs sorted

uncons₁ : ∀ {x xs} → Sorted (x ∷ xs) → x ≤* xs
uncons₁ (h ∷ sorted) = h

uncons₂ : ∀ {x xs} → Sorted (x ∷ xs) → Sorted xs
uncons₂ (h ∷ sorted) = sorted

SortedOf : val (list A) → val (list A) → Set
SortedOf l l' = l ↭ l' × Sorted l'

SortResult : cmp (Π (list A) λ _ → F (list A)) → val (list A) → Set
SortResult sort l = ◯ (∃ λ l' → sort l ≡ ret l' × SortedOf l l')

IsSort : cmp (Π (list A) λ _ → F (list A)) → Set
IsSort sort = ∀ l → SortResult sort l

IsSort⇒≡ : ∀ sort₁ → IsSort sort₁ → ∀ sort₂ → IsSort sort₂ → ◯ (sort₁ ≡ sort₂)
IsSort⇒≡ sort₁ correct₁ sort₂ correct₂ u =
  funext λ l →
    let (l'₁ , ≡₁ , ↭₁ , sorted₁) = correct₁ l u in
    let (l'₂ , ≡₂ , ↭₂ , sorted₂) = correct₂ l u in
    begin
      sort₁ l
    ≡⟨ ≡₁ ⟩
      ret l'₁
    ≡⟨ Eq.cong ret (unique-sorted sorted₁ sorted₂ (trans (↭-sym ↭₁) ↭₂)) ⟩
      ret l'₂
    ≡˘⟨ ≡₂ ⟩
      sort₂ l
    ∎
      where open ≡-Reasoning

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

module Definition.Typed.Consequences.Canonicity where

open import Definition.Untyped

open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Empty
open import Tools.Nat
open import Tools.Product

-- Turns a natural number into its term representation
sucᵏ : Nat → Term
sucᵏ 0 = zero
sucᵏ (1+ n) = suc (sucᵏ n)

-- No neutral terms are well-formed in an empty context

-- we need to postulate consistency
-- as we have several uninhabited propositions, we build an predicate
-- to characterize them

-- Note that we could also have defined reductions to Empty of other
-- forms of unihabited types

data isFalse : Term → Set where
  isEmpty : ∀ {lEmpty} → isFalse (Empty lEmpty)
  isIdℕΠ : ∀ {r A rA B} → isFalse (Id (Univ r ⁰) ℕ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰))
  isIdΠℕ : ∀ {r A rA B} → isFalse (Id (Univ r ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) ℕ)
  isIdΠΠ%! : ∀ {r A B A' B'} → isFalse (Id (Univ r ⁰) (Π A ^ % ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ ! ° ⁰ ▹ B' ° ⁰ ° ⁰))
  isIdΠΠ!% : ∀ {r A B A' B'} → isFalse (Id (Univ r ⁰) (Π A ^ ! ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ % ° ⁰ ▹ B' ° ⁰ ° ⁰))

consistency = ∀ {t A l} → isFalse A → ε ⊢ t ∷ A ^ [ % , l ] → ⊥

noNe : ∀ {t A r} → consistency → ε ⊢ t ∷ A ^ r → Neutral t → ⊥

-- impossible cases thanks to consistency
noNe consistency (Emptyrecⱼ A ⊢e) Emptyrecₙ = consistency isEmpty ⊢e
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) castℕΠₙ = consistency isIdℕΠ [A]₂
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) castΠℕₙ = consistency isIdΠℕ [A]₂
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) castΠΠ%!ₙ = consistency isIdΠΠ%! [A]₂
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) castΠΠ!%ₙ = consistency isIdΠΠ!% [A]₂

-- possible cases proven by induction
noNe consistency (⊢t ∘ⱼ ⊢t₁) (∘ₙ neT) = noNe consistency  ⊢t neT
noNe consistency (natrecⱼ x ⊢t ⊢t₁ ⊢t₂) (natrecₙ neT) = noNe consistency ⊢t₂ neT
noNe consistency (var x₁ ()) (var x)
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (Idₙ neT) = noNe consistency [A] neT
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (Idℕₙ neT) = noNe consistency [A]₁ neT
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (Idℕ0ₙ neT) = noNe consistency [A]₂ neT
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (IdℕSₙ neT) = noNe consistency [A]₂ neT
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (IdUₙ neT) = noNe consistency [A]₁ neT
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (IdUℕₙ neT) = noNe consistency [A]₂ neT
noNe consistency (Idⱼ [A] [A]₁ [A]₂) (IdUΠₙ neT) = noNe consistency [A]₂ neT
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) (castₙ neT) = noNe consistency [A] neT
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) (castℕₙ neT) = noNe consistency [A]₁ neT
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) (castΠₙ neT) = noNe consistency [A]₁ neT
noNe consistency (castⱼ [A] [A]₁ [A]₂ [A]₃) (castℕℕₙ neT) = noNe consistency [A]₃ neT
noNe consistency (conv ⊢t x) (var n) = noNe consistency ⊢t (var n)
noNe consistency (conv ⊢t x) (∘ₙ neT) = noNe consistency ⊢t (∘ₙ neT)
noNe consistency (conv ⊢t x) (natrecₙ neT) = noNe consistency ⊢t (natrecₙ neT)
noNe consistency (conv ⊢t x) (Idₙ neT) = noNe consistency ⊢t (Idₙ neT)
noNe consistency (conv ⊢t x) (Idℕₙ neT) = noNe consistency ⊢t (Idℕₙ neT)
noNe consistency (conv ⊢t x) (Idℕ0ₙ neT) = noNe consistency ⊢t (Idℕ0ₙ neT)
noNe consistency (conv ⊢t x) (IdℕSₙ neT) = noNe consistency ⊢t (IdℕSₙ neT)
noNe consistency (conv ⊢t x) (IdUₙ neT) = noNe consistency ⊢t (IdUₙ neT)
noNe consistency (conv ⊢t x) (IdUℕₙ neT) = noNe consistency ⊢t (IdUℕₙ neT)
noNe consistency (conv ⊢t x) (IdUΠₙ neT) = noNe consistency ⊢t (IdUΠₙ neT)
noNe consistency (conv ⊢t x) (castₙ neT) = noNe consistency ⊢t (castₙ neT)
noNe consistency (conv ⊢t x) (castℕₙ neT) = noNe consistency ⊢t (castℕₙ neT)
noNe consistency (conv ⊢t x) (castΠₙ neT) = noNe consistency ⊢t (castΠₙ neT)
noNe consistency (conv ⊢t x) (castℕℕₙ neT) = noNe consistency ⊢t (castℕℕₙ neT)
noNe consistency (conv ⊢t x) castℕΠₙ = noNe consistency ⊢t castℕΠₙ
noNe consistency (conv ⊢t x) castΠℕₙ = noNe consistency ⊢t castΠℕₙ
noNe consistency (conv ⊢t x) castΠΠ%!ₙ = noNe consistency ⊢t castΠΠ%!ₙ
noNe consistency (conv ⊢t x) castΠΠ!%ₙ = noNe consistency ⊢t castΠΠ!%ₙ
noNe consistency (conv ⊢t x) Emptyrecₙ = noNe consistency ⊢t Emptyrecₙ

-- Helper function for canonicity for reducible natural properties
canonicity″ : ∀ {t}
              → consistency
              → Natural-prop ε t
              → ∃ λ k → ε ⊢ t ≡ sucᵏ k ∷ ℕ ^ [ ! , ι ⁰ ]
canonicity″ consistency (sucᵣ (ℕₜ n₁ d n≡n prop)) =
  let a , b = canonicity″ consistency prop
  in  1+ a , suc-cong (trans (subset*Term (redₜ d)) b)
canonicity″ consistency zeroᵣ = 0 , refl (zeroⱼ ε)
canonicity″ consistency (ne (neNfₜ neK ⊢k k≡k)) = ⊥-elim (noNe consistency ⊢k neK)

-- Helper function for canonicity for specific reducible natural numbers
canonicity′ : ∀ {t l}
             → consistency
             → ([ℕ] : ε ⊩⟨ l ⟩ℕ ℕ)
             → ε ⊩⟨ l ⟩ t ∷ ℕ ^ [ ! , ι ⁰ ] / ℕ-intr [ℕ]
             → ∃ λ k → ε ⊢ t ≡ sucᵏ k ∷ ℕ ^ [ ! , ι ⁰ ]
canonicity′ consistency (noemb [ℕ]) (ℕₜ n d n≡n prop) = let a , b = canonicity″ consistency prop
                                          in  a , trans (subset*Term (redₜ d)) b
canonicity′ consistency (emb emb< [ℕ]) [t] = canonicity′ consistency [ℕ] [t]
canonicity′ consistency (emb ∞< [ℕ]) [t] = canonicity′ consistency [ℕ] [t]

-- Canonicity of natural numbers
canonicity : ∀ {t} →
             consistency →
             ε ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ] →
             ∃ λ k → ε ⊢ t ≡ sucᵏ k ∷ ℕ ^ [ ! , ι ⁰ ]
canonicity consistency ⊢t with reducibleTerm ⊢t
canonicity consistency ⊢t | [ℕ] , [t] =
  canonicity′ consistency (ℕ-elim [ℕ]) (irrelevanceTerm [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [t])


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

module Data.Binary.PerformanceTests.Addition where

open import Prelude
open import Data.Binary.Definition
open import Data.Binary.Addition using (_+_)

sum-r : 𝔹 → ℕ → 𝔹
sum-r′ : 𝔹 → ℕ → 𝔹

sum-r′ x zero    = x
sum-r′ x (suc n) = x + sum-r (2ᵇ x) n

sum-r x zero    = x
sum-r x (suc n) = x + sum-r′ (1ᵇ x) n

sum-l : 𝔹 → ℕ → 𝔹
sum-l′ : 𝔹 → ℕ → 𝔹

sum-l′ x zero    = x
sum-l′ x (suc n) = sum-l (2ᵇ x) n + x

sum-l x zero    = x
sum-l x (suc n) = sum-l′ (1ᵇ x) n + x

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

f : 𝔹
f = one-thousand

n : ℕ
n = 1000

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

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Issue2469 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.IO renaming (IO to BIO)
open import Agda.Builtin.String
open import Agda.Builtin.IO
open import Common.IO
open import Common.Prelude
open import Common.Sum
open import Common.Product

data F : Nat → Set where
  [] : F zero
  _∷1 : ∀ {n} → F n → F (suc n)
  _∷2 : ∀ {n} → F n → F (suc (suc n))

f : ∀ k → F (suc k) → F k ⊎ Maybe ⊥
f zero a = inj₂ nothing
f k (xs ∷1) = inj₂ nothing
-- to (suc k) xs = inj₂ nothing  -- This is fine
f (suc k) = λ xs → inj₂ nothing  -- This segfaults

myshow : F 1 ⊎ Maybe ⊥ → String
-- myshow (inj₁ b) = ""        -- This is fine
myshow (inj₁ (b ∷1)) = "bla"      -- This segfaults
myshow _ = "blub"

main : IO ⊤
main =  putStrLn (myshow (f 1 ([] ∷2)))


text:
{-# OPTIONS --type-in-type #-} -- enables cheating
                               -- 2:10 : why

-- https://www.youtube.com/watch?v=2LxtHeZlaVw

module HC-Lec3 where

open import HC-Lec1
open import HC-Lec2

postulate
  -- equal inputs go to equal outputs
  -- (whereas structural equality would require equal implementations)
  extensionality : {S : Set} {T : S -> Set}
                -- 24:00 : make f and g implicit : https://www.youtube.com/watch?v=RCRddhYegzI
                -> {f g : (x : S) -> T x}
                -> ((x : S) -> f x == g x)
                ->             f   == g

-- 2:45

record Category : Set where
  field
    -- things
    Obj  : Set
    _~>_ : Obj -> Obj -> Set

    -- operations
    id~>  : {T     : Obj} -> T ~> T
    _>~>_ : {R S T : Obj} -> R ~> S -> S ~> T -> R ~> T

    -- laws
    law-id~>>~> : {S T : Obj} -> (f : S ~> T) -> (id~> >~> f)    == f
    law->~>id~> : {S T : Obj} -> (f : S ~> T) -> (f    >~> id~>) == f
    law->~>>~>  : {Q R S T : Obj}
               -> (f : Q ~> R) -> (g : R ~> S) -> (h : S ~> T)
               -> ((f >~> g) >~> h) == (f >~> (g >~> h))

-- 7:50

SET : Category
SET = record
        { Obj         = Set
        ; _~>_        = λ S T -> S -> T
        ; id~>        = id
        ; _>~>_       = _>>_
        ; law-id~>>~> = refl
        ; law->~>id~> = refl
        ; law->~>>~>  = λ f g h → refl (λ x → h (g (f x)))
        }

-- 11:50
-- A PREORDER is a category where there is at most one arrow between any two objects.
-- Therefore arrows are unique.

-- all proofs of '>=' are equivalent
unique->= : (m n : Nat) (p q : m >= n) -> p == q
unique->=      m   zero   p q = refl <>
unique->= (suc m) (suc n) p q = unique->= m n p q

NAT->= : Category
NAT->= = record
           { Obj         = Nat
           ; _~>_        = _>=_
           ; id~>        = λ {n : Nat} → refl->= n
           ; _>~>_       = λ {r s t : Nat} r>=s s>=t → trans->= r s t r>=s s>=t
           ; law-id~>>~> = λ {m n : Nat} f → unique->= m n (trans->= m m n (refl->= m) f) f
           ; law->~>id~> = λ {m n : Nat} f → unique->= m n (trans->= m n n f (refl->= n)) f
           ; law->~>>~>  = λ {q r s t : Nat} q>=r r>=s s>=t →
                            unique->= q t
                              (trans->= q s t (trans->= q r s q>=r r>=s) s>=t)
                              (trans->= q r t  q>=r (trans->= r s t r>=s s>=t))
           }

-- 22:07

-- A MONOID is a category with Obj = One.
-- The values in the monoid are the *arrows*.
-- Only one object, so arrows are the ways to get from Nat to Nat.
ONE-Nat : Category
ONE-Nat = record
            { Obj         = One
            ; _~>_        = λ _ _ -> Nat
            ; id~>        = zero
            ; _>~>_       = _+N_
            ; law-id~>>~> = refl
            ; law->~>id~> = +N-zero
            ; law->~>>~>  = assocLR-+N
            }

-- 26:05

-- Note : this is controversial : because this notion of equality is structural.
-- But equality could be defined by isomorphism instead.
-- - In this case, there could be multiple ways for something to be equal to itself.
-- - equality on Bool : True to True  and False to False
--                  or  True to False and False to True

-- structural equality is unique
eqUnique : {X : Set} {x y : X} -> (p q : x == y) -> p == q
eqUnique (refl x) (refl _) = refl (refl x)

eqUnique' : {X : Set} {x y : X} -> (p q : x == y) -> p == q
eqUnique' {_} {_} {y} p q rewrite q | p = refl (refl y)

DISCRETE : (X : Set) -> Category
DISCRETE X = record
               { Obj         = X
               ; _~>_        = _==_
               ; id~>        = λ {x} -> refl x
               ; _>~>_       = λ {(refl x) (refl .x) → refl x}
               ; law-id~>>~> = λ f     → eqUnique _ f
               ; law->~>id~> = λ f     → eqUnique _ f
               ; law->~>>~>  = λ f g h → eqUnique _ _
               }

-- 40:50

module FUNCTOR where
  open Category

  record _=>_ (C D : Category) : Set where -- functor from C to D
    field
      -- operations
      F-Obj : Obj C -> Obj D
      F-map : {S T : Obj C} -> _~>_ C S T -> _~>_ D (F-Obj S) (F-Obj T)

      -- laws
      F-map-id~> : {T : Obj C} -> F-map (id~> C {T}) == id~> D {F-Obj T}
      F-map->~>  : {R S T : Obj C} (f : _~>_ C R S) (g : _~>_ C S T)
                -> F-map (_>~>_ C f g) == _>~>_ D (F-map f) (F-map g)
open FUNCTOR

-- https://www.youtube.com/watch?v=RCRddhYegzI

-- 4:10

vMap : {n : Nat} {S T : Set} -> (S -> T) -> Vec S n -> Vec T n
vMap f       []  = []
vMap f (x :: xs) = f x :: vMap f xs

vMap-id : {n : Nat} {X : Set} (xs : Vec X n) -> vMap id xs == id xs
vMap-id       []  = refl []
vMap-id (x :: xs)
  rewrite vMap-id xs
  = refl (x :: xs)

vMapCp : {n : Nat} {R S T : Set} {r->s : R -> S} {s->t : S -> T}
      -> (xs : Vec R n)
      -> vMap (r->s >> s->t) xs == vMap s->t (vMap r->s xs)
vMapCp []  = refl []
vMapCp {r->s = r->s} {s->t = s->t} (r :: rs)
  with vMapCp {r->s = r->s} {s->t = s->t} rs
...| xxx
  rewrite xxx
   = refl (s->t (r->s r) :: vMap s->t (vMap r->s rs))

-- vector as a functor
VEC : Nat -> SET => SET
VEC n = record
          { F-Obj      = λ X -> Vec X n
          ; F-map      = vMap
          ; F-map-id~> = extensionality vMap-id
          ; F-map->~>  = λ {R S T : Set} (r->s : R → S) (s->t : S → T)
                         → extensionality vMapCp
          }

-- 15:20

vTakeCp : {X : Set} {m n p : Nat}
       -> (m>=n : m >= n) -> (n>=p : n >= p) -> (xs : Vec X m)
       -> vTake m p (trans->= m n p m>=n n>=p)                 xs
       == vTake n p                      n>=p  (vTake m n m>=n xs)
vTakeCp {_}     {m}     {n}  {zero} m>=n n>=p _ = refl []
vTakeCp {_} {suc m} {suc n} {suc p} m>=n n>=p (x :: xs)
  rewrite vTakeCp {_} {m} {n} {p} m>=n n>=p xs
  = refl (x :: vTake n p n>=p (vTake m n m>=n xs))

-- another way to think of vector as a functor
VTAKE : Set -> NAT->= => SET
VTAKE X = record
            { F-Obj      = Vec X  -- something that turns a number into a SET
            ; F-map      = λ {m} {n} m>=n xs -> vTake m n m>=n xs
            ; F-map-id~> = extensionality (vTakeIdFact _)
            ; F-map->~>  = λ r>=s s>=t → extensionality (vTakeCp r>=s s>=t)
            }

-- 24:53

ADD : Nat -> NAT->= => NAT->=
ADD d = record
          { F-Obj = (d +N_) -- function that adds d to another number
          ; F-map = λ {s} {t} -> f-map' d s t
          -- two proofs of >= are equal to each other
          ; F-map-id~> = λ {T : Nat} -> unique->= (d +N T)
                                                  (d +N T)
                                                  (f-map' d T T (refl->= T))
                                                  (refl->= (d +N T))
          ; F-map->~> = λ {R} {S} {T}f g →
                                       unique->= (d +N R)
                                                 (d +N T)
                                                 (f-map' d R T (trans->= R S T f g))
                                                 (trans->= (d +N R) (d +N S) (d +N T)
                                                           (f-map' d R S f)
                                                           (f-map' d S T g))
          }
 where
  f-map' : ∀ d s t
         → (NAT->= Category.~>       s)        t
         → (NAT->= Category.~> (d +N s)) (d +N t)
  f-map'  zero   s t s>=t =              s>=t
  f-map' (suc d) s t s>=t = f-map' d s t s>=t

-- 41:00

CATEGORY : Category
CATEGORY = record
             { Obj         = Category
             ; _~>_        = _=>_
             ; id~>        = λ {T} -> record
                                        { F-Obj      = id
                                        ; F-map      = id
                                        ; F-map-id~> = refl (Category.id~> T)
                                        ; F-map->~>  = λ f g → refl ((T Category.>~> f) g)
                                        }
             ; _>~>_       = λ r=>s s=>t → record
                                             { F-Obj      = F-Obj r=>s >> F-Obj s=>t
                                             ; F-map      = F-map r=>s >> F-map s=>t
                                             ; F-map-id~> = {!!}
                                             ; F-map->~>  = λ f g → {!!}
                                             }
             ; law-id~>>~> = {!!}
             ; law->~>id~> = {!!}
             ; law->~>>~>  = {!!}
             }
             where open _=>_

-- 45:35
-- Category where Obj are FUNCTORS

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

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

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


text:
{- 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
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Util

-- This module provides some scaffolding to define the handlers for our fake/simple
-- "implementation" and connect them to the interface of the SystemModel.

module LibraBFT.Impl.Handle
  (hash    : BitString → Hash)
  (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)
  where
 open import LibraBFT.Impl.Consensus.ChainedBFT.EventProcessor hash hash-cr
 open RWST-do

 -- This represents an uninitialised EventProcessor, about which we know nothing, which we use as
 -- the initial EventProcessor for every peer until it is initialised.
 postulate
   fakeEP : EventProcessor

 -- Eventually, the initialization should establish some properties we care about, but for now we
 -- just initialise again to fakeEP, which means we cannot prove the base case for various
 -- properties, e.g., in Impl.Properties.VotesOnce
 initialEventProcessorAndMessages
     : (a : Author) → EpochConfig → EventProcessor
     → EventProcessor × List NetworkMsg
 initialEventProcessorAndMessages a _ _ = fakeEP , []

 handle : NodeId → NetworkMsg → Instant → LBFT Unit
 handle _self msg now
    with msg
 ...| P p = processProposalMsg now p
 ...| V v = processVote now v
 ...| C c = return unit            -- We don't do anything with commit messages, they are just for defining Correctness.

 -- For now, the SystemModel supports only one kind of action: to send a Message.  Later it might
 -- include things like logging, crashes, assertion failures, etc.  At that point, definitions like
 -- the following might become part of the SystemModel, but they are included here to enable the
 -- temporary scaffolding below.

 data Action (Msg : Set) : Set where
   send : Msg → Action Msg

 action-send-injective : ∀ {Msg}{m m' : Msg} → send m ≡ send m' → m ≡ m'
 action-send-injective refl = refl

 msgToSend : {Msg : Set} → Action Msg → Msg
 msgToSend (send m) = m

 msgToSend≡ : ∀ {Msg x}{m : Msg} → m ≡ msgToSend x → send m ≡ x
 msgToSend≡ {_} {send m} {m} refl = refl

 -- Note: the SystemModel allows anyone to receive any message sent, so intended recipient is ignored;
 -- it is included in the model only to facilitate future work on liveness properties, when we will need
 -- assumptions about message delivery between honest peers.
 outputToActions : EventProcessor → Output → List (Action NetworkMsg)
 outputToActions ep (BroadcastProposal p) = List-map (const (Action.send (P p)))
                                                     (List-map proj₁
                                                               (kvm-toList (:vvAddressToValidatorInfo (₋epValidators (₋epEC ep)))))
 outputToActions _  (LogErr x)            = []
 outputToActions _  (SendVote v toList)   = List-map (const (Action.send (V v))) toList

 outputsToActions : ∀ {State} → List Output → List (Action NetworkMsg)
 outputsToActions {st} = concat ∘ List-map (outputToActions st)

 runHandler : EventProcessor → LBFT Unit → EventProcessor × List (Action NetworkMsg)
 runHandler st handler = ×-map₂ (outputsToActions {st}) (proj₂ (LBFT-run handler st))

 -- And ultimately, the all-knowing system layer only cares about the
 -- step function.
 peerStep : NodeId → NetworkMsg → Instant → EventProcessor → EventProcessor × List (Action NetworkMsg)
 peerStep nid msg ts st = runHandler st (handle nid msg ts)

 -- This (temporary) wrapper bridges the gap between our (draft) concrete handler and
 -- the form required by the new system model, which does not (yet) support actions other
 -- than send.
 peerStepWrapper : NodeId → NetworkMsg → EventProcessor → EventProcessor × List NetworkMsg
 peerStepWrapper nid msg st = ×-map₂ (List-map msgToSend) (peerStep nid msg 0 st)

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:
data ⊤ : Set where
  tt : ⊤

f : ⊤ → ⊤
f tt = tt

foo : ⊤ → ⊤
foo t with f t
... | x with f t
... | y with f t
... | z = {!z!}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module InequalityReasoningExercise where

open import EqualityAux

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero}  = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n       _         = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

module ≤-Reasoning where

  infix  1 ≤-begin_
  infixr 2 _≤⟨⟩_ _≤⟨_⟩_ _≤-≡⟨_⟩_
  infix  3 _≤-∎

  ≤-begin_ : ∀ {x y : ℕ}
    → x ≤ y
      -----
    → x ≤ y
  ≤-begin x≤y = x≤y

  _≤⟨⟩_ : ∀ (x : ℕ) {y : ℕ}
    → x ≤ y
      -----
    → x ≤ y
  x ≤⟨⟩ x≤y = x≤y

  _≤⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ}
    → x ≤ y
    → y ≤ z
      -----
    → x ≤ z
  x ≤⟨ x≤y ⟩ y≤z = ≤-trans x≤y y≤z

  _≤-≡⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ}
    → x ≡ y
    → y ≤ z
      -----
    → x ≤ z
  x ≤-≡⟨ refl ⟩ y≤z = ≤-trans ≤-refl y≤z

  _≤-∎ : ∀ (x : ℕ)
      -----
    → x ≤ x
  x ≤-∎ = ≤-refl

open ≤-Reasoning

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero p q p≤q =
  ≤-begin
    zero + p
  ≤⟨⟩
    p
  ≤⟨ p≤q ⟩
    q
  ≤⟨⟩
    zero + q
  ≤-∎

+-monoʳ-≤ (suc n) p q p≤q =
  ≤-begin
    (suc n) + p
  ≤⟨⟩
    suc (n + p)
  ≤⟨ s≤s (+-monoʳ-≤ n p q p≤q) ⟩
    suc (n + q)
  ≤⟨⟩
    (suc n) + q
  ≤-∎

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n =
  ≤-begin
    m + p
  ≤-≡⟨ +-comm m p ⟩
    p + m
  ≤⟨ +-monoʳ-≤ p m n m≤n ⟩
    p + n
  ≤-≡⟨ +-comm p n ⟩
    n + p
  ≤-∎

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q =
  ≤-begin
    m + p
  ≤⟨ +-monoˡ-≤ m n p m≤n ⟩
    n + p
  ≤⟨ +-monoʳ-≤ n p q p≤q ⟩
    n + q
  ≤-∎


text:
------------------------------------------------------------------------------
-- Terminating mirror function
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Mirror.MirrorListTerminatingSL where

open import Data.List

------------------------------------------------------------------------------
-- The rose tree type.
data Tree (A : Set) : Set where
  tree : A → List (Tree A) → Tree A

------------------------------------------------------------------------------
-- An alternative and terminating definition of mirror. Adapted from
-- http://stackoverflow.com/questions/9146928/termination-of-structural-induction

-- The mirror function.
mirror       : {A : Set} → Tree A → Tree A
mirrorBranch : {A : Set} → List (Tree A) → List (Tree A)

mirror       (tree a ts) = tree a (reverse (mirrorBranch ts))
mirrorBranch []          = []
mirrorBranch (t ∷ ts)    = mirror t ∷ mirrorBranch ts


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Application {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening using (id)
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Helper function for application of specific type derivations.
-- unsightly code duplication because of my hack for shapeview
-- can't be bothered to fix for now...
appTerm′ : ∀ {F G t u Γ l l′ l″}
          ([F] : Γ ⊩⟨ l″ ⟩ F)
          ([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
          ([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
          ([t] : Γ ⊩⟨ l ⟩ t ∷ Π F ▹ G / Π-intr [ΠFG])
          ([u] : Γ ⊩⟨ l″ ⟩ u ∷ F / [F])
        → Γ ⊩⟨ l′ ⟩ t ∘ u ∷ G [ u ] / [G[u]]
appTerm′ {t = t} {Γ = Γ} [F] [G[u]] (noemb (Πᵣ F G D ⊢F ⊢G A≡A [F′] [G′] G-ext))
         (Πₜ f d funcF f≡f [f] [f]₁) [u] =
  let ΠFG≡ΠF′G′ = whnfRed* (red D) Πₙ
      F≡F′ , G≡G′ = Π-PE-injectivity ΠFG≡ΠF′G′
      F≡idF′ = PE.trans F≡F′ (PE.sym (wk-id _))
      idG′ᵤ≡Gᵤ = PE.cong (λ x → x [ _ ]) (PE.trans (wk-lift-id _) (PE.sym G≡G′))
      idf∘u≡f∘u = (PE.cong (λ x → x ∘ _) (wk-id _))
      ⊢Γ = wf ⊢F
      [u]′ = irrelevanceTerm′ F≡idF′ [F] ([F′] id ⊢Γ) [u]
      [f∘u] = irrelevanceTerm″ idG′ᵤ≡Gᵤ idf∘u≡f∘u
                                ([G′] id ⊢Γ [u]′) [G[u]] ([f]₁ id ⊢Γ [u]′)
      ⊢u = escapeTerm [F] [u]
      d′ = PE.subst (λ x → Γ ⊢ t ⇒* f ∷ x) (PE.sym ΠFG≡ΠF′G′) (redₜ d)
  in  proj₁ (redSubst*Term (app-subst* d′ ⊢u) [G[u]] [f∘u])
appTerm′ [F] [G[u]] (emb 0<1 x) (ιx [t]) [u] = appTerm′ [F] [G[u]] x [t] [u]

-- Application of reducible terms.
appTerm : ∀ {F G t u Γ l l′ l″}
          ([F] : Γ ⊩⟨ l″ ⟩ F)
          ([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
          ([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
          ([t] : Γ ⊩⟨ l ⟩ t ∷ Π F ▹ G / [ΠFG])
          ([u] : Γ ⊩⟨ l″ ⟩ u ∷ F / [F])
        → Γ ⊩⟨ l′ ⟩ t ∘ u ∷ G [ u ] / [G[u]]
appTerm [F] [G[u]] [ΠFG] [t] [u] =
  let [t]′ = irrelevanceTerm [ΠFG] (Π-intr (Π-elim [ΠFG])) [t]
  in  appTerm′ [F] [G[u]] (Π-elim [ΠFG]) [t]′ [u]

-- Helper function for application congurence of specific type derivations.
app-congTerm′ : ∀ {F G t t′ u u′ Γ l l′}
          ([F] : Γ ⊩⟨ l′ ⟩ F)
          ([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
          ([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
          ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Π F ▹ G / Π-intr [ΠFG])
          ([u] : Γ ⊩⟨ l′ ⟩ u ∷ F / [F])
          ([u′] : Γ ⊩⟨ l′ ⟩ u′ ∷ F / [F])
          ([u≡u′] : Γ ⊩⟨ l′ ⟩ u ≡ u′ ∷ F / [F])
        → Γ ⊩⟨ l′ ⟩ t ∘ u ≡ t′ ∘ u′ ∷ G [ u ] / [G[u]]
app-congTerm′ {F′} {G′} {t = t} {t′ = t′} {Γ = Γ}
              [F] [G[u]] (noemb (Πᵣ F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext))
              (Πₜ₌ f g [ ⊢t , ⊢f , d ] [ ⊢t′ , ⊢g , d′ ] funcF funcG t≡u
                   (Πₜ f′ [ _ , ⊢f′ , d″ ] funcF′ f≡f [f] [f]₁)
                   (Πₜ g′ [ _ , ⊢g′ , d‴ ] funcG′ g≡g [g] [g]₁) [t≡u])
              [a] [a′] [a≡a′] =
  let [ΠFG] = Πᵣ′ F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext
      ΠFG≡ΠF′G′ = whnfRed* (red D) Πₙ
      F≡F′ , G≡G′ = Π-PE-injectivity ΠFG≡ΠF′G′
      f≡f′ = whrDet*Term (d , functionWhnf funcF) (d″ , functionWhnf funcF′)
      g≡g′ = whrDet*Term (d′ , functionWhnf funcG) (d‴ , functionWhnf funcG′)
      F≡wkidF′ = PE.trans F≡F′ (PE.sym (wk-id _))
      t∘x≡wkidt∘x : {a b : Term} → wk id a ∘ b PE.≡ a ∘ b
      t∘x≡wkidt∘x {a} {b} = PE.cong (λ x → x ∘ b) (wk-id a)
      t∘x≡wkidt∘x′ : {a : Term} → wk id g′ ∘ a PE.≡ g ∘ a
      t∘x≡wkidt∘x′ {a} = PE.cong (λ x → x ∘ a) (PE.trans (wk-id _) (PE.sym g≡g′))
      wkidG₁[u]≡G[u] = PE.cong (λ x → x [ _ ])
                               (PE.trans (wk-lift-id _) (PE.sym G≡G′))
      wkidG₁[u′]≡G[u′] = PE.cong (λ x → x [ _ ])
                                 (PE.trans (wk-lift-id _) (PE.sym G≡G′))
      ⊢Γ = wf ⊢F
      [u]′ = irrelevanceTerm′ F≡wkidF′ [F] ([F]₁ id ⊢Γ) [a]
      [u′]′ = irrelevanceTerm′ F≡wkidF′ [F] ([F]₁ id ⊢Γ) [a′]
      [u≡u′]′ = irrelevanceEqTerm′ F≡wkidF′ [F] ([F]₁ id ⊢Γ) [a≡a′]
      [G[u′]] = irrelevance′ wkidG₁[u′]≡G[u′] ([G] id ⊢Γ [u′]′)
      [G[u≡u′]] = irrelevanceEq″ wkidG₁[u]≡G[u] wkidG₁[u′]≡G[u′]
                                  ([G] id ⊢Γ [u]′) [G[u]]
                                  (G-ext id ⊢Γ [u]′ [u′]′ [u≡u′]′)
      [f′] : Γ ⊩⟨ _ ⟩ f′ ∷ Π F′ ▹ G′ / [ΠFG]
      [f′] = Πₜ f′ (idRedTerm:*: ⊢f′) funcF′ f≡f [f] [f]₁
      [g′] : Γ ⊩⟨ _ ⟩ g′ ∷ Π F′ ▹ G′ / [ΠFG]
      [g′] = Πₜ g′ (idRedTerm:*: ⊢g′) funcG′ g≡g [g] [g]₁
      [f∘u] = appTerm [F] [G[u]] [ΠFG]
                      (irrelevanceTerm″ PE.refl (PE.sym f≡f′) [ΠFG] [ΠFG] [f′])
                      [a]
      [g∘u′] = appTerm [F] [G[u′]] [ΠFG]
                       (irrelevanceTerm″ PE.refl (PE.sym g≡g′) [ΠFG] [ΠFG] [g′])
                       [a′]
      [tu≡t′u] = irrelevanceEqTerm″ t∘x≡wkidt∘x t∘x≡wkidt∘x wkidG₁[u]≡G[u]
                                     ([G] id ⊢Γ [u]′) [G[u]]
                                     ([t≡u] id ⊢Γ [u]′)
      [t′u≡t′u′] = irrelevanceEqTerm″ t∘x≡wkidt∘x′ t∘x≡wkidt∘x′ wkidG₁[u]≡G[u]
                                       ([G] id ⊢Γ [u]′) [G[u]]
                                       ([g] id ⊢Γ [u]′ [u′]′ [u≡u′]′)
      d₁ = PE.subst (λ x → Γ ⊢ t ⇒* f ∷ x) (PE.sym ΠFG≡ΠF′G′) d
      d₂ = PE.subst (λ x → Γ ⊢ t′ ⇒* g ∷ x) (PE.sym ΠFG≡ΠF′G′) d′
      [tu≡fu] = proj₂ (redSubst*Term (app-subst* d₁ (escapeTerm [F] [a]))
                                     [G[u]] [f∘u])
      [gu′≡t′u′] = convEqTerm₂ [G[u]] [G[u′]] [G[u≡u′]]
                     (symEqTerm [G[u′]]
                       (proj₂ (redSubst*Term (app-subst* d₂ (escapeTerm [F] [a′]))
                                             [G[u′]] [g∘u′])))
  in  transEqTerm [G[u]] (transEqTerm [G[u]] [tu≡fu] [tu≡t′u])
                         (transEqTerm [G[u]] [t′u≡t′u′] [gu′≡t′u′])
app-congTerm′ [F] [G[u]] (emb 0<1 x) (ιx [t≡t′]) [u] [u′] [u≡u′] =
  app-congTerm′ [F] [G[u]] x [t≡t′] [u] [u′] [u≡u′]

-- Application congurence of reducible terms.
app-congTerm : ∀ {F G t t′ u u′ Γ l l′}
          ([F] : Γ ⊩⟨ l′ ⟩ F)
          ([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
          ([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
          ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Π F ▹ G / [ΠFG])
          ([u] : Γ ⊩⟨ l′ ⟩ u ∷ F / [F])
          ([u′] : Γ ⊩⟨ l′ ⟩ u′ ∷ F / [F])
          ([u≡u′] : Γ ⊩⟨ l′ ⟩ u ≡ u′ ∷ F / [F])
        → Γ ⊩⟨ l′ ⟩ t ∘ u ≡ t′ ∘ u′ ∷ G [ u ] / [G[u]]
app-congTerm [F] [G[u]] [ΠFG] [t≡t′] =
  let [t≡t′]′ = irrelevanceEqTerm [ΠFG] (Π-intr (Π-elim [ΠFG])) [t≡t′]
  in  app-congTerm′ [F] [G[u]] (Π-elim [ΠFG]) [t≡t′]′

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.BlockStorage.BlockStore
import      LibraBFT.Impl.Consensus.BlockStorage.BlockTree    as BlockTree
open import LibraBFT.Impl.Consensus.ConsensusTypes.Vote       as Vote
import      LibraBFT.Impl.Consensus.PersistentLivenessStorage as PersistentLivenessStorage
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Hash
open import Util.KVMap                                        as Map
open import Util.PKCS
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open Invariants
open RoundManagerTransProps
open QCProps

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

module new
  (storage              : PersistentLivenessStorage)
  (initialData          : RecoveryData)
  (stateComp            : StateComputer)
  (maxPrunedBlocksInMem : Usize)
  where

  -- TODO-2: May require refinement (additional requirements and/or properties, particularly regarding ECinfo)
  Contract : ECinfo → EitherD-Post ErrLog BlockStore
  Contract _ (Left _)   = ⊤
  Contract eci (Right bs) = BlockStoreInv (bs , eci)

  postulate
    contract : ∀ {eci}
             → Contract eci (new-e-abs storage initialData stateComp maxPrunedBlocksInMem)
module executeBlockESpec (bs : BlockStore) (block : Block) where

  Ok : Set
  Ok = ∃[ eb ] (executeBlockE bs block ≡ Right eb)

  record ContractOk (eb : ExecutedBlock) : Set where
    constructor mkContractOk
    field
      ebBlock≡ : block ≡ eb ^∙ ebBlock

  postulate -- TODO: prove
    contract : (isOk : Ok) → ContractOk (proj₁ isOk)

module executeAndInsertBlockESpec (bs0 : BlockStore) (vblock : ValidBlock) where
  block   = vbBlock vblock
  block-c = vbValid vblock
  open executeAndInsertBlockE bs0 block

  open import LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockTree

  blockId = block ^∙ bId

  ------   These are used only outside this module.
  Ok : Set
  Ok = ∃₂ λ bs' eb → executeAndInsertBlockE bs0 block ≡ Right (bs' , eb)

  open Reqs block (bs0 ^∙ bsInner)

  record ContractOk (bs' : BlockStore) (eb : ExecutedBlock) : Set where
    constructor mkContractOk
    field
      ebBlock≈ : NoHC1 → eb ^∙ ebBlock ≈Block block
      bsInv    : ∀ {eci}
                 → Preserves BlockStoreInv (bs0 , eci) (bs' , eci)
      -- executeAndInsertBlockE does not modify BlockTree fields other than btIDToBlock
      bs≡x : bs0 ≡ (bs' & (bsInner ∙ btIdToBlock) ∙~ (bs0 ^∙ bsInner ∙ btIdToBlock))

  Contract : EitherD-Post ErrLog (BlockStore × ExecutedBlock)
  Contract (Left x) = ⊤
  Contract (Right (bs' , eb)) = ContractOk bs' eb

  -- TUTORIAL: This proof has some additional commentary helping to understand the structure of the
  -- proof, and showing an example of how using abstract variants of functions makes proofs more
  -- resilient to change, as explained in
  -- https://github.com/oracle/bft-consensus-agda/blob/main/docs/PeerHandlerContracts.org
  contract' : EitherD-weakestPre step₀ Contract
  -- step₀ is a maybeSD in context of EitherD.  Therefore, via MonadMaybeD and EitherD-MonadMaybeD,
  -- this translates to EitherD-maybe.  We first deal with the easy case, applying the NoHC1
  -- function provided to ebBlock≈ to evidence eb≡ that eb is in btIdToBlock.
  proj₂ contract' eb eb≡ =
    mkContractOk (λ nohc → nohc eb≡ block-c) id refl
  proj₁ contract' getBlock≡nothing = contract₁
    where
    -- step₁ is again a maybeSD; if bs0 ^∙ bsRoot ≡ nothing, the Contract is trivial
    contract₁ : EitherD-weakestPre step₁ Contract
    proj₁ contract₁ _ = tt
    -- otherwise, bs0 ^∙ bsRoot ≡ just bsr, and we have an ifD; in the true branch, step₁ returns a
    -- Left, so again it is trivial
    proj₁ (proj₂ contract₁ bsr bsr≡) _ = tt
    -- in the else branch, we call step₂ bsr
    proj₂ (proj₂ contract₁ bsr bsr≡) btr<br = contract₂
      where
      contract₃ : ∀ eb → block ≡ (eb ^∙ ebBlock)
                  → EitherD-weakestPre (step₃ eb) Contract

      module EB = executeBlockESpec bs0 block
      open EB.ContractOk

      contract₂ : EitherD-weakestPre (step₂ bsr) Contract
      proj₂ contract₂ eb eb≡ ._             executeBlockE≡Right@refl = let con = (EB.contract (eb , eb≡))
                                                                       in contract₃ eb
                                                                                (EB.ContractOk.ebBlock≡ con)

      proj₁ contract₂ (ErrCBlockNotFound _) executeBlockE≡Left = tt
      proj₁ contract₂ (ErrVerify _)         executeBlockE≡Left = tt
      proj₁ contract₂ (ErrInfo _)           executeBlockE≡Left = tt
      -- if executeBlockE returns Left (ErrECCBlockNotFound parentBlockId), then we have two casesdue to
      -- eitherSD (pathFromRoot parentBlockId bs0) LeftD λ blocksToReexecute →
      -- in the first case, we have a Left, so it's easy
      proj₁        (proj₁ contract₂ (ErrECCBlockNotFound parentBlockId) executeBlockE≡Left) _ _ = tt
      -- in the second case, we have
      -- case⊎D (forM) blocksToReexecute (executeBlockE bs0 ∘ (_^∙ ebBlock)) of λ where
      -- and therefore two more cases; if the case⊎D returns Left, it's easy again
      proj₁ (proj₂ (proj₁ contract₂ (ErrECCBlockNotFound parentBlockId) executeBlockE≡Left) blocksToReexecute btr≡) _ _ = tt
      -- if the case⊎D returns a Right, we call executeBlockE₀ (the EitherD variant).  We use executeBlockE≡ to handle case
      -- analysis on the result of calling the abstract executeBlockE variant, ensuring we must use the contract for
      -- executeBlockE because the proof cannot "look into" the implementation of executeBlockE, which makes the proof
      -- more resilient in case of changes in its implementation.
      -- TODO-2: clean this up by writing a general version of the contract for executeBlockE
      proj₂ (proj₂ (proj₁ contract₂ (ErrECCBlockNotFound parentBlockId) executeBlockE≡Left) blocksToReexecute btr≡) _ _
        with  executeBlockE bs0  block | inspect
             (executeBlockE bs0) block
      ... | Left  x | [ R ] rewrite executeBlockE≡ R = tt
      ... | Right y | [ R ] rewrite executeBlockE≡ R =
        λ where c refl ._ refl →
                  let con = EB.contract (c , R) in
                  contract₃ c
                            (ebBlock≡ con)
                            _ refl

      contract₃ eb refl _ _ = contract₄
        where

        contract₄ : EitherD-weakestPre (step₄ eb) Contract
        contract₄
           with insertBlockESpec.contract eb (bs0 ^∙ bsInner)
        ...| con
           with BlockTree.insertBlockE.E eb (bs0 ^∙ bsInner)
        ...| Left _ = tt
        ...| Right (bt' , eb') =
           λ where ._ refl → mkContractOk IBE.blocks≈ btP bss≡x
           where
           module IBE = insertBlockESpec.ContractOk con

           open BlockStoreInv

           btP : ∀ {eci} → Preserves BlockStoreInv (bs0 , eci) ((bs0 & bsInner ∙~ bt') , eci)
           btP (mkBlockStoreInv bti) = mkBlockStoreInv (IBE.btiPres bti)

           bss≡x : bs0 ≡ (bs0 & bsInner ∙~ bt' & bsInner ∙ btIdToBlock ∙~ (bs0 ^∙ (bsInner ∙ btIdToBlock)))
           bss≡x rewrite sym IBE.bt≡x = refl

  contract : Contract (executeAndInsertBlockE bs0 block)
  contract = EitherD-contract (executeAndInsertBlockE.step₀ bs0 block) Contract contract'

module executeAndInsertBlockMSpec (vb : ValidBlock) where
  b = vbBlock vb

  -- NOTE: This function returns any errors, rather than producing them as output.
  module _ (pre : RoundManager) where
    bs = pre ^∙ lBlockStore

    contract
      : ∀ Post
        → (∀ e → {- At the moment we do not need to know why it failed -} Post (Left e) pre [])
        → ((isOk : executeAndInsertBlockESpec.Ok bs vb) → let (bs' , eb , _) = isOk in
             executeAndInsertBlockESpec.ContractOk bs vb bs' eb
           → Post (Right eb) (pre & rmBlockStore ∙~ bs') [])
        → LBFT-weakestPre (executeAndInsertBlockM b) Post pre
    proj₁ (contract Post pfBail pfOk ._ refl) e ≡left = pfBail e
    proj₂ (contract Post pfBail pfOk ._ refl) (bs' , eb) ≡right ._ refl unit refl
       with executeAndInsertBlockESpec.contract bs vb
    ...| con rewrite ≡right = pfOk (bs' , eb , refl) con

module insertSingleQuorumCertMSpec
  (qc : QuorumCert) where

  module _ (pre : RoundManager) where

    record Contract (r : Either ErrLog Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General invariants / properties
        rmInv         : Preserves RoundManagerInv pre post
        noEpochChange : NoEpochChange pre post
        noMsgOuts     : OutputProps.NoMsgs outs
        -- Voting
        noVote        : VoteNotGenerated pre post true
        -- Signatures
        qcPost : ∈Post⇒∈PreOr (_≡ qc) pre post

    postulate -- TODO-2: prove
      contract' : LBFT-weakestPre (insertSingleQuorumCertM qc) Contract pre

    contract : ∀ Q → RWS-Post-⇒ Contract Q → LBFT-weakestPre (insertSingleQuorumCertM qc) Q pre
    contract Q pf = LBFT-⇒ (insertSingleQuorumCertM qc) pre contract' pf

module syncInfoMSpec where
  syncInfo : RoundManager → SyncInfo
  syncInfo pre =
    SyncInfo∙new (pre ^∙ lBlockStore ∙ bsHighestQuorumCert)
                 (pre ^∙ lBlockStore ∙ bsHighestCommitCert)
                 (pre ^∙ lBlockStore ∙ bsHighestTimeoutCert)

  contract : ∀ pre Post → (Post (syncInfo pre) pre []) → LBFT-weakestPre syncInfoM Post pre
  contract pre Post pf ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl = pf


text:
open import Data.Product using ( _×_ ; _,_ ; proj₁ ; proj₂ )
open import FRP.LTL.RSet.Core using ( RSet ; ⟦_⟧ )
open import FRP.LTL.RSet.Globally using ( [_] )
open import FRP.LTL.RSet.Causal using ( _⊵_ ; arr )
open import FRP.LTL.RSet.Stateless using ( _⇒_ )

module FRP.LTL.RSet.Product where

infixr 2 _∧_

-- Conjunction of LTL formulae

_∧_ : RSet → RSet → RSet
(A ∧ B) t = A t × B t

-- Product structure

fst : ∀ {A B} → ⟦ (A ∧ B) ⊵ A ⟧
fst {A} {B} = arr [ (λ {u} (ab : A u × B u) → proj₁ ab) ]

snd : ∀ {A B} → ⟦ (A ∧ B) ⊵ B ⟧
snd {A} {B} = arr [ (λ {u} (ab : A u × B u) → proj₂ ab) ]

_&&&_ :  ∀ {A B C} → ⟦ (A ⊵ B) ⇒ (A ⊵ C) ⇒ (A ⊵ (B ∧ C)) ⟧
(f &&& g) s≤t σ = (f s≤t σ , g s≤t σ)

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity.Sigma

module HoTT.Pi.Transport where

transport-→ : ∀ {i j k} {X : 𝒰 i} (A : X → 𝒰 j) (B : X → 𝒰 k)
              {x₁ x₂ : X} (p : x₁ == x₂) (f : A x₁ → B x₁) →
              transport (λ x → A x → B x) p f == transport B p ∘ f ∘ transport A (p ⁻¹)
transport-→ A B refl f = refl

module _ {i j k} {X : 𝒰 i} (A : X → 𝒰 j) (B : {x : X} → A x → 𝒰 k)
         {x₁ x₂ : X} (p : x₁ == x₂) (f : Π[ a ∶ A x₁ ] B a) (a : A x₂)
  where
  private
    B̂ : Σ[ x ∶ X ] A x → 𝒰 k
    B̂ w = B (pr₂ w)
  transport-Π : transport (λ x → Π[ a ∶ A x ] B a) p f a ==
                transport {x = x₁ , transport _ (p ⁻¹) a} {y = x₂ , a}
                  B̂ (pair⁼ (p ⁻¹ , refl) ⁻¹) (f (transport A (p ⁻¹) a))
  transport-Π rewrite p = refl

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott