text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.ZariskiLattice.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Powerset using (⊆-refl-consequence)

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                      ; ·-identityʳ to ·ℕ-rid)
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Poset

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.RadicalIdeal
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.Algebra.CommRing.Localisation.InvertingElements
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommAlgebra.Properties
open import Cubical.Algebra.CommAlgebra.Localisation
open import Cubical.Algebra.RingSolver.ReflectionSolving
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.BigOps
open import Cubical.Algebra.Matrix

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open Iso
open BinaryRelation
open isEquivRel

private
  variable
    ℓ ℓ' : Level

module ZarLat (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open Exponentiation R'
 open BinomialThm R'
 open CommIdeal R'
 open RadicalIdeal R'
 open isCommIdeal
 open ProdFin R'

 private
  R = fst R'
  A = Σ[ n ∈ ℕ ] (FinVec R n)
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]

 _∼_ : A → A → Type (ℓ-suc ℓ)
 (_ , α) ∼ (_ , β) = √ ⟨ α ⟩ ≡ √ ⟨ β ⟩

 ∼EquivRel : isEquivRel (_∼_)
 reflexive ∼EquivRel _ = refl
 symmetric ∼EquivRel _ _ = sym
 transitive ∼EquivRel _ _ _ = _∙_

 ZL : Type (ℓ-suc ℓ)
 ZL = A / _∼_

 0z : ZL
 0z = [ 0 , (λ ()) ]

 1z : ZL
 1z = [ 1 , (replicateFinVec 1 1r) ]

 _∨z_ : ZL → ZL → ZL
 _∨z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
                          (λ (_ , α) (_ , β) → (_ , α ++Fin β))
   (λ (_ , α) (_ , β) → cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α)))
    λ (_ , α) (_ , β) (_ , γ) α∼β → --need to show α∨γ ∼ β∨γ
      √ ⟨ α ++Fin γ ⟩      ≡⟨ cong √ (FGIdealAddLemma _ α γ) ⟩
      √ (⟨ α ⟩ +i ⟨ γ ⟩)    ≡⟨ sym (√+LContr _ _) ⟩
      √ (√ ⟨ α ⟩ +i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I +i ⟨ γ ⟩)) α∼β ⟩
      √ (√ ⟨ β ⟩ +i ⟨ γ ⟩) ≡⟨ √+LContr _ _ ⟩
      √ (⟨ β ⟩ +i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealAddLemma _ β γ)) ⟩
      √ ⟨ β ++Fin γ ⟩ ∎

 _∧z_ : ZL → ZL → ZL
 _∧z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
                          (λ (_ , α) (_ , β) → (_ , α ··Fin β))
   (λ (_ , α) (_ , β) → cong √ (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α)))
    λ (_ , α) (_ , β) (_ , γ) α∼β → --need to show α∧γ ∼ β∧γ
      √ ⟨ α ··Fin γ ⟩       ≡⟨ cong √ (FGIdealMultLemma _ α γ) ⟩
      √ (⟨ α ⟩ ·i ⟨ γ ⟩)    ≡⟨ sym (√·LContr _ _) ⟩
      √ (√ ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I ·i ⟨ γ ⟩)) α∼β ⟩
      √ (√ ⟨ β ⟩ ·i ⟨ γ ⟩) ≡⟨ √·LContr _ _ ⟩
      √ (⟨ β ⟩ ·i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealMultLemma _ β γ)) ⟩
      √ ⟨ β ··Fin γ ⟩ ∎

 -- join axioms
 ∨zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∨z (𝔟 ∨z 𝔠) ≡ (𝔞 ∨z 𝔟) ∨z 𝔠
 ∨zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
          λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (cong √ (IdealAddAssoc _ _ _ _))

 ∨zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∨z 𝔟 ≡ 𝔟 ∨z 𝔞
 ∨zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
        λ (_ , α) (_ , β) → eq/ _ _
          (cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α)))

 ∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
 ∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → eq/ _ _ refl

 ∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
 ∨zRid _ = ∨zComm _ _ ∙ ∨zLid _

 -- -- meet axioms
 ∧zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∧z 𝔠) ≡ (𝔞 ∧z 𝔟) ∧z 𝔠
 ∧zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
    λ (_ , α) (_ , β) (_ , γ) → eq/ _ _
      (√ ⟨ α ··Fin (β ··Fin γ) ⟩     ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
       √ (⟨ α ⟩ ·i ⟨ β ··Fin γ ⟩)    ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealMultLemma _ _ _) ⟩
       √ (⟨ α ⟩ ·i (⟨ β ⟩ ·i ⟨ γ ⟩)) ≡⟨ cong √ (·iAssoc _ _ _) ⟩
       √ ((⟨ α ⟩ ·i ⟨ β ⟩) ·i ⟨ γ ⟩) ≡⟨ cong (λ x → √ (x ·i ⟨ γ ⟩)) (sym (FGIdealMultLemma _ _ _)) ⟩
       √ (⟨ α ··Fin β ⟩ ·i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealMultLemma _ _ _)) ⟩
       √ ⟨ (α ··Fin β) ··Fin γ ⟩     ∎)

 ∧zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z 𝔟 ≡ 𝔟 ∧z 𝔞
 ∧zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
        λ (_ , α) (_ , β) → eq/ _ _
          (cong √ (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α)))

 ∧zRid : ∀ (𝔞 : ZL) → 𝔞 ∧z 1z ≡ 𝔞
 ∧zRid = SQ.elimProp (λ _ → squash/ _ _)
   λ (_ , α) → eq/ _ _ (cong √
     (⟨ α ··Fin (replicateFinVec 1 1r) ⟩ ≡⟨ FGIdealMultLemma _ _ _ ⟩
      ⟨ α ⟩ ·i ⟨ (replicateFinVec 1 1r) ⟩ ≡⟨ cong (⟨ α ⟩ ·i_) (contains1Is1 _ (indInIdeal _ _ zero)) ⟩
      ⟨ α ⟩ ·i 1Ideal                     ≡⟨ ·iRid _ ⟩
      ⟨ α ⟩ ∎))

 -- absorption and distributivity
 ∧zAbsorb∨z : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z (𝔞 ∨z 𝔟) ≡ 𝔞
 ∧zAbsorb∨z = SQ.elimProp2 (λ _ _ → squash/ _ _)
            λ (_ , α) (_ , β) → eq/ _ _
              (√ ⟨ α ··Fin (α ++Fin β) ⟩     ≡⟨ cong √ (FGIdealMultLemma _ α (α ++Fin β)) ⟩
               √ (⟨ α ⟩ ·i ⟨ α ++Fin β ⟩)    ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ α β) ⟩
               √ (⟨ α ⟩ ·i (⟨ α ⟩ +i ⟨ β ⟩)) ≡⟨ √·Absorb+ _ _ ⟩
               √ ⟨ α ⟩ ∎)

 ∧zLDist∨z : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∨z 𝔠) ≡ (𝔞 ∧z 𝔟) ∨z (𝔞 ∧z 𝔠)
 ∧zLDist∨z = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
   λ (_ , α) (_ , β) (_ , γ) → eq/ _ _
     (√ ⟨ α ··Fin (β ++Fin γ) ⟩            ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
      √ (⟨ α ⟩ ·i ⟨ β ++Fin γ ⟩)           ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ _ _) ⟩
      √ (⟨ α ⟩ ·i (⟨ β ⟩ +i ⟨ γ ⟩))        ≡⟨ cong √ (·iRdist+i _ _ _) ⟩
      -- L/R-dist are swapped
      -- in Lattices vs Rings
      √ (⟨ α ⟩ ·i ⟨ β ⟩ +i ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong₂ (λ x y → √ (x +i y))
                                                     (sym (FGIdealMultLemma _ _ _))
                                                     (sym (FGIdealMultLemma _ _ _)) ⟩
      √ (⟨ α ··Fin β ⟩ +i ⟨ α ··Fin γ ⟩)   ≡⟨ cong √ (sym (FGIdealAddLemma _ _ _)) ⟩
      √ ⟨ (α ··Fin β) ++Fin (α ··Fin γ) ⟩  ∎)

 ZariskiLattice : DistLattice (ℓ-suc ℓ)
 fst ZariskiLattice = ZL
 DistLatticeStr.0l (snd ZariskiLattice) = 0z
 DistLatticeStr.1l (snd ZariskiLattice) = 1z
 DistLatticeStr._∨l_ (snd ZariskiLattice) = _∨z_
 DistLatticeStr._∧l_ (snd ZariskiLattice) = _∧z_
 DistLatticeStr.isDistLattice (snd ZariskiLattice) =
   makeIsDistLattice∧lOver∨l squash/ ∨zAssoc ∨zRid ∨zComm
                                       ∧zAssoc ∧zRid ∧zComm ∧zAbsorb∨z ∧zLDist∨z

module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where

 open CommRingStr (R' .snd)
 open RingTheory (CommRing→Ring R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open Exponentiation R'

 open DistLatticeStr (L' .snd) renaming (is-set to isSetL)
 open Join L'
 open LatticeTheory (DistLattice→Lattice L')
 open Order (DistLattice→Lattice L')
 open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L'))
 open PosetReasoning IndPoset
 open PosetStr (IndPoset .snd) hiding (_≤_)
 private
  R = fst R'
  L = fst L'

 record IsZarMap (d : R → L) : Type (ℓ-max ℓ ℓ') where
  constructor iszarmap

  field
   pres0 : d 0r ≡ 0l
   pres1 : d 1r ≡ 1l
   ·≡∧ : ∀ x y → d (x · y) ≡ d x ∧l d y
   +≤∨ : ∀ x y → d (x + y) ≤ d x ∨l d y

  ∑≤⋁ : {n : ℕ} (U : FinVec R n) → d (∑ U) ≤ ⋁ λ i → d (U i)
  ∑≤⋁ {n = zero} U = ∨lRid _ ∙ pres0
  ∑≤⋁ {n = suc n} U = d (∑ U)                        ≤⟨ ∨lIdem _ ⟩
                       d (U zero  + ∑ (U ∘ suc))     ≤⟨ +≤∨ _ _ ⟩
                       d (U zero) ∨l d (∑ (U ∘ suc)) ≤⟨ ≤-∨LPres _ _ _ (∑≤⋁ (U ∘ suc)) ⟩
                       d (U zero) ∨l ⋁ (d ∘ U ∘ suc) ≤⟨ ∨lIdem _ ⟩
                       ⋁ (d ∘ U) ◾

  d·LCancel : ∀ x y → d (x · y) ≤ d y
  d·LCancel x y = subst (λ a → a ≤ d y) (sym (·≡∧ x y)) (∧≤LCancelJoin _ _)

  linearCombination≤LCancel : {n : ℕ} (α β : FinVec R n)
                            → d (linearCombination R' α β) ≤ ⋁ (d ∘ β)
  linearCombination≤LCancel α β = is-trans _ _ _ (∑≤⋁ (λ i → α i · β i))
                                                 (≤-⋁Ext _ _ λ i → d·LCancel (α i) (β i))

  ZarMapIdem : ∀ (n : ℕ) (x : R) → d (x ^ (suc n)) ≡ d x
  ZarMapIdem zero x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) pres1 ∙∙ ∧lRid _
  ZarMapIdem (suc n) x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) (ZarMapIdem n x) ∙∙ ∧lIdem _

  ZarMapExpIneq : ∀ (n : ℕ) (x : R) → d x ≤ d (x ^ n)
  ZarMapExpIneq zero x = cong (d x ∨l_) pres1 ∙∙ 1lRightAnnihilates∨l _ ∙∙ sym pres1
  ZarMapExpIneq (suc n) x = subst (λ y → d x ≤ y) (sym (ZarMapIdem _ x)) (∨lIdem _)

  -- the crucial lemma about "Zariski maps"
  open CommIdeal R'
  open RadicalIdeal R'
  open isCommIdeal
  private
   ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
   ⟨ V ⟩ = ⟨ V ⟩[ R' ]

  ZarMapRadicalIneq : ∀ {n : ℕ} (α : FinVec R n) (x : R)
                    → x ∈ √ ⟨ α ⟩ → d x ≤ ⋁ (d ∘ α)
  ZarMapRadicalIneq α x = PT.elim (λ _ → isSetL _ _)
         (uncurry (λ n → (PT.elim (λ _ → isSetL _ _) (uncurry (curriedHelper n)))))
   where
   curriedHelper : (n : ℕ) (β : FinVec R _)
                 → x ^ n ≡ linearCombination R' β α → d x ≤ ⋁ (d ∘ α)
   curriedHelper n β xⁿ≡∑βα = d x ≤⟨ ZarMapExpIneq n x ⟩
                              d (x ^ n)
     ≤⟨ subst (λ y → y ≤ ⋁ (d ∘ α)) (sym (cong d xⁿ≡∑βα)) (linearCombination≤LCancel β α) ⟩
                              ⋁ (d ∘ α) ◾

module ZarLatUniversalProp (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open Exponentiation R'
 open BinomialThm R'
 open CommIdeal R'
 open RadicalIdeal R'
 open isCommIdeal
 open ProdFin R'

 open ZarLat R'
 open IsZarMap

 private
  R = fst R'
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]

 D : R → ZL
 D x = [ 1 , replicateFinVec 1 x ] -- λ x → √⟨x⟩

 isZarMapD : IsZarMap R' ZariskiLattice D
 pres0 isZarMapD = eq/ _ _ (cong √ (0FGIdeal _ ∙ sym (emptyFGIdeal _ _)))
 pres1 isZarMapD = refl
 ·≡∧ isZarMapD x y = cong {B = λ _ → ZL} (λ U → [ 1 , U ]) (Length1··Fin x y)
 +≤∨ isZarMapD x y = eq/ _ _ (cong √ (CommIdeal≡Char (inclOfFGIdeal _ 3Vec ⟨ 2Vec ⟩ 3Vec⊆2Vec)
                                                       (inclOfFGIdeal _ 2Vec ⟨ 3Vec ⟩ 2Vec⊆3Vec)))
  where
  2Vec = replicateFinVec 1 x ++Fin replicateFinVec 1 y
  3Vec = replicateFinVec 1 (x + y) ++Fin (replicateFinVec 1 x ++Fin replicateFinVec 1 y)

  3Vec⊆2Vec : ∀ (i : Fin 3) → 3Vec i ∈ ⟨ 2Vec ⟩
  3Vec⊆2Vec zero = ⟨ 2Vec ⟩ .snd .+Closed (indInIdeal _ _ zero) (indInIdeal _ _ (suc zero))
  3Vec⊆2Vec (suc zero) = indInIdeal _ _ zero
  3Vec⊆2Vec (suc (suc zero)) = indInIdeal _ _ (suc zero)

  2Vec⊆3Vec : ∀ (i : Fin 2) → 2Vec i ∈ ⟨ 3Vec ⟩
  2Vec⊆3Vec zero = indInIdeal _ _ (suc zero)
  2Vec⊆3Vec (suc zero) = indInIdeal _ _ (suc (suc zero))

 -- defintion of the universal property
 hasZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L)
                        → IsZarMap R' L D
                        → Type _
 hasZarLatUniversalProp {ℓ' = ℓ'} L D _ = ∀ (L' : DistLattice ℓ') (d : R → fst L')
                                       → IsZarMap R' L' d
                                       → ∃![ χ ∈ DistLatticeHom L L' ] (fst χ) ∘ D ≡ d

 isPropZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L) (isZarMapD : IsZarMap R' L D)
                         → isProp (hasZarLatUniversalProp L D isZarMapD)
 isPropZarLatUniversalProp L D isZarMapD = isPropΠ3 (λ _ _ _ → isPropIsContr)

 ZLHasUniversalProp : hasZarLatUniversalProp ZariskiLattice D isZarMapD
 ZLHasUniversalProp L' d isZarMapd = (χ , funExt χcomp) , χunique
  where
  open DistLatticeStr (snd L') renaming (is-set to isSetL)
  open LatticeTheory (DistLattice→Lattice L')
  open Join L'
  open IsLatticeHom
  L = fst L'

  χ : DistLatticeHom ZariskiLattice L'
  fst χ = SQ.rec isSetL (λ (_ , α) → ⋁ (d ∘ α))
                         λ (_ , α) (_ , β) → curriedHelper α β
   where
   curriedHelper : {n m : ℕ} (α : FinVec R n) (β : FinVec R m)
                 → √ ⟨ α ⟩ ≡ √ ⟨ β ⟩ → ⋁ (d ∘ α) ≡ ⋁ (d ∘ β)
   curriedHelper α β √⟨α⟩≡√⟨β⟩ = is-antisym _ _ ineq1 ineq2
    where
    open Order (DistLattice→Lattice L')
    open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L'))
    open PosetReasoning IndPoset
    open PosetStr (IndPoset .snd) hiding (_≤_)

    incl1 : √ ⟨ α ⟩ ⊆ √ ⟨ β ⟩
    incl1 = ⊆-refl-consequence _ _ (cong fst √⟨α⟩≡√⟨β⟩) .fst

    ineq1 : ⋁ (d ∘ α) ≤ ⋁ (d ∘ β)
    ineq1 = ⋁IsMax (d ∘ α) (⋁ (d ∘ β))
            λ i → ZarMapRadicalIneq isZarMapd β (α i) (√FGIdealCharLImpl α ⟨ β ⟩ incl1 i)

    incl2 : √ ⟨ β ⟩ ⊆ √ ⟨ α ⟩
    incl2 = ⊆-refl-consequence _ _ (cong fst √⟨α⟩≡√⟨β⟩) .snd

    ineq2 : ⋁ (d ∘ β) ≤ ⋁ (d ∘ α)
    ineq2 = ⋁IsMax (d ∘ β) (⋁ (d ∘ α))
            λ i → ZarMapRadicalIneq isZarMapd α (β i) (√FGIdealCharLImpl β ⟨ α ⟩ incl2 i)

  pres0 (snd χ) = refl
  pres1 (snd χ) = ∨lRid _ ∙ isZarMapd .pres1
  pres∨l (snd χ) = elimProp2 (λ _ _ → isSetL _ _) (uncurry (λ n α → uncurry (curriedHelper n α)))
   where
   curriedHelper : (n : ℕ) (α : FinVec R n) (m : ℕ) (β : FinVec R m)
                 → ⋁ (d ∘ (α ++Fin β)) ≡ ⋁ (d ∘ α) ∨l ⋁ (d ∘ β)
   curriedHelper zero α _ β = sym (∨lLid _)
   curriedHelper (suc n) α _ β =
                   ⋁ (d ∘ (α ++Fin β)) ≡⟨ refl ⟩
                   d (α zero) ∨l ⋁ (d ∘ ((α ∘ suc) ++Fin β))

                  ≡⟨ cong (d (α zero) ∨l_) (curriedHelper _ (α ∘ suc) _ β) ⟩

                   d (α zero) ∨l (⋁ (d ∘ α ∘ suc) ∨l ⋁ (d ∘ β))
                  ≡⟨ ∨lAssoc _ _ _ ⟩

                   ⋁ (d ∘ α) ∨l ⋁ (d ∘ β) ∎

  pres∧l (snd χ) = elimProp2 (λ _ _ → isSetL _ _) (uncurry (λ n α → uncurry (curriedHelper n α)))
   where
   -- have to repeat this one here so the termination checker won't complain
   oldHelper : (n : ℕ) (α : FinVec R n) (m : ℕ) (β : FinVec R m)
             → ⋁ (d ∘ (α ++Fin β)) ≡ ⋁ (d ∘ α) ∨l ⋁ (d ∘ β)
   oldHelper zero α _ β = sym (∨lLid _)
   oldHelper (suc n) α _ β = cong (d (α zero) ∨l_) (oldHelper _ (α ∘ suc) _ β) ∙ ∨lAssoc _ _ _

   curriedHelper : (n : ℕ) (α : FinVec R n) (m : ℕ) (β : FinVec R m)
                 → ⋁ (d ∘ (α ··Fin β)) ≡ ⋁ (d ∘ α) ∧l ⋁ (d ∘ β)
   curriedHelper zero α _ β = sym (0lLeftAnnihilates∧l _)
   curriedHelper (suc n) α _ β =
      ⋁ (d ∘ (α ··Fin β)) ≡⟨ refl ⟩
      ⋁ (d ∘ ((λ j → α zero · β j) ++Fin ((α ∘ suc) ··Fin β)))

     ≡⟨ oldHelper _ (λ j → α zero · β j) _ ((α ∘ suc) ··Fin β) ⟩

      ⋁ (d ∘ (λ j → α zero · β j)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))

     ≡⟨ cong (_∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))) (⋁Ext (λ j → isZarMapd .·≡∧ (α zero) (β j))) ⟩

      ⋁ (λ j → d (α zero) ∧l d (β j)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))

     ≡⟨ cong (_∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))) (sym (⋁Meetrdist _ _)) ⟩

      (d (α zero) ∧l ⋁ (d ∘ β)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))

     ≡⟨ cong ((d (α zero) ∧l ⋁ (d ∘ β)) ∨l_) (curriedHelper _ (α ∘ suc) _ β) ⟩

      (d (α zero) ∧l ⋁ (d ∘ β)) ∨l (⋁ (d ∘ α ∘ suc) ∧l ⋁ (d ∘ β))

     ≡⟨ sym (∧lRdist∨l _ _ _) ⟩

      ⋁ (d ∘ α) ∧l ⋁ (d ∘ β) ∎

  χcomp : ∀ (f : R) → χ .fst (D f) ≡ d f
  χcomp f = ∨lRid (d f)

  χunique : (y : Σ[ χ' ∈ DistLatticeHom ZariskiLattice L' ] fst χ' ∘ D ≡ d)
          → (χ , funExt χcomp) ≡ y
  χunique (χ' , χ'∘D≡d) = Σ≡Prop (λ _ → isSetΠ (λ _ → isSetL) _ _) (LatticeHom≡f _ _
                                 (funExt (elimProp (λ _ → isSetL _ _) (uncurry uniqHelper))))
   where
   uniqHelper : (n : ℕ) (α : FinVec R n) → fst χ [ n , α ] ≡ fst χ' [ n , α ]
   uniqHelper zero _ = sym (cong (λ α → fst χ' [ 0 , α ]) (funExt (λ ())) ∙ χ' .snd .pres0)
   uniqHelper (suc n) α =
       ⋁ (d ∘ α) ≡⟨ refl ⟩
       d (α zero) ∨l ⋁ (d ∘ α ∘ suc)

      ≡⟨ cong (d (α zero) ∨l_) (uniqHelper n (α ∘ suc)) ⟩ -- the inductive step

       d (α zero) ∨l fst χ' [ n , α ∘ suc ]

      ≡⟨ cong (_∨l fst χ' [ n , α ∘ suc ]) (sym (funExt⁻ χ'∘D≡d (α zero))) ⟩

       fst χ' (D (α zero)) ∨l fst χ' [ n , α ∘ suc ]

      ≡⟨ sym (χ' .snd .pres∨l _ _) ⟩

       fst χ' (D (α zero) ∨z [ n , α ∘ suc ])

      ≡⟨ cong (λ β → fst χ' [ suc n , β ]) (funExt (λ { zero → refl ; (suc i) → refl })) ⟩

       fst χ' [ suc n , α ] ∎

-- An equivalent definition that doesn't bump up the unviverse level
module SmallZarLat (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open CommIdeal R'
 open RadicalIdeal R'
 open ZarLat R'

 open Iso

 private
  R = fst R'
  A = Σ[ n ∈ ℕ ] (FinVec R n)
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]
  -- This is small!
  _≼_ : A → A → Type ℓ
  (_ , α) ≼ (_ , β) = ∀ i → α i ∈ √ ⟨ β ⟩

 _∼'_ :  A → A → Type ℓ
 α ∼' β = (α ≼ β) × (β ≼ α)

 -- lives in the same universe as R
 ZL' : Type ℓ
 ZL' = A / (_∼'_)

 IsoLarLatSmall : Iso ZL ZL'
 IsoLarLatSmall = relBiimpl→TruncIso ~→∼' ~'→∼
  where
  ~→∼' : ∀ {a b : A} → a ∼ b → a ∼' b
  ~→∼' r = √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) r h)
         , √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) (sym r) h)

  ~'→∼ : ∀ {a b : A} → a ∼' b → a ∼ b
  ~'→∼ r = CommIdeal≡Char (√FGIdealCharRImpl _ ⟨ _ ⟩ (fst r))
                          (√FGIdealCharRImpl _ ⟨ _ ⟩ (snd r))

 ZL≃ZL' : ZL ≃ ZL'
 ZL≃ZL' = isoToEquiv IsoLarLatSmall

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
------------------------------------------------------------------------
-- The semantics in Lambda.Closure.Relational and
-- Lambda.Closure.Functional are equivalent
------------------------------------------------------------------------

module Lambda.Closure.Equivalence where

open import Axiom.ExcludedMiddle
open import Category.Monad.Partiality as Partiality
  using (_⊥; never; steps; module Steps)
open import Codata.Musical.Notation
open import Data.Empty using (⊥-elim)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Data.Nat.Induction
import Data.Nat.Properties as ℕ
import Data.Nat.Solver as ℕ
open import Data.Product
open import Data.Sum
open import Data.Vec using (Vec; []; _∷_)
open import Function
import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Negation

open ℕ.+-*-Solver using (solve; _:=_; _:+_; con)
open Partiality._⊥
private
  open module PE {A : Set} = Partiality.Equality (_≡_ {A = A})
  open module PR {A : Set} =
    Partiality.Reasoning (P.isEquivalence {A = A})
    hiding (_≡⟨_⟩_) renaming (_∎ to _□)

open import Lambda.Syntax
open Closure Tm
open import Lambda.Closure.Relational as R
open import Lambda.Closure.Functional as F hiding (module Workaround)
open PF

------------------------------------------------------------------------
-- Successful, terminating computations

-- The functional semantics is complete with respect to the relational
-- one.

complete⇓ : ∀ {n} {t : Tm n} {ρ v} →
            ρ ⊢ t ⇓ v → ⟦ t ⟧ ρ ≈ return v
complete⇓ var = _ □
complete⇓ con = _ □
complete⇓ ƛ   = _ □
complete⇓ {ρ = ρ} {v} (app {t₁} {t₂} {t = t} {ρ′} {v′ = v′} t₁⇓ t₂⇓ t₁t₂⇓) =
  ⟦ t₁ · t₂ ⟧ ρ                  ≅⟨ ·-comp t₁ t₂ ⟩
  ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ          ≈⟨ complete⇓ t₁⇓ ⟦·⟧-cong complete⇓ t₂⇓ ⟩
  return (ƛ t ρ′) ⟦·⟧ return v′  ≳⟨ laterˡ (_ □) ⟩
  ⟦ t ⟧ (v′ ∷ ρ′)                ≈⟨ complete⇓ t₁t₂⇓ ⟩
  return v                       □

-- The functional semantics is sound with respect to the relational
-- one.

sound⇓ : ∀ {n} (t : Tm n) {ρ : Env n} {v} →
         ⟦ t ⟧ ρ ≈ return v → ρ ⊢ t ⇓ v
sound⇓ t t⇓ = <′-rec P sound⇓′ (steps t⇓) t t⇓ P.refl
  where
  P : ℕ → Set
  P s = ∀ {n} (t : Tm n) {ρ : Env n} {v}
          (t⇓ : ⟦ t ⟧ ρ ≈ return v) → steps t⇓ ≡ s → ρ ⊢ t ⇓ v

  sound⇓′ : ∀ s → <′-Rec P s → P s
  sound⇓′ s rec (con i)           (now P.refl) _  = con
  sound⇓′ s rec (var x)           (now P.refl) _  = var
  sound⇓′ s rec (ƛ t)             (now P.refl) _  = ƛ
  sound⇓′ s rec (t₁ · t₂) {ρ} {v} t₁t₂⇓        eq
    with >>=-inversion-⇓ (⟦ t₁ ⟧ ρ) (
           ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ  ≅⟨ sym $ ·-comp t₁ t₂ ⟩
           ⟦ t₁ · t₂ ⟧ ρ          ≈⟨ t₁t₂⇓ ⟩
           return v               □)
  sound⇓′ s rec (t₁ · t₂) {ρ}     t₁t₂⇓ eq | (v₁    , t₁⇓ , t₂∙⇓ , eq₁) with >>=-inversion-⇓ (⟦ t₂ ⟧ ρ) t₂∙⇓
  sound⇓′ s rec (t₁ · t₂)         t₁t₂⇓ eq | (con i , t₁⇓ , t₂∙⇓ , eq₁) | (v₂ , t₂⇓ , now ()    , _  )
  sound⇓′ s rec (t₁ · t₂) {ρ} {v} t₁t₂⇓ eq | (ƛ t _ , t₁⇓ , t₂∙⇓ , eq₁) | (v₂ , t₂⇓ , laterˡ ∙⇓ , eq₂) =
    app (rec (steps t₁⇓) ₁< t₁ t₁⇓ P.refl)
        (rec (steps t₂⇓) ₂< t₂ t₂⇓ P.refl)
        (rec (steps  ∙⇓) ∙< t   ∙⇓ P.refl)
    where
    open ℕ.≤-Reasoning

    ₁₂∙< = begin
      1 + steps t₁⇓ + (steps t₂⇓ + steps ∙⇓)                 ≡⟨ solve 3 (λ x y z → con 1 :+ x :+ (y :+ z) :=
                                                                                x :+ (y :+ (con 1 :+ z)))
                                                                        P.refl (steps t₁⇓) (steps t₂⇓) _ ⟩
      steps t₁⇓ + (steps t₂⇓ + (1 + steps ∙⇓))               ≡⟨ P.cong (_+_ (steps t₁⇓)) eq₂ ⟩
      steps t₁⇓ + steps t₂∙⇓                                 ≡⟨ eq₁ ⟩
      steps (⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ  ≅⟨ sym $ ·-comp t₁ t₂ ⟩
             ⟦ t₁ · t₂ ⟧ ρ          ≈⟨ t₁t₂⇓ ⟩
             return v               □)                       ≡⟨ Steps.left-identity (sym $ ·-comp t₁ t₂) _ ⟩
      steps (⟦ t₁ · t₂ ⟧ ρ          ≈⟨ t₁t₂⇓ ⟩
             return v               □)                       ≡⟨ Steps.right-identity t₁t₂⇓ (return v □) ⟩
      steps t₁t₂⇓                                            ≡⟨ eq ⟩
      s                                                      ∎

    ₁< = ℕ.≤⇒≤′ (begin
      1 + steps t₁⇓                           ≤⟨ ℕ.m≤m+n (1 + steps t₁⇓) _ ⟩
      1 + steps t₁⇓ + (steps t₂⇓ + steps ∙⇓)  ≤⟨ ₁₂∙< ⟩
      s                                       ∎)

    ₂∙< = begin
      1 + steps t₂⇓ + steps ∙⇓                ≤⟨ s≤s (ℕ.m≤n+m _ (steps t₁⇓)) ⟩
      1 + steps t₁⇓ + (steps t₂⇓ + steps ∙⇓)  ≤⟨ ₁₂∙< ⟩
      s                                       ∎

    ₂< = ℕ.≤⇒≤′ (begin
      1 + steps t₂⇓             ≤⟨ ℕ.m≤m+n (1 + steps t₂⇓) _ ⟩
      1 + steps t₂⇓ + steps ∙⇓  ≤⟨ ₂∙< ⟩
      s                         ∎)

    ∙< = ℕ.≤⇒≤′ (begin
      1 + steps ∙⇓              ≤⟨ s≤s (ℕ.m≤n+m _ (steps t₂⇓)) ⟩
      1 + steps t₂⇓ + steps ∙⇓  ≤⟨ ₂∙< ⟩
      s                         ∎)

------------------------------------------------------------------------
-- Non-terminating computations

-- The functional semantics is complete for non-terminating computations.

module Complete⇑ where

  infix  4 _≈P_ _≈W_
  infixr 2 _≅⟪_⟫_ _≳⟪_⟫_ _≈⟪_⟫_

  data _≈P_ : Maybe Value ⊥ → Maybe Value ⊥ → Set₁ where
    ⌈_⌉ : ∀ {x y} (x≳y : x ≳ y) → x ≈P y

    later : ∀ {x y} (x≈y : ∞ (♭ x ≈P ♭ y)) → later x ≈P later y

    _>>=P_ : ∀ {x₁ x₂ f₁ f₂} →
             (x₁≈x₂ : x₁ ≈P x₂) (f₁≈f₂ : ∀ x → f₁ x ≈P f₂ x) →
             (x₁ >>= f₁) ≈P (x₂ >>= f₂)
    _⟦·⟧P_ : ∀ {v₁₁ v₁₂ v₂₁ v₂₂} →
             (v₁₁≈v₂₁ : v₁₁ ≈P v₂₁) (v₁₂≈v₂₂ : v₁₂ ≈P v₂₂) →
             v₁₁ ⟦·⟧ v₁₂ ≈P v₂₁ ⟦·⟧ v₂₂

    _≅⟪_⟫_ : ∀ x {y z} (x≅y : x ≅  y) (y≈z : y ≈P z) → x ≈P z
    _≳⟪_⟫_ : ∀ x {y z} (x≳y : x ≳  y) (y≈z : y ≈P z) → x ≈P z
    _≈⟪_⟫_ : ∀ x {y z} (x≈y : x ≈P y) (y≅z : y ≅  z) → x ≈P z

  private

    data _≈W_ : Maybe Value ⊥ → Maybe Value ⊥ → Set₁ where
      now    : ∀ {v}                      → now   v ≈W now   v
      later  : ∀ {x y} (x≈y : ♭ x ≈P ♭ y) → later x ≈W later y
      laterˡ : ∀ {x y} (x≈y : ♭ x ≈W   y) → later x ≈W       y

    ⌈_⌉W : ∀ {x y} → x ≳ y → x ≈W y
    ⌈ now P.refl ⌉W = now
    ⌈ later  x≳y ⌉W = later ⌈ ♭ x≳y ⌉
    ⌈ laterˡ x≳y ⌉W = laterˡ ⌈ x≳y ⌉W

    program : ∀ {x y} → x ≈W y → x ≈P y
    program now          = ⌈ now P.refl ⌉
    program (later  x≈y) = later (♯ x≈y)
    program (laterˡ x≈y) = _ ≳⟪ laterˡ (_ □) ⟫ program x≈y

    _>>=W_ : ∀ {x₁ x₂ f₁ f₂} →
             x₁ ≈W x₂ → (∀ x → f₁ x ≈W f₂ x) →
             (x₁ >>= f₁) ≈W (x₂ >>= f₂)
    now {v = nothing} >>=W f₁≈f₂ = now
    now {v = just v } >>=W f₁≈f₂ = f₁≈f₂ v
    later  x≈y        >>=W f₁≈f₂ = later (x≈y >>=P (program ∘ f₁≈f₂))
    laterˡ x≈y        >>=W f₁≈f₂ = laterˡ (x≈y >>=W f₁≈f₂)

    _⟦·⟧W_ : ∀ {v₁₁ v₁₂ v₂₁ v₂₂} →
             v₁₁ ≈W v₂₁ → v₁₂ ≈W v₂₂ → v₁₁ ⟦·⟧ v₁₂ ≈W v₂₁ ⟦·⟧ v₂₂
    v₁₁≈v₂₁ ⟦·⟧W v₁₂≈v₂₂ =
      v₁₁≈v₂₁ >>=W λ v₁ →
      v₁₂≈v₂₂ >>=W λ v₂ →
      ⌈ ⟪ v₁ ∙ v₂ ⟫P □ ⌉W
      where open F.Workaround

    trans≅≈W : ∀ {x y z} → x ≅ y → y ≈W z → x ≈W z
    trans≅≈W (now P.refl) now           = now
    trans≅≈W (later  x≅y) (later  y≈z)  = later (_ ≅⟪ ♭ x≅y ⟫ y≈z)
    trans≅≈W (later  x≅y) (laterˡ y≈z)  = laterˡ (trans≅≈W (♭ x≅y) y≈z)

    trans≳≈W : ∀ {x y z} → x ≳ y → y ≈W z → x ≈W z
    trans≳≈W (now P.refl) now           = now
    trans≳≈W (later  x≳y) (later  y≈z)  = later (_ ≳⟪ ♭ x≳y ⟫ y≈z)
    trans≳≈W (later  x≳y) (laterˡ y≈z)  = laterˡ (trans≳≈W (♭ x≳y) y≈z)
    trans≳≈W (laterˡ x≳y)         y≈z   = laterˡ (trans≳≈W x≳y y≈z)

    trans≈W≅ : ∀ {x y z} → x ≈W y → y ≅ z → x ≈W z
    trans≈W≅ now          (now P.refl) = now
    trans≈W≅ (later  x≈y) (later y≅z)  = later (_ ≈⟪ x≈y ⟫ ♭ y≅z)
    trans≈W≅ (laterˡ x≈y)        y≅z   = laterˡ (trans≈W≅ x≈y y≅z)

    whnf : ∀ {x y} → x ≈P y → x ≈W y
    whnf ⌈ x≳y ⌉                = ⌈ x≳y ⌉W
    whnf (later x≈y)            = later (♭ x≈y)
    whnf (x₁≈x₂ >>=P f₁≈f₂)     = whnf x₁≈x₂ >>=W λ v → whnf (f₁≈f₂ v)
    whnf (v₁₁≈v₂₁ ⟦·⟧P v₁₂≈v₂₂) = whnf v₁₁≈v₂₁ ⟦·⟧W whnf v₁₂≈v₂₂
    whnf (x ≅⟪ x≅y ⟫ y≈z)       = trans≅≈W x≅y (whnf y≈z)
    whnf (x ≳⟪ x≳y ⟫ y≈z)       = trans≳≈W x≳y (whnf y≈z)
    whnf (x ≈⟪ x≈y ⟫ y≅z)       = trans≈W≅ (whnf x≈y) y≅z

  mutual

    -- Note that the types of soundW and soundP could be strengthened:
    -- laterʳ is not used.

    private

      soundW : ∀ {x y} → x ≈W y → x ≈ y
      soundW now          = now P.refl
      soundW (later  x≈y) = later (♯ soundP x≈y)
      soundW (laterˡ x≈y) = laterˡ (soundW x≈y)

    soundP : ∀ {x y} → x ≈P y → x ≈ y
    soundP x≈y = soundW (whnf x≈y)

  -- The language _≈P_ does not include transitivity for weak
  -- equality, as this would be unsound. Instead some limited notions
  -- of transitivity are used:
  --
  -- • Weak equality can be combined with strong equality on both
  --   sides.
  --
  -- • The _≳_ order can be "prepended" to a weak equality. Note that
  --   results of the form "x ≈ return v" can be turned into
  --   "x ≳ return v", as in the first case below.

  complete⇑ : ∀ {n} {t : Tm n} {ρ : Env n} →
              ρ ⊢ t ⇑ → ⟦ t ⟧ ρ ≈P never
  complete⇑ {ρ = ρ} (app {t₁} {t₂} {t = t} {ρ′} {v} t₁⇓ t₂⇓ t₁t₂⇑) =
    ⟦ t₁ · t₂ ⟧ ρ                 ≅⟪ ·-comp t₁ t₂ ⟫
    ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ         ≳⟪ Partiality.now⇒now (complete⇓ t₁⇓) ⟦·⟧-cong
                                     Partiality.now⇒now (complete⇓ t₂⇓) ⟫
    return (ƛ t ρ′) ⟦·⟧ return v  ≅⟪ later (♯ (_ □)) ⟫
    later (♯ ⟦ t ⟧ (v ∷ ρ′))      ≈⟪ later (♯ complete⇑ (♭ t₁t₂⇑)) ⟫
    never                         □
  complete⇑ {ρ = ρ} (·ˡ {t₁} {t₂} t₁⇑) =
    ⟦ t₁ · t₂ ⟧ ρ          ≅⟪ ·-comp t₁ t₂ ⟫
    ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ  ≈⟪ complete⇑ (♭ t₁⇑) ⟦·⟧P ⌈ ⟦ t₂ ⟧ ρ □ ⌉ ⟫
    never ⟦·⟧ ⟦ t₂ ⟧ ρ     ≅⟨ Partiality.left-zero _ ⟩
    never                  □
  complete⇑ {ρ = ρ} (·ʳ {t₁} {t₂} {v} t₁⇓ t₂⇑) =
    ⟦ t₁ · t₂ ⟧ ρ          ≅⟪ ·-comp t₁ t₂ ⟫
    ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ  ≈⟪ ⌈ Partiality.now⇒now (complete⇓ t₁⇓) ⌉ ⟦·⟧P complete⇑ (♭ t₂⇑) ⟫
    return v ⟦·⟧ never     ≅⟨ Partiality.left-zero _ ⟩
    never                  □

complete⇑ : ∀ {n} {t : Tm n} {ρ : Env n} →
            ρ ⊢ t ⇑ → ⟦ t ⟧ ρ ≈ never
complete⇑ = Complete⇑.soundP ∘ Complete⇑.complete⇑

-- The functional semantics is sound for non-terminating computations.
-- I assume excluded middle here because double-negation elimination
-- is used "infinitely often".

sound⇑ : ExcludedMiddle Level.zero →
         ∀ {n} (t : Tm n) {ρ : Env n} →
         ⟦ t ⟧ ρ ≈ never → ρ ⊢ t ⇑
sound⇑ em (con i)       i⇑    = ⊥-elim (Partiality.now≉never i⇑)
sound⇑ em (var x)       x⇑    = ⊥-elim (Partiality.now≉never x⇑)
sound⇑ em (ƛ t)         ƛ⇑    = ⊥-elim (Partiality.now≉never ƛ⇑)
sound⇑ em (t₁ · t₂) {ρ} t₁t₂⇑
  with decidable-stable em $ >>=-inversion-⇑ (⟦ t₁ ⟧ ρ) (
         ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ  ≅⟨ sym $ ·-comp t₁ t₂ ⟩
         ⟦ t₁ · t₂ ⟧ ρ          ≈⟨ t₁t₂⇑ ⟩
         never                  □)
sound⇑ em (t₁ · t₂)     ⇑ | inj₁ t₁⇑               = ·ˡ (♯ sound⇑ em t₁ t₁⇑)
sound⇑ em (t₁ · t₂) {ρ} ⇑ | inj₂ (v₁ , t₁⇓ , t₂∙⇑)
  with decidable-stable em $ >>=-inversion-⇑ (⟦ t₂ ⟧ ρ) t₂∙⇑
sound⇑ em (t₁ · t₂) ⇑ | inj₂ (v₁    , t₁⇓ , t₂∙⇑) | inj₁ t₂⇑             = ·ʳ (sound⇓ t₁ t₁⇓) (♯ sound⇑ em t₂ t₂⇑)
sound⇑ em (t₁ · t₂) ⇑ | inj₂ (con i , t₁⇓ , t₂∙⇑) | inj₂ (v₂ , t₂⇓ , ∙⇑) = ⊥-elim (Partiality.now≉never ∙⇑)
sound⇑ em (t₁ · t₂) ⇑ | inj₂ (ƛ t _ , t₁⇓ , t₂∙⇑) | inj₂ (v₂ , t₂⇓ , ∙⇑) =
  app (sound⇓ t₁ t₁⇓) (sound⇓ t₂ t₂⇓) (♯ sound⇑ em t (Partiality.later⁻¹ ∙⇑))

------------------------------------------------------------------------
-- Crashing computations

-- The functional semantics is complete for crashing computations.

complete↯ : ExcludedMiddle Level.zero →
            ∀ {n} (t : Tm n) (ρ : Env n) →
            ρ ⊢ t ↯ → ⟦ t ⟧ ρ ≈ fail
complete↯ em t ρ ¬⇒
  with decidable-stable em $
         Partiality.now-or-never {_∼_ = _≡_} P.refl
                                 {k = Partiality.weak} (⟦ t ⟧ ρ)
... | inj₂ t⇑             = ⊥-elim (proj₂ ¬⇒ (sound⇑ em t t⇑))
... | inj₁ (nothing , t↯) = t↯
... | inj₁ (just v  , t⇓) = ⊥-elim (proj₁ ¬⇒ (-, sound⇓ t t⇓))

-- The functional semantics is sound for crashing computations.

sound↯ : ∀ {n} {t : Tm n} {ρ : Env n} →
         ⟦ t ⟧ ρ ≈ fail → ρ ⊢ t ↯
sound↯ {t = t} {ρ} t↯ = (¬⇓ , ¬⇑)
  where
  ¬⇓ : ¬ (∃ λ v → ρ ⊢ t ⇓ v)
  ¬⇓ (v , t⇓) with
    fail      ≈⟨ sym t↯ ⟩
    ⟦ t ⟧ ρ   ≈⟨ complete⇓ t⇓ ⟩
    return v  □
  ... | now ()

  ¬⇑ : ¬ (ρ ⊢ t ⇑)
  ¬⇑ t⇑ = Partiality.now≉never (
    fail     ≈⟨ sym t↯ ⟩
    ⟦ t ⟧ ρ  ≈⟨ complete⇑ t⇑ ⟩
    never    □)

ext: agda

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module sn-calculus-compatconf.eview where

open import sn-calculus-compatconf.base
open import sn-calculus-compatconf.in-lift  using (1-steplρ-E-view-ecin-lift)
open import sn-calculus-compatconf.split    using (1-steplρ-E-view-ecsplit)
open import sn-calculus-compatconf.same     using (1-steplρ-E-view-ecsame)

open import sn-calculus
open import utility renaming (_U̬_ to _∪_)
open import context-properties
  using (get-view ; ->E-view ; ->pot-view)

open import sn-calculus-confluence
  using (R-confluent)

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

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

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

open ->E-view
open ->pot-view

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

open ListSet Data.Nat._≟_

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

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

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

  ∃ λ { (θo , Ao , po) →
    (ρ⟨ θq , Aq ⟩· q        sn⟶* ρ⟨ θo , Ao ⟩· po) ×
    (ρ⟨ θ , A ⟩· C ⟦ ro ⟧c sn⟶* ρ⟨ θo , Ao ⟩· po) }

1-steplρ-E-view (CBρ cb) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ rinsn⟶₁ro
  with get-context-prefix p≐E⟦qin⟧ p≐C⟦rin⟧
1-steplρ-E-view (CBρ cb) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ rinsn⟶₁ro | ecsame =
  map proj₁ (map (sn⟶*-inclusion ∘ sn⟶-inclusion) (sn⟶*-inclusion ∘ sn⟶-inclusion ∘ proj₁))
    (1-steplρ-E-view-ecsame cb p≐E⟦qin⟧ q≐E⟦qo⟧ e-view
      p≐C⟦rin⟧ (plugc refl) rinsn⟶₁ro)
1-steplρ-E-view (CBρ cb) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ rinsn⟶₁ro | ecin-lift =
  ⊥-elim
   (1-steplρ-E-view-ecin-lift cb p≐E⟦qin⟧ q≐E⟦qo⟧ e-view
     p≐C⟦rin⟧ (plugc refl) rinsn⟶₁ro)
1-steplρ-E-view (CBρ cb) p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ rinsn⟶₁ro | ecsplit div
  with 1-steplρ-E-view-ecsplit cb div p≐E⟦qin⟧ q≐E⟦qo⟧ e-view
                                            p≐C⟦rin⟧ (plugc refl) rinsn⟶₁ro
... | po , inj₁ refl  , _ , _ , _ , ρθ·rsn⟶₁ρθq·po , e-view' =
  _ , rrefl ,′ sn⟶*-inclusion (sn⟶-inclusion ρθ·rsn⟶₁ρθq·po)
... | po , inj₂ qsn⟶po , _ , _ , _ , ρθ·rsn⟶₁ρθq·po , e-view' =
   _ , sn⟶*-inclusion (Context1-sn⟶ (cenv _ _) qsn⟶po) ,′ sn⟶*-inclusion (sn⟶-inclusion ρθ·rsn⟶₁ρθq·po)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Union of two binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Union where

open import Data.Product
open import Data.Sum
open import Function using (_∘_)
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Nullary using (yes; no)

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

_∪_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
      REL A B ℓ₁ → REL A B ℓ₂ → REL A B (ℓ₁ ⊔ ℓ₂)
L ∪ R = λ i j → L i j ⊎ R i j

------------------------------------------------------------------------
-- Properties

module _ {a ℓ} {A : Set a} (L : Rel A ℓ) (R : Rel A ℓ) where

  reflexive : Reflexive L ⊎ Reflexive R → Reflexive (L ∪ R)
  reflexive (inj₁ L-refl) = inj₁ L-refl
  reflexive (inj₂ R-refl) = inj₂ R-refl

  total : Total L ⊎ Total R → Total (L ∪ R)
  total (inj₁ L-total) x y = [ inj₁ ∘ inj₁ , inj₂ ∘ inj₁ ] (L-total x y)
  total (inj₂ R-total) x y = [ inj₁ ∘ inj₂ , inj₂ ∘ inj₂ ] (R-total x y)

  min : ∀ {⊤} → Minimum L ⊤ ⊎ Minimum R ⊤ → Minimum (L ∪ R) ⊤
  min = [ inj₁ ∘_ , inj₂ ∘_ ]

  max : ∀ {⊥} → Maximum L ⊥ ⊎ Maximum R ⊥ → Maximum (L ∪ R) ⊥
  max = [ inj₁ ∘_ , inj₂ ∘_ ]

module _ {a ℓ} {A : Set a} {L : Rel A ℓ} {R : Rel A ℓ} where

  symmetric : Symmetric L → Symmetric R → Symmetric (L ∪ R)
  symmetric L-sym R-sym = [ inj₁ ∘ L-sym , inj₂ ∘ R-sym ]

  respects : ∀ {p} {P : A → Set p} →
             P Respects L → P Respects R → P Respects (L ∪ R)
  respects resp-L resp-R = [ resp-L , resp-R ]

module _ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b}
         (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where

  implies : (≈ ⇒ L) ⊎ (≈ ⇒ R) → ≈ ⇒ (L ∪ R)
  implies = [ inj₁ ∘_ , inj₂ ∘_ ]

  irreflexive : Irreflexive ≈ L → Irreflexive ≈ R → Irreflexive ≈ (L ∪ R)
  irreflexive L-irrefl R-irrefl x≈y = [ L-irrefl x≈y , R-irrefl x≈y ]

module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} {L : REL A B ℓ₁} {R : REL A B ℓ₂} where

  decidable : Decidable L → Decidable R → Decidable (L ∪ R)
  decidable L? R? x y with L? x y | R? x y
  ... | yes Lxy | _       = yes (inj₁ Lxy)
  ... | no  _   | yes Rxy = yes (inj₂ Rxy)
  ... | no ¬Lxy | no ¬Rxy = no [ ¬Lxy , ¬Rxy ]


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core algebraic definitions
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Algebra`.

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

module Algebra.Core where

open import Level using (_⊔_)

------------------------------------------------------------------------
-- Unary and binary operations

Op₁ : ∀ {ℓ} → Set ℓ → Set ℓ
Op₁ A = A → A

Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
Op₂ A = A → A → A

------------------------------------------------------------------------
-- Left and right actions

Opₗ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
Opₗ A B = A → B → B

Opᵣ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
Opᵣ A B = B → A → B


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to AllPairs
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.AllPairs.Properties where

open import Data.List hiding (any)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as All
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
open import Data.Bool.Base using (true; false)
open import Data.Fin.Base using (Fin)
open import Data.Fin.Properties using (suc-injective)
open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-refl; ≤-step)
open import Function using (_∘_; flip)
open import Relation.Binary using (Rel; DecSetoid)
open import Relation.Binary.PropositionalEquality using (_≢_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (does)

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {a b ℓ} {A : Set a} {B : Set b} {R : Rel A ℓ} {f : B → A} where

  map⁺ : ∀ {xs} → AllPairs (λ x y → R (f x) (f y)) xs →
         AllPairs R (map f xs)
  map⁺ []           = []
  map⁺ (x∉xs ∷ xs!) = All.map⁺ x∉xs ∷ map⁺ xs!

------------------------------------------------------------------------
-- ++

module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where

  ++⁺ : ∀ {xs ys} → AllPairs R xs → AllPairs R ys →
        All (λ x → All (R x) ys) xs → AllPairs R (xs ++ ys)
  ++⁺ []         Rys _              = Rys
  ++⁺ (px ∷ Rxs) Rys (Rxys ∷ Rxsys) = All.++⁺ px Rxys ∷ ++⁺ Rxs Rys Rxsys

------------------------------------------------------------------------
-- concat

module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where

  concat⁺ : ∀ {xss} → All (AllPairs R) xss →
            AllPairs (λ xs ys → All (λ x → All (R x) ys) xs) xss →
            AllPairs R (concat xss)
  concat⁺ []           []              = []
  concat⁺ (pxs ∷ pxss) (Rxsxss ∷ Rxss) = ++⁺ pxs (concat⁺ pxss Rxss)
    (All.map All.concat⁺ (All.All-swap Rxsxss))

------------------------------------------------------------------------
-- take and drop

module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where

  take⁺ : ∀ {xs} n → AllPairs R xs → AllPairs R (take n xs)
  take⁺ zero    pxs        = []
  take⁺ (suc n) []         = []
  take⁺ (suc n) (px ∷ pxs) = All.take⁺ n px ∷ take⁺ n pxs

  drop⁺ : ∀ {xs} n → AllPairs R xs → AllPairs R (drop n xs)
  drop⁺ zero    pxs       = pxs
  drop⁺ (suc n) []        = []
  drop⁺ (suc n) (_ ∷ pxs) = drop⁺ n pxs

------------------------------------------------------------------------
-- applyUpTo

module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where

  applyUpTo⁺₁ : ∀ f n → (∀ {i j} → i < j → j < n → R (f i) (f j)) → AllPairs R (applyUpTo f n)
  applyUpTo⁺₁ f zero    Rf = []
  applyUpTo⁺₁ f (suc n) Rf =
    All.applyUpTo⁺₁ _ n (Rf (s≤s z≤n) ∘ s≤s) ∷
    applyUpTo⁺₁ _ n (λ i≤j j<n → Rf (s≤s i≤j) (s≤s j<n))

  applyUpTo⁺₂ : ∀ f n → (∀ i j → R (f i) (f j)) → AllPairs R (applyUpTo f n)
  applyUpTo⁺₂ f n Rf = applyUpTo⁺₁ f n (λ _ _ → Rf _ _)

------------------------------------------------------------------------
-- applyDownFrom

module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where

  applyDownFrom⁺₁ : ∀ f n → (∀ {i j} → j < i → i < n → R (f i) (f j)) →
                    AllPairs R (applyDownFrom f n)
  applyDownFrom⁺₁ f zero    Rf = []
  applyDownFrom⁺₁ f (suc n) Rf =
    All.applyDownFrom⁺₁ _ n (flip Rf ≤-refl)  ∷
    applyDownFrom⁺₁ f n (λ j<i i<n → Rf j<i (≤-step i<n))

  applyDownFrom⁺₂ : ∀ f n → (∀ i j → R (f i) (f j)) → AllPairs R (applyDownFrom f n)
  applyDownFrom⁺₂ f n Rf = applyDownFrom⁺₁ f n (λ _ _ → Rf _ _)

------------------------------------------------------------------------
-- tabulate

module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) →
              AllPairs R (tabulate f)
  tabulate⁺ {zero}  fᵢ~fⱼ = []
  tabulate⁺ {suc n} fᵢ~fⱼ =
    All.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷
    tabulate⁺ (fᵢ~fⱼ ∘ (_∘ suc-injective))

------------------------------------------------------------------------
-- filter

module _ {a ℓ p} {A : Set a} {R : Rel A ℓ}
         {P : Pred A p} (P? : Decidable P) where

  filter⁺ : ∀ {xs} → AllPairs R xs → AllPairs R (filter P? xs)
  filter⁺ {_}      []           = []
  filter⁺ {x ∷ xs} (x∉xs ∷ xs!) with does (P? x)
  ... | false = filter⁺ xs!
  ... | true  = All.filter⁺ P? x∉xs ∷ filter⁺ xs!


text:
record R₁ (M : Set → Set) : Set₁ where
  field
    return : ∀ {A} → A → M A
    map    : ∀ {A B} → (A → B) → M A → M B

open R₁ ⦃ … ⦄ public

record R₂ (M : Set → Set) : Set₁ where
  field
    instance
      r₁ : R₁ M

data Wrap₁ (A : Set) : Set where
  box : A → Wrap₁ A

instance

  r₁ : R₁ Wrap₁
  R₁.return r₁ x         = box x
  R₁.map    r₁ f (box x) = box (f x)

record Wrap₂ (A : Set) : Set where
  field
    run : A

postulate
  instance
    r₂ : R₂ Wrap₂

  A     : Set
  f     : A → A
  g     : A → Wrap₁ A
  _≡_   : {A : Set} → A → A → Set
  refl  : {A : Set} (x : A) → x ≡ x
  trans : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
  id    : {A : Set} (x : A) {y : A} → x ≡ y → x ≡ y

h : ∀ x → map f (g x) ≡ map f (return x) → map f (g x) ≡ return (f x)
h x eq =
  trans (map f (g x))
    eq
    (id (map f (return x))
        (refl (return (f x))))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Algebra
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.List.Any as LA using (Any; here; there)
open import Data.List.Any.BagAndSetEquality as B
open import Data.Product as PR using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; flip)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as I using ()
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)

open import Data.Environment
open import nodcap.Base
open import nodcap.NF.Typing

module nodcap.NF.Expand where

open I.Inverse using (to; from)
private module ++ {a} {A : Set a} = Monoid (L.monoid A)

{-# TERMINATING #-}
-- Lemma:
--   We can expand an instance of ?[ n ] A into n repetitions of A,
--   by induction on n.
--
-- Problematic calls:
--   * in the recursive call under cont, the index n is split as
--     n₁ + n₂, for which we have n₁, n₂ < n, but not definitionally.
mutual
  expand : {Γ : Environment} {A : Type} {n : ℕ⁺} →

    ⊢ⁿᶠ ?[ n ] A ∷ Γ →
    --------------------
    ⊢ⁿᶠ replicate⁺ n A ++ Γ

  expand (mk?₁ x) = x
  expand (cont {Γ} {A} {m} {n} x)
    = P.subst (λ Δ → ⊢ⁿᶠ Δ ++ Γ) (replicate⁺-++-commute m n)
    $ P.subst ⊢ⁿᶠ_ (P.sym (++.assoc (replicate⁺ m A) (replicate⁺ n A) Γ))
    $ exch (swp [] (replicate⁺ m A) (replicate⁺ n A))
    $ expand {n = n}
    $ exch (fwd [] (replicate⁺ m A))
    $ expand {n = m} x
  expand {Γ} {A} {n} (exch b x)
    = exch (B.++-cong {xs₁ = replicate⁺ n A} I.id (del-from b (here P.refl)))
    $ expandIn (from b ⟨$⟩ here P.refl) x

  expandIn : {Γ : Environment} {A : Type} {n : ℕ⁺} (i : ?[ n ] A ∈ Γ) →

    ⊢ⁿᶠ Γ →
    ----------------------------
    ⊢ⁿᶠ replicate⁺ n A ++ Γ - i

  expandIn (here P.refl) x = expand x
  expandIn {_} {A} {n} (there i) (send {Γ} {Δ} x h)
    with split Γ i
  ... | inj₁ (j , p) rewrite p
      = exch (swp [] (replicate⁺ n A) (_ ∷ []))
      $ P.subst ⊢ⁿᶠ_ (++.assoc (_ ∷ replicate⁺ n A) (Γ - j) Δ)
      $ flip send h
      $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
      $ expandIn (there j) x
  ... | inj₂ (j , p) rewrite p
      = exch (swp [] (replicate⁺ n A) (_ ∷ Γ))
      $ send x
      $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
      $ expandIn (there j) h
  expandIn {Γ} {A} {n} (there i) (recv x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ recv
    $ exch (swp [] (_ ∷ _ ∷ []) (replicate⁺ n A))
    $ expandIn (there (there i)) x
  expandIn {Γ} {A} {n} (there i) (sel₁ x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ sel₁
    $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
    $ expandIn (there i) x
  expandIn {Γ} {A} {n} (there i) (sel₂ x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ sel₂
    $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
    $ expandIn (there i) x
  expandIn {Γ} {A} {n} (there i) (case x h)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ case
      ( exch (swp [] (_ ∷ []) (replicate⁺ n A))
      $ expandIn (there i) x )
      ( exch (swp [] (_ ∷ []) (replicate⁺ n A))
      $ expandIn (there i) h )
  expandIn (there ()) halt
  expandIn {Γ} {A} {n} (there i) (wait x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ wait
    $ expandIn i x
  expandIn {Γ} {A} {n} (there i)  loop
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ loop
  expandIn {Γ} {A} {n} (there i) (mk?₁ x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ mk?₁
    $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
    $ expandIn (there i) x
  expandIn {Γ} {A} {n} (there i) (mk!₁ x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ mk!₁
    $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
    $ expandIn (there i) x
  expandIn {Γ} {A} {n} (there i) (cont x)
    = exch (swp [] (replicate⁺ n A) (_ ∷ []))
    $ cont
    $ exch (swp [] (_ ∷ _ ∷ []) (replicate⁺ n A))
    $ expandIn (there (there i)) x
  expandIn {_} {A} {n} (there i) (pool {Γ} {Δ} x y)
    with split Γ i
  ... | inj₁ (j , p) rewrite p
      = exch (swp [] (replicate⁺ n A) (_ ∷ []))
      $ P.subst ⊢ⁿᶠ_ (++.assoc (_ ∷ replicate⁺ n A) (Γ - j) Δ)
      $ flip pool y
      $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
      $ expandIn (there j) x
  ... | inj₂ (j , p) rewrite p
      = exch (swp [] (replicate⁺ n A) (_ ∷ Γ))
      $ pool x
      $ exch (swp [] (_ ∷ []) (replicate⁺ n A))
      $ expandIn (there j) y
  expandIn {Γ} {A} {n} i (exch b x)
    = exch (B.++-cong {xs₁ = replicate⁺ n A} I.id (del-from b i))
    $ expandIn (from b ⟨$⟩ i) x

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
open import Type

module Graph {ℓ₁ ℓ₂} (V : Type{ℓ₁}) where

-- A graph is represented by a binary relation which states whether there is an edge from one vertex to another.
-- In other words, a graph is here defined by only its adjacency relation.
-- This is by default (without any assumptions) a directed multigraph which is possibly infinite.
--
-- An object of type Graph is the adjacency relation.
-- For (_⟶_ : Graph), (a b : V), an object of type (a ⟶ b) is an edge from vertices a to b, and its existence means that there is an edge from a to b.
Graph : Type
Graph = (V → V → Type{ℓ₂})

module _ (_⟶_ : Graph) where
  -- Two vertices are adjacent when there is an edge from the first one to the second one.
  Adjacent = _⟶_

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Definition of Terminal object and some properties

module Categories.Object.Terminal {o ℓ e} (C : Category o ℓ e) where

open import Level

open import Relation.Binary using (IsEquivalence; Setoid)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Morphism C
open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟)
open import Categories.Morphism.Reasoning C

open Category C
open HomReasoning

record Terminal : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊤ : Obj
    ! : {A : Obj} → (A ⇒ ⊤)
    !-unique : ∀ {A} → (f : A ⇒ ⊤) → ! ≈ f

  !-unique₂ : ∀ {A} {f g : A ⇒ ⊤} → f ≈ g
  !-unique₂ {A} {f} {g} = begin
    f ≈˘⟨ !-unique f ⟩
    ! ≈⟨ !-unique g ⟩
    g ∎
    where open HomReasoning

  ⊤-id : (f : ⊤ ⇒ ⊤) → f ≈ id
  ⊤-id _ = !-unique₂

open Terminal

from-⊤-is-Mono : ∀ {A : Obj} {t : Terminal} → (f : ⊤ t ⇒ A) → Mono f
from-⊤-is-Mono {_} {t} _ = λ _ _ _ → !-unique₂ t

up-to-iso : (t₁ t₂ : Terminal) → ⊤ t₁ ≅ ⊤ t₂
up-to-iso t₁ t₂ = record
  { from = ! t₂
  ; to   = ! t₁
  ; iso  = record { isoˡ = ⊤-id t₁ _; isoʳ = ⊤-id t₂ _ }
  }

transport-by-iso : (t : Terminal) → ∀ {X} → ⊤ t ≅ X → Terminal
transport-by-iso t {X} t≅X = record
  { ⊤        = X
  ; !        = from ∘ ! t
  ; !-unique = λ h → begin
    from ∘ ! t     ≈⟨ refl⟩∘⟨ !-unique t (to ∘ h)  ⟩
    from ∘ to ∘ h  ≈⟨ cancelˡ isoʳ ⟩
    h              ∎
  }
  where open _≅_ t≅X

up-to-iso-unique : ∀ t t′ → (i : ⊤ t ≅ ⊤ t′) → up-to-iso t t′ ≃ i
up-to-iso-unique t t′ i = ⌞ !-unique t′ _ ⌟

up-to-iso-invˡ : ∀ {t X} {i : ⊤ t ≅ X} → up-to-iso t (transport-by-iso t i) ≃ i
up-to-iso-invˡ {t} {i = i} = up-to-iso-unique t (transport-by-iso t i) i

up-to-iso-invʳ : ∀ {t t′} → ⊤ (transport-by-iso t (up-to-iso t t′)) ≡ ⊤ t′
up-to-iso-invʳ {t} {t′} = ≡.refl

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- Non-empty lists
------------------------------------------------------------------------

module Data.List.NonEmpty where

open import Data.Product hiding (map)
open import Data.Nat
open import Data.Function
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.List as List using (List; []; _∷_)
open import Category.Monad
open import Relation.Binary.PropositionalEquality

infixr 5 _∷_ _∷ʳ_ _⁺++⁺_ _++⁺_ _⁺++_

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

length_-1 : ∀ {A} → List⁺ A → ℕ
length [ x ]  -1 = 0
length x ∷ xs -1 = 1 + length xs -1

------------------------------------------------------------------------
-- Conversion

fromVec : ∀ {n A} → Vec A (suc n) → List⁺ A
fromVec {zero}  (x ∷ _)  = [ x ]
fromVec {suc n} (x ∷ xs) = x ∷ fromVec xs

toVec : ∀ {A} (xs : List⁺ A) → Vec A (suc (length xs -1))
toVec [ x ]    = Vec.[_] x
toVec (x ∷ xs) = x ∷ toVec xs

lift : ∀ {A B} →
       (∀ {m} → Vec A (suc m) → ∃ λ n → Vec B (suc n)) →
       List⁺ A → List⁺ B
lift f xs = fromVec (proj₂ (f (toVec xs)))

fromList : ∀ {A} → A → List A → List⁺ A
fromList x xs = fromVec (Vec.fromList (x ∷ xs))

toList : ∀ {A} → List⁺ A → List A
toList = Vec.toList ∘ toVec

------------------------------------------------------------------------
-- Other operations

head : ∀ {A} → List⁺ A → A
head = Vec.head ∘ toVec

tail : ∀ {A} → List⁺ A → List A
tail = Vec.toList ∘ Vec.tail ∘ toVec

map : ∀ {A B} → (A → B) → List⁺ A → List⁺ B
map f = lift (λ xs → (, Vec.map f xs))

-- Right fold. Note that s is only applied to the last element (see
-- the examples below).

foldr : {A B : Set} → (A → B → B) → (A → B) → List⁺ A → B
foldr c s [ x ]    = s x
foldr c s (x ∷ xs) = c x (foldr c s xs)

-- Left fold. Note that s is only applied to the first element (see
-- the examples below).

foldl : {A B : Set} → (B → A → B) → (A → B) → List⁺ A → B
foldl c s [ x ]    = s x
foldl c s (x ∷ xs) = foldl c (c (s x)) xs

-- Append (several variants).

_⁺++⁺_ : ∀ {A} → List⁺ A → List⁺ A → List⁺ A
xs ⁺++⁺ ys = foldr _∷_ (λ x → x ∷ ys) xs

_⁺++_ : ∀ {A} → List⁺ A → List A → List⁺ A
xs ⁺++ ys = foldr _∷_ (λ x → fromList x ys) xs

_++⁺_ : ∀ {A} → List A → List⁺ A → List⁺ A
xs ++⁺ ys = List.foldr _∷_ ys xs

concat : ∀ {A} → List⁺ (List⁺ A) → List⁺ A
concat [ xs ]     = xs
concat (xs ∷ xss) = xs ⁺++⁺ concat xss

monad : RawMonad List⁺
monad = record
  { return = [_]
  ; _>>=_  = λ xs f → concat (map f xs)
  }

reverse : ∀ {A} → List⁺ A → List⁺ A
reverse = lift (,_ ∘′ Vec.reverse)

-- Snoc.

_∷ʳ_ : ∀ {A} → List⁺ A → A → List⁺ A
xs ∷ʳ x = foldr _∷_ (λ y → y ∷ [ x ]) xs

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

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private
 module Examples {A B : Set}
                 (_⊕_ : A → B → B)
                 (_⊗_ : B → A → B)
                 (f : A → B)
                 (a b c : A)
                 where

  hd : head (a ∷ b ∷ [ c ]) ≡ a
  hd = refl

  tl : tail (a ∷ b ∷ [ c ]) ≡ b ∷ c ∷ []
  tl = refl

  mp : map f (a ∷ b ∷ [ c ]) ≡ f a ∷ f b ∷ [ f c ]
  mp = refl

  right : foldr _⊕_ f (a ∷ b ∷ [ c ]) ≡ a ⊕ (b ⊕ f c)
  right = refl

  left : foldl _⊗_ f (a ∷ b ∷ [ c ]) ≡ (f a ⊗ b) ⊗ c
  left = refl

  ⁺app⁺ : (a ∷ b ∷ [ c ]) ⁺++⁺ (b ∷ [ c ]) ≡
          a ∷ b ∷ c ∷ b ∷ [ c ]
  ⁺app⁺ = refl

  ⁺app : (a ∷ b ∷ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
          a ∷ b ∷ c ∷ b ∷ [ c ]
  ⁺app = refl

  app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷ [ c ]) ≡
          a ∷ b ∷ c ∷ b ∷ [ c ]
  app⁺ = refl

  conc : concat ((a ∷ b ∷ [ c ]) ∷ [ b ∷ [ c ] ]) ≡
         a ∷ b ∷ c ∷ b ∷ [ c ]
  conc = refl

  rev : reverse (a ∷ b ∷ [ c ]) ≡ c ∷ b ∷ [ a ]
  rev = refl

  snoc : (a ∷ b ∷ [ c ]) ∷ʳ a ≡ a ∷ b ∷ c ∷ [ a ]
  snoc = refl

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of terms (Fig. 1a and 1b).
------------------------------------------------------------------------

-- The syntax of terms depends on the syntax of simple types
-- (because terms are indexed by types in order to rule out
-- ill-typed terms). But we are in the Parametric.* hierarchy, so
-- we don't know the full syntax of types, only how to lift the
-- syntax of base types into the syntax of simple types. This
-- means that we have to be parametric in the syntax of base
-- types, too.
--
-- In such parametric modules that depend on other parametric
-- modules, we first import our dependencies under a more
-- convenient name.

import Parametric.Syntax.Type as Type

-- Then we start the module proper, with parameters for all
-- extension points of our dependencies. Note that here, the
-- "Structure" naming convenion makes some sense, because we can
-- say that we need some "Type.Structure" in order to define the
-- "Term.Structure".

module Parametric.Syntax.Term
    (Base : Type.Structure)
  where

-- Now inside the module, we can open our dependencies with the
-- parameters for their extension points. Again, here the name
-- "Structure" makes some sense, because we can say that we want
-- to access the "Type.Structure" that is induced by Base.

open Type.Structure Base

-- At this point, we have dealt with the extension points of our
-- dependencies, and we have all the definitions about simple
-- types, contexts, variables, and variable sets in scope that we
-- provided in Parametric.Syntax.Type. Now we can proceed to
-- define our own extension point, following the pattern
-- explained in Parametric.Syntax.Type.

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function using (_∘_)
open import Data.Unit
open import Data.Sum

-- Our extension point is a set of primitives, indexed by the
-- types of their arguments and their return type. In general, if
-- you're confused about what an extension point means, you might
-- want to open the corresponding module in the Nehemiah
-- hierarchy to see how it is implemented in the example
-- plugin. In this case, that would be the Nehemiah.Syntax.Term
-- module.

Structure : Set₁
Structure = Type → Set

module Structure (Const : Structure) where

  -- Declarations of Term and Terms to enable mutual recursion.
  --
  -- Note that terms are indexed by contexts and types. In the
  -- paper, we define the abstract syntax of terms in Fig 1a and
  -- then define a type system in Fig 1b. All lemmas and theorems
  -- then explicitly specify that they only hold for well-typed
  -- terms. Here, we use the indices to define a type that can
  -- only hold well-typed terms in the first place.
  data Term
    (Γ : Context) :
    (τ : Type) → Set

  open import Base.Data.DependentList public

  -- (Terms Γ Σ) represents a list of terms with types from Σ
  -- with free variables bound in Γ.
  Terms : Context → Context → Set
  Terms Γ = DependentList (Term Γ)

  -- (Term Γ τ) represents a term of type τ
  -- with free variables bound in Γ.
  data Term Γ where
    -- constants aka. primitives
    const : ∀ {τ} →
      (c : Const τ) →
      Term Γ τ
    var : ∀ {τ} →
      (x : Var Γ τ) →
      Term Γ τ
    app : ∀ {σ τ}
      (s : Term Γ (σ ⇒ τ)) →
      (t : Term Γ σ) →
      Term Γ τ
    -- we use de Bruijn indices, so we don't need binding occurrences.
    abs : ∀ {σ τ}
      (t : Term (σ • Γ) τ) →
      Term Γ (σ ⇒ τ)

  -- Free variables
  FV : ∀ {τ Γ} → Term Γ τ → Vars Γ

  FV (const ι) = none
  FV (var x) = singleton x
  FV (abs t) = tail (FV t)
  FV (app s t) = FV s ∪ FV t

  closed? : ∀ {τ Γ} → (t : Term Γ τ) → (FV t ≡ none) ⊎ ⊤
  closed? t = empty? (FV t)

  -- Weakening

  weaken : ∀ {Γ₁ Γ₂ τ} →
    (Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
    Term Γ₁ τ →
    Term Γ₂ τ
  weaken Γ₁≼Γ₂ (const c) = const c
  weaken Γ₁≼Γ₂ (var x) = var (weaken-var Γ₁≼Γ₂ x)
  weaken Γ₁≼Γ₂ (app s t) = app (weaken Γ₁≼Γ₂ s) (weaken Γ₁≼Γ₂ t)
  weaken Γ₁≼Γ₂ (abs {σ} t) = abs (weaken (keep σ • Γ₁≼Γ₂) t)

  -- Specialized weakening
  weaken₁ : ∀ {Γ σ τ} →
    Term Γ τ → Term (σ • Γ) τ
  weaken₁ t = weaken (drop _ • ≼-refl) t

  weaken₂ : ∀ {Γ α β τ} →
    Term Γ τ → Term (α • β • Γ) τ
  weaken₂ t = weaken (drop _ • drop _ • ≼-refl) t

  weaken₃ : ∀ {Γ α β γ τ} →
    Term Γ τ → Term (α • β • γ • Γ) τ
  weaken₃ t = weaken (drop _ • drop _ • drop _ • ≼-refl) t

  -- Shorthands for nested applications
  app₂ : ∀ {Γ α β γ} →
    Term Γ (α ⇒ β ⇒ γ) →
    Term Γ α → Term Γ β → Term Γ γ
  app₂ f x = app (app f x)

  app₃ : ∀ {Γ α β γ δ} →
    Term Γ (α ⇒ β ⇒ γ ⇒ δ) →
    Term Γ α → Term Γ β → Term Γ γ → Term Γ δ
  app₃ f x = app₂ (app f x)

  app₄ : ∀ {Γ α β γ δ ε} →
    Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε) →
    Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
    Term Γ ε
  app₄ f x = app₃ (app f x)

  app₅ : ∀ {Γ α β γ δ ε ζ} →
    Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε ⇒ ζ) →
    Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
    Term Γ ε → Term Γ ζ
  app₅ f x = app₄ (app f x)

  app₆ : ∀ {Γ α β γ δ ε ζ η} →
    Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε ⇒ ζ ⇒ η) →
    Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
    Term Γ ε → Term Γ ζ → Term Γ η
  app₆ f x = app₅ (app f x)

  -- HOAS-like smart constructors for lambdas, for different arities.

  -- We could also write this:
  module NamespaceForBadAbs₁ where
    abs₁′ :
      ∀ {Γ τ₁ τ} →
        (Term (τ₁ • Γ) τ₁ → Term (τ₁ • Γ) τ) →
        (Term Γ (τ₁ ⇒ τ))
    abs₁′ {Γ} {τ₁} = λ f → abs (f (var this))

  -- However, this is less general, and it is harder to reuse. In particular,
  -- this cannot be used inside abs₂, ..., abs₆.

  -- Now, let's write other variants with a loop!
  open import Data.Vec using (_∷_; []; Vec; foldr; [_]; reverse)
  open import Data.Nat
  module AbsNHelpers where
    open import Function
    hoasArgType : ∀ {n} → Context → Type → Vec Type n → Set
    hoasArgType Γ τres = foldr _ (λ a b → a → b) (Term Γ τres) ∘ Data.Vec.map (Term Γ)
    -- That is,
    --hoasArgType Γ τres [] = Term Γ τres
    --hoasArgType Γ τres (τ₀ ∷ τs) = Term Γ τ₀ → hoasArgType Γ τres τs

    hoasResType : ∀ {n} → Type → Vec Type n → Type
    hoasResType τres = foldr _ _⇒_ τres

    absNType : {n : ℕ} → Vec _ n → Set
    absNType τs = ∀ {Γ τres} →
      (f : ∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → hoasArgType Γ′ τres τs) →
      Term Γ (hoasResType τres τs)

    drop-≼-l : ∀ {Γ Γ′ τ} → (τ • Γ ≼ Γ′) → Γ ≼ Γ′
    drop-≼-l Γ′≼Γ′₁ = ≼-trans (drop _ • ≼-refl) Γ′≼Γ′₁

    absN : {n : ℕ} → (τs : Vec _ n) → absNType τs
    absN []        f = f {Γ≼Γ′ = ≼-refl}
    absN (τ₁ ∷ τs) f =
      abs (absN τs
        (λ {_} {Γ′≼Γ′₁} →
          f
            {Γ≼Γ′ = drop-≼-l Γ′≼Γ′₁}
            (weaken Γ′≼Γ′₁ (var this))))

    -- Using a similar trick, we can declare absV (where V stands for variadic),
    -- which takes the N implicit type arguments individually, collects them and
    -- passes them on to absN. This is inspired by the example in the Agda 2.4.0
    -- release notes about support for varying arity. To collect them, we need
    -- to use an accumulator argument.

    absVType : ∀ n {m} (τs : Vec Type m) → Set
    absVType zero       τs = absNType (reverse τs)
    absVType (suc n) τs = {τ₁ : Type} → absVType n (τ₁ ∷ τs)

    absVAux : ∀ {m} → (τs : Vec Type m) → ∀ n → absVType n τs
    absVAux τs zero    = absN (reverse τs)
    -- (Support for varying arity does not work here, so {τ₁} must be bound in
    -- the right-hand side).
    absVAux τs (suc n) {τ₁} = absVAux (τ₁ ∷ τs) n --λ {τ₁} → absVAux (τ₁ ∷ τs) n

    -- "Initialize" accumulator to the empty list.
    absV = absVAux []
    -- We could maybe define absV directly, without going through absN, by
    -- making hoasArgType and hoasResType also variadic, but I don't see a clear
    -- advantage.

  open AbsNHelpers using (absV) public

  {-
  Example types:
  absV 1:
    {τ₁ : Type} {Γ : Context} {τres : Type} →
      ({Γ′ : Context} {Γ≼Γ′ : Γ ≼ Γ′} → Term Γ′ τ₁ → Term Γ′ τres) →
      Term Γ (τ₁ ⇒ τres)

  absV 2:
    {τ₁ : Type} {τ₁ = τ₂ : Type} {Γ : Context} {τres : Type} →
      ({Γ′ : Context} {Γ≼Γ′ : Γ ≼ Γ′} →
       Term Γ′ τ₁ → Term Γ′ τ₂ → Term Γ′ τres) →
      Term Γ (τ₁ ⇒ τ₂ ⇒ τres)

  -}

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --type-in-type --no-pattern-matching #-}
open import Spire.IDarkwingDuck.Primitive
open import Spire.IDarkwingDuck.Derived
module Spire.IDarkwingDuck.Examples where

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

ℕR : Data
ℕR = Decl End End
  ("zero" ∷ "suc" ∷ [])
  (End tt , Rec tt (End tt) , tt)

ℕ : Set
ℕ = Form ℕR

zero : ℕ
zero = inj ℕR here

suc : ℕ → ℕ
suc = inj ℕR (there here)

VecR : Data
VecR = Decl
  (Arg Set λ _ → End)
  (λ _ → Arg ℕ λ _ → End)
  ("nil" ∷ "cons" ∷ [])
  (λ A →
    End (zero , tt)
  , IArg ℕ (λ n → Arg A λ _ → Rec (n , tt) (End (suc n , tt)))
  , tt
  )

Vec : (A : Set) → ℕ → Set
Vec = Form VecR

nil : {A : Set} → Vec A zero
nil = inj VecR here

cons : {A : Set} {n : ℕ} (x : A) (xs : Vec A n) → Vec A (suc n)
cons = inj VecR (there here)

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

add : ℕ → ℕ → ℕ
add = elim ℕR
  (λ n → ℕ → ℕ)
  (λ n → n)
  (λ m ih n → suc (ih n))

mult : ℕ → ℕ → ℕ
mult = elim ℕR
  (λ n → ℕ → ℕ)
  (λ n → zero)
  (λ m ih n → add n (ih n))

append : {A : Set} {m n : ℕ} (xs : Vec A m) (ys : Vec A n) → Vec A (add m n)
append {A} {m} {n} = elim VecR
  (λ m xs → (ys : Vec A n) → Vec A (add m n))
  (λ ys → ys)
  (λ x xs ih ys → cons x (ih ys))
  m

concat : {A : Set} {m n : ℕ} (xss : Vec (Vec A m) n) → Vec A (mult n m)
concat {A} {m} {n} = elim VecR
  (λ n xss → Vec A (mult n m))
  nil
  (λ xs xss ih → append xs ih)
  n

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

one : ℕ
one = suc zero

two : ℕ
two = suc one

three : ℕ
three = suc two

[1,2] : Vec ℕ two
[1,2] = cons one (cons two nil)

[3] : Vec ℕ one
[3] = cons three nil

[1,2,3] : Vec ℕ three
[1,2,3] = cons one (cons two (cons three nil))

test-append : [1,2,3] ≡ append [1,2] [3]
test-append = refl

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
module 08-higherOrder where

explicitize : ∀ {A : Set} {B : A → Set} → ({{x : A}} → B x) → (x : A) → B x
explicitize f x = f {{x}}

implicitize : ∀ {A : Set} {B : A → Set} → ((x : A) → B x) → {{x : A}} → B x
implicitize f {{x}} = f x

data T : Set where
  tt : T

test = explicitize (λ {{t : T}} → t)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2018-11-23, issue #3404, regression in Agda 2.5.4
--
-- The positivity checker judged postulates in mutual blocks
-- as constants, since it found no uses of its arguments.
--
-- The natural cure is to not unleash the positivity checker
-- onto things that do not have a definition, such as postulates.

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

cong : ∀{A B : Set} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

trans : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

module UnsolvedMeta where

  postulate        A : Set
  mutual postulate B : A → Set       -- Problem WAS: B is judged constant
  postulate        f : (a : A) → B a

  g : (a : A) → B a
  g a = f _  -- WAS: yellow

  -- Should solve.

-- False golfing:

module Word64 where

  {-# BUILTIN WORD64 Word64 #-}

  primitive        primWord64ToNat   : Word64 → Nat
  mutual primitive primWord64FromNat : Nat → Word64
    -- Before fix of #3404, positivity checker judged
    -- a primitive in a mutual block as constant.

  fromNatConst : ∀ x y → primWord64FromNat x ≡ primWord64FromNat y
  fromNatConst x y = refl

  -- Should fail with error like:
  --
  -- x != y of type Nat
  -- when checking that the expression refl has type
  -- primWord64FromNat x ≡ primWord64FromNat y

  0≡1 : 0 ≡ 1
  0≡1 = cong primWord64ToNat (fromNatConst 0 1)

-- Guillaume Brunerie's original example:

mutual
  postulate
    2^  : Nat → Nat  -- If this function is deemed constant,
    2^0 : 1 ≡ 2^ 0   -- then these equalities can be composed.
    2^1 : 2^ 1 ≡ 2

bad : 1 ≡ 2
bad = trans 2^0 2^1

-- Should fail with error like:
--
-- 1 != 0 of type Nat
-- when checking that the expression 2^1 has type 2^ 0 ≡ 2

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
-- Andreas, 2014-09-02, reported by Nisse

-- {-# OPTIONS -v scope.mod.inst:30 #-}

record R : Set₁ where
  field
    A : Set

-- works : (A : R) → let open R A renaming (A to B) in B → B
-- works _ a = a

test : (A : R) → let open R A in A → A
test _ a = a

-- WAS:
-- Either the A introduced by the let should shadow the outer A, or an
-- ambiguity error should be raised. Current error message:
--
-- R !=< Set of type Set₁
-- when checking that the expression A has type Set

-- NOW: ambiguity error.


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Monoid.BigOp where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.SIP

open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.FinData

open import Cubical.Algebra.Monoid.Base

private
  variable
    ℓ ℓ' : Level

module MonoidBigOp (M' : Monoid ℓ) where
 private M = ⟨ M' ⟩
 open MonoidStr (snd M')

 bigOp : {n : ℕ} → FinVec M n → M
 bigOp = foldrFin _·_ ε

 bigOpExt : ∀ {n} {V W : FinVec M n} → ((i : Fin n) → V i ≡ W i) → bigOp V ≡ bigOp W
 bigOpExt h = cong bigOp (funExt h)

 bigOpε : ∀ n → bigOp (replicateFinVec n ε) ≡ ε
 bigOpε zero = refl
 bigOpε (suc n) = cong (ε ·_) (bigOpε n) ∙ ·IdR _

 bigOpLast : ∀ {n} (V : FinVec M (suc n)) → bigOp V ≡ bigOp (V ∘ weakenFin) · V (fromℕ n)
 bigOpLast {n = zero} V = ·IdR _ ∙ sym (·IdL _)
 bigOpLast {n = suc n} V = cong (V zero ·_) (bigOpLast (V ∘ suc)) ∙ ·Assoc _ _ _

 -- requires a commutative monoid:
 bigOpSplit : (∀ x y → x · y ≡ y · x)
            → {n : ℕ} → (V W : FinVec M n) → bigOp (λ i → V i · W i) ≡ bigOp V · bigOp W
 bigOpSplit _ {n = zero} _ _ = sym (·IdR _)
 bigOpSplit comm {n = suc n} V W =
    V zero · W zero · bigOp (λ i → V (suc i) · W (suc i))
  ≡⟨ (λ i → V zero · W zero · bigOpSplit comm (V ∘ suc) (W ∘ suc) i) ⟩
    V zero · W zero · (bigOp (V ∘ suc) · bigOp (W ∘ suc))
  ≡⟨ sym (·Assoc _ _ _) ⟩
    V zero · (W zero · (bigOp (V ∘ suc) · bigOp (W ∘ suc)))
  ≡⟨ cong (V zero ·_) (·Assoc _ _ _) ⟩
    V zero · ((W zero · bigOp (V ∘ suc)) · bigOp (W ∘ suc))
  ≡⟨ cong (λ x → V zero · (x · bigOp (W ∘ suc))) (comm _ _) ⟩
    V zero · ((bigOp (V ∘ suc) · W zero) · bigOp (W ∘ suc))
  ≡⟨ cong (V zero ·_) (sym (·Assoc _ _ _)) ⟩
    V zero · (bigOp (V ∘ suc) · (W zero · bigOp (W ∘ suc)))
  ≡⟨ ·Assoc _ _ _ ⟩
    V zero · bigOp (V ∘ suc) · (W zero · bigOp (W ∘ suc)) ∎

 bigOpSplit++ : (∀ x y → x · y ≡ y · x)
              → {n m : ℕ} → (V : FinVec M n) → (W : FinVec M m)
              → bigOp (V ++Fin W) ≡ bigOp V · bigOp W

 bigOpSplit++ comm {n = zero} V W = sym (·IdL _)
 bigOpSplit++ comm {n = suc n} V W = cong (V zero ·_) (bigOpSplit++ comm (V ∘ suc) W) ∙ ·Assoc _ _ _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ {A : Set} (P : A → Set) where

  postulate
    bla : {x : A} {{_ : P x}} → Set → Set

  test :  {x : A} {{_ : P x}} → Set → Set
  test B = bla B


text:
module Issue4408 where

comp :
  (A : Set)
  (B : A → Set)
  (C : (x : A) → B x → Set) →
  ((x : A) (y : B x) → C x y) →
  (g : (x : A) → B x) →
  ((x : A) → C x (g x))
comp _ _ _ f g x = f x (g x)

data Unit : Set where
  unit : Unit

P : Unit → Set
P unit = Unit

Q : Unit → Set → Set
Q unit = λ _ → Unit

f : (x : Unit) → P x → P x
f unit x = x

g :
  (A : Set) →
  ((x : Unit) → Q x A → P x) →
  ((x : Unit) → Q x A → P x)
g A h x = comp _ _ _ (λ _ → f _) (h _)

max_forks_repo_name: shlevy/agda


text:
import      Lvl
open import Type

module Type.Functions {ℓₗ : Lvl.Level}{ℓₒ₁}{ℓₒ₂} {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where

open import Function.Domains
open import Type.Properties.Empty
open import Type.Properties.Singleton

record Bijective (f : X → Y) : Type{ℓₗ Lvl.⊔ ℓₒ₁ Lvl.⊔ ℓₒ₂} where
  constructor intro
  field
    proof : ∀{y} → IsUnit{ℓₗ Lvl.⊔ ℓₒ₁} (Unapply {ℓₗ}{X = X}{Y = Y} f(y))

record Injective (f : X → Y) : Type{ℓₗ Lvl.⊔ ℓₒ₁ Lvl.⊔ ℓₒ₂} where
  constructor intro
  field
    proof : ∀{y} → MereProposition{ℓₗ Lvl.⊔ ℓₒ₁} (Unapply {ℓₗ}{X = X}{Y = Y} f(y))

record Surjective (f : X → Y) : Type{ℓₗ Lvl.⊔ ℓₒ₁ Lvl.⊔ ℓₒ₂} where
  constructor intro
  field
    proof : ∀{y} → ◊(Unapply {ℓₗ}{X = X}{Y = Y} f(y))


text:
------------------------------------------------------------------------
-- Parallel substitutions (defined using an inductive family)
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Basics
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import Function using (id; _∘_; _$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
 module Dummy₁ {t} (T : Term-like t) where

  open Term-like T

  infixl 5 _▻_

  -- Substitutions, represented as sequences of terms.

  data Sub : ∀ {Γ Δ} → Γ ⇨̂ Δ → Set (i ⊔ u ⊔ e ⊔ t) where
    ε   : ∀ {Δ} → Sub ε̂[ Δ ]
    _▻_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
          (ρ : Sub ρ̂) (t : Δ ⊢ σ /̂ ρ̂) → Sub (ρ̂ ▻̂[ σ ] ⟦ t ⟧)

  -- A sequence of matching substitutions. (The reflexive transitive
  -- closure of Sub.)

  data Subs {Γ} : ∀ {Δ} → Γ ⇨̂ Δ → Set (i ⊔ u ⊔ e ⊔ t) where
    ε   : Subs îd[ Γ ]
    _▻_ : ∀ {Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
          (ρs : Subs ρ̂₁) (ρ : Sub ρ̂₂) → Subs (ρ̂₁ ∘̂ ρ̂₂)

open Dummy₁ public

-- Originally these substitutions were defined without the context
-- morphism index, but this led to the need to prove lots of lemmas
-- which hold by definition in the current setting. As an example the
-- map function (in deBruijn.Substitution.Data.Map) is currently
-- defined as follows:
--
--   -- Map.
--
--   map : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
--         [ T₁ ⟶ T₂ ] ρ̂₂ → Sub T₁ ρ̂₁ → Sub T₂ (ρ̂₁ ∘̂ ρ̂₂)
--   map           f ε        = ε
--   map {ρ̂₂ = ρ̂₂} f (ρ₁ ▻ t) =
--     P.subst (λ v → Sub T₂ (⟦ ρ₁ ⟧⇨ ∘̂ ρ̂₂ ▻̂ v))
--             (≅-Value-⇒-≡ $ P.sym $ corresponds f t)
--             (map f ρ₁ ▻ f · t)
--
-- Previously it was defined roughly as follows (the code below is
-- untested and has been adapted to the current version of the
-- library, as it was at the time of writing, with some imagined
-- changes):
--
--   mutual
--
--     -- Map.
--
--     map : ∀ {Γ Δ Ε} {ρ̂₂ : Δ ⇨̂ Ε} →
--           [ T₁ ⟶ T₂ ] ρ̂₂ → (ρ₁ : Γ ⇨₁ Δ) → Γ ⇨₂ Ε
--     map f ε                 = ε
--     map f (_▻_ {σ = σ} ρ t) =
--       map f ρ ▻
--       P.subst (λ ρ̂ → _ ⊢₂ σ /̂ ρ̂)
--               (≅-⇨̂-⇒-≡ $ P.sym $ map-lemma f ρ)
--               (f · t)
--
--     abstract
--
--       map-lemma :
--         ∀ {Γ Δ Ε} {ρ̂₂ : Δ ⇨̂ Ε} →
--         (f : [ T₁ ⟶ T₂ ] ρ̂₂) (ρ₁ : Γ ⇨₁ Δ) →
--         ⟦ map f ρ₁ ⟧₂⇨ ≅-⇨̂ ⟦ ρ₁ ⟧₁⇨ ∘̂ ρ₂
--       map-lemma           f ε                 = P.refl
--       map-lemma {ρ₂ = ρ₂} f (_▻_ {σ = σ} ρ t) =
--         ▻̂-cong P.refl (map-lemma f ρ) (begin
--           [ ⟦ P.subst (λ ρ̂ → _ ⊢₂ σ /̂ ρ̂)
--                       (≅-⇨̂-⇒-≡ $ P.sym (map-lemma f ρ))
--                       (f · t) ⟧₂                        ]  ≡⟨ Term-like.⟦⟧-cong T₂
--                                                                 (Term-like.drop-subst-⊢ T₂
--                                                                    (λ ρ̂ → σ /̂ ρ̂)
--                                                                    (≅-⇨̂-⇒-≡ $ P.sym (map-lemma f ρ))) ⟩
--           [ ⟦ f · t ⟧₂                                  ]  ≡⟨ P.sym $ corresponds f t ⟩
--           [ ⟦ t ⟧₁ /̂Val ρ₂                              ]  ∎)

private
 module Dummy₂ {t} {T : Term-like t} where

  open Term-like T

  -- Some variants.

  ε⇨[_] : ∀ Δ → Sub T ε̂[ Δ ]
  ε⇨[ _ ] = ε

  infixl 5 _▻⇨[_]_

  _▻⇨[_]_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} →
            Sub T ρ̂ → ∀ σ (t : Δ ⊢ σ /̂ ρ̂) → Sub T (ρ̂ ▻̂[ σ ] ⟦ t ⟧)
  ρ ▻⇨[ _ ] t = ρ ▻ t

  ε⇨⋆[_] : ∀ Γ → Subs T îd[ Γ ]
  ε⇨⋆[ _ ] = ε

  -- Equality of substitutions.

  record [⇨] : Set (i ⊔ u ⊔ e ⊔ t) where
    constructor [_]
    field
      {Γ Δ} : Ctxt
      {ρ̂}   : Γ ⇨̂ Δ
      ρ     : Sub T ρ̂

  infix 4 _≅-⇨_

  _≅-⇨_ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (ρ₁ : Sub T ρ̂₁)
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (ρ₂ : Sub T ρ̂₂) → Set _
  ρ₁ ≅-⇨ ρ₂ = _≡_ {A = [⇨]} [ ρ₁ ] [ ρ₂ ]

  ≅-⇨-⇒-≡ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} {ρ₁ ρ₂ : Sub T ρ̂} →
            ρ₁ ≅-⇨ ρ₂ → ρ₁ ≡ ρ₂
  ≅-⇨-⇒-≡ P.refl = P.refl

  -- Certain uses of substitutivity can be removed.

  drop-subst-Sub :
    ∀ {a} {A : Set a} {x₁ x₂ : A} {Γ Δ}
    (f : A → Γ ⇨̂ Δ) {ρ} (eq : x₁ ≡ x₂) →
    P.subst (λ x → Sub T (f x)) eq ρ ≅-⇨ ρ
  drop-subst-Sub f P.refl = P.refl

  -- Equality of sequences of substitutions.

  record [⇨⋆] : Set (i ⊔ u ⊔ e ⊔ t) where
    constructor [_]
    field
      {Γ Δ} : Ctxt
      {ρ̂}   : Γ ⇨̂ Δ
      ρs    : Subs T ρ̂

  infix 4 _≅-⇨⋆_

  _≅-⇨⋆_ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (ρs₁ : Subs T ρ̂₁)
             {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (ρs₂ : Subs T ρ̂₂) → Set _
  ρs₁ ≅-⇨⋆ ρs₂ = _≡_ {A = [⇨⋆]} [ ρs₁ ] [ ρs₂ ]

  ≅-⇨⋆-⇒-≡ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} {ρs₁ ρs₂ : Subs T ρ̂} →
             ρs₁ ≅-⇨⋆ ρs₂ → ρs₁ ≡ ρs₂
  ≅-⇨⋆-⇒-≡ P.refl = P.refl

  -- Interpretation of substitutions: context morphisms.

  ⟦_⟧⇨ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Γ ⇨̂ Δ
  ⟦_⟧⇨ {ρ̂ = ρ̂} _ = ρ̂

  ⟦_⟧⇨⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T ρ̂ → Γ ⇨̂ Δ
  ⟦_⟧⇨⋆ {ρ̂ = ρ̂} _ = ρ̂

  -- Application of substitutions to types.

  infixl 8 _/I_ _/_ _/⋆_

  _/I_ : ∀ {Γ Δ i} {ρ̂ : Γ ⇨̂ Δ} → IType Γ i → Sub T ρ̂ → IType Δ i
  σ /I ρ = σ /̂I ⟦ ρ ⟧⇨

  _/_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Type Γ → Sub T ρ̂ → Type Δ
  σ / ρ = σ /̂ ⟦ ρ ⟧⇨

  _/⋆_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Type Γ → Subs T ρ̂ → Type Δ
  σ /⋆ ρs = σ /̂ ⟦ ρs ⟧⇨⋆

  -- Application of substitutions to values.

  infixl 8 _/Val_

  _/Val_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
           Value Γ σ → Sub T ρ̂ → Value Δ (σ /̂ ρ̂)
  v /Val ρ = v /̂Val ⟦ ρ ⟧⇨

  -- Application of substitutions to context extensions.

  infixl 8 _/⁺_ _/⁺⋆_ _/₊_ _/₊⋆_

  _/⁺_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt⁺ Γ → Sub T ρ̂ → Ctxt⁺ Δ
  Γ⁺ /⁺ ρ = Γ⁺ /̂⁺ ⟦ ρ ⟧⇨

  _/⁺⋆_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt⁺ Γ → Subs T ρ̂ → Ctxt⁺ Δ
  Γ⁺ /⁺⋆ ρs = Γ⁺ /̂⁺ ⟦ ρs ⟧⇨⋆

  _/₊_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt₊ Γ → Sub T ρ̂ → Ctxt₊ Δ
  Γ₊ /₊ ρ = Γ₊ /̂₊ ⟦ ρ ⟧⇨

  _/₊⋆_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt₊ Γ → Subs T ρ̂ → Ctxt₊ Δ
  Γ₊ /₊⋆ ρs = Γ₊ /̂₊ ⟦ ρs ⟧⇨⋆

  -- Application of substitutions to variables.

  infixl 8 _/∋_ _/∋-lemma_

  _/∋_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ∋ σ → (ρ : Sub T ρ̂) → Δ ⊢ σ / ρ
  zero  /∋ (ρ ▻ y) = y
  suc x /∋ (ρ ▻ y) = x /∋ ρ

  abstract

    _/∋-lemma_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρ : Sub T ρ̂) →
                 x /̂∋ ⟦ ρ ⟧⇨ ≅-Value ⟦ x /∋ ρ ⟧
    zero  /∋-lemma (ρ ▻ y) = P.refl
    suc x /∋-lemma (ρ ▻ y) = x /∋-lemma ρ

  app∋ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → [ Var ⟶ T ] ρ̂
  app∋ ρ = record
    { function    = λ _ x → x /∋       ρ
    ; corresponds = λ _ x → x /∋-lemma ρ
    }

  -- The tail of a nonempty substitution.

  tail : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} → Sub T ρ̂ → Sub T (t̂ail ρ̂)
  tail (ρ ▻ t) = ρ

  -- The head of a nonempty substitution.

  head : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) → Δ ⊢ σ / tail ρ
  head (ρ ▻ t) = t

  head-lemma : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) →
               ĥead ⟦ ρ ⟧⇨ ≅-Value ⟦ head ρ ⟧
  head-lemma (ρ ▻ t) = P.refl

  -- Fold for sequences of substitutions.

  fold : ∀ {f} (F : ∀ {Γ Δ} → Γ ⇨̂ Δ → Set f) {Γ} →
         F (îd {Γ = Γ}) →
         (∀ {Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
            F ρ̂₁ → Sub T ρ̂₂ → F (ρ̂₁ ∘̂ ρ̂₂)) →
         ∀ {Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T ρ̂ → F ρ̂
  fold F nil cons ε        = nil
  fold F nil cons (ρs ▻ ρ) = cons (fold F nil cons ρs) ρ

  -- Some congruence lemmas.

  ε⇨-cong : ∀ {Δ₁ Δ₂} → Δ₁ ≅-Ctxt Δ₂ → ε⇨[ Δ₁ ] ≅-⇨ ε⇨[ Δ₂ ]
  ε⇨-cong P.refl = P.refl

  ▻⇨-cong :
    ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {t₁ : Δ₁ ⊢ σ₁ / ρ₁}
      {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {t₂ : Δ₂ ⊢ σ₂ / ρ₂} →
    σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ → t₁ ≅-⊢ t₂ →
    ρ₁ ▻⇨[ σ₁ ] t₁ ≅-⇨ ρ₂ ▻⇨[ σ₂ ] t₂
  ▻⇨-cong P.refl P.refl P.refl = P.refl

  ε⇨⋆-cong : ∀ {Γ₁ Γ₂} → Γ₁ ≡ Γ₂ → ε⇨⋆[ Γ₁ ] ≅-⇨⋆ ε⇨⋆[ Γ₂ ]
  ε⇨⋆-cong P.refl = P.refl

  ▻⇨⋆-cong :
    ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
      {ρs₁ : Subs T ρ̂₁₁} {ρ₁ : Sub T ρ̂₂₁}
      {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
      {ρs₂ : Subs T ρ̂₁₂} {ρ₂ : Sub T ρ̂₂₂} →
    ρs₁ ≅-⇨⋆ ρs₂ → ρ₁ ≅-⇨ ρ₂ → ρs₁ ▻ ρ₁ ≅-⇨⋆ ρs₂ ▻ ρ₂
  ▻⇨⋆-cong P.refl P.refl = P.refl

  ⟦⟧⇨-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
             ρ₁ ≅-⇨ ρ₂ → ⟦ ρ₁ ⟧⇨ ≅-⇨̂ ⟦ ρ₂ ⟧⇨
  ⟦⟧⇨-cong P.refl = P.refl

  /I-cong :
    ∀ {i}
      {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {σ₁ : IType Γ₁ i} {ρ₁ : Sub T ρ̂₁}
      {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {σ₂ : IType Γ₂ i} {ρ₂ : Sub T ρ̂₂} →
    σ₁ ≅-IType σ₂ → ρ₁ ≅-⇨ ρ₂ → σ₁ /I ρ₁ ≅-IType σ₂ /I ρ₂
  /I-cong P.refl P.refl = P.refl

  /-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
             {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
           σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ → σ₁ / ρ₁ ≅-Type σ₂ / ρ₂
  /-cong P.refl P.refl = P.refl

  /⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
            Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ /⁺ ρ₁ ≅-Ctxt⁺ Γ⁺₂ /⁺ ρ₂
  /⁺-cong P.refl P.refl = P.refl

  /⁺⋆-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁}
               {Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} →
             Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρs₁ ≅-⇨⋆ ρs₂ →
             Γ⁺₁ /⁺⋆ ρs₁ ≅-Ctxt⁺ Γ⁺₂ /⁺⋆ ρs₂
  /⁺⋆-cong P.refl P.refl = P.refl

  /₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
            Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ → Γ₊₁ /₊ ρ₁ ≅-Ctxt₊ Γ₊₂ /₊ ρ₂
  /₊-cong P.refl P.refl = P.refl

  /₊⋆-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁}
               {Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} →
             Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρs₁ ≅-⇨⋆ ρs₂ →
             Γ₊₁ /₊⋆ ρs₁ ≅-Ctxt₊ Γ₊₂ /₊⋆ ρs₂
  /₊⋆-cong P.refl P.refl = P.refl

  /∋-cong : ∀ {Γ₁ Δ₁ σ₁} {x₁ : Γ₁ ∋ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
              {Γ₂ Δ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
            x₁ ≅-∋ x₂ → ρ₁ ≅-⇨ ρ₂ → x₁ /∋ ρ₁ ≅-⊢ x₂ /∋ ρ₂
  /∋-cong P.refl P.refl = P.refl

  tail-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ▻ σ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ▻ σ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
              ρ₁ ≅-⇨ ρ₂ → tail ρ₁ ≅-⇨ tail ρ₂
  tail-cong P.refl = P.refl

  head-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ▻ σ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ▻ σ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
              ρ₁ ≅-⇨ ρ₂ → head ρ₁ ≅-⊢ head ρ₂
  head-cong P.refl = P.refl

  abstract

    -- Some eta-laws.

    ηε : ∀ {Δ} {ρ̂ : ε ⇨̂ Δ} (ρ : Sub T ρ̂) → ρ ≅-⇨ ε⇨[ Δ ]
    ηε ε = P.refl

    η▻ : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) →
         ρ ≅-⇨ tail ρ ▻⇨[ σ ] head ρ
    η▻ (ρ ▻ t) = P.refl

    -- Two substitutions are equal if their indices are equal and
    -- their projections are pairwise equal.

    extensionality :
      ∀ {Γ Δ₁} {ρ̂₁ : Γ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
          {Δ₂} {ρ̂₂ : Γ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
      Δ₁ ≅-Ctxt Δ₂ → (∀ {σ} (x : Γ ∋ σ) → x /∋ ρ₁ ≅-⊢ x /∋ ρ₂) →
      ρ₁ ≅-⇨ ρ₂
    extensionality {ρ₁ = ε}       {ρ₂ = ε}       Δ₁≅Δ₂ hyp = ε⇨-cong Δ₁≅Δ₂
    extensionality {ρ₁ = ρ₁ ▻ t₁} {ρ₂ = ρ₂ ▻ t₂} Δ₁≅Δ₂ hyp =
      ▻⇨-cong P.refl
              (extensionality Δ₁≅Δ₂ (hyp ∘ suc))
              (hyp zero)

open Dummy₂ public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
-- Andreas, 2019-08-19, issue #4007 reported by nad

-- The scope checker was not run in the TCEnv of the interaction meta.
-- Thus, the extended lambda was not inheriting the IsAbstract from
-- the AbstractMode of the meta, leading to checking the
-- extended lambda in the wrong ConcreteMode.

-- {-# OPTIONS -v interaction.give:20 #-}
-- {-# OPTIONS -v scope.extendedLambda:10 #-}
-- {-# OPTIONS -v tc.term.exlam:20 #-}
-- -- {-# OPTIONS -v tc.decl:10 #-}
-- {-# OPTIONS -v tc.interaction:20 #-}
-- {-# OPTIONS -v tc.decl.abstract:25 #-}
-- {-# OPTIONS -v tc.meta.check:20 #-}
-- {-# OPTIONS -v tc.meta.new:50 #-}

abstract

  data D : Set where
    c : D

  works : D → D
  works = λ { c → c }

  test : D → D
  test = {!λ { c → c }!} -- give

-- Giving should succeed.


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

open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Rings.Lemmas
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Rings.IntegralDomains.Definition
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Fields.Fields
open import Fields.Orders.Total.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module Fields.Orders.Lemmas {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {o} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {F : Field R} {pRing : PartiallyOrderedRing R pOrder} (oF : TotallyOrderedField F pRing) where

abstract

  open import Rings.InitialRing R
  open Ring R
  open PartiallyOrderedRing pRing
  open Group additiveGroup
  open TotallyOrderedRing (TotallyOrderedField.oRing oF)
  open SetoidTotalOrder total
  open import Rings.Orders.Partial.Lemmas pRing
  open import Rings.Orders.Total.Lemmas (TotallyOrderedField.oRing oF)
  open import Fields.Lemmas F
  open Setoid S
  open SetoidPartialOrder pOrder
  open Equivalence eq
  open Field F

  clearDenominatorHalf : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → x < (y * 1/2) → (x + x) < y
  clearDenominatorHalf x y 1/2 pr1/2 x<1/2y = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *DistributesOver+) (Equivalence.transitive eq *Commutative (*WellDefined pr1/2 (Equivalence.reflexive eq)))) identIsIdent) (ringAddInequalities x<1/2y x<1/2y)

  clearDenominatorHalf' : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → (x * 1/2) < y → x < (y + y)
  clearDenominatorHalf' x y 1/2 pr1/2 1/2x<y = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq *DistributesOver+) (Equivalence.transitive eq (Equivalence.transitive eq *Commutative (*WellDefined pr1/2 (Equivalence.reflexive eq))) identIsIdent)) (Equivalence.reflexive eq) (ringAddInequalities 1/2x<y 1/2x<y)

  halveInequality : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → (x + x) < y → x < (y * 1/2)
  halveInequality x y 1/2 pr1/2 2x<y with totality 0R 1R
  ... | inl (inl 0<1') = <WellDefined (halfHalves 1/2 pr1/2) (Equivalence.reflexive eq) (ringCanMultiplyByPositive {_} {_} {1/2} (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 λ bad → irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bad) 0<1')))) 2x<y)
  ... | inl (inr 1<0) = <WellDefined (halfHalves 1/2 pr1/2) (Equivalence.reflexive eq) (ringCanMultiplyByPositive {_} {_} {1/2} (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 λ bad → irreflexive {0R} (<WellDefined (Equivalence.symmetric eq bad) (Equivalence.reflexive eq) 1<0)))) 2x<y)
  ... | inr 0=1 = exFalso (irreflexive {0R} (<WellDefined (oneZeroImpliesAllZero R 0=1) (oneZeroImpliesAllZero R 0=1) 2x<y))

  halveInequality' : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → x < (y + y) → (x * 1/2) < y
  halveInequality' x y 1/2 pr1/2 x<2y with halveInequality (inverse y) (inverse x) 1/2 pr1/2 (<WellDefined (invContravariant additiveGroup) (Equivalence.reflexive eq) (ringSwapNegatives' x<2y))
  ... | bl = ringSwapNegatives (<WellDefined (Equivalence.reflexive eq) (ringMinusExtracts' R) bl)

  dense : (charNot2 : ((1R + 1R) ∼ 0R) → False) {x y : A} → (x < y) → Sg A (λ i → (x < i) && (i < y))
  dense charNot2 {x} {y} x<y with halve charNot2 1R
  dense charNot2 {x} {y} x<y | 1/2 , pr1/2 = ((x + y) * 1/2) , (halveInequality x (x + y) 1/2 pr1/2 (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition x<y x)) ,, halveInequality' (x + y) y 1/2 pr1/2 (orderRespectsAddition x<y y))

  halfLess : (e/2 e : A) → (0<e : 0G < e) → (pr : e/2 + e/2 ∼ e) → e/2 < e
  halfLess e/2 e 0<e pr with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<e)
  ... | 0<e/2 = <WellDefined identLeft pr (orderRespectsAddition 0<e/2 e/2)

  inversePositiveIsPositive : {a b : A} → (a * b) ∼ 1R → 0R < b → 0R < a
  inversePositiveIsPositive {a} {b} ab=1 0<b with totality 0R a
  inversePositiveIsPositive {a} {b} ab=1 0<b | inl (inl 0<a) = 0<a
  inversePositiveIsPositive {a} {b} ab=1 0<b | inl (inr a<0) with <WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg _ _ 0<b a<0)
  ... | ab<0 = exFalso (1<0False (<WellDefined ab=1 (Equivalence.reflexive eq) ab<0))
  inversePositiveIsPositive {a} {b} ab=1 0<b | inr 0=a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<b))
    where
      0=1 : 0R ∼ 1R
      0=1 = Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) ab=1

  halvesEqual : ((1R + 1R ∼ 0R) → False) → (1/2 1/2' : A) → (1/2 + 1/2) ∼ 1R → (1/2' + 1/2') ∼ 1R → 1/2 ∼ 1/2'
  halvesEqual charNot2 1/2 1/2' pr1 pr2 = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq identIsIdent) (Equivalence.transitive eq *Commutative (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq p1) *Commutative)))) (Equivalence.transitive eq r (Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq *Commutative p1)) *Commutative) (identIsIdent)))
    where
      p : 1/2 * (1R + 1R) ∼ 1/2' * (1R + 1R)
      p = Equivalence.transitive eq *DistributesOver+ (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq *Commutative identIsIdent) (Equivalence.transitive eq *Commutative identIsIdent)) pr1) (Equivalence.transitive eq (Equivalence.symmetric eq pr2) (+WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative identIsIdent)) (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative identIsIdent))))) (Equivalence.symmetric eq *DistributesOver+))
      x : A
      x with Field.allInvertible F (1R + 1R) charNot2
      ... | y , _ = y
      p1 : (x * (1R + 1R)) ∼ 1R
      p1 with Field.allInvertible F (1R + 1R) charNot2
      ... | _ , pr = pr
      q : ((1/2 * (1R + 1R)) * x) ∼ ((1/2' * (1R + 1R)) * x)
      q = *WellDefined p (Equivalence.reflexive eq)
      r : (1/2 * ((1R + 1R) * x)) ∼ (1/2' * ((1R + 1R) * x))
      r = Equivalence.transitive eq *Associative (Equivalence.transitive eq q (Equivalence.symmetric eq *Associative))

  private
    orderedFieldIntDom : {a b : A} → (a * b ∼ 0R) → (a ∼ 0R) || (b ∼ 0R)
    orderedFieldIntDom {a} {b} ab=0 with totality 0R a
    ... | inl (inl x) = inr (Equivalence.transitive eq (Equivalence.transitive eq (symmetric identIsIdent) (*WellDefined q reflexive)) p')
      where
        a!=0 : (a ∼ Group.0G additiveGroup) → False
        a!=0 pr = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (symmetric pr) reflexive x)
        invA : A
        invA = underlying (Field.allInvertible F a a!=0)
        q : 1R ∼ (invA * a)
        q with Field.allInvertible F a a!=0
        ... | invA , pr = symmetric pr
        p : invA * (a * b) ∼ invA * Group.0G additiveGroup
        p = *WellDefined reflexive ab=0
        p' : (invA * a) * b ∼ Group.0G additiveGroup
        p' = Equivalence.transitive eq (symmetric *Associative) (Equivalence.transitive eq p (Ring.timesZero R))
    orderedFieldIntDom {a} {b} ab=0 | inl (inr x) = inr (Equivalence.transitive eq (Equivalence.transitive eq (symmetric identIsIdent) (*WellDefined q reflexive)) p')
      where
        a!=0 : (a ∼ Group.0G additiveGroup) → False
        a!=0 pr = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder reflexive (symmetric pr) x)
        invA : A
        invA = underlying (Field.allInvertible F a a!=0)
        q : 1R ∼ (invA * a)
        q with Field.allInvertible F a a!=0
        ... | invA , pr = symmetric pr
        p : invA * (a * b) ∼ invA * Group.0G additiveGroup
        p = *WellDefined reflexive ab=0
        p' : (invA * a) * b ∼ Group.0G additiveGroup
        p' = Equivalence.transitive eq (symmetric *Associative) (Equivalence.transitive eq p (Ring.timesZero R))
    orderedFieldIntDom {a} {b} ab=0 | inr x = inl (Equivalence.symmetric (Setoid.eq S) x)

  orderedFieldIsIntDom :  IntegralDomain R
  IntegralDomain.intDom orderedFieldIsIntDom = decidedIntDom R orderedFieldIntDom
  IntegralDomain.nontrivial orderedFieldIsIntDom pr = Field.nontrivial F (Equivalence.symmetric (Setoid.eq S) pr)

  charZero : (n : ℕ) → (0R ∼ (fromN (succ n))) → False
  charZero n 0=sn = irreflexive (<WellDefined 0=sn reflexive (fromNPreservesOrder (0<1 (Field.nontrivial F)) (succIsPositive n)))
  charZero' : (n : ℕ) → ((fromN (succ n)) ∼ 0R) → False
  charZero' n pr = charZero n (symmetric pr)