text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a strict order to incorporate a new supremum
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Supremum

open import Relation.Binary

module Relation.Binary.Construct.Add.Supremum.Strict
  {a r} {A : Set a} (_<_ : Rel A r) where

open import Level using (_⊔_)
open import Data.Product
open import Function
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl)
open import Relation.Nullary.Construct.Add.Supremum
import Relation.Binary.Construct.Add.Supremum.Equality as Equality
import Relation.Binary.Construct.Add.Supremum.NonStrict as NonStrict

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

infix 4 _<⁺_

data _<⁺_ : Rel (A ⁺) (a ⊔ r) where
  [_]    : {k l : A} → k < l → [ k ] <⁺ [ l ]
  [_]<⊤⁺ : (k : A)           → [ k ] <⁺ ⊤⁺

------------------------------------------------------------------------
-- Relational properties

[<]-injective : ∀ {k l} → [ k ] <⁺ [ l ] → k < l
[<]-injective [ p ] = p

<⁺-asym : Asymmetric _<_ → Asymmetric _<⁺_
<⁺-asym <-asym [ p ]    [ q ] = <-asym p q

<⁺-trans : Transitive _<_ → Transitive _<⁺_
<⁺-trans <-trans [ p ] [ q ]    = [ <-trans p q ]
<⁺-trans <-trans [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺

<⁺-dec : Decidable _<_ → Decidable _<⁺_
<⁺-dec _<?_ [ k ] [ l ] = Dec.map′ [_] [<]-injective (k <? l)
<⁺-dec _<?_ [ k ] ⊤⁺    = yes [ k ]<⊤⁺
<⁺-dec _<?_ ⊤⁺    [ l ] = no (λ ())
<⁺-dec _<?_ ⊤⁺    ⊤⁺    = no (λ ())

<⁺-irrelevant : Irrelevant _<_ → Irrelevant _<⁺_
<⁺-irrelevant <-irr [ p ]    [ q ]    = P.cong _ (<-irr p q)
<⁺-irrelevant <-irr [ k ]<⊤⁺ [ k ]<⊤⁺ = P.refl

module _ {r} {_≤_ : Rel A r} where

  open NonStrict _≤_

  <⁺-transʳ : Trans _≤_ _<_ _<_ → Trans _≤⁺_ _<⁺_ _<⁺_
  <⁺-transʳ <-transʳ [ p ] [ q ]    = [ <-transʳ p q ]
  <⁺-transʳ <-transʳ [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺

  <⁺-transˡ : Trans _<_ _≤_ _<_ → Trans _<⁺_ _≤⁺_ _<⁺_
  <⁺-transˡ <-transˡ [ p ]    [ q ]       = [ <-transˡ p q ]
  <⁺-transˡ <-transˡ [ p ]    ([ _ ] ≤⊤⁺) = [ _ ]<⊤⁺
  <⁺-transˡ <-transˡ [ k ]<⊤⁺ (⊤⁺ ≤⊤⁺)    = [ k ]<⊤⁺

------------------------------------------------------------------------
-- Relational properties + propositional equality

<⁺-cmp-≡ : Trichotomous _≡_ _<_ → Trichotomous _≡_ _<⁺_
<⁺-cmp-≡ <-cmp ⊤⁺    ⊤⁺    = tri≈ (λ ()) refl (λ ())
<⁺-cmp-≡ <-cmp ⊤⁺    [ l ] = tri> (λ ()) (λ ()) [ l ]<⊤⁺
<⁺-cmp-≡ <-cmp [ k ] ⊤⁺    = tri< [ k ]<⊤⁺ (λ ()) (λ ())
<⁺-cmp-≡ <-cmp [ k ] [ l ] with <-cmp k l
... | tri< a ¬b    ¬c = tri< [ a ] (¬b ∘ []-injective) (¬c ∘ [<]-injective)
... | tri≈ ¬a refl ¬c = tri≈ (¬a ∘ [<]-injective) refl (¬c ∘ [<]-injective)
... | tri> ¬a ¬b    c = tri> (¬a ∘ [<]-injective) (¬b ∘ []-injective) [ c ]

<⁺-irrefl-≡ : Irreflexive _≡_ _<_ → Irreflexive _≡_ _<⁺_
<⁺-irrefl-≡ <-irrefl refl [ x ] = <-irrefl refl x

<⁺-respˡ-≡ : _<⁺_ Respectsˡ _≡_
<⁺-respˡ-≡ = P.subst (_<⁺ _)

<⁺-respʳ-≡ : _<⁺_ Respectsʳ _≡_
<⁺-respʳ-≡ = P.subst (_ <⁺_)

<⁺-resp-≡ : _<⁺_ Respects₂ _≡_
<⁺-resp-≡ = <⁺-respʳ-≡ , <⁺-respˡ-≡

------------------------------------------------------------------------
-- Relational properties + setoid equality

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  <⁺-cmp : Trichotomous _≈_ _<_ → Trichotomous _≈⁺_ _<⁺_
  <⁺-cmp <-cmp ⊤⁺    ⊤⁺    = tri≈ (λ ()) ⊤⁺≈⊤⁺ (λ ())
  <⁺-cmp <-cmp ⊤⁺    [ l ] = tri> (λ ()) (λ ()) [ l ]<⊤⁺
  <⁺-cmp <-cmp [ k ] ⊤⁺    = tri< [ k ]<⊤⁺ (λ ()) (λ ())
  <⁺-cmp <-cmp [ k ] [ l ] with <-cmp k l
  ... | tri< a ¬b ¬c = tri< [ a ] (¬b ∘ [≈]-injective) (¬c ∘ [<]-injective)
  ... | tri≈ ¬a b ¬c = tri≈ (¬a ∘ [<]-injective) [ b ] (¬c ∘ [<]-injective)
  ... | tri> ¬a ¬b c = tri> (¬a ∘ [<]-injective) (¬b ∘ [≈]-injective) [ c ]

  <⁺-irrefl : Irreflexive _≈_ _<_ → Irreflexive _≈⁺_ _<⁺_
  <⁺-irrefl <-irrefl [ p ] [ q ] = <-irrefl p q

  <⁺-respˡ-≈⁺ : _<_ Respectsˡ _≈_ → _<⁺_ Respectsˡ _≈⁺_
  <⁺-respˡ-≈⁺ <-respˡ-≈ [ p ] [ q ]      = [ <-respˡ-≈ p q ]
  <⁺-respˡ-≈⁺ <-respˡ-≈ [ p ] ([ l ]<⊤⁺) = [ _ ]<⊤⁺
  <⁺-respˡ-≈⁺ <-respˡ-≈ ⊤⁺≈⊤⁺ q          = q

  <⁺-respʳ-≈⁺ : _<_ Respectsʳ _≈_ → _<⁺_ Respectsʳ _≈⁺_
  <⁺-respʳ-≈⁺ <-respʳ-≈ [ p ] [ q ] = [ <-respʳ-≈ p q ]
  <⁺-respʳ-≈⁺ <-respʳ-≈ ⊤⁺≈⊤⁺ q     = q

  <⁺-resp-≈⁺ : _<_ Respects₂ _≈_ → _<⁺_ Respects₂ _≈⁺_
  <⁺-resp-≈⁺ = map <⁺-respʳ-≈⁺ <⁺-respˡ-≈⁺

------------------------------------------------------------------------
-- Structures + propositional equality

<⁺-isStrictPartialOrder-≡ : IsStrictPartialOrder _≡_ _<_ →
                            IsStrictPartialOrder _≡_ _<⁺_
<⁺-isStrictPartialOrder-≡ strict = record
  { isEquivalence = P.isEquivalence
  ; irrefl        = <⁺-irrefl-≡ irrefl
  ; trans         = <⁺-trans trans
  ; <-resp-≈      = <⁺-resp-≡
  } where open IsStrictPartialOrder strict

<⁺-isDecStrictPartialOrder-≡ : IsDecStrictPartialOrder _≡_ _<_ →
                               IsDecStrictPartialOrder _≡_ _<⁺_
<⁺-isDecStrictPartialOrder-≡ dectot = record
  { isStrictPartialOrder = <⁺-isStrictPartialOrder-≡ isStrictPartialOrder
  ; _≟_                  = ≡-dec _≟_
  ; _<?_                 = <⁺-dec _<?_
  } where open IsDecStrictPartialOrder dectot

<⁺-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
                          IsStrictTotalOrder _≡_ _<⁺_
<⁺-isStrictTotalOrder-≡ strictot = record
  { isEquivalence = P.isEquivalence
  ; trans         = <⁺-trans trans
  ; compare       = <⁺-cmp-≡ compare
  } where open IsStrictTotalOrder strictot

------------------------------------------------------------------------
-- Structures + setoid equality

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  <⁺-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ →
                            IsStrictPartialOrder _≈⁺_ _<⁺_
  <⁺-isStrictPartialOrder strict = record
    { isEquivalence = ≈⁺-isEquivalence isEquivalence
    ; irrefl        = <⁺-irrefl irrefl
    ; trans         = <⁺-trans trans
    ; <-resp-≈      = <⁺-resp-≈⁺ <-resp-≈
    } where open IsStrictPartialOrder strict

  <⁺-isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ →
                               IsDecStrictPartialOrder _≈⁺_ _<⁺_
  <⁺-isDecStrictPartialOrder dectot = record
    { isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
    ; _≟_                  = ≈⁺-dec _≟_
    ; _<?_                 = <⁺-dec _<?_
    } where open IsDecStrictPartialOrder dectot

  <⁺-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                          IsStrictTotalOrder _≈⁺_ _<⁺_
  <⁺-isStrictTotalOrder strictot = record
    { isEquivalence = ≈⁺-isEquivalence isEquivalence
    ; trans         = <⁺-trans trans
    ; compare       = <⁺-cmp compare
    } where open IsStrictTotalOrder strictot


text:
module _ where

module A where

  infix 2 _↑
  infix 1 c

  data D : Set where
    ●  : D
    _↑ : D → D
    c  : {x y : D} → D

  syntax c {x = x} {y = y} = x ↓ y

module B where

  infix 1 c

  data D : Set where
    c : {y x : D} → D

  syntax c {y = y} {x = x} = y ↓ x

open A
open B

rejected : A.D
rejected = ● ↑ ↓ ●

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --safe #-}
module Issue4949 where

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical renaming (primIMax to _∨_)
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma

open import Agda.Builtin.Cubical.Glue renaming (prim^glue to glue)

idIsEquiv : ∀ {ℓ} (A : Set ℓ) → isEquiv (\ (x : A) → x)
equiv-proof (idIsEquiv A) y =
  ((y , \ _ → y) , λ z i → z .snd (primINeg i) , λ j → z .snd (primINeg i ∨ j))

idEquiv : ∀ {ℓ} (A : Set ℓ) → Σ _ (isEquiv {A = A} {B = A})
idEquiv A .fst = \ x → x
idEquiv A .snd = idIsEquiv A

Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
       → (Te : Partial φ (Σ (Set ℓ') \ T → Σ _ (isEquiv {A = T} {B = A})))
       → Set ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

ua : ∀ {ℓ} {A B : Set ℓ} → A ≃ B → A ≡ B
ua {A = A} {B = B} e i = Glue B (λ { (i = i0) → (A , e)
                                   ; (i = i1) → (B , idEquiv B) })

⊤₀ = ⊤
⊤₁ = Σ ⊤ \ _ → ⊤

prf : isEquiv {A = ⊤₀} {B = ⊤₁} _
equiv-proof prf y = (_ , \ i → _) , (\ y → \ i → _ , (\ j → _))

u : ⊤₀ ≡ ⊤₁
u = ua ((λ _ → _) , prf)

uniq : ∀ i j → u (i ∨ j)
uniq i j = glue (λ { (i = i0) (j = i0) → tt ; (i = i1) → tt , tt ; (j = i1) → tt , tt }) _

-- comparing the partial element argument of `glue` should happen at the right type.
-- if it does not we get problems with eta.
test : ∀ j → uniq i0 j ≡ glue (λ { (i0 = i0) (j = i0) → tt ; (j = i1) → tt , tt }) (tt , tt)
test j = \ k → uniq i0 j

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Problem 4: ``50 shades of continuity''

{-
C(f)        =  ∀ c : X. Cat(f,c)
Cat(f,c)    =  ∀ ε > 0. ∃ δ > 0. Q(f,c,ε,δ)
Q(f,c,ε,δ)  =  ∀ x : X.  abs(x - c) < δ  ⇒  abs(f x - f c) < ε

C'(f)       =  ∃ getδ : X -> RPos -> RPos. ∀ c : X. ∀ ε > 0. Q(f,c,ε,getδ c ε)

4a: Define UC(f):

UC(f) = ∀ ε > 0. ∃ δ > 0. ∀ y : X. Q(f,y,ε,δ)

4b: Define UC'(f):

UC'(f) = ∃ newδ : RPos -> RPos. ∀ ε > 0. ∀ y : X. Q(f,y,ε,newδ ε)

The function |newδ| computes a suitable "global" |δ| from any |ε|,
which shows |Q| for any |y|.

4c: Prove |∀ f : X -> ℝ. UC'(f) => C'(f)|.

The proof is a function from a pair (newδ, puc) to a pair (getδ, pc).

proof f (newδ, puc) = (getδ, pc)
  where  getδ c ε = newδ ε
         pc c ε = puc ε c   -- (1)

The type of (1) is

  Q(f,c,ε,newδ ε)
=
  Q(f,c,ε,getδ c ε)

which is the type of |pc c ε|.

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

Below is a self-contained proof in Agda just to check the above. It is
not part of the exam question.

-}

postulate
  R RPos : Set
  abs : R -> RPos
  _-_ : R -> R -> R
  _<_ : RPos -> RPos -> Set

X = R  -- to avoid trouble with lack of subtyping

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

Q : (X -> R) -> X -> RPos -> RPos -> Set
Q f c ε δ  =  (x : X) -> (abs(  x -   c) < δ)  ->
                         (abs(f x - f c) < ε)

Cat : (X -> R) -> X -> Set
Cat f c    =  (ε : RPos) -> Sigma RPos (\δ ->
                                  Q f c ε δ)

C : (X -> R) -> Set
C f        =  (c : X) -> Cat f c

C' : (X -> R) -> Set
C' f =  Sigma (X -> RPos -> RPos) (\getδ ->
              (c : X) -> (ε : RPos) -> Q f c ε (getδ c ε))

UC : (X -> R) -> Set
UC f = (ε : RPos) -> Sigma RPos (\δ ->
                           (y : X) -> Q f y ε δ)

UC' : (X -> R) -> Set
UC' f = Sigma (RPos -> RPos) (\newδ ->
              (ε : RPos) -> (y : X) -> Q f y ε (newδ ε))

proof : (f : X -> R) -> UC' f -> C' f
proof f (newδ , puc) = (getδ , pc)
  where  getδ  = \c -> newδ
         pc    = \c ε -> puc ε c

max_stars_repo_name: nicolabotta/DSLsofMath

max_issues_repo_name: nicolabotta/DSLsofMath

max_forks_repo_name: nicolabotta/DSLsofMath


text:
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
module Data.QuadTree.LensProofs.Valid-LensA where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws
open import Data.Lens.Proofs.LensPostulates
open import Data.Lens.Proofs.LensComposition
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.SafeFunctions
open import Data.QuadTree.Implementation.PublicFunctions
open import Data.QuadTree.Implementation.DataLenses

--- Lens laws for lensA

ValidLens-LensA-ViewSet :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ViewSet (lensA {t} {dep})
ValidLens-LensA-ViewSet (CVQuadrant (Leaf x) {p1}) (CVQuadrant (Leaf v) {p2}) =
    begin
        view lensA (set lensA (CVQuadrant (Leaf x) {p1}) (CVQuadrant (Leaf v) {p2}))
    =⟨⟩
        getConst
            (lensA CConst
            (ifc (x == v && v == v && v == v)
                then CVQuadrant (Leaf x)
                else CVQuadrant (Node (Leaf x) (Leaf v) (Leaf v) (Leaf v))))
    =⟨ sym (propFnIfc (x == v && v == v && v == v) (λ x -> getConst (lensA CConst x))) ⟩
        (ifc (x == v && v == v && v == v)
        then (CVQuadrant (Leaf x))
        else (CVQuadrant (Leaf x)))
    =⟨ propIfcBranchesSame {c = (x == v && v == v && v == v)} (CVQuadrant (Leaf x)) ⟩
         (CVQuadrant (Leaf x))
    end
ValidLens-LensA-ViewSet (CVQuadrant (Node a b c d)) (CVQuadrant (Leaf v)) = refl
ValidLens-LensA-ViewSet (CVQuadrant (Leaf x) {p1}) (CVQuadrant (Node a b@(Leaf vb) c@(Leaf vc) d@(Leaf vd)) {p2}) =
    begin
        view lensA (set lensA (CVQuadrant (Leaf x) {p1}) (CVQuadrant (Node a b c d) {p2}))
    =⟨⟩
        getConst (lensA CConst (
            ifc (x == vb && vb == vc && vc == vd)
            then (CVQuadrant (Leaf x))
            else (CVQuadrant (Node (Leaf x) (Leaf vb) (Leaf vc) (Leaf vd)))
        ))
    =⟨ sym (propFnIfc (x == vb && vb == vc && vc == vd) (λ x -> getConst (lensA CConst x))) ⟩
        (ifc (x == vb && vb == vc && vc == vd)
        then (CVQuadrant (Leaf x))
        else (CVQuadrant (Leaf x)))
    =⟨ propIfcBranchesSame {c = (x == vb && vb == vc && vc == vd)} (CVQuadrant (Leaf x)) ⟩
        (CVQuadrant (Leaf x))
    end
ValidLens-LensA-ViewSet (CVQuadrant (Leaf x)) (CVQuadrant (Node a (Leaf x₁) (Leaf x₂) (Node d d₁ d₂ d₃))) = refl
ValidLens-LensA-ViewSet (CVQuadrant (Leaf x)) (CVQuadrant (Node a (Leaf x₁) (Node c c₁ c₂ c₃) d)) = refl
ValidLens-LensA-ViewSet (CVQuadrant (Leaf x)) (CVQuadrant (Node a (Node b b₁ b₂ b₃) c d)) = refl
ValidLens-LensA-ViewSet (CVQuadrant (Node toa tob toc tod)) (CVQuadrant (Node a b c d)) = refl

ValidLens-LensA-SetView :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> SetView (lensA {t} {dep})
ValidLens-LensA-SetView {t} {dep} qd@(CVQuadrant (Leaf x) {p}) =
    begin
        set lensA (view lensA qd) qd
    =⟨⟩
        ((ifc (x == x && x == x && x == x)
            then (CVQuadrant (Leaf x))
            else λ {{z}} -> (CVQuadrant (Node (Leaf x) (Leaf x) (Leaf x) (Leaf x)))))
    =⟨ ifcTrue (x == x && x == x && x == x) (andCombine (eqReflexivity x) (andCombine (eqReflexivity x) (eqReflexivity x))) ⟩
        CVQuadrant (Leaf x)
    end
ValidLens-LensA-SetView {t} {dep} cv@(CVQuadrant qd@(Node (Leaf a) (Leaf b) (Leaf c) (Leaf d)) {p}) =
    begin
        set lensA (view lensA cv) cv
    =⟨⟩
        (ifc (a == b && b == c && c == d) then (CVQuadrant (Leaf a)) else (CVQuadrant (Node (Leaf a) (Leaf b) (Leaf c) (Leaf d))))
    =⟨ ifcFalse (a == b && b == c && c == d) (notTrueToFalse (andSnd {depth qd <= S dep} {isCompressed qd} p)) ⟩
        (CVQuadrant (Node (Leaf a) (Leaf b) (Leaf c) (Leaf d)))
    end
ValidLens-LensA-SetView (CVQuadrant (Node (Leaf x) (Leaf x₁) (Leaf x₂) (Node qd₃ qd₄ qd₅ qd₆))) = refl
ValidLens-LensA-SetView (CVQuadrant (Node (Leaf x) (Leaf x₁) (Node qd₂ qd₄ qd₅ qd₆) qd₃)) = refl
ValidLens-LensA-SetView (CVQuadrant (Node (Leaf x) (Node qd₁ qd₄ qd₅ qd₆) qd₂ qd₃)) = refl
ValidLens-LensA-SetView (CVQuadrant (Node (Node qd qd₄ qd₅ qd₆) qd₁ qd₂ qd₃)) = refl

ValidLens-LensA-SetSet-Lemma : {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> (x a b c d : VQuadrant t {dep})
    -> set lensA x (combine a b c d) ≡ (combine x b c d)
ValidLens-LensA-SetSet-Lemma {t} {dep} (CVQuadrant x@(Leaf xv)) (CVQuadrant a@(Leaf va)) (CVQuadrant b@(Leaf vb)) (CVQuadrant c@(Leaf vc)) (CVQuadrant d@(Leaf vd)) =
    begin
        (runIdentity (lensA (λ _ → CIdentity (CVQuadrant (Leaf xv)))
            (ifc va == vb && vb == vc && vc == vd
            then CVQuadrant (Leaf va)
            else CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd)))))
    =⟨ sym $ propFnIfc (va == vb && vb == vc && vc == vd) (λ g -> (runIdentity (lensA (λ _ → CIdentity (CVQuadrant (Leaf xv) {andCombine (zeroLteAny dep) IsTrue.itsTrue})) g ) ) ) ⟩
        (ifc va == vb && vb == vc && vc == vd
            then ifc xv == va && va == va && va == va
                then CVQuadrant (Leaf xv)
                else CVQuadrant (Node (Leaf xv) (Leaf va) (Leaf va) (Leaf va))
            else ifc xv == vb && vb == vc && vc == vd
                then CVQuadrant (Leaf xv)
                else CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ ifcTrueMap {c = va == vb && vb == vc && vc == vd}
            (λ p -> cong
                (λ q -> ifc xv == q && q == q && q == q
                    then CVQuadrant (Leaf xv) {andCombine (zeroLteAny (S dep)) IsTrue.itsTrue}
                    else (λ {{p}} -> CVQuadrant (Node (Leaf xv) (Leaf q) (Leaf q) (Leaf q)) {andCombine (zeroLteAny (dep)) (falseToNotTrue p)}) )
                (eqToEquiv va vb (andFst {va == vb} p))  ) ⟩

        (ifc va == vb && vb == vc && vc == vd
            then ifc xv == vb && vb == vb && vb == vb
                then CVQuadrant (Leaf xv) {andCombine (zeroLteAny (S dep)) IsTrue.itsTrue}
                else (λ {{p}} -> CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vb) (Leaf vb)) {andCombine (zeroLteAny (dep)) (falseToNotTrue p)})
            else ifc xv == vb && vb == vc && vc == vd
                then CVQuadrant (Leaf xv)
                else CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ ifcTrueMap {c = va == vb && vb == vc && vc == vd}
            (λ p -> cong
                (λ q -> ifc xv == vb && vb == q && q == q
                    then CVQuadrant (Leaf xv) {andCombine (zeroLteAny (S dep)) IsTrue.itsTrue}
                    else (λ {{p}} -> CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf q) (Leaf q)) {andCombine (zeroLteAny (dep)) (falseToNotTrue p)}) )
                (eqToEquiv vb vc (andFst $ andSnd {va == vb} p))  ) ⟩

        (ifc va == vb && vb == vc && vc == vd
            then ifc xv == vb && vb == vc && vc == vc
                then CVQuadrant (Leaf xv) {andCombine (zeroLteAny (S dep)) IsTrue.itsTrue}
                else (λ {{p}} -> CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vc)) {andCombine (zeroLteAny (dep)) (falseToNotTrue p)})
            else ifc xv == vb && vb == vc && vc == vd
                then CVQuadrant (Leaf xv)
                else CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ ifcTrueMap {c = va == vb && vb == vc && vc == vd}
            (λ p -> cong
                (λ q -> ifc xv == vb && vb == vc && vc == q
                    then CVQuadrant (Leaf xv) {andCombine (zeroLteAny (S dep)) IsTrue.itsTrue}
                    else (λ {{p}} -> CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf q)) {andCombine (zeroLteAny (dep)) (falseToNotTrue p)}) )
                (eqToEquiv vc vd (andSnd $ andSnd {va == vb} p))  ) ⟩

        (ifc va == vb && vb == vc && vc == vd
            then ifc xv == vb && vb == vc && vc == vd
                then CVQuadrant (Leaf xv) {andCombine (zeroLteAny (S dep)) IsTrue.itsTrue}
                else (λ {{p}} -> CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd)) {andCombine (zeroLteAny (dep)) (falseToNotTrue p)})
            else ifc xv == vb && vb == vc && vc == vd
                then CVQuadrant (Leaf xv)
                else CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ propIfcBranchesSame {c = va == vb && vb == vc && vc == vd}
        (ifc xv == vb && vb == vc && vc == vd then CVQuadrant (Leaf xv) else CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd))) ⟩

        (ifc xv == vb && vb == vc && vc == vd
            then CVQuadrant (Leaf xv)
            else CVQuadrant (Node (Leaf xv) (Leaf vb) (Leaf vc) (Leaf vd)))
    end
ValidLens-LensA-SetSet-Lemma {t} {dep} cvx@(CVQuadrant x@(Node x1 x2 x3 x4) {p}) cva@(CVQuadrant a@(Leaf va)) cvb@(CVQuadrant b@(Leaf vb)) cvc@(CVQuadrant c@(Leaf vc)) cvd@(CVQuadrant d@(Leaf vd)) =
    begin
        runIdentity (lensA (λ _ → CIdentity cvx)
            (ifc va == vb && vb == vc && vc == vd
            then CVQuadrant (Leaf va)
            else CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd))))
    =⟨ sym $ propFnIfc (va == vb && vb == vc && vc == vd) (λ g -> (runIdentity (lensA (λ _ → CIdentity cvx) g ) ) ) ⟩
        (ifc va == vb && vb == vc && vc == vd
        then CVQuadrant (Node x (Leaf va) (Leaf va) (Leaf va))
        else CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ ifcTrueMap {c = va == vb && vb == vc && vc == vd} (λ p -> cong (λ q -> combine cvx (cvq q) (cvq q) (cvq q)) (eqToEquiv va vb (andFst {va == vb} p)))   ⟩
        (ifc va == vb && vb == vc && vc == vd
        then CVQuadrant (Node x (Leaf vb) (Leaf vb) (Leaf vb))
        else CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ ifcTrueMap {c = va == vb && vb == vc && vc == vd} (λ p -> cong (λ q -> combine cvx cvb (cvq q) (cvq q)) (eqToEquiv vb vc (andFst $ andSnd {va == vb} p)))   ⟩
        (ifc va == vb && vb == vc && vc == vd
        then CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vc))
        else CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ ifcTrueMap {c = va == vb && vb == vc && vc == vd} (λ p -> cong (λ q -> combine cvx cvb cvc (cvq q)) (eqToEquiv vc vd (andSnd $ andSnd {va == vb} p)))   ⟩
        (ifc va == vb && vb == vc && vc == vd
        then CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd))
        else CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd)))
    =⟨ propIfcBranchesSame {c = va == vb && vb == vc && vc == vd} (CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd))) ⟩
        CVQuadrant (Node x (Leaf vb) (Leaf vc) (Leaf vd))
    end where
        -- Construct a valid leaf from a value
        cvq : t -> VQuadrant t {dep}
        cvq q = CVQuadrant (Leaf q) {andCombine (zeroLteAny dep) IsTrue.itsTrue}
ValidLens-LensA-SetSet-Lemma (CVQuadrant _) (CVQuadrant (Leaf _)) (CVQuadrant (Leaf _)) (CVQuadrant (Leaf _)) (CVQuadrant (Node _ _ _ _)) = refl
ValidLens-LensA-SetSet-Lemma (CVQuadrant _) (CVQuadrant (Leaf _)) (CVQuadrant (Leaf _)) (CVQuadrant (Node _ _ _ _)) (CVQuadrant _) = refl
ValidLens-LensA-SetSet-Lemma (CVQuadrant _) (CVQuadrant (Leaf _)) (CVQuadrant (Node _ _ _ _)) (CVQuadrant _) (CVQuadrant _) = refl
ValidLens-LensA-SetSet-Lemma (CVQuadrant _) (CVQuadrant (Node _ _ _ _)) (CVQuadrant _) (CVQuadrant _) (CVQuadrant _) = refl

ValidLens-LensA-SetSet :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> SetSet (lensA {t} {dep})
ValidLens-LensA-SetSet a@(CVQuadrant qda) b@(CVQuadrant qdb) x@(CVQuadrant qdx@(Leaf xv)) =
    begin
        set lensA (CVQuadrant qdb) (combine (CVQuadrant qda) (CVQuadrant (Leaf xv)) (CVQuadrant (Leaf xv)) (CVQuadrant (Leaf xv)))
    =⟨ ValidLens-LensA-SetSet-Lemma (CVQuadrant qdb) (CVQuadrant qda) (CVQuadrant (Leaf xv)) (CVQuadrant (Leaf xv)) (CVQuadrant (Leaf xv)) ⟩
        combine (CVQuadrant qdb) (CVQuadrant (Leaf xv)) (CVQuadrant (Leaf xv)) (CVQuadrant (Leaf xv))
    end
ValidLens-LensA-SetSet (CVQuadrant qda) (CVQuadrant qdb) (CVQuadrant qdx@(Node xa xb xc xd)) =
    begin
        set lensA (CVQuadrant qdb) (combine (CVQuadrant qda) (CVQuadrant xb) (CVQuadrant xc) (CVQuadrant xd))
    =⟨ ValidLens-LensA-SetSet-Lemma (CVQuadrant qdb) (CVQuadrant qda) (CVQuadrant xb) (CVQuadrant xc) (CVQuadrant xd) ⟩
        combine (CVQuadrant qdb) (CVQuadrant xb) (CVQuadrant xc) (CVQuadrant xd)
    end

ValidLens-LensA : {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ValidLens (VQuadrant t {S dep}) (VQuadrant t {dep})
ValidLens-LensA = CValidLens lensA (ValidLens-LensA-ViewSet) (ValidLens-LensA-SetView) (ValidLens-LensA-SetSet)

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
import      LibraBFT.Impl.Consensus.BlockStorage.BlockStore            as BlockStore
import      LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockStore as BSprops
open import LibraBFT.Impl.Consensus.EpochManager                       as EpochManager
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.MetricsSafetyRules                 as MetricsSafetyRules
open import LibraBFT.Impl.Consensus.Properties.MetricsSafetyRules
import      LibraBFT.Impl.Consensus.RoundManager                       as RoundManager
open import LibraBFT.Impl.Consensus.RoundManager.Properties
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRulesManager     as SafetyRulesManager
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Hash
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open InitProofDefs
open Invariants
open EpochManagerInv
open SafetyRulesInv
open SafetyDataInv

module LibraBFT.Impl.Consensus.EpochManager.Properties where

module newSpec
  (nodeConfig                : NodeConfig)
  (stateComp                 : StateComputer)
  (persistentLivenessStorage : PersistentLivenessStorage)
  (obmAuthor                 : Author)
  (obmSK                     : SK)
  where

  -- TODO-2: May require refinement (additional requirements and/or properties)
  Contract : EitherD-Post ErrLog EpochManager
  Contract (Left _)   = ⊤
  Contract (Right em) = ∀ {sr} → em ^∙ emSafetyRulesManager ∙ srmInternalSafetyRules ≡ SRWLocal sr
                               → sr ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ nothing

  postulate
    contract : Contract (EpochManager.new nodeConfig stateComp persistentLivenessStorage obmAuthor obmSK)

module startRoundManager'Spec
  (self0                : EpochManager)
  (now                  : Instant)
  (recoveryData         : RecoveryData)
  (epochState0          : EpochState)
  (obmNeedFetch         : ObmNeedFetch)
  (obmProposalGenerator : ProposalGenerator)
  (obmVersion           : Version)
  where

  open startRoundManager'-ed self0 now recoveryData epochState0
                             obmNeedFetch obmProposalGenerator obmVersion

  lastVote = recoveryData ^∙ rdLastVote
  proposalGenerator = obmProposalGenerator
  roundState = createRoundState-abs self0 now
  proposerElection = createProposerElection epochState0
  srUpdate : SafetyRules → SafetyRules
  srUpdate  = _& srPersistentStorage ∙ pssSafetyData ∙ sdEpoch ∙~ epochState0 ^∙ esEpoch
  initProcessor : SafetyRules → BlockStore → RoundManager
  initProcessor sr bs =
    RoundManager∙new
      obmNeedFetch
      epochState0
      bs
      roundState
      proposerElection
      proposalGenerator
      (srUpdate sr)
      (self0 ^∙ emConfig ∙ ccSyncOnly)

  ecInfo = mkECinfo (epochState0 ^∙ esVerifier) (epochState0 ^∙ esEpoch)

  SRVoteEpoch≡ : SafetyRules → Epoch → Set
  SRVoteEpoch≡ sr epoch = ∀ {v} → sr ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ just v
                                → v ^∙ vEpoch ≡ epoch

  SRVoteRound≤ : SafetyRules → Set
  SRVoteRound≤ sr = let sd = sr ^∙ srPersistentStorage ∙ pssSafetyData
                     in Meta.getLastVoteRound sd ≤ sd ^∙ sdLastVotedRound

  initRMInv : ∀ {sr bs}
            → ValidatorVerifier-correct (epochState0 ^∙ esVerifier)
            → SafetyDataInv (sr ^∙ srPersistentStorage ∙ pssSafetyData)
            → sr ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ nothing
            → BlockStoreInv (bs , ecInfo)
            → RoundManagerInv (initProcessor sr bs)
  initRMInv {sr} vvCorr sdInv refl bsInv = mkRoundManagerInv vvCorr refl bsInv (mkSafetyRulesInv (mkSafetyDataInv refl z≤n))

  contract-continue2 :
      ∀ {sr bs}
    → ValidatorVerifier-correct (epochState0 ^∙ esVerifier)
    → SafetyRulesInv sr
    → sr ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ nothing
    → BlockStoreInv (bs , ecInfo)
    → EitherD-weakestPre (continue2-abs lastVote bs sr) (InitContract lastVote)
  contract-continue2 {sr} {bs} vvCorr srInv lvNothing bsInv rewrite continue2-abs-≡
    with LBFT-contract (RoundManager.start-abs now lastVote)
                       (Contract initRM initRMCorr)
                       (initProcessor sr bs)
                       (contract' initRM initRMCorr)
      where
        open startSpec now lastVote
        initRM     = initProcessor sr bs
        initRMCorr = initRMInv {sr} {bs} vvCorr (sdInv srInv) lvNothing bsInv

  ...| inj₁ (_    , er≡j ) rewrite er≡j = tt
  ...| inj₂ (er≡n , ico) rewrite er≡n =
         LBFT-post (RoundManager.start-abs now lastVote)
                   (initProcessor sr bs)
         , refl , ico

  contract-continue1
    : ∀ {bs}
    → BlockStoreInv (bs , ecInfo)
    → ValidatorVerifier-correct (epochState0 ^∙ esVerifier)
    → EpochManagerInv self0
    → EitherD-weakestPre (continue1-abs lastVote bs) (InitContract lastVote)
  contract-continue1 {bs} bsInv vvCorr emi rewrite continue1-abs-≡
     with  self0 ^∙    emSafetyRulesManager ∙ srmInternalSafetyRules | inspect
          (self0 ^∙_) (emSafetyRulesManager ∙ srmInternalSafetyRules)
  ...| SRWLocal safetyRules | [ R ]
     with emiSRI emi R
  ...| (sri , lvNothing)
     with performInitializeSpec.contract safetyRules (self0 ^∙ emStorage) sri lvNothing
  ...| piProp
     with MetricsSafetyRules.performInitialize-abs safetyRules (self0 ^∙ emStorage)
  ...| Left _ = tt
  ...| Right sr = contract-continue2 vvCorr (performInitializeSpec.ContractOk.srPres    piProp sri)
                                            (performInitializeSpec.ContractOk.lvNothing piProp) bsInv

  contract' :
      ValidatorVerifier-correct (epochState0 ^∙ esVerifier)
    → EpochManagerInv self0
    → EitherD-weakestPre
                (EpochManager.startRoundManager'-ed-abs
                   self0 now recoveryData epochState0
                   obmNeedFetch obmProposalGenerator obmVersion)
              (InitContract lastVote)
  contract' vvCorr emi rewrite startRoundManager'-ed-abs-≡
     with BSprops.new.contract (self0 ^∙ emStorage) recoveryData stateComputer
                               (self0 ^∙ emConfig ∙ ccMaxPrunedBlocksInMem)
  ...| bsprop
     with BlockStore.new-e-abs (self0 ^∙ emStorage) recoveryData stateComputer
                               (self0 ^∙ emConfig ∙ ccMaxPrunedBlocksInMem)
  ...| Left  _  = tt
  ...| Right bs = contract-continue1 bsprop vvCorr emi


text:
{- https://lists.chalmers.se/pipermail/agda/2013/006033.html http://code.haskell.org/~Saizan/unification/ 18-Nov-2013 Andrea Vezzosi -}
module UnifyProof2 where

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality
open import Function
open import Relation.Nullary
open import Data.Product renaming (map to _***_)
open import Data.Empty
open import Data.Maybe using (maybe; nothing; just; monad; Maybe)
open import Data.Sum
open import Unify
open import UnifyProof
open Σ₁
open import Data.List renaming (_++_ to _++L_)
open ≡-Reasoning
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

-- We use a view so that we need to handle fewer cases in the main proof
data Amgu : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Maybe (∃ (AList m)) -> Set where
  Flip : ∀ {m s t acc} -> amgu t s acc ≡ amgu s t acc ->
    Amgu {m} t s acc (amgu t s acc) -> Amgu         s            t            acc        (amgu s t acc)
  leaf-leaf : ∀ {m acc} ->             Amgu {m}     leaf         leaf         acc        (just acc)
  leaf-fork : ∀ {m s t acc} ->         Amgu {m}     leaf         (s fork t)   acc        nothing
  fork-fork : ∀ {m s1 s2 t1 t2 acc} -> Amgu {m}     (s1 fork s2) (t1 fork t2) acc        (amgu s2 t2 =<< amgu s1 t1 acc)
  var-var   : ∀ {m x y} ->             Amgu         (i x)        (i y)        (m , anil) (just (flexFlex x y))
  var-t : ∀ {m x t} -> i x ≢ t ->      Amgu         (i x)        t            (m , anil) (flexRigid x t)
  s-t : ∀{m s t n σ r z} ->            Amgu {suc m} s            t            (n , σ asnoc r / z) ((λ σ -> σ ∃asnoc r / z) <$>
                                                                                amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ))

view : ∀ {m : ℕ} -> (s t : Term m) -> (acc : ∃ (AList m)) -> Amgu s t acc (amgu s t acc)
view leaf         leaf         acc        = leaf-leaf
view leaf         (s fork t)   acc        = leaf-fork
view (s fork t)   leaf         acc        = Flip refl leaf-fork
view (s1 fork s2) (t1 fork t2) acc        = fork-fork
view (i x)        (i y)        (m , anil) = var-var
view (i x)        leaf         (m , anil) = var-t (λ ())
view (i x)        (s fork t)   (m , anil) = var-t (λ ())
view leaf         (i x)        (m , anil) = Flip refl (var-t (λ ()))
view (s fork t)   (i x)        (m , anil) = Flip refl (var-t (λ ()))
view (i x)        (i x')       (n , σ asnoc r / z) = s-t
view (i x)        leaf         (n , σ asnoc r / z) = s-t
view (i x)        (s fork t)   (n , σ asnoc r / z) = s-t
view leaf         (i x)        (n , σ asnoc r / z) = s-t
view (s fork t)   (i x)        (n , σ asnoc r / z) = s-t

amgu-Correctness : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Set
amgu-Correctness s t (l , ρ) =
    (∃ λ n → ∃ λ σ → π₁ (Max (Unifies s t [-◇ sub ρ ])) (sub σ) × amgu s t (l , ρ) ≡ just (n , σ ++ ρ ))
  ⊎ (Nothing ((Unifies s t) [-◇ sub ρ ]) ×  amgu s t (l , ρ) ≡ nothing)

amgu-Ccomm : ∀ {m} s t acc -> amgu {m} s t acc ≡ amgu t s acc -> amgu-Correctness s t acc -> amgu-Correctness t s acc
amgu-Ccomm s t (l , ρ) st≡ts = lemma
  where
    Unst = (Unifies s t) [-◇ sub ρ ]
    Unts = (Unifies t s) [-◇ sub ρ ]

    Unst⇔Unts : ((Unifies s t) [-◇ sub ρ ]) ⇔ ((Unifies t s) [-◇ sub ρ ])
    Unst⇔Unts = Properties.fact5 (Unifies s t) (Unifies t s) (sub ρ) (Properties.fact1 {_} {s} {t})

    lemma : amgu-Correctness s t (l , ρ) -> amgu-Correctness t s (l , ρ)
    lemma (inj₁ (n , σ , MaxUnst , amgu≡just)) =
      inj₁ (n , σ , proj₁ (Max.fact Unst Unts Unst⇔Unts (sub σ)) MaxUnst , trans (sym st≡ts) amgu≡just)
    lemma (inj₂ (NoUnst , amgu≡nothing)) =
      inj₂ ((λ {_} → Properties.fact2 Unst Unts Unst⇔Unts NoUnst) , trans (sym st≡ts) amgu≡nothing)

amgu-c : ∀ {m s t l ρ} -> Amgu s t (l , ρ) (amgu s t (l , ρ)) ->
           (∃ λ n → ∃ λ σ → π₁ (Max ((Unifies s t) [-◇ sub ρ ])) (sub σ) × amgu {m} s t (l , ρ) ≡ just (n , σ ++ ρ ))
         ⊎ (Nothing ((Unifies s t) [-◇ sub ρ ])                          × amgu {m} s t (l , ρ) ≡ nothing)
amgu-c {m} {s} {t} {l} {ρ} amg with amgu s t (l , ρ)
amgu-c {l = l} {ρ} leaf-leaf | ._
  = inj₁ (l , anil , trivial-problem {_} {_} {leaf} {sub ρ} , cong (λ x -> just (l , x)) (sym (SubList.anil-id-l ρ)) )
amgu-c leaf-fork | .nothing = inj₂ ((λ _ () ) , refl)
amgu-c {m} {s1 fork s2} {t1 fork t2} {l} {ρ} fork-fork | ._
  with amgu s1 t1 (l , ρ)  | amgu-c $ view s1 t1 (l , ρ)
...  | .nothing            | inj₂ (nounify , refl) = inj₂ ((λ {_} -> No[Q◇ρ]→No[P◇ρ] No[Q◇ρ]) , refl)
  where
    P = Unifies (s1 fork s2) (t1 fork t2)
    Q = (Unifies s1 t1 ∧ Unifies s2 t2)
    Q⇔P : Q ⇔ P
    Q⇔P = switch P Q (Properties.fact1' {_} {s1} {s2} {t1} {t2})
    No[Q◇ρ]→No[P◇ρ] : Nothing (Q [-◇ sub ρ ]) -> Nothing (P [-◇ sub ρ ])
    No[Q◇ρ]→No[P◇ρ] = Properties.fact2 (Q [-◇ sub ρ ]) (P [-◇ sub ρ ]) (Properties.fact5 Q P (sub ρ) Q⇔P)
    No[Q◇ρ] : Nothing (Q [-◇ sub ρ ])
    No[Q◇ρ] = failure-propagation.first (sub ρ) (Unifies s1 t1) (Unifies s2 t2) nounify

... | .(just (n , σ ++ ρ)) | inj₁ (n , σ , a , refl)
 with amgu s2 t2 (n , σ ++ ρ) | amgu-c (view s2 t2 (n , (σ ++ ρ)))
... | .nothing                | inj₂ (nounify , refl) = inj₂ ( (λ {_} -> No[Q◇ρ]→No[P◇ρ] No[Q◇ρ]) , refl)
    where
    P = Unifies (s1 fork s2) (t1 fork t2)
    Q = (Unifies s1 t1 ∧ Unifies s2 t2)
    Q⇔P : Q ⇔ P
    Q⇔P = switch P Q (Properties.fact1' {_} {s1} {s2} {t1} {t2})
    No[Q◇ρ]→No[P◇ρ] : Nothing (Q [-◇ sub ρ ]) -> Nothing (P [-◇ sub ρ ])
    No[Q◇ρ]→No[P◇ρ] = Properties.fact2 (Q [-◇ sub ρ ]) (P [-◇ sub ρ ]) (Properties.fact5 Q P (sub ρ) Q⇔P)
    No[Q◇ρ] : Nothing (Q [-◇ sub ρ ])
    No[Q◇ρ] = failure-propagation.second (sub ρ) (sub σ) (Unifies s1 t1) (Unifies s2 t2) a
       (λ f Unifs2t2-f◇σ◇ρ → nounify f (π₂ (Unifies s2 t2) (λ t → cong (f ◃) (sym (SubList.fact1 σ ρ t))) Unifs2t2-f◇σ◇ρ))

... | .(just (n1 , σ1 ++ (σ ++ ρ))) | inj₁ (n1 , σ1 , b , refl)
    = inj₁ (n1 , σ1 ++ σ , Max[P∧Q◇ρ][σ1++σ] , cong (λ σ -> just (n1 , σ)) (++-assoc σ1 σ ρ))
    where
      P = Unifies s1 t1
      Q = Unifies s2 t2
      P∧Q = P ∧ Q
      C = Unifies (s1 fork s2) (t1 fork t2)
      Max[C◇ρ]⇔Max[P∧Q◇ρ] : Max (C [-◇ sub ρ ]) ⇔ Max (P∧Q [-◇ sub ρ ])
      Max[C◇ρ]⇔Max[P∧Q◇ρ] = Max.fact (C [-◇ sub ρ ]) (P∧Q [-◇ sub ρ ]) (Properties.fact5 C P∧Q (sub ρ)
                      (Properties.fact1' {_} {s1} {s2} {t1} {t2}))
      Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] : Max (Q [-◇ sub (σ ++ ρ)]) ⇔ Max (Q [-◇ sub σ ◇ sub ρ ])
      Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] = Max.fact (Q [-◇ sub (σ ++ ρ)]) (Q [-◇ sub σ ◇ sub ρ ]) (Properties.fact6 Q (SubList.fact1 σ ρ))
      Max[P∧Q◇ρ][σ1++σ] : π₁ (Max (C [-◇ sub ρ ])) (sub (σ1 ++ σ))
      Max[P∧Q◇ρ][σ1++σ] = π₂ (Max (C [-◇ sub ρ ])) (≐-sym (SubList.fact1 σ1 σ))
               (proj₂ (Max[C◇ρ]⇔Max[P∧Q◇ρ] (sub σ1 ◇ sub σ))
                      (optimist (sub ρ) (sub σ) (sub σ1) P Q (DClosed.fact1 s1 t1) a (proj₁ (Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] (sub σ1)) b)))

amgu-c {suc l} {i x} {i y} (var-var) | .(just (flexFlex x y))
   with thick x y | Thick.fact1 x y (thick x y) refl
...  | .(just y') | inj₂ (y' , thinxy'≡y , refl )
  = inj₁ (l , anil asnoc i y' / x , var-elim-i-≡ x (i y) (sym (cong i thinxy'≡y)) , refl )
...  | .nothing | inj₁ ( x≡y , refl ) rewrite sym x≡y
  = inj₁ (suc l , anil , trivial-problem {_} {_} {i x} {sub anil} , refl)
amgu-c {suc l} {i x} {t} (var-t ix≢t) | .(flexRigid x t)
 with check x t | check-prop x t
... | .nothing  | inj₂ ( ps , r , refl) = inj₂ ( (λ {_} -> No-Unifier )  , refl)
  where
    No-Unifier : {n : ℕ} (f : Fin (suc l) → Term n) → f x ≡ f ◃ t → ⊥
    No-Unifier f fx≡f◃t = ix≢t (sym (trans r (cong (λ ps -> ps ⊹ i x) ps≡[])))
          where
            ps≡[] : ps ≡ []
            ps≡[] = map-[] f ps (No-Cycle (f x) ((f ◃S) ps)
                  (begin f x             ≡⟨ fx≡f◃t ⟩
                         f ◃ t           ≡⟨ cong (f ◃) r ⟩
                         f ◃ (ps ⊹ i x)  ≡⟨ StepM.fact2 f (i x) ps ⟩
                         (f ◃S) ps ⊹ f x ∎))

... | .(just t') | inj₁ (t' , r , refl) = inj₁ ( l , anil asnoc t' / x , var-elim-i-≡ x t r , refl )

amgu-c {suc m} {s} {t} {l} {ρ asnoc r / z} s-t
  | .((λ x' → x' ∃asnoc r / z) <$>
      (amgu ((r for z) ◃ s) ((r for z) ◃ t) (l , ρ)))
  with amgu-c (view ((r for z) ◃ s) ((r for z) ◃ t) (l , ρ))
... | inj₂ (nounify , ra) = inj₂ ( (λ {_} -> NoQ→NoP nounify) , cong (_<$>_ (λ x' → x' ∃asnoc r / z)) ra )
      where
        P = Unifies s t [-◇ sub (ρ asnoc r / z) ]
        Q = Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub ρ ]
        NoQ→NoP : Nothing Q → Nothing P
        NoQ→NoP = Properties.fact2 Q P (switch P Q (step-prop s t ρ r z))
... | inj₁ (n , σ , a , ra)  = inj₁ (n , σ , proj₂ (MaxP⇔MaxQ (sub σ)) a , cong (_<$>_ (λ x' → x' ∃asnoc r / z)) ra)
      where
        P = Unifies s t [-◇ sub (ρ asnoc r / z) ]
        Q = Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub ρ ]
        MaxP⇔MaxQ : Max P ⇔ Max Q
        MaxP⇔MaxQ = Max.fact P Q (step-prop s t ρ r z)
amgu-c {m} {s} {t} {l} {ρ} (Flip amguts≡amgust amguts) | ._ = amgu-Ccomm t s (l , ρ) amguts≡amgust (amgu-c amguts)
amgu-c {zero} {i ()}  _ | _

mgu-c : ∀ {m} (s t : Term m) ->
          (∃ λ n → ∃ λ σ → π₁ (Max (Unifies s t)) (sub σ) × mgu s t ≡ just (n , σ))
        ⊎ (Nothing (Unifies s t)                          × mgu s t ≡ nothing)
mgu-c {m} s t = amgu-c (view s t (m , anil))


text:
{-# OPTIONS --without-K #-}
module sets.fin.ordering where

open import equality.core
open import function.isomorphism
open import sets.core
open import sets.fin.core
open import sets.fin.properties
import sets.nat.ordering as N

_<_ : ∀ {n} → Fin n → Fin n → Set
i < j = toℕ i N.< toℕ j
infixr 4 _<_

ord-from-ℕ : ∀ {n} {i j : Fin n}
           → Ordering N._<_ (toℕ i) (toℕ j)
           → Ordering _<_ i j
ord-from-ℕ (lt p) = lt p
ord-from-ℕ (eq p) = eq (toℕ-inj p)
ord-from-ℕ (gt p) = gt p

compare : ∀ {n} → (i j : Fin n) → Ordering _<_ i j
compare i j = ord-from-ℕ (N.compare (toℕ i) (toℕ j))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module ComplexIMPORT where

{-# IMPORT Prelude as P #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module AmbiguousModule where

module A where
module B where
  module A where

open B
open A


text:
{-# OPTIONS --cubical --no-import-sorts --safe --guardedness #-}
module Cubical.Codata.Stream.Base where

open import Cubical.Core.Everything

record Stream (A : Type₀) : Type₀ where
  coinductive
  constructor _,_
  field
    head : A
    tail : Stream A

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:
module Pragmas where

-- Check that Haskell code is parsed with the correct language pragmas
{-# FOREIGN AGDA2HS
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
#-}

{-# FOREIGN AGDA2HS
foo :: Bool -> a -> (a, Int)
foo = \ case
  False -> (, 0)
  True  -> (, 1)
#-}


text:
postulate
  F : Set → Set

G : Set
G = {!F ?!}

-- KEEP COMMENTS AT THE END to not mess with the ranges in Issue2174.sh

-- Andreas, 2016-09-10, issue #2174 reported by Nisse

-- First infer, then give should goalify the questionmark


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function using (id; flip)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Functions.Embedding

open import Cubical.Data.Nat hiding (_+_; _*_)
open import Cubical.Data.NatPlusOne using (ℕ₊₁→ℕ)
open import Cubical.Data.Int
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Data.Prod

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Group.Morphism

open import Cubical.Algebra.Monoid.Properties using (isPropIsMonoid; module MonoidLemmas)

open import Cubical.Relation.Unary as Unary hiding (isPropValued)
open import Cubical.Relation.Binary as Binary hiding (isPropValued)
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Relation.Binary.Reasoning.Equality

open import Cubical.Algebra.Group.MorphismProperties public
  using (GroupPath; uaGroup; carac-uaGroup; Group≡; caracGroup≡)

private
  variable
    ℓ ℓ′ : Level

isPropIsGroup : ∀ {G : Type ℓ} {_•_ ε _⁻¹} → isProp (IsGroup G _•_ ε _⁻¹)
isPropIsGroup {G = G} {_•_} {ε} {_⁻¹} (isgroup aMon aInv) (isgroup bMon bInv) =
  cong₂ isgroup (isPropIsMonoid aMon bMon) (isPropInverse (IsMonoid.is-set aMon) _•_ _⁻¹ ε aInv bInv)

module GroupLemmas (G : Group ℓ) where
  open Group G

  open MonoidLemmas monoid public using (ε-comm) renaming (_^′_ to _^′′_; ^semi≡^ to ^semi≡^mon)

  invInvo : Involutive _⁻¹
  invInvo a = cancelʳ (a ⁻¹) (inverseˡ (a ⁻¹) ∙ sym (inverseʳ a))

  invId : ε ⁻¹ ≡ ε
  invId = cancelʳ ε (inverseˡ ε ∙ sym (identityʳ ε))

  invDistr : Homomorphic₂ _⁻¹ _•_ (flip _•_)
  invDistr x y = sym (inv-uniqueˡ _ _ (
    (x • y) • (y ⁻¹ • x ⁻¹)
      ≡˘⟨ assoc (x • y) (y ⁻¹) (x ⁻¹) ⟩
    x • y / y / x
      ≡⟨ cong (_/ x) (assoc _ _ _ ∙ cong (x •_) (inverseʳ y)) ⟩
    x • ε / x
      ≡⟨ cong (_/ x) (identityʳ x) ∙ inverseʳ x ⟩
    ε ∎))

  inv-comm : ∀ x → x • x ⁻¹ ≡ x ⁻¹ • x
  inv-comm x = inverseʳ x ∙ sym (inverseˡ x)

  isEquiv-•ˡ : ∀ x → isEquiv (x •_)
  isEquiv-•ˡ x = isoToIsEquiv (iso _ (x ⁻¹ •_) section-• retract-•)
    where
      section-• : section (x •_) (x ⁻¹ •_)
      section-• y =
        x • (x ⁻¹ • y) ≡˘⟨ assoc x (x ⁻¹) y ⟩
        x • x ⁻¹ • y   ≡⟨ cong (_• y) (inverseʳ x) ⟩
        ε • y          ≡⟨ identityˡ y ⟩
        y              ∎

      retract-• : retract (x •_) (x ⁻¹ •_)
      retract-• y =
        x ⁻¹ • (x • y) ≡˘⟨ assoc (x ⁻¹) x y ⟩
        x ⁻¹ • x • y   ≡⟨ cong (_• y) (inverseˡ x) ⟩
        ε • y          ≡⟨ identityˡ y ⟩
        y              ∎

  isEquiv-•ʳ : ∀ x → isEquiv (_• x)
  isEquiv-•ʳ x = isoToIsEquiv (iso _ (_• x ⁻¹) section-• retract-•)
    where
      section-• : section (_• x) (_• x ⁻¹)
      section-• y =
        y • x ⁻¹ • x   ≡⟨ assoc y (x ⁻¹) x ⟩
        y • (x ⁻¹ • x) ≡⟨ cong (y •_) (inverseˡ x) ⟩
        y • ε          ≡⟨ identityʳ y ⟩
        y              ∎

      retract-• : retract (_• x) (_• x ⁻¹)
      retract-• y =
        y • x • x ⁻¹   ≡⟨ assoc y x (x ⁻¹) ⟩
        y • (x • x ⁻¹) ≡⟨ cong (y •_) (inverseʳ x) ⟩
        y • ε          ≡⟨ identityʳ y ⟩
        y              ∎

  inv-≡ʳ : ∀ {x y} → x • y ⁻¹ ≡ ε → x ≡ y
  inv-≡ʳ p = inv-uniqueʳ _ _ p ∙ invInvo _

  inv-≡ˡ : ∀ {x y} → x ⁻¹ • y ≡ ε → x ≡ y
  inv-≡ˡ p = sym (invInvo _) ∙ sym (inv-uniqueˡ _ _ p)

  ≡-invʳ : ∀ {x y} → x ≡ y → x • y ⁻¹ ≡ ε
  ≡-invʳ p = subst (λ y → _ • y ⁻¹ ≡ ε) p (inverseʳ _)

  ≡-invˡ : ∀ {x y} → x ≡ y → x ⁻¹ • y ≡ ε
  ≡-invˡ p = subst (λ y → _ • y ≡ ε) p (inverseˡ _)

  ^-sucˡ : ∀ x n → x ^ sucInt n ≡ x • x ^ n
  ^-sucˡ x (pos n)                = refl
  ^-sucˡ x (negsuc zero)          = sym (inverseʳ x)
  ^-sucˡ x (negsuc (suc zero))    =
    x ^ -1          ≡⟨⟩
    x ⁻¹            ≡˘⟨ identityˡ _ ⟩
    ε • x ⁻¹        ≡˘⟨ cong (_• x ⁻¹) (inverseʳ x) ⟩
    x • x ⁻¹ • x ⁻¹ ≡⟨ assoc _ _ _ ⟩
    x • (x ^ -2)    ∎
  ^-sucˡ x (negsuc (suc (suc n))) =
    x ^ sucInt (negsuc (suc (suc n)))  ≡⟨⟩
    x ^ negsuc (suc n)                 ≡⟨⟩
    x ⁻¹ • x ^ negsuc n                ≡⟨⟩
    x ⁻¹ • x ^ sucInt (negsuc (suc n)) ≡⟨ cong (x ⁻¹ •_) (^-sucˡ x (negsuc (suc n))) ⟩
    x ⁻¹ • (x • x ^ negsuc (suc n))    ≡˘⟨ assoc _ _ _ ⟩
    x ⁻¹ • x • x ^ negsuc (suc n)      ≡˘⟨ cong (_• x ^ negsuc (suc n)) (inv-comm x) ⟩
    x • x ⁻¹ • x ^ negsuc (suc n)      ≡⟨ assoc _ _ _ ⟩
    x • (x ⁻¹ • x ^ negsuc (suc n))    ≡⟨⟩
    x • x ^ negsuc (suc (suc n))       ∎

  ^-sucʳ : ∀ x n → x ^ sucInt n ≡ x ^ n • x
  ^-sucʳ x (pos zero)       = ε-comm x
  ^-sucʳ x (pos (suc n))    =
    x ^ pos (suc (suc n)) ≡⟨⟩
    x • x ^ pos (suc n)   ≡⟨ cong (x •_) (^-sucʳ x (pos n)) ⟩
    x • (x ^ pos n • x)   ≡˘⟨ assoc _ _ _ ⟩
    x • x ^ pos n • x     ≡⟨⟩
    x ^ pos (suc n) • x   ∎
  ^-sucʳ x (negsuc zero)          = sym (inverseˡ x)
  ^-sucʳ x (negsuc (suc zero))    =
    x ⁻¹              ≡˘⟨ identityʳ _ ⟩
    x ⁻¹ • ε          ≡˘⟨ cong (x ⁻¹ •_) (inverseˡ x) ⟩
    x ⁻¹ • (x ⁻¹ • x) ≡˘⟨ assoc _ _ _ ⟩
    x ^ -2 • x        ∎
  ^-sucʳ x (negsuc (suc (suc n))) =
    x ^ sucInt (negsuc (suc (suc n)))  ≡⟨⟩
    x ^ negsuc (suc n)                 ≡⟨⟩
    x ⁻¹ • x ^ negsuc n                ≡⟨⟩
    x ⁻¹ • x ^ sucInt (negsuc (suc n)) ≡⟨ cong (x ⁻¹ •_) (^-sucʳ x (negsuc (suc n))) ⟩
    x ⁻¹ • (x ^ negsuc (suc n) • x)    ≡˘⟨ assoc _ _ _ ⟩
    x ⁻¹ • x ^ negsuc (suc n) • x      ≡⟨⟩
    x ^ negsuc (suc (suc n)) • x       ∎

  ^-predˡ : ∀ x n → x ^ predInt n ≡ x ⁻¹ • x ^ n
  ^-predˡ x (pos zero) = sym (identityʳ _)
  ^-predˡ x (pos (suc zero)) =
    ε              ≡˘⟨ inverseˡ x ⟩
    x ⁻¹ • x       ≡˘⟨ cong (x ⁻¹ •_) (identityʳ x) ⟩
    x ⁻¹ • (x • ε) ∎
  ^-predˡ x (pos (suc (suc n))) =
    x ^ predInt (pos (suc (suc n))) ≡⟨⟩
    x ^ pos (suc n)                 ≡⟨⟩
    x • x ^ pos n                   ≡⟨⟩
    x • x ^ predInt (pos (suc n))   ≡⟨ cong (x •_) (^-predˡ x (pos (suc n))) ⟩
    x • (x ⁻¹ • x ^ pos (suc n))    ≡˘⟨ assoc _ _ _ ⟩
    x • x ⁻¹ • x ^ pos (suc n)      ≡⟨ cong (_• x ^ pos (suc n)) (inv-comm x) ⟩
    x ⁻¹ • x • x ^ pos (suc n)      ≡⟨ assoc _ _ _ ⟩
    x ⁻¹ • (x • x ^ pos (suc n))    ≡⟨⟩
    x ⁻¹ • x ^ pos (suc (suc n))    ∎
  ^-predˡ x (negsuc n) = refl

  ^-predʳ : ∀ x n → x ^ predInt n ≡ x ^ n • x ⁻¹
  ^-predʳ x (pos zero) = sym (identityˡ _)
  ^-predʳ x (pos (suc zero)) =
    ε              ≡˘⟨ identityʳ _ ⟩
    ε • ε          ≡˘⟨ cong (ε •_) (inverseʳ _) ⟩
    ε • (x • x ⁻¹) ≡˘⟨ assoc _ _ _ ⟩
    ε • x • x ⁻¹   ≡˘⟨ cong (_• x ⁻¹) (ε-comm _) ⟩
    x • ε • x ⁻¹   ∎
  ^-predʳ x (pos (suc (suc n))) =
    x ^ predInt (pos (suc (suc n))) ≡⟨⟩
    x ^ pos (suc n)                 ≡⟨⟩
    x • x ^ pos n                   ≡⟨⟩
    x • x ^ predInt (pos (suc n))   ≡⟨ cong (x •_) (^-predʳ x (pos (suc n))) ⟩
    x • (x ^ pos (suc n) • x ⁻¹)    ≡˘⟨ assoc _ _ _ ⟩
    x • x ^ pos (suc n) • x ⁻¹      ≡⟨⟩
    x ^ pos (suc (suc n)) • x ⁻¹    ∎
  ^-predʳ x (negsuc zero) = refl
  ^-predʳ x (negsuc (suc n)) =
    x ^ predInt (negsuc (suc n))  ≡⟨⟩
    x ^ negsuc (suc (suc n))      ≡⟨⟩
    x ⁻¹ • x ^ negsuc (suc n)     ≡⟨⟩
    x ⁻¹ • x ^ predInt (negsuc n) ≡⟨ cong (x ⁻¹ •_) (^-predʳ x (negsuc n)) ⟩
    x ⁻¹ • (x ^ negsuc n • x ⁻¹)  ≡˘⟨ assoc _ _ _ ⟩
    x ⁻¹ • x ^ negsuc n • x ⁻¹    ≡⟨⟩
    x ^ negsuc (suc n) • x ⁻¹     ∎

  ^-plus : ∀ x → Homomorphic₂ (x ^_) _+_ _•_
  ^-plus x m (pos zero) = sym (identityʳ (x ^ m))
  ^-plus x m (pos (suc n)) =
    x ^ sucInt (m +pos n)   ≡⟨ ^-sucʳ x (m +pos n) ⟩
    x ^ (m +pos n) • x      ≡⟨ cong (_• x) (^-plus x m (pos n)) ⟩
    x ^ m • x ^ pos n • x   ≡⟨ assoc _ _ _ ⟩
    x ^ m • (x ^ pos n • x) ≡˘⟨ cong (x ^ m •_) (^-sucʳ x (pos n)) ⟩
    x ^ m • x ^ pos (suc n) ∎
  ^-plus x m (negsuc zero) = ^-predʳ x m
  ^-plus x m (negsuc (suc n)) =
    x ^ predInt (m +negsuc n)     ≡⟨ ^-predʳ x (m +negsuc n) ⟩
    x ^ (m +negsuc n) • x ⁻¹      ≡⟨ cong (_• x ⁻¹) (^-plus x m (negsuc n)) ⟩
    x ^ m • x ^ negsuc n • x ⁻¹   ≡⟨ assoc _ _ _ ⟩
    x ^ m • (x ^ negsuc n • x ⁻¹) ≡˘⟨ cong (x ^ m •_) (^-predʳ x (negsuc n)) ⟩
    x ^ m • x ^ negsuc (suc n)    ∎

  _^′_ : ⟨ G ⟩ → ℕ → ⟨ G ⟩
  _^′_ = IsMonoid._^_ isMonoid

  ^mon≡^ : ∀ x n → x ^′ n ≡ x ^ pos n
  ^mon≡^ x zero = refl
  ^mon≡^ x (suc n) = cong (x •_) (^mon≡^ x n)

  ^semi≡^ : ∀ x n → x ^′′ n ≡ x ^ pos (ℕ₊₁→ℕ n)
  ^semi≡^ x n = ^semi≡^mon x n ∙ ^mon≡^ x (ℕ₊₁→ℕ n)

module Conjugation (G : Group ℓ) where
  open Group G
  open GroupLemmas G using (isEquiv-•ˡ; isEquiv-•ʳ)

  module _ (g : ⟨ G ⟩) where

    conjugate : ⟨ G ⟩ → ⟨ G ⟩
    conjugate x = g • x • g ⁻¹

    conjugate-isEquiv : isEquiv conjugate
    conjugate-isEquiv = compIsEquiv (isEquiv-•ˡ g) (isEquiv-•ʳ (g ⁻¹))

    conjugate-hom : Homomorphic₂ conjugate _•_ _•_
    conjugate-hom x y =
      g • (x • y) • g ⁻¹              ≡˘⟨ cong (λ v → g • (v • y) • g ⁻¹) (identityʳ x) ⟩
      g • (x • ε • y) • g ⁻¹          ≡˘⟨ cong (λ v → g • (x • v • y) • g ⁻¹) (inverseˡ g) ⟩
      g • (x • (g ⁻¹ • g) • y) • g ⁻¹ ≡˘⟨ cong (λ v → g • (v • y) • g ⁻¹) (assoc _ _ _) ⟩
      g • (x • g ⁻¹ • g • y) • g ⁻¹   ≡˘⟨ cong (_• g ⁻¹) (assoc _ _ _) ⟩
      g • (x • g ⁻¹ • g) • y • g ⁻¹   ≡˘⟨ cong (λ v → v • y • g ⁻¹) (assoc _ _ _) ⟩
      g • (x • g ⁻¹) • g • y • g ⁻¹   ≡˘⟨ cong (λ v → v • g • y • g ⁻¹) (assoc _ _ _) ⟩
      g • x • g ⁻¹ • g • y • g ⁻¹     ≡⟨ cong (_• g ⁻¹) (assoc _ _ _) ⟩
      g • x • g ⁻¹ • (g • y) • g ⁻¹   ≡⟨ assoc _ _ _ ⟩
      g • x • g ⁻¹ • (g • y • g ⁻¹)   ∎

    conjugate-isHom : IsGroupHom G G conjugate
    conjugate-isHom = isgrouphom conjugate-hom

    conjugate-Hom : GroupHom G G
    conjugate-Hom = record { isHom = conjugate-isHom }

    conjugate-Equiv : GroupEquiv G G
    conjugate-Equiv = record { eq = conjugate , conjugate-isEquiv; isHom = conjugate-isHom }

    conjugate-Path : G ≡ G
    conjugate-Path = uaGroup conjugate-Equiv

  Conjugate : Rel ⟨ G ⟩ ℓ
  Conjugate a b = (∃[ g ∈ ⟨ G ⟩ ] conjugate g a ≡ b) , squash

module Kernel {G : Group ℓ} {H : Group ℓ′} (hom : GroupHom G H) where
  private
    module G = Group G
    module H = Group H
  open GroupHom hom renaming (fun to f)
  open GroupLemmas

  Kernel′ : RawPred ⟨ G ⟩ ℓ′
  Kernel′ x = f x ≡ H.ε

  isPropKernel : Unary.isPropValued Kernel′
  isPropKernel x = H.is-set (f x) H.ε

  Kernel : Pred ⟨ G ⟩ ℓ′
  Kernel = Unary.fromRaw Kernel′ isPropKernel

  ker-preservesId : G.ε ∈ Kernel
  ker-preservesId = preservesId

  ker-preservesOp : G._•_ Unary.Preserves₂ Kernel
  ker-preservesOp {x} {y} fx≡ε fy≡ε =
    f (x G.• y) ≡⟨ preservesOp x y ⟩
    f x H.• f y ≡⟨ cong₂ H._•_ fx≡ε fy≡ε ⟩
    H.ε H.• H.ε ≡⟨ H.identityʳ H.ε ⟩
    H.ε         ∎

  ker-preservesInv : G._⁻¹ Unary.Preserves Kernel
  ker-preservesInv {x} fx≡ε =
    f (x G.⁻¹) ≡⟨ preservesInv _ ⟩
    f x H.⁻¹   ≡⟨ cong H._⁻¹ fx≡ε ⟩
    H.ε H.⁻¹   ≡⟨ invId H ⟩
    H.ε        ∎

  ker⊆ε→inj : Kernel ⊆ ｛ G.ε ｝ → ∀ {x y} → f x ≡ f y → x ≡ y
  ker⊆ε→inj sub fx≡fy = inv-≡ʳ G (rec (G.is-set _ _) id (sub (preservesOp+Inv _ _ ∙ ≡-invʳ H fx≡fy)))
    where
      preservesOp+Inv : ∀ a b → f (a G.• b G.⁻¹) ≡ f a H.• f b H.⁻¹
      preservesOp+Inv a b = preservesOp a (b G.⁻¹) ∙ cong (f a H.•_) (preservesInv b)

  ker⊆ε→emb : Kernel ⊆ ｛ G.ε ｝ → isEmbedding f
  ker⊆ε→emb sub = injEmbedding G.is-set H.is-set (ker⊆ε→inj sub)

  inj→ker⊆ε : (∀ {x y} → f x ≡ f y → x ≡ y) → Kernel ⊆ ｛ G.ε ｝
  inj→ker⊆ε inj fx≡ε = ∣ inj (fx≡ε ∙ sym preservesId) ∣

  emb→ker⊆ε : isEmbedding f → Kernel ⊆ ｛ G.ε ｝
  emb→ker⊆ε emb = inj→ker⊆ε (invIsEq (emb _ _))


text:
------------------------------------------------------------------------
-- The syntax of the untyped λ-calculus
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Lambda.Simplified.Syntax where

open import Equality.Propositional
open import Prelude

open import Vec.Function equality-with-J

------------------------------------------------------------------------
-- Terms

-- Variables are represented using de Bruijn indices.

infixl 9 _·_

data Tm (n : ℕ) : Type where
  var : (x : Fin n) → Tm n
  ƛ   : Tm (suc n) → Tm n
  _·_ : Tm n → Tm n → Tm n

------------------------------------------------------------------------
-- Closure-based definition of values

-- Environments and values. Defined in a module parametrised by the
-- type of terms.

module Closure (Tm : ℕ → Type) where

  mutual

    -- Environments.

    Env : ℕ → Type
    Env n = Vec Value n

    -- Values. Lambdas are represented using closures, so values do
    -- not contain any free variables.

    data Value : Type where
      ƛ : ∀ {n} (t : Tm (suc n)) (ρ : Env n) → Value

------------------------------------------------------------------------
-- Examples

-- A non-terminating term.

ω : Tm 0
ω = ƛ (var fzero · var fzero)

Ω : Tm 0
Ω = ω · ω

-- A call-by-value fixpoint combinator.

Z : Tm 0
Z = ƛ (t · t)
  where
  t = ƛ (var (fsuc fzero) ·
         ƛ (var (fsuc fzero) · var (fsuc fzero) · var fzero))

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Classical.Semantics.Homomorphism (𝔏 : Signature) where
open Signature(𝔏)

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.ListSized
open import Data.ListSized.Functions
open import Formalization.PredicateLogic.Classical.Semantics(𝔏)
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Functional using (_∘_ ; _∘₂_ ; _←_)
open import Logic.Propositional as Logic using (_↔_)
import      Logic.Predicate     as Logic
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Natural
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet)
open        Sets.PredicateSet.BoundedQuantifiers
open import Structure.Function.Domain
open import Syntax.Function
open import Type.Dependent renaming (intro to _,_)
open import Type.Properties.Decidable
open import Type

private variable ℓ ℓₘ ℓₘ₁ ℓₘ₂ ℓₑ : Lvl.Level
private variable P : Type{ℓₚ}
private variable args n vars : ℕ
private variable 𝔐 : Model

private variable A B C S : Model{ℓₘ}
private variable fi : Obj n
private variable ri : Prop n
private variable xs : List(dom(S))(n)

record Homomorphism (A : Model{ℓₘ₁}) (B : Model{ℓₘ₂}) (f : dom(A) → dom(B)) : Type{ℓₚ Lvl.⊔ ℓₒ Lvl.⊔ Lvl.of(Type.of A) Lvl.⊔ Lvl.of(Type.of B)} where
  field
    preserve-functions : ∀{xs} → (f(fn(A) fi xs) ≡ fn(B) fi (map f xs))
    preserve-relations : ∀{xs} → IsTrue(rel(A) ri xs) → IsTrue(rel(B) ri (map f xs))

_→ₛₜᵣᵤ_ : Model{ℓₘ₁} → Model{ℓₘ₂} → Type
A →ₛₜᵣᵤ B = Logic.∃(Homomorphism A B)

record Embedding (A : Model{ℓₘ₁}) (B : Model{ℓₘ₂}) (f : dom(A) → dom(B)) : Type{ℓₚ Lvl.⊔ ℓₒ Lvl.⊔ Lvl.of(Type.of A) Lvl.⊔ Lvl.of(Type.of B)} where
  constructor intro
  field
    ⦃ homomorphism ⦄ : Homomorphism(A)(B)(f)
    ⦃ injection ⦄    : Injective(f)
    preserve-relations-converse : ∀{xs} → IsTrue(rel(A) ri xs) ← IsTrue(rel(B) ri (map f xs))

open import Data
open import Data.Boolean.Stmt
open import Data.ListSized.Proofs
open import Functional
open import Function.Equals
open import Function.Proofs
open import Lang.Instance
open import Logic.Predicate
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Transitivity

idₛₜᵣᵤ : A →ₛₜᵣᵤ A
∃.witness idₛₜᵣᵤ = id
Homomorphism.preserve-functions (∃.proof (idₛₜᵣᵤ {A = A})) {n} {fi} {xs} = congruence₁(fn A fi) (symmetry(_≡_) (_⊜_.proof map-id))
Homomorphism.preserve-relations (∃.proof (idₛₜᵣᵤ {A = A})) {n} {ri} {xs} = substitute₁ₗ(IsTrue ∘ rel A ri) (_⊜_.proof map-id)

_∘ₛₜᵣᵤ_ : let _ = A ; _ = B ; _ = C in (B →ₛₜᵣᵤ C) → (A →ₛₜᵣᵤ B) → (A →ₛₜᵣᵤ C)
∃.witness (([∃]-intro f) ∘ₛₜᵣᵤ ([∃]-intro g)) = f ∘ g
Homomorphism.preserve-functions (∃.proof (_∘ₛₜᵣᵤ_ {A = A} {B = B} {C = C} ([∃]-intro f ⦃ hom-f ⦄) ([∃]-intro g ⦃ hom-g ⦄))) {fi = fi} {xs} =
  congruence₁(f) (Homomorphism.preserve-functions hom-g)
  🝖 Homomorphism.preserve-functions hom-f
  🝖 congruence₁(fn C fi) (symmetry(_≡_) (_⊜_.proof (map-[∘] {f = f}{g = g}) {xs}))
Homomorphism.preserve-relations (∃.proof (_∘ₛₜᵣᵤ_ {A = A} {B = B} {C = C} ([∃]-intro f ⦃ hom-f ⦄) ([∃]-intro g ⦃ hom-g ⦄))) {ri = ri} {xs} =
  substitute₁ₗ(IsTrue ∘ rel C ri) (_⊜_.proof map-[∘] {xs})
  ∘ Homomorphism.preserve-relations hom-f
  ∘ Homomorphism.preserve-relations hom-g

import      Data.Tuple as Tuple
open import Function.Equals
open import Function.Equals.Proofs
open import Function.Inverse
open import Lang.Inspect
open import Logic.Predicate.Equiv
open import Structure.Category
open import Structure.Categorical.Properties
open import Structure.Function.Domain.Proofs

instance
  map-function : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → Function ⦃ [⊜]-equiv ⦄ ⦃ [⊜]-equiv ⦄ (map{A = A}{B = B}{n = n})
  map-function {A = A}{B = B} = intro proof where
    proof : ∀{f g : A → B} → (f ⊜ g) → (map{n = n} f ⊜ map g)
    _⊜_.proof (proof p) {∅}     = reflexivity(_≡_)
    _⊜_.proof (proof p) {x ⊰ l} = congruence₂(_⊰_) (_⊜_.proof p) (_⊜_.proof (proof p) {l})

instance
  Structure-Homomorphism-category : Category(_→ₛₜᵣᵤ_ {ℓₘ})
  Category._∘_ Structure-Homomorphism-category = _∘ₛₜᵣᵤ_
  Category.id  Structure-Homomorphism-category = idₛₜᵣᵤ
  BinaryOperator.congruence (Category.binaryOperator Structure-Homomorphism-category) = [⊜][∘]-binaryOperator-raw
  _⊜_.proof (Morphism.Associativity.proof (Category.associativity Structure-Homomorphism-category) {_} {_} {_} {_} {[∃]-intro f} {[∃]-intro g} {[∃]-intro h}) {x} = reflexivity(_≡_) {f(g(h(x)))}
  _⊜_.proof (Morphism.Identityₗ.proof (Tuple.left (Category.identity Structure-Homomorphism-category)) {f = [∃]-intro f}) {x} = reflexivity(_≡_) {f(x)}
  _⊜_.proof (Morphism.Identityᵣ.proof (Tuple.right (Category.identity Structure-Homomorphism-category)) {f = [∃]-intro f}) {x} = reflexivity(_≡_) {f(x)}

module _ {F@([∃]-intro f) : _→ₛₜᵣᵤ_ {ℓₘ}{ℓₘ} A B} where
  isomorphism-surjective-embedding : Morphism.Isomorphism ⦃ [≡∃]-equiv ⦃ [⊜]-equiv ⦄ ⦄ (\{A} → _∘ₛₜᵣᵤ_ {A = A})(idₛₜᵣᵤ)(F) ↔ (Surjective(f) Logic.∧ Embedding(A)(B)(f))
  Tuple.left isomorphism-surjective-embedding (Logic.[∧]-intro surj embed) = [∃]-intro ([∃]-intro _ ⦃ hom ⦄) ⦃ Logic.[∧]-intro inverₗ inverᵣ ⦄ where
    f⁻¹ = invᵣ-surjective f ⦃ surj ⦄
    instance
      inver : Inverse(f)(f⁻¹)
      inver = Logic.[∧]-elimᵣ ([∃]-proof (bijective-to-invertible ⦃ bij = injective-surjective-to-bijective(f)  ⦃ Embedding.injection embed ⦄ ⦃ surj ⦄ ⦄))

    instance
      hom : Homomorphism(B)(A)(f⁻¹)
      Homomorphism.preserve-functions hom {fi = fi} {xs = xs} =
        f⁻¹(fn B fi xs)                   🝖[ _≡_ ]-[ congruence₁(f⁻¹) (congruence₁(fn B fi) (_⊜_.proof map-id)) ]-sym
        f⁻¹(fn B fi (map id xs))          🝖[ _≡_ ]-[ congruence₁(f⁻¹) (congruence₁(fn B fi) (_⊜_.proof (congruence₁(map) (intro (Inverseᵣ.proof(Logic.[∧]-elimᵣ inver)))) {xs})) ]-sym
        f⁻¹(fn B fi (map (f ∘ f⁻¹) xs))   🝖[ _≡_ ]-[ congruence₁(f⁻¹) (congruence₁(fn B fi) (_⊜_.proof map-[∘] {xs})) ]
        f⁻¹(fn B fi (map f (map f⁻¹ xs))) 🝖[ _≡_ ]-[ congruence₁(f⁻¹) (Homomorphism.preserve-functions (Embedding.homomorphism embed)) ]-sym
        f⁻¹(f(fn A fi (map f⁻¹ xs)))      🝖[ _≡_ ]-[ Inverseₗ.proof(Logic.[∧]-elimₗ inver) ]
        fn A fi (map f⁻¹ xs)              🝖-end

      Homomorphism.preserve-relations hom {ri = ri} {xs = xs} p = Embedding.preserve-relations-converse embed {xs = map f⁻¹ xs} (substitute₁(IsTrue ∘ rel B ri) (_⊜_.proof proof {xs}) p) where
        proof =
          id                🝖[ _⊜_ ]-[ map-id ]-sym
          map id            🝖[ _⊜_ ]-[ congruence₁(map) (intro (Inverseᵣ.proof(Logic.[∧]-elimᵣ inver))) ]-sym
          map(f ∘ f⁻¹)      🝖[ _⊜_ ]-[ map-[∘] ]
          (map f ∘ map f⁻¹) 🝖-end

    inverₗ : Morphism.Inverseₗ _ _ F ([∃]-intro f⁻¹)
    Morphism.Inverseₗ.proof inverₗ = intro(Inverseₗ.proof(Logic.[∧]-elimₗ inver))

    inverᵣ : Morphism.Inverseᵣ _ _ F ([∃]-intro f⁻¹)
    Morphism.Inverseᵣ.proof inverᵣ = intro(Inverseᵣ.proof(Logic.[∧]-elimᵣ inver))
  Tuple.right isomorphism-surjective-embedding iso = Logic.[∧]-intro infer (intro (\{n}{ri}{xs} → {!proof!})) where
    instance
      bij : Bijective(f)
    instance
      inj : Injective(f)
      inj = bijective-to-injective(f)
    instance
      surj : Surjective(f)
      surj = bijective-to-surjective(f)
    proof : IsTrue(rel A ri xs) ← IsTrue(rel B ri (map f(xs)))
    proof p relation x = {!!}
    proof2 : let _ = (rel A ri xs) in Surjective(f)
    proof2 = {!!}
-- (intro (proof {!!} {!!}))

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:
-- A module which re-exports Type.Category.ExtensionalFunctionsCategory as the default category for types, and defines some shorthand names for categorical stuff.
module Type.Category where

open import Functional
open import Function.Equals
open import Logic.Predicate
open import Relator.Equals.Proofs.Equiv
import      Structure.Category.Functor               as Category
import      Structure.Category.Monad.ExtensionSystem as Category
import      Structure.Category.NaturalTransformation as Category
open import Syntax.Transitivity
open import Type

module _ {ℓ} where
  open import Type.Category.ExtensionalFunctionsCategory{ℓ} public

  -- Shorthand for the category-related types in the category of types.
  Functor = Category.Endofunctor(typeExtensionalFnCategory) -- TODO: Should not be an endofunctor. Let it be parameterized by different levels
  module Functor {F} ⦃ functor : Functor(F) ⦄ where
    open Category.Endofunctor(typeExtensionalFnCategory) functor public

    module HaskellNames where
      _<$_ : ∀{x y} → y → (F(x) → F(y))
      _<$_ = map ∘ const

      _$>_ : ∀{x y} → F(x) → y → F(y)
      _$>_ = swap(_<$_)

      _<$>_ : ∀{x y} → (x → y) → (F(x) → F(y))
      _<$>_ = map

      _<&>_ : ∀{x y} → F(x) → (x → y) → F(y)
      _<&>_ = swap(_<$>_)

      -- Applies an unlifted argument to a lifted function, returning a lifted value.
      -- TODO: When `f` is an instance of `Applicative`, it should be functionally equivalent
      -- to `f <*> pure x` because:
      --   f <*$> x
      --   = fmap ($ x) f //Definition: <*$>
      --   = pure ($ x) <*> f //Applicative: "As a consequence of these laws, the Functor instance for f will satisfy..."
      --   = f <*> pure x //Applicative: interchange
      _<*$>_ : ∀{x y : Type{ℓ}} → F(x → y) → (x → F(y))
      f <*$> x = (_$ x) <$> f

  module _ {F₁} ⦃ functor₁ : Functor(F₁) ⦄ {F₂} ⦃ functor₂ : Functor(F₂) ⦄ where
    NaturalTransformation : (∀{T} → F₁(T) → F₂(T)) → Type
    NaturalTransformation η = Category.NaturalTransformation {Cₗ = typeExtensionalFnCategoryObject} {Cᵣ = typeExtensionalFnCategoryObject} ([∃]-intro F₁) ([∃]-intro F₂) (T ↦ η{T})
    module NaturalTransformation {η : ∀{T} → F₁(T) → F₂(T)} ⦃ nt : NaturalTransformation(η) ⦄ where
      open Category.NaturalTransformation {Cₗ = typeExtensionalFnCategoryObject} {Cᵣ = typeExtensionalFnCategoryObject} {[∃]-intro F₁} {[∃]-intro F₂} nt public

    {-
    -- All mappings between functors are natural.
    -- Also called: Theorems for free.
    -- TODO: Is this correct? Is this provable? Maybe one needs to prove stuff about how types are formed?
    natural-functor-mapping : ∀{η : ∀{T} → F₁(T) → F₂(T)} → NaturalTransformation(η)
    Dependent._⊜_.proof (Category.NaturalTransformation.natural (natural-functor-mapping {η}) {X}{Y} {f}) {F₁X} =
      (η ∘ (Functor.map f)) F₁X 🝖[ _≡_ ]-[]
      η(Functor.map f(F₁X))     🝖[ _≡_ ]-[ {!!} ]
      Functor.map f (η(F₁X))    🝖[ _≡_ ]-[]
      ((Functor.map f) ∘ η) F₁X 🝖-end
    -}

  Monad = Category.ExtensionSystem{cat = typeExtensionalFnCategoryObject}
  module Monad {T} ⦃ monad : Monad(T) ⦄ where
    open Category.ExtensionSystem{cat = typeExtensionalFnCategoryObject} (monad) public

    -- Do notation for monads.
    open import Syntax.Do
    instance
      doNotation : DoNotation(T)
      return ⦃ doNotation ⦄ = HaskellNames.return
      _>>=_  ⦃ doNotation ⦄ = swap(HaskellNames.bind)

  open Monad using () renaming (doNotation to Monad-doNotation) public


text:
module Lib.List where

open import Lib.Prelude
open import Lib.Id

infix  30 _∈_
infixr 40 _::_ _++_
infix  45 _!_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

{-# COMPILED_DATA List [] [] (:) #-}
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}

_++_ : {A : Set} -> List A -> List A -> List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f z [] = z
foldr f z (x :: xs) = f x (foldr f z xs)

map : {A B : Set} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

map-id : forall {A}(xs : List A) -> map id xs ≡ xs
map-id [] = refl
map-id (x :: xs) with map id xs | map-id xs
... | .xs | refl = refl

data _∈_ {A : Set} : A -> List A -> Set where
  hd : forall {x xs}   ->           x ∈ x :: xs
  tl : forall {x y xs} -> x ∈ xs -> x ∈ y :: xs

data All {A : Set}(P : A -> Set) : List A -> Set where
  []   : All P []
  _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)

head : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> P x
head (x :: xs) = x

tail : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> All P xs
tail (x :: xs) = xs

_!_ : forall {A}{P : A -> Set}{x xs} -> All P xs -> x ∈ xs -> P x
xs ! hd   = head xs
xs ! tl n = tail xs ! n

tabulate : forall {A}{P : A -> Set}{xs} -> ({x : A} -> x ∈ xs -> P x) -> All P xs
tabulate {xs = []}      f = []
tabulate {xs = x :: xs} f = f hd :: tabulate (f ∘ tl)

mapAll : forall {A B}{P : A -> Set}{Q : B -> Set}{xs}(f : A -> B) ->
         ({x : A} -> P x -> Q (f x)) -> All P xs -> All Q (map f xs)
mapAll f h [] = []
mapAll f h (x :: xs) = h x :: mapAll f h xs

mapAll- : forall {A}{P Q : A -> Set}{xs} ->
          ({x : A} -> P x -> Q x) -> All P xs -> All Q xs
mapAll- {xs = xs} f zs with map id xs | map-id xs | mapAll id f zs
... | .xs | refl | r = r

infix 20 _⊆_

data _⊆_ {A : Set} : List A -> List A -> Set where
  stop : [] ⊆ []
  drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
  keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys

⊆-refl : forall {A}{xs : List A} -> xs ⊆ xs
⊆-refl {xs = []}      = stop
⊆-refl {xs = x :: xs} = keep ⊆-refl

_∣_ : forall {A}{P : A -> Set}{xs ys} -> All P ys -> xs ⊆ ys -> All P xs
[]        ∣ stop   = []
(x :: xs) ∣ drop p = xs ∣ p
(x :: xs) ∣ keep p = x :: (xs ∣ p)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.NaturalTransformation where

open import Cubical.Categories.NaturalTransformation.Base public
open import Cubical.Categories.NaturalTransformation.Properties public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- AVL trees
------------------------------------------------------------------------

-- AVL trees are balanced binary search trees.

-- The search tree invariant is specified using the technique
-- described by Conor McBride in his talk "Pivotal pragmatism".

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

open import Relation.Binary using (StrictTotalOrder)

module Data.AVL
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
  where

open import Data.Bool.Base using (Bool)
import Data.DifferenceList as DiffList
open import Data.List.Base as List using (List)
open import Data.Maybe using (Maybe; nothing; just; is-just)
open import Data.Nat.Base using (suc)
open import Data.Product hiding (map)
open import Function as F
open import Level using (_⊔_)
open import Relation.Unary

open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
import Data.AVL.Indexed strictTotalOrder as Indexed
open Indexed using (K&_ ; ⊥⁺ ; ⊤⁺; ⊥⁺<⊤⁺; ⊥⁺<[_]<⊤⁺; ⊥⁺<[_]; [_]<⊤⁺)

------------------------------------------------------------------------
-- Re-export some core definitions publically

open Indexed using (Value; MkValue; const) public

------------------------------------------------------------------------
-- Types and functions with hidden indices

data Tree {v} (V : Value v) : Set (a ⊔ v ⊔ ℓ₂) where
  tree : ∀ {h} → Indexed.Tree V ⊥⁺ ⊤⁺ h → Tree V

module _ {v} {V : Value v} where

  private
    Val = Value.family V

  empty : Tree V
  empty = tree $′ Indexed.empty ⊥⁺<⊤⁺

  singleton : (k : Key) → Val k → Tree V
  singleton k v = tree (Indexed.singleton k v ⊥⁺<[ k ]<⊤⁺)

  insert : (k : Key) → Val k → Tree V → Tree V
  insert k v (tree t) = tree $′ proj₂ $ Indexed.insert k v t ⊥⁺<[ k ]<⊤⁺

  insertWith : (k : Key) → (Maybe (Val k) → Val k) →
               Tree V → Tree V
  insertWith k f (tree t) = tree $′ proj₂ $ Indexed.insertWith k f t ⊥⁺<[ k ]<⊤⁺

  delete : Key → Tree V → Tree V
  delete k (tree t) = tree $′ proj₂ $ Indexed.delete k t ⊥⁺<[ k ]<⊤⁺

  lookup : (k : Key) → Tree V → Maybe (Val k)
  lookup k (tree t) = Indexed.lookup k t ⊥⁺<[ k ]<⊤⁺

module _ {v w} {V : Value v} {W : Value w} where

  private
    Val = Value.family V
    Wal = Value.family W

  map : ∀[ Val ⇒ Wal ] → Tree V → Tree W
  map f (tree t) = tree $ Indexed.map f t

module _ {v} {V : Value v} where

  private
    Val = Value.family V

  infix 4 _∈?_

  _∈?_ : Key → Tree V → Bool
  k ∈? t = is-just (lookup k t)

  headTail : Tree V → Maybe ((K& V) × Tree V)
  headTail (tree (Indexed.leaf _)) = nothing
  headTail (tree {h = suc _} t)    with Indexed.headTail t
  ... | (k , _ , _ , t′) = just (k , tree (Indexed.castˡ ⊥⁺<[ _ ] t′))

  initLast : Tree V → Maybe (Tree V × (K& V))
  initLast (tree (Indexed.leaf _)) = nothing
  initLast (tree {h = suc _} t)    with Indexed.initLast t
  ... | (k , _ , _ , t′) = just (tree (Indexed.castʳ t′ [ _ ]<⊤⁺) , k)

  -- The input does not need to be ordered.

  fromList : List (K& V) → Tree V
  fromList = List.foldr (uncurry insert) empty

  -- Returns an ordered list.

  toList : Tree V → List (K& V)
  toList (tree t) = DiffList.toList (Indexed.toDiffList t)

  -- Naive implementations of union.

module _ {v w} {V : Value v} {W : Value w} where
  private
    Val = Value.family V
    Wal = Value.family W

  unionWith : (∀ {k} → Val k → Maybe (Wal k) → Wal k) →
              -- Left → right → result.
              Tree V → Tree W → Tree W
  unionWith f t₁ t₂ =
    List.foldr (uncurry $ λ k v → insertWith k (f v)) t₂ (toList t₁)

  -- Left-biased.

module _ {v} {V : Value v} where

  private Val = Value.family V

  union : Tree V → Tree V → Tree V
  union = unionWith F.const

  unionsWith : (∀ {k} → Val k → Maybe (Val k) → Val k) → List (Tree V) → Tree V
  unionsWith f ts = List.foldr (unionWith f) empty ts

  -- Left-biased.

  unions : List (Tree V) → Tree V
  unions = unionsWith F.const


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

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

module Dijkstra.EitherLike where

open import Haskell.Prelude

open import Level
  renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)
  public

module _ {ℓ₀ ℓ₁ ℓ₂ : Level} where
  EL-type = Set ℓ₁ → Set ℓ₂ → Set ℓ₀
  EL-level = ℓ₁ ℓ⊔ ℓ₂ ℓ⊔ ℓ₀

  -- Utility to make passing between `Either` and `EitherD` more convenient
  record EitherLike (E : EL-type) : Set (ℓ+1 EL-level) where
    field
      fromEither : ∀ {A : Set ℓ₁} {B : Set ℓ₂} → Either A B → E A B
      toEither   : ∀ {A : Set ℓ₁} {B : Set ℓ₂} → E A B → Either A B
  open EitherLike ⦃ ... ⦄ public

  EL-func : EL-type → Set (ℓ+1 EL-level)
  EL-func EL = ⦃ mel : EitherLike EL ⦄ → Set EL-level

instance
  EitherLike-Either : ∀ {ℓ₁ ℓ₂} → EitherLike{ℓ₁ ℓ⊔ ℓ₂}{ℓ₁}{ℓ₂} Either
  EitherLike.fromEither EitherLike-Either = id
  EitherLike.toEither   EitherLike-Either = id


text:
open import Prelude

open import StateMachineModel
open StateMachine
open System
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (Tri)

module Behaviors
       (State : Set)
       (Event : Set)
       (sys : System State Event)
       (_∈Set?_ : (ev : Event) (evSet : EventSet) → Dec (evSet ev))
  where

  open LeadsTo State Event sys

  StMachine = stateMachine sys

  -- A Behavior is a coinductive data type, such that it has a head with a given
  -- state S and a tail that can be next state for an existent transition or can
  -- be finite, which means that there is no enabled transition

  -- Question : Would it make more sense the behavior over
  --            ReachableState instead of State???
  record Behavior (S : State) : Set where
    coinductive
    field
      tail  : ∃[ ev ] ( Σ[ enEv ∈ enabled StMachine ev S ]
                 Behavior (action StMachine enEv) )
              ⊎
              ¬ ( ∃[ ev ] enabled StMachine ev S )
  open Behavior

  -- Auxiliary function that allows to do pattern matching on the RHS of an
  -- expression.
  -- (ref: https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html)
  case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
  case x of f = f x

  -- Inductive data type to express that Any State ∈ Behavior (AnyS∈B) satisfies
  -- a given Predicate P at a given index n
  -- It's similar to the Any for Lists, with the difference that in the 'there'
  -- contructor we also need to give a proof that the behavior has a tail t.
  data AnySt {st} (P : Pred State 0ℓ) : ℕ → Pred (Behavior st) 0ℓ where
    here  : ∀ {σ : Behavior st} → P st → AnySt P zero σ
    there : ∀ {e enEv t} {σ : Behavior st} (n : ℕ) → tail σ ≡ inj₁ (e , enEv , t)
            → AnySt P n t → AnySt P (suc n) σ

  -- Syntactic sugar for better reading of lemmas:
  -- σ satisfies P at i if there is a state ∈ σ that satisfies P at i
  _satisfies_at_ : ∀ {st} (σ : Behavior st) (P : Pred State 0ℓ) → ℕ → Set
  σ satisfies P at i = AnySt P i σ

  -- Gives the tail of the behavior after n transitions.
  -- If the behavior is finite returns the behavior itself
  drop : ∀ {st} → ℕ → (σ : Behavior st) → ∃[ s ] Behavior s
  drop {st} zero σ = st , σ
  drop {st} (suc n) σ with tail σ
  ... | inj₁ (e , enEv , t) = drop n t
  ... | inj₂ ¬enEv = st , σ

  -- Inductive data type to express that all states in a behavior n satisfy a
  -- Predicate P up to a given index n
  -- It's similar to the All for Lists, with the difference that in the '_∷_'
  -- contructor we also need to give a proof that the behavior has a tail t.
  data AllSt {st} (P : Pred State 0ℓ) : ℕ → Pred (Behavior st) 0ℓ where
    last  : ∀ {σ : Behavior st} → P st → AllSt P zero σ
    _∷_∣_ : ∀ {e enEv t n} {σ : Behavior st} → tail σ ≡ inj₁ (e , enEv , t)
            → P st → AllSt P n t → AllSt P (suc n) σ

  -- Syntactic sugar for better reading of lemmas
  AllSt_upTo_satisfy_ : ∀ {st} (σ : Behavior st) → ℕ → (P : Pred State 0ℓ) → Set
  AllSt σ upTo n satisfy P = AllSt P n σ

 ------------------------------------------------------------------------------
 -- PROOF of SOUNDNESS for LEADS-TO PROOF RULES
 ------------------------------------------------------------------------------
  -- If a behavior σ satisfies P at i then it exists a state s at index i such
  -- that s is reachable and P s
  witness : ∀ {st : State} {i} {σ : Behavior st} {P : Pred State 0ℓ}
            → Reachable {sm = StMachine} st
            → σ satisfies P at i
            → ∃[ state ]
                 (Σ[ rSt ∈ Reachable {sm = StMachine} state ] P state)
  witness {st} rS (here ps) = st , rS , ps
  witness {st} rS (there {σ = σ} n eq satP)
    with tail σ | eq
  ... | inj₁ (e , enEv , t) | refl = witness (step rS enEv) satP

  -- If a behavior σ satisfies Q ∪ R at a given index i then
  -- or σ satisfies Q at i or σ satisfies R at i
  trans2 :  ∀ {st} {Q R : Pred State 0ℓ} {i : ℕ} {σ : Behavior st}
              → σ satisfies (Q ∪ R) at i
              →   σ satisfies Q at i
                ⊎ σ satisfies R at i
  trans2 (here (inj₁ qS)) = inj₁ (here qS)
  trans2 (here (inj₂ rS)) = inj₂ (here rS)
  trans2 {σ = σ} (there n eq tailQ∨R)
    with tail σ | eq
  ... | inj₁ (e , enEv , t) | refl
      with trans2 tailQ∨R
  ... | inj₁ anyQ = inj₁ (there n eq anyQ)
  ... | inj₂ anyR = inj₂ (there n eq anyR)

  -- If σ satisfies (R ⇒ Q) at a given index i and if R is an invariant then
  -- σ satisfies Q at i
  useInv : ∀ {st} {Q R : Pred State 0ℓ} {i : ℕ} {σ : Behavior st}
              → Invariant StMachine R
              → Reachable {sm = StMachine} st
              → σ satisfies (R ⇒ Q) at i
              → σ satisfies Q at i
  useInv inv rS (here r→q) = here (r→q (inv rS))
  useInv inv rS (there {e} {enEv} n eq sat)
    = there n eq (useInv inv (step rS enEv) sat)

  -- If σ satisfies (P ∩ S) at i then σ satisfies P at i and σ satisfies S at i
  split-Conjunction : ∀ {st} {P S : Pred State 0ℓ}
                     {i : ℕ} {σ : Behavior st}
                   → σ satisfies (P ∩ S) at i
                   → σ satisfies P at i × σ satisfies S at i
  split-Conjunction (here (p' , s))
    = here p' , here s
  split-Conjunction (there {e} {enEv} n eq satP'∧S)
    with split-Conjunction satP'∧S
  ... | tailP' , tailS = (there n eq tailP') , (there n eq tailS)

  -- If a behavior σ satisfies a stable predicate S at a given index i, and
  -- satisfies Q at a given k ≥ i then  σ satisfies (Q ∩ S) at k
  stableAux : ∀ {st} {Q S : Pred State 0ℓ}
                {i k : ℕ} {σ : Behavior st}
                → Stable StMachine S
                → σ satisfies S at i
                → i ≤ k
                → σ satisfies Q at k
                → σ satisfies (Q ∩ S) at k
  stableAux stable (here sS) i<k (here qS)
    = here (qS , sS)
  stableAux {σ = σ} stable (here sS) i<k (there {e} {enEv} n eq satQ')
    = there n eq (stableAux stable (here (stable enEv sS)) z≤n satQ')
  stableAux stable (there n eq satS) i<k (there n₁ eq₁ satQ')
    with trans (sym eq₁) eq
  ... | refl
      with stableAux stable satS (≤-pred i<k) satQ'
  ... | satT = there n₁ eq₁ satT

  -- Let A be a concurrent system. EventSet is a subset of events of A.
  -- The EventSet evSet is enabled in a state st if:
  --    ∃[ e ∈ evSet ] enabled e st (see definition of enabledSet)

  -- A behavior σ satisfies weak fairness for evSet if given that
  -- evSet is continuously enabled then it will eventually occurs
  postulate
    weak-fairness : ∀ {st}
                    → (evSet : EventSet)
                    → weakFairness sys evSet
                    → (σ : Behavior st)
                    →  ∃[ n ] (AllSt σ upTo n satisfy (enabledSet StMachine evSet)
                              → case tail (proj₂ (drop n σ)) of
                                λ { (inj₁ (e , enEv , t)) → e ∈ evSet
                                  ; (inj₂ ¬enEv) → ⊥ })

  -- For all n, given the constraints of the viaEvSet rule of LeadsTo, we know
  -- that either we reach Q at some point or in all states up to that n the evSet
  -- will be enabled
  soundness-WF : ∀ {st} {P Q : Pred State 0ℓ}
                 → Reachable {sm = StMachine} st
                 → (evSet : EventSet)
                 → (σ : Behavior st)
                 → (n : ℕ)
                 → P st
                 → (∀ (e : Event) → evSet e → [ P ] e [ Q ])
                 → (∀ (e : Event) → ¬ (evSet e) → [ P ] e [ P ∪ Q ])
                 → Invariant (stateMachine sys) (P ⇒ enabledSet StMachine evSet)
                 → Σ[ j ∈ ℕ ] 0 ≤ j × σ satisfies Q at j
                 ⊎ AllSt σ upTo n satisfy (enabledSet StMachine evSet ∩ P)

  soundness-WF rS evSet σ zero ps c₁ c₂ c₃ = inj₂ (last ((c₃ rS ps) , ps))
  soundness-WF rS evSet σ (suc n) ps c₁ c₂ c₃
    with tail σ    | inspect tail σ
  ... | inj₂ ¬enEv | _ =  case c₃ rS ps of
                          λ { (ev , _ , enEv) → ⊥-elim (¬enEv (ev , enEv)) }
  ... | inj₁ (ev , enEv , t) | Reveal[ t≡i₁ ]
      with ev ∈Set? evSet
  ...   | yes ∈evSet
          = case c₁ ev ∈evSet of
            λ { (hoare p→q) → inj₁ (1 , z≤n , (there 0 t≡i₁ (here (p→q ps enEv)))) }
  ...   | no ¬∈evSet
        with c₂ ev ¬∈evSet
  ...     | hoare p∨q
          with p∨q ps enEv
  ...       | inj₂ qActionSt = inj₁ (1 , z≤n , (there 0 t≡i₁ (here qActionSt)))
  ...       | inj₁ pActionSt
            with soundness-WF (step rS enEv) evSet t n pActionSt c₁ c₂ c₃
  ...         | inj₁ (j , 0<j , anyQT) = inj₁ (suc j , z≤n , there j t≡i₁ anyQT)
  ...         | inj₂ allT = inj₂ ( t≡i₁ ∷ ( c₃ rS ps , ps)∣ allT)

  -- If all states in a behavior σ up to an index n satisfy (P ∩ Q), then
  -- all states in σ up to n satisfy P and all states in σ up to n satisfy Q
  allP∧Q⇒allP∧allQ : ∀ {st} {P Q : Pred State 0ℓ}
                → (n : ℕ)
                → (σ : Behavior st)
                → AllSt σ upTo n satisfy (P ∩ Q)
                → AllSt σ upTo n satisfy P × AllSt σ upTo n satisfy Q
  allP∧Q⇒allP∧allQ zero σ (last (p , q)) = (last p) , (last q)
  allP∧Q⇒allP∧allQ (suc n) σ (eq ∷ (ps , qs) ∣ allPQ)
    with tail σ | eq
  ... | inj₁ (ev , enEv , t) | refl
      with allP∧Q⇒allP∧allQ n t allPQ
  ...   | allP , allQ = (eq ∷ ps ∣ allP) , (eq ∷ qs ∣ allQ)

  -- If all states up to an index n in a behavior σ satisfy P, the state at the
  -- nᵗʰ state of σ satisfy P
  dropNsatP : ∀ {st} {P : Pred State 0ℓ} (n : ℕ)
                → (σ : Behavior st)
                → AllSt σ upTo n satisfy P
                → P (proj₁ (drop n σ))
  dropNsatP zero σ (last ps) = ps
  dropNsatP (suc n) σ (t≡i₁ ∷ ps ∣ allP)
    with tail σ          | t≡i₁
  ... | inj₁ (_ , _ , t) | refl = dropNsatP n t allP

  -- If the nᵗʰ state of σ satisfy P at 1 then σ satisfy Q at (suc n)
  dropN⇒σsat : ∀ {st} {Q : Pred State 0ℓ}
                   → (n : ℕ)
                   → (σ : Behavior st)
                   → proj₂ (drop n σ) satisfies Q at 1
                   → σ satisfies Q at (suc n)
  dropN⇒σsat zero    σ satQ = satQ
  dropN⇒σsat (suc n) σ satQ
    with tail σ | inspect tail σ
  ... | inj₂ ¬ev | _ = case satQ of
                       λ { (there {e} {enEv} 0 t≡inj₁ x)
                                  → ⊥-elim (¬ev (e , enEv)) }
  ... | inj₁ (e , enEv , t) | Reveal[ eq ]
      with dropN⇒σsat n t satQ
  ...   | anyQ = there (suc n) eq anyQ

  -- If a behavior σ satisfy that it exists a w such that F w at index i then
  -- it exists a w such that σ satisfy Fw at index i
  σ⊢Fw : ∀ {st} {F : Z → Pred State 0ℓ} {i : ℕ} {σ : Behavior st}
         → σ satisfies [∃ w ∶ F w ] at i
         → Σ[ w ∈ ℕ ] σ satisfies F w at i
  σ⊢Fw (here (w , fw)) = w , (here fw)
  σ⊢Fw (there n eq satF)
    with σ⊢Fw satF
  ... | w , fw = w , (there n eq fw)

  -- If a behavior σ satisfy that it exists a w₁ such that w₁ < w and F w₁
  -- at an index i then it exists a w₁ such that w₁ < w and
  -- σ satisfy F w₁ at index i
  σ⊢Fw< : ∀ {st} {F : Z → Pred State 0ℓ} {j w : ℕ} {σ : Behavior st}
          → σ satisfies [∃ w₁ ⇒ _< w ∶ F w₁ ] at j
          → Σ[ w₁ ∈ ℕ ] w₁ < w × σ satisfies F w₁ at j
  σ⊢Fw< (here (w₁ , w₁<w , fw₁)) = w₁ , w₁<w , (here fw₁)
  σ⊢Fw< (there n x satF)
    with σ⊢Fw< satF
  ... | w , x<w , fw = w , x<w , (there n x fw)

  -- The following definitions are mutual because the soundness proof use the
  -- lemma wfr→Q in the viaWFR rule to prove that given the viaWFR rule we reach
  -- a state that satisfies Q, and the wfr→Q lemma uses the soundness proof to
  -- prove that progress is made in the well founded ranking, which means that
  -- either we get to a state that satisfies Q or we reach a state where exists
  -- a w₁ such that w₁ < w and F w₁. This implies that or we reach Q or w₁ will
  -- become 0 and Q must hold.
  mutual

    wfr→Q : ∀ {w₁ w i : ℕ} {st} {F : Z → Pred State 0ℓ} {Q : Pred State 0ℓ}
               → w₁ < w
               → Reachable {sm = StMachine} st
               → (σ : Behavior st)
               → σ satisfies F w₁ at i
               → (∀ (w : Z) → F w l-t (Q ∪ [∃ x ⇒ _< w ∶ F x ]))
               →  Σ[ j ∈ ℕ ] i ≤ j × σ satisfies Q at j
    wfr→Q {zero}   {suc w} w₁<w rS σ satF fw→q∪f
      with soundness-aux rS σ satF (fw→q∪f 0)
    ... | n , i≤n , anyQ∨⊥
        with trans2 anyQ∨⊥
    ...   | inj₁ anyQ = n , i≤n , anyQ
    ...   | inj₂ imp
          with witness rS imp
    ...     | ()
    wfr→Q {suc w₁} {suc w} (s≤s w₁<w) rS σ satF fw→q∪f
      with soundness-aux rS σ satF (fw→q∪f (suc w₁))
    ... | n , i≤n , anyQ∨F
        with trans2 anyQ∨F
    ...   | inj₁ satQ = n , i≤n , satQ
    ...   | inj₂ satw
          with σ⊢Fw< satw
    ...     | w₂ , w₂<sw₁ , satw<
            with wfr→Q {w = w} (≤-trans w₂<sw₁ w₁<w) rS σ satw< fw→q∪f
    ...       | j , n≤j , anyQ = j , ≤-trans i≤n n≤j , anyQ

    soundness-aux : ∀ {st} {P Q} {i : ℕ}
                    → Reachable {sm = StMachine} st
                    → (σ : Behavior st)
                    → σ satisfies P at i
                    → P l-t Q
                    → Σ[ j ∈ ℕ ] i ≤ j × σ satisfies Q at j

    soundness-aux rS σ (here ps) (viaEvSet evSet wf c₁ c₂ c₃)
      with weak-fairness evSet wf σ
    ... | n , wfa
        with soundness-WF rS evSet σ n ps c₁ c₂ c₃
    ...   | inj₁ satQ   = satQ
    ...   | inj₂ allE∧P
          with allP∧Q⇒allP∧allQ n σ allE∧P
    ...     | allE , allP
            with wfa allE
    ...       | v
              with tail (proj₂ (drop n σ)) | inspect tail (proj₂ (drop n σ))
    ...         | inj₂ ¬enEv | _ = ⊥-elim v
    ...         | inj₁ (e , enEv , t) | Reveal[ t≡i₁ ]
                  = case c₁ e v of
                    λ { (hoare p→q) → let pSt = dropNsatP n σ allP
                                          q⊢1 = there 0 t≡i₁ (here (p→q pSt enEv))
                                      in (suc n) , z≤n , dropN⇒σsat n σ q⊢1 }

    soundness-aux rS σ (here ps) (viaInv inv) = 0 , z≤n , here (inv rS ps)

    soundness-aux rS σ (here ps) (viaTrans p→r r→q)
      with soundness-aux rS σ (here ps) p→r
    ... | n , 0<n , anyR
        with soundness-aux rS σ anyR r→q
    ... | j , n<j , anyQ = j , ≤-trans 0<n n<j , anyQ

    soundness-aux rS σ (here ps) (viaTrans2 p→q∨r r→q)
      with soundness-aux rS σ (here ps) p→q∨r
    ... | n , 0<n , anyQ∨R
        with trans2 anyQ∨R
    ...   | inj₁ anyQ = n , z≤n , anyQ
    ...   | inj₂ anyR
          with soundness-aux rS σ anyR r→q
    ...     | j , n≤j , anyQ  = j , ≤-trans 0<n n≤j , anyQ

    soundness-aux rS σ (here ps) (viaDisj p₁∨p₂ p₁→q p₂→q)
      with p₁∨p₂ ps
    ... | inj₁ p₁S = soundness-aux rS σ (here p₁S) p₁→q
    ... | inj₂ p₂S = soundness-aux rS σ (here p₂S) p₂→q

    soundness-aux rS σ (here ps) (viaUseInv invR p∧r→r⇒q)
      with soundness-aux rS σ (here (ps , invR rS)) p∧r→r⇒q
    ... | n , 0≤n , anyR⇒Q
        with useInv invR rS anyR⇒Q
    ... | anyQ = n , 0≤n , anyQ

    soundness-aux rS σ (here ps) (viaWFR F c₁ c₂)
            with soundness-aux rS σ (here ps) c₁
    ... | n , 0<n , q∪f
        with trans2 q∪f
    ...   | inj₁ anyQ = n , 0<n , anyQ
    ...   | inj₂ anyF
          with σ⊢Fw anyF
    ...     | w , satFw
            with soundness-aux rS σ satFw (c₂ w)
    ...       | j , n<j , anyQ∪F
              with trans2 anyQ∪F
    ...         | inj₁ anyQw  = j , z≤n , anyQw
    ...         | inj₂ anyFw
                with σ⊢Fw< anyFw
    ...           | w₁ , w₁<w , satFw₁
                  with wfr→Q w₁<w rS σ satFw₁ c₂
    ...             | k , j<k , anyQ = k , z≤n , anyQ

    soundness-aux rS σ (here ps) (viaAllVal invR p∧r→q)
      with invR rS
    ... | a , rA = soundness-aux rS σ (here (ps , rA)) (p∧r→q a)

    soundness-aux rS σ (here ps) (viaStable stableS p→p'∧s p'→q' q'∧s→q)
      with soundness-aux rS σ (here ps) p→p'∧s
    ... | n , 0≤n , anyP'∧S
        with split-Conjunction anyP'∧S
    ... | anyP' , anyS
          with soundness-aux rS σ anyP' p'→q'
    ...   | k , n≤k , anyQ'
          with soundness-aux rS σ (stableAux stableS anyS n≤k anyQ') q'∧s→q
    ...     | j , k≤j , anyQ = j , ≤-trans 0≤n (≤-trans n≤k k≤j) , anyQ

    soundness-aux rS σ (there {e} {enEv} {t} i t≡i₁ σ⊢P) p→q
       with soundness-aux (step rS enEv) t σ⊢P p→q
    ... | j , i≤j , tail⊢Q = suc j , s≤s i≤j , (there j t≡i₁ tail⊢Q)

  -- Soundness proof for all Behaviors that start in one initial state
  soundnessLt : ∀ {s₀} {P Q} {i} → initial StMachine s₀
              → (σ : Behavior s₀)
              → σ satisfies P at i
              → P l-t Q
              → ∃[ j ] (i ≤ j × σ satisfies Q at j)
  soundnessLt s₀ σ σ⊢P p→q = soundness-aux (init s₀) σ σ⊢P p→q

 ------------------------------------------------------------------------------
 -- PROOF of SOUNDNESS for INVARIANCE PROOF RULE
 ------------------------------------------------------------------------------

  record AllStates {st} (σ : Behavior st) (P : Pred State 0ℓ) : Set where
    coinductive
    field
      head-Sat  : P st
      tail-Sat  : ∀ {e enEv t} → tail σ ≡ inj₁ (e , enEv , t) → AllStates t P
  open Behavior

  soundnessInv-rS : ∀ {st} {P} → Reachable {sm = StMachine} st
                  → (σ : Behavior st)
                  → Invariant StMachine P
                  → AllStates σ P
  AllStates.head-Sat (soundnessInv-rS rS σ invP) = invP rS
  AllStates.tail-Sat (soundnessInv-rS rS σ invP) {e} {enEv} {t} t≡i₁
    = soundnessInv-rS (step rS enEv) t invP

  soundnessInv : ∀ {st} {P} → initial StMachine st
                 → (σ : Behavior st)
                 → Invariant StMachine P
                 → AllStates σ P
  soundnessInv s₀ σ invP = soundnessInv-rS (init s₀) σ invP

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Decidable.Sets
open import Lists.Lists
open import Numbers.Naturals.Semiring

module UnorderedSet.Definition {a : _} {V : Set a} (dec : DecidableSet V) where

data UnorderedSetOf : List V → Set a where
  empty' : UnorderedSetOf []
  addCons : (v : V) → (vs : List V) → .(contains vs v → False) → UnorderedSetOf vs → UnorderedSetOf (v :: vs)

record UnorderedSet : Set a where
  field
    elts : List V
    set : UnorderedSetOf elts

empty : UnorderedSet
empty = record { elts = [] ; set = empty' }

add : V → UnorderedSet → UnorderedSet
add v record { elts = elts ; set = set } with containsDecidable dec elts v
... | inl x = record { elts = elts ; set = set }
... | inr x = record { elts = v :: elts ; set = addCons v elts x set }

singleton : V → UnorderedSet
singleton v = record { elts = v :: [] ; set = addCons v [] (λ ()) empty' }

ofList : (l : List V) → UnorderedSet
ofList [] = record { elts = [] ; set = empty' }
ofList (x :: l) = add x (ofList l)

union : UnorderedSet → UnorderedSet → UnorderedSet
union record { elts = eltsA ; set = setA } record { elts = eltsB ; set = setB } = ofList (eltsA ++ eltsB)

count : UnorderedSet → ℕ
count record { elts = e ; set = _ } = length e

setContains : (v : V) → UnorderedSet → Set a
setContains v record { elts = elts ; set = set } = contains elts v


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

-- The Everything module of undecidability analysis
-- In Agda, we use first order de Bruijn indices to represent variables, that is, the
-- natural numbers.
module Everything where

-- Subtyping problems of all following calculi are undecidable.  In this technical
-- work, our reduction proofs stop at F<: deterministic (F<:ᵈ), the undecidability of
-- which is justified by Pierce92.

-- F<: F<:⁻ F<:ᵈ
import FsubMinus

-- D<:
--
-- The examination of D<: is composed of the following files:
import DsubDef -- defines the syntax of D<:.
import Dsub -- defines the simplified subtyping judgment per Lemma 2 in the paper.
import DsubFull -- defines the original definition of D<:.
import DsubEquivSimpler -- defines D<: normal form and shows that D<: subtyping is undecidable.
import DsubNoTrans -- shows that D<: subtyping without transitivity remains undecidable.
import DsubTermUndec -- shows that D<: term typing is also undecidable.

-- other things

-- properties of F<:⁻
import FsubMinus2


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Signs
------------------------------------------------------------------------

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

module Data.Sign where

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

open import Data.Sign.Base public
open import Data.Sign.Properties public
  using (_≟_)


text:
-- We need to look at irrelevant variables in meta instantiation occurs check.
-- Here's why.
module Issue483 where

data _==_ {A : Set}(x : A) : A → Set where
  refl : x == x

data ⊥ : Set where

resurrect : .⊥ → ⊥
resurrect ()

data D : Set where
  c : (x : ⊥) → (.(y : ⊥) → x == resurrect y) → D

d : D
d = c _ (λ y → refl)
-- this should leave an unsolved meta!  An error is too harsh.
{-
-- Cannot instantiate the metavariable _21 to resurrect _ since it
-- contains the variable y which is not in scope of the metavariable
-- when checking that the expression refl has type _21 == resurrect _
-}

¬d : D → ⊥
¬d (c x _) = x

oops : ⊥
oops = ¬d d


text:
data Greeting : Set where
  hello : Greeting

greet : Greeting
greet = hello

max_stars_repo_name: supeterlau/bedev

max_issues_repo_name: supeterlau/bedev

max_forks_repo_name: supeterlau/bedev


text:
-- Jesper, Andreas, 2018-10-29, issue #3332
--
-- WAS: With-inlining failed in termination checker
-- due to a DontCare protecting the clause bodies
-- (introduced by Prop).

{-# OPTIONS --prop #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.List

postulate
  A : Set

_++_ : List A → List A → List A
[] ++ l = l
(a ∷ l) ++ l' = a ∷ (l ++ l')

module PropEquality where

  data _≐_ {A : Set} (a : A) : A → Prop where
    refl : a ≐ a

  test : (l : List A) → (l ++ []) ≐ l
  test [] = refl
  test (x ∷ xs) with xs ++ [] | test xs
  test (x ∷ xs) | .xs | refl = refl

module SquashedEquality where

  data Squash (A : Set) : Prop where
    sq : A → Squash A

  test : (l : List A) → Squash (l ++ [] ≡ l)
  test [] = sq refl
  test (x ∷ l) with test l
  test (x ∷ l) | sq eq     with l ++ [] | eq
  test (x ∷ l) | .(test l) | .l | refl = sq refl

-- Both should succeed.