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

module PragmasRespected where

postulate
  Foo : {A : Set₁} → Set
  Bar : Foo {A = Set}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
module gcd where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import nat
open import logic

open Factor

gcd1 : ( i i0 j j0 : ℕ ) → ℕ
gcd1 zero i0 zero j0 with <-cmp i0 j0
... | tri< a ¬b ¬c = i0
... | tri≈ ¬a refl ¬c = i0
... | tri> ¬a ¬b c = j0
gcd1 zero i0 (suc zero) j0 = 1
gcd1 zero zero (suc (suc j)) j0 = j0
gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
gcd1 (suc zero) i0 zero j0 = 1
gcd1 (suc (suc i)) i0 zero zero = i0
gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0

gcd : ( i j : ℕ ) → ℕ
gcd i j = gcd1 i i j j

gcd20 : (i : ℕ) → gcd i 0 ≡ i
gcd20 zero = refl
gcd20 (suc i) = gcd201 (suc i) where
    gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
    gcd201 zero = refl
    gcd201 (suc zero) = refl
    gcd201 (suc (suc i)) = refl

gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
gcd22 zero i0 zero o0 = refl
gcd22 zero i0 (suc o) o0 = refl
gcd22 (suc i) i0 zero o0 = refl
gcd22 (suc i) i0 (suc o) o0 = refl

gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
gcdmm zero m with <-cmp m m
... | tri< a ¬b ¬c = refl
... | tri≈ ¬a refl ¬c = refl
... | tri> ¬a ¬b c = refl
gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )

gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
gcdsym2 i j with <-cmp i j | <-cmp j i
... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c)
... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c)
... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
gcdsym1 zero zero zero zero = refl
gcdsym1 zero zero zero (suc j0) = refl
gcdsym1 zero (suc i0) zero zero = refl
gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
gcdsym1 zero zero (suc zero) j0 = refl
gcdsym1 zero zero (suc (suc j)) j0 = refl
gcdsym1 zero (suc i0) (suc zero) j0 = refl
gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
gcdsym1 (suc zero) i0 zero j0 = refl
gcdsym1 (suc (suc i)) i0 zero zero = refl
gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0)
gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )

gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
gcdsym {n} {m} = gcdsym1 n n m m

gcd11 : ( i  : ℕ ) → gcd i i ≡ i
gcd11 i = gcdmm i i

gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
gcd203 zero = refl
gcd203 (suc i) = gcd205 (suc i) where
   gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
   gcd205 zero = refl
   gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)

gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
gcd204 zero = refl
gcd204 (suc zero) = refl
gcd204 (suc (suc zero)) = refl
gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i))

gcd+j : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
gcd+j i j = gcd200 i i j j refl refl where
       gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
       gcd202 zero j1 = refl
       gcd202 (suc i) j1 = cong suc (gcd202 i j1)
       gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0
       gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl
       gcd201 i i0 j j0 (suc j1) = begin
          gcd1 (i + suc j1)   (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
          gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
          gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
          gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
       gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
       gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl
       gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
       gcd200 zero zero (suc zero) .1 i=i0 refl = refl
       gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin
          gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩
          suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩
          gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning
       gcd200 zero (suc i0) (suc j) .(suc j) () refl
       gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin
          gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩
          1 ≡⟨ sym ( gcd204 (suc j)) ⟩
          gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
       gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()

open _∧_

gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
   → Dividable k (i - j) ∧ Dividable k (j - i)
   → Dividable k ( gcd1 i i0 j j0 )
gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-j with <-cmp i0 j0
... | tri< a ¬b ¬c = i0f
... | tri≈ ¬a refl ¬c = i0f
... | tri> ¬a ¬b c = j0f
gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-j = ⊥-elim (div1 k>1 (proj2 i-j)) -- can't happen
gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = j0f
gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-j =
    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (proj2 i-j) (div-div k>1 i0f (proj2 i-j))
gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-j  = ⊥-elim (div1 k>1 (proj1 i-j)) -- can't happen
gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-j  = i0f
gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-j  = --
     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) (proj1 i-j) (decf (DtoF j0f)) j0f (div-div k>1 (proj1 i-j) j0f )
gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  =
     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j
gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  =
     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j

gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j )
   → Dividable k ( gcd i  j )
gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)

di-next : {i i0 j j0 : ℕ} → Dividable i0  ((j0 + suc i) - suc j ) ∧ Dividable j0 ((i0 + suc j) - suc i) →
           Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i)
di-next {i} {i0} {j} {j0} x =
      ⟪ ( subst (λ k → Dividable i0 (k - suc j)) ( begin
               j0 + suc i ≡⟨ sym (+-assoc j0 1 i ) ⟩
               (j0 + 1) + i ≡⟨ cong (λ k → k + i) (+-comm j0 _ ) ⟩
               suc (j0 + i) ∎ ) (proj1 x) ) ,
       ( subst (λ k → Dividable j0 (k - suc i)) ( begin
               i0 + suc j ≡⟨ sym (+-assoc i0 1 j ) ⟩
               (i0 + 1) + j ≡⟨ cong (λ k → k + j) (+-comm i0 _ ) ⟩
               suc (i0 + j) ∎ ) (proj2 x) ) ⟫
           where open ≡-Reasoning

di-next1 : {i0 j j0 : ℕ} →  Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∧ Dividable j0 (suc (i0 + suc (suc j)))
       →    Dividable (suc i0) ((suc (suc j) + i0) - suc j) ∧ Dividable (suc (suc j)) ((suc i0 + suc j) - i0)
di-next1 {i0} {j} {j0} x =
      ⟪ record { factor = 1 ; is-factor = begin
           1 * suc i0 + 0 ≡⟨ cong suc ( trans (+-comm _ 0)  (+-comm _ 0) ) ⟩
           suc i0  ≡⟨ sym (minus+y-y {suc i0} {j})  ⟩
           (suc i0 + j) - j ≡⟨ cong (λ k → k - j ) (+-comm (suc i0) _ ) ⟩
           (suc j + suc i0 ) - suc j ≡⟨ cong (λ k → k - suc j) (sym (+-assoc (suc j) 1 i0 ))  ⟩
           ((suc j + 1) + i0) - suc j ≡⟨ cong (λ k → (k + i0) - suc j) (+-comm _ 1) ⟩
           (suc (suc j) + i0) - suc j ∎ }  ,
        subst (λ k → Dividable (suc (suc j)) k) ( begin
               suc (suc j) ≡⟨ sym ( minus+y-y {suc (suc j)}{i0} ) ⟩
               (suc (suc j) + i0 ) - i0  ≡⟨ cong (λ k → (k + i0) - i0) (cong suc (+-comm 1 _ )) ⟩
               ((suc j + 1) + i0 ) - i0  ≡⟨ cong (λ k → k - i0) (+-assoc (suc j) 1  _ ) ⟩
               (suc j + suc i0 ) - i0  ≡⟨ cong (λ k → k - i0) (+-comm (suc j) _) ⟩
               ((suc i0 + suc j)   - i0) ∎ ) div= ⟫
           where open ≡-Reasoning

gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j
gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
     gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0  → gcd1 i i0 j j0 > 0
     gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0
     ... | tri< a ¬b ¬c = 0<i
     ... | tri≈ ¬a refl ¬c = 0<i
     ... | tri> ¬a ¬b c = 0<j
     gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n
     gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j
     gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j)
     gcd>01 (suc zero) i0 zero j0 0<i 0<j =  s≤s z≤n
     gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i
     gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i))  j0 (suc j0) (s≤s z≤n) 0<j
     gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where
         gcd033 : (i i0 j j0  : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡  gcd1 i i0 j j0
         gcd033 zero zero zero zero = refl
         gcd033 zero zero (suc j) zero = refl
         gcd033 (suc i) zero j zero = refl
         gcd033 zero zero zero (suc j0) = refl
         gcd033 (suc i) zero zero (suc j0) = refl
         gcd033 zero zero (suc j) (suc j0) = refl
         gcd033 (suc i) zero (suc j) (suc j0) = refl
         gcd033 zero (suc i0) j j0 = refl
         gcd033 (suc i) (suc i0) j j0 = refl

-- gcd loop invariant
--
record GCD ( i i0 j j0 : ℕ ) : Set where
   field
     i<i0  : i ≤ i0
     j<j0  : j ≤ j0
     div-i : Dividable i0 ((j0 + i) - j)
     div-j : Dividable j0 ((i0 + j) - i)

div-11 : {i j : ℕ } → Dividable i ((j + i) - j)
div-11 {i} {j} = record { factor = 1 ; is-factor = begin
   1 * i + 0 ≡⟨ +-comm _ 0  ⟩
   i + 0  ≡⟨  +-comm _ 0 ⟩
   i  ≡⟨ sym (minus+y-y {i} {j}) ⟩
   (i + j ) - j  ≡⟨ cong (λ k → k  - j ) (+-comm i j )  ⟩
   (j + i) - j ∎ } where open ≡-Reasoning

div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k
div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where
        decl : {m  : ℕ } → 0 < m → m - k < m
        decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m
        ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k
        ind m prev d with <-cmp (suc m) k
        ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= )
        ... | tri>  ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where
           ind1 : gcd (m - k) k ≡ gcd m k
           ind1 = begin
               gcd (m - k) k  ≡⟨ sym (gcd+j (m - k)  _) ⟩
               gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩
               gcd m k ∎ where open ≡-Reasoning
        ... | tri< a ¬b ¬c with <-cmp 0 m
        ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d )
        ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k)
        fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k
        fzero 0 eq d = trans  (gcdsym {0} {k} ) (gcd20 k)
        fzero (suc m) eq d with <-cmp (suc m) k
        ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d )
        ... | tri≈ ¬a refl ¬c = gcdmm k k
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) )
        I : Ninduction ℕ  _  (λ x → x)
        I = record {
              pnext = λ p → p - k
            ; fzero = λ {m} eq → fzero m eq
            ; decline = λ {m} lt → decl lt
            ; ind = λ {p} prev → ind p prev
          }

GCDi : {i j : ℕ } → GCD i i j j
GCDi {i} {j} = record { i<i0 = refl-≤ ; j<j0 = refl-≤ ; div-i = div-11 {i} {j} ; div-j = div-11 {j} {i} }

GCD-sym : {i i0 j j0 : ℕ} → GCD i i0 j j0 → GCD j j0 i i0
GCD-sym g = record { i<i0 = GCD.j<j0 g ; j<j0 = GCD.i<i0 g ; div-i = GCD.div-j g ; div-j = GCD.div-i g }

pred-≤ : {i i0 : ℕ } → suc i ≤ suc i0 → i ≤ suc i0
pred-≤ {i} {i0} (s≤s lt) = ≤-trans lt refl-≤s

gcd-next : {i i0 j j0 : ℕ} → GCD (suc i) i0 (suc j) j0 → GCD i i0 j j0
gcd-next {i} {0} {j} {0} ()
gcd-next {i} {suc i0} {j} {suc j0} g = record { i<i0 = pred-≤ (GCD.i<i0 g) ; j<j0 = pred-≤ (GCD.j<j0 g)
  ; div-i = proj1 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ )
  ; div-j = proj2 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }

gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD i0 (suc i0) (suc j) (suc (suc j))
gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s
  ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }

-- gcd-dividable1 : ( i i0 j j0 : ℕ )
--      → Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
--      → Dividable ( gcd1 i i0 j j0  ) i0 ∧ Dividable ( gcd1 i i0 j j0  ) j0
-- gcd-dividable1  zero i0 zero j0 with <-cmp i0 j0
-- ... | tri< a ¬b ¬c = ⟪ div= , {!!} ⟫ -- Dividable i0  (j0 + i - j ) ∧ Dividable j0 (i0 + j - i)
-- ... | tri≈ ¬a refl ¬c = {!!}
-- ... | tri> ¬a ¬b c = {!!}
-- gcd-dividable1 zero i0 (suc zero) j0 = {!!}
-- gcd-dividable1 i i0 j j0 = {!!}

gcd-dividable : ( i j  : ℕ )
      → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
gcd-dividable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
   {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
        F : ℕ ∧ ℕ → ℕ
        F ⟪ 0 , 0 ⟫ = 0
        F ⟪ 0 , suc j ⟫ = 0
        F ⟪ suc i , 0 ⟫ = 0
        F ⟪ suc i , suc j ⟫ with <-cmp i j
        ... | tri< a ¬b ¬c = suc j
        ... | tri≈ ¬a b ¬c = 0
        ... | tri> ¬a ¬b c = suc i
        F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0)
        F0 {zero} {zero} p = case1 refl
        F0 {zero} {suc j} p =  case2 (case1 refl)
        F0 {suc i} {zero} p =  case2 (case2 refl)
        F0 {suc i} {suc j} p with <-cmp i j
        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
        ... | tri≈ ¬a refl ¬c =  case1 refl
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
        F00 :  {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
        F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq
        ... | case1 refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
        ... | case2 (case1 refl) = ⟪  subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
                                    , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
        ... | case2 (case2 refl) = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
                                    , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫
        Fsym :  {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫
        Fsym {0} {0} = refl
        Fsym {0} {suc j} = refl
        Fsym {suc i} {0} = refl
        Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i
        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
        ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b))
        ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
        ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
        ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
        ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
        ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b))
        ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)

        record Fdec ( i j : ℕ ) : Set where
           field
               ni : ℕ
               nj : ℕ
               fdec :  0 < F ⟪ i , j ⟫  → F ⟪ ni , nj ⟫  < F ⟪ i , j ⟫

        fd1 : ( i j k : ℕ ) → i < j  → k ≡ j - i →  F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫
        fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j ))
        fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where
               fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i  →  F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫
               fd2 i j k i<j eq with <-cmp i k | <-cmp i j
               ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where
                    fd3 : suc k < suc j  -- suc j - suc i < suc j
                    fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n))
               ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j))
               ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j))
               ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n
               ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j)
               ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c =  s≤s z≤n -- i > j
               ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where
                    fd4 : suc i < suc j
                    fd4 = s≤s a
               ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c =  ⊥-elim (¬a₁ i<j)
               ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ =  ⊥-elim (¬a₁ i<j)

        fedc0 : (i j : ℕ ) → Fdec i j
        fedc0 0 0 = record { ni =  0 ; nj = 0 ; fdec = λ ()  }
        fedc0 (suc i) 0 = record { ni =  suc i ; nj = 0 ; fdec = λ ()  }
        fedc0 0 (suc j)  = record { ni =  0 ; nj = suc j ; fdec = λ ()  }
        fedc0 (suc i) (suc j) with <-cmp i j
        ... | tri< i<j ¬b ¬c = record { ni =  suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl  }
        ... | tri≈ ¬a refl ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where
              fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫
              fd0 {i} with <-cmp i i
              ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
              ... | tri≈ ¬a b ¬c = refl
              ... | tri> ¬a ¬b c =  ⊥-elim ( ¬b refl )
        ... | tri> ¬a ¬b c = record { ni =  i - j ; nj = suc j ; fdec = λ lt →
            subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) }

        ind3 : {i j : ℕ } → i < j
               → Dividable (gcd (suc i) (j - i)) (suc i)
               → Dividable (gcd (suc i) (suc j)) (suc i)
        ind3 {i} {j} a prev =
               subst (λ k → Dividable k (suc i)) ( begin
                 gcd (suc i) (j - i)  ≡⟨ gcdsym {suc i} {j - i} ⟩
                 gcd (j - i ) (suc i)   ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩
                 gcd ((j - i) + suc i) (suc i)  ≡⟨ cong (λ k → gcd k (suc i)) ( begin
                  (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n →  suc (suc i) ≤ suc (suc (suc n))
                  suc j ∎ ) ⟩
                 gcd (suc j) (suc i)  ≡⟨ gcdsym {suc j} {suc i} ⟩
                 gcd (suc i) (suc j)  ∎ ) prev where open ≡-Reasoning
        ind7 : {i j : ℕ } → (i < j ) → (j - i) + suc i ≡ suc j
        ind7 {i} {j} a = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa)  ⟩
                        suc j ∎  where open ≡-Reasoning
        ind6 : {i j k : ℕ } → i < j
               → Dividable k (j - i)
               → Dividable k (suc i)
               → Dividable k (suc j)
        ind6 {i} {j} {k} i<j dj di = subst (λ g → Dividable k g ) (ind7 i<j) (proj1 (div+div dj di))
        ind4 : {i j : ℕ } → i < j
               → Dividable (gcd (suc i) (j - i)) (j - i)
               → Dividable (gcd (suc i) (suc j)) (j - i)
        ind4 {i} {j} i<j prev = subst (λ k → k) ( begin
                 Dividable (gcd (suc i) (j - i)) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc i}  ) ⟩
                 Dividable (gcd (j - i ) (suc i) ) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) ( sym (gcd+j  (j - i) (suc i))) ⟩
                 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i)  ≡⟨ cong  (λ k → Dividable (gcd k (suc i)) (j - i)) (ind7 i<j ) ⟩
                 Dividable (gcd (suc j) (suc i)) (j - i)    ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩
                 Dividable (gcd (suc i) (suc j)) (j - i)   ∎ ) prev where open ≡-Reasoning

        ind :   ( i j : ℕ ) →
              Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j))
            ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j))
            → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
        ind zero zero prev = ind0 where
           ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero
           ind0 = ⟪ div0 , div0 ⟫
        ind zero (suc j) prev = ind1 where
           ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j)
           ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div=  ⟫
        ind (suc i) zero prev = ind2 where
           ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero
           ind2 = ⟪  subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫
        ind (suc i) (suc j) prev with <-cmp i j
        ... | tri< a ¬b ¬c = ⟪ ind3 a (proj1 prev)  , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫
        ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where
           ind5 : Dividable (gcd (suc i) (suc i)) (suc i)
           ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div=
        ... | tri> ¬a ¬b c = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c  (proj2 prev) ⟫ where
           ind9 : {i j : ℕ} → i < j → gcd (j - i) (suc i) ≡ gcd (suc j) (suc i)
           ind9 {i} {j} i<j = begin
                 gcd (j - i ) (suc i)    ≡⟨ sym (gcd+j (j - i ) (suc i)  ) ⟩
                 gcd (j - i + suc i) (suc i)    ≡⟨ cong (λ k → gcd k (suc i)) (ind7 i<j ) ⟩
                 gcd (suc j) (suc i)   ∎  where open ≡-Reasoning
           ind8 :  { i j : ℕ } → i < j
               → Dividable (gcd (j - i) (suc i)) (j - i)
               → Dividable (gcd (j - i) (suc i)) (suc i)
               → Dividable (gcd (suc j) (suc i)) (suc j)
           ind8 {i} {j} i<j dji di = ind6 i<j (subst (λ k → Dividable k (j - i)) (ind9 i<j) dji)  (subst (λ k → Dividable k (suc i)) (ind9 i<j) di)
           ind10 :  { i j : ℕ } → j < i
               → Dividable (gcd (i - j) (suc j)) (suc j)
               → Dividable (gcd (suc i) (suc j)) (suc j)
           ind10 {i} {j} j<i dji = subst (λ g → Dividable g (suc j) ) (begin
             gcd (i - j) (suc j)  ≡⟨ sym (gcd+j (i - j) (suc j)) ⟩
             gcd (i - j + suc j) (suc j)  ≡⟨ cong (λ k → gcd k (suc j)) (ind7 j<i ) ⟩
             gcd (suc i) (suc j) ∎ ) dji where open ≡-Reasoning

        I : Finduction (ℕ ∧ ℕ) _ F
        I = record {
              fzero = F00
            ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) ,  Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫
            ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p))  lt
            ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
          }

f-div>0 :  { k i  : ℕ } → (d : Dividable k i ) → 0 < i → 0 < Dividable.factor d
f-div>0 {k} {i} d 0<i with <-cmp 0 (Dividable.factor d)
... | tri< a ¬b ¬c = a
... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (begin
      0 * k + 0  ≡⟨ cong (λ g → g * k + 0) b  ⟩
      Dividable.factor d * k + 0  ≡⟨ Dividable.is-factor d ⟩
      i  ∎ ) 0<i ) where open ≡-Reasoning

gcd-≤i : ( i j  : ℕ ) → 0 < i → i ≤ j → gcd i j ≤ i
gcd-≤i zero _ () z≤n
gcd-≤i (suc i) (suc j) _ (s≤s i<j) = begin
      gcd (suc i) (suc j)   ≡⟨ sym m*1=m ⟩
      gcd (suc i) (suc j) * 1  ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩
      gcd (suc i) (suc j) * f  ≡⟨ +-comm 0 _ ⟩
      gcd (suc i) (suc j) * f  + 0  ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _  ) ⟩
      Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j)))  ⟩
      suc i  ∎ where
          d = proj1 (gcd-dividable (suc i) (suc j))
          f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j)))
          open ≤-Reasoning

gcd-≤ : { i j  : ℕ } → 0 < i → 0 < j  →  gcd i j ≤ i
gcd-≤ {i} {j} 0<i 0<j with <-cmp i j
... | tri< a ¬b ¬c = gcd-≤i i j 0<i (<to≤ a)
... | tri≈ ¬a refl ¬c = gcd-≤i i j 0<i refl-≤
... | tri> ¬a ¬b c = ≤-trans (subst (λ k → k ≤ j) (gcdsym {j} {i}) (gcd-≤i j i 0<j (<to≤ c))) (<to≤ c)

record Euclid (i j gcd : ℕ ) : Set where
  field
    eqa : ℕ
    eqb : ℕ
    is-equ< : eqa * i > eqb * j → (eqa * i) - (eqb * j) ≡ gcd
    is-equ> : eqb * j > eqa * i → (eqb * j) - (eqa * i) ≡ gcd
    is-equ= : eqa * i ≡ eqb * j → 0 ≡ gcd

ge3 : {a b c d : ℕ } → b > a → b - a ≡ d - c → d > c
ge3 {a} {b} {c} {d} b>a eq = minus>0→x<y (subst (λ k → 0 < k ) eq (minus>0 b>a))

ge01 : ( i0 j j0 ea eb : ℕ )
   → ( di : GCD 0 (suc i0) (suc (suc j)) j0 )
  →  (((ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0)  ≡ (ea * suc i0) + (eb * (Dividable.factor (GCD.div-i di)) ) * suc i0 )
        ∧ (  (eb * j0) ≡ (eb * suc (suc j) +  (eb * (Dividable.factor (GCD.div-i di)) ) * suc i0) )
ge01 i0 j j0 ea eb di  = ⟪ ge011 , ge012 ⟫ where
   f = Dividable.factor (GCD.div-i di)
   ge4 :  suc (j0 + 0) > suc (suc j)
   ge4 = subst (λ k → k > suc (suc j)) (+-comm 0 _ ) ( s≤s (GCD.j<j0  di ))
   ge011 :   (ea + eb * f) * suc i0 ≡ ea * suc i0 + eb * f * suc i0
   ge011 = begin
      (ea + eb * f) * suc i0 ≡⟨ *-distribʳ-+ (suc i0)  ea  _ ⟩
      ea * suc i0 + eb * f * suc i0 ∎ where open ≡-Reasoning
   ge012 :  eb * j0 ≡ eb * suc (suc j) + eb * f * suc i0
   ge012 = begin
      eb * j0  ≡⟨ cong (λ k → eb * k) ( begin
        j0 ≡⟨ +-comm 0 _ ⟩
        j0 + 0 ≡⟨ sym (minus+n {j0 + 0} {suc (suc j)} ge4)  ⟩
        ((j0 + 0) - (suc (suc j))) + suc (suc j) ≡⟨  +-comm _ (suc (suc j)) ⟩
        suc (suc j) + ((j0 + 0) -  suc (suc j)) ≡⟨ cong (λ k → suc (suc j) + k ) (sym (Dividable.is-factor (GCD.div-i di))) ⟩
        suc (suc j) + (f * suc i0 + 0) ≡⟨  cong (λ k → suc (suc j) + k )  ( +-comm _ 0  ) ⟩
        suc (suc j) + (f * suc i0 )  ∎  ) ⟩
      eb * (suc (suc j) + (f * suc i0 ) ) ≡⟨ *-distribˡ-+  eb (suc (suc j)) (f * suc i0) ⟩
      eb * suc (suc j) + eb * (f * suc i0) ≡⟨ cong (λ k → eb * suc (suc j) + k ) ((sym (*-assoc eb _ _ )) ) ⟩
      eb * suc (suc j) + eb * f * suc i0 ∎ where open ≡-Reasoning

ge20 : {i0 j0 : ℕ } →  i0 ≡ 0 → 0 ≡ gcd1 zero i0 zero j0
ge20 {i0} {zero} refl = refl
ge20 {i0} {suc j0} refl = refl

gcd-euclid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Euclid i0 j0 (gcd1 i i0 j j0)
gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0
... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () ; is-equ= = ge21 }  where
   ge21 : 1 * i0 ≡ 0 * j0 → 0 ≡ i0
   ge21 eq = trans (sym eq) (+-comm i0 0)
... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () ; is-equ= = λ eq →  trans (sym eq) (+-comm i0 0) }
... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 ; is-equ= = ge22 }  where
   ge22 : 0 * i0 ≡ 1 * j0 → 0 ≡ j0
   ge22 eq = trans eq (+-comm j0 0)
-- i<i0  : zero ≤ i0
-- j<j0  : 1 ≤ j0
-- div-i : Dividable i0 ((j0 + zero) - 1)  -- fi * i0 ≡ (j0 + zero) - 1
-- div-j : Dividable j0 ((i0 + 1) - zero) --  fj * j0 ≡ (i0 + 1) - zero
gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = Dividable.factor (GCD.div-j di) ; is-equ< = λ lt → ⊥-elim ( ge7 lt) ; is-equ> = λ _ → ge6
      ; is-equ= = λ eq → ⊥-elim (nat-≡< (sym (minus<=0 (subst (λ k → k ≤ 1 * i0) eq refl-≤ ))) (subst (λ k → 0 < k) (sym ge6) a<sa )) } where
   ge6 :  (Dividable.factor (GCD.div-j di) * j0) - (1 * i0) ≡ gcd1 zero i0 1 j0
   ge6  =  begin
        (Dividable.factor (GCD.div-j di) * j0) - (1 * i0)   ≡⟨  cong (λ k → k  - (1 * i0)) (+-comm 0 _)  ⟩
        (Dividable.factor (GCD.div-j di) * j0 + 0) - (1 * i0)   ≡⟨ cong (λ k → k  - (1 * i0)) (Dividable.is-factor (GCD.div-j di) )  ⟩
        ((i0 + 1) - zero) - (1 * i0)   ≡⟨ refl  ⟩
        (i0 + 1) - (i0 + 0)   ≡⟨ minus+yx-yz {_} {i0} {0}  ⟩
       1   ∎ where open ≡-Reasoning
   ge7 : ¬ ( 1 * i0 > Dividable.factor (GCD.div-j di) * j0 )
   ge7 lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6) (s≤s z≤n)))
gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0
    ; is-equ= = λ eq → subst (λ k → 0 ≡ k) (+-comm _ 0) eq }
gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
... | e = record { eqa = ea + eb * f ; eqb =  eb
      ;  is-equ= =  λ eq → Euclid.is-equ= e (ge23 eq)
      ;  is-equ< =  λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 )
      ;  is-equ> =  λ lt → subst (λ k → (eb * j0) - ((ea + eb * f) * suc i0) ≡ k ) (Euclid.is-equ> e (ge3 lt (ge2 ))) (ge2 ) } where
   ea = Euclid.eqa e
   eb = Euclid.eqb e
   f = Dividable.factor (GCD.div-i di)
   ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))
   ge1 = begin
      ((ea + eb * f) * suc i0) - (eb * j0) ≡⟨ cong₂ (λ j k → j - k ) (proj1 (ge01  i0 j j0 ea eb di)) (proj2 (ge01  i0 j j0 ea eb di))  ⟩
      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) )  ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)}  ⟩
      (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
   ge2 : (eb * j0) - ((ea + eb * f) * suc i0)  ≡  (eb * suc (suc j)) - (ea * suc i0)
   ge2 = begin
      (eb * j0) - ((ea + eb * f) * suc i0)  ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01  i0 j j0 ea eb di)) (proj1 (ge01  i0 j j0 ea eb di))  ⟩
      ( eb * suc (suc j) + ((eb * f) * (suc i0)) ) - (ea * suc i0 + (eb * f ) * suc i0 )   ≡⟨  minus+xy-zy {eb * suc (suc j)}{(eb * f ) * suc i0} {ea * suc i0}  ⟩
      (eb * suc (suc j)) - (ea * suc i0)   ∎ where open ≡-Reasoning
   ge23 : (ea + eb * f) * suc i0 ≡ eb * j0 → ea * suc i0 ≡ eb * suc (suc j)
   ge23 eq = begin
       ea * suc i0     ≡⟨ sym (minus+y-y {_} {(eb * f ) * suc i0} ) ⟩
       (ea * suc i0 +  ((eb * f ) * suc i0 )) -  ((eb * f ) * suc i0 )  ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 )) (sym ( proj1 (ge01  i0 j j0 ea eb di)))  ⟩
       ((ea + eb * f) * suc i0)  -  ((eb * f ) * suc i0 )  ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 ))  eq ⟩
        (eb * j0) -  ((eb * f ) * suc i0 )  ≡⟨  cong (λ k → k - ((eb * f ) * suc i0 )) ( proj2 (ge01  i0 j j0 ea eb di)) ⟩
       (eb * suc (suc j) +  ((eb * f ) * suc i0 )) -  ((eb * f ) * suc i0 )  ≡⟨ minus+y-y {_} {(eb * f ) * suc i0 }  ⟩
       eb * suc (suc j)   ∎ where open ≡-Reasoning
gcd-euclid1 (suc zero) i0 zero j0 di = record { eqb = 1 ; eqa = Dividable.factor (GCD.div-i di) ; is-equ> = λ lt → ⊥-elim ( ge7' lt) ; is-equ< = λ _ → ge6'
       ; is-equ= = λ eq → ⊥-elim (nat-≡< (sym (minus<=0 (subst (λ k → k ≤ 1 * j0) (sym eq) refl-≤ ))) (subst (λ k → 0 < k) (sym ge6') a<sa )) } where
   ge6' :  (Dividable.factor (GCD.div-i di) * i0) - (1 * j0) ≡ gcd1 (suc zero) i0 zero j0
   ge6'  =  begin
        (Dividable.factor (GCD.div-i di) * i0) - (1 * j0)   ≡⟨  cong (λ k → k  - (1 * j0)) (+-comm 0 _)  ⟩
        (Dividable.factor (GCD.div-i di) * i0 + 0) - (1 * j0)   ≡⟨ cong (λ k → k  - (1 * j0)) (Dividable.is-factor (GCD.div-i di) )  ⟩
        ((j0 + 1) - zero) - (1 * j0)   ≡⟨ refl  ⟩
        (j0 + 1) - (j0 + 0)   ≡⟨ minus+yx-yz {_} {j0} {0}  ⟩
       1   ∎ where open ≡-Reasoning
   ge7' : ¬ ( 1 * j0 > Dividable.factor (GCD.div-i di) * i0 )
   ge7' lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6') (s≤s z≤n)))
gcd-euclid1 (suc (suc i)) i0 zero zero di = record { eqb = 0 ; eqa = 1 ; is-equ> = λ () ; is-equ< = λ _ → +-comm _ 0
    ; is-equ= =  λ eq → subst (λ k → 0 ≡ k) (+-comm _ 0) (sym eq) }
gcd-euclid1 (suc (suc i)) i0 zero (suc j0) di with gcd-euclid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di)))
... | e =  record { eqa = ea ; eqb =  eb + ea * f
      ; is-equ= = λ eq → Euclid.is-equ= e (ge24 eq)
      ;  is-equ< =  λ lt → subst (λ k → ((ea * i0) - ((eb + ea * f) * suc j0))  ≡ k ) (Euclid.is-equ< e (ge3 lt ge4)) ge4
      ;  is-equ> =  λ lt → subst (λ k →  (((eb + ea * f) * suc j0) - (ea * i0)) ≡ k ) (Euclid.is-equ> e (ge3 lt ge5)) ge5 } where
   ea = Euclid.eqa e
   eb = Euclid.eqb e
   f = Dividable.factor (GCD.div-j di)
   ge5 : (((eb + ea * f) * suc j0) - (ea * i0)) ≡ ((eb * suc j0) - (ea * suc (suc i)))
   ge5 = begin
       ((eb + ea * f) * suc j0) - (ea * i0) ≡⟨ cong₂ (λ j k → j - k ) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩
      ( eb * suc j0 + (ea * f )* suc j0) - (ea * suc (suc i) + (ea * f )* suc j0) ≡⟨ minus+xy-zy {_} {(ea * f )* suc j0} {ea * suc (suc i)}   ⟩
       (eb * suc j0) - (ea * suc (suc i)) ∎ where open ≡-Reasoning
   ge4 : ((ea * i0) - ((eb + ea * f) * suc j0)) ≡ ((ea * suc (suc i)) - (eb * suc j0))
   ge4 = begin
        (ea * i0) - ((eb + ea * f) * suc j0) ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩
        (ea * suc (suc i) + (ea * f )* suc j0) - ( eb * suc j0 + (ea * f )* suc j0)  ≡⟨ minus+xy-zy {ea * suc (suc i)} {(ea * f )* suc j0} { eb * suc j0}   ⟩
        (ea * suc (suc i)) - (eb * suc j0) ∎ where open ≡-Reasoning
   ge24 : ea * i0 ≡ (eb + ea * f) * suc j0 → ea * suc (suc i) ≡ eb * suc j0
   ge24 eq = begin
       ea * suc (suc i)   ≡⟨ sym ( minus+y-y {_} {(ea * f ) * suc j0 })  ⟩
       (ea * suc (suc i) + (ea * f ) * suc j0 ) - ((ea * f ) * suc j0) ≡⟨  cong (λ k → k - ((ea * f ) * suc j0 )) (sym (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )))  ⟩
        (ea * i0) - ((ea * f ) * suc j0)  ≡⟨  cong (λ k → k - ((ea * f ) * suc j0 )) eq  ⟩
       ((eb + ea * f) * suc j0) - ((ea * f ) * suc j0) ≡⟨   cong (λ k → k - ((ea * f ) * suc j0 )) ((proj1 (ge01 j0 i i0 eb ea (GCD-sym di)))) ⟩
       ( eb * suc j0 + (ea * f ) * suc j0 ) - ((ea * f ) * suc j0) ≡⟨  minus+y-y {_} {(ea * f ) * suc j0 }  ⟩
       eb * suc j0   ∎ where open ≡-Reasoning
gcd-euclid1 (suc zero) i0 (suc j) j0 di =
     gcd-euclid1 zero i0 j j0  (gcd-next di)
gcd-euclid1 (suc (suc i)) i0 (suc j) j0  di =
     gcd-euclid1 (suc i) i0 j j0 (gcd-next di)

ge12 : (p x : ℕ) → 0 < x → 1 < p → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  ( gcd p x ≡ 1 ) ∨ ( Dividable p x )
ge12 p x 0<x 1<p prime with decD {p} {x} 1<p
... | yes y = case2 y
... | no nx with <-cmp (gcd p x ) 1
... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (s≤s (gcd>0 p x (<-trans a<sa 1<p)  0<x) ) )
... | tri≈ ¬a b ¬c = case1 b
... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (prime (gcd p x) ge13 (<to≤ c) )) ge18 ) where
        --  1 < gcd p x
        ge13 :  gcd p x < p -- gcd p x ≡ p → ¬ nx
        ge13 with <-cmp (gcd p x ) p
        ... | tri< a ¬b ¬c = a
        ... | tri≈ ¬a b ¬c = ⊥-elim ( nx (subst (λ k → Dividable k x) b (proj2 (gcd-dividable p x ))))
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ (<-trans a<sa 1<p) 0<x) c )
        ge19 : Dividable (gcd p x) p
        ge19 = proj1 (gcd-dividable p x )
        ge18 :   1 < gcd p  (gcd p x) --  Dividable p  (gcd p x) → gcd p  (gcd p x) ≡  (gcd p x) > 1
        ge18 = subst (λ k → 1 < k ) (sym (div→gcd {p} {gcd p x} c ge19 )) c

gcd-euclid : ( p a b : ℕ )  → 1 < p  → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (a * b)  → Dividable p a ∨ Dividable p b
gcd-euclid p a b 1<p 0<a 0<b prime div-ab with decD {p} {a} 1<p
... | yes y = case1 y
... | no np = case2 ge16  where
    f = Dividable.factor div-ab
    ge10 : gcd p a ≡ 1
    ge10 with ge12 p a 0<a 1<p prime
    ... | case1 x = x
    ... | case2 x = ⊥-elim ( np x )
    ge11 : Euclid p a (gcd p a)
    ge11 = gcd-euclid1 p p a a GCDi
    ea = Euclid.eqa ge11
    eb = Euclid.eqb ge11
    ge18 : (f * eb) * p ≡  b * (a * eb )
    ge18 = begin
         (f * eb) * p  ≡⟨ *-assoc (f) (eb) p ⟩
         f * (eb * p)  ≡⟨ cong (λ k →  f  * k)  (*-comm _ p) ⟩
          f * (p * eb )  ≡⟨ sym (*-assoc  (f) p (eb) ) ⟩
         (f * p ) * eb   ≡⟨ cong (λ k → k * eb ) (+-comm 0  (f * p )) ⟩
         (f * p + 0) * eb   ≡⟨ cong (λ k → k *  eb) (((Dividable.is-factor div-ab))) ⟩
         (a * b) * eb   ≡⟨ cong (λ k → k *  eb) (*-comm a b) ⟩
         (b * a) * eb   ≡⟨ *-assoc b a (eb ) ⟩
         b * (a * eb ) ∎ where open ≡-Reasoning
    ge19 : ( ea * p ) ≡ (  eb * a ) → ((b * ea) - (f * eb)) * p + 0 ≡ b
    ge19 eq = ⊥-elim ( nat-≡< (Euclid.is-equ= ge11 eq) (subst (λ k → 0 < k ) (sym ge10) a<sa ) )
    ge14 : ( ea * p ) > (  eb * a ) → ((b * ea) - (f * eb)) * p + 0 ≡ b
    ge14 lt = begin
         (((b * ea) - (f * eb)) * p) + 0 ≡⟨ +-comm _ 0 ⟩
         ((b * ea) - ((f * eb)) * p) ≡⟨ distr-minus-* {_} {f * eb} {p} ⟩
         ((b * ea) * p) - (((f * eb) * p))  ≡⟨ cong (λ k → ((b * ea) * p)  - k  ) ge18 ⟩
         ((b * ea) * p) - (b * (a * eb ))  ≡⟨ cong (λ k → k - (b * (a * eb)) ) (*-assoc b _ p) ⟩
         (b * (ea * p)) - (b * (a * eb ))  ≡⟨ sym ( distr-minus-*' {b} {ea * p} {a * eb} )  ⟩
         b * (( ea * p) - (a * eb) )  ≡⟨ cong (λ k → b * ( ( ea * p) - k)) (*-comm a (eb)) ⟩
         (b * ( (ea * p)) -  (eb * a) )  ≡⟨ cong (b *_) (Euclid.is-equ< ge11 lt )⟩
         b * gcd p a  ≡⟨ cong (b *_) ge10 ⟩
         b * 1  ≡⟨ m*1=m ⟩
         b ∎ where open ≡-Reasoning
    ge15 : ( ea * p ) < (  eb * a ) →  ((f * eb) - (b * ea ) ) * p + 0 ≡ b
    ge15 lt = begin
         ((f * eb) - (b * ea)  ) * p + 0  ≡⟨  +-comm _ 0 ⟩
         ((f * eb) - (b * ea)  ) * p   ≡⟨ distr-minus-* {_} {b * ea} {p} ⟩
         ((f * eb) * p) - ((b * ea) * p)    ≡⟨ cong (λ k → k - ((b * ea) * p)   ) ge18 ⟩
         (b * (a * eb )) - ((b * ea) * p )   ≡⟨   cong (λ k → (b * (a * eb)) - k ) (*-assoc b _ p) ⟩
         (b * (a * eb )) - (b * (ea * p) )   ≡⟨  sym ( distr-minus-*' {b} {a * eb} {ea * p}  ) ⟩
         b * ( (a * eb) - (ea * p) )  ≡⟨  cong (λ k → b * ( k - ( ea * p) )) (*-comm a (eb))  ⟩
         b * ( (eb * a) - (ea * p)  )  ≡⟨ cong (b *_) (Euclid.is-equ> ge11 lt) ⟩
         b * gcd p a  ≡⟨ cong (b *_) ge10 ⟩
         b * 1  ≡⟨ m*1=m ⟩
         b ∎ where open ≡-Reasoning
    ge17 : (x  y : ℕ ) → x ≡ y → x ≤ y
    ge17 x x refl = refl-≤
    ge16 : Dividable p b
    ge16 with <-cmp ( ea * p ) (  eb * a )
    ... | tri< a ¬b ¬c = record { factor = (f * eb)  - (b * ea) ; is-factor = ge15 a }
    ... | tri≈ ¬a eq ¬c = record { factor = (b * ea) - ( f * eb) ; is-factor = ge19 eq }
    ... | tri> ¬a ¬b c = record { factor = (b * ea) -  (f * eb) ; is-factor = ge14 c }

gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
gcdmul+1 zero n = gcd204 n
gcdmul+1 (suc m) n = begin
      gcd (suc m * n + 1) n ≡⟨⟩
      gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin
         n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩
         m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩
         m * n + (n + 1)  ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩
         m * n + (1 + n)  ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩
         m * n + 1 + n ∎
       ) ⟩
      gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩
      gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
      1 ∎ where open ≡-Reasoning

m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq

ext: agda

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
module Dave.Algebra.Naturals.Exponentiation where
  open import Dave.Algebra.Naturals.Definition
  open import Dave.Algebra.Naturals.Multiplication
  open import Dave.Algebra.Naturals.Addition

  _^_ : ℕ → ℕ → ℕ
  a ^ zero = 1
  a ^ suc b = (a ^ b) * a

  infixl 8 _^_

  ^-distribₗ : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
  ^-distribₗ m zero p = refl
  ^-distribₗ m (suc n) p = begin
    m ^ (suc n + p) ≡⟨⟩
    m ^ suc (n + p) ≡⟨⟩
    (m ^ (n + p)) * m ≡⟨ cong (λ a → a * m) (^-distribₗ m n p) ⟩
    (m ^ n) * (m ^ p) * m ≡⟨ IsCommutativeMonoid.swap021 ℕ-*-IsCommutativeMonoid (m ^ n) (m ^ p) m ⟩
    (m ^ n) * m * (m ^ p) ≡⟨⟩
    (m ^ n) * (m ^ 1) * (m ^ p) ≡⟨ cong (λ a → a * (m ^ p)) (sym (^-distribₗ m n 1)) ⟩
    (m ^ (n + 1)) * (m ^ p) ≡⟨ cong (λ a → (m ^ a) * (m ^ p)) (+-add1ᵣ n) ⟩
    (m ^ suc n) * (m ^ p) ∎

  ^-distribᵣ : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
  ^-distribᵣ m n zero = refl
  ^-distribᵣ m n (suc p) = begin
     (m * n) ^ suc p ≡⟨⟩
     ((m * n) ^ p) * (m * n) ≡⟨ cong (λ a → a * (m * n)) (^-distribᵣ m n p) ⟩
     (m ^ p) * (n ^ p) * (m * n) ≡⟨ sym (IsSemigroup.assoc ℕ-*-IsSemigroup ((m ^ p) * (n ^ p)) m n) ⟩
     (m ^ p) * (n ^ p) * m * n ≡⟨ cong (λ a → a * n) (IsCommutativeMonoid.swap021 ℕ-*-IsCommutativeMonoid (m ^ p) (n ^ p) m) ⟩
     (m ^ p) * m * (n ^ p) * n ≡⟨ IsSemigroup.assoc ℕ-*-IsSemigroup ((m ^ p) * m) (n ^ p) n ⟩
     (m ^ p) * m * ((n ^ p) * n) ≡⟨⟩
     (m ^ p) * (m ^ 1) * ((n ^ p) * (n ^ 1)) ≡⟨ cong (λ a → a * ((n ^ p) * (n ^ 1))) (sym (^-distribₗ m p 1)) ⟩
     (m ^ (p + 1)) * ((n ^ p) * (n ^ 1)) ≡⟨ cong (λ a → (m ^ a) * ((n ^ p) * (n ^ 1))) (+-add1ᵣ p) ⟩
     (m ^ suc p) * ((n ^ p) * (n ^ 1)) ≡⟨ cong (λ a → (m ^ suc p) * a) (sym (^-distribₗ n p 1)) ⟩
     (m ^ suc p) * (n ^ (p + 1)) ≡⟨ cong (λ a → (m ^ suc p) * (n ^ a)) (+-add1ᵣ p) ⟩
     (m ^ suc p) * (n ^ suc p) ∎

  ^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
  ^-*-assoc m n zero = sym (begin
    m ^ (n * zero) ≡⟨ cong (λ a → m ^ a) (*-zero n) ⟩
    1 ∎)
  ^-*-assoc m n (suc p) = begin
    (m ^ n) ^ suc p ≡⟨⟩
    (m ^ n) ^ p * (m ^ n) ≡⟨ cong (λ a → a * (m ^ n)) (^-*-assoc m n p) ⟩
    m ^ (n * p) * (m ^ n) ≡⟨ sym (^-distribₗ m (n * p) n) ⟩
    m ^ (n * p + n) ≡⟨ cong (λ a → m ^ a ) (sym (*-distrib1ᵣ-+ₗ n p)) ⟩
    m ^ (n * (p + 1)) ≡⟨ cong (λ a → m ^ (n * a)) (+-add1ᵣ p) ⟩
    m ^ (n * suc p) ∎


text:
------------------------------------------------------------------------------
-- Lists of natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.List where

open import FOTC.Base

-- The FOTC lists of natural numbers type (inductive predicate for
-- total lists of natural numbers).
open import FOTC.Data.Nat.List.Type public

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat

data Unit : Set where
  c : ⊤ → Nat → ⊤ → Unit

-- Note that the ⊤ arguments get erased and shouldn't be present in
-- the Haskell version of Unit.
{-# FOREIGN GHC data Unit = Unit Integer #-}
{-# COMPILE GHC Unit = data Unit (Unit) #-}

postulate print : Nat → IO ⊤
{-# COMPILE GHC print = print #-}
{-# COMPILE JS  print = function (x) { return function(cb) { process.stdout.write(x + "\n"); cb(0) } } #-}

foo : Unit → IO ⊤
foo (c _ n _) = print n

main : IO ⊤
main = foo (c _ 12345 _)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2018-06-12, issue #2170
-- Reported by tomjack

{-# OPTIONS --irrelevant-projections --subtyping #-}

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

infixr 42 _,_
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ

record Irr (A : Set) : Set where
  constructor irr
  field
    .unirr : A
open Irr

-- Usually,  unirr (irr a) = .(a)  which is  DontCare a  in internal syntax.
-- The DontCare protection of an irrelevant field could be circumvented
-- using subtyping  irr : (.Bool → Irr Bool) ≤ (Bool → Irr Bool):
-- The argument  a  in  (i a)  would not have ArgInfo Irrelevant, even
-- after substitution irr/i.  Since the DontCare came from the ArgInfo of a,
-- there was none.  Now, the record constructor name also carries ArgInfo for
-- each of its fields, which is used to produce a DontCare.

bizarre : Irr (Σ (Bool → Irr Bool) (λ i → Σ (Irr Bool → Bool) (λ u → (a : Bool) → u (i a) ≡ a)))
bizarre = irr (irr , unirr , λ a → refl)  -- Should not pass

-- Expected error:
-- .(a) != a of type Bool
-- when checking that the expression refl has type .(a) ≡ a

-- The rest is proving False.

data ⊥ : Set where

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

true≠false : ¬ (true ≡ false)
true≠false ()

infixr 30 _∙_
_∙_ : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ q = q

infix 42 !_
!_ : {A : Set} {x y : A} → x ≡ y → y ≡ x
! refl = refl

map-irr : {A B : Set} → (A → B) → Irr A → Irr B
map-irr f (irr x) = irr (f x)

factivity : ¬ (Irr ⊥)
factivity (irr ())

bad : Irr (true ≡ false)
bad = map-irr (λ { (i , u , s) → ! (s true) ∙ s false }) bizarre

boom : ⊥
boom = factivity (map-irr true≠false bad)

-- the hole here is is .(a) ≡ a
-- bizarre' : Irr (Σ (Irr Bool → Bool) (λ u → (a : Bool) → u (irr a) ≡ a))
-- bizarre' = irr (unirr , (λ a → {!!}))

-- also fails, unirr (irr a) = .(a)
-- bizarre' : Irr (Σ (Bool → Irr Bool) (λ i → Σ (Irr Bool → Bool) (λ u → (a : Bool) → u (i a) ≡ a)))
-- bizarre' = irr (irr , unirr , (λ a → refl {x = unirr (irr a)})

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Issue73 where

record ImplicitField (a : Set) : Set where
    field
        aField : a
        {anImplicitField} : a
open ImplicitField public
{-# COMPILE AGDA2HS ImplicitField class #-}


text:
module nfa136 where

open import logic
open import nfa
open import automaton
open import Data.List
open import finiteSet
open import Data.Fin
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

data  StatesQ   : Set  where
   q1 : StatesQ
   q2 : StatesQ
   q3 : StatesQ

data  A2   : Set  where
   a0 : A2
   b0 : A2

finStateQ : FiniteSet StatesQ
finStateQ = record {
        Q←F = Q←F
      ; F←Q  = F←Q
      ; finiso→ = finiso→
      ; finiso← = finiso←
   } where
       Q←F : Fin 3 → StatesQ
       Q←F zero = q1
       Q←F (suc zero) = q2
       Q←F (suc (suc zero)) = q3
       F←Q : StatesQ → Fin 3
       F←Q q1 = zero
       F←Q q2 = suc zero
       F←Q q3 = suc (suc zero)
       finiso→ : (q : StatesQ) → Q←F (F←Q q) ≡ q
       finiso→ q1 = refl
       finiso→ q2 = refl
       finiso→ q3 = refl
       finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
       finiso← zero = refl
       finiso← (suc zero) = refl
       finiso← (suc (suc zero)) = refl
       finiso← (suc (suc (suc ())))

transition136 : StatesQ  → A2  → StatesQ → Bool
transition136 q1 b0 q2 = true
transition136 q1 a0 q1 = true  -- q1 → ep → q3
transition136 q2 a0 q2 = true
transition136 q2 a0 q3 = true
transition136 q2 b0 q3 = true
transition136 q3 a0 q1 = true
transition136 _ _ _ = false

end136 : StatesQ → Bool
end136  q1 = true
end136  _ = false

start136 : StatesQ → Bool
start136 q1 = true
start136 _ = false

exists136 : (StatesQ → Bool) → Bool
exists136 f = f q1 \/ f q2 \/ f q3

to-list-136 : (StatesQ → Bool) → List StatesQ
to-list-136 f = tl1 where
   tl3 : List StatesQ
   tl3 with f q3
   ... | true = q3 ∷  []
   ... | false = []
   tl2 : List StatesQ
   tl2 with f q2
   ... | true = q2 ∷ tl3
   ... | false = tl3
   tl1 : List StatesQ
   tl1 with f q1
   ... | true = q1 ∷ tl2
   ... | false = tl2

nfa136 :  NAutomaton  StatesQ A2
nfa136 =  record { Nδ = transition136; Nend = end136 }

example136-1 = Naccept nfa136 exists136 start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )

t146-1 = Ntrace nfa136 exists136 to-list-136 start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )

example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] )

example136-2 = Naccept nfa136 exists136 start136( b0  ∷ a0  ∷ b0 ∷ a0 ∷ b0 ∷ [] )
t146-2 = Ntrace nfa136 exists136 to-list-136 start136( b0  ∷ a0  ∷ b0 ∷ a0 ∷ b0 ∷ [] )

open FiniteSet

nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool
nx now [] = now
nx now ( i ∷ ni ) = (Nmoves nfa136 exists136 (nx now ni) i )

example136-3 = to-list-136 start136
example136-4 = to-list-136 (nx start136  ( a0  ∷ b0 ∷ a0 ∷ [] ))

open import sbconst2

fm136 : Automaton ( StatesQ → Bool  )  A2
fm136  = subset-construction exists136 nfa136

open NAutomaton

lemma136 : ( x : List A2 ) → Naccept nfa136 exists136 start136 x  ≡ accept fm136 start136 x
lemma136 x = lemma136-1 x start136 where
    lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool )
        → Naccept nfa136 exists136 states x  ≡ accept fm136 states x
    lemma136-1 [] _ = refl
    lemma136-1 (h ∷ t) states = lemma136-1 t (δconv exists136 (Nδ nfa136) states h)


text:
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

infix 1 Σ-syntax
Σ-syntax = Σ
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

pair : Set → Set
pair A = Σ[ _ ∈ A ] A

diag : Set → Set
diag A = Σ[ p ∈ pair A ] fst p ≡ snd p

diag-pat : Set → Set
diag-pat A = Σ[ p@(x , y) ∈ pair A ] p ≡ (y , x)

-- WAS: parse error for p@(x , y)
-- WANT: success


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

--
-- A pointed type is a type together with a point in it. This module
-- defines the universe of pointed types which we denote by Type● ℓ.
-- Like the type universe Type ℓ, it is an inhabitant of Type (ℓ + 1).
--
-- Editing notes:
--     ● : \ci followed by selecting the 1 option
--     ∙ : \.

module hott.core.universe.pointed where

open import hott.core.sigma
open import hott.core.universe

-- The pointed type is nothing but a dependent pair where the first
-- component is itself a type.
Type● : (ℓ : Level) → Type (lsuc ℓ)
Type● ℓ = Σ λ x → x

-- The level 0 of pointed types.
Type∙  = Type● lzero

Type∙₀ = Type● lzero
Type∙₁ = Type● lone
Type∙₂ = Type● ltwo
Type∙₃ = Type● lthree
Type∙₄ = Type● lfour
Type∙₅ = Type● lfive
Type∙₆ = Type● lsix
Type∙₇ = Type● lseven
Type∙₈ = Type● leight
Type∙₉ = Type● lnine

--
-- Topologically pointed types are spaces with a distinguished point
-- called the base. We give function to recover the space and the base
-- point from it. These are essentially the projections but we give
-- better names for it.
--

space : ∀{ℓ} → Type● ℓ → Type ℓ
space = fst

base : ∀{ℓ} → (A● : Type● ℓ) → space A●
base = snd

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
{-# OPTIONS --universe-polymorphism #-}
module Graphs.Graph where

open import Level
open import Categories.Support.Equivalence
open import Relation.Binary
  using (Rel; IsEquivalence; module IsEquivalence; Reflexive; Symmetric; Transitive)
  renaming (_⇒_ to _⊆_)
open import Relation.Binary.PropositionalEquality
  using ()
  renaming (_≡_ to _≣_)

record Graph (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    Obj     : Set o
    _↝_     : Obj → Obj → Set ℓ
    _≈_     : {A B : Obj} → Rel (A ↝ B) e
    .equiv  : ∀ {A B : Obj} → IsEquivalence (_≈_ {A}{B})

  edge-setoid : ∀ {A B : Obj} → Setoid ℓ e
  edge-setoid {A}{B} = record
    { Carrier       = A ↝ B
    ; _≈_           = _≈_
    ; isEquivalence = equiv
    }

  module Equiv {A B : Obj} where
    private
      module e = IsEquivalence
      .q : IsEquivalence _≈_
      q = equiv {A} {B}

    .refl : Reflexive _≈_
    refl = e.refl q
    .trans : Transitive _≈_
    trans = e.trans q
    .sym : Symmetric _≈_
    sym = e.sym q
    .reflexive : _≣_ ⊆ _≈_
    reflexive = e.reflexive q

_[_↝_] : ∀ {o ℓ e} → (G : Graph o ℓ e) → Graph.Obj G → Graph.Obj G → Set ℓ
G [ A ↝ B ] = Graph._↝_ G A B

_[_≈_] : ∀ {o ℓ e} → (G : Graph o ℓ e) → {A B : Graph.Obj G} → Rel (G [ A ↝ B ]) e
G [ f ≈ g ] = Graph._≈_ G f g

module Heterogeneous {o ℓ e} (G : Graph o ℓ e) where
  open Graph G
  open Equiv renaming (refl to refl′; sym to sym′; trans to trans′)

  data _~_ {A B} (f : A ↝ B) : ∀ {X Y} → (X ↝ Y) → Set (ℓ ⊔ e) where
    ≈⇒~ : {g : A ↝ B} → .(f ≈ g) → f ~ g

  refl : ∀ {A B} {f : A ↝ B} → f ~ f
  refl = ≈⇒~ refl′

  sym : ∀ {A B} {f : A ↝ B} {D E} {g : D ↝ E} → f ~ g → g ~ f
  sym (≈⇒~ f≈g) = ≈⇒~ (sym′ f≈g)

  trans : ∀ {A B} {f : A ↝ B}
             {D E} {g : D ↝ E}
             {F G} {h : F ↝ G}
          → f ~ g → g ~ h → f ~ h
  trans (≈⇒~ f≈g) (≈⇒~ g≈h) = ≈⇒~ (trans′ f≈g g≈h)

_[_~_] : ∀ {o ℓ e} (G : Graph o ℓ e) {A B} (f : G [ A ↝ B ]) {X Y} (g : G [ X ↝ Y ]) → Set (ℓ ⊔ e)
G [ f ~ g ] = Heterogeneous._~_ G f g

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- Up-to techniques for strong bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Bisimilarity.Up-to {ℓ} (lts : LTS ℓ) where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bisimilarity lts
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Relation
import Up-to

open LTS lts

------------------------------------------------------------------------
-- The general up-to machinery, instantiated with the StepC container

open Up-to StepC public

------------------------------------------------------------------------
-- Some examples (based on techniques presented by Pous and Sangiorgi
-- in "Enhancements of the bisimulation proof method")

-- Up to bisimilarity.

Up-to-bisimilarity : Trans₂ ℓ Proc
Up-to-bisimilarity R = Bisimilarity ∞ ⊙ R ⊙ Bisimilarity ∞

-- Up to bisimilarity is monotone.

up-to-bisimilarity-monotone : Monotone Up-to-bisimilarity
up-to-bisimilarity-monotone R⊆S =
  Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))

-- Up to bisimilarity is size-preserving.

up-to-bisimilarity-size-preserving : Size-preserving Up-to-bisimilarity
up-to-bisimilarity-size-preserving
  R⊆∼i {p₁ , p₄} (p₂ , p₁∼p₂ , p₃ , p₂Rp₃ , p₃∼p₄) =
    p₁  ∼⟨ p₁∼p₂ ⟩
    p₂  ∼⟨ R⊆∼i p₂Rp₃ ⟩
    p₃  ∼⟨ p₃∼p₄ ⟩■
    p₄

-- Up to union with bisimilarity.

Up-to-∪∼ : Trans₂ ℓ Proc
Up-to-∪∼ R = R ∪ Bisimilarity ∞

-- Up to union with bisimilarity is monotone.

up-to-∪∼-monotone : Monotone Up-to-∪∼
up-to-∪∼-monotone R⊆S = ⊎-map R⊆S id

-- Up to union with bisimilarity is size-preserving.
--
-- The proof is similar to parts of the proof of Corollary 6.3.15 from
-- Pous and Sangiorgi's "Enhancements of the bisimulation proof
-- method".

up-to-∪∼-size-preserving : Size-preserving Up-to-∪∼
up-to-∪∼-size-preserving =
  ∪-closure
    id-size-preserving
    (const-size-preserving (Bisimilarity ∞  ⊆⟨ id ⟩∎
                            Bisimilarity ∞  ∎))

-- Up to transitive closure.

Up-to-* : Trans₂ ℓ Proc
Up-to-* R = R *

-- Up to transitive closure is monotone.

up-to-*-monotone : Monotone Up-to-*
up-to-*-monotone R⊆S = Σ-map id (λ {n} → ^^-mono R⊆S n)
  where
  ^^-mono : ∀ {R S} → R ⊆ S →
            ∀ n → R ^^ n ⊆ S ^^ n
  ^^-mono R⊆S zero    = id
  ^^-mono R⊆S (suc n) = Σ-map id (Σ-map R⊆S (^^-mono R⊆S n))

-- Up to transitive closure is size-preserving.

up-to-*-size-preserving : Size-preserving Up-to-*
up-to-*-size-preserving =
  _⇔_.from (monotone→⇔ up-to-*-monotone) drop-*
  where
  drop-* : ∀ {i} → Bisimilarity i * ⊆ Bisimilarity i
  drop-* {x = p , .p} (zero  , refl)           = p ■
  drop-* {x = p , r}  (suc n , q , p∼q , ∼ⁿqr) =
    p  ∼⟨ p∼q ⟩
    q  ∼⟨ drop-* (n , ∼ⁿqr) ⟩■
    r

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Issue1232.List where

import Issue1232.Nat


text:
record C (A : Set) : Set where
  field f : A → A

open C {{...}}

module M (A : Set) where
  data D : Set where
    d : A → D

  instance
    CD : C D
    CD = record { f = λ x → x }

data Bool : Set where
  false true : Bool

open M Bool

-- Bug: M.CD is not considered in instance search
x : D
x = f (M.d false)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Cubical.Core.Everything

Sq : {A : Set} {a0 a1 b0 b1 : A}
     (u  : a0 ≡ a1) (v  : b0 ≡ b1)
     (r0 : a0 ≡ b0) (r1 : a1 ≡ b1)
     → Set
Sq u v r0 r1 = PathP (λ i → r0 i ≡ r1 i) u v

ConstSq : {A : Set} {a : A} (p : a ≡ a) →
          Sq p p p p
ConstSq {A} p i j = compCCHM (λ _ → A)
  (~ i ∨ i ∨ ~ j ∨ j)
  (λ k → λ { (i = i0) → p j
           ; (i = i1) → p (k ∧ j)
           ; (j = i0) → p i
           ; (j = i1) → p (k ∧ i)
           })
  (p (i ∨ j))

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


text:
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin; _≟_)
open import Data.Nat using (ℕ)
open import Data.Product using (∃-syntax; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec using (lookup; _[_]≔_)
open import Data.Vec.Properties using (lookup∘update; lookup∘update′)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary.PropositionalEquality using (sym; trans; _≡_; refl; cong; _≢_; module ≡-Reasoning)
open import Data.Product using (∃-syntax; _,_; proj₁; proj₂; _×_)
open ≡-Reasoning

open import Common
open import Global
open import Local

private
  variable
    n : ℕ
    l : Label
    p q : Fin n
    g gSub : Global n
    lSub : Local n

project : Global n -> Fin n -> Local n
project endG _
  = endL
project (msgSingle p q p≢q l gSub) r
  with p ≟ r   | q ≟ r
... | yes _    | no _     = sendSingle q l (project gSub r)
... | no _     | yes _    = recvSingle p l (project gSub r)
... | no _     | no _     = project gSub r
... | yes refl | yes refl = ⊥-elim (p≢q refl)

proj-prefix-other :
  (r s t : Fin n)
  -> ∀{ r≢s }
  -> (gSub : Global n)
  -> r ≢ t
  -> s ≢ t
  -> project (msgSingle r s r≢s l gSub) t ≡ project gSub t
proj-prefix-other r s t _ r≢t s≢t
  with  r ≟ t  | s ≟ t
... | yes refl | _        = ⊥-elim (r≢t refl)
... | _        | yes refl = ⊥-elim (s≢t refl)
... | no _     | no _     = refl

proj-prefix-send :
  (r s : Fin n)
  -> (gSub : Global n)
  -> (r≢s : r ≢ s)
  -> project (msgSingle r s r≢s l gSub) r ≡ sendSingle s l (project gSub r)
proj-prefix-send r s _ r≢s
  with  r ≟ r | s ≟ r
... | yes _   | no _     = refl
... | _       | yes refl = ⊥-elim (r≢s refl)
... | no r≢r  | no _     = ⊥-elim (r≢r refl)

proj-prefix-recv :
  (r s : Fin n)
  -> (gSub : Global n)
  -> (r≢s : r ≢ s)
  -> project (msgSingle r s r≢s l gSub) s ≡ recvSingle r l (project gSub s)
proj-prefix-recv r s _ r≢s
  with  r ≟ s  | s ≟ s
... | no _     | yes _   = refl
... | yes refl | _       = ⊥-elim (r≢s refl)
... | _        | no s≢s  = ⊥-elim (s≢s refl)

record _↔_ { n : ℕ } (g : Global n) (c : Configuration n) : Set where
  field
    isProj : ∀(p : Fin n) -> lookup c p ≡ project g p

proj-inv-send :
  project {n} g p ≡ sendSingle q l lSub
  -> ∃[ p≢q ] ∃[ gSub ] g ≡ msgSingle p q p≢q l gSub × project gSub p ≡ lSub
     ⊎
     ∃[ r ] ∃[ s ] ∃[ r≢s ] ∃[ l′ ] ∃[ gSub ]
       g ≡ msgSingle r s r≢s l′ gSub ×
       r ≢ p ×
       s ≢ p ×
       project gSub p ≡ sendSingle q l lSub
proj-inv-send {g = g@endG} projSend = ⊥-elim (endL≢sendSingle projSend)
proj-inv-send {n} {g = g@(msgSingle r s r≢s l′ gSub)} {p} {q} {l} {ltSub} projSend
  with r ≟ p    | s ≟ p
... | yes refl | yes refl = ⊥-elim (r≢s refl)
... | no r≢p   | no s≢p   = inj₂ (r , s , r≢s , l′ , gSub , refl , r≢p , s≢p , projSend)
... | yes refl | no s≢p
      with sendSingle-injective projSend
...     | refl , refl , refl  = inj₁ (r≢s , gSub , refl , refl)

proj-inv-recv :
  project {n} g p ≡ recvSingle q l lSub
  -> ∃[ p≢q ] ∃[ gSub ] g ≡ msgSingle q p p≢q l gSub × project gSub p ≡ lSub
     ⊎
     ∃[ r ] ∃[ s ] ∃[ r≢s ] ∃[ l′ ] ∃[ gSub ]
       g ≡ msgSingle r s r≢s l′ gSub ×
       r ≢ p ×
       s ≢ p ×
       project gSub p ≡ recvSingle q l lSub
proj-inv-recv {g = g@endG} projRecv = ⊥-elim (endL≢recvSingle projRecv)
proj-inv-recv {n} {g = g@(msgSingle r s r≢s l′ gSub)} {p} {q} {l} {lSub} projRecv
  with r ≟ p   | s ≟ p
... | yes refl | yes refl = ⊥-elim (r≢s refl)
... | no r≢p   | no s≢p   = inj₂ (r , s , r≢s , l′ , gSub , refl , r≢p , s≢p , projRecv)
... | no r≢p   | yes refl
      with recvSingle-injective projRecv
...     | refl , refl , refl = inj₁ (r≢s , gSub , refl , refl)

proj-inv-send-recv :
  ∀ { lpSub lqSub }
  -> project {n} g p ≡ sendSingle q l lpSub
  -> project {n} g q ≡ recvSingle p l lqSub
  -> ∃[ p≢q ] ∃[ gSub ] g ≡ msgSingle p q p≢q l gSub × project gSub p ≡ lpSub × project gSub q ≡ lqSub
     ⊎
     ∃[ r ] ∃[ s ] ∃[ r≢s ] ∃[ l′ ] ∃[ gSub ]
       g ≡ msgSingle r s r≢s l′ gSub ×
       r ≢ p ×
       s ≢ p ×
       r ≢ q ×
       s ≢ q ×
       project gSub p ≡ sendSingle q l lpSub ×
       project gSub q ≡ recvSingle p l lqSub
proj-inv-send-recv {n} {g} {p} {q} {l} {lpSub} {lqSub} projSend projRecv
  with proj-inv-send {n} {g} projSend | proj-inv-recv {n} {g} projRecv
... | inj₁ (p≢q₁ , gSub₁ , refl , proj-g₁-p)
    | inj₁ (_ , _ , refl , proj-g₂-q)
        = inj₁ (p≢q₁ , gSub₁ , refl , proj-g₁-p , proj-g₂-q)
proj-inv-send-recv {n} {g} {p} {q} {l} {ltp′} {ltq′} projSend projRecv
    | inj₁ (_ , _ , refl , _)
    | inj₂ (_ , _ , _ , _ , _ , refl , _ , s≢q , _)
        = ⊥-elim (s≢q refl)
proj-inv-send-recv {n} {g} {p} {q} {l} {ltp′} {ltq′} projSend projRecv
    | inj₂ (_ , _ , _ , _ , _ , refl , r≢p , _ , _)
    | inj₁ (_ , _ , refl , _)
        = ⊥-elim (r≢p refl)
proj-inv-send-recv {n} {g} {p} {q} {l} {ltp′} {ltq′} projSend projRecv
    | inj₂ (r , s , r≢s , l′ , gSub₁ , refl , r≢p , s≢p , proj-g₁-p)
    | inj₂ (_ , _ , _   , _  , gSub₂ , refl , r≢q , s≢q , proj-g₂-q)
        = inj₂ (r , s , r≢s , l′ , gSub₁ , refl , r≢p , s≢p , r≢q , s≢q , proj-g₁-p , proj-g₂-q)

config-gt-remove-prefix :
  ∀ { p≢q gSub }
  -> (g : Global n)
  -> (c : Configuration n)
  -> g ↔ c
  -> g ≡ msgSingle p q p≢q l gSub
  -> ∃[ cSub ] cSub ≡ (c [ p ]≔ project gSub p) [ q ]≔ project gSub q × gSub ↔ cSub
config-gt-remove-prefix {n} {p} {q} {_} {p≢q} {gSub} g c assoc refl
  = cSub , refl , (record { isProj = isProj-gSub })
    where
      lpSub = project gSub p
      lqSub = project gSub q
      cSub = (c [ p ]≔ lpSub) [ q ]≔ lqSub
      isProj-gSub : ∀ (r : Fin n) -> lookup cSub r ≡ project gSub r
      isProj-gSub r
        with p ≟ r    | q ≟ r
      ... | yes refl | yes refl = ⊥-elim (p≢q refl)
      ... | yes refl | no  _
          rewrite lookup∘update′ p≢q (c [ p ]≔ lpSub) lqSub
          rewrite lookup∘update p c lpSub
          = refl
      ... | no _    | yes refl
          rewrite lookup∘update q (c [ p ]≔ lpSub) lqSub
          = refl
      ... | no p≢r  | no  q≢r
          rewrite lookup∘update′ (¬≡-flip q≢r) (c [ p ]≔ lpSub) lqSub
          rewrite lookup∘update′ (¬≡-flip p≢r) c lpSub
          rewrite _↔_.isProj assoc r
          = proj-prefix-other p q r gSub p≢r q≢r

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on strings
------------------------------------------------------------------------

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

module Data.String.Properties where

open import Data.Bool.Base
open import Data.String.Base

import Data.Char.Properties as Charₚ
import Data.List.Properties as Listₚ

open import Function
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (map′; ⌊_⌋)
open import Relation.Binary using (Decidable; Setoid; DecSetoid; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality.Core
open import Data.List.Relation.Binary.Lex.Strict as StrictLex
import Relation.Binary.Construct.On as On
import Relation.Binary.PropositionalEquality as PropEq

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.String.Properties public
  renaming ( primStringToListInjective to toList-injective)

------------------------------------------------------------------------
-- Equality

infix 4 _≟_
_≟_ : Decidable {A = String} _≡_
x ≟ y = map′ (toList-injective x y) (cong toList)
      $ Listₚ.≡-dec Charₚ._≟_ (toList x) (toList y)

setoid : Setoid _ _
setoid = PropEq.setoid String

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_

------------------------------------------------------------------------
-- Lexicographic ordering on strings.

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder =
  On.strictTotalOrder
    (StrictLex.<-strictTotalOrder Charₚ.strictTotalOrder)
    toList

------------------------------------------------------------------------
-- Alternative Boolean equality test.
--
-- Why is the definition _==_ = primStringEquality not used? One
-- reason is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.

infix 4 _==_
_==_ : String → String → Bool
s₁ == s₂ = ⌊ s₁ ≟ s₂ ⌋

private

  -- The following unit test does not type-check (at the time of
  -- writing) if _==_ is replaced by primStringEquality.

  data P : (String → Bool) → Set where
    p : (c : String) → P (_==_ c)

  unit-test : P (_==_ "")
  unit-test = p _


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.FiniteMultiset.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary
open import Cubical.HITs.FiniteMultiset.Base
open import Cubical.Structures.MultiSet
open import Cubical.Relation.Nullary.DecidableEq

private
  variable
    ℓ : Level
    A : Type ℓ

infixr 30 _++_

_++_ : ∀ (xs ys : FMSet A) → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs zs p q i j ++ ys =
  trunc (xs ++ ys) (zs ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

unitl-++ : ∀ (xs : FMSet A) → [] ++ xs ≡ xs
unitl-++ xs = refl

unitr-++ : ∀ (xs : FMSet A) → xs ++ [] ≡ xs
unitr-++ = ElimProp.f (trunc _ _) refl (λ x p → cong (_∷_ x) p)

assoc-++ : ∀ (xs ys zs : FMSet A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ = ElimProp.f (isPropΠ2 (λ _ _ → trunc _ _))
                      (λ ys zs → refl)
                      (λ x p ys zs → cong (_∷_ x) (p ys zs))

cons-++ : ∀ (x : A) (xs : FMSet A) → x ∷ xs ≡ xs ++ [ x ]
cons-++ x = ElimProp.f (trunc _ _)
  refl
  (λ y {xs} p → comm x y xs ∙ cong (_∷_ y) p)

comm-++ : ∀ (xs ys : FMSet A) → xs ++ ys ≡ ys ++ xs
comm-++ = ElimProp.f (isPropΠ (λ _ → trunc _ _))
  (λ ys → sym (unitr-++ ys))
  (λ x {xs} p ys → cong (x ∷_) (p ys)
                 ∙ cong (_++ xs) (cons-++ x ys)
                 ∙ sym (assoc-++ ys [ x ] xs))

module FMSetUniversal {ℓ} {M : Type ℓ} (MSet : isSet M)
  (e : M) (_⊗_ : M → M → M)
  (comm-⊗ : ∀ x y → x ⊗ y ≡ y ⊗ x) (assoc-⊗ : ∀ x y z → x ⊗ (y ⊗ z) ≡ (x ⊗ y) ⊗ z)
  (unit-⊗ : ∀ x → e ⊗ x ≡ x)
  (f : A → M) where

  f-extend : FMSet A → M
  f-extend = Rec.f MSet e (λ x m → f x ⊗ m)
         (λ x y m → comm-⊗ (f x) (f y ⊗ m) ∙ sym (assoc-⊗ (f y) m (f x)) ∙ cong (f y ⊗_) (comm-⊗ m (f x)))

  f-extend-nil : f-extend [] ≡ e
  f-extend-nil = refl

  f-extend-cons : ∀ x xs → f-extend (x ∷ xs) ≡ f x ⊗ f-extend xs
  f-extend-cons x xs = refl

  f-extend-sing : ∀ x → f-extend [ x ] ≡ f x
  f-extend-sing x = comm-⊗ (f x) e ∙ unit-⊗ (f x)

  f-extend-++ : ∀ xs ys → f-extend (xs ++ ys) ≡ f-extend xs ⊗ f-extend ys
  f-extend-++ = ElimProp.f (isPropΠ λ _ → MSet _ _)
    (λ ys → sym (unit-⊗ (f-extend ys)))
    (λ x {xs} p ys → cong (f x ⊗_) (p ys) ∙ assoc-⊗ (f x) (f-extend xs) (f-extend ys))

  module _ (h : FMSet A → M) (h-nil : h [] ≡ e) (h-sing : ∀ x → h [ x ] ≡ f x)
           (h-++ : ∀ xs ys → h (xs ++ ys) ≡ h xs ⊗ h ys) where

    f-extend-unique : h ≡ f-extend
    f-extend-unique = funExt (ElimProp.f (MSet _ _)
                              h-nil
                              (λ x {xs} p → (h-++ [ x ] xs) ∙ cong (_⊗ h xs) (h-sing x) ∙ cong (f x ⊗_) p))

-- We want to construct a multiset-structure on FMSet A, the empty set and insertion are given by the constructors,
-- for the count part we use the recursor

-- If A has decidable equality we can define the count-function:
module _(discA : Discrete A) where
 FMScount-∷* : A → A → ℕ → ℕ
 FMScount-∷* a x n with discA a x
 ... | yes a≡x = suc n
 ... | no  a≢x = n

 FMScount-comm* :  (a x y : A) (n : ℕ)
                  →  FMScount-∷* a x (FMScount-∷* a y n)
                   ≡ FMScount-∷* a y (FMScount-∷* a x n)
 FMScount-comm* a x y n with discA a x | discA a y
 ... | yes a≡x | yes a≡y = refl
 ... | yes a≡x | no  a≢y = refl
 ... | no  a≢x | yes a≡y = refl
 ... | no  a≢x | no  a≢y = refl

 FMScount : A → FMSet A → ℕ
 FMScount a = Rec.f isSetℕ 0 (FMScount-∷* a) (FMScount-comm* a)

 FMS-with-str : MultiSet A (Discrete→isSet discA)
 FMS-with-str = (FMSet A , [] , _∷_ , FMScount)

 -- We prove some useful properties of the FMScount function
 FMScount-≡-lemma : ∀ {a} {x} xs → a ≡ x → FMScount a (x ∷ xs) ≡ suc (FMScount a xs)
 FMScount-≡-lemma {a} {x} xs a≡x with discA a x
 ...                         | yes _   = refl
 ...                         | no  a≢x = ⊥.rec (a≢x a≡x)

 FMScount-≡-lemma-refl : ∀ {x} xs → FMScount x (x ∷ xs) ≡ suc (FMScount x xs)
 FMScount-≡-lemma-refl {x} xs = FMScount-≡-lemma xs refl

 FMScount-≢-lemma : ∀ {a} {x} xs → ¬ a ≡ x → FMScount a (x ∷ xs) ≡ FMScount a xs
 FMScount-≢-lemma {a} {x} xs a≢x with discA a x
 ...                         | yes a≡x = ⊥.rec (a≢x a≡x)
 ...                         | no  _   = refl

 FMScount-0-lemma : ∀ xs → (∀ a → FMScount a xs ≡ 0) → xs ≡ []
 FMScount-0-lemma = ElimProp.f (isPropΠ λ _ → trunc _ _) (λ _ → refl) θ
  where
  θ : ∀ x {xs} → ((∀ a → FMScount a xs ≡ 0) → xs ≡ [])
               → ((∀ a → FMScount a (x ∷ xs) ≡ 0) → (x ∷ xs) ≡ [])
  θ x {xs} _ p = ⊥.rec (snotz (sym (FMScount-≡-lemma-refl xs) ∙ p x))

 -- we define a function that removes an element a from a finite multiset once
 -- by simultaneously defining two lemmas about it
 remove1 : A → FMSet A → FMSet A
 remove1 a [] = []
 remove1 a (x ∷ xs) with (discA a x)
 ...               | yes _ = xs
 ...               | no  _ = x ∷ remove1 a xs
 remove1 a (comm x y xs i) with discA a x with discA a y
 ... | yes a≡x      | yes a≡y = ((sym a≡y ∙ a≡x) i) ∷ xs
 ... | yes a≡x      | no  _   = y ∷ (eq i)
   where
     eq : xs ≡ remove1 a (x ∷ xs)
     eq with discA a x
     eq | yes _   = refl
     eq | no  a≢x = ⊥.rec (a≢x a≡x)
 remove1 a (comm x y xs i) | no  _        | yes a≡y = x ∷ (eq i)
   where
   eq : remove1 a (y ∷ xs) ≡ xs
   eq with discA a y
   eq | yes _   = refl
   eq | no  a≢y = ⊥.rec (a≢y a≡y)
 remove1 a (comm x y xs i) | no  a≢x      | no  a≢y = ((λ i → x ∷ (p i)) ∙∙ comm x y (remove1 a xs) ∙∙ (λ i → y ∷ (sym q i))) i
   where
    p : remove1 a (y ∷ xs) ≡ y ∷ (remove1 a xs)
    p with discA a y
    p | yes a≡y = ⊥.rec (a≢y a≡y)
    p | no  _   = refl
    q : remove1 a (x ∷ xs) ≡ x ∷ (remove1 a xs)
    q with discA a x
    q | yes a≡x = ⊥.rec (a≢x a≡x)
    q | no  _   = refl
 remove1 a (trunc xs ys p q i j) = trunc (remove1 a xs) (remove1 a ys) (cong (remove1 a) p) (cong (remove1 a) q) i j

 remove1-≡-lemma : ∀ {a} {x} xs → a ≡ x → xs ≡ remove1 a (x ∷ xs)
 remove1-≡-lemma {a} {x} xs a≡x with discA a x
 ...                            | yes _   = refl
 ...                            | no  a≢x = ⊥.rec (a≢x a≡x)

 remove1-≢-lemma : ∀ {a} {x} xs → ¬ a ≡ x → remove1 a (x ∷ xs) ≡ x ∷ remove1 a xs
 remove1-≢-lemma {a} {x} xs a≢x with discA a x
 ...                            | yes a≡x = ⊥.rec (a≢x a≡x)
 ...                            | no  _   = refl

 remove1-predℕ-lemma : ∀ a xs → FMScount a (remove1 a xs) ≡ predℕ (FMScount a xs)
 remove1-predℕ-lemma a = ElimProp.f (isSetℕ _ _) refl θ
  where
  θ : ∀ x {xs} → FMScount a (remove1 a xs) ≡ predℕ (FMScount a xs)
               → FMScount a (remove1 a (x ∷ xs)) ≡ predℕ (FMScount a (x ∷ xs))
  θ x {xs} p with discA a x
  ...        | yes _   = refl
  ...        | no  a≢x = FMScount-≢-lemma (remove1 a xs) a≢x ∙ p

 remove1-zero-lemma : ∀ a xs → FMScount a xs ≡ zero → xs ≡ remove1 a xs
 remove1-zero-lemma a = ElimProp.f (isPropΠ λ _ → trunc _ _) (λ _ → refl) θ
  where
  θ : ∀ x {xs} → (FMScount a xs ≡ zero → xs ≡ remove1 a xs)
               → FMScount a (x ∷ xs) ≡ zero → x ∷ xs ≡ remove1 a (x ∷ xs)
  θ x {xs} hyp p with discA a x
  ...            | yes _ = ⊥.rec (snotz p)
  ...            | no  _ = cong (x ∷_) (hyp p)

 remove1-suc-lemma : ∀ a n xs → FMScount a xs ≡ suc n → xs ≡ a ∷ (remove1 a xs)
 remove1-suc-lemma a n = ElimProp.f (isPropΠ λ _ → trunc _ _) (λ p → ⊥.rec (znots p)) θ
  where
  θ : ∀ x {xs} → (FMScount a xs ≡ suc n → xs ≡ a ∷ (remove1 a xs))
               → FMScount a (x ∷ xs) ≡ suc n → x ∷ xs ≡ a ∷ (remove1 a (x ∷ xs))
  θ x {xs} hyp p with discA a x
  ...            | yes a≡x = (λ i → (sym a≡x i) ∷ xs)
  ...            | no  a≢x = cong (x ∷_) (hyp p) ∙ comm x a (remove1 a xs)

 FMScount-remove1-≢-lemma : ∀ {a} {x} xs → ¬ a ≡ x → FMScount a (remove1 x xs) ≡ FMScount a xs
 FMScount-remove1-≢-lemma {a} {x} xs a≢x with discreteℕ (FMScount x xs) zero
 ...                     | yes p = cong (FMScount a) (sym (remove1-zero-lemma x xs p))
 ...                     | no ¬p = sym (FMScount-≢-lemma (remove1 x xs) a≢x) ∙ cong (FMScount a) eq₁
   where
   eq₁ : (x ∷ remove1 x xs) ≡ xs
   eq₁ = sym (remove1-suc-lemma x (predℕ (FMScount x xs)) xs (suc-predℕ (FMScount x xs) ¬p))

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:
{-# OPTIONS --show-implicit --verbose=tc.reconstruct:50 #-}
open import ExtractSac as ES using ()
open import Extract (ES.kompile-fun)

open import Data.Nat
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.Fin using (Fin; zero; suc; #_)

open import Relation.Binary.PropositionalEquality

open import Reflection

open import Structures
open import ReflHelper
open import Function

open import Array.Base

-- Check that Vec² and List ∘ Vec are treated correctly.
-- Here we transpose a 2d array using Vec operations.
-- Note that we are using local where-defined functions.

test-20f : ∀ m n → Vec (Vec ℕ n) m → Vec (Vec ℕ m) n
test-20f 0       n []       = repl []
  where
    repl : ∀ {k} → Vec ℕ 0 → Vec _ k
    repl {0} x     = []
    repl {suc _} x = x ∷ repl x
test-20f (suc _) n (x ∷ xs) = xzip x (test-20f _ n xs)
  where
    xzip : ∀ {n} → Vec _ n → Vec _ n → Vec _ n
    xzip []       []       = []
    xzip (x ∷ xs) (y ∷ ys) = (x ∷ y) ∷ xzip xs ys

test₂₀ : kompile test-20f [] [] ≡ ok _
test₂₀ = refl

-- simplified version of the test20 for debugging purposes.
test-20f′ : ∀ n → Vec ℕ n → Vec (Vec ℕ 1) n → Vec (Vec ℕ 2) n
test-20f′ n xs ys = xzip xs ys
  where
    xzip : ∀ {n} → Vec _ n → Vec _ n → Vec _ n
    xzip []       []       = []
    xzip (x ∷ xs) (y ∷ ys) = (x ∷ y) ∷ xzip xs ys

test₂₀′ : kompile test-20f′ [] [] ≡ ok _
test₂₀′ = refl

-- Make sure that we can handle lists of hom. objects
test-21f : ∀ n → List (Vec ℕ n)
test-21f n = []

test₂₁ : kompile test-21f [] [] ≡ ok _
test₂₁ = refl

-- Test that cons and friends work on a simple example
test-22f : ∀ n → Vec (Vec ℕ n) 1
test-22f n = repl 0 ∷ []
 where
    repl : ∀ {m} → ℕ → Vec ℕ m
    repl {0} x     = []
    repl {suc _} x = x ∷ repl x

test₂₂ : kompile test-22f [] [] ≡ ok _
test₂₂ = refl

-- Test that polymorphic functions are failing with a reasonable error
test-23f : ∀ {X : Set} → X → X
test-23f x = x

test₂₃ : _≡_ {A = Prog} (kompile test-23f [] []) $ error _
test₂₃ = refl

-- FIXME: This gives a buggy assertion on the argument (that is not present)
test-24f : Vec ℕ (1 + 2)
test-24f = 1 ∷ 2 ∷ 3 ∷ []

test₂₄ : kompile test-24f [] [] ≡ ok _
test₂₄ = refl

-- Array stuff
test-25f : ℕ → Ar ℕ 1 V.[ 5 ]
test-25f n = cst n

test₂₅ : kompile test-25f [] [] ≡ ok _
test₂₅ = refl

-- Element-wise addition.
test-26f : ∀ {d s} → (a b : Ar ℕ d s) → Ar ℕ d s
test-26f a b = imap λ iv → sel a iv + sel b iv

test₂₆ : kompile test-26f [] [] ≡ ok _
test₂₆ = refl

test-27f : ∀ {d s} → (a b : Ar ℕ d s) → Ar ℕ d s
test-27f (imap a) (imap b) = imap λ iv → a iv + b iv

test₂₇ : kompile test-27f [] [] ≡ ok _
test₂₇ = refl

test-28f : ∀ {d s} → (a b : Ar ℕ d s) → Ar ℕ d s
test-28f (imap _) (imap a) = imap λ iv → a iv + 1

test₂₈ : kompile test-28f [] [] ≡ ok _
test₂₈ = refl

-- Testing for dot and absurd arguments of the imap.
test-29f : ∀ {d s} → (a b : Ar ℕ d s) → a ≡ b → Ar ℕ d s
test-29f (imap .a) (imap a) refl = imap λ iv → a iv + 1

test₂₉ : kompile test-29f [] [] ≡ ok _
test₂₉ = refl

-- We cannot write this:
--
-- open import Data.Empty
-- test-30f : Ar ⊥ 1 V.[ 1 ] → ⊥
-- test-30f (imap ())
--
-- even though `f` in imap has type Ix 1 [1] → ⊥, which doesn't exist.

-- If non-lambda is found as an argument of the imap.
test-31f : Ar ℕ 1 V.[ 10 ] → Ar ℕ 1 V.[ 10 ]
test-31f (imap f) = imap f

test₃₁ : kompile test-31f [] [] ≡ ok _
test₃₁ = refl

-- Index types
test-32f : Ix 2 (3 ∷ 4 ∷ []) → Fin 3
test-32f ix = ix-lookup ix (# 0)

test₃₂ : kompile test-32f [] [] ≡ ok _
test₃₂ = refl

module mat-mul where
  postulate
    asum : ∀ {n} → Ar ℕ 1 (n ∷ []) → ℕ

  mm : ∀ {m n k} → let Mat a b = Ar ℕ 2 (a ∷ b ∷ []) in
                  Mat m n → Mat n k → Mat m k
  mm (imap a) (imap b) = imap λ iv →
                                    let i = ix-lookup iv (# 0)
                                        j = ix-lookup iv (# 1)
                                    in asum (imap λ kv → let k = ix-lookup kv (# 0)
                                                         in a (i ∷ k ∷ []) * b (k ∷ j ∷ []))

  mm-kompiled = kompile mm [] (quote asum ∷ [])
  test₃₃ : mm-kompiled ≡ ok _
  test₃₃ = refl

-- This test ensurest that even if bound variables appear in
-- different order than in the telescope, we can still use them.
test-34f : ∀ {d s} → Ix (suc d) s → ℕ
test-34f {_}{x ∷ s} (_∷_ i ix) =  x

test-34t = kompile test-34f [] []
test₃₄ : test-34t ≡ ok ("\n\n// Function Example-02.test-34f\n"
                      ++ "int\nExample_02_test_34f(int x_1, int[.] x_2, int[.] x_4) {\n"
                      ++ "/* assert (dim (x_4) == (1 + x_1)) */\n/* assert (x_4 < x_2) */\n"
                      ++ "/* assert (shape (x_2)[[0]] == (1 + x_1)) */"
                      ++ "int __ret;\nd = x_1;\nx = hd (x_2);\ns = tl (x_2);\n"
                      ++ "i = hd (x_4);\nix = tl (x_4);\n__ret = x;\n"
                      ++ "return __ret;\n}\n\n")
test₃₄ = refl

test-35f : ∀ {d s} → Ix (suc d) s → ℕ
test-35f {_} (_∷_ {d}{s}{x} i ix) =  x

test₃₅ : kompile test-35f [] [] ≡ ok ("\n\n// Function Example-02.test-35f\n"
                                   ++ "int\nExample_02_test_35f(int x_1, int[.] x_2, int[.] x_4) {\n"
                                   ++ "/* assert (dim (x_4) == (1 + x_1)) */\n/* assert (x_4 < x_2) */\n"
                                   ++ "/* assert (shape (x_2)[[0]] == (1 + x_1)) */"
                                   ++ "int __ret;\nd = x_1;\nx = hd (x_2);\ns = tl (x_2);\n"
                                   ++ "i = hd (x_4);\nix = tl (x_4);\n__ret = x;\n"
                                   ++ "return __ret;\n}\n\n")
test₃₅ = refl

test-fold1 : ∀ {n} → Ar ℕ 1 V.[ n ] → Ar ℕ 1 V.[ n ]
test-fold1 a = imap λ iv → sel a iv + 5

test-fold : ∀ {n} → Ar ℕ 1 V.[ n ] → Ar ℕ 1 V.[ n ]
test-fold a = imap λ iv → sel (test-fold1 a) iv + 6

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
module Golden.Factorial where

open import Agda.Builtin.Nat

fac : Nat -> Nat
fac 0 = 1
fac (suc n) = suc n * fac n

a = fac 0
b = fac 10

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The binary relation defined by a constant
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Constant where

open import Relation.Binary

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

Const : ∀ {a b c} {A : Set a} {B : Set b} → Set c → REL A B c
Const I = λ _ _ → I

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

module _ {a c} (A : Set a) {C : Set c} where

  refl : C → Reflexive {A = A} (Const C)
  refl c = c

  sym : Symmetric {A = A} (Const C)
  sym c = c

  trans : Transitive {A = A} (Const C)
  trans c d = c

  isEquivalence : C → IsEquivalence {A = A} (Const C)
  isEquivalence c = record
    { refl  = λ {x} → refl c {x}
    ; sym   = λ {x} {y} → sym {x} {y}
    ; trans = λ {x} {y} {z} → trans {x} {y} {z}
    }

  setoid : C → Setoid a c
  setoid x = record { isEquivalence = isEquivalence x }


text:
module HOAny where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool

data Wrapper (M : Set → Set) : Set where
  mnat  : M Nat → Wrapper M
  mbool : M Bool → Wrapper M

{-# FOREIGN GHC data AgdaWrapper m = Mnat (m Integer) | Mbool (m Bool) #-}
{-# COMPILE GHC Wrapper = data AgdaWrapper (Mnat | Mbool) #-}

map : ∀ {M N} → (∀ {n} → M n → N n) → Wrapper M → Wrapper N
map f (mnat mn)  = mnat (f mn)
map f (mbool mb) = mbool (f mb)

-- Higher-order use of Any in the compiled code:

-- data AgdaWrapper m = Mnat (m Integer) | Mbool (m Bool)

-- map ::
--  (() -> ()) ->
--  (() -> ()) ->
--  (() -> AgdaAny -> AgdaAny) -> AgdaWrapper AgdaAny -> AgdaWrapper AgdaAny

-- WAS:
-- The expected kind to AgdaWrapper's argument is * -> *
-- but AgdaAny's kind is *

-- WANT: SUCCESS
-- made possible by making AgdaAny poly-kinded

open import Common.Prelude

main : IO Unit
main = putStrLn ""


text:
open import Algebra using (CommutativeRing)

module AKS.Polynomial {c ℓ} (R : CommutativeRing c ℓ) where

open import AKS.Polynomial.Properties R public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
-- Andreas, 2016-06-02
-- The filename "Issue.1947.agda" is invalid as "1947" is not a valid name.

module _ where


text:
import      Lvl

module Structure.Groupoid {ℓₒ ℓₘ ℓₑ : Lvl.Level} where

open import Functional using (swap)
open import Logic
open import Logic.Predicate
open import Logic.Propositional
import      Structure.Categorical.Names as Names
open import Structure.Categorical.Properties
open import Structure.Category{ℓₒ}{ℓₘ}{ℓₑ}
open import Structure.Operator
open import Structure.Relator.Equivalence
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

{- TODO: It would be nice if groupoids were defined using a category as a record field and if categories were defined using a semicategory as a record field (they are "substructures" of each other) so that no code-duplication is necessary, but the problem is how long the projections/copatterns become with this approach.
postulate A B C : Type{Lvl.𝟎}

record R : Type{Lvl.𝟎} where
  field
    a : A
    b : B

record R2 : Type{Lvl.𝟎} where
  field
    r : R
    c : C
  open R(r) public
  -- a = R.a r

-- This is not possible, but would be nice:
r2 : R2
R2.a r2 = ?
R2.b r2 = ?
R2.c r2 = ?

-- One must write this:
r2 : R2
R2.r(R.a r2) = ?
R2.r(R.b r2) = ?
R2.c r2 = ?

which means that the copatterns would be longer and longer for each nesting a record has.
If Agda had support for "copattern/projection synonyms" or if the example above worked, then
-}

-- Obj is the collection of objects.
-- _⟶_ is the collection of morphisms.
module _
  {Obj : Type{ℓₒ}}
  (_⟶_ : Obj → Obj → Type{ℓₘ})
  ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(x ⟶ y) ⦄
  where

  -- A groupoid is a structure on a relation called a morphism.
  --
  -- It can be seen as a generalization of the structure in invertible functions between a collection of types/sets.
  -- More specifically, the algebraic properties of functions regarding composition and the identity function together with an function inverter.
  -- In this case, sets are objects and functions are morphisms.
  --
  -- It can also be seen as a generalized algebraic structure, or more specifically a generalization of groups.
  -- The type of a group's operator is usually restricted to a single type, but a groupoid allows it to vary (depending on the rules of morphism instead).
  -- (One can loosely call a groupoid to be a group without the "closed" property of algebraic structures).
  -- In this case, the binary operation is (_∘_) and the laws are the usual identity, associative and inverse laws.
  --
  -- An alternative interpretation of the definition:
  -- A type (Obj) and a binary relation (Morphism) on this type is a groupoid when:
  -- • The relator is transitive.
  -- • The relator is reflexive.
  -- • The relator is symmetric.
  -- • The reflexivity proof inside the transitivity proof does not result in a new proof.
  -- • Chains of the transitivity proofs can be applied in any order and the resulting proof will be the same.
  -- • Transitivity of a proof of a pair and its symmetry is the reflexivity proof.
  -- In other words, this is a specialized equivalence relation/setoid on `Obj`. If the morphism equivalence is trivial (always true) for a groupoid, then the groupoid describes the same structure as an equivalence relation does.
  -- See `Relator.Equals.Category` for an example of this kind of binary relation.
  --
  -- A groupoid is the common pattern seen in all the examples above.
  record Groupoid : Stmt{ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
    field
      _∘_ : Names.SwappedTransitivity(_⟶_)
      id  : Names.Reflexivity(_⟶_)
      inv : Names.Symmetry(_⟶_)
    infixr 20 _∘_

    field
      ⦃ binaryOperator ⦄ : ∀{x y z} → BinaryOperator(_∘_ {x}{y}{z})
      ⦃ associativity ⦄ : Morphism.Associativity(\{x} → _∘_ {x})
      ⦃ identity ⦄ : Morphism.Identity(_∘_)(\{x} → id{x})
      ⦃ inverter ⦄ : Polymorphism.Inverter(_∘_)(\{x} → id{x})(inv)

    -- This can be interpreted as proof of symmetry when `Morphism` is interpreted as a binary relation.
    morphism-symmetry : Symmetry(_⟶_)
    morphism-symmetry = intro inv

    category : Category(_⟶_)
    Category._∘_            category = _∘_
    Category.id             category = id
    Category.binaryOperator category = binaryOperator
    Category.associativity  category = associativity
    Category.identity       category = identity

    open Category(category) hiding (_∘_ ; id ; binaryOperator ; associativity ; identity) public
    open Polymorphism.Inverter(_∘_)(\{x} → id{x})(inv)(inverter) renaming (left to inverterₗ ; right to inverterᵣ) public

    morphism-equivalence : Equivalence(_⟶_)
    Equivalence.reflexivity  morphism-equivalence = morphism-reflexivity
    Equivalence.symmetry     morphism-equivalence = morphism-symmetry
    Equivalence.transitivity morphism-equivalence = morphism-transitivity

    object-equiv : Equiv(Obj)
    object-equiv = intro(_⟶_) ⦃ morphism-equivalence ⦄

    morphism-setoid : Setoid
    morphism-setoid = [∃]-intro Obj ⦃ object-equiv ⦄

-- A category object can be used when one refers to a category as an object.
-- Examples of usage are in functors (morphism between categories) or in equivalences of categories.
record GroupoidObject : Stmt{Lvl.𝐒(ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {Object}           : Type{ℓₒ}
    {Morphism}         : Object → Object → Type{ℓₘ}
    ⦃ morphism-equiv ⦄ : ∀{x y} → Equiv{ℓₑ}(Morphism x y)
    groupoid           : Groupoid(Morphism)

  open Groupoid(groupoid) public
  instance
    groupoid-instance = groupoid

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
module tests.Coind where

open import Prelude.IO
open import Prelude.Level
open import Prelude.Nat
open import Prelude.Unit

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

data Stream (A : Set) : Set where
  _::_ : (x : A) (xs : ∞ (Stream A)) → Stream A

ones : Stream Nat
ones = 1 :: (♯ ones)

twos : Stream Nat
twos = 2 :: (♯ twos)

incr : Nat -> Stream Nat
incr n = n :: (♯ (incr (n + 1)))

printStream : Nat -> Stream Nat -> IO Unit
printStream Z _ = putStrLn ""
printStream (S steps) (n :: ns) =
    printNat n ,,
    printStream steps (♭ ns)

main : IO Unit
main =
    printStream 10 twos ,,
    printStream 10 ones ,,
    printStream 10 (incr Z)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Logic.Propositional.Equiv where

import      Lvl
open import Logic
open import Logic.Propositional
import      Logic.Propositional.Theorems as Theorems
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable T A B : Type{ℓ}

instance
  [↔]-reflexivity : Reflexivity{ℓ₂ = ℓ}(_↔_)
  [↔]-reflexivity = intro Theorems.[↔]-reflexivity

instance
  [↔]-symmetry : Symmetry{ℓ₂ = ℓ}(_↔_)
  [↔]-symmetry = intro Theorems.[↔]-symmetry

instance
  [↔]-transitivity : Transitivity{ℓ₂ = ℓ}(_↔_)
  [↔]-transitivity = intro Theorems.[↔]-transitivity

instance
  [↔]-equivalence : Equivalence{ℓ₂ = ℓ}(_↔_)
  [↔]-equivalence = intro

instance
  [↔]-equiv : Equiv(Stmt{ℓ})
  [↔]-equiv = intro(_↔_) ⦃ [↔]-equivalence ⦄