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

module Correctness where

open import Convertibility public
open import Semantics public

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE idmono⊩⋆ #-}

-- TODO: Naming things.

module _ {{_ : Model}} where
  ⟦_≔_⟧∈ : ∀ {C Γ w} → (i : C ∈ Γ) → w ⟪ Γ ∖ i ⊫ C ⟫ →
           ∀ {A} → A ∈ Γ → w ⟪ Γ ∖ i ⊫ A ⟫
  ⟦ i ≔ ⟪c⟫ ⟧∈ j  with i ≟∈ j
  ⟦ i ≔ ⟪c⟫ ⟧∈ .i | same   = ⟪c⟫
  ⟦ i ≔ ⟪c⟫ ⟧∈ ._ | diff j = ⟪var⟫ j

  lem≔∈ : ∀ {A C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (j : A ∈ Γ) →
          ⟦ i ≔ eval c ⟧∈ j ≡ eval ([ i ≔ c ]∈ j) {w}
  lem≔∈ i c j  with i ≟∈ j
  lem≔∈ i c .i | same   = refl
  lem≔∈ i c ._ | diff j = refl

-- TODO: Naming things.

module _ {{_ : Model}} where
  plug : ∀ {C Γ w} → (i : C ∈ Γ) → w ⊩⋆ Γ ∖ i → w ⊩ C → w ⊩⋆ Γ
  plug top     γ       s = γ , s
  plug (pop i) (γ , r) s = plug i γ s , r

  ⟦_≔_⟧ : ∀ {C Γ w} → (i : C ∈ Γ) → w ⟪ Γ ∖ i ⊫ C ⟫ →
          ∀ {A} → (∀ {w′} → w′ ⟪ Γ ⊫ A ⟫) → w ⟪ Γ ∖ i ⊫ A ⟫
  ⟦ i ≔ ⟪c⟫ ⟧ ⟪d⟫ = λ γ → ⟪d⟫ (plug i γ (⟪c⟫ γ))

  -- TODO: The var case in lem≔.

  postulate
    oops≔var₁ : ∀ {C Γ w} → (i : C ∈ Γ) (⟪c⟫ : w ⟪ Γ ∖ i ⊫ C ⟫) (γ : w ⊩⋆ Γ ∖ i) →
                ⟪var⟫ {C} i (plug i γ (⟪c⟫ γ)) ≡ ⟪c⟫ γ
  -- oops≔var₁ top     ⟪c⟫ γ       = refl
  -- oops≔var₁ (pop i) ⟪c⟫ (γ , s) = {!!}

  postulate
    oops≔var₂ : ∀ {A C Γ w} → (i : C ∈ Γ) (⟪c⟫ : w ⟪ Γ ∖ i ⊫ C ⟫) (j : A ∈ Γ ∖ i) (γ : w ⊩⋆ Γ ∖ i) →
                ⟪var⟫ {A} (mono∈ (thin⊆ i) j) (plug i γ (⟪c⟫ γ)) ≡ ⟪var⟫ {A} j γ
  -- oops≔var₂ top     ⟪c⟫ j γ       = cong² ⟪var⟫ (idmono∈ j) refl
  -- oops≔var₂ (pop i) ⟪c⟫ j (γ , s) = {!!}

  oops≔var : ∀ {A C Γ w} → (i : C ∈ Γ) (⟪c⟫ : w ⟪ Γ ∖ i ⊫ C ⟫) (j : A ∈ Γ) →
             ⟦ i ≔ ⟪c⟫ ⟧ {A} (⟪var⟫ {A} j) ≡ ⟦ i ≔ ⟪c⟫ ⟧∈ {A} j
  oops≔var i ⟪c⟫ j  with i ≟∈ j
  oops≔var i ⟪c⟫ .i | same   = funext (λ γ → oops≔var₁ i ⟪c⟫ γ)
  oops≔var i ⟪c⟫ ._ | diff j = funext (λ γ → oops≔var₂ i ⟪c⟫ j γ)

  -- TODO: The lam case in lem≔.

  lem₁ : ∀ {C Γ w w′} → (i : C ∈ Γ) (γ : w ⊩⋆ Γ ∖ i) (s : w ⊩ C) (p : w ≤ w′) →
         mono⊩⋆ p (plug i γ s) ≡ plug i (mono⊩⋆ p γ) (mono⊩ {C} p s)
  lem₁ top     γ       s p = refl
  lem₁ (pop i) (γ , r) s p = cong² _,_ (lem₁ i γ s p) refl

  mutual
    postulate
      lem₂ : ∀ {A Γ w w′} → (p : w ≤ w′) (d : Γ ⊢ A) (γ : w ⊩⋆ Γ) →
             mono⊩ {A} p (eval d γ) ≡ eval d (mono⊩⋆ p γ)
    -- lem₂ p (var {A} j)        γ = {!!}
    -- lem₂ p (lam {A} {B} d)    γ = {!!}
    -- lem₂ p (app {A} {B} d e)  γ = {!!}
    -- lem₂ p (pair {A} {B} d e) γ = lem₂pair p d e γ
    -- lem₂ p (fst {A} {B} d)    γ = lem₂fst p d γ
    -- lem₂ p (snd {A} {B} d)    γ = lem₂snd p d γ
    -- lem₂ p unit               γ = refl

    lem₂pair : ∀ {A B Γ w w′} → (p : w ≤ w′) (d : Γ ⊢ A) (e : Γ ⊢ B) (γ : w ⊩⋆ Γ) →
               mono⊩ {A ⩕ B} p (⟪pair⟫ {A} {B} (eval d) (eval e) γ) ≡ ⟪pair⟫ {A} {B} (eval d) (eval e) (mono⊩⋆ p γ)
    lem₂pair {A} {B} p d e γ =
      begin
        mono⊩ {A ⩕ B} p (⟪pair⟫ {A} {B} (eval d) (eval e) γ)
      ≡⟨⟩
        ⟪pair⟫ {A} {B} (λ γ′ → mono⊩ {A} p (eval d γ)) (λ γ′ → mono⊩ {B} p (eval e γ)) (mono⊩⋆ p γ)
      ≡⟨ cong² (λ ⟪d⟫ ⟪e⟫ → ⟪pair⟫ {A} {B} ⟪d⟫ ⟪e⟫ (mono⊩⋆ p γ)) (funext (λ γ′ → lem₂ p d γ)) (funext (λ γ′ → lem₂ p e γ)) ⟩
        ⟪pair⟫ {A} {B} (λ γ′ → eval d (mono⊩⋆ p γ)) (λ γ′ → eval e (mono⊩⋆ p γ)) (mono⊩⋆ p γ)
      ≡⟨⟩
        ⟪pair⟫ {A} {B} (eval d) (eval e) (mono⊩⋆ p γ)
      ∎

    lem₂fst : ∀ {A B Γ w w′} → (p : w ≤ w′) (d : Γ ⊢ A ⩕ B) (γ : w ⊩⋆ Γ) →
              mono⊩ {A} p (⟪fst⟫ {A} {B} (eval d) γ) ≡ ⟪fst⟫ {A} {B} (eval d) (mono⊩⋆ p γ)
    lem₂fst {A} {B} p d γ =
      begin
        mono⊩ {A} p (⟪fst⟫ {A} {B} (eval d) γ)
      ≡⟨⟩
        ⟪fst⟫ {A} {B} (λ γ′ → mono⊩ {A ⩕ B} p (eval d γ)) (mono⊩⋆ p γ)
      ≡⟨ cong (λ ⟪d⟫ → ⟪fst⟫ {A} {B} ⟪d⟫ (mono⊩⋆ p γ)) (funext (λ γ′ → lem₂ p d γ)) ⟩
        ⟪fst⟫ {A} {B} (λ γ′ → eval d (mono⊩⋆ p γ)) (mono⊩⋆ p γ)
      ≡⟨⟩
        ⟪fst⟫ {A} {B} (eval d) (mono⊩⋆ p γ)
      ∎

    lem₂snd : ∀ {A B Γ w w′} → (p : w ≤ w′) (d : Γ ⊢ A ⩕ B) (γ : w ⊩⋆ Γ) →
              mono⊩ {B} p (⟪snd⟫ {A} {B} (eval d) γ) ≡ ⟪snd⟫ {A} {B} (eval d) (mono⊩⋆ p γ)
    lem₂snd {A} {B} p d γ =
      begin
        mono⊩ {B} p (⟪snd⟫ {A} {B} (eval d) γ)
      ≡⟨⟩
        ⟪snd⟫ {A} {B} (λ γ′ → mono⊩ {A ⩕ B} p (eval d γ)) (mono⊩⋆ p γ)
      ≡⟨ cong (λ ⟪d⟫ → ⟪snd⟫ {A} {B} ⟪d⟫ (mono⊩⋆ p γ)) (funext (λ γ′ → lem₂ p d γ)) ⟩
        ⟪snd⟫ {A} {B} (λ γ′ → eval d (mono⊩⋆ p γ)) (mono⊩⋆ p γ)
      ≡⟨⟩
        ⟪snd⟫ {A} {B} (eval d) (mono⊩⋆ p γ)
      ∎

  postulate
    oops≔lam₂ : ∀ {A C Γ w w′} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (γ : w ⊩⋆ Γ ∖ i) (p : w ≤ w′) (s : w′ ⊩ A) →
                mono⊩ {C} p (eval c γ) ≡ eval (mono⊢ (weak⊆ {A = A}) c) (mono⊩⋆ p γ , s)
  -- oops≔lam₂ i c γ p s = {!!}

  oops≔lam₁ : ∀ {A B C Γ w w′} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ , A ⊢ B) (γ : w ⊩⋆ Γ ∖ i) (p : w ≤ w′) (s : w′ ⊩ A) →
              eval d (mono⊩⋆ p (plug i γ (eval c γ)) , s) ≡ eval d (plug i (mono⊩⋆ p γ) (eval (mono⊢ (weak⊆ {A = A}) c) (mono⊩⋆ p γ , s)) , s)
  oops≔lam₁ {A} {B} {C} i c d γ p s =
    begin
      eval d (mono⊩⋆ p (plug i γ (eval c γ)) , s)
    ≡⟨ cong (eval d) (cong² _,_ (lem₁ i γ (eval c γ) p) refl) ⟩
      eval d (plug i (mono⊩⋆ p γ) (mono⊩ {C} p (eval c γ)) , s)
    ≡⟨ cong (eval d) (cong² _,_ (cong² (plug i) refl (oops≔lam₂ i c γ p s)) refl) ⟩
      eval d (plug i (mono⊩⋆ p γ) (eval (mono⊢ weak⊆ c) (mono⊩⋆ p γ , s)) , s)
    ∎

  oops≔lam : ∀ {A B C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ , A ⊢ B) →
             ⟦ i ≔ eval c {w} ⟧ {A ⇒ B} (⟪lam⟫ {A} {B} (eval d)) ≡
               ⟪lam⟫ {A} {B} (⟦ pop {A = C} {B = A} i ≔ eval (mono⊢ (weak⊆ {A = A}) c) ⟧ {B} (eval d))
  oops≔lam i c d = funext (λ γ → ⟨funext⟩ (funext (λ p → funext (λ s → oops≔lam₁ i c d γ p s))))

  mutual
    lem≔ : ∀ {A C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ ⊢ A) →
           ⟦ i ≔ eval c ⟧ {A} (eval d) ≡ eval ([ i ≔ c ] d) {w}
    lem≔ i c (var j)    = lem≔var i c j
    lem≔ i c (lam d)    = lem≔lam i c d
    lem≔ i c (app d e)  = lem≔app i c d e
    lem≔ i c (pair d e) = lem≔pair i c d e
    lem≔ i c (fst d)    = lem≔fst i c d
    lem≔ i c (snd d)    = lem≔snd i c d
    lem≔ i c unit       = lem≔unit i c

    lem≔var : ∀ {A C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (j : A ∈ Γ) →
              ⟦ i ≔ eval c ⟧ {A} (⟪var⟫ {A} j) ≡ eval ([ i ≔ c ] (var j)) {w}
    lem≔var {A} i c j =
      begin
        ⟦ i ≔ eval c ⟧ {A} (⟪var⟫ {A} j)
      ≡⟨ oops≔var i (eval c) j ⟩
        ⟦ i ≔ eval c ⟧∈ {A} j
      ≡⟨ lem≔∈ i c j ⟩
        eval ([ i ≔ c ]∈ j)
      ≡⟨⟩
        eval ([ i ≔ c ] (var j))
      ∎

    lem≔lam : ∀ {A B C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ , A ⊢ B) →
              ⟦ i ≔ eval c ⟧ {A ⇒ B} (⟪lam⟫ {A} {B} (eval d)) ≡ eval ([ i ≔ c ] (lam d)) {w}
    lem≔lam {A} {B} {C} i c d =
      begin
        ⟦ i ≔ eval c ⟧ {A ⇒ B} (⟪lam⟫ {A} {B} (eval d))
      ≡⟨ oops≔lam i c d ⟩
        ⟪lam⟫ {A} {B} (⟦ pop {A = C} {B = A} i ≔ eval (mono⊢ (weak⊆ {A = A}) c) ⟧ {B} (eval d))
      ≡⟨ cong (⟪lam⟫ {A} {B}) (⟨funext⟩ (lem≔ (pop i) (mono⊢ (weak⊆ {A = A}) c) d)) ⟩
        ⟪lam⟫ {A} {B} (eval ([ pop {A = C} {B = A} i ≔ mono⊢ (weak⊆ {A = A}) c ] d))
      ≡⟨⟩
        eval (lam ([ pop i ≔ mono⊢ weak⊆ c ] d))
      ≡⟨⟩
        eval ([ i ≔ c ] (lam d))
      ∎

    lem≔app : ∀ {A B C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ ⊢ A ⇒ B) (e : Γ ⊢ A) →
              ⟦ i ≔ eval c ⟧ {B} (⟪app⟫ {A} {B} (eval d) (eval e)) ≡ eval ([ i ≔ c ] (app d e)) {w}
    lem≔app {A} {B} i c d e =
      begin
        ⟦ i ≔ eval c ⟧ {B} (⟪app⟫ {A} {B} (eval d) (eval e))
      ≡⟨⟩
        ⟪app⟫ {A} {B} (⟦ i ≔ eval c ⟧ {A ⇒ B} (eval d)) (⟦ i ≔ eval c ⟧ {A} (eval e))
      ≡⟨ cong² (⟪app⟫ {A} {B}) (lem≔ i c d) (funext (λ γ → extfun (lem≔ i c e) γ)) ⟩
        ⟪app⟫ {A} {B} (eval ([ i ≔ c ] d)) (eval ([ i ≔ c ] e))
      ≡⟨⟩
        eval (app ([ i ≔ c ] d) ([ i ≔ c ] e))
      ≡⟨⟩
        eval ([ i ≔ c ] (app d e))
      ∎

    lem≔pair : ∀ {A B C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ ⊢ A) (e : Γ ⊢ B) →
               ⟦ i ≔ eval c ⟧ {A ⩕ B} (⟪pair⟫ {A} {B} (eval d) (eval e)) ≡ eval ([ i ≔ c ] (pair d e)) {w}
    lem≔pair {A} {B} i c d e =
      begin
        ⟦ i ≔ eval c ⟧ {A ⩕ B} (⟪pair⟫ {A} {B} (eval d) (eval e))
      ≡⟨⟩
        ⟪pair⟫ {A} {B} (⟦ i ≔ eval c ⟧ {A} (eval d)) (⟦ i ≔ eval c ⟧ {B} (eval e))
      ≡⟨ cong² (⟪pair⟫ {A} {B}) (lem≔ i c d) (lem≔ i c e) ⟩
        ⟪pair⟫ {A} {B} (eval ([ i ≔ c ] d)) (eval ([ i ≔ c ] e))
      ≡⟨⟩
        eval (pair ([ i ≔ c ] d) ([ i ≔ c ] e))
      ≡⟨⟩
        eval ([ i ≔ c ] (pair d e))
      ∎

    lem≔fst : ∀ {A B C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ ⊢ A ⩕ B) →
              ⟦ i ≔ eval c ⟧ {A} (⟪fst⟫ {A} {B} (eval d)) ≡ eval ([ i ≔ c ] (fst d)) {w}
    lem≔fst {A} {B} i c d =
      begin
        ⟦ i ≔ eval c ⟧ {A} (⟪fst⟫ {A} {B} (eval d))
      ≡⟨⟩
        ⟪fst⟫ {A} {B} (⟦ i ≔ eval c ⟧ {A ⩕ B} (eval d))
      ≡⟨ cong (⟪fst⟫ {A} {B}) (lem≔ i c d) ⟩
        ⟪fst⟫ {A} {B} (eval ([ i ≔ c ] d))
      ≡⟨⟩
        eval (fst ([ i ≔ c ] d))
      ≡⟨⟩
        eval ([ i ≔ c ] (fst d))
      ∎

    lem≔snd : ∀ {A B C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) (d : Γ ⊢ A ⩕ B) →
              ⟦ i ≔ eval c ⟧ {B} (⟪snd⟫ {A} {B} (eval d)) ≡ eval ([ i ≔ c ] (snd d)) {w}
    lem≔snd {A} {B} i c d =
      begin
        ⟦ i ≔ eval c ⟧ {B} (⟪snd⟫ {A} {B} (eval d))
      ≡⟨⟩
        ⟪snd⟫ {A} {B} (⟦ i ≔ eval c ⟧ {A ⩕ B} (eval d))
      ≡⟨ cong (⟪snd⟫ {A} {B}) (lem≔ i c d) ⟩
        ⟪snd⟫ {A} {B} (eval ([ i ≔ c ] d))
      ≡⟨⟩
        eval (snd ([ i ≔ c ] d))
      ≡⟨⟩
        eval ([ i ≔ c ] (snd d))
      ∎

    lem≔unit : ∀ {C Γ w} → (i : C ∈ Γ) (c : Γ ∖ i ⊢ C) →
               ⟦ i ≔ eval c ⟧ {⫪} ⟪unit⟫ ≡ eval ([ i ≔ c ] unit) {w}
    lem≔unit i c = refl

-- TODO: Naming things.

-- NOTE: This is using {-# REWRITE idmono⊩⋆ #-}.

module _ {{_ : Model}} where
  lemreduce⇒ : ∀ {A B Γ w} → (d : Γ , A ⊢ B) (e : Γ ⊢ A) →
                ⟪app⟫ {A} {B} (⟪lam⟫ {A} {B} (eval d)) (eval e {w}) ≡ eval ([ top ≔ e ] d) {w}
  lemreduce⇒ d e = lem≔ top e d

-- TODO: The expand⇒ case in eval✓.

module _ {{_ : Model}} where
  postulate
    lemexpand⇒ : ∀ {A B Γ w} → (d : Γ ⊢ A ⇒ B) →
                  eval d {w} ≡ ⟪lam⟫ {A} {B} (⟪app⟫ {A} {B} {Γ , A} (eval (mono⊢ {A ⇒ B} (weak⊆ {A = A}) d)) (⟪v₀⟫ {A}))
  -- lemexpand⇒ d = {!!}

-- Correctness of evaluation with respect to β-η-equivalence.

module _ {{_ : Model}} where
  eval✓ : ∀ {A Γ} {d d′ : Γ ⊢ A} {w} → d ≡ᵝᵑ d′ → eval d {w} ≡ eval d′ {w}
  eval✓ refl≡ᵝᵑ                   = refl
  eval✓ (trans≡ᵝᵑ p q)            = trans (eval✓ p) (eval✓ q)
  eval✓ (sym≡ᵝᵑ p)                = sym (eval✓ p)
  eval✓ (cong≡ᵝᵑlam {A} {B} p)    = cong (⟪lam⟫ {A} {B}) (⟨funext⟩ (eval✓ p))
  eval✓ (cong≡ᵝᵑapp {A} {B} p q)  = cong² (⟪app⟫ {A} {B}) (eval✓ p) (eval✓ q)
  eval✓ (cong≡ᵝᵑpair {A} {B} p q) = cong² (⟪pair⟫ {A} {B}) (eval✓ p) (eval✓ q)
  eval✓ (cong≡ᵝᵑfst {A} {B} p)    = cong (⟪fst⟫ {A} {B}) (eval✓ p)
  eval✓ (cong≡ᵝᵑsnd {A} {B} p)    = cong (⟪snd⟫ {A} {B}) (eval✓ p)
  eval✓ (reduce⇒ d e)            = lemreduce⇒ d e
  eval✓ (reduce⩕₁ d e)            = refl
  eval✓ (reduce⩕₂ d e)            = refl
  eval✓ (expand⇒ d)              = lemexpand⇒ d
  eval✓ (expand⩕ d)               = refl
  eval✓ (expand⫪ d)              = refl

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness


text:
{-# OPTIONS --without-K --safe #-}
module PiFracMemSem where

open import Relation.Binary.Core
open import Data.Empty
open import Function
open import Data.Nat
open import Data.Nat.Properties
open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.Vec
open import Data.Vec.Relation.Unary.Any.Properties
open import Data.Vec.Any hiding (map)
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ-syntax)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  renaming ([_] to R[_])
open import PiFracDyn

infix  80 ∣_∣

∣_∣ : (A : 𝕌) → ℕ
∣ 𝟘 ∣ = 0
∣ 𝟙 ∣ = 1
∣ A₁ +ᵤ A₂ ∣ = ∣ A₁ ∣ + ∣ A₂ ∣
∣ A₁ ×ᵤ A₂ ∣ = ∣ A₁ ∣ * ∣ A₂ ∣
∣ 𝟙/ A ∣ = 1

Vec× : ∀ {n m} {A B : Set} → Vec A n → Vec B m → Vec (A × B) (n * m)
Vec× va vb = concat (map (λ a₁ → map (a₁ ,_) vb) va)

∈map : ∀ {ℓ₁ ℓ₂} {n} {A : Set ℓ₁} {B : Set ℓ₂} {v : Vec A n} → (f : A → B) → (a : A)
     → Any (a ≡_) v → Any (f a ≡_) (map f v)
∈map f a (here refl) = here refl
∈map f a (there a∈v) = there (∈map f a a∈v)

inVec× : ∀ {n m} {A B : Set} → (va : Vec A n) → (vb : Vec B m)
       → (a : A) (b : B)
       → Any (a ≡_) va → Any (b ≡_) vb
       → Any ((a , b) ≡_) (Vec× va vb)
inVec× (a ∷ va) vb .a b (here refl) b∈vb = ++⁺ˡ {xs = map (a ,_) vb} (∈map _ _ b∈vb)
inVec× (x ∷ va) vb a b (there a∈va) b∈vb = ++⁺ʳ (map (x ,_) vb) (inVec× va vb a b a∈va b∈vb)

any≡← : ∀ {ℓ} {A : Set ℓ} {n} {a} → (v : Vec A n) → (i : Fin n) → a ≡ lookup v i → Any (a ≡_) v
any≡← (_ ∷ _)  Fin.0F refl = here refl
any≡← (_ ∷ v) (suc i) refl = there (any≡← v i refl)

Enum : (A : 𝕌) → Vec ⟦ A ⟧ ∣ A ∣
Enum 𝟘         = []
Enum 𝟙          = tt ∷ []
Enum (A₁ +ᵤ A₂) = map inj₁ (Enum A₁) ++ map inj₂ (Enum A₂)
Enum (A₁ ×ᵤ A₂) = Vec× (Enum A₁) (Enum A₂)
Enum (𝟙/ A) = ○ ∷ []

Find : {A : 𝕌} (x : ⟦ A ⟧) → Σ[ i ∈ Fin ∣ A ∣ ] (x ≡ lookup (Enum A) i)
Find {𝟘} ()
Find {𝟙} tt = index tt∈𝟙 , lookup-index tt∈𝟙
  where
    tt∈𝟙 : Any (tt ≡_) (Enum 𝟙)
    tt∈𝟙 = here refl
Find {A₁ +ᵤ A₂} (inj₁ x) =
  let i , p₁ = Find x in
  let x∈A₁ : Any ((inj₁ x) ≡_) (Enum (A₁ +ᵤ A₂))
      x∈A₁ = ++⁺ˡ {xs = map inj₁ (Enum A₁)} (∈map inj₁ x (any≡← _ i p₁)) in
  index x∈A₁ , lookup-index x∈A₁
Find {A₁ +ᵤ A₂} (inj₂ y) =
  let j , p₂ = Find y in
  let y∈A₂ : Any ((inj₂ y) ≡_) (Enum (A₁ +ᵤ A₂))
      y∈A₂ = ++⁺ʳ (map inj₁ (Enum A₁)) (∈map inj₂ y (any≡← _ j p₂)) in
  index y∈A₂ , lookup-index y∈A₂
Find {A₁ ×ᵤ A₂} (x , y) =
  let i , p₁ = Find x
      j , p₂ = Find y in
  let xy∈A₁×A₂ : Any ((x , y) ≡_) (Enum (A₁ ×ᵤ A₂))
      xy∈A₁×A₂ = inVec× (Enum A₁) (Enum A₂) x y (any≡← (Enum A₁) i p₁) (any≡← (Enum A₂) j p₂) in
  index xy∈A₁×A₂ , lookup-index xy∈A₁×A₂
Find {𝟙/ A} ○ = index ○∈𝟙/A , lookup-index ○∈𝟙/A
  where
    ○∈𝟙/A : Any (○ ≡_) (Enum (𝟙/ A))
    ○∈𝟙/A = here refl

Find' : {A : 𝕌} (x : ⟦ A ⟧) → Fin ∣ A ∣
Find' = proj₁ ∘ Find

data State (A : 𝕌) : Set where
  ⟪_[_]⟫ : Vec ⟦ A ⟧ ∣ A ∣ → Fin ∣ A ∣ → State A

resolve : {A : 𝕌} → State A → ⟦ A ⟧
resolve ⟪ v [ i ]⟫ = lookup v i

st : {A B : 𝕌} → ⟦ A ⟧ → (c : A ↔ B) → Σ[ C ∈ 𝕌 ] (C ↔ B × State C)
st (inj₂ y) (unite₊l {t})                   = _ , id↔ , ⟪ Enum t [ Find' y ]⟫
st a (uniti₊l {t})                          = _ , id↔ , ⟪ (Enum (𝟘 +ᵤ t)) [ Find' a ]⟫
st (inj₁ x) (unite₊r {t})                   = _ , id↔ , ⟪ Enum t [ Find' x ]⟫
st a (uniti₊r {t})                          = _ , id↔ , ⟪ (Enum (t +ᵤ 𝟘)) [ Find' {t +ᵤ 𝟘} (inj₁ a) ]⟫
st (inj₁ x) (swap₊ {t₁} {t₂})               = _ , id↔ , ⟪ Enum _ [ Find' {t₂ +ᵤ t₁} (inj₂ x) ]⟫
st (inj₂ y) (swap₊ {t₁} {t₂})               = _ , id↔ , ⟪ Enum _ [ Find' {t₂ +ᵤ t₁} (inj₁ y) ]⟫
st (inj₁ x) (assocl₊ {t₁} {t₂} {t₃})        = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ +ᵤ t₂) +ᵤ t₃} (inj₁ (inj₁ x)) ]⟫
st (inj₂ (inj₁ x)) (assocl₊ {t₁} {t₂} {t₃}) = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ +ᵤ t₂) +ᵤ t₃} (inj₁ (inj₂ x)) ]⟫
st (inj₂ (inj₂ y)) (assocl₊ {t₁} {t₂} {t₃}) = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ +ᵤ t₂) +ᵤ t₃} (inj₂ y) ]⟫
st (inj₁ (inj₁ x)) (assocr₊ {t₁} {t₂} {t₃}) = _ , id↔ , ⟪ Enum _ [ Find' {t₁ +ᵤ t₂ +ᵤ t₃} (inj₁ x) ]⟫
st (inj₁ (inj₂ y)) (assocr₊ {t₁} {t₂} {t₃}) = _ , id↔ , ⟪ Enum _ [ Find' {t₁ +ᵤ t₂ +ᵤ t₃} (inj₂ (inj₁ y)) ]⟫
st (inj₂ y) (assocr₊ {t₁} {t₂} {t₃})        = _ , id↔ , ⟪ Enum _ [ Find' {t₁ +ᵤ t₂ +ᵤ t₃} (inj₂ (inj₂ y)) ]⟫
st (tt , y) unite⋆l                         = _ , id↔ , ⟪ Enum _ [ Find' y ]⟫
st a uniti⋆l                                = _ , id↔ , ⟪ Enum _ [ Find' (tt , a) ]⟫
st (x , tt) unite⋆r                         = _ , id↔ , ⟪ Enum _ [ Find' x ]⟫
st a uniti⋆r                                = _ , id↔ , ⟪ Enum _ [ Find' (a , tt) ]⟫
st (x , y) swap⋆                            = _ , id↔ , ⟪ Enum _ [ Find' (y , x) ]⟫
st (x , y , z) assocl⋆                      = _ , id↔ , ⟪ Enum _ [ Find' ((x , y) , z) ]⟫
st ((x , y) , z) assocr⋆                    = _ , id↔ , ⟪ Enum _ [ Find' (x , y , z) ]⟫
st (inj₁ x , y) (dist {t₁} {t₂} {t₃})       = _ , id↔ , ⟪ Enum _ [ Find' {t₁ ×ᵤ t₃ +ᵤ t₂ ×ᵤ t₃} (inj₁ (x , y)) ]⟫
st (inj₂ x , y) (dist {t₁} {t₂} {t₃})       = _ , id↔ , ⟪ Enum _ [ Find' {t₁ ×ᵤ t₃ +ᵤ t₂ ×ᵤ t₃} (inj₂ (x , y)) ]⟫
st (inj₁ (x , y)) (factor {t₁} {t₂} {t₃})   = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ +ᵤ t₂) ×ᵤ t₃} (inj₁ x , y) ]⟫
st (inj₂ (y , z)) (factor {t₁} {t₂} {t₃})   = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ +ᵤ t₂) ×ᵤ t₃} (inj₂ y , z) ]⟫
st (x , inj₁ y) (distl {t₁} {t₂} {t₃})      = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)} (inj₁ (x , y)) ]⟫
st (x , inj₂ y) (distl {t₁} {t₂} {t₃})      = _ , id↔ , ⟪ Enum _ [ Find' {(t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)} (inj₂ (x , y)) ]⟫
st (inj₁ (x , y)) (factorl {t₁} {t₂} {t₃})  = _ , id↔ , ⟪ Enum _ [ Find' {t₁ ×ᵤ (t₂ +ᵤ t₃)} (x , inj₁ y) ]⟫
st (inj₂ (x , z)) (factorl {t₁} {t₂} {t₃})  = _ , id↔ , ⟪ Enum _ [ Find' {t₁ ×ᵤ (t₂ +ᵤ t₃)} (x , inj₂ z) ]⟫
st tt (η {t} v)                           = _ , id↔ , ⟪ Enum (t ×ᵤ (𝟙/ v)) [ Find' {t ×ᵤ (𝟙/ v)} (v , ○) ]⟫
st (x , ○) (ε {t} v) with 𝕌dec t v x
st (x , ○) (ε {t} v) | yes _ = _ , id↔ , ⟪ Enum _ [ Find' tt ]⟫
st (x , ○) (ε {t} v) | no  _ = _ , (ε {t} v) , ⟪ Enum (t ×ᵤ (𝟙/ v)) [ Find' {t ×ᵤ (𝟙/ v)} (x , ○) ]⟫
st a id↔                                    = _ , id↔ , ⟪ Enum _ [ Find' a ]⟫
st a (id↔ ⊚ c)                              = _ , c , ⟪ Enum _ [ Find' a ]⟫
st a (c₁ ⊚ c₂)                              = let _ , c , st' = st a c₁ in
                                              _ , c ⊚ c₂ , st'
st (inj₁ x) (_⊕_ {t₁} {t₂} {_} {t₄} id↔ c₂) = _ , id↔ , ⟪ Enum _ [ Find' {_ +ᵤ t₄} (inj₁ x) ]⟫
st (inj₁ x) (_⊕_ {t₁} {t₂} c₁ c₂)           = let _ , c , st' = st x c₁ in
                                              _ , c ⊕ c₂ , ⟪ Enum _ [ Find' {_ +ᵤ t₂} (inj₁ $ resolve st') ]⟫
st (inj₂ y) (_⊕_ {t₁} {t₂} {t₃} {_} c₁ id↔) = _ , id↔ , ⟪ Enum _ [ Find' {t₃ +ᵤ _} (inj₂ y) ]⟫
st (inj₂ y) (_⊕_ {t₁} c₁ c₂)                = let _ , c , st' = st y c₂ in
                                              _ , c₁ ⊕ c , ⟪ Enum _ [ Find' {t₁ +ᵤ _} (inj₂ $ resolve st') ]⟫
st (x , y) (id↔ ⊗ id↔)                      = _ , id↔ , ⟪ Enum _ [ Find' (x , y) ]⟫
st (x , y) (id↔ ⊗ c₂)                       = let _ , c , st' = st y c₂ in
                                               _ , id↔ ⊗ c , ⟪ Enum _ [ Find' (x , resolve st') ]⟫
st (x , y) (c₁ ⊗ c₂)                        = let _ , c , st' = st x c₁ in
                                              _ , c ⊗ c₂ , ⟪ Enum _ [ Find' (resolve st' , y) ]⟫

step : {A B : 𝕌} (c : A ↔ B) → State A → Σ[ C ∈ 𝕌 ] (C ↔ B × State C)
step c ⟪ v [ i ]⟫ = st (lookup v i) c

data State' : Set where
  ⟪_∥_[_]⟫ : {A B : 𝕌} → A ↔ B → Vec ⟦ A ⟧ ∣ A ∣ → Fin ∣ A ∣ → State'

step' : State' → State'
step' ⟪ c ∥ v [ i ]⟫ with step c ⟪ v [ i ]⟫
step' ⟪ c ∥ v [ i ]⟫ | _ , c' , ⟪ v' [ i' ]⟫ = ⟪ c' ∥ v' [ i' ]⟫

run : (n : ℕ) → State' → Vec State' (suc n)
run 0 st = [ st ]
run (suc n) st with run n st
... | sts with last sts
... | ⟪ cx ∥ vx [ ix ]⟫ rewrite +-comm 1 (suc n) = sts ++ [ step' ⟪ cx ∥ vx [ ix ]⟫ ]

ex₁ : Vec State' 33
ex₁ = run 32 ⟪ id' ∥ Enum 𝟚 [ Fin.fromℕ 1 ]⟫

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Common.Prelude
open import Common.Equality
open import Common.Reflection

pattern _`+_ a b = def (quote _+_) (vArg a ∷ vArg b ∷ [])

`_ : Term → Term
` con c [] = con (quote Term.con) (vArg (lit (qname c)) ∷ vArg (con (quote []) []) ∷ [])
` _        = unknown

-- Prevent quotation
data WrapTerm : Set where
  wrap : Term → WrapTerm

macro
  eval : WrapTerm → Tactic
  eval (wrap u) hole = bindTC (normalise u) λ u → unify hole (` u)

t : Term
t = lam visible (abs "n" (lit (nat 1) `+ var 0 []))

lem : eval (wrap t) ≡ Term.con (quote suc) []
lem = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Hilbert-style formalisation of closed syntax.
-- Sequences of terms.

module OldBasicILP.UntypedSyntax.ClosedHilbertSequential where

open import OldBasicILP.UntypedSyntax.Common public

-- Closed, untyped representations.

data Rep : ℕ → Set where
  NIL   : Rep zero
  MP    : ∀ {n} → Fin n → Fin n → Rep n → Rep (suc n)
  CI    : ∀ {n} → Rep n → Rep (suc n)
  CK    : ∀ {n} → Rep n → Rep (suc n)
  CS    : ∀ {n} → Rep n → Rep (suc n)
  NEC   : ∀ {n} → ∀ {`n} → Rep (suc `n) → Rep n → Rep (suc n)
  CDIST : ∀ {n} → Rep n → Rep (suc n)
  CUP   : ∀ {n} → Rep n → Rep (suc n)
  CDOWN : ∀ {n} → Rep n → Rep (suc n)
  CPAIR : ∀ {n} → Rep n → Rep (suc n)
  CFST  : ∀ {n} → Rep n → Rep (suc n)
  CSND  : ∀ {n} → Rep n → Rep (suc n)
  UNIT  : ∀ {n} → Rep n → Rep (suc n)

-- Anti-bug wrappers.

record Proof : Set where
  constructor [_]
  field
    {len} : ℕ
    rep   : Rep (suc len)

open ClosedSyntax (Proof) public

-- Concatenation of representations.

_⧺ᴿ_ : ∀ {n₁ n₂} → Rep n₁ → Rep n₂ → Rep (n₁ + n₂)
r₁ ⧺ᴿ NIL       = r₁
r₁ ⧺ᴿ MP i j r₂ = MP (monoFin weak≤+₂ i) (monoFin weak≤+₂ j) (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CI r₂     = CI (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CK r₂     = CK (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CS r₂     = CS (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ NEC `r r₂ = NEC `r (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CDIST r₂  = CDIST (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CUP r₂    = CUP (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CDOWN r₂  = CDOWN (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CPAIR r₂  = CPAIR (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CFST r₂   = CFST (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ CSND r₂   = CSND (r₁ ⧺ᴿ r₂)
r₁ ⧺ᴿ UNIT r₂   = UNIT (r₁ ⧺ᴿ r₂)

-- Modus ponens and necessitation in nested form.

APP : ∀ {n₁ n₂} → Rep (suc n₁) → Rep (suc n₂) → Rep (suc (suc n₂ + suc n₁))
APP {n₁} {n₂} r₁ r₂ = MP zero (monoFin (weak≤+₁ (suc n₁)) zero) (r₂ ⧺ᴿ r₁)

BOX : ∀ {n} → Rep (suc n) → Rep (suc zero)
BOX {n} r = NEC r NIL

-- Derivations.

mutual
  infix 3 ⊢ᴰ_
  data ⊢ᴰ_ : Cx Ty → Set where
    nil   : ⊢ᴰ ∅
    mp    : ∀ {Ξ A B}   → A ▻ B ∈ Ξ → A ∈ Ξ → ⊢ᴰ Ξ → ⊢ᴰ Ξ , B
    ci    : ∀ {Ξ A}     → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ▻ A
    ck    : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ▻ B ▻ A
    cs    : ∀ {Ξ A B C} → ⊢ᴰ Ξ → ⊢ᴰ Ξ , (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C

    nec   : ∀ {Ξ A}     → ∀ {`Ξ} → (d : ⊢ᴰ `Ξ , A)
                        → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ ᴿ⌊ d ⌋ ] ⦂ A

    cdist : ∀ {Ξ A B}   → ∀ {n₁ n₂} → {r₁ : Rep (suc n₁)} → {r₂ : Rep (suc n₂)}
                        → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ r₁ ] ⦂ (A ▻ B) ▻ [ r₂ ] ⦂ A ▻ [ APP r₁ r₂ ] ⦂ B

    cup   : ∀ {Ξ A}     → ∀ {n} → {r : Rep (suc n)}
                        → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ r ] ⦂ A ▻ [ BOX r ] ⦂ [ r ] ⦂ A

    cdown : ∀ {Ξ A}     → ∀ {n} → {r : Rep (suc n)}
                        → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ r ] ⦂ A ▻ A

    cpair : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ▻ B ▻ A ∧ B
    cfst  : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ∧ B ▻ A
    csnd  : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ∧ B ▻ B
    unit  : ∀ {Ξ}       → ⊢ᴰ Ξ → ⊢ᴰ Ξ , ⊤

  -- Projection from derivations to representations.

  ᴿ⌊_⌋ : ∀ {Ξ} → ⊢ᴰ Ξ → Rep ᴺ⌊ Ξ ⌋
  ᴿ⌊ nil ⌋      = NIL
  ᴿ⌊ mp i j d ⌋ = MP ⁱ⌊ i ⌋ ⁱ⌊ j ⌋ ᴿ⌊ d ⌋
  ᴿ⌊ ci d ⌋     = CI ᴿ⌊ d ⌋
  ᴿ⌊ ck d ⌋     = CK ᴿ⌊ d ⌋
  ᴿ⌊ cs d ⌋     = CS ᴿ⌊ d ⌋
  ᴿ⌊ nec `d d ⌋ = NEC ᴿ⌊ `d ⌋ ᴿ⌊ d ⌋
  ᴿ⌊ cdist d ⌋  = CDIST ᴿ⌊ d ⌋
  ᴿ⌊ cup d ⌋    = CUP ᴿ⌊ d ⌋
  ᴿ⌊ cdown d ⌋  = CDOWN ᴿ⌊ d ⌋
  ᴿ⌊ cpair d ⌋  = CPAIR ᴿ⌊ d ⌋
  ᴿ⌊ cfst d ⌋   = CFST ᴿ⌊ d ⌋
  ᴿ⌊ csnd d ⌋   = CSND ᴿ⌊ d ⌋
  ᴿ⌊ unit d ⌋   = UNIT ᴿ⌊ d ⌋

-- Anti-bug wrappers.

infix 3 ⊢_
⊢_ : Ty → Set
⊢ A = ∃ (λ Ξ → ⊢ᴰ Ξ , A)

-- Concatenation of derivations.

_⧺ᴰ_ : ∀ {Ξ₁ Ξ₂} → ⊢ᴰ Ξ₁ → ⊢ᴰ Ξ₂ → ⊢ᴰ Ξ₁ ⧺ Ξ₂
d₁ ⧺ᴰ nil       = d₁
d₁ ⧺ᴰ mp i j d₂ = mp (mono∈ weak⊆⧺₂ i) (mono∈ weak⊆⧺₂ j) (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ ci d₂     = ci (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ ck d₂     = ck (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cs d₂     = cs (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ nec `d d₂ = nec `d (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cdist d₂  = cdist (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cup d₂    = cup (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cdown d₂  = cdown (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cpair d₂  = cpair (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cfst d₂   = cfst (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ csnd d₂   = csnd (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ unit d₂   = unit (d₁ ⧺ᴰ d₂)

-- Modus ponens and necessitation in nested form.

app : ∀ {A B} → ⊢ A ▻ B → ⊢ A → ⊢ B
app {A} {B} (Ξ₁ , d₁) (Ξ₂ , d₂) = Ξ₃ , d₃
  where Ξ₃ = (Ξ₂ , A) ⧺ (Ξ₁ , A ▻ B)
        d₃ = mp top (mono∈ (weak⊆⧺₁ (Ξ₁ , A ▻ B)) top) (d₂ ⧺ᴰ d₁)

box : ∀ {A} → (t : ⊢ A) → ⊢ [ ᴿ⌊ π₂ t ⌋ ] ⦂ A
box (Ξ , d) = ∅ , nec d nil

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Nat.Sum where

open import Data.Nat
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open DecTotalOrder decTotalOrder hiding (refl)

+id : (n : ℕ) → n + zero ≡  n
+id zero = refl
+id (suc n) = cong suc (+id n)

+assoc : (m n : ℕ) → m + suc n ≡ suc (m + n)
+assoc zero n = refl
+assoc (suc m) n = cong suc (+assoc m n)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module CH where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
zero      + m  = m
(succ n)  + m  = succ (n + m)

infix 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

{-
t1 : {n : ℕ} -> zero ≡ n
t1 = refl
-}

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

sym : ∀ x y → x == y → y == x
sym .a .a (refl' a) = refl' a

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
-- This is mainly a test of the quality of error messages for
-- termination problems.

module TerminationLambda where

postulate Id : Set → Set

F : Set → Set
F = λ A → F (Id A)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module UniDB.Morph.Shifts where

open import UniDB.Spec

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

data Shifts : MOR where
  refl : {γ : Dom} → Shifts γ γ
  step : {γ₁ γ₂ : Dom} (ξ : Shifts γ₁ γ₂) → Shifts γ₁ (suc γ₂)
  skip : {γ₁ γ₂ : Dom} (ξ : Shifts γ₁ γ₂) → Shifts (suc γ₁) (suc γ₂)

shiftIx : {γ₁ γ₂ : Dom} (ξ : Shifts γ₁ γ₂) (i : Ix γ₁) → Ix γ₂
shiftIx refl     i       = i
shiftIx (step ξ) i       = suc (shiftIx ξ i)
shiftIx (skip ξ) zero    = zero
shiftIx (skip ξ) (suc i) = suc (shiftIx ξ i)

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

instance
  iLkShifts : {T : STX} {{vrT : Vr T}} → Lk T Shifts
  lk {{iLkShifts}} ξ i = vr (shiftIx ξ i)

  iUpShifts : Up Shifts
  _↑₁    {{iUpShifts}} refl = refl
  _↑₁    {{iUpShifts}} ξ          = skip ξ
  _↑_    {{iUpShifts}} ξ 0        = ξ
  _↑_    {{iUpShifts}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpShifts}} ξ          = refl
  ↑-suc  {{iUpShifts}} ξ δ⁺       = refl

  iIdmShifts : Idm Shifts
  idm {{iIdmShifts}} γ = refl {γ}

  iWkmShifts : Wkm Shifts
  wkm {{iWkmShifts}} zero    = idm _
  wkm {{iWkmShifts}} (suc δ) = step (wkm δ)

  iCompShifts : Comp Shifts
  _⊙_ {{iCompShifts}} ξ₁        refl      = ξ₁
  _⊙_ {{iCompShifts}} ξ₁        (step ξ₂) = step (ξ₁ ⊙ ξ₂)
  _⊙_ {{iCompShifts}} refl      (skip ξ₂) = skip ξ₂
  _⊙_ {{iCompShifts}} (step ξ₁) (skip ξ₂) = step (ξ₁ ⊙ ξ₂)
  _⊙_ {{iCompShifts}} (skip ξ₁) (skip ξ₂) = skip (ξ₁ ⊙ ξ₂)

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

shiftIx-⊙ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts γ₁ γ₂) (ξ₂ : Shifts γ₂ γ₃) →
  (i : Ix γ₁) → shiftIx (ξ₁ ⊙ ξ₂) i ≡ shiftIx ξ₂ (shiftIx ξ₁ i)
shiftIx-⊙ ξ₁        refl      i       = refl
shiftIx-⊙ ξ₁        (step ξ₂) i       = cong suc (shiftIx-⊙ ξ₁ ξ₂ i)
shiftIx-⊙ refl      (skip ξ₂) i       = refl
shiftIx-⊙ (step ξ₁) (skip ξ₂) i       = cong suc (shiftIx-⊙ ξ₁ ξ₂ i)
shiftIx-⊙ (skip ξ₁) (skip ξ₂) zero    = refl
shiftIx-⊙ (skip ξ₁) (skip ξ₂) (suc i) = cong suc (shiftIx-⊙ ξ₁ ξ₂ i)

shiftIx-wkm : {γ : Dom} (δ : Dom) (i : Ix γ) →
  shiftIx (wkm δ) i ≡ wk δ i
shiftIx-wkm zero    i = refl
shiftIx-wkm (suc δ) i = cong suc (shiftIx-wkm δ i)

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

instance
  iUpIdmShifts : UpIdm Shifts
  idm-↑₁ {{iUpIdmShifts}} = refl

  iCompIdmShifts : CompIdm Shifts
  ⊙-idm {{iCompIdmShifts}} ξ        = refl
  idm-⊙ {{iCompIdmShifts}} refl     = refl
  idm-⊙ {{iCompIdmShifts}} (step ξ) = cong step (idm-⊙ ξ)
  idm-⊙ {{iCompIdmShifts}} (skip ξ) = refl

  iUpCompShifts : UpComp Shifts
  ⊙-↑₁ {{iUpCompShifts}} ξ        refl     = refl
  ⊙-↑₁ {{iUpCompShifts}} refl     (step ζ) = cong (skip ∘ step) (idm-⊙ ζ)
  ⊙-↑₁ {{iUpCompShifts}} (step ξ) (step ζ) = refl
  ⊙-↑₁ {{iUpCompShifts}} (skip ξ) (step ζ) = refl
  ⊙-↑₁ {{iUpCompShifts}} refl     (skip ζ) = refl
  ⊙-↑₁ {{iUpCompShifts}} (step ξ) (skip ζ) = refl
  ⊙-↑₁ {{iUpCompShifts}} (skip ξ) (skip ζ) = refl

  iWkmHomShifts : WkmHom Shifts
  wkm-zero {{iWkmHomShifts}}   = refl
  wkm-suc  {{iWkmHomShifts}} δ = refl

module _ {T : STX} {{vrT : Vr T}} where

  instance
    iLkUpShifts : {{wkT : Wk T}} {{wkVrT : WkVr T}} → LkUp T Shifts
    lk-↑₁-zero {{iLkUpShifts}} refl       = refl
    lk-↑₁-zero {{iLkUpShifts}} (step ξ)   = refl
    lk-↑₁-zero {{iLkUpShifts}} (skip ξ)   = refl
    lk-↑₁-suc  {{iLkUpShifts}} refl i     = sym (wk₁-vr i)
    lk-↑₁-suc  {{iLkUpShifts}} (step ξ) i = sym (wk₁-vr (suc (shiftIx ξ i)))
    lk-↑₁-suc  {{iLkUpShifts}} (skip ξ) i = sym (wk₁-vr (shiftIx (skip ξ) i))

    iLkRenShifts : LkRen T Shifts
    lk-ren {{iLkRenShifts}} ξ i = refl

    iLkIdmShifts : LkIdm T Shifts
    lk-idm {{iLkIdmShifts}} i = refl

    iLkWkmShifts : LkWkm T Shifts
    lk-wkm {{iLkWkmShifts}} δ i = cong vr (shiftIx-wkm δ i)

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
module Issue1422 where

open import Common.Level public using (Level ; lzero ; lsuc) renaming (_⊔_ to _l⊔_)
open import Common.Equality public

-- # Relations

relation : ∀ {ℓ} ℓ' → Set ℓ → Set (lsuc ℓ' l⊔ ℓ)
relation ℓ' α = α → α → Set ℓ'

reflexive : ∀ {ℓ ℓ'} {α : Set ℓ} → relation ℓ' α → Set (ℓ l⊔ ℓ')
reflexive _R_ = ∀ {x} → x R x

antisymmetric : ∀ {ℓ ℓ'} {α : Set ℓ} → relation ℓ' α → Set (ℓ l⊔ ℓ')
antisymmetric _R_ = ∀ {x y} → x R y → y R x → x ≡ y

_⇉_ : ∀ {ℓ₁ ℓ₁' ℓ₂ ℓ₂'} {α : Set ℓ₁} {β : Set ℓ₂} (_R₁_ : relation ℓ₁' α) (_R₂_ : relation ℓ₂' β) → relation (ℓ₁ l⊔ ℓ₁' l⊔ ℓ₂') (α → β)
(_R₁_ ⇉ _R₂_) f g = ∀ {x y} → x R₁ y → f x R₂ g y

proper : ∀ {ℓ ℓ'} {α : Set ℓ} (_R_ : relation ℓ' α) → α → Set ℓ'
proper _R_ x = x R x

-- # Dom

record Dom {ℓ} ℓ' (D : Set ℓ) : Set (lsuc ℓ l⊔ lsuc ℓ') where
  field
    ⟦_⟧ : D → Set ℓ'
open Dom {{...}} public

-- # Partial Order

record PartialOrder {ℓ} ℓ' (α : Set ℓ) : Set (ℓ l⊔ lsuc ℓ') where
  infix  4 _⊑_
  field
    _⊑_ : relation ℓ' α
    ⊑-reflexivity : reflexive _⊑_
    ⊑-antisymmetry : antisymmetric _⊑_

open PartialOrder {{...}} public

monotonic : ∀ {ℓ₁ ℓ₁' ℓ₂ ℓ₂'} {α : Set ℓ₁} {{αPO : PartialOrder ℓ₁' α}} {β : Set ℓ₂} {{βPO : PartialOrder ℓ₂' β}} → (α → β) → Set (ℓ₁ l⊔ ℓ₁' l⊔ ℓ₂')
monotonic = proper (_⊑_ ⇉ _⊑_)


text:
------------------------------------------------------------------------------
-- Distributive laws base
------------------------------------------------------------------------------

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

module DistributiveLaws.Base where

infixl 7 _·_

------------------------------------------------------------------------------
-- First-order logic with equality.
--
-- NB. This is an equational theory, so we do not import the logical
-- constants.
open import Common.FOL.FOL-Eq public using ( _≡_ ; D ; refl ; subst ; sym )

-- Distributive laws axioms

postulate
  _·_ : D → D → D  -- The binary operation.

  leftDistributive  : ∀ x y z → x · (y · z) ≡ (x · y) · (x · z)
  rightDistributive : ∀ x y z → (x · y) · z ≡ (x · z) · (y · z)
{-# ATP axioms leftDistributive rightDistributive #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

module completeness where
  -- any hole is new to a complete expression
  e-complete-hnn : ∀{e u} → e ecomplete → hole-name-new e u
  e-complete-hnn (ECFix cmp) = HNNFix (e-complete-hnn cmp)
  e-complete-hnn ECVar = HNNVar
  e-complete-hnn (ECAp cmp1 cmp2) = HNNAp (e-complete-hnn cmp1) (e-complete-hnn cmp2)
  e-complete-hnn ECUnit = HNNUnit
  e-complete-hnn (ECPair cmp cmp₁) = HNNPair (e-complete-hnn cmp) (e-complete-hnn cmp₁)
  e-complete-hnn (ECFst cmp) = HNNFst (e-complete-hnn cmp)
  e-complete-hnn (ECSnd cmp) = HNNSnd (e-complete-hnn cmp)
  e-complete-hnn (ECCtor cmp) = HNNCtor (e-complete-hnn cmp)
  e-complete-hnn (ECCase cmp h) = HNNCase (e-complete-hnn cmp) λ i<∥rules∥ → e-complete-hnn (h i<∥rules∥)
  e-complete-hnn (ECAsrt cmp1 cmp2) = HNNAsrt (e-complete-hnn cmp1) (e-complete-hnn cmp2)

  {- TODO : probably delete
  e-hnn-complete : ∀{e} → (∀{u} → hole-name-new e u) → e ecomplete
  e-hnn-complete hnn∀ = {!!}
  -}

  -- a complete expression is holes-disjoint to all expressions
  e-complete-disjoint : ∀{e1 e2} → e1 ecomplete → holes-disjoint e1 e2
  e-complete-disjoint (ECFix cmp) = HDFix (e-complete-disjoint cmp)
  e-complete-disjoint ECVar = HDVar
  e-complete-disjoint (ECAp cmp1 cmp2) = HDAp (e-complete-disjoint cmp1) (e-complete-disjoint cmp2)
  e-complete-disjoint ECUnit = HDUnit
  e-complete-disjoint (ECPair cmp cmp₁) = HDPair (e-complete-disjoint cmp) (e-complete-disjoint cmp₁)
  e-complete-disjoint (ECFst cmp) = HDFst (e-complete-disjoint cmp)
  e-complete-disjoint (ECSnd cmp) = HDSnd (e-complete-disjoint cmp)
  e-complete-disjoint (ECCtor cmp) = HDCtor (e-complete-disjoint cmp)
  e-complete-disjoint (ECCase cmp h) = HDCase (e-complete-disjoint cmp) λ i<∥rules∥ → e-complete-disjoint (h i<∥rules∥)
  e-complete-disjoint (ECAsrt cmp1 cmp2) = HDAsrt (e-complete-disjoint cmp1) (e-complete-disjoint cmp2)

  -- TODO a holes-disjoint-sym check - very involved but arguably pretty important

  -- TODO we should generalize this, to a theorem that says that if a hole name is new in
  -- e, then it is new in r and k
  {- TODO}
  -- if e evals to r, and e is complete, then r is complete
  eval-completeness : ∀{Δ Σ' Γ E e r τ k} →
                        E env-complete →
                        Δ , Σ' , Γ ⊢ E →
                        Δ , Σ' , Γ ⊢ e :: τ →
                        E ⊢ e ⇒ r ⊣ k →
                        e ecomplete →
                        r rcomplete
  eval-completeness Ecmp Γ⊢E (TALam _ _) EFun (ECLam ecmp) = RCLam Ecmp ecmp
  eval-completeness Ecmp Γ⊢E (TAFix _ _ _) EFix (ECFix ecmp) = RCFix Ecmp ecmp
  eval-completeness (ENVC Ecmp) Γ⊢E (TAVar _) (EVar h) ECVar = Ecmp h
  eval-completeness Ecmp Γ⊢E (TAApp _ ta-f ta-arg) (EApp {Ef = Ef} {x} {r2 = r2} CF∞ eval-f eval-arg eval-ef) (ECAp cmp-f cmp-arg)
    with eval-completeness Ecmp Γ⊢E ta-f eval-f cmp-f | preservation Γ⊢E ta-f eval-f
  ... | RCLam (ENVC Efcmp) efcmp | TALam Γ'⊢Ef (TALam _ ta-ef)
    = eval-completeness (ENVC env-cmp) (EnvInd Γ'⊢Ef (preservation Γ⊢E ta-arg eval-arg)) ta-ef eval-ef efcmp
      where
        env-cmp : ∀{x' rx'} → (x' , rx') ∈ (Ef ,, (x , r2)) → rx' rcomplete
        env-cmp {x'} {rx'} h with ctx-split {Γ = Ef} h
        env-cmp {x'} {rx'} h | Inl (_ , x'∈Ef) = Efcmp x'∈Ef
        env-cmp {x'} {rx'} h | Inr (_ , rx'==r2) rewrite rx'==r2 =
          eval-completeness Ecmp Γ⊢E ta-arg eval-arg cmp-arg
  eval-completeness Ecmp Γ⊢E (TAApp _ ta-f ta-arg) (EAppFix {Ef = Ef} {f} {x} {ef} {r2 = r2} CF∞ h eval-f eval-arg eval-ef) (ECAp cmp-f cmp-arg)
    rewrite h with eval-completeness Ecmp Γ⊢E ta-f eval-f cmp-f | preservation Γ⊢E ta-f eval-f
  ... | RCFix (ENVC Efcmp) efcmp | TAFix Γ'⊢Ef (TAFix _ _ ta-ef) =
    eval-completeness (ENVC new-Ef+-cmp) new-ctxcons ta-ef eval-ef efcmp
    where
      new-ctxcons =
        EnvInd (EnvInd Γ'⊢Ef (preservation Γ⊢E ta-f eval-f)) (preservation Γ⊢E ta-arg eval-arg)
      new-Ef-cmp  : ∀{x' rx'} → (x' , rx') ∈ (Ef ,, (f , [ Ef ]fix f ⦇·λ x => ef ·⦈)) → rx' rcomplete
      new-Ef-cmp  {x'} {rx'} h with ctx-split {Γ = Ef} h
      new-Ef-cmp  {x'} {rx'} h | Inl (_ , x'∈Ef) = Efcmp x'∈Ef
      new-Ef-cmp  {x'} {rx'} h | Inr (_ , rx'==r2) rewrite rx'==r2 = RCFix (ENVC Efcmp) efcmp
      new-Ef+-cmp : ∀{x' rx'} → (x' , rx') ∈ (Ef ,, (f , [ Ef ]fix f ⦇·λ x => ef ·⦈) ,, (x , r2)) → rx' rcomplete
      new-Ef+-cmp {x'} {rx'} h with ctx-split {Γ = Ef ,, (f , [ Ef ]fix f ⦇·λ x => ef ·⦈)} h
      new-Ef+-cmp {x'} {rx'} h | Inl (_ , x'∈Ef+) = new-Ef-cmp x'∈Ef+
      new-Ef+-cmp {x'} {rx'} h | Inr (_ , rx'==r2) rewrite rx'==r2 =
        eval-completeness Ecmp Γ⊢E ta-arg eval-arg cmp-arg
  eval-completeness Ecmp Γ⊢E (TAApp _ ta1 ta2) (EAppUnfinished eval1 _ _ eval2) (ECAp ecmp1 ecmp2) =
    RCAp (eval-completeness Ecmp Γ⊢E ta1 eval1 ecmp1) (eval-completeness Ecmp Γ⊢E ta2 eval2 ecmp2)
  eval-completeness Ecmp Γ⊢E (TATpl ∥es∥==∥τs∥ _ tas) (ETuple ∥es∥==∥rs∥ ∥es∥==∥ks∥ evals) (ECTpl cmps) =
    RCTpl λ {i} rs[i] →
      let
        _ , es[i] = ∥l1∥==∥l2∥→l1[i]→l2[i] (! ∥es∥==∥rs∥) rs[i]
        _ , ks[i] = ∥l1∥==∥l2∥→l1[i]→l2[i] ∥es∥==∥ks∥ es[i]
        _ , τs[i] = ∥l1∥==∥l2∥→l1[i]→l2[i] ∥es∥==∥τs∥ es[i]
      in
      eval-completeness Ecmp Γ⊢E (tas es[i] τs[i]) (evals es[i] rs[i] ks[i]) (cmps es[i])
  eval-completeness Ecmp Γ⊢E (TAGet ∥rs⊫=∥τs∥ i<∥τs∥ ta) (EGet _ i<∥rs∥ eval) (ECGet ecmp)
    with eval-completeness Ecmp Γ⊢E ta eval ecmp
  ... | RCTpl h = h i<∥rs∥
  eval-completeness Ecmp Γ⊢E (TAGet _ i<∥τs∥ ta) (EGetUnfinished eval _) (ECGet ecmp) =
    RCGet (eval-completeness Ecmp Γ⊢E ta eval ecmp)
  eval-completeness Ecmp Γ⊢E (TACtor _ _ ta) (ECtor eval) (ECCtor ecmp) =
    RCCtor (eval-completeness Ecmp Γ⊢E ta eval ecmp)
  eval-completeness {Σ' = Σ'} (ENVC Ecmp) Γ⊢E (TACase d∈Σ'1 ta h1 h2) (EMatch {E = E} {xc = xc} {r' = r'} CF∞ form eval eval-ec) (ECCase ecmp rules-cmp)
    with h2 form
  ... | _ , _ , _ , _ , c∈cctx1 , ta-ec
    with preservation Γ⊢E ta eval
  ... | TACtor {cctx = cctx} d∈Σ' c∈cctx ta-r'
    rewrite ctxunicity {Γ = π1 Σ'} d∈Σ'1 d∈Σ' | ctxunicity {Γ = cctx} c∈cctx1 c∈cctx =
    eval-completeness (ENVC new-E-cmp) (EnvInd Γ⊢E ta-r') ta-ec eval-ec (rules-cmp form)
    where
      new-E-cmp : ∀{x' rx'} → (x' , rx') ∈ (E ,, (xc , r')) → rx' rcomplete
      new-E-cmp {x'} {rx'} x'∈E+ with ctx-split {Γ = E} x'∈E+
      ... | Inl (_ , x'∈E) = Ecmp x'∈E
      ... | Inr (_ , rx'==r') rewrite rx'==r'
        with eval-completeness (ENVC Ecmp) Γ⊢E ta eval ecmp
      ... | RCCtor r'cmp = r'cmp
  eval-completeness Ecmp Γ⊢E (TACase _ ta _ _) (EMatchUnfinished eval _) (ECCase ecmp rulescmp) =
    RCCase Ecmp (eval-completeness Ecmp Γ⊢E ta eval ecmp) rulescmp
  eval-completeness Ecmp Γ⊢E (TAHole _) EHole ()
  eval-completeness Ecmp Γ⊢E (TAPF _) EPF (ECPF pf-cmp) = RCPF pf-cmp
  eval-completeness Ecmp Γ⊢E (TAAsrt _ _ _) (EAsrt _ _ _) (ECAsrt _ _) = RCTpl (λ ())
  -}

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


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

module Experiment.FingerTree.Common where
open import Level renaming (zero to lzero ; suc to lsuc)
open import Algebra
open import Data.Product
open import Function.Core
open import Function.Endomorphism.Propositional
open import Data.Nat hiding (_⊔_)
import Data.Nat.Properties as ℕₚ

foldr-to-foldMap : ∀ {a b e} {F : Set a → Set a} →
 (∀ {A : Set a} {B : Set b} → (A → B → B) → B → F A → B) →
 ∀ {A : Set a} (M : Monoid b e) → (A → Monoid.Carrier M) → F A → Monoid.Carrier M
foldr-to-foldMap foldr M f xs = foldr (λ x m → Monoid._∙_ M (f x) m) (Monoid.ε M) xs

foldMap-to-foldr : ∀ {a b} {F : Set a → Set a} →
  (∀ {A : Set a} (M : Monoid b b) → (A → Monoid.Carrier M) → F A → Monoid.Carrier M) →
  ∀ {A : Set a} {B : Set b} → (A → B → B) → B → F A → B
foldMap-to-foldr foldMap {B = B} f e xs = foldMap (∘-id-monoid B) f xs e

dual : ∀ {c e} → Monoid c e → Monoid c e
dual m = record
  { Carrier = Carrier
  ; _≈_      = _≈_
  ; _∙_      = flip _∙_
  ; ε        = ε
  ; isMonoid = record
    { isSemigroup = record
      { isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = λ x≈y u≈v → ∙-cong u≈v x≈y
        }
      ; assoc   = λ x y z → sym $ assoc z y x
      }
    ; identity    = identityʳ , identityˡ
    }
  }
  where open Monoid m

foldMap-to-foldl : ∀ {a b} {F : Set a → Set a} →
  (∀ {A : Set a} (M : Monoid b b) → (A → Monoid.Carrier M) → F A → Monoid.Carrier M) →
  ∀ {A : Set a} {B : Set b} → (B → A → B) → B → F A → B
foldMap-to-foldl foldMap {B = B} f e xs = foldMap (dual (∘-id-monoid B)) (flip f) xs e

record RawFoldable {a} (F : Set a → Set a) : Set (lsuc a) where
  field
    foldMap : ∀ {A : Set a} (M : Monoid a a) → (A → Monoid.Carrier M) → F A → Monoid.Carrier M

  fold : (M : Monoid a a) → F (Monoid.Carrier M) → Monoid.Carrier M
  fold M = foldMap M id

  foldr : ∀ {A B : Set a} → (A → B → B) → B → F A → B
  foldr {A} {B} f e xs = foldMap (∘-id-monoid B) f xs e

  foldl : ∀ {A B : Set a} → (B → A → B) → B → F A → B
  foldl {A} {B} f e xs = foldMap (dual (∘-id-monoid B)) (flip f) xs e

fromFoldr : ∀ {a} {F : Set a → Set a} →
  (∀ {A B : Set a} → (A → B → B) → B → F A → B) → RawFoldable {a} F
fromFoldr foldr = record
  { foldMap = foldr-to-foldMap foldr
  }


text:
-- Andreas, 2017-06-16, issue #2604:
-- Symbolic anchors in generated HTML.

module Issue2604 where

test1 : Set₁  -- Symbolic anchor
test1 = bla
  where
  bla = Set   -- Position anchor

test2 : Set₁  -- Symbolic anchor
test2 = bla
  where
  bla = Set   -- Position anchor

test3 : Set₁  -- Symbolic anchor
test3 = bla
  module M where
  bla = Set  -- Symbolic anchor

module NamedModule where
  test4 : Set₁  -- Symbolic anchor
  test4 = M.bla

module _ where
  test5 : Set₁  -- Position anchor
  test5 = M.bla

-- Testing whether # in anchors confuses the browsers.
-- Not Firefox 54.0, at least (Andreas, 2017-06-20).
-- However, the Nu Html Checker complains (someone else, later).

# : Set₁
# = Set

#a : Set₁
#a = #

b# : Set₁
b# = #a

## : Set₁
## = b#

-- The href attribute values #A and #%41 are (correctly?) treated as
-- pointers to the same destination by Firefox 54.0. To point to %41
-- one should use #%2541.

A : Set₁
A = Set

%41 : Set₁
%41 = A

-- Ampersands may need to be encoded in some way. The blaze-html
-- library takes care of encoding id attribute values, and we manually
-- replace ampersands with %26 in the fragment parts of href attribute
-- values.

&amp : Set₁
&amp = Set

&lt : Set₁
&lt = &amp

-- Test of fixity declarations. The id attribute value for the
-- operator in the fixity declaration should be unique.

infix 0 _%42∀_

_%42∀_ : Set₁
_%42∀_ = Set

-- The following two variants of the character Ö should result in
-- distinct links.

Ö : Set₁
Ö = Set

Ö : Set₁
Ö = Ö


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

open import lib.Basics
open import lib.NConnected
open import lib.types.Bool
open import lib.types.FunctionSeq
open import lib.types.Pointed
open import lib.types.Suspension.Core
open import lib.types.TLevel

module lib.types.Suspension.Iterated where

Susp^ : ∀ {i} (n : ℕ) → Type i → Type i
Susp^ O X = X
Susp^ (S n) X = Susp (Susp^ n X)

Susp^-pt : ∀ {i} (n : ℕ) (A : Ptd i) → Susp^ n (de⊙ A)
Susp^-pt O A = pt A
Susp^-pt (S n) A = north

⊙Susp^ : ∀ {i} (n : ℕ) → Ptd i → Ptd i
⊙Susp^ n X = ptd (Susp^ n (de⊙ X)) (Susp^-pt n X)

abstract
  Susp^-conn : ∀ {i} (n : ℕ) {A : Type i} {m : ℕ₋₂}
    {{_ : is-connected m A}} → is-connected (⟨ n ⟩₋₂ +2+ m) (Susp^ n A)
  Susp^-conn O = ⟨⟩
  Susp^-conn (S n) = Susp-conn (Susp^-conn n)

  ⊙Susp^-conn' : ∀ {i} (n : ℕ) {A : Type i}
    {{_ : is-connected 0 A}} → is-connected ⟨ n ⟩ (Susp^ n A)
  ⊙Susp^-conn' O = ⟨⟩
  ⊙Susp^-conn' (S n) = Susp-conn (⊙Susp^-conn' n)

Susp^-fmap : ∀ {i j} (n : ℕ) {A : Type i} {B : Type j}
  → (A → B) → Susp^ n A → Susp^ n B
Susp^-fmap O f = f
Susp^-fmap (S n) f = Susp-fmap (Susp^-fmap n f)

⊙Susp^-fmap-pt : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  (f : X ⊙→ Y)
  → Susp^-fmap n (fst f) (pt (⊙Susp^ n X)) == pt (⊙Susp^ n Y)
⊙Susp^-fmap-pt O f = snd f
⊙Susp^-fmap-pt (S n) f = idp

⊙Susp^-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → ⊙Susp^ n X ⊙→ ⊙Susp^ n Y
⊙Susp^-fmap n f = Susp^-fmap n (fst f) , ⊙Susp^-fmap-pt n f

Susp^-fmap-idf : ∀ {i} (n : ℕ) (A : Type i)
  → Susp^-fmap n (idf A) == idf (Susp^ n A)
Susp^-fmap-idf O A = idp
Susp^-fmap-idf (S n) A = ↯ $
  Susp-fmap (Susp^-fmap n (idf A))
    =⟪ ap Susp-fmap (Susp^-fmap-idf n A) ⟫
  Susp-fmap (idf _)
    =⟪ λ= (Susp-fmap-idf _) ⟫
  idf (Susp^ (S n) A) ∎∎

transport-Susp^ : ∀ {i} {A B : Type i} (n : ℕ) (p : A == B)
  → transport (Susp^ n) p == Susp^-fmap n (coe p)
transport-Susp^ n idp = ! (Susp^-fmap-idf n _)

⊙Susp^-fmap-idf : ∀ {i} (n : ℕ) (X : Ptd i)
  → ⊙Susp^-fmap n (⊙idf X) ◃⊙idf =⊙∘ ⊙idf-seq
⊙Susp^-fmap-idf O X = =⊙∘-in idp
⊙Susp^-fmap-idf (S n) X =
  ⊙Susp^-fmap (S n) (⊙idf X) ◃⊙idf
    =⊙∘₁⟨ ap ⊙Susp-fmap (Susp^-fmap-idf n (de⊙ X)) ⟩
  ⊙Susp-fmap (idf _) ◃⊙idf
    =⊙∘⟨ ⊙Susp-fmap-idf (Susp^ n (de⊙ X)) ⟩
  ⊙idf-seq ∎⊙∘

⊙transport-⊙Susp^ : ∀ {i} {X Y : Ptd i} (n : ℕ) (p : X == Y)
  → ⊙transport (⊙Susp^ n) p == ⊙Susp^-fmap n (⊙coe p)
⊙transport-⊙Susp^ n p@idp = ! (=⊙∘-out (⊙Susp^-fmap-idf n _))

Susp^-fmap-cst : ∀ {i j} (n : ℕ) {A : Type i} {Y : Ptd j}
  → Susp^-fmap n {A = A} (λ _ → pt Y) == (λ _ → pt (⊙Susp^ n Y))
Susp^-fmap-cst O = idp
Susp^-fmap-cst (S n) {A} {Y} = ↯ $
  Susp-fmap (Susp^-fmap n {A = A} (λ _ → pt Y))
    =⟪ ap Susp-fmap (Susp^-fmap-cst n) ⟫
  Susp-fmap (λ _ → pt (⊙Susp^ n Y))
    =⟪ λ= (Susp-fmap-cst (pt (⊙Susp^ n Y))) ⟫
  (λ _ → north) ∎∎

⊙Susp^-fmap-cst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ⊙Susp^-fmap n (⊙cst {X = X} {Y = Y}) == ⊙cst
⊙Susp^-fmap-cst O = idp
⊙Susp^-fmap-cst (S n) = ap ⊙Susp-fmap (Susp^-fmap-cst n) ∙ ⊙Susp-fmap-cst

Susp^-fmap-∘ : ∀ {i j k} (n : ℕ) {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (f : A → B)
  → Susp^-fmap n (g ∘ f) == Susp^-fmap n g ∘ Susp^-fmap n f
Susp^-fmap-∘ O g f = idp
Susp^-fmap-∘ (S n) g f =
  Susp-fmap (Susp^-fmap n (g ∘ f))
    =⟨ ap Susp-fmap (Susp^-fmap-∘ n g f) ⟩
  Susp-fmap (Susp^-fmap n g ∘ Susp^-fmap n f)
    =⟨ λ= (Susp-fmap-∘ (Susp^-fmap n g) (Susp^-fmap n f)) ⟩
  Susp^-fmap (S n) g ∘ Susp^-fmap (S n) f =∎

⊙Susp^-fmap-∘ : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ⊙Susp^-fmap n (g ⊙∘ f) == ⊙Susp^-fmap n g ⊙∘ ⊙Susp^-fmap n f
⊙Susp^-fmap-∘ O g f = idp
⊙Susp^-fmap-∘ (S n) g f =
  ap ⊙Susp-fmap (Susp^-fmap-∘ n (fst g) (fst f))
  ∙ ⊙Susp-fmap-∘ (Susp^-fmap n (fst g)) (Susp^-fmap n (fst f))

⊙Susp^-fmap-seq : ∀ {i} (n : ℕ) {X : Ptd i} {Y : Ptd i}
  → X ⊙–→ Y
  → ⊙Susp^ n X ⊙–→ ⊙Susp^ n Y
⊙Susp^-fmap-seq n ⊙idf-seq = ⊙idf-seq
⊙Susp^-fmap-seq n (f ◃⊙∘ fs) = ⊙Susp^-fmap n f ◃⊙∘ ⊙Susp^-fmap-seq n fs

⊙Susp^-fmap-seq-∘ : ∀ {i} (n : ℕ) {X : Ptd i} {Y : Ptd i} (fs : X ⊙–→ Y)
  → ⊙Susp^-fmap n (⊙compose fs) ◃⊙idf =⊙∘ ⊙Susp^-fmap-seq n fs
⊙Susp^-fmap-seq-∘ n ⊙idf-seq = ⊙Susp^-fmap-idf n _
⊙Susp^-fmap-seq-∘ n (f ◃⊙∘ fs) = =⊙∘-in $
  ⊙Susp^-fmap n (f ⊙∘ ⊙compose fs)
    =⟨ ⊙Susp^-fmap-∘ n f (⊙compose fs) ⟩
  ⊙Susp^-fmap n f ⊙∘ ⊙Susp^-fmap n (⊙compose fs)
    =⟨ ap (⊙Susp^-fmap n f ⊙∘_) (=⊙∘-out (⊙Susp^-fmap-seq-∘ n fs)) ⟩
  ⊙Susp^-fmap n f ⊙∘ ⊙compose (⊙Susp^-fmap-seq n fs) =∎

⊙Susp^-fmap-seq-=⊙∘ : ∀ {i} (n : ℕ) {X : Ptd i} {Y : Ptd i} {fs gs : X ⊙–→ Y}
  → fs =⊙∘ gs
  → ⊙Susp^-fmap-seq n fs =⊙∘ ⊙Susp^-fmap-seq n gs
⊙Susp^-fmap-seq-=⊙∘ n {fs = fs} {gs = gs} p =
  ⊙Susp^-fmap-seq n fs
    =⊙∘⟨ !⊙∘ $ ⊙Susp^-fmap-seq-∘ n fs ⟩
  ⊙Susp^-fmap n (⊙compose fs) ◃⊙idf
    =⊙∘₁⟨ ap (⊙Susp^-fmap n) (=⊙∘-out p) ⟩
  ⊙Susp^-fmap n (⊙compose gs) ◃⊙idf
    =⊙∘⟨ ⊙Susp^-fmap-seq-∘ n gs ⟩
  ⊙Susp^-fmap-seq n gs ∎⊙∘

⊙Sphere : (n : ℕ) → Ptd₀
⊙Sphere n = ⊙Susp^ n ⊙Bool

Sphere : (n : ℕ) → Type₀
Sphere n = de⊙ (⊙Sphere n)

abstract
  instance
    Sphere-conn : ∀ (n : ℕ) → is-connected ⟨ n ⟩₋₁ (Sphere n)
    Sphere-conn 0 = inhab-conn true
    Sphere-conn (S n) = Susp-conn (Sphere-conn n)

-- favonia: [S¹] has its own elim rules in Circle.agda.
⊙S⁰ = ⊙Sphere 0
⊙S¹ = ⊙Sphere 1
⊙S² = ⊙Sphere 2
⊙S³ = ⊙Sphere 3
S⁰ = Sphere 0
S¹ = Sphere 1
S² = Sphere 2
S³ = Sphere 3

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
-- agda -c -isrc -i/usr/share/agda-stdlib/ src/Main.agda
module Main where

open import IO
open import Function
open import Coinduction
open import Data.String using (String; toList; fromList)
open import Example

-- main = interact $ unline . reverse . lines
main = run (♯ getContents >>= ♯_ ∘ eachline ( fromList ∘ rev ∘ toList) ) where

  open import Data.Maybe
  open import Data.Product
  open import Data.List using ([]; _∷_; [_])
  open import Data.Colist using (Colist; []; _∷_)
  open import Data.String using (Costring; _++_)
  open import Data.Unit using (⊤; tt)
  open import Category.Monad.Partiality

  takeLine : Costring → Maybe (String × ∞ Costring) ⊥
  takeLine [] = now nothing -- EOF
  takeLine xs = go "" xs where
    go : String → Costring → Maybe (String × ∞ Costring) ⊥
    go acc [] = now (just (acc , ♯ []))
    go acc (x ∷ xs) with fromList [ x ]
    go acc (_ ∷ xs) | "\n" = now (just (acc , xs))
    go acc (_ ∷ xs) | last = later (♯ go (acc ++ last) (♭ xs))

  takeLine' : Costring → (String × Costring) ⊥
  takeLine' xs = go "" xs where
    go : String → Costring → (String × Costring) ⊥
    go acc [] = now (acc , [])
    go acc (x ∷ xs) with fromList [ x ]
    go acc (x ∷ xs) | "\n" = now (acc , (♭ xs))
    go acc (x ∷ xs) | last = later (♯ go (acc ++ last) (♭ xs))

  eachline : (String → String) → Costring → IO ⊤
  eachline f = go ∘ takeLine where
    go : Maybe (String × ∞ Costring) ⊥ → IO ⊤
    go (now nothing) = return tt
    go (now (just (line , xs))) = ♯ putStrLn (f line) >> ♯ go (takeLine (♭ xs))
    go (later x) = ♯ return tt >> ♯ go (♭ x)

  eachline' : (String → String) → Costring → IO ⊤
  eachline' f = go ∘ takeLine' where
    go : (String × Costring) ⊥ → IO ⊤
    go (now (line , xs)) = ♯ putStrLn (f line) >> ♯ go (takeLine' xs)
    go (later x) = ♯ return tt >> ♯ go (♭ x)

max_stars_repo_name: notogawa/agda-haskell-example

max_issues_repo_name: notogawa/agda-haskell-example

max_forks_repo_name: notogawa/agda-haskell-example


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2020 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 Data.Empty
open import Data.Fin.Properties using (toℕ<n; toℕ-injective)
open import Data.Product
open import Data.Sum
open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Nat.Properties
open import Data.Nat.Induction
open import Data.List renaming (map to List-map)
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All

import Relation.Binary.PropositionalEquality as Eq
open import Relation.Binary.Definitions
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

open import Relation.Binary.PropositionalEquality renaming ( [_] to Reveal[_])
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
 using (_≅_; ≅-to-≡; ≡-to-≅; _≇_)
 renaming (cong to ≅-cong; refl to ≅-refl; cong₂ to ≅-cong₂)
open import Relation.Nullary
open import Relation.Binary.Core
open import Relation.Nullary.Negation using (contradiction; contraposition)
import Relation.Nullary using (¬_)
open import Function

-- This module defines the hop relation used by the original AAOSL due to Maniatis
-- and Baker, and proves various properties needed to establish it as a valid
-- DepRel, so that we can instantiate the asbtract model with it to demonstrate that
-- it is an instance of the class of AAOSLs for which we prove our properties.

module AAOSL.Hops where

 open import AAOSL.Lemmas
 open import Data.Nat.Even

 -- The level of an index is 0 for index 0,
 -- otherwise, it is one plus the number of times
 -- that two divides said index.
 --
 -- lvlOf must be marked terminating because in one branch
 -- we make recursive call on the quotient of the argument, which
 -- is not obviously smaller than that argument
 -- This is justified by proving that lvlOf is equal to lvlOfWF,
 -- which uses well-founded recursion
 {-# TERMINATING #-}
 lvlOf : ℕ → ℕ
 lvlOf 0 = 0
 lvlOf (suc n) with even? (suc n)
 ...| no  _ = 1
 ...| yes e = suc (lvlOf (quotient e))

 -- level of an index with well-founded recursion
 lvlOfWFHelp : (n : ℕ) → Acc _<_ n → ℕ
 lvlOfWFHelp 0 p = 0
 lvlOfWFHelp (suc n) (acc rs) with even? (suc n)
 ... | no _ = 1
 ... | yes (divides q eq) = suc (lvlOfWFHelp q (rs q (1+n=m*2⇒m<1+n q n eq)))

 lvlOfWF : ℕ → ℕ
 lvlOfWF n = lvlOfWFHelp n (<-wellFounded n)

 -- When looking at an index in the form 2^k * d, the level of
 -- said index is more easily defined.
 lvlOf' : ∀{n} → Pow2 n → ℕ
 lvlOf' zero          = zero
 lvlOf' (pos l _ _ _) = suc l

 -------------------------------------------
 -- Properties of lvlOf, lvlOfWF, and lvlOf'
 lvlOf≡lvlOfWFHelp : (n : ℕ) (p : Acc _<_ n) → lvlOf n ≡ lvlOfWFHelp n p
 lvlOf≡lvlOfWFHelp 0 p = refl
 lvlOf≡lvlOfWFHelp (suc n) (acc rs) with even? (suc n)
 ... | no _ = refl
 ... | yes (divides q eq) =
   cong suc (lvlOf≡lvlOfWFHelp q (rs q (1+n=m*2⇒m<1+n q n eq)))

 lvlOf≡lvlOfWF : (n : ℕ) → lvlOf n ≡ lvlOfWF n
 lvlOf≡lvlOfWF n = lvlOf≡lvlOfWFHelp n (<-wellFounded n)

 lvlOf≡lvlOf' : ∀ n → lvlOf n ≡ lvlOf' (to n)
 lvlOf≡lvlOf' n rewrite lvlOf≡lvlOfWF n = go n (<-wellFounded n)
   where
   go : (n : ℕ) (p : Acc _<_ n) → lvlOfWFHelp n p ≡ lvlOf' (to n)
   go 0 p = refl
   go (suc n) (acc rs) with even? (suc n)
   ... | no _ = refl
   ... | yes (divides q eq) with go q (rs q (1+n=m*2⇒m<1+n q n eq))
   ... | ih with to q
   ... | pos l d odd prf = cong suc ih

 lvl≥2-even : ∀ {n} → 2 ≤ lvlOf n → Even n
 lvl≥2-even {suc n} x
    with 2 ∣? (suc n)
 ...| yes prf = prf
 ...| no  prf = ⊥-elim ((≤⇒≯ x) (s≤s (s≤s z≤n)))

 lvlOfodd≡1 : ∀ n → Odd n → lvlOf n ≡ 1
 lvlOfodd≡1 0 nodd = ⊥-elim (nodd (divides zero refl))
 lvlOfodd≡1 (suc n) nodd
    with even? (suc n)
 ...| yes prf = ⊥-elim (nodd prf)
 ...| no  prf = refl

 -- We eventually need to 'undo' a level
 lvlOf-undo : ∀{j}(e : Even (suc j)) → suc (lvlOf (quotient e)) ≡ lvlOf (suc j)
 lvlOf-undo {j} e with even? (suc j)
 ...| no  abs = ⊥-elim (abs e)
 ...| yes prf rewrite even-irrelevant e prf = refl

 ∣-cmp : ∀{t u n} → (suc t * u) ∣ n → (d : suc t ∣ n) → u ∣ (quotient d)
 ∣-cmp {t} {u} {n} (divides q1 e1) (divides q2 e2)
   rewrite sym (*-assoc q1 (suc t) u)
         | *-comm q1 (suc t)
         | *-comm q2 (suc t)
         | *-assoc (suc t) q1 u
         = divides q1 (*-cancelˡ-≡ t (trans (sym e2) e1))

 ∣-0< : ∀{n t} → 0 < n → (d : suc t ∣ n) → 0 < quotient d
 ∣-0< hip (divides zero    e) = ⊥-elim (<⇒≢ hip (sym e))
 ∣-0< hip (divides (suc q) e) = s≤s z≤n

 lvlOf-mono : ∀{n} k → 0 < n → 2 ^ k ∣ n → k ≤ lvlOf n
 lvlOf-mono zero            hip prf = z≤n
 lvlOf-mono {suc n} (suc k) hip prf
   with even? (suc n)
 ...| no abs   = ⊥-elim (abs (divides (quotient prf * (2 ^ k))
                  (trans (_∣_.equality prf)
                  (trans (cong ((quotient prf) *_) (sym (*-comm (2 ^ k) 2)))
                         (sym (*-assoc (quotient prf) (2 ^ k) 2))))))
 ...| yes prf' = s≤s (lvlOf-mono {quotient prf'} k (∣-0< hip prf') (∣-cmp prf prf'))

 -- This property can be strenghtened to < if we ever need.
 lvlOf'-mono : ∀{k} d → 0 < d → k ≤ lvlOf' (to (2 ^ k * d))
 lvlOf'-mono {k} d 0<d
   with to d
 ...| pos {d} kk dd odd eq
        with (2 ^ (k + kk)) * dd ≟ (2 ^ k) * d
 ...|      no  xx = ⊥-elim (xx  ( trans (cong (_* dd) (^-distribˡ-+-* 2 k kk))
                                        (trans (*-assoc (2 ^ k) (2 ^ kk) dd)
                                               (cong (λ x → (2 ^ k) * x) (sym eq)))))
 ...|      yes xx
             with to-reduce {(2 ^ k) * d} {k + kk} {dd} (sym xx) odd
 ...|          xx1 = ≤-trans (≮⇒≥ (m+n≮m k kk))
                             (≤-trans (n≤1+n (k + kk)) -- TODO-1: easy to strengthen to <; omit this step
                                      (≤-reflexive (sym (cong lvlOf' xx1))))

 -- And a progress property about levels:
 -- These will be much easier to reason about in terms of lvlOf'
 -- as we can see in lvlOf-correct.
 lvlOf-correct : ∀{l j} → l < lvlOf j → 2 ^ l ≤ j
 lvlOf-correct {l} {j} prf
   rewrite lvlOf≡lvlOf' j
   with to j
 ...| zero              = ⊥-elim (1+n≢0 (n≤0⇒n≡0 prf))
 ...| pos l' d odd refl = 2^kd-mono (≤-unstep2 prf) (0<odd odd)

 -- lvlOf-prog states that if we have not reached 0, we landed somewhere
 -- where we can hop again at the same level.
 lvlOf-prog : ∀{l j} → 0 < j ∸ 2 ^ l → l < lvlOf j → l < lvlOf (j ∸ 2 ^ l)
 lvlOf-prog {l} {j} hip l<lvl
   rewrite lvlOf≡lvlOf' j | lvlOf≡lvlOf' (j ∸ 2 ^ l)
   with to j
 ...| zero              = ⊥-elim (1+n≰n (≤-trans l<lvl z≤n))
 ...| pos l₁ d₁ o₁ refl
   rewrite 2^ld-2l l₁ l d₁ (≤-unstep2 l<lvl)
      with l ≟ l₁
 ...| no  l≢l₁ rewrite to-2^kd l (odd-2^kd-1 (l₁ ∸ l) d₁
                                   (0<m-n (≤∧≢⇒< (≤-unstep2 l<lvl) l≢l₁))
                                   (0<odd o₁))
                     = ≤-refl
 ...| yes refl rewrite n∸n≡0 l₁ | +-comm d₁ 0
   with odd∸1-even o₁
 ...| divides q prf rewrite prf
                          | sym (*-assoc (2 ^ l₁) q 2)
                          | a*b*2-lemma (2 ^ l₁) q
                          = lvlOf'-mono {suc l₁} q (1≤m*n⇒0<n {m = 2 ^ suc l₁} hip)

 lvlOf-no-overshoot : ∀ j l → suc l < lvlOf j → 0 < j ∸ 2 ^ l
 lvlOf-no-overshoot j l hip
   rewrite lvlOf≡lvlOf' j with to j
 ...| zero           = ⊥-elim (1+n≰n (≤-trans (s≤s z≤n) hip))
 ...| pos k d o refl = 0<m-n {2 ^ k * d} {2 ^ l}
                         (<-≤-trans (2^-mono (≤-unstep2 hip))
                                    (2^kd-mono {k} {k} ≤-refl (0<odd o)))

 ---------------------------
 -- The AAOSL Structure --
 ---------------------------

 -------------------------------
 -- Hops

 -- Encoding our hops into a relation. A value of type 'H l j i'
 -- witnesses the existence of a hop from j to i at level l.
 data H : ℕ → ℕ → ℕ → Set where
   hz : ∀ x → H 0 (suc x) x
   hs : ∀ {l x y z}
      → H l x y
      → H l y z
      → suc l < lvlOf x
      → H (suc l) x z

 -----------------------------
 -- Hop's universal properties

 -- The universal property comes for free
 h-univ : ∀{l j i} → H l j i → i < j
 h-univ (hz x)      = s≤s ≤-refl
 h-univ (hs h h₁ _) = <-trans (h-univ h₁) (h-univ h)

 -- It is easy to prove there are no hops from zero
 h-from0-⊥ : ∀{l i} → H l 0 i → ⊥
 h-from0-⊥ (hs h h₁ _) = h-from0-⊥ h

 -- And it is easy to prove that i is a distance of 2 ^ l away
 -- from j.
 h-univ₂ : ∀{l i j} → H l j i → i ≡ j ∸ 2 ^ l
 h-univ₂ (hz x) = refl
 h-univ₂ (hs {l = l} {j} h₀ h₁ _)
   rewrite h-univ₂ h₀
         | h-univ₂ h₁
         | +-comm (2 ^ l) 0
         | sym (∸-+-assoc j (2 ^ l) (2 ^ l))
         = refl

 -- and vice versa.
 h-univ₁ : ∀{l i j} → H l j i → j ≡ i + 2 ^ l
 h-univ₁ (hz x) = sym (+-comm x 1)
 h-univ₁ (hs {l = l} {z = i} h₀ h₁ _)
   rewrite h-univ₁ h₀
         | h-univ₁ h₁
         | +-comm (2 ^ l) 0
         = +-assoc i (2 ^ l) (2 ^ l)

 --------------
 -- H and lvlOf

 -- A value of type H says something about the levels of their indices
 h-lvl-src : ∀{l j i} → H l j i → l < lvlOf j
 h-lvl-src (hz x)    with even? (suc x)
 ...| no  _ = s≤s z≤n
 ...| yes _ = s≤s z≤n
 h-lvl-src (hs h₀ h₁ prf) = prf

 h-lvl-tgt : ∀{l j i} → 0 < i → H l j i → l < lvlOf i
 h-lvl-tgt prf h rewrite h-univ₂ h = lvlOf-prog prf (h-lvl-src h)

 h-lvl-inj : ∀{l₁ l₂ j i} (h₁ : H l₁ j i)(h₂ : H l₂ j i) → l₁ ≡ l₂
 h-lvl-inj {i = i} h₁ h₂
   = 2^-injective (+-cancelˡ-≡ i (trans (sym (h-univ₁ h₁)) (h-univ₁ h₂)))

 -- TODO-1: document reasons for this pragma and justify it
 {-# TERMINATING #-}
 h-lvl-half : ∀{l j i y l₁} → H l j y → H l y i → H l₁ j i → lvlOf y ≡ suc l
 h-lvl-half w₀ w₁ (hz n) = ⊥-elim (1+n≰n (≤-<-trans (h-univ w₁) (h-univ w₀)))
 h-lvl-half {l}{j}{i}{y} w₀ w₁ (hs {l = l₁} {y = y₁} sh₀ sh₁ x)
   -- TODO-2: factor out a lemma to prove l₁ ≡ l and y₁ ≡ y (already exists?)
   with l₁ ≟ l
 ...| no imp
        with j ≟ i + (2 ^ l₁) + (2 ^ l₁) | j ≟ i + (2 ^ l) + (2 ^ l)
 ...|     no imp1 | _       rewrite h-univ₁ sh₁ = ⊥-elim (imp1 (h-univ₁ sh₀))
 ...|     yes _   | no imp1 rewrite h-univ₁ w₁  = ⊥-elim (imp1 (h-univ₁ w₀))
 ...|     yes j₁  | yes j₂
            with trans (sym j₂) j₁
 ...|         xx5 rewrite +-assoc i (2 ^ l)  (2 ^ l)
                        | +-assoc i (2 ^ l₁) (2 ^ l₁)
                with +-cancelˡ-≡ i xx5
 ...|             xx6 rewrite sym (+-identityʳ (2 ^ l))
                            | sym (+-identityʳ (2 ^ l₁))
                            | +-assoc (2 ^ l)  0 ((2 ^ l)  + 0)
                            | +-assoc (2 ^ l₁) 0 ((2 ^ l₁) + 0)
                            | *-comm 2 (2 ^ l)
                            | *-comm 2 (2 ^ l₁)
                              = ⊥-elim (imp (sym (2^-injective {l} {l₁} (
                                                    sym (*2-injective (2 ^ l) (2 ^ l₁) xx6)))))
 h-lvl-half {l = l}{j = j}{i = i}{y = y} w₀ w₁ (hs {l = l₁} {y = y₁} sh₀ sh₁ x)
    | yes xx1 rewrite xx1
        with y₁ ≟ y
 ...|     no  imp = ⊥-elim (imp (+-cancelʳ-≡ y₁ y (trans (sym (h-univ₁ sh₀)) (h-univ₁ w₀))))
 ...|     yes y₁≡y rewrite y₁≡y
            with w₀
 ...|         hs {l = l-1} ssh₀ ssh₁ xx rewrite sym xx1
              = h-lvl-half sh₀ sh₁ (hs sh₀ sh₁ x)
 ...|         hz y = lvlOfodd≡1 y (even-suc-odd y (lvl≥2-even {suc y} x))

 -- If a hop goes over an index, then the level of this index is strictly
 -- less than the level of the hop. The '≤' is there because
 -- l starts at zero.
 --
 -- For example, lvlOf 4 ≡ 3; the only hops that can go over 4 are
 -- those with l of 3 or higher. In fact, there is one at l ≡ 2
 -- from 4 to 0: H 2 4 0
 h-lvl-mid : ∀{l j i} → (k : ℕ) → H l j i → i < k → k < j → lvlOf k ≤ l
 h-lvl-mid k (hz x)       i<k k<j = ⊥-elim (n≮n k (<-≤-trans k<j i<k))
 h-lvl-mid {j = j} k (hs {l = l₀}{y = y} w₀ w₁ x) i<k k<j
    with <-cmp k y
 ...| tri< k<y k≢y k≯y = ≤-step (h-lvl-mid k w₁ i<k k<y)
 ...| tri> k≮y k≢y k>y = ≤-step (h-lvl-mid k w₀ k>y k<j)
 ...| tri≈ k≮y k≡y k≯y rewrite k≡y = ≤-reflexive (h-lvl-half w₀ w₁ (hs {l = l₀}{y = y} w₀ w₁ x))

 h-lvl-≤₁ : ∀{l₁ l₂ j i₁ i₂}
          → (h : H l₁ j i₁)(v : H l₂ j i₂)
          → i₂ < i₁
          → l₁ < l₂
 h-lvl-≤₁ {l₁} {l₂} {j} {i₁} {i₂} h v i₂<i₁ =
   let h-univ = h-univ₁ h
       v-univ = h-univ₁ v
       eqj    = trans (sym v-univ) h-univ
   in log-mono l₁ l₂ (n+p≡m+q∧n<m⇒q<p i₂<i₁ eqj)

 h-lvl-≤₂ : ∀{l₁ l₂ j₁ j₂ i}
          → (h : H l₁ j₁ i)(v : H l₂ j₂ i)
          → j₁ < j₂
          → l₁ < l₂
 h-lvl-≤₂ {l₁} {l₂} {j₁} {j₂} {i} h v j₂<j₁ =
    let h-univ = h-univ₁ h
        v-univ = h-univ₁ v
    in log-mono l₁ l₂ (+-cancelˡ-< i (subst (i + (2 ^ l₁) <_) v-univ (subst (_< j₂) h-univ j₂<j₁)))

 ------------------------------
 -- Correctness and Irrelevance

 h-correct : ∀ j l → l < lvlOf j → H l j (j ∸ 2 ^ l)
 h-correct (suc j) zero prf    = hz j
 h-correct (suc j) (suc l) prf
   with h-correct (suc j) l
 ...| ind with 2 ∣? (suc j)
 ...| no  _ = ⊥-elim (ss≰1 prf)
 ...| yes e with ind (≤-unstep prf)
 ...| res₀
   with h-correct (suc j ∸ 2 ^ l) l
          (lvlOf-prog {l} {suc j}
            (lvlOf-no-overshoot (suc j) l (subst (suc l <_ ) (lvlOf-undo e) prf))
            (subst (l <_) (lvlOf-undo e) (≤-unstep prf)))
 ...| res₁
   rewrite +-comm (2 ^ l) 0
         | ∸-+-assoc (suc j) (2 ^ l) (2 ^ l)
         = hs res₀ res₁ (subst (suc l <_) (lvlOf-undo e) prf)

 h-irrelevant : ∀{l i j}
   → (h₁ : H l j i)
   → (h₂ : H l j i)
   → h₁ ≡ h₂
 h-irrelevant (hz x)       (hz .x)       = refl
 h-irrelevant (hs {y = y} h₁ h₃ x) (hs {y = z} h₂ h₄ x₁)
   rewrite ≤-irrelevant x x₁
   with y ≟ z
 ...| no abs   = ⊥-elim (abs (trans (h-univ₂ h₁) (sym (h-univ₂ h₂))))
 ...| yes refl = cong₂ (λ P Q → hs P Q x₁) (h-irrelevant h₁ h₂) (h-irrelevant h₃ h₄)

 -------------------------------------------------------------------
 -- The non-overlapping property is stated in terms
 -- of subhops. The idea is that a hop is either separate
 -- from another one, or is entirely contained within the larger one.
 --
 -- Entirely contained comes from _⊆Hop_

 data _⊆Hop_ : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
             → H l₁ j₁ i₁
             → H l₂ j₂ i₂
             → Set where
   here  : ∀{l i j}(h : H l j i) → h ⊆Hop h
   left  : ∀{l₁ i₁ j₁ l₂ i₂ w j₂ }
         → (h  : H l₁ j₁ i₁)
         → (w₀ : H l₂ j₂ w)
         → (w₁ : H l₂ w i₂)
         → (p  : suc l₂ < lvlOf j₂)
         → h ⊆Hop w₀
         → h ⊆Hop (hs w₀ w₁ p)
   right : ∀{l₁ i₁ j₁ l₂ i₂ w j₂}
         → (h  : H l₁ j₁ i₁)
         → (w₀ : H l₂ j₂ w)
         → (w₁ : H l₂ w i₂)
         → (p  : suc l₂ < lvlOf j₂)
         → h ⊆Hop w₁
         → h ⊆Hop (hs w₀ w₁ p)

 ⊆Hop-refl : ∀{l₁ l₂ j i}
           → (h₁ : H l₁ j i)
           → (h₂ : H l₂ j i)
           → h₁ ⊆Hop h₂
 ⊆Hop-refl h₁ h₂ with h-lvl-inj h₁ h₂
 ...| refl rewrite h-irrelevant h₁ h₂ = here h₂

 ⊆Hop-univ : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
           → (h1 : H l₁ j₁ i₁)
           → (h2 : H l₂ j₂ i₂)
           → h1 ⊆Hop h2
           → i₂ ≤ i₁ × j₁ ≤ j₂ × l₁ ≤ l₂
 ⊆Hop-univ h1 .h1 (here .h1) = ≤-refl , ≤-refl , ≤-refl
 ⊆Hop-univ h1 (hs w₀ w₁ p) (left h1 w₀ w₁ q hip)
   with ⊆Hop-univ h1 w₀ hip
 ...| a , b , c = (≤-trans (<⇒≤ (h-univ w₁)) a) , b , ≤-step c
 ⊆Hop-univ h1 (hs w₀ w₁ p) (right h1 w₀ w₁ q hip)
   with ⊆Hop-univ h1 w₁ hip
 ...| a , b , c = a , ≤-trans b (<⇒≤ (h-univ w₀)) , ≤-step c

 ⊆Hop-univ₁ : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
            → (h1 : H l₁ j₁ i₁)
            → (h2 : H l₂ j₂ i₂)
            → h1 ⊆Hop h2
            → i₂ ≤ i₁
 ⊆Hop-univ₁ h1 h2 h1h2 = proj₁ (⊆Hop-univ h1 h2 h1h2)

 ⊆Hop-src-≤ : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
            → (h1 : H l₁ j₁ i₁)
            → (h2 : H l₂ j₂ i₂)
            → h1 ⊆Hop h2
            → j₁ ≤ j₂
 ⊆Hop-src-≤ h1 h2 h1h2 = (proj₁ ∘ proj₂) (⊆Hop-univ h1 h2 h1h2)

 -- If two hops are not strictly the same, then the level of
 -- the smaller hop is strictly smaller than the level of
 -- the bigger hop.
 --
 -- VERY IMPORTANT
 ⊆Hop-univ-lvl : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
               → (h₁ : H l₁ j₁ i₁)
               → (h₂ : H l₂ j₂ i₂)
               → h₁ ⊆Hop h₂
               → j₁ < j₂
               → l₁ < l₂
 ⊆Hop-univ-lvl {l₁}{i₁}{j₁}{l₂}{i₂}{j₂} h₁ h₂ h₁⊆Hoph₂ j₁<j₂
                = let r₁ : i₂ + (2 ^ l₁) ≤ i₁ + (2 ^ l₁)
                      r₁ = +-monoˡ-≤ (2 ^ l₁) (proj₁ (⊆Hop-univ h₁ h₂ h₁⊆Hoph₂))
                      r₂ : i₁ + (2 ^ l₁) < i₂ + (2 ^ l₂)
                      r₂ = subst₂ _<_ (h-univ₁ h₁) (h-univ₁ h₂) j₁<j₂
                  in log-mono l₁ l₂ ((+-cancelˡ-< i₂) (≤-<-trans r₁ r₂))

 hz-⊆ : ∀{l j i k}
      → (v : H l j i)
      → i ≤ k
      → k < j
      → hz k ⊆Hop v
 hz-⊆ (hz x)      i<k k<j
   rewrite ≤-antisym (≤-unstep2 k<j) i<k = here (hz x)
 hz-⊆ {k = k} (hs {y = y} v v₁ x) i<k k<j
   with k <? y
 ...| yes k<y = right (hz k) v v₁ x (hz-⊆ v₁ i<k k<y)
 ...| no  k≮y = left  (hz k) v v₁ x (hz-⊆ v (≮⇒≥ k≮y) k<j)

 ⊆Hop-inj₁ : ∀{l₁ l₂ j i₁ i₂}
           → (h : H l₁ j i₁)(v : H l₂ j i₂)
           → i₂ < i₁
           → h ⊆Hop v
 ⊆Hop-inj₁ {i₁ = i₁} h (hz x) prf
  = ⊥-elim (n≮n i₁ (<-≤-trans (h-univ h) prf))
 ⊆Hop-inj₁ {l} {j = j} {i₁ = i₁} h (hs {l = l₁} {y = y} v v₁ x) prf
   with y ≟ i₁
 ...| yes refl = left h v v₁ x (⊆Hop-refl h v)
 ...| no  y≢i₁
   with h-lvl-≤₁ h (hs v v₁ x) prf
 ...| sl≤sl₁
   with h-univ₂ h | h-univ₂ v
 ...| prf1 | prf2
    = let r : j ∸ (2 ^ l₁) ≤ j ∸ (2 ^ l)
          r = ∸-monoʳ-≤ {m = 2 ^ l} {2 ^ l₁} j (^-mono l l₁ (≤-unstep2 sl≤sl₁))
       in left h v v₁ x (⊆Hop-inj₁ h v (≤∧≢⇒< (subst₂ _≤_ (sym prf2) (sym prf1) r) y≢i₁))

 ⊆Hop-inj₂ : ∀{l₁ l₂ j₁ j₂ i}
           → (h : H l₁ j₁ i)(v : H l₂ j₂ i)
           → j₁ < j₂
           → h ⊆Hop v
 ⊆Hop-inj₂ h (hz x) prf
   = ⊥-elim (n≮n _ (<-≤-trans prf (h-univ h)))
 ⊆Hop-inj₂ {l} {j₁ = j₁} {i = i} h (hs {l = l₁} {y = y} v v₁ x) prf
   with y ≟ j₁
 ...| yes refl = right h v v₁ x (⊆Hop-refl h v₁)
 ...| no y≢j₁
   with h-lvl-≤₂ h (hs v v₁ x) prf
 ...| sl≤sl₁
   with h-univ₁ h | h-univ₁ v₁
 ...| prf1 | prf2
    = let r : i + 2 ^ l ≤ i + 2 ^ l₁
          r = +-monoʳ-≤ i (^-mono l l₁ (≤-unstep2 sl≤sl₁))
       in right h v v₁ x (⊆Hop-inj₂ h v₁ (≤∧≢⇒< (subst₂ _≤_ (sym prf1) (sym prf2) r) (y≢j₁ ∘ sym)))

 ⊆Hop-inj₃ : ∀{l₁ l₂ j₁ j₂ i₁ i₂}
           → (h : H l₁ j₁ i₁)(v : H l₂ j₂ i₂)
           → i₁ ≡ i₂ → j₁ ≡ j₂ → h ⊆Hop v
 ⊆Hop-inj₃ h v refl refl with h-lvl-inj h v
 ...| refl rewrite h-irrelevant h v = here v

 -- This datatype encodes all the possible hop situations. This makes is
 -- much easier to structure proofs talking about two hops.
 data HopStatus : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
                → H l₁ j₁ i₁
                → H l₂ j₂ i₂
                → Set where
   -- Same hop; we carry the proofs explicitly here to be able to control
   -- when to perform the rewrites.
   Same : ∀{l₁ i₁ j₁ l₂ i₂ j₂}(h₁ : H l₁ j₁ i₁)(h₂ : H l₂ j₂ i₂)
        → i₁ ≡ i₂
        → j₁ ≡ j₂
        → HopStatus h₁ h₂

   --     h₂           h₁
   -- ⌜⁻⁻⁻⁻⁻⁻⁻⌝    ⌜⁻⁻⁻⁻⁻⁻⁻⌝
   -- |       |    |       |
   -- i₂  <   j₂ ≤ i₁  <   j₁
   SepL : ∀{l₁ i₁ j₁ l₂ i₂ j₂}(h₁ : H l₁ j₁ i₁)(h₂ : H l₂ j₂ i₂)
        → j₂ ≤ i₁
        → HopStatus h₁ h₂

   --     h₁           h₂
   -- ⌜⁻⁻⁻⁻⁻⁻⁻⌝    ⌜⁻⁻⁻⁻⁻⁻⁻⌝
   -- |       |    |       |
   -- i₁  <   j₁ ≤ i₂  <   j₂
   SepR : ∀{l₁ i₁ j₁ l₂ i₂ j₂}(h₁ : H l₁ j₁ i₁)(h₂ : H l₂ j₂ i₂)
        → j₁ ≤ i₂
        → HopStatus h₁ h₂

   --             h₂
   --  ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
   --  ∣                      ∣
   --  ∣          h₁          ∣
   --  ∣      ⌜⁻⁻⁻⁻⁻⁻⁻⌝       |
   --  |      |       |       |
   --  i₂  ≤  i₁  ⋯   j₁  ≤   j₂
   SubL : ∀{l₁ i₁ j₁ l₂ i₂ j₂}(h₁ : H l₁ j₁ i₁)(h₂ : H l₂ j₂ i₂)
        → i₂ < i₁ ⊎ j₁ < j₂ -- makes sure hops differ!
        → h₁ ⊆Hop h₂
        → HopStatus h₁ h₂

   --             h₁
   --  ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
   --  ∣                      ∣
   --  ∣          h₂          ∣
   --  ∣      ⌜⁻⁻⁻⁻⁻⁻⁻⌝       |
   --  |      |       |       |
   --  i₁  ≤  i₂  ⋯   j₂  <   j₁
   SubR : ∀{l₁ i₁ j₁ l₂ i₂ j₂}(h₁ : H l₁ j₁ i₁)(h₂ : H l₂ j₂ i₂)
        → i₁ < i₂ ⊎ j₂ < j₁ -- makes sure hops differ
        → h₂ ⊆Hop h₁
        → HopStatus h₁ h₂

 -- Finally, we can prove our no-overlap property. As it turns out, it is
 -- just a special case of general non-overlapping, and therefore, it is
 -- defined as such.
 mutual
  -- Distinguish is used to understand the relation between two arbitrary hops.
  -- It is used to perform the induction step on arbitrary hops. Note how
  -- 'no-overlap' has a clause that impedes the hops from being equal.
  distinguish : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
               → (h₁ : H l₁ j₁ i₁)
               → (h₂ : H l₂ j₂ i₂)
               → HopStatus h₁ h₂
  distinguish {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h1 h2
    with <-cmp i₁ i₂
  ...| tri≈ i₁≮i₂ i₁≡i₂ i₂≮i₁
    with <-cmp j₁ j₂
  ...| tri≈ j₁≮j₂ j₁≡j₂ j₂≮j₁ = Same h1 h2 i₁≡i₂ j₁≡j₂
  ...| tri< j₁<j₂ j₁≢j₂ j₂≮j₁ rewrite i₁≡i₂ = SubL h1 h2 (inj₂ j₁<j₂) (⊆Hop-inj₂ h1 h2 j₁<j₂)
  ...| tri> j₁≮j₂ j₁≢j₂ j₂<j₁ rewrite i₁≡i₂ = SubR h1 h2 (inj₂ j₂<j₁) (⊆Hop-inj₂ h2 h1 j₂<j₁)
  distinguish {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h1 h2
     | tri< i₁<i₂ i₁≢i₂ i₂≮i₁
    with <-cmp j₁ j₂
  ...| tri≈ j₁≮j₂ j₁≡j₂ j₂≮j₁ rewrite j₁≡j₂ = SubR h1 h2 (inj₁ i₁<i₂) (⊆Hop-inj₁ h2 h1 i₁<i₂)
  ...| tri< j₁<j₂ j₁≢j₂ j₂≮j₁ with no-overlap h2 h1 i₁<i₂
  ...| inj₁ a = SepR h1 h2 a
  ...| inj₂ b = SubR h1 h2 (inj₁ i₁<i₂) b
  distinguish {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h1 h2
     | tri< i₁<i₂ i₁≢i₂ i₂≮i₁
     | tri> j₁≮j₂ j₁≢j₂ j₂<j₁ with no-overlap h2 h1 i₁<i₂
  ...| inj₁ a = SepR h1 h2 a
  ...| inj₂ b = SubR h1 h2 (inj₁ i₁<i₂) b
  distinguish {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h1 h2
     | tri> i₁≮i₂ i₁≢i₂ i₂<i₁
    with <-cmp j₁ j₂
  ...| tri≈ j₁≮j₂ j₁≡j₂ j₂≮j₁ rewrite j₁≡j₂ = SubL h1 h2 (inj₁ i₂<i₁) (⊆Hop-inj₁ h1 h2 i₂<i₁)
  ...| tri< j₁<j₂ j₁≢j₂ j₂≮j₁ with no-overlap h1 h2 i₂<i₁
  ...| inj₁ a = SepL h1 h2 a
  ...| inj₂ b = SubL h1 h2 (inj₁ i₂<i₁) b
  distinguish {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h1 h2
     | tri> i₁≮i₂ i₁≢i₂ i₂<i₁
     | tri> j₁≮j₂ j₁≢j₂ j₂<j₁ with no-overlap h1 h2 i₂<i₁
  ...| inj₁ a = SepL h1 h2 a
  ...| inj₂ b = SubL h1 h2 (inj₁ i₂<i₁) b

  no-overlap-< : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
               → (h₁ : H l₁ j₁ i₁)
               → (h₂ : H l₂ j₂ i₂)
               → i₂ < i₁
               → i₁ < j₂
               → j₁ ≤ j₂
  no-overlap-< h₁ h₂ prf hip with no-overlap h₁ h₂ prf
  ...| inj₁ imp = ⊥-elim (1+n≰n (≤-trans hip imp))
  ...| inj₂ res = ⊆Hop-src-≤ h₁ h₂ res

  -- TODO-1: rename to nocross for consistency with paper
  -- Non-overlapping is more general, as hops might be completely
  -- separate and then, naturally won't overlap.
  no-overlap : ∀{l₁ i₁ j₁ l₂ i₂ j₂}
              → (h₁ : H l₁ j₁ i₁)
              → (h₂ : H l₂ j₂ i₂)
              → i₂ < i₁ -- this ensures h₁ ≢ h₂.
              → (j₂ ≤ i₁) ⊎ (h₁ ⊆Hop h₂)

  no-overlap h  (hz x) prf = inj₁ prf
  no-overlap {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h₁ (hs {y = y} v₀ v₁ v-ok) hip
    with distinguish h₁ v₀
  ...| SepL _ _ prf      = inj₁ prf
  ...| SubL _ _ case prf = inj₂ (left h₁ v₀ v₁ v-ok prf)
  ...| Same _ _ p1 p2    = inj₂ (left h₁ v₀ v₁ v-ok (⊆Hop-inj₃ h₁ v₀ p1 p2))
  no-overlap {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h₁ (hs {y = y} v₀ v₁ v-ok) hip
     | SepR _ _ j₁≤y
    with distinguish h₁ v₁
  ...| SepL _ _ prf              = ⊥-elim (<⇒≱ (h-univ h₁) (≤-trans j₁≤y prf))
  ...| SepR _ _ prf              = ⊥-elim (n≮n i₂ (<-trans hip (<-≤-trans (h-univ h₁) prf)))
  ...| SubR _ _ (inj₁ i₁<i₂) prf = ⊥-elim (n≮n i₂ (<-trans hip i₁<i₂))
  ...| SubR _ _ (inj₂ y<j₁)  prf = ⊥-elim (n≮n j₁ (≤-<-trans j₁≤y y<j₁))
  ...| SubL _ _ case prf         = inj₂ (right h₁ v₀ v₁ v-ok prf)
  ...| Same _ _ p1 p2            = inj₂ (right h₁ v₀ v₁ v-ok (⊆Hop-inj₃ h₁ v₁ p1 p2))
  no-overlap {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h₁ (hs {y = y} v₀ v₁ v-ok) hip
     | SubR _ _ (inj₁ i₁<y)  v₀⊆h₁
    with distinguish h₁ v₁
  ...| SepL _ _ prf              = ⊥-elim (n≮n i₁ (<-≤-trans i₁<y prf))
  ...| SepR _ _ prf              = ⊥-elim (n≮n i₂ (<-≤-trans (<-trans hip (h-univ h₁)) prf))
  ...| SubR _ _ (inj₁ i₁<i₂) prf = ⊥-elim (n≮n i₂ (<-trans hip i₁<i₂))
  ...| SubR _ _ (inj₂ y<j₁)  prf = ⊥-elim (≤⇒≯ (no-overlap-< h₁ v₁ hip i₁<y) y<j₁)
  ...| SubL _ _ case prf         = inj₂ (right h₁ v₀ v₁ v-ok prf)
  ...| Same _ _ p1 p2            = inj₂ (right h₁ v₀ v₁ v-ok (⊆Hop-inj₃ h₁ v₁ p1 p2))
  no-overlap {l₁} {i₁} {j₁} {l₂} {i₂} {j₂} h₁ (hs {y = y} v₀ v₁ v-ok) hip
     -- Here is the nasty case. We have to argue why this is impossible
     -- WITHOUT resorting to 'nov h₁ (hs v₀ v₁ v-ok)', otherwise this would
     -- result in an infinite loop. Note how 'nov' doesn't pattern match
     -- on any argument.
     --
     -- Here's what this looks like:
     --
     --               (hs v₀ v₁ v-ok)
     --          ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
     --          |                   h₁  |
     --          |        ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁺⁻⁻⁻⁻⁻⁻⁻⌝
     --          |        ∣              |       ∣
     --          |   v₁   ∣          v₀  |       ∣
     --          ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁺⁻⁻⁻⁻⁻⁻⌜⁻⁻⁻⁻⁻⁻⁻⌝       |
     --          |        |      |       |       |
     --          i₂   <   i₁  ≤  y   ⋯   j₂  <   j₁
     --
     -- We can pattern match on i₁ ≟ y
     | SubR _ _ (inj₂ j₂<j₁) v₀⊆h₁
    with i₁ ≟ y
     -- And we quickly discover that if i≢y, we have a crossing between
     -- v₁ and h₁, and that's impossible.
  ...| no  i₁≢y = ⊥-elim (n≮n y (<-≤-trans (<-trans (h-univ v₀) j₂<j₁)
                                (no-overlap-< h₁ v₁ hip (≤∧≢⇒< (⊆Hop-univ₁ v₀ h₁ v₀⊆h₁) i₁≢y))))
     -- The hard part really is when i₁ ≡ y, here's how this looks like:
     --
     --            (hs v₀ v₁ v-ok)
     -- lvl l+1  ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
     --          |                |   h₁
     --          |        ⌜⁻⁻⁻⁻⁻⁻⁻⁺⁻⁻⁻⁻⁻⁻⁻⌝   lvl l₁
     --          |        ∣       |       ∣
     --          |   v₁   ∣   v₀  |       ∣
     -- lvl l    ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁺⁻⁻⁻⁻⁻⁻⁻⌝       |
     --          |        |       |       |
     --          i₂   <   i₁  ⋯   j₂  <   j₁
     --
     -- We must show that the composite hop (hs v₀ v₁ v-ok) is impossible to build
     -- to show that the crossing doesn't happen.
     --
     -- Hence, we MUST reason about the levels of the indices and eliminate 'v-ok',
     -- Which is possible with a bit of struggling about levels.
  ...| yes refl  with h-lvl-tgt (≤-trans (s≤s z≤n) hip) v₀
  ...| l≤lvli₁   with ⊆Hop-univ-lvl _ _ v₀⊆h₁ j₂<j₁
  ...| l<l₁      with h-lvl-mid i₁ (hs v₀ v₁ v-ok) hip (h-univ v₀)
  ...| lvli₁≤l+1 with h-lvl-tgt (≤-trans (s≤s z≤n) hip) h₁
  ...| l₁≤lvli₁  rewrite ≤-antisym lvli₁≤l+1 l≤lvli₁
     = ⊥-elim (n≮n _ (<-≤-trans l<l₁ (≤-unstep2 l₁≤lvli₁)))

max_stars_repo_name: cwjnkins/aaosl-agda

max_issues_repo_name: cwjnkins/aaosl-agda

max_forks_repo_name: cwjnkins/aaosl-agda


text:
{-# OPTIONS --cubical --no-import-sorts --postfix-projections #-}
module Cubical.Codata.M.Bisimilarity where

open import Cubical.Core.Everything
open import Cubical.Codata.M
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Foundations.Everything
open Helpers using (J')

-- Bisimilarity as a coinductive record type.
record _≈_ {X : Type₀} {C : IxCont X} {x : X} (a b : M C x) : Type₀ where
  coinductive
  constructor _,_
  field
    head≈ : a .head ≡ b .head
    tails≈ : ∀ y → (pa : C .snd x (a .head) y) (pb : C .snd x (b .head) y)
             → (\ i → C .snd x (head≈ i) y) [ pa ≡ pb ]
             → a .tails y pa ≈ b .tails y pb

open _≈_ public

module _ {X : Type₀} {C : IxCont X} where

  -- Here we show that `a ≡ b` and `a ≈ b` are equivalent.
  --
  -- A direct construction of an isomorphism, like we do for streams,
  -- would be complicated by the type dependencies between the fields
  -- of `M C x` and even more so between the fields of the bisimilarity relation itself.
  --
  -- Instead we rely on theorem 4.7.7 of the HoTT book (fiberwise equivalences) to show that `misib` is an equivalence.

  misib : {x : X} (a b : M C x) → a ≡ b → a ≈ b
  misib a b eq .head≈ i          = eq i .head
  misib a b eq .tails≈ y pa pb q = misib (a .tails y pa) (b .tails y pb) (\ i → eq i .tails y (q i))

  -- With `a` fixed, `misib` is a fiberwise transformation between (a ≡_) and (a ≈_).
  --
  -- We show that the induced map on the total spaces is an
  -- equivalence because it is a map of contractible types.
  --
  -- The domain is the HoTT singleton type, so contractible, while the
  -- codomain is shown to be contractible by `contr-T` below.

  T : ∀ {x} → M C x → Type _
  T a = Σ (M C _) \ b → a ≈ b

  private
    lemma : ∀ {A} (B : Type₀) (P : A ≡ B) (pa : P i0) (pb : P i1) (peq : PathP (\ i → P i) pa pb)
          → PathP (\ i → PathP (\ j → P j) (transp (\ k → P (~ k ∧ i)) (~ i) (peq i)) pb)
                  peq
                  (\ j → transp (\ k → P (~ k ∨ j)) j pb)
    lemma {A} = J' _ \ pa → J' _ \ { i j → transp (\ _ → A) (~ i ∨ j) pa }

  -- We predefine `u'` so that Agda will agree that `contr-T-fst` is productive.
  private
    module Tails x a φ (u : Partial φ (T {x} a)) y (p : C .snd x (hcomp (λ i .o → u o .snd .head≈ i) (a .head)) y) where
      q = transp (\ i → C .snd x (hfill (\ i o → u o .snd .head≈ i) (inS (a .head)) (~ i)) y) i0 p
      a' = a .tails y q
      u' : Partial φ (T a')
      u' (φ = i1) = u 1=1 .fst .tails y p
                  , u 1=1 .snd .tails≈ y q p \ j → transp (\ i → C .snd x (u 1=1 .snd .head≈ (~ i ∨ j)) y) j p

  contr-T-fst : ∀ x a φ → Partial φ (T {x} a) → M C x
  contr-T-fst x a φ u .head      = hcomp (\ i o → u o .snd .head≈ i) (a .head)
  contr-T-fst x a φ u .tails y p = contr-T-fst y a' φ u'
    where
      open Tails x a φ u y p

  -- `contr-T-snd` is productive as the corecursive call appears as
  -- the main argument of transport, which is guardedness-preserving.
  {-# TERMINATING #-}
  contr-T-snd : ∀ x a φ → (u : Partial φ (T {x} a)) → a ≈ contr-T-fst x a φ u
  contr-T-snd x a φ u .head≈ i = hfill (λ { i (φ = i1) → u 1=1 .snd .head≈ i }) (inS (a .head)) i
  contr-T-snd x a φ u .tails≈ y pa pb peq =
    let r = contr-T-snd y (a .tails y pa) φ (\ { (φ = i1) → u 1=1 .fst .tails y pb , u 1=1 .snd .tails≈ y pa pb peq }) in
      transport (\ i → a .tails y pa
                ≈ contr-T-fst y (a .tails y (sym (fromPathP (\ i → peq (~ i))) i)) φ
                  (\ { (φ = i1) → u 1=1 .fst .tails y pb , u 1=1 .snd .tails≈ y
                                  ((fromPathP (\ i → peq (~ i))) (~ i)) pb
                                  \ j → lemma _ (λ h → C .snd x (u _ .snd .head≈ h) y) pa pb peq i j })) r

  contr-T : ∀ x a φ → Partial φ (T {x} a) → T a
  contr-T x a φ u .fst = contr-T-fst x a φ u
  contr-T x a φ u .snd = contr-T-snd x a φ u

  contr-T-φ-fst : ∀ x a → (u : Partial i1 (T {x} a)) → contr-T x a i1 u .fst ≡ u 1=1 .fst
  contr-T-φ-fst x a u i .head = u 1=1 .fst .head
  contr-T-φ-fst x a u i .tails y p
   = let
        q = (transp (\ i → C .snd x (hfill (\ i o → u o .snd .head≈ i) (inS (a .head)) (~ i)) y) i0 p)
      in contr-T-φ-fst y (a .tails y q)
                       (\ o → u o .fst .tails y p
                            , u o .snd .tails≈ y q p \ j → transp (\ i → C .snd x (u 1=1 .snd .head≈ (~ i ∨ j)) y) j p)
                       i

  -- `contr-T-φ-snd` is productive as the corecursive call appears as
  -- the main argument of transport, which is guardedness-preserving (even for paths of a coinductive type).
  {-# TERMINATING #-}
  contr-T-φ-snd : ∀ x a → (u : Partial i1 (T {x} a)) → (\ i → a ≈ contr-T-φ-fst x a u i) [ contr-T x a i1 u .snd ≡ u 1=1 .snd ]
  contr-T-φ-snd x a u i .head≈ = u _ .snd .head≈
  contr-T-φ-snd x a u i .tails≈ y pa pb peq = let
    eqh = u 1=1 .snd .head≈
    r = contr-T-φ-snd y (a .tails y pa) (\ o → u o .fst .tails y pb , u 1=1 .snd .tails≈ y pa pb peq)
    F : I → Type _
    F k = a .tails y pa
        ≈ contr-T-fst y
            (a .tails y (transp (λ j → C .snd x (eqh (k ∧ ~ j)) y) (~ k) (peq k)))
            i1
            (λ _ → u _ .fst .tails y pb
                 , u _ .snd .tails≈ y
                       (transp (λ j → C .snd x (eqh (k ∧ ~ j)) y) (~ k) (peq k))
                       pb
                       (λ j → lemma (C .snd x (u 1=1 .fst .head) y) (λ h → C .snd x (eqh h) y) pa pb peq k j)
             )
    u0 = contr-T-snd y (a .tails y pa) i1 (λ o → u o .fst .tails y pb , u o .snd .tails≈ y pa pb peq)
   in transport
         (λ l → PathP
           (λ z → a .tails y pa
                ≈ contr-T-φ-fst y
                   (a .tails y (transp (λ k → C .snd x (u 1=1 .snd .head≈ (~ k ∧ l)) y) (~ l) (peq l)))
                   (λ _ → u _ .fst .tails y pb
                        , u _ .snd .tails≈ y (transp (λ k → C .snd x (u _ .snd .head≈ (~ k ∧ l)) y) (~ l) (peq l)) pb
                               \ j → lemma (C .snd x (u 1=1 .fst .head) y) (λ h → C .snd x (eqh h) y) pa pb peq l j)
                   z)
           (transpFill {A = F i0} i0 (\ i → inS (F i)) u0 l)
           (u _ .snd .tails≈ y pa pb peq))
         r
         i

  contr-T-φ : ∀ x a → (u : Partial i1 (T {x} a)) → contr-T x a i1 u ≡ u 1=1
  contr-T-φ x a u i .fst = contr-T-φ-fst x a u i
  contr-T-φ x a u i .snd = contr-T-φ-snd x a u i

  contr-T' : ∀ {x} a → isContr (T {x} a)
  contr-T' a = isContrPartial→isContr (contr-T _ a) \ u → sym (contr-T-φ _ a (\ _ → u))

  bisimEquiv : ∀ {x} {a b : M C x} → isEquiv (misib a b)
  bisimEquiv = isContrToUniv _≈_ (misib _ _) contr-T'

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:
{-

Half adjoint equivalences ([HAEquiv])

- Iso to HAEquiv ([iso→HAEquiv])
- Equiv to HAEquiv ([equiv→HAEquiv])
- Cong is an equivalence ([congEquiv])

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

record isHAEquiv {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) : Type (ℓ-max ℓ ℓ') where
  field
    g : B → A
    linv : ∀ a → g (f a) ≡ a
    rinv : ∀ b → f (g b) ≡ b
    com : ∀ a → cong f (linv a) ≡ rinv (f a)

  -- from redtt's ha-equiv/symm
  com-op : ∀ b → cong g (rinv b) ≡ linv (g b)
  com-op b j i = hcomp (λ k → λ { (i = i0) → linv (g b) (j ∧ (~ k))
                                ; (j = i0) → g (rinv b i)
                                ; (j = i1) → linv (g b) (i ∨ (~ k))
                                ; (i = i1) → g b })
                       (cap1 j i)

    where cap0 : Square {- (j = i0) -} (λ i → f (g (rinv b i)))
                        {- (j = i1) -} (λ i → rinv b i)
                        {- (i = i0) -} (λ j → f (linv (g b) j))
                        {- (i = i1) -} (λ j → rinv b j)

          cap0 j i = hcomp (λ k → λ { (i = i0) → com (g b) (~ k) j
                                    ; (j = i0) → f (g (rinv b i))
                                    ; (j = i1) → rinv b i
                                    ; (i = i1) → rinv b j })
                           (rinv (rinv b i) j)

          filler : I → I → A
          filler j i = hfill (λ k → λ { (i = i0) → g (rinv b k)
                                      ; (i = i1) → g b })
                             (inS (linv (g b) i)) j

          cap1 : Square {- (j = i0) -} (λ i → g (rinv b i))
                        {- (j = i1) -} (λ i → g b)
                        {- (i = i0) -} (λ j → linv (g b) j)
                        {- (i = i1) -} (λ j → g b)

          cap1 j i = hcomp (λ k → λ { (i = i0) → linv (linv (g b) j) k
                                    ; (j = i0) → linv (g (rinv b i)) k
                                    ; (j = i1) → filler i k
                                    ; (i = i1) → filler j k })
                           (g (cap0 j i))

  isHAEquiv→Iso : Iso A B
  Iso.fun isHAEquiv→Iso = f
  Iso.inv isHAEquiv→Iso = g
  Iso.rightInv isHAEquiv→Iso = rinv
  Iso.leftInv isHAEquiv→Iso = linv

  isHAEquiv→isEquiv : isEquiv f
  isHAEquiv→isEquiv .equiv-proof y = (g y , rinv y) , isCenter where
    isCenter : ∀ xp → (g y , rinv y) ≡ xp
    isCenter (x , p) i = gy≡x i , ry≡p i where
      gy≡x : g y ≡ x
      gy≡x = sym (cong g p) ∙∙ refl ∙∙ linv x

      lem0 : Square (cong f (linv x)) p (cong f (linv x)) p
      lem0 i j = invSides-filler p (sym (cong f (linv x))) (~ i) j

      ry≡p : Square (rinv y) p (cong f gy≡x) refl
      ry≡p i j = hcomp (λ k → λ { (i = i0) → cong rinv p k j
                                ; (i = i1) → lem0 k j
                                ; (j = i0) → f (doubleCompPath-filler (sym (cong g p)) refl (linv x) k i)
                                ; (j = i1) → p k })
                       (com x (~ i) j)

open isHAEquiv using (isHAEquiv→Iso; isHAEquiv→isEquiv) public

HAEquiv : (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
HAEquiv A B = Σ[ f ∈ (A → B) ] isHAEquiv f

-- vogt's lemma (https://ncatlab.org/nlab/show/homotopy+equivalence#vogts_lemma)
iso→HAEquiv : Iso A B → HAEquiv A B
iso→HAEquiv e = f , isHAEquivf
  where
    f = Iso.fun e
    g = Iso.inv e
    ε = Iso.rightInv e
    η = Iso.leftInv e

    Hfa≡fHa : (f : A → A) → (H : ∀ a → f a ≡ a) → ∀ a → H (f a) ≡ cong f (H a)
    Hfa≡fHa f H = J (λ f p → ∀ a → funExt⁻ (sym p) (f a) ≡ cong f (funExt⁻ (sym p) a))
                    (λ a → refl)
                    (sym (funExt H))

    isHAEquivf : isHAEquiv f
    isHAEquiv.g isHAEquivf         = g
    isHAEquiv.linv isHAEquivf       = η
    isHAEquiv.rinv isHAEquivf b i   =
      hcomp (λ j → λ { (i = i0) → ε (f (g b)) j
                     ; (i = i1) → ε b j })
            (f (η (g b) i))
    isHAEquiv.com isHAEquivf a i j =
      hcomp (λ k → λ { (i = i0) → ε (f (η a j)) k
                     ; (j = i0) → ε (f (g (f a))) k
                     ; (j = i1) → ε (f a) k})
            (f (Hfa≡fHa (λ x → g (f x)) η a (~ i) j))

equiv→HAEquiv : A ≃ B → HAEquiv A B
equiv→HAEquiv e = e .fst , λ where
  .isHAEquiv.g → invIsEq (snd e)
  .isHAEquiv.linv → retIsEq (snd e)
  .isHAEquiv.rinv → secIsEq (snd e)
  .isHAEquiv.com a → flipSquare (slideSquare (commSqIsEq (snd e) a))

congIso : {x y : A} (e : Iso A B) → Iso (x ≡ y) (Iso.fun e x ≡ Iso.fun e y)
congIso {x = x} {y} e = goal
  where
  open isHAEquiv (iso→HAEquiv e .snd)
  open Iso

  goal : Iso (x ≡ y) (Iso.fun e x ≡ Iso.fun e y)
  fun goal   = cong (iso→HAEquiv e .fst)
  inv goal p = sym (linv x) ∙∙ cong g p ∙∙ linv y
  rightInv goal p i j =
    hcomp (λ k → λ { (i = i0) → iso→HAEquiv e .fst
                                  (doubleCompPath-filler (sym (linv x)) (cong g p) (linv y) k j)
                   ; (i = i1) → rinv (p j) k
                   ; (j = i0) → com x i k
                   ; (j = i1) → com y i k })
          (iso→HAEquiv e .fst (g (p j)))
  leftInv goal p i j =
    hcomp (λ k → λ { (i = i1) → p j
                   ; (j = i0) → Iso.leftInv e x (i ∨ k)
                   ; (j = i1) → Iso.leftInv e y (i ∨ k) })
          (Iso.leftInv e (p j) i)

invCongFunct : {x : A} (e : Iso A B) (p : Iso.fun e x ≡ Iso.fun e x) (q : Iso.fun e x ≡ Iso.fun e x)
             → Iso.inv (congIso e) (p ∙ q) ≡ Iso.inv (congIso e) p ∙ Iso.inv (congIso e) q
invCongFunct {x = x} e p q = helper (Iso.inv e) _ _ _
  where
  helper : {x : A} {y : B} (f : A → B) (r : f x ≡ y) (p q : x ≡ x)
         → (sym r ∙∙ cong f (p ∙ q) ∙∙ r) ≡ (sym r ∙∙ cong f p ∙∙ r) ∙ (sym r ∙∙ cong f q ∙∙ r)
  helper {x = x} f =
    J (λ y r → (p q : x ≡ x)
    → (sym r ∙∙ cong f (p ∙ q) ∙∙ r) ≡ (sym r ∙∙ cong f p ∙∙ r) ∙ (sym r ∙∙ cong f q ∙∙ r))
      λ p q → (λ i → rUnit (congFunct f p q i) (~ i))
             ∙ λ i → rUnit (cong f p) i ∙ rUnit (cong f q) i

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical