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

-- Proof relevant separation algebras
module Relation.Ternary.Separation where

open import Function
open import Level

open import Data.Unit using (tt; ⊤)
open import Data.Product hiding (map)
open import Data.List.Relation.Ternary.Interleaving.Propositional hiding (map)
open import Data.List.Relation.Binary.Equality.Propositional

open import Relation.Unary hiding (Empty)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import Algebra
open import Algebra.Structures using (IsMonoid)
open import Algebra.FunctionProperties.Core

∥_∥ : ∀ {ℓ a} {A : Set a} {P : Pred A ℓ} {Φ} → P Φ → A
∥_∥ {Φ = Φ} _ = Φ

Exactly : ∀ {a} {A : Set a} → A → Pred A a
Exactly x y = y ≡ x

module _ where
  open import Data.List

  Just : ∀ {a} {A : Set a} → A → Pred (List A) _
  Just t = Exactly [ t ]

record RawSep {a} (Carrier : Set a) : Set (suc a) where

  SPred : (ℓ : Level) → Set _
  SPred ℓ = Pred Carrier ℓ

  field
    _⊎_≣_ : (Φ₁ Φ₂ : Carrier) → SPred a

  -- we can see the three point relation as a predicate on the carrier
  _⊎_ = _⊎_≣_

  -- buy one, get a preorder for free
  _≤_ : Rel Carrier _
  Φ₁ ≤ Φ = ∃ λ Φ₂ → Φ₁ ⊎ Φ₂ ≣ Φ

  -- remainder
  rem : ∀ {x y} → x ≤ y → Carrier
  rem (z , _) = z

  -- separating conjunction
  infixr 10 _×⟨_⟩_
  record Conj {p q} (P : SPred p) (Q : ∀ {Φ} → P Φ → SPred q) Φ : Set (p ⊔ q ⊔ a) where
    inductive
    constructor _×⟨_⟩_
    field
      {Φₗ Φᵣ} : Carrier

      px  : P Φₗ
      sep : Φₗ ⊎ Φᵣ ≣ Φ
      qx  : Q px Φᵣ

  infixr 9 ∃[_]✴_
  ∃[_]✴_ = Conj

  infixr 9 _✴_
  _✴_ : ∀ {p q} → SPred p → SPred q → SPred (p ⊔ q ⊔ a)
  P ✴ Q = ∃[ P ]✴ const Q

  -- | Separating implication / magic is what you wand

  infixr 8 _─✴[_]_
  record _─✴[_]_ {b p q} {A : Set b} (P : Pred A p) (j : A → Carrier) (Q : SPred q) (Φᵢ : Carrier) : Set (p ⊔ q ⊔ a ⊔ b) where
    constructor wand
    field
      app : ∀ {Φₚ} → P Φₚ → ∀ {Φ} → Φᵢ ⊎ j Φₚ ≣ Φ → Q Φ

  open _─✴[_]_ public

  infixr 8 _─✴_
  _─✴_ : ∀ {p q} (P : SPred p) (Q : SPred q) → SPred (p ⊔ q ⊔ a)
  _─✴_ = _─✴[ id ]_

  _$⟨_⟩_ : ∀ {p q Φ₁ Φ₂ Φ} {P : SPred p} {Q : SPred q} →
           (P ─✴ Q) Φ₁ → Φ₁ ⊎ Φ₂ ≣ Φ → P Φ₂ → Q Φ
  f $⟨ σ ⟩ px = app f px σ

  -- | The update modality

  -- the naked version, which doesn't coop well with inference:
  ⤇' : ∀ {p} (P : SPred p) → SPred (a ⊔ p)
  ⤇' P Φᵢ = ∀ {Φⱼ Φₖ} → Φᵢ ⊎ Φⱼ ≣ Φₖ → ∃₂ λ Φₗ Φ → Φₗ ⊎ Φⱼ ≣ Φ × P Φₗ
  -- Φᵢ is what we own, Φⱼ is an arbitrary frame.
  -- We may update Φᵢ as long as we do not disturb the framing

  -- wrapped
  record ⤇ {p} (P : SPred p) Φᵢ : Set (a ⊔ p) where
    constructor local
    field
      update : ⤇' P Φᵢ

  open ⤇ public

  infixr 8 _==✴_
  _==✴_ : ∀ {p q} → (P : SPred p) (Q : SPred q) → SPred (p ⊔ q ⊔ a)
  P ==✴ Q = P ─✴ (⤇ Q)

record IsSep {ℓ₁} {A} (s : RawSep {ℓ₁} A) : Set ℓ₁ where
  open RawSep s

  field
    ⊎-comm  : ∀ {Φ₁ Φ₂}        → ∀[ Φ₁ ⊎ Φ₂ ⇒ Φ₂ ⊎ Φ₁ ]
    ⊎-assoc : ∀ {a b ab c abc} → a ⊎ b ≣ ab → ab ⊎ c ≣ abc →
                                 ∃ λ bc → a ⊎ bc ≣ abc × b ⊎ c ≣ bc

  ⊎-unassoc : ∀ {b c bc a abc} → a ⊎ bc ≣ abc → b ⊎ c ≣ bc →
                                 ∃ λ ab → a ⊎ b ≣ ab × ab ⊎ c ≣ abc
  ⊎-unassoc σ₁ σ₂ =
    let _ , σ₃ , σ₄ = ⊎-assoc (⊎-comm σ₂) (⊎-comm σ₁)
    in -, ⊎-comm σ₄ , ⊎-comm σ₃

  variable
    Φ₁ Φ₂ Φ₃ Φ : A

  module _ where
    resplit : ∀ {a b c d ab cd abcd} →
              a ⊎ b ≣ ab → c ⊎ d ≣ cd → ab ⊎ cd ≣ abcd →
              ∃₂ λ ac bd → a ⊎ c ≣ ac × b ⊎ d ≣ bd × ac  ⊎ bd  ≣ abcd
    resplit σ₁ σ₂ σ     with ⊎-assoc σ₁ σ
    ... | bcd , σ₃ , σ₄ with ⊎-unassoc σ₄ (⊎-comm σ₂)
    ... | bd  , σ₅ , σ₆ with ⊎-unassoc σ₃ σ₆
    ... | abd , σ₇ , σ₈ with ⊎-unassoc (⊎-comm σ₈) σ₇
    ... | ac  , τ  , τ' = -, -, ⊎-comm τ , σ₅ , τ'

  -- pairs commute
  module _ {p q} {P : SPred p} {Q : SPred q} where
    ✴-swap : ∀[ (P ✴ Q) ⇒ (Q ✴ P) ]
    ✴-swap (px ×⟨ σ ⟩ qx) = qx ×⟨ ⊎-comm σ ⟩ px

  -- pairs rotate and reassociate
  module _ {p q r} {P : SPred p} {Q : SPred q} {R : SPred r} where
    ✴-assocₗ : ∀[ P ✴ (Q ✴ R) ⇒ (P ✴ Q) ✴ R ]
    ✴-assocₗ (p ×⟨ σ₁ ⟩ (q ×⟨ σ₂ ⟩ r)) =
      let _ , σ₃ , σ₄ = ⊎-assoc (⊎-comm σ₂) (⊎-comm σ₁) in
      (p ×⟨ ⊎-comm σ₄ ⟩ q) ×⟨ ⊎-comm σ₃ ⟩ r

    ✴-assocᵣ : ∀[ (P ✴ Q) ✴ R ⇒ P ✴ (Q ✴ R) ]
    ✴-assocᵣ ((p ×⟨ σ₁ ⟩ q) ×⟨ σ₂ ⟩ r) =
      let _ , σ₃ , σ₄ = ⊎-assoc σ₁ σ₂ in
      p ×⟨ σ₃ ⟩ q ×⟨ σ₄ ⟩ r

    ✴-rotateᵣ : ∀[ P ✴ (Q ✴ R) ⇒ R ✴ P ✴ Q ]
    ✴-rotateᵣ (p ×⟨ σ₁ ⟩ (q ×⟨ σ₂ ⟩ r)) =
      let _ , σ₃ , σ₄ = ⊎-assoc (⊎-comm σ₂) (⊎-comm σ₁) in
      r ×⟨ σ₃ ⟩ p ×⟨ ⊎-comm σ₄ ⟩ q

    ✴-rotateₗ : ∀[ P ✴ (Q ✴ R) ⇒ Q ✴ R ✴ P ]
    ✴-rotateₗ (p ×⟨ σ₁ ⟩ (q ×⟨ σ₂ ⟩ r)) =
      let _ , σ₃ , σ₄ = ⊎-assoc σ₂ (⊎-comm σ₁) in
      q ×⟨ σ₃ ⟩ r ×⟨ σ₄ ⟩ p

  module _ {p q} {P : SPred p} {Q : SPred q} where
    apply : ∀[ (P ─✴ Q) ✴ P ⇒ Q ]
    apply (px ×⟨ sep ⟩ qx) =  app px qx sep

  -- mapping
  module _ {p q p' q'}
    {P : SPred p} {Q : SPred q} {P' : SPred p'} {Q' : SPred q'} where

    ⟨_⟨✴⟩_⟩ : ∀[ P ⇒ P' ] → ∀[ Q ⇒ Q' ] → ∀[ P ✴ Q ⇒ P' ✴ Q' ]
    ⟨_⟨✴⟩_⟩ f g (px ×⟨ sep ⟩ qx) = (f px) ×⟨ sep ⟩ (g qx)

    both : ∀[ (P ─✴ P') ✴ (Q ─✴ Q') ⇒ P ✴ Q ─✴ P' ✴ Q' ]
    app (both (f ×⟨ σ₁ ⟩ g)) (px ×⟨ σ₂ ⟩ qx) σ₃ with resplit σ₁ σ₂ σ₃
    ... | _ , _ , σ₄ , σ₅ , σ₆ = apply (f ×⟨ σ₄ ⟩ px) ×⟨ σ₆ ⟩ apply (g ×⟨ σ₅ ⟩ qx)

  module _ {p q r} {P : SPred p} {Q : SPred q} {R : SPred r} where

    ✴-curry : ∀[ (P ─✴ (Q ─✴ R)) ⇒ (P ✴ Q) ─✴ R ]
    app (✴-curry f) (p ×⟨ σ₁ ⟩ q) σ₂ =
      let _ , σ₃ , σ₄ = ⊎-unassoc σ₂ σ₁ in app (app f p σ₃) q σ₄

    intro : ∀[ (P ✴ Q) ⇒ R ] → ∀[ P ⇒ (Q ─✴ R) ]
    app (intro f px) qx s = f (px ×⟨ s ⟩ qx)

    com : ∀[ (P ─✴ Q) ✴ (Q ─✴ R) ⇒ (P ─✴ R) ]
    app (com (f ×⟨ s ⟩ g)) px s' = let _ , eq₁ , eq₂ = ⊎-assoc (⊎-comm s) s' in app g (app f px eq₂) eq₁

    ✴-uncurry : ∀[ (P ✴ Q ─✴ R) ⇒ P ─✴ (Q ─✴ R) ]
    app (app (✴-uncurry f) p σ₁) q σ₂ = let _ , σ₃ , σ₄ = ⊎-assoc σ₁ σ₂ in app f (p ×⟨ σ₄ ⟩ q) σ₃

  module _ where

    ≤-trans : Φ₁ ≤ Φ₂ → Φ₂ ≤ Φ₃ → Φ₁ ≤ Φ₃
    ≤-trans (τ₁ , Φ₁⊎τ₁=Φ₂) (τ₂ , Φ₂⊎τ₂=Φ₃) =
      let τ₃ , p , q = ⊎-assoc Φ₁⊎τ₁=Φ₂ Φ₂⊎τ₂=Φ₃ in τ₃ , p

  module _ where
    -- disjointness
    _◆_ : _ → _ → SPred _
    Φₗ ◆ Φᵣ = Exactly Φₗ ✴ Exactly Φᵣ

record IsUnitalSep {c} {C : Set c} (sep : RawSep C) un : Set (suc c) where
  field
    overlap {{ isSep }}  : IsSep sep

  open RawSep sep

  ε = un

  field
    ⊎-idˡ    : ∀ {Φ} → ε ⊎ Φ ≣ Φ
    ⊎-id⁻ˡ   : ∀ {Φ₁ Φ₂} → ε ⊎ Φ₁ ≣ Φ₂ → Φ₁ ≡ Φ₂

  open IsSep isSep

  ⊎-idʳ : ∀ {Φ} → Φ ⊎ ε ≣ Φ
  ⊎-idʳ = ⊎-comm ⊎-idˡ

  ⊎-id⁻ʳ : ∀ {Φ} → ∀[ (Φ ⊎ ε) ⇒ (Φ ≡_) ]
  ⊎-id⁻ʳ = ⊎-id⁻ˡ ∘ ⊎-comm

  infix 10 ε[_]
  ε[_] : ∀ {ℓ} → Pred C ℓ → Set ℓ
  ε[ P ] = P ε

  {- Emptyness -}
  module _ where

    data Empty {p} (P : Set p) : SPred (c ⊔ p) where
      emp : P → Empty P ε

    pattern empty = emp tt

    Emp : SPred c
    Emp = Empty ⊤

  module _ where
    ε⊎ε : ∀[ ε ⊎ ε ⇒ Emp ]
    ε⊎ε p with ⊎-id⁻ˡ p
    ... | (P.refl) = empty

    ✴-idʳ : ∀ {p} {P : SPred p} → ∀[ P ⇒ P ✴ Emp ]
    ✴-idʳ px = px ×⟨ ⊎-idʳ ⟩ empty

    -- a resource-polymorphic function is a pure wand
    wandit : ∀ {p q} {P : SPred p} {Q : SPred q} → ∀[ P ⇒ Q ] → ε[ P ─✴ Q ]
    app (wandit f) p σ rewrite ⊎-id⁻ˡ σ = f p

    _⟨✴⟩_ : ∀ {p q} {P : SPred p} {Q : SPred q} → ε[ P ─✴ Q ] → ∀[ P ⇒ Q ]
    w ⟨✴⟩ p = app w p ⊎-idˡ

  {- A free preorder -}
  module _ where

    ≤-reflexive : Φ₁ ≡ Φ₂ → Φ₁ ≤ Φ₂
    ≤-reflexive P.refl = ε , ⊎-idʳ

    ≤-isPreorder : IsPreorder _≡_ _≤_
    ≤-isPreorder = record
      { isEquivalence = P.isEquivalence
      ; reflexive = ≤-reflexive
      ; trans = ≤-trans }

    ≤-preorder : Preorder _ _ _
    ≤-preorder = record { isPreorder = ≤-isPreorder }

    ε-minimal : ∀ {Φ} → ε ≤ Φ
    ε-minimal {Φ} = Φ , ⊎-idˡ

  {- Framing where we forget the actual resource owned -}
  module ↑-Frames where

    infixl 1000 _↑
    _↑ : ∀ {ℓ} → SPred ℓ → SPred _
    P ↑ = P ✴ U

    pattern _⇑_ p sep = p ×⟨ sep ⟩ tt

    module _ {ℓ} {P : SPred ℓ} where

      return : ∀[ P ⇒ P ↑ ]
      return p = p ×⟨ ⊎-idʳ ⟩ tt

      join : ∀[ (P ↑) ↑ ⇒ P ↑ ]
      join ((p ×⟨ σ₁ ⟩ tt) ×⟨ σ₂ ⟩ tt) =
        let _ , σ₃ = ≤-trans (-, σ₁) (-, σ₂) in p ×⟨ σ₃ ⟩ tt

    module _ {ℓ₁ ℓ₂} {P : SPred ℓ₁} {Q : SPred ℓ₂} where

      map : ∀[ P ⇒ Q ] → ∀[ P ↑ ⇒ Q ↑ ]
      map f (px ⇑ sep) = f px ⇑ sep

    module _ {ℓ₁ ℓ₂} {P : SPred ℓ₁} {Q : SPred ℓ₂} where

      ↑-bind : ∀[ P ⇒ Q ↑ ] → ∀[ P ↑ ⇒ Q ↑ ]
      ↑-bind f px = join (map f px)

    {- Projections out of separating conjunction using framing -}
    module _ where

      π₁ : ∀ {p q} {P : SPred p} {Q : SPred q} → ∀[ (P ✴ Q) ⇒ P ↑ ]
      π₁ (px ×⟨ sep ⟩ _) = px ⇑ sep

      π₂ : ∀ {p q} {P : SPred p} {Q : SPred q} → ∀[ (P ✴ Q) ⇒ Q ↑ ]
      π₂ (_ ×⟨ sep ⟩ qx) = qx ⇑ ⊎-comm sep

record IsConcattative {c} {C : Set c} (sep : RawSep C) : Set (suc c) where
  open RawSep sep

  field
    overlap {{ isSep }}  : IsSep sep

    _∙_ : C → C → C
    ⊎-∙ₗ : ∀ {Φ₁ Φ₂ Φ Φₑ} → Φ₁ ⊎ Φ₂ ≣ Φ → (Φₑ ∙ Φ₁) ⊎ Φ₂ ≣ (Φₑ ∙ Φ)

  open IsSep isSep

  ⊎-∙ᵣ : ∀ {Φ₁ Φ₂ Φ Φₑ} → Φ₁ ⊎ Φ₂ ≣ Φ → Φ₁ ⊎ (Φₑ ∙ Φ₂) ≣ (Φₑ ∙ Φ)
  ⊎-∙ᵣ s = ⊎-comm (⊎-∙ₗ (⊎-comm s))

record IsPositive {c} {C : Set c} (sep : RawSep C) : Set (suc c) where
  open RawSep sep

  field
    {ε} : _
    overlap {{ isUnitalSep }} : IsUnitalSep sep ε
    overlap {{ isSep }}       : IsSep sep

  open IsUnitalSep isUnitalSep using (⊎-id⁻ˡ)

  field
    ⊎-εˡ : ∀ {Φ₁ Φ₂} → Φ₁ ⊎ Φ₂ ≣ ε → Φ₁ ≡ ε

  ⊎-ε : ∀ {Φ₁ Φ₂} → Φ₁ ⊎ Φ₂ ≣ ε → Φ₁ ≡ ε × Φ₂ ≡ ε
  ⊎-ε σ with ⊎-εˡ σ
  ... | P.refl with ⊎-id⁻ˡ σ
  ... | P.refl = P.refl , P.refl

record Separation c : Set (suc c) where
  field
    Carrier : Set c
    overlap {{ raw }}   : RawSep Carrier
    overlap {{ isSep }} : IsSep raw

record UnitalSep c : Set (suc c) where
  field
    Carrier : Set c
    ε       : _
    overlap {{ sep }}         : RawSep Carrier
    overlap {{ isUnitalSep }} : IsUnitalSep sep ε

record MonoidalSep c : Set (suc c) where
  field
    Carrier : Set c
    ε       : _
    overlap {{ sep }}         : RawSep Carrier
    overlap {{ isSep }}       : IsSep sep
    overlap {{ isUnitalSep }} : IsUnitalSep sep ε
    overlap {{ isConcat }}    : IsConcattative sep

  open RawSep sep
  open IsSep isSep
  open IsConcattative isConcat
  open IsUnitalSep isUnitalSep hiding (ε)

  field
    overlap {{ monoid }}      : IsMonoid {A = Carrier} _≡_ _∙_ ε

  open IsMonoid monoid

  ⊎-∙ : ∀ {Φₗ Φᵣ : Carrier} → Φₗ ⊎ Φᵣ ≣ (Φₗ ∙ Φᵣ)
  ⊎-∙ {Φₗ} {Φᵣ} =
    P.subst (λ φ → φ ⊎ Φᵣ ≣ (Φₗ ∙ Φᵣ))
      (identityʳ Φₗ)
      (⊎-∙ₗ {Φₑ = Φₗ} (⊎-idˡ {Φᵣ}))

  instance unital : UnitalSep _
  unital = record { ε = ε }

module _ {c} {C : Set c} where

  εOf : ∀ (r : RawSep C) {u} {{ _ : IsUnitalSep r u }} → C
  εOf _ {{ un }}= IsUnitalSep.ε un

open RawSep ⦃...⦄ public
open IsConcattative ⦃...⦄ public
open IsUnitalSep ⦃...⦄ public
open IsPositive ⦃...⦄ hiding (ε) public
open UnitalSep ⦃...⦄ public hiding (Carrier; ε)
open IsSep ⦃...⦄ public
open MonoidalSep ⦃...⦄ public hiding (Carrier; ε)


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

open import HoTT
open import cohomology.Theory

{- Useful lemmas concerning the functorial action of C -}

module cohomology.Functor {i} (CT : CohomologyTheory i) where

open CohomologyTheory CT

CF-inverse : (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y)) (g : fst (Y ⊙→ X))
  → g ⊙∘ f == ⊙idf _ → (CF-hom n f) ∘ᴳ (CF-hom n g) == idhom _
CF-inverse n f g p = ! (CF-comp n g f) ∙ ap (CF-hom  n) p ∙ CF-ident n

ext: agda

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
{-# OPTIONS --copatterns #-}

module LecStr where

open import CS410-Prelude
open import CS410-Nat
open import CS410-Functor

record Stream (X : Set) : Set where
  coinductive
  field
    head : X
    tail : Stream X
open Stream

count : Nat -> Stream Nat
head (count n) = n
tail (count n) = count (suc n)

nats : Stream Nat
nats = count zero

poke : Nat
poke = head (tail (tail (tail nats)))

repeat : {X : Set} -> X -> Stream X
head (repeat x) = x
tail (repeat x) = repeat x

strApp : {S T : Set} -> Stream (S -> T) -> Stream S -> Stream T
head (strApp fs ss) = (head fs) (head ss)
tail (strApp fs ss) = strApp (tail fs) (tail ss)

strMap : {S T : Set} -> (S -> T) -> Stream S -> Stream T
strMap f ss = strApp (repeat f) ss

diagonal : {X : Set} -> Stream (Stream X) -> Stream X
head (diagonal xss) = head (head xss)
tail (diagonal xss) = diagonal (strMap tail (tail xss))

{- productivity checker rejects
fibo : Stream Nat
head fibo = 1
head (tail fibo) = 1
tail (tail fibo) = strApp (strApp (repeat _+N_) (tail fibo)) fibo
-}

data CoList' (X : Set) : Set
record CoList (X : Set) : Set where
  coinductive
  constructor thunk
  field
    force : CoList' X
data CoList' X where
  [] : CoList' X
  _::_ : X -> CoList X -> CoList' X

module CoListExamples where
  open CoList

  short : CoList Nat
  short = thunk (0 :: thunk (1 :: thunk (2 :: thunk [])))

  long : forall {X} -> Stream X -> CoList X
  force (long s) = head s :: long (tail s)

  _++_ : forall {X} -> CoList X -> CoList X -> CoList X
  force (xs ++ ys) with force xs
  force (xs ++ ys) | [] = force ys
  force (xs ++ ys) | x :: xs' = x :: (xs' ++ ys)

{-
  concat : forall {X} -> CoList (CoList X) -> CoList X
  force (concat xss) with force xss
  force (concat xss) | [] = []
  force (concat xss) | xs :: xss' with force xs
  force (concat xss) | xs :: xss' | [] = ? -- oops force (concat xss')
  force (concat xss) | xs :: xss' | x :: xs' = x :: concat (thunk (xs' :: xss'))
-}

-- nonempty CoLists
-- tails for Streams
-- " n.e. CoLists


text:
--{-# OPTIONS -v tc.data:100 #-}
module Issue830 where

_⟶_ : Set₁ → Set → Set₁
A ⟶ B = A → B

data ⟨Set⟩ : Set where
  [_] : Set ⟶ ⟨Set⟩

-- should fail

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module x where

{-
------------------------------------------------------------------------------
Abstract

Relational program derivation technique :
- stepwise refining a relational spec to a program by algebraic rules.
- program obtained is correct by construction

Dependent type theory rich enough to express correctness properties verified by type checker.

Library, Algebra of Programming in Agda (AoPA)
- http://www.iis.sinica.edu.tw/~scm/2008/aopa/
- encodes relational derivations
- A program is coupled with an algebraic derivation whose correctness is guaranteed by type system

------------------------------------------------------------------------------
1 Introduction

relational program derivation
- specs are input-output relations that are stepwise refined by an algebra of programs.

paper show how program derivation can be encoded in a type and its proof term.

- case study using Curry-Howard isomorphism
- modelled a many concepts that occur in relational program derivation
  including relational folds, relational division, and converse-of-a-function.
  - e.g., Minimum, is defined using division and intersection
  - e.g., greedy theorem proved using the universal property of minimum.
  - the theorem can be used to deal with a number of optimisation problems specified as folds.
• to ensure termination with unfolds and hylomorphisms, enable programmer to
  model an unfold as the relational converse of a fold, but demand a proof of accessibility
  before it is refined to a functional unfold.

------------------------------------------------------------------------------
2 Overview of Relational Program Derivation

Merit of functional programming : programs can be manipulated by equational reasoning.

Program derivation in Bird-Meertens style 1989b) typically start with a specification,
as a function, that is obviously correct but not efficient.

Algebraic identities are then applied, in successive steps,
to show that the specification equals another functional program that is more efficient.

Typical example : Maximum Segment Sum (Gries, 1989; Bird, 1989a), specification :
    max · map sum · segs
where
- segs produces all consecutive segments of the input list of numbers
- map sum computes their summation
- maximum is picked by max
Specification can be shown, after transformation, to be equal a version using foldr (linear).

In 90’s there was a trend in the program derivation community to move from functions to relations.
- spec given in terms of an input/output relation
- relation is refined to smaller, more deterministic relations in each step,
- until obtaining a function

Relational derivation advantages:
- spec often more concise than corresponding functional specification
- optimisation problems can be specified using relations generating all possible solutions
- easier to talk about program inversion

The catch: *must reason in terms of inequalities rather than equalities*

denoted by R : B ← A
- relation R from A to B
- subset of set of pairs B × A
- A function f is seen as a special case where (b, a) ∈ f and (b' , a) ∈ f implies b = b'

converse R˘ : A ← B of R : B ← A
- defined by (a, b) ∈ R ˘ if (b, a) ∈ R

composition of two relations R : C ← B and S : B ← A
- defined by: (c, a) ∈ R ◦ S if ∃b : (c, b) ∈ R ∧ (b, a) ∈ S

power transpose ΛR of R : B ← A
- is a function from A to P B (subsets of B)
- ΛR a = { b | (b, a) ∈ R }.

relation ∈ : A ← P A
- maps a set to one of its arbitrary members
- converse: ∋ : P A ← A

product of two relations, R × S
- defined by ((c, d), (a, b)) ∈ R × S if (c, a) ∈ R and (d, b) ∈ S

--      step fun      base  input    output
foldr : (A → B → B) → B   → List A → B

generalisation to a relation, denote foldR

              input    step relation  base cases
foldR R : B ← List A ← (B ← (A×B))    (set s : PB)

-- relation mapping a list to one of its arbitrary subsequences
subseq = foldR (cons ∪ outr) {[ ]}
where
  cons (x, xs) = x :: xs -- cons keeps the current element
  outr (x, xs) = xs      -- outr drops the current element

Relational fold defined in terms of functional fold:

   foldR R s = ∈ ◦ foldr Λ(R ◦ (id " ∈)) s

of type List A → P B that collects all the results in a set.

step function Λ(R ◦ (id " ∈))  : has type (A × P B) → P B
(id " ∈) : (A × B) ← (A × P B) : pairs current element with one of the results from previous step
                                 before passing the pair to R

foldR R s satisfies the universal property:
foldR R s = S ⇔ R ◦ (id " S) = S ◦ cons ∧ s = ΛS [ ]

-- induction rule
-- states that foldR R s is the unique fixed-point of the monotonic function
λ X → (R ◦ (id " X) ◦ cons ˘) ∪ {(b, [ ]) | b ∈ s}

-- computation rule
-- foldR R s is also the least prefix-point, therefore
foldR R s ⊆ S ⇐ R ◦ (id " S) ⊆ S ◦ cons ∧ s ⊆ ΛS [ ],
R ◦ (id " foldR R s) ⊆ foldR R s ◦ cons ∧ s ⊆ Λ(foldR R s) [ ].

If an optimisation problem can be specified by generating all possible solutions using
foldR or converse of foldR before picking the best one, Bird and de Moor (1997) gave a
number of conditions under which the specification can be refined to a greedy algorithm, a
dynamic programming algorithm, or something in-between.

------------------------------------------------------------------------------
3 A Crash Course in Agda
-}

-- Fig. 2. Some examples of datatype definitions.

data List (A : Set) : Set where
  []   : List A
  _∷_  : A → List A → List A

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data _≤_ : ℕ → ℕ → Set where
  ≤-refl : {n   : ℕ} → n ≤ n
  ≤-step : {m n : ℕ} → m ≤ n → m ≤ suc n

_<_ : ℕ → ℕ → Set
m < n = suc m ≤ n

-- Fig. 3. An encoding of first-order intuitionistic logic in Agda.

-- Truth : has one unique term — a record with no fields
record ⊤ : Set where

-- Falsity : type with no constructors therefore no inhabitants
data ⊥ : Set where

-- Disjunction : proof deduced either from a proof of P or a proof of Q
data _⨄_ (A B : Set) : Set where
  inj1 : A → A ⨄ B
  inj2 : B → A ⨄ B

-- Dependent Pair : type of 2nd may depend on the first component
data Σ (A : Set)(B : A → Set) : Set where
  _,_ : (x : A) → (y : B x) → Σ A B

proj₁ : ∀ {A B} → Σ A B → A
proj₁ (x , y) = x

proj₂ : ∀ {A B} → (p : Σ A B) → B (proj₁ p)
proj₂ (x , y) = y

-- Conjunction
_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)

-- Existential Quantification
-- to prove the proposition ∃ P, where P is a predicate on terms of type A
-- provide, in a pair, a witness w : A and a proof of P w.
∃ : {A : Set} (P : A → Set) → Set
∃ = Σ _

-- Universal Quantification
-- of predicate P on type A is encoded as a dependent function type
-- whose elements, given any x : A, must produce a proof of P x.
-- Agda provides a short hand ∀ x → P x in place of (x : A) → P x when A can be inferred.

-- Implication
-- P → Q is represented as a function taking a proof of P to a proof of Q
-- no new notation for it

-- Predicates
-- on type A are represented by A → Set.
-- e.g., (λ n → zero < n) : N → Set
-- is a predicate stating that a natural number is positive.

{-
3.2 Identity Type

term of type x ≡ y is proof x and y are equal
-}

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

-- REFLEXIVE : by definition

-- SYMMETRIC
≡-sym : {A : Set}{x y : A} → x ≡ y → y ≡ x
≡-sym {A}{x}{.x} ≡-refl = ≡-refl

-- TRANSITIVE
≡-trans : {A : Set}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans {A}{x}{.x}{z} ≡-refl x≡z = x≡z -- could replace x≡z with ≡-refl

-- SUBSTITUTIVE — if x ≡ y, they are interchangeable in all contexts
≡-subst : {A : Set}(P : A → Set){x y : A} → x ≡ y → P x → P y
≡-subst P ≡-refl Px = Px

≡-cong : {A B : Set}(f : A → B){x y : A} → x ≡ y → f x ≡ f y
≡-cong f ≡-refl = ≡-refl
{-
≡ NOT EXTENSIONAL
Qquality of terms is checked by expanding them to normal forms.
Problem comparing higher-order values: e.g., sum·map sum     and     sum · concat
while defining the same function summing up a list of lists of numbers, are not “equal” under ≡ .

Can define extensional equality for (non-dependent) functions on first-order values:
-}
_≐_ : {A B : Set} → (A → B) → (A → B) → Set
f ≐ g = ∀ x → f x ≡ g x
{-
≐ NOT SUBSTITUTIVE : congruence of ≐ has to be proved for each context.

Refinement in preorder reasoning usually involves replacing terms in provably monotonic contexts.
This is a significant overhead; but given that this overhead
is incurred anyway, not having extensional equality is no extra trouble.

3.3 Preorder Reasoning

To prove e1 ≡ e2 is to construct a term having that type.

For any binary relation ∼ that is reflexive and transitive
- for which one can construct terms ∼-refl and ∼-trans having the types described in above
can derive a set of combinators, shown in Fig. 4,
which enables one to construct a term of type e₁ ∼ en  in algebraic style.

-- Fig. 4. Combinators for preorder reasoning.
infixr 2 _∼⟨_⟩_
infix  2 _∼∎

_∼⟨_⟩_ : {A : Set}(x : A){y z : A} → x ∼ y → y ∼ z → x ∼ z
x ∼⟨ x∼y ⟩ y∼z = ∼-trans x∼y y∼z

_∼∎ : {A : Set}(x : A) → x ∼ x
x ∼∎ = ∼-refl

implication as a relation:
-}
_⇒_ : Set → Set → Set
P ⇒ Q = P → Q

_⇐_ : Set → Set → Set
P ⇐ Q = Q ⇒ P
{-
Reflexivity and transitivity of ⇐ , for example, can be simply given by ⇐-refl = id and
⇐-trans = · , where · is function composition. Therefore, they induce a pair of operators
_⇐⟨_⟩_ and ⇐∎ for logical reasoning.

Hierarchy of universes
- Set, the type of small types, is in sort Set1

When instantiating ∼ in Fig. 4 to ⇐ : Set → Set → Set
- notice that the type A : Set itself cannot be instantiated to Set, which is in Set1

We resolve this by using different module generators for different universes.
More on this in Sect. 4.1.

3.4 Functional Derivation

Since _≐_ is reflexive and transitive (not shown), it induces its preorder reasoning operators.

Fig. 5 shows a proof of the universal property of foldr.

The steps using ≡-refl are equivalences Agda proves by expanding definitions.
The inductive hypothesis is established by a recursive call to foldr-universal.
-}
infix  3 _≡∎
infixr 2 _≡⟨⟩_ _≡⟨_⟩_
infix  1 begin_

begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

_≡⟨⟩_ : {A : Set} (x {y} : A) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

_≡⟨_⟩_ : {A : Set} (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ x≡y ⟩ y≡z = ≡-trans x≡y y≡z

_≡∎ : {A : Set} (x : A) → x ≡ x
_≡∎ _ = ≡-refl
{-
Fig. 5. Proving the universal property for foldr
-}
foldr              : {A B : Set}
                   → (A → B → B) → B → List A
                   → B
foldr f e      []  = e
foldr f e (x ∷ xs) = f x (foldr f e xs)

{- https://www.cs.nott.ac.uk/~pszgmh/fold.pdf
For finite lists, the universal property of fold can be stated as the following equivalence
between two definitions for a function g that processes lists:
g      []  = v
                         ⇔ g = fold f v
g (x ∷ xs) = f x (g xs)

right-to-left : substituting g = fold f v into the two equations for g gives recursive fold def
left-to-right : two equations for g are the assumptions required to show that g = fold f v
using a simple proof by induction on finite lists (Bird, 1998)

universal property states that for finite lists the function fold f v is not just a
solution to its defining equations, but the unique solution.

Utility of universal property : makes explicit the two assumptions
required for a certain pattern of inductive proof.

For specific cases, by verifying the two assumptions (typically done without need for induction)
can then appeal to the universal property to complete the inductive proof that g = fold f v.

universal PROPERTY of fold : encapsulates a pattern of inductive proof concerning lists
just as the fold OPERATOR  : encapsulates a pattern of recursion for processing lists
-}
foldr-universal : ∀ {A B} (h : List A → B) f e
                → (h [] ≡ e)
                → (∀ x xs → h (x ∷ xs) ≡ f x (h xs))
                → h ≐ foldr f e
foldr-universal h f e base step      []  = base
foldr-universal h f e base step (x ∷ xs) =
  begin
    h (x ∷ xs)
  ≡⟨ step x xs ⟩
    f x (h xs)
  ≡⟨ ≡-cong (f x) (foldr-universal h f e base step xs) ⟩
    f x (foldr f e xs)
  ≡⟨ ≡-refl ⟩
    foldr f e (x ∷ xs)
  ≡∎
{-
-- Can use the universal property to prove the foldr-fusion theorem:

_·_ : {A : Set} {B : A → Set} {C : (x : A) → B x → Set}
    → (f : {x : A} (y : B x) → C x y)
    → (g : (x : A) → B x)
    → (x : A) → C x (g x)
(f · g) x = f (g x)

-- TODO compile problems
foldr-fusion : ∀ {A B C} (h : B → C) {f : A → B → B} {g : A → C → C}
             → {e : B}
             → (∀ x y → h (f x y) ≡ g x (h y))
             → (h · foldr f e) ≐ (foldr g (h e))
foldr-fusion h {f} {g} e fuse =
  foldr-universal (h · foldr f e) g (h e) ≡-refl (λ x xs → fuse x (foldr f e xs))
-}

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

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

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


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

open import HoTT
open import homotopy.PtdAdjoint
open import homotopy.SuspAdjointLoop
open import cohomology.WithCoefficients

module cohomology.SuspAdjointLoopIso where

module SuspAdjointLoopIso {i} where

  private
    hadj : HomAdjoint {i} {i} Σ⊣Ω.SuspFunctor Σ⊣Ω.LoopFunctor
    hadj = counit-unit-to-hom Σ⊣Ω.adj

    module A = HomAdjoint hadj

  module _ (X Y : Ptd i) where

    abstract
      pres-comp : (h₁ h₂ : ⊙Susp X ⊙→ ⊙Ω Y)
        → –> (A.eq X (⊙Ω Y)) (⊙Ω-∙ ⊙∘ ⊙fanout h₁ h₂)
           == ⊙Ω-∙ ⊙∘ ⊙fanout (–> (A.eq X (⊙Ω Y)) h₁) (–> (A.eq X (⊙Ω Y)) h₂)
      pres-comp h₁ h₂ =
        B.nat-cod h₁ h₂ ⊙Ω-∙
        ∙ ap (_⊙∘ ⊙fanout (–> (A.eq X (⊙Ω Y)) h₁) (–> (A.eq X (⊙Ω Y)) h₂))
             arr2-lemma
        where
        module A× = RightAdjoint× hadj
        module B = RightAdjointBinary hadj

        ap2-lemma : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
          (f : A × B → C) {r s : A × B} (p : r == s)
          → ap f p == ap2 (curry f) (ap fst p) (ap snd p)
        ap2-lemma f idp = idp

        ⊙ap2-lemma : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
          (f : X ⊙× Y ⊙→ Z)
          → ⊙Ω-fmap f == ⊙Ω-fmap2 f ⊙∘ ⊙fanout (⊙Ω-fmap ⊙fst) (⊙Ω-fmap ⊙snd)
        ⊙ap2-lemma (f , idp) = ⊙λ= (ap2-lemma f) idp

        arr2-lemma : B.arr2 ⊙Ω-∙ == ⊙Ω-∙
        arr2-lemma =
          ⊙Ω-fmap ⊙Ω-∙ ⊙∘ A×.⊙out _ _
            =⟨ ⊙ap2-lemma ⊙Ω-∙ |in-ctx _⊙∘ A×.⊙out _ _ ⟩
          (⊙Ω-fmap2 ⊙Ω-∙ ⊙∘ A×.⊙into _ _) ⊙∘ A×.⊙out _ _
            =⟨ ⊙∘-assoc (⊙Ω-fmap2 ⊙Ω-∙) (A×.⊙into _ _) (A×.⊙out _ _) ⟩
          ⊙Ω-fmap2 ⊙Ω-∙ ⊙∘ (A×.⊙into _ _ ⊙∘ A×.⊙out _ _)
            =⟨ A×.⊙into-out _ _ |in-ctx ⊙Ω-fmap2 ⊙Ω-∙ ⊙∘_ ⟩
          ⊙Ω-fmap2 ⊙Ω-∙
            =⟨ ⊙Ω-fmap2-∙ ⟩
          ⊙Ω-∙ ∎

    iso : Trunc-⊙→Ω-group (⊙Susp X) Y ≃ᴳ Trunc-⊙→Ω-group X (⊙Ω Y)
    iso = Trunc-group-emap (≃-to-≃ᴳˢ (A.eq X (⊙Ω Y)) pres-comp)

  abstract
    nat-dom : {X Y : Ptd i} (f : X ⊙→ Y) (Z : Ptd i)
      → fst (iso X Z) ∘ᴳ Trunc-⊙→Ω-group-fmap-dom (⊙Susp-fmap f) Z
        == Trunc-⊙→Ω-group-fmap-dom f (⊙Ω Z) ∘ᴳ fst (iso Y Z)
    nat-dom f Z = group-hom= $ λ= $ Trunc-elim
      (λ _ → =-preserves-level Trunc-level)
      (λ g → ap [_] (! (A.nat-dom f (⊙Ω Z) g)))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Induction.Everything where

open import Cubical.Induction.WellFounded public

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module Examples.PingPong where

open import ActorMonad public
open import Prelude

-- An example including three actors: spawner, pinger, ponger
--
-- Spawner is the actor that starts it all.
-- Spawner spawns both pinger and ponger.
-- Then spawner send the reference of ponger to pinger,
-- and the reference of pinger to ponger.
--
-- Pinger is an actor that can receive Bool messages.
-- Pinger counts the number of 'false' messages it receives, until it receives a 'true'
--
-- Ponger is an actor that can receive Nat messages.
-- Ponger keeps sending 'false' until it receives a message containing 10.

Spawnbox : InboxShape
Spawnbox = []

mutual
  PingValues = [ Bool ]ˡ
  PongValues = [ ℕ ]ˡ

  PingRefs : TypingContext
  PingRefs = [ ⊠-of-values PongValues ]ˡ
  PongRefs : TypingContext
  PongRefs = [ ⊠-of-values PingValues ]ˡ

  PongReferenceMessage : MessageType
  PongReferenceMessage = [ ReferenceType (⊠-of-values PongValues) ]ˡ

  BoolMessage : MessageType
  BoolMessage = [ ValueType Bool ]ˡ

  Pingbox : InboxShape
  Pingbox = BoolMessage ∷ [ PongReferenceMessage ]ˡ

  PingReferenceMessage : MessageType
  PingReferenceMessage = [ ReferenceType (⊠-of-values PingValues) ]ˡ

  NatMessage : MessageType
  NatMessage = [ ValueType ℕ ]ˡ

  Pongbox : InboxShape
  Pongbox = NatMessage ∷ [ PingReferenceMessage ]ˡ

constPingrefs : {A : Set₁} → (A → TypingContext)
constPingrefs _ =  PingRefs

pingMainActor : (i : Size) (A : Set₁) → Set₂
pingMainActor i A = ∞ActorM i Pingbox A PingRefs constPingrefs

mutual
  pingReceive : ∀ {i} (msg : Message Pingbox) → ∞ActorM i Pingbox (Lift (lsuc lzero) Bool) (add-references PingRefs msg) constPingrefs
  pingReceive (Msg Z (b ∷ [])) = return b
  pingReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPingValue
  pingReceive (Msg (S (S ())) x₁)

  loopTillPingValue : ∀ {i} → pingMainActor i (Lift (lsuc lzero) Bool)
  loopTillPingValue .force = receive ∞>>= pingReceive

pinger : ∀ {i} → ∞ActorM (↑ i) Pingbox ⊤₁ [] constPingrefs
pinger .force = loopTillPong ∞>> pingMain 0
  where
    loopTillPong : ∀ {i} → ∞ActorM i Pingbox ⊤₁ [] constPingrefs
    loopTillPong .force = receive ∞>>= ((λ
      { (Msg Z x₁) → loopTillPong
      ; (Msg (S Z) x₁) → return _
      ; (Msg (S (S ())) x₁)
      }))
    pingMain : ∀ {i} → ℕ → pingMainActor i ⊤₁
    pingMain n .force = loopTillPingValue ∞>>= λ
      { (lift false) → (Z ![t: Z ] ( [ lift n ]ᵃ)) >> pingMain (suc n)
      ; (lift true) → return _}

constPongrefs : {A : Set₁} → (A → TypingContext)
constPongrefs _ = PongRefs

pongMainActor : (i : Size) (A : Set₁) → Set₂
pongMainActor i A = ∞ActorM i Pongbox A PongRefs constPongrefs

mutual
  pongReceive : ∀ {i} (msg : Message Pongbox) → ∞ActorM i Pongbox (Lift (lsuc lzero) ℕ) (add-references PongRefs msg) constPongrefs
  pongReceive (Msg Z (n ∷ [])) = return n
  pongReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPongValue
  pongReceive (Msg (S (S ())) _)
  loopTillPongValue : ∀ {i} → pongMainActor i (Lift (lsuc lzero) ℕ)
  loopTillPongValue .force = receive ∞>>= pongReceive

ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs
ponger .force = loopTillPing ∞>> ((Z ![t: Z ] ([ lift false ]ᵃ)) >> pongMain)
  where
    loopTillPing : ∀ {i} → ∞ActorM i Pongbox ⊤₁ [] constPongrefs
    loopTillPing .force = receive ∞>>= λ {
      (Msg Z _) → loopTillPing
      ; (Msg (S Z) _) → return _
      ; (Msg (S (S ())) _)
      }
    pongMain : ∀ {i} → pongMainActor i ⊤₁
    pongMain .force = loopTillPongValue ∞>>= λ {
      (lift 10) → Z ![t: Z ] [ lift true ]ᵃ
      ; (lift n) → Z ![t: Z ] [ lift false ]ᵃ >> pongMain
      }

spawner : ∀ {i} → ∞ActorM i Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ [ Pongbox ]ˡ)
spawner = do
  spawn∞ ponger
  spawn∞ pinger
  Z ![t: S Z ] [ [ S Z ]>: [ Z ]ᵐ ]ᵃ
  S Z ![t: S Z ] [ [ Z ]>: [ Z ]ᵐ ]ᵃ

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module Issue1252 where

data Bool : Set where
  true false : Bool

{-# COMPILE GHC Bool = data Bool (True | False) #-}

foo : Bool → Bool
foo true  = false
foo false = true

{-# COMPILE GHC foo as foohs #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --safe #-}
-- https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-revised.pdf

module Constructive.OmniscienceAlt where

open import Level renaming (zero to lzero; suc to lsuc)
import Data.Bool as 𝔹 using (_≤_)
open import Data.Bool as 𝔹 using (Bool; true; false; T; f≤t; b≤b; _∧_; not; _∨_)
import Data.Bool.Properties as 𝔹ₚ
open import Data.Empty
open import Data.Unit using (tt)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod
open import Data.Sum as Sum
open import Function.Base
open import Relation.Binary as B
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable
import Relation.Unary as U

-- agda-misc
open import Constructive.Axiom
open import Constructive.Axiom.Properties
open import Constructive.Axiom.Properties.Base.Lemma
open import Constructive.Common
open import Constructive.Combinators

ℕ∞ : Set
ℕ∞ = Σ (ℕ → Bool) λ x → ∀ i → T (x i) → T (x (suc i))

fromℕ-C : ℕ → ℕ → Bool
fromℕ-C zero    zero    = false
fromℕ-C zero    (suc n) = true
fromℕ-C (suc m) zero    = false
fromℕ-C (suc m) (suc n) = fromℕ-C m n

fromℕ-convergent : ∀ n i → T (fromℕ-C n i) → T (fromℕ-C n (suc i))
fromℕ-convergent zero    (suc i) t = tt
fromℕ-convergent (suc n) (suc i) t = fromℕ-convergent n i t

fromℕ : ℕ → ℕ∞
fromℕ n = fromℕ-C n , fromℕ-convergent n

∞ : ℕ∞
∞ = (λ _ → false) , (λ i x → x)

_≈_ : Rel (ℕ → Bool) lzero
α ≈ β = ∀ i → α i ≡ β i

_≉_ : Rel (ℕ → Bool) lzero
α ≉ β = ¬ (α ≈ β)

_#_ : Rel (ℕ → Bool) lzero
α # β = ∃ λ i → α i ≢ β i

#⇒≉  : {α β : ℕ → Bool} → α # β → α ≉ β
#⇒≉ {α} {β} (i , αi≢βi) α≈β = αi≢βi (α≈β i)

≈-refl : {α : ℕ → Bool} → α ≈ α
≈-refl _ = refl

≈-sym : {α β : ℕ → Bool} → α ≈ β → β ≈ α
≈-sym α≈β i = sym (α≈β i)

≈-trans : {α β γ : ℕ → Bool} → α ≈ β → β ≈ γ → α ≈ γ
≈-trans α≈β β≈γ i = trans (α≈β i) (β≈γ i)

_≈∞_ : Rel ℕ∞ lzero
x ≈∞ y = proj₁ x ≈ proj₁ y

_≉∞_ : Rel ℕ∞ lzero
x ≉∞ y = proj₁ x ≉ proj₁ y

_#∞_ : Rel ℕ∞ lzero
x #∞ y = proj₁ x # proj₁ y

-- Proposition 3.1
-- r = ≤-any

≤-any : (ℕ → Bool) → (ℕ → Bool)
≤-any α zero    = α 0
≤-any α (suc n) = α (suc n) ∨ ≤-any α n

≤-any-idem : ∀ α → ≤-any (≤-any α) ≈ ≤-any α
≤-any-idem α zero    = refl
≤-any-idem α (suc n) = begin
  (α (suc n) ∨ ≤-any α n) ∨ ≤-any (≤-any α) n
    ≡⟨ cong ((α (suc n) ∨ ≤-any α n) ∨_) $ ≤-any-idem α n ⟩
  (α (suc n) ∨ ≤-any α n) ∨ ≤-any α n
    ≡⟨ 𝔹ₚ.∨-assoc (α (suc n)) (≤-any α n) (≤-any α n) ⟩
  α (suc n) ∨ (≤-any α n ∨ ≤-any α n)
    ≡⟨ cong (α (suc n) ∨_) $ 𝔹ₚ.∨-idem (≤-any α n) ⟩
  α (suc n) ∨ ≤-any α n
    ∎
  where open ≡-Reasoning

private
  T-∧-× : ∀ {x y} → T (x ∧ y) → (T x × T y)
  T-∧-× {true} {true} t = tt , tt

  T-×-∧ : ∀ {x y} → (T x × T y) → T (x ∧ y)
  T-×-∧ {true} {true} (tt , tt) = tt

  T-∨-introʳ : ∀ {x y} → T y → T (x ∨ y)
  T-∨-introʳ {true} {true} t = tt
  T-∨-introʳ {false} {true} t = tt

  T-∨-introˡ : ∀ {x y} → T x → T (x ∨ y)
  T-∨-introˡ {true} {true} t = tt
  T-∨-introˡ {true} {false} t = tt

≤-any-convergent : ∀ α i → T (≤-any α i) → T (≤-any α (suc i))
≤-any-convergent α n t = T-∨-introʳ t

≤-any-ℕ∞ : (ℕ → Bool) → ℕ∞
≤-any-ℕ∞ α = ≤-any α , ≤-any-convergent α

≤-any-construct : ∀ α n → T (α n) → T (≤-any α n)
≤-any-construct α zero    t = t
≤-any-construct α (suc n) t = T-∨-introˡ t

private
  not-injective : ∀ {x y} → not x ≡ not y → x ≡ y
  not-injective {false} {false} refl = refl
  not-injective {true}  {true}  refl = refl

  x≢y⇒not[x]≡y : ∀ {x y} → x ≢ y → not x ≡ y
  x≢y⇒not[x]≡y {false} {false} x≢y = contradiction refl x≢y
  x≢y⇒not[x]≡y {false} {true} x≢y = refl
  x≢y⇒not[x]≡y {true} {false} x≢y = refl
  x≢y⇒not[x]≡y {true} {true} x≢y = contradiction refl x≢y

  x≢y⇒x≡not[y] : ∀ {x y} → x ≢ y → x ≡ not y
  x≢y⇒x≡not[y] {x} {y} x≢y = subst (_≡ not y) (𝔹ₚ.not-involutive x) $
                             x≢y⇒not[x]≡y {not x} {not y} (x≢y ∘′ not-injective)

  x≡y⇒not[x]≢y : ∀ {x y} → x ≡ y → not x ≢ y
  x≡y⇒not[x]≢y {false} {false} p ()
  x≡y⇒not[x]≢y {false} {true} () q
  x≡y⇒not[x]≢y {true} {false} () q
  x≡y⇒not[x]≢y {true} {true} p ()

  not[x]≡true→x≢true : ∀ {x} → not x ≡ true → x ≢ true
  not[x]≡true→x≢true {false} refl ()
  not[x]≡true→x≢true {true}  ()   p

  false≢true : false ≢ true
  false≢true ()

lpo-Bool⇒∀x→x#∞⊎x≈∞ : LPO-Bool ℕ → ∀ x → (x #∞ ∞) ⊎ (x ≈∞ ∞)
lpo-Bool⇒∀x→x#∞⊎x≈∞ lpo-Bool (α , con) with lpo-Bool α
... | inj₁ (x , αx≡true) = inj₁ (x , λ αx≡false → false≢true (trans (sym αx≡false) αx≡true))
... | inj₂ ¬∃x→αx≡true   = inj₂ λ i →  x≢y⇒x≡not[y] $′ ¬∃P→∀¬P ¬∃x→αx≡true i

T-to-≡ : ∀ {x} → T x → x ≡ true
T-to-≡ {true} tx = refl

≡-to-T : ∀ {x} → x ≡ true → T x
≡-to-T {true} x≡true = tt

private
  T-¬-not : ∀ {x} → ¬ (T x) → T (not x)
  T-¬-not {false} n = tt
  T-¬-not {true}  n = n tt

  T-not-¬ : ∀ {x} → T (not x) → ¬ (T x)
  T-not-¬ {false} tt ()
  T-not-¬ {true}  () y

¬T-≤-any : ∀ α x → ¬ T (≤-any α x) → ∃ λ y → ¬ T (α y)
¬T-≤-any α zero    ¬T with α 0 | inspect α 0
... | true  | [ α0≡true ]  = contradiction tt ¬T
... | false | [ α0≡false ] = zero , (λ T[α0] → subst T α0≡false T[α0])
¬T-≤-any α (suc x) ¬T with α (suc x) | inspect α (suc x)
... | true  | [ αsn≡true ] = ¬T-≤-any α x ¬T
... | false | [ αsn≡false ] = (suc x) , (λ T[αsn] → subst T αsn≡false T[αsn])
{-
¬T-≤-any′ : ∀ α x → ¬ T (≤-any (not ∘′ α) x) → ∃ λ y → T (α y)
¬T-≤-any′ α x ¬T =
  Prod.map₂ (λ nt → subst T (𝔹ₚ.not-involutive _) (T-¬-not nt)) $′
  ¬T-≤-any (not ∘ α) x ¬T

∀x→x#∞⊎x≈∞⇒lpo-Bool : (∀ x → (x #∞ ∞) ⊎ (x ≈∞ ∞)) → LPO-Bool ℕ
∀x→x#∞⊎x≈∞⇒lpo-Bool ≈∞? P with ≈∞? (≤-any-ℕ∞ (λ n → not (P n)))
... | inj₁ (x , ≤-any[not∘P,x]≢true) =
  inj₁ (Prod.map₂ T-to-≡ (¬T-≤-any′ P x (contraposition T-to-≡ ≤-any[not∘P,x]≢true)))
... | inj₂ ∀i→≤-any[not∘P,i]≡true =
  inj₂ (∀¬P→¬∃P λ i → not[x]≡true→x≢true (T-to-≡ $ ≤-any-extract (not ∘ P) i $ ≡-to-T (∀i→≤-any[not∘P,i]≡true i)))

--  ≤-any (λ n → not (P n)) x ≡ true → ⊥
-- ≤-any (not ∘ P) x ≡ false
--
--  ---------------------------
--  T (≤-any P x)
-}


text:
module UnSizedIO.Object where

open import Data.Product

record Interface : Set₁ where
  field
    Method  : Set
    Result  : (m : Method) → Set
open Interface public

-- A simple object just returns for a method the response
-- and the object itself
record Object (i : Interface) : Set where
  coinductive
  field
    objectMethod : (m : Method i) → Result i m × Object i

open Object public

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Equality where

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

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

-- so that we know to parse
infixr 40 _::_

-- some hacks 'cuz we don't do pragmas
one : Nat
one = suc zero

two : Nat
two = suc (suc zero)

three : Nat
three = suc (suc (suc zero))

3things : Vec Nat three
3things = zero :: one :: zero :: []

3things' : Vec Nat (one + two)
3things' = 3things

-- getting boring aint it?
3things'' : Vec Nat (two + one)
3things'' = 3things'

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
{-# OPTIONS --show-implicit #-}
{-# OPTIONS -v tc.interaction:20 #-}

------------------------------------------------------------------------
-- Library

id : ∀ {X : Set} → X → X
id x = x

infixr 9 _∘_

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

record Σ (X : Set) (Y : X → Set) : Set where
  constructor _,_
  field
    proj₁ : X
    proj₂ : Y proj₁

open Σ public

syntax Σ X (λ x → Y) = Σ[ x ∈ X ] Y

data _≡_ {X : Set} (x : X) : X → Set where
  refl : x ≡ x

subst : ∀ {A} (P : A → Set) {x y} → x ≡ y → P x → P y
subst P refl p = p

record _▷_ (I O : Set) : Set₁ where
  constructor _◃_/_
  field
    Parameter  : (o : O) → Set
    Arity      : ∀ {o} (p : Parameter o) → Set
    input      : ∀ {o} (p : Parameter o) (a : Arity p) → I

open _▷_ public

Pow : Set → Set₁
Pow X = X → Set

infix 4 _⊆_

_⊆_ : ∀ {X} → Pow X → Pow X → Set
P ⊆ Q = ∀ {x} → P x → Q x

⟦_⟧ : ∀ {I O} → I ▷ O → (Pow I → Pow O)
⟦ P ◃ A / s ⟧ X o = Σ[ p ∈ P o ] ((a : A p) → X (s p a))

Alg : ∀ {O} → O ▷ O → Pow O → Set
Alg Σ X = ⟦ Σ ⟧ X ⊆ X

module _ {I₁ I₂ O₁ O₂} where

  record ContainerMorphism
         (C₁ : I₁ ▷ O₁) (C₂ : I₂ ▷ O₂)
         (f : I₁ → I₂) (g : O₁ → O₂)
         (_∼_ : I₂ → I₂ → Set) (_≈_ : Set → Set → Set)
         (_·_ : ∀ {A B} → A ≈ B → A → B) :
         Set where
    field
      parameter  : Parameter C₁ ⊆ Parameter C₂ ∘ g
      arity      : ∀ {o} {p₁ : Parameter C₁ o} →
                   Arity C₂ (parameter p₁) ≈ Arity C₁ p₁
      coherent   : ∀ {o} {p₁ : Parameter C₁ o} {a₂ : Arity C₂ (parameter p₁)} →
                   f (input C₁ p₁ (arity · a₂)) ∼ input C₂ (parameter p₁) a₂

  open ContainerMorphism public

  _⇒[_/_]_ : I₁ ▷ O₁ → (I₁ → I₂) → (O₁ → O₂) →
             I₂ ▷ O₂ → Set
  C₁ ⇒[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_  (λ R₂ R₁ → R₂ → R₁)
                                                      (λ f x → f x)

⟪_⟫ : ∀ {I} {C₁ C₂ : I ▷ I} →
      C₁ ⇒[ id / id ] C₂ → (X : Pow I) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
⟪ m ⟫ X (c , k) = parameter m c , λ a₂ →
  subst X (coherent m) (k (arity m a₂))

------------------------------------------------------------------------
-- Example

weaken : ∀ {I} {Ω : I ▷ I} {Ψ : I ▷ I} {X : Pow I} →
         Alg Ψ X → Ω ⇒[ id / id ] Ψ → Alg Ω X
weaken {I}{Ω}{Ψ}{X = X} φ m {i} (p , k) = φ {x = i} (⟪ m ⟫ {!X!} (p , k))

weaken2 : ∀ {I} {Ω : I ▷ I} {Ψ : I ▷ I} {X : Pow I} →
          Alg Ψ X → Ω ⇒[ id / id ] Ψ → Alg Ω X
weaken2 {I}{Ω}{Ψ}{X = X} φ m {i} (p , k) = φ {i} (⟪ m ⟫ X (p , k))


text:
{-# OPTIONS -v impossible:10 #-}
-- Andreas, 2021-05-12, issue #5379
module ImpossibleVerboseReduceM where

-- Note: keep ReduceM as first word after IMPOSSIBLE!
{-# IMPOSSIBLE ReduceM should also print this debug message. #-}

-- Should print the text after IMPOSSIBLE and then raise an internal error.

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2014-03-27 fixed issue

{-# OPTIONS --copatterns --sized-types #-}

open import Common.Size

mutual
  data D (i : Size) : Set where
    inn : R i → D i

  record R (i : Size) : Set where
    -- Note: not coinductive
    field
      force : (j : Size< i) → D j
open R

inh : (i : Size) → R i
force (inh i) j = inn (inh j)

-- inh should be rejected by termination checker

data ⊥ : Set where

elim : D ∞ → ⊥
elim (inn r) = elim (force r ∞)

absurd : ⊥
absurd = elim (inn (inh ∞))

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Issue276 where

boo : {S T : Set}(f : S -> T)(x y : S) ->
      ((P : S -> Set) -> P x -> P y) ->
       (P : T -> Set) -> P (f x) -> P (f y)
boo = \ f x y q P -> q (\ s -> P (f s))

record Pack (S : Set) : Set where
  constructor pack
  field
    unpack : S

open Pack

unpack' : {S : Set} -> Pack S -> S
unpack' (pack s) = s

foo : {S : Set}(x : Pack S)(P : Pack S -> Set) -> P (pack (unpack x)) -> P x
foo = \ x P p -> p

goo : {S : Set}(x : Pack S)(P : S -> Set) -> P (unpack x) -> P (unpack' x)
goo = \ x -> boo unpack' (pack (unpack x)) x (foo x)

{- normal form of goo is \ x P p -> p -}

goo' : {S : Set}(x : Pack S)(P : S -> Set) -> P (unpack x) -> P (unpack' x)
goo' = \ x P p -> p
{-
/Users/conor/Desktop/fooling/RecConBug.agda:27,19-20
unpack x != unpack' x of type .S
when checking that the expression p has type P (unpack' x)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Reduction where

open import Prelude
open import Lambda
open import Subst
open import Trans

infix 10 _⟶β_

data _⟶β_ : forall {Γ τ} -> (t u : Term Γ τ) -> Set where
  β   : forall {Γ σ τ}{t : Term (Γ , σ) τ} Δ {u : Term (Γ ++ Δ) σ} ->
        (ƛ t) ↑ Δ • u ⟶β t ↑ Δ / [ Δ ⟵ u ]
  wk⟶ : forall {Γ σ τ}{t₁ t₂ : Term Γ τ} ->
        t₁ ⟶β t₂ -> wk {σ = σ} t₁ ⟶β wk t₂
  •⟶L : forall {Γ σ τ}{t₁ t₂ : Term Γ (σ ⟶ τ)}{u : Term Γ σ} ->
        t₁ ⟶β t₂ -> t₁ • u ⟶β t₂ • u
  •⟶R : forall {Γ σ τ}{t : Term Γ (σ ⟶ τ)}{u₁ u₂ : Term Γ σ} ->
        u₁ ⟶β u₂ -> t • u₁ ⟶β t • u₂
  ƛ⟶  : forall {Γ σ τ}{t₁ t₂ : Term (Γ , σ) τ} ->
        t₁ ⟶β t₂ -> ƛ t₁ ⟶β ƛ t₂

_⟶β*_ : {Γ : Ctx}{τ : Type}(x y : Term Γ τ) -> Set
x ⟶β* y = [ _⟶β_ ]* x y

↑⟶β : {Γ : Ctx}(Δ : Ctx){τ : Type}{t u : Term Γ τ} ->
         t ⟶β u ->  t ↑ Δ ⟶β u ↑ Δ
↑⟶β ε       r = r
↑⟶β (Δ , σ) r = wk⟶ (↑⟶β Δ r)


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Task B
------------------------------------------------------------------------------

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

module DistributiveLaws.TaskB-HalvedStepsATP where

open import DistributiveLaws.Base

open import Common.FOL.Relation.Binary.EqReasoning

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

-- We prove the half of the proof steps (skipping the even ones) of
-- DistributiveLaws.TaskB-I using the ATPs.

prop₂ : ∀ u x y z →
        (x · y · (z · u)) · ((x · y · (z · u)) · (x · z · (y · u))) ≡
          x · z · (y · u)
prop₂ u x y z =

-- The numbering of the proof step justifications are associated with
-- the numbers used in DistributiveLaws.TaskB-I.

  xy·zu · (xy·zu · xz·yu)                                       ≡⟨ j₁₋₃ ⟩
  xy·zu · (x·zu · xz·yu · (y·zu · xz·yu))                       ≡⟨ j₃₋₅ ⟩
  xy·zu · (xz · xu·yu · (y·zu · xz·yu))                         ≡⟨ j₅₋₇ ⟩
  xy·zu · (xz · xyu · (yz·yu · xz·yu))                          ≡⟨ j₇₋₉ ⟩
  xy·zu · (xz · xyu · (yxz · yu))                               ≡⟨ j₉₋₁₁ ⟩
  xy·zu · (xz · xyu · (y·xu · z·yu))                            ≡⟨ j₁₁₋₁₃ ⟩
  xz·yz · xyu · (xz · xyu · (y·xu · z·yu))                      ≡⟨ j₁₃₋₁₅ ⟩
  xz · xyu · (yz · xyu · (y·xu · z·yu))                         ≡⟨ j₁₅₋₁₇ ⟩
  xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu))          ≡⟨ j₁₇₋₁₉ ⟩
  xz · xyu ·
  (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))   ≡⟨ j₁₉₋₂₁ ⟩
  xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu)))       ≡⟨ j₂₁₋₂₃ ⟩
  xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))          ≡⟨ j₂₃₋₂₅ ⟩
  (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))               ≡⟨ j₂₅₋₂₇ ⟩
  xz · xyu · (y · xu·zu · (zy·xu · zy·zu))                      ≡⟨ j₂₇₋₂₉ ⟩
  xz · xyu · (y·zy · xu·zu)                                     ≡⟨ j₂₉₋₃₁ ⟩
  xz·xy · xzu · (y·zy · xzu)                                    ≡⟨ j₃₁₋₃₃ ⟩
  x·zy · y·zy · xzu                                             ≡⟨ j₃₃₋₃₅ ⟩
  xzy · xzu                                                     ≡⟨ j₃₅ ⟩
  xz·yu                                                         ∎
  where
  -- Two variables abbreviations

  xz = x · z
  yu = y · u
  yz = y · z
  zy = z · y
  {-# ATP definitions xz yu yz zy #-}

  -- Three variables abbreviations

  xyu = x · y · u
  xzu = x · z · u
  xzy = x · z · y
  yxz = y · x · z
  {-# ATP definitions xyu xzu xzy yxz #-}

  x·zu = x · (z · u)
  x·zy = x · (z · y)
  {-# ATP definitions x·zu x·zy #-}

  y·xu = y · (x · u)
  y·yu = y · (y · u)
  y·zu = y · (z · u)
  y·zy = y · (z · y)
  {-# ATP definitions y·xu y·yu y·zu y·zy #-}

  z·xu = z · (x · u)
  z·yu = z · (y · u)
  {-# ATP definitions z·xu z·yu #-}

  -- Four variables abbreviations

  xu·yu = x · u · (y · u)
  xu·zu = x · u · (z · u)
  {-# ATP definitions xu·yu xu·zu #-}

  xy·zu = x · y · (z · u)
  {-# ATP definition xy·zu #-}

  xz·xy = x · z · (x · y)
  xz·yu = x · z · (y · u)
  xz·yz = x · z · (y · z)
  {-# ATP definitions xz·xy xz·yu xz·yz #-}

  yz·yu = y · z · (y · u)
  {-# ATP definition yz·yu #-}

  zy·xu = z · y · (x · u)
  zy·zu = z · y · (z · u)
  {-# ATP definitions zy·xu zy·zu #-}

  -- Steps justifications

  postulate j₁₋₃ : xy·zu · (xy·zu · xz·yu) ≡
                   xy·zu · (x·zu · xz·yu · (y·zu · xz·yu))
  {-# ATP prove j₁₋₃ #-}

  postulate j₃₋₅ : xy·zu · (x·zu · xz·yu · (y·zu · xz·yu)) ≡
                   xy·zu · (xz · xu·yu · (y·zu · xz·yu))
  {-# ATP prove j₃₋₅ #-}

  postulate j₅₋₇ : xy·zu · (xz · xu·yu · (y·zu · xz·yu)) ≡
                   xy·zu · (xz · xyu · (yz·yu · xz·yu))
  {-# ATP prove j₅₋₇ #-}

  postulate j₇₋₉ : xy·zu · (xz · xyu · (yz·yu · xz·yu)) ≡
                   xy·zu · (xz · xyu · (yxz · yu))
  {-# ATP prove j₇₋₉ #-}

  postulate j₉₋₁₁ : xy·zu · (xz · xyu · (yxz · yu)) ≡
                    xy·zu · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₉₋₁₁ #-}

  postulate j₁₁₋₁₃ : xy·zu · (xz · xyu · (y·xu · z·yu)) ≡
                     xz·yz · xyu · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₁₋₁₃ #-}

  postulate j₁₃₋₁₅ : xz·yz · xyu · (xz · xyu · (y·xu · z·yu)) ≡
                     xz · xyu · (yz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₃₋₁₅ #-}

  postulate j₁₅₋₁₇ : xz · xyu · (yz · xyu · (y·xu · z·yu)) ≡
                     xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu))
  {-# ATP prove j₁₅₋₁₇ #-}

  postulate j₁₇₋₁₉ : xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu)) ≡
                     xz · xyu ·
                    (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₁₇₋₁₉ #-}

  postulate
    j₁₉₋₂₁ : xz · xyu ·
             (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
             xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₁₉₋₂₁ #-}

  postulate
    j₂₁₋₂₃ : xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu))) ≡
             xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₂₁₋₂₃ #-}

  postulate j₂₃₋₂₅ : xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu))) ≡
                     (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))
  {-# ATP prove j₂₃₋₂₅ #-}

  postulate j₂₅₋₂₇ : (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu)) ≡
                     xz · xyu · (y · xu·zu · (zy·xu · zy·zu))
  {-# ATP prove j₂₅₋₂₇ #-}

  postulate j₂₇₋₂₉ : xz · xyu · (y · xu·zu · (zy·xu · zy·zu)) ≡
                     xz · xyu · (y·zy · xu·zu)
  {-# ATP prove j₂₇₋₂₉ #-}

  postulate j₂₉₋₃₁ : xz · xyu · (y·zy · xu·zu) ≡
                     xz·xy · xzu · (y·zy · xzu)
  {-# ATP prove j₂₉₋₃₁ #-}

  postulate j₃₁₋₃₃ : xz·xy · xzu · (y·zy · xzu) ≡
                     x·zy · y·zy · xzu
  {-# ATP prove j₃₁₋₃₃ #-}

  postulate j₃₃₋₃₅ : x·zy · y·zy · xzu ≡ xzy · xzu
  {-# ATP prove j₃₃₋₃₅ #-}

  postulate j₃₅ : xzy · xzu ≡ xz·yu
  {-# ATP prove j₃₅ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Two out-of-scope variables are given the same name #3678

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

postulate
  A : Set
  B : A → Set
  a : A

Pi : (A → Set) → Set
Pi B = {x : A} → B x

foo : Pi \ y →  Σ (B y) \ _ → Pi \ z → Σ (y ≡ a → B z) \ _ → B y → B z → A
foo = {!!} , (\ { refl → {!!} }) , {!!}

-- Expected:
-- ...
-- ?2 : B x₁ → B x₂ → A  (not the same name for these variables)


text:
-- Long version, the final version is Nat.agda
module NatTry where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

one two three four : ℕ
one   = suc zero
two   = suc one
three = suc two
four  = suc three

_+_ : ℕ → ℕ → ℕ
zero  + b = b
suc a + b = suc (a + b)

data Bool : Set where
  true  : Bool
  false : Bool

_≟_ : ℕ → ℕ → Bool
zero  ≟ zero  = true
suc a ≟ suc b = a ≟ b
_     ≟ _     = false

infix 4 _≟_

assocProp : ℕ → ℕ → ℕ → Bool
assocProp a b c =  (a + b) + c ≟ a + (b + c)

reflProp : ℕ → Bool
reflProp n =  n ≟ n

module isTrue-direct where

  data isTrue : Bool → Set where
    ok : isTrue true

  unitTest : isTrue (assocProp one one two)
  unitTest = ok

  refl-True : (n : ℕ) → isTrue (reflProp n)
  refl-True zero = ok
  refl-True (suc n) = refl-True n

  assocProp-zero-True : (n m : ℕ) → isTrue (assocProp zero n m)
  assocProp-zero-True n m = refl-True (n + m)

  assocProp-True : (n m k : ℕ) → isTrue (assocProp n m k)
  assocProp-True zero    m k = assocProp-zero-True m k
  assocProp-True (suc n) m k = assocProp-True n m k

-------- switch to _≡_

module ≡-Bool where

  -- propositional equalitiy on Bool
  data _≡_ : Bool → Bool → Set where
    refl : {a : Bool} → a ≡ a  -- the Bool paramter is hidden

  infix 4 _≡_

  isTrue : Bool → Set
  isTrue x = x ≡ true

-- generic propositional equality
data _≡_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≡ a

infix 4 _≡_

-- This is the type of the refl constructor
-- The parameters are hidden
refl′ : {A : Set} {a : A} → a ≡ a
refl′ = refl

isTrue : Bool → Set
isTrue x = x ≡ true

refl-True : (n : ℕ) → isTrue (reflProp n)
refl-True zero = refl
refl-True (suc n) = refl-True n

unitTest : isTrue (assocProp one one two)
unitTest = refl

assocProp-zero-True : (n m : ℕ) → isTrue (assocProp zero n m)
assocProp-zero-True n m = refl-True (n + m)

assocProp-True : (n m k : ℕ) → isTrue (assocProp n m k)
assocProp-True zero    m k = assocProp-zero-True m k
assocProp-True (suc n) m k = assocProp-True n m k

---- switch from _≟_

cong : {A B : Set} {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl

cong-suc : {a b : ℕ} → a ≡ b → suc a ≡ suc b
cong-suc = cong suc

≡-to-≟ : {a b : ℕ} → a ≡ b → isTrue (a ≟ b)
≡-to-≟ {a} refl = refl-True a

≟-to-≡ : (a b : ℕ) → isTrue (a ≟ b) → a ≡ b
≟-to-≡ zero zero i = refl
≟-to-≡ zero (suc b) ()
≟-to-≡ (suc a) zero ()
≟-to-≡ (suc a) (suc b) i = cong-suc (≟-to-≡ a b i)

-- the rest is in Nat.agda

max_stars_repo_name: divipp/agda-intro-prezi

max_issues_repo_name: divipp/agda-intro-prezi

max_forks_repo_name: divipp/agda-intro-prezi


text:
------------------------------------------------------------------------
-- η-expansion of simply-kinded types in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Simple.EtaExpansion where

open import Data.Fin using (Fin; zero; suc; raise; lift)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.List using ([]; _∷_; _∷ʳ_)
open import Data.Maybe using (Maybe)
open import Data.Nat using (zero; suc)
open import Data.Product as Prod using (_,_)
open import Data.Vec as Vec using ([])
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Syntax.WeakEquality
open import FOmegaInt.Kinding.Simple

------------------------------------------------------------------------
-- η-expansion of simply kinded types.
--
-- TODO: explain the point of this and how "simple" kinding differs
-- from "canonical" kinding.

open Syntax
open SimpleCtx
open Substitution hiding (_↑; _↑⋆_; sub; subst)
open SimpHSubstLemmas
open RenamingCommutes
open WeakHereditarySubstitutionEquality
open WeakEqEtaExpansion
open KindedRenaming
open KindedHereditarySubstitution
open Kinding

module TrackSimpleKindsKindedEtaExp where
  private
    module V  = VarSubst
    module TK = TrackSimpleKindsEtaExp

  -- NOTE. The definition of the functions η-exp-Var∈ and η-exp-Ne∈
  -- below are structurally recursive in the *shape* parameter k, but
  -- *not* in the kind j because we need to weaken the domain j₁ of
  -- the dependent kind (j = Π j₁ j₂) in the arrow case.  The
  -- additional hypothesis ⌊ j ⌋≡ k ensures that k is indeed the shape
  -- of the kind j.

  mutual

    -- η-expansion preserves simple kinding of neutral types.

    η-exp-Var∈ : ∀ {n} {Γ : Ctx n} {x j k} (hyp : ⌊ j ⌋≡ k) →
                 Γ ⊢ j kds → Γ ⊢Var x ∈ k →
                 Γ ⊢Nf TK.η-exp j hyp (var∙ x) ∈ k
    η-exp-Var∈ hyp j-kd x∈k = η-exp-Ne∈ hyp j-kd (∈-∙ x∈k ∈-[])

    η-exp-Ne∈ : ∀ {n} {Γ : Ctx n} {a j k} (hyp : ⌊ j ⌋≡ k) →
                Γ ⊢ j kds → Γ ⊢Ne a ∈ k → Γ ⊢Nf TK.η-exp j hyp a ∈ k
    η-exp-Ne∈ is-★ (kds-⋯ b∈* c∈*) a∈★ = ∈-ne a∈★
    η-exp-Ne∈ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) (kds-Π j₁-kds j₂-kds)
              (∈-∙ {x} {_} {_} {as} x∈l l∋as∈k₁⇒k₂) =
      subst (λ j → _ ⊢Nf η-x∙as ∈ j ⇒ _) (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁)
            (∈-Π-i j₁-kds (η-exp-Ne∈ ⌊j₂⌋≡k₂ j₂-kds x∙as·z∈k₂))
      where
        η-x∙as = TK.η-exp _ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) (var x ∙ as)
        z∈k₁ = η-exp-Var∈ (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (kds-weaken j₁-kds)
                          (∈-var zero (cong kd (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁)))
        x∙as·z∈k₂ = Ne∈-Π-e (Ne∈-weaken (∈-∙ x∈l l∋as∈k₁⇒k₂)) z∈k₁

  mutual

    -- η-expansion of neutrals followed by hereditary substitution
    -- vanishes if the substitution hits the head of the neutral.

    η-exp-var-Hit-/⟨⟩ : ∀ {k m n Γ Δ} {x a j} (hyp : ⌊ j ⌋≡ k) {σ : SVSub m n} →
                       Hit σ x a → Γ ⊢ j kds → Γ ⊢Var x ∈ k → Δ ⊢/⟨ k ⟩ σ ∈ Γ →
                       TK.η-exp j hyp (var∙ x) /⟨ k ⟩ σ  ≈  var∙ x /⟨ k ⟩ σ
    η-exp-var-Hit-/⟨⟩ hyp hitP j-kds x∈k σ∈Γ =
      η-exp-ne-Hit-/⟨⟩ hyp hitP j-kds (∈-∙ x∈k ∈-[]) σ∈Γ

    η-exp-ne-Hit-/⟨⟩ : ∀ {k l m n Γ Δ} {x a as j} (hyp : ⌊ j ⌋≡ k)
                       {σ : SVSub m n} → Hit σ x a → Γ ⊢ j kds →
                       Γ ⊢Ne var x ∙ as ∈ k → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                       TK.η-exp j hyp (var x ∙ as) /⟨ l ⟩ σ  ≈
                         var x ∙ as /⟨ l ⟩ σ
    η-exp-ne-Hit-/⟨⟩ is-★ hitP j-kds a∈k σ∈Γ = ≈-refl _
    η-exp-ne-Hit-/⟨⟩ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) hitP
                     (kds-Π j₁-kds j₂-kds) (∈-∙ {as = as} x∈l l∋as∈k₁⇒k₂) σ∈Γ
      with lookup-/⟨⟩∈-Hit σ∈Γ x∈l hitP
    η-exp-ne-Hit-/⟨⟩ {l = l} {Γ = Γ} {a = a}
                     (is-⇒ {j₁} {j₂} {k₁} {k₂} ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) {σ} hitP
                     (kds-Π j₁-kds j₂-kds)
                     (∈-∙ {as = as} (∈-var {l} x Γ[x]≡kd-l) l∋as∈k₁⇒k₂) σ∈Γ
                   | a∈l , refl =
      let hitP-σ↑ = hitP ↑
          ηz      = TK.η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)
          as′     = weakenSpine as
          ηz∈k₁   = η-exp-Var∈ (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (kds-weaken j₁-kds)
                               (∈-var zero refl)
          kd-l∷Γ[x+1]≡kd-l = trans (lookup-suc (kd l) Γ x) Γ[x]≡kd-l
          x+1∈l            = ∈-var (suc x) kd-l∷Γ[x+1]≡kd-l
          l∋as∈k₁⇒k₂′      = Sp∈-weaken l∋as∈k₁⇒k₂
          σ↑∈k₁∷Γ          = ∈-H↑ σ∈Γ
          l∋as//σ∈k₁⇒k₂    = Sp∈-/⟨⟩ l∋as∈k₁⇒k₂ σ∈Γ
          a∙as/σ∈k₁⇒k₂     = Nf∈-∙∙ a∈l l∋as//σ∈k₁⇒k₂
          j′ , a′ , j′-kds , a′∈k₁⇒k₂ , rest = Nf∈-⇒-inv a∙as/σ∈k₁⇒k₂
          ⌊j′⌋≡k₁ , a∙as/σ≡Λj′a′             = rest
          ⌊j₁/σ⌋≡⌊j′⌋ = let open ≡-Reasoning in begin
            ⌊ j₁ Kind/⟨ l ⟩ σ ⌋  ≡⟨ ⌊⌋-Kind/⟨⟩ j₁ ⟩
            ⌊ j₁ ⌋               ≡⟨ ⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁ ⟩
            k₁                   ≡⟨ sym ⌊j′⌋≡k₁ ⟩
            ⌊ j′ ⌋               ∎
          open ≈-Reasoning
      in begin
        TK.η-exp (Π j₁ j₂) (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) (var x ∙ as) /⟨ l ⟩ σ
      ≈⟨ ≈-Λ∙ ⌊j₁/σ⌋≡⌊j′⌋ (begin
          TK.η-exp j₂ ⌊j₂⌋≡k₂
            (weakenElim (var x ∙ as) ⌜·⌝ ηz) /⟨ l ⟩ σ ↑
        ≡⟨ cong (λ y → TK.η-exp _ ⌊j₂⌋≡k₂ (var y ∙ as′ ⌜·⌝ ηz) /⟨ l ⟩ σ ↑)
                (VarLemmas.lookup-wk x) ⟩
          TK.η-exp j₂ ⌊j₂⌋≡k₂ (var (suc x) ∙ as′ ⌜·⌝ ηz) /⟨ l ⟩ σ ↑
        ≈⟨ η-exp-ne-Hit-/⟨⟩ ⌊j₂⌋≡k₂ hitP-σ↑
                            (subst (λ k → kd k ∷ _ ⊢ _ kds) (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁)
                                   j₂-kds)
                            (∈-∙ x+1∈l (∈-∷ʳ l∋as∈k₁⇒k₂′ ηz∈k₁)) σ↑∈k₁∷Γ ⟩
          var (suc x) ∙ as′ ⌜·⌝ ηz /⟨ l ⟩ σ ↑
        ≡⟨ cong (_?∙∙⟨ l ⟩ ((as′ ∷ʳ ηz) //⟨ l ⟩ σ ↑)) (lookup-Hit hitP-σ↑) ⟩
          weakenElim a ∙∙⟨ l ⟩ ((as′ ∷ʳ ηz) //⟨ l ⟩ σ ↑)
        ≡⟨ cong (_ ∙∙⟨ l ⟩_) (++-//⟨⟩ (as′) (_ ∷ [])) ⟩
          weakenElim a ∙∙⟨ l ⟩ (as′ //⟨ l ⟩ σ ↑ ∷ʳ ηz /⟨ l ⟩ σ ↑)
        ≡⟨ Nf∈-++-∙∙⟨⟩ (Nf∈-weaken a∈l) (Sp∈-/⟨⟩ l∋as∈k₁⇒k₂′ σ↑∈k₁∷Γ)
                       (∈-∷ (Nf∈-/⟨⟩ ηz∈k₁ σ↑∈k₁∷Γ) ∈-[]) ⟩
          weakenElim a ∙∙⟨ l ⟩ (as′ //⟨ l ⟩ σ ↑) ⌜·⌝⟨ k₁ ⇒ k₂ ⟩ (ηz /⟨ l ⟩ σ ↑)
        ≡⟨ cong (λ bs → weakenElim a ∙∙⟨ l ⟩ bs ⌜·⌝⟨ k₁ ⇒ k₂ ⟩ (ηz /⟨ l ⟩ σ ↑))
                (wk-//⟨⟩-↑⋆ 0 as) ⟩
          weakenElim a ∙∙⟨ l ⟩ weakenSpine (as //⟨ l ⟩ σ) ⌜·⌝⟨ k₁ ⇒ k₂ ⟩
            (ηz /⟨ l ⟩ σ ↑)
        ≡˘⟨ cong (_⌜·⌝⟨ k₁ ⇒ k₂ ⟩ (ηz /⟨ l ⟩ σ ↑))
                 (∙∙⟨⟩-/Var a l (as //⟨ l ⟩ σ)) ⟩
          weakenElim (a ∙∙⟨ l ⟩ (as //⟨ l ⟩ σ)) ⌜·⌝⟨ k₁ ⇒ k₂ ⟩ (ηz /⟨ l ⟩ σ ↑)
        ≡⟨ cong ((_⌜·⌝⟨ k₁ ⇒ k₂ ⟩ _) ∘ weakenElim) a∙as/σ≡Λj′a′ ⟩
          weakenElim (Λ∙ j′ a′) ⌜·⌝⟨ k₁ ⇒ k₂ ⟩ (ηz /⟨ l ⟩ σ ↑)
        ≡⟨ cong (weakenElim (Λ∙ j′ a′) ⌜·⌝⟨ k₁ ⇒ k₂ ⟩_)
                (TK.η-exp-ne-Miss-/⟨⟩ zero zero (⌊⌋≡-weaken ⌊j₁⌋≡k₁) under) ⟩
          weakenElim (Λ∙ j′ a′) ⌜·⌝⟨ k₁ ⇒ k₂ ⟩
            TK.η-exp (weakenKind′ j₁ Kind/⟨ l ⟩ σ ↑) (⌊⌋≡-/⟨⟩ (⌊⌋≡-weaken ⌊j₁⌋≡k₁))
                     (var∙ zero)
        ≈⟨ Nf∈-[]-η-var [] (⌊⌋≡-/⟨⟩ (⌊⌋≡-weaken ⌊j₁⌋≡k₁))
                        (kds-/⟨⟩ (kds-weaken j₁-kds) σ↑∈k₁∷Γ) a′∈k₁⇒k₂ ⟩
          a′
        ∎) ⟩
        Λ∙ j′ a′
      ≡⟨ sym a∙as/σ≡Λj′a′ ⟩
        a ∙∙⟨ l ⟩ (as //⟨ l ⟩ σ)
      ≡˘⟨ cong (_?∙∙⟨ l ⟩ (as //⟨ l ⟩ σ)) (lookup-Hit hitP) ⟩
        var x ∙ as /⟨ l ⟩ σ
      ∎

    -- Hereditary substitutions of a variable by its η-expansion vanish.
    --
    -- NOTE.  Both the statement and the proof of this lemma are
    -- complicated by the use of de Bruijn notation in combination
    -- with single-variable (hereditary) substitution.  When
    -- formulated using the usual, human-readable variable notation,
    -- the lemma simply says that
    --
    --   e [ηⱼ(x)/ʲx] = e
    --
    -- where "e [a/ʲx]" denotes hereditary substitution of a for x in
    -- expression e at kind j, and "ηⱼ(x)" denotes the η-expansion of
    -- x at kind j.  Using de Bruijn notation, this substitution only
    -- makes sense if there are actually _two_ copies of the variable
    -- x in e on the LHS (say x and x′): one to be replaced (x) and a
    -- second one (x′) to be η-expanded and substituted for x.  To
    -- make the equation well-scoped, we therefore weaken e to
    -- introduce a new variable x′ = (suc x) just after x, which after
    -- substitution for x will correspond precisely to the de Bruijn
    -- index of x itself.  The stated form of the lemma is obtained by
    -- letting x be the n-th variable in a context with (n + m) free
    -- variables, i.e. we fix x = (raise n zero) in e.
    --
    -- Note also that the proof of this lemma is currently the only
    -- place in the development where the Eq? predicate from the
    -- FOmegaInt.Syntax.SingleVariableSubstitution module is used.
    -- It's probably possible to reformulate the proof without using
    -- this predicate, but that will likely render the proof even
    -- harder to follow than it already is.

    kds-[]-η-var : ∀ {k m n} (Γ₂ : CtxExt (suc m) n) {Γ₁ j l}
                   (hyp : ⌊ j ⌋≡ k) → kd k ∷ Γ₁ ⊢ j kds →
                   Γ₂ ++ kd k ∷ Γ₁ ⊢ l kds →
                   let l′ = l Kind′/Var (V.wk V.↑) V.↑⋆ n
                   in l′ Kind/⟨ k ⟩ sub (TK.η-exp j hyp (var∙ zero)) ↑⋆ n ≋ l
    kds-[]-η-var Γ₂ hyp j-kds (kds-⋯ a∈★ b∈★) =
      ≋-⋯ (Nf∈-[]-η-var Γ₂ hyp j-kds a∈★) (Nf∈-[]-η-var Γ₂ hyp j-kds b∈★)
    kds-[]-η-var Γ₂ hyp j-kds (kds-Π k-kds l-kds) =
      ≋-Π (kds-[]-η-var Γ₂ hyp j-kds k-kds)
          (kds-[]-η-var (_ ∷ Γ₂) hyp j-kds l-kds)

    Nf∈-[]-η-var : ∀ {k m n} (Γ₂ : CtxExt (suc m) n) {Γ₁ a j l}
                   (hyp : ⌊ j ⌋≡ k) → kd k ∷ Γ₁ ⊢ j kds →
                   Γ₂ ++ kd k ∷ Γ₁ ⊢Nf a ∈ l →
                   let a′ = a Elim/Var (V.wk V.↑) V.↑⋆ n
                   in a′ /⟨ k ⟩ sub (TK.η-exp j hyp (var∙ zero)) ↑⋆ n ≈ a
    Nf∈-[]-η-var Γ₂ hyp j-kds ∈-⊥-f = ≈-refl ⊥∙
    Nf∈-[]-η-var Γ₂ hyp j-kds ∈-⊤-f = ≈-refl ⊤∙
    Nf∈-[]-η-var Γ₂ hyp j-kds (∈-∀-f k-kds a∈★) =
      ≈-∀∙ (kds-[]-η-var Γ₂ hyp j-kds k-kds)
           (Nf∈-[]-η-var (_ ∷ Γ₂) hyp j-kds a∈★)
    Nf∈-[]-η-var Γ₂ hyp j-kds (∈-→-f a∈★ b∈★) =
      ≈-⇒∙ (Nf∈-[]-η-var Γ₂ hyp j-kds a∈★) (Nf∈-[]-η-var Γ₂ hyp j-kds b∈★)
    Nf∈-[]-η-var {k} {_} {n} Γ₂ hyp j-kds (∈-Π-i {l} l-kds a∈k) =
      let open ≡-Reasoning
          ρ = (V.wk V.↑) V.↑⋆ n
          σ = sub (TK.η-exp _ hyp (var∙ zero)) ↑⋆ n
      in ≈-Λ∙ (begin
             ⌊ l Kind′/Var ρ Kind/⟨ k ⟩ σ ⌋  ≡⟨ ⌊⌋-Kind/⟨⟩ (l Kind′/Var ρ) ⟩
             ⌊ l Kind′/Var ρ ⌋               ≡⟨ ⌊⌋-Kind′/Var l ⟩
             ⌊ l ⌋                           ∎)
           (Nf∈-[]-η-var (_ ∷ Γ₂) hyp j-kds a∈k)
    Nf∈-[]-η-var {_} {_} {n} Γ₂ hyp j-kds (∈-ne (∈-∙ (∈-var x _) k∋as∈★))
      with compare n x
    Nf∈-[]-η-var {k} {_} {n} Γ₂ {Γ₁} {_} {j} hyp j-kds
                 (∈-ne (∈-∙ {as = as} (∈-var ._ Γ[x]≡kd-k′) k′∋as∈★))
      | yes refl =
      begin
        lookupSV σ (x V./ (V.wk V.↑) V.↑⋆ n) ?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)
      ≡⟨ cong (λ z → lookupSV σ z ?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ))
              (lookup-raise-↑⋆ n zero refl) ⟩
        lookupSV σ (raise n zero) ?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)
      ≡⟨ cong (_?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)) (lookup-Hit hitP) ⟩
        weakenElim⋆ n ηz ∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)
      ≡˘⟨ cong (_∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)) (EL./Var-wk⋆ n) ⟩
        (ηz Elim/Var V.wk⋆ n) ∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)
      ≈⟨ ≈-∙∙⟨⟩ k (≈-refl _) (Sp∈-[]-η-var Γ₂ hyp j-kds k∋as∈★) ⟩
        (ηz Elim/Var V.wk⋆ n) ∙∙⟨ k ⟩ as
      ≡⟨ cong (_∙∙⟨ k ⟩ as) (TK.η-exp-/Var hyp (var∙ zero)) ⟩
        TK.η-exp (j Kind′/Var V.wk⋆ n) (⌊⌋≡-/Var hyp)
                 (var∙ zero Elim/Var V.wk⋆ n) ∙∙⟨ k ⟩ as
      ≡⟨ cong (λ y → TK.η-exp (j Kind′/Var V.wk⋆ n) (⌊⌋≡-/Var hyp)
                              (var∙ y) ∙∙⟨ k ⟩ as)
              (lookup-wk⋆ zero n) ⟩
        TK.η-exp (j Kind′/Var V.wk⋆ n) (⌊⌋≡-/Var hyp) (var∙ x) ∙∙⟨ k ⟩ as
      ≈⟨ η-exp-ne-∙∙ (⌊⌋≡-/Var hyp)
                     (subst (_ ⊢_kds) (sym (KL./Var-wk⋆ n))
                            (kds-weaken⋆ Γ₂ j-kds))
                     (∈-∙ (∈-var x Γ[x]≡kd-k) ∈-[]) k∋as∈★ ⟩
        var x ∙ as
      ∎
      where
        x = raise n zero
        Γ = Γ₂ ++ kd k ∷ Γ₁

        Γ[x]≡kd-k = begin
          lookup Γ (raise n zero)   ≡⟨ lookup-weaken⋆ n Γ₂ _ zero ⟩
          weakenSAsc⋆ n (kd k)      ≡⟨ weakenSAsc⋆-id n ⟩
          kd k                      ∎
          where open ≡-Reasoning

        ηz     = TK.η-exp j hyp (var∙ zero)
        σ      = sub ηz ↑⋆ n
        as′    = as //Var (V.wk V.↑) V.↑⋆ n
        hitP   = Hit-sub-↑⋆ n
        k′≡k   = kd-inj′ (trans (sym Γ[x]≡kd-k′) Γ[x]≡kd-k)
        k∋as∈★ = subst (_ ⊢_∋∙ _ ∈ _) k′≡k k′∋as∈★

        open ≈-Reasoning
        open ExtLemmas₁ VarLemmas.lemmas₁ using (lookup-wk⋆; lookup-raise-↑⋆)
        module EL = TermLikeLemmas termLikeLemmasElim
        module KL = TermLikeLemmas termLikeLemmasKind′
    Nf∈-[]-η-var {k} {_} {n} Γ₂ {_} {_} {j} hyp j-kds
                 (∈-ne (∈-∙ {as = as} (∈-var ._ Γ[x]≡kd-k′) k′∋as∈★))
      | no y refl =
      begin
        lookupSV σ (x V./ (V.wk V.↑) V.↑⋆ n) ?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)
      ≡⟨ cong (λ z → lookupSV σ z ?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)) eq ⟩
        lookupSV σ (lift n suc x) ?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)
      ≡⟨ cong (_?∙∙⟨ k ⟩ (as′ //⟨ k ⟩ σ)) (lookup-Miss (Miss-sub-↑⋆ n x)) ⟩
        var x ∙ (as′ //⟨ k ⟩ σ)
      ≈⟨ ≈-∙ (≈-var x) (Sp∈-[]-η-var Γ₂ hyp j-kds k′∋as∈★) ⟩
        var x ∙ as
      ∎
      where
        x   = lift n suc y
        ηz  = TK.η-exp j hyp (var∙ zero)
        σ   = sub ηz ↑⋆ n
        as′ = as //Var (V.wk V.↑) V.↑⋆ n

        eq = begin
          x V./ (V.wk V.↑) V.↑⋆ n       ≡⟨ VarLemmas.lookup-wk-↑⋆-↑⋆ 1 n x ⟩
          lift n (lift 1 suc) x               ≡⟨⟩
          lift n (lift 1 suc) (lift n suc y)  ≡⟨ sym (lift-commutes 0 n y) ⟩
          lift n suc (lift n suc y)           ≡⟨⟩
          lift n suc x                        ∎
          where open ≡-Reasoning

        open ≈-Reasoning

    Sp∈-[]-η-var : ∀ {k m n} (Γ₂ : CtxExt (suc m) n) {Γ₁ as j l₁ l₂}
                   (hyp : ⌊ j ⌋≡ k) → kd k ∷ Γ₁ ⊢ j kds →
                   Γ₂ ++ kd k ∷ Γ₁ ⊢ l₁ ∋∙ as ∈ l₂ →
                   let as′ = as //Var (V.wk V.↑) V.↑⋆ n
                   in as′ //⟨ k ⟩ sub (TK.η-exp j hyp (var∙ zero)) ↑⋆ n ≈Sp as
    Sp∈-[]-η-var Γ₂ hyp j-kds ∈-[] = ≈-[]
    Sp∈-[]-η-var Γ₂ hyp j-kds (∈-∷ a∈l₁ l₂∋as∈l₃) =
      ≈-∷ (Nf∈-[]-η-var Γ₂ hyp j-kds a∈l₁) (Sp∈-[]-η-var Γ₂ hyp j-kds l₂∋as∈l₃)

    -- Reducing applications cancel out η-expansion of neutrals.

    η-exp-ne-∙∙ : ∀ {n} {Γ : Ctx n} {a bs j k} (hyp : ⌊ j ⌋≡ k) →
                  Γ ⊢ j kds → Γ ⊢Ne a ∈ k → Γ ⊢ k ∋∙ bs ∈ ★ →
                  TK.η-exp j hyp a ∙∙⟨ k ⟩ bs  ≈  a ∙∙ bs
    η-exp-ne-∙∙ is-★ j-kds a∈k ∈-[] = subst (_ ≈_) (sym (∙∙-[] _)) (≈-refl _)
    η-exp-ne-∙∙ {a = a} (is-⇒ {j₁} {j₂} {k₁} {k₂} ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂)
                (kds-Π j₁-kds j₂-kds) a∈k₁⇒k₂ (∈-∷ {b} {bs} b∈k₁ k₂∋bs∈★) =
      begin
        TK.η-exp (Π j₁ j₂) (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) a ⌜·⌝⟨ k₁ ⇒ k₂ ⟩ b ∙∙⟨ k₂ ⟩ bs
      ≈⟨ ≈-∙∙⟨⟩ k₂ (η-exp-ne-⌜·⌝ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂ j₁-kds a∈k₁⇒k₂ b∈k₁)
                (≈Sp-refl bs) ⟩
        TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (a ⌜·⌝ b) ∙∙⟨ k₂ ⟩ bs
      ≈⟨ η-exp-ne-∙∙ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) j₂[b]-kds (Ne∈-Π-e a∈k₁⇒k₂ b∈k₁) k₂∋bs∈★ ⟩
        (a ⌜·⌝ b) ∙∙ bs
      ≡⟨ ∙∙-++ a (b ∷ []) bs ⟩
        a ∙∙ (b ∷ bs)
      ∎
      where
        open ≈-Reasoning
        j₂[b]-kds = kds-/⟨⟩ (subst (λ k → kd k ∷ _ ⊢ j₂ kds)
                                   (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁) j₂-kds)
                            (∈-hsub b∈k₁)

    η-exp-ne-⌜·⌝ : ∀ {n} {Γ : Ctx n} {a b j₁ j₂ k₁ k₂}
                   (hyp₁ : ⌊ j₁ ⌋≡ k₁) (hyp₂ : ⌊ j₂ ⌋≡ k₂) →
                   Γ ⊢ j₁ kds → Γ ⊢Ne a ∈ k₁ ⇒ k₂ → Γ ⊢Nf b ∈ k₁ →
                   TK.η-exp (Π j₁ j₂) (is-⇒ hyp₁ hyp₂) a ⌜·⌝⟨ k₁ ⇒ k₂ ⟩ b  ≈
                     TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ hyp₂) (a ⌜·⌝ b)
    η-exp-ne-⌜·⌝ {b = b} {j₁} {j₂} {k₁} ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂ j₁-kds
                 (∈-∙ {x} {_} {_} {as} x∈l l∋as∈k₁⇒k₂) b∈k₁ =
      let ηz = TK.η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)
      in begin
        TK.η-exp j₂ ⌊j₂⌋≡k₂
                 (weakenElim (var∙ x) ∙∙ weakenSpine as ⌜·⌝ ηz) /⟨ k₁ ⟩ sub b
      ≡⟨ cong (λ y → TK.η-exp _ ⌊j₂⌋≡k₂ (var y ∙ weakenSpine as ⌜·⌝ ηz) /⟨ k₁ ⟩ _)
              (VarLemmas.lookup-wk x)  ⟩
        TK.η-exp j₂ ⌊j₂⌋≡k₂ (var (suc x) ∙ weakenSpine as ⌜·⌝ ηz) /⟨ k₁ ⟩ sub b
      ≡⟨ TK.η-exp-ne-Miss-/⟨⟩ (suc x) x ⌊j₂⌋≡k₂ over ⟩
        TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
          (var x ∙ ((weakenSpine as ∷ʳ ηz) //⟨ k₁ ⟩ sub b))
      ≡⟨ cong (λ bs → TK.η-exp _ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (var x ∙ bs))
              (++-//⟨⟩ (weakenSpine as) _) ⟩
        TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
          (var x ∙ (weakenSpine as //⟨ k₁ ⟩ sub b) ⌜·⌝ (ηz /⟨ k₁ ⟩ sub b))
      ≡⟨ cong (λ bs → TK.η-exp _ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (var x ∙ bs ⌜·⌝ _))
              (//Var-wk-↑⋆-hsub-vanishes 0 as) ⟩
        TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
                 (var x ∙ as ⌜·⌝ (ηz /⟨ k₁ ⟩ sub b))
      ≈⟨ ≈-η-exp′ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
                  (≈-⌜·⌝ (≈-refl (var x ∙ as))
                         (η-exp-var-Hit-/⟨⟩ (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (Hit-sub-↑⋆ 0)
                                            (kds-weaken j₁-kds)
                                            (∈-var zero refl) (∈-hsub b∈k₁))) ⟩
        TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (var x ∙ as ⌜·⌝
          (var∙ zero /⟨ k₁ ⟩ sub b))
      ≡⟨⟩
        TK.η-exp (j₂ Kind[ b ∈ k₁ ]) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (var x ∙ as ⌜·⌝ b)
      ∎
      where open ≈-Reasoning

private module TK = TrackSimpleKindsKindedEtaExp

-- η-expansion preserves simple kinding of neutral types.

η-exp-Var∈ : ∀ {n} {Γ : Ctx n} {x k} →
             Γ ⊢ k kds → Γ ⊢Var x ∈ ⌊ k ⌋ → Γ ⊢Nf η-exp k (var∙ x) ∈ ⌊ k ⌋
η-exp-Var∈ k-kd x∈⌊k⌋ = TK.η-exp-Var∈ (⌊⌋-⌊⌋≡ _) k-kd x∈⌊k⌋

η-exp-Ne∈ : ∀ {n} {Γ : Ctx n} {a k} →
            Γ ⊢ k kds → Γ ⊢Ne a ∈ ⌊ k ⌋ → Γ ⊢Nf η-exp k a ∈ ⌊ k ⌋
η-exp-Ne∈ k-kd a∈⌊k⌋ = TK.η-exp-Ne∈ (⌊⌋-⌊⌋≡ _) k-kd a∈⌊k⌋

-- η-expansion of neutrals followed by hereditary substitution
-- vanish if the substitution hits the head of the neutral.

η-exp-ne-Hit-/⟨⟩ : ∀ {k m n Γ Δ} {x a as j} {σ : SVSub m n} →
                   Hit σ x a → Γ ⊢ j kds → Γ ⊢Ne var x ∙ as ∈ ⌊ j ⌋ →
                   Δ ⊢/⟨ k ⟩ σ ∈ Γ →
                   η-exp j (var x ∙ as) /⟨ k ⟩ σ  ≈  var x ∙ as /⟨ k ⟩ σ
η-exp-ne-Hit-/⟨⟩ hitP j-kds x∙as∈k σ∈Γ =
  TK.η-exp-ne-Hit-/⟨⟩ (⌊⌋-⌊⌋≡ _) hitP j-kds x∙as∈k σ∈Γ

η-exp-var-Hit-/⟨⟩ : ∀ {k m n Γ Δ} {x a j} {σ : SVSub m n} →
                    Hit σ x a → Γ ⊢ j kds → Γ ⊢Var x ∈ ⌊ j ⌋ →
                    Δ ⊢/⟨ k ⟩ σ ∈ Γ →
                    η-exp j (var∙ x) /⟨ k ⟩ σ  ≈  var∙ x /⟨ k ⟩ σ
η-exp-var-Hit-/⟨⟩ hitP j-kds x∈k σ∈Γ =
  η-exp-ne-Hit-/⟨⟩ hitP j-kds (∈-∙ x∈k ∈-[]) σ∈Γ

-- Hereditary substitutions of a variable by its η-expansion vanish.

kds-[]-η-var : ∀ {m n} (Γ₂ : CtxExt (suc m) n) {Γ₁ j k} →
               Γ₁ ⊢ j kds → Γ₂ ++ kd ⌊ j ⌋ ∷ Γ₁ ⊢ k kds →
               let j′ = weakenKind′ j
                   k′ = k Kind′/Var (VarSubst.wk VarSubst.↑) VarSubst.↑⋆ n
               in k′ Kind/⟨ ⌊ j′ ⌋ ⟩ sub (η-exp j′ (var∙ zero)) ↑⋆ n ≋ k
kds-[]-η-var Γ₂ {Γ₁} {j} j-kds k-kds =
  TK.kds-[]-η-var Γ₂ (⌊⌋-⌊⌋≡ _) (kds-weaken j-kds)
                  (subst (λ l → Γ₂ ++ kd l ∷ Γ₁ ⊢ _ kds)
                         (sym (⌊⌋-Kind′/Var j)) k-kds)

Nf∈-[]-η-var : ∀ {m n} (Γ₂ : CtxExt (suc m) n) {Γ₁ a j k} →
               Γ₁ ⊢ j kds → Γ₂ ++ kd ⌊ j ⌋ ∷ Γ₁ ⊢Nf a ∈ k →
               let j′ = weakenKind′ j
                   a′ = a Elim/Var (VarSubst.wk VarSubst.↑) VarSubst.↑⋆ n
               in a′ /⟨ ⌊ j′ ⌋ ⟩ sub (η-exp j′ (var∙ zero)) ↑⋆ n ≈ a
Nf∈-[]-η-var Γ₂ {Γ₁} {a} {j} j-kds a∈k =
  TK.Nf∈-[]-η-var Γ₂ (⌊⌋-⌊⌋≡ _) (kds-weaken j-kds)
                  (subst (λ l → Γ₂ ++ kd l ∷ Γ₁ ⊢Nf _ ∈ _)
                         (sym (⌊⌋-Kind′/Var j)) a∈k)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
------------------------------------------------------------------------
-- Some examples related to Nat.Wrapper, defined in Cubical Agda
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

open import Equality.Path as P
open import Prelude hiding (zero; suc; _+_)

open import Bijection equality-with-J using (_↔_)

module Nat.Wrapper.Cubical
  -- The underlying representation of natural numbers.
  (Nat′ : Type)
  -- A bijection between this representation and the unary natural
  -- numbers.
  (Nat′↔ℕ : Nat′ ↔ ℕ)
  where

open import Equality.Path.Univalence
open import Logical-equivalence using (_⇔_)

import Equivalence equality-with-J as Eq
open import Erased.Cubical equality-with-paths
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
import Nat equality-with-J as Nat
import Univalence-axiom equality-with-J as U

open import Nat.Wrapper equality-with-J Nat′ Nat′↔ℕ as NW
open NW.[]-cong instance-of-[]-cong-axiomatisation

private
  variable
    A   : Type
    m n : A

------------------------------------------------------------------------
-- Could Nat have been defined using the propositional truncation
-- instead of Erased?

-- Could Nat have been defined using ∥_∥ instead of Erased? Let us
-- try.

-- Given a truncated natural number we can kind of apply Nat-[_] to
-- it, because Nat-[_] is a family of contractible types. (The code
-- uses univalence.)

Nat-[]′ : ∥ ℕ ∥ → ∃ λ (A : Type) → Contractible A
Nat-[]′ = Trunc.rec
  (U.∃-H-level-H-level-1+ ext univ 0)
  (λ n → Nat-[ n ]
       , propositional⇒inhabited⇒contractible
           Nat-[]-propositional
           ( _↔_.from Nat′↔ℕ n
           , [ _↔_.right-inverse-of Nat′↔ℕ n ]
           ))

Nat-[_]′ : ∥ ℕ ∥ → Type
Nat-[ n ]′ = proj₁ (Nat-[]′ n)

-- Thus we can form a variant of Nat.

Nat-with-∥∥ : Type
Nat-with-∥∥ = Σ ∥ ℕ ∥ Nat-[_]′

-- However, this variant is isomorphic to the unit type.

Nat-with-∥∥↔⊤ : Nat-with-∥∥ ↔ ⊤
Nat-with-∥∥↔⊤ =
  _⇔_.to contractible⇔↔⊤ $
  Σ-closure 0
    (propositional⇒inhabited⇒contractible
       truncation-is-proposition ∣ 0 ∣)
    (proj₂ ∘ Nat-[]′)

-- And thus it is not isomorphic to the natural numbers.

¬-Nat-with-∥∥↔ℕ : ¬ (Nat-with-∥∥ ↔ ℕ)
¬-Nat-with-∥∥↔ℕ =
  Nat-with-∥∥ ↔ ℕ  ↝⟨ F._∘ inverse Nat-with-∥∥↔⊤ ⟩
  ⊤ ↔ ℕ            ↝⟨ (λ hyp → _↔_.injective (inverse hyp) refl) ⟩
  0 ≡ 1            ↝⟨ Nat.0≢+ ⟩□
  ⊥                □

------------------------------------------------------------------------
-- Addition of "wrapped" numbers is commutative and associative

module _ (o : Operations) where

  open Operations-for-Nat o
  open Operations-for-Nat-correct o

  private

    -- A lemma used several times below.

    from[to+to]≡+ :
      ∀ m →
      _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n) ≡ m + n
    from[to+to]≡+ {n = n} m =
      _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)  ≡⟨ cong (_↔_.from Nat↔ℕ) $ sym $ to-ℕ-+ m n ⟩
      _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ (m + n))                     ≡⟨ _↔_.left-inverse-of Nat↔ℕ _ ⟩∎
      m + n                                                     ∎

  -- First two "traditional" proofs.

  -- Addition is commutative.

  +-comm-traditional : ∀ m {n} → m + n ≡ n + m
  +-comm-traditional m {n = n} =
    m + n                                                     ≡⟨ sym $ from[to+to]≡+ m ⟩
    _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)  ≡⟨ cong (_↔_.from Nat↔ℕ) $ Nat.+-comm (_↔_.to Nat↔ℕ m) ⟩
    _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ m)  ≡⟨ from[to+to]≡+ n ⟩∎
    n + m                                                     ∎

  -- Addition is associative.

  +-assoc-traditional : ∀ m {n o} → m + (n + o) ≡ (m + n) + o
  +-assoc-traditional m {n = n} {o = o} =
    m + (n + o)                                                     ≡⟨ cong (m +_) $ sym $ from[to+to]≡+ n ⟩

    m + (_↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ o))  ≡⟨ sym $ from[to+to]≡+ m ⟩

    _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m
                      Prelude.+
                    _↔_.to Nat↔ℕ (_↔_.from Nat↔ℕ
                      (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ o)))   ≡⟨ cong (λ n → _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ n)) $
                                                                       _↔_.right-inverse-of Nat↔ℕ _ ⟩
    _↔_.from Nat↔ℕ
      (_↔_.to Nat↔ℕ m
         Prelude.+
       (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ o))                   ≡⟨ cong (_↔_.from Nat↔ℕ) $ Nat.+-assoc (_↔_.to Nat↔ℕ m) ⟩

    _↔_.from Nat↔ℕ
      ((_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)
         Prelude.+
       _↔_.to Nat↔ℕ o)                                              ≡⟨ cong (λ n → _↔_.from Nat↔ℕ (n Prelude.+ _↔_.to Nat↔ℕ o)) $ sym $
                                                                       _↔_.right-inverse-of Nat↔ℕ _ ⟩
    _↔_.from Nat↔ℕ
      (_↔_.to Nat↔ℕ (_↔_.from Nat↔ℕ
         (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n))
         Prelude.+
       _↔_.to Nat↔ℕ o)                                              ≡⟨ from[to+to]≡+ (_↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)) ⟩

    (_↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)) + o  ≡⟨ cong (_+ o) $ from[to+to]≡+ {n = n} m ⟩∎

    (m + n) + o                                                     ∎

  -- The following proofs are instead based on a technique used by
  -- Vezzosi, Mörtberg and Abel in "Cubical Agda: A Dependently Typed
  -- Programming Language with Univalence and Higher Inductive Types".

  -- The type of unary natural numbers is equal to the type of wrapped
  -- natural numbers.

  ℕ≡Nat : ℕ ≡ Nat
  ℕ≡Nat = sym (≃⇒≡ (Eq.↔⇒≃ Nat↔ℕ))

  -- Addition of unary natural numbers is, in a certain sense, equal
  -- to addition of wrapped natural numbers.

  +≡+ : P.[ (λ i → ℕ≡Nat i → ℕ≡Nat i → ℕ≡Nat i) ] Prelude._+_ ≡ _+_
  +≡+ =
    Prelude._+_                                                         ≡⟨ (λ i → transport
                                                                                (λ j → ℕ≡Nat (min i j) → ℕ≡Nat (min i j) → ℕ≡Nat (min i j))
                                                                                (- i) Prelude._+_) ⟩h
    transport (λ i → ℕ≡Nat i → ℕ≡Nat i → ℕ≡Nat i) 0̲ Prelude._+_         ≡⟨⟩
    (λ m n → _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n))  ≡⟨ (⟨ext⟩ λ m → ⟨ext⟩ λ _ → from[to+to]≡+ m) ⟩∎
    _+_                                                                 ∎

  -- Addition is commutative.

  +-comm-cubical : ∀ m {n} → m + n ≡ n + m
  +-comm-cubical =
    transport
      (λ i → (m {n} : ℕ≡Nat i) → +≡+ i m n ≡ +≡+ i n m)
      0̲
      Nat.+-comm

  -- Addition is associative.

  +-assoc-cubical : ∀ m {n o} → m + (n + o) ≡ (m + n) + o
  +-assoc-cubical =
    transport
      (λ i → (m {n o} : ℕ≡Nat i) →
             +≡+ i m (+≡+ i n o) ≡ +≡+ i (+≡+ i m n) o)
      0̲
      Nat.+-assoc

  -- This proof technique seems to scale better than the one used
  -- above, at least for examples of the kind used here.

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties about natural number operations
------------------------------------------------------------------------

module Data.Nat.Properties.Simple where

open import Data.Nat as Nat
open import Function
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
open import Data.Product
open import Data.Sum

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

+-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
+-assoc zero    _ _ = refl
+-assoc (suc m) n o = cong suc $ +-assoc m n o

+-right-identity : ∀ n → n + 0 ≡ n
+-right-identity zero = refl
+-right-identity (suc n) = cong suc $ +-right-identity n

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm zero    n = sym $ +-right-identity n
+-comm (suc m) n =
  begin
    suc m + n
  ≡⟨ refl ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨ sym (+-suc n m) ⟩
    n + suc m
  ∎

+-*-suc : ∀ m n → m * suc n ≡ m + m * n
+-*-suc zero    n = refl
+-*-suc (suc m) n =
  begin
    suc m * suc n
  ≡⟨ refl ⟩
    suc n + m * suc n
  ≡⟨ cong (λ x → suc n + x) (+-*-suc m n) ⟩
    suc n + (m + m * n)
  ≡⟨ refl ⟩
    suc (n + (m + m * n))
  ≡⟨ cong suc (sym $ +-assoc n m (m * n)) ⟩
    suc (n + m + m * n)
  ≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
    suc (m + n + m * n)
  ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
    suc (m + (n + m * n))
  ≡⟨ refl ⟩
    suc m + suc m * n
  ∎

*-right-zero : ∀ n → n * 0 ≡ 0
*-right-zero zero = refl
*-right-zero (suc n) = *-right-zero n

*-comm : ∀ m n → m * n ≡ n * m
*-comm zero    n = sym $ *-right-zero n
*-comm (suc m) n =
  begin
    suc m * n
  ≡⟨ refl ⟩
    n + m * n
  ≡⟨ cong (λ x → n + x) (*-comm m n) ⟩
    n + n * m
  ≡⟨ sym (+-*-suc n m) ⟩
    n * suc m
  ∎

distribʳ-*-+ : ∀ m n o → (n + o) * m ≡ n * m + o * m
distribʳ-*-+ m zero    o = refl
distribʳ-*-+ m (suc n) o =
  begin
    (suc n + o) * m
  ≡⟨ refl ⟩
    m + (n + o) * m
  ≡⟨ cong (_+_ m) $ distribʳ-*-+ m n o ⟩
    m + (n * m + o * m)
  ≡⟨ sym $ +-assoc m (n * m) (o * m) ⟩
    m + n * m + o * m
  ≡⟨ refl ⟩
    suc n * m + o * m
  ∎

*-assoc : ∀ m n o → (m * n) * o ≡ m * (n * o)
*-assoc zero    n o = refl
*-assoc (suc m) n o =
  begin
    (suc m * n) * o
  ≡⟨ refl ⟩
    (n + m * n) * o
  ≡⟨ distribʳ-*-+ o n (m * n) ⟩
    n * o + (m * n) * o
  ≡⟨ cong (λ x → n * o + x) $ *-assoc m n o ⟩
    n * o + m * (n * o)
  ≡⟨ refl ⟩
    suc m * (n * o)
  ∎


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

module Definition.Conversion.Lift where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Conversion.Soundness
open import Definition.Conversion.Reduction
open import Definition.Conversion.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Reduction
open import Definition.Typed.Consequences.Equality

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Lifting of algorithmic equality of types from WHNF to generic types.
liftConv : ∀ {A B rA Γ}
          → Γ ⊢ A [conv↓] B ^ rA
          → Γ ⊢ A [conv↑] B ^ rA
liftConv A<>B =
  let ⊢A , ⊢B = syntacticEq (soundnessConv↓ A<>B)
      whnfA , whnfB = whnfConv↓ A<>B
  in  [↑] _ _ (id ⊢A) (id ⊢B) whnfA whnfB A<>B

-- Lifting of algorithmic equality of terms from WHNF to generic terms.
liftConvTerm : ∀ {t u A Γ l}
             → Γ ⊢ t [conv↓] u ∷ A ^ l
             → Γ ⊢ t [conv↑] u ∷ A ^ l
liftConvTerm t<>u =
  let ⊢A , ⊢t , ⊢u = syntacticEqTerm (soundnessConv↓Term t<>u)
      whnfA , whnfT , whnfU = whnfConv↓Term t<>u
  in  [↑]ₜ _ _ _ (id ⊢A) (id ⊢t) (id ⊢u) whnfA whnfT whnfU t<>u

mutual
  -- Helper function for lifting from neutrals to generic terms in WHNF.
  lift~toConv↓!′ : ∀ {t u A A′ Γ l lA }
                → Γ ⊩⟨ l ⟩ A′ ^ [ ! , lA ]
                → Γ ⊢ A′ ⇒* A ^ [ ! , lA ]
                → Γ ⊢ t ~ u ↓! A ^ lA
                → Γ ⊢ t [conv↓] u ∷ A ^ lA
  lift~toConv↓!′ (Uᵣ′ _ l r l' l< PE.refl d) D ([~] A D₁ whnfB k~l)
                rewrite U≡A-whnf (trans (sym (subset* (red d))) (subset* D)) whnfB =
    ne ([~] A D₁ Uₙ k~l)
  lift~toConv↓!′ (ℕᵣ D) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , ℕₙ) (D₁ , whnfB)) =
    ℕ-ins ([~] A D₂ ℕₙ k~l)
  lift~toConv↓!′ (ne′ K D neK K≡K) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , ne neK) (D₁ , whnfB)) =
    let _ , ⊢t , ⊢u = syntacticEqTerm (soundness~↑! k~l)
        A≡K = subset* D₂
    in  ne-ins (conv ⊢t A≡K) (conv ⊢u A≡K) neK ([~] A D₂ (ne neK) k~l)
  lift~toConv↓!′ (Πᵣ′ rF lF lG l< l<' F G D ⊢F ⊢G A≡A [F] [G] G-ext) D₁ ([~] A D₂ whnfB k~l) with PE.sym (whrDet* (red D , Πₙ) (D₁ , whnfB))
  lift~toConv↓!′ (Πᵣ′ ! lF lG l< l<' F G D ⊢F ⊢G A≡A [F] [G] G-ext) D₁ ([~] A D₂ whnfB k~l) | PE.refl =
    let ⊢ΠFG , ⊢t , ⊢u = syntacticEqTerm (soundness~↓! ([~] A D₂ Πₙ k~l))
        neT , neU = ne~↑! k~l
        ⊢Γ = wf ⊢F
        var0 = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here)
                       (genRefl (var (⊢Γ ∙ ⊢F) here))
        0≡0 = lift~toConv↑′ ([F] (step id) (⊢Γ ∙ ⊢F)) (var-refl′ (var (⊢Γ ∙ ⊢F) here))
        k∘0≡l∘0 = lift~toConv↑′ ([G] (step id) (⊢Γ ∙ ⊢F) var0)
                                (~↑! (app-cong (wk~↓! (step id) (⊢Γ ∙ ⊢F) ([~] A D₂ Πₙ k~l)) 0≡0))
    in  η-eq l< l<' ⊢F ⊢t ⊢u (ne neT) (ne neU)
             (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x ^ _)
                       (wkSingleSubstId _)
                       k∘0≡l∘0)
  lift~toConv↓!′ (Πᵣ′ % lF lG l< l<' F G D ⊢F ⊢G A≡A [F] [G] G-ext) D₁ ([~] A D₂ whnfB k~l) | PE.refl =
    let ⊢ΠFG , ⊢t , ⊢u = syntacticEqTerm (soundness~↓! ([~] A D₂ Πₙ k~l))
        neT , neU = ne~↑! k~l
        ⊢Γ = wf ⊢F
        var0 = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here)
                       (genRefl (var (⊢Γ ∙ ⊢F) here))
        k∘0≡l∘0 = lift~toConv↑′ ([G] (step id) (⊢Γ ∙ ⊢F) var0)
                                 (~↑! (app-cong (wk~↓! (step id) (⊢Γ ∙ ⊢F) ([~] A D₂ Πₙ k~l)) (%~↑ (var (⊢Γ ∙ ⊢F) here) (var (⊢Γ ∙ ⊢F) here))))
    in  η-eq l< l<' ⊢F ⊢t ⊢u (ne neT) (ne neU)
             (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x ^ _)
                       (wkSingleSubstId _)
                       k∘0≡l∘0)
  lift~toConv↓!′ (emb emb< [A]) D t~u = lift~toConv↓!′ [A] D t~u
  lift~toConv↓!′ (emb ∞< [A]) D t~u = lift~toConv↓!′ [A] D t~u

  -- Helper function for lifting from neutrals to generic terms.
  lift~toConv↑!′ : ∀ {t u A Γ l lA}
                → Γ ⊩⟨ l ⟩ A ^ [ ! , lA ]
                → Γ ⊢ t ~ u ↑! A ^ lA
                → Γ ⊢ t [conv↑] u ∷ A ^ lA
  lift~toConv↑!′ [A] t~u =
    let B , whnfB , D = whNorm′ [A]
        t~u↓ = [~] _ (red D) whnfB t~u
        neT , neU = ne~↑! t~u
        _ , ⊢t , ⊢u = syntacticEqTerm (soundness~↓! t~u↓)
    in  [↑]ₜ _ _ _ (red D) (id ⊢t) (id ⊢u) whnfB
             (ne neT) (ne neU) (lift~toConv↓!′ [A] (red D) t~u↓)

  lift~toConv↑′ : ∀ {t u A  Γ l lA}
                → Γ ⊩⟨ l ⟩ A ^ [ ! , lA ]
                → Γ ⊢ t ~ u ↑ A ^ [ ! , lA ]
                → Γ ⊢ t [conv↑] u ∷ A ^ lA
  lift~toConv↑′ [A] (~↑! x) = lift~toConv↑!′ [A] x

-- Lifting of algorithmic equality of terms from neutrals to generic terms in WHNF.
lift~toConv↓! : ∀ {t u A Γ lA}
             → Γ ⊢ t ~ u ↓! A ^ lA
             → Γ ⊢ t [conv↓] u ∷ A ^ lA
lift~toConv↓! ([~] A D whnfB k~l) =
  lift~toConv↓!′ (reducible (proj₁ (syntacticRed D))) D ([~] A D whnfB k~l)

lift~toConv↓ : ∀ {t u A Γ lA}
             → Γ ⊢ t ~ u ↓! A ^ lA
             → Γ ⊢ t [conv↓] u ∷ A ^ lA
lift~toConv↓ x = lift~toConv↓! x

-- Lifting of algorithmic equality of terms from neutrals to generic terms.
lift~toConv↑! : ∀ {t u A Γ lA}
             → Γ ⊢ t ~ u ↑! A ^ lA
             → Γ ⊢ t [conv↑] u ∷ A ^ lA
lift~toConv↑! t~u =
  lift~toConv↑!′ (reducible (proj₁ (syntacticEqTerm (soundness~↑! t~u)))) t~u

lift~toConv↑ : ∀ {t u A Γ lA}
             → Γ ⊢ t ~ u ↑ A ^ [ ! , lA ]
             → Γ ⊢ t [conv↑] u ∷ A ^ lA
lift~toConv↑ (~↑! t~u) = lift~toConv↑! t~u

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module Data.Fin.Extra where

open import Data.Nat
    renaming (suc to S; zero to Z; _+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Fin

open import Function
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality

inject-1 : ∀ {n} → (i : Fin (S n)) → toℕ i ≢ n → Fin n
inject-1 {Z}   zero    p = contradiction refl p
inject-1 {Z}   (suc i) p = i
inject-1 {S n} zero    p = zero
inject-1 {S n} (suc i) p = suc (inject-1 i (p ∘ cong S))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Extensions.List where

open import Prelude

open import Data.List
open import Data.Fin using (fromℕ≤; zero; suc)
open import Data.List.All hiding (lookup; map)
open import Data.Maybe hiding (All; map)
open import Relation.Nullary
open import Relation.Nullary.Decidable using (map′)
open import Relation.Binary.Core using (REL; Reflexive; Transitive)
open import Relation.Binary.List.Pointwise hiding (refl; map)

data _[_]=_ {a} {A : Set a} : List A → ℕ → A → Set where
  here : ∀ {x xs} → (x ∷ xs) [ 0 ]= x
  there : ∀ {x y xs n} → xs [ n ]= x → (y ∷ xs) [ suc n ]= x

[]=-functional : ∀ {a} {A : Set a} → (l : List A) → (i : ℕ) →
                   ∀ {x y : A} → l [ i ]= x → l [ i ]= y → x ≡ y
[]=-functional .(_ ∷ _) .0 here here = refl
[]=-functional .(_ ∷ _) .(suc _) (there p) (there q) = []=-functional _ _ p q

[]=-map : ∀ {a b}{A : Set a}{B : Set b}{l : List A}{i x}{f : A → B} →
            l [ i ]= x → (map f l) [ i ]= (f x)
[]=-map here = here
[]=-map (there p) = there ([]=-map p)

maybe-lookup : ∀ {a}{A : Set a} → ℕ → List A → Maybe A
maybe-lookup n [] = nothing
maybe-lookup zero (x ∷ μ) = just x
maybe-lookup (suc n) (x ∷ μ) = maybe-lookup n μ

maybe-lookup-safe : ∀ {a}{A : Set a}{l : List A} {i x} → l [ i ]= x → maybe-lookup i l ≡ just x
maybe-lookup-safe here = refl
maybe-lookup-safe (there p) = maybe-lookup-safe p

lookup : ∀ {a} {A : Set a} → (l : List A) → Fin (length l) → A
lookup [] ()
lookup (x ∷ l) zero = x
lookup (x ∷ l) (suc p) = lookup l p

dec-lookup : ∀ {a} {A : Set a} → (i : ℕ) → (l : List A) → Dec (∃ λ x → l [ i ]= x)
dec-lookup _ [] = no (λ{ (_ , ())})
dec-lookup zero (x ∷ l) = yes (x , here)
dec-lookup (suc i) (_ ∷ l) = map′
  (λ{ (x , p) → x , there p})
  (λ{ (x , there p) → x , p})
  (dec-lookup i l)

all-lookup : ∀ {a} {A : Set a} {l : List A} {i x p P} → l [ i ]= x → All {p = p} P l → P x
all-lookup here (px ∷ l) = px
all-lookup (there i) (px ∷ l) = all-lookup i l

infixl 10 _[_]≔_
_[_]≔_ : ∀ {a} {A : Set a} → (l : List A) → Fin (length l) → A → List A
[] [ () ]≔ x
(x ∷ xs) [ zero ]≔ x' = x' ∷ xs
(x ∷ xs) [ suc i ]≔ y = xs [ i ]≔ y

module _ where
  open import Data.List.Any
  open Membership-≡

  _[_]≔'_ : ∀ {a} {A : Set a}{x} → (l : List A) → x ∈ l → A → List A
  [] [ () ]≔' y
  (x ∷ l) [ here px ]≔' y = y ∷ l
  (x ∷ l) [ there px ]≔' y = x ∷ (l [ px ]≔' y)

  ≔'-[]= :  ∀ {a} {A : Set a}{x}{l : List A} (p : x ∈ l) → ∀ {y} → y ∈ (l [ p ]≔' y)
  ≔'-[]= (here px) = here refl
  ≔'-[]= (there p) = there (≔'-[]= p)

-- proof matters; update a particular witness of a property
_All[_]≔_ : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} {i x} →
            All P xs → xs [ i ]= x → P x → All P xs
[] All[ () ]≔ px
(px ∷ xs) All[ here ]≔ px' = px' ∷ xs
(px ∷ xs) All[ there i ]≔ px' = px ∷ (xs All[ i ]≔ px')

-- prefix predicate for lists
infix 4 _⊑_
data _⊑_ {a} {A : Set a} : List A → List A → Set where
  [] : ∀ {ys} → [] ⊑ ys
  _∷_ : ∀ x {xs ys} → xs ⊑ ys → x ∷ xs ⊑ x ∷ ys

⊑-refl : ∀ {a} {A : Set a} → Reflexive (_⊑_ {A = A})
⊑-refl {x = []} = []
⊑-refl {x = x ∷ xs} = x ∷ ⊑-refl

⊑-trans : ∀ {a} {A : Set a} → Transitive (_⊑_ {A = A})
⊑-trans [] _ = []
⊑-trans (x ∷ p) (.x ∷ q) = x ∷ ⊑-trans p q

-- list extensions; reverse prefix relation
infix 4 _⊒_
_⊒_ : ∀ {a} {A : Set a} → List A → List A → Set
xs ⊒ ys = ys ⊑ xs

-- appending to a list gives a list extension;
-- or, appending to a list makes the original a prefix
∷ʳ-⊒ : ∀ {a} {A : Set a} (x : A) xs → xs ∷ʳ x ⊒ xs
∷ʳ-⊒ x [] = []
∷ʳ-⊒ x (x₁ ∷ Σ₁) = x₁ ∷ (∷ʳ-⊒ x Σ₁)

-- indexes into a prefix point to the same element in extensions
xs⊒ys[i] : ∀ {a} {A : Set a} {xs : List A} {ys : List A} {i y} →
           xs [ i ]= y → (p : ys ⊒ xs) → ys [ i ]= y
xs⊒ys[i] here (x ∷ q) = here
xs⊒ys[i] (there p) (x ∷ q) = there (xs⊒ys[i] p q)

-- prefix is preserved by map
⊑-map : ∀ {a b} {A : Set a} {B : Set b} {xs ys : List A} {f : A → B} →
        xs ⊑ ys → map f xs ⊑ map f ys
⊑-map [] = []
⊑-map {f = f} (x ∷ p) = f x ∷ (⊑-map p)

module Pointwise where
  pointwise-length : ∀ {a b ℓ A B P l m} → Rel {a} {b} {ℓ} {A} {B} P l m → length l ≡ length m
  pointwise-length [] = refl
  pointwise-length (x∼y ∷ p) = cong suc (pointwise-length p)

  []=-length : ∀ {a} {A : Set a} {L : List A} {i x} → L [ i ]= x → i < length L
  []=-length here = s≤s z≤n
  []=-length (there p) = s≤s ([]=-length p)

  ∷ʳ[length] : ∀ {a} {A : Set a} (l : List A) x → (l ∷ʳ x) [ length l ]= x
  ∷ʳ[length] [] y = here
  ∷ʳ[length] (x ∷ Σ) y = there (∷ʳ[length] Σ y)

  all-∷ʳ : ∀ {a p} {A : Set a} {l : List A} {x} {P : A → Set p} → All P l → P x → All P (l ∷ʳ x)
  all-∷ʳ [] q = q ∷ []
  all-∷ʳ (px ∷ p) q = px ∷ (all-∷ʳ p q)

  pointwise-∷ʳ : ∀ {a b ℓ A B P l m x y} → Rel {a} {b} {ℓ} {A} {B} P l m → P x y →
                Rel {a} {b} {ℓ} {A} {B} P (l ∷ʳ x) (m ∷ʳ y)
  pointwise-∷ʳ [] q = q ∷ []
  pointwise-∷ʳ (x∼y ∷ p) q = x∼y ∷ (pointwise-∷ʳ p q)

  pointwise-lookup : ∀ {a b ℓ A B P l m i x} → Rel {a} {b} {ℓ} {A} {B} P l m →
                     l [ i ]= x → ∃ λ y → P x y
  pointwise-lookup (x∼y ∷ r) here = , x∼y
  pointwise-lookup (x∼y ∷ r) (there p) = pointwise-lookup r p

  pointwise-maybe-lookup : ∀ {a b ℓ A B P l m i x} → Rel {a} {b} {ℓ} {A} {B} P l m →
                     l [ i ]= x → ∃ λ y → maybe-lookup i m ≡ just y × P x y
  pointwise-maybe-lookup [] ()
  pointwise-maybe-lookup (x∼y ∷ r) here = , refl , x∼y
  pointwise-maybe-lookup (x∼y ∷ r) (there p) = pointwise-maybe-lookup r p

  postulate
    pointwise-[]≔ : ∀ {a b ℓ A B P l m i x y} →
                    Rel {a} {b} {ℓ} {A} {B} P l m → (p : l [ i ]= x) → (q : i < length m) → P x y →
                    Rel {a} {b} {ℓ} {A} {B} P l (m [ fromℕ≤ q ]≔ y)
  {-}
  pointwise-[]≔ [] () r
  pointwise-[]≔ (x∼y ∷ r) here (s≤s z≤n) z = z ∷ r
  pointwise-[]≔ (x∼y ∷ r) (there p) (s≤s q) z = subst (λ x → Rel _ _ x) {!!} (x∼y ∷ pointwise-[]≔ r p q z)
  -}

open Pointwise public


text:
-- Andreas 2016-01-06

-- {-# OPTIONS -v error.checkclause:60 #-}

data D : Set where
  c : D

test : (x y z : D) → Set
test _ c _ with D
test x y z | _ = D

-- Expected output: clause should be printed as is in error message,
-- including underscore patterns.