text:
open import Prelude
open import Nat
open import contexts
open import dom-eq
open import dynamics-core
open import lemmas-disjointness
open import statics-core

module disjointness where
  -- if a hole name is new in a term, then the resultant context is
  -- disjoint from any singleton context with that hole name
  mutual
    elab-new-disjoint-synth : ∀ {e u τ d Δ Γ Γ' τ'} →
                              hole-name-new e u →
                              Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                              Δ ## (■ (u , Γ' , τ'))
    elab-new-disjoint-synth HNNum ESNum = empty-disj _
    elab-new-disjoint-synth (HNPlus hn hn₁) (ESPlus apt x x₁ x₂) = disjoint-parts (elab-new-disjoint-ana hn x₁) (elab-new-disjoint-ana hn₁ x₂)
    elab-new-disjoint-synth (HNAsc hn) (ESAsc x) = elab-new-disjoint-ana hn x
    elab-new-disjoint-synth HNVar (ESVar x₁) = empty-disj (■ (_ , _ , _))
    elab-new-disjoint-synth (HNLam2 hn) (ESLam x₁ exp) = elab-new-disjoint-synth hn exp
    elab-new-disjoint-synth (HNHole x) ESEHole = disjoint-singles x
    elab-new-disjoint-synth (HNNEHole x hn) (ESNEHole x₁ exp) = disjoint-parts (disjoint-singles x) (elab-new-disjoint-synth hn exp)
    elab-new-disjoint-synth (HNAp hn hn₁) (ESAp x x₁ x₂ x₃ x₄ x₅) =
                                            disjoint-parts (elab-new-disjoint-ana hn x₄)
                                                  (elab-new-disjoint-ana hn₁ x₅)
    elab-new-disjoint-synth (HNPair hn hn₁) (ESPair x x₁ exp exp₁) = disjoint-parts (elab-new-disjoint-synth hn exp) (elab-new-disjoint-synth hn₁ exp₁)
    elab-new-disjoint-synth (HNLam1 hn) ()
    elab-new-disjoint-synth (HNInl hn) ()
    elab-new-disjoint-synth (HNInr hn) ()
    elab-new-disjoint-synth (HNCase hn hn₁ hn₂) ()
    elab-new-disjoint-synth (HNFst hn) (ESFst x x₁ x₂) = elab-new-disjoint-ana hn x₂
    elab-new-disjoint-synth (HNSnd hn) (ESSnd x x₁ x₂) = elab-new-disjoint-ana hn x₂

    elab-new-disjoint-ana : ∀{e u τ d Δ Γ Γ' τ' τ2} →
                            hole-name-new e u →
                            Γ ⊢ e ⇐ τ ~> d :: τ2 ⊣ Δ →
                            Δ ## (■ (u , Γ' , τ'))
    elab-new-disjoint-ana hn (EASubsume x x₁ x₂ x₃) = elab-new-disjoint-synth hn x₂
    elab-new-disjoint-ana (HNLam1 hn) (EALam x₁ x₂ ex) = elab-new-disjoint-ana hn ex
    elab-new-disjoint-ana (HNHole x) EAEHole = disjoint-singles x
    elab-new-disjoint-ana (HNNEHole x hn) (EANEHole x₁ x₂) = disjoint-parts (disjoint-singles x) (elab-new-disjoint-synth hn x₂)
    elab-new-disjoint-ana (HNInl hn) (EAInl x x₁) = elab-new-disjoint-ana hn x₁
    elab-new-disjoint-ana (HNInr hn) (EAInr x x₁) = elab-new-disjoint-ana hn x₁
    elab-new-disjoint-ana (HNCase hn hn₁ hn₂) (EACase x x₁ x₂ x₃ x₄ x₅ _ _ x₆ x₇ x₈ x₉) = disjoint-parts (elab-new-disjoint-synth hn x₆) (disjoint-parts (elab-new-disjoint-ana hn₁ x₈) (elab-new-disjoint-ana hn₂ x₉))

  -- dual of the above: if elaborating a term produces a context that's
  -- disjoint with a singleton context, it must be that the index is a new
  -- hole name in the original term
  mutual
    elab-disjoint-new-synth : ∀{e τ d Δ u Γ Γ' τ'} →
                              Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                              Δ ## (■ (u , Γ' , τ')) →
                              hole-name-new e u
    elab-disjoint-new-synth ESNum disj = HNNum
    elab-disjoint-new-synth (ESPlus {Δ1 = Δ1} apt x x₁ x₂) disj
      with elab-disjoint-new-ana x₁ (disjoint-union1 disj) | elab-disjoint-new-ana x₂ (disjoint-union2 {Γ1 = Δ1} disj)
    ... | ih1 | ih2 = HNPlus ih1 ih2
    elab-disjoint-new-synth (ESVar x₁) disj = HNVar
    elab-disjoint-new-synth (ESLam x₁ ex) disj = HNLam2 (elab-disjoint-new-synth ex disj)
    elab-disjoint-new-synth (ESAp {Δ1 = Δ1} x x₁ x₂ x₃ x₄ x₅) disj
      with elab-disjoint-new-ana x₄ (disjoint-union1 disj) | elab-disjoint-new-ana x₅ (disjoint-union2 {Γ1 = Δ1} disj)
    ... | ih1 | ih2 = HNAp ih1 ih2
    elab-disjoint-new-synth {Γ = Γ} ESEHole disj = HNHole (singles-notequal disj)
    elab-disjoint-new-synth {Γ = Γ} (ESNEHole {u = u} {Δ = Δ} x ex) disj = HNNEHole (singles-notequal (disjoint-union1 {Γ2 = Δ} disj)) (elab-disjoint-new-synth ex (disjoint-union2 {Γ1 = ■ (u , Γ , ⦇-⦈)} {Γ2 = Δ} disj))
    elab-disjoint-new-synth (ESAsc x) disj = HNAsc (elab-disjoint-new-ana x disj)
    elab-disjoint-new-synth (ESPair {Δ1 = Δ1} {Δ2 = Δ2} x x₁ x₂ x₃) disj = HNPair (elab-disjoint-new-synth x₂ (disjoint-union1 {Γ1 = Δ1} {Γ2 = Δ2} disj)) (elab-disjoint-new-synth x₃ (disjoint-union2 {Γ1 = Δ1} {Γ2 = Δ2} disj))
    elab-disjoint-new-synth (ESFst x x₁ x₂) disj = HNFst (elab-disjoint-new-ana x₂ disj)
    elab-disjoint-new-synth (ESSnd x x₁ x₂) disj = HNSnd (elab-disjoint-new-ana x₂ disj)

    elab-disjoint-new-ana : ∀{e τ d Δ u Γ Γ' τ2 τ'} →
                            Γ ⊢ e ⇐ τ ~> d :: τ2 ⊣ Δ →
                            Δ ## (■ (u , Γ' , τ')) →
                            hole-name-new e u
    elab-disjoint-new-ana (EALam x₁ x₂ ex) disj = HNLam1 (elab-disjoint-new-ana ex disj)
    elab-disjoint-new-ana (EASubsume x x₁ x₂ x₃) disj = elab-disjoint-new-synth x₂ disj
    elab-disjoint-new-ana EAEHole disj = HNHole (singles-notequal disj)
    elab-disjoint-new-ana {Γ = Γ} (EANEHole {u = u} {τ = τ} {Δ = Δ} x x₁) disj = HNNEHole (singles-notequal (disjoint-union1 {Γ2 = Δ} disj)) (elab-disjoint-new-synth x₁ (disjoint-union2 {Γ1 = ■ (u , Γ , τ)} {Γ2 = Δ} disj))
    elab-disjoint-new-ana (EAInl x x₁) disj = HNInl (elab-disjoint-new-ana x₁ disj)
    elab-disjoint-new-ana (EAInr x x₁) disj = HNInr (elab-disjoint-new-ana x₁ disj)
    elab-disjoint-new-ana {Γ = Γ} (EACase {Δ = Δ} {Δ1 = Δ1} {Δ2 = Δ2} x x₁ x₂ x₃ x₄ x₅ _ _ x₆ x₇ x₈ x₉) disj = HNCase (elab-disjoint-new-synth x₆ (disjoint-union1 disj)) (elab-disjoint-new-ana x₈ (disjoint-union1 {Γ2 = Δ2} (disjoint-union2 {Γ1 = Δ} disj))) (elab-disjoint-new-ana x₉ (disjoint-union2 {Γ1 = Δ1} (disjoint-union2 {Γ1 = Δ} disj)))

  -- collect up the hole names of a term as the indices of a trivial context
  data holes : (e : hexp) (H : ⊤ ctx) → Set where
    HNum   : ∀{n} → holes (N n) ∅
    HPlus  : ∀{e1 e2 H1 H2} → holes e1 H1 → holes e2 H2 → holes (e1 ·+ e2) (H1 ∪ H2)
    HAsc   : ∀{e τ H} → holes e H → holes (e ·: τ) H
    HVar   : ∀{x} → holes (X x) ∅
    HLam1  : ∀{x e H} → holes e H → holes (·λ x e) H
    HLam2  : ∀{x e τ H} → holes e H → holes (·λ x ·[ τ ] e) H
    HAp    : ∀{e1 e2 H1 H2} → holes e1 H1 → holes e2 H2 → holes (e1 ∘ e2) (H1 ∪ H2)
    HInl   : ∀{e H} → holes e H → holes (inl e) H
    HInr   : ∀{e H} → holes e H → holes (inr e) H
    HCase  : ∀{e x e1 y e2 H H1 H2} → holes e H → holes e1 H1 → holes e2 H2 → holes (case e x e1 y e2) (H ∪ (H1 ∪ H2))
    HPair  : ∀{e1 e2 H1 H2} → holes e1 H1 → holes e2 H2 → holes ⟨ e1 , e2 ⟩ (H1 ∪ H2)
    HFst   : ∀{e H} → holes e H → holes (fst e) H
    HSnd   : ∀{e H} → holes e H → holes (snd e) H
    HEHole : ∀{u} → holes (⦇-⦈[ u ]) (■ (u , <>))
    HNEHole : ∀{e u H} → holes e H → holes (⦇⌜ e ⌟⦈[ u ]) (H ,, (u , <>))

  -- the above judgement has mode (∀,∃). this doesn't prove uniqueness; any
  -- context that extends the one computed here will be indistinguishable
  -- but we'll treat this one as canonical
  find-holes : (e : hexp) → Σ[ H ∈ ⊤ ctx ](holes e H)
  find-holes (N n) = ∅ , HNum
  find-holes (e1 ·+ e2) with find-holes e1 | find-holes e2
  ... | (h1 , d1) | (h2 , d2)  = (h1 ∪ h2 ) , (HPlus d1 d2)
  find-holes (e ·: x) with find-holes e
  ... | (h , d) = h , (HAsc d)
  find-holes (X x) = ∅ , HVar
  find-holes (·λ x e) with find-holes e
  ... | (h , d) = h , HLam1 d
  find-holes (·λ x ·[ x₁ ] e) with find-holes e
  ... | (h , d) = h , HLam2 d
  find-holes (e1 ∘ e2) with find-holes e1 | find-holes e2
  ... | (h1 , d1) | (h2 , d2)  = (h1 ∪ h2 ) , (HAp d1 d2)
  find-holes ⦇-⦈[ x ] = (■ (x , <>)) , HEHole
  find-holes ⦇⌜ e ⌟⦈[ x ] with find-holes e
  ... | (h , d) = h ,, (x , <>) , HNEHole d
  find-holes (inl e) with find-holes e
  ... | (h , d) = h , HInl d
  find-holes (inr e) with find-holes e
  ... | (h , d) = h , HInr d
  find-holes (case e x e₁ x₁ e₂) with find-holes e | find-holes e₁ | find-holes e₂
  ... | (h , d) | (h1 , d1) | (h2 , d2) = (h ∪ (h1 ∪ h2)) , HCase d d1 d2
  find-holes ⟨ e , e₁ ⟩ with find-holes e | find-holes e₁
  ... | (h , d) | (h1 , d1) = h ∪ h1 , HPair d d1
  find-holes (fst e) with find-holes e
  ... | (h , d) = h , HFst d
  find-holes (snd e) with find-holes e
  ... | (h , d) = h , HSnd d

  -- if a hole name is new then it's apart from the collection of hole
  -- names
  lem-apart-new : ∀{e H u} → holes e H → hole-name-new e u → u # H
  lem-apart-new HNum x = refl
  lem-apart-new (HPlus {H1 = H1} {H2 = H2} h h₁) (HNPlus hn hn₁) = apart-parts H1 H2 _ (lem-apart-new h hn) (lem-apart-new h₁ hn₁)
  lem-apart-new (HAsc h) (HNAsc hn) = lem-apart-new h hn
  lem-apart-new HVar HNVar = refl
  lem-apart-new (HLam1 h) (HNLam1 hn) = lem-apart-new h hn
  lem-apart-new (HLam2 h) (HNLam2 hn) = lem-apart-new h hn
  lem-apart-new (HAp {H1 = H1} {H2 = H2} h h₁) (HNAp hn hn₁) = apart-parts H1 H2 _ (lem-apart-new h hn) (lem-apart-new h₁ hn₁)
  lem-apart-new HEHole (HNHole x) = apart-singleton (flip x)
  lem-apart-new (HNEHole {u = u'} {H = H} h) (HNNEHole  {u = u}  x hn) = apart-parts (■ (u' , <>)) H u (apart-singleton (flip x)) (lem-apart-new h hn)
  lem-apart-new (HInl h) (HNInl hn) = lem-apart-new h hn
  lem-apart-new (HInr h) (HNInr hn) = lem-apart-new h hn
  lem-apart-new (HCase {H = H} {H1 = H1} {H2 = H2} h h₁ h₂) (HNCase {u = u'} hn hn₁ hn₂) = apart-parts H (H1 ∪ H2) u' (lem-apart-new h hn) (apart-parts H1 H2 u' (lem-apart-new h₁ hn₁) (lem-apart-new h₂ hn₂))
  lem-apart-new (HPair {H1 = H1} {H2 = H2} h h₁) (HNPair {u = u} hn hn₁) = apart-parts H1 H2 u (lem-apart-new h hn) (lem-apart-new h₁ hn₁)
  lem-apart-new (HFst h) (HNFst hn) = lem-apart-new h hn
  lem-apart-new (HSnd h) (HNSnd hn) = lem-apart-new h hn

  -- if the holes of two expressions are disjoint, so are their collections
  -- of hole names
  holes-disjoint-disjoint : ∀{e1 e2 H1 H2} →
                            holes e1 H1 →
                            holes e2 H2 →
                            holes-disjoint e1 e2 →
                            H1 ## H2
  holes-disjoint-disjoint HNum he2 HDNum = empty-disj _
  holes-disjoint-disjoint (HPlus he1 he2) he3 (HDPlus hd hd₁) = disjoint-parts (holes-disjoint-disjoint he1 he3 hd) (holes-disjoint-disjoint he2 he3 hd₁)
  holes-disjoint-disjoint (HAsc he1) he2 (HDAsc hd) = holes-disjoint-disjoint he1 he2 hd
  holes-disjoint-disjoint HVar he2 HDVar = empty-disj _
  holes-disjoint-disjoint (HLam1 he1) he2 (HDLam1 hd) = holes-disjoint-disjoint he1 he2 hd
  holes-disjoint-disjoint (HLam2 he1) he2 (HDLam2 hd) = holes-disjoint-disjoint he1 he2 hd
  holes-disjoint-disjoint (HAp he1 he2) he3 (HDAp hd hd₁) = disjoint-parts (holes-disjoint-disjoint he1 he3 hd) (holes-disjoint-disjoint he2 he3 hd₁)
  holes-disjoint-disjoint HEHole he2 (HDHole x) = lem-apart-sing-disj (lem-apart-new he2 x)
  holes-disjoint-disjoint (HNEHole he1) he2 (HDNEHole x hd) = disjoint-parts (lem-apart-sing-disj (lem-apart-new he2 x)) (holes-disjoint-disjoint he1 he2 hd)
  holes-disjoint-disjoint (HInl he1) he2 (HDInl hd) = holes-disjoint-disjoint he1 he2 hd
  holes-disjoint-disjoint (HInr he1) he2 (HDInr hd) = holes-disjoint-disjoint he1 he2 hd
  holes-disjoint-disjoint (HCase he1 he3 he4) he2 (HDCase hd hd₁ hd₂) = disjoint-parts (holes-disjoint-disjoint he1 he2 hd) (disjoint-parts (holes-disjoint-disjoint he3 he2 hd₁) (holes-disjoint-disjoint he4 he2 hd₂))
  holes-disjoint-disjoint (HPair he1 he3) he2 (HDPair hd hd₁) = disjoint-parts (holes-disjoint-disjoint he1 he2 hd) (holes-disjoint-disjoint he3 he2 hd₁)
  holes-disjoint-disjoint (HFst he1) he2 (HDFst hd) = holes-disjoint-disjoint he1 he2 hd
  holes-disjoint-disjoint (HSnd he1) he2 (HDSnd hd) = holes-disjoint-disjoint he1 he2 hd

  -- the holes of an expression have the same domain as the context
  -- produced during expansion; that is, we don't add anything we don't
  -- find in the term during expansion.
  mutual
    holes-delta-ana : ∀{Γ H e τ d τ' Δ} →
                      holes e H →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      dom-eq Δ H
    holes-delta-ana (HLam1 h) (EALam x₁ x₂ exp) = holes-delta-ana h exp
    holes-delta-ana h (EASubsume x x₁ x₂ x₃) = holes-delta-synth h x₂
    holes-delta-ana (HEHole {u = u}) EAEHole = dom-single u
    holes-delta-ana (HNEHole {u = u} h) (EANEHole x x₁) = dom-union (lem-apart-sing-disj (lem-apart-new h (elab-disjoint-new-synth x₁ x))) (dom-single u) (holes-delta-synth h x₁)
    holes-delta-ana (HInl h) (EAInl x x₁) = holes-delta-ana h x₁
    holes-delta-ana (HInr h) (EAInr x x₁) = holes-delta-ana h x₁
    holes-delta-ana (HCase h h₁ h₂) (EACase {Δ = Δ} x x₁ x₂ x₃ x₄ x₅ _ _ x₆ x₇ x₈ x₉) = dom-union (##-comm (disjoint-parts (##-comm (holes-disjoint-disjoint h h₁ x)) (##-comm (holes-disjoint-disjoint h h₂ x₁)))) (holes-delta-synth h x₆) (dom-union (holes-disjoint-disjoint h₁ h₂ x₂) (holes-delta-ana h₁ x₈) (holes-delta-ana h₂ x₉))

    holes-delta-synth : ∀{Γ H e τ d Δ} →
                        holes e H →
                        Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                        dom-eq Δ H
    holes-delta-synth HNum ESNum = dom-∅
    holes-delta-synth (HPlus h h₁) (ESPlus x apt x₁ x₂) = dom-union (holes-disjoint-disjoint h h₁ x) (holes-delta-ana h x₁) (holes-delta-ana h₁ x₂)
    holes-delta-synth (HAsc h) (ESAsc x) = holes-delta-ana h x
    holes-delta-synth HVar (ESVar x₁) = dom-∅
    holes-delta-synth (HLam2 h) (ESLam x₁ exp) = holes-delta-synth h exp
    holes-delta-synth (HAp h h₁) (ESAp x x₁ x₂ x₃ x₄ x₅) = dom-union (holes-disjoint-disjoint h h₁ x) (holes-delta-ana h x₄) (holes-delta-ana h₁ x₅)
    holes-delta-synth (HEHole {u = u}) ESEHole = dom-single u
    holes-delta-synth (HNEHole {u = u} h) (ESNEHole x exp) = dom-union (lem-apart-sing-disj (lem-apart-new h (elab-disjoint-new-synth exp x))) (dom-single u) (holes-delta-synth h exp)
    holes-delta-synth (HPair h h₁) (ESPair x x₁ exp exp₁) = dom-union (holes-disjoint-disjoint h h₁ x) (holes-delta-synth h exp) (holes-delta-synth h₁ exp₁)
    holes-delta-synth (HLam1 hn) ()
    holes-delta-synth (HInl hn) ()
    holes-delta-synth (HInr hn) ()
    holes-delta-synth (HCase hn hn₁ hn₂) ()
    holes-delta-synth (HFst hn) (ESFst x x₁ x₂) = holes-delta-ana hn x₂
    holes-delta-synth (HSnd hn) (ESSnd x x₁ x₂) = holes-delta-ana hn x₂
  -- this is one of the main results of this file:
  --
  -- if you elaborate two hole-disjoint expressions analytically, the Δs
  -- produced are disjoint.
  --
  -- the proof technique here is explcitly *not* structurally inductive on the
  -- expansion judgement, because that approach relies on weakening of
  -- expansion, which is false because of the substitution contexts. giving
  -- expansion weakning would take away unicity, so we avoid the whole
  -- question.
  elab-ana-disjoint : ∀{e1 e2 τ1 τ2 e1' e2' τ1' τ2' Γ1 Γ2 Δ1 Δ2} →
                      holes-disjoint e1 e2 →
                      Γ1 ⊢ e1 ⇐ τ1 ~> e1' :: τ1' ⊣ Δ1 →
                      Γ2 ⊢ e2 ⇐ τ2 ~> e2' :: τ2' ⊣ Δ2 →
                      Δ1 ## Δ2
  elab-ana-disjoint {e1} {e2} hd ana1 ana2
    with find-holes e1 | find-holes e2
  ... | (_ , he1) | (_ , he2) = dom-eq-disj (holes-disjoint-disjoint he1 he2 hd)
                                            (holes-delta-ana he1 ana1)
                                            (holes-delta-ana he2 ana2)

  elab-synth-disjoint : ∀{e1 e2 τ1 τ2 e1' e2' Γ1 Γ2 Δ1 Δ2} →
                        holes-disjoint e1 e2 →
                        Γ1 ⊢ e1 ⇒ τ1 ~> e1' ⊣ Δ1 →
                        Γ2 ⊢ e2 ⇒ τ2 ~> e2' ⊣ Δ2 →
                        Δ1 ## Δ2
  elab-synth-disjoint {e1} {e2} hd synth1 synth2
    with find-holes e1 | find-holes e2
  ... | (_ , he1) | (_ , he2) = dom-eq-disj (holes-disjoint-disjoint he1 he2 hd)
                                            (holes-delta-synth he1 synth1)
                                            (holes-delta-synth he2 synth2)

  elab-synth-ana-disjoint : ∀{e1 e2 τ1 τ2 e1' e2' τ2' Γ1 Γ2 Δ1 Δ2} →
                            holes-disjoint e1 e2 →
                            Γ1 ⊢ e1 ⇒ τ1 ~> e1' ⊣ Δ1 →
                            Γ2 ⊢ e2 ⇐ τ2 ~> e2' :: τ2' ⊣ Δ2 →
                            Δ1 ## Δ2
  elab-synth-ana-disjoint {e1} {e2} hd synth ana
    with find-holes e1 | find-holes e2
  ... | (_ , he1) | (_ , he2) = dom-eq-disj (holes-disjoint-disjoint he1 he2 hd)
                                            (holes-delta-synth he1 synth)
                                            (holes-delta-ana he2 ana)

ext: agda

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂  )
open import FRP.LTL.Time.Interval using ( _⊑_ ; _~_ ; _⌢_∵_ )
open import FRP.LTL.ISet.Core using ( ISet ; [_] ; _,_ ; M⟦_⟧ ; splitM⟦_⟧ ; subsumM⟦_⟧ )

module FRP.LTL.ISet.Sum where

_∨_ : ISet → ISet → ISet
A ∨ B = [ (λ i → M⟦ A ⟧ i ⊎ M⟦ B ⟧ i) , split , subsum ] where

  split : ∀ i j i~j →
    (M⟦ A ⟧ (i ⌢ j ∵ i~j) ⊎ M⟦ B ⟧ (i ⌢ j ∵ i~j)) →
      ((M⟦ A ⟧ i ⊎ M⟦ B ⟧ i) × (M⟦ A ⟧ j ⊎ M⟦ B ⟧ j))
  split i j i~j (inj₁ σ) with splitM⟦ A ⟧ i j i~j σ
  split i j i~j (inj₁ σ) | (σ₁ , σ₂) = (inj₁ σ₁ , inj₁ σ₂)
  split i j i~j (inj₂ τ) with splitM⟦ B ⟧ i j i~j τ
  split i j i~j (inj₂ τ) | (τ₁ , τ₂) = (inj₂ τ₁ , inj₂ τ₂)

  subsum : ∀ i j → (i ⊑ j) → (M⟦ A ⟧ j ⊎ M⟦ B ⟧ j) → (M⟦ A ⟧ i ⊎ M⟦ B ⟧ i)
  subsum i j i⊑j (inj₁ σ) = inj₁ (subsumM⟦ A ⟧ i j i⊑j σ)
  subsum i j i⊑j (inj₂ τ) = inj₂ (subsumM⟦ B ⟧ i j i⊑j τ)

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty AVL trees, where equality for keys is propositional equality
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; IsStrictTotalOrder; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

module Data.AVL.NonEmpty.Propositional
  {k r} {Key : Set k} {_<_ : Rel Key r}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

open import Level

private strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder}
open import Data.AVL.Value (StrictTotalOrder.Eq.setoid strictTotalOrder)
import Data.AVL.NonEmpty strictTotalOrder as AVL⁺

Tree⁺ : ∀ {v} (V : Key → Set v) → Set (k ⊔ v ⊔ r)
Tree⁺ V = AVL⁺.Tree⁺ λ where
  .Value.family          → V
  .Value.respects refl t → t

open AVL⁺ hiding (Tree⁺) public


text:
module Vec where

import Nat
import Fin

open Nat hiding (_==_; _<_)
open Fin

data Nil : Set where
  vnil : Nil

data Cons (A As : Set) : Set where
  vcons : A -> As -> Cons A As

mutual
  Vec' : Nat -> Set -> Set
  Vec' zero    A = Nil
  Vec' (suc n) A = Cons A (Vec n A)

  data Vec (n : Nat)(A : Set) : Set where
    vec : Vec' n A -> Vec n A

ε : {A : Set} -> Vec zero A
ε = vec vnil

_∷_ : {A : Set}{n : Nat} -> A -> Vec n A -> Vec (suc n) A
x ∷ xs = vec (vcons x xs)

_!_ : {n : Nat}{A : Set} -> Vec n A -> Fin n -> A
_!_ {zero}   _                 (fin ())
_!_ {suc n} (vec (vcons x xs)) (fin fz)     = x
_!_ {suc n} (vec (vcons x xs)) (fin (fs i)) = xs ! i

map : {n : Nat}{A B : Set} -> (A -> B) -> Vec n A -> Vec n B
map {zero}  f (vec vnil)         = ε
map {suc n} f (vec (vcons x xs)) = f x ∷ map f xs

fzeroToN-1 : (n : Nat) -> Vec n (Fin n)
fzeroToN-1 zero    = ε
fzeroToN-1 (suc n) = fzero ∷ map fsuc (fzeroToN-1 n)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-11-09, issue 1710 reported by vejkse
-- {-# OPTIONS -v tc.with:20 #-}

record wrap (A : Set) : Set where
  field
    out : A
open wrap public

record MapsFrom (A : Set) : Set₁ where
  field
    cod : Set
    map : A → cod
open MapsFrom public

wrapped : (A : Set) → MapsFrom A
cod (wrapped A) = wrap A
out (map (wrapped A) a) with a
... | _ = a

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Text.Lex where

open import Prelude

record TokenDFA {s} (A : Set) (Tok : Set) : Set (lsuc s) where
  field
    State   : Set s
    initial : State
    accept  : State → Maybe Tok
    consume : A → State → Maybe State

instance
  FunctorTokenDFA : ∀ {s} {A : Set} → Functor (TokenDFA {s = s} A)
  TokenDFA.State   (fmap {{FunctorTokenDFA}} f dfa) = TokenDFA.State dfa
  TokenDFA.initial (fmap {{FunctorTokenDFA}} f dfa) = TokenDFA.initial dfa
  TokenDFA.accept  (fmap {{FunctorTokenDFA}} f dfa) s = f <$> TokenDFA.accept dfa s
  TokenDFA.consume (fmap {{FunctorTokenDFA}} f dfa) = TokenDFA.consume dfa

keywordToken : {A : Set} {{EqA : Eq A}} → List A → TokenDFA A ⊤
TokenDFA.State   (keywordToken {A = A} kw)    = List A
TokenDFA.initial (keywordToken kw)            = kw
TokenDFA.accept  (keywordToken kw) []         = just _
TokenDFA.accept  (keywordToken kw) (_ ∷ _)    = nothing
TokenDFA.consume (keywordToken kw) _ []       = nothing
TokenDFA.consume (keywordToken kw) y (x ∷ xs) = ifYes (x == y) then just xs else nothing

matchToken : ∀ {A : Set} (p : A → Bool) → TokenDFA A (List (Σ A (IsTrue ∘ p)))
TokenDFA.State (matchToken {A = A} p) = List (Σ A (IsTrue ∘ p))
TokenDFA.initial (matchToken _)       = []
TokenDFA.accept  (matchToken _) xs    = just (reverse xs)
TokenDFA.consume (matchToken p) x xs  = if′ p x then just ((x , it) ∷ xs) else nothing

natToken : TokenDFA Char Nat
natToken = pNat <$> matchToken isDigit
  where pNat = foldl (λ { n (d , _) → 10 * n + (charToNat d - charToNat '0') }) 0

identToken : ∀ {A : Set} → (A → Bool) → (A → Bool) → TokenDFA A (List A)
TokenDFA.State   (identToken {A = A} _ _) = Maybe (List A)
TokenDFA.initial (identToken _ _) = nothing
TokenDFA.accept  (identToken _ _) = fmap reverse
TokenDFA.consume (identToken first _) x nothing   = if first x then just (just [ x ])    else nothing
TokenDFA.consume (identToken _ then)  x (just xs) = if then  x then just (just (x ∷ xs)) else nothing

module _ {s : Level} {A Tok : Set} where
  private
    DFA = TokenDFA {s = s} A Tok
    open TokenDFA

    init : DFA → Σ DFA State
    init d = d , initial d

    feed : A → Σ DFA State → Either DFA (Σ DFA State)
    feed x (d , s) = maybe (left d) (right ∘ _,_ d) (consume d x s)

    accepts : List (Σ DFA State) → List Tok
    accepts = concatMap (λ { (d , s) → maybe [] [_] (accept d s) })

    tokenize-loop : List DFA → List (Σ DFA State) → List A → List Tok
    tokenize-loop idle active [] =
      case accepts active of λ where
        []      → []  -- not quite right if there are active DFAs
        (t ∷ _) → [ t ]
    tokenize-loop idle [] (x ∷ xs) =
      flip uncurry (partitionMap (feed x) (map init idle)) λ where
        idle₁ []      → []
        idle₁ active₁ → tokenize-loop idle₁ active₁ xs
    tokenize-loop idle active (x ∷ xs) =
      flip uncurry (partitionMap (feed x) active) λ where
        idle₁ [] →
          case accepts active of λ where
            []      → []
            (t ∷ _) →
              flip uncurry (partitionMap (feed x) (map init (idle ++ idle₁))) λ where
                _ []          → t ∷ []
                idle₂ active₂ → t List.∷ tokenize-loop idle₂ active₂ xs
        idle₁ active₁ → tokenize-loop (idle ++ idle₁) active₁ xs

  tokenize : List (TokenDFA {s = s} A Tok) → List A → List Tok
  tokenize dfas xs = tokenize-loop dfas [] xs

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module Common.Equality where

open import Common.Level

infix 4 _≡_

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

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

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

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

sym : ∀ {a}{A : Set a}{x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {a}{A : Set a}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Int.Core where

open import Agda.Builtin.Int public
  renaming (Int to ℤ)
  using (pos; negsuc)
open import Agda.Builtin.TrustMe
open import Classes
open import Core
open import Data.Nat.Core
  renaming (module Props to ℕP)
  using (ℕ; ℕ-Number; ℕ-Plus; ℕ-Times; suc; zero)

_-ℕ_ : ℕ → ℕ → ℤ
x -ℕ zero = pos x
zero -ℕ suc y = negsuc y
suc x -ℕ suc y = x -ℕ y

infixl 6 _-ℕ_

instance
  ℤ-Negative : Negative ℤ
  ℤ-Negative =
    record {
      Constraint = λ _ → ⊤;
      fromNeg = λ x → zero -ℕ x
    }

  ℤ-Number : Number ℤ
  ℤ-Number =
    record {
      Constraint = λ _ → ⊤;
      fromNat = λ x → pos x
    }

  ℤ,≡ : Equiv ℤ
  ℤ,≡ = PropEq ℤ

instance
  ℤ-Plus : Plus ℤ
  ℤ-Plus = record { _+_ = _+ℤ_ }
    where
    _+ℤ_ : ℤ → ℤ → ℤ
    pos x +ℤ pos y = pos (x + y)
    pos x +ℤ negsuc y = x -ℕ suc y
    negsuc x +ℤ pos y = y -ℕ suc x
    negsuc x +ℤ negsuc y = negsuc (suc (x + y))

  ℤ-Times : Times ℤ
  ℤ-Times = record { _*_ = _*ℤ_ }
    where
    _*ℤ_ : ℤ → ℤ → ℤ
    pos x *ℤ pos y = pos (x * y)
    pos zero *ℤ negsuc y = 0
    pos (suc x) *ℤ negsuc y = negsuc (y + x * suc y)
    negsuc x *ℤ pos zero = 0
    negsuc x *ℤ pos (suc y) = negsuc (y + x * suc y)
    negsuc x *ℤ negsuc y = pos (suc x * suc y)

neg : ℤ → ℤ
neg = _*_ -1

_-_ : ℤ → ℤ → ℤ
x - y = x + neg y

infixl 6 _-_

module Props where
  open module MyEquiv {A : Set} = Equiv (PropEq A)

  private
    _!+!_ = cong2 (the (ℤ → ℤ → ℤ) _+_)
    _!-ℕ!_ = cong2 _-ℕ_
    _!*!_ = cong2 (the (ℤ → ℤ → ℤ) _*_)

    R = λ {A} (x : A) → refl {x = x}

    infixl 6 _!+!_ _!-ℕ!_
    infixl 7 _!*!_

  sub-neg-zero : ∀ x → x -ℕ zero ≈ pos x
  sub-neg-zero _ = refl

  +-left-id : ∀ x → 0 + x ≈ x
  +-left-id (pos n) = refl
  +-left-id (negsuc n) = refl

  +-right-id : ∀ x → x + 0 ≈ x
  +-right-id (pos x) = cong pos (ℕP.+-right-id x)
  +-right-id (negsuc x) = refl

  +-comm : ∀ x y → x + y ≈ y + x
  +-comm (pos x) (pos y) = cong pos (ℕP.+-comm x y)
  +-comm (pos x) (negsuc y) = refl
  +-comm (negsuc x) (pos y) = refl
  +-comm (negsuc x) (negsuc y) = cong negsuc (cong suc (ℕP.+-comm x y))

  sub-sum-right : ∀ x y z → x -ℕ suc (y + z) ≈ negsuc y + (x -ℕ z)
  sub-sum-right x zero zero = refl
  sub-sum-right zero zero (suc z) = refl
  sub-sum-right (suc x) zero (suc z) = sub-sum-right x zero z
  sub-sum-right x (suc y) zero = R x !-ℕ! cong suc (cong suc (ℕP.+-right-id y))
  sub-sum-right zero (suc y) (suc z) = cong negsuc (cong suc (ℕP.+-suc-assoc y z))
  sub-sum-right (suc x) (suc y) (suc z) =
    begin
      x -ℕ suc (y + suc z)      ≈[ R x !-ℕ! cong suc (ℕP.+-suc-assoc y z) ]
      x -ℕ suc (suc y + z)      ≈[ sub-sum-right x (suc y) z ]
      negsuc (suc y) + (x -ℕ z)
    qed

  sub-sum-left : ∀ x y z → (x + y) -ℕ z ≈ pos x + (y -ℕ z)
  sub-sum-left zero y z = sym (+-left-id (y -ℕ z))
  sub-sum-left (suc x) y zero = refl
  sub-sum-left (suc x) zero (suc z) = ℕP.+-right-id x !-ℕ! R z
  sub-sum-left (suc x) (suc y) (suc z) =
    begin
      (x + suc y) -ℕ z       ≈[ ℕP.+-suc-assoc x y !-ℕ! R z ]
      suc (x + y) -ℕ z       ≈[ sub-sum-left (suc x) y z ]
      pos (suc x) + (y -ℕ z)
    qed

  +-assoc : ∀ x y z → (x + y) + z ≈ x + (y + z)
  +-assoc (pos x) (pos y) (pos z) = cong pos (ℕP.+-assoc x _ _)
  +-assoc (pos x) (pos y) (negsuc z) = sub-sum-left x y (suc z)
  +-assoc (pos x) (negsuc y) (pos z) =
    begin
      (x -ℕ suc y) + pos z ≈[ +-comm (x -ℕ suc y) (pos z) ]
      pos z + (x -ℕ suc y) ≈[ sym (sub-sum-left z x (suc y)) ]
      (z + x) -ℕ suc y     ≈[ ℕP.+-comm z x !-ℕ! R (suc y) ]
      (x + z) -ℕ suc y     ≈[ sub-sum-left x z (suc y) ]
      pos x + (z -ℕ suc y)
    qed
  +-assoc (pos x) (negsuc y) (negsuc z) =
    begin
      x -ℕ suc y + negsuc z   ≈[ +-comm (x -ℕ suc y) (negsuc z) ]
      negsuc z + (x -ℕ suc y) ≈[ sym (sub-sum-right x z (suc y)) ]
      x -ℕ (suc z + suc y)    ≈[ R x !-ℕ! ℕP.+-comm (suc z) (suc y) ]
      x -ℕ (suc y + suc z)    ≈[ R x !-ℕ! cong suc (ℕP.+-suc-assoc y z) ]
      x -ℕ suc (suc (y + z))
    qed
  +-assoc (negsuc x) (pos y) (pos z) =
    begin
      (y -ℕ suc x) + pos z ≈[ +-comm (y -ℕ suc x) (pos z) ]
      pos z + (y -ℕ suc x) ≈[ sym (sub-sum-left z y (suc x)) ]
      (z + y) -ℕ suc x     ≈[ ℕP.+-comm z y !-ℕ! R (suc x) ]
      (y + z) -ℕ suc x
    qed
  +-assoc (negsuc x) (pos y) (negsuc z) =
    begin
      y -ℕ suc x + negsuc z   ≈[ +-comm (y -ℕ suc x) (negsuc z) ]
      negsuc z + (y -ℕ suc x) ≈[ sym (sub-sum-right y z (suc x)) ]
      y -ℕ (suc z + suc x)    ≈[ R y !-ℕ! ℕP.+-comm (suc z) (suc x) ]
      y -ℕ (suc x + suc z)    ≈[ sub-sum-right y x (suc z) ]
      negsuc x + (y -ℕ suc z)
    qed
  +-assoc (negsuc x) (negsuc y) (pos zero) = refl
  +-assoc (negsuc x) (negsuc y) (pos (suc z)) = sub-sum-right z x y
  +-assoc (negsuc x) (negsuc y) (negsuc z) =
    cong negsuc $ cong suc $
    begin
      suc ((x + y) + z) ≈[ cong suc (ℕP.+-assoc x y z) ]
      suc (x + (y + z)) ≈[ sym (ℕP.+-suc-assoc x (y + z)) ]
      x + (suc (y + z))
    qed

  *-left-id : ∀ x → 1 * x ≈ x
  *-left-id (pos x) = cong pos (ℕP.+-right-id x)
  *-left-id (negsuc x) = cong negsuc (ℕP.+-right-id x)

  *-right-id : ∀ x → x * 1 ≈ x
  *-right-id (pos x) = cong pos (ℕP.*-right-id x)
  *-right-id (negsuc x) =
    cong negsuc (trans (ℕP.*-comm x 1) (ℕP.+-right-id x))

  *-assoc : ∀ x y z → (x * y) * z ≈ x * (y * z)
  *-assoc (pos x) (pos y) (pos z) = cong pos (ℕP.*-assoc x y z)
  *-assoc (pos zero) (pos zero) (negsuc z) = refl
  *-assoc (pos zero) (pos (suc y)) (negsuc z) = refl
  *-assoc (pos (suc x)) (pos zero) (negsuc z) =
    begin
      pos (x * 0) * negsuc z ≈[ cong pos (ℕP.*-right-zero x) !*! R (negsuc z) ]
      pos 0 * negsuc z       ≈[ cong pos (sym (ℕP.*-right-zero x)) ]
      pos (x * 0)
    qed
  *-assoc (pos (suc x)) (pos (suc y)) (negsuc z) =
    cong negsuc $ ℕP.suc-inj $
    ℕP.*-assoc (suc x) (suc y) (suc z)
  *-assoc (pos zero) (negsuc y) (pos zero) = refl
  *-assoc (pos zero) (negsuc y) (pos (suc z)) = refl
  *-assoc (pos (suc x)) (negsuc y) (pos zero) = cong pos (sym (ℕP.*-right-zero x))
  *-assoc (pos (suc x)) (negsuc y) (pos (suc z)) =
    cong negsuc $ ℕP.suc-inj $
    ℕP.*-assoc (suc x) (suc y) (suc z)
  *-assoc (pos zero) (negsuc y) (negsuc z) = refl
  *-assoc (pos (suc x)) (negsuc y) (negsuc z) = cong pos (ℕP.*-assoc (suc x) (suc y) (suc z))
  *-assoc (negsuc x) (pos zero) (pos z) = refl
  *-assoc (negsuc x) (pos (suc y)) (pos zero) = R (negsuc x) !*! cong pos (sym (ℕP.*-right-zero y))
  *-assoc (negsuc x) (pos (suc y)) (pos (suc z)) =
    cong negsuc $ ℕP.suc-inj $
    ℕP.*-assoc (suc x) (suc y) (suc z)
  *-assoc (negsuc x) (pos zero) (negsuc z) = refl
  *-assoc (negsuc x) (pos (suc y)) (negsuc z) = cong pos (ℕP.*-assoc (suc x) (suc y) (suc z))
  *-assoc (negsuc x) (negsuc y) (pos zero) = cong pos (ℕP.*-right-zero (y + x * suc y))
  *-assoc (negsuc x) (negsuc y) (pos (suc z)) = cong pos (ℕP.*-assoc (suc x) (suc y) (suc z))
  *-assoc (negsuc x) (negsuc y) (negsuc z) =
    cong negsuc $ ℕP.suc-inj $
    ℕP.*-assoc (suc x) (suc y) (suc z)

  *-comm : ∀ x y → x * y ≈ y * x
  *-comm (pos x) (pos y) = cong pos (ℕP.*-comm x y)
  *-comm (pos zero) (negsuc y) = refl
  *-comm (pos (suc x)) (negsuc y) = cong negsuc (ℕP.suc-inj (ℕP.*-comm (suc x) (suc y)))
  *-comm (negsuc x) (pos zero) = refl
  *-comm (negsuc x) (pos (suc y)) = cong negsuc (ℕP.suc-inj (ℕP.*-comm (suc x) (suc y)))
  *-comm (negsuc x) (negsuc y) = cong pos (ℕP.*-comm (suc x) (suc y))

  *-left-zero : ∀ x → 0 * x ≈ 0
  *-left-zero (pos x) = refl
  *-left-zero (negsuc x) = refl

  neg-invol : ∀ x → neg (neg x) ≈ x
  neg-invol x =
    begin
      -1 * (-1 * x) ≈[ sym (*-assoc -1 -1 x) ]
      1 * x         ≈[ *-left-id x ]
      x
    qed

  *-right-zero : ∀ x → x * 0 ≈ 0
  *-right-zero x = trans (*-comm x 0) (*-left-zero x)

  *-suc-dist : ∀ x y → pos (suc x) * y ≈ y + pos x * y
  *-suc-dist x (pos y) = refl
  *-suc-dist zero (negsuc y) = cong negsuc (ℕP.+-right-id y)
  *-suc-dist (suc x) (negsuc y) = sub-sum-right 0 y (suc (y + x * suc y))

  *-+-left-dist-ℕ : ∀ x a b → pos x * (a + b) ≈ pos x * a + pos x * b
  *-+-left-dist-ℕ zero a b =
    begin
      0 * (a + b)   ≈[ *-left-zero (a + b) ]
      0             ≈[ sym (*-left-zero a) !+! sym (*-left-zero b) ]
      0 * a + 0 * b
    qed
  *-+-left-dist-ℕ (suc x) a b =
    begin
      pos (suc x) * (a + b)             ≈[ *-suc-dist x (a + b) ]
      (a + b) + pos x * (a + b)         ≈[ R (a + b) !+! *-+-left-dist-ℕ x a b ]
      (a + b) + (pos x * a + pos x * b) ≈[ +-assoc a b (pos x * a + pos x * b) ]
      a + (b + (pos x * a + pos x * b)) ≈[ R a !+! sym (+-assoc b (pos x * a) (pos x * b)) ]
      a + ((b + pos x * a) + pos x * b) ≈[ R a !+! (+-comm b (pos x * a) !+! R (pos x * b)) ]
      a + ((pos x * a + b) + pos x * b) ≈[ R a !+! +-assoc (pos x * a) b (pos x * b) ]
      a + (pos x * a + (b + pos x * b)) ≈[ sym (+-assoc a (pos x * a) (b + pos x * b)) ]
      (a + pos x * a) + (b + pos x * b) ≈[ sym (*-suc-dist x a) !+! sym (*-suc-dist x b) ]
      pos (suc x) * a + pos (suc x) * b
    qed

  *-+-left-dist : ∀ x a b → x * (a + b) ≈ x * a + x * b
  *-+-left-dist (pos x) a b = *-+-left-dist-ℕ x a b
  *-+-left-dist (negsuc x) a b =
    begin
      negsuc x * (a + b)                              ≈[ sym (neg-invol (negsuc x)) !*! R (a + b) ]
      -1 * (pos (suc (x + zero))) * (a + b)           ≈[ cong neg (cong pos (ℕP.+-right-id (suc x))) !*! R (a + b) ]
      -1 * (pos (suc x)) * (a + b)                    ≈[ *-assoc -1 (pos (suc x)) (a + b) ]
      -1 * (pos (suc x) * (a + b))                    ≈[ R -1 !*! *-+-left-dist-ℕ (suc x) a b ]
      -1 * (pos (suc x) * a + pos (suc x) * b)        ≈[ -1-left-dist (pos (suc x) * a) (pos (suc x) * b) ]
      -1 * (pos (suc x) * a) + -1 * (pos (suc x) * b) ≈[ sym (*-assoc -1 (pos (suc x)) a) !+! sym (*-assoc -1 (pos (suc x)) b) ]
      -1 * pos (suc x) * a + -1 * pos (suc x) * b     ≈[ R -1 !*! cong pos (cong suc (sym (ℕP.+-right-id x))) !*! R a !+!
                                                         R -1 !*! cong pos (cong suc (sym (ℕP.+-right-id x))) !*! R b ]
      -1 * pos (suc (x + 0)) * a + -1 * pos (suc (x + 0)) * b  ≈[ neg-invol (negsuc x) !*! R a !+! neg-invol (negsuc x) !*! R b ]
      negsuc x * a + negsuc x * b
    qed

    where
    -- TODO
    -1-left-dist : ∀ x y → neg (x + y) ≈ neg x + neg y
    -1-left-dist _ _ = primTrustMe

  *-+-right-dist : ∀ a b x → (a + b) * x ≈ a * x + b * x
  *-+-right-dist a b x =
    begin
      (a + b) * x   ≈[ *-comm (a + b) x ]
      x * (a + b)   ≈[ *-+-left-dist x a b ]
      x * a + x * b ≈[ (*-comm x a) !+! (*-comm x b) ]
      a * x + b * x
    qed

  +-left-inv : ∀ x → neg x + x ≈ 0
  +-left-inv x =
    begin
      -1 * x + x     ≈[ R (-1 * x) !+! sym (*-left-id x) ]
      -1 * x + 1 * x ≈[ sym (*-+-right-dist -1 1 x) ]
      0 * x          ≈[ *-left-zero x ]
      0
    qed

  +-right-inv : ∀ x → x + neg x ≈ 0
  +-right-inv x =
    begin
      x + neg x           ≈[ sym (neg-invol x) !+! R (neg x) ]
      neg (neg x) + neg x ≈[ +-left-inv (neg x) ]
      0
    qed

  neg-flip : ∀ x y → neg (x - y) ≈ y - x
  neg-flip x y =
    begin
      neg (x - y)         ≈[ *-+-left-dist -1 x (neg y) ]
      neg x + neg (neg y) ≈[ R (neg x) !+! neg-invol y ]
      neg x + y           ≈[ +-comm (neg x) y ]
      y - x
    qed

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


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

module Data.Bool where

open import Data.Bool.Base public
open import Data.Bool.Truth public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module WellTypedTermsNBEModel where

open import Library
open import Naturals
open import WellTypedTerms
open import RMonads.REM
open import FunctorCat
open import Categories.Sets
open NatT
open Σ

-- normal forms

mutual
  data Nf (Γ : Con) : Ty → Set where
    lam : ∀{σ τ} → Nf (Γ < σ) τ → Nf Γ (σ ⇒ τ)
    ne  : Ne Γ ι → Nf Γ ι

  data Ne (Γ : Con) : Ty → Set where
    var : ∀{σ} → Var Γ σ → Ne Γ σ
    app : ∀{σ τ} → Ne Γ (σ ⇒ τ) → Nf Γ σ → Ne Γ τ

mutual
  renNf : ∀{Γ Δ} → Ren Δ Γ → ∀{σ} → Nf Δ σ → Nf Γ σ
  renNf ρ (lam n) = lam (renNf (wk ρ) n)
  renNf ρ (ne n)  = ne  (renNe ρ n)

  renNe : ∀{Γ Δ} → Ren Δ Γ → ∀{σ} → Ne Δ σ → Ne Γ σ
  renNe ρ (var x)    = var (ρ x)
  renNe ρ (app n n') = app (renNe ρ n) (renNf ρ n')

mutual
  renNfid : ∀{Γ} σ (v : Nf Γ σ) → renNf id v ≅ v
  renNfid ι (ne x) = cong ne (renNeid ι x)
  renNfid (σ ⇒ τ) (lam v) = cong lam $
    proof
    renNf (wk id) v
    ≅⟨ cong (λ (ρ : Ren _ _) → renNf ρ v)
            (iext λ _ → ext wkid) ⟩
    renNf id v
    ≅⟨ renNfid τ v ⟩
    v
    ∎

  renNeid : ∀{Γ} σ (v : Ne Γ σ) → renNe id v ≅ v
  renNeid σ (var x) = refl
  renNeid τ (app {σ} v x) = cong₂ app (renNeid (σ ⇒ τ) v) (renNfid σ x)

mutual
  renNecomp : ∀{Δ Γ B}(ρ : Ren Δ Γ)(ρ' : Ren Γ B) σ (v : Ne Δ σ) →
             renNe (ρ' ∘ ρ) v ≅ renNe ρ' (renNe ρ v)
  renNecomp ρ ρ' σ (var x)       = refl
  renNecomp ρ ρ' τ (app {σ} v x) = cong₂
    Ne.app
    (renNecomp ρ ρ' (σ ⇒ τ) v)
    (renNfcomp ρ ρ' σ x)

  renNfcomp : ∀{Δ Γ B}(ρ : Ren Δ Γ)(ρ' : Ren Γ B) σ (v : Nf Δ σ) →
             renNf (ρ' ∘ ρ) v ≅ renNf ρ' (renNf ρ v)
  renNfcomp ρ ρ' (σ ⇒ τ) (lam v) = cong Nf.lam $
    proof
    renNf (wk (ρ' ∘ ρ)) v
    ≅⟨ cong (λ (ρ : Ren _ _) → renNf ρ v)
            (iext λ _ → ext (wkcomp ρ' ρ)) ⟩
    renNf (wk ρ' ∘ wk ρ) v
    ≅⟨ renNfcomp (wk ρ) (wk ρ') τ v ⟩
    renNf (wk ρ') (renNf (wk ρ) v)
    ∎
  renNfcomp ρ ρ' ι       (ne x)  = cong ne (renNecomp ρ ρ' ι x)

mutual
  Val : Con → Ty → Set
  Val Γ ι       = Ne Γ ι
  Val Γ (σ ⇒ τ) = ∀{B} →  Ren Γ B → Val B σ → Val B τ

--      (λ f → ∀{B B'}(ρ : Ren Γ B)(ρ' : Ren B B')(a : Val B σ) → renV ρ' (f ρ a) ≅ f (ρ' ∘ ρ) (renV ρ' a))

renV : ∀{Γ Δ} → Ren Δ Γ → ∀{σ} → Val Δ σ → Val Γ σ
renV ρ {ι}     n = renNe ρ n
renV {Γ}{Δ} ρ {σ ⇒ τ} f = λ ρ' → f (ρ' ∘ ρ)

{-
Ren Γ B → Val B σ → Val B τ
|                       |
\/                      \/
Ren Γ B' → Val B' σ → Val B' τ

-}
-- interpretation of contexts

Env : Con → Con → Set
Env Γ Δ = ∀{σ} →  Var Γ σ → Val Δ σ

_<<_ : ∀{Γ Δ σ} → Env Γ Δ → Val Δ σ → Env (Γ < σ) Δ
(γ << v) vz     = v
(γ << v) (vs x) = γ x

eval : ∀{Γ Δ σ} → Env Δ Γ → Tm Δ σ → Val Γ σ
eval γ (var i)   = γ i
eval γ (lam t)   = λ ρ v → eval ((renV ρ ∘ γ) << v) t
eval γ (app t u) = eval γ t id (eval γ u)

lem : ∀{B Γ Δ σ}(ρ : Ren Γ B)(γ : Env Δ Γ)(t : Tm Δ σ) →
      renV ρ (eval γ t) ≅ eval (renV ρ ∘ γ) t
lem = {!!}

renVid : ∀{Γ} σ (v : Val Γ σ) → renV id v ≅ v
renVid ι       v = renNeid ι v
renVid (σ ⇒ τ) v = refl

renVcomp : ∀{Δ Γ B}(ρ : Ren Δ Γ)(ρ' : Ren Γ B) σ (v : Val Δ σ) →
         renV (ρ' ∘ ρ) v ≅ renV ρ' (renV ρ v)
renVcomp ρ ρ' ι       v = renNecomp ρ ρ' ι v
renVcomp ρ ρ' (σ ⇒ τ) v = refl

renV<< : ∀{B' B Γ}(α  : Ren B B')(β : Env Γ B){σ}(v : Val B σ) →
        ∀{ρ}(y : Var (Γ < σ) ρ) →
        ((renV α ∘ β) << renV α v) y ≅ (renV α ∘ (β << v)) y
renV<< α β v vz = refl
renV<< α β v (vs y) = refl

substeval : ∀{σ τ}(p : σ ≅ τ){Γ B : Con}{γ : Env Γ B}(t : Tm Γ σ) →
      (subst (Val B) p  ∘ eval γ) t ≅ (eval γ ∘ subst (Tm Γ) p) t
substeval refl t = refl

wk<< : ∀{B Γ Δ}(α  : Ren Γ Δ)(β : Env Δ B){σ}(v : Val B σ) →
        ∀{ρ}(y : Var (Γ < σ) ρ) →
        ((β ∘ α) << v) y ≅ (β << v) (wk α y)
wk<< α β v vz     = refl
wk<< α β v (vs y) = refl

<<eq : ∀{Γ Δ σ}{β β' : Env Γ Δ} → (λ{σ} → β {σ}) ≅ (λ{σ} → β' {σ}) →
        (v : Val Δ σ) → (λ {σ} → (β << v) {σ}) ≅ (λ {σ} → (β' << v) {σ})
<<eq refl v = refl

reneval : ∀{B Γ Δ σ}(α : Ren Γ Δ)(β : Env Δ B)(t : Tm Γ σ) →
          eval (β ∘ α) t
          ≅
          (eval β ∘ ren α) t
reneval α β (var x)   = refl
reneval α β (app t u) =
  cong₂ (λ f x → f id x) (reneval α β t) (reneval α β u)
reneval {B} α β (lam t) = iext λ B' → ext λ (ρ : Ren B B') → ext λ v →
  proof
  eval ((renV ρ ∘ β ∘ α) << v) t
  ≅⟨ cong (λ (γ : Env _ B') → eval γ t)
          (iext λ _ → ext (wk<< α (renV ρ ∘ β) v)) ⟩
  eval (((renV ρ ∘ β) << v) ∘ wk α) t
  ≅⟨ reneval (wk α) ((renV ρ ∘ β) << v) t ⟩
  eval ((renV ρ ∘ β) << v) (ren (wk α) t)
  ∎

lifteval : ∀{B Γ Δ σ τ}(α : Sub Γ Δ)(β : Env Δ B)
           (v : Val B σ)(y : Var (Γ < σ) τ) →
           ((eval β ∘ α) << v) y ≅ (eval (β << v) ∘ lift α) y
lifteval α β v vz     = refl
lifteval α β v (vs x) = reneval vs (β << v) (α x)

subeval : ∀{B Γ Δ σ}(α : Sub Γ Δ)(β : Env Δ B)(t : Tm Γ σ) →
          eval (eval β ∘ α) t ≅ (eval β ∘ sub α) t
subeval α β (var x)   = refl
subeval α β (app t u) = cong₂ (λ f x → f id x) (subeval α β t) (subeval α β u)
subeval {B} α β (lam t) = iext λ B' → ext λ (ρ : Ren B B') → ext λ v →
  proof
  eval ((renV ρ ∘ eval β ∘ α) << v) t
  ≅⟨ cong (λ (γ : Env _ B') → eval (γ << v) t)
          (iext λ _ → ext λ x → lem ρ β (α x)) ⟩
  eval ((eval (renV ρ ∘ β) ∘ α) << v) t
  ≅⟨ cong (λ (γ : Env _ B') → eval γ t)
          (iext λ _ → ext λ x → lifteval α (renV ρ ∘ β) v x) ⟩
  eval (eval ((renV ρ ∘ β) << v) ∘ lift α) t
  ≅⟨ subeval (lift α) ((renV ρ ∘ β) << v) t ⟩
  eval ((λ {σ} x → renV ρ (β x)) << v) (sub (lift α) t)
  ∎

modelRAlg : Con → RAlg TmRMonad
modelRAlg Γ = record {
  acar  = Val Γ;
  astr  = λ γ → eval γ;
  alaw1 = refl;
  alaw2 = λ {B} {Δ} {α} {γ} → iext (λ σ → ext (subeval α γ))}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------
-- Regular expressions
------------------------------------------------------------------------

open import Setoids

module RegExps (S : Setoid) where

infix  8 _⋆
infixl 7 _⊙_
infixl 6 _∣_
infix  1 _∈‿⟦_⟧

open import Prelude
private open module S' = Setoid S

------------------------------------------------------------------------
-- Regular expressions

data RegExp : Set where
  ∅   : RegExp                      -- Matches nothing.
  ε   : RegExp                      -- Matches the empty string.
  •   : RegExp                      -- Matches any single character.
  sym : carrier -> RegExp           -- Matches the given character.
  _⋆  : RegExp -> RegExp            -- Kleene star.
  _∣_ : RegExp -> RegExp -> RegExp  -- Choice.
  _⊙_ : RegExp -> RegExp -> RegExp  -- Sequencing.

------------------------------------------------------------------------
-- Size of a regular expression

size : RegExp -> ℕ
size (re ⋆)      = 1 + size re
size (re₁ ∣ re₂) = 1 + size re₁ + size re₂
size (re₁ ⊙ re₂) = 1 + size re₁ + size re₂
size _           = 1

------------------------------------------------------------------------
-- Semantics of regular expressions

-- The type xs ∈‿⟦ re ⟧ is inhabited iff xs matches the regular
-- expression re.

data _∈‿⟦_⟧ : [ carrier ] -> RegExp -> Set where
  matches-ε   : [] ∈‿⟦ ε ⟧
  matches-•   : forall {x} -> x ∷ [] ∈‿⟦ • ⟧
  matches-sym : forall {x y} -> x ≈ y -> x ∷ [] ∈‿⟦ sym y ⟧
  matches-⋆   : forall {xs re}
              -> xs ∈‿⟦ ε ∣ re ⊙ re ⋆ ⟧ -> xs ∈‿⟦ re ⋆ ⟧
  matches-∣ˡ   : forall {xs re₁ re₂}
              -> xs ∈‿⟦ re₁ ⟧ -> xs ∈‿⟦ re₁ ∣ re₂ ⟧
  matches-∣ʳ   : forall {xs re₁ re₂}
              -> xs ∈‿⟦ re₂ ⟧ -> xs ∈‿⟦ re₁ ∣ re₂ ⟧
  matches-⊙   : forall {xs₁ xs₂ re₁ re₂}
              -> xs₁ ∈‿⟦ re₁ ⟧ -> xs₂ ∈‿⟦ re₂ ⟧
              -> xs₁ ++ xs₂ ∈‿⟦ re₁ ⊙ re₂ ⟧

------------------------------------------------------------------------
-- Is the regular expression bypassable?

bypassable : (re : RegExp) -> Maybe ([] ∈‿⟦ re ⟧)
bypassable ∅           = nothing
bypassable ε           = just matches-ε
bypassable •           = nothing
bypassable (sym _)     = nothing
bypassable (re ⋆)      = just (matches-⋆ (matches-∣ˡ matches-ε))
bypassable (re₁ ∣ re₂) with bypassable re₁ | bypassable re₂
bypassable (re₁ ∣ re₂) | just m  | _       = just (matches-∣ˡ m)
bypassable (re₁ ∣ re₂) | nothing | just m  = just (matches-∣ʳ m)
bypassable (re₁ ∣ re₂) | nothing | nothing = nothing
bypassable (re₁ ⊙ re₂) with bypassable re₁ | bypassable re₂
bypassable (re₁ ⊙ re₂) | just m₁ | just m₂ = just (matches-⊙ m₁ m₂)
bypassable (re₁ ⊙ re₂) | _       | _       = nothing


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- List membership and some related definitions
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where

open import Function using (_∘_; id; flip)
open import Data.Fin using (Fin; zero; suc)
open import Data.List.Base as List using (List; []; _∷_; length; lookup)
open import Data.List.Relation.Unary.Any
  using (Any; index; map; here; there)
open import Data.Product as Prod using (∃; _×_; _,_)
open import Relation.Unary using (Pred)
open import Relation.Nullary using (¬_)

open Setoid S renaming (Carrier to A)

open Data.List.Relation.Unary.Any using (_∷=_; _─_) public

------------------------------------------------------------------------
-- Definitions

infix 4 _∈_ _∉_

_∈_ : A → List A → Set _
x ∈ xs = Any (x ≈_) xs

_∉_ : A → List A → Set _
x ∉ xs = ¬ x ∈ xs

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

mapWith∈ : ∀ {b} {B : Set b}
           (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
mapWith∈ []       f = []
mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)

------------------------------------------------------------------------
-- Finding and losing witnesses

module _ {p} {P : Pred A p} where

  find : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
  find (here px)   = (_ , here refl , px)
  find (there pxs) = Prod.map id (Prod.map there id) (find pxs)

  lose : P Respects _≈_ →  ∀ {x xs} → x ∈ xs → P x → Any P xs
  lose resp x∈xs px = map (flip resp px) x∈xs

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

-- Version 0.16

map-with-∈ = mapWith∈
{-# WARNING_ON_USAGE map-with-∈
"Warning: map-with-∈ was deprecated in v0.16.
Please use mapWith∈ instead."
#-}


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

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

data Mult3 : ℕ → Set where
  0-mult : Mult3 0
  SSS-mult : ∀ n → Mult3 n → Mult3 (suc (suc (suc n)))

data Mult3' : ℕ → Set where
  30-mult : Mult3' 30
  21-mult : Mult3' 21
  sum-mult : ∀ n m → Mult3' n → Mult3' m → Mult3' (n + m)
  diff-mult : ∀ l n m → Mult3' n → Mult3' m → l + n ≡ m → Mult3' l

silly3 : Mult3' 3
silly3 = diff-mult 3 9 12 (diff-mult 9 21 30 21-mult 30-mult refl) (diff-mult 12 9 21 (diff-mult 9 21 30 21-mult 30-mult refl) 21-mult refl) refl

lemma-plus : ∀ {n m : ℕ} → Mult3 n → Mult3 m → Mult3 (n + m)
lemma-plus 0-mult m = m
lemma-plus {m = m₁} (SSS-mult n n₁) m = SSS-mult (n + m₁) (lemma-plus n₁ m)

lemma-minus : ∀ {l n : ℕ} → Mult3 n → Mult3 (n + l) → Mult3 l
lemma-minus {l} {.0} 0-mult m₁ = m₁
lemma-minus {l} {.(suc (suc (suc n)))} (SSS-mult n n₁) (SSS-mult .(n + l) m₁) = lemma-minus n₁ m₁

lemma-silly : ∀ {m n : ℕ} → Mult3 m → m ≡ n → Mult3 n
lemma-silly m eq rewrite eq = m

mult-imp-mult' : ∀ {n : ℕ} → Mult3 n → Mult3' n
mult-imp-mult' 0-mult = diff-mult zero 30 30 30-mult 30-mult refl
mult-imp-mult' (SSS-mult n M) = sum-mult 3 n silly3 (mult-imp-mult' M)

mult'-imp-mult : ∀ {n : ℕ} → Mult3' n → Mult3 n
mult'-imp-mult 30-mult = SSS-mult 27
                           (SSS-mult 24
                            (SSS-mult 21
                             (SSS-mult 18
                              (SSS-mult 15
                               (SSS-mult 12
                                (SSS-mult 9 (SSS-mult 6 (SSS-mult 3 (SSS-mult zero 0-mult)))))))))
mult'-imp-mult 21-mult = SSS-mult 18
                           (SSS-mult 15
                            (SSS-mult 12
                             (SSS-mult 9 (SSS-mult 6 (SSS-mult 3 (SSS-mult zero 0-mult))))))
mult'-imp-mult (sum-mult n m M M₁) = lemma-plus (mult'-imp-mult M) (mult'-imp-mult M₁)
mult'-imp-mult (diff-mult l n m M M₁ x) rewrite +-comm l n = lemma-minus {l} {n} (mult'-imp-mult M) (lemma-silly {m} {n + l} (mult'-imp-mult M₁) (sym x))

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module plfa.part1.Negation where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _<_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import plfa.part1.Isomorphism using (_≃_; extensionality)

¬_ : Set → Set
¬ A = A → ⊥

¬-elim : ∀ {A : Set}
  → ¬ A
  → A
    ---
  → ⊥
¬-elim ¬x x = ¬x x

infix 3 ¬_

¬¬-intro : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A
¬¬-intro x  =  λ{¬x → ¬x x}

¬¬¬-elim : ∀ {A : Set}
  → ¬ ¬ ¬ A
    -------
  → ¬ A
¬¬¬-elim ¬¬¬x  =  λ x → ¬¬¬x (¬¬-intro x)

contraposition : ∀ {A B : Set}
  → (A → B)
    -----------
  → (¬ B → ¬ A)
contraposition f ¬y x = ¬y (f x)

_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y  =  ¬ (x ≡ y)

_ : 1 ≢ 2
_ = λ()

peano : ∀ {m : ℕ} → zero ≢ suc m
peano = λ()

id : ⊥ → ⊥
id x = x

id′ : ⊥ → ⊥
id′ ()

assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
assimilation ¬x ¬x′ = extensionality (λ x → ⊥-elim (¬x x))

assimilation' : ∀ {A : Set} {¬x ¬x′ : ¬ A} → ¬x ≡ ¬x′
assimilation' {A} {¬x} {¬x′} = assimilation ¬x ¬x′

<-irreflexive : ∀ {n : ℕ} → ¬ (n < n)
<-irreflexive (Data.Nat.s≤s x) = <-irreflexive x

⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
⊎-dual-× = record {
                  to = λ {x → (λ z → x (inj₁ z)) , λ x₁ → x (inj₂ x₁) };
                  from = λ { (fst , snd) (inj₁ x) → fst x ;
                             (fst , snd) (inj₂ y) → snd y} ;
                  from∘to = λ {¬x → assimilation'} ;
                  to∘from = λ { (fst , snd) → refl} }

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


text:
-- Andreas 2012-07-07
module Issue674 where

record unit : Set where
  constructor tt

module A ⦃ t : unit ⦄ (i : unit) where
  id : unit → unit
  id x = x

open A {{t = _}} tt

module N = A {{ tt }} tt
open N

open A {{tt}} tt

module M = A tt
open M

open A tt
-- the last statement caused a panic when inserting the instance meta
-- because due to open it found candidates in scope that were not
-- in the signature yet


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

module Chord where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Data.Fin        using (Fin; toℕ) renaming (zero to fz; suc to fs)
open import Data.List       using (List; map; []; _∷_; _++_; zip)
open import Data.Nat        using (ℕ)
open import Data.Product    using (_×_)
open import Data.String     using (String) renaming (_++_ to _++s_)

open import Function        using (_∘_)

open import AssocList
open import BitVec
open import Pitch
open import Util            using (_+N_)

data Root : Type where
  root : Fin s12 → Root

showRoot : Root → String
showRoot (root fz)                                                        = "I"
showRoot (root (fs fz))                                                   = "♭II"
showRoot (root (fs (fs fz)))                                              = "II"
showRoot (root (fs (fs (fs fz))))                                         = "♭III"
showRoot (root (fs (fs (fs (fs fz)))))                                    = "III"
showRoot (root (fs (fs (fs (fs (fs fz))))))                               = "IV"
showRoot (root (fs (fs (fs (fs (fs (fs fz)))))))                          = "♭V"
showRoot (root (fs (fs (fs (fs (fs (fs (fs fz))))))))                     = "V"
showRoot (root (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))                = "♭VI"
showRoot (root (fs (fs (fs (fs (fs (fs (fs (fs (fs fz))))))))))           = "VI"
showRoot (root (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))      = "♭VII"
showRoot (root (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))))) = "VII"

data Quality : Type where
  maj  : Quality
  min  : Quality
  dom7 : Quality
  maj7 : Quality

showQuality : Quality → String
showQuality maj  = "maj"
showQuality min  = "min"
showQuality dom7 = "⁷"
showQuality maj7 = "maj⁷"

RootQuality : Type
RootQuality = Root × Quality

showRootQuality : RootQuality → String
showRootQuality (r , q) = showRoot r ++s showQuality q

Notes : Type
Notes = BitVec s12

ChordList : Type
ChordList = AList Notes RootQuality

-- The list should not include the root.
makeChord : Root → List ℕ → Notes
makeChord (root n) []       = BitVec.insert n empty
makeChord (root n) (x ∷ xs) = BitVec.insert (n +N x) (makeChord (root n) xs)

-- The list should not include the root.
qualityNotes : Quality → List ℕ
qualityNotes maj  = 4 ∷ 7 ∷ []
qualityNotes min  = 3 ∷ 7 ∷ []
qualityNotes dom7 = 4 ∷ 7 ∷ 10 ∷ []
qualityNotes maj7 = 4 ∷ 7 ∷ 11 ∷ []

makeChordQuality : RootQuality → Notes
makeChordQuality (r , q) = makeChord r (qualityNotes q)

---------

--addMajor

aa = show (makeChordQuality (root fz , maj))

{-
allPairs : {A : Type} → List A → List (A × A)
allPairs []       = []
allPairs (x ∷ xs) = map (x ,_) xs ++ allPairs xs

aa = allPairs (c 5 ∷ e 5 ∷ g 5 ∷ [])
bb = zip aa (map (toℕ ∘ unIntervalClass ∘ pitchPairToIntervalClass) aa)
-}

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module Base.Change.Equivalence.Realizers where

open import Relation.Binary.PropositionalEquality
open import Base.Change.Algebra
open import Level
open import Data.Unit
open import Data.Product
open import Function
open import Postulate.Extensionality

open import Base.Change.Equivalence

-- Here we give lemmas about realizers for function changes. Using these lemmas,
-- you can simply write a "realizer" for a derivative for f (that is, the
-- computational part of the derivative, without any embedded proof), show
-- separately that it's change-equivalent to the nil change for f and get a
-- proper function change; this code proves the needed validity lemmas.
--
-- Given a type of codes for types, such lemmas should be provable by induction
-- on those types; something similar is done in the proof of erasure, though
-- details are quite different.
--
-- For now, we do something close to unrolling the induction manually for
-- functions of arity 1, 2 and 3 since those are actually used in the codebase.
-- I didn't actually write the induction though, and I'm not sure how to do it.
--
-- So there are two attempts which might give ideas; one is
-- equiv-raw-change-to-change-binary and equiv-raw-change-to-change-ternary, the
-- other is equiv-raw-change-to-change-binary′ and
-- equiv-raw-change-to-change-ternary′.
module _
  {a} {A : Set a} {{CA : ChangeAlgebra A}}
  {b} {B : Set b} {{CB : ChangeAlgebra B}}
  (f : A → B)
  where
  private
    Set′ = Set (a ⊔ b)

  equiv₁ : ∀ (df′ : Δ f) (df-realizer : RawChange f) → Set′
  equiv₁ df′ df-realizer = apply df′ ≡ df-realizer

  equiv-raw-change-to-change-ResType :
    ∀ (df-realizer : RawChange f) → Set′
  equiv-raw-change-to-change-ResType df-realizer =
    Σ[ df′ ∈ Δ f ] equiv₁ df′ df-realizer

  equiv-hp :
      ∀ (df : Δ f) (df-realizer : RawChange f) → Set′
  equiv-hp df df-realizer = (∀ a da → apply df a da ≙₍ f a ₎ df-realizer a da)

  -- This is sort of the "base case" of the proof mentioned above.
  equiv-raw-change-to-change :
    ∀ (df : Δ f) (df-realizer : RawChange f) →
      equiv-hp df df-realizer →
      equiv-raw-change-to-change-ResType df-realizer
  equiv-raw-change-to-change df df-realizer ≙df = record { apply = df-realizer ; correct = df-realizer-correct} , refl
    where
      df-realizer-correct : ∀ a da → f (a ⊞ da) ⊞ df-realizer (a ⊞ da) (nil (a ⊞ da)) ≡ f a ⊞ df-realizer a da
      df-realizer-correct a da
        rewrite sym (proof (≙df a da))
        | sym (proof (≙df (a ⊞ da) (nil (a ⊞ da))))
        = correct df a da

  equiv-raw-deriv-to-deriv :
    ∀ (df-realizer : RawChange f) →
      equiv-hp (nil f) df-realizer →
      IsDerivative f df-realizer
  equiv-raw-deriv-to-deriv df-realizer ≙df with equiv-raw-change-to-change (nil f) df-realizer ≙df
  equiv-raw-deriv-to-deriv .(FunctionChanges.apply nil-f) ≙df | nil-f , refl =
    equiv-nil-is-derivative nil-f (delta-ext ≙df)

module _
  {a} {A : Set a} {{CA : ChangeAlgebra A}}
  {b} {B : Set b} {{CB : ChangeAlgebra B}}
  {c} {C : Set c} {{CC : ChangeAlgebra C}}
  (f : A → B → C) where
  private
    Set′ = Set (a ⊔ b ⊔ c)

  -- This is, sort of, an instance of the inductive step in the proof mentioned above.
  RawChangeBinary :
    Set′
  RawChangeBinary = ∀ a (da : Δ a) → RawChange (f a)

  equiv-hp-binary : ∀ (df : Δ f) (df-realizer : RawChangeBinary) → Set′
  equiv-hp-binary df df-realizer =
    ∀ a da → equiv-hp (f a) (apply df a da) (df-realizer a da)

  equiv₂ : ∀ (df′ : Δ f) (df-realizer : RawChangeBinary) → Set′
  equiv₂ df′ df-realizer = ∀ a da → equiv₁ (f a) (apply df′ a da) (df-realizer a da)

  equiv-raw-change-to-change-binary-ResType :
    ∀ (df-realizer : RawChangeBinary) → Set′
  equiv-raw-change-to-change-binary-ResType df-realizer =
    Σ[ df′ ∈ Δ f ] equiv₂ df′ df-realizer

  equiv-raw-change-to-change-binary equiv-raw-change-to-change-binary′ :
    ∀ (df : Δ f) (df-realizer : RawChangeBinary) →
      equiv-hp-binary df df-realizer →
      equiv-raw-change-to-change-binary-ResType df-realizer
  equiv-raw-change-to-change-binary df df-realizer ≙df = proj₁ (equiv-raw-change-to-change f df df₁′ ≙df₁′) , λ a da → refl
    where
      module _ (a : A) (da : Δ a) where
        f₁ = f a
        df₁ : Δ f₁
        df₁ = apply df a da
        df-realizer₁ = df-realizer a da
        ≙df₁ = ≙df a da
        df-realizer₁-correct : ∀ b db → f₁ (b ⊞ db) ⊞ df-realizer₁ (b ⊞ db) (nil (b ⊞ db)) ≡ f₁ b ⊞ df-realizer₁ b db
        df-realizer₁-correct b db
          rewrite sym (proof (≙df₁ b db))
          | sym (proof (≙df₁ (b ⊞ db) (nil (b ⊞ db))))
          = correct df₁ b db
        df₁′ : Δ f₁
        df₁′ = record { apply = df-realizer₁ ; correct = df-realizer₁-correct }
        ≙df₁′ : df₁ ≙₍ f₁ ₎ df₁′
        ≙df₁′ = delta-ext ≙df₁

  equiv-raw-change-to-change-binary′ df df-realizer ≙df = record { apply = df₁′ ; correct = λ a da → ext (df-realizer-correct a da) } , λ a da → refl
    where
      module _ (a : A) (da : Δ a) where
        f₁ = f a
        df₁ : Δ f₁
        df₁ = apply df a da
        df-realizer₁ = df-realizer a da
        ≙df₁ = ≙df a da
        df₁′ = proj₁ (equiv-raw-change-to-change f₁ df₁ df-realizer₁ ≙df₁)
        df-realizer-correct : ∀ b → f (a ⊞ da) b ⊞ df-realizer (a ⊞ da) (nil (a ⊞ da)) b (nil b) ≡ f a b ⊞ df-realizer a da b (nil b)
        df-realizer-correct b
          rewrite sym (proof (≙df a da b (nil b)))
          | sym (proof (≙df (a ⊞ da) (nil (a ⊞ da)) b (nil b)))
          = cong (λ □ → □ b) (correct df a da)

  equiv-raw-deriv-to-deriv-binary :
    ∀ (df-realizer : RawChangeBinary) →
      (≙df : equiv-hp-binary (nil f) df-realizer) →
      IsDerivative f (apply (proj₁ (equiv-raw-change-to-change-binary (nil f) df-realizer ≙df)))
  equiv-raw-deriv-to-deriv-binary df-realizer ≙df a da with equiv-raw-change-to-change-binary (nil f) df-realizer ≙df
  ... | nil-f , nil-f≡df with sym (nil-f≡df a da)
  ... | df-a-da≡nil-f-a-da rewrite df-a-da≡nil-f-a-da = equiv-nil-is-derivative nil-f (delta-ext {df = nil f} {dg = nil-f} (λ a da → doe (ext (lemma a da)))) a da
    where
      lemma : ∀ a da b → (f a ⊞ apply (nil f) a da) b ≡ (f a ⊞ apply nil-f a da) b
      lemma a da b rewrite nil-f≡df a da = proof (≙df a da b (nil b))

module _
  {a} {A : Set a} {{CA : ChangeAlgebra A}}
  {b} {B : Set b} {{CB : ChangeAlgebra B}}
  {c} {C : Set c} {{CC : ChangeAlgebra C}}
  {d} {D : Set d} {{CD : ChangeAlgebra D}}
  (f : A → B → C → D)
  where
  private
    Set′ = Set (a ⊔ b ⊔ c ⊔ d)

  -- This is an adapted copy of the above "inductive step".
  RawChangeTernary : Set′
  RawChangeTernary = ∀ a (da : Δ a) → RawChangeBinary (f a)

  equiv-hp-ternary : ∀ (df : Δ f) (df-realizer : RawChangeTernary) → Set′
  equiv-hp-ternary df df-realizer =
    ∀ a da → equiv-hp-binary (f a) (apply df a da) (df-realizer a da)

  equiv₃ : ∀ (df′ : Δ f) (df-realizer : RawChangeTernary) → Set′
  equiv₃ df′ df-realizer = ∀ a da → equiv₂ (f a) (apply df′ a da) (df-realizer a da)

  equiv-raw-change-to-change-ternary-ResType :
    ∀ (df-realizer : RawChangeTernary) → Set′
  equiv-raw-change-to-change-ternary-ResType df-realizer =
    Σ[ df′ ∈ Δ f ] equiv₃ df′ df-realizer

  equiv-raw-change-to-change-ternary equiv-raw-change-to-change-ternary′ :
    ∀ (df : Δ f) (df-realizer : RawChangeTernary) →
      equiv-hp-ternary df df-realizer →
      equiv-raw-change-to-change-ternary-ResType df-realizer

  equiv-raw-change-to-change-ternary df df-realizer ≙df =
    proj₁ (equiv-raw-change-to-change-binary f df df₁′ ≙df₁′) , λ a da b db → refl
    where
      module _ (a : A) (da : Δ a) (b : B) (db : Δ b) where
        f₁ = f a b
        df₁ : Δ f₁
        df₁ = apply (apply df a da) b db
        df-realizer₁ = df-realizer a da b db
        ≙df₁ = ≙df a da b db

        df-realizer₁-correct : ∀ c dc → f₁ (c ⊞ dc) ⊞ df-realizer₁ (c ⊞ dc) (nil (c ⊞ dc)) ≡ f₁ c ⊞ df-realizer₁ c dc
        df-realizer₁-correct c dc
          rewrite sym (proof (≙df₁ c dc))
          | sym (proof (≙df₁ (c ⊞ dc) (nil (c ⊞ dc))))
          = correct df₁ c dc
        df₁′ : Δ f₁
        df₁′ = record { apply = df-realizer₁ ; correct = df-realizer₁-correct }
        ≙df₁′ : df₁ ≙₍ f₁ ₎ df₁′
        ≙df₁′ = delta-ext ≙df₁

  equiv-raw-change-to-change-ternary′ df df-realizer ≙df = record { apply = df₁′ ; correct = λ a da → ext (λ b → ext (df-realizer-correct a da b)) } , λ a da b db → refl
    where
      module _ (a : A) (da : Δ a) where
        f₁ = f a
        df₁ : Δ f₁
        df₁ = apply df a da
        df-realizer₁ = df-realizer a da
        ≙df₁ = ≙df a da
        df₁′ = proj₁ (equiv-raw-change-to-change-binary f₁ df₁ df-realizer₁ ≙df₁)
        df-realizer-correct : ∀ b c → f (a ⊞ da) b c ⊞ df-realizer (a ⊞ da) (nil (a ⊞ da)) b (nil b) c (nil c) ≡ f a b c ⊞ df-realizer a da b (nil b) c (nil c)
        df-realizer-correct b c
          rewrite sym (proof (≙df a da b (nil b) c (nil c)))
          | sym (proof (≙df (a ⊞ da) (nil (a ⊞ da)) b (nil b) c (nil c)))
          = cong (λ □ → □ b c) (correct df a da)

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:
open import Agda.Builtin.Nat
open import Agda.Builtin.Int
open import Agda.Builtin.Equality

fromNeg : Nat → Int
fromNeg zero    = pos 0
fromNeg (suc x) = negsuc x

{-# BUILTIN FROMNEG fromNeg #-}

-- A negative number

neg : Int
neg = -20

-- Matching against negative numbers

lit : Int → Nat
lit -20 = 0  -- Error thrown here
lit _   = 1

-- Testing reduction rules

test0 : lit -20 ≡ 0
test0 = refl

test1 : lit -2 ≡ 1
test1 = refl

-- Error WAS: Internal error in expandLitPattern
-- Error NOW: Type mismatch when checking that the pattern -20 has type Int

-- Ideally, this would succeed.


text:
module Tactic.Reflection.Equality where

open import Prelude
open import Builtin.Reflection
open import Builtin.Float

instance
  EqVisibility : Eq Visibility
  _==_ {{EqVisibility}} visible  visible  = yes refl
  _==_ {{EqVisibility}} visible  hidden   = no (λ ())
  _==_ {{EqVisibility}} visible  instance′ = no (λ ())
  _==_ {{EqVisibility}} hidden   visible  = no (λ ())
  _==_ {{EqVisibility}} hidden   hidden   = yes refl
  _==_ {{EqVisibility}} hidden   instance′ = no (λ ())
  _==_ {{EqVisibility}} instance′ visible  = no (λ ())
  _==_ {{EqVisibility}} instance′ hidden   = no (λ ())
  _==_ {{EqVisibility}} instance′ instance′ = yes refl

  EqRelevance : Eq Relevance
  _==_ {{EqRelevance}} relevant   relevant   = yes refl
  _==_ {{EqRelevance}} relevant   irrelevant = no (λ ())
  _==_ {{EqRelevance}} irrelevant relevant   = no (λ ())
  _==_ {{EqRelevance}} irrelevant irrelevant = yes refl

  EqArgInfo : Eq ArgInfo
  _==_ {{EqArgInfo}} (arg-info v r) (arg-info v₁ r₁) =
    decEq₂ arg-info-inj₁ arg-info-inj₂ (v == v₁) (r == r₁)

  EqArg : ∀ {A} {{EqA : Eq A}} → Eq (Arg A)
  _==_ {{EqArg}} (arg i x) (arg i₁ x₁) = decEq₂ arg-inj₁ arg-inj₂ (i == i₁) (x == x₁)

  EqLiteral : Eq Literal
  _==_ {{EqLiteral}} = eqLit
    where
      eqLit : (x y : Literal) → Dec (x ≡ y)
      eqLit (nat    x) (nat    y) = decEq₁ nat-inj    (x == y)
      eqLit (word64 x) (word64 y) = decEq₁ word64-inj (x == y)
      eqLit (float  x) (float  y) = decEq₁ float-inj  (x == y)
      eqLit (char   x) (char   y) = decEq₁ char-inj   (x == y)
      eqLit (string x) (string y) = decEq₁ string-inj (x == y)
      eqLit (name   x) (name   y) = decEq₁ name-inj   (x == y)
      eqLit (meta   x) (meta   y) = decEq₁ meta-inj   (x == y)

      eqLit (nat    _) (float  _) = no λ()
      eqLit (nat    _) (word64 _) = no λ()
      eqLit (nat    _) (char   _) = no λ()
      eqLit (nat    _) (string _) = no λ()
      eqLit (nat    _) (name   _) = no λ()
      eqLit (nat    _) (meta   _) = no λ()
      eqLit (word64 _) (nat    _) = no λ()
      eqLit (word64 _) (float  _) = no λ()
      eqLit (word64 _) (char   _) = no λ()
      eqLit (word64 _) (string _) = no λ()
      eqLit (word64 _) (name   _) = no λ()
      eqLit (word64 _) (meta   _) = no λ()
      eqLit (float  _) (nat    _) = no λ()
      eqLit (float  _) (word64 _) = no λ()
      eqLit (float  _) (char   _) = no λ()
      eqLit (float  _) (string _) = no λ()
      eqLit (float  _) (name   _) = no λ()
      eqLit (float  _) (meta   _) = no λ()
      eqLit (char   _) (nat    _) = no λ()
      eqLit (char   _) (word64 _) = no λ()
      eqLit (char   _) (float  _) = no λ()
      eqLit (char   _) (string _) = no λ()
      eqLit (char   _) (name   _) = no λ()
      eqLit (char   _) (meta   _) = no λ()
      eqLit (string _) (nat    _) = no λ()
      eqLit (string _) (word64 _) = no λ()
      eqLit (string _) (float  _) = no λ()
      eqLit (string _) (char   _) = no λ()
      eqLit (string _) (name   _) = no λ()
      eqLit (string _) (meta   _) = no λ()
      eqLit (name   _) (nat    _) = no λ()
      eqLit (name   _) (word64 _) = no λ()
      eqLit (name   _) (float  _) = no λ()
      eqLit (name   _) (char   _) = no λ()
      eqLit (name   _) (string _) = no λ()
      eqLit (name   _) (meta   _) = no λ()
      eqLit (meta   _) (nat    _) = no λ()
      eqLit (meta   _) (word64 _) = no λ()
      eqLit (meta   _) (float  _) = no λ()
      eqLit (meta   _) (char   _) = no λ()
      eqLit (meta   _) (string _) = no λ()
      eqLit (meta   _) (name   _) = no λ()

private
  eqSort   : (x y : Sort)    → Dec (x ≡ y)
  eqTerm   : (x y : Term)    → Dec (x ≡ y)
  eqPat    : (x y : Pattern) → Dec (x ≡ y)
  eqClause : (x y : Clause)  → Dec (x ≡ y)

  eqArgTerm : (x y : Arg Term) → Dec (x ≡ y)
  eqArgTerm (arg i x) (arg i₁ x₁) = decEq₂ arg-inj₁ arg-inj₂ (i == i₁) (eqTerm x x₁)

  eqArgPat : (x y : Arg Pattern) → Dec (x ≡ y)
  eqArgPat (arg i x) (arg i₁ x₁) = decEq₂ arg-inj₁ arg-inj₂ (i == i₁) (eqPat x x₁)

  eqAbsTerm : (x y : Abs Term) → Dec (x ≡ y)
  eqAbsTerm (abs s x) (abs s₁ x₁) = decEq₂ abs-inj₁ abs-inj₂ (s == s₁) (eqTerm x x₁)

  eqPats : (x y : List (Arg Pattern)) → Dec (x ≡ y)
  eqPats [] [] = yes refl
  eqPats [] (x ∷ xs) = no λ ()
  eqPats (x ∷ xs) [] = no λ ()
  eqPats (x ∷ xs) (y ∷ ys) = decEq₂ cons-inj-head cons-inj-tail (eqArgPat x y) (eqPats xs ys)

  eqArgs : (x y : List (Arg Term)) → Dec (x ≡ y)
  eqArgs [] [] = yes refl
  eqArgs [] (x ∷ xs) = no λ ()
  eqArgs (x ∷ xs) [] = no λ ()
  eqArgs (x ∷ xs) (y ∷ ys) = decEq₂ cons-inj-head cons-inj-tail (eqArgTerm x y) (eqArgs xs ys)

  eqClauses : (x y : List Clause) → Dec (x ≡ y)
  eqClauses [] [] = yes refl
  eqClauses [] (x ∷ xs) = no λ ()
  eqClauses (x ∷ xs) [] = no λ ()
  eqClauses (x ∷ xs) (y ∷ ys) = decEq₂ cons-inj-head cons-inj-tail (eqClause x y) (eqClauses xs ys)

  eqTerm (var x args) (var x₁ args₁) = decEq₂ var-inj₁ var-inj₂ (x == x₁) (eqArgs args args₁)
  eqTerm (con c args) (con c₁ args₁) = decEq₂ con-inj₁ con-inj₂ (c == c₁) (eqArgs args args₁)
  eqTerm (def f args) (def f₁ args₁) = decEq₂ def-inj₁ def-inj₂ (f == f₁) (eqArgs args args₁)
  eqTerm (meta x args) (meta x₁ args₁) = decEq₂ meta-inj₁ meta-inj₂ (x == x₁) (eqArgs args args₁)
  eqTerm (lam v x) (lam v₁ y) = decEq₂ lam-inj₁ lam-inj₂ (v == v₁) (eqAbsTerm x y)
  eqTerm (pi t₁ t₂) (pi t₃ t₄) = decEq₂ pi-inj₁ pi-inj₂ (eqArgTerm t₁ t₃) (eqAbsTerm t₂ t₄)
  eqTerm (agda-sort x) (agda-sort x₁) = decEq₁ sort-inj (eqSort x x₁)
  eqTerm (lit l) (lit l₁)   = decEq₁ lit-inj (l == l₁)
  eqTerm (pat-lam c args) (pat-lam c₁ args₁) = decEq₂ pat-lam-inj₁ pat-lam-inj₂ (eqClauses c c₁) (eqArgs args args₁)
  eqTerm unknown unknown = yes refl

  eqTerm (var x args) (con c args₁) = no λ ()
  eqTerm (var x args) (def f args₁) = no λ ()
  eqTerm (var x args) (lam v y) = no λ ()
  eqTerm (var x args) (pi t₁ t₂) = no λ ()
  eqTerm (var x args) (agda-sort x₁) = no λ ()
  eqTerm (var x args) (lit x₁) = no λ ()
  eqTerm (var x args) unknown = no λ ()
  eqTerm (con c args) (var x args₁) = no λ ()
  eqTerm (con c args) (def f args₁) = no λ ()
  eqTerm (con c args) (lam v y) = no λ ()
  eqTerm (con c args) (pi t₁ t₂) = no λ ()
  eqTerm (con c args) (agda-sort x) = no λ ()
  eqTerm (con c args) (lit x) = no λ ()
  eqTerm (con c args) unknown = no λ ()
  eqTerm (def f args) (var x args₁) = no λ ()
  eqTerm (def f args) (con c args₁) = no λ ()
  eqTerm (def f args) (lam v y) = no λ ()
  eqTerm (def f args) (pi t₁ t₂) = no λ ()
  eqTerm (def f args) (agda-sort x) = no λ ()
  eqTerm (def f args) (lit x) = no λ ()
  eqTerm (def f args) unknown = no λ ()
  eqTerm (lam v x) (var x₁ args) = no λ ()
  eqTerm (lam v x) (con c args) = no λ ()
  eqTerm (lam v x) (def f args) = no λ ()
  eqTerm (lam v x) (pi t₁ t₂) = no λ ()
  eqTerm (lam v x) (agda-sort x₁) = no λ ()
  eqTerm (lam v x) (lit x₁) = no λ ()
  eqTerm (lam v x) unknown = no λ ()
  eqTerm (pi t₁ t₂) (var x args) = no λ ()
  eqTerm (pi t₁ t₂) (con c args) = no λ ()
  eqTerm (pi t₁ t₂) (def f args) = no λ ()
  eqTerm (pi t₁ t₂) (lam v y) = no λ ()
  eqTerm (pi t₁ t₂) (agda-sort x) = no λ ()
  eqTerm (pi t₁ t₂) (lit x) = no λ ()
  eqTerm (pi t₁ t₂) unknown = no λ ()
  eqTerm (agda-sort x) (var x₁ args) = no λ ()
  eqTerm (agda-sort x) (con c args) = no λ ()
  eqTerm (agda-sort x) (def f args) = no λ ()
  eqTerm (agda-sort x) (lam v y) = no λ ()
  eqTerm (agda-sort x) (pi t₁ t₂) = no λ ()
  eqTerm (agda-sort x) (lit x₁) = no λ ()
  eqTerm (agda-sort x) unknown = no λ ()
  eqTerm (lit x) (var x₁ args) = no λ ()
  eqTerm (lit x) (con c args) = no λ ()
  eqTerm (lit x) (def f args) = no λ ()
  eqTerm (lit x) (lam v y) = no λ ()
  eqTerm (lit x) (pi t₁ t₂) = no λ ()
  eqTerm (lit x) (agda-sort x₁) = no λ ()
  eqTerm (lit x) unknown = no λ ()
  eqTerm unknown (var x args) = no λ ()
  eqTerm unknown (con c args) = no λ ()
  eqTerm unknown (def f args) = no λ ()
  eqTerm unknown (lam v y) = no λ ()
  eqTerm unknown (pi t₁ t₂) = no λ ()
  eqTerm unknown (agda-sort x) = no λ ()
  eqTerm unknown (lit x) = no λ ()

  eqTerm (var _ _) (meta _ _) = no λ ()
  eqTerm (con _ _) (meta _ _) = no λ ()
  eqTerm (def _ _) (meta _ _) = no λ ()
  eqTerm (lam _ _) (meta _ _) = no λ ()
  eqTerm (pi _ _) (meta _ _) = no λ ()
  eqTerm (agda-sort _) (meta _ _) = no λ ()
  eqTerm (lit _) (meta _ _) = no λ ()
  eqTerm unknown (meta _ _) = no λ ()
  eqTerm (meta _ _) (var _ _) = no λ ()
  eqTerm (meta _ _) (con _ _) = no λ ()
  eqTerm (meta _ _) (def _ _) = no λ ()
  eqTerm (meta _ _) (lam _ _) = no λ ()
  eqTerm (meta _ _) (pi _ _) = no λ ()
  eqTerm (meta _ _) (agda-sort _) = no λ ()
  eqTerm (meta _ _) (lit _) = no λ ()
  eqTerm (meta _ _) unknown = no λ ()

  eqTerm (var _ _) (pat-lam _ _) = no λ ()
  eqTerm (con _ _) (pat-lam _ _) = no λ ()
  eqTerm (def _ _) (pat-lam _ _) = no λ ()
  eqTerm (lam _ _) (pat-lam _ _) = no λ ()
  eqTerm (pi _ _) (pat-lam _ _) = no λ ()
  eqTerm (meta _ _) (pat-lam _ _) = no λ ()
  eqTerm (agda-sort _) (pat-lam _ _) = no λ ()
  eqTerm (lit _) (pat-lam _ _) = no λ ()
  eqTerm unknown (pat-lam _ _) = no λ ()
  eqTerm (pat-lam _ _) (var _ _) = no λ ()
  eqTerm (pat-lam _ _) (con _ _) = no λ ()
  eqTerm (pat-lam _ _) (def _ _) = no λ ()
  eqTerm (pat-lam _ _) (lam _ _) = no λ ()
  eqTerm (pat-lam _ _) (pi _ _) = no λ ()
  eqTerm (pat-lam _ _) (meta _ _) = no λ ()
  eqTerm (pat-lam _ _) (agda-sort _) = no λ ()
  eqTerm (pat-lam _ _) (lit _) = no λ ()
  eqTerm (pat-lam _ _) unknown = no λ ()

  eqSort (set t) (set t₁) = decEq₁ set-inj (eqTerm t t₁)
  eqSort (lit n) (lit n₁) = decEq₁ slit-inj (n == n₁)
  eqSort unknown unknown = yes refl
  eqSort (set t) (lit n) = no λ ()
  eqSort (set t) unknown = no λ ()
  eqSort (lit n) (set t) = no λ ()
  eqSort (lit n) unknown = no λ ()
  eqSort unknown (set t) = no λ ()
  eqSort unknown (lit n) = no λ ()

  eqPat (con c ps) (con c₁ ps₁) = decEq₂ pcon-inj₁ pcon-inj₂ (c == c₁) (eqPats ps ps₁)
  eqPat  dot        dot         = yes refl
  eqPat (var s)    (var s₁)     = decEq₁ pvar-inj (s == s₁)
  eqPat (lit l)    (lit l₁)     = decEq₁ plit-inj (l == l₁)
  eqPat (proj f)   (proj f₁)    = decEq₁ proj-inj (f == f₁)
  eqPat  absurd     absurd      = yes refl

  eqPat (con _ _) dot      = no λ ()
  eqPat (con _ _) (var _)  = no λ ()
  eqPat (con _ _) (lit _)  = no λ ()
  eqPat (con _ _) (proj _) = no λ ()
  eqPat (con _ _) absurd   = no λ ()

  eqPat dot (con _ _) = no λ ()
  eqPat dot (var _)   = no λ ()
  eqPat dot (lit _)   = no λ ()
  eqPat dot (proj _)  = no λ ()
  eqPat dot absurd    = no λ ()

  eqPat (var _) (con _ _) = no λ ()
  eqPat (var _) dot       = no λ ()
  eqPat (var _) (lit _)   = no λ ()
  eqPat (var _) (proj _)  = no λ ()
  eqPat (var _) absurd    = no λ ()

  eqPat (lit _) (con _ _) = no λ ()
  eqPat (lit _) dot       = no λ ()
  eqPat (lit _) (var _)   = no λ ()
  eqPat (lit _) (proj _)  = no λ ()
  eqPat (lit _) absurd    = no λ ()

  eqPat (proj _) (con _ _) = no λ ()
  eqPat (proj _) dot       = no λ ()
  eqPat (proj _) (var _)   = no λ ()
  eqPat (proj _) (lit _)   = no λ ()
  eqPat (proj _) absurd    = no λ ()

  eqPat absurd (con _ _) = no λ ()
  eqPat absurd dot       = no λ ()
  eqPat absurd (var _)   = no λ ()
  eqPat absurd (lit _)   = no λ ()
  eqPat absurd (proj _)  = no λ ()

  eqClause (clause ps t)      (clause ps₁ t₁)     = decEq₂ clause-inj₁ clause-inj₂ (eqPats ps ps₁) (eqTerm t t₁)
  eqClause (absurd-clause ps) (absurd-clause ps₁) = decEq₁ absurd-clause-inj (eqPats ps ps₁)
  eqClause (clause _ _) (absurd-clause _) = no λ ()
  eqClause (absurd-clause _) (clause _ _) = no λ ()

instance
  EqTerm : Eq Term
  _==_ {{EqTerm}} = eqTerm

  EqSort : Eq Sort
  _==_ {{EqSort}} = eqSort

  EqClause : Eq Clause
  _==_ {{EqClause}} = eqClause

  EqPattern : Eq Pattern
  _==_ {{EqPattern}} = eqPat

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Natural where

open import Agda.Builtin.Equality

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

-- seven = suc (suc (suc (suc (suc (suc (suc zero))))))

{-# BUILTIN NATURAL ℕ #-}

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

{-# BUILTIN NATPLUS _+_ #-}

+-id : ∀ (a : ℕ) → a + zero ≡ zero + a
+-id zero = refl
+-id (suc a) rewrite +-id a = refl

+-comm : ∀ (a b : ℕ) → a + b ≡ b + a
+-comm zero b rewrite +-id b = refl
+-comm (suc a) zero rewrite +-id (suc a) = refl
+-comm (suc a) (suc b)
    rewrite +-comm a (suc b)
    | +-comm b (suc a)
    | +-comm a b  = refl

+-asso : ∀ (a b c : ℕ) → a + b + c ≡ a + (b + c)
+-asso zero b c = refl
+-asso (suc a) zero c
    rewrite +-id (suc a)
    | +-id a = refl
+-asso (suc a) (suc b) zero
    rewrite +-id (suc a + suc b)
    | +-id b = refl
+-asso (suc a) (suc b) (suc c)
    rewrite (+-comm a (suc b))
    | +-comm (b + a) (suc c)
    | +-comm b a
    | +-comm c (a + b)
    | +-comm b (suc c)
    | +-comm a (suc (suc (c + b)))
    | +-comm c b
    | +-comm (b + c) a
    | +-asso a b c = refl

+-rear : ∀ (a b c d : ℕ) → a + b + (c + d) ≡ a + (b + c) + d
+-rear zero b c d rewrite +-asso b c d = refl
+-rear (suc a) b c d
    rewrite (+-asso (suc a) b (c + d))
    | +-asso a (b + c) d
    | +-asso b c d = refl

+-swap : ∀ (a b c : ℕ) → a + (b + c) ≡ b + (a + c)
+-swap a b c
    rewrite (+-comm a (b + c))
    | +-comm b (a + c)
    | +-asso a c b
    | +-comm c b
    | +-comm a (b + c) = refl

_*_ : ℕ → ℕ → ℕ
infixl 7 _*_
zero * b = zero
suc a * b = b + a * b

{-# BUILTIN NATTIMES _*_ #-}

*-id : ∀ (a : ℕ) → a * (suc zero) ≡ (suc zero) * a
*-id zero = refl
*-id (suc a)
    rewrite +-comm (suc zero) a
    | *-id a = refl

*-z : ∀ (a : ℕ) → a * zero ≡ zero * a
*-z zero = refl
*-z (suc a) rewrite *-z a = refl

*-comm : ∀ (a b : ℕ) → a * b ≡ b * a
*-comm zero b rewrite *-z b = refl
*-comm (suc a) zero rewrite *-z a = refl
*-comm (suc a) (suc b)
    rewrite (*-comm a (suc b))
    | (*-comm b (suc a))
    | (*-comm a b )
    | (+-comm b (a + b * a))
    | (+-comm a (b + b * a))
    | (+-comm a (b * a))
    | (+-comm b (b * a))
    | (+-asso (b * a) a b)
    | (+-asso (b * a) b a)
    | (+-comm a b) = refl

*-+-dist-r : ∀ (a b c : ℕ) → (a + b) * c ≡ a * c + b * c
*-+-dist-r zero b c = refl
*-+-dist-r (suc a) zero c
    rewrite (+-comm (suc a) zero)
    | +-comm a zero
    | +-asso c (a * c) zero
    | +-comm (a * c) zero = refl
*-+-dist-r (suc a) (suc b) c
    rewrite (+-comm a (suc b))
    | +-rear c (a * c) c (b * c)
    | +-comm (a * c) c
    | +-asso c (c + a * c) (b * c)
    | +-asso c (a * c) (b * c)
    | +-comm (a * c) (b * c)
    | *-+-dist-r b a c = refl

*-+-dist-l : ∀ (a b c : ℕ) → a * (b + c) ≡ a * b + a * c
*-+-dist-l a zero c rewrite (*-z a) = refl
*-+-dist-l a (suc b) zero
    rewrite (+-comm (suc b) zero)
    | *-z a
    | +-comm (a * suc b) zero = refl
*-+-dist-l a (suc b) (suc c)
    rewrite (+-comm b (suc c))
    | *-comm a (suc (suc (c + b)))
    | *-comm a (suc b)
    | *-comm a (suc c)
    | +-rear a (b * a) a (c * a)
    | +-comm (b * a) a
    | +-asso a (a + b * a) (c * a)
    | +-asso a (b * a) (c * a)
    | +-comm (b * a) (c * a)
    | *-comm (c + b) a
    | *-comm c a
    | *-comm b a
    | *-+-dist-l a c b = refl

*-asso : ∀ (a b c : ℕ) → a * b * c ≡ a * (b * c)
*-asso zero b c = refl
*-asso (suc a) zero c rewrite (*-asso a zero c) = refl
*-asso (suc a) (suc b) c
    rewrite (*-+-dist-r (suc b) (a * suc b) c)
    | *-asso a (suc b) c = refl

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

^-dist-+-*-l : ∀ (a b c : ℕ) →  a ^ (b + c) ≡ (a ^ b) * (a ^ c)
^-dist-+-*-l a zero c
    rewrite (+-comm zero (a ^ c))
    | +-asso (a ^ c) zero zero = refl
^-dist-+-*-l a (suc b) c
    rewrite *-asso a (a ^ b) (a ^ c)
    | ^-dist-+-*-l a b c = refl

^-dist-*-r : ∀ (a b c : ℕ) → (a * b) ^ c ≡ (a ^ c) * (b ^ c)
^-dist-*-r a b zero rewrite (+-comm (suc zero) zero) = refl
^-dist-*-r a b (suc c)
    rewrite (*-asso a (a ^ c) (b * (b ^ c)))
    | *-comm (a ^ c) (b * (b ^ c))
    | *-asso b (b ^ c) (a ^ c)
    | *-comm (b ^ c) (a ^ c)
    | *-asso a b ((a * b) ^ c)
    | ^-dist-*-r a b c = refl

^-asso-* : ∀ (a b c : ℕ) → (a ^ b) ^ c ≡ a ^ (b * c)
^-asso-* a b zero rewrite (*-comm b zero) = refl
^-asso-* a b (suc c)
    rewrite (*-comm b (suc c))
    | ^-dist-+-*-l a b (c * b)
    | *-comm c b
    | ^-asso-* a b c = refl

data Bin : Set where
    ⟨⟩ : Bin
    _O : Bin → Bin
    _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (n O) = n I
inc (n I) = (inc n) O

to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin → ℕ
from ⟨⟩ = zero
from (n O) = 2 * (from n)
from (n I) = suc (2 * (from n))

thm₁ : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
thm₁ ⟨⟩ = refl
thm₁ (a O) = refl
thm₁ (a I)
    rewrite thm₁ a
    | +-comm (suc (from a)) zero
    | +-comm (from a) zero
    | +-comm (from a) (suc (from a)) = refl

-- thm₂ : ∀ (b : Bin) → to (from b) = b
-- 这是错误的，因为 Bin 中的 (⟨⟩ O) 和 (⟨⟩)
-- 都和 自然数 的 0 对应
-- from 并非单射

thm₃ : ∀ (n : ℕ) → from (to n) ≡ n
thm₃ zero = refl
thm₃ (suc n)
  rewrite thm₁ (to (suc n))
    | thm₁ (to n)
    | thm₃ n = refl

max_stars_repo_name: kands-code/agda-exercise

max_issues_repo_name: kands-code/agda-exercise

max_forks_repo_name: kands-code/agda-exercise


text:
open import Agda.Builtin.Bool

data D : Set where
  run-time        : D
  @0 compile-time : D

-- This code should be rejected: Both f compile-time and f run-time
-- are type-correct run-time terms.

f : @0 D → Bool
f compile-time = true
f run-time     = false

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------
-- Solver for commutative ring or semiring equalities
------------------------------------------------------------------------

-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
-- code below is not optimised like theirs, though.

open import Algebra
open import Algebra.RingSolver.AlmostCommutativeRing

module Algebra.RingSolver
  (coeff : RawRing)            -- Coefficient "ring".
  (r : AlmostCommutativeRing)  -- Main "ring".
  (morphism : coeff -Raw-AlmostCommutative⟶ r)
  where

import Algebra.RingSolver.Lemmas as L; open L coeff r morphism
private module C = RawRing coeff
open AlmostCommutativeRing r hiding (zero)
import Algebra.FunctionProperties as P; open P _≈_
open import Algebra.Morphism
open _-RawRing⟶_ morphism renaming (⟦_⟧ to ⟦_⟧')
import Algebra.Operations as Ops; open Ops semiring

open import Relation.Binary
import Relation.Binary.PropositionalEquality as PropEq
import Relation.Binary.Reflection as Reflection

open import Data.Nat using (ℕ; suc; zero) renaming (_+_ to _ℕ-+_)
open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.Vec
open import Data.Function hiding (_∶_)

infix  9 _↑ :-_ -‿NF_
infixr 9 _:^_ _^-NF_ _:↑_
infix  8 _*x _*x+_
infixl 8 _:*_ _*-NF_ _↑-*-NF_
infixl 7 _:+_ _+-NF_ _:-_
infixl 0 _∶_

------------------------------------------------------------------------
-- Polynomials

data Op : Set where
  [+] : Op
  [*] : Op

-- The polynomials are indexed over the number of variables.

data Polynomial (m : ℕ) : Set where
  op   : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m) → Polynomial m
  con  : (c : C.carrier) → Polynomial m
  var  : (x : Fin m) → Polynomial m
  _:^_ : (p : Polynomial m) (n : ℕ) → Polynomial m
  :-_  : (p : Polynomial m) → Polynomial m

-- Short-hand notation.

_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:+_ = op [+]

_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:*_ = op [*]

_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
x :- y = x :+ :- y

-- Semantics.

sem : Op → Op₂ carrier
sem [+] = _+_
sem [*] = _*_

⟦_⟧ : ∀ {n} → Polynomial n → Vec carrier n → carrier
⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ
⟦ con c ⟧      ρ = ⟦ c ⟧'
⟦ var x ⟧      ρ = lookup x ρ
⟦ p :^ n ⟧     ρ = ⟦ p ⟧ ρ ^ n
⟦ :- p ⟧       ρ = - ⟦ p ⟧ ρ

private

  -- Equality.

  _≛_ : ∀ {n} → Polynomial n → Polynomial n → Set
  p₁ ≛ p₂ = ∀ {ρ} → ⟦ p₁ ⟧ ρ ≈ ⟦ p₂ ⟧ ρ

  -- Reindexing.

  _:↑_ : ∀ {n} → Polynomial n → (m : ℕ) → Polynomial (m ℕ-+ n)
  op o p₁ p₂ :↑ m = op o (p₁ :↑ m) (p₂ :↑ m)
  con c      :↑ m = con c
  var x      :↑ m = var (Fin.raise m x)
  (p :^ n)   :↑ m = (p :↑ m) :^ n
  (:- p)     :↑ m = :- (p :↑ m)

------------------------------------------------------------------------
-- Normal forms of polynomials

private

  -- The normal forms (Horner forms) are indexed over
  -- * the number of variables in the polynomial, and
  -- * an equivalent polynomial.

  data Normal : (n : ℕ) → Polynomial n → Set where
    con   : (c : C.carrier) → Normal 0 (con c)
    _↑    : ∀ {n p'} (p : Normal n p') → Normal (suc n) (p' :↑ 1)
    _*x+_ : ∀ {n p' c'} (p : Normal (suc n) p') (c : Normal n c') →
            Normal (suc n) (p' :* var zero :+ c' :↑ 1)
    _∶_   : ∀ {n p₁ p₂} (p : Normal n p₁) (eq : p₁ ≛ p₂) → Normal n p₂

  ⟦_⟧-NF : ∀ {n p} → Normal n p → Vec carrier n → carrier
  ⟦ p ∶ _   ⟧-NF ρ       = ⟦ p ⟧-NF ρ
  ⟦ con c   ⟧-NF ρ       = ⟦ c ⟧'
  ⟦ p ↑     ⟧-NF (x ∷ ρ) = ⟦ p ⟧-NF ρ
  ⟦ p *x+ c ⟧-NF (x ∷ ρ) = (⟦ p ⟧-NF (x ∷ ρ) * x) + ⟦ c ⟧-NF ρ

------------------------------------------------------------------------
-- Normalisation

private

  con-NF : ∀ {n} → (c : C.carrier) → Normal n (con c)
  con-NF {zero}  c = con c
  con-NF {suc _} c = con-NF c ↑

  _+-NF_ : ∀ {n p₁ p₂} → Normal n p₁ → Normal n p₂ → Normal n (p₁ :+ p₂)
  (p₁ ∶ eq₁) +-NF (p₂ ∶ eq₂) = p₁ +-NF p₂                    ∶ eq₁  ⟨ +-pres-≈ ⟩ eq₂
  (p₁ ∶ eq)  +-NF p₂         = p₁ +-NF p₂                    ∶ eq   ⟨ +-pres-≈ ⟩ refl
  p₁         +-NF (p₂ ∶ eq)  = p₁ +-NF p₂                    ∶ refl ⟨ +-pres-≈ ⟩ eq
  con c₁     +-NF con c₂     = con (C._+_ c₁ c₂)             ∶ +-homo _ _
  p₁ ↑       +-NF p₂ ↑       = (p₁ +-NF p₂) ↑                ∶ refl
  p₁ *x+ c₁  +-NF p₂ ↑       = p₁ *x+ (c₁ +-NF p₂)           ∶ sym (+-assoc _ _ _)
  p₁ *x+ c₁  +-NF p₂ *x+ c₂  = (p₁ +-NF p₂) *x+ (c₁ +-NF c₂) ∶ lemma₁ _ _ _ _ _
  p₁ ↑       +-NF p₂ *x+ c₂  = p₂ *x+ (p₁ +-NF c₂)           ∶ lemma₂ _ _ _

  _*x : ∀ {n p} → Normal (suc n) p → Normal (suc n) (p :* var zero)
  p *x = p *x+ con-NF C.0# ∶ lemma₀ _

  mutual

    -- The first function is just a variant of _*-NF_ which I used to
    -- make the termination checker believe that the code is
    -- terminating.

    _↑-*-NF_ : ∀ {n p₁ p₂} →
               Normal n p₁ → Normal (suc n) p₂ →
               Normal (suc n) (p₁ :↑ 1 :* p₂)
    p₁ ↑-*-NF (p₂ ∶ eq)   = p₁ ↑-*-NF p₂                    ∶ refl ⟨ *-pres-≈ ⟩ eq
    p₁ ↑-*-NF p₂ ↑        = (p₁ *-NF p₂) ↑                  ∶ refl
    p₁ ↑-*-NF (p₂ *x+ c₂) = (p₁ ↑-*-NF p₂) *x+ (p₁ *-NF c₂) ∶ lemma₄ _ _ _ _

    _*-NF_ : ∀ {n p₁ p₂} →
             Normal n p₁ → Normal n p₂ → Normal n (p₁ :* p₂)
    (p₁ ∶ eq₁)  *-NF (p₂ ∶ eq₂)  = p₁ *-NF p₂                      ∶ eq₁  ⟨ *-pres-≈ ⟩ eq₂
    (p₁ ∶ eq)   *-NF p₂          = p₁ *-NF p₂                      ∶ eq   ⟨ *-pres-≈ ⟩ refl
    p₁          *-NF (p₂ ∶ eq)   = p₁ *-NF p₂                      ∶ refl ⟨ *-pres-≈ ⟩ eq
    con c₁      *-NF con c₂      = con (C._*_ c₁ c₂)               ∶ *-homo _ _
    p₁ ↑        *-NF p₂ ↑        = (p₁ *-NF p₂) ↑                  ∶ refl
    (p₁ *x+ c₁) *-NF p₂ ↑        = (p₁ *-NF p₂ ↑) *x+ (c₁ *-NF p₂) ∶ lemma₃ _ _ _ _
    p₁ ↑        *-NF (p₂ *x+ c₂) = (p₁ ↑ *-NF p₂) *x+ (p₁ *-NF c₂) ∶ lemma₄ _ _ _ _
    (p₁ *x+ c₁) *-NF (p₂ *x+ c₂) =
      (p₁ *-NF p₂) *x *x +-NF
      (p₁ *-NF c₂ ↑ +-NF c₁ ↑-*-NF p₂) *x+ (c₁ *-NF c₂)            ∶ lemma₅ _ _ _ _ _

  -‿NF_ : ∀ {n p} → Normal n p → Normal n (:- p)
  -‿NF (p ∶ eq)  = -‿NF p ∶ -‿pres-≈ eq
  -‿NF con c     = con (C.-_ c) ∶ -‿homo _
  -‿NF (p ↑)     = (-‿NF p) ↑
  -‿NF (p *x+ c) = -‿NF p *x+ -‿NF c ∶ lemma₆ _ _ _

  var-NF : ∀ {n} → (i : Fin n) → Normal n (var i)
  var-NF zero    = con-NF C.1# *x+ con-NF C.0# ∶ lemma₇ _
  var-NF (suc i) = var-NF i ↑

  _^-NF_ : ∀ {n p} → Normal n p → (i : ℕ) → Normal n (p :^ i)
  p ^-NF zero  = con-NF C.1#     ∶ 1-homo
  p ^-NF suc n = p *-NF p ^-NF n ∶ refl

  normaliseOp : ∀ (o : Op) {n p₁ p₂} →
                Normal n p₁ → Normal n p₂ → Normal n (p₁ ⟨ op o ⟩ p₂)
  normaliseOp [+] = _+-NF_
  normaliseOp [*] = _*-NF_

  normalise : ∀ {n} (p : Polynomial n) → Normal n p
  normalise (op o p₁ p₂) = normalise p₁ ⟨ normaliseOp o ⟩ normalise p₂
  normalise (con c)      = con-NF c
  normalise (var i)      = var-NF i
  normalise (p :^ n)     = normalise p ^-NF n
  normalise (:- p)       = -‿NF normalise p

⟦_⟧↓ : ∀ {n} → Polynomial n → Vec carrier n → carrier
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧-NF ρ

------------------------------------------------------------------------
-- Correctness

private
  sem-pres-≈ : ∀ op → sem op Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
  sem-pres-≈ [+] = +-pres-≈
  sem-pres-≈ [*] = *-pres-≈

  raise-sem : ∀ {n x} (p : Polynomial n) ρ →
              ⟦ p :↑ 1 ⟧ (x ∷ ρ) ≈ ⟦ p ⟧ ρ
  raise-sem (op o p₁ p₂) ρ = raise-sem p₁ ρ ⟨ sem-pres-≈ o ⟩
                             raise-sem p₂ ρ
  raise-sem (con c)      ρ = refl
  raise-sem (var x)      ρ = refl
  raise-sem (p :^ n)     ρ = raise-sem p ρ ⟨ ^-pres-≈ ⟩
                             PropEq.refl {x = n}
  raise-sem (:- p)       ρ = -‿pres-≈ (raise-sem p ρ)

  nf-sound : ∀ {n p} (nf : Normal n p) ρ →
             ⟦ nf ⟧-NF ρ ≈ ⟦ p ⟧ ρ
  nf-sound (nf ∶ eq)         ρ       = nf-sound nf ρ ⟨ trans ⟩ eq
  nf-sound (con c)           ρ       = refl
  nf-sound (_↑ {p' = p'} nf) (x ∷ ρ) =
    nf-sound nf ρ ⟨ trans ⟩ sym (raise-sem p' ρ)
  nf-sound (_*x+_ {c' = c'} nf₁ nf₂) (x ∷ ρ) =
    (nf-sound nf₁ (x ∷ ρ) ⟨ *-pres-≈ ⟩ refl)
      ⟨ +-pres-≈ ⟩
    (nf-sound nf₂ ρ ⟨ trans ⟩ sym (raise-sem c' ρ))

-- Completeness can presumably also be proved (i.e. the normal forms
-- should be unique, if the casts are ignored).

------------------------------------------------------------------------
-- "Tactics"

open Reflection setoid var ⟦_⟧ ⟦_⟧↓ (nf-sound ∘ normalise)
  public using (prove; solve) renaming (_⊜_ to _:=_)

-- For examples of how solve and _:=_ can be used to
-- semi-automatically prove ring equalities, see, for instance,
-- Data.Digit or Data.Nat.DivMod.

max_issues_repo_name: larrytheliquid/Lemmachine


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

module function.overloading {i j}{X : Set i}{Y : Set j} where

open import level
open import sum
open import overloading.core

fun-is-fun : Coercion (X → Y) (X → Y)
fun-is-fun = coerce-self _

private
  module fun-methods {k}{Source : Set k}
                     ⦃ c : Coercion Source (X → Y) ⦄ where
    open Coercion c public using ()
      renaming (coerce to apply)
open fun-methods public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
module Base.Isomorphism where

open import Relation.Binary.PropositionalEquality using (_≡_)

-- The stdlib contains `Function.Inverse`, which seems to have a similar purpose, but is more complicated.

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler