text:
{-
The equivalent "goodness" of can-θ w.r.t. the rmerge reduction.
The main properties of the Can function proved in this file are:

  canθₛ-mergeˡ : ∀ {E θ' r p BV FV} sigs θ →
    CorrectBinding p BV FV →
    p ≐ E ⟦ ρ θ' · r ⟧e →
    ∀ S' →
      Signal.unwrap S' ∉ SigMap.keys (Env.sig θ') →
      Signal.unwrap S' ∈ Canθₛ (SigMap.union sigs (Env.sig θ')) 0 (E ⟦ r ⟧e) θ →
      Signal.unwrap S' ∈ Canθₛ sigs 0 p θ

  canθₛ-mergeʳ : ∀ sigs θ' r θ →
    distinct' (proj₁ (Dom θ)) (SigMap.keys sigs) →
    ∀ S' →
      Signal.unwrap S' ∈ Canθₛ (SigMap.union sigs (Env.sig θ')) 0 r θ →
      Signal.unwrap S' ∈ Canθₛ (Env.sig θ') 0 r θ

and their corresponding counterparts for the shared variables.

-}
module Esterel.Lang.CanFunction.MergePotentialRuleTheta where

open import utility
  renaming (_U̬_ to _∪_ ; _|̌_ to _-_)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Base
open import Esterel.Lang.CanFunction.CanThetaContinuation
open import Esterel.Lang.CanFunction.MergePotentialRuleLeftInductive
open import Esterel.Lang.CanFunction.NonMergePotentialRules
open import Esterel.Context
  using (EvaluationContext1 ; EvaluationContext ; _⟦_⟧e ; _≐_⟦_⟧e)
open import Esterel.Context.Properties
  using (plug ; unplug)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open EvaluationContext1
open _≐_⟦_⟧e

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

open ListSet Data.Nat._≟_
  using (set-subtract ; set-subtract-[] ; set-subtract-split ; set-subtract-merge
       ; set-subtract-notin
       ; set-remove ; set-remove-mono-∈ ; set-remove-removed ; set-remove-not-removed
       ; set-subtract-[a]≡set-remove)

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

open ≡-Reasoning

canθₖ-mergeˡ : ∀ {E θ' r p BV FV A} sigs θ →
  CorrectBinding p BV FV →
  p ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e →
  ∀ k →
    k ∈ Canθₖ (SigMap.union sigs (Env.sig θ')) 0 (E ⟦ r ⟧e) θ →
    k ∈ Canθₖ sigs 0 p θ
canθₖ-mergeˡ {E} {θ'} {r} {A = A} sigs θ cb p≐E⟦ρθ'r⟧ k k∈canθ-sigs←θ'-E⟦r⟧-θ
  rewrite sym (unplug p≐E⟦ρθ'r⟧)
  with binding-extract cb (((E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ∋ plug refl)
... | (BVp , FVp) , (BVp⊆BV , FVp⊆FV) , cbρθ'r@(CBρ cbp)
  with binding-subst cb (((E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ∋ plug refl) cbρθ'r
                     ((λ _ ()) ,′ (λ _ ()) ,′ (λ _ ()))
                     ((λ _ ()) ,′ (λ _ ()) ,′ (λ _ ()))
                     CBnothing
... | (BV' , FV') , (BVnothin⊆BV , FVnothin⊆FV) , cbnothin
  rewrite canθ'-←-distribute sigs (Env.sig θ') 0 (E ⟦ r ⟧e) θ =
  canθₖ-mergeˡ-sigs-induction sigs 0 (Env.sig θ') (Env.shr θ') (Env.var θ') r θ
    ((E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e) ∋ plug refl) cbnothin
    (distinct'-sym
      (dist'++ˡ
        (distinct'-sym
          (proj₁
            (distinct-term-context-help (ρ⟨ θ' , A ⟩· r) E cb cbρθ'r BVp⊆BV cbnothin)))))
    k k∈canθ-sigs←θ'-E⟦r⟧-θ

canθₛ-mergeˡ : ∀ {E θ' r p BV FV A} sigs θ →
  CorrectBinding p BV FV →
  p ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e →
  ∀ S' →
    Signal.unwrap S' ∉ SigMap.keys (Env.sig θ') →
    Signal.unwrap S' ∈ Canθₛ (SigMap.union sigs (Env.sig θ')) 0 (E ⟦ r ⟧e) θ →
    Signal.unwrap S' ∈ Canθₛ sigs 0 p θ
canθₛ-mergeˡ {E} {θ'} {r} {A = A} sigs θ cb p≐E⟦ρθ'r⟧ S' S'∉Domθ' S'∈canθ-sigs←θ'-E⟦r⟧-θ
  rewrite sym (unplug p≐E⟦ρθ'r⟧)
  with binding-extract cb (((E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ∋ plug refl)
... | (BVp , FVp) , (BVp⊆BV , FVp⊆FV) , cbρθ'r@(CBρ cbp)
  with binding-subst cb (((E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ∋ plug refl) cbρθ'r
                     ((λ _ ()) ,′ (λ _ ()) ,′ (λ _ ()))
                     ((λ _ ()) ,′ (λ _ ()) ,′ (λ _ ()))
                     CBnothing
... | (BV' , FV') , (BVnothin⊆BV , FVnothin⊆FV) , cbnothin
  rewrite canθ'-←-distribute sigs (Env.sig θ') 0 (E ⟦ r ⟧e) θ =
  canθₛ-mergeˡ-sigs-induction sigs 0 (Env.sig θ') (Env.shr θ') (Env.var θ') r θ
    ((E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e) ∋ plug refl) cbnothin
    (distinct'-sym
      (dist'++ˡ
        (distinct'-sym
          (proj₁
            (distinct-term-context-help (ρ⟨ θ' , A ⟩· r) E cb cbρθ'r BVp⊆BV cbnothin)))))
    (Signal.unwrap S')
    S'∉Domθ' S'∈canθ-sigs←θ'-E⟦r⟧-θ

canθₛₕ-mergeˡ : ∀ {E θ' r p BV FV A} sigs θ →
  CorrectBinding p BV FV →
  p ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e →
  ∀ s' →
    SharedVar.unwrap s' ∉ ShrMap.keys (Env.shr θ') →
    SharedVar.unwrap s' ∈ Canθₛₕ (SigMap.union sigs (Env.sig θ')) 0 (E ⟦ r ⟧e) θ →
    SharedVar.unwrap s' ∈ Canθₛₕ sigs 0 p θ
canθₛₕ-mergeˡ {E} {θ'} {r} {A = A} sigs θ cb p≐E⟦ρθ'r⟧ s' s'∉Domθ' s'∈canθ-sigs←θ'-E⟦r⟧-θ
  rewrite sym (unplug p≐E⟦ρθ'r⟧)
  with binding-extract cb (((E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ∋ plug refl)
... | (BVp , FVp) , (BVp⊆BV , FVp⊆FV) , cbρθ'r@(CBρ cbp)
  with binding-subst cb (((E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ≐ E ⟦ ρ⟨ θ' , A ⟩· r ⟧e) ∋ plug refl) cbρθ'r
                     ((λ _ ()) ,′ (λ _ ()) ,′ (λ _ ()))
                     ((λ _ ()) ,′ (λ _ ()) ,′ (λ _ ()))
                     CBnothing
... | (BV' , FV') , (BVnothin⊆BV , FVnothin⊆FV) , cbnothin
  rewrite canθ'-←-distribute sigs (Env.sig θ') 0 (E ⟦ r ⟧e) θ =
  canθₛₕ-mergeˡ-sigs-induction sigs 0 (Env.sig θ') (Env.shr θ') (Env.var θ') r θ
    ((E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e) ∋ plug refl) cbnothin
    (distinct'-sym
      (dist'++ˡ
        (distinct'-sym
          (proj₁
            (distinct-term-context-help (ρ⟨ θ' , A ⟩· r) E cb cbρθ'r BVp⊆BV cbnothin)))))
    (SharedVar.unwrap s')
    s'∉Domθ' s'∈canθ-sigs←θ'-E⟦r⟧-θ

canθₛ-mergeʳ-add-sig-notin : ∀ sigs' r θ S status →
  S ∉ proj₁ (Dom θ) →
  S ∉ SigMap.keys sigs' →
  ∀ S'' →
    S'' ∈ Canθₛ sigs' 0 r (θ ← [ (S ₛ) ↦ status ]) →
    S'' ∈ Canθₛ sigs' 0 r θ
canθₛ-mergeʳ-add-sig-notin sigs' r θ S status S∉Domθ S∉sigs'
  S'' S''∈canθ-sigs'-r-θ←[S]
  rewrite canθ-is-unknown-lemma sigs' 0 r θ (S ₛ) S∉Domθ
            (subst (S ∉_)
               (sym (map-id (SigMap.keys sigs')))
               S∉sigs')
  = canθₛ-add-sig-monotonic sigs' 0 r θ (S ₛ) status
      S'' S''∈canθ-sigs'-r-θ←[S]

canθₛ-mergeʳ-sigs-induction : ∀ sigs S sigs' r θ →
  distinct' (proj₁ (Dom θ)) (map (_+_ S) (SigMap.keys sigs)) →
  ∀ S'' →
    S'' ∈ proj₁ (Canθ' sigs S (Canθ sigs' 0 r) θ) →
    S'' ∈ proj₁               (Canθ sigs' 0 r θ)
canθₛ-mergeʳ-sigs-induction [] S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  = S''∈canθ'-sigs-canθ-sigs'-r-θ
canθₛ-mergeʳ-sigs-induction (nothing ∷ sigs) S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  = canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ θ≠sigs
      S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
canθₛ-mergeʳ-sigs-induction (just Signal.present ∷ sigs) S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.present θ S∈sigs'
  = canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛ-mergeʳ-add-sig-notin sigs' r θ S Signal.present
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' S''
      (canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env-present (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.present S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env-present (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        S'' S''∈canθ'-sigs-canθ-sigs'-r-θ)
canθₛ-mergeʳ-sigs-induction (just Signal.absent ∷ sigs) S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.absent θ S∈sigs'
  = canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛ-mergeʳ-add-sig-notin sigs' r θ S Signal.absent
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' S''
      (canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env-absent (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.absent S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env-absent (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        S'' S''∈canθ'-sigs-canθ-sigs'-r-θ)
canθₛ-mergeʳ-sigs-induction (just Signal.unknown ∷ sigs) S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  with any (_≟_ S) (proj₁ (Canθ' sigs (suc S) (Canθ sigs' 0 r) (θ ← [S]-env (S ₛ))))
canθₛ-mergeʳ-sigs-induction (just Signal.unknown ∷ sigs) S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  | yes S∈canθ'-sigs-canθ-sigs'-r-θ←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.unknown θ S∈sigs'
  = canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛ-mergeʳ-add-sig-notin sigs' r θ S Signal.unknown
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' S''
      (canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.unknown S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        S'' S''∈canθ'-sigs-canθ-sigs'-r-θ)
canθₛ-mergeʳ-sigs-induction (just Signal.unknown ∷ sigs) S sigs' r θ θ≠sigs
  S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
  | no  S∉canθ'-sigs-canθ-sigs'-r-θ←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.absent θ S∈sigs'
  = canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) S'' S''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛ-mergeʳ-add-sig-notin sigs' r θ S Signal.absent
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' S''
      (canθₛ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env-absent (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.absent S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env-absent (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        S'' S''∈canθ'-sigs-canθ-sigs'-r-θ)

canθₛ-mergeʳ : ∀ sigs θ' r θ →
  distinct' (proj₁ (Dom θ)) (SigMap.keys sigs) →
  ∀ S' →
    Signal.unwrap S' ∈ Canθₛ (SigMap.union sigs (Env.sig θ')) 0 r θ →
    Signal.unwrap S' ∈ Canθₛ (Env.sig θ') 0 r θ
canθₛ-mergeʳ sigs θ' r θ θ≠sigs S' S'∈canθ-sigs←θ'-r-θ
  rewrite canθ'-←-distribute sigs (Env.sig θ') 0 r θ
  = canθₛ-mergeʳ-sigs-induction sigs 0 (Env.sig θ') r θ
      (subst (distinct' _) (sym (map-id (SigMap.keys sigs))) θ≠sigs)
      (Signal.unwrap S') S'∈canθ-sigs←θ'-r-θ

canθₛₕ-mergeʳ-add-sig-notin : ∀ sigs' r θ S status →
  S ∉ proj₁ (Dom θ) →
  S ∉ SigMap.keys sigs' →
  ∀ s'' →
    s'' ∈ Canθₛₕ sigs' 0 r (θ ← [ (S ₛ) ↦ status ]) →
    s'' ∈ Canθₛₕ sigs' 0 r θ
canθₛₕ-mergeʳ-add-sig-notin sigs' r θ S status S∉Domθ S∉sigs'
  s'' s''∈canθ-sigs'-r-θ←[S]
  rewrite canθ-is-unknown-lemma sigs' 0 r θ (S ₛ) S∉Domθ
            (subst (S ∉_)
               (sym (map-id (SigMap.keys sigs')))
               S∉sigs')
  = canθₛₕ-add-sig-monotonic sigs' 0 r θ (S ₛ) status
      s'' s''∈canθ-sigs'-r-θ←[S]

canθₛₕ-mergeʳ-sigs-induction : ∀ sigs S sigs' r θ →
  distinct' (proj₁ (Dom θ)) (map (_+_ S) (SigMap.keys sigs)) →
  ∀ s'' →
    s'' ∈ proj₂ (proj₂ (Canθ' sigs S (Canθ sigs' 0 r) θ)) →
    s'' ∈ proj₂ (proj₂               (Canθ sigs' 0 r θ))
canθₛₕ-mergeʳ-sigs-induction [] S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  = s''∈canθ'-sigs-canθ-sigs'-r-θ
canθₛₕ-mergeʳ-sigs-induction (nothing ∷ sigs) S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  = canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ θ≠sigs
      s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
canθₛₕ-mergeʳ-sigs-induction (just Signal.present ∷ sigs) S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.present θ S∈sigs'
  = canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛₕ-mergeʳ-add-sig-notin sigs' r θ S Signal.present
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' s''
      (canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env-present (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.present S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env-present (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        s'' s''∈canθ'-sigs-canθ-sigs'-r-θ)
canθₛₕ-mergeʳ-sigs-induction (just Signal.absent ∷ sigs) S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.absent θ S∈sigs'
  = canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛₕ-mergeʳ-add-sig-notin sigs' r θ S Signal.absent
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' s''
      (canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env-absent (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.absent S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env-absent (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        s'' s''∈canθ'-sigs-canθ-sigs'-r-θ)
canθₛₕ-mergeʳ-sigs-induction (just Signal.unknown ∷ sigs) S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  with any (_≟_ S) (proj₁ (Canθ' sigs (suc S) (Canθ sigs' 0 r) (θ ← [S]-env (S ₛ))))
canθₛₕ-mergeʳ-sigs-induction (just Signal.unknown ∷ sigs) S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  | yes S∈canθ'-sigs-canθ-sigs'-r-θ←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.unknown θ S∈sigs'
  = canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛₕ-mergeʳ-add-sig-notin sigs' r θ S Signal.unknown
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' s''
      (canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.unknown S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        s'' s''∈canθ'-sigs-canθ-sigs'-r-θ)
canθₛₕ-mergeʳ-sigs-induction (just Signal.unknown ∷ sigs) S sigs' r θ θ≠sigs
  s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
  | no  S∉canθ'-sigs-canθ-sigs'-r-θ←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  with any (_≟_ S) (SigMap.keys sigs')
... | yes S∈sigs'
  rewrite  canθ'-inner-shadowing-irr sigs (suc S) sigs' r S Signal.absent θ S∈sigs'
  = canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r θ
      (dist'++ʳ {V2 = S + 0 ∷ []} θ≠sigs) s'' s''∈canθ'-sigs-canθ-sigs'-r-θ
... | no  S∉sigs'
  rewrite +-comm S 0
  = canθₛₕ-mergeʳ-add-sig-notin sigs' r θ S Signal.absent
      (λ S∈Domθ → θ≠sigs S S∈Domθ (here refl)) S∉sigs' s''
      (canθₛₕ-mergeʳ-sigs-induction sigs (suc S) sigs' r (θ ← [S]-env-absent (S ₛ))
        (λ S'' S''∈Domθ←[S] S''∈map-+-suc-S-sigs → -- TODO: should make this a function
          Data.Sum.[ (λ S''∈Domθ → θ≠sigs S'' S''∈Domθ (there S''∈map-+-suc-S-sigs)) ,
                     (λ S''∈[S] →
                       subst (_∉ _)
                         (sym (Env.sig-single-∈-eq (S'' ₛ) (S ₛ) Signal.absent S''∈[S]))
                         (n∉map-suc-n-+ S (SigMap.keys sigs))
                       S''∈map-+-suc-S-sigs) ]
            (Env.sig-←⁻ {θ} {[S]-env-absent (S ₛ)} (S'' ₛ) S''∈Domθ←[S]))
        s'' s''∈canθ'-sigs-canθ-sigs'-r-θ)

canθₛₕ-mergeʳ : ∀ sigs θ' r θ →
  distinct' (proj₁ (Dom θ)) (SigMap.keys sigs) →
  ∀ s' →
    SharedVar.unwrap s' ∈ Canθₛₕ (SigMap.union sigs (Env.sig θ')) 0 r θ →
    SharedVar.unwrap s' ∈ Canθₛₕ (Env.sig θ') 0 r θ
canθₛₕ-mergeʳ sigs θ' r θ θ≠sigs s' s'∈canθ-sigs←θ'-r-θ
  rewrite canθ'-←-distribute sigs (Env.sig θ') 0 r θ
  = canθₛₕ-mergeʳ-sigs-induction sigs 0 (Env.sig θ') r θ
      (subst (distinct' _) (sym (map-id (SigMap.keys sigs))) θ≠sigs)
      (SharedVar.unwrap s') s'∈canθ-sigs←θ'-r-θ

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------------
-- Conversion rules for the nest function
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Nest.ConversionRulesATP where

open import FOT.FOTC.Program.Nest.NestConditional

open import FOTC.Base

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

postulate nest-0 : nest zero ≡ zero
{-# ATP prove nest-0 #-}

postulate nest-S : ∀ n → nest (succ₁ n) ≡ nest (nest n)
{-# ATP prove nest-S #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Structure.Relator.Function where

import      Lvl
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Functional
open import Structure.Setoid
open import Structure.Setoid.Uniqueness
open import Structure.Relator
open import Type

private variable ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₑ₂ : Lvl.Level

module _ {A : Type{ℓₒ₁}}{B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ (φ : A → B → Stmt{ℓₒ₃}) where
  module _ (f : A → B) where
    record Computable : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₒ₃ Lvl.⊔ ℓₑ₂} where
      constructor intro
      field proof : ∀{x}{y} → (f(x) ≡ y) → φ(x)(y)
    computable = inst-fn Computable.proof

  -- A binary operation is total when every LHS have at least one RHS in which the relation holds.
  record Total : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₒ₃} where
    constructor intro
    field proof : ∀{x} → ∃(y ↦ φ(x)(y))

    compute : A → B
    compute(x) = [∃]-witness(proof{x})

    computableFunction : ⦃ _ : ∀{x} → UnaryRelator(φ(x)) ⦄ → ∃(Computable)
    ∃.witness computableFunction = compute
    Computable.proof (∃.proof computableFunction) {x} eq = substitute₁(φ(x)) eq ([∃]-proof(proof{x}))
  total = inst-fn Total.proof

  -- A binary operation is a function when every LHS have at least one RHS in which the relation holds.
  record Function : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₒ₃ Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : ∀{x} → Unique(φ(x))
  function = inst-fn Function.proof
  -- (∀{x}{y₁ y₂} → φ(x)(y₁) → φ(x)(y₂) → (y₁ ≡ y₂))

  totalFunction : ⦃ _ : Total ⦄ → ⦃ _ : Function ⦄ → (∀{x} → ∃!(φ(x)))
  totalFunction = [∧]-intro total function

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
data   ⊥ : Set where
record ⊤ : Set where

data Bool : Set where
  false : Bool
  true  : Bool

True : Bool → Set
True false = ⊥
True true  = ⊤

Foo : (b : Bool) → True b → Set
Foo true  _  = ⊤
-- The problem rises because I have removed this impossible case.
-- Foo false ()

test : (b : Bool) (t : True b) → Foo b t → ⊤
test true  p x = _
test false p x = _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Testing nested axioms
------------------------------------------------------------------------------

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

module NestedAxioms.B where

open import NestedAxioms.A

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

postulate
  c : D
  b≡c : b ≡ c
{-# ATP axiom b≡c #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module LearnYouAn where
  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

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

  -- if_then_else_ : ∀ { a } → Bool → a → a → a

  data _even : ℕ → Set where
    ZERO : zero even
    STEP : ∀ {x} → x even → suc (suc x) even

  proof₁ : suc (suc (suc (suc zero))) even
  proof₁ = STEP (STEP ZERO)

  proof₂′ : (A : Set) → A → A
  proof₂′ _ x = x

  proof₂ : ℕ → ℕ
  proof₂ = proof₂′ ℕ


text:
{-# OPTIONS --warning=error #-}

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Vectors
open import Semirings.Definition
open import Categories.Definition
open import Orders
open import Categories.Functor.Definition
open import Categories.Examples

module Categories.Category where

postulate
  extensionality : {a b : _} {S : Set a} {T : S → Set b} {f g : (x : S) → T x} → ((x : S) → f x ≡ g x) → f ≡ g

≡Unique : {a : _} {X : Set a} → {a b : X} → (p1 p2 : a ≡ b) → (p1 ≡ p2)
≡Unique refl refl = refl

NatPreorder : Category {lzero} {lzero}
NatPreorder = record { objects = ℕ ; arrows = λ m n → m ≤N n ; id = λ x → inr refl ; _∘_ = λ f g → leqTransitive g f ; rightId = λ x<y → leqUnique (leqTransitive x<y (inr refl)) x<y ; leftId = λ x<y → leqUnique (leqTransitive (inr refl) x<y) x<y ; associative = λ z<=w y<=z x<=y → leqUnique (leqTransitive (leqTransitive x<=y y<=z) z<=w) (leqTransitive x<=y (leqTransitive y<=z z<=w)) }
  where
    leqTransitive : {a b c : ℕ} → (a ≤N b) → (b ≤N c) → (a ≤N c)
    leqTransitive (inl a<b) (inl b<c) = inl (TotalOrder.<Transitive ℕTotalOrder a<b b<c)
    leqTransitive (inl a<b) (inr b=c) rewrite b=c = inl a<b
    leqTransitive (inr a=b) (inl b<c) rewrite a=b = inl b<c
    leqTransitive (inr a=b) (inr b=c) rewrite a=b | b=c = inr refl

    <Nunique : {a b : ℕ} → (p1 p2 : a <N b) → p1 ≡ p2
    <Nunique {a} {b} (le a-b pr1) (le a-b2 pr2) = go a-b pr1 a-b2 pr2 p'
      where
        p : a-b2 +N a ≡ a-b +N a
        p rewrite equalityCommutative pr1 = succInjective pr2
        p' : a-b2 ≡ a-b
        p' = canSubtractFromEqualityRight p
        go : (a-b : ℕ) (pr1 : succ (a-b +N a) ≡ b) (a-b2 : ℕ) (pr2 : succ (a-b2 +N a) ≡ b) (p : a-b2 ≡ a-b) → (le a-b pr1) ≡ (le a-b2 pr2)
        go a-b pr1 a-b2 pr2 eq rewrite eq = applyEquality (λ i → le a-b i) (≡Unique pr1 pr2)

    leqUnique : {a b : ℕ} → (p1 : a ≤N b) → (p2 : a ≤N b) → p1 ≡ p2
    leqUnique (inl a<b) (inl a<b2) = applyEquality inl (<Nunique a<b a<b2)
    leqUnique (inl a<b) (inr a=b) rewrite a=b = exFalso (lessIrreflexive a<b)
    leqUnique (inr a=b) (inl a<b) rewrite a=b = exFalso (lessIrreflexive a<b)
    leqUnique (inr a=b1) (inr a=b2) rewrite a=b1 | a=b2 = refl

NatMonoid : Category {lzero} {lzero}
NatMonoid = record { objects = True ; arrows = λ _ _ → ℕ ; id = λ x → 0 ; _∘_ = λ f g → f +N g ; rightId = λ f → refl ; leftId = λ f → Semiring.sumZeroRight ℕSemiring f ; associative = λ a b c → Semiring.+Associative ℕSemiring a b c }

typeCastCat : {a b c d : _} {C : Category {a} {b}} {D : Category {c} {d}} (F : Functor C D) (G : Functor C D) (S T : Category.objects C) (pr : Functor.onObj F ≡ Functor.onObj G) → Category.arrows D (Functor.onObj G S) (Functor.onObj G T) ≡ Category.arrows D (Functor.onObj F S) (Functor.onObj F T)
typeCastCat F G S T pr rewrite pr = refl

equalityFunctionsEqual : {a b : _} {A : Set a} {B : Set b} (f : A → (B ≡ B)) → (g : A → (B ≡ B)) → (f ≡ g)
equalityFunctionsEqual f g = extensionality λ x → ≡Unique (f x) (g x)

equalityFunctionsEqual' : {a b : _} {A : Set a} {B : Set b} (f : A → (B ≡ B)) → (g : A → (B ≡ B)) → (f ≡ g)
equalityFunctionsEqual' f g = extensionality λ x → ≡Unique (f x) (g x)

functorsEqual' : {a b c d : _} {C : Category {a} {b}} {D : Category {c} {d}} (F : Functor C D) (G : Functor C D) (objEq : (Functor.onObj F) ≡ Functor.onObj G) (arrEq : ∀ {S T : Category.objects C} → {f : Category.arrows C S T} → (Functor.onArrow F {S} {T} f ≡ (typeCast (Functor.onArrow G {S} {T} f) (typeCastCat F G S T objEq)))) → F ≡ G
functorsEqual' record { onObj = onObjF ; onArrow = onArrowF ; mapId = mapIdF ; mapCompose = mapComposeF } record { onObj = onObjG ; onArrow = onArrowG ; mapId = mapIdG ; mapCompose = mapComposeG } prObj prArr rewrite prObj = {!!}

VEC : {a : _} → ℕ → Functor (SET {a}) (SET {a})
VEC {a} n = record { onObj = λ X → Vec X n ; onArrow = λ f → λ v → vecMap f v ; mapId = extensionality mapId' ; mapCompose = λ f g → extensionality λ vec → help f g vec }
  where
    vecMapLemma : {a : _} {T : Set a} {n : ℕ} (v : Vec T n) → vecMap (Category.id SET T) v ≡ v
    vecMapLemma {a} v with inspect (SET {a})
    vecMapLemma {a} v | y with≡ SetCopy = vecMapIdFact (λ i → refl) v
    mapId' : {a : _} {T : Set a} {n : ℕ} → (v : Vec T n) → vecMap (Category.id SET T) v ≡ Category.id SET (Vec T n) v
    mapId' v rewrite vecMapLemma v = refl
    help : ∀ {a n} {X Y Z : Category.objects (SET {a})} (f : X → Y) (g : Y → Z) (vec : Vec X n) → vecMap (λ x → g (f x)) vec ≡ vecMap g (vecMap f vec)
    help f g vec = equalityCommutative (vecMapCompositionFact (λ x → refl) vec)

CATEGORY : {a b : _} → Category {lsuc b ⊔ lsuc a} {b ⊔ a}
CATEGORY {a} {b} = record { objects = Category {a} {b} ; arrows = λ C D → Functor C D ; _∘_ = λ F G → functorCompose F G ; id = λ C → idFunctor C ; rightId = λ F → {!!} ; leftId = λ F → {!!} ; associative = {!!} }
  where
    rightIdFact : {a b c d : _} → {C : Category {a} {b}} {D : Category {c} {d}} (F : Functor C D) → functorCompose (idFunctor D) F ≡ F
    rightIdFact {C = C} {D} F = {!!}


text:
module Oscar.Data.Proposextensequality where

open import Oscar.Data.Proposequality using (_≡_)
open import Oscar.Level

infix 4 _≡̇_
_≡̇_ : ∀ {a} {A : Set a} {b} {B : A → Set b} → ((x : A) → B x) → ((x : A) → B x) → Set (a ⊔ b)
f ≡̇ g = ∀ x → f x ≡ g x


text:
module _ where

open import Agda.Builtin.List
open import Agda.Builtin.Reflection

macro

  easy : Term → TC _
  easy t =
    bindTC (freshName "A") λ A →
    bindTC (declarePostulate (arg (arg-info visible relevant) A)
                             (agda-sort (lit 0))) λ _ →
    unify (def A []) t

B : Set
B = {!easy!}

-- WAS:
-- Parse error
-- ;<ERROR>
-- Example.A...

-- SHOULD: complain that A is not in scope

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- There was a bug which caused the type checker to forget
-- the name of implicit arguments which weren't used in the
-- return type.
module UnusedNamedImplicits where

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

-- Simple example
f : {n m : Nat} -> Nat
f {m = m} = m

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

data Even : Nat -> Set where
  evenZ  : Even zero
  evenSS : {n : Nat} -> Even n -> Even (suc (suc n))

index : {n : Nat} -> Even n -> Nat
index  evenZ     = zero
index (evenSS e) = suc (suc (index e))

sameIndex : {n : Nat}(e : Even n) -> index e == n
sameIndex evenZ = refl
sameIndex (evenSS e) with index e | sameIndex e
... | ._ | refl = refl

-- It could also show up when the argument is used in the top level type,
-- but not by the generated type for the with function.
* : {n : Nat}{e : Even n} -> Even (index e)
* {e = e} with index e | sameIndex e
... | ._ | refl = e

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
-- Andreas, 2018-10-27, issue #3323, reported by Guillaume Brunerie
--
-- Mismatches between original and repeated parameter list
-- should not lead to internal errors.

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record R ..(b : Bool) : Set
record R .b where  -- Cannot change relevance
  field foo : Bool

-- Should fail.


text:
------------------------------------------------------------------------
-- Bag equivalence for lists
------------------------------------------------------------------------

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

open import Equality

module Bag-equivalence
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq hiding (trans)

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id; swap)

open import Bijection eq using (_↔_; module _↔_; Σ-≡,≡↔≡)
open import Equality.Decision-procedures eq
open import Fin eq as Finite
open import Function-universe eq as Function-universe
  hiding (_∘_; Kind; module Kind; bijection)
open import H-level eq
open import H-level.Closure eq
open import Injection eq using (_↣_)
open import List eq
open import Monad eq hiding (map)
open import Nat eq hiding (_≟_)

private
  variable
    a ℓ p q                  : Level
    A B                      : Type a
    P Q                      : A → Type p
    x y z                    : A
    xs xs₁ xs₂ ys ys₁ ys₂ zs : List A
    xss yss                  : List (List A)
    k                        : Function-universe.Kind
    m n                      : ℕ

------------------------------------------------------------------------
-- Any

-- Any.

Any : (A → Type p) → List A → Type p
Any P []       = ⊥
Any P (x ∷ xs) = P x ⊎ Any P xs

-- Alternative definition of Any.

data Any′ {A : Type a} (P : A → Type p) : List A → Type (a ⊔ p) where
  here  : ∀ {x xs} → P x       → Any′ P (x ∷ xs)
  there : ∀ {x xs} → Any′ P xs → Any′ P (x ∷ xs)

-- The two definitions of Any are isomorphic.

Any′-[] : Any′ P [] ↔ ⊥ {ℓ = ℓ}
Any′-[] = record
  { surjection = record
    { logical-equivalence = record
      { from = λ ()
      ; to   = λ ()
      }
    ; right-inverse-of = λ ()
    }
  ; left-inverse-of = λ ()
  }

Any′-∷ : Any′ P (x ∷ xs) ↔ P x ⊎ Any′ P xs
Any′-∷ = record
  { surjection = record
    { logical-equivalence = record
      { from = [ here , there ]
      ; to   = λ where
                 (here p)  → inj₁ p
                 (there p) → inj₂ p
        }
    ; right-inverse-of = [ (λ _ → refl _) , (λ _ → refl _) ]
    }
  ; left-inverse-of = λ where
      (here _)  → refl _
      (there _) → refl _
  }

Any↔Any′ : Any P xs ↔ Any′ P xs
Any↔Any′ {P = P} {xs = []} =
  ⊥          ↔⟨ inverse Any′-[] ⟩
  Any′ P []  □
Any↔Any′ {P = P} {xs = x ∷ xs} =
  P x ⊎ Any P xs   ↔⟨ id ⊎-cong Any↔Any′ {P = P} ⟩
  P x ⊎ Any′ P xs  ↔⟨ inverse Any′-∷ ⟩
  Any′ P (x ∷ xs)  □

------------------------------------------------------------------------
-- Lemmas relating Any to some basic list functions

Any-++ : (P : A → Type p) (xs ys : List A) →
         Any P (xs ++ ys) ↔ Any P xs ⊎ Any P ys
Any-++ P [] ys =
  Any P ys      ↔⟨ inverse ⊎-left-identity ⟩
  ⊥ ⊎ Any P ys  □
Any-++ P (x ∷ xs) ys =
  P x ⊎ Any P (xs ++ ys)       ↔⟨ id ⊎-cong Any-++ P xs ys ⟩
  P x ⊎ (Any P xs ⊎ Any P ys)  ↔⟨ ⊎-assoc ⟩
  (P x ⊎ Any P xs) ⊎ Any P ys  □

Any-concat : (P : A → Type p) (xss : List (List A)) →
             Any P (concat xss) ↔ Any (Any P) xss
Any-concat P []         = id
Any-concat P (xs ∷ xss) =
  Any P (xs ++ concat xss)       ↔⟨ Any-++ P xs (concat xss) ⟩
  Any P xs ⊎ Any P (concat xss)  ↔⟨ id ⊎-cong Any-concat P xss ⟩
  Any P xs ⊎ Any (Any P) xss     □

Any-map : (P : B → Type p) (f : A → B) (xs : List A) →
          Any P (map f xs) ↔ Any (P ∘ f) xs
Any-map P f []       = id
Any-map P f (x ∷ xs) =
  P (f x)   ⊎ Any P (map f xs)  ↔⟨ id ⊎-cong Any-map P f xs ⟩
  (P ∘ f) x ⊎ Any (P ∘ f) xs    □

Any->>= : {A B : Type ℓ}
          (P : B → Type p) (xs : List A) (f : A → List B) →
          Any P (xs >>= f) ↔ Any (Any P ∘ f) xs
Any->>= P xs f =
  Any P (concat (map f xs))  ↔⟨ Any-concat P (map f xs) ⟩
  Any (Any P) (map f xs)     ↔⟨ Any-map (Any P) f xs ⟩
  Any (Any P ∘ f) xs         □

Any-filter : (P : A → Type p) (p : A → Bool) (xs : List A) →
             Any P (filter p xs) ↔ Any (λ x → P x × T (p x)) xs
Any-filter P p []       = ⊥ □
Any-filter P p (x ∷ xs) with p x
... | true  =
   P x      ⊎ Any P (filter p xs)           ↔⟨ inverse ×-right-identity ⊎-cong Any-filter P p xs ⟩
  (P x × ⊤) ⊎ Any (λ x → P x × T (p x)) xs  □
... | false =
  Any P (filter p xs)                       ↔⟨ Any-filter P p xs ⟩
              Any (λ x → P x × T (p x)) xs  ↔⟨ inverse ⊎-left-identity ⟩
  ⊥₀        ⊎ Any (λ x → P x × T (p x)) xs  ↔⟨ inverse ×-right-zero ⊎-cong (_ □) ⟩
  (P x × ⊥) ⊎ Any (λ x → P x × T (p x)) xs  □

------------------------------------------------------------------------
-- List membership

infix 4 _∈_

_∈_ : A → List A → Type _
x ∈ xs = Any (λ y → x ≡ y) xs

-- Any can be expressed using _∈_.

Any-∈ : (P : A → Type p) (xs : List A) →
        Any P xs ↔ ∃ λ x → P x × x ∈ xs
Any-∈ P [] =
  ⊥                  ↔⟨ inverse ×-right-zero ⟩
  (∃ λ x → ⊥₀)       ↔⟨ ∃-cong (λ x → inverse ×-right-zero) ⟩
  (∃ λ x → P x × ⊥)  □
Any-∈ P (x ∷ xs) =
  P x                   ⊎ Any P xs                ↔⟨ ∃-intro P x ⊎-cong Any-∈ P xs ⟩
  (∃ λ y → P y × y ≡ x) ⊎ (∃ λ y → P y × y ∈ xs)  ↔⟨ inverse ∃-⊎-distrib-left ⟩
  (∃ λ y → P y × y ≡ x ⊎ P y × y ∈ xs)            ↔⟨ ∃-cong (λ y → inverse ×-⊎-distrib-left) ⟩
  (∃ λ y → P y × (y ≡ x ⊎ y ∈ xs))                □

-- Using this property we can prove that Any and _⊎_ commute.

Any-⊎ : (P : A → Type p) (Q : A → Type q) (xs : List A) →
        Any (λ x → P x ⊎ Q x) xs ↔ Any P xs ⊎ Any Q xs
Any-⊎ P Q xs =
  Any (λ x → P x ⊎ Q x) xs                         ↔⟨ Any-∈ (λ x → P x ⊎ Q x) xs ⟩
  (∃ λ x → (P x ⊎ Q x) × x ∈ xs)                   ↔⟨ ∃-cong (λ x → ×-⊎-distrib-right) ⟩
  (∃ λ x → P x × x ∈ xs ⊎ Q x × x ∈ xs)            ↔⟨ ∃-⊎-distrib-left ⟩
  (∃ λ x → P x × x ∈ xs) ⊎ (∃ λ x → Q x × x ∈ xs)  ↔⟨ inverse $ Any-∈ P xs ⊎-cong Any-∈ Q xs ⟩
  Any P xs ⊎ Any Q xs                              □

------------------------------------------------------------------------
-- Some lemmas related to list membership

-- If f and g are pointwise equal for elements in xs, then map f xs
-- and map g xs are equal.

map-cong-∈ :
  (f g : A → B) (xs : List A) →
  (∀ {x} → x ∈ xs → f x ≡ g x) →
  map f xs ≡ map g xs
map-cong-∈ p q []       p≡q = refl _
map-cong-∈ p q (x ∷ xs) p≡q =
  cong₂ _∷_ (p≡q (inj₁ (refl _))) (map-cong-∈ p q xs (p≡q ∘ inj₂))

-- If p and q are pointwise equal for elements in xs, then filter p xs
-- and filter q xs are equal.

filter-cong-∈ :
  (p q : A → Bool) (xs : List A) →
  (∀ {x} → x ∈ xs → p x ≡ q x) →
  filter p xs ≡ filter q xs
filter-cong-∈ p q []       p≡q = refl _
filter-cong-∈ p q (x ∷ xs) p≡q
  with p x | q x | p≡q (inj₁ (refl _))
     | filter-cong-∈ p q xs (p≡q ∘ inj₂)
... | true  | true  | _   | ih = cong (x ∷_) ih
... | false | false | _   | ih = ih
... | true  | false | t≡f | _  = ⊥-elim $ Bool.true≢false t≡f
... | false | true  | f≡t | _  = ⊥-elim $ Bool.true≢false $ sym f≡t

-- The ordering of natural numbers can be related to list membership
-- and nats-<.

<-↔-∈-nats-< : m < n ↔ m ∈ nats-< n
<-↔-∈-nats-< {m = m} {n = zero} =
  m < zero         ↝⟨ <zero↔ ⟩
  ⊥                ↔⟨⟩
  m ∈ nats-< zero  □
<-↔-∈-nats-< {m = m} {n = suc n} =
  m < suc n             ↔⟨⟩
  suc m ≤ suc n         ↝⟨ suc≤suc↔ ⟩
  m ≤ n                 ↝⟨ ≤↔<⊎≡ ⟩
  m < n ⊎ m ≡ n         ↝⟨ ⊎-comm ⟩
  m ≡ n ⊎ m < n         ↝⟨ Function-universe.id ⊎-cong <-↔-∈-nats-< ⟩
  m ≡ n ⊎ m ∈ nats-< n  ↔⟨⟩
  m ∈ nats-< (suc n)    □

------------------------------------------------------------------------
-- Bag and set equivalence and the subset and subbag orders

-- Various kinds of relatedness.
--
-- NOTE: Perhaps it would be better to define the subbag property in
-- terms of embeddings, rather than injections. The HoTT book (first
-- edition) claims that injectivity "is an ill-behaved notion for
-- non-sets".

open Function-universe public using (Kind) hiding (module Kind)

module Kind where

  open Function-universe public
    using ()
    renaming ( implication         to subset
             ; logical-equivalence to set
             ; injection           to subbag
             ; bijection           to bag
             ; equivalence         to bag-with-equivalence
             ; equivalenceᴱ        to bag-with-equivalenceᴱ
             )

open Kind public

-- A general definition of "relatedness" for lists.

infix 4 _∼[_]_

_∼[_]_ : {A : Type a} → List A → Kind → List A → Type a
xs ∼[ k ] ys = ∀ z → z ∈ xs ↝[ k ] z ∈ ys

-- Bag equivalence.

infix 4 _≈-bag_

_≈-bag_ : {A : Type a} → List A → List A → Type a
xs ≈-bag ys = xs ∼[ bag ] ys

-- Alternative definition of bag equivalence.

infix 4 _≈-bag′_

record _≈-bag′_ {A : Type a} (xs ys : List A) : Type a where
  field
    bijection : Fin (length xs) ↔ Fin (length ys)
    related   : xs And ys Are-related-by bijection

-- Yet another definition of bag equivalence. This definition is taken
-- from Coq's standard library.

infixr 5 _∷_
infix  4 _≈-bag″_

data _≈-bag″_ {A : Type a} : List A → List A → Type a where
  []    : [] ≈-bag″ []
  _∷_   : ∀ x {xs ys} (xs≈ys : xs ≈-bag″ ys) → x ∷ xs ≈-bag″ x ∷ ys
  swap  : ∀ {x y xs} → x ∷ y ∷ xs ≈-bag″ y ∷ x ∷ xs
  trans : ∀ {xs ys zs}
          (xs≈ys : xs ≈-bag″ ys) (ys≈zs : ys ≈-bag″ zs) → xs ≈-bag″ zs

------------------------------------------------------------------------
-- Some congruence lemmas

Any-cong : (∀ x → P x ↝[ k ] Q x) → xs ∼[ k ] ys →
           Any P xs ↝[ k ] Any Q ys
Any-cong {P = P} {Q = Q} {xs = xs} {ys = ys} P↔Q xs≈ys =
  Any P xs                ↔⟨ Any-∈ P xs ⟩
  (∃ λ z → P z × z ∈ xs)  ↝⟨ ∃-cong (λ z → P↔Q z ×-cong xs≈ys z) ⟩
  (∃ λ z → Q z × z ∈ ys)  ↔⟨ inverse (Any-∈ Q ys) ⟩
  Any Q ys                □

++-cong : xs₁ ∼[ k ] ys₁ → xs₂ ∼[ k ] ys₂ →
          xs₁ ++ xs₂ ∼[ k ] ys₁ ++ ys₂
++-cong {xs₁ = xs₁} {ys₁ = ys₁} {xs₂ = xs₂} {ys₂ = ys₂}
        xs₁∼ys₁ xs₂∼ys₂ = λ z →
  z ∈ xs₁ ++ xs₂     ↔⟨ Any-++ _ xs₁ xs₂ ⟩
  z ∈ xs₁ ⊎ z ∈ xs₂  ↝⟨ xs₁∼ys₁ z ⊎-cong xs₂∼ys₂ z ⟩
  z ∈ ys₁ ⊎ z ∈ ys₂  ↔⟨ inverse (Any-++ _ ys₁ ys₂) ⟩
  z ∈ ys₁ ++ ys₂     □

map-cong : (f : A → B) → xs ∼[ k ] ys → map f xs ∼[ k ] map f ys
map-cong {xs = xs} {ys = ys} f xs∼ys = λ z →
  z ∈ map f xs            ↔⟨ Any-map _ f xs ⟩
  Any (λ x → z ≡ f x) xs  ↝⟨ Any-cong (λ x → z ≡ f x □) xs∼ys ⟩
  Any (λ x → z ≡ f x) ys  ↔⟨ inverse (Any-map _ f ys) ⟩
  z ∈ map f ys            □

concat-cong : xss ∼[ k ] yss → concat xss ∼[ k ] concat yss
concat-cong {xss = xss} {yss = yss} xss∼yss = λ z →
  z ∈ concat xss           ↔⟨ Any-concat _ xss ⟩
  Any (λ zs → z ∈ zs) xss  ↝⟨ Any-cong (λ zs → z ∈ zs □) xss∼yss ⟩
  Any (λ zs → z ∈ zs) yss  ↔⟨ inverse (Any-concat _ yss) ⟩
  z ∈ concat yss           □

>>=-cong : {A B : Type ℓ} {xs ys : List A} {f g : A → List B} →
           xs ∼[ k ] ys → (∀ x → f x ∼[ k ] g x) →
           (xs >>= f) ∼[ k ] (ys >>= g)
>>=-cong {xs = xs} {ys = ys} {f = f} {g = g} xs∼ys f∼g = λ z →
  z ∈ xs >>= f            ↔⟨ Any->>= _ xs f ⟩
  Any (λ x → z ∈ f x) xs  ↝⟨ Any-cong (λ x → f∼g x z) xs∼ys ⟩
  Any (λ x → z ∈ g x) ys  ↔⟨ inverse (Any->>= _ ys g) ⟩
  z ∈ ys >>= g            □

filter-cong : (p : A → Bool) (xs ys : List A) →
              xs ∼[ k ] ys → filter p xs ∼[ k ] filter p ys
filter-cong p xs ys xs∼ys = λ z →
  z ∈ filter p xs                 ↔⟨ Any-filter _ p xs ⟩
  Any (λ x → z ≡ x × T (p x)) xs  ↝⟨ Any-cong (λ _ → _ □) xs∼ys ⟩
  Any (λ x → z ≡ x × T (p x)) ys  ↔⟨ inverse (Any-filter _ p ys) ⟩
  z ∈ filter p ys                 □

------------------------------------------------------------------------
-- More properties

-- Any preserves decidability of equality.

module Dec (dec : ∀ {x} → Decidable-equality (P x)) where

  infix 4 _≟_

  _≟_ : Decidable-equality (Any P xs)
  _≟_ {xs = _ ∷ _} = ⊎.Dec._≟_ dec _≟_

-- If the type of x is a set, then equality is decidable for x ∈ xs.

module Dec-∈ (A-set : Is-set A) where

  infix 4 _≟_

  _≟_ : ∀ {x xs} → Decidable-equality (x ∈ xs)
  _≟_ = Dec._≟_ λ _ _ → yes (A-set _ _)

-- Bind distributes from the left over append.

>>=-left-distributive :
  {A B : Type ℓ} (xs : List A) (f g : A → List B) →
  xs >>= (λ x → f x ++ g x) ≈-bag (xs >>= f) ++ (xs >>= g)
>>=-left-distributive xs f g = λ z →
  z ∈ xs >>= (λ x → f x ++ g x)                    ↔⟨ Any->>= (_≡_ z) xs (λ x → f x ++ g x) ⟩
  Any (λ x → z ∈ f x ++ g x) xs                    ↔⟨ Any-cong (λ x → Any-++ (_≡_ z) (f x) (g x)) (λ _ → id) ⟩
  Any (λ x → z ∈ f x ⊎ z ∈ g x) xs                 ↔⟨ Any-⊎ (λ x → z ∈ f x) (λ x → z ∈ g x) xs ⟩
  Any (λ x → z ∈ f x) xs ⊎ Any (λ x → z ∈ g x) xs  ↔⟨ inverse (Any->>= (_≡_ z) xs f ⊎-cong Any->>= (_≡_ z) xs g) ⟩
  z ∈ xs >>= f ⊎ z ∈ xs >>= g                      ↔⟨ inverse (Any-++ (_≡_ z) (xs >>= f) (xs >>= g)) ⟩
  z ∈ (xs >>= f) ++ (xs >>= g)                     □

-- This property does not hold for ordinary list equality.

¬->>=-left-distributive :
  ¬ ({A B : Type} (xs : List A) (f g : A → List B) →
     xs >>= (λ x → f x ++ g x) ≡ (xs >>= f) ++ (xs >>= g))
¬->>=-left-distributive distrib = Bool.true≢false true≡false
  where
  tf = true ∷ false ∷ []
  f  = λ x → x ∷ []
  g  = f

  ttff≡tftf : true ∷ true ∷ false ∷ false ∷ [] ≡
              true ∷ false ∷ true ∷ false ∷ []
  ttff≡tftf = distrib tf f g

  true≡false : true ≡ false
  true≡false = List.cancel-∷-head (List.cancel-∷-tail ttff≡tftf)

-- _++_ is commutative.

++-comm : (xs ys : List A) → xs ++ ys ≈-bag ys ++ xs
++-comm xs ys = λ z →
  z ∈ xs ++ ys     ↔⟨ Any-++ (_≡_ z) xs ys ⟩
  z ∈ xs ⊎ z ∈ ys  ↔⟨ ⊎-comm ⟩
  z ∈ ys ⊎ z ∈ xs  ↔⟨ inverse (Any-++ (_≡_ z) ys xs) ⟩
  z ∈ ys ++ xs     □

-- _++_ is idempotent (when set equivalence is used).

++-idempotent : (xs : List A) → xs ++ xs ∼[ set ] xs
++-idempotent xs = λ z →
  z ∈ xs ++ xs     ↔⟨ Any-++ (_≡_ z) xs xs ⟩
  z ∈ xs ⊎ z ∈ xs  ↝⟨ ⊎-idempotent ⟩
  z ∈ xs           □

-- The so-called "range splitting" property (see, for instance,
-- Hoogendijks "(Relational) Programming Laws in the Boom Hierarchy of
-- Types").

range-splitting : (p : A → Bool) (xs : List A) →
                  filter p xs ++ filter (not ∘ p) xs ≈-bag xs
range-splitting p xs = λ z →
  z ∈ filter p xs ++ filter (not ∘ p) xs                  ↔⟨ Any-++ _ _ (filter (not ∘ p) xs) ⟩
  z ∈ filter p xs ⊎ z ∈ filter (not ∘ p) xs               ↔⟨ Any-filter _ p xs ⊎-cong Any-filter _ (not ∘ p) xs ⟩
  Any (λ x → z ≡ x × T (p x)) xs ⊎
    Any (λ x → z ≡ x × T (not (p x))) xs                  ↔⟨ inverse $ Any-⊎ _ _ xs ⟩
  Any (λ x → z ≡ x × T (p x) ⊎ z ≡ x × T (not (p x))) xs  ↔⟨ Any-cong (λ x → lemma (z ≡ x) (p x)) (λ x → x ∈ xs □) ⟩
  z ∈ xs                                                  □
  where
  lemma : ∀ {a} (A : Type a) (b : Bool) → A × T b ⊎ A × T (not b) ↔ A
  lemma A b =
    A × T b ⊎ A × T (not b)  ↔⟨ ×-comm ⊎-cong ×-comm ⟩
    T b × A ⊎ T (not b) × A  ↔⟨ if-lemma (λ _ → A) id id b ⟩
    A                        □

-- The so-called "range disjunction" property, strengthened to use the
-- subbag preorder instead of set equivalence.

range-disjunction :
  (p q : A → Bool) (xs : List A) →
  filter (λ x → p x ∨ q x) xs ∼[ subbag ]
  filter p xs ++ filter q xs
range-disjunction p q xs = λ z →
  z ∈ filter (λ x → p x ∨ q x) xs                                  ↔⟨ Any-filter _ (λ x → p x ∨ q x) _ ⟩
  Any (λ x → z ≡ x × T (p x ∨ q x)) xs                             ↝⟨ Any-cong (λ x → lemma (z ≡ x) (p x) (q x)) (λ x → x ∈ xs □) ⟩
  Any (λ x → z ≡ x × T (p x) ⊎ z ≡ x × T (q x)) xs                 ↔⟨ Any-⊎ _ _ _ ⟩
  Any (λ x → z ≡ x × T (p x)) xs ⊎ Any (λ x → z ≡ x × T (q x)) xs  ↔⟨ inverse (Any-filter _ p _ ⊎-cong Any-filter _ q _) ⟩
  z ∈ filter p xs ⊎ z ∈ filter q xs                                ↔⟨ inverse $ Any-++ _ _ _ ⟩
  z ∈ filter p xs ++ filter q xs                                   □
  where
  inj : (b₁ b₂ : Bool) → T (b₁ ∨ b₂) ↣ T b₁ ⊎ T b₂
  inj true  true  = record { to = inj₁; injective = λ _ → refl _  }
  inj true  false = record { to = inj₁; injective = ⊎.cancel-inj₁ }
  inj false true  = record { to = inj₂; injective = ⊎.cancel-inj₂ }
  inj false false = record { to = λ (); injective = λ {}          }

  lemma : ∀ {a} (A : Type a) (b₁ b₂ : Bool) →
          A × T (b₁ ∨ b₂) ↣ A × T b₁ ⊎ A × T b₂
  lemma A b₁ b₂ =
    A × T (b₁ ∨ b₂)      ↝⟨ id ×-cong inj b₁ b₂ ⟩
    A × (T b₁ ⊎ T b₂)    ↔⟨ ×-⊎-distrib-left ⟩
    A × T b₁ ⊎ A × T b₂  □

------------------------------------------------------------------------
-- The first two definitions of bag equivalence above are logically
-- equivalent

-- One direction follows from the following lemma, which states that
-- list membership can be expressed as "there is an index which points
-- to the element".
--
-- As an aside, note that the right-hand side is almost
-- index xs ⁻¹ z.

∈-index : (xs : List A) → z ∈ xs ↔ ∃ λ i → z ≡ index xs i
∈-index {z = z} [] =
  ⊥                               ↔⟨ inverse $ ∃-Fin-zero _ ⟩
  (∃ λ (i : ⊥) → z ≡ index [] i)  □
∈-index {z = z} (x ∷ xs) =
  z ≡ x ⊎ z ∈ xs                    ↔⟨ id ⊎-cong ∈-index xs ⟩
  z ≡ x ⊎ (∃ λ i → z ≡ index xs i)  ↔⟨ inverse $ ∃-Fin-suc _ ⟩
  (∃ λ i → z ≡ index (x ∷ xs) i)    □

-- The index which points to the element.

index-of : z ∈ xs → Fin (length xs)
index-of = proj₁ ∘ _↔_.to (∈-index _)

-- For the other direction a sequence of lemmas is used.

-- The first lemma states that ∃ λ z → z ∈ xs is isomorphic to Fin n,
-- where n is the length of xs. Thierry Coquand pointed out that this
-- is a generalisation of singleton-contractible.

Fin-length : (xs : List A) → (∃ λ z → z ∈ xs) ↔ Fin (length xs)
Fin-length xs =
  (∃ λ z → z ∈ xs)                  ↔⟨ ∃-cong (λ _ → ∈-index xs) ⟩
  (∃ λ z → ∃ λ i → z ≡ index xs i)  ↔⟨ ∃-comm ⟩
  (∃ λ i → ∃ λ z → z ≡ index xs i)  ↔⟨⟩
  (∃ λ i → Singleton (index xs i))  ↔⟨ ∃-cong (λ _ → _⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩
  Fin (length xs) × ⊤               ↔⟨ ×-right-identity ⟩
  Fin (length xs)                   □

-- From this lemma we get that lists which are bag equivalent have
-- related lengths.

Fin-length-cong : xs ≈-bag ys → Fin (length xs) ↔ Fin (length ys)
Fin-length-cong {xs = xs} {ys = ys} xs≈ys =
  Fin (length xs)   ↔⟨ inverse $ Fin-length xs ⟩
  ∃ (λ z → z ∈ xs)  ↔⟨ ∃-cong xs≈ys ⟩
  ∃ (λ z → z ∈ ys)  ↔⟨ Fin-length ys ⟩
  Fin (length ys)   □

abstract

  -- In fact, they have equal lengths.

  length-cong : xs ≈-bag ys → length xs ≡ length ys
  length-cong = _⇔_.to Finite.isomorphic-same-size ∘ Fin-length-cong

  -- All that remains (except for some bookkeeping) is to show that
  -- the isomorphism which Fin-length-cong returns relates the two
  -- lists.

  Fin-length-cong-relates :
    {xs ys : List A} (xs≈ys : xs ≈-bag ys) →
    xs And ys Are-related-by Fin-length-cong xs≈ys
  Fin-length-cong-relates {xs = xs} {ys = ys} xs≈ys i =
    index xs i                                ≡⟨ proj₂ $ to (∈-index _) $ to (xs≈ys _) (from (∈-index _) (i , refl _)) ⟩
    index ys (proj₁ $ to (∈-index _) $
              to (xs≈ys _) $
              from (∈-index _) (i , refl _))  ≡⟨⟩
    index ys (to (Fin-length-cong xs≈ys) i)   ∎
    where open _↔_

-- We get that the two definitions of bag equivalence are logically
-- equivalent.

≈⇔≈′ : xs ≈-bag ys ⇔ xs ≈-bag′ ys
≈⇔≈′ = record
  { to   = λ xs≈ys → record
             { bijection = Fin-length-cong xs≈ys
             ; related   = Fin-length-cong-relates xs≈ys
             }
  ; from = from
  }
  where
  equality-lemma : y ≡ z → (x ≡ y) ↔ (x ≡ z)
  equality-lemma = flip-trans-isomorphism

  from : xs ≈-bag′ ys → xs ≈-bag ys
  from {xs = xs} {ys = ys} xs≈ys z =
    z ∈ xs                    ↔⟨ ∈-index xs ⟩
    ∃ (λ i → z ≡ index xs i)  ↔⟨ Σ-cong (_≈-bag′_.bijection xs≈ys)
                                        (λ i → equality-lemma $
                                                 _≈-bag′_.related xs≈ys i) ⟩
    ∃ (λ i → z ≡ index ys i)  ↔⟨ inverse (∈-index ys) ⟩
    z ∈ ys                    □

------------------------------------------------------------------------
-- Left cancellation

-- We have basically already showed that cons is left cancellative for
-- the (first) alternative definition of bag equivalence.

∷-left-cancellative′ : ∀ xs ys → x ∷ xs ≈-bag′ x ∷ ys → xs ≈-bag′ ys
∷-left-cancellative′ {x = x} xs ys x∷xs≈x∷ys = record
  { bijection = Finite.cancel-suc (_≈-bag′_.bijection x∷xs≈x∷ys)
  ; related   = Finite.cancel-suc-preserves-relatedness x xs ys
                  (_≈-bag′_.bijection x∷xs≈x∷ys)
                  (_≈-bag′_.related x∷xs≈x∷ys)
  }

-- By the equivalence above we get the result also for the first
-- definition of bag equivalence, but we can show this directly, with
-- the help of some lemmas.

abstract

  -- The index-of function commutes with applications of certain
  -- inverses. Note that the last three equational reasoning steps do
  -- not need to be written out; I included them in an attempt to make
  -- it easier to understand why the lemma holds.

  index-of-commutes :
    {xs ys : List A} (xs≈ys : xs ≈-bag ys) (p : z ∈ xs) →
    index-of (_↔_.to (xs≈ys z) p) ≡
    _↔_.to (Fin-length-cong xs≈ys) (index-of p)
  index-of-commutes {z = z} {xs = xs} {ys = ys} xs≈ys p =
    index-of $ to (xs≈ys z) p                                     ≡⟨⟩

    index-of $ proj₂ $ Σ-map P.id (λ {x} → to (xs≈ys x)) (z , p)  ≡⟨ cong (index-of ∘ proj₂ ∘ Σ-map P.id (to (xs≈ys _))) $ sym $
                                                                     left-inverse-of (Fin-length xs) (z , p) ⟩
    index-of $ proj₂ $ Σ-map P.id (λ {x} → to (xs≈ys x)) $
    from (Fin-length xs) $ to (Fin-length xs) (z , p)             ≡⟨⟩

    to (Fin-length ys) $ Σ-map P.id (λ {x} → to (xs≈ys x)) $
    from (Fin-length xs) $ index-of p                             ≡⟨⟩

    to (Fin-length-cong xs≈ys) $ index-of p                       ∎
    where
    open _↔_

  -- Bag equivalence isomorphisms preserve index equality. Note that
  -- this means that, even if the underlying equality is proof
  -- relevant, a bag equivalence isomorphism cannot map two distinct
  -- proofs, that point to the same position, to different positions.

  index-equality-preserved :
    {xs ys : List A} {p q : z ∈ xs}
    (xs≈ys : xs ≈-bag ys) →
    index-of p ≡ index-of q →
    index-of (_↔_.to (xs≈ys z) p) ≡ index-of (_↔_.to (xs≈ys z) q)
  index-equality-preserved {z = z} {p = p} {q = q} xs≈ys eq =
    index-of (_↔_.to (xs≈ys z) p)                ≡⟨ index-of-commutes xs≈ys p ⟩
    _↔_.to (Fin-length-cong xs≈ys) (index-of p)  ≡⟨ cong (_↔_.to (Fin-length-cong xs≈ys)) eq ⟩
    _↔_.to (Fin-length-cong xs≈ys) (index-of q)  ≡⟨ sym $ index-of-commutes xs≈ys q ⟩∎
    index-of (_↔_.to (xs≈ys z) q)                ∎

-- If x ∷ xs is bag equivalent to x ∷ ys, then xs and ys are bag
-- equivalent.

∷-left-cancellative : x ∷ xs ≈-bag x ∷ ys → xs ≈-bag ys
∷-left-cancellative {x = x} x∷xs≈x∷ys z =
  ⊎-left-cancellative
    (x∷xs≈x∷ys z)
    (lemma x∷xs≈x∷ys)
    (lemma (inverse ∘ x∷xs≈x∷ys))
  where
  abstract

    -- If the equality type is proof irrelevant (so that p and q are
    -- equal), then this lemma can be proved without the help of
    -- index-equality-preserved.

    lemma : (inv : x ∷ xs ≈-bag x ∷ ys) →
            Well-behaved (_↔_.to (inv z))
    lemma {xs = xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ =
      ⊎.inj₁≢inj₂ (
        fzero                                   ≡⟨⟩
        index-of {xs = x ∷ xs} (inj₁ p)         ≡⟨ cong index-of $ sym $ to-from hyp₂ ⟩
        index-of {xs = x ∷ xs} (from (inj₁ q))  ≡⟨ index-equality-preserved (inverse ∘ inv) (refl _) ⟩
        index-of {xs = x ∷ xs} (from (inj₁ p))  ≡⟨ cong index-of $ to-from hyp₁ ⟩
        index-of {xs = x ∷ xs} (inj₂ z∈xs)      ≡⟨⟩
        fsuc (index-of {xs = xs} z∈xs)          ∎)
      where open _↔_ (inv z)

-- Cons is not left cancellative for set equivalence.

∷-not-left-cancellative :
  ¬ (∀ {A : Type} {x : A} {xs ys} →
     x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
∷-not-left-cancellative cancel =
  _⇔_.to (cancel (++-idempotent (tt ∷ [])) tt) (inj₁ (refl _))

-- _++_ is left and right cancellative (for bag equivalence).

++-left-cancellative :
  ∀ xs → xs ++ ys ≈-bag xs ++ zs → ys ≈-bag zs
++-left-cancellative []       eq = eq
++-left-cancellative (x ∷ xs) eq =
  ++-left-cancellative xs (∷-left-cancellative eq)

++-right-cancellative : xs ++ zs ≈-bag ys ++ zs → xs ≈-bag ys
++-right-cancellative {xs = xs} {zs = zs} {ys = ys} eq =
  ++-left-cancellative zs (λ z →
    z ∈ zs ++ xs  ↔⟨ ++-comm zs xs z ⟩
    z ∈ xs ++ zs  ↔⟨ eq z ⟩
    z ∈ ys ++ zs  ↔⟨ ++-comm ys zs z ⟩
    z ∈ zs ++ ys  □)

------------------------------------------------------------------------
-- The third definition of bag equivalence is sound with respect to
-- the other two

-- _∷_ preserves _∼[ k ]_.

infixr 5 _∷-cong_

_∷-cong_ : x ≡ y → xs ∼[ k ] ys → x ∷ xs ∼[ k ] y ∷ ys
_∷-cong_ {x = x} {y = y} {xs = xs} {ys = ys} x≡y xs≈ys = λ z →
  z ≡ x ⊎ z ∈ xs  ↝⟨ from-bijection (flip-trans-isomorphism x≡y) ⊎-cong xs≈ys z ⟩□
  z ≡ y ⊎ z ∈ ys  □

-- We can swap the first two elements of a list.

swap-first-two : x ∷ y ∷ xs ≈-bag y ∷ x ∷ xs
swap-first-two {x = x} {y = y} {xs = xs} = λ z →
   z ≡ x ⊎ z ≡ y  ⊎ z ∈ xs  ↔⟨ ⊎-assoc ⟩
  (z ≡ x ⊎ z ≡ y) ⊎ z ∈ xs  ↔⟨ ⊎-comm ⊎-cong id ⟩
  (z ≡ y ⊎ z ≡ x) ⊎ z ∈ xs  ↔⟨ inverse ⊎-assoc ⟩
   z ≡ y ⊎ z ≡ x  ⊎ z ∈ xs  □

-- The third definition of bag equivalence is sound with respect to
-- the first one.

≈″⇒≈ : xs ≈-bag″ ys → xs ≈-bag ys
≈″⇒≈ []                  = λ _ → id
≈″⇒≈ (x ∷ xs≈ys)         = refl _ ∷-cong ≈″⇒≈ xs≈ys
≈″⇒≈ swap                = swap-first-two
≈″⇒≈ (trans xs≈ys ys≈zs) = λ z → _ ↔⟨ ≈″⇒≈ xs≈ys z ⟩ ≈″⇒≈ ys≈zs z

-- The other direction should also be provable, but I expect that this
-- requires some work.

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Numeric.Nat.Prime.Properties where

open import Prelude
open import Control.WellFounded
open import Numeric.Nat.Properties
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.GCD
open import Numeric.Nat.GCD.Extended
open import Numeric.Nat.GCD.Properties
open import Numeric.Nat.Prime
open import Tactic.Nat

prime-nonzero : ∀ {p} → Prime p → NonZero p
prime-nonzero {0} (prime p>1 _) = refute p>1
prime-nonzero {suc _} _ = _

prime-coprime/divide : ∀ p a → Prime p → Either (Coprime p a) (p Divides a)
prime-coprime/divide p a (prime _ isp) with gcd p a
prime-coprime/divide p a (prime _ isp) | gcd-res d isGCD =
  case isp d (IsGCD.d|a isGCD) of λ where
    (left d=1)   → left  d=1
    (right refl) → right (IsGCD.d|b isGCD)

prime-divide-prime : ∀ {p q} → Prime p → Prime q → p Divides q → p ≡ q
prime-divide-prime {p} (prime p>1 _) (prime _ dq) p|q =
  case dq p p|q of λ where
    (left refl) → refute p>1
    (right p=q) → p=q

prime-split : ∀ {p} a b → Prime p → p Divides (a * b) → Either (p Divides a) (p Divides b)
prime-split a b isP p|ab =
  case prime-coprime/divide _ a isP of λ where
    (left p/a)  → right (coprime-divide-mul-l _ a b p/a p|ab)
    (right p|a) → left p|a

-- It's enough to check prime divisors when checking coprimality.
module _ (a b : Nat) (f : ∀ p → Prime p → p Divides a → p Divides b → p Divides 1) where

  private
    coprimeByPrimes′ : (k : Nat) → Acc _<_ k → k Divides a → k Divides b → k Divides 1
    coprimeByPrimes′ k (acc wf) k|a k|b =
      case isPrime k of λ where
        (yes isP) → f k isP k|a k|b
        (no (composite i j i>1 j>1 refl)) →
          let i|1 : i Divides 1
              i|1 = coprimeByPrimes′ i (wf i (less-mul-l i>1 j>1))
                                       (mul-divides-l i j a k|a) (mul-divides-l i j b k|b)
              j|1 : j Divides 1
              j|1 = coprimeByPrimes′ j (wf j (less-mul-r i>1 j>1))
                                       (mul-divides-r i j a k|a) (mul-divides-r i j b k|b)
          in case₂ divides-one i|1 , divides-one j|1 of λ where
               refl refl → factor! 1
        (tiny (diff! 0)) → factor! 1
        (tiny (diff! 1)) →
          case₂ divides-zero k|a , divides-zero k|b of λ where
            refl refl →
              let 2∤1 = fromDec (2 divides? 1)
                  2|0 = fromDec (2 divides? 0) in
              ⊥-elim (2∤1 (f 2 (fromDec (decPrime 2)) 2|0 2|0))
        (tiny (diff (suc (suc _)) eq)) → refute eq

  coprimeByPrimes : Coprime a b
  coprimeByPrimes = coprimeByDivide a b λ k → coprimeByPrimes′ k (wfNat k)

coprime-mul-r : ∀ a b c → Coprime a b → Coprime a c → Coprime a (b * c)
coprime-mul-r a b c a/b a/c =
  coprimeByPrimes a (b * c) λ p isP p|a p|bc →
  case prime-split b c isP p|bc of λ where
    (left  p|b) → divide-coprime p a b a/b p|a p|b
    (right p|c) → divide-coprime p a c a/c p|a p|c

coprime-mul-l : ∀ a b c → Coprime a c → Coprime b c → Coprime (a * b) c
coprime-mul-l a b c a/c b/c =
  coprime-sym c _ (coprime-mul-r c a b (coprime-sym a _ a/c) (coprime-sym b _ b/c))

prime-divide-coprime : ∀ p a b → Prime p → Coprime a b → p Divides a → p Divides b → ⊥
prime-divide-coprime p a b isP a/b p|a p|b =
  case divides-one {p} (divide-coprime p a b a/b p|a p|b) of λ where
    refl → fromDec (decPrime 1) isP

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:
open import Agda.Builtin.Bool public
open import Agda.Builtin.Nat public

data IsTrue : Bool → Set where
  instance truth : IsTrue true

postulate
  foo : {{IsTrue (3 < 2)}} → Nat

test : Nat
test = foo

max_forks_repo_name: shlevy/agda


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Naturals.Order.WellFounded
open import Orders.WellFounded.Induction
open import Orders.Total.Definition
open import Semirings.Definition

module Numbers.Naturals.Division where

open import Numbers.Naturals.EuclideanAlgorithm public using (_∣_ ; zeroDividesNothing ; divisionAlgResult ; divides ; biggerThanCantDivide ; aDivA ; aDivZero ; divEquality ; oneDivN ; dividesBothImpliesDividesSum ; dividesBothImpliesDividesDifference)

divOneImpliesOne : {a : ℕ} → a ∣ 1 → a ≡ 1
divOneImpliesOne {zero} a|1 = exFalso (zeroDividesNothing _ a|1)
divOneImpliesOne {succ zero} a|1 = refl
divOneImpliesOne {succ (succ a)} (divides record { quot = zero ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | multiplicationNIsCommutative a 0 = exFalso (naughtE pr)
divOneImpliesOne {succ (succ a)} (divides record { quot = (succ quot) ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite Semiring.commutative ℕSemiring quot (succ (quot +N a *N succ quot)) = exFalso (naughtE (equalityCommutative (succInjective pr)))


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.PeifferGraph 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.ReflGraph

open GroupLemmas
open MorphismLemmas

private
  variable
    ℓ ℓ' : Level

module _ (𝒢 : ReflGraph ℓ ℓ') where
  open ReflGraphNotation 𝒢

  ----------------------------------------------------
  -- The peiffer condition for reflexive graphs,
  -- i.e. the missing property to turn a precrossed
  -- module into a crossed module
  ----------------------------------------------------
  isPeifferGraph : Type ℓ'
  isPeifferGraph = (a b : ⟨ G₁ ⟩) → ((is b +₁ (a -₁ it a)) +₁ (-is b +₁ b)) +₁ it a ≡ b +₁ a

  -- G₁ is a set, so isPeifferGraph is a proposition
  isPropIsPeifferGraph : isProp isPeifferGraph
  isPropIsPeifferGraph = isPropΠ2 (λ a b → set₁ (((is b +₁ (a -₁ it a)) +₁ (-is b +₁ b)) +₁ it a) (b +₁ a))

  ---------------------------------------------------
  -- lemmas about the peiffer graphs
  ---------------------------------------------------
  module _ (isPeifferG : isPeifferGraph) where
   abstract
     -- the peiffer condition can be simplified to this
     isPeifferGraph2 : (a b : ⟨ G₁ ⟩) → (a -₁ it a) +₁ (-is b +₁ b) ≡ (-is b +₁ (b +₁ a)) -₁ it a
     isPeifferGraph2 a b = (a -₁ ita) +₁ (-isb +₁ b)
                              ≡⟨ sym (lCancel-lId G₁ isb ((a -₁ ita) +₁ (-isb +₁ b)))
                                 ∙ sym (rCancel-rId G₁ ((-isb +₁ isb) +₁ ((a -₁ ita) +₁ (-isb +₁ b))) ita) ⟩
                           ((-isb +₁ isb) +₁ ((a -₁ ita) +₁ (-isb +₁ b))) +₁ (ita -₁ ita)
                              ≡⟨ assoc₁ ((-isb +₁ isb) +₁ ((a -₁ ita) +₁ (-isb +₁ b))) ita -ita ⟩
                           (((-isb +₁ isb) +₁ ((a -₁ ita) +₁ (-isb +₁ b))) +₁ ita) +₁ -ita
                              ≡⟨ cong (λ z → (z +₁ ita) -₁ ita)
                                      (sym (assoc₁ -isb isb _)) ⟩
                           ((-isb +₁ (isb +₁ ((a -₁ ita) +₁ (-isb +₁ b)))) +₁ ita) +₁ -ita
                              ≡⟨ cong (λ z → ((-isb +₁ z) +₁ ita) +₁ -ita)
                                      (assoc₁ _ _ _) ⟩
                           ((-isb +₁ ((isb +₁ (a -₁ ita)) +₁ (-isb +₁ b))) +₁ ita) +₁ -ita
                              ≡⟨ cong (_+₁ -ita)
                                      (sym (assoc₁ -isb _ ita)) ⟩
                           (-isb +₁ (((isb +₁ (a -₁ ita)) +₁ (-isb +₁ b)) +₁ ita)) -₁ ita
                             ≡⟨ cong (λ z → (-isb +₁ z) -₁ ita)
                                     (isPeifferG a b) ⟩
                           (-isb +₁ (b +₁ a)) -₁ ita ∎
                           where
                             -a = -₁ a
                             -ita = -it a
                             ita = it a
                             isb = is b
                             -isb = -is b
                             -b = -₁ b

     -- inverting both sides of the identity isPeifferGraph2 and simplifying
     -- gives this
     isPeifferGraph3 : (a b : ⟨ G₁ ⟩) → (-₁ b) +₁ (is b +₁ (it a -₁ a)) ≡ it a +₁ ((-₁ a) +₁ ((-₁ b) +₁ is b))
     isPeifferGraph3 a b = -b +₁ (isb +₁ (ita -₁ a))
                              ≡⟨ cong (λ z → -b +₁ (z +₁ (ita -₁ a)))
                                      (sym (invInvo G₁ isb))
                                 ∙ cong (λ z → -b +₁ ((-₁ -isb) +₁ (z -₁ a)))
                                        (sym (invInvo G₁ ita)) ⟩
                           -b +₁ ((-₁ -isb) +₁ ((-₁ -ita) -₁ a))
                              ≡⟨ sym (invDistr₄ G₁ a -ita -isb b) ⟩
                           -₁ (((a +₁ -ita) +₁ -isb) +₁ b)
                              ≡⟨ cong -₁_ (sym (assoc₁ _ -isb b)) ⟩
                           -₁ ((a -₁ ita) +₁ (-isb +₁ b))
                             ≡⟨ cong -₁_ (isPeifferGraph2 a b) ⟩
                           -₁ ((-isb +₁ (b +₁ a)) -₁ ita)
                             ≡⟨ cong (λ z → -₁ (z -₁ ita)) (assoc₁ -isb b a) ⟩
                           -₁ (((-isb +₁ b) +₁ a) -₁ ita)
                             ≡⟨ invDistr₄ G₁ -isb b a -ita ⟩
                           (-₁ -ita) +₁ (-a +₁ (-b +₁ (-₁ -isb)))
                             ≡⟨ cong (_+₁ (-a +₁ (-b +₁ (-₁ -isb))))
                                     (invInvo G₁ ita)
                                ∙ cong (λ z → ita +₁ (-a +₁ (-b +₁ z)))
                                       (invInvo G₁ isb) ⟩
                           ita +₁ (-a +₁ (-b +₁ isb)) ∎
                           where
                             -a = -₁ a
                             -ita = -₁ (it a)
                             ita = it a
                             isb = is b
                             -isb = -₁ isb
                             -b = -₁ b

     -- plugging -a and -b into isPeifferGraph4 gives this
     isPeifferGraph4 : (a b : ⟨ G₁ ⟩) → b +₁ ((-₁ (is b)) +₁ ((-₁ (it a)) +₁ a)) ≡ (-₁ (it a)) +₁ (a +₁ (b -₁ (is b)))
     isPeifferGraph4 a b = b +₁ (-isb +₁ (-ita +₁ a))
                             ≡⟨ cong (_+₁ (-isb +₁ (-ita +₁ a)))
                                     (sym (invInvo G₁ b)) ⟩
                           (-₁ -b) +₁ (-isb +₁ (-ita +₁ a))
                             ≡⟨ cong (λ z → (-₁ -b) +₁ (-isb +₁ (-ita +₁ z)))
                                     (sym (invInvo G₁ a)) ⟩
                           (-₁ -b) +₁ (-isb +₁ (-ita -₁ -a))
                             ≡⟨ cong (λ z → (-₁ -b) +₁ (-isb +₁ (z -₁ -a))) (sym (mapInv ι∘τ a)) ⟩
                           (-₁ -b) +₁ (-isb +₁ ((it -a) -₁ -a))
                             ≡⟨ cong (λ z → (-₁ -b) +₁ (z +₁ ((it -a) -₁ -a))) (sym (mapInv ι∘σ b)) ⟩
                           (-₁ -b) +₁ (is -b +₁ ((it -a) -₁ -a))
                             ≡⟨ isPeifferGraph3 -a -b ⟩
                           it -a +₁ ((-₁ -a) +₁ ((-₁ -b) +₁ is -b))
                             ≡⟨ cong (_+₁ ((-₁ -a) +₁ ((-₁ -b) +₁ is -b)))
                                     (mapInv ι∘τ a) ⟩
                           -ita +₁ ((-₁ -a) +₁ ((-₁ -b) +₁ is -b))
                             ≡⟨ cong (λ z → -ita +₁ (z +₁ ((-₁ -b) +₁ is -b)))
                                     (invInvo G₁ a) ⟩
                           -ita +₁ (a +₁ ((-₁ -b) +₁ is -b))
                             ≡⟨ cong (λ z → -ita +₁ (a +₁ (z +₁ is -b)))
                                     (invInvo G₁ b) ⟩
                           -ita +₁ (a +₁ (b +₁ is -b))
                             ≡⟨ cong (λ z → -ita +₁ (a +₁ (b +₁ z)))
                                     (mapInv ι∘σ b) ⟩
                           -ita +₁ (a +₁ (b -₁ isb)) ∎
                           where
                             -a = -₁ a
                             -ita = -it a
                             isb = is b
                             -isb = -is b
                             -b = -₁ b

-----------------------------------------------
-- URG structure on the type of peiffer graphs
--
--   isPeifferGraph
--        |
--    ReflGraph
-----------------------------------------------

module _ (ℓ ℓ' : Level) where
  private
    ℓℓ' = ℓ-max ℓ ℓ'

  𝒮ᴰ-ReflGraph\Peiffer : URGStrᴰ (𝒮-ReflGraph ℓ ℓℓ')
                                 (λ 𝒢 → isPeifferGraph 𝒢)
                                 ℓ-zero
  𝒮ᴰ-ReflGraph\Peiffer = Subtype→Sub-𝒮ᴰ (λ 𝒢 → isPeifferGraph 𝒢 , isPropIsPeifferGraph 𝒢)
                                        (𝒮-ReflGraph ℓ ℓℓ')

  PeifferGraph : Type (ℓ-suc ℓℓ')
  PeifferGraph = Σ[ 𝒢 ∈ ReflGraph ℓ ℓℓ' ] isPeifferGraph 𝒢

  𝒮-PeifferGraph : URGStr PeifferGraph ℓℓ'
  𝒮-PeifferGraph = ∫⟨ 𝒮-ReflGraph ℓ ℓℓ' ⟩ 𝒮ᴰ-ReflGraph\Peiffer

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
open import FRP.JS.Behaviour using ( Beh ; [_] ; map ; accumHoldBy )
open import FRP.JS.Event using ( Evt ; tag )
open import FRP.JS.DOM using ( DOM ; element ; text ; listen ; click ; _++_ ; element+ ; _+++_ )
open import FRP.JS.RSet using ( RSet ; ⟦_⟧ ; ⟨_⟩ ; _⇒_ )
open import FRP.JS.Nat using ( ℕ ; _+_ ; _*_ ; _∸_ ; show )
open import FRP.JS.Time using ( Time )
open import FRP.JS.String using ( String )
open import FRP.JS.Bool using ( Bool ; true ; false )
open import FRP.JS.Product using ( _∧_ ; _,_ )

module FRP.JS.Demo.Calculator.Model where

data Op : Set where
  plus minus times eq : Op

data Button : Set where
  digit : ℕ → Button
  op : Op → Button
  clear : Button

data State : Set where
  state : ℕ → ℕ → Bool → Op → State

init : State
init = state 0 0 false eq

eval : ℕ → Op → ℕ → ℕ
eval m plus  n = m + n
eval m minus n = m ∸ n
eval m times n = m * n
eval m eq    n = n

step : State → Button → State
step (state m n true  p) (digit d) = state m (n * 10 + d) true  p
step (state m n false p) (digit d) = state n d            true  p
step (state m n true  p) (op q)    = state n (eval m p n) false q
step (state m n false p) (op q)    = state m (eval m p n) false q
step (state m n b     p) clear     = state 0 0            false eq

button$ : Button → String
button$ (digit d)   = show d
button$ (op plus)   = "+"
button$ (op minus)  = "-"
button$ (op times)  = "×"
button$ (op eq)     = "="
button$ clear       = "C"

state$ : State → String
state$ (state m n b p) = show n

model : ⟦ Evt ⟨ Button ⟩ ⇒ Beh ⟨ State ⟩ ⟧
model = accumHoldBy step init

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:
module _ where

open import DeadCodePatSyn.Lib

-- Check that pattern synonyms count when computing dead code
f : _ → Set₁
f not-hidden = Set


text:
module Eq where

  import Prelude
  open Prelude

  abstract
    data _=^=_ {a : Set} (x y : a) : Set1 where
      leibniz : ((P : a -> Set) -> P x <-> P y) -> x =^= y

    leibnizSubst :  {a : Set} -> {x y : a}
                 -> x =^= y -> (P : a -> Set) -> P x -> P y
    leibnizSubst (leibniz f) P p = iffLeft (f P) p

    leibnizRefl : {a : Set} -> {x : a} -> x =^= x
    leibnizRefl = leibniz (\_ -> iff id id)

    leibnizSym : {a : Set} -> {x y : a} -> x =^= y -> y =^= x
    leibnizSym (leibniz f) =
      leibniz (\P -> iff (iffRight (f P)) (iffLeft (f P)))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Maybes where one of the elements satisfies a given property
------------------------------------------------------------------------

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

module Data.Maybe.Relation.Unary.Any where

open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Product as Prod using (∃; _,_; -,_)
open import Function using (id)
open import Function.Equivalence using (_⇔_; equivalence)
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_; cong)
open import Relation.Unary
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

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

data Any {a p} {A : Set a} (P : Pred A p) : Pred (Maybe A) (a ⊔ p) where
  just : ∀ {x} → P x → Any P (just x)

------------------------------------------------------------------------
-- Basic operations

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

  drop-just : ∀ {x} → Any P (just x) → P x
  drop-just (just px) = px

  just-equivalence : ∀ {x} → P x ⇔ Any P (just x)
  just-equivalence = equivalence just drop-just

  map : ∀ {q} {Q : Pred A q} → P ⊆ Q → Any P ⊆ Any Q
  map f (just px) = just (f px)

  satisfied : ∀ {x} → Any P x → ∃ P
  satisfied (just p) = -, p

------------------------------------------------------------------------
-- (un/)zip(/With)

module _ {a p q r} {A : Set a} {P : Pred A p} {Q : Pred A q} {R : Pred A r} where

  zipWith : P ∩ Q ⊆ R → Any P ∩ Any Q ⊆ Any R
  zipWith f (just px , just qx) = just (f (px , qx))

  unzipWith : P ⊆ Q ∩ R → Any P ⊆ Any Q ∩ Any R
  unzipWith f (just px) = Prod.map just just (f px)

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  zip : Any P ∩ Any Q ⊆ Any (P ∩ Q)
  zip = zipWith id

  unzip : Any (P ∩ Q) ⊆ Any P ∩ Any Q
  unzip = unzipWith id

------------------------------------------------------------------------
-- Seeing Any as a predicate transformer

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

  dec : Decidable P → Decidable (Any P)
  dec P-dec nothing  = no λ ()
  dec P-dec (just x) = Dec.map just-equivalence (P-dec x)

  irrelevant : Irrelevant P → Irrelevant (Any P)
  irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q)

  satisfiable : Satisfiable P → Satisfiable (Any P)
  satisfiable P-satisfiable = Prod.map just just P-satisfiable


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatPlusOne.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne.Base

open import Cubical.Reflection.StrictEquiv

1+Path : ℕ ≡ ℕ₊₁
1+Path = ua e
  where
  unquoteDecl e = declStrictEquiv e 1+_ -1+_

ℕ₊₁→ℕ-inj : ∀ {m n} → ℕ₊₁→ℕ m ≡ ℕ₊₁→ℕ n → m ≡ n
ℕ₊₁→ℕ-inj p i = 1+ (injSuc p i)

infixl 7 _·₊₁_

_·₊₁_ : ℕ₊₁ → ℕ₊₁ → ℕ₊₁
(1+ m) ·₊₁ (1+ n) = 1+ (n + m · (suc n))

private
  ℕ₊₁→ℕ-·₊₁-comm : ∀ m n → ℕ₊₁→ℕ (m ·₊₁ n) ≡ (ℕ₊₁→ℕ m) · (ℕ₊₁→ℕ n)
  ℕ₊₁→ℕ-·₊₁-comm (1+ m) (1+ n) = refl

·₊₁-comm : ∀ m n → m ·₊₁ n ≡ n ·₊₁ m
·₊₁-comm (1+ m) (1+ n) = cong 1+_ (injSuc (·-comm (suc m) (suc n)))

·₊₁-assoc : ∀ m n o → m ·₊₁ (n ·₊₁ o) ≡ m ·₊₁ n ·₊₁ o
·₊₁-assoc (1+ m) (1+ n) (1+ o) = cong 1+_ (injSuc (·-assoc (suc m) (suc n) (suc o)))

·₊₁-identityˡ : ∀ n → 1 ·₊₁ n ≡ n
·₊₁-identityˡ (1+ n) = cong 1+_ (injSuc (·-identityˡ (suc n)))

·₊₁-identityʳ : ∀ n → n ·₊₁ 1 ≡ n
·₊₁-identityʳ (1+ n) = cong 1+_ (injSuc (·-identityʳ (suc n)))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- Quotients of additive categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Additive.Quotient where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Categories.Additive.Base
open import Cubical.Categories.Additive.Properties
open import Cubical.Categories.Category.Base
open import Cubical.Categories.Constructions.Quotient
open import Cubical.Categories.Limits.Terminal
open import Cubical.Foundations.Prelude
open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)

private
  variable
    ℓ ℓ' ℓq : Level

-- Quotients of preadditive categories
module _ (C : PreaddCategory ℓ ℓ') where
  open PreaddCategory C
  open PreaddCategoryTheory C

  module _ (_~_ : {x y : ob} (f g : Hom[ x , y ] ) → Type ℓq)
           (~refl : {x y : ob} (f : Hom[ x , y ] ) → f ~ f)
           (~cong⋆ : {x y z : ob}
                     (f f' : Hom[ x , y ]) → f ~ f'
                   → (g g' : Hom[ y , z ]) → g ~ g'
                   → (f ⋆ g) ~ (f' ⋆ g'))
           (~cong+ : {x y : ob} (f f' g g' : Hom[ x , y ])
                   → f ~ f' → g ~ g' → (f + g) ~ (f' + g'))
           (~cong- : {x y : ob} (f f' : Hom[ x , y ])
                   → f ~ f' → (- f) ~ (- f'))           where

    private
      C/~ = QuotientCategory cat _~_ ~refl ~cong⋆
      Hom[_,_]/~ = λ (x y : ob) → (Hom[ x , y ]) / _~_
      _⋆/~_ = C/~ .Category._⋆_

      _+/~_ : {x y : ob} (f g : Hom[ x , y ]/~) → Hom[ x , y ]/~
      _+/~_ = setQuotBinOp ~refl ~refl _+_ ~cong+

    -- Quotient group structure on homsets
    private
      open AbGroupStr renaming (_+_ to add; -_ to inv)
      homAbStr/~ : (x y : ob) → AbGroupStr Hom[ x , y ]/~
      homAbStr/~ x y .0g        = ⟦ 0h ⟧
      homAbStr/~ x y .add       = _+/~_
      homAbStr/~ x y .inv       = (setQuotUnaryOp -_ ~cong-)
      homAbStr/~ x y .isAbGroup = makeIsAbGroup squash/
          (elimProp3 (λ _ _ _ → squash/ _ _)  λ _ _ _ → cong ⟦_⟧ (+assoc _ _ _))
          (elimProp  (λ _     → squash/ _ _)  λ _     → cong ⟦_⟧ (+idr _))
          (elimProp  (λ _     → squash/ _ _)  λ _     → cong ⟦_⟧ (+invr _))
          (elimProp2 (λ _ _   → squash/ _ _)  λ _ _   → cong ⟦_⟧ (+comm _ _))

    -- Distributivity
    ⋆distl+/~ : {x y z : ob} → (f : Hom[ x , y ]/~) → (g g' : Hom[ y , z ]/~) →
        f  ⋆/~  (g  +/~  g')  ≡  (f  ⋆/~  g)  +/~  (f  ⋆/~  g')
    ⋆distl+/~ = elimProp3 (λ _ _ _ → squash/ _ _) λ _ _ _ → cong ⟦_⟧ (⋆distl+ _ _ _)

    ⋆distr+/~ : {x y z : ob} → (f f' : Hom[ x , y ]/~) → (g : Hom[ y , z ]/~) →
        (f  +/~  f')  ⋆/~  g  ≡  (f  ⋆/~  g)  +/~  (f'  ⋆/~  g)
    ⋆distr+/~ = elimProp3 (λ _ _ _ → squash/ _ _) λ _ _ _ → cong ⟦_⟧ (⋆distr+ _ _ _)

    -- Quotient of preadditive category
    open PreaddCategory
    open PreaddCategoryStr
    PreaddQuotient : PreaddCategory ℓ (ℓ-max ℓ' ℓq)
    PreaddQuotient .cat = QuotientCategory (cat C) _~_ ~refl ~cong⋆
    PreaddQuotient .preadd .homAbStr = homAbStr/~
    PreaddQuotient .preadd .⋆distl+ = ⋆distl+/~
    PreaddQuotient .preadd .⋆distr+ = ⋆distr+/~

-- Quotients of additive categories
module _ (A : AdditiveCategory ℓ ℓ') where
  open AdditiveCategory A

  module _ (_~_ : {x y : ob} (f g : Hom[ x , y ] ) → Type ℓq)
           (~refl : {x y : ob} (f : Hom[ x , y ] ) → f ~ f)
           (~cong⋆ : {x y z : ob}
                     (f f' : Hom[ x , y ]) → f ~ f'
                   → (g g' : Hom[ y , z ]) → g ~ g'
                   → (f ⋆ g) ~ (f' ⋆ g'))
           (~cong+ : {x y : ob} (f f' g g' : Hom[ x , y ])
                   → f ~ f' → g ~ g' → (f + g) ~ (f' + g'))
           (~cong- : {x y : ob} (f f' : Hom[ x , y ])
                   → f ~ f' → (- f) ~ (- f'))           where

    private
      A/~ = PreaddQuotient preaddcat _~_ ~refl ~cong⋆ ~cong+ ~cong-

    -- Zero object
    open ZeroObject
    zero/~ : ZeroObject A/~
    zero/~ .z = zero .z
    zero/~ .zInit = isInitial/~ cat _~_ ~refl ~cong⋆ (zInit zero)
    zero/~ .zTerm = isTerminal/~ cat _~_ ~refl ~cong⋆ (zTerm zero)

    -- Biproducts
    module _ (x y : ob) where
      open Biproduct
      open IsBiproduct

      biprod/~ : Biproduct A/~ x y
      biprod/~ .x⊕y = x ⊕ y
      biprod/~ .i₁ = ⟦ i₁ (biprod x y) ⟧
      biprod/~ .i₂ = ⟦ i₂ (biprod x y) ⟧
      biprod/~ .π₁ = ⟦ π₁ (biprod x y) ⟧
      biprod/~ .π₂ = ⟦ π₂ (biprod x y) ⟧
      biprod/~ .isBipr .i₁⋆π₁ = cong ⟦_⟧ (i₁⋆π₁ (biprod x y))
      biprod/~ .isBipr .i₁⋆π₂ = cong ⟦_⟧ (i₁⋆π₂ (biprod x y))
      biprod/~ .isBipr .i₂⋆π₁ = cong ⟦_⟧ (i₂⋆π₁ (biprod x y))
      biprod/~ .isBipr .i₂⋆π₂ = cong ⟦_⟧ (i₂⋆π₂ (biprod x y))
      biprod/~ .isBipr .∑π⋆i  = cong ⟦_⟧ (∑π⋆i  (biprod x y))

    open AdditiveCategoryStr
    AdditiveQuotient : AdditiveCategory ℓ (ℓ-max ℓ' ℓq)
    AdditiveQuotient .preaddcat = A/~
    AdditiveQuotient .addit .zero = zero/~
    AdditiveQuotient .addit .biprod = biprod/~

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical