text:
{-# OPTIONS --no-termination-check #-}
module PiMeadow where

open import Level
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- infixr 20 _◎_

{-
postulate
  A : Set
  a b c : A
  p : a ≡ b
  q : b ≡ c

data <_> {a : Level} {A : Set a} (x : A) : Set a where
         singleton : {y : A} → y ≡ x -> < x >

irr : singleton {_} {A} {b} p ≡ singleton {_} {A} {b} (sym q)
irr = {!!}

-}
data <_> {a : Level} {A : Set a} (x : A) : Set a where
         singleton : {y : A} → y ≡ x -> < x >

-- Courtesy of Wolfram Kahl, a dependent cong₂
cong₂D  :  {a b c : Level} {A : Set a} {B : A → Set b} {C : Set c} (f : (x : A) → B x → C)
          →  {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂}
          →  (x₁≡x₂ : x₁ ≡ x₂) → y₁ ≡ subst B (sym x₁≡x₂) y₂ → f x₁ y₁ ≡ f x₂ y₂
cong₂D f refl refl = refl

mutual
  data B : Set₁ where
    ZERO  : B
    ONE   : B
    PLUS  : B → B → B
    TIMES : B → B → B
    SING  : (b : B) → ⟦ b ⟧ → B
    RECIP : (b : B) → ⟦ b ⟧ → B
    DPAIR : (b : B) → (⟦ b ⟧ → B) → B

  ⟦_⟧ : B → Set
  ⟦ ZERO ⟧         = ⊥
  ⟦ ONE ⟧          = ⊤
  ⟦ PLUS b₁ b₂ ⟧   = ⟦ b₁ ⟧ ⊎ ⟦ b₂ ⟧
  ⟦ TIMES b₁ b₂ ⟧  = ⟦ b₁ ⟧ × ⟦ b₂ ⟧
  ⟦ SING b v ⟧  = <_> {A = ⟦ b ⟧} v
  ⟦ RECIP b v ⟧      = <_> {A = ⟦ b ⟧} v → ⊤
  ⟦ DPAIR b c ⟧ = Σ ⟦ b ⟧ (λ v → ⟦ c v ⟧)

-- Useful abbrev
leftIdemp : (b : B) → ⟦ b ⟧ → B
leftIdemp b v = TIMES (SING b v) (RECIP b v)

mutual
  data _⟷_ : B → B → Set₁ where
    unite₊ : {b : B} → PLUS ZERO b ⟷ b
    uniti₊ : {b : B} → b ⟷ PLUS ZERO b
    swap₊ : {b₁ b₂ : B} → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
    assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
    assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
    unite⋆  : { b : B } → TIMES ONE b ⟷ b
    uniti⋆  : { b : B } → b ⟷ TIMES ONE b
    swap⋆ : {b₁ b₂ : B} → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
    assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
    assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
    id⟷ : {b : B } → b ⟷ b
    op    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
    _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
    _◑_    : { b₁ b₂ : B } {c d : ⟦ b₂ ⟧ → B} →
               (b₁ ⟷ DPAIR b₂ c) →
               (∀ {v} → c v ⟷ d v ) → (b₁ ⟷ DPAIR b₂ d )
 {-   _◐_    : { b₁ b₂ : B } {c d : ⟦ b₂ ⟧ → B} →
               (∀ {v} → c v ⟷ d v ) → (b₁ ⟷ DPAIR b₂ c) →
                (b₁ ⟷ DPAIR b₂ d ) -}
    lift    : { b₁ b₂ : B } {v : ⟦ b₁ ⟧ } {w : ⟦ b₂ ⟧ }
                (c : b₁ ⟷ b₂) → (w ≡ eval c v) →
                (SING b₁ v ⟷ SING b₂ w)
    _⊕_    : { b₁ b₂ b₃ b₄ : B } →
             (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
    _⊗_    : { b₁ b₂ b₃ b₄ : B } →
             (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)
    η : {b : B} → b ⟷ DPAIR b (λ v → leftIdemp b v)
    ε : {b : B} → (DPAIR b (λ v → leftIdemp b v)) ⟷ b

  eval : {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → ⟦ b₁ ⟧ → ⟦ b₂ ⟧
  eval unite₊ (inj₁ ())
  eval unite₊ (inj₂ v) = v
  eval uniti₊ v = inj₂ v
  eval swap₊ (inj₁ x) = inj₂ x
  eval swap₊ (inj₂ y) = inj₁ y
  eval assocl₊ (inj₁ x) = inj₁ (inj₁ x)
  eval assocl₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  eval assocl₊ (inj₂ (inj₂ x)) = inj₂ x
  eval assocr₊ (inj₁ (inj₁ x)) = inj₁ x
  eval assocr₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  eval assocr₊ (inj₂ y) = inj₂ (inj₂ y)
  eval unite⋆ (tt , x) = x
  eval uniti⋆ v = ( tt , v)
  eval swap⋆ (v₁ , v₂) = (v₂ , v₁)
  eval assocl⋆ (x , (y , z)) = ((x , y), z)
  eval assocr⋆ ((x , y), z) = (x , (y , z))
  eval id⟷ v = v
  eval (op c) v = evalB c v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (inj₁ x) = inj₁ (eval c₁ x)
  eval (c₁ ⊕ c₂) (inj₂ y) = inj₂ (eval c₂ y)
  eval (c₁ ⊗ c₂) (x , y) = (eval c₁ x , eval c₂ y)
  eval (η {b}) v = v , ((singleton refl) , (λ x → tt))
  eval (ε {b}) (w , c) = w
  eval (c₁ ◑ c₂) v = proj₁ v₂ , eval (c₂ {proj₁ v₂}) (proj₂ v₂)
    where v₂ = eval c₁ v
{-  eval (c₁ ◐ c₂) v = proj₁ v₂ , eval (c₁ {proj₁ v₂}) (proj₂ v₂)
    where v₂ = eval c₂ v -}
  eval (lift c z) (singleton {y = v} prf) = singleton {y = eval c v} (trans (cong (eval c) prf) (sym z))
  -- eval (lift c z) (singleton {y = v} refl) = singleton {y = eval c v} (sym z)
  -- eval (lift {- w = .(eval c v) -} c refl) (singleton {y = v} refl) = singleton {y = eval c v} refl
  evalB :  {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → ⟦ b₂ ⟧ → ⟦ b₁ ⟧
  evalB uniti₊ (inj₁ ())
  evalB uniti₊ (inj₂ v) = v
  evalB unite₊ v = inj₂ v
  evalB swap₊ (inj₁ x) = inj₂ x
  evalB swap₊ (inj₂ y) = inj₁ y
  evalB assocr₊ (inj₁ x) = inj₁ (inj₁ x)
  evalB assocr₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalB assocr₊ (inj₂ (inj₂ x)) = inj₂ x
  evalB assocl₊ (inj₁ (inj₁ x)) = inj₁ x
  evalB assocl₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalB assocl₊ (inj₂ y) = inj₂ (inj₂ y)
  evalB uniti⋆ (tt , x) = x
  evalB unite⋆ v = ( tt , v)
  evalB swap⋆ (v₁ , v₂) = (v₂ , v₁)
  evalB assocr⋆ (x , (y , z)) = ((x , y), z)
  evalB assocl⋆ ((x , y), z) = (x , (y , z))
  evalB id⟷ v = v
  evalB (op c) v = eval c v
  evalB (c₁ ◎ c₂) v = evalB c₁ (evalB c₂ v)
  evalB (c₁ ⊕ c₂) (inj₁ x) = inj₁ (evalB c₁ x)
  evalB (c₁ ⊕ c₂) (inj₂ y) = inj₂ (evalB c₂ y)
  evalB (c₁ ⊗ c₂) (x , y) = (evalB c₁ x , evalB c₂ y)
  evalB (η {b}) (w , c) = w
  evalB (ε {b}) v = v , ((singleton refl) , (λ x → tt))
  evalB (c₁ ◑ c₂) (v , x) = evalB c₁ (v , evalB c₂ x)
{-  evalB (c₁ ◐ c₂) (v , x) = evalB c₂ (v , evalB c₁ x) -}
  evalB (lift {v = v} c z) _ = eval (lift (op c) (reverse v c)) (singleton {y = eval c v} refl)

  reverse : {b₁ b₂ : B} (v : ⟦ b₁ ⟧) → (c : b₁ ⟷ b₂) → v ≡ evalB c (eval c v)
  reverse (inj₁ ()) unite₊
  reverse (inj₂ y) unite₊ = refl
  reverse v uniti₊ = refl
  reverse (inj₁ x) swap₊ = refl
  reverse (inj₂ y) swap₊ = refl
  reverse (inj₁ x) assocl₊ = refl
  reverse (inj₂ (inj₁ x)) assocl₊ = refl
  reverse (inj₂ (inj₂ y)) assocl₊ = refl
  reverse (inj₁ (inj₁ x)) assocr₊ = refl
  reverse (inj₁ (inj₂ y)) assocr₊ = refl
  reverse (inj₂ y) assocr₊ = refl
  reverse v unite⋆ = refl
  reverse v uniti⋆ = refl
  reverse v swap⋆ = refl
  reverse v assocl⋆ = refl
  reverse v assocr⋆ = refl
  reverse v id⟷ = refl
  reverse v (op c) = reverse' c v
  reverse v (c ◎ c₁) = trans (reverse v c) (cong (evalB c) eq)
     where eq : eval c v ≡ evalB c₁ (eval c₁ (eval c v))
           eq = reverse (eval c v) c₁
  reverse v (_◑_ {_} {b₂} {c} c₁ u) = trans eq₁ (cong (evalB c₁) eq₃)
    where y : Σ ⟦ b₂ ⟧ (λ ww → ⟦ c ww ⟧)
          y = eval c₁ v
          eq₁ : v ≡ evalB c₁ y
          eq₁ = reverse v c₁
          eq₂ : proj₂ y ≡ evalB u (eval u (proj₂ y))
          eq₂ = reverse (proj₂ y) u
          eq₃ : y ≡ (proj₁ y , evalB u (eval u (proj₂ y)))
          eq₃ = cong (λ z → (proj₁ y , z)) eq₂
{-  reverse v (_◐_ {_} {b₂} {c} c₁ c₂) = {!!} -}
--  reverse (singleton {.v₂} refl) (lift {v = v₂} {.(eval c v₂)} c refl) =  {!cong singleton {! proof-irrelevance  {! (reverse v₂ c)  !} ?!} !}
  reverse (singleton prf₁) (lift {v = v₂} c prf₂) =
      cong₂D (λ x e → singleton {y = x} e)
            (trans prf₁ (reverse v₂ c)) (proof-irrelevance prf₁ _)
  reverse (inj₁ x) (c ⊕ _) = cong inj₁ (reverse x c)
  reverse (inj₂ y) (_ ⊕ c) = cong inj₂ (reverse y c)
  reverse (x , y) (c₁ ⊗ c₂) = cong₂ _,_ (reverse x c₁) (reverse y c₂)
  reverse v η = refl
  reverse (_ , (singleton refl , _)) ε = refl

  reverse' : {b₁ b₂ : B} (c : b₁ ⟷ b₂) → (w : ⟦ b₂ ⟧) → w ≡ eval c (evalB c w)
  reverse' unite₊ w = refl
  reverse' uniti₊ (inj₁ ())
  reverse' uniti₊ (inj₂ y) = refl
  reverse' swap₊ (inj₁ x) = refl
  reverse' swap₊ (inj₂ y) = refl
  reverse' assocl₊ (inj₁ (inj₁ x)) = refl
  reverse' assocl₊ (inj₁ (inj₂ y)) = refl
  reverse' assocl₊ (inj₂ y) = refl
  reverse' assocr₊ (inj₁ x) = refl
  reverse' assocr₊ (inj₂ (inj₁ x)) = refl
  reverse' assocr₊ (inj₂ (inj₂ y)) = refl
  reverse' unite⋆ w = refl
  reverse' uniti⋆ w = refl
  reverse' swap⋆ w = refl
  reverse' assocl⋆ w = refl
  reverse' assocr⋆ w = refl
  reverse' id⟷ w = refl
  reverse' (op c) w = reverse w c
  reverse' (c ◎ c₁) w = trans (reverse' c₁ w) (cong (eval c₁) (reverse' c (evalB c₁ w)))
  reverse' {b₁} {DPAIR b₂ d} (_◑_ {c = c} c₁ c₂) (w₁ , w₂)
    rewrite (sym (reverse' c₁ (w₁ , evalB c₂ w₂))) | (sym (reverse' c₂ w₂)) =  refl
{-  reverse' (c₁ ◐ c₂) w = {!!} -}
  reverse' (lift {v = v} {w = .(eval c v)} c refl) (singleton refl) = cong₂D (λ x e → singleton {y = x} e) (reverse' c (eval c v)) (proof-irrelevance refl _)
  reverse' (c ⊕ _) (inj₁ x) = cong inj₁ (reverse' c x)
  reverse' (_ ⊕ c) (inj₂ y) = cong inj₂ (reverse' c y)
  reverse' (c₁ ⊗ c₂) (x , y) = cong₂ _,_ (reverse' c₁ x) (reverse' c₂ y)
  reverse' η (_ , singleton refl , _ ) = refl
  reverse' ε w = refl

-- they are properly inverse of each other
-- easy direction
η∘ε : {b : B} (v : ⟦ b ⟧) → eval {b} (η ◎ ε) v ≡ v
η∘ε _ = refl

-- hard direction.
ε∘η : {b : B} (v : ⟦ b ⟧) → { w : Σ < v > (λ _ → < v > → ⊤) }
      → (eval {DPAIR b (leftIdemp b) } {_} (ε ◎ η) (v , w)) ≡ (v , w)
ε∘η {b} v {(singleton refl , r )} = cong f {v , v , (singleton refl)} refl
    where f : Σ ⟦ b ⟧ (λ x → Σ ⟦ b ⟧ (λ y → < v >)) →
                Σ ⟦ b ⟧ (λ z → Σ < z > (λ x → < z > → ⊤ ))
          f (_ , (_ , j)) = (v , j , r)

-- Now need to write some actual programs...
makeFunc : {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → b₁ ⟷ DPAIR b₁ (λ x → TIMES (SING b₂ (eval c x)) (RECIP b₁ x))
makeFunc {b₁} {b₂} c = η {b₁} ◑ (λ {v₁} →  (lift c refl) ⊗ id⟷)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------------
-- Properties of the alter list
------------------------------------------------------------------------------

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

module FOT.FOTC.UnguardedCorecursion.Alter.PropertiesI where

open import FOT.FOTC.UnguardedCorecursion.Alter.Alter

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Data.Stream.Type
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- TODO (23 December 2013).
-- alter-Stream : Stream alter
-- alter-Stream = Stream-coind A h refl
--   where
--   A : D → Set
--   A xs = xs ≡ alter

--   h : ∀ {xs} → A xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'
--   h Ax = true , (false ∷ alter) , trans Ax alter-eq , {!!}

-- TODO (23 December 2013).
-- alter≈alter' : alter ≈ alter'
-- alter≈alter' = ≈-coind B h₁ h₂
--   where
--   B : D → D → Set
--   B xs ys = xs ≡ xs

--   h₁ : B alter alter' → ∃[ x' ] ∃[ xs' ] ∃[ ys' ]
--          alter ≡ x' ∷ xs' ∧ alter' ≡ x' ∷ ys' ∧ B xs' ys'
--   h₁ _ = true
--          , false ∷ alter
--          , map not₀ alter'
--          , alter-eq
--          , alter'-eq
--          , refl

--   h₂ : B alter alter'
--   h₂ = refl

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-

This file proves a variety of basic results about paths:

- refl, sym, cong and composition of paths. This is used to set up
  equational reasoning.

- Transport, subst and functional extensionality

- J and its computation rule (up to a path)

- Σ-types and contractibility of singletons

- Converting PathP to and from a homogeneous path with transp

- Direct definitions of lower h-levels

- Export natural numbers

- Export universe lifting

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Prelude where

open import Cubical.Core.Primitives public

infixr 30 _∙_
infix  3 _∎
infixr 2 _≡⟨_⟩_
infixr 2.5 _≡⟨_⟩≡⟨_⟩_

-- Basic theory about paths. These proofs should typically be
-- inlined. This module also makes equational reasoning work with
-- (non-dependent) paths.

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : A → Type ℓ
    x y z w : A

refl : x ≡ x
refl {x = x} = λ _ → x
{-# INLINE refl #-}

sym : x ≡ y → y ≡ x
sym p i = p (~ i)
{-# INLINE sym #-}

symP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} →
       (p : PathP A x y) → PathP (λ i → A (~ i)) y x
symP p j = p (~ j)

cong : ∀ (f : (a : A) → B a) (p : x ≡ y) →
       PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)
{-# INLINE cong #-}

cong₂ : ∀ {C : (a : A) → (b : B a) → Type ℓ} →
        (f : (a : A) → (b : B a) → C a b) →
        (p : x ≡ y) →
        {u : B x} {v : B y} (q : PathP (λ i → B (p i)) u v) →
        PathP (λ i → C (p i) (q i)) (f x u) (f y v)
cong₂ f p q i = f (p i) (q i)
{-# INLINE cong₂ #-}

{- The most natural notion of homogenous path composition
    in a cubical setting is double composition:

       x ∙ ∙ ∙ > w
       ^         ^
   p⁻¹ |         | r        ^
       |         |        j |
       y — — — > z          ∙ — >
            q                 i

   `p ∙∙ q ∙∙ r` gives the line at the top,
   `doubleCompPath-filler p q r` gives the whole square
-}

doubleComp-faces : {x y z w : A } (p : x ≡ y) (r : z ≡ w)
                 → (i : I) (j : I) → Partial (i ∨ ~ i) A
doubleComp-faces p r i j (i = i0) = p (~ j)
doubleComp-faces p r i j (i = i1) = r j

_∙∙_∙∙_ : w ≡ x → x ≡ y → y ≡ z → w ≡ z
(p ∙∙ q ∙∙ r) i =
  hcomp (doubleComp-faces p r i) (q i)

doubleCompPath-filler : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
                      → PathP (λ j → p (~ j) ≡ r j) q (p ∙∙ q ∙∙ r)
doubleCompPath-filler p q r j i =
  hfill (doubleComp-faces p r i) (inS (q i)) j

-- any two definitions of double composition are equal
compPath-unique : ∀ (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
                  → (α β : Σ[ s ∈ x ≡ w ] PathP (λ j → p (~ j) ≡ r j) q s)
                  → α ≡ β
compPath-unique p q r (α , α-filler) (β , β-filler) t
  = (λ i → cb i1 i) , (λ j i → cb j i)
  where cb : I → I → _
        cb j i = hfill (λ j → λ { (t = i0) → α-filler j i
                                ; (t = i1) → β-filler j i
                                ; (i = i0) → p (~ j)
                                ; (i = i1) → r j })
                       (inS (q i)) j

{- For single homogenous path composition, we take `p = refl`:

     x ∙ ∙ ∙ > z
     ‖         ^
     ‖         | r        ^
     ‖         |        j |
     x — — — > y          ∙ — >
          q                 i

   `q ∙ r` gives the line at the top,
   `compPath-filler q r` gives the whole square
-}

_∙_ : x ≡ y → y ≡ z → x ≡ z
p ∙ q = refl ∙∙ p ∙∙ q

compPath-filler : (p : x ≡ y) (q : y ≡ z) → PathP (λ j → x ≡ q j) p (p ∙ q)
compPath-filler p q = doubleCompPath-filler refl p q

-- We could have also defined single composition by taking `r = refl`:

_∙'_ : x ≡ y → y ≡ z → x ≡ z
p ∙' q = p ∙∙ q ∙∙ refl

compPath'-filler : (p : x ≡ y) (q : y ≡ z) → PathP (λ j → p (~ j) ≡ z) q (p ∙' q)
compPath'-filler p q = doubleCompPath-filler p q refl

-- It's easy to show that `p ∙ q` also has such a filler:
compPath-filler' : (p : x ≡ y) (q : y ≡ z) → PathP (λ j → p (~ j) ≡ z) q (p ∙ q)
compPath-filler' {z = z} p q j i =
  hcomp (λ k → λ { (i = i0) → p (~ j)
                 ; (i = i1) → q k
                 ; (j = i0) → q (i ∧ k) })
        (p (i ∨ ~ j))
-- Note: We can omit a (j = i1) case here since when (j = i1), the whole expression is
--  definitionally equal to `p ∙ q`. (Notice that `p ∙ q` is also an hcomp.) Nevertheless,
--  we could have given `compPath-filler p q k i` as the (j = i1) case.

-- From this, we can show that these two notions of composition are the same
compPath≡compPath' : (p : x ≡ y) (q : y ≡ z) → p ∙ q ≡ p ∙' q
compPath≡compPath' p q j =
  compPath-unique p q refl (p ∙ q  , compPath-filler' p q)
                           (p ∙' q , compPath'-filler p q) j .fst

-- Heterogeneous path composition and its filler:

compPathP : ∀ {A : I → Type ℓ} {x : A i0} {y : A i1} {B_i1 : Type ℓ} {B : (A i1) ≡ B_i1} {z : B i1}
            → PathP A x y → PathP (λ i → B i) y z → PathP (λ j → ((λ i → A i) ∙ B) j) x z
compPathP {A = A} {x = x} {B = B} p q i =
  comp (λ j → compPath-filler (λ i → A i) B j i)
       (λ j → λ { (i = i0) → x ;
                  (i = i1) → q j })
       (p i)

compPathP' : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y z : A} {x' : B x} {y' : B y} {z' : B z} {p : x ≡ y} {q : y ≡ z}
             (P : PathP (λ i → B (p i)) x' y') (Q : PathP (λ i → B (q i)) y' z')
          → PathP (λ i → B ((p ∙ q) i)) x' z'
compPathP' {B = B} {x' = x'} {p = p} {q = q} P Q i =
  comp (λ j → B (compPath-filler p q j i))
       (λ j → λ { (i = i0) → x'  ;
                  (i = i1) → Q j })
       (P i)

compPathP-filler : ∀ {A : I → Type ℓ} {x : A i0} {y : A i1} {B_i1 : Type ℓ} {B : A i1 ≡ B_i1} {z : B i1}
                   → (p : PathP A x y) (q : PathP (λ i → B i) y z)
                   → PathP (λ j → PathP (λ k → (compPath-filler (λ i → A i) B j k)) x (q j)) p (compPathP p q)
compPathP-filler {A = A} {x = x} {B = B} p q j i =
  fill (λ j → compPath-filler (λ i → A i) B j i)
       (λ j → λ { (i = i0) → x ;
                  (i = i1) → q j })
       (inS (p i)) j

compPathP'-filler : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y z : A} {x' : B x} {y' : B y} {z' : B z} {p : x ≡ y} {q : y ≡ z}
             (P : PathP (λ i → B (p i)) x' y') (Q : PathP (λ i → B (q i)) y' z')
          → PathP (λ j → PathP (λ i → B (compPath-filler p q j i)) x' (Q j)) P (compPathP' {x = x} {y = y} {x' = x'} {y' = y'} P Q)
compPathP'-filler {B = B} {x' = x'} {p = p} {q = q} P Q j i =
  fill (λ j → B (compPath-filler p q j i))
       (λ j → λ { (i = i0) → x'  ;
                  (i = i1) → Q j })
       (inS (P i))
       j

_≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ x≡y ⟩ y≡z = x≡y ∙ y≡z

≡⟨⟩-syntax : (x : A) → x ≡ y → y ≡ z → x ≡ z
≡⟨⟩-syntax = _≡⟨_⟩_
infixr 2 ≡⟨⟩-syntax
syntax ≡⟨⟩-syntax x (λ i → B) y = x ≡[ i ]⟨ B ⟩ y

≡⟨⟩⟨⟩-syntax : (x y : A) → x ≡ y → y ≡ z → z ≡ w → x ≡ w
≡⟨⟩⟨⟩-syntax x y p q r = p ∙∙ q ∙∙ r
infixr 3 ≡⟨⟩⟨⟩-syntax
syntax ≡⟨⟩⟨⟩-syntax x y B C = x ≡⟨ B ⟩≡ y ≡⟨ C ⟩≡

_≡⟨_⟩≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → z ≡ w → x ≡ w
_ ≡⟨ x≡y ⟩≡⟨ y≡z ⟩ z≡w = x≡y ∙∙ y≡z ∙∙ z≡w

_∎ : (x : A) → x ≡ x
_ ∎ = refl

-- Transport, subst and functional extensionality

-- transport is a special case of transp
transport : {A B : Type ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

-- Transporting in a constant family is the identity function (up to a
-- path). If we would have regularity this would be definitional.
transportRefl : (x : A) → transport refl x ≡ x
transportRefl {A = A} x i = transp (λ _ → A) i x

transport-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : A)
                   → PathP (λ i → p i) x (transport p x)
transport-filler p x i = transp (λ j → p (i ∧ j)) (~ i) x

-- We want B to be explicit in subst
subst : (B : A → Type ℓ') (p : x ≡ y) → B x → B y
subst B p pa = transport (λ i → B (p i)) pa

subst2 : ∀ {ℓ' ℓ''} {B : Type ℓ'} {z w : B} (C : A → B → Type ℓ'')
        (p : x ≡ y) (q : z ≡ w) → C x z → C y w
subst2 B p q b = transport (λ i → B (p i) (q i)) b

substRefl : (px : B x) → subst B refl px ≡ px
substRefl px = transportRefl px

funExt : {B : A → I → Type ℓ'}
  {f : (x : A) → B x i0} {g : (x : A) → B x i1}
  → ((x : A) → PathP (B x) (f x) (g x))
  → PathP (λ i → (x : A) → B x i) f g
funExt p i x = p x i

implicitFunExt : {B : A → I → Type ℓ'}
  {f : {x : A} → B x i0} {g : {x : A} → B x i1}
  → ({x : A} → PathP (B x) (f {x}) (g {x}))
  → PathP (λ i → {x : A} → B x i) f g
implicitFunExt p i {x} = p {x} i

-- the inverse to funExt (see Functions.FunExtEquiv), converting paths
-- between functions to homotopies; `funExt⁻` is called `happly` and
-- defined by path induction in the HoTT book (see function 2.9.2 in
-- section 2.9)
funExt⁻ : {B : A → I → Type ℓ'}
  {f : (x : A) → B x i0} {g : (x : A) → B x i1}
  → PathP (λ i → (x : A) → B x i) f g
  → ((x : A) → PathP (B x) (f x) (g x))
funExt⁻ eq x i = eq i x

-- J for paths and its computation rule

module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
  J : (p : x ≡ y) → P y p
  J p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d

  JRefl : J refl ≡ d
  JRefl = transportRefl d

  J-∙ : (p : x ≡ y) (q : y ≡ z)
    → J (p ∙ q) ≡ transport (λ i → P (q i) (λ j → compPath-filler p q i j)) (J p)
  J-∙ p q k =
    transp
      (λ i → P (q (i ∨ ~ k))
      (λ j → compPath-filler p q (i ∨ ~ k) j)) (~ k)
      (J (λ j → compPath-filler p q (~ k) j))

-- Converting to and from a PathP

module _ {A : I → Type ℓ} {x : A i0} {y : A i1} where
  toPathP : transp (\ i → A i) i0 x ≡ y → PathP A x y
  toPathP p i = hcomp (λ j → λ { (i = i0) → x
                               ; (i = i1) → p j })
                      (transp (λ j → A (i ∧ j)) (~ i) x)

  fromPathP : PathP A x y → transp (\ i → A i) i0 x ≡ y
  fromPathP p i = transp (λ j → A (i ∨ j)) i (p i)

-- Whiskering a dependent path by a path

_◁_ : ∀ {ℓ} {A : I → Type ℓ} {a₀ a₀' : A i0} {a₁ : A i1}
  → a₀ ≡ a₀' → PathP A a₀' a₁ → PathP A a₀ a₁
(p ◁ q) i =
  hcomp (λ j → λ {(i = i0) → p (~ j); (i = i1) → q i1}) (q i)

_▷_ : ∀ {ℓ} {A : I → Type ℓ} {a₀ : A i0} {a₁ a₁' : A i1}
  → PathP A a₀ a₁ → a₁ ≡ a₁' → PathP A a₀ a₁'
(p ▷ q) i =
  hcomp (λ j → λ {(i = i0) → p i0; (i = i1) → q j}) (p i)

-- Direct definitions of lower h-levels

isContr : Type ℓ → Type ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

isProp : Type ℓ → Type ℓ
isProp A = (x y : A) → x ≡ y

isSet : Type ℓ → Type ℓ
isSet A = (x y : A) → isProp (x ≡ y)

isGroupoid : Type ℓ → Type ℓ
isGroupoid A = ∀ a b → isSet (Path A a b)

is2Groupoid : Type ℓ → Type ℓ
is2Groupoid A = ∀ a b → isGroupoid (Path A a b)

-- Contractibility of singletons

singlP : (A : I → Type ℓ) (a : A i0) → Type _
singlP A a = Σ[ x ∈ A i1 ] PathP A a x

singl : (a : A) → Type _
singl {A = A} a = singlP (λ _ → A) a

isContrSingl : (a : A) → isContr (singl a)
isContrSingl a = (a , refl) , λ p i → p .snd i , λ j → p .snd (i ∧ j)

isContrSinglP : (A : I → Type ℓ) (a : A i0) → isContr (singlP A a)
isContrSinglP A a .fst = _ , transport-filler (λ i → A i) a
isContrSinglP A a .snd (x , p) i =
  _ , λ j → fill (\ i → A i) (λ j → λ {(i = i0) → transport-filler (λ i → A i) a j; (i = i1) → p j}) (inS a) j

SquareP :
  (A : I → I → Type ℓ)
  {a₀₀ : A i0 i0} {a₀₁ : A i0 i1} (a₀₋ : PathP (λ j → A i0 j) a₀₀ a₀₁)
  {a₁₀ : A i1 i0} {a₁₁ : A i1 i1} (a₁₋ : PathP (λ j → A i1 j) a₁₀ a₁₁)
  (a₋₀ : PathP (λ i → A i i0) a₀₀ a₁₀) (a₋₁ : PathP (λ i → A i i1) a₀₁ a₁₁)
  → Type ℓ
SquareP A a₀₋ a₁₋ a₋₀ a₋₁ = PathP (λ i → PathP (λ j → A i j) (a₋₀ i) (a₋₁ i)) a₀₋ a₁₋

Square :
  {a₀₀ a₀₁ : A} (a₀₋ : a₀₀ ≡ a₀₁)
  {a₁₀ a₁₁ : A} (a₁₋ : a₁₀ ≡ a₁₁)
  (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁)
  → Type _
Square a₀₋ a₁₋ a₋₀ a₋₁ = PathP (λ i → a₋₀ i ≡ a₋₁ i) a₀₋ a₁₋

isSet' : Type ℓ → Type ℓ
isSet' A =
  {a₀₀ a₀₁ : A} (a₀₋ : a₀₀ ≡ a₀₁)
  {a₁₀ a₁₁ : A} (a₁₋ : a₁₀ ≡ a₁₁)
  (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁)
  → Square a₀₋ a₁₋ a₋₀ a₋₁

Cube :
  {a₀₀₀ a₀₀₁ : A} {a₀₀₋ : a₀₀₀ ≡ a₀₀₁}
  {a₀₁₀ a₀₁₁ : A} {a₀₁₋ : a₀₁₀ ≡ a₀₁₁}
  {a₀₋₀ : a₀₀₀ ≡ a₀₁₀} {a₀₋₁ : a₀₀₁ ≡ a₀₁₁}
  (a₀₋₋ : Square a₀₀₋ a₀₁₋ a₀₋₀ a₀₋₁)
  {a₁₀₀ a₁₀₁ : A} {a₁₀₋ : a₁₀₀ ≡ a₁₀₁}
  {a₁₁₀ a₁₁₁ : A} {a₁₁₋ : a₁₁₀ ≡ a₁₁₁}
  {a₁₋₀ : a₁₀₀ ≡ a₁₁₀} {a₁₋₁ : a₁₀₁ ≡ a₁₁₁}
  (a₁₋₋ : Square a₁₀₋ a₁₁₋ a₁₋₀ a₁₋₁)
  {a₋₀₀ : a₀₀₀ ≡ a₁₀₀} {a₋₀₁ : a₀₀₁ ≡ a₁₀₁}
  (a₋₀₋ : Square a₀₀₋ a₁₀₋ a₋₀₀ a₋₀₁)
  {a₋₁₀ : a₀₁₀ ≡ a₁₁₀} {a₋₁₁ : a₀₁₁ ≡ a₁₁₁}
  (a₋₁₋ : Square a₀₁₋ a₁₁₋ a₋₁₀ a₋₁₁)
  (a₋₋₀ : Square a₀₋₀ a₁₋₀ a₋₀₀ a₋₁₀)
  (a₋₋₁ : Square a₀₋₁ a₁₋₁ a₋₀₁ a₋₁₁)
  → Type _
Cube a₀₋₋ a₁₋₋ a₋₀₋ a₋₁₋ a₋₋₀ a₋₋₁ =
  PathP (λ i → Square (a₋₀₋ i) (a₋₁₋ i) (a₋₋₀ i) (a₋₋₁ i)) a₀₋₋ a₁₋₋

isGroupoid' : Type ℓ → Type ℓ
isGroupoid' A =
  {a₀₀₀ a₀₀₁ : A} {a₀₀₋ : a₀₀₀ ≡ a₀₀₁}
  {a₀₁₀ a₀₁₁ : A} {a₀₁₋ : a₀₁₀ ≡ a₀₁₁}
  {a₀₋₀ : a₀₀₀ ≡ a₀₁₀} {a₀₋₁ : a₀₀₁ ≡ a₀₁₁}
  (a₀₋₋ : Square a₀₀₋ a₀₁₋ a₀₋₀ a₀₋₁)
  {a₁₀₀ a₁₀₁ : A} {a₁₀₋ : a₁₀₀ ≡ a₁₀₁}
  {a₁₁₀ a₁₁₁ : A} {a₁₁₋ : a₁₁₀ ≡ a₁₁₁}
  {a₁₋₀ : a₁₀₀ ≡ a₁₁₀} {a₁₋₁ : a₁₀₁ ≡ a₁₁₁}
  (a₁₋₋ : Square a₁₀₋ a₁₁₋ a₁₋₀ a₁₋₁)
  {a₋₀₀ : a₀₀₀ ≡ a₁₀₀} {a₋₀₁ : a₀₀₁ ≡ a₁₀₁}
  (a₋₀₋ : Square a₀₀₋ a₁₀₋ a₋₀₀ a₋₀₁)
  {a₋₁₀ : a₀₁₀ ≡ a₁₁₀} {a₋₁₁ : a₀₁₁ ≡ a₁₁₁}
  (a₋₁₋ : Square a₀₁₋ a₁₁₋ a₋₁₀ a₋₁₁)
  (a₋₋₀ : Square a₀₋₀ a₁₋₀ a₋₀₀ a₋₁₀)
  (a₋₋₁ : Square a₀₋₁ a₁₋₁ a₋₀₁ a₋₁₁)
  → Cube a₀₋₋ a₁₋₋ a₋₀₋ a₋₁₋ a₋₋₀ a₋₋₁

-- Essential consequences of isProp and isContr
isProp→PathP : ∀ {B : I → Type ℓ} → ((i : I) → isProp (B i))
               → (b0 : B i0) (b1 : B i1)
               → PathP (λ i → B i) b0 b1
isProp→PathP hB b0 b1 = toPathP (hB _ _ _)

isPropIsContr : isProp (isContr A)
isPropIsContr (c0 , h0) (c1 , h1) j =
  h0 c1 j , λ y i → hcomp (λ k → λ { (i = i0) → h0 (h0 c1 j) k;
                                     (i = i1) → h0 y k;
                                     (j = i0) → h0 (h0 y i) k;
                                     (j = i1) → h0 (h1 y i) k}) c0

isContr→isProp : isContr A → isProp A
isContr→isProp (x , p) a b i =
  hcomp (λ j → λ { (i = i0) → p a j
                 ; (i = i1) → p b j }) x

isProp→isSet : isProp A → isSet A
isProp→isSet h a b p q j i =
  hcomp (λ k → λ { (i = i0) → h a a k
                 ; (i = i1) → h a b k
                 ; (j = i0) → h a (p i) k
                 ; (j = i1) → h a (q i) k }) a

isProp→isSet' : isProp A → isSet' A
isProp→isSet' h {a} p q r s i j =
  hcomp (λ k → λ { (i = i0) → h a (p j) k
                 ; (i = i1) → h a (q j) k
                 ; (j = i0) → h a (r i) k
                 ; (j = i1) → h a (s i) k}) a

isPropIsProp : isProp (isProp A)
isPropIsProp f g i a b = isProp→isSet f a b (f a b) (g a b) i

isPropSingl : {a : A} → isProp (singl a)
isPropSingl = isContr→isProp (isContrSingl _)

isPropSinglP : {A : I → Type ℓ} {a : A i0} → isProp (singlP A a)
isPropSinglP = isContr→isProp (isContrSinglP _ _)

-- Universe lifting

record Lift {i j} (A : Type i) : Type (ℓ-max i j) where
  constructor lift
  field
    lower : A

open Lift public

liftExt : ∀ {A : Type ℓ} {a b : Lift {ℓ} {ℓ'} A} → (lower a ≡ lower b) → a ≡ b
liftExt x i = lift (x i)

doubleCompPath-filler∙ : {a b c d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d)
                       → PathP (λ i → p i ≡ r (~ i)) (p ∙ q ∙ r) q
doubleCompPath-filler∙ {A = A} {b = b} p q r j i =
  hcomp (λ k → λ { (i = i0) → p j
                  ; (i = i1) → side j k
                  ; (j = i1) → q (i ∧ k)})
        (p (j ∨ i))
  where
  side : I → I → A
  side i j =
    hcomp (λ k → λ { (i = i1) → q j
                    ; (j = i0) → b
                    ; (j = i1) → r (~ i ∧ k)})
          (q j)

PathP→compPathL : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
           → PathP (λ i → p i ≡ q i) r s
           → sym p ∙ r ∙ q ≡ s
PathP→compPathL {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (j ∨ k)
                  ; (i = i1) → q (j ∨ k)
                  ; (j = i0) → doubleCompPath-filler∙ (sym p) r q (~ k) i
                  ; (j = i1) → s i })
        (P j i)

PathP→compPathR : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
           → PathP (λ i → p i ≡ q i) r s
           → r ≡ p ∙ s ∙ sym q
PathP→compPathR {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (j ∧ (~ k))
                  ; (i = i1) → q (j ∧ (~ k))
                  ; (j = i0) → r i
                  ; (j = i1) → doubleCompPath-filler∙ p s (sym q) (~ k) i})
        (P j i)

-- otherdir

compPathL→PathP : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
           → sym p ∙ r ∙ q ≡ s
           → PathP (λ i → p i ≡ q i) r s
compPathL→PathP {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (~ k ∨ j)
                  ; (i = i1) → q (~ k ∨ j)
                  ; (j = i0) → doubleCompPath-filler∙ (sym p) r q k i
                  ; (j = i1) → s i})
        (P j i)

compPathR→PathP : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
                → r ≡ p ∙ s ∙ sym q
                → PathP (λ i → p i ≡ q i) r s
compPathR→PathP {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (k ∧ j)
                  ; (i = i1) → q (k ∧ j)
                  ; (j = i0) → r i
                  ; (j = i1) → doubleCompPath-filler∙  p s (sym q) k i})
        (P j i)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- Andreas, 2012-11-18: abstract record values
module Issue759 where

import Common.Level

abstract
  record Wrap (A : Set) : Set where
    field wrapped : A
  open Wrap public

  wrap : {A : Set} → A → Wrap A
  wrap a = record { wrapped = a }

-- caused 'Not in Scope: recCon-NOT-PRINTED'
-- during eta-contraction in serialization

-- should work now

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Structure.Operator.Group where

import      Lvl
open import Logic
open import Logic.IntroInstances
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function
open import Structure.Operator.Monoid using (Monoid)
open import Structure.Operator.Properties hiding (commutativity)
open import Type
open import Type.Size

-- A type and a binary operator using this type is a group when:
-- • It is a monoid.
-- • The operator have an inverse in both directions.
record Group {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ monoid ⦄ : Monoid(_▫_)
  open Monoid(monoid) public

  field
    ⦃ inverse-existence ⦄ : ∃(InverseFunction(_▫_) ⦃ identity-existence ⦄)

  inv = [∃]-witness inverse-existence

  field
    ⦃ inv-function ⦄ : Function(inv)

  instance
    inverse : InverseFunction (_▫_) inv
    inverse = [∃]-proof inverse-existence

  instance
    inverseₗ : InverseFunctionₗ (_▫_) inv
    inverseₗ = InverseFunction.left(inverse)

  instance
    inverseᵣ : InverseFunctionᵣ (_▫_) inv
    inverseᵣ = InverseFunction.right(inverse)

  inv-op : T → T → T
  inv-op x y = x ▫ inv y

record CommutativeGroup {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ group ⦄         : Group (_▫_)
    ⦃ commutativity ⦄ : Commutativity (_▫_)
  open Group(group) public

{- TODO: See Monoid for how this should be rewritten to fit how it is done in Category
module Morphism where
  module _ {ℓ₁ ℓ₂} {X : Type{ℓ₁}} ⦃ _ : Equiv(X) ⦄ {_▫X_ : X → X → X} ⦃ structureₗ : Group(_▫X_) ⦄ {Y : Type{ℓ₂}} ⦃ _ : Equiv(Y) ⦄ {_▫Y_ : Y → Y → Y} ⦃ structureᵣ : Group(_▫Y_) ⦄ (f : X → Y) where
    -- Group homomorphism
    record Homomorphism : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro

      idₗ = Group.id(structureₗ)
      idᵣ = Group.id(structureᵣ)

      invₗ = Group.inv(structureₗ)
      invᵣ = Group.inv(structureᵣ)

      field
        preserve-op  : ∀{x y : X} → (f(x ▫X y) ≡ f(x) ▫Y f(y))
        -- TODO: These may be unneccessary because they follow from preserve-op when Function(f)
        preserve-inv : ∀{x : X} → (f(invₗ x) ≡ invᵣ(f(x)))
        preserve-id  : (f(idₗ) ≡ idᵣ)

    -- Group monomorphism (Injective homomorphism)
    record Monomorphism : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        ⦃ homomorphism ⦄ : Homomorphism
        ⦃ size ⦄         : (X ≼ Y)

    -- Group epimorphism (Surjective homomorphism)
    record Epimorphism : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        ⦃ homomorphism ⦄ : Homomorphism
        ⦃ size ⦄         : (X ≽ Y)

    -- Group isomorphism (Bijective homomorphism)
    record Isomorphism : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field
        ⦃ homomorphism ⦄ : Homomorphism
        ⦃ size ⦄         : (X ≍ Y)

  _↣_ : ∀{ℓ₁ ℓ₂} → {X : Type{ℓ₁}} → ⦃ _ : Equiv(X) ⦄ → (_▫X_ : X → X → X) → ⦃ structureₗ : Group(_▫X_) ⦄ → {Y : Type{ℓ₂}} → ⦃ _ : Equiv(Y) ⦄ → (_▫Y_ : Y → Y → Y) → ⦃ structureᵣ : Group(_▫Y_) ⦄ → Stmt{ℓ₁ Lvl.⊔ ℓ₂}
  (_▫X_) ↣ (_▫Y_) = ∃(Monomorphism{_▫X_ = _▫X_}{_▫Y_ = _▫Y_})

  _↠_ : ∀{ℓ₁ ℓ₂} → {X : Type{ℓ₁}} → ⦃ _ : Equiv(X) ⦄ → (_▫X_ : X → X → X) → ⦃ structureₗ : Group(_▫X_) ⦄ → {Y : Type{ℓ₂}} → ⦃ _ : Equiv(Y) ⦄ → (_▫Y_ : Y → Y → Y) → ⦃ structureᵣ : Group(_▫Y_) ⦄ → Stmt{ℓ₁ Lvl.⊔ ℓ₂}
  (_▫X_) ↠ (_▫Y_) = ∃(Epimorphism{_▫X_ = _▫X_}{_▫Y_ = _▫Y_})

  _⤖_ : ∀{ℓ₁ ℓ₂} → {X : Type{ℓ₁}} → ⦃ _ : Equiv(X) ⦄ → (_▫X_ : X → X → X) → ⦃ structureₗ : Group(_▫X_) ⦄ → {Y : Type{ℓ₂}} → ⦃ _ : Equiv(Y) ⦄ → (_▫Y_ : Y → Y → Y) → ⦃ structureᵣ : Group(_▫Y_) ⦄ → Stmt{ℓ₁ Lvl.⊔ ℓ₂}
  (_▫X_) ⤖ (_▫Y_) = ∃(Isomorphism{_▫X_ = _▫X_}{_▫Y_ = _▫Y_})
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties
------------------------------------------------------------------------

module Data.Bool.Properties where

open import Data.Bool as Bool
open import Data.Fin
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Algebra
open import Algebra.Structures
import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl)
open P.≡-Reasoning
import Algebra.FunctionProperties as FP; open FP (_≡_ {A = Bool})
open import Data.Product
open import Data.Sum
open import Data.Empty

------------------------------------------------------------------------
-- Duality

-- Can we take advantage of duality in some (nice) way?

------------------------------------------------------------------------
-- (Bool, ∨, ∧, false, true) forms a commutative semiring

private

  ∨-assoc : Associative _∨_
  ∨-assoc true  y z = refl
  ∨-assoc false y z = refl

  ∧-assoc : Associative _∧_
  ∧-assoc true  y z = refl
  ∧-assoc false y z = refl

  ∨-comm : Commutative _∨_
  ∨-comm true  true  = refl
  ∨-comm true  false = refl
  ∨-comm false true  = refl
  ∨-comm false false = refl

  ∧-comm : Commutative _∧_
  ∧-comm true  true  = refl
  ∧-comm true  false = refl
  ∧-comm false true  = refl
  ∧-comm false false = refl

  distrib-∧-∨ : _∧_ DistributesOver _∨_
  distrib-∧-∨ = distˡ , distʳ
    where
    distˡ : _∧_ DistributesOverˡ _∨_
    distˡ true  y z = refl
    distˡ false y z = refl

    distʳ : _∧_ DistributesOverʳ _∨_
    distʳ x y z =
                      begin
       (y ∨ z) ∧ x
                      ≡⟨ ∧-comm (y ∨ z) x ⟩
       x ∧ (y ∨ z)
                      ≡⟨ distˡ x y z ⟩
       x ∧ y ∨ x ∧ z
                      ≡⟨ P.cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
       y ∧ x ∨ z ∧ x
                      ∎

isCommutativeSemiring-∨-∧
  : IsCommutativeSemiring _≡_ _∨_ _∧_ false true
isCommutativeSemiring-∨-∧ = record
  { +-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = P.isEquivalence
      ; assoc         = ∨-assoc
      ; ∙-cong        = P.cong₂ _∨_
      }
    ; identityˡ = λ _ → refl
    ; comm      = ∨-comm
    }
  ; *-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = P.isEquivalence
      ; assoc         = ∧-assoc
      ; ∙-cong        = P.cong₂ _∧_
      }
      ; identityˡ = λ _ → refl
    ; comm      = ∧-comm
    }
  ; distribʳ = proj₂ distrib-∧-∨
  ; zeroˡ    = λ _ → refl
  }

commutativeSemiring-∨-∧ : CommutativeSemiring _ _
commutativeSemiring-∨-∧ = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = false
  ; 1#                    = true
  ; isCommutativeSemiring = isCommutativeSemiring-∨-∧
  }

module RingSolver =
  Solver (ACR.fromCommutativeSemiring commutativeSemiring-∨-∧) _≟_

------------------------------------------------------------------------
-- (Bool, ∧, ∨, true, false) forms a commutative semiring

private

  distrib-∨-∧ : _∨_ DistributesOver _∧_
  distrib-∨-∧ = distˡ , distʳ
    where
    distˡ : _∨_ DistributesOverˡ _∧_
    distˡ true  y z = refl
    distˡ false y z = refl

    distʳ : _∨_ DistributesOverʳ _∧_
    distʳ x y z =
                          begin
       (y ∧ z) ∨ x
                          ≡⟨ ∨-comm (y ∧ z) x ⟩
       x ∨ (y ∧ z)
                          ≡⟨ distˡ x y z ⟩
       (x ∨ y) ∧ (x ∨ z)
                          ≡⟨ P.cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
       (y ∨ x) ∧ (z ∨ x)
                          ∎

isCommutativeSemiring-∧-∨
  : IsCommutativeSemiring _≡_ _∧_ _∨_ true false
isCommutativeSemiring-∧-∨ = record
  { +-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = P.isEquivalence
      ; assoc         = ∧-assoc
      ; ∙-cong        = P.cong₂ _∧_
      }
    ; identityˡ = λ _ → refl
    ; comm      = ∧-comm
    }
  ; *-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = P.isEquivalence
      ; assoc         = ∨-assoc
      ; ∙-cong        = P.cong₂ _∨_
      }
    ; identityˡ = λ _ → refl
    ; comm      = ∨-comm
    }
  ; distribʳ = proj₂ distrib-∨-∧
  ; zeroˡ    = λ _ → refl
  }

commutativeSemiring-∧-∨ : CommutativeSemiring _ _
commutativeSemiring-∧-∨ = record
  { _+_                   = _∧_
  ; _*_                   = _∨_
  ; 0#                    = true
  ; 1#                    = false
  ; isCommutativeSemiring = isCommutativeSemiring-∧-∨
  }

------------------------------------------------------------------------
-- (Bool, ∨, ∧, not, true, false) is a boolean algebra

private

  absorptive : Absorptive _∨_ _∧_
  absorptive = abs-∨-∧ , abs-∧-∨
    where
    abs-∨-∧ : _∨_ Absorbs _∧_
    abs-∨-∧ true  y = refl
    abs-∨-∧ false y = refl

    abs-∧-∨ : _∧_ Absorbs _∨_
    abs-∧-∨ true  y = refl
    abs-∧-∨ false y = refl

  not-∧-inverse : Inverse false not _∧_
  not-∧-inverse =
    ¬x∧x≡⊥ , (λ x → ∧-comm x (not x) ⟨ P.trans ⟩ ¬x∧x≡⊥ x)
    where
    ¬x∧x≡⊥ : LeftInverse false not _∧_
    ¬x∧x≡⊥ false = refl
    ¬x∧x≡⊥ true  = refl

  not-∨-inverse : Inverse true not _∨_
  not-∨-inverse =
    ¬x∨x≡⊤ , (λ x → ∨-comm x (not x) ⟨ P.trans ⟩ ¬x∨x≡⊤ x)
    where
    ¬x∨x≡⊤ : LeftInverse true not _∨_
    ¬x∨x≡⊤ false = refl
    ¬x∨x≡⊤ true  = refl

isBooleanAlgebra : IsBooleanAlgebra _≡_ _∨_ _∧_ not true false
isBooleanAlgebra = record
  { isDistributiveLattice = record
      { isLattice = record
          { isEquivalence = P.isEquivalence
          ; ∨-comm        = ∨-comm
          ; ∨-assoc       = ∨-assoc
          ; ∨-cong        = P.cong₂ _∨_
          ; ∧-comm        = ∧-comm
          ; ∧-assoc       = ∧-assoc
          ; ∧-cong        = P.cong₂ _∧_
          ; absorptive    = absorptive
          }
      ; ∨-∧-distribʳ = proj₂ distrib-∨-∧
      }
  ; ∨-complementʳ = proj₂ not-∨-inverse
  ; ∧-complementʳ = proj₂ not-∧-inverse
  ; ¬-cong        = P.cong not
  }

booleanAlgebra : BooleanAlgebra _ _
booleanAlgebra = record
  { _∨_              = _∨_
  ; _∧_              = _∧_
  ; ¬_               = not
  ; ⊤                = true
  ; ⊥                = false
  ; isBooleanAlgebra = isBooleanAlgebra
  }

------------------------------------------------------------------------
-- (Bool, xor, ∧, id, false, true) forms a commutative ring

private

  xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
  xor-is-ok true  y = refl
  xor-is-ok false y = P.sym $ proj₂ CS.*-identity _
    where module CS = CommutativeSemiring commutativeSemiring-∨-∧

commutativeRing-xor-∧ : CommutativeRing _ _
commutativeRing-xor-∧ = commutativeRing
  where
  import Algebra.Properties.BooleanAlgebra as BA
  open BA booleanAlgebra
  open XorRing _xor_ xor-is-ok

module XorRingSolver =
  Solver (ACR.fromCommutativeRing commutativeRing-xor-∧) _≟_

------------------------------------------------------------------------
-- Miscellaneous other properties

not-involutive : Involutive not
not-involutive true  = refl
not-involutive false = refl

not-¬ : ∀ {x y} → x ≡ y → x ≢ not y
not-¬ {true}  refl ()
not-¬ {false} refl ()

¬-not : ∀ {x y} → x ≢ y → x ≡ not y
¬-not {true}  {true}  x≢y = ⊥-elim (x≢y refl)
¬-not {true}  {false} _   = refl
¬-not {false} {true}  _   = refl
¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)

⇔→≡ : {b₁ b₂ b : Bool} → b₁ ≡ b ⇔ b₂ ≡ b → b₁ ≡ b₂
⇔→≡ {true } {true }         hyp = refl
⇔→≡ {true } {false} {true } hyp = P.sym (Equivalence.to hyp ⟨$⟩ refl)
⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp ⟨$⟩ refl
⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp ⟨$⟩ refl
⇔→≡ {false} {true } {false} hyp = P.sym (Equivalence.to hyp ⟨$⟩ refl)
⇔→≡ {false} {false}         hyp = refl

T-≡ : ∀ {b} → T b ⇔ b ≡ true
T-≡ {false} = equivalence (λ ())       (λ ())
T-≡ {true}  = equivalence (const refl) (const _)

T-not-≡ : ∀ {b} → T (not b) ⇔ b ≡ false
T-not-≡ {false} = equivalence (const refl) (const _)
T-not-≡ {true}  = equivalence (λ ())       (λ ())

T-∧ : ∀ {b₁ b₂} → T (b₁ ∧ b₂) ⇔ (T b₁ × T b₂)
T-∧ {true}  {true}  = equivalence (const (_ , _)) (const _)
T-∧ {true}  {false} = equivalence (λ ())          proj₂
T-∧ {false} {_}     = equivalence (λ ())          proj₁

T-∨ : ∀ {b₁ b₂} → T (b₁ ∨ b₂) ⇔ (T b₁ ⊎ T b₂)
T-∨ {true}  {b₂}    = equivalence inj₁ (const _)
T-∨ {false} {true}  = equivalence inj₂ (const _)
T-∨ {false} {false} = equivalence inj₁ [ id , id ]

proof-irrelevance : ∀ {b} (p q : T b) → p ≡ q
proof-irrelevance {true}  _  _  = refl
proof-irrelevance {false} () ()

push-function-into-if :
  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) x {y z} →
  f (if x then y else z) ≡ (if x then f y else f z)
push-function-into-if _ true  = P.refl
push-function-into-if _ false = P.refl


text:
module x03-842Relations-hc-2 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym) -- added sym
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-comm; *-comm; *-zeroʳ)

------------------------------------------------------------------------------
-- inequality : ≤

data _≤_ : ℕ → ℕ → Set where

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

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

infix 4 _≤_

_ : 2 ≤ 4 -- multiple 'refine' will do this automatically
_ = s≤s (s≤s z≤n)

_ : 2 ≤ 4 -- implicit args
_ = s≤s {1} {3} (s≤s {0} {2} z≤n)

_ : 2 ≤ 4 -- named implicit args
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} z≤n)

_ : 2 ≤ 4 -- some implicit named args
_ = s≤s {n = 3} (s≤s {m = 0} z≤n)

--------------------------------------------------
-- inversion
inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  →     m ≤     n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

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

--------------------------------------------------
-- transitive
≤-trans : ∀ {m n p : ℕ} -- note implicit arguments
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans  z≤n           n≤p  = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

≤-trans′ : ∀ (m n p : ℕ) -- without implicit arguments
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′      .0      _       _
         z≤n n≤p            = z≤n
≤-trans′ (suc m) (suc n) (suc p)
        (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)

--------------------------------------------------
-- antisymmetry

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym      z≤n       z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) rewrite ≤-antisym m≤n n≤m = refl

--------------------------------------------------
-- total ordering def with parameters

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

-- equivalent def without parameters
data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

-- prove ≤ is a total order -- using WITH
≤-total : ∀ (m n : ℕ) → Total m n
≤-total  zero        n = forward z≤n
≤-total (suc m)  zero  = flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | forward x        = forward (s≤s x)
... | flipped x        = flipped (s≤s x)

≤-total′ : ∀ (m n : ℕ) → Total m n -- using helper defined in 'where'
≤-total′  zero        n  = forward z≤n
≤-total′ (suc m)  zero   = flipped z≤n
≤-total′ (suc m) (suc n) = helper (≤-total m n)
  where
    helper : Total m n → Total (suc m) (suc n)
    helper (forward x) = forward (s≤s x)
    helper (flipped x) = flipped (s≤s x)

-- same but split on n first
≤-totalN : ∀ (m n : ℕ) → Total m n
≤-totalN      m   zero   = flipped z≤n
≤-totalN zero         n  = forward z≤n
≤-totalN (suc m) (suc n) with ≤-totalN m n
... | forward x = forward (s≤s x)
... | flipped x = flipped (s≤s x)

--------------------------------------------------
-- monotonicity of + with respect to ≤

-- inequality added on right
+-monoʳ-≤ : ∀ (m p q : ℕ)
  →     p ≤     q
    -------------
  → m + p ≤ m + q
+-monoʳ-≤  zero   p q p≤q = p≤q
+-monoʳ-≤ (suc m) p q p≤q           -- suc  m + p  ≤ suc  m + q
                                    -- suc (m + p) ≤ suc (m + q)
  = s≤s (+-monoʳ-≤ m p q p≤q)  -- can be done by refine then recurse

-- inequality added on left
+-monoˡ-≤ : ∀ (p q m : ℕ)
  → p     ≤ q
    -------------
  → p + m ≤ q + m
+-monoˡ-≤ p q m p≤q  -- p + m ≤ q + m
  rewrite
    +-comm p m       -- m + p ≤ q + m
  | +-comm q m       -- m + p ≤ m + q
  = +-monoʳ-≤ m p q p≤q

-- combine above
+-mono-≤ : ∀ (m n p q : ℕ)
  → m     ≤ n
  →     p ≤     q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q = ≤-trans (+-monoʳ-≤ m p q p≤q ) (+-monoˡ-≤ m n q m≤n)

--------------------------------------------------
-- monotonicity of *

m≤n→n≡0→n≡0 : ∀ (m : ℕ) → m ≤ zero → m ≡ 0
m≤n→n≡0→n≡0 zero m≤0 = refl

-- inequality multiplied on right
*-monoʳ-≤ : ∀ (m p q : ℕ)
  →     p ≤     q
    -------------
  → m * p ≤ m * q
*-monoʳ-≤ zero   p       q  p≤q = z≤n
*-monoʳ-≤ m   zero       q  p≤q -- m *  zero ≤ m * q
  rewrite
    *-zeroʳ m                   --         0 ≤ m * q
  = z≤n
*-monoʳ-≤ m      p    zero  p≤q -- m *     p ≤ m * zero
  rewrite
    *-zeroʳ m                   -- m *     p ≤ 0
  | m≤n→n≡0→n≡0 p p≤q           -- m *     0 ≤ 0
  | *-zeroʳ m                   --         0 ≤ 0
  = z≤n
*-monoʳ-≤ m (suc p) (suc q) p≤q -- m * suc p ≤ m * suc q
  rewrite
    *-comm m (suc p)            -- m + p * m ≤ m * suc q
  | *-comm m (suc q)            -- m + p * m ≤ m + q * m
  | *-comm p m                  -- m + m * p ≤ m + q * m
  | *-comm q m                  -- m + m * p ≤ m + m * q
  = +-monoʳ-≤ m (m * p) (m * q) (*-monoʳ-≤ m p q (inv-s≤s p≤q))

-- inequality multiplied on left
*-monoˡ-≤ : ∀ (p q m : ℕ)
  → p     ≤ q
    -------------
  → p * m ≤ q * m
*-monoˡ-≤  p q m p≤q  -- p * m ≤ q * m
  rewrite
    *-comm p m        -- m * p ≤ q * m
  | *-comm q m        -- m * p ≤ m * q
  = *-monoʳ-≤ m p q p≤q

*-mono-≤ : ∀ (m n p q : ℕ)
  → m     ≤ n
  →     p ≤     q
    -------------
  → m * p ≤ n * q
*-mono-≤ m n p q m≤n p≤q = ≤-trans (*-monoʳ-≤ m p q p≤q ) (*-monoˡ-≤ m n q m≤n)

------------------------------------------------------------------------------
-- strict inequality : <

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

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

<-trans : ∀ {m n p : ℕ}
        → m < n
        → n < p
        -------
        → m < p
<-trans  z<s    (s<s y) = z<s
<-trans (s<s x) (s<s y) = s<s (<-trans x y)

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

data Trichotomy (m n : ℕ) : Set where
  is-< : m < n → Trichotomy m n
  is-≡ : m ≡ n → Trichotomy m n
  is-> : n < m → Trichotomy m n

suc-injective : ∀ {m n : ℕ} → suc m ≡ suc n → m ≡ n
suc-injective refl = refl

m≡n→sucm≡sucn : ∀ (m n : ℕ) → m ≡ n → suc m ≡ suc n
m≡n→sucm≡sucn  zero    zero   p = refl
m≡n→sucm≡sucn  zero   (suc n) ()
m≡n→sucm≡sucn (suc m)  zero   ()
m≡n→sucm≡sucn (suc m) (suc n) p = cong suc (m≡n→sucm≡sucn m n (suc-injective p))

<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n
<-trichotomy  zero    zero   = is-≡ refl
<-trichotomy  zero   (suc n) = is-< z<s
<-trichotomy (suc m)  zero   = is-> z<s
<-trichotomy (suc m) (suc n) with <-trichotomy m n
... | is-< m<n = is-< (s<s m<n)
... | is-≡ m≡n = is-≡ (m≡n→sucm≡sucn m n m≡n)
... | is-> n<m = is-> (s<s n<m)

------------------------------------------------------------------------------
-- monotonicity of + with respect to <

-- all I did was copy the +-monoʳ-≤ proof and replace ≤ with < - it worked
-- inequality added on right
+-monoʳ-< : ∀ (m p q : ℕ)
  →     p <     q
    -------------
  → m + p < m + q
+-monoʳ-<  zero   p q p<q = p<q
+-monoʳ-< (suc m) p q p<q
  = s<s (+-monoʳ-< m p q p<q)

-- inequality added on left
+-monoˡ-< : ∀ (p q m : ℕ)
  → p     < q
    -------------
  → p + m < q + m
+-monoˡ-< p q m p<q
  rewrite
    +-comm p m
  | +-comm q m
  = +-monoʳ-< m p q p<q

-- combine above
+-mono-< : ∀ (m n p q : ℕ)
  → m     < n
  →     p <     q
    -------------
  → m + p < n + q
+-mono-< m n p q m<n p<q = <-trans (+-monoʳ-< m p q p<q ) (+-monoˡ-< m n q m<n)

------------------------------------------------------------------------------
-- Proofs showing relation between strict inequality and inequality.
-- (Do the proofs in the order below, to avoid induction for two of the four proofs.)

--------------------------------------------------
-- turn ≤ into <

≤-<-to : ∀ {m n : ℕ}
       → m ≤     n
       → m < suc n
≤-<-to  {zero}  {zero}  z≤n      = z<s
≤-<-to  {zero} {suc n}  z≤n      = z<s
≤-<-to {suc m} {suc n} (s≤s m≤n) = s<s (≤-<-to m≤n)
--- removing unneeded stuff
≤-<-to' : ∀ {m n : ℕ}
        → m ≤     n
        → m < suc n
≤-<-to'                 z≤n      = z<s
≤-<-to'                (s≤s m≤n) = s<s (≤-<-to' m≤n)

≤-<--to′ : ∀ {m n : ℕ}
         → suc m ≤ n
         →     m < n
≤-<--to′ (s≤s sm≤n) = ≤-<-to sm≤n

--------------------------------------------------
-- turn < into ≤

≤-<-from : ∀ {m n : ℕ}
         →     m < n
         → suc m ≤ n
≤-<-from  z<s      = s≤s z≤n
≤-<-from (s<s m<n) = s≤s (≤-<-from m<n)

≤-<-from′ : ∀ {m n : ℕ}
          → m < suc n
          → m ≤     n
≤-<-from′  z<s       = z≤n
≤-<-from′ (s<s m<sn) = ≤-<-from m<sn

------------------------------------------------------------------------------
-- use the above to give a proof of <-trans that uses ≤-trans

m<n→m<sucn : ∀ {m n : ℕ} → m < n → m < suc n
m<n→m<sucn  z<s      = z<s
m<n→m<sucn (s<s m<n) = s<s (m<n→m<sucn m<n)

<-trans' : ∀ {m n p : ℕ}
        → m < n
        →     n < p
        -------
        → m <     p
<-trans' m<n n<p = ≤-<--to′ (≤-trans (≤-<-from m<n) ( ≤-<-from′ (m<n→m<sucn n<p)))

------------------------------------------------------------------------------
-- Mutually recursive datatypes. Specify types first, then definitions.

data even : ℕ → Set
data odd  : ℕ → Set

-- HC : added 'E' suffix to constructors
data even where

  zeroE :
      ---------
      even zero

  sucE  : ∀ {n : ℕ}
    → odd       n
      ------------
    → even (suc n)

-- HC : added 'O' suffix to constructor
data odd where

  sucO   : ∀ {n : ℕ}
    → even     n
      -----------
    → odd (suc n)

-------------------------
-- Mutually recursive proofs.  Specify types first, then implementations.

e+e≡e : ∀ {m n : ℕ}
  → even  m
  → even      n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd  m
  → even     n
    -----------
  → odd (m + n)

e+e≡e  zeroE   en =               en
e+e≡e (sucE x) en = sucE (o+e≡o x en)

o+e≡o (sucO x) en = sucO (e+e≡e x en)

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

o+o≡e : ∀ {m n : ℕ}
  → odd   m
  → odd       n
  --------------
  → even (m + n)

e+o≡o : ∀ {m n : ℕ}
  → even m
  → odd      n
    -----------
  → odd (m + n)

e+o≡o  zeroE   on = on
e+o≡o (sucE m) (sucO n) = sucO (o+o≡e m (sucO n))

o+o≡e (sucO m) on = sucE (e+o≡o m on)

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:
-- Andreas, 2012-04-03, reported by pumpkingod
module Issue596 where

import Common.Irrelevance
open import Common.Level
open import Common.Equality
open import Common.Prelude renaming (Nat to ℕ)

infixl 7 _*_

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

-- inlined from Data.Product

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁
open Σ public

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

infixr 2 _×_

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ x ∶ A ] B

-- inlined from Data.Nat.Divisibility and Data.Nat.Coprimality

infix 4 _∣_

data _∣_ : ℕ → ℕ → Set where
  divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n

Coprime : (m n : ℕ) → Set
Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1

record ℚ⁺ : Set where
  constructor rat⁺
  field
    numerator     : ℕ
    denominator-1 : ℕ

  denominator : ℕ
  denominator = suc denominator-1

  field
    .coprime      : Coprime numerator denominator

-- inlined from Data.Nat.LCM

record LCM (i j lcm : ℕ) : Set where
  constructor is -- Andreas, 2012-04-02 added constructor
  field
    -- The lcm is a common multiple.
    commonMultiple : i ∣ lcm × j ∣ lcm

    -- The lcm divides all common multiples, i.e. the lcm is the least
    -- common multiple according to the partial order _∣_.
    least : ∀ {m} → i ∣ m × j ∣ m → lcm ∣ m

postulate
  lcm : (i j : ℕ) → ∃ λ d → LCM i j d
  undefined : ∀ {a}{A : Set a} → A

0#⁺ : ℚ⁺
0#⁺ = rat⁺ 0 0 undefined -- (∣1⇒≡1 ∘ proj₂)

_+⁺_ : ℚ⁺ → ℚ⁺ → ℚ⁺
_+⁺_ = undefined

-- the offending with-clause
+⁺-idˡ : ∀ q → 0#⁺ +⁺ q ≡ q
+⁺-idˡ (rat⁺ n d c) with lcm (suc zero) (suc d)
...                | q = undefined

-- should succeed

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Structure.Categorical.Properties where

import      Functional.Dependent as Fn
open import Lang.Instance
import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Structure.Setoid
import      Structure.Categorical.Names as Names
import      Structure.Operator.Names as Names
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Syntax.Function
open import Type
open import Type.Properties.Singleton

private variable ℓₒ ℓₘ ℓₑ : Lvl.Level
private variable Obj : Type{ℓₒ}

module Object where
  module _ (Morphism : Obj → Obj → Type{ℓₘ}) where
    open Names.ArrowNotation(Morphism)

    module _ ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(x ⟶ y) ⦄ where
      -- An initial object is an object in which there is an unique morphism from it to every object.
      Initial : Obj → Stmt
      Initial(x) = (∀{y} → IsUnit(x ⟶ y))

      -- An terminal object is an object in which there is an unique morphism to it from every object.
      Terminal : Obj → Stmt
      Terminal(y) = (∀{x} → IsUnit(x ⟶ y))

module Morphism where
  module _ {Morphism : Obj → Obj → Type{ℓₘ}} ⦃ equiv-morphism : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄ where
    open Names.ArrowNotation(Morphism)

    module OperModule (_▫_ : Names.SwappedTransitivity(_⟶_)) where
      record Associativity : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
        constructor intro
        field proof : Names.Morphism.Associativity{Morphism = Morphism}(_▫_)
      associativity = inst-fn Associativity.proof

      module _ {x : Obj} (f : x ⟶ x) where
        record Idempotent : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
          constructor intro
          field proof : Names.Morphism.Idempotent{Morphism = Morphism}(_▫_)(f)
        idempotent = inst-fn Idempotent.proof

      module IdModule (id : Names.Reflexivity(_⟶_)) where
        record Identityₗ : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
          constructor intro
          field proof : Names.Morphism.Identityₗ(_▫_)(\{a} → id{a})
        identityₗ = inst-fn Identityₗ.proof

        record Identityᵣ : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
          constructor intro
          field proof : Names.Morphism.Identityᵣ(_▫_)(\{a} → id{a})
        identityᵣ = inst-fn Identityᵣ.proof

        Identity = Identityₗ ∧ Identityᵣ
        identity-left  = inst-fn{X = Identity}(Identityₗ.proof Fn.∘ [∧]-elimₗ{Q = Identityᵣ})
        identity-right = inst-fn{X = Identity}(Identityᵣ.proof Fn.∘ [∧]-elimᵣ{P = Identityₗ})

        module _ {x : Obj} (f : x ⟶ x) where
          record Involution : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
            constructor intro
            field proof : Names.Morphism.Involution{Morphism = Morphism}(_▫_)(id)(f)
          involution = inst-fn Involution.proof

        module _ {x y : Obj} (f : x ⟶ y) where
          module _ (f⁻¹ : y ⟶ x) where
            -- A morphism have a right inverse morphism.
            -- Also called: Split monomorphism, retraction
            record Inverseₗ : Stmt{ℓₘ Lvl.⊔ ℓₑ} where
              constructor intro
              field proof : Names.Morphism.Inverseₗ(_▫_)(\{a} → id{a})(f)(f⁻¹)
            inverseₗ = inst-fn Inverseₗ.proof

            -- A morphism have a right inverse morphism.
            -- Also called: Split epimorphism, section
            record Inverseᵣ : Stmt{ℓₘ Lvl.⊔ ℓₑ} where
              constructor intro
              field proof : Names.Morphism.Inverseᵣ(_▫_)(\{a} → id{a})(f)(f⁻¹)
            inverseᵣ = inst-fn Inverseᵣ.proof

            Inverse = Inverseₗ ∧ Inverseᵣ
            module Inverse(inverse : Inverse) where
              instance
                left : Inverseₗ
                left = [∧]-elimₗ inverse

              instance
                right : Inverseᵣ
                right = [∧]-elimᵣ inverse

          Invertibleₗ = ∃(Inverseₗ)
          Invertibleᵣ = ∃(Inverseᵣ)

          -- A morphism is an isomorphism when it is invertible with respect to the operator.
          -- For the set and functions category, it means that f is bijective.
          Isomorphism : Stmt
          Isomorphism = ∃(Inverse)
          module Isomorphism ⦃ iso : Isomorphism ⦄ where
            instance inverse = [∃]-proof iso
            instance inverse-left  = [∧]-elimₗ inverse
            instance inverse-right = [∧]-elimᵣ inverse

          inv : ⦃ Isomorphism ⦄ → (y ⟶ x)
          inv ⦃ p ⦄ = [∃]-witness p

        -- Proposition stating that two objects are isomorphic.
        Isomorphic : Obj → Obj → Stmt
        Isomorphic(x)(y) = ∃(Isomorphism{x}{y})
        _⤖_ = Isomorphic

        module _ {x : Obj} (f : ⟲ x) where
          -- A morphism is an automorphism when it is an endomorphism and an isomorphism.
          Automorphism : Stmt
          Automorphism = Isomorphism(f)

        Automorphic : Obj → Stmt
        Automorphic(x) = ∃(Automorphism{x})

      module _ {x y : Obj} (f : x ⟶ y) where
        -- A morphism is an monomorphism when it is left-cancellable ("injective").
        -- ∀{z}{g₁ g₂ : z ⟶ x} → (f ∘ g₁ ≡ f ∘ g₂) → (g₁ ≡ g₂)
        record Monomorphism : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
          constructor intro
          field
            proof : ∀{z} → Names.CancellationOnₗ {T₂ = z ⟶ x} (_▫_) (f)
        cancellationₗ = inst-fn Monomorphism.proof

        -- A morphism is an epimorphism when it is right-cancellable ("surjective").
        -- ∀{z}{g₁ g₂ : y ⟶ z} → (g₁ ∘ f ≡ g₂ ∘ f) → (g₁ ≡ g₂)
        record Epimorphism : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
          constructor intro
          field
            proof : ∀{z} → Names.CancellationOnᵣ {T₁ = y ⟶ z} (_▫_) (f)
        cancellationᵣ = inst-fn Epimorphism.proof

      -- Proposition stating that two objects are monomorphic.
      Monomorphic : Obj → Obj → Stmt
      Monomorphic(x)(y) = ∃(Monomorphism{x}{y})
      _↣_ = Monomorphic

      -- Proposition stating that two objects are epimorphic.
      Epimorphic : Obj → Obj → Stmt
      Epimorphic(x)(y) = ∃(Epimorphism{x}{y})
      _↠_ = Epimorphic

    open OperModule public
    open IdModule   public

module Polymorphism where
  module _ {Morphism : Obj → Obj → Type{ℓₘ}} ⦃ equiv-morphism : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄ where
    open Names.ArrowNotation(Morphism)

    module OperModule (_▫_ : Names.SwappedTransitivity(_⟶_)) where
      module _ (x y : Obj) (f : ∀{x y} → (x ⟶ y)) where
        record IdempotentOn : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
          constructor intro
          field proof : Names.Polymorphism.IdempotentOn{Morphism = Morphism}(_▫_)(x)(y)(f)
        idempotent-on = inst-fn IdempotentOn.proof

      module IdModule (id : Names.Reflexivity(_⟶_)) where
        module _ (x y : Obj) (f : ∀{x y} → (x ⟶ y)) where
          record InvolutionOn : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
            constructor intro
            field proof : Names.Polymorphism.InvolutionOn{Morphism = Morphism}(_▫_)(id) (x)(y) (f)
          involution-on = inst-fn InvolutionOn.proof

        module _ (f : ∀{x y} → (x ⟶ y)) where
          record Involution : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
            constructor intro
            field proof : Names.Polymorphism.Involution{Morphism = Morphism}(_▫_)(id)(f)
          involution = inst-fn Involution.proof

        module _ (inv : ∀{x y : Obj} → (x ⟶ y) → (y ⟶ x)) where
          -- A morphism have a right inverse morphism.
          -- Also called: Split monomorphism, retraction
          record Inverterₗ : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
            constructor intro
            field proof : ∀{x y : Obj}{f : x ⟶ y} → Names.Morphism.Inverseₗ(_▫_)(\{a} → id{a})(f)(inv f)
            instance
              inverseₗ : ∀{x y : Obj}{f : x ⟶ y} → Morphism.Inverseₗ(_▫_)(\{x} → id{x})(f)(inv f)
              inverseₗ = Morphism.intro proof

          inverterₗ = inst-fn Inverterₗ.proof

          -- A morphism have a right inverse morphism.
          -- Also called: Split epimorphism, section
          record Inverterᵣ : Stmt{Lvl.of(Obj) Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
            constructor intro
            field proof : ∀{x y : Obj}{f : x ⟶ y} → Names.Morphism.Inverseᵣ(_▫_)(\{a} → id{a})(f)(inv f)
            instance
              inverseᵣ : ∀{x y : Obj}{f : x ⟶ y} → Morphism.Inverseᵣ(_▫_)(\{x} → id{x})(f)(inv f)
              inverseᵣ = Morphism.intro proof
          inverterᵣ = inst-fn Inverterᵣ.proof

          Inverter = Inverterₗ ∧ Inverterᵣ
          module Inverter(inverter : Inverter) where
            instance
              left : Inverterₗ
              left = [∧]-elimₗ inverter
            open Inverterₗ(left) public

            instance
              right : Inverterᵣ
              right = [∧]-elimᵣ inverter
            open Inverterᵣ(right) public

            module _ {x y : Obj} {f : x ⟶ y} where
              instance
                inverse : Morphism.Inverse(_▫_)(\{x} → id{x})(f)(inv f)
                inverse = [∧]-intro inverseₗ inverseᵣ
              open Morphism.Inverse(_▫_)(\{x} → id{x})(f)(inv f)(inverse) renaming (left to inverseₗ ; right to inverseᵣ)

            invertibleₗ : ∀{x y : Obj}{f : x ⟶ y} → Morphism.Invertibleₗ(_▫_)(\{x} → id{x})(f)
            invertibleₗ {f = f} = [∃]-intro (inv f) ⦃ inverseₗ ⦄

            invertibleᵣ : ∀{x y : Obj}{f : x ⟶ y} → Morphism.Invertibleᵣ(_▫_)(\{x} → id{x})(f)
            invertibleᵣ {f = f} = [∃]-intro (inv f) ⦃ inverseᵣ ⦄

            isomorphism : ∀{x y : Obj}{f : x ⟶ y} → Morphism.Isomorphism(_▫_)(\{x} → id{x})(f)
            isomorphism {f = f} = [∃]-intro (inv f) ⦃ inverse ⦄

    open OperModule public
    open IdModule   public


text:
open import Relation.Unary
open import Relation.Ternary.Separation

module Relation.Ternary.Separation.Monad.Error {ℓ} {A : Set ℓ}
  {{r : RawSep A}}
  {u} {{_ : IsUnitalSep r u}}
  where

open import Level
open import Function
open import Data.Unit
open import Data.Sum
open import Relation.Unary renaming (U to True)
open import Relation.Unary.PredicateTransformer using (PT; Pt)
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Binary.PropositionalEquality

module _ where
  record ExceptT (M : Pt A ℓ) (E : Set ℓ) (P : Pred A ℓ) (Φ : A) : Set ℓ where
    constructor partial
    field
      runErr : M ((λ _ → E) ∪ P) Φ

  open ExceptT public

  open import Relation.Ternary.Separation.Monad.Identity

  Except : ∀ E → Pt A ℓ
  Except E = ExceptT Identity.Id E

  pattern error e = partial (inj₁ e)
  pattern ✓ x     = partial (inj₂ x)

  data Err : Set ℓ where
    err : Err

  ErrorT : (M : Pt A ℓ) {{monad : Monads.Monad ⊤ ℓ (λ _ _ → M) }} → Pt A ℓ
  ErrorT M = ExceptT M Err

  open import Relation.Ternary.Separation.Monad.Identity

  Error : Pt A ℓ
  Error = ErrorT Identity.Id

module ExceptTrans
  (M : Pt A ℓ)
  {{monad : Monads.Monad ⊤ ℓ (λ _ _ → M) }}
  (Exc : Set ℓ) where

  open Monads

  instance
    except-monad : Monad ⊤ ℓ (λ _ _ → ExceptT M Exc)
    runErr (Monad.return except-monad px) =
      return (inj₂ px)
    runErr (app (Monad.bind except-monad f) (partial mpx) σ) = do
      inj₂ px ×⟨ σ₂ ⟩ f ← mpx &⟨ _ ─✴ _ ∥ ⊎-comm σ ⟩ f
        where
          (inj₁ e ×⟨ σ₂ ⟩ f) → return (inj₁ e)
      case app f px (⊎-comm σ₂) of λ where
        (partial z) → z

  mapExc : ∀ {E₁ E₂ P} → (E₁ → E₂) → ∀[ ExceptT M E₁ P ⇒ ExceptT M E₂ P ]
  mapExc f (partial mc) = partial (mapM mc λ where (inj₁ e) → inj₁ (f e); (inj₂ px) → inj₂ px)

module ExceptMonad (Exc : Set ℓ) where
  open import Relation.Ternary.Separation.Monad.Identity
  open ExceptTrans Identity.Id {{ Identity.id-monad }} Exc public

module ErrorTrans (M : Pt A ℓ) {{monad : Monads.Monad ⊤ ℓ (λ _ _ → M) }} where
  open import Relation.Ternary.Separation.Monad.Identity
  open ExceptTrans M {{ monad }} Err public
    renaming (except-monad to error-monad)

module ErrorMonad where
  open import Relation.Ternary.Separation.Monad.Identity
  open ExceptTrans Identity.Id {{ Identity.id-monad }} Err public
    renaming (except-monad to error-monad)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
{-
  This is inspired by/copied from:
  https://github.com/agda/agda-stdlib/blob/master/src/Tactic/MonoidSolver.agda
-}
module Cubical.Algebra.RingSolver.ReflectionSolving where

open import Cubical.Foundations.Prelude hiding (Type)
open import Cubical.Functions.Logic

open import Agda.Builtin.Reflection hiding (Type)
open import Agda.Builtin.String

open import Cubical.Reflection.Base

open import Cubical.Data.Maybe
open import Cubical.Data.Sigma
open import Cubical.Data.List
open import Cubical.Data.Nat.Literals public
open import Cubical.Data.Int using (fromNegInt; fromNatInt) public
open import Cubical.Data.Nat using (ℕ) renaming (_+_ to _+ℕ_)
open import Cubical.Data.FinData using () renaming (zero to fzero; suc to fsuc) public
open import Cubical.Data.Bool
open import Cubical.Data.Bool.SwitchStatement
open import Cubical.Data.Vec using (Vec) renaming ([] to emptyVec; _∷_ to _∷vec_) public

open import Cubical.Algebra.RingSolver.AlgebraExpression public
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.RawAlgebra
open import Cubical.Algebra.RingSolver.IntAsRawRing
open import Cubical.Algebra.RingSolver.CommRingSolver renaming (solve to ringSolve)

private
  variable
    ℓ : Level

  _==_ = primQNameEquality
  {-# INLINE _==_ #-}

  record VarInfo : Type ℓ-zero where
    field
      varName : String
      varType : Arg Term
      index : ℕ

  getArgs : Term → Maybe (Term × Term)
  getArgs (def n xs) =
    if n == (quote PathP)
    then go xs
    else nothing
      where
      go : List (Arg Term) → Maybe (Term × Term)
      go (varg x ∷ varg y ∷ []) = just (x , y)
      go (x ∷ xs)               = go xs
      go _                      = nothing
  getArgs _ = nothing

  constructSolution : ℕ → List VarInfo → Term → Term → Term → Term
  constructSolution n varInfos R lhs rhs =
    encloseWithIteratedLambda (map VarInfo.varName varInfos) solverCall
    where
      encloseWithIteratedLambda : List String → Term → Term
      encloseWithIteratedLambda (varName ∷ xs) t = lam visible (abs varName (encloseWithIteratedLambda xs t))
      encloseWithIteratedLambda [] t = t

      variableList : List VarInfo → Arg Term
      variableList [] = varg (con (quote emptyVec) [])
      variableList (varInfo ∷ varInfos)
        = varg (con (quote _∷vec_) (varg (var (VarInfo.index varInfo) []) ∷ (variableList varInfos) ∷ []))

      solverCall = def
         (quote ringSolve)
         (varg R ∷ varg lhs ∷ varg rhs
           ∷ variableList (rev varInfos)
           ∷ varg (def (quote refl) []) ∷ [])

module pr (R : CommRing {ℓ}) {n : ℕ} where
  private
    νR = CommRing→RawℤAlgebra R

  open CommRingStr (snd R)

  0' : Expr ℤAsRawRing (fst R) n
  0' = K 0

  1' : Expr ℤAsRawRing (fst R) n
  1' = K 1

module _ (cring : Term) where
  private
    νR = def (quote CommRing→RawℤAlgebra) (varg cring ∷ [])

  open pr

  mutual
    `0` : List (Arg Term) → Term
    `0` [] = def (quote 0') (varg cring ∷ [])
    `0` (varg fstcring ∷ xs) = `0` xs
    `0` (harg _ ∷ xs) = `0` xs
    `0` _ = unknown

    `1` : List (Arg Term) → Term
    `1` [] = def (quote 1') (varg cring ∷ [])
    `1` (varg fstcring ∷ xs) = `1` xs
    `1` (harg _ ∷ xs) = `1` xs
    `1` _ = unknown

    `_·_` : List (Arg Term) → Term
    `_·_` (harg _ ∷ xs) = `_·_` xs
    `_·_` (varg _ ∷ varg x ∷ varg y ∷ []) =
      con
        (quote _·'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
    `_·_` _ = unknown

    `_+_` : List (Arg Term) → Term
    `_+_` (harg _ ∷ xs) = `_+_` xs
    `_+_` (varg _ ∷ varg x ∷ varg y ∷ []) =
      con
        (quote _+'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
    `_+_` _ = unknown

    `-_` : List (Arg Term) → Term
    `-_` (harg _ ∷ xs) = `-_` xs
    `-_` (varg _ ∷ varg x ∷ []) =
      con
        (quote -'_) (varg (buildExpression x) ∷ [])
    `-_` _ = unknown

    K' : List (Arg Term) → Term
    K' xs = con (quote K) xs

    finiteNumberAsTerm : ℕ → Term
    finiteNumberAsTerm ℕ.zero = con (quote fzero) []
    finiteNumberAsTerm (ℕ.suc n) = con (quote fsuc) (varg (finiteNumberAsTerm n) ∷ [])

    buildExpression : Term → Term
    buildExpression (var index _) = con (quote ∣) (varg (finiteNumberAsTerm index) ∷ [])
    buildExpression t@(def n xs) =
      switch (n ==_) cases
        case (quote CommRingStr.0r)  ⇒ `0` xs     break
        case (quote CommRingStr.1r)  ⇒ `1` xs     break
        case (quote CommRingStr._·_) ⇒ `_·_` xs   break
        case (quote CommRingStr._+_) ⇒ `_+_` xs   break
        case (quote (CommRingStr.-_))  ⇒ `-_` xs    break
        default⇒ (K' xs)
    buildExpression t@(con n xs) =
      switch (n ==_) cases
        case (quote CommRingStr.0r)  ⇒ `0` xs     break
        case (quote CommRingStr.1r)  ⇒ `1` xs     break
        case (quote CommRingStr._·_) ⇒ `_·_` xs   break
        case (quote CommRingStr._+_) ⇒ `_+_` xs   break
        case (quote (CommRingStr.-_))  ⇒ `-_` xs    break
        default⇒ (K' xs)
    buildExpression t = unknown

  toAlgebraExpression : Maybe (Term × Term) → Maybe (Term × Term)
  toAlgebraExpression nothing = nothing
  toAlgebraExpression (just (lhs , rhs)) = just (buildExpression lhs , buildExpression rhs)

private
  adjustDeBruijnIndex : (n : ℕ) → Term → Term
  adjustDeBruijnIndex n (var k args) = var (k +ℕ n) args
  adjustDeBruijnIndex n _ = unknown

  getVarsAndEquation : Term → Maybe (List VarInfo × Term)
  getVarsAndEquation t =
    let
      (rawVars , equationTerm) = extractVars t
      maybeVars = addIndices (length rawVars) rawVars
    in map-Maybe (_, equationTerm) maybeVars
    where
          extractVars : Term → List (String × Arg Term) × Term
          extractVars (pi argType (abs varName t)) with extractVars t
          ...                                         | xs , equation = (varName , argType) ∷ xs , equation
          extractVars equation = [] , equation

          addIndices : ℕ → List (String × Arg Term) → Maybe (List VarInfo)
          addIndices ℕ.zero         []        = just []
          addIndices (ℕ.suc countVar) ((varName , argType) ∷ list) =
            map-Maybe (λ varList → record { varName = varName ; varType = argType ; index = countVar }
                                   ∷ varList)
                      (addIndices countVar list)
          addIndices _ _ = nothing

  solve-macro : Term → Term → TC Unit
  solve-macro cring hole = do
    hole′ ← inferType hole >>= normalise
    just (varInfos , equation) ← returnTC (getVarsAndEquation hole′)
      where
        nothing
          → typeError (strErr "Something went wrong when getting the variable names in "
                         ∷ termErr hole′ ∷ [])
    adjustedCring ← returnTC (adjustDeBruijnIndex (length varInfos) cring)
    just (lhs , rhs) ← returnTC (toAlgebraExpression adjustedCring (getArgs equation))
      where
        nothing
          → typeError(
              strErr "Error while trying to buils ASTs for the equation " ∷
              termErr equation ∷ [])
    let solution = constructSolution (length varInfos) varInfos adjustedCring lhs rhs
    unify hole solution

macro
  solve : Term → Term → TC _
  solve = solve-macro

fromℤ : (R : CommRing {ℓ}) → ℤ → fst R
fromℤ = scalar

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.MaybeEmbed

open import Tools.Unit as TU
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Validity of the Empty type.
Emptyᵛ : ∀ {Γ ll l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ Empty ll ^ [ % , ι ll ] / [Γ]
Emptyᵛ [Γ] ⊢Δ [σ] = Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ))) , λ _ x₂ → id (univ (Emptyⱼ ⊢Δ))

-- Validity of the Empty type as a term.
Emptyᵗᵛ : ∀ {Γ l ll} ([Γ] : ⊩ᵛ Γ) → (l< : ι ll <∞ l)
    → Γ ⊩ᵛ⟨ l ⟩ Empty ll ∷ Univ % ll ^ [ ! , next ll ]  / [Γ] / Uᵛ l< [Γ]
Emptyᵗᵛ {ll = ll} [Γ] emb< ⊢Δ [σ] = let ⊢Empty  = Emptyⱼ ⊢Δ
                       in  Uₜ (Empty ll) (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) (λ x ⊢Δ' → Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ'))))
                           , λ x x₁ → Uₜ₌ -- Empty Empty (idRedTerm:*: ⊢Empty) (idRedTerm:*: ⊢Empty) Emptyₙ Emptyₙ
                                   (Uₜ (Empty ll) (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) (λ x₂ ⊢Δ' → Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ')))))
                                   (Uₜ (Empty ll) (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) (λ x₂ ⊢Δ' → Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ')))))
                                   (≅ₜ-Emptyrefl ⊢Δ) λ [ρ] ⊢Δ' → id (univ (Emptyⱼ ⊢Δ'))
Emptyᵗᵛ {ll = ll} [Γ] ∞< ⊢Δ [σ] = let ⊢Empty  = Emptyⱼ ⊢Δ
                       in  Uₜ (Empty ll) (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) (λ x ⊢Δ' → Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ'))))
                           , λ x x₁ → Uₜ₌ -- Empty Empty (idRedTerm:*: ⊢Empty) (idRedTerm:*: ⊢Empty) Emptyₙ Emptyₙ
                                   (Uₜ (Empty ll) (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) (λ x₂ ⊢Δ' → Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ')))))
                                   (Uₜ (Empty ll) (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) (λ x₂ ⊢Δ' → Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Δ')))))
                                   (≅ₜ-Emptyrefl ⊢Δ) λ [ρ] ⊢Δ' → id (univ (Emptyⱼ ⊢Δ'))

Unitᵗᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ ∞ ⟩ Unit ∷ (SProp l) ^ [ ! , next l ] / [Γ] / maybeEmbᵛ {A = SProp l} [Γ] (Uᵛ (proj₂ (levelBounded _)) [Γ])
Unitᵗᵛ {Γ} {l} [Γ] = let [SProp] = maybeEmbᵛ {A = SProp l} [Γ] (Uᵛ {rU = %} (proj₂ (levelBounded _)) [Γ])
                         [Empty] = Emptyᵛ {ll = l} {l = ∞} [Γ]
                         [Γ∙Empty] = (_∙_ {Γ} {Empty l} [Γ] [Empty])
                         [SProp]₁ : Γ ∙ Empty l ^ [ % , ι l ] ⊩ᵛ⟨ ∞ ⟩ (SProp l) ^ [ ! , next l ] / [Γ∙Empty]
                         [SProp]₁ {Δ} {σ} = maybeEmbᵛ {A = SProp l} [Γ∙Empty] (λ {Δ} {σ} → Uᵛ (proj₂ (levelBounded _)) [Γ∙Empty] {Δ} {σ}) {Δ} {σ}
                         [Empty]₁ = maybeEmbTermᵛ {A = SProp l} {t = Empty l} [Γ] (Uᵛ {rU = %} (proj₂ (levelBounded _)) [Γ]) (Emptyᵗᵛ {ll = l} [Γ] (proj₂ (levelBounded _)))
                         [Empty]₂ = maybeEmbTermᵛ {A = SProp l} {t = Empty l} [Γ∙Empty] (λ {Δ} {σ} → Uᵛ (proj₂ (levelBounded _)) [Γ∙Empty] {Δ} {σ}) (Emptyᵗᵛ {ll = l} [Γ∙Empty] (proj₂ (levelBounded _)))
                in maybeEmbTermᵛ {A = SProp l} {t = Unit} [Γ] [SProp]
                                 (Πᵗᵛ {Empty l} {Empty l} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] ( Emptyᵛ {ll = l} [Γ]) (λ {Δ} {σ} → [SProp]₁ {Δ} {σ}) [Empty]₁ (λ {Δ} {σ} → [Empty]₂ {Δ} {σ}))

Unit≡Unit : ∀ {Γ l} (⊢Γ : ⊢ Γ)
          → Γ ⊢ Unit {l} ≅ Unit {l} ∷ SProp l ^ [ ! , next l ]
Unit≡Unit ⊢Γ = ≅ₜ-Π-cong (≡is≤ PE.refl) (≡is≤ PE.refl) (univ (Emptyⱼ ⊢Γ)) (≅ₜ-Emptyrefl ⊢Γ) (≅ₜ-Emptyrefl (⊢Γ ∙ univ (Emptyⱼ ⊢Γ)))

Unitᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ ι l ⟩ Unit ^ [ % , ι l ] / [Γ]
Unitᵛ {Γ} {l} [Γ] = univᵛ {A = Unit} [Γ] (≡is≤ PE.refl) (maybeEmbᵛ {A = SProp l} [Γ] (Uᵛ {rU = %} (proj₂ (levelBounded _)) [Γ])) (Unitᵗᵛ {l = l} [Γ])

UnitType : ∀ {Γ l} (⊢Γ : ⊢ Γ) → Γ ⊩⟨ ι l ⟩ Unit ^ [ % , ι l ]
UnitType {Γ} ⊢Γ = proj₁ (Unitᵛ ε {Γ} {idSubst} ⊢Γ TU.tt)

EmptyType : ∀ {Γ l} (⊢Γ : ⊢ Γ) → Γ ⊩⟨ ι l ⟩ Empty l ^ [ % , ι l ]
EmptyType {Γ} ⊢Γ = proj₁ (Emptyᵛ ε {Γ} {idSubst} ⊢Γ TU.tt)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
-- Andreas, 2016-02-02 postpone type checking of extended lambda
-- See also issue 480 and 1159

open import Common.Maybe
open import Common.String

record ⊤ : Set where

record IOInterface : Set₁ where
  field  Command   :  Set
         Response  :  (m : Command) → Set
open IOInterface

data IO I A : Set where
  act'     :  (c : Command I) (f : Response I c → IO I A)  → IO I A
  return   :  (a : A)                                      → IO I A

-- Alias of constructor which is a function
act :  ∀{I A} (c : Command I) (f : Response I c → IO I A) → IO I A
act c f    =  act' c f

data C : Set where
  getLine   :  C
  putStrLn  :  String → C

R : C → Set
R  getLine      =  Maybe String
R (putStrLn s)  =  ⊤

I : IOInterface
Command   I  =  C
Response  I  =  R

works : IO I ⊤
works = act'  getLine        λ{ nothing → return _ ; (just line) →
        act (putStrLn line)  λ _ →
        return _            }

test : IO I ⊤
test = act  getLine         λ{ nothing → return _ ; (just line) →
       act (putStrLn line)  λ _ →
       return _            }

-- Test with do-notation

_>>=_ : ∀ {A B} → IO I A → (A → IO I B) → IO I B
act' c f >>= k = act' c λ x → f x >>= k
return a >>= k = k a

_>>_ : ∀ {A B} → IO I A → IO I B → IO I B
m >> m' = m >>= λ _ → m'

getLineIO : IO I (Maybe String)
getLineIO = act' getLine return

putStrLnIO : String → IO I ⊤
putStrLnIO s = act' (putStrLn s) return

works' : IO I ⊤
works' = do
  just line ← getLineIO where nothing → return _
  putStrLnIO line
  return _

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
open import Prelude

module Implicits.Semantics where

open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Semantics.Type public
open import Implicits.Semantics.Context public
open import Implicits.Semantics.RewriteContext public
open import Implicits.Semantics.Term public
open import Implicits.Semantics.Preservation public

open import SystemF.Everything as F using ()

module Semantics
  (_⊢ᵣ_ : ∀ {ν} → ICtx ν → Type ν → Set)
  (⟦_,_⟧r : ∀ {ν n} {K : Ktx ν n} {a} → (proj₂ K) ⊢ᵣ a → K# K →
            ∃ λ t → ⟦ proj₁ K ⟧ctx→ F.⊢ t ∈ ⟦ a ⟧tp→) where

  open TypingRules _⊢ᵣ_
  open TermSemantics _⊢ᵣ_ ⟦_,_⟧r public
  open Preservation _⊢ᵣ_ ⟦_,_⟧r public


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
-}
{-# OPTIONS --allow-unsolved-metas #-}

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

open import Optics.All
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.RoundManager.Properties
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Util.Util
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Types
open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})

module LibraBFT.Impl.Handle.Properties where
  open import LibraBFT.Impl.Consensus.RoundManager
  open import LibraBFT.Impl.Handle

  -- This proof is complete except for pieces that are directly about the handlers.  Our
  -- fake/simple handler does not yet obey the needed properties, so we can't finish this yet.
  impl-sps-avp : StepPeerState-AllValidParts
  -- In our fake/simple implementation, init and handling V and C msgs do not send any messages
  impl-sps-avp _ hpk (step-init _) m∈outs part⊂m ver         = ⊥-elim (¬Any[] m∈outs)
  impl-sps-avp _ hpk (step-msg {sndr , V vm} _ _) m∈outs _ _ = ⊥-elim (¬Any[] m∈outs)
  impl-sps-avp _ hpk (step-msg {sndr , C cm} _ _) m∈outs _ _ = ⊥-elim (¬Any[] m∈outs)
  -- These aren't true yet, because processProposalMsgM sends fake votes that don't follow the rules for ValidPartForPK
  impl-sps-avp preach hpk (step-msg {sndr , P pm} m∈pool ps≡) m∈outs v⊂m ver ¬init
     with m∈outs
     -- Handler sends at most one vote, so it can't be "there"
  ...| there {xs = xs} imp = ⊥-elim (¬Any[] imp)
  ...| here refl
     with v⊂m
  ...| vote∈qc vs∈qc rbld≈ qc∈m
     with qc∈m
  ...| xxx = {!x!}                -- We will prove that votes represented in the SyncInfo of a
                                  -- proposal message were sent before, so these will be inj₂.
                                  -- This will be based on an invariant of the implementation, for
                                  -- example that the QCs included in the SyncInfo of a VoteMsg have
                                  -- been sent before.  We will need to use hash injectivity and
                                  -- signature injectivity to ensure a different vote was not sent
                                  -- previously with the same signature.

  impl-sps-avp {pk = pk} {α = α} {st = st} preach hpk (step-msg {sndr , P pm} m∈pool ps≡) m∈outs v⊂m ver ¬init
     | here refl
     | vote∈vm {si}
     with MsgWithSig∈? {pk} {ver-signature ver} {msgPool st}
  ...| yes msg∈ = inj₂ msg∈
  ...| no  msg∉ = inj₁ ( mkPCS4PK {! !} {!!} (inGenInfo refl) {!!} {!!} {!!}
       -- The implementation will need to provide evidence that the peer is a member of
       -- the epoch of the message it's sending and that it is assigned pk for that epoch.
                        , msg∉)

  open Structural impl-sps-avp

  ----- Properties that bridge the system model gap to the handler -----
  msgsToSendWereSent1 : ∀ {pid ts pm vm} {st : RoundManager}
                      → send (V vm) ∈ proj₂ (peerStep pid (P pm) ts st)
                      → ∃[ αs ] (SendVote vm αs ∈ LBFT-outs (handle pid (P pm) ts) st)
  msgsToSendWereSent1 {pid} {ts} {pm} {vm} {st} send∈acts
     with send∈acts
     -- The fake handler sends only to node 0 (fakeAuthor), so this doesn't
     -- need to be very general yet.
     -- TODO-1: generalize this proof so it will work when the set of recipients is
     -- not hard coded.

     -- The system model allows any message sent to be received by any peer (so the list of
     -- recipients it essentially ignored), meaning that our safety proofs will be for a slightly
     -- stronger model.  Progress proofs will require knowledge of recipients, though, so we will
     -- keep the implementation model faithful to the implementation.
  ...| here refl = fakeAuthor ∷ [] , here refl

  -- This captures which kinds of messages are sent by handling which kind of message.  It will
  -- require additional disjuncts when we implement processVote.
  msgsToSendWereSent : ∀ {pid nm m} {st : RoundManager}
                     → send m ∈ proj₂ (peerStepWrapper pid nm st)
                     → send m ∈ proj₂ (peerStep pid nm 0 st)
                     × ∃[ vm ] ∃[ pm ] (m ≡ V vm × nm ≡ P pm)
  msgsToSendWereSent {pid} {nm = nm} {m} {st} m∈outs
    with nm
  ...| C _ = ⊥-elim (¬Any[] m∈outs)
  ...| V _ = ⊥-elim (¬Any[] m∈outs)
  ...| P pm
     with m∈outs
  ...| here v∈outs
       with m
  ...| P _ = ⊥-elim (P≢V (action-send-injective v∈outs))
  ...| C _ = ⊥-elim (C≢V (action-send-injective v∈outs))
  ...| V vm rewrite sym v∈outs = here refl , vm , pm , refl , refl

  proposalHandlerSentVote : ∀ {pid ts pm vm} {st : RoundManager}
                          → send (V vm) ∈ proj₂ (peerStepWrapper pid (P pm) st)
                          → ∃[ αs ] (SendVote vm αs ∈ LBFT-outs (handle pid (P pm) ts) st)
  proposalHandlerSentVote {pid} {ts} {pm} {vm} {st} m∈outs
     with msgsToSendWereSent {pid} {P pm} {st = st} m∈outs
  ...| send∈ , vm , pm' , refl , refl
     with msgsToSendWereSent1 {pid} {ts} {pm'} {st = st} send∈
  ...| αs , sv = αs , sv

  ----- Properties that relate handler to system state -----

  data _∈RoundManager_ (qc : QuorumCert) (rm : RoundManager) : Set where
    inHQC : qc ≡ ₋rmHighestQC rm       → qc ∈RoundManager rm
    inHCC : qc ≡ ₋rmHighestCommitQC rm → qc ∈RoundManager rm

  postulate -- TODO-2: this will be proved for the implementation, confirming that honest
            -- participants only store QCs comprising votes that have actually been sent.
   -- Votes stored in highesQuorumCert and highestCommitCert were sent before.
   -- Note that some implementations might not ensure this, but LibraBFT does
   -- because even the leader of the next round sends its own vote to itself,
   -- as opposed to using it to construct a QC using its own unsent vote.

   qcVotesSentB4 : ∀{pid qc vs pk}{st : SystemState}
                 → ReachableSystemState st
                 → initialised st pid ≡ initd
                 → qc ∈RoundManager (peerStates st pid)
                 → vs ∈ qcVotes qc
                 → ¬ (∈GenInfo (proj₂ vs))
                 → MsgWithSig∈ pk (proj₂ vs) (msgPool st)

   -- We can prove this easily because we don't yet do epoch changes,
   -- so only the initial EC is relevant.  Later, this will require us to use the fact that
   -- epoch changes require proof of committing an epoch-changing transaction.
  availEpochsConsistent :
     ∀{pid pid' v v' pk}{st : SystemState}
     → ReachableSystemState st
     → (pkvpf  : PeerCanSignForPK st v  pid  pk)
     → (pkvpf' : PeerCanSignForPK st v' pid' pk)
     → PeerCanSignForPK.𝓔 pkvpf ≡ PeerCanSignForPK.𝓔 pkvpf'
  availEpochsConsistent r (mkPCS4PK _ _ (inGenInfo refl) _ _ _)
                          (mkPCS4PK _ _ (inGenInfo refl) _ _ _) = refl

  -- Always true, so far, as no epoch changes.
  noEpochIdChangeYet : ∀ {pre : SystemState}{pid}{ppre ppost msgs}
                     → ReachableSystemState pre
                     → ppre ≡ peerStates pre pid
                     → StepPeerState pid (msgPool pre) (initialised pre) ppre (ppost , msgs)
                     → initialised pre pid ≡ initd
                     → (₋rmEC ppre) ^∙ rmEpoch ≡ (₋rmEC ppost) ^∙ rmEpoch
  noEpochIdChangeYet _ ppre≡ (step-init uni) ini = ⊥-elim (uninitd≢initd (trans (sym uni) ini))
  noEpochIdChangeYet _ ppre≡ (step-msg {(_ , m)} _ _) ini
     with m
  ...| P p = refl
  ...| V v = refl
  ...| C c = refl

  open SyncInfo

  -- QCs in VoteMsg come from RoundManager
  VoteMsgQCsFromRoundManager :
       ∀ {pid s' outs pk}{pre : SystemState}
       → ReachableSystemState pre
       -- For any honest call to /handle/ or /init/,
       → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
       → ∀{v vm qc} → Meta-Honest-PK pk
       -- For every vote v represented in a message output by the call
       → v ⊂Msg (V vm)
       → send (V vm) ∈ outs
       → qc QC∈SyncInfo (vm ^∙ vmSyncInfo)
       → qc ∈RoundManager (peerStates pre pid)
  VoteMsgQCsFromRoundManager r (step-init _) _ _ ()
  VoteMsgQCsFromRoundManager {pid} {pre = pre} r (step-msg {_ , P pm} m∈pool pinit) {v} {vm}
                             hpk v⊂m m∈outs qc∈m
     with peerStates pre pid
  ...| rm
     with proposalHandlerSentVote {pid} {0} {pm} {vm} {rm} m∈outs
  ...| _ , v∈outs
     with qc∈m
  ...| withVoteSIHighQC refl
       = inHQC (cong ₋siHighestQuorumCert (procPMCerts≡ {0} {pm} {rm} v∈outs))

  VoteMsgQCsFromRoundManager {pid} {pre = pre} r (step-msg {_ , P pm} m∈pool pinit) {v} {vm1}
                             hpk v⊂m m∈outs qc∈m
     | rm
     | _ , v∈outs
     | withVoteSIHighCC hqcIsJust
     with cong ₋siHighestCommitCert (procPMCerts≡ {0} {pm} {rm} v∈outs)
  ...| refl
     with (rm ^∙ rmHighestQC) ≟QC (rm ^∙ rmHighestCommitQC)
  ...| true  because (ofʸ refl) = ⊥-elim (maybe-⊥ hqcIsJust refl)
  ...| false because _          = inHCC (just-injective (sym hqcIsJust))

  newVoteSameEpochGreaterRound : ∀ {pre : SystemState}{pid s' outs v m pk}
                               → ReachableSystemState pre
                               → StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs)
                               → ¬ (∈GenInfo (₋vSignature v))
                               → Meta-Honest-PK pk
                               → v ⊂Msg m → send m ∈ outs → (sig : WithVerSig pk v)
                               → ¬ MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
                               → v ^∙ vEpoch ≡ (₋rmEC (peerStates pre pid)) ^∙ rmEpoch
                               × suc ((₋rmEC (peerStates pre pid)) ^∙ rmLastVotedRound) ≡ v ^∙ vRound  -- New vote for higher round than last voted
                               × v ^∙ vRound ≡ ((₋rmEC s') ^∙ rmLastVotedRound)     -- Last voted round is round of new vote
  newVoteSameEpochGreaterRound {pre = pre} {pid} {v = v} {m} {pk} r (step-msg {(_ , P pm)} msg∈pool pinit) ¬init hpk v⊂m m∈outs sig vnew
     rewrite pinit
     with msgsToSendWereSent {pid} {P pm} {m} {peerStates pre pid} m∈outs
  ...| _ , vm , _ , refl , refl
    with proposalHandlerSentVote {pid} {0} {pm} {vm} {peerStates pre pid} m∈outs
  ...| _ , v∈outs
     rewrite SendVote-inj-v  (Any-singleton⁻ v∈outs)
           | SendVote-inj-si (Any-singleton⁻ v∈outs)
    with v⊂m
       -- Rebuilding keeps the same signature, and the SyncInfo included with the
       -- VoteMsg sent comprises QCs from the peer's state.  Votes represented in
       -- those QCS have signatures that have been sent before, contradicting the
       -- assumption that v's signature has not been sent before.
  ...| vote∈vm {si} = refl , refl , refl
  ...| vote∈qc {vs = vs} {qc} vs∈qc v≈rbld (inV qc∈m)
                  rewrite cong ₋vSignature v≈rbld
                        | procPMCerts≡ {0} {pm} {peerStates pre pid} {vm} v∈outs
    with qcVotesSentB4 r pinit (VoteMsgQCsFromRoundManager r (step-msg msg∈pool pinit) hpk v⊂m (here refl) qc∈m) vs∈qc ¬init
  ...| sentb4 = ⊥-elim (vnew sentb4)

  -- We resist the temptation to combine this with the noEpochChangeYet because in future there will be epoch changes
  lastVoteRound-mono : ∀ {pre : SystemState}{pid}{ppre ppost msgs}
                     → ReachableSystemState pre
                     → ppre ≡ peerStates pre pid
                     → StepPeerState pid (msgPool pre) (initialised pre) ppre (ppost , msgs)
                     → initialised pre pid ≡ initd
                     → (₋rmEC ppre) ^∙ rmEpoch ≡ (₋rmEC ppost) ^∙ rmEpoch
                     → (₋rmEC ppre) ^∙ rmLastVotedRound ≤ (₋rmEC ppost) ^∙ rmLastVotedRound
  lastVoteRound-mono _ ppre≡ (step-init uni) ini = ⊥-elim (uninitd≢initd (trans (sym uni) ini))
  lastVoteRound-mono _ ppre≡ (step-msg {(_ , m)} _ _) _
     with m
  ...| P p = const (≤-step (≤-reflexive refl))
  ...| V v = const (≤-reflexive refl)
  ...| C c = const (≤-reflexive refl)

  postulate -- TODO-1: prove it
    ¬genVotesRound≢0  : ∀ {pk sig}{st : SystemState}
                      → ReachableSystemState st
                      → Meta-Honest-PK pk
                      → (mws : MsgWithSig∈ pk sig (msgPool st))
                      → ¬ (∈GenInfo sig)
                      → (msgPart mws) ^∙ vRound ≢ 0

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module _ where

open import Data.Nat using (_+_ ;  _≤′_ ; suc)
open import Induction.Nat using (<-rec)
open import Esterel.Lang.CanFunction
open import Function using (_∋_ ; _∘_ ; id ; _$_)
open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc)
open import utility
open import noetherian using (noetherian ; ∥_∥s)
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; subst ; cong ; trans ; module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)
open import Data.Empty
open import sn-calculus
open import context-properties -- get view, E-views
open import Esterel.Lang.Binding
open import Data.Maybe using ( just )
-- open import coherence
open import Data.List.Any
open import Data.List.Any.Properties
open import Esterel.Lang.CanFunction.Base
open import eval
open import blocked
open import Data.List.All
open import eval

open ≡-Reasoning using (_≡⟨_⟩_ ; _≡⟨⟩_ ; _∎)

open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Data.FiniteMap
import Data.OrderedListMap as OMap
open import Data.Nat as Nat using (ℕ)
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 Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import sn-calculus-compatconf using (1-step)

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 import binding-preserve

open import sn-calculus-props
open import par-swap
open import par-swap.union-properties
open import calculus
open import calculus.properties

evalsn≡ₑ-consistent : ∀{output output'} θ p → CB (ρ⟨ θ , GO ⟩· p) → evalsn≡ₑ p θ output → evalsn≡ₑ p θ output' → output ≡ output'
evalsn≡ₑ-consistent θ p ⊢cb-p (evalsn-complete ρθ·p≡q complete-q) (evalsn-complete ρθ·p≡r complete-r)
  with sn≡ₑ-consistent (proj₂ (sn≡ₑ-preserve-cb ⊢cb-p ρθ·p≡q)) (rtrn (rsym ρθ·p≡q  ⊢cb-p) ρθ·p≡r)
... | (s , qsn⟶*s , rsn⟶*s)
  with inescapability-of-complete-sn complete-q qsn⟶*s
... | complete-s
   with ρ-stays-ρ-sn⟶* qsn⟶*s | ρ-stays-ρ-sn⟶* rsn⟶*s
... | θq , _ , _ , refl | θr , _ , _ , refl
   with equality-of-complete-sn⟶* complete-q qsn⟶*s
      | equality-of-complete-sn⟶* complete-r rsn⟶*s
... | refl , refl | refl , refl = refl

eval∥R∪sn≡ₑ-consistent : ∀ {output output'} θ p →
  CB (ρ⟨ θ , GO ⟩· p) →
  eval∥R∪sn≡ₑ p θ output →
  eval∥R∪sn≡ₑ p θ output' →
  output ≡ output'
eval∥R∪sn≡ₑ-consistent θ p ⊢cb-p (eval∥R∪sn-complete ρθ·p≡q complete-q) (eval∥R∪sn-complete ρθ·p≡r complete-r)
  with ∥R∪sn≡ₑ-consistent (proj₂ (∥R∪sn≡ₑ-preserve-cb ⊢cb-p ρθ·p≡q)) (∪trn (∪sym ρθ·p≡q  ⊢cb-p) ρθ·p≡r)
... | (s , qsn⟶*s , rsn⟶*s)
  with inescapability-of-complete-∪ complete-q qsn⟶*s
... | complete-s
   with ρ-stays-ρ-∪ qsn⟶*s | ρ-stays-ρ-∪ rsn⟶*s
... | θq , _ , _ , refl | θr , _ , _ , refl
   with equality-of-complete-∪ complete-q qsn⟶*s
      | equality-of-complete-∪ complete-r rsn⟶*s
... | refl , refl | refl , refl = refl

eval≡ₑ->eval∥R∪sn≡ : ∀ {p θ output} ->
  eval≡ₑ p θ output →
  eval∥R∪sn≡ₑ p θ output
eval≡ₑ->eval∥R∪sn≡ (eval-complete ρθ·p≡q complete-q) =
  eval∥R∪sn-complete (≡ₑ-to-∥R∪sn≡ₑ ρθ·p≡q) complete-q

eval≡ₑ-consistent : ∀ {output output'} θ p →
  CB (ρ⟨ θ , GO ⟩· p) →
  eval≡ₑ p θ output →
  eval≡ₑ p θ output' →
  output ≡ output'
eval≡ₑ-consistent θ p CBρp eval≡₁ eval≡₂
  = eval∥R∪sn≡ₑ-consistent θ p CBρp
      (eval≡ₑ->eval∥R∪sn≡ eval≡₁)
      (eval≡ₑ->eval∥R∪sn≡ eval≡₂)

sn≡ₑ=>eval : ∀ p θp outputp q θq outputq → CB (ρ⟨ θp , GO ⟩· p) → (ρ⟨ θp , GO ⟩· p) sn≡ₑ (ρ⟨ θq , GO ⟩· q) → evalsn≡ₑ p θp outputp → evalsn≡ₑ q θq outputq → outputp ≡ outputq
sn≡ₑ=>eval _ _ _ _ _ _ CB eq (evalsn-complete ρθ·p≡q complete-q) (evalsn-complete ρθ·p≡q₁ complete-q₁)
  with sn≡ₑ-consistent (proj₂ (sn≡ₑ-preserve-cb CB ρθ·p≡q)) (rtrn (rsym ρθ·p≡q  CB) (rtrn eq ρθ·p≡q₁))
... | (s , qsn⟶*s , rsn⟶*s)
  with inescapability-of-complete-sn complete-q qsn⟶*s
... | complete-s
   with ρ-stays-ρ-sn⟶* qsn⟶*s | ρ-stays-ρ-sn⟶* rsn⟶*s
... | θq , _ , _ , refl | θr , _ , _ , refl
   with equality-of-complete-sn⟶* complete-q qsn⟶*s
      | equality-of-complete-sn⟶* complete-q₁ rsn⟶*s
... | refl , refl | refl , refl = refl

∥R∪sn≡ₑ=>eval : ∀ p θp outputp q θq outputq →
  CB (ρ⟨ θp , GO ⟩· p) →
  (ρ⟨ θp , GO ⟩· p) ∥R∪sn≡ₑ (ρ⟨ θq , GO ⟩· q) →
  eval∥R∪sn≡ₑ p θp outputp →
  eval∥R∪sn≡ₑ q θq outputq →
  outputp ≡ outputq
∥R∪sn≡ₑ=>eval _ _ _ _ _ _ CB eq (eval∥R∪sn-complete ρθ·p≡q complete-q) (eval∥R∪sn-complete ρθ·p≡q₁ complete-q₁)
  with ∥R∪sn≡ₑ-consistent (proj₂ (∥R∪sn≡ₑ-preserve-cb CB ρθ·p≡q)) (∪trn (∪sym ρθ·p≡q  CB) (∪trn eq ρθ·p≡q₁))
... | (s , qsn⟶*s , rsn⟶*s)
  with inescapability-of-complete-∪ complete-q qsn⟶*s
... | complete-s
   with ρ-stays-ρ-∪ qsn⟶*s | ρ-stays-ρ-∪ rsn⟶*s
... | θq , _ , _ , refl | θr , _ , _ , refl
   with equality-of-complete-∪ complete-q qsn⟶*s
      | equality-of-complete-∪ complete-q₁ rsn⟶*s
... | refl , refl | refl , refl = refl

≡ₑ=>eval : ∀ p θp outputp q θq outputq →
  CB (ρ⟨ θp , GO ⟩· p) →
  (ρ⟨ θp , GO ⟩· p) ≡ₑ (ρ⟨ θq , GO ⟩· q) # [] →
  eval≡ₑ p θp outputp →
  eval≡ₑ q θq outputq →
  outputp ≡ outputq
≡ₑ=>eval p θp outputp q θq outputq CBρp ρp≡ₑρq eval≡₁ eval≡₂
  = ∥R∪sn≡ₑ=>eval p θp outputp q θq outputq CBρp
      (≡ₑ-to-∥R∪sn≡ₑ ρp≡ₑρq)
      (eval≡ₑ->eval∥R∪sn≡ eval≡₁)
      (eval≡ₑ->eval∥R∪sn≡ eval≡₂)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus