text:
open import Nat
open import Prelude
open import contexts
open import core
open import type-assignment-unicity

module canonical-indeterminate-forms where

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at base type
  data cif-base : (Δ : hctx) (d : iexp) → Set where
    CIFBEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⦈⟨ u , σ ⟩) ×
         ((u :: b [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
       → cif-base Δ d
    CIFBNEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: b [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-base Δ d
    CIFBAp : ∀ {Δ d} →
      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2 ∈ typ ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2 ==> b) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-base Δ d
    CIFBFst : ∀{Δ d} →
      Σ[ d' ∈ iexp ] Σ[ τ2 ∈ typ ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: b ⊗ τ2) ×
         (d' indet) ×
         (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
         (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
        )
        → cif-base Δ d
    CIFBSnd : ∀{Δ d} →
        Σ[ d' ∈ iexp ] Σ[ τ1 ∈ typ ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ1 ⊗ b) ×
         (d' indet) ×
         (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
         (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
        )
        → cif-base Δ d
    CIFBCast : ∀ {Δ d} →
      Σ[ d' ∈ iexp ]
        ((d == d' ⟨ ⦇·⦈ ⇒ b ⟩) ×
         (Δ , ∅ ⊢ d' :: ⦇·⦈) ×
         (d' indet) ×
         ((d'' : iexp) (τ' : typ) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
        )
        → cif-base Δ d
    CIFBFailedCast : ∀ {Δ d} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == d' ⟨ τ' ⇒⦇⦈⇏ b ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (τ' ≠ b)
        )
       → cif-base Δ d

  canonical-indeterminate-forms-base : ∀{Δ d} →
                                       Δ , ∅ ⊢ d :: b →
                                       d indet →
                                       cif-base Δ d
  canonical-indeterminate-forms-base TAConst ()
  canonical-indeterminate-forms-base (TAVar x₁) ()
  canonical-indeterminate-forms-base (TAAp wt wt₁) (IAp x ind x₁) = CIFBAp (_ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-base (TAEHole x x₁) IEHole = CIFBEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-base (TANEHole x wt x₁) (INEHole x₂) = CIFBNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-base (TACast wt x) (ICastHoleGround x₁ ind x₂) = CIFBCast (_ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-base (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) = CIFBFailedCast (_ , _ , refl , x , x₅ , x₇)
  canonical-indeterminate-forms-base (TAFst wt) (IFst ind h1 h2) = CIFBFst (_ , _ , refl , wt , ind , h1 , h2)
  canonical-indeterminate-forms-base (TASnd wt) (ISnd ind h1 h2) = CIFBSnd (_ , _ , refl , wt , ind , h1 , h2)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at arrow type
  data cif-arr : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
    CIFAEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⦈⟨ u , σ ⟩) ×
         ((u :: (τ1 ==> τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-arr Δ d τ1 τ2
    CIFANEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: (τ1 ==> τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-arr Δ d τ1 τ2
    CIFAAp : ∀{d Δ τ1 τ2} →
      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2' ∈ typ ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ==> τ2)) ×
         (Δ , ∅ ⊢ d2 :: τ2') ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFAFst : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: (τ1 ==> τ2) ⊗ τ') ×
         (d' indet) ×
         (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
         (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFASnd : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊗ (τ1 ==> τ2)) ×
         (d' indet) ×
         (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
         (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFACast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
        ((d == d' ⟨ (τ1' ==> τ2') ⇒ (τ1 ==> τ2) ⟩) ×
          (Δ , ∅ ⊢ d' :: τ1' ==> τ2') ×
          (d' indet) ×
          ((τ1' ==> τ2') ≠ (τ1 ==> τ2))
        )
       → cif-arr Δ d τ1 τ2
    CIFACastHole : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ iexp ]
        ((d == (d' ⟨ ⦇·⦈ ⇒ ⦇·⦈ ==> ⦇·⦈ ⟩)) ×
         (τ1 == ⦇·⦈) ×
         (τ2 == ⦇·⦈) ×
         (Δ , ∅ ⊢ d' :: ⦇·⦈) ×
         (d' indet) ×
         ((d'' : iexp) (τ' : typ) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFAFailedCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
          ((d == (d' ⟨ τ' ⇒⦇⦈⇏ ⦇·⦈ ==> ⦇·⦈ ⟩) ) ×
           (τ1 == ⦇·⦈) ×
           (τ2 == ⦇·⦈) ×
           (Δ , ∅ ⊢ d' :: τ') ×
           (τ' ground) ×
           (τ' ≠ (⦇·⦈ ==> ⦇·⦈))
           )
          → cif-arr Δ d τ1 τ2

  canonical-indeterminate-forms-arr : ∀{Δ d τ1 τ2 } →
                                       Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                                       d indet →
                                       cif-arr Δ d τ1 τ2
  canonical-indeterminate-forms-arr (TAVar x₁) ()
  canonical-indeterminate-forms-arr (TALam _ wt) ()
  canonical-indeterminate-forms-arr (TAAp wt wt₁) (IAp x ind x₁) = CIFAAp (_ , _ , _ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-arr (TAEHole x x₁) IEHole = CIFAEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-arr (TANEHole x wt x₁) (INEHole x₂) = CIFANEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-arr (TACast wt x) (ICastArr x₁ ind) = CIFACast (_ , _ , _ , _ , _ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-arr (TACast wt TCHole2) (ICastHoleGround x₁ ind GHole) = CIFACastHole (_ , refl , refl , refl , wt , ind , x₁)
  canonical-indeterminate-forms-arr (TAFailedCast x x₁ GHole x₃) (IFailedCast x₄ x₅ GHole x₇) = CIFAFailedCast (_ , _ , refl , refl , refl , x , x₅ , x₇)
  canonical-indeterminate-forms-arr (TAFst wt) (IFst ind h1 h2) = CIFAFst (_ , _ , refl , wt , ind , h1 , h2)
  canonical-indeterminate-forms-arr (TASnd wt) (ISnd ind h1 h2) = CIFASnd (_ , _ , refl , wt , ind , h1 , h2)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at hole type
  data cif-hole : (Δ : hctx) (d : iexp) → Set where
    CIFHEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⦈⟨ u , σ ⟩) ×
         ((u :: ⦇·⦈ [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-hole Δ d
    CIFHNEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: ⦇·⦈ [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-hole Δ d
    CIFHAp : ∀ {Δ d} →
      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2 ∈ typ ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: (τ2 ==> ⦇·⦈)) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
      → cif-hole Δ d
    CIFHFst : ∀{Δ d} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
       ((d == fst d') ×
        (Δ , ∅ ⊢ d' :: ⦇·⦈ ⊗ τ') ×
        (d' indet) ×
        (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
        (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
       )
      → cif-hole Δ d
    CIFHSnd : ∀{Δ d} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
       ((d == snd d') ×
        (Δ , ∅ ⊢ d' :: τ' ⊗ ⦇·⦈) ×
        (d' indet) ×
        (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
        (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
       )
      → cif-hole Δ d
    CIFHCast : ∀ {Δ d} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == d' ⟨ τ' ⇒ ⦇·⦈ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (d' indet)
        )
      → cif-hole Δ d

  canonical-indeterminate-forms-hole : ∀{Δ d} →
                                       Δ , ∅ ⊢ d :: ⦇·⦈ →
                                       d indet →
                                       cif-hole Δ d
  canonical-indeterminate-forms-hole (TAVar x₁) ()
  canonical-indeterminate-forms-hole (TAAp wt wt₁) (IAp x ind x₁) = CIFHAp (_ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-hole (TAEHole x x₁) IEHole = CIFHEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-hole (TANEHole x wt x₁) (INEHole x₂) = CIFHNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-hole (TACast wt x) (ICastGroundHole x₁ ind) = CIFHCast (_ , _ , refl , wt , x₁ , ind)
  canonical-indeterminate-forms-hole (TACast wt x) (ICastHoleGround x₁ ind ())
  canonical-indeterminate-forms-hole (TAFailedCast x x₁ () x₃) (IFailedCast x₄ x₅ x₆ x₇)
  canonical-indeterminate-forms-hole (TAFst wt) (IFst ind h1 h2) = CIFHFst (_ , _ , refl , wt , ind , h1 , h2)
  canonical-indeterminate-forms-hole (TASnd wt) (ISnd ind h1 h2) = CIFHSnd (_ , _ , refl , wt , ind , h1 , h2)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at product type
  data cif-prod : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
    CIFPEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⦈⟨ u , σ ⟩) ×
         ((u :: (τ1 ⊗ τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-prod Δ d τ1 τ2
    CIFPNEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: (τ1 ⊗ τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-prod Δ d τ1 τ2
    CIFPAp : ∀{d Δ τ1 τ2} →
      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2' ∈ typ ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ⊗ τ2)) ×
         (Δ , ∅ ⊢ d2 :: τ2') ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPFst : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: (τ1 ⊗ τ2) ⊗ τ') ×
         (d' indet) ×
         (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
         (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPSnd : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊗ (τ1 ⊗ τ2)) ×
         (d' indet) ×
         (∀{d1 d2} → d' ≠ ⟨ d1 , d2 ⟩) ×
         (∀{d'' τ1 τ2 τ3 τ4} → d' ≠ (d'' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPPair1 : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ]
        ((d == ⟨ d1 , d2 ⟩) ×
         (Δ , ∅ ⊢ d1 :: τ1) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         d1 indet ×
         d2 final
        )
        → cif-prod Δ d τ1 τ2
    CIFPPair2 : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ]
        ((d == ⟨ d1 , d2 ⟩) ×
         (Δ , ∅ ⊢ d1 :: τ1) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         d1 final ×
         d2 indet
        )
        → cif-prod Δ d τ1 τ2
    CIFPCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
        ((d == d' ⟨ (τ1' ⊗ τ2') ⇒ (τ1 ⊗ τ2) ⟩) ×
          (Δ , ∅ ⊢ d' :: τ1' ⊗ τ2') ×
          (d' indet) ×
          ((τ1' ⊗ τ2') ≠ (τ1 ⊗ τ2)) ×
          ((τ1' ⊗ τ2') ~ (τ1 ⊗ τ2))
        )
       → cif-prod Δ d τ1 τ2
    CIFPCastHole : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ iexp ]
        ((d == (d' ⟨ ⦇·⦈ ⇒ ⦇·⦈ ⊗ ⦇·⦈ ⟩)) ×
         (τ1 == ⦇·⦈) ×
         (τ2 == ⦇·⦈) ×
         (Δ , ∅ ⊢ d' :: ⦇·⦈) ×
         (d' indet) ×
         ((d'' : iexp) (τ' : typ) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPFailedCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
          ((d == (d' ⟨ τ' ⇒⦇⦈⇏ ⦇·⦈ ⊗ ⦇·⦈ ⟩) ) ×
           (τ1 == ⦇·⦈) ×
           (τ2 == ⦇·⦈) ×
           (Δ , ∅ ⊢ d' :: τ') ×
           (τ' ground) ×
           (τ' ≠ (⦇·⦈ ⊗ ⦇·⦈) ×
           d' final))
          → cif-prod Δ d τ1 τ2

  canonical-indeterminate-forms-prod : ∀{Δ d τ1 τ2 } →
                                       Δ , ∅ ⊢ d :: (τ1 ⊗ τ2) →
                                       d indet →
                                       cif-prod Δ d τ1 τ2
  canonical-indeterminate-forms-prod (TAVar x₁) ()
  canonical-indeterminate-forms-prod (TAAp wt wt₁) (IAp x ind x₁) = CIFPAp (_ , _ , _ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-prod (TAEHole x x₁) IEHole = CIFPEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-prod (TANEHole x wt x₁) (INEHole x₂) = CIFPNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-prod (TACast wt x) (ICastProd x₁ ind) = CIFPCast (_ , _ , _ , _ , _ , refl , wt , ind , x₁ , x)
  canonical-indeterminate-forms-prod (TACast wt TCHole2) (ICastHoleGround x₁ ind GProd) = CIFPCastHole (_ , refl , refl , refl , wt , ind , x₁)
  canonical-indeterminate-forms-prod (TAFailedCast wt x GProd x₂) (IFailedCast x₃ x₄ GProd x₆) = CIFPFailedCast (_ , _ , refl , refl , refl , wt , x₄ , x₆ , x₃)
  canonical-indeterminate-forms-prod (TAFst wt) (IFst ind h1 h2) = CIFPFst (_ , _ , refl , wt , ind , h1 , h2)
  canonical-indeterminate-forms-prod (TASnd wt) (ISnd ind h1 h2) = CIFPSnd (_ , _ , refl , wt , ind , h1 , h2)
  canonical-indeterminate-forms-prod (TAPair wt wt₁) (IPair1 ind x) = CIFPPair1 (_ , _ , refl , wt , wt₁ , ind , x)
  canonical-indeterminate-forms-prod (TAPair wt wt₁) (IPair2 x ind) = CIFPPair2 (_ , _ , refl , wt , wt₁ , x , ind)

  canonical-indeterminate-forms-coverage : ∀{Δ d τ} →
                                           Δ , ∅ ⊢ d :: τ →
                                           d indet →
                                           τ ≠ b →
                                           ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ==> τ2)) →
                                           τ ≠ ⦇·⦈ →
                                           ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ⊗ τ2)) →
                                           ⊥
  canonical-indeterminate-forms-coverage TAConst () nb na nh
  canonical-indeterminate-forms-coverage (TAVar x₁) () nb na nh
  canonical-indeterminate-forms-coverage (TALam _ wt) () nb na nh
  canonical-indeterminate-forms-coverage {τ = b} (TAAp wt wt₁) (IAp x ind x₁) nb na nh _ = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TAAp wt wt₁) (IAp x ind x₁) nb na nh _ = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAAp wt wt₁) (IAp x ind x₁) nb na nh _ = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TAEHole x x₁) IEHole nb na nh _ = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TAEHole x x₁) IEHole nb na nh _ = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAEHole x x₁) IEHole nb na nh _ = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TANEHole x wt x₁) (INEHole x₂) nb na nh _ = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TANEHole x wt x₁) (INEHole x₂) nb na nh _ = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TANEHole x wt x₁) (INEHole x₂) nb na nh _ = na τ τ₁ refl
  canonical-indeterminate-forms-coverage (TACast wt x) (ICastArr x₁ ind) nb na nh _ = na _ _ refl
  canonical-indeterminate-forms-coverage (TACast wt x) (ICastGroundHole x₁ ind) nb na nh _ = nh refl
  canonical-indeterminate-forms-coverage {τ = b} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh _ = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh _ = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh _ = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) z _ _ _ = z refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) _ _ z _ = z refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) _ z _ _ = z τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TAFst wt) (IFst ind x _) nb na nh np = nb refl
  canonical-indeterminate-forms-coverage {τ = b} (TASnd wt) (ISnd ind x _) nb na nh np = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TAFst wt) (IFst ind x _) nb na nh np = nh refl
  canonical-indeterminate-forms-coverage {τ = ⦇·⦈} (TASnd wt) (ISnd ind x _) nb na nh np = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAFst wt) (IFst ind x _) nb na nh np = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TASnd wt) (ISnd ind x _) nb na nh np = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TAAp wt wt₁) (IAp x ind x₁) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TAEHole x x₁) IEHole nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TANEHole x wt x₁) (INEHole x₂) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TACast wt x) (ICastProd x₁ ind) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TAFailedCast wt x x₁ x₂) (IFailedCast x₃ x₄ x₅ x₆) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TAFst wt) (IFst ind x _) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TASnd wt) (ISnd ind x _) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TAPair wt wt₁) (IPair1 ind x) nb na nh np = np τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊗ τ₁} (TAPair wt wt₁) (IPair2 x ind) nb na nh np = np τ τ₁ refl

ext: agda

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.ZCohomology.Properties where

open import Cubical.ZCohomology.Base
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Data.NatMinusTwo.Base
open import Cubical.Data.Empty
open import Cubical.Data.Sigma
open import Cubical.Data.Prod.Base
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Nullification
open import Cubical.Data.Int
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation

open import Cubical.HITs.Pushout
open import Cubical.Data.Sum.Base
open import Cubical.Data.HomotopyGroup
open import Cubical.Data.Bool
private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

{- Equivalence between cohomology of A and reduced cohomology of (A + 1) -}
coHomRed+1Equiv : (n : ℕ) →
                 (A : Set ℓ) →
                 (coHom n A) ≡ (coHomRed n ((A ⊎ Unit , inr (tt))))
coHomRed+1Equiv zero A i = ∥ helpLemma {C = (Int , pos 0)} i ∥₀
  module coHomRed+1 where
  helpLemma : {C : Pointed ℓ} → ( (A → (typ C)) ≡  ((((A ⊎ Unit) , inr (tt)) →* C)))
  helpLemma {C = C} = isoToPath (iso map1
                                     map2
                                     (λ b → linvPf b)
                                     (λ _  → refl))
    where
    map1 : (A → typ C) → ((((A ⊎ Unit) , inr (tt)) →* C))
    map1 f = map1' , refl module helpmap where
      map1' : A ⊎ Unit → fst C
      map1' (inl x) = f x
      map1' (inr x) = pt C

    map2 : ((((A ⊎ Unit) , inr (tt)) →* C)) → (A → typ C)
    map2 (g , pf) x = g (inl x)

    linvPf : (b :((((A ⊎ Unit) , inr (tt)) →* C))) →  map1 (map2 b) ≡ b
    linvPf (f , snd) i = (λ x → helper x i)  , λ j → snd ((~ i) ∨ j)
      where
      helper : (x : A ⊎ Unit) → ((helpmap.map1') (map2 (f , snd)) x) ≡ f x
      helper (inl x) = refl
      helper (inr tt) = sym snd

coHomRed+1Equiv (suc n) A i = ∥ coHomRed+1.helpLemma A i {C = ((coHomK (suc n)) , ∣ north ∣)} i ∥₀

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------
-- Examples
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing.Examples where

open import Data.List
open import Data.Vec using ([]; _∷_)
open import Data.Nat
open import Data.Bool
open import Data.Char using (Char)
import Data.Char.Properties as C
import Data.String as S
open S using (String)
open import Codata.Musical.Notation
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import StructurallyRecursiveDescentParsing.Index
open import StructurallyRecursiveDescentParsing.Grammar
open import StructurallyRecursiveDescentParsing.DepthFirst
open import StructurallyRecursiveDescentParsing.Lib
open Token C.decSetoid

-- Some functions used to simplify the examples a little.

infix 5 _∈?_/_ _∈?_

_∈?_/_ : ∀ {NT i R} →
         String → Parser NT Char i R → Grammar NT Char → List R
s ∈? p / g = parseComplete (⟦ p ⟧ g) (S.toList s)

_∈?_ : ∀ {i R} → String → Parser EmptyNT Char i R → List R
s ∈? p = s ∈? p / emptyGrammar

module Ex₁ where

  mutual

    -- e ∷= 0 + e | 0

    data Nonterminal : NonTerminalType where
      e : Nonterminal i Char

    private
      i = _

    grammar : Grammar Nonterminal Char
    grammar e = tok '0' ⊛> tok '+' ⊛> ! e
              ∣ tok '0'

  ex₁ : "0+0" ∈? ! e / grammar ≡ [ '0' ]
  ex₁ = P.refl

module Ex₂ where

  mutual

    -- e ∷= f + e | f
    -- f ∷= 0 | 0 * f | ( e )

    data Nonterminal : NonTerminalType where
      expr   : Nonterminal i₁ Char
      factor : Nonterminal i₂ Char

    private
      i₁ = _
      i₂ = _

    grammar : Grammar Nonterminal Char
    grammar expr   = ! factor ⊛> tok '+' ⊛> ! expr
                   ∣ ! factor
    grammar factor = tok '0'
                   ∣ tok '0' ⊛> tok '*' ⊛> ! factor
                   ∣ tok '(' ⊛> ! expr <⊛ tok ')'

  ex₁ : "(0*)" ∈? ! expr / grammar ≡ []
  ex₁ = P.refl

  ex₂ : "0*(0+0)" ∈? ! expr / grammar ≡ [ '0' ]
  ex₂ = P.refl

{-
module Ex₃ where

  mutual

    -- This is not allowed:

    -- e ∷= f + e | f
    -- f ∷= 0 | f * 0 | ( e )

    data Nonterminal : NonTerminalType where
      expr   : Nonterminal i₁ Char
      factor : Nonterminal i₂ Char

    private
      i₁ = _
      i₂ = _

  grammar : Grammar Nonterminal Char
  grammar expr   = ! factor ⊛> tok '+' ⊛> ! expr
                 ∣ ! factor
  grammar factor = tok '0'
                 ∣ ! factor ⊛> tok '*' ⊛> tok '0'
                 ∣ tok '(' ⊛> ! expr <⊛ tok ')'
-}

module Ex₄ where

  mutual

    -- The language aⁿbⁿcⁿ, which is not context free.

    -- The non-terminal top returns the number of 'a' characters
    -- parsed.

    data NT : NonTerminalType where
      top :            NT i₁ ℕ  -- top     ∷= aⁿbⁿcⁿ
      as  :        ℕ → NT i₂ ℕ  -- as n    ∷= aˡ⁺¹bⁿ⁺ˡ⁺¹cⁿ⁺ˡ⁺¹
      bcs : Char → ℕ → NT i₃ ℕ  -- bcs x n ∷= xⁿ⁺¹

    private
      i₁ = _
      i₂ = _
      i₃ = _

    grammar : Grammar NT Char
    grammar top             = return 0 ∣ ! (as zero)
    grammar (as n)          = suc <$ tok 'a' ⊛
                              ( ! (as (suc n))
                              ∣ _+_ <$> ! (bcs 'b' n) ⊛ ! (bcs 'c' n)
                              )
    grammar (bcs c zero)    = tok c ⊛> return 0
    grammar (bcs c (suc n)) = tok c ⊛> ! (bcs c n)

  ex₁ : "aaabbbccc" ∈? ! top / grammar ≡ [ 3 ]
  ex₁ = P.refl

  ex₂ : "aaabbccc" ∈? ! top / grammar ≡ []
  ex₂ = P.refl

module Ex₄′ where

  mutual

    -- A monadic variant of Ex₄.

    aⁿbⁿcⁿ = return 0
           ∣ tok 'a' +            !>>= λ as → ♯
             (let n = length as in
              exactly n (tok 'b') ⊛>
              exactly n (tok 'c') ⊛>
              return n)

    ex₁ : "aaabbbccc" ∈? aⁿbⁿcⁿ ≡ [ 3 ]
    ex₁ = P.refl

  ex₂ : "aaabbccc" ∈? aⁿbⁿcⁿ ≡ []
  ex₂ = P.refl

module Ex₅ where

  mutual

    -- A grammar making use of a parameterised parser from the
    -- library.

    data NT : NonTerminalType where
      a  : NT i₁ Char
      as : NT i₂ ℕ

    private
      i₁ = _
      i₂ = _

    grammar : Grammar NT Char
    grammar a  = tok 'a'
    grammar as = length <$> ! a ⋆

  ex₁ : "aaaaa" ∈? ! as / grammar ≡ [ 5 ]
  ex₁ = P.refl

module Ex₆ where

  mutual

    -- A grammar which uses the chain≥ combinator.

    data NT : NonTerminalType where
      op   : NT i₁ (ℕ → ℕ → ℕ)
      expr : (a : Assoc) → NT i₂ ℕ

    private
      i₁ = _
      i₂ = _

    grammar : Grammar NT Char
    grammar op       = _+_ <$ tok '+'
                     ∣ _*_ <$ tok '*'
                     ∣ _∸_ <$ tok '∸'
    grammar (expr a) = chain≥ 0 a number (! op)

  ex₁ : "12345" ∈? number / grammar ≡ [ 12345 ]
  ex₁ = P.refl

  ex₂ : "1+5*2∸3" ∈? ! (expr left) / grammar ≡ [ 9 ]
  ex₂ = P.refl

  ex₃ : "1+5*2∸3" ∈? ! (expr right) / grammar ≡ [ 1 ]
  ex₃ = P.refl

module Ex₇ where

  mutual

    -- A proper expression example.

    data NT : NonTerminalType where
      expr   : NT i₁ ℕ
      term   : NT i₂ ℕ
      factor : NT i₃ ℕ
      addOp  : NT i₄ (ℕ → ℕ → ℕ)
      mulOp  : NT i₅ (ℕ → ℕ → ℕ)

    private
      i₁ = _
      i₂ = _
      i₃ = _
      i₄ = _
      i₅ = _

    grammar : Grammar NT Char
    grammar expr   = chain≥ 0 left (! term)   (! addOp)
    grammar term   = chain≥ 0 left (! factor) (! mulOp)
    grammar factor = tok '(' ⊛> ! expr <⊛ tok ')'
                   ∣ number
    grammar addOp  = _+_ <$ tok '+'
                   ∣ _∸_ <$ tok '∸'
    grammar mulOp  = _*_ <$ tok '*'

  ex₁ : "1+5*2∸3" ∈? ! expr / grammar ≡ [ 8 ]
  ex₁ = P.refl

  ex₂ : "1+5*(2∸3)" ∈? ! expr / grammar ≡ [ 1 ]
  ex₂ = P.refl

module Ex₈ where

  mutual

    -- An example illustrating the use of one grammar within another.

    data NT : NonTerminalType where
      lib   : ∀ {i R} (nt : Ex₇.NT i R) → NT i R
      exprs : NT i (List ℕ)

    private
      i = _

    expr = lib Ex₇.expr

    grammar : Grammar NT Char
    grammar (lib nt) = mapNT lib (Ex₇.grammar nt)
    grammar exprs    = ! expr sepBy tok ','

  ex₁ : "1,2∸1" ∈? ! exprs / grammar ≡ [ 1 ∷ 1 ∷ [] ]
  ex₁ = P.refl

module Ex₉ where

  mutual

    -- An example illustrating the use of one grammar within another
    -- when the inner grammar contains non-terminals parameterised on
    -- parsers, and the outer grammar instantiates one of these
    -- parsers with an outer non-terminal.

    infix 55 _★ _∔

    data LibraryNT (NT : NonTerminalType) (Tok : Set) :
                   NonTerminalType where
      _★ : ∀ {c R} → Parser NT Tok (false ◇ c) R →
           LibraryNT NT Tok (i₁ c) (List R)
      _∔ : ∀ {c R} → Parser NT Tok (false ◇ c) R →
           LibraryNT NT Tok (i₂ c) (List R)

    private
      i₁ i₂ : _ → _
      i₁ = _
      i₂ = _

    library : ∀ {NT Tok} → (∀ {i R} → LibraryNT NT Tok i R → NT i R) →
              ∀ {i R} → LibraryNT NT Tok i R → Parser NT Tok i R
    library lift (p ★) = return [] ∣ ! (lift (p ∔))
    library lift (p ∔) = p              >>= λ x  →
                         ! (lift (p ★)) >>= λ xs →
                         return (x ∷ xs)

  mutual

    data NT : NonTerminalType where
      lib : ∀ {i R} → LibraryNT NT Char i R → NT i R
      a   : NT i₃ Char
      as  : NT i₄ (List Char)

    private
      i₃ = _
      i₄ = _

    grammar : Grammar NT Char
    grammar (lib nt) = library lib nt
    grammar a        = tok 'a'
    grammar as       = ! (lib (! a ★))

  ex₁ : "aa" ∈? ! as / grammar ≡ [ 'a' ∷ 'a' ∷ [] ]
  ex₁ = P.refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Issue261 where

postulate
  List : Set → Set
  nil : ∀ A → List A
  Nat : Set

works-now : List Nat
works-now with nil _
... | xs = xs

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module _ where

module A where

  data D : Set where
    !_ : D

module B where

  data D : Set where
    !_ : D

open A

test : B.D
test = !_


text:
------------------------------------------------------------------------
-- An alternative definition of the partiality monad: a variant of the
-- delay monad quotiented by a notion of weak bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

module Partiality-monad.Coinductive.Alternative where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (⊥↔⊥)
open import H-level equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
open import Quotient equality-with-paths

import Delay-monad.Alternative as A
import Delay-monad.Alternative.Equivalence as A
import Delay-monad.Alternative.Weak-bisimilarity as A
import Delay-monad.Bisimilarity as B
import Partiality-monad.Coinductive as C

-- The partiality monad, defined as the alternative definition of the
-- delay monad quotiented by weak bisimilarity.

_⊥ : ∀ {a} → Type a → Type a
A ⊥ = A.Delay A / A._≈_

-- The partiality monad is a set.

⊥-is-set : ∀ {a} {A : Type a} → Is-set (A ⊥)
⊥-is-set = /-is-set

-- This definition of the partiality monad is isomorphic to the one in
-- Partiality-monad.Coinductive, for sets, assuming extensionality.

⊥↔⊥ : ∀ {a} {A : Type a} →
      Is-set A →
      B.Extensionality a →
      A ⊥ ↔ A C.⊥
⊥↔⊥ {A = A} A-set delay-ext = D↔D /-cong lemma
  where
  D↔D = A.Delay↔Delay delay-ext

  lemma : (x y : A.Delay A) →
          x A.≈ y ⇔ ∥ _↔_.to D↔D x B.≈ _↔_.to D↔D y ∥
  lemma x y =
    x A.≈ y                            ↔⟨ inverse $ ∥∥↔ (A.≈-propositional x y) ⟩
    ∥ x A.≈ y ∥                        ↝⟨ ∥∥-cong-⇔ (A.≈⇔≈ A-set x y) ⟩□
    ∥ _↔_.to D↔D x B.≈ _↔_.to D↔D y ∥  □

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.

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

module Relation.Binary.Indexed.Heterogeneous.Definitions where

open import Level
import Relation.Binary.Core as B
import Relation.Binary.Definitions as B
import Relation.Binary.PropositionalEquality.Core as P
open import Relation.Binary.Indexed.Heterogeneous.Core

private
  variable
    i a ℓ : Level
    I : Set i

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

Reflexive : (A : I → Set a) → IRel A ℓ → Set _
Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})

Symmetric : (A : I → Set a) → IRel A ℓ → Set _
Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_

Transitive : (A : I → Set a) → IRel A ℓ → Set _
Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Data.Dyck.Empty where

open import Prelude
open import Data.Nat using (_+_)
open import Data.Vec.Iterated using (Vec; _∷_; []; foldlN; head)

private
  variable
    n : ℕ

--------------------------------------------------------------------------------
-- Binary trees: definition and associated functions
--------------------------------------------------------------------------------

data Tree (A : Type a) : Type a where
  ◇ : Tree A
  [_] : A → Tree A
  _*_ : Tree A → Tree A → Tree A

--------------------------------------------------------------------------------
-- Programs: definition and associated functions
--------------------------------------------------------------------------------

data Prog (A : Type a) : ℕ → Type a where
  halt : Prog A 1
  push : A → Prog A (1 + n) → Prog A n
  pull : Prog A (1 + n) → Prog A (2 + n)
  skip : Prog A (1 + n) → Prog A n

--------------------------------------------------------------------------------
-- Conversion from a Prog to a Tree
--------------------------------------------------------------------------------

prog→tree⊙ : Prog A n → Vec (Tree A) n → Tree A
prog→tree⊙ halt        (v ∷ [])       = v
prog→tree⊙ (push v is) st             = prog→tree⊙ is ([ v ] ∷ st)
prog→tree⊙ (pull   is) (t₁ ∷ t₂ ∷ st) = prog→tree⊙ is (t₂ * t₁ ∷ st)
prog→tree⊙ (skip   is) st             = prog→tree⊙ is (◇ ∷ st)

prog→tree : Prog A zero → Tree A
prog→tree ds = prog→tree⊙ ds []

--------------------------------------------------------------------------------
-- Conversion from a Tree to a Prog
--------------------------------------------------------------------------------

tree→prog⊙ : Tree A → Prog A (suc n) → Prog A n
tree→prog⊙ [ x ]     = push x
tree→prog⊙ (xs * ys) = tree→prog⊙ xs ∘ tree→prog⊙ ys ∘ pull
tree→prog⊙ ◇         = skip

tree→prog : Tree A → Prog A zero
tree→prog tr = tree→prog⊙ tr halt

--------------------------------------------------------------------------------
-- Proof of isomorphism
--------------------------------------------------------------------------------

tree→prog→tree⊙ :  {is : Prog A (1 + n)} {st : Vec (Tree A) n} (e : Tree A) →
  prog→tree⊙ (tree→prog⊙ e is) st ≡ prog→tree⊙ is (e ∷ st)
tree→prog→tree⊙ [ x ]     = refl
tree→prog→tree⊙ (xs * ys) = tree→prog→tree⊙ xs ; tree→prog→tree⊙ ys
tree→prog→tree⊙ ◇         = refl

prog→tree→prog⊙ :  {st : Vec (Tree A) n} (is : Prog A n) →
 tree→prog (prog→tree⊙ is st) ≡ foldlN (Prog A) tree→prog⊙ is st
prog→tree→prog⊙  halt       = refl
prog→tree→prog⊙ (push i is) = prog→tree→prog⊙ is
prog→tree→prog⊙ (pull   is) = prog→tree→prog⊙ is
prog→tree→prog⊙ (skip   is) = prog→tree→prog⊙ is

prog-iso : Prog A zero ⇔ Tree A
prog-iso .fun = prog→tree
prog-iso .inv = tree→prog
prog-iso .rightInv = tree→prog→tree⊙
prog-iso .leftInv  = prog→tree→prog⊙

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-

Holey congruence where there is a 'general' `cong` function available, as in one
that works for any given function.

-}

open import Holes.Prelude

-- NOTE: Why can't we accept the actual functions as arguments instead of quoted
-- versions? Because macros don't play nicely with modules.
module Holes.Cong.General
  (quote-cong : Name)
  (quote-sym : Name)
  where

open Holes.Prelude public using (quote-term)

import Holes.Term as HTerm

-- NOTE: This doesn't work! The place that uses the macros has to import
-- Holes.Term using (⌞_⌟) manually.
-- open HTerm using (⌞_⌟) public

open HTerm

private
  -- If the given term is one that has arguments, returns them.

  getArgs : Term → Maybe (List (Arg Term))
  getArgs (var x args) = just args
  getArgs (con c args) = just args
  getArgs (def f args) = just args
  getArgs (pat-lam cs args) = just args
  getArgs _ = nothing

  -- In a list of arguments, returns the relevant ones for a binary relation.

  ≈relevantArgs : List (Arg Term) → Maybe (Term × Term)
  ≈relevantArgs (_ ∷ _ ∷ arg _ x ∷ arg _ y ∷ []) = just (x , y)
  ≈relevantArgs _ = nothing

-- Given a type of the form `x ≡ y`, returns the pair `x , y`.

  decompose≈ : Term → Maybe (Term × Term)
  decompose≈ = getArgs >=> ≈relevantArgs

  applyCong : Term → Term → Term
  applyCong lambda inner-equality =
    def quote-cong
        ( basicArg lambda           -- f : A → B
        ∷ basicArg inner-equality   -- x ≈ y
        ∷ [])

  applySym : Term → Term
  applySym equality =
    def quote-sym
        ( basicArg equality    -- i ≈ j
        ∷ [])

  autoCongWithType : Term → Type → TC Term
  autoCongWithType equalityTerm targetType =
    -- Try to decompose the goal type, which should be of the form `x ≈ y`, into
    -- `x` and `y`. Throw a type error if this is not possible.
    liftMaybe ( strErr "Term is not of the form x ≈ y:"
              ∷ termErr targetType
              ∷ []) (decompose≈ targetType) >>=² λ goalLhs _ →
    -- Try to extract the holes in the LHS. Throw a type error if this is not
    -- possible.
    checkedTermToHoley′ (printHoleyErr goalLhs) goalLhs >>=² λ _ lhsHoley →
    -- Construct a lambda expression into the holes in the LHS.
    return (holeyToLam lhsHoley) >>= λ lhsLam →
    -- Apply the `cong` function with our newly constructed lambda and the
    -- provided equality term. Most implicit arguments are left unknown, and
    -- then inferred by Agda when we call `checkType`.
    return (applyCong lhsLam equalityTerm) >>= λ congTerm →
    -- Try to check the type of the cong term. If it doesn't work, try it
    -- symmetrically. If that doesn't work, try the first again so that the user
    -- gets a nicer error message.
    checkType congTerm targetType
      ⟨ catchTC ⟩
    checkType (applySym congTerm) targetType
      ⟨ catchTC ⟩
    checkType congTerm targetType
    -- `checkType` hopefully returns to us the `cong` call with filled implicit
    -- arguments. Assuming the user's logic is correct, this is what we need to
    -- prove the goal.

  cong!′ : Term → Term → TC ⊤
  cong!′ equalityTerm target =
    inferType target >>=
    autoCongWithType equalityTerm >>=
    unify target

macro
  cong! : Term → Term → TC ⊤
  cong! = cong!′


text:
open import FRP.JS.Nat using ( ℕ ) renaming ( _<_ to _<N_ ; _≤_ to _≤N_ )
open import FRP.JS.Bool using ( Bool ; true ; false ; not )

module FRP.JS.Char where

infix 4 _≟_ _≠_ _<_ _≤_

open import FRP.JS.Primitive public using ( Char )

private
 primitive
  primCharToNat    : Char → ℕ
  primCharEquality : Char → Char → Bool

toNat : Char → ℕ
toNat = primCharToNat

{-# COMPILED_JS toNat function(c) { return c.charCodeAt(0); } #-}

_≟_ : Char → Char → Bool
_≟_ = primCharEquality

{-# COMPILED_JS _≟_ function(c) { return function(d) { return c === d; }; } #-}

_≠_ : Char → Char → Bool
c ≠ d = not (c ≟ d)

{-# COMPILED_JS _≠_ function(c) { return function(d) { return c !== d; }; } #-}

_<_ : Char → Char → Bool
c < d = toNat c <N toNat d

{-# COMPILED_JS _<_ function(c) { return function(d) { return c < d; }; } #-}

_≤_ : Char → Char → Bool
c ≤ d = toNat c ≤N toNat d

{-# COMPILED_JS _≤_ function(c) { return function(d) { return c <= d; }; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Groupoid where

open import Level using (Level; suc; _⊔_)

open import Categories.Category using (Category)
import Categories.Morphism

record IsGroupoid {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C public

  open Categories.Morphism C

  infix 10 _⁻¹

  field
    _⁻¹ : ∀ {A B} → A ⇒ B → B ⇒ A
    iso : ∀ {A B} {f : A ⇒ B} → Iso f (f ⁻¹)

  module iso {A B f} = Iso (iso {A} {B} {f})

  equiv-obj : ∀ {A B} → A ⇒ B → A ≅ B
  equiv-obj f = record
    { from = f
    ; to   = _
    ; iso  = iso
    }

  -- this definition doesn't seem to 'carry its weight'
  equiv-obj-sym : ∀ {A B} → A ⇒ B → B ≅ A
  equiv-obj-sym f = ≅.sym (equiv-obj f)

-- A groupoid is a category that has a groupoid structure

record Groupoid (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    category   : Category o ℓ e
    isGroupoid : IsGroupoid category

  open IsGroupoid isGroupoid public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module plfa.part1.Midterm where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
-- you can add any import definitions that you need
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; _>_; z≤n; s≤s; _≤?_)
open import Data.Nat.Properties using (+-assoc; +-suc; *-suc; +-comm; *-distribˡ-+; *-identityʳ)
open import Relation.Nullary using (yes; no)
open import plfa.part1.Induction using (*-distrib-+; *-zero)
-- used for rewrite
simplify : ∀ {A : Set} (x : A) → x ≡ x
simplify x = refl

sum : ℕ → ℕ
sum 0 = 0
sum n@(suc sn) = sum sn + n

-- Problem 1
-- remove the "postulate" and prove this theorem, which is a version of
--   sum n ≡ n * (n + 1) / 2
---postulate
simple : ∀ (n : ℕ) → (sum n) * 2 ≡ (suc n) * n
simple zero = refl
simple (suc n) rewrite *-distrib-+ (sum n) (suc n) 2
                | simple n
                | simplify  n
                | *-suc n n
                | +-comm n (n * n)
                | sym (+-assoc n (n * n) n)
                | +-comm n (n * n) | +-assoc (n * n) n n
                | sym (+-suc (n * n)  (n + n)) | sym (+-assoc n (n * n) (suc (n + n)))
                | +-comm n (n * n)
                | sym (+-suc (n * n) n)
                | +-assoc (n * n) n (suc (n + n))
                | sym (+-suc (n * n) (n + suc (n + n)))
                | sym (+-suc n (suc (n + n)))
                | sym (+-assoc (n * n) n (suc (suc (n + n))))
                | *-suc n 1
                | *-identityʳ n = refl

-- Problem 2
-- remove the postulate and implement this function, which gives an Natural
-- number approximation of square root
postulate
  sqrt : ℕ → ℕ

-- you can run these test cases
-- _ : sqrt 0 ≡ 0
-- _ = refl
-- _ : sqrt 1 ≡ 1
-- _ = refl
-- _ : sqrt 2 ≡ 1
-- _ = refl
-- _ : sqrt 3 ≡ 1
-- _ = refl
-- _ : sqrt 4 ≡ 2
-- _ = refl
-- _ : sqrt 5 ≡ 2
-- _ = refl
-- _ : sqrt 6 ≡ 2
-- _ = refl
-- _ : sqrt 7 ≡ 2
-- _ = refl
-- _ : sqrt 8 ≡ 2
-- _ = refl
-- _ : sqrt 9 ≡ 3
-- _ = refl
-- _ : sqrt 10 ≡ 3
-- _ = refl
-- _ : sqrt 11 ≡ 3
-- _ = refl
-- _ : sqrt 12 ≡ 3
-- _ = refl
-- _ : sqrt 13 ≡ 3
-- _ = refl
-- _ : sqrt 14 ≡ 3
-- _ = refl
-- _ : sqrt 15 ≡ 3
-- _ = refl
-- _ : sqrt 16 ≡ 4
-- _ = refl
-- _ : sqrt 17 ≡ 4
-- _ = refl
-- _ : sqrt 18 ≡ 4
-- _ = refl
-- _ : sqrt 19 ≡ 4
-- _ = refl
-- _ : sqrt 20 ≡ 4
-- _ = refl
-- _ : sqrt 21 ≡ 4
-- _ = refl
-- _ : sqrt 22 ≡ 4
-- _ = refl
-- _ : sqrt 23 ≡ 4
-- _ = refl
-- _ : sqrt 24 ≡ 4
-- _ = refl
-- _ : sqrt 24 ≡ 4
-- _ = refl
-- _ : sqrt 24 ≡ 4
-- _ = refl
-- _ : sqrt 25 ≡ 5
-- _ = refl
-- _ : sqrt 26 ≡ 5
-- _ = refl
-- _ : sqrt 27 ≡ 5
-- _ = refl


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

open import Data.Nat        using (ℕ; zero; suc; _+_; _*_; _≤_ ; _>_; _<_; _≥_; z≤n; s≤s)
open import Data.Sum        using (_⊎_; inj₁; inj₂)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

module Nat where

-- Useful functions for natural numbers

_-_ : (n m : ℕ) → {m ≤ n} → ℕ
(n     - zero)  {z≤n}   = n
(suc n - suc m) {s≤s p} = _-_ n m {p}

_-_⟨_⟩ : (n m : ℕ) → (m ≤ n) → ℕ
_-_⟨_⟩ n m m≤n = _-_ n m {m≤n}

m+n-m=n : (m n : ℕ) → {m≤n : m ≤ n} → m + (n - m ⟨ m≤n ⟩) ≡ n
m+n-m=n zero    n       {z≤n}     = refl
m+n-m=n (suc m) (suc n) {s≤s m≤n} = cong suc (m+n-m=n m n {m≤n})

<-∨-≥ : (m n : ℕ) → m < n ⊎ m ≥ n
<-∨-≥ zero    zero    = inj₂ z≤n
<-∨-≥ zero    (suc n) = inj₁ (s≤s z≤n)
<-∨-≥ (suc m) zero    = inj₂ z≤n
<-∨-≥ (suc m) (suc n) with <-∨-≥ m n
... | inj₁ m<n = inj₁ (s≤s m<n)
... | inj₂ m≥n = inj₂ (s≤s m≥n)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS  --sized-types --show-implicit #-}

module SizedTypesScopeViolationInMeta where

open import Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

-- exposing a bug in size constraint solving

-- *** Exception: Inconsistent meta: _73 [[CtxId 420],[CtxId 418]]
A : Set1
A = (Id : {i : Size} -> Nat {_} -> Set)
    (k : Size)(m : Nat {↑ k}) -> Id {k} m
    ->
    (j : Size)(n : Nat {j}) -> Id {j} n

{-
mutual

--   id : {i : Size} -> Nat {_} -> Nat {i}  -- FAILS
  id : {i : Size} -> Nat {i} -> Nat {i}
  id x = x

  succ : {i : Size} -> Nat {i} -> Nat {↑ i}
  succ x = suc (id x)
-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module sv20.assign1.First where

{- Code partially taken from the book "Programming Language Foundations in
 - Agda" by Philip Wadler, Wen Kokke, Jeremy Siek and many others. The book
 - can be found at https://plfa.github.io/
 -
 - Based on chapter 1 - Natural numbers - https://plfa.github.io/Naturals/
 -
 - The solution for the homework can be found from line 161
 -}

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

-- Gives us the power of writing `3` to mean `suc (suc (suc zero))` :)
{-# BUILTIN NATURAL ℕ #-}

import Relation.Binary.PropositionalEquality as Eq
open import Function.Base using (flip)
open Eq using (_≡_; _≢_; refl; cong; sym; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

_+_ : ℕ → ℕ → ℕ
zero + n = n                -- +-def₀
(suc m) + n = suc (m + n)   -- +-def₁

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

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

-- Monus
_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

infixl 6  _+_  _∸_
infixl 7  _*_
infixr 8  _^_

assoc-+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
assoc-+ zero n p = refl
assoc-+ (suc m) n p rewrite assoc-+ m n p = refl

comm-+₀ : ∀ (m : ℕ) → m + zero ≡ m
comm-+₀ zero = refl
-- Proofs on natural numbers can be written in a manner that ressembles a pen
-- and paper proof. For example:
comm-+₀ (suc n) =
  begin
    suc n + zero
  ≡⟨⟩ -- By addition definition
    suc (n + zero)
  ≡⟨ cong suc (comm-+₀ n) ⟩
    suc n
  ∎
-- But often, proofs are written for Agda to check them and not to humans to
-- read them. The above proof can be written succintly as:
--comm-+₀ (suc n) rewrite comm-+₀ n = refl

succ_right : ∀ (n m : ℕ) → suc (n + m) ≡ n + suc m
succ_right zero m = refl
succ_right (suc n) m rewrite succ_right n m = refl
--succ_right (suc n) m = cong suc (succ_right n m)
--succ_right (suc n) m =
--  begin
--    suc (suc n + m)
--  ≡⟨⟩
--    suc (suc (n + m))
--  ≡⟨ cong suc (succ_right n m) ⟩
--    suc (n + suc m)
--  ≡⟨⟩
--    suc n + suc m
--  ∎

comm-+ : ∀ (n m : ℕ) → n + m ≡ m + n
comm-+ zero n = sym (comm-+₀ n)
comm-+ (suc n) m rewrite comm-+ n m | succ_right m n = refl
--comm-+ (suc n) m = trans (cong suc (comm-+ n m)) (succ_right m n)
--comm-+ (suc n) m =
--  begin
--    suc n + m
--  ≡⟨⟩ -- +-def₁
--    suc (n + m)
--  ≡⟨ cong suc (comm-+ n m) ⟩
--    suc (m + n)
--  ≡⟨ succ_right m n ⟩
--    m + suc n
--  ∎

swap-m-n-+ : ∀ (m n p) → m + (n + p) ≡ n + (m + p)
swap-m-n-+ m n p rewrite
    sym (assoc-+ m n p)
  | sym (assoc-+ n m p)
  | comm-+ m n
  = refl

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

suc-right-* : ∀ (m n) → m * suc n ≡ m + m * n
suc-right-* zero n = refl
suc-right-* (suc m) n
  rewrite
    suc-right-* m n
  | sym (assoc-+ n m (m * n))
  | comm-+ n m
  | assoc-+ m n (m * n)
  = refl

comm-* : ∀ (m n : ℕ) → m * n ≡ n * m
comm-* zero n rewrite right-zero-* n = refl
comm-* (suc m) n
  rewrite
    comm-* m n
  | suc-right-* n m
  = refl

distr-*-+ : ∀ (m n p) → (m + n) * p ≡ m * p + n * p
distr-*-+ zero _ _ = refl
distr-*-+ (suc m) n p
  rewrite
    distr-*-+ m n p
  | assoc-+ p (m * p) (n * p)
  = refl

distl-*-+ : ∀ (p m n) → p * (m + n) ≡ p * m + p * n
distl-*-+ zero _ _ = refl
distl-*-+ (suc p) m n
  rewrite
    distl-*-+ p m n
  | sym (assoc-+ (m + n) (p * m) (p * n))
  | sym (assoc-+ (m + p * m) n (p * n))
  | assoc-+ m n (p * m)
  | comm-+ n (p * m)
  | assoc-+ m (p * m) n
  = refl

assoc-* : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
assoc-* zero n p = refl
assoc-* (suc m) n p
  rewrite
    assoc-* m n p
  | distr-*-+ n (m * n) p
  | assoc-* m n p
  = refl

swap-m-n-* : ∀ (m n p) → m * (n * p) ≡ n * (m * p)
swap-m-n-* m n p rewrite
    sym (assoc-* m n p)
  | sym (assoc-* n m p)
  | comm-* m n
  = refl

------------------------------------------------------------------------------------------
--                                   HOMEWORK SOLUTION                                  --
------------------------------------------------------------------------------------------

-- We want to proof that:
distr-^-* : ∀ (m n p) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)

-- We will prove the `distr-^-*` by induction. To prove something by induction
-- in Agda, we use recursion.

-- The first basic case is when `p = 0`
distr-^-* m n zero =
  begin
    (m * n) ^ zero
  ≡⟨⟩ -- The builtin option "NATURAL" allows us to write `0` instead of `zero`
    (m * n) ^ 0
  ≡⟨⟩ -- because:   n ^ zero  =  suc zero
    suc 0
  ≡⟨⟩ -- because:   zero + n = n
    suc (0 + 0)
  ≡⟨⟩ -- because:   (suc m) + n = suc (m + n)
    suc 0 + 0
  ≡⟨⟩ -- Agda builtin option "NATURAL" allows us to write `1` instead of `suc 0`
    1 + 0
  ≡⟨⟩ -- because:   zero    * n  =  zero
    1 + 0 * 1
  ≡⟨⟩ -- because:   (suc m) * n  =  n + (m * n)
    suc 0 * 1
  ≡⟨⟩ -- `1` instead of `suc 0`
    1 * 1
  ≡⟨⟩ -- because:   n ^ zero  =  suc zero
    1 * (n ^ 0)
  ≡⟨⟩ -- because:   n ^ zero  =  suc zero
    (m ^ 0) * (n ^ 0)
  ∎

-- Agda computes every expression it is given until it can't apply any more
-- rules, i.e, Agda reduces every expression to its normal form.
-- For example, if we give Agda the expression `2 + 1`, it will apply the
-- rule `(suc m) + n = suc (m + n)` until it arrives to
-- `suc (suc (suc zero))`, `3`.
--
-- Notice that every line in the previous proof reduces to `1`. This means
-- that Agda read the previous proof as:
--
--distr-^-* m n zero =
--  begin
--    1
--  ≡⟨⟩
--    1
--  ≡⟨⟩ -- ...
--    1
--  ≡⟨⟩
--    1
--  ∎
--
-- So we could have written a shorter proof saying that `1 ≡⟨⟩ 1 ∎` and it
-- would sufficient for Agda to approve our proof.
--
--distr-^-* _ _ zero = 1 ≡⟨⟩ 1 ∎
--
-- In fact, `1 ≡⟨⟩ 1 ∎` can be written as `refl` in Agda.
--
--distr-^-* _ _ zero = refl

-- The following two base cases can be easily proven with the same technique as
-- the previous proof:
distr-^-* zero _ (suc p) = refl

-- For the last base case, we need a little more human involvement because the
-- expressions do not reduce completly to a common normal form.
distr-^-* (suc m) zero (suc p) =
  begin
    (suc m * 0) ^ suc p
  ≡⟨⟩ -- Agda reduces the expression to
    m * 0 * (m * 0) ^ p
  -- Applying `right-zero-*` (`n * 0 ≡ 0`) lemma to the left side
  ≡⟨ cong (_* (m * 0) ^ p) (right-zero-* m) ⟩
    0 * (m * 0) ^ p
  ≡⟨⟩ -- reduces to
    0
  -- Applying `sym ∘ right-zero-*` (`0 ≡ n * 0`) lemma to the left side
  ≡⟨ sym (right-zero-* (suc m ^ suc p)) ⟩
    (suc m ^ suc p) * 0
  ≡⟨⟩ -- reduces to
    (suc m ^ p + m * suc m ^ p) * 0
  ≡⟨⟩ -- reduced from our goal
    (suc m ^ suc p) * (0 ^ suc p)
  ∎
--
-- Notice how the previous proof required us to tell Agda which "lemmas" to use
-- to be able to link the left side of the proof with the right side.
--
-- As before, we have more ways to write the previous proof. We can forgo all
-- the intermediate steps and tell Agda which lemmas the proof needs.
--
--distr-^-* (suc m) 0 (suc p) =
--  trans
--    (cong (_* (m * 0) ^ p) (right-zero-* m))
--    (sym (right-zero-* (suc m ^ suc p)))
--
-- An even shorter proof can be written using `rewrite`. `rewrite` will try to
-- apply the `lemmas` we tell it to apply once, descending order. If the
-- rewriting process works by the end, we will only need `refl` to indicate
-- that both sides of the proof are the same.
--
--distr-^-* (suc m) zero (suc p)
--  rewrite
---- We start with what we want to proof:
----
----  (suc m * zero) ^ suc p ≡ suc m ^ suc p * zero ^ suc p
----
----  which reduces to
----
----  m * 0 * (m * 0) ^ p ≡ (suc m ^ p + m * suc m ^ p) * 0
----
--    right-zero-* m -- asking to rewrite all appearances of `m * 0` for `0`
----
----  λ m p → 0 * 0 ^ p ≡ (suc m ^ p + m * suc m ^ p) * 0
----
----  which reduces to
----
----  0 ≡ (suc m ^ p + m * suc m ^ p) * 0
----
--  -- asking to rewrite all appearances of `(suc m ^ suc p) * 0` for `0`
--  -- (notice that: `(suc m ^ suc p)` reduces to `(suc m ^ p + m * suc m ^ p)`)
--  | right-zero-* (suc m ^ suc p)
----
----  0 ≡ 0
----
----  We have arrived to a expression where both sides are equal. Thus we have
----  found a proof.
--  = refl
--

--  The final part of the inductive proof requires us to proof the inductive
--  case:
distr-^-* (suc m) (suc n) (suc p)
  rewrite
-- First we start with expression:
--
--  (m * n) ^ p ≡ (m ^ p) * (n ^ p)
--
--  Reducing the expression  to its normal form:
--
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡ (suc m ^ p + m * suc m ^ p) * (suc n ^ p + n * suc n ^ p)
--  Applying distributivity of _+_ over _*_
    distr-*-+ (suc m ^ p) (m * suc m ^ p) (suc n ^ p + n * suc n ^ p)
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * (suc n ^ p + n * suc n ^ p)
--    + m * suc m ^ p * (suc n ^ p + n * suc n ^ p)
  | assoc-* m (suc m ^ p) (suc n ^ p + n * suc n ^ p)
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * (suc n ^ p + n * suc n ^ p)
--    + m * (suc m ^ p * (suc n ^ p + n * suc n ^ p))
  | distl-*-+ (suc m ^ p) (suc n ^ p) (n * suc n ^ p)
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | comm-* m (suc n)
--    suc (n + (m + n * m)) ^ p
--    + (n + (m + n * m)) * suc (n + (m + n * m)) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | comm-* n m
--    suc (n + (m + m * n)) ^ p
--    + (n + (m + m * n)) * suc (n + (m + m * n)) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | sym (suc-right-* m n)
--    suc (n + m * suc n) ^ p
--    + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | distr-^-* (suc m) (suc n) p -- INDUCTIVE HYPOTHESIS!!
--    suc m ^ p * suc n ^ p + (n + m * suc n) * (suc m ^ p * suc n ^ p)
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | distr-*-+ n (m * suc n) (suc m ^ p * suc n ^ p)
--    suc m ^ p * suc n ^ p + (n * (suc m ^ p * suc n ^ p)
--    + m * suc n * (suc m ^ p * suc n ^ p))
--    ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | distl-*-+ m (suc m ^ p * suc n ^ p) (suc m ^ p * (n * suc n ^ p))
--    suc m ^ p * suc n ^ p + (n * (suc m ^ p * suc n ^ p)
--    + m * suc n * (suc m ^ p * suc n ^ p))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | comm-* m (suc n)
--    suc m ^ p * suc n ^ p + (n * (suc m ^ p * suc n ^ p)
--    + (m + n * m) * (suc m ^ p * suc n ^ p))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | distr-*-+ m (n * m) (suc m ^ p * suc n ^ p)
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | swap-m-n-* n (suc m ^ p) (suc n ^ p)
--    suc m ^ p * suc n ^ p +
--    (suc m ^ p * (n * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | swap-m-n-* (suc m ^ p) n (suc n ^ p)
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + n * (suc m ^ p * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * (n * (suc m ^ p * suc n ^ p)))
  | sym (assoc-* m n (suc m ^ p * suc n ^ p))
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + n * (suc m ^ p * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * n * (suc m ^ p * suc n ^ p))
  | comm-* m n
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--    ≡
--    suc m ^ p * suc n ^ p + n * (suc m ^ p * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p))
  | assoc-+ (suc m ^ p * suc n ^ p) (n * (suc m ^ p * suc n ^ p))
    (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p))
--
-- We finally find that the two expressions are equal!
--
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--    ≡
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--
-- QED
  = refl

-- The full proof without comments:
--distr-^-* : ∀ (m n p) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
--distr-^-* _       _       zero    = refl
--distr-^-* zero    _       (suc p) = refl
--distr-^-* (suc m) zero    (suc p)
--  rewrite
--    right-zero-* m
--  | right-zero-* (suc m ^ suc p)
--  = refl
--distr-^-* (suc m) (suc n) (suc p)
--  rewrite
--    distr-*-+ (suc m ^ p) (m * suc m ^ p) (suc n ^ p + n * suc n ^ p)
--  | assoc-* m (suc m ^ p) (suc n ^ p + n * suc n ^ p)
--  | distl-*-+ (suc m ^ p) (suc n ^ p) (n * suc n ^ p)
--  | comm-* m (suc n)
--  | comm-* n m
--  | sym (suc-right-* m n)
--  | distr-^-* (suc m) (suc n) p
--  | distr-*-+ n (m * suc n) (suc m ^ p * suc n ^ p)
--  | distl-*-+ m (suc m ^ p * suc n ^ p) (suc m ^ p * (n * suc n ^ p))
--  | comm-* m (suc n)
--  | distr-*-+ m (n * m) (suc m ^ p * suc n ^ p)
--  | swap-m-n-* n (suc m ^ p) (suc n ^ p)
--  | swap-m-n-* (suc m ^ p) n (suc n ^ p)
--  | sym (assoc-* m n (suc m ^ p * suc n ^ p))
--  | comm-* m n
--  | assoc-+ (suc m ^ p * suc n ^ p) (n * (suc m ^ p * suc n ^ p))
--    (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p))
--  = refl


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

-- Identity-on-Objects Functor for (Object-)Unbundled Categories

module Categories.Functor.IdentityOnObjects where

open import Data.Product using (_,_)
open import Function using () renaming (id to id→)
open import Level

open import Categories.Category.Unbundled using (Category)
open import Categories.Category.Unbundled.Properties using (pack′)
open import Categories.Category.Unbundled.Utilities using (module Equiv)
open import Categories.Functor.Core using (Functor)

private
  variable
    o ℓ e ℓ′ e′ : Level

record IdentityOnObjects {Obj : Set o} (C : Category Obj ℓ e) (D : Category Obj ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ ℓ′ ⊔ e′) where
  eta-equality
  private module C = Category C
  private module D = Category D

  field
    F₁ : ∀ {A B} → (A C.⇒ B) → A D.⇒ B

    identity     : ∀ {A} → F₁ (C.id {A}) D.≈ D.id
    homomorphism : ∀ {X Y Z} {f : X C.⇒ Y} {g : Y C.⇒ Z} →
                     F₁ (g C.∘ f) D.≈ F₁ g D.∘ F₁ f
    F-resp-≈     : ∀ {A B} {f g : A C.⇒ B} → f C.≈ g → F₁ f D.≈ F₁ g

IOO⇒Functor : {Ob : Set o} {C : Category Ob ℓ e} {D : Category Ob ℓ′ e′} →
  (F : IdentityOnObjects C D) → Functor (pack′ C) (pack′ D)
IOO⇒Functor F = record { F₀ = id→; IOO }
  where module IOO = IdentityOnObjects F

id-IOO : {Obj : Set o} {C : Category Obj ℓ e} → IdentityOnObjects C C
id-IOO {C = C} = record { F₁ = id→ ; identity = refl ; homomorphism = refl ; F-resp-≈ = id→ }
  where open Equiv C

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --no-termination-check #-}

module Data.Nat where

import Prelude
import Data.Bool as Bool

open Prelude
open Bool

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

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN SUC suc #-}
{-# BUILTIN ZERO zero #-}

infix 40 _==_ _<_ _≤_ _>_ _≥_
infixl 60 _+_ _-_
infixl 70 _*_
infixr 80 _^_
infix 100 _!

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

_-_ : Nat -> Nat -> Nat
zero  - m     = zero
suc n - zero  = suc n
suc n - suc m = n - m

_*_ : Nat -> Nat -> Nat
zero  * m = zero
suc n * m = m + n * m

_^_ : Nat -> Nat -> Nat
n ^ zero  = 1
n ^ suc m = n * n ^ m

_! : Nat -> Nat
zero  ! = 1
suc n ! = suc n * n !

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATMINUS _-_ #-}
{-# BUILTIN NATTIMES _*_ #-}

_==_ : Nat -> Nat -> Bool
zero  == zero  = true
zero  == suc _ = false
suc _ == zero  = false
suc n == suc m = n == m

_<_ : Nat -> Nat -> Bool
n     < zero  = false
zero  < suc m = true
suc n < suc m = n < m

_≤_ : Nat -> Nat -> Bool
n ≤ m = n < suc m

_>_ = flip _<_
_≥_ = flip _≤_

{-# BUILTIN NATEQUALS _==_ #-}
{-# BUILTIN NATLESS   _<_  #-}

divSucAux : Nat -> Nat -> Nat -> Nat -> Nat
divSucAux k m zero    j       = k
divSucAux k m (suc n) zero    = divSucAux (suc k) m n m
divSucAux k m (suc n) (suc j) = divSucAux k m n j

modSucAux : Nat -> Nat -> Nat -> Nat -> Nat
modSucAux k m zero    j       = k
modSucAux k m (suc n) zero    = modSucAux zero m n m
modSucAux k m (suc n) (suc j) = modSucAux (suc k) m n j

{-# BUILTIN NATDIVSUCAUX divSucAux #-}
{-# BUILTIN NATMODSUCAUX modSucAux #-}

div : Nat -> Nat -> Nat
div n  zero   = zero
div n (suc m) = divSucAux zero m n m

mod : Nat -> Nat -> Nat
mod n  zero   = zero
mod n (suc m) = modSucAux zero m n m

gcd : Nat -> Nat -> Nat
gcd a 0 = a
gcd a b = gcd b (mod a b)

lcm : Nat -> Nat -> Nat
lcm a b = div (a * b) (gcd a b)

even : Nat -> Bool
even n = mod n 2 == 0

odd : Nat -> Bool
odd n = mod n 2 == 1

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text: module Categories.Functor.Monoidal where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2016-09-20 issue #2197
-- We are now only turning eta-equality on after positivity check.
-- This is at the end of the mutual block.

module _ where

open import Common.Equality

module Works where

  mutual

    record ⊤ : Set where
      eta-equality

    test : ∀ {x y : ⊤} → x ≡ y
    test = refl

mutual

  record ⊤ : Set where

  test : ∀ {x y : ⊤} → x ≡ y
  test = refl
    -- Fails, as eta-equality is only turned on after mutual block.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.XModule where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Structures.Constant

open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.Action

private
  variable
    ℓ ℓ' : Level

-------------------------------------------------
-- Definitions and properties of
-- equivariance and peiffer condition
-------------------------------------------------
module _ ((((G₀ , H) , _α_) , isAct) : Action ℓ ℓ') (φ : GroupHom H G₀) where

  open GroupNotation₀ G₀
  open GroupNotationᴴ H

  private
    f = GroupHom.fun φ

  -- α is equivariant w.r.t φ if φ (g α h) ≡ g + (φ h) - g
  isEquivariant : Type (ℓ-max ℓ ℓ')
  isEquivariant = (g : ⟨ G₀ ⟩) → (h : ⟨ H ⟩) → f (g α h) ≡ (g +₀ f h) -₀ g

  -- G₀ is a set, so isEquivariant is a proposition
  isPropIsEquivariant : isProp isEquivariant
  isPropIsEquivariant = isPropΠ2 (λ g h → set₀ (f (g α h)) ((g +₀ f h) -₀ g))

  -- (α, φ) satisfies the peiffer condition, if
  -- (φ h) α h' ≡ h + h' - h
  isPeiffer : Type ℓ'
  isPeiffer = (h h' : ⟨ H ⟩) → (f h) α h' ≡ (h +ᴴ h') -ᴴ h

  -- H is a set, so isPeiffer is a proposition
  isPropIsPeiffer : isProp isPeiffer
  isPropIsPeiffer = isPropΠ2 (λ h h' → setᴴ ((f h) α h') ((h +ᴴ h') -ᴴ h))

module _ (ℓ ℓ' : Level) where
  ----------------------
  -- Define the types of
  -- - Actions α with a morphism φ
  -- - Precrossed modules
  -- - Crossed modules
  -- and add URG structures to them
  ----------------------
  ActionB = Σ[ (((G₀ , H) , _α_) , isAct) ∈ Action ℓ ℓ' ] (GroupHom H G₀)
  PreXModule = Σ[ (α , φ) ∈ ActionB ] (isEquivariant α φ)
  XModule = Σ[ ((α , φ) , isEqui) ∈ PreXModule ] (isPeiffer α φ)

  -- displayed over 𝒮-Action, a morphism back
  -- by lifting the morphism back over Grp² twice
  𝒮ᴰ-Action\PreXModuleStr : URGStrᴰ (𝒮-Action ℓ ℓ')
                           (λ (((G , H) , _) , _) → GroupHom H G)
                           (ℓ-max ℓ ℓ')
  𝒮ᴰ-Action\PreXModuleStr = VerticalLift2-𝒮ᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                                               (𝒮ᴰ-G²\B ℓ ℓ')
                                               (𝒮ᴰ-G²\Las ℓ ℓ')
                                               (𝒮ᴰ-G²Las\Action ℓ ℓ')

  𝒮-PreXModuleStr : URGStr ActionB (ℓ-max ℓ ℓ')
  𝒮-PreXModuleStr = ∫⟨ 𝒮-Action ℓ ℓ' ⟩ 𝒮ᴰ-Action\PreXModuleStr

  -- add equivariance condition
  -- use that equivariance is a proposition
  𝒮ᴰ-PreXModule : URGStrᴰ 𝒮-PreXModuleStr
                         (λ (α , φ) → isEquivariant α φ)
                         ℓ-zero
  𝒮ᴰ-PreXModule = Subtype→Sub-𝒮ᴰ (λ (α , φ) → isEquivariant α φ , isPropIsEquivariant α φ)
                                 𝒮-PreXModuleStr

  𝒮-PreXModule : URGStr PreXModule (ℓ-max ℓ ℓ')
  𝒮-PreXModule = ∫⟨ 𝒮-PreXModuleStr ⟩ 𝒮ᴰ-PreXModule

  -- add the proposition isPeiffer to precrossed modules
  𝒮ᴰ-XModule : URGStrᴰ 𝒮-PreXModule
                       (λ ((α , φ) , isEqui) → isPeiffer α φ)
                       ℓ-zero
  𝒮ᴰ-XModule = Subtype→Sub-𝒮ᴰ (λ ((α , φ) , isEqui) → isPeiffer α φ , isPropIsPeiffer α φ)
                              𝒮-PreXModule

  𝒮-XModule : URGStr XModule (ℓ-max ℓ ℓ')
  𝒮-XModule = ∫⟨ 𝒮-PreXModule ⟩ 𝒮ᴰ-XModule

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Vector where

open import OscarPrelude
open import Arity

record Vector (A : Set) (𝑎 : Arity) : Set
 where
  constructor ⟨_⟩
  field
    vector : Vec A (arity 𝑎)

open Vector public

instance EqVector : {A : Set} ⦃ _ : Eq A ⦄ {𝑎 : Arity} → Eq (Vector A 𝑎)
Eq._==_ EqVector _ = decEq₁ (cong vector) ∘ (_≟_ on vector $ _)


text:
{-

Type-level differentiation in Agda; or differentiation of functors!

Most things below are just restatements of elementary category theory.

The new things are Diff, which defines the derivative of an arbitrary
functor from Set to Set, and _+++_ _***_ _∘∘∘_ which show how to
differentiate sums, products and compositions of such functors.

-}

{-# OPTIONS --type-in-type #-}  -- needed in (fun (Diff f) x)
module DiffFunctor where

-- ( syntax )
infix 6 _[_]
infix 5 _∘∘_
infix 5 _∘∘∘_
infix 4 _**_
infix 4 _***_
infix 3 _++_
infix 2 _=>_

-- Numbers are formalised as sets!
Num = Set

-- ( addition of numbers )
data _+_ (a : Num) (b : Num) : Num where
  inl : a -> a + b
  inr : b -> a + b

[_,_] : {a b c : Num} -> (a -> c) -> (b -> c) -> (a + b -> c)
[ a , b ] (inl x) = a x
[ a , b ] (inr x) = b x

map[+] : {a₀ b₀ a₁ b₁ : Num} -> (a₀ -> a₁) -> (b₀ -> b₁) -> (a₀ + b₀ -> a₁ + b₁)
map[+] a b (inl x) = inl (a x)
map[+] a b (inr x) = inr (b x)

-- ( multiplication of numbers )
data _*_ (a : Num) (b : Num) : Num where
  pair : a -> b -> a * b

⟨_,_⟩ : {a b c : Num} -> (c -> a) -> (c -> b) -> (c -> a * b)
⟨ a , b ⟩ x = pair (a x) (b x)

map[*] : {a₀ b₀ a₁ b₁ : Num} -> (a₀ -> a₁) -> (b₀ -> b₁) -> (a₀ * b₀ -> a₁ * b₁)
map[*] a b (pair x y) = pair (a x) (b y)

-- Functions are formalised as functors!
record Fun : Set where
  constructor _[_]
  field
    fun : Num -> Num
    map : {x y : Num} -> (u : x -> y) -> (fun x -> fun y)

open Fun

-- ( pointwise addition of functions )
_++_ : Fun -> Fun -> Fun
fun (f ++ g) x = fun f x + fun g x
map (f ++ g) u = map[+] (map f u) (map g u)

-- ( pointwise multiplication of functions )
_**_ : Fun -> Fun -> Fun
fun (f ** g) x = fun f x * fun g x
map (f ** g) u = map[*] (map f u) (map g u)

-- ( composition of functions )
_∘∘_ : Fun -> Fun -> Fun
fun (f ∘∘ g) x = fun f (fun g x)
map (f ∘∘ g) u = map f (map g u)

-- Differentiation is parametric consumption of a resource!
-- You are supposed to use dx : h precisely once, like in linear logic.
Diff : Fun -> Fun
fun (Diff f) x = {h : Num} -> (dx : h) -> fun f (x + h)
map (Diff f) u f[x+·] dx = map f (map[+] u (\dx -> dx)) (f[x+·] dx)

-- A differentiation rule is a natural transformation! (in reverse)
_=>_ : Fun -> Fun -> Set
f => g = ((x : Num) -> fun f x -> fun g x)
-- (omitting naturality conditions)

-- ( derivative of sum )
_+++_ : (f g : Fun) -> Diff f ++ Diff g => Diff (f ++ g)
(f +++ g) x (inl f[x+·]) dx = inl (f[x+·] dx)
(f +++ g) x (inr g[x+·]) dx = inr (g[x+·] dx)

-- (derivative of product )
_***_ : (f g : Fun) -> Diff f ** g ++ f ** Diff g => Diff (f ** g)
(f *** g) x (inl (pair f[x+·] g[x])) dx = pair (f[x+·] dx) (map g inl g[x])
(f *** g) x (inr (pair f[x] g[x+·])) dx = pair (map f inl f[x]) (g[x+·] dx)

-- ( derivative of composition )
_∘∘∘_ : (f g : Fun) -> Diff f ∘∘ g ** Diff g => Diff (f ∘∘ g)
(f ∘∘∘ g) x (pair f[g[x]+·] g[x+·]) {h} dx = f[g[x+dx]]
  where
    f[g[x+dx]] : fun (f ∘∘ g) (x + h)
    f[g[x+dx]] = map f [ map g inl , g[x+·] ] (f[g[x]+·] dx)

{-

Things that need to be done:
 - Define higher order derivatives as follows:
       HighDiff n f x = forall h. h |n| -> f (x + h)
   Here h |n| stands for n copies of the resource h. Try to show
       n! -> Diff^n f => HighDiff n f.
 - Explore differential calculus in several variables.
 - Explore integration and differential equations. (hard)
 - Solve partial differential equations. (good luck)
 - Explore inverse functions. (hard)
 - Write some examples, such as
       0 => Diff (Const a)
       1 => Diff Id
       n * Id^(n-1) => Diff Id^n
       List ** List => Diff List
       derivatives of linear transformations

-}

max_stars_repo_name: JoelSjogren/diff-functor

max_issues_repo_name: JoelSjogren/diff-functor

max_forks_repo_name: JoelSjogren/diff-functor


text:
module Long where

data Nat : Set where
  z : Nat
  s : (n : Nat) → Nat

data Exp : Set where
  val : (n : Nat) → Exp
  throw : Exp

data Maybe (A : Set) : Set where
  Just    : A → Maybe A
  Nothing : Maybe A

abstract

  s′ : Nat → Nat
  s′ = s

eval : Exp → Maybe Nat
eval (val n) = ?
eval throw   = ?

data D : Nat → Set where
  d : D z

foo : D {!!}
foo = {!!}

bar : D z
bar = {!!}

baz : Maybe {!!}
baz = {!!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
open import Prelude

module Implicits.Syntax.Type.Unification where

open import Data.Maybe as Maybe
open import Data.Unit
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification.McBride as McBride using (
  substitute; asub; AList; _//_) public
open import Data.Vec.Properties
open import Data.Nat as N using ()
open import Data.Nat.Properties.Simple
open import Category.Monad

open import Data.Fin.Substitution
open import Implicits.Substitutions
open import Implicits.Syntax.MetaType public
open import Implicits.Substitutions.Lemmas
open McBride using (substitute; asub; AList; ASub; _//_; asub-weaken) public

private
  module M = MetaTypeMetaSubst
  module T = MetaTypeTypeSubst

-- Just a bit stricter than mcbride.mgu
-- We require here as well that all meta variables are instantiated
-- (this is equivalent to the ⊢unamb constraint in Oliveira)
mgu : ∀ {m ν} (a : MetaType m ν) → (b : SimpleType ν) → Maybe (Sub (flip MetaType ν) m zero)
mgu a b with McBride.mgu a (simpl b)
mgu a b | just (zero , u) = just (asub u)
mgu a b | just (suc m , _) = nothing
mgu a b | nothing = nothing

Unifier : ∀ {m ν} → (MetaType m ν) → SimpleType ν → (Sub (flip MetaType ν) m zero) → Set
Unifier {m} a b u = from-meta (a M./ u) ≡ (simpl b)

Unifiable : ∀ {m ν} → (MetaType m ν) → SimpleType ν → Set
Unifiable a τ = ∃ (Unifier a τ)

◁-Unifiable : ∀ {m ν} → MetaType m ν → SimpleType ν → Set
◁-Unifiable x τ = Unifiable (x M.◁m) τ

meta-weaken = M.weaken
smeta-weaken = M.smeta-weaken
open-meta = M.open-meta


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to lists
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Pointwise where

open import Function
open import Function.Inverse using (Inverse)
open import Data.Product hiding (map)
open import Data.List.Base as List hiding (map; head; tail)
open import Data.List.Properties using (≡-dec)
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.Nat using (ℕ; zero; suc)
open import Level
open import Relation.Nullary
open import Relation.Nullary.Negation using (contradiction)
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Unary as U using (Pred)
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

infixr 5 _∷_

data Pointwise {a b ℓ} {A : Set a} {B : Set b}
         (_∼_ : REL A B ℓ) : List A → List B → Set (a ⊔ b ⊔ ℓ) where
  []  : Pointwise _∼_ [] []
  _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Pointwise _∼_ xs ys) →
        Pointwise _∼_ (x ∷ xs) (y ∷ ys)

------------------------------------------------------------------------
-- Operations

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  head : ∀ {x y xs ys} → Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
  head (x∼y ∷ xs∼ys) = x∼y

  tail : ∀ {x y xs ys} → Pointwise _∼_ (x ∷ xs) (y ∷ ys) →
         Pointwise _∼_ xs ys
  tail (x∼y ∷ xs∼ys) = xs∼ys

  rec : ∀ {c} (P : ∀ {xs ys} → Pointwise _∼_ xs ys → Set c) →
        (∀ {x y xs ys} {xs∼ys : Pointwise _∼_ xs ys} →
          (x∼y : x ∼ y) → P xs∼ys → P (x∼y ∷ xs∼ys)) →
        P [] →
        ∀ {xs ys} (xs∼ys : Pointwise _∼_ xs ys) → P xs∼ys
  rec P c n []            = n
  rec P c n (x∼y ∷ xs∼ys) = c x∼y (rec P c n xs∼ys)

  map : ∀ {ℓ₂} {_≈_ : REL A B ℓ₂} →
        _≈_ ⇒ _∼_ → Pointwise _≈_ ⇒ Pointwise _∼_
  map ≈⇒∼ []            = []
  map ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ map ≈⇒∼ xs≈ys

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

reflexive : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
            {_≈_ : REL A B ℓ₁} {_∼_ : REL A B ℓ₂} →
            _≈_ ⇒ _∼_ → Pointwise _≈_ ⇒ Pointwise _∼_
reflexive ≈⇒∼ []            = []
reflexive ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ reflexive ≈⇒∼ xs≈ys

refl : ∀ {a ℓ} {A : Set a} {_∼_ : Rel₂ A ℓ} →
       Reflexive _∼_ → Reflexive (Pointwise _∼_)
refl rfl {[]}     = []
refl rfl {x ∷ xs} = rfl ∷ refl rfl

symmetric : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
            {_≈_ : REL A B ℓ₁} {_∼_ : REL B A ℓ₂} →
            Sym _≈_ _∼_ → Sym (Pointwise _≈_) (Pointwise _∼_)
symmetric sym []            = []
symmetric sym (x∼y ∷ xs∼ys) = sym x∼y ∷ symmetric sym xs∼ys

transitive : ∀ {a b c ℓ₁ ℓ₂ ℓ₃}
             {A : Set a} {B : Set b} {C : Set c}
             {_≋_ : REL A B ℓ₁} {_≈_ : REL B C ℓ₂} {_∼_ : REL A C ℓ₃} →
             Trans _≋_ _≈_ _∼_ →
             Trans (Pointwise _≋_) (Pointwise _≈_) (Pointwise _∼_)
transitive trans []            []            = []
transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
  trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs

antisymmetric : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b}
                {_≤_ : REL A B ℓ₁} {_≤′_ : REL B A ℓ₂} {_≈_ : REL A B ℓ₃} →
                Antisym _≤_ _≤′_ _≈_ →
                Antisym (Pointwise _≤_) (Pointwise _≤′_) (Pointwise _≈_)
antisymmetric antisym []            []            = []
antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) =
  antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs

respects₂ : ∀ {a ℓ₁ ℓ₂} {A : Set a}
            {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
            _∼_ Respects₂ _≈_ →
            (Pointwise _∼_) Respects₂ (Pointwise _≈_)
respects₂ {_≈_ = _≈_} {_∼_} resp = resp¹ , resp²
  where
  resp¹ : ∀ {xs} → (Pointwise _∼_ xs) Respects (Pointwise _≈_)
  resp¹ []            []            = []
  resp¹ (x≈y ∷ xs≈ys) (z∼x ∷ zs∼xs) =
    proj₁ resp x≈y z∼x ∷ resp¹ xs≈ys zs∼xs

  resp² : ∀ {ys} → (flip (Pointwise _∼_) ys) Respects (Pointwise _≈_)
  resp² []            []            = []
  resp² (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) =
    proj₂ resp x≈y x∼z ∷ resp² xs≈ys xs∼zs

decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
            Decidable _∼_ → Decidable (Pointwise _∼_)
decidable dec []       []       = yes []
decidable dec []       (y ∷ ys) = no (λ ())
decidable dec (x ∷ xs) []       = no (λ ())
decidable dec (x ∷ xs) (y ∷ ys) with dec x y
... | no ¬x∼y = no (¬x∼y ∘ head)
... | yes x∼y with decidable dec xs ys
...   | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
...   | yes xs∼ys = yes (x∼y ∷ xs∼ys)

isEquivalence : ∀ {a ℓ} {A : Set a} {_≈_ : Rel₂ A ℓ} →
                IsEquivalence _≈_ → IsEquivalence (Pointwise _≈_)
isEquivalence eq = record
  { refl  = refl       Eq.refl
  ; sym   = symmetric  Eq.sym
  ; trans = transitive Eq.trans
  } where module Eq = IsEquivalence eq

isPreorder : ∀ {a ℓ₁ ℓ₂} {A : Set a}
             {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
             IsPreorder _≈_ _∼_ → IsPreorder (Pointwise _≈_) (Pointwise _∼_)
isPreorder pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = reflexive     Pre.reflexive
  ; trans         = transitive    Pre.trans
  } where module Pre = IsPreorder pre

isPartialOrder : ∀ {a ℓ₁ ℓ₂} {A : Set a}
                 {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} →
                 IsPartialOrder _≈_ _≤_ →
                 IsPartialOrder (Pointwise _≈_) (Pointwise _≤_)
isPartialOrder po = record
  { isPreorder = isPreorder    PO.isPreorder
  ; antisym    = antisymmetric PO.antisym
  } where module PO = IsPartialOrder po

isDecEquivalence : ∀ {a ℓ} {A : Set a} {_≈_ : Rel₂ A ℓ} →
                   IsDecEquivalence _≈_ →
                   IsDecEquivalence (Pointwise _≈_)
isDecEquivalence eq = record
  { isEquivalence = isEquivalence DE.isEquivalence
  ; _≟_           = decidable     DE._≟_
  } where module DE = IsDecEquivalence eq

preorder : ∀ {p₁ p₂ p₃} → Preorder p₁ p₂ p₃ → Preorder _ _ _
preorder p = record
  { isPreorder = isPreorder (Preorder.isPreorder p)
  }

poset : ∀ {c ℓ₁ ℓ₂} → Poset c ℓ₁ ℓ₂ → Poset _ _ _
poset p = record
  { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
  }

setoid : ∀ {c ℓ} → Setoid c ℓ → Setoid _ _
setoid s = record
  { isEquivalence = isEquivalence (Setoid.isEquivalence s)
  }

decSetoid : ∀ {c ℓ} → DecSetoid c ℓ → DecSetoid _ _
decSetoid d = record
  { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
  }

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

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              (∀ i → f i ∼ g i) → Pointwise _∼_ (tabulate f) (tabulate g)
  tabulate⁺ {zero}  f∼g = []
  tabulate⁺ {suc n} f∼g = f∼g fzero ∷ tabulate⁺ (f∼g ∘ fsuc)

  tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              Pointwise _∼_ (tabulate f) (tabulate g) → (∀ i → f i ∼ g i)
  tabulate⁻ {zero}  []            ()
  tabulate⁻ {suc n} (x∼y ∷ xs∼ys) fzero    = x∼y
  tabulate⁻ {suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i

------------------------------------------------------------------------
-- _++_

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  ++⁺ : ∀ {ws xs ys zs} → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs)
  ++⁺ []            ys∼zs = ys∼zs
  ++⁺ (w∼x ∷ ws∼xs) ys∼zs = w∼x ∷ ++⁺ ws∼xs ys∼zs

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

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  concat⁺ : ∀ {xss yss} → Pointwise (Pointwise _∼_) xss yss →
            Pointwise _∼_ (concat xss) (concat yss)
  concat⁺ []                = []
  concat⁺ (xs∼ys ∷ xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)

------------------------------------------------------------------------
-- length

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  Pointwise-length : ∀ {xs ys} → Pointwise _∼_ xs ys →
                     length xs ≡ length ys
  Pointwise-length []            = P.refl
  Pointwise-length (x∼y ∷ xs∼ys) = P.cong ℕ.suc (Pointwise-length xs∼ys)

------------------------------------------------------------------------
-- reverse

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  reverseAcc⁺ : ∀ {as bs as′ bs′} → Pointwise R as′ bs′ → Pointwise R as bs →
                Pointwise R (reverseAcc as′ as) (reverseAcc bs′ bs)
  reverseAcc⁺ rs′ []       = rs′
  reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs

  reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs)
  reverse⁺ = reverseAcc⁺ []

------------------------------------------------------------------------
-- map

module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : REL C D r} where

  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
         Pointwise (λ a b → R (f a) (g b)) as bs →
         Pointwise R (List.map f as) (List.map g bs)
  map⁺ f g []       = []
  map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs

  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
         Pointwise R (List.map f as) (List.map g bs) →
         Pointwise (λ a b → R (f a) (g b)) as bs
  map⁻ {[]} {[]} f g [] = []
  map⁻ {[]} {b ∷ bs} f g rs with Pointwise-length rs
  ... | ()
  map⁻ {a ∷ as} {[]} f g rs with Pointwise-length rs
  ... | ()
  map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs

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

module _ {a b r p q} {A : Set a} {B : Set b} {R : REL A B r}
         {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decidable Q)
         (P⇒Q : ∀ {a b} → R a b → P a → Q b) (Q⇒P : ∀ {a b} → R a b → Q b → P a)
         where

  filter⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (filter P? as) (filter Q? bs)
  filter⁺ []       = []
  filter⁺ {a ∷ _} {b ∷ _} (r ∷ rs) with P? a | Q? b
  ... | yes p | yes q = r ∷ filter⁺ rs
  ... | yes p | no ¬q = contradiction (P⇒Q r p) ¬q
  ... | no ¬p | yes q = contradiction (Q⇒P r q) ¬p
  ... | no ¬p | no ¬q = filter⁺ rs

------------------------------------------------------------------------
-- replicate

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  replicate⁺ : ∀ {a b} → R a b → ∀ n → Pointwise R (replicate n a) (replicate n b)
  replicate⁺ r 0       = []
  replicate⁺ r (suc n) = r ∷ replicate⁺ r n

------------------------------------------------------------------------
-- Irrelevance

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  irrelevant : Irrelevant R → Irrelevant (Pointwise R)
  irrelevant R-irr [] [] = P.refl
  irrelevant R-irr (r ∷ rs) (r₁ ∷ rs₁) =
    P.cong₂ _∷_ (R-irr r r₁) (irrelevant R-irr rs rs₁)

------------------------------------------------------------------------
-- Properties of propositional pointwise

module _ {a} {A : Set a} where

  Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_
  Pointwise-≡⇒≡ []               = P.refl
  Pointwise-≡⇒≡ (P.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys
  ... | P.refl = P.refl

  ≡⇒Pointwise-≡ :  _≡_ ⇒ Pointwise {A = A} _≡_
  ≡⇒Pointwise-≡ P.refl = refl P.refl

  Pointwise-≡↔≡ : Inverse (setoid (P.setoid A)) (P.setoid (List A))
  Pointwise-≡↔≡ = record
    { to         = record { _⟨$⟩_ = id; cong = Pointwise-≡⇒≡ }
    ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Pointwise-≡ }
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl P.refl
      ; right-inverse-of = λ _ → P.refl
      }
    }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

Rel    = Pointwise
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.15.
Please use Pointwise instead."
#-}
Rel≡⇒≡ = Pointwise-≡⇒≡
{-# WARNING_ON_USAGE Rel≡⇒≡
"Warning: Rel≡⇒≡ was deprecated in v0.15.
Please use Pointwise-≡⇒≡ instead."
#-}
≡⇒Rel≡ = ≡⇒Pointwise-≡
{-# WARNING_ON_USAGE ≡⇒Rel≡
"Warning: ≡⇒Rel≡ was deprecated in v0.15.
Please use ≡⇒Pointwise-≡ instead."
#-}
Rel↔≡  = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Rel↔≡
"Warning: Rel↔≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}

-- Version 1.0

decidable-≡ = ≡-dec
{-# WARNING_ON_USAGE decidable-≡
"Warning: decidable-≡ was deprecated in v1.0.
Please use ≡-dec from `Data.List.Properties` instead."
#-}


text:
------------------------------------------------------------------------
-- Identifiers
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module Examples.Identifier where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char
open import Data.List.NonEmpty
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary

open import Grammar.Infinite as Grammar
  using (Grammar) hiding (module Grammar)
open import Pretty using (Doc; Pretty-printer)
open import Renderer
open import Utilities

-- Lower-case (ASCII) characters.

is-lower : Char → Bool
is-lower t = ('a' ≤?C t) ∧ (t ≤?C 'z')

-- A problematic attempt to define a grammar and a corresponding
-- pretty-printer for identifiers.

module Problematic where

  -- The grammar can be defined.

  identifier : Grammar (List⁺ Char)
  identifier = (proj₁ <$> sat is-lower) +
    where open Grammar

  -- However, it is impossible to define a corresponding
  -- pretty-printer.

  no-printer : ¬ Pretty-printer identifier
  no-printer identifier-printer = no-doc (identifier-printer [ 'A' ])
    where
    open Grammar

    lemma : ∀ {p : Char → Bool} {t s s′} →
            t ∷ s ∈ (proj₁ <$> sat p) + · s′ → T (p t)
    lemma (⊛-sem (<$>-sem (<$>-sem {x = _ , ok} _)) _) = ok

    no-doc : ¬ Doc identifier [ 'A' ]
    no-doc d = lemma (proj₂ (Renderer.string-exists d))

-- Identifiers.

Identifier : Set
Identifier = List⁺ (∃ λ t → T (is-lower t))

identifier : Grammar Identifier
identifier = sat is-lower +
  where open Grammar

identifier-printer : Pretty-printer identifier
identifier-printer = map+ (sat is-lower)
  where open Pretty

-- Identifiers possibly followed by whitespace.

identifier-w : Grammar Identifier
identifier-w = identifier <⊛ whitespace ⋆
  where open Grammar

identifier-w-printer : Pretty-printer identifier-w
identifier-w-printer n = identifier-printer n <⊛ nil-⋆
  where open Pretty

test : render 80 (identifier-w-printer (str⁺ "aaa")) ≡ "aaa"
test = refl

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


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

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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Fields.Orders.Total.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {_<_ : A → A → Set c} {pOrder : SetoidPartialOrder S _<_} {F : Field R} (p : PartiallyOrderedField F pOrder) where

open Setoid S
open Equivalence eq
open Ring R
open Group additiveGroup
open import Groups.Lemmas additiveGroup
open import Groups.Cyclic.Definition additiveGroup
open import Groups.Cyclic.DefinitionLemmas additiveGroup
open import Groups.Orders.Archimedean (toGroup R (PartiallyOrderedField.oRing p))
open import Rings.Orders.Partial.Lemmas (PartiallyOrderedField.oRing p)
open import Rings.InitialRing R
open SetoidPartialOrder pOrder
open PartiallyOrderedRing (PartiallyOrderedField.oRing p)
open Field F

ArchimedeanField : Set (a ⊔ c)
ArchimedeanField = (x : A) → (0R < x) → Sg ℕ (λ n → x < (fromN n))

private
  lemma : (r : A) (N : ℕ) → (positiveEltPower 1R N * r) ∼ positiveEltPower r N
  lemma r zero = timesZero'
  lemma r (succ n) = transitive *DistributesOver+' (+WellDefined identIsIdent (lemma r n))

  findBound : (0<1 : 0R < 1R) → (r s : A) (N : ℕ) → (1R < r) → (s < positiveEltPower 1R N) → s < positiveEltPower r N
  findBound _ r s zero 1<r s<N = s<N
  findBound 0<1 r s (succ N) 1<r s<N = <Transitive s<N (<WellDefined (transitive *Commutative identIsIdent) (lemma r (succ N)) (ringCanMultiplyByPositive' (fromNPreservesOrder 0<1 (succIsPositive N)) 1<r))

archFieldToGrp : ((x y : A) → 0R < x → (x * y) ∼ 1R → 0R < y) → ArchimedeanField → Archimedean
archFieldToGrp reciprocalPositive a r s 0<r 0<s with allInvertible r (λ r=0 → irreflexive (<WellDefined reflexive r=0 0<r))
... | inv , prInv with a inv (reciprocalPositive r inv 0<r (transitive *Commutative prInv))
... | N , invBound with a s 0<s
... | Ns , nSBound = (Ns *N N) , <WellDefined reflexive (symmetric (elementPowerMultiplies (nonneg Ns) (nonneg N) r)) (findBound (<WellDefined reflexive (transitive *Commutative prInv) (orderRespectsMultiplication 0<r (reciprocalPositive r inv 0<r (transitive *Commutative prInv)))) (positiveEltPower r N) s Ns m nSBound)
  where
    m : 1R < positiveEltPower r N
    m = <WellDefined prInv (lemma r N) (ringCanMultiplyByPositive 0<r invBound)

archToArchField : 0R < 1R → Archimedean → ArchimedeanField
archToArchField 0<1 arch a 0<a with arch 1R a 0<1 0<a
... | N , pr = N , pr