text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.RadicalIdeal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Sum hiding (map)
open import Cubical.Data.FinData hiding (elim)
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                      ; _choose_ to _ℕchoose_ ; snotz to ℕsnotz)
open import Cubical.Data.Nat.Order

open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

module _ (R' : CommRing ℓ) where
 private R = fst R'
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open Exponentiation R'
 open BinomialThm R'
 open isCommIdeal

 √ : ℙ R → ℙ R --\surd
 √ I x = (∃[ n ∈ ℕ ] x ^ n ∈ I) , isPropPropTrunc

 ^∈√→∈√ : ∀ (I : ℙ R) (x : R) (n : ℕ) → x ^ n ∈ √ I → x ∈ √ I
 ^∈√→∈√ I x n =
         map (λ { (m , [xⁿ]ᵐ∈I) → (n ·ℕ m) , subst-∈ I (sym (^-rdist-·ℕ x n m)) [xⁿ]ᵐ∈I })

 ∈→∈√ : ∀ (I : ℙ R) (x : R) → x ∈ I → x ∈ √ I
 ∈→∈√ I _ x∈I = ∣ 1 , subst-∈ I (sym (·Rid _)) x∈I ∣

 √OfIdealIsIdeal : ∀ (I : ℙ R) → isCommIdeal R' I → isCommIdeal R' (√ I)
 +Closed (√OfIdealIsIdeal I ici) {x = x} {y = y} = map2 +ClosedΣ
  where
  +ClosedΣ : Σ[ n ∈ ℕ ] x ^ n ∈ I → Σ[ n ∈ ℕ ] y ^ n ∈ I → Σ[ n ∈ ℕ ] (x + y) ^ n ∈ I
  +ClosedΣ (n , xⁿ∈I) (m , yᵐ∈I) = (n +ℕ m)
                                  , subst-∈ I (sym (BinomialThm (n +ℕ m) _ _)) ∑Binomial∈I
   where
   binomialCoeff∈I : ∀ i → ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i) ∈ I
   binomialCoeff∈I i with ≤-+-split n m (toℕ i) (pred-≤-pred (toℕ<n i))
   ... | inl n≤i = subst-∈ I (sym path) (·Closed ici _ xⁿ∈I)
    where
    useSolver : ∀ a b c d → a · (b · c) · d ≡ a · b · d · c
    useSolver = solve R'
    path : ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡ ((n +ℕ m) choose toℕ i) · x ^ (toℕ i ∸ n) · y ^ (n +ℕ m ∸ toℕ i) · x ^ n
    path = ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ cong (λ k → ((n +ℕ m) choose toℕ i) · x ^ k · y ^ (n +ℕ m ∸ toℕ i))
                 (sym (≤-∸-+-cancel n≤i)) ⟩
           ((n +ℕ m) choose toℕ i) · x ^ ((toℕ i ∸ n) +ℕ n) · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ cong (λ z → ((n +ℕ m) choose toℕ i) · z · y ^ (n +ℕ m ∸ toℕ i))
                 (sym (·-of-^-is-^-of-+ x (toℕ i ∸ n) n)) ⟩
           ((n +ℕ m) choose toℕ i) · (x ^ (toℕ i ∸ n) · x ^ n) · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ useSolver _ _ _ _ ⟩
           ((n +ℕ m) choose toℕ i) · x ^ (toℕ i ∸ n) · y ^ (n +ℕ m ∸ toℕ i) · x ^ n ∎

   ... | inr m≤n+m-i = subst-∈ I (sym path) (·Closed ici _ yᵐ∈I)
    where
    path : ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡ ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ ((n +ℕ m ∸ toℕ i) ∸ m) · y ^ m
    path = ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ cong (λ k → ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ k)
                 (sym (≤-∸-+-cancel m≤n+m-i)) ⟩
           ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (((n +ℕ m ∸ toℕ i) ∸ m) +ℕ m)
         ≡⟨ cong (((n +ℕ m) choose toℕ i) · x ^ toℕ i ·_)
                 (sym (·-of-^-is-^-of-+ y ((n +ℕ m ∸ toℕ i) ∸ m) m)) ⟩
           ((n +ℕ m) choose toℕ i) · x ^ toℕ i · (y ^ ((n +ℕ m ∸ toℕ i) ∸ m) · y ^ m)
         ≡⟨ ·Assoc _ _ _ ⟩
           ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ ((n +ℕ m ∸ toℕ i) ∸ m) · y ^ m ∎

   ∑Binomial∈I : ∑ (BinomialVec (n +ℕ m) x y) ∈ I
   ∑Binomial∈I = ∑Closed R' (I , ici) (BinomialVec (n +ℕ m) _ _) binomialCoeff∈I
 contains0 (√OfIdealIsIdeal I ici) =
   ∣ 1 , subst-∈ I (sym (0LeftAnnihilates 1r)) (ici .contains0) ∣
 ·Closed (√OfIdealIsIdeal I ici) r =
   map λ { (n , xⁿ∈I) → n , subst-∈ I (sym (^-ldist-· r _ n)) (ici .·Closed (r ^ n) xⁿ∈I) }

 -- important lemma for characterization of the Zariski lattice
 √FGIdealChar : {n : ℕ} (V : FinVec R n) (I : CommIdeal R')
                → √ (fst ⟨ V ⟩[ R' ]) ⊆ √ (fst I) ≃ (∀ i → V i ∈ √ (fst I))
 √FGIdealChar V I = isEquivPropBiimpl→Equiv (⊆-isProp (√ (fst ⟨ V ⟩[ R' ])) (√ (fst I)))
                                              (isPropΠ (λ _ → √ (fst I) _ .snd)) .fst
                                              (ltrImpl , rtlImpl)
  where
  open KroneckerDelta (CommRing→Ring R')
  ltrImpl : √ (fst ⟨ V ⟩[ R' ]) ⊆ √ (fst I) → (∀ i → V i ∈ √ (fst I))
  ltrImpl √⟨V⟩⊆√I i = √⟨V⟩⊆√I _ (∈→∈√ (fst ⟨ V ⟩[ R' ]) (V i)
                                        ∣ (λ j → δ i j) , sym (∑Mul1r _ _ i) ∣)

  rtlImpl : (∀ i → V i ∈ √ (fst I)) → √ (fst ⟨ V ⟩[ R' ]) ⊆ √ (fst I)
  rtlImpl ∀i→Vi∈√I x = PT.elim (λ _ → √ (fst I) x .snd)
                                λ { (n , xⁿ∈⟨V⟩) → ^∈√→∈√ (fst I) x n (elimHelper _ xⁿ∈⟨V⟩) }
   where
   isCommIdeal√I = √OfIdealIsIdeal (fst I) (snd I)
   elimHelper : ∀ (y : R) → y ∈ (fst ⟨ V ⟩[ R' ]) → y ∈ √ (fst I)
   elimHelper y = PT.elim (λ _ → √ (fst I) y .snd)
                   λ { (α , y≡∑αV) → subst-∈ (√ (fst I)) (sym y≡∑αV)
                                           (∑Closed R' (√ (fst I) , isCommIdeal√I)
                                           (λ i → α i · V i)
                                           (λ i → isCommIdeal√I .·Closed (α i) (∀i→Vi∈√I i))) }


text:
{-# OPTIONS --cubical --allow-unsolved-metas #-}

open import Agda.Primitive.Cubical

module _ where

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
{-# BUILTIN PATHP PathP #-}

data D {ℓ} (A : Set ℓ) : Set ℓ where
  c : PathP _ _ _

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- "Ordinal notations via simultaneous definitions"

module Experiment.Ord where

open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Sum

data Ord : Set
data _<_ : Rel Ord lzero
_≥_ : Rel Ord lzero
fst : Ord → Ord
data Ord where
  𝟎 : Ord
  ω^_+_[_] : (a b : Ord) → a ≥ fst b → Ord
data _<_ where
  <₁ : {a : Ord} → a ≢ 𝟎 → 𝟎 < a
  <₂ : {a b c d : Ord} (r : a ≥ fst c) (s : b ≥ fst d) →
       a < b → ω^ a + c [ r ] < ω^ b + d [ s ]
  <₃ : {a b c : Ord} → (r : a ≥ fst b) (s : a ≥ fst c) → b < c → ω^ a + b [ r ] < ω^ a + c [ s ]
fst 𝟎                = 𝟎
fst (ω^ α + _ [ _ ]) = α
a ≥ b = (b < a) ⊎ (a ≡ b)

_+_ : Ord → Ord → Ord
𝟎 + b = b
a@(ω^ _ + _ [ _ ]) + 𝟎 = a
ω^ a + c [ r ] + ω^ b + d [ s ] = {!   !}

_*_ : Ord → Ord → Ord
a * b = {!   !}


text:
module list where

open import level
open import bool
open import eq
open import maybe
open import nat
open import unit
open import product
open import empty
open import sum

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data 𝕃 {ℓ} (A : Set ℓ) : Set ℓ where
  [] : 𝕃 A
  _::_ : (x : A) (xs : 𝕃 A) → 𝕃 A

{-# BUILTIN LIST 𝕃 #-}
{-# COMPILE GHC 𝕃 = data [] ([] | (:)) #-}

list = 𝕃

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixr 6 _::_ _++_
infixr 5 _shorter_ _longer_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

[_] : ∀ {ℓ} {A : Set ℓ} → A → 𝕃 A
[ x ] = x :: []

is-empty : ∀{ℓ}{A : Set ℓ} → 𝕃 A → 𝔹
is-empty [] = tt
is-empty (_ :: _) = ff

tail : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → 𝕃 A
tail [] = []
tail (x :: xs) = xs

head : ∀{ℓ}{A : Set ℓ} → (l : 𝕃 A) → is-empty l ≡ ff → A
head [] ()
head (x :: xs) _ = x

head2 : ∀{ℓ}{A : Set ℓ} → (l : 𝕃 A) → maybe A
head2 [] = nothing
head2 (a :: _) = just a

last : ∀{ℓ}{A : Set ℓ} → (l : 𝕃 A) → is-empty l ≡ ff → A
last [] ()
last (x :: []) _ = x
last (x :: (y :: xs)) _ = last (y :: xs) refl

_++_ : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → 𝕃 A → 𝕃 A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

concat : ∀{ℓ}{A : Set ℓ} → 𝕃 (𝕃 A) → 𝕃 A
concat [] = []
concat (l :: ls) = l ++ concat ls

repeat : ∀{ℓ}{A : Set ℓ} → ℕ → A → 𝕃 A
repeat 0 a = []
repeat (suc n) a = a :: (repeat n a)

map : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → 𝕃 A → 𝕃 B
map f []        = []
map f (x :: xs) = f x :: map f xs

-- The hom part of the list functor.
list-funct : {ℓ : Level}{A B : Set ℓ} → (A → B) → (𝕃 A → 𝕃 B)
list-funct f l = map f l

{- (maybe-map f xs) returns (just ys) if f returns (just y_i) for each
   x_i in the list xs.  Otherwise, (maybe-map f xs) returns nothing. -}
𝕃maybe-map : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → maybe B) → 𝕃 A → maybe (𝕃 B)
𝕃maybe-map f []       = just []
𝕃maybe-map f (x :: xs) with f x
𝕃maybe-map f (x :: xs) | nothing = nothing
𝕃maybe-map f (x :: xs) | just y with 𝕃maybe-map f xs
𝕃maybe-map f (x :: xs) | just y | nothing = nothing
𝕃maybe-map f (x :: xs) | just y | just ys = just (y :: ys)

foldr : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (A → B → B) → B → 𝕃 A → B
foldr f b [] = b
foldr f b (a :: as) = f a (foldr f b as)

length : ∀{ℓ}{A : Set ℓ} → 𝕃 A → ℕ
length [] = 0
length (x :: xs) = suc (length xs)

reverse-helper : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A → 𝕃 A
reverse-helper h [] = h
reverse-helper h (x :: xs) = reverse-helper (x :: h) xs

reverse : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A
reverse l = reverse-helper [] l

reverse-bad : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A
reverse-bad [] = []
reverse-bad (x :: l) = reverse-bad l ++ [ x ]

list-member : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l : 𝕃 A) → 𝔹
list-member eq a [] = ff
list-member eq a (x :: xs) with eq a x
... | tt = tt
... | ff = list-member eq a xs

list-member-prop : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l : 𝕃 A) → Set
list-member-prop eq a [] = ⊥
list-member-prop eq a (x :: xs) with eq a x
... | tt = ⊤
... | ff = list-member-prop eq a xs

list-minus : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(l1 l2 : 𝕃 A) → 𝕃 A
list-minus eq [] l2 = []
list-minus eq (x :: xs) l2 =
  let r = list-minus eq xs l2 in
    if list-member eq x l2 then r else x :: r

_longer_ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → 𝔹
[] longer y = ff
(x :: xs) longer [] = tt
(x :: xs) longer (y :: ys) = xs longer ys

_shorter_ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → 𝔹
x shorter y = y longer x

-- return tt iff all elements in the list satisfy the given predicate pred.
list-all : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) → 𝔹
list-all pred [] = tt
list-all pred (x :: xs) = pred x && list-all pred xs

all-pred : {ℓ : Level}{X : Set ℓ} → (X → Set ℓ) → 𝕃 X → Set ℓ
all-pred f [] = ⊤
all-pred f (x₁ :: xs) = (f x₁) ∧ (all-pred f xs)

-- return tt iff at least one element in the list satisfies the given predicate pred.
list-any : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) → 𝔹
list-any pred [] = ff
list-any pred (x :: xs) = pred x || list-any pred xs

list-and : (l : 𝕃 𝔹) → 𝔹
list-and [] = tt
list-and (x :: xs) = x && (list-and xs)

list-or : (l : 𝕃 𝔹) → 𝔹
list-or [] = ff
list-or (x :: l) = x || list-or l

list-max : ∀{ℓ}{A : Set ℓ} (lt : A → A → 𝔹) → 𝕃 A → A → A
list-max lt [] x = x
list-max lt (y :: ys) x = list-max lt ys (if lt y x then x else y)

isSublist : ∀{ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A → (A → A → 𝔹) → 𝔹
isSublist l1 l2 eq = list-all (λ a → list-member eq a l2) l1

=𝕃 : ∀{ℓ}{A : Set ℓ} → (A → A → 𝔹) → (l1 : 𝕃 A) → (l2 : 𝕃 A) → 𝔹
=𝕃 eq (a :: as) (b :: bs) = eq a b && =𝕃 eq as bs
=𝕃 eq [] [] = tt
=𝕃 eq _ _ = ff

filter : ∀{ℓ}{A : Set ℓ} → (A → 𝔹) → 𝕃 A → 𝕃 A
filter p [] = []
filter p (x :: xs) = let r = filter p xs in
                     if p x then x :: r else r

-- remove all elements equal to the given one
remove : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l : 𝕃 A) → 𝕃 A
remove eq a l = filter (λ x → ~ (eq a x)) l

{- nthTail n l returns the part of the list after the first n elements,
   or [] if the list has fewer than n elements -}
nthTail : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕃 A → 𝕃 A
nthTail 0 l = l
nthTail n [] = []
nthTail (suc n) (x :: l) = nthTail n l

nth : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕃 A → maybe A
nth _ [] = nothing
nth 0 (x :: xs) = just x
nth (suc n) (x :: xs) = nth n xs

-- nats-down N returns N :: (N-1) :: ... :: 0 :: []
nats-down : ℕ → 𝕃 ℕ
nats-down 0 = [ 0 ]
nats-down (suc x) = suc x :: nats-down x

zip : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂} → 𝕃 A → 𝕃 B → 𝕃 (A × B)
zip [] [] = []
zip [] (x :: l₂) = []
zip (x :: l₁) [] = []
zip (x :: l₁) (y :: l₂) = (x , y) :: zip l₁ l₂

unzip : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂} → 𝕃 (A × B) → (𝕃 A × 𝕃 B)
unzip [] = ([] , [])
unzip ((x , y) :: ps) with unzip ps
... | (xs , ys) = x :: xs , y :: ys

inPairListFst : {A B : Set} → (A → A → 𝔹) → A → 𝕃 (A ∧ B) → Set
inPairListFst _ w [] = ⊥
inPairListFst _=A_ w ((a , b) :: c) with w =A a
... | tt = ⊤
... | ff = inPairListFst _=A_ w c

map-⊎ : {ℓ₁ ℓ₂ ℓ₃ : Level} → {A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃} → (A → C) → (B → C) → 𝕃 (A ⊎ B) → 𝕃 C
map-⊎ f g [] = []
map-⊎ f g (inj₁ x :: l) = f x :: map-⊎ f g l
map-⊎ f g (inj₂ y :: l) = g y :: map-⊎ f g l

proj-⊎₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → 𝕃 (A ⊎ B) → (𝕃 A)
proj-⊎₁ [] = []
proj-⊎₁ (inj₁ x :: l) = x :: proj-⊎₁ l
proj-⊎₁ (inj₂ y :: l) = proj-⊎₁ l

proj-⊎₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → 𝕃 (A ⊎ B) → (𝕃 B)
proj-⊎₂ [] = []
proj-⊎₂ (inj₁ x :: l) = proj-⊎₂ l
proj-⊎₂ (inj₂ y :: l) = y :: proj-⊎₂ l

drop-nothing : ∀{ℓ}{A : Set ℓ} → 𝕃 (maybe A) → 𝕃 A
drop-nothing [] = []
drop-nothing (nothing :: aa) = drop-nothing aa
drop-nothing (just a :: aa) = a :: drop-nothing aa

index : ∀{ℓ}{A : Set ℓ} → A → (A → A → 𝔹) → ℕ → 𝕃 A → maybe ℕ
index x _ c [] = nothing
index x _eq_ c (y :: l) with x eq y
... | tt = just c
... | ff = index x _eq_ (suc c) l

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-
Joseph Eremondi
Utrecht University Capita Selecta
UU# 4229924
July 22, 2015
-}

module SemiLinRE where

open import Data.Vec
open import Data.Nat
import Data.Fin as Fin

open import Data.List
import Data.List.All
open import Data.Bool
open import Data.Char

open import Data.Maybe

open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.Core

open import Category.Monad

open import Data.Nat.Properties.Simple

open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Utils

open import Function

import RETypes

open import Data.Sum

open import SemiLin

open import Data.Vec.Equality
open import Data.Nat.Properties.Simple

module VecNatEq = Data.Vec.Equality.DecidableEquality (Relation.Binary.PropositionalEquality.decSetoid Data.Nat._≟_)

--Find the Parikh vector of a given word
--Here cmap is the mapping of each character to its position
--in the Parikh vector
wordParikh : {n : ℕ} -> (Char -> Fin.Fin n) -> (w : List Char) -> Parikh n
wordParikh cmap [] = v0
wordParikh cmap (x ∷ w) = (basis (cmap x)) +v (wordParikh cmap w)

--Show that the Parikh of concatenating two words
--Is the sum of their Parikhs
wordParikhPlus : {n : ℕ}
  -> (cmap : Char -> Fin.Fin n)
  -> (u : List Char)
  -> (v : List Char)
  -> wordParikh cmap (u Data.List.++ v) ≡ (wordParikh cmap u) +v (wordParikh cmap v)
wordParikhPlus cmap [] v = sym v0identLeft
wordParikhPlus {n} cmap (x ∷ u) v  =
  begin
    basis (cmap x) +v wordParikh cmap (u ++l v)
  ≡⟨ cong (λ y → basis (cmap x) +v y) (wordParikhPlus cmap u v) ⟩
    basis (cmap x) +v (wordParikh cmap u +v wordParikh cmap v)
  ≡⟨ sym vAssoc ⟩
    ((basis (cmap x) +v wordParikh cmap u) +v wordParikh cmap v ∎)
    where
      _++l_ = Data.List._++_

--The algorithm mapping regular expressions to the Parikh set of
--the language matched by the RE
--We prove this correct below
reSemiLin : {n : ℕ} {null? : RETypes.Null?} -> (Char -> Fin.Fin n) -> RETypes.RE null? -> SemiLinSet n
reSemiLin cmap RETypes.ε = Data.List.[ v0 , 0 , [] ]
reSemiLin cmap RETypes.∅ = []
reSemiLin cmap (RETypes.Lit x) = Data.List.[ basis (cmap x ) , 0 , [] ]
reSemiLin cmap (r1 RETypes.+ r2) = reSemiLin cmap r1 Data.List.++ reSemiLin cmap r2
reSemiLin cmap (r1 RETypes.· r2) = reSemiLin cmap r1 +s reSemiLin cmap r2
reSemiLin cmap (r RETypes.*)  = starSemiLin (reSemiLin cmap r)

{-
Show that s* ⊆ s +v s*
Not implemented due to time restrictions,
but should be possible, given that linStarExtend is implemented
in SemiLin.agda
-}
starExtend
  :  {n : ℕ}
  -> (v1 v2 : Parikh n )
  -> ( s ss : SemiLinSet n)
  -> ss ≡ starSemiLin s
  -> InSemiLin v1 s
  -> InSemiLin v2 ss
  -> InSemiLin (v1 +v v2) (starSemiLin s)
starExtend v1 v2 s ss spf inS inSS = {!!}

{-
Show that s* ⊇ s +v s*
Not completely implemented due to time restrictions,
but should be possible, given that linStarDecomp is implemented
in SemiLin.agda.

There are also some hard parts, for example, dealing with the proofs
that the returned vectors are non-zero (otherwise, we'd just trivially return v0 and v)
-}
starDecomp
 :  {n : ℕ}
 -> (v : Parikh n)
 -> (s ss : SemiLinSet n)
 -> v ≢ v0
 -> ss ≡ starSemiLin s
 -> InSemiLin v ss
 -> (∃ λ v1 -> ∃ λ v2 -> v1 +v v2 ≡ v × InSemiLin v1 s × InSemiLin v2 ss × v1 ≢ v0  )
starDecomp v s ss vpf spf inSemi = {!!}
{-
starDecomp v sh st .(sh ∷ st) .((v0 , 0 , []) ∷ starSum sh st ∷ []) vnz refl refl (InHead .v .(v0 , 0 , []) .(starSum sh st ∷ []) x) with emptyCombZero v x | vnz (emptyCombZero v x)
starDecomp .v0 sh st .(sh ∷ st) .((v0 , zero , []) ∷ [] Data.List.++ starSum sh st ∷ []) vnz refl refl (InHead .v0 .(v0 , zero , []) .(starSum sh st ∷ []) x) | refl | ()
starDecomp v sh [] .(sh ∷ []) .((v0 , 0 , []) ∷ (proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) ∷ []) vnz refl refl (InTail .v .(v0 , 0 , []) .((proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) ∷ []) (InHead .v .(proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) .[] starComb)) with linStarDecomp v sh _ vnz {!!} refl starComb
starDecomp v sh [] .(sh ∷ []) .((v0 , zero , []) ∷ [] Data.List.++ starSum sh [] ∷ []) vnz refl refl (InTail .v .(v0 , zero , []) .(starSum sh [] ∷ []) (InHead .v .(proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) .[] starComb)) | inj₁ lComb = v , v0 , v0identRight , InHead v sh [] lComb , InHead v0 (v0 , zero , []) _ (v0 , refl) , vnz
starDecomp v sh [] .(sh ∷ []) .((v0 , zero , []) ∷ [] Data.List.++ starSum sh [] ∷ []) vnz refl refl (InTail .v .(v0 , zero , []) .(starSum sh [] ∷ []) (InHead .v .(proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) .[] starComb)) | inj₂ (v1 , v2 , sumPf , comb1 , comb2 , zpf ) = v1 , v2 , sumPf , InHead v1 sh [] comb1 ,  InTail v2 (v0 , zero , []) _ (InHead v2 _ [] comb2) , zpf
starDecomp v sh [] .(sh ∷ []) .((v0 , 0 , []) ∷ (proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) ∷ []) vnz refl refl (InTail .v .(v0 , 0 , []) .((proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) ∷ []) (InTail .v .(proj₁ sh , suc (proj₁ (proj₂ sh)) , proj₁ sh ∷ proj₂ (proj₂ sh)) .[] ()))
starDecomp v sh (x ∷ st) .(sh ∷ x ∷ st) .((v0 , 0 , []) ∷ (proj₁ x +v proj₁ (starSum sh st) , suc (proj₁ (proj₂ x) + proj₁ (proj₂ (starSum sh st))) , proj₁ x ∷ proj₂ (proj₂ x) Data.Vec.++ proj₂ (proj₂ (starSum sh st))) ∷ []) vnz refl refl (InTail .v .(v0 , 0 , []) .((proj₁ x +v proj₁ (starSum sh st) , suc (proj₁ (proj₂ x) + proj₁ (proj₂ (starSum sh st))) , proj₁ x ∷ proj₂ (proj₂ x) Data.Vec.++ proj₂ (proj₂ (starSum sh st))) ∷ []) inSemi) = {!!} -}

--Stolen from the stdlib
listIdentity : {A : Set} -> (x : List A) -> (x Data.List.++ [] ) ≡ x
listIdentity [] = refl
listIdentity (x ∷ xs) = cong (_∷_ x) (listIdentity xs)

{-
Show that +s is actually the sum of two sets, that is,
if v1 is in S1, and v2 is in S2, then v1 +v v2
is in S1 +s S2
-}
sumPreserved :
  {n : ℕ}
  -> (u : Parikh n)
  -> (v : Parikh n)
  -- -> (uv : Parikh n)
  -> (su : SemiLinSet n)
  -> (sv : SemiLinSet n)
  -- -> (suv : SemiLinSet n)
  -- -> (uv ≡ u +v v)
  -- -> (suv ≡ su +s sv)
  -> InSemiLin u su
  -> InSemiLin v sv
  -> InSemiLin (u +v v) (su +s sv)
sumPreserved u v .((ub , um , uvecs) ∷ st) .((vb , vm , vvecs) ∷ st₁) (InHead .u (ub , um , uvecs) st (uconsts , upf)) (InHead .v (vb , vm , vvecs) st₁ (vconsts , vpf))
  rewrite   upf | vpf
  = InHead (u +v v) (ub +v vb , um + vm , uvecs Data.Vec.++ vvecs) (Data.List.map (_+l_ (ub , um , uvecs)) st₁ Data.List.++
                                                                       Data.List.foldr Data.List._++_ []
                                                                       (Data.List.map
                                                                        (λ z → z +l (vb , vm , vvecs) ∷ Data.List.map (_+l_ z) st₁) st))
  ((uconsts Data.Vec.++ vconsts) , trans (combSplit ub vb um vm uvecs vvecs uconsts vconsts)
  (sym (subst (λ x → u +v v ≡ x +v applyLinComb vb vm vvecs vconsts) (sym upf) (cong (λ x → u +v x) (sym vpf)))) )

sumPreserved u v .(sh ∷ st) .(sh₁ ∷ st₁) (InHead .u sh st x) (InTail .v sh₁ st₁ vIn) =
  let
    subCall1 : InSemiLin (u +v v) ((sh ∷ []) +s  st₁)
    subCall1 = sumPreserved u v (sh ∷ []) ( st₁) (InHead u sh [] x) vIn

    eqTest : (sh ∷ []) +s ( st₁) ≡ Data.List.map (λ l2 → sh +l l2) st₁
    eqTest =
      begin
      (sh ∷ []) +s (st₁)
      ≡⟨ refl ⟩
      Data.List.map (λ l2 → sh +l l2) ( st₁) Data.List.++ []
      ≡⟨ listIdentity (Data.List.map (_+l_ sh) st₁) ⟩
      Data.List.map (λ l2 → sh +l l2) (st₁)
      ≡⟨ refl ⟩
      (Data.List.map (λ l2 → sh +l l2) st₁ ∎)

    newCall = slExtend (u +v v) (Data.List.map (_+l_ sh) st₁) (subst (InSemiLin (u +v v)) eqTest subCall1) (sh +l sh₁) --
  in slConcatRight (u +v v) (Data.List.map (λ l2 → sh +l l2) (sh₁ ∷ st₁)) newCall (Data.List.foldr Data.List._++_ []
                                                                                (Data.List.map (λ z → z +l sh₁ ∷ Data.List.map (_+l_ z) st₁) st))
sumPreserved u v .(sh ∷ st) sv (InTail .u sh st uIn) vIn =
  (slConcatLeft (u +v v) (st +s sv) (sumPreserved u v st sv uIn vIn) (Data.List.map (λ x → sh +l x) sv))

--A useful lemma, avoids having to dig into the List monoid instance
rightCons : {A : Set} -> (l : List A) -> (l Data.List.++ [] ≡ l)
rightCons [] = refl
rightCons (x ∷ l) rewrite rightCons l = refl

{-
Show that, if a vector is in the union of two semi-linear sets,
then it must be in one of those sets.
Used in the proof for Union.
Called concat because we represent semi-linear sets as lists,
so union is just concatenating two semi-linear sets
-}
decomposeConcat
  :  {n : ℕ}
  -> (v : Parikh n)
  -> (s1 s2 s3 : SemiLinSet n)
  -> (s3 ≡ s1 Data.List.++ s2 )
  -> InSemiLin v s3
  -> InSemiLin v s1 ⊎ InSemiLin v s2
decomposeConcat v [] s2 .s2 refl inSemi = inj₂ inSemi
decomposeConcat v (x ∷ s1) s2 .(x ∷ s1 Data.List.++ s2) refl (InHead .v .x .(s1 Data.List.++ s2) x₁) = inj₁ (InHead v x s1 x₁)
decomposeConcat v (x ∷ s1) s2 .(x ∷ s1 Data.List.++ s2) refl (InTail .v .x .(s1 Data.List.++ s2) inSemi) with decomposeConcat v s1 s2 _ refl inSemi
decomposeConcat v (x₁ ∷ s1) s2 .(x₁ ∷ s1 Data.List.++ s2) refl (InTail .v .x₁ .(s1 Data.List.++ s2) inSemi) | inj₁ x = inj₁ (InTail v x₁ s1 x)
decomposeConcat v (x ∷ s1) s2 .(x ∷ s1 Data.List.++ s2) refl (InTail .v .x .(s1 Data.List.++ s2) inSemi) | inj₂ y = inj₂ y

concatEq : {n : ℕ} -> (l : LinSet n) -> (s : SemiLinSet n) -> (l ∷ []) +s s ≡ (Data.List.map (_+l_ l) s)
concatEq l [] = refl
concatEq l (x ∷ s) rewrite concatEq l s | listIdentity (l ∷ [])  = refl

{-
Show that if v is in l1 +l l2, then v = v1 +v v2 for some
v1 in l1 and v2 in l2.
This is the other half of the correcness proof of our sum functions, +l and +s
-}
decomposeLin
  :  {n : ℕ}
  -> (v : Parikh n)
  -> (l1 l2 l3 : LinSet n)
  -> (l3 ≡ l1 +l l2 )
  -> LinComb v l3
  -> ∃ λ v1 → ∃ λ v2 -> (v1 +v v2 ≡ v) × (LinComb v1 l1) × (LinComb v2 l2 )
decomposeLin .(applyLinComb (b1 +v b2) (m1 + m2) (vecs1 Data.Vec.++ vecs2) coeffs) (b1 , m1 , vecs1) (b2 , m2 , vecs2) .(b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) refl (coeffs , refl) with Data.Vec.splitAt m1 coeffs
decomposeLin .(applyLinComb (b1 +v b2) (m1 + m2) (vecs1 Data.Vec.++ vecs2) (coeffs1 Data.Vec.++ coeffs2)) (b1 , m1 , vecs1) (b2 , m2 , vecs2) .(b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) refl (.(coeffs1 Data.Vec.++ coeffs2) , refl) | coeffs1 , coeffs2 , refl rewrite combSplit b1 b2 m1 m2 vecs1 vecs2 coeffs1 coeffs2
  = applyLinComb b1 m1 vecs1 coeffs1 , (applyLinComb b2 m2 vecs2 coeffs2 , (refl , ((coeffs1 , refl) , (coeffs2 , refl))))

{-
Show that our Parikh function is a superset of the actual Parikh image of a Regular Expression.

We do this by showing that, for every word matching an RE, its Parikh vector
is in the Parikh Image of the RE
-}
reParikhCorrect :
  {n : ℕ}
  -> {null? : RETypes.Null?}
  -> (cmap : Char -> Fin.Fin n)
  -> (r : RETypes.RE null?)
  -> (w : List Char )
  -> RETypes.REMatch w r
  -> (wordPar : Parikh n)
  -> (wordParikh cmap w ≡ wordPar)
  -> (langParikh : SemiLinSet n)
  -> (langParikh ≡ reSemiLin cmap r )
  -> (InSemiLin wordPar langParikh )
reParikhCorrect cmap .RETypes.ε .[] RETypes.EmptyMatch .v0 refl .((v0 , 0 , []) ∷ []) refl = InHead v0 (v0 , zero , []) [] ([] , refl)
reParikhCorrect cmap .(RETypes.Lit c) .(c ∷ []) (RETypes.LitMatch c) .(basis (cmap c) +v v0) refl .((basis (cmap c) , 0 , []) ∷ []) refl =
  InHead (basis (cmap c) +v v0) (basis (cmap c) , zero , []) [] (subst (λ x → LinComb x (basis (cmap c) , zero , [])) (sym v0identRight) (v0 , (v0apply (basis (cmap c)) [])))
reParikhCorrect cmap (r1 RETypes.+ .r2) w (RETypes.LeftPlusMatch r2 match) wordPar wpf langParikh lpf =
  let
    leftParikh = reSemiLin cmap r1
    leftInSemi = reParikhCorrect cmap r1 w match wordPar wpf leftParikh refl
    --Idea: show that langParikh is leftParikh ++ rightParikh
    --And that this means that it must be in the concatentation
    extendToConcat : InSemiLin wordPar ((reSemiLin cmap r1 ) Data.List.++ (reSemiLin cmap r2))
    extendToConcat = slConcatRight wordPar (reSemiLin cmap r1) leftInSemi (reSemiLin cmap r2)
  in subst (λ x → InSemiLin wordPar x) (sym lpf) extendToConcat
reParikhCorrect cmap (.r1 RETypes.+ r2) w (RETypes.RightPlusMatch r1 match) wordPar wpf langParikh lpf = let
    rightParikh = reSemiLin cmap r2
    rightInSemi = reParikhCorrect cmap r2 w match wordPar wpf rightParikh refl
    --Idea: show that langParikh is leftParikh ++ rightParikh
    --And that this means that it must be in the concatentation
    extendToConcat : InSemiLin wordPar ((reSemiLin cmap r1 ) Data.List.++ (reSemiLin cmap r2))
    extendToConcat = slConcatLeft wordPar (reSemiLin cmap r2) rightInSemi (reSemiLin cmap r1)
  in subst (λ x → InSemiLin wordPar x) (sym lpf) extendToConcat
reParikhCorrect cmap (r1 RETypes.· r2) s3 (RETypes.ConcatMatch {s1 = s1} {s2 = s2} {spf = spf} match1 match2) .(wordParikh cmap s3) refl ._ refl rewrite (sym spf) |  (wordParikhPlus cmap s1 s2) =
 let
    leftParikh = reSemiLin cmap r1
    leftInSemi : InSemiLin (wordParikh cmap s1) leftParikh
    leftInSemi = reParikhCorrect cmap r1 s1 match1 (wordParikh cmap s1) refl (reSemiLin cmap r1) refl

    rightParikh = reSemiLin cmap r2
    rightInSemi : InSemiLin (wordParikh cmap s2) rightParikh
    rightInSemi = reParikhCorrect cmap r2 s2 match2 (wordParikh cmap s2) refl (reSemiLin cmap r2) refl

    wordParikhIsPlus : (wordParikh cmap s1) +v (wordParikh cmap s2) ≡ (wordParikh cmap (s1 Data.List.++ s2 ))
    wordParikhIsPlus = sym (wordParikhPlus cmap s1 s2)

  in sumPreserved (wordParikh cmap s1) (wordParikh cmap s2) leftParikh rightParikh leftInSemi rightInSemi
reParikhCorrect cmap (r RETypes.*) [] RETypes.EmptyStarMatch .v0 refl .(starSemiLin (reSemiLin cmap r)) refl = zeroInStar (reSemiLin cmap r) (starSemiLin (reSemiLin cmap r)) refl
reParikhCorrect cmap (r RETypes.*) .(s1 Data.List.++ s2 ) (RETypes.StarMatch {s1 = s1} {s2 = s2} {spf = refl} m1 m2) ._ refl .(starSemiLin (reSemiLin cmap r)) refl rewrite wordParikhPlus cmap s1 s2 =
  starExtend (wordParikh cmap s1) (wordParikh cmap s2) (reSemiLin cmap r) _ refl (reParikhCorrect cmap r s1 m1 (wordParikh cmap s1) refl (reSemiLin cmap r) refl) (reParikhCorrect cmap (r RETypes.*) s2 m2 (wordParikh cmap s2) refl (starSemiLin (reSemiLin cmap r)) refl)

{-
Show that if v is in s1 +s s2, then v = v1 +v v2 for some
v1 in s1 and v2 in s2.
This is the other half of the correcness proof of our sum functions, +l and +s
-}
decomposeSum
  :  {n : ℕ}
  -> (v : Parikh n)
  -> (s1 s2 s3 : SemiLinSet n)
  -> (s3 ≡ s1 +s s2 )
  -> InSemiLin v s3
  -> ∃ λ (v1 : Parikh n) → ∃ λ (v2 : Parikh n) -> (v1 +v v2 ≡ v) × (InSemiLin v1 s1) × (InSemiLin v2 s2 )
decomposeSum v [] [] .[] refl ()
decomposeSum v [] (x ∷ s2) .[] refl ()
decomposeSum v (x ∷ s1) [] .(Data.List.foldr Data.List._++_ [] (Data.List.map (λ l1 → []) s1)) refl ()
decomposeSum v ((b1 , m1 , vecs1) ∷ s1) ((b2 , m2 , vecs2) ∷ s2) ._ refl (InHead .v .(b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) ._ lcomb) =
  let
    (v1 , v2 , plusPf , comb1 , comb2 ) = decomposeLin v (b1 , m1 , vecs1) (b2 , m2 , vecs2) (b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) refl lcomb
  in v1 , v2 , plusPf , InHead v1 (b1 , m1 , vecs1) s1 comb1 , InHead v2 (b2 , m2 , vecs2) s2 comb2
decomposeSum v ((b1 , m1 , vecs1) ∷ s1) ((b2 , m2 , vecs2) ∷ s2) ._ refl (InTail .v .(b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) ._ inSemi) with decomposeConcat v (Data.List.map (_+l_ (b1 , m1 , vecs1)) s2) (Data.List.foldr Data.List._++_ []
                                                                                (Data.List.map
                                                                                (λ z → z +l (b2 , m2 , vecs2) ∷ Data.List.map (_+l_ z) s2) s1)) (Data.List.map (_+l_ (b1 , m1 , vecs1)) s2 Data.List.++
                                                                                Data.List.foldr Data.List._++_ []
                                                                                (Data.List.map
                                                                                (λ z → z +l (b2 , m2 , vecs2) ∷ Data.List.map (_+l_ z) s2) s1)) refl inSemi
decomposeSum v ((b1 , m1 , vecs1) ∷ s1) ((b2 , m2 , vecs2) ∷ s2) .((b1 , m1 , vecs1) +l (b2 , m2 , vecs2) ∷ Data.List.map (_+l_ (b1 , m1 , vecs1)) s2 Data.List.++ Data.List.foldr Data.List._++_ [] (Data.List.map _ s1)) refl (InTail .v .(b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) .(Data.List.map (_+l_ (b1 , m1 , vecs1)) s2 Data.List.++ Data.List.foldr Data.List._++_ [] (Data.List.map _ s1)) inSemi) | inj₁ inSub =
  let
    subCall1 = decomposeSum v ((b1 , m1 , vecs1) ∷ []) s2 _ refl (subst (λ x → InSemiLin v x) (sym (concatEq (b1 , m1 , vecs1) s2)) inSub)
    v1 , v2 , pf , xIn , yIn = subCall1
  in v1 , (v2 , (pf , (slCons v1 s1 (b1 , m1 , vecs1) xIn , slExtend v2 s2 yIn (b2 , m2 , vecs2))))
decomposeSum v ((b1 , m1 , vecs1) ∷ s1) ((b2 , m2 , vecs2) ∷ s2) .((b1 , m1 , vecs1) +l (b2 , m2 , vecs2) ∷ Data.List.map (_+l_ (b1 , m1 , vecs1)) s2 Data.List.++ Data.List.foldr Data.List._++_ [] (Data.List.map _ s1)) refl (InTail .v .(b1 +v b2 , m1 + m2 , vecs1 Data.Vec.++ vecs2) .(Data.List.map (_+l_ (b1 , m1 , vecs1)) s2 Data.List.++ Data.List.foldr Data.List._++_ [] (Data.List.map _ s1)) inSemi) | inj₂ inSub =
 let
   subCall1 = decomposeSum v s1 ((b2 , m2 , vecs2) ∷ s2) _ refl inSub
   v1 , v2 , pf , xIn , yIn = subCall1
 in v1 , v2 , pf , slExtend v1 s1 xIn (b1 , m1 , vecs1) , yIn

{-
Show that the generated Parikh image is a subset of the actual Parikh image.

We do this by showing that, for every vector in the generated Parikh image,
there's some word matched by the RE whose Parikh vector is that vector.
-}
--We have to convince the compiler that this is terminating
--Since I didn't have time to implement the proofs of non-zero vectors
--Which show that we only recurse on strictly smaller vectors in the Star case
{-# TERMINATING #-}
reParikhComplete : {n : ℕ} -> {null? : RETypes.Null?}
  -> (cmap : Char -> Fin.Fin n)
--  -> (imap : Fin.Fin n -> Char)
--  -> (invPf1 : (x : Char ) -> imap (cmap x) ≡ x)
--  -> (invPf2 : (x : Fin.Fin n ) -> cmap (imap x) ≡ x )
  -> (r : RETypes.RE null?)
  -> (v : Parikh n )
  -> (langParikh : SemiLinSet n)
  -> langParikh ≡ (reSemiLin cmap r )
  -> (InSemiLin v langParikh )
  -> ∃ (λ w -> (v ≡ wordParikh cmap w) × (RETypes.REMatch w r) )
reParikhComplete cmap RETypes.ε .v0 .((v0 , 0 , []) ∷ []) refl (InHead .v0 .(v0 , 0 , []) .[] (combConsts , refl)) = [] , refl , RETypes.EmptyMatch
reParikhComplete cmap RETypes.ε v .((v0 , 0 , []) ∷ []) refl (InTail .v .(v0 , 0 , []) .[] ())

--reParikhComplete cmap  RETypes.ε v .(sh ∷ st) lpf (InTail .v sh st inSemi) = {!!}
reParikhComplete cmap  RETypes.∅ v [] lpf ()
reParikhComplete cmap  RETypes.∅ v (h ∷ t) () inSemi
reParikhComplete cmap (RETypes.Lit x) langParikh [] inSemi ()
reParikhComplete cmap (RETypes.Lit x) .(basis (cmap x)) .((basis (cmap x) , 0 , []) ∷ []) refl (InHead .(basis (cmap x)) .(basis (cmap x) , 0 , []) .[] (consts , refl)) = (x ∷ []) , (sym v0identRight , RETypes.LitMatch x)
reParikhComplete cmap (RETypes.Lit x) v .((basis (cmap x) , 0 , []) ∷ []) refl (InTail .v .(basis (cmap x) , 0 , []) .[] ())
--reParikhComplete cmap (RETypes.Lit x) v .((basis (cmap x) , 0 , []) ∷ []) refl (InTail .v .(basis (cmap x) , 0 , []) .[] ())
reParikhComplete {null? = null?} cmap  (r1 RETypes.+ r2) v langParikh lpf inSemi with decomposeConcat v (reSemiLin cmap r1) (reSemiLin cmap r2) langParikh lpf inSemi
... | inj₁ in1 =
  let
    (subw , subPf , subMatch) = reParikhComplete cmap  r1 v (reSemiLin cmap r1) refl in1
  in subw , (subPf , (RETypes.LeftPlusMatch r2 subMatch))
... | inj₂ in2 =
  let
    (subw , subPf , subMatch) = reParikhComplete cmap  r2 v (reSemiLin cmap r2) refl in2
  in subw , (subPf , (RETypes.RightPlusMatch r1 subMatch))
reParikhComplete cmap (r1 RETypes.· r2) v ._ refl inSemi with decomposeSum v (reSemiLin cmap r1) (reSemiLin cmap r2) (reSemiLin cmap r1 +s reSemiLin cmap r2) refl inSemi | reParikhComplete cmap r1 (proj₁ (decomposeSum v (reSemiLin cmap r1) (reSemiLin cmap r2)
                                                                                (reSemiLin cmap r1 +s reSemiLin cmap r2) refl inSemi)) (reSemiLin cmap r1) refl (proj₁ (proj₂ (proj₂ (proj₂ (decomposeSum v (reSemiLin cmap r1) (reSemiLin cmap r2)
                                                                                (reSemiLin cmap r1 +s reSemiLin cmap r2) refl inSemi))))) | reParikhComplete cmap r2 (proj₁ (proj₂ (decomposeSum v (reSemiLin cmap r1) (reSemiLin cmap r2)
                                                                                (reSemiLin cmap r1 +s reSemiLin cmap r2) refl inSemi))) (reSemiLin cmap r2) refl (proj₂ (proj₂ (proj₂ (proj₂ (decomposeSum v (reSemiLin cmap r1) (reSemiLin cmap r2)
                                                                                (reSemiLin cmap r1 +s reSemiLin cmap r2) refl inSemi)))))
reParikhComplete cmap (r1 RETypes.· r2) .(wordParikh cmap w1 +v wordParikh cmap w2) .(Data.List.foldr Data.List._++_ [] (Data.List.map _ (reSemiLin cmap r1))) refl inSemi | .(wordParikh cmap w1) , .(wordParikh cmap w2) , refl , inSemi1 , inSemi2 | w1 , refl , match1 | w2 , refl , match2 = (w1 Data.List.++ w2) , ((sym (wordParikhPlus cmap w1 w2)) , (RETypes.ConcatMatch match1 match2))

reParikhComplete cmap (r RETypes.*) v langParikh lpf inSemi with (reSemiLin cmap r )
reParikhComplete cmap (r RETypes.*) v .((v0 , 0 , []) ∷ []) refl (InHead .v .(v0 , 0 , []) .[] x) | [] = [] , ((sym (proj₂ x)) , RETypes.EmptyStarMatch)
reParikhComplete cmap (r RETypes.*) v .((v0 , 0 , []) ∷ []) refl (InTail .v .(v0 , 0 , []) .[] ()) | []
reParikhComplete cmap (r RETypes.*) v .((v0 , 0 , []) ∷ starSum x rsl ∷ []) refl inSemi | x ∷ rsl =
  let
    --The first hole is the non-zero proofs that I couldn't work out
    --I'm not totally sure about the second, but I think I just need to apply some associativity to inSemi to get it to fit
    --into the second hole.
    splitVec = starDecomp v (reSemiLin cmap r) _ {!!} refl {!!}
    v1 , v2 , vpf , inS , inSS , _ = splitVec
    subCall1 = reParikhComplete cmap r v1 _ refl inS
    w1 , wpf1 , match  = subCall1
    subCall2 = reParikhComplete cmap (r RETypes.*) v2 _ refl inSS
    w2 , wpf2 , match2 = subCall2
  in (w1 Data.List.++ w2) , (trans (sym vpf) (sym (wordParikhPlus cmap w1 w2)) , RETypes.StarMatch match match2)

max_stars_repo_name: JoeyEremondi/agda-parikh

max_issues_repo_name: JoeyEremondi/agda-parikh

max_forks_repo_name: JoeyEremondi/agda-parikh


text:
open import Level
open import Ordinals
module cardinal {n : Level } (O : Ordinals {n}) where

open import zf
open import logic
import OD
import ODC
import OPair
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core

open inOrdinal O
open OD O
open OD.OD
open OPair O
open ODAxiom odAxiom

import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

open _∧_
open _∨_
open Bool
open _==_

open HOD

-- _⊗_ : (A B : HOD) → HOD
-- A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))

Func :  OD
Func = record { def = λ x → def ZFProduct x
    ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }

FuncP :  ( A B : HOD ) → HOD
FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
    ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) }
       ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }

record Injection (A B : Ordinal ) : Set n where
   field
       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y

record Bijection (A B : Ordinal ) : Set n where
   field
       fun←  : (x : Ordinal ) → odef (* A)  x → Ordinal
       fun→  : (x : Ordinal ) → odef (* B)  x → Ordinal
       funB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( fun← x lt )
       funA  : (x : Ordinal ) → ( lt : odef (* B)  x ) → odef (* A) ( fun→ x lt )
       fiso← : (x : Ordinal ) → ( lt : odef (* B)  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
       fiso→ : (x : Ordinal ) → ( lt : odef (* A)  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x

Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b
Bernstein = {!!}

_=c=_ : ( A B : HOD ) → Set n
A =c= B = Bijection ( & A ) ( & B )

_c<_ : ( A B : HOD ) → Set n
A c< B = ¬ ( Injection (& A)  (& B) )

Card : OD
Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }

record Cardinal (a : Ordinal ) : Set (suc n) where
   field
       card : Ordinal
       ciso : Bijection a card
       cmax : (x : Ordinal) → card o< x → ¬ Bijection a x

Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
Cardinal∈ = {!!}

Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t )
Cardinal⊆ = {!!}

Cantor1 : { u : HOD } → u c< Power u
Cantor1 = {!!}

Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
Cantor2 = {!!}

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
{-# OPTIONS --without-K #-}
import Level as L
open import Type
open import Function
open import Algebra
open import Algebra.FunctionProperties.NP
open import Data.Nat.NP hiding (_^_)
open import Data.Nat.Properties
open import Data.One hiding (_≤_)
open import Data.Sum
open import Data.Maybe.NP
open import Data.Product
open import Data.Bits
open import Data.Zero
open import Data.Bool.NP as Bool
import Function.Equality as FE
open FE using (_⟨$⟩_ ; ≡-setoid)
import Function.Injection as Finj
import Function.Inverse as FI
open FI using (_↔_; module Inverse)
open import Function.LeftInverse using (_RightInverseOf_)
import Function.Related as FR
open import Function.Related.TypeIsomorphisms.NP
open import Relation.Binary.NP
open import Relation.Binary.Sum
open import Relation.Binary.Product.Pointwise
open import Relation.Unary.Logical
open import Relation.Binary.Logical
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_; _≗_)
open import Search.Type

module sum-setoid where

SearchExtFun-úber : ∀ {A B} → (SF : Search (A → B)) → SearchInd SF → SearchExtFun SF
SearchExtFun-úber sf sf-ind op {f = f}{g} f≈g = sf-ind (λ s → s op f ≡ s op g) (≡.cong₂ op) (λ x → f≈g (λ _ → ≡.refl))

SearchExtFun-úber' : ∀ {A B} → (SF : Search (A → B)) → SearchInd SF → SearchExtFun SF
SearchExtFun-úber' sf sf-ind op {f = f}{g} f≈g = sf-ind (λ s → s op f ≡ s op g) (≡.cong₂ op) (λ x → f≈g (λ _ → ≡.refl))

SearchExtoid : ∀ {A : Setoid L.zero L.zero} → Search (Setoid.Carrier A) → ★₁
SearchExtoid {A} sᴬ = ∀ {M} op {f g : A FE.⟶ ≡.setoid M} → Setoid._≈_ (A FE.⇨ ≡.setoid M) f g →  sᴬ op (_⟨$⟩_ f) ≡ sᴬ op (_⟨$⟩_ g)

sum-lin⇒sum-zero : ∀ {A} → {sum : Sum A} → SumLin sum → SumZero sum
sum-lin⇒sum-zero sum-lin = sum-lin (λ _ → 0) 0

sum-mono⇒sum-ext : ∀ {A} → {sum : Sum A} → SumMono sum → SumExt sum
sum-mono⇒sum-ext sum-mono f≗g = ℕ≤.antisym (sum-mono (ℕ≤.reflexive ∘ f≗g)) (sum-mono (ℕ≤.reflexive ∘ ≡.sym ∘ f≗g))

sum-ext+sum-hom⇒sum-mono : ∀ {A} → {sum : Sum A} → SumExt sum → SumHom sum → SumMono sum
sum-ext+sum-hom⇒sum-mono {sum = sum} sum-ext sum-hom {f} {g} f≤°g =
    sum f                         ≤⟨ m≤m+n _ _ ⟩
    sum f + sum (λ x → g x ∸ f x) ≡⟨ ≡.sym (sum-hom _ _) ⟩
    sum (λ x → f x + (g x ∸ f x)) ≡⟨ sum-ext (m+n∸m≡n ∘ f≤°g) ⟩
    sum g ∎ where open ≤-Reasoning

record SumPropoid (As : Setoid L.zero L.zero) : ★₁ where
  constructor _,_
  module ≈ᴬ = Setoid As
  open ≈ᴬ using () renaming (_≈_ to _≈ᴬ_; Carrier to A)
  field
    search     : Search A
    search-ind : SearchInd search

  ⟦search⟧ : ∀ {Aᵣ : A → A → ★}
               (Aᵣ-refl : Reflexive Aᵣ)
              → ⟦Search⟧₁ Aᵣ search
  ⟦search⟧ Aᵣ-refl Mᵣ ∙ᵣ fᵣ = search-ind (λ s → Mᵣ (s _ _) (s _ _))
                                         (λ η → ∙ᵣ η)
                                         (λ _ → fᵣ Aᵣ-refl)

  -- this one is given for completness but the asking for the Aₚ predicate
  -- to be trivial makes this result useless.
  [search] : ∀ (Aₚ : A → ★)
               (Aₚ-triv : ∀ x → Aₚ x)
             → [Search] Aₚ search
  [search] Aₚ Aₚ-triv {M} Mₚ ∙ₚ fₚ =
    search-ind (λ s → Mₚ (s _ _)) (λ η → ∙ₚ η) (λ x → fₚ (Aₚ-triv x))

  search-sg-ext : SearchSgExt search
  search-sg-ext sg {f} {g} f≈°g = search-ind (λ s → s _ f ≈ s _ g) ∙-cong f≈°g
    where open Sgrp sg

  foo : ∀ {A : ★} {R : A → A → ★} → Reflexive R → _≡_ ⇒ R
  foo R-refl ≡.refl = R-refl

  search-ext : SearchExt search
  -- search-ext op {g = g} pf = ⟦search⟧ {_≡_} ≡.refl _≡_ (λ η → ≡.cong₂ op η) (≡.trans (pf _) ∘ ≡.cong g) -- (foo (λ {x} → pf x))
  search-ext op pf = ⟦search⟧ {_≡_} ≡.refl _≡_ (λ η → ≡.cong₂ op η)
                                               (foo (λ {x} → pf x))
 -- (λ { {x} .{x} ≡.refl → pf _ })
  -- {!search-extoid op = ⟦search⟧ {_≈ᴬ_} ≈ᴬ.refl _≡_ (λ η → ≡.cong₂ op η)!}

  search-mono : SearchMono search
  search-mono _⊆_ _∙-mono_ {f} {g} f⊆°g = search-ind (λ s → s _ f ⊆ s _ g) _∙-mono_ f⊆°g

  search-swap : SearchSwap search
  search-swap sg f {sᴮ} pf = search-ind (λ s → s _ (sᴮ ∘ f) ≈ sᴮ (s _ ∘ flip f)) (λ p q → trans (∙-cong p q) (sym (pf _ _))) (λ _ → refl)
    where open Sgrp sg

  searchMon : SearchMon A
  searchMon m = search _∙_
    where open Mon m

  search-ε : Searchε searchMon
  search-ε m = search-ind (λ s → s _ (const ε) ≈ ε) (λ x≈ε y≈ε → trans (∙-cong x≈ε y≈ε) (proj₁ identity ε)) (λ _ → refl)
    where open Mon m

  search-hom : SearchMonHom searchMon
  search-hom cm f g = search-ind (λ s → s _ (f ∙° g) ≈ s _ f ∙ s _ g)
                                 (λ p₀ p₁ → trans (∙-cong p₀ p₁) (∙-interchange _ _ _ _)) (λ _ → refl)
    where open CMon cm

  search-hom′ :
      ∀ {S T}
        (_+_ : Op₂ S)
        (_*_ : Op₂ T)
        (f   : S → T)
        (g   : A → S)
        (hom : ∀ x y → f (x + y) ≡ f x * f y)
        → f (search _+_ g) ≡ search _*_ (f ∘ g)
  search-hom′ _+_ _*_ f g hom = search-ind (λ s → f (s _+_ g) ≡ s _*_ (f ∘ g))
                                           (λ p q → ≡.trans (hom _ _) (≡.cong₂ _*_ p q))
                                           (λ _ → ≡.refl)

  StableUnder : As FE.⟶ As  → ★₁
  StableUnder p = ∀ {B} (op : Op₂ B) f → search op f ≡ search op (f ∘ _⟨$⟩_ p)

  sum : Sum A
  sum = search _+_

  sum-ind : SumInd sum
  sum-ind P P+ Pf = search-ind (λ s → P (s _+_)) P+ Pf

  sum-ext : SumExt sum
  sum-ext = search-ext _+_

  sum-zero : SumZero sum
  sum-zero = search-ε ℕ+.monoid

  sum-hom : SumHom sum
  sum-hom = search-hom ℕ°.+-commutativeMonoid

  sum-mono : SumMono sum
  sum-mono = search-mono _≤_ _+-mono_

  sum-lin : SumLin sum
  sum-lin f zero    = sum-zero
  sum-lin f (suc k) = ≡.trans (sum-hom f (λ x → k * f x)) (≡.cong₂ _+_ (≡.refl {x = sum f}) (sum-lin f k))

  SumStableUnder : As FE.⟶ As → ★
  SumStableUnder p = ∀ (f : As FE.⟶ ≡.setoid ℕ) → sum (_⟨$⟩_ f) ≡ sum (_⟨$⟩_ (f FE.∘ p))

  sumStableUnder : ∀ {p} → StableUnder p → SumStableUnder p
  sumStableUnder SU-p f = SU-p _+_ (_⟨$⟩_ f)

  Card : ℕ
  Card = sum (const 1)

  count : Count A
  count f = sum (Bool.toℕ ∘ f)

  count-ext : CountExt count
  count-ext f≗g = sum-ext (≡.cong Bool.toℕ ∘ f≗g)

  CountStableUnder : As FE.⟶ As → ★
  CountStableUnder p = ∀ (f : As FE.⟶ ≡.setoid Bool) → count (_⟨$⟩_ f) ≡ count (_⟨$⟩_ (f FE.∘ p))

  countStableUnder : ∀ {p} → SumStableUnder p → CountStableUnder p
  countStableUnder sumSU-p f = sumSU-p (≡.:→-to-Π Bool.toℕ FE.∘ f)

  search-extoid : SearchExtoid {As} search
  -- search-extoid op {f = f}{g} f≈g = search-ind (λ s₁ → s₁ op (_⟨$⟩_ f) ≡ s₁ op (_⟨$⟩_ g)) (≡.cong₂ op) (λ x → f≈g (Setoid.refl As))
  search-extoid op = ⟦search⟧ {_≈ᴬ_} ≈ᴬ.refl _≡_ (λ η → ≡.cong₂ op η)

SumProp : ★ → ★₁
SumProp A = SumPropoid (≡.setoid A)

open SumPropoid public

search-swap' : ∀ {A B} cm (μA : SumPropoid A) (μB : SumPropoid B) f →
               let open CMon cm
                   sᴬ = search μA _∙_
                   sᴮ = search μB _∙_ in
               sᴬ (sᴮ ∘ f) ≈ sᴮ (sᴬ ∘ flip f)
search-swap' cm μA μB f = search-swap μA sg f (search-hom μB cm)
  where open CMon cm

sum-swap : ∀ {A B} (μA : SumPropoid A) (μB : SumPropoid B) f →
           sum μA (sum μB ∘ f) ≡ sum μB (sum μA ∘ flip f)
sum-swap = search-swap' ℕ°.+-commutativeMonoid

_≈Sum_ : ∀ {A} → (sum₀ sum₁ : Sum A) → ★
sum₀ ≈Sum sum₁ = ∀ f → sum₀ f ≡ sum₁ f

_≈Search_ : ∀ {A} → (s₀ s₁ : Search A) → ★₁
s₀ ≈Search s₁ = ∀ {B} (op : Op₂ B) f → s₀ op f ≡ s₁ op f

μ𝟙 : SumProp 𝟙
μ𝟙 = srch , ind
  where
    srch : Search 𝟙
    srch _ f = f _

    ind : SearchInd srch
    ind _ _ Pf = Pf _

μBit : SumProp Bit
μBit = searchBit , ind
  where
    searchBit : Search Bit
    searchBit _∙_ f = f 0b ∙ f 1b

    ind : SearchInd searchBit
    ind _ _P∙_ Pf = Pf 0b P∙ Pf 1b

infixr 4 _+Search_

_+Search_ : ∀ {A B} → Search A → Search B → Search (A ⊎ B)
(searchᴬ +Search searchᴮ) _∙_ f = searchᴬ _∙_ (f ∘ inj₁) ∙ searchᴮ _∙_ (f ∘ inj₂)

_+SearchInd_ : ∀ {A B} {sᴬ : Search A} {sᴮ : Search B} →
                 SearchInd sᴬ → SearchInd sᴮ → SearchInd (sᴬ +Search sᴮ)
(Psᴬ +SearchInd Psᴮ) P P∙ Pf
  = P∙ (Psᴬ (λ s → P (λ _ f → s _ (f ∘ inj₁))) P∙ (Pf ∘ inj₁))
       (Psᴮ (λ s → P (λ _ f → s _ (f ∘ inj₂))) P∙ (Pf ∘ inj₂))

infixr 4 _+Sum_

_+Sum_ : ∀ {A B} → Sum A → Sum B → Sum (A ⊎ B)
(sumᴬ +Sum sumᴮ) f = sumᴬ (f ∘ inj₁) + sumᴮ (f ∘ inj₂)

_+μ_ : ∀ {A B} → SumPropoid A → SumPropoid B → SumPropoid (A ⊎-setoid B)
μA +μ μB = _ , search-ind μA +SearchInd search-ind μB

infixr 4 _×Search_

-- liftM2 _,_ in the continuation monad
_×Search_ : ∀ {A B} → Search A → Search B → Search (A × B)
(searchᴬ ×Search searchᴮ) op f = searchᴬ op (λ x → searchᴮ op (curry f x))

_×SearchInd_ : ∀ {A B} {sᴬ : Search A} {sᴮ : Search B}
               → SearchInd sᴬ → SearchInd sᴮ → SearchInd (sᴬ ×Search sᴮ)
(Psᴬ ×SearchInd Psᴮ) P P∙ Pf =
  Psᴬ (λ s → P (λ _ _ → s _ _)) P∙ (Psᴮ (λ s → P (λ _ _ → s _ _)) P∙ ∘ curry Pf)

_×SearchExt_ : ∀ {A B} {sᴬ : Search A} {sᴮ : Search B} →
              SearchExt sᴬ → SearchExt sᴮ → SearchExt (sᴬ ×Search sᴮ)
(sᴬ-ext ×SearchExt sᴮ-ext) sg f≗g = sᴬ-ext sg (sᴮ-ext sg ∘ curry f≗g)

infixr 4 _×Sum_

-- liftM2 _,_ in the continuation monad
_×Sum_ : ∀ {A B} → Sum A → Sum B → Sum (A × B)
(sumᴬ ×Sum sumᴮ) f = sumᴬ (λ x₀ →
                       sumᴮ (λ x₁ →
                         f (x₀ , x₁)))

infixr 4 _×μ_

_×μ_ : ∀ {A B} → SumPropoid A → SumPropoid B → SumPropoid (A ×-setoid B)
μA ×μ μB = _ , search-ind μA ×SearchInd search-ind μB

sum-const : ∀ {A} (μA : SumProp A) → ∀ k → sum μA (const k) ≡ Card μA * k
sum-const μA k
  rewrite ℕ°.*-comm (Card μA) k
        | ≡.sym (sum-lin μA (const 1) k)
        | proj₂ ℕ°.*-identity k = ≡.refl

infixr 4 _×Sum-proj₁_ _×Sum-proj₁'_ _×Sum-proj₂_ _×Sum-proj₂'_

_×Sum-proj₁_ : ∀ {A B}
                 (μA : SumProp A)
                 (μB : SumProp B)
                 f →
                 sum (μA ×μ μB) (f ∘ proj₁) ≡ Card μB * sum μA f
(μA ×Sum-proj₁ μB) f
  rewrite sum-ext μA (sum-const μB ∘ f)
        = sum-lin μA f (Card μB)

_×Sum-proj₂_ : ∀ {A B}
                 (μA : SumProp A)
                 (μB : SumProp B)
                 f →
                 sum (μA ×μ μB) (f ∘ proj₂) ≡ Card μA * sum μB f
(μA ×Sum-proj₂ μB) f = sum-const μA (sum μB f)

_×Sum-proj₁'_ : ∀ {A B}
                  (μA : SumProp A) (μB : SumProp B)
                  {f} {g} →
                  sum μA f ≡ sum μA g →
                  sum (μA ×μ μB) (f ∘ proj₁) ≡ sum (μA ×μ μB) (g ∘ proj₁)
(μA ×Sum-proj₁' μB) {f} {g} sumf≡sumg
  rewrite (μA ×Sum-proj₁ μB) f
        | (μA ×Sum-proj₁ μB) g
        | sumf≡sumg = ≡.refl

_×Sum-proj₂'_ : ∀ {A B}
                  (μA : SumProp A) (μB : SumProp B)
                  {f} {g} →
                  sum μB f ≡ sum μB g →
                  sum (μA ×μ μB) (f ∘ proj₂) ≡ sum (μA ×μ μB) (g ∘ proj₂)
(μA ×Sum-proj₂' μB) sumf≡sumg = sum-ext μA (const sumf≡sumg)

μ-view : ∀ {A B} → (A FE.⟶ B) → SumPropoid A → SumPropoid B
μ-view {A}{B} A→B μA = searchᴮ , ind
  where
    searchᴮ : Search (Setoid.Carrier B)
    searchᴮ m f = search μA m (f ∘ _⟨$⟩_ A→B)

    ind : SearchInd searchᴮ
    ind P P∙ Pf = search-ind μA (λ s → P (λ _ f → s _ (f ∘ _⟨$⟩_ A→B))) P∙ (Pf ∘ _⟨$⟩_ A→B)

μ-iso : ∀ {A B} → (FI.Inverse A B) → SumPropoid A → SumPropoid B
μ-iso A↔B = μ-view (Inverse.to A↔B)

μ-view-preserve : ∀ {A B} (A→B : A FE.⟶ B)(B→A : B FE.⟶ A)(A≈B : A→B RightInverseOf B→A)
                  (f : A FE.⟶ ≡.setoid ℕ) (μA : SumPropoid A)
                → sum μA (_⟨$⟩_ f) ≡ sum (μ-view A→B μA) (_⟨$⟩_ (f FE.∘  B→A))
μ-view-preserve {A}{B} A→B B→A A≈B f μA = sum-ext μA (λ x → FE.cong f (Setoid.sym A (A≈B x) ))

μ-iso-preserve : ∀ {A B} (A↔B : A ↔ B) f (μA : SumProp A) → sum μA f ≡ sum (μ-iso A↔B μA) (f ∘ _⟨$⟩_ (Inverse.from A↔B))
μ-iso-preserve A↔B f μA = μ-view-preserve (Inverse.to A↔B) (Inverse.from A↔B)
                            (Inverse.left-inverse-of A↔B)
                          (≡.:→-to-Π f) μA

open import Data.Fin using (Fin; zero; suc)
open import Data.Vec.NP as Vec using (Vec; tabulate; _++_) renaming (map to vmap; sum to vsum; foldr to vfoldr; foldr₁ to vfoldr₁)

vmsum : ∀ m {n} → let open Mon m in
                  Vec C n → C
vmsum m = vfoldr _ _∙_ ε
  where open Monoid m

vsgsum : ∀ sg {n} → let open Sgrp sg in
                    Vec C (suc n) → C
vsgsum sg = vfoldr₁ _∙_
  where open Sgrp sg

-- let's recall that: tabulate f ≗ vmap f (allFin n)

-- searchMonFin : ∀ n → SearchMon (Fin n)
-- searchMonFin n m f = vmsum m (tabulate f)

searchFinSuc : ∀ n → Search (Fin (suc n))
searchFinSuc n _∙_ f = vfoldr₁ _∙_ (tabulate f)

μMaybe : ∀ {A} → SumProp A → SumProp (Maybe A)
μMaybe μA = srch , ind where
  srch : Search (Maybe _)
  srch _∙_ f = f nothing ∙ search μA _∙_ (f ∘ just)
  ind : SearchInd srch
  ind P _P∙_ Pf = Pf nothing
               P∙ search-ind μA (λ s → P (λ op f → s op (f ∘ just))  ) _P∙_ (Pf ∘ just)

μMaybeIso : ∀ {A} → SumProp A → SumProp (Maybe A)
μMaybeIso μA = μ-iso (FI.sym Maybe↔𝟙⊎ FI.∘ lift-⊎) (μ𝟙 +μ μA)

μMaybe^ : ∀ {A} n → SumProp A → SumProp (Maybe^ n A)
μMaybe^ zero    μA = μA
μMaybe^ (suc n) μA = μMaybe (μMaybe^ n μA)

μFinSuc : ∀ n → SumProp (Fin (suc n))
μFinSuc n = searchFinSuc n , ind n
  where ind : ∀ n → SearchInd (searchFinSuc n)
        ind zero    P P∙ Pf = Pf zero
        ind (suc n) P P∙ Pf = P∙ (Pf zero) (ind n (λ s → P (λ op f → s op (f ∘ suc))) P∙ (Pf ∘ suc))
-- -}
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import Agda.Primitive

open import Equality

module Quotient where

  is-prop : ∀ {ℓ} (A : Set ℓ) → Set ℓ
  is-prop A = ∀ (x y : A) → x ≡ y

  record is-equivalence {ℓ k} {A : Set ℓ} (E : A → A → Set k) : Set (ℓ ⊔ k) where
    field
      equiv-prop : ∀ {x y} → is-prop (E x y)
      equiv-refl : ∀ {x} → E x x
      equiv-symm : ∀ {x y} → E x y → E y x
      equiv-tran : ∀ {x y z} → E x y → E y z → E x z

  record Equivalence {ℓ} (A : Set ℓ) : Set (lsuc ℓ) where
    field
      equiv-relation : A → A → Set ℓ
      equiv-is-equivalence : is-equivalence equiv-relation

  is-set : ∀ {ℓ} (A : Set ℓ) → Set ℓ
  is-set A = ∀ (x y : A) (p q : x ≡ y) → p ≡ q

  record HSet ℓ : Set (lsuc ℓ) where
    field
      hset-type : Set ℓ
      hset-is-set : is-set hset-type

  record Quotient {ℓ} (A : Set ℓ) (E : Equivalence A) : Set (lsuc ℓ) where
    open Equivalence

    field
      quot-type : Set ℓ
      quot-class : ∀ (x : A) → quot-type
      quot-≡ : ∀ {x y : A} → equiv-relation E x y → quot-class x ≡ quot-class y
      quot-is-set : is-set quot-type
      quot-elim :
        ∀ (B : ∀ quot-type → Set ℓ)
          (f : ∀ (x : A) → B (quot-class x)) →
          (∀ (x y : A) {ε : equiv-relation E x y} → transport B (quot-≡ ε) (f x) ≡ f y) →
          ∀ (ξ : quot-type) → B ξ
      quot-compute :
        ∀ (B : ∀ quot-type → Set ℓ)  →
          (f : ∀ (x : A) → B (quot-class x)) →
          (η : ∀ (x y : A) {ε : equiv-relation E x y} → transport B (quot-≡ ε) (f x) ≡ f y) →
          (quot-elim ? quot-class η)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

open import HoTT
open import lib.cubical.elims.CubeMove
open import lib.cubical.elims.CofWedge

module lib.cubical.elims.SuspSmash where

module _ {i j k} {X : Ptd i} {Y : Ptd j} {C : Type k}
  (f : Suspension (X ∧ Y) → C) (g : Suspension (X ∧ Y) → C)
  (north* : f (north _) == g (north _))
  (south* : f (south _) == g (south _))
  (cod* : (s : fst X × fst Y) → Square north* (ap f (merid _ (cfcod _ s)))
                                (ap g (merid _ (cfcod _ s))) south*)
  where

  private
    base* = transport
      (λ κ → Square north* (ap f (merid _ κ)) (ap g (merid _ κ)) south*)
      (! (cfglue _ (winl (snd X))))
      (cod* (snd X , snd Y))

    CubeType : (w : X ∨ Y)
      → Square north* (ap f (merid _ (cfcod _ (∨-in-× X Y w))))
               (ap g (merid _ (cfcod _ (∨-in-× X Y w)))) south*
      → Type _
    CubeType w sq =
      Cube base* sq
        (natural-square (λ _ → north*) (cfglue _ w))
        (natural-square (ap f ∘ merid _) (cfglue _ w))
        (natural-square (ap g ∘ merid _) (cfglue _ w))
        (natural-square (λ _ → south*) (cfglue _ w))

    fill : (w : X ∨ Y)
      (sq : Square north* (ap f (merid _ (cfcod _ (∨-in-× X Y w))))
                   (ap g (merid _ (cfcod _ (∨-in-× X Y w)))) south*)
      → Σ (Square north* idp idp north*) (λ p → CubeType w (p ⊡h sq))
    fill w sq =
      (fst fill' ,
       cube-right-from-front (fst fill') sq (snd fill'))
      where
      fill' = fill-cube-right _ _ _ _ _

    fill0 = fill (winl (snd X)) (cod* (snd X , snd Y))
    fillX = λ x → fill (winl x) (fst fill0 ⊡h cod* (x , snd Y))
    fillY = λ y → fill (winr y) (fst fill0 ⊡h cod* (snd X , y))

    fillX0 : fst (fillX (snd X)) == hid-square
    fillX0 = ⊡h-unit-l-unique _ (fst fill0 ⊡h cod* (snd X , snd Y))
               (fill-cube-right-unique (snd (fillX (snd X)))
                ∙ ! (fill-cube-right-unique (snd fill0)))

    fillY0 : fst (fillY (snd Y)) == hid-square
    fillY0 = ⊡h-unit-l-unique _ (fst fill0 ⊡h cod* (snd X , snd Y))
               (fill-cube-right-unique (snd (fillY (snd Y)))
                ∙ ! (fill-cube-right-unique
                       (snd (fill (winr (snd Y)) (cod* (snd X , snd Y)))))
                ∙ ! (ap (λ w → fst (fill w (cod* (∨-in-× X Y w)))
                                ⊡h cod* (snd X , snd Y))
                     wglue))
      where
      fill-square : (w : X ∨ Y)
        → Square north* (ap f (merid _ (cfcod _ (∨-in-× X Y w))))
                 (ap g (merid _ (cfcod _ (∨-in-× X Y w)))) south*
      fill-square w =
        fst (fill-cube-right base*
              (natural-square (λ _ → north*) (cfglue _ w))
              (natural-square (ap f ∘ merid _) (cfglue _ w))
              (natural-square (ap g ∘ merid _) (cfglue _ w))
              (natural-square (λ _ → south*) (cfglue _ w)))

    abstract
      coh : (s : X ∧ Y)
        → north* == south* [ (λ z → f z == g z) ↓ merid _ s ]
      coh = ↓-='-from-square ∘ cof-wedge-square-elim _ _ _ _
        base*
        (λ {(x , y) →
          fst (fillX x) ⊡h fst (fillY y) ⊡h fst fill0 ⊡h cod* (x , y)})
        (λ x → transport (λ sq → CubeType (winl x) (fst (fillX x) ⊡h sq))
          (! (ap (λ sq' → sq' ⊡h fst fill0 ⊡h cod* (x , snd Y)) fillY0
              ∙ ⊡h-unit-l (fst fill0 ⊡h cod* (x , snd Y))))
          (snd (fillX x)))
        (λ y → transport (CubeType (winr y))
          (! (ap (λ sq' → sq' ⊡h fst (fillY y) ⊡h fst fill0 ⊡h cod* (snd X , y))
                 fillX0
              ∙ ⊡h-unit-l (fst (fillY y) ⊡h fst fill0 ⊡h cod* (snd X , y))))
        (snd (fillY y)))

  susp-smash-path-elim : ((σ : Suspension (X ∧ Y)) → f σ == g σ)
  susp-smash-path-elim = Suspension-elim _ north* south* coh

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors where at least one element satisfies a given property
------------------------------------------------------------------------

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

module Data.Vec.Relation.Unary.Any {a} {A : Set a} where

open import Data.Empty
open import Data.Fin
open import Data.Nat using (zero; suc)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Vec as Vec using (Vec; []; [_]; _∷_)
open import Data.Product as Prod using (∃; _,_)
open import Level using (_⊔_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary

------------------------------------------------------------------------
-- Any P xs means that at least one element in xs satisfies P.

data Any {p} (P : A → Set p) : ∀ {n} → Vec A n → Set (a ⊔ p) where
  here  : ∀ {n x} {xs : Vec A n} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {n x} {xs : Vec A n} (pxs : Any P xs) → Any P (x ∷ xs)

------------------------------------------------------------------------
-- Operations on Any

module _ {p} {P : A → Set p} {n x} {xs : Vec A n} where

-- If the tail does not satisfy the predicate, then the head will.

  head : ¬ Any P xs → Any P (x ∷ xs) → P x
  head ¬pxs (here px)   = px
  head ¬pxs (there pxs) = contradiction pxs ¬pxs

-- If the head does not satisfy the predicate, then the tail will.
  tail : ¬ P x → Any P (x ∷ xs) → Any P xs
  tail ¬px (here  px)  = ⊥-elim (¬px px)
  tail ¬px (there pxs) = pxs

-- Convert back and forth with sum
  toSum : Any P (x ∷ xs) → P x ⊎ Any P xs
  toSum (here px)   = inj₁ px
  toSum (there pxs) = inj₂ pxs

  fromSum : P x ⊎ Any P xs → Any P (x ∷ xs)
  fromSum = [ here , there ]′

map : ∀ {p q} {P : A → Set p} {Q : A → Set q} →
      P ⊆ Q → ∀ {n} → Any P {n} ⊆ Any Q {n}
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

index : ∀ {p} {P : A → Set p} {n} {xs : Vec A n} → Any P xs → Fin n
index (here  px)  = zero
index (there pxs) = suc (index pxs)

-- If any element satisfies P, then P is satisfied.
satisfied : ∀ {p} {P : A → Set p} {n} {xs : Vec A n} → Any P xs → ∃ P
satisfied (here px)   = _ , px
satisfied (there pxs) = satisfied pxs

------------------------------------------------------------------------
-- Properties of predicates preserved by Any

module _ {p} {P : A → Set p} where

  any : Decidable P → ∀ {n} → Decidable (Any P {n})
  any P? []       = no λ()
  any P? (x ∷ xs) with P? x
  ... | yes px = yes (here px)
  ... | no ¬px = Dec.map′ there (tail ¬px) (any P? xs)

  satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n})
  satisfiable (x , p) {zero}  = x ∷ [] , here p
  satisfiable (x , p) {suc n} = Prod.map (x ∷_) there (satisfiable (x , p))


text:
{-# OPTIONS --sized-types #-}
module BBHeap.Height {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_ hiding (#)
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import SNat

# : {b : Bound} → BBHeap b → SNat
# leaf = zero
# (left {l = l} {r = r} _ _) = succ (# l + # r)
# (right {l = l} {r = r} _ _) = succ (# l + # r)

height : {b : Bound} → BBHeap b → SNat
height leaf = zero
height (left {l = l} _ _) = succ (height l)
height (right {l = l} _ _) = succ (height l)

#' : {b : Bound} → BBHeap b → SNat
#' leaf = zero
#' (left {r = r}  _ _) = succ (#' r + #' r)
#' (right {r = r} _ _) = succ (#' r + #' r)

height' : {b : Bound} → BBHeap b → SNat
height' leaf = zero
height' (left {r = r} _ _) = succ (height' r)
height' (right {r = r} _ _) = succ (height' r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Relation.Binary.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.HITs.SetQuotients.Base

module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : A → A → Type ℓ') where
  isRefl : Type (ℓ-max ℓ ℓ')
  isRefl = (a : A) → R a a

  isSym : Type (ℓ-max ℓ ℓ')
  isSym = (a b : A) → R a b → R b a

  isTrans : Type (ℓ-max ℓ ℓ')
  isTrans = (a b c : A)  → R a b → R b c → R a c

  record isEquivRel : Type (ℓ-max ℓ ℓ') where
    constructor EquivRel
    field
      reflexive : isRefl
      symmetric : isSym
      transitive : isTrans

  isPropValued : Type (ℓ-max ℓ ℓ')
  isPropValued = (a b : A) → isProp (R a b)

  isEffective : Type (ℓ-max ℓ ℓ')
  isEffective = (a b : A) →
    let x : A / R
        x = [ a ]
        y : A / R
        y = [ b ]
    in (x ≡ y) ≃ R a b

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

module Properties where

import Properties.Contradiction
import Properties.Dec
import Properties.DecSubtyping
import Properties.Equality
import Properties.Functions
import Properties.Remember
import Properties.Step
import Properties.StrictMode
import Properties.Subtyping
import Properties.TypeCheck
import Properties.TypeNormalization

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


text:
{-# OPTIONS --rewriting        #-}
{-# OPTIONS --confluence-check #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

module _ (A : Set) where
  postulate
    D : Set
    f : D → D → D
    r : (x y z : D) → f x (f y z) ≡ f x z

  {-# REWRITE r #-}
  -- WAS:
  -- Confluence check failed: f x (f y (f y₁ z)) reduces to both
  -- f x (f y₁ z) and f x (f y z) which are not equal because
  -- y != y₁ of type D
  -- when checking confluence of the rewrite rule r with itself

  module _ (x y y₁ z : D) where
    -- SUCCEEDS:
    _ : f x (f y₁ z) ≡ f x (f y z)
    _ = refl

max_stars_repo_name: Soares/agda

max_issues_repo_name: Soares/agda

max_forks_repo_name: Soares/agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import Util.PKCS
open import Util.Prelude
open import Yasm.Types

-- This module defines the types used to define a SystemModel.
module Yasm.Base (ℓ-PeerState : Level) where
 -- Our system is configured through a value of type
 -- SystemParameters where we specify:
 record SystemTypeParameters : Set (ℓ+1 ℓ-PeerState) where
  constructor mkSysTypeParms
  field
    PeerId    : Set
    _≟PeerId_ : ∀ (p₁ p₂ : PeerId) → Dec (p₁ ≡ p₂)
    Bootstrap : Set
    -- A relation specifying what Signatures are included in bootstrapInfo
    ∈BootstrapInfo  : Bootstrap → Signature → Set
    PeerState : Set ℓ-PeerState
    Msg       : Set
    Part      : Set -- Types of interest that can be represented in Msgs

    -- The messages must be able to carry signatures
    instance Part-sig : WithSig Part

    -- A relation specifying what Parts are included in a Msg.

    -- TODO-2: I changed the name of this to append the G because of the pain disambiguating it from
    -- NetworkMsg.⊂Msg.  This issue https://github.com/agda/agda/issues/2175 suggests I should have
    -- been able to get this right without renaming, but...  I'd like to underastand how to do this
    -- right, but for expedience, not now.
    _⊂MsgG_       : Part → Msg → Set

 module _ (systypes : SystemTypeParameters) where
   open SystemTypeParameters systypes

   record SystemInitAndHandlers : Set (ℓ+1 ℓ-PeerState) where
    constructor mkSysInitAndHandlers
    field
      -- The same bootstrap information is given to any uninitialised peer before
      -- it can handle any messages.
      bootstrapInfo : Bootstrap

      -- Represents an uninitialised PeerState, about which we know nothing whatsoever
      initPS    : PeerState

      -- Bootstraps a peer.  Our current system model is simplistic in that unsuccessful
      -- initialisation of a peer has no side effects.  In future, we could change the return type
      -- of bootstrap to Maybe PeerState × List (Action Msg), allowing for it to return nothing, but
      -- to include actions such as sending messages, logging, etc.  We are not doing so now as it
      -- is disruptive to existing proofs and modeling and verifying properties about unsuccessful
      -- initialisation is not a priority.
      bootstrap : PeerId → Bootstrap → Maybe (PeerState × List (Action Msg))

      -- Handles a message on a previously initialized peer.
      handle : PeerId → Msg → PeerState → PeerState × List (Action Msg)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Nullary.HLevels where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Functions.Fixpoint

open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    A : Type ℓ

isPropPopulated : isProp (Populated A)
isPropPopulated = isPropΠ λ x → 2-Constant→isPropFixpoint (x .fst) (x .snd)

isPropHSeparated : isProp (HSeparated A)
isPropHSeparated f g i x y a = HSeparated→isSet f x y (f x y a) (g x y a) i

isPropCollapsible≡ : isProp (Collapsible≡ A)
isPropCollapsible≡ {A = A} f = (isPropΠ2 λ x y → isPropCollapsiblePointwise) f where
  sA : isSet A
  sA = Collapsible≡→isSet f
  gA : isGroupoid A
  gA = isSet→isGroupoid sA
  isPropCollapsiblePointwise : ∀ {x y} → isProp (Collapsible (x ≡ y))
  isPropCollapsiblePointwise {x} {y} (a , ca) (b , cb) = λ i → endoFunction i , endoFunctionIsConstant i where
    endoFunction : a ≡ b
    endoFunction = funExt λ p → sA _ _ (a p) (b p)
    isProp2-Constant : (k : I) → isProp (2-Constant (endoFunction k))
    isProp2-Constant k = isPropΠ2 λ r s → gA x y (endoFunction k r) (endoFunction k s)
    endoFunctionIsConstant : PathP (λ i → 2-Constant (endoFunction i)) ca cb
    endoFunctionIsConstant = isProp→PathP isProp2-Constant ca cb

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

module Test₁ where

  macro

    Unify-with-⊤ : Term → TC ⊤
    Unify-with-⊤ goal = unify goal (quoteTerm ⊤)

  ⊤′ : Set
  ⊤′ = Unify-with-⊤

  unit-test : ⊤′
  unit-test = tt

module Test₂ where

  macro

    Unify-with-⊤ : Term → TC ⊤
    Unify-with-⊤ goal = noConstraints (unify goal (quoteTerm ⊤))

  ⊤′ : Set
  ⊤′ = Unify-with-⊤

  unit-test : ⊤′
  unit-test = tt

module Test₃ where

  P : Bool → Set
  P true  = Bool
  P false = Bool

  f : (b : Bool) → P b
  f true  = true
  f false = false

  pattern varg x = arg (arg-info visible relevant) x

  create-constraint : TC Set
  create-constraint =
    unquoteTC (def (quote P)
                 (varg (def (quote f) (varg unknown ∷ [])) ∷ []))

  macro

    Unify-with-⊤ : Term → TC ⊤
    Unify-with-⊤ goal =
      catchTC (noConstraints (bindTC create-constraint λ _ →
                              returnTC tt))
              (unify goal (quoteTerm ⊤))

  ⊤′ : Set
  ⊤′ = Unify-with-⊤

  unit-test : ⊤′
  unit-test = tt


text:
module IndexOnBuiltin where

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

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

data Fin : Nat -> Set where
  fz : {n : Nat} -> Fin (suc n)
  fs : {n : Nat} -> Fin n -> Fin (suc n)

f : Fin 2 -> Fin 1
f fz     = fz
f (fs i) = i

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --allow-unsolved-metas     #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module AgdaIntroduction where

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/Nat.agda).
infixl 10 _*_
infixl 9  _+_
infixr 5  _∷_ _++_
infix  4  _≡_

-- Dependent function types
id : (A : Set) → A → A
id A x = x

-- λ-notation
id₂ : (A : Set) → A → A
id₂ = λ A → λ x → x

id₃ : (A : Set) → A → A
id₃ = λ A x → x

-- Implicit arguments
id₄ : {A : Set} → A → A
id₄ x = x

id₅ : {A : Set} → A → A
id₅ = λ x → x

-- Inductively defined sets and families
data Bool : Set where
  false true : Bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

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

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (succ n)

data Fin : ℕ → Set where
  fzero : {n : ℕ} → Fin (succ n)
  fsucc : {n : ℕ} → Fin n → Fin (succ n)

-- Structurally recursive functions and pattern matching
_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)

map : {A B : Set} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

f : ℕ → ℕ
f zero = zero
{-# CATCHALL #-}
f _    = succ zero

-- The absurd pattern
magic : {A : Set} → Fin zero → A
magic ()

-- The with constructor

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

filter' : {A : Set} → (A → Bool) → List A → List A
filter' p [] = []
filter' p (x ∷ xs) with p x
filter' p (x ∷ xs) | true  = x ∷ filter' p xs
filter' p (x ∷ xs) | false = filter' p xs

-- Mutual definitions
even : ℕ → Bool
odd  : ℕ → Bool

even zero     = true
even (succ n) = odd n

odd zero   = false
odd (succ n) = even n

data EvenList : Set
data OddList  : Set

data EvenList where
  []  : EvenList
  _∷_ : ℕ → OddList → EvenList

data OddList where
  _∷_ : ℕ → EvenList → OddList

-- Normalisation

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

length : {A : Set} → List A → ℕ
length []       = zero
length (x ∷ xs) = succ zero + length xs

_++_ : {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

succCong : {m n : ℕ} → m ≡ n → succ m ≡ succ n
succCong refl = refl

length-++ : {A : Set}(xs ys : List A) →
            length (xs ++ ys) ≡ length xs + length ys
length-++ [] ys       = refl
length-++ (x ∷ xs) ys = succCong (length-++ xs ys)

-- Coverage and termination checkers
head : {A : Set} → List A → A
head []       = ?
head (x ∷ xs) = x

ack : ℕ → ℕ → ℕ
ack zero     n        = succ n
ack (succ m) zero     = ack m (succ zero)
ack (succ m) (succ n) = ack m (ack (succ m) n)

-- Combinators for equational reasoning

postulate
  sym   : {A : Set}{a b : A} → a ≡ b → b ≡ a
  trans : {A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
  subst : {A : Set}(P : A → Set){a b : A} → a ≡ b → P a → P b

postulate
  _*_             : ℕ → ℕ → ℕ
  *-comm          : ∀ m n → m * n ≡ n * m
  *-rightIdentity : ∀ n → n * succ zero ≡ n

*-leftIdentity : ∀ n → succ zero * n ≡ n
*-leftIdentity n =
  trans {ℕ} {succ zero * n} {n * succ zero} {n} (*-comm (succ zero) n) (*-rightIdentity n)

module ER
  {A     : Set}
  (_∼_   : A → A → Set)
  (∼-refl  : ∀ {x} → x ∼ x)
  (∼-trans : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z)
  where

  infixr 5 _∼⟨_⟩_
  infix  6 _∎

  _∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y ∼ z → x ∼ z
  _ ∼⟨ x∼y ⟩ y∼z = ∼-trans x∼y y∼z

  _∎ : ∀ x → x ∼ x
  _∎ _ = ∼-refl

open module ≡-Reasoning = ER _≡_ (refl {ℕ}) (trans {ℕ})
  renaming ( _∼⟨_⟩_ to _≡⟨_⟩_ )

*-leftIdentity' : ∀ n → succ zero * n ≡ n
*-leftIdentity' n =
  succ zero * n ≡⟨ *-comm (succ zero) n ⟩
  n * succ zero ≡⟨ *-rightIdentity n ⟩
  n             ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Data.Option.Proofs where

import      Lvl
open import Data
open import Data.Option
open import Data.Option.Functions
open import Functional
open import Structure.Setoid using (Equiv)
open import Structure.Function.Domain
open import Structure.Function
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level
private variable T A B C : Type{ℓ}
private variable x : T
private variable o : Option(T)

module _ where
  open Structure.Setoid
  open import Function.Equals

  module _ ⦃ _ : let _ = A ; _ = B ; _ = C in Equiv{ℓₑ}(Option(C)) ⦄ {f : B → C}{g : A → B} where
    map-preserves-[∘] : (map(f ∘ g) ⊜ (map f) ∘ (map g))
    _⊜_.proof map-preserves-[∘] {None}   = reflexivity(_≡_)
    _⊜_.proof map-preserves-[∘] {Some x} = reflexivity(_≡_)

  module _ ⦃ _ : Equiv{ℓₑ}(Option(A)) ⦄ where
    map-preserves-id : (map id ⊜ id)
    _⊜_.proof map-preserves-id {None}   = reflexivity(_≡_)
    _⊜_.proof map-preserves-id {Some x} = reflexivity(_≡_)

    andThenᵣ-Some : ((_andThen Some) ⊜ id)
    _⊜_.proof andThenᵣ-Some {None}   = reflexivity(_≡_)
    _⊜_.proof andThenᵣ-Some {Some x} = reflexivity(_≡_)

  module _ ⦃ _ : Equiv{ℓₑ}(Option(A)) ⦄ where
    andThenᵣ-None : o andThen (const{Y = Option(A)} None) ≡ None
    andThenᵣ-None {o = None}   = reflexivity(_≡_)
    andThenᵣ-None {o = Some x} = reflexivity(_≡_)

  module _ ⦃ _ : let _ = A in Equiv{ℓₑ}(Option(B)) ⦄ {f : A → Option(B)} where
    andThenₗ-None : (None andThen f ≡ None)
    andThenₗ-None = reflexivity(_≡_)

    andThenₗ-Some : (Some(x) andThen f ≡ f(x))
    andThenₗ-Some = reflexivity(_≡_)

  module _ ⦃ _ : let _ = A ; _ = B in Equiv{ℓₑ}(Option(C)) ⦄ {f : A → Option(B)} {g : B → Option(C)} where
    andThen-associativity : (o andThen (p ↦ f(p) andThen g) ≡ (o andThen f) andThen g)
    andThen-associativity {None}   = reflexivity(_≡_)
    andThen-associativity {Some x} = reflexivity(_≡_)

module _ where
  open import Function.Equals

  module _ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ ⦃ equiv-option-B : Equiv{ℓₑ}(Option B) ⦄ ⦃ some-func : Function(Some) ⦄  where
    map-function : Function(map {T₁ = A}{T₂ = B})
    Dependent._⊜_.proof (Function.congruence map-function (Dependent.intro p)) {None}   = reflexivity _
    Dependent._⊜_.proof (Function.congruence map-function (Dependent.intro p)) {Some x} = congruence₁(Some) p

  module _ ⦃ equiv-option-B : Equiv{ℓₑ}(Option B) ⦄ where
    andThen-function : Function(Functional.swap(_andThen_ {T₁ = A}{T₂ = B}))
    Dependent._⊜_.proof (Function.congruence andThen-function {f} {g} _)                   {None}   = reflexivity _
    Dependent._⊜_.proof (Function.congruence andThen-function {f} {g} (Dependent.intro p)) {Some x} = p{x}

module _
  ⦃ equiv-T     : Equiv{ℓₑ₁}(T) ⦄
  ⦃ equiv-opt-T : Equiv{ℓₑ₂}(Option(T)) ⦄
  ⦃ some-func   : Function(Some) ⦄
  {_▫_ : T → T → T}
  where

  open Structure.Setoid

  instance
    and-combine-associativity : ⦃ _ : Associativity(_▫_) ⦄ → Associativity(and-combine(_▫_))
    and-combine-associativity = intro p where
      p : Names.Associativity(and-combine(_▫_))
      p {None}   {None}   {None}   = reflexivity(_≡_)
      p {None}   {None}   {Some _} = reflexivity(_≡_)
      p {None}   {Some _} {None}   = reflexivity(_≡_)
      p {None}   {Some _} {Some _} = reflexivity(_≡_)
      p {Some _} {None}   {None}   = reflexivity(_≡_)
      p {Some _} {None}   {Some _} = reflexivity(_≡_)
      p {Some _} {Some _} {None}   = reflexivity(_≡_)
      p {Some _} {Some _} {Some _} = congruence₁(Some) (associativity(_▫_))

  module _ where --instance
    or-combine-associativity : ∀{f} ⦃ idemp-f : Idempotent(f) ⦄ (_ : ∀{x y} → (f(x) ▫ y ≡ f(x ▫ y))) (_ : ∀{x y} → (x ▫ f(y) ≡ f(x ▫ y))) → ⦃ _ : Associativity(_▫_) ⦄ → Associativity(or-combine(_▫_) f f) -- TODO: What are the unnamed properties here in the assumptions called? Also, the constant function of an absorber have all these properties. The identity function also have it.
    or-combine-associativity {f = f} compatₗ compatᵣ = intro p where
      p : Names.Associativity(or-combine(_▫_) f f)
      p {None}   {None}   {None}   = reflexivity(_≡_)
      p {None}   {None}   {Some z} = congruence₁(Some) (symmetry(_≡_) (idempotent(f)))
      p {None}   {Some y} {None}   = reflexivity(_≡_)
      p {None}   {Some y} {Some z} = congruence₁(Some) compatₗ
      p {Some x} {None}   {None}   = congruence₁(Some) (idempotent(f))
      p {Some x} {None}   {Some z} = congruence₁(Some) (transitivity(_≡_) compatₗ (symmetry(_≡_) compatᵣ))
      p {Some x} {Some y} {None}   = congruence₁(Some) (symmetry(_≡_) compatᵣ)
      p {Some x} {Some y} {Some z} = congruence₁(Some) (associativity(_▫_))

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

-- You probably want to start with this module:
import README

-- For a brief presentation of every single module, head over to
import Everything

-- Otherwise, here is an exhaustive, stern list of all the available modules:


text:
{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness #-}
module Agda.Builtin.Cubical.Glue where

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
                                             primHComp to hcomp; primTransp to transp; primComp to comp;
                                             itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to ouc)

module Helpers where
    -- Homogeneous filling
    hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
              (u : ∀ i → Partial φ A)
              (u0 : A [ φ ↦ u i0 ]) (i : I) → A
    hfill {φ = φ} u u0 i =
      hcomp (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
                     ; (i = i0) → ouc u0 })
            (ouc u0)

    -- Heterogeneous filling defined using comp
    fill : ∀ {ℓ : I → Level} (A : ∀ i → Set (ℓ i)) {φ : I}
             (u : ∀ i → Partial φ (A i))
             (u0 : A i0 [ φ ↦ u i0 ]) →
             ∀ i →  A i
    fill A {φ = φ} u u0 i =
      comp (λ j → A (i ∧ j)) _
           (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
                    ; (i = i0) → ouc u0 })
           (ouc {φ = φ} u0)

    module _ {ℓ} {A : Set ℓ} where
      refl : {x : A} → x ≡ x
      refl {x = x} = λ _ → x

      sym : {x y : A} → x ≡ y → y ≡ x
      sym p = λ i → p (~ i)

      cong : ∀ {ℓ'} {B : A → Set ℓ'} {x y : A}
             (f : (a : A) → B a) (p : x ≡ y)
           → PathP (λ i → B (p i)) (f x) (f y)
      cong f p = λ i → f (p i)

    isContr : ∀ {ℓ} → Set ℓ → Set ℓ
    isContr A = Σ A \ x → (∀ y → x ≡ y)

    fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ')
    fiber {A = A} f y = Σ A \ x → f x ≡ y

open Helpers

-- We make this a record so that isEquiv can be proved using
-- copatterns. This is good because copatterns don't get unfolded
-- unless a projection is applied so it should be more efficient.
record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
  field
    equiv-proof : (y : B) → isContr (fiber f y)

open isEquiv public

infix 4 _≃_

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) \ f → (isEquiv f)

equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
equivFun e = fst e

-- Improved version of equivProof compared to Lemma 5 in CCHM. We put
-- the (φ = i0) face in contr' making it be definitionally c in this
-- case. This makes the computational behavior better, in particular
-- for transp in Glue.
equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
           → ∀ ψ → (Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a
equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb
  where
    contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A
    contr' {A = A} (c , p) φ u = hcomp (λ i → λ { (φ = i1) → p (u 1=1) i
                                                ; (φ = i0) → c }) c

{-# BUILTIN EQUIV      _≃_        #-}
{-# BUILTIN EQUIVFUN   equivFun   #-}
{-# BUILTIN EQUIVPROOF equivProof #-}

primitive
    primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
      → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
      → Set ℓ'
    prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
      → PartialP φ T → A → primGlue A T e
    prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
      → primGlue A T e → A

    -- Needed for transp in Glue.
    primFaceForall : (I → I) → I

module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where
  private
    E : (i : I) → Set (ℓ i)
    E  = λ i → P i
    ~E : (i : I) → Set (ℓ (~ i))
    ~E = λ i → P (~ i)

    A = P i0
    B = P i1

    f : A → B
    f x = transp E i0 x

    g : B → A
    g y = transp ~E i0 y

    u : ∀ i → A → E i
    u i x = transp (λ j → E (i ∧ j)) (~ i) x

    v : ∀ i → B → E i
    v i y = transp (λ j → ~E ( ~ i ∧ j)) i y

    fiberPath : (y : B) → (xβ0 xβ1 : fiber f y) → xβ0 ≡ xβ1
    fiberPath y (x0 , β0) (x1 , β1) k = ω , λ j → δ (~ j) where
      module _ (j : I) where
        private
          sys : A → ∀ i → PartialP (~ j ∨ j) (λ _ → E (~ i))
          sys x i (j = i0) = v (~ i) y
          sys x i (j = i1) = u (~ i) x
        ω0 = comp ~E _ (sys x0) ((β0 (~ j)))
        ω1 = comp ~E _ (sys x1) ((β1 (~ j)))
        θ0 = fill ~E (sys x0) (inc (β0 (~ j)))
        θ1 = fill ~E (sys x1) (inc (β1 (~ j)))
      sys = λ {j (k = i0) → ω0 j ; j (k = i1) → ω1 j}
      ω = hcomp sys (g y)
      θ = hfill sys (inc (g y))
      δ = λ (j : I) → comp E _
            (λ i → λ { (j = i0) → v i y ; (k = i0) → θ0 j (~ i)
                     ; (j = i1) → u i ω ; (k = i1) → θ1 j (~ i) })
             (θ j)

    γ : (y : B) → y ≡ f (g y)
    γ y j = comp E _ (λ i → λ { (j = i0) → v i y
                            ; (j = i1) → u i (g y) }) (g y)

  pathToisEquiv : isEquiv f
  pathToisEquiv .equiv-proof y .fst .fst = g y
  pathToisEquiv .equiv-proof y .fst .snd = sym (γ y)
  pathToisEquiv .equiv-proof y .snd = fiberPath y _

  pathToEquiv : A ≃ B
  pathToEquiv .fst = f
  pathToEquiv .snd = pathToisEquiv

{-# BUILTIN PATHTOEQUIV pathToEquiv #-}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


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

-- Copied from "https://code.google.com/p/agda/issues/attachmentText?id=846&aid=8460000000&name=DivModUtils.agda&token=GDo1rQ6ldpTKOCjtbzSWPu19HL0%3A1373287197978"

module DivModUtils where

open import Data.Nat
open import Data.Bool
open import Data.Nat.DivMod
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Fin using (Fin; toℕ; zero; suc; fromℕ≤)
open import Data.Fin.Properties
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Relation.Binary
open import Data.Empty
open import Relation.Nullary.Negation
open ≡-Reasoning
open ≤-Reasoning
  renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩'_)
open DecTotalOrder decTotalOrder
  using () renaming (refl to ≤-refl; antisym to ≤-antisym)
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-comm; +-assoc)

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

i+[j∸m]≡i+j∸m : ∀ i j m → m ≤ j → i + (j ∸ m) ≡ i + j ∸ m
i+[j∸m]≡i+j∸m i zero zero lt = refl
i+[j∸m]≡i+j∸m i zero (suc m) ()
i+[j∸m]≡i+j∸m i (suc j) zero lt = refl
i+[j∸m]≡i+j∸m i (suc j) (suc m) (s≤s m≤j) = begin
  i + (j ∸ m)             ≡⟨ i+[j∸m]≡i+j∸m i j m m≤j ⟩
  suc (i + j) ∸ suc m     ≡⟨ cong (λ y → y ∸ suc m) $
                            solve 2
                              (λ i' j' → con 1 :+ (i' :+ j') := i' :+ (con 1 :+ j'))
                              refl i j ⟩
  (i + suc j) ∸ suc m ∎
  where open SemiringSolver

-- Following code taken from
-- https://github.com/copumpkin/derpa/blob/master/REPA/Index.agda#L210

-- the next few bits are lemmas to prove uniqueness of euclidean division

-- first : for nonzero divisors, a nonzero quotient would require a larger
-- dividend than is consistent with a zero quotient, regardless of
-- remainders.

large : ∀ {d} {r : Fin (suc d)} x (r′ : Fin (suc d)) → toℕ r ≢ suc x * suc d + toℕ r′
large {d} {r} x r′ pf = irrefl pf (
    start
      suc (toℕ r)
    ≤⟨ bounded r ⟩
      suc d
    ≤⟨ m≤m+n (suc d) (x * suc d) ⟩
      suc d + x * suc d -- same as (suc x * suc d)
    ≤⟨ m≤m+n (suc x * suc d) (toℕ r′) ⟩
      suc x * suc d + toℕ r′ -- clearer in two steps, and we'd need assoc anyway
    □)
  where
  open ≤-Reasoning
  open Relation.Binary.StrictTotalOrder Data.Nat.Properties.strictTotalOrder

-- a raw statement of the uniqueness, in the arrangement of terms that's
-- easiest to work with computationally

addMul-lemma′ : ∀ x x′ d (r r′ : Fin (suc d)) →
  x * suc d + toℕ r ≡ x′ * suc d + toℕ r′ → r ≡ r′ × x ≡ x′
addMul-lemma′ zero zero d r r′ hyp = (toℕ-injective hyp) , refl
addMul-lemma′ zero (suc x′) d r r′ hyp = ⊥-elim (large x′ r′ hyp)
addMul-lemma′ (suc x) zero d r r′ hyp = ⊥-elim (large x r (sym hyp))
addMul-lemma′ (suc x) (suc x′) d r r′ hyp
                      rewrite +-assoc (suc d) (x * suc d) (toℕ r)
                            | +-assoc (suc d) (x′ * suc d) (toℕ r′)
                      with addMul-lemma′ x x′ d r r′ (cancel-+-left (suc d) hyp)
... | pf₁ , pf₂ = pf₁ , cong suc pf₂

-- and now rearranged to the order that Data.Nat.DivMod uses

addMul-lemma : ∀ x x′ d (r r′ : Fin (suc d)) →
  toℕ r + x * suc d ≡ toℕ r′ + x′ * suc d → r ≡ r′ × x ≡ x′
addMul-lemma x x′ d r r′ hyp rewrite +-comm (toℕ r) (x * suc d)
                                   | +-comm (toℕ r′) (x′ * suc d)
  = addMul-lemma′ x x′ d r r′ hyp

DivMod-lemma : ∀ x d (r : Fin (suc d)) → (res : DivMod (toℕ r + x * suc d) (suc d)) →
  res ≡ result x r refl
DivMod-lemma x d r (result q r′ eq) with addMul-lemma x q d r r′ eq
DivMod-lemma x d r (result .x .r eq) | refl , refl =
  cong (result x r) (proof-irrelevance eq refl)

divMod-lemma : ∀ x d (r : Fin (suc d)) →
  (toℕ r + x * suc d) divMod suc d ≡ result x r refl
divMod-lemma x d r with (toℕ r + x * suc d) divMod suc d
divMod-lemma x d r | q rewrite DivMod-lemma x d r q = refl

mod-lemma : ∀ x d (r : Fin (suc d)) → (toℕ r + x * suc d) mod suc d ≡ r
mod-lemma x d r rewrite divMod-lemma x d r = refl

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Chain
  {U : Set}(T : U -> Set)
  (_==_ : {a b : U} -> T a -> T b -> Set)
  (refl : {a : U}(x : T a) -> x == x)
  (trans : {a b c : U}(x : T a)(y : T b)(z : T c) -> x == y -> y == z -> x == z)
  where

infix 30 _∼_
infix 3 proof_
infixl 2 _≡_by_
infix 1 _qed

data _∼_ {a b : U}(x : T a)(y : T b) : Set where
  prf : x == y -> x ∼ y

proof_ : {a : U}(x : T a) -> x ∼ x
proof x = prf (refl x)

_≡_by_ : {a b c : U}{x : T a}{y : T b} -> x ∼ y -> (z : T c) -> y == z -> x ∼ z
prf p ≡ z by q = prf (trans _ _ _ p q)

_qed : {a b : U}{x : T a}{y : T b} -> x ∼ y -> x == y
prf p qed = p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2013-03-15 issue reported by Nisse
-- {-# OPTIONS -v tc.proj:40 -v tc.conv.elim:40 #-}
module Issue821 where

import Common.Level

data D (A : Set) : Set where
  c : D A → D A

f : (A : Set) → D A → D A
f A (c x) = x

postulate
  A : Set
  P : D A → Set
  x : D A
  p : P x
  Q : P (f A x) → Set

Foo : Set₁
Foo = Q p

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:466

-- Reason was that f is projection-like so the test x =?= f A x
-- actually becomes x =?= x .f with unequal spine shapes (empty vs. non-empty).
-- Agda thought this was impossible.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda