text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of Rational numbers
------------------------------------------------------------------------

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

module Data.Rational.Properties where

open import Algebra.Consequences.Propositional
open import Algebra.Morphism
open import Algebra.Bundles
import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphisms
import Algebra.Morphism.GroupMonomorphism as GroupMonomorphisms
import Algebra.Morphism.RingMonomorphism as RingMonomorphisms
import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
open import Data.Integer.Base as ℤ using (ℤ; ∣_∣; +_; -[1+_]; 0ℤ; _◃_)
open import Data.Integer.Coprimality using (coprime-divisor)
import Data.Integer.Properties as ℤ
open import Data.Integer.GCD using (gcd; gcd[i,j]≡0⇒i≡0; gcd[i,j]≡0⇒j≡0)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕ
open import Data.Nat.Coprimality as C using (Coprime; coprime?)
open import Data.Nat.Divisibility hiding (/-cong)
import Data.Nat.GCD as ℕ
import Data.Nat.DivMod as ℕ
open import Data.Product using (_×_; _,_)
open import Data.Rational.Base
open import Data.Rational.Unnormalised as ℚᵘ
  using (ℚᵘ; *≡*; *≤*) renaming (↥_ to ↥ᵘ_; ↧_ to ↧ᵘ_; _≃_ to _≃ᵘ_; _≤_ to _≤ᵘ_)
import Data.Rational.Unnormalised.Properties as ℚᵘ
open import Data.Sum.Base
open import Data.Unit using (tt)
import Data.Sign as S
open import Function using (_∘_ ; _$_; Injective)
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Morphism.Structures
import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms
open import Relation.Nullary using (yes; no; recompute)
open import Relation.Nullary.Decidable as Dec
  using (True; False; fromWitness; fromWitnessFalse)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Decidable as Dec using (True; fromWitness; map′)
open import Relation.Nullary.Product using (_×-dec_)

open import Algebra.Definitions {A = ℚ} _≡_
open import Algebra.Structures {A = ℚ} _≡_

private
  infix 4 _≢0
  _≢0 : ℕ → Set
  n ≢0 = False (n ℕ.≟ 0)

  recomputeCP : ∀ {n d} → .(Coprime n d) → Coprime n d
  recomputeCP {n} {d} c = recompute (coprime? n d) c

------------------------------------------------------------------------
-- Propositional equality
------------------------------------------------------------------------

mkℚ-injective : ∀ {n₁ n₂ d₁ d₂} .{c₁ : Coprime ∣ n₁ ∣ (suc d₁)}
                                .{c₂ : Coprime ∣ n₂ ∣ (suc d₂)} →
                mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂ → n₁ ≡ n₂ × d₁ ≡ d₂
mkℚ-injective refl = refl , refl

infix 4 _≟_

_≟_ : Decidable {A = ℚ} _≡_
mkℚ n₁ d₁ _ ≟ mkℚ n₂ d₂ _ =
  map′ (λ { (refl , refl) → refl }) mkℚ-injective (n₁ ℤ.≟ n₂ ×-dec d₁ ℕ.≟ d₂)

≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid ℚ

≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_

------------------------------------------------------------------------
-- mkℚ
------------------------------------------------------------------------

mkℚ-cong : ∀ {n₁ n₂ d₁ d₂}
           .{c₁ : Coprime ∣ n₁ ∣ (suc d₁)}
           .{c₂ : Coprime ∣ n₂ ∣ (suc d₂)} →
           n₁ ≡ n₂ → d₁ ≡ d₂ → mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
mkℚ-cong refl refl = refl

------------------------------------------------------------------------
-- mkℚ′
------------------------------------------------------------------------

mkℚ+-cong : ∀ {n₁ n₂ d₁ d₂} d₁≢0 d₂≢0
           .{c₁ : Coprime n₁ d₁}
           .{c₂ : Coprime n₂ d₂} →
           n₁ ≡ n₂ → d₁ ≡ d₂ →
           mkℚ+ n₁ d₁ {d₁≢0} c₁ ≡ mkℚ+ n₂ d₂ {d₂≢0} c₂
mkℚ+-cong _ _ refl refl = refl

↥-mkℚ+ : ∀ n d {d≢0} .{c : Coprime n d} → ↥ (mkℚ+ n d {d≢0} c) ≡ + n
↥-mkℚ+ n (suc d) = refl

↧-mkℚ+ : ∀ n d {d≢0} .{c : Coprime n d} → ↧ (mkℚ+ n d {d≢0} c) ≡ + d
↧-mkℚ+ n (suc d) = refl

------------------------------------------------------------------------
-- Numerator and denominator equality
------------------------------------------------------------------------

≡⇒≃ : _≡_ ⇒ _≃_
≡⇒≃ refl = refl

≃⇒≡ : _≃_ ⇒ _≡_
≃⇒≡ {x = mkℚ n₁ d₁ c₁} {y = mkℚ n₂ d₂ c₂} eq = helper
  where
  open ≡-Reasoning

  1+d₁∣1+d₂ : suc d₁ ∣ suc d₂
  1+d₁∣1+d₂ = coprime-divisor (+ suc d₁) n₁ (+ suc d₂)
    (C.sym (recomputeCP c₁)) $
    divides ∣ n₂ ∣ $ begin
      ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ cong ∣_∣ eq ⟩
      ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ ℤ.abs-*-commute n₂ (+ suc d₁) ⟩
      ∣ n₂ ∣ ℕ.* suc d₁    ∎

  1+d₂∣1+d₁ : suc d₂ ∣ suc d₁
  1+d₂∣1+d₁ = coprime-divisor (+ suc d₂) n₂ (+ suc d₁)
    (C.sym (recomputeCP c₂)) $
    divides ∣ n₁ ∣ (begin
      ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ cong ∣_∣ (sym eq) ⟩
      ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ ℤ.abs-*-commute n₁ (+ suc d₂) ⟩
      ∣ n₁ ∣ ℕ.* suc d₂    ∎)

  helper : mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
  helper with ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
  ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) (λ ()) eq
  ...   | refl = refl

------------------------------------------------------------------------
-- Properties of -_
------------------------------------------------------------------------

↥-neg : ∀ p → ↥ (- p) ≡ ℤ.- (↥ p)
↥-neg (mkℚ -[1+ _ ] _ _) = refl
↥-neg (mkℚ +0       _ _) = refl
↥-neg (mkℚ +[1+ _ ] _ _) = refl

↧-neg : ∀ p → ↧ (- p) ≡ ↧ p
↧-neg (mkℚ -[1+ _ ] _ _) = refl
↧-neg (mkℚ +0       _ _) = refl
↧-neg (mkℚ +[1+ _ ] _ _) = refl

------------------------------------------------------------------------
-- Properties of normalize
------------------------------------------------------------------------

normalize-coprime : ∀ {n d-1} .(c : Coprime n (suc d-1)) →
                    normalize n (suc d-1) ≡ mkℚ (+ n) d-1 c
normalize-coprime {n} {d-1} c = begin
  normalize n d              ≡⟨⟩
  mkℚ+ (n ℕ./ g) (d ℕ./ g) _ ≡⟨ mkℚ+-cong n/g≢0 d/1≢0 {c₂ = c₂} (ℕ./-congʳ {n≢0 = g≢0} g≡1) (ℕ./-congʳ {n≢0 = g≢0} g≡1) ⟩
  mkℚ+ (n ℕ./ 1) (d ℕ./ 1) _ ≡⟨ mkℚ+-cong d/1≢0 _ {c₂ = c} (ℕ.n/1≡n n) (ℕ.n/1≡n d) ⟩
  mkℚ+ n d _                 ≡⟨⟩
  mkℚ (+ n) d-1 _            ∎
  where
  open ≡-Reasoning; d = suc d-1; g = ℕ.gcd n d
  c′ = recomputeCP c
  c₂ : Coprime (n ℕ./ 1) (d ℕ./ 1)
  c₂ = subst₂ Coprime (sym (ℕ.n/1≡n n)) (sym (ℕ.n/1≡n d)) c′
  g≡1 = C.coprime⇒gcd≡1 c′
  g≢0   = fromWitnessFalse (ℕ.gcd[m,n]≢0 n d (inj₂ λ()))
  n/g≢0 = fromWitnessFalse (ℕ.n/gcd[m,n]≢0 n d {_} {g≢0})
  d/1≢0 = fromWitnessFalse (subst (_≢ 0) (sym (ℕ.n/1≡n d)) λ())

↥-normalize : ∀ i n {n≢0} → ↥ (normalize i n {n≢0}) ℤ.* gcd (+ i) (+ n) ≡ + i
↥-normalize i n@(suc n-1) = begin
  ↥ (normalize i n) ℤ.* + g  ≡⟨ cong (ℤ._* + g) (↥-mkℚ+ _ (n ℕ./ g) {n/g≢0}) ⟩
  + (i ℕ./ g)       ℤ.* + g  ≡⟨⟩
  S.+ ◃ i ℕ./ g     ℕ.* g    ≡⟨ cong (S.+ ◃_) (ℕ.m/n*n≡m (ℕ.gcd[m,n]∣m i n)) ⟩
  S.+ ◃ i                    ≡⟨ ℤ.+◃n≡+n i ⟩
  + i                        ∎
  where
  open ≡-Reasoning; g = ℕ.gcd i n
  g≢0   = fromWitnessFalse (ℕ.gcd[m,n]≢0 i n (inj₂ λ()))
  n/g≢0 = fromWitnessFalse (ℕ.n/gcd[m,n]≢0 i n {_} {g≢0})

↧-normalize : ∀ i n {n≢0} → ↧ (normalize i n {n≢0}) ℤ.* gcd (+ i) (+ n) ≡ + n
↧-normalize i n@(suc n-1) = begin
  ↧ (normalize i n) ℤ.* + g  ≡⟨ cong (ℤ._* + g) (↧-mkℚ+ _ (n ℕ./ g) {n/g≢0}) ⟩
  + (n ℕ./ g)       ℤ.* + g  ≡⟨⟩
  S.+ ◃ n ℕ./ g     ℕ.* g    ≡⟨ cong (S.+ ◃_) (ℕ.m/n*n≡m (ℕ.gcd[m,n]∣n i n)) ⟩
  S.+ ◃ n                    ≡⟨ ℤ.+◃n≡+n n ⟩
  + n                        ∎
  where
  open ≡-Reasoning; g = ℕ.gcd i n
  g≢0   = fromWitnessFalse (ℕ.gcd[m,n]≢0 i n (inj₂ λ()))
  n/g≢0 = fromWitnessFalse (ℕ.n/gcd[m,n]≢0 i n {_} {g≢0})

------------------------------------------------------------------------
-- Properties of toℚ/fromℚ
------------------------------------------------------------------------

toℚᵘ-cong : toℚᵘ Preserves _≡_ ⟶ _≃ᵘ_
toℚᵘ-cong refl = *≡* refl

toℚᵘ-injective : Injective _≡_ _≃ᵘ_ toℚᵘ
toℚᵘ-injective (*≡* eq) = ≃⇒≡ eq

toℚᵘ-isRelHomomorphism : IsRelHomomorphism _≡_ _≃ᵘ_ toℚᵘ
toℚᵘ-isRelHomomorphism = record
  { cong = toℚᵘ-cong
  }

toℚᵘ-isRelMonomorphism : IsRelMonomorphism _≡_ _≃ᵘ_ toℚᵘ
toℚᵘ-isRelMonomorphism = record
  { isHomomorphism = toℚᵘ-isRelHomomorphism
  ; injective      = toℚᵘ-injective
  }

fromℚᵘ-toℚᵘ : ∀ p → fromℚᵘ (toℚᵘ p) ≡ p
fromℚᵘ-toℚᵘ (mkℚ (+ n)      d-1 c) = normalize-coprime c
fromℚᵘ-toℚᵘ (mkℚ (-[1+ n ]) d-1 c) = cong (-_) (normalize-coprime c)

------------------------------------------------------------------------
-- Properties of _≤_
------------------------------------------------------------------------

drop-*≤* : ∀ {p q} → p ≤ q → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p)
drop-*≤* (*≤* pq≤qp) = pq≤qp

------------------------------------------------------------------------
-- toℚᵘ is a isomorphism

toℚᵘ-mono-≤ : ∀ {p q} → p ≤ q → toℚᵘ p ≤ᵘ toℚᵘ q
toℚᵘ-mono-≤ (*≤* p≤q) = *≤* p≤q

toℚᵘ-cancel-≤ : ∀ {p q} → toℚᵘ p ≤ᵘ toℚᵘ q → p ≤ q
toℚᵘ-cancel-≤ (*≤* p≤q) = *≤* p≤q

toℚᵘ-isOrderHomomorphism-≤ : IsOrderHomomorphism _≡_ _≃ᵘ_ _≤_ _≤ᵘ_ toℚᵘ
toℚᵘ-isOrderHomomorphism-≤ = record
  { cong = toℚᵘ-cong
 ; mono = toℚᵘ-mono-≤
  }

toℚᵘ-isOrderMonomorphism-≤ : IsOrderMonomorphism _≡_ _≃ᵘ_ _≤_ _≤ᵘ_ toℚᵘ
toℚᵘ-isOrderMonomorphism-≤ = record
  { isOrderHomomorphism = toℚᵘ-isOrderHomomorphism-≤
  ; injective           = toℚᵘ-injective
  ; cancel              = toℚᵘ-cancel-≤
  }

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

private
  module ≤-Monomorphism = OrderMonomorphisms toℚᵘ-isOrderMonomorphism-≤

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive refl = *≤* ℤ.≤-refl

≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl

≤-trans : Transitive _≤_
≤-trans = ≤-Monomorphism.trans ℚᵘ.≤-trans

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym (*≤* le₁) (*≤* le₂) = ≃⇒≡ (ℤ.≤-antisym le₁ le₂)

≤-total : Total _≤_
≤-total p q = [ inj₁ ∘ *≤* , inj₂ ∘ *≤* ]′ (ℤ.≤-total (↥ p ℤ.* ↧ q) (↥ q ℤ.* ↧ p))

infix 4 _≤?_
_≤?_ : Decidable _≤_
p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p)

≤-irrelevant : Irrelevant _≤_
≤-irrelevant (*≤* p≤q₁) (*≤* p≤q₂) = cong *≤* (ℤ.≤-irrelevant p≤q₁ p≤q₂)

------------------------------------------------------------------------
-- Structures

≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

------------------------------------------------------------------------
-- Bundles

≤-decTotalOrder : DecTotalOrder _ _ _
≤-decTotalOrder = record
  { Carrier         = ℚ
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = ≤-isDecTotalOrder
  }

------------------------------------------------------------------------
-- Properties of _<_
------------------------------------------------------------------------

drop-*<* : ∀ {p q} → p < q → (↥ p ℤ.* ↧ q) ℤ.< (↥ q ℤ.* ↧ p)
drop-*<* (*<* pq<qp) = pq<qp

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

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ (*<* p<q) = *≤* (ℤ.<⇒≤ p<q)

<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (*<* p<p) = ℤ.<-irrefl refl p<p

<-asym : Asymmetric _<_
<-asym (*<* p<q) (*<* q<p) = ℤ.<-asym p<q q<p

<-≤-trans : Trans _<_ _≤_ _<_
<-≤-trans {p} {q} {r} (*<* p<q) (*≤* q≤r) = *<*
  (ℤ.*-cancelʳ-<-non-neg _ (begin-strict
  let n₁ = ↥ p; n₂ = ↥ q; n₃ = ↥ r; sd₁ = ↧ p; sd₂ = ↧ q; sd₃ = ↧ r in
  (n₁  ℤ.* sd₃) ℤ.* sd₂  ≡⟨ ℤ.*-assoc n₁ sd₃ sd₂ ⟩
  n₁   ℤ.* (sd₃ ℤ.* sd₂) ≡⟨ cong (n₁ ℤ.*_) (ℤ.*-comm sd₃ sd₂) ⟩
  n₁   ℤ.* (sd₂ ℤ.* sd₃) ≡⟨ sym (ℤ.*-assoc n₁ sd₂ sd₃) ⟩
  (n₁  ℤ.* sd₂) ℤ.* sd₃  <⟨ ℤ.*-monoʳ-<-pos (ℕ.pred (↧ₙ r)) p<q ⟩
  (n₂  ℤ.* sd₁) ℤ.* sd₃  ≡⟨ cong (ℤ._* sd₃) (ℤ.*-comm n₂ sd₁) ⟩
  (sd₁ ℤ.* n₂)  ℤ.* sd₃  ≡⟨ ℤ.*-assoc sd₁ n₂ sd₃ ⟩
  sd₁  ℤ.* (n₂  ℤ.* sd₃) ≤⟨ ℤ.*-monoˡ-≤-pos (ℕ.pred (↧ₙ p)) q≤r ⟩
  sd₁  ℤ.* (n₃  ℤ.* sd₂) ≡⟨ sym (ℤ.*-assoc sd₁ n₃ sd₂) ⟩
  (sd₁ ℤ.* n₃)  ℤ.* sd₂  ≡⟨ cong (ℤ._* sd₂) (ℤ.*-comm sd₁ n₃) ⟩
  (n₃  ℤ.* sd₁) ℤ.* sd₂  ∎))
  where open ℤ.≤-Reasoning

≤-<-trans : Trans _≤_ _<_ _<_
≤-<-trans {p} {q} {r} (*≤* p≤q) (*<* q<r) = *<*
  (ℤ.*-cancelʳ-<-non-neg _ (begin-strict
  let n₁ = ↥ p; n₂ = ↥ q; n₃ = ↥ r; sd₁ = ↧ p; sd₂ = ↧ q; sd₃ = ↧ r in
  (n₁  ℤ.* sd₃) ℤ.* sd₂  ≡⟨ ℤ.*-assoc n₁ sd₃ sd₂ ⟩
  n₁   ℤ.* (sd₃ ℤ.* sd₂) ≡⟨ cong (n₁ ℤ.*_) (ℤ.*-comm sd₃ sd₂) ⟩
  n₁   ℤ.* (sd₂ ℤ.* sd₃) ≡⟨ sym (ℤ.*-assoc n₁ sd₂ sd₃) ⟩
  (n₁  ℤ.* sd₂) ℤ.* sd₃  ≤⟨ ℤ.*-monoʳ-≤-pos (ℕ.pred (↧ₙ r)) p≤q ⟩
  (n₂  ℤ.* sd₁) ℤ.* sd₃  ≡⟨ cong (ℤ._* sd₃) (ℤ.*-comm n₂ sd₁) ⟩
  (sd₁ ℤ.* n₂)  ℤ.* sd₃  ≡⟨ ℤ.*-assoc sd₁ n₂ sd₃ ⟩
  sd₁  ℤ.* (n₂  ℤ.* sd₃) <⟨ ℤ.*-monoˡ-<-pos (ℕ.pred (↧ₙ p)) q<r ⟩
  sd₁  ℤ.* (n₃  ℤ.* sd₂) ≡⟨ sym (ℤ.*-assoc sd₁ n₃ sd₂) ⟩
  (sd₁ ℤ.* n₃)  ℤ.* sd₂  ≡⟨ cong (ℤ._* sd₂) (ℤ.*-comm sd₁ n₃) ⟩
  (n₃  ℤ.* sd₁) ℤ.* sd₂  ∎))
  where open ℤ.≤-Reasoning

<-trans : Transitive _<_
<-trans p<q = ≤-<-trans (<⇒≤ p<q)

infix 4 _<?_

_<?_ : Decidable _<_
p <? q = Dec.map′ *<* drop-*<* ((↥ p ℤ.* ↧ q) ℤ.<? (↥ q ℤ.* ↧ p))

<-cmp : Trichotomous _≡_ _<_
<-cmp p q with ℤ.<-cmp (↥ p ℤ.* ↧ q) (↥ q ℤ.* ↧ p)
... | tri< < ≢ ≯ = tri< (*<* <)        (≢ ∘ ≡⇒≃) (≯ ∘ drop-*<*)
... | tri≈ ≮ ≡ ≯ = tri≈ (≮ ∘ drop-*<*) (≃⇒≡ ≡)   (≯ ∘ drop-*<*)
... | tri> ≮ ≢ > = tri> (≮ ∘ drop-*<*) (≢ ∘ ≡⇒≃) (*<* >)

<-irrelevant : Irrelevant _<_
<-irrelevant (*<* p<q₁) (*<* p<q₂) = cong *<* (ℤ.<-irrelevant p<q₁ p<q₂)

<-respʳ-≡ : _<_ Respectsʳ _≡_
<-respʳ-≡ = subst (_ <_)

<-respˡ-≡ : _<_ Respectsˡ _≡_
<-respˡ-≡ = subst (_< _)

<-resp-≡ : _<_ Respects₂ _≡_
<-resp-≡ = <-respʳ-≡ , <-respˡ-≡

------------------------------------------------------------------------
-- Structures

<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
  { isEquivalence = isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans
  ; <-resp-≈      = <-resp-≡
  }

<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
  { isEquivalence = isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

------------------------------------------------------------------------
-- Bundles

<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
<-strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder
  }

<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder
  }

------------------------------------------------------------------------
-- A specialised module for reasoning about the _≤_ and _<_ relations
------------------------------------------------------------------------

module ≤-Reasoning where
  open import Relation.Binary.Reasoning.Base.Triple
    ≤-isPreorder
    <-trans
    (resp₂ _<_)
    <⇒≤
    <-≤-trans
    ≤-<-trans
    public
    hiding (step-≈; step-≈˘)

------------------------------------------------------------------------
-- Properties of _/_
------------------------------------------------------------------------

↥-/ : ∀ i n {n≢0} → ↥ (i / n) {n≢0} ℤ.* gcd i (+ n) ≡ i
↥-/ (+ m)    (suc n) = ↥-normalize m (suc n)
↥-/ -[1+ m ] (suc n) = begin-equality
  ↥ (- norm)   ℤ.* + g  ≡⟨ cong (ℤ._* + g) (↥-neg norm) ⟩
  ℤ.- (↥ norm) ℤ.* + g  ≡⟨ sym (ℤ.neg-distribˡ-* (↥ norm) (+ g)) ⟩
  ℤ.- (↥ norm  ℤ.* + g) ≡⟨ cong (ℤ.-_) (↥-normalize (suc m) (suc n)) ⟩
  S.- ◃ suc m           ≡⟨⟩
  -[1+ m ]              ∎
  where
  open ℤ.≤-Reasoning
  g = ℕ.gcd (suc m) (suc n)
  norm = normalize (suc m) (suc n)

↧-/ : ∀ i n {n≢0} → ↧ (i / n) {n≢0} ℤ.* gcd i (+ n) ≡ + n
↧-/ (+ m)    (suc n) = ↧-normalize m (suc n)
↧-/ -[1+ m ] (suc n) = begin-equality
  ↧ (- norm) ℤ.* + g  ≡⟨ cong (ℤ._* + g) (↧-neg norm) ⟩
  ↧ norm     ℤ.* + g  ≡⟨ ↧-normalize (suc m) (suc n) ⟩
  + (suc n)           ∎
  where
  open ℤ.≤-Reasoning
  g = ℕ.gcd (suc m) (suc n)
  norm = normalize (suc m) (suc n)

↥p/↧p≡p : ∀ p → ↥ p / ↧ₙ p ≡ p
↥p/↧p≡p (mkℚ (+ n)    d-1 prf) = normalize-coprime prf
↥p/↧p≡p (mkℚ -[1+ n ] d-1 prf) = cong (-_) (normalize-coprime prf)

0/n≡0 : ∀ n {n≢0} → (0ℤ / n) {n≢0} ≡ 0ℚ
0/n≡0 n@(suc n-1) {n≢0} = mkℚ+-cong n/n≢0 _ {c₂ = 0-cop-1} (ℕ.0/n≡0 (ℕ.gcd 0 n)) (ℕ.n/n≡1 n)
  where
  n/n≢0 = subst _≢0 (sym (ℕ.n/n≡1 n)) _
  0-cop-1 = C.sym (C.1-coprimeTo 0)

------------------------------------------------------------------------
-- Properties of _+_
------------------------------------------------------------------------

private
  ↥+ᵘ : ℚ → ℚ → ℤ
  ↥+ᵘ p q = ↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p

  ↧+ᵘ : ℚ → ℚ → ℤ
  ↧+ᵘ p q = ↧ p ℤ.* ↧ q

  +-nf : ℚ → ℚ → ℤ
  +-nf p q = gcd (↥+ᵘ p q) (↧+ᵘ p q)

↥-+ : ∀ p q → ↥ (p + q) ℤ.* +-nf p q ≡ ↥+ᵘ p q
↥-+ p q = ↥-/ (↥+ᵘ p q) (↧ₙ p ℕ.* ↧ₙ q)

↧-+ : ∀ p q → ↧ (p + q) ℤ.* +-nf p q ≡ ↧+ᵘ p q
↧-+ p q = ↧-/ (↥+ᵘ p q) (↧ₙ p ℕ.* ↧ₙ q)

------------------------------------------------------------------------
-- Raw bundles

+-rawMagma : RawMagma 0ℓ 0ℓ
+-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  }

+-rawMonoid : RawMonoid 0ℓ 0ℓ
+-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  ; ε   = 0ℚ
  }

+-0-rawGroup : RawGroup 0ℓ 0ℓ
+-0-rawGroup = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  ; ε   = 0ℚ
  ; _⁻¹ = -_
  }

+-*-rawRing : RawRing 0ℓ 0ℓ
+-*-rawRing = record
  { _≈_ = _≡_
  ; _+_ = _+_
  ; _*_ = _*_
  ; -_  = -_
  ; 0#  = 0ℚ
  ; 1#  = 1ℚ
  }

------------------------------------------------------------------------
-- Monomorphic to unnormalised _+_

open Definitions ℚ ℚᵘ ℚᵘ._≃_

toℚᵘ-homo-+ : Homomorphic₂ toℚᵘ _+_ ℚᵘ._+_
toℚᵘ-homo-+ p q with +-nf p q ℤ.≟ 0ℤ
... | yes nf[p,q]≡0 = *≡* (begin
  ↥ (p + q) ℤ.* ↧+ᵘ p q   ≡⟨ cong (ℤ._* ↧+ᵘ p q) eq ⟩
  0ℤ        ℤ.* ↧+ᵘ p q   ≡⟨⟩
  0ℤ        ℤ.* ↧ (p + q) ≡⟨ cong (ℤ._* ↧ (p + q)) (sym eq2) ⟩
  ↥+ᵘ p q   ℤ.* ↧ (p + q) ∎)
  where
  open ≡-Reasoning
  eq2 : ↥+ᵘ p q ≡ 0ℤ
  eq2 = gcd[i,j]≡0⇒i≡0 (↥+ᵘ p q) (↧+ᵘ p q) nf[p,q]≡0

  eq : ↥ (p + q) ≡ 0ℤ
  eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))

... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) nf[p,q]≢0 (begin
  ↥ (p + q) ℤ.* ↧+ᵘ p q    ℤ.* +-nf p q   ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩
  ↥ (p + q) ℤ.* +-nf p q   ℤ.* ↧+ᵘ p q    ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩
  ↥+ᵘ p q   ℤ.* ↧+ᵘ p q                   ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩
  ↥+ᵘ p q   ℤ.* (↧ (p + q) ℤ.* +-nf p q)  ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩
  ↥+ᵘ p q   ℤ.* ↧ (p + q)  ℤ.* +-nf p q   ∎))
  where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup

toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ
toℚᵘ-isMagmaHomomorphism-+ = record
  { isRelHomomorphism = toℚᵘ-isRelHomomorphism
  ; homo              = toℚᵘ-homo-+
  }

toℚᵘ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-rawMonoid ℚᵘ.+-rawMonoid toℚᵘ
toℚᵘ-isMonoidHomomorphism-+ = record
  { isMagmaHomomorphism = toℚᵘ-isMagmaHomomorphism-+
  ; ε-homo              = ℚᵘ.≃-refl
  }

toℚᵘ-isMonoidMonomorphism-+ : IsMonoidMonomorphism +-rawMonoid ℚᵘ.+-rawMonoid toℚᵘ
toℚᵘ-isMonoidMonomorphism-+ = record
  { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-+
  ; injective            = toℚᵘ-injective
  }

------------------------------------------------------------------------
-- Monomorphic to unnormalised -_

toℚᵘ-homo‿- : Homomorphic₁ toℚᵘ (-_) (ℚᵘ.-_)
toℚᵘ-homo‿- (mkℚ +0       _ _) = *≡* refl
toℚᵘ-homo‿- (mkℚ +[1+ _ ] _ _) = *≡* refl
toℚᵘ-homo‿- (mkℚ -[1+ _ ] _ _) = *≡* refl

toℚᵘ-isGroupHomomorphism-+ : IsGroupHomomorphism +-0-rawGroup ℚᵘ.+-0-rawGroup toℚᵘ
toℚᵘ-isGroupHomomorphism-+ = record
  { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-+
  ; ⁻¹-homo              = toℚᵘ-homo‿-
  }

toℚᵘ-isGroupMonomorphism-+ : IsGroupMonomorphism +-0-rawGroup ℚᵘ.+-0-rawGroup toℚᵘ
toℚᵘ-isGroupMonomorphism-+ = record
  { isGroupHomomorphism = toℚᵘ-isGroupHomomorphism-+
  ; injective           = toℚᵘ-injective
  }

------------------------------------------------------------------------
-- Algebraic properties

private
  module +-Monomorphism = GroupMonomorphisms toℚᵘ-isGroupMonomorphism-+

+-assoc : Associative _+_
+-assoc = +-Monomorphism.assoc ℚᵘ.+-isMagma ℚᵘ.+-assoc

+-comm : Commutative _+_
+-comm = +-Monomorphism.comm ℚᵘ.+-isMagma ℚᵘ.+-comm

+-identityˡ : LeftIdentity 0ℚ _+_
+-identityˡ = +-Monomorphism.identityˡ ℚᵘ.+-isMagma ℚᵘ.+-identityˡ

+-identityʳ : RightIdentity 0ℚ _+_
+-identityʳ = +-Monomorphism.identityʳ ℚᵘ.+-isMagma ℚᵘ.+-identityʳ

+-identity : Identity 0ℚ _+_
+-identity = +-identityˡ , +-identityʳ

+-inverseˡ : LeftInverse 0ℚ -_ _+_
+-inverseˡ = +-Monomorphism.inverseˡ ℚᵘ.+-isMagma ℚᵘ.+-inverseˡ

+-inverseʳ : RightInverse 0ℚ -_ _+_
+-inverseʳ = +-Monomorphism.inverseʳ ℚᵘ.+-isMagma ℚᵘ.+-inverseʳ

+-inverse : Inverse 0ℚ -_ _+_
+-inverse = +-Monomorphism.inverse ℚᵘ.+-isMagma ℚᵘ.+-inverse

-‿cong :  Congruent₁ (-_)
-‿cong = +-Monomorphism.⁻¹-cong ℚᵘ.+-isMagma ℚᵘ.-‿cong

------------------------------------------------------------------------
-- Structures

+-isMagma : IsMagma _+_
+-isMagma = +-Monomorphism.isMagma ℚᵘ.+-isMagma

+-isSemigroup : IsSemigroup _+_
+-isSemigroup = +-Monomorphism.isSemigroup ℚᵘ.+-isSemigroup

+-0-isMonoid : IsMonoid _+_ 0ℚ
+-0-isMonoid = +-Monomorphism.isMonoid ℚᵘ.+-0-isMonoid

+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0ℚ
+-0-isCommutativeMonoid = +-Monomorphism.isCommutativeMonoid ℚᵘ.+-0-isCommutativeMonoid

+-0-isGroup : IsGroup _+_ 0ℚ (-_)
+-0-isGroup = +-Monomorphism.isGroup ℚᵘ.+-0-isGroup

+-0-isAbelianGroup : IsAbelianGroup _+_ 0ℚ (-_)
+-0-isAbelianGroup = +-Monomorphism.isAbelianGroup ℚᵘ.+-0-isAbelianGroup

------------------------------------------------------------------------
-- Packages

+-magma : Magma 0ℓ 0ℓ
+-magma = record
  { isMagma = +-isMagma
  }

+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
  { isSemigroup = +-isSemigroup
  }

+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
  { isMonoid = +-0-isMonoid
  }

+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
  { isCommutativeMonoid = +-0-isCommutativeMonoid
  }

+-0-group : Group 0ℓ 0ℓ
+-0-group = record
  { isGroup = +-0-isGroup
  }

+-0-abelianGroup : AbelianGroup 0ℓ 0ℓ
+-0-abelianGroup = record
  { isAbelianGroup = +-0-isAbelianGroup
  }

------------------------------------------------------------------------
-- Properties of _*_
------------------------------------------------------------------------

private
  *-nf : ℚ → ℚ → ℤ
  *-nf p q = gcd (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q)

↥-* : ∀ p q → ↥ (p * q) ℤ.* *-nf p q ≡ ↥ p ℤ.* ↥ q
↥-* p q = ↥-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q)

↧-* : ∀ p q → ↧ (p * q) ℤ.* *-nf p q ≡ ↧ p ℤ.* ↧ q
↧-* p q = ↧-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q)

------------------------------------------------------------------------
-- Raw bundles

*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  }

*-rawMonoid : RawMonoid 0ℓ 0ℓ
*-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  ; ε   = 1ℚ
  }

------------------------------------------------------------------------
-- Monomorphic to unnormalised _*_

toℚᵘ-homo-* : Homomorphic₂ toℚᵘ _*_ ℚᵘ._*_
toℚᵘ-homo-* p q with *-nf p q ℤ.≟ 0ℤ
... | yes nf[p,q]≡0 = *≡* (begin
  ↥ (p * q)     ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) eq ⟩
  0ℤ            ℤ.* (↧ p ℤ.* ↧ q) ≡⟨⟩
  0ℤ            ℤ.* ↧ (p * q)     ≡⟨ cong (ℤ._* ↧ (p * q)) (sym eq2) ⟩
  (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q)     ∎)
  where
  open ≡-Reasoning
  eq2 : ↥ p ℤ.* ↥ q ≡ 0ℤ
  eq2 = gcd[i,j]≡0⇒i≡0 (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q) nf[p,q]≡0

  eq : ↥ (p * q) ≡ 0ℤ
  eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) nf[p,q]≢0 (begin
  ↥ (p * q)     ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩
  ↥ (p * q)     ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩
  (↥ p ℤ.* ↥ q) ℤ.* (↧ p ℤ.* ↧ q)              ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩
  (↥ p ℤ.* ↥ q) ℤ.* (↧ (p * q) ℤ.* *-nf p q)   ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩
  (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q)  ℤ.* *-nf p q    ∎))
  where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup

toℚᵘ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℚᵘ.*-rawMagma toℚᵘ
toℚᵘ-isMagmaHomomorphism-* = record
  { isRelHomomorphism = toℚᵘ-isRelHomomorphism
  ; homo              = toℚᵘ-homo-*
  }

toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-rawMonoid ℚᵘ.*-rawMonoid toℚᵘ
toℚᵘ-isMonoidHomomorphism-* = record
  { isMagmaHomomorphism = toℚᵘ-isMagmaHomomorphism-*
  ; ε-homo              = ℚᵘ.≃-refl
  }

toℚᵘ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-rawMonoid ℚᵘ.*-rawMonoid toℚᵘ
toℚᵘ-isMonoidMonomorphism-* = record
  { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-*
  ; injective            = toℚᵘ-injective
  }

toℚᵘ-isRingHomomorphism-+-* : IsRingHomomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ
toℚᵘ-isRingHomomorphism-+-* = record
  { +-isGroupHomomorphism  = toℚᵘ-isGroupHomomorphism-+
  ; *-isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-*
  }

toℚᵘ-isRingMonomorphism-+-* : IsRingMonomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ
toℚᵘ-isRingMonomorphism-+-* = record
  { isRingHomomorphism = toℚᵘ-isRingHomomorphism-+-*
  ; injective          = toℚᵘ-injective
  }

------------------------------------------------------------------------
-- Algebraic properties

private
  module *-Monomorphism = RingMonomorphisms toℚᵘ-isRingMonomorphism-+-*

*-assoc : Associative _*_
*-assoc = *-Monomorphism.*-assoc ℚᵘ.*-isMagma ℚᵘ.*-assoc

*-comm : Commutative _*_
*-comm = *-Monomorphism.*-comm ℚᵘ.*-isMagma ℚᵘ.*-comm

*-identityˡ : LeftIdentity 1ℚ _*_
*-identityˡ = *-Monomorphism.*-identityˡ ℚᵘ.*-isMagma ℚᵘ.*-identityˡ

*-identityʳ : RightIdentity 1ℚ _*_
*-identityʳ = *-Monomorphism.*-identityʳ ℚᵘ.*-isMagma ℚᵘ.*-identityʳ

*-identity : Identity 1ℚ _*_
*-identity = *-identityˡ , *-identityʳ

*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ = *-Monomorphism.distribˡ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-distribˡ-+

*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ = *-Monomorphism.distribʳ ℚᵘ.+-0-isGroup ℚᵘ.*-isMagma ℚᵘ.*-distribʳ-+

*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

------------------------------------------------------------------------
-- Structures

*-isMagma : IsMagma _*_
*-isMagma = *-Monomorphism.*-isMagma ℚᵘ.*-isMagma

*-isSemigroup : IsSemigroup _*_
*-isSemigroup = *-Monomorphism.*-isSemigroup ℚᵘ.*-isSemigroup

*-1-isMonoid : IsMonoid _*_ 1ℚ
*-1-isMonoid = *-Monomorphism.*-isMonoid ℚᵘ.*-1-isMonoid

*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1ℚ
*-1-isCommutativeMonoid = *-Monomorphism.*-isCommutativeMonoid ℚᵘ.*-1-isCommutativeMonoid

+-*-isRing : IsRing _+_ _*_ -_ 0ℚ 1ℚ
+-*-isRing = *-Monomorphism.isRing ℚᵘ.+-*-isRing

------------------------------------------------------------------------
-- Packages

*-magma : Magma 0ℓ 0ℓ
*-magma = record
  { isMagma = *-isMagma
  }

*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
  { isSemigroup = *-isSemigroup
  }

*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
  { isMonoid = *-1-isMonoid
  }

*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
  { isCommutativeMonoid = *-1-isCommutativeMonoid
  }

+-*-ring : Ring 0ℓ 0ℓ
+-*-ring = record
  { isRing = +-*-isRing
  }

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

-- Version 1.0

≤-irrelevance = ≤-irrelevant
{-# WARNING_ON_USAGE ≤-irrelevance
"Warning: ≤-irrelevance was deprecated in v1.0.
Please use ≤-irrelevant instead."
#-}


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

module Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Dec where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Def
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Decidable.Logic

private
  variable p : Level

◇? : ∀ {P : A → Type p} → (∀ x → Dec (P x)) → (xs : 𝒦 A) → Dec (◇ P xs)
◇? {A = A} {P = P} P? = 𝒦-elim-prop (λ {xs} → isPropDec (isProp-◇ {P = P} {xs = xs})) (λ x xs → fn x xs (P? x)) (no (Poly⊥⇔Mono⊥ .fun))
  where
  fn : ∀ x xs → Dec (P x) → Dec (◇ P xs) → Dec (◇ P (x ∷ xs))
  fn x xs (yes Px) Pxs = yes ∣ inl Px ∣
  fn x xs (no ¬Px) (yes Pxs) = yes ∣ inr Pxs ∣
  fn x xs (no ¬Px) (no ¬Pxs) = no (refute-trunc (either′ ¬Px ¬Pxs))

ext: agda

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Relation.Binary.Core

module TreeSort.Impl2.Correctness.Order  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_)  where

open import BBSTree _≤_
open import BBSTree.Properties _≤_ trans≤
open import Data.List
open import Function using (_∘_)
open import List.Sorted _≤_
open import TreeSort.Impl2 _≤_ tot≤

theorem-treeSort-sorted : (xs : List A) → Sorted (flatten (treeSort xs))
theorem-treeSort-sorted = lemma-bbst-sorted ∘ treeSort

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue637 where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

infixl 60 _+_
_+_ : Nat → Nat → Nat
zero + n = n
suc m + n = suc (n + m)

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

`1 = suc zero
`2 = suc `1
`3 = suc `2
`4 = `2 + `2
`8 = `4 + `4
`16 = `8 + `8
`32 = `16 + `16
`50 = `32 + `16 + `2
`64 = `32 + `32
`100 = `64 + `32 + `4
`200 = `100 + `100
`400 = `200 + `200
`800 = `400 + `400
`1000 = `800 + `200
`2000 = `1000 + `1000
`4000 = `2000 + `2000

prf : `16 ≡ (`4 + (`4 + `8))
prf = refl

infixr 40 _∷_
data Vec : Nat → Set where
  [] : Vec zero
  _∷_ : ∀ {n} → Nat → Vec n → Vec (suc n)

fromN : ∀ {n} → Nat → Vec n
fromN {zero} _ = []
fromN {suc n} x = x ∷ fromN (suc x)

sum : ∀ {n} → Vec n → Nat
sum [] = zero
sum (n ∷ ns) = n + sum ns

prf₁ : sum (fromN {`100} `1) ≡ (`4000 + `1000 + `50)
prf₁ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module plfa-exercises.Practice3 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning using (_≡⟨⟩_; _≡⟨_⟩_; begin_; _∎)
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ; *-distribʳ-+; +-suc; *-suc; *-comm)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_; flip)
open import Level using (Level)
open import plfa.part1.Isomorphism using (_≃_; _⇔_)
--import Data.List.All using (All; []; _∷_)
open import Data.List using (List; []; _∷_; _++_; length; reverse; map; foldr; downFrom; foldl)
open import Axiom.Extensionality.Propositional using (Extensionality)
import Data.Nat.Solver as NatSolver
open import Data.Sum using (_⊎_; inj₁; inj₂)

-- Exercises from plfa Lists

map∘compose₀ : ∀ {A B C : Set} (f : A → B) (g : B → C) (xs : List A) → map (g ∘ f) xs ≡ (map g ∘ map f) xs
map∘compose₀ f g [] = refl
map∘compose₀ f g (x ∷ xs) = cong (g (f x) ∷_) (map∘compose₀ f g xs)

module _ (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′) where

  map∘compose : ∀ {A B C : Set}
                (f : A → B) (g : B → C)
              → map (g ∘ f) ≡ (map g ∘ map f)
  map∘compose f g = ext (map∘compose₀ f g)

map-++-distribute : ∀ {A B : Set}
                    (f : A → B) (xs ys : List A)
                  → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-distribute f []       ys = refl
map-++-distribute f (x ∷ xs) ys = cong (f x ∷_) (map-++-distribute f xs ys)

data Tree (A B : Set) : Set where
  leaf : A → Tree A B
  node : Tree A B → B → Tree A B → Tree A B

map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
map-Tree f g (leaf a) = leaf (f a)
map-Tree f g (node lt b rt) = node (map-Tree f g lt) (g b) (map-Tree f g rt)

--node (leaf 5) (3 ∷ []) (leaf 0)
--map-Tree suc (6 ∷_) (node (leaf 5) (3 ∷ []) (leaf 0))

product : List ℕ → ℕ
product = foldr _*_ 1

_ : product (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡ 24
_ = refl

sum : List ℕ → ℕ
sum = foldr _+_ 0

sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom zero = refl
sum-downFrom 1    = refl
sum-downFrom (suc (suc n))
  rewrite
--    sum (downFrom (suc (suc n))) * 2 ≡ suc (suc n) * (suc (suc n) ∸ 1)
--    suc (suc ((n + (n + foldr _+_ 0 (downFrom n))) * 2)) ≡ suc (n + suc (n + n * suc n))
      *-distribʳ-+ 2 n (foldr _+_ 0 (downFrom (suc n)))
--    suc (suc (n * 2 + (n + foldr _+_ 0 (downFrom n)) * 2)) ≡ suc (n + suc (n + n * suc n))
    | sum-downFrom (suc n)
--    suc (suc (n * 2 + (n + n * n))) ≡ suc (n + suc (n + n * suc n))
    | +-suc n (n + n * suc n)
--    suc (suc (n * 2 + (n + n * n))) ≡ suc (suc (n + (n + n * suc n)))
    | *-suc n n
--    suc (suc (n * 2 + (n + n * n))) ≡ suc (suc (n + (n + (n + n * n))))
    | *-comm n 2
--    suc (suc (n + (n + 0) + (n + n * n))) ≡ suc (suc (n + (n + (n + n * n))))
    | +-identityʳ n
--    suc (suc (n + n + (n + n * n))) ≡ suc (suc (n + (n + (n + n * n))))
    | +-assoc n n (n + n * n)
--    suc (suc (n + (n + (n + n * n)))) ≡ suc (suc (n + (n + (n + n * n))))
  = refl

sum-downFrom` : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom` zero = refl
sum-downFrom` 1    = refl
sum-downFrom` (suc (suc n))
  rewrite
--    sum (downFrom (suc (suc n))) * 2 ≡ suc (suc n) * (suc (suc n) ∸ 1)
--    suc (suc ((n + (n + foldr _+_ 0 (downFrom n))) * 2)) ≡ suc (n + suc (n + n * suc n))
      *-distribʳ-+ 2 n (foldr _+_ 0 (downFrom (suc n)))
--    suc (suc (n * 2 + (n + foldr _+_ 0 (downFrom n)) * 2)) ≡ suc (n + suc (n + n * suc n))
    | sum-downFrom` (suc n)
--    suc (suc (n * 2 + (n + n * n))) ≡ suc (n + suc (n + n * suc n))
  = simplified n
  where
    open NatSolver using (module +-*-Solver)
    open +-*-Solver using (solve; _:+_; _:*_; _:=_; con)

    simplified : ∀ n → 2 + (n * 2 + (n + n * n)) ≡ 1 + (n + (1 + (n + n * (1 + n))))
    simplified = solve 1 (λ n → con 2 :+ (n :* con 2 :+ (n :+ n :* n)) := con 1 :+ (n :+ (con 1 :+ (n :+ n :* (con 1 :+ n))))) refl

-- solve 1 (λ n → n :+ con 1 := con 1 :+ n) refl
--open NatSolver using (module +-*-Solver)
--open +-*-Solver using (solve; _:+_; _:*_; _:=_; con; Polynomial)
--
--lemma : ∀ x y → x + y * 1 + 3 ≡ 2 + 1 + y + x
--lemma = solve 2 (λ x y → x :+ y :* con 1 :+ con 3 := con 2 :+ con 1 :+ y :+ x) refl

record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where
  field
    assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
    identityˡ : ∀ (x : A) → e ⊗ x ≡ x
    identityʳ : ∀ (x : A) → x ⊗ e ≡ x

open IsMonoid

foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs : List A) (y : A) → foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ y
foldr-monoid _⊗_ e ⊗-monoid [] y =
  begin
    foldr _⊗_ y []
  ≡⟨⟩
    y
  ≡⟨ sym (identityˡ ⊗-monoid y) ⟩
    (e ⊗ y)
  ≡⟨⟩
    foldr _⊗_ e [] ⊗ y
  ∎
foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
  begin
    foldr _⊗_ y (x ∷ xs)
  ≡⟨⟩
    x ⊗ (foldr _⊗_ y xs)
  ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e ⊗-monoid xs y) ⟩
    x ⊗ (foldr _⊗_ e xs ⊗ y)
  ≡⟨ sym (assoc ⊗-monoid x (foldr _⊗_ e xs) y) ⟩
    (x ⊗ foldr _⊗_ e xs) ⊗ y
  ≡⟨⟩
    foldr _⊗_ e (x ∷ xs) ⊗ y
  ∎

--foldl : {A B : Set} (f : B → A → B) → B → List A → B
--foldl f b [] = b
--foldl f b (a ∷ as') = foldl f (f b a) as'

_ : foldl _∸_ 20 (4 ∷ 3 ∷ []) ≡ 13
_ =
 begin
  foldl _∸_ 20             (4 ∷ 3 ∷ []) ≡⟨⟩
  foldl _∸_ (20 ∸ 4)       (3 ∷ [])     ≡⟨⟩
  foldl _∸_ ((20 ∸ 4) ∸ 3) []           ≡⟨⟩
  (20 ∸ 4) ∸ 3                          ≡⟨⟩
  13
 ∎

_ : foldr _∸_ 20 (4 ∷ 3 ∷ []) ≡ 4
_ =
 begin
  foldr _∸_ 20 (4 ∷ 3 ∷ []) ≡⟨⟩
  4 ∸ foldr _∸_ 20 (3 ∷ []) ≡⟨⟩
  4 ∸ (3 ∸ foldr _∸_ 20 []) ≡⟨⟩
  4 ∸ (3 ∸ 20) ≡⟨⟩
  4 ∸ 0 ≡⟨⟩
  4
 ∎

foldl-monoid : {A : Set}
               (_⊗_ : A → A → A) (e : A)
             → IsMonoid _⊗_ e
             → ∀ (y : A) (xs : List A)
             → (y ⊗ foldl _⊗_ e xs) ≡ foldl _⊗_ y xs
foldl-monoid _⊗_ e monoid-⊗ y [] = identityʳ monoid-⊗ y
foldl-monoid _⊗_ e monoid-⊗ y (x ∷ xs) =
  begin
    y ⊗ foldl _⊗_ e (x ∷ xs)  ≡⟨⟩
    y ⊗ foldl _⊗_ (e ⊗ x) xs  ≡⟨ cong (λ exp → y ⊗ foldl _⊗_ exp xs) (identityˡ monoid-⊗ x) ⟩
    y ⊗ foldl _⊗_ x xs        ≡⟨ cong (y ⊗_) (sym (foldl-monoid _⊗_ e monoid-⊗ x xs)) ⟩
    y ⊗ (x ⊗ foldl _⊗_ e xs)  ≡⟨ sym (assoc monoid-⊗ y x (foldl _⊗_ e xs)) ⟩
    (y ⊗ x) ⊗ foldl _⊗_ e xs  ≡⟨ foldl-monoid _⊗_ e monoid-⊗ (y ⊗ x) xs ⟩
    foldl _⊗_ (y ⊗ x) xs      ≡⟨⟩
    foldl _⊗_ y (x ∷ xs)
  ∎

foldr-monoid-foldl₀ : ∀ {A : Set} {_⊗_ : A → A → A} {e : A}
                   → (xs : List A)
                   → IsMonoid _⊗_ e
                   → foldr _⊗_ e xs ≡ foldl _⊗_ e xs
foldr-monoid-foldl₀ [] _ = refl
foldr-monoid-foldl₀ {_} {_⊗_} {e} (x ∷ xs) monoid-⊗ =
  begin
    foldr _⊗_ e (x ∷ xs)   ≡⟨⟩
    x ⊗ foldr _⊗_ e xs     ≡⟨ cong (x ⊗_) (foldr-monoid-foldl₀ xs monoid-⊗) ⟩
    x ⊗ foldl _⊗_ e xs     ≡⟨ foldl-monoid _⊗_ e monoid-⊗ x xs ⟩
    foldl _⊗_ x xs         ≡⟨ cong (λ exp → foldl _⊗_ exp xs) (sym (identityˡ monoid-⊗ x)) ⟩
    foldl _⊗_ (e ⊗ x) xs   ≡⟨⟩
    foldl _⊗_ e (x ∷ xs)
  ∎

module _ (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′) where
  foldr-monoid-foldl : ∀ {A : Set} {_⊗_ : A → A → A} {e : A}
                     → IsMonoid _⊗_ e
                     → foldr _⊗_ e ≡ foldl _⊗_ e
  foldr-monoid-foldl monoid-⊗ = ext (λ xs → foldr-monoid-foldl₀ xs monoid-⊗)

data All {A : Set} (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)

pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

_ : All (_≤ 2) [ 0 , 1 , 2 ]  -- These brackes desugar to ∷ and [] for List definition
_ = [ z≤n , s≤s z≤n , s≤s (s≤s z≤n) ]  -- ∷ and [] from All constructors

++-assoc : ∀ {A : Set} (xs ys zs : List A)
  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs =
  begin
    ((x ∷ xs) ++ ys) ++ zs ≡⟨⟩
    x ∷ (xs ++ ys) ++ zs   ≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩
    x ∷ xs ++ ys ++ zs     ≡⟨⟩
    (x ∷ xs) ++ ys ++ zs
  ∎

length-++ : ∀ {A : Set} (xs ys : List A)
  → length (xs ++ ys) ≡ length xs + length ys
length-++ [] ys = refl
length-++ (x ∷ xs) ys =
  begin
    length ((x ∷ xs) ++ ys)      ≡⟨⟩
    suc (length (xs ++ ys))      ≡⟨ cong suc (length-++ xs ys) ⟩
    suc (length xs + length ys)  ≡⟨⟩
    suc (length xs) + length ys  ≡⟨⟩
    length (x ∷ xs) + length ys
  ∎

++-[] : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-[] [] = refl
++-[] (x ∷ xs) = cong (x ∷_) (++-[] xs)

data Any {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} → P x → Any P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)

infix 4 _∈_ _∉_

_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∉ xs = ¬ (x ∈ xs)

_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
_ = here refl
--_ = there (there (here refl))

---- Left as exercise for another day
--reverse-inv : ∀ {A : Set} (x : A) (xs : List A)
--  → reverse (x ∷ xs) ≡ reverse xs ++ [ x ]
--reverse-inv _ [] = refl
--reverse-inv y (x ∷ xs) =
--  begin
--    reverse (y ∷ x ∷ xs)  ≡⟨⟩
--    foldl _∷`_ [ x , y ] xs  ≡⟨ ? ⟩ -- LEFT FOR LATER
--    foldl _∷`_ [ x ] xs ++ [ y ]  ≡⟨⟩
--    reverse (x ∷ xs) ++ [ y ]
--  ∎
---- λ y x xs →  ≡
---- λ y x xs → foldl (λ y₁ x₁ → x₁ ∷ y₁) [ x , y ] xs ≡ foldl (λ y₁ x₁ → x₁ ∷ y₁) [ x ] xs ++ [ y ]
--  where
--  _∷`_ = flip _∷_
--
--reverse-++-distrib : ∀ {A : Set} (xs ys : List A)
--  → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
--reverse-++-distrib [] ys = sym (++-[] (reverse ys))
--reverse-++-distrib (x ∷ xs) ys =
--  begin
--    reverse ((x ∷ xs) ++ ys)                  ≡⟨⟩
--    reverse (x ∷ (xs ++ ys))                  ≡⟨ reverse-inv x (xs ++ ys) ⟩
--    reverse (xs ++ ys) ++ [ x ]               ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
--    (reverse ys ++ reverse xs) ++ [ x ]       ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
--    reverse ys ++ (reverse xs ++ [ x ])       ≡⟨ sym (cong (reverse ys ++_) (reverse-inv x xs)) ⟩
--    reverse ys ++ reverse (x ∷ xs)
--  ∎
--    --foldl _∷`_ [ x ] (xs ++ ys)               ≡⟨ ? ⟩
--    --foldl _∷`_ [] ys ++ foldl _∷`_ [ x ] xs   ≡⟨⟩

exercise-823→ : ∀ {A : Set} {z : A} (xs ys : List A)
              → z ∈ (xs ++ ys) → (z ∈ xs) ⊎ (z ∈ ys)
exercise-823→ []       [] ()
exercise-823→ []       _  z∈[]++ys         = inj₂ z∈[]++ys
exercise-823→ (_ ∷ _)  _  (here refl)      = inj₁ (here refl)
exercise-823→ (x ∷ xs) ys (there z∈xs++ys) with exercise-823→ xs ys z∈xs++ys
...                                       | inj₁ z∈xs = inj₁ (there z∈xs)
...                                       | inj₂ z∈ys = inj₂ z∈ys

exercise-823← : ∀ {A : Set} {z : A} (xs ys : List A)
             → (z ∈ xs) ⊎ (z ∈ ys) → z ∈ (xs ++ ys)
exercise-823← []       _  (inj₁ ())
exercise-823← []       _  (inj₂ z∈ys) = z∈ys
exercise-823← (_ ∷ _)  [] (inj₂ ())
exercise-823← (_ ∷ _)  _  (inj₁ (here z∈xs)) = here z∈xs
exercise-823← (x ∷ xs) ys (inj₁ (there z∈xs)) with exercise-823← xs ys (inj₁ z∈xs)
...                                           | z∈xs++ys = there z∈xs++ys
exercise-823← (_ ∷ xs) ys (inj₂ z∈y∷ys) with exercise-823← xs ys (inj₂ z∈y∷ys)
...                                     | z∈xs++y∷ys = there z∈xs++y∷ys

exercise-823 : ∀ {A : Set} {z : A} (xs ys : List A)
             → (z ∈ xs ++ ys) ⇔ (z ∈ xs ⊎ z ∈ ys)
exercise-823 xs ys = record { to = exercise-823→ xs ys ; from = exercise-823← xs ys }


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

-- The 'Trivial' instance, with a single arrow between objects

module Categories.Theory.Lawvere.Instance.Triv where

open import Data.Nat using (_*_)
open import Data.Unit.Polymorphic using (⊤; tt)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; isEquivalence)

open import Categories.Theory.Lawvere using (LawvereTheory)

Triv : ∀ {ℓ} → LawvereTheory ℓ ℓ
Triv = record
  { L = record
          { _⇒_ = λ _ _ → ⊤
          ; _≈_ = _≡_
          ; assoc = refl
          ; sym-assoc = refl
          ; identityˡ = refl
          ; identityʳ = refl
          ; identity² = refl
          ; equiv = isEquivalence
          ; ∘-resp-≈ = λ _ _ → refl
          }
  ; T = record
    { terminal = record { ⊤ = 0 ; ⊤-is-terminal = record { ! = tt ; !-unique = λ _ → refl } }
    ; products = record
      { product = λ {m} {n} → record
        { A×B = m * n
        ; project₁ = refl
        ; project₂ = refl
        ; unique = λ _ _ → refl
        }
      }
    }
  ; I = record
    { F₁ = λ _ → tt
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = λ _ → refl
    }
  ; CartF = record
    { F-resp-⊤ = record { ! = tt ; !-unique = λ _ → refl }
    ; F-resp-× = record { ⟨_,_⟩ = λ _ _ → tt ; project₁ = refl ; project₂ = refl ; unique = λ _ _ → refl }
    }
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

   Copyright (c) 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 LibraBFT.Prelude
open import LibraBFT.Lemmas
-- TODO-2: The following import should be eliminated and replaced
-- with the necessary module parameters (PK and MetaHonestPK)
open import LibraBFT.Base.PKCS

-- This module brings in the base types used through libra
-- and those necessary for the abstract model.
module LibraBFT.Abstract.Types.EpochConfig
  (UID    : Set)
  (NodeId : Set)
  where

  open import LibraBFT.Base.Types

  ℓ-EC : Level
  ℓ-EC = ℓ+1 0ℓ

  -- An epoch-configuration carries only simple data about the epoch; the complicated
  -- parts will be provided by the System, defined below.
  --
  -- The reason for the separation is that we should be able to provide
  -- an EpochConfig from a single peer state.
  record EpochConfig : Set ℓ-EC where
    constructor EpochConfig∙new
    field
      genesisUID : UID
      epoch      : Epoch
      authorsN  : ℕ

    -- The set of members of this epoch.
    Member : Set
    Member = Fin authorsN

    -- There is a partial isomorphism between NodeIds and the
    -- authors participating in this epoch.
    field
      toNodeId  : Member → NodeId
      isMember? : NodeId → Maybe Member

      nodeid-author-id : ∀{α}     → isMember? (toNodeId α) ≡ just α
      author-nodeid-id : ∀{nid α} → isMember? nid ≡ just α
                                  → toNodeId α ≡ nid

      getPubKey : Member → PK

      PK-inj : ∀ {m1 m2} → getPubKey m1 ≡ getPubKey m2 → m1 ≡ m2

      IsQuorum : List Member → Set

      bft-assumption : ∀ {xs ys}
                     → IsQuorum xs → IsQuorum ys
                     → ∃[ α ] (α ∈ xs × α ∈ ys × Meta-Honest-PK (getPubKey α))

  open EpochConfig

  PK-inj-same-ECs : ∀ {𝓔₁ 𝓔₂ : EpochConfig}{mbr₁ mbr₂}
                  → 𝓔₁ ≡ 𝓔₂
                  → getPubKey 𝓔₁ mbr₁ ≡ getPubKey 𝓔₂ mbr₂
                  → toNodeId 𝓔₁ mbr₁ ≡ toNodeId 𝓔₂ mbr₂
  PK-inj-same-ECs {𝓔₁} refl pks≡ = cong (toNodeId 𝓔₁) (PK-inj 𝓔₁ pks≡)

  module _ (ec : EpochConfig) where
    NodeId-PK-OK : PK → NodeId → Set
    NodeId-PK-OK pk pid = ∃[ m ] (toNodeId ec m ≡ pid × getPubKey ec m ≡ pk)

    NodeId-PK-OK-injective : ∀ {pk pid1 pid2}
                           → NodeId-PK-OK pk pid1
                           → NodeId-PK-OK pk pid2
                           → pid1 ≡ pid2
    NodeId-PK-OK-injective (m1 , pid1 , pk1) (m2 , pid2 , pk2)
       rewrite PK-inj ec (trans pk1 (sym pk2)) = trans (sym pid1) pid2

  module WithAbsVote (𝓔 : EpochConfig) where
    -- The abstract model is connected to the implementaton by means of
    -- 'VoteEvidence'. The record module will be parameterized by a
    -- v of type 'VoteEvidence 𝓔 UID'; this v will provide evidence
    -- that a given author voted for a given block (identified by the UID)
    -- on the specified round.
    --
    -- When it comes time to instantiate the v above concretely, it will
    -- be something that states that we have a signature from the specified
    -- author voting for the specified block.
    record AbsVoteData : Set where
      constructor AbsVoteData∙new
      field
        abs-vRound     : Round
        abs-vMember    : EpochConfig.Member 𝓔
        abs-vBlockUID  : UID
    open AbsVoteData public

    AbsVoteData-η : ∀ {r1 r2 : Round} {m1 m2 : EpochConfig.Member 𝓔} {b1 b2 : UID}
                  → r1 ≡ r2
                  → m1 ≡ m2
                  → b1 ≡ b2
                  → AbsVoteData∙new r1 m1 b1 ≡ AbsVoteData∙new r2 m2 b2
    AbsVoteData-η refl refl refl = refl

    VoteEvidence : Set₁
    VoteEvidence = AbsVoteData → Set

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Agda.Builtin.Float where

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Int
open import Agda.Builtin.String

postulate Float : Set
{-# BUILTIN FLOAT Float #-}

primitive
  primFloatEquality : Float → Float → Bool
  primFloatLess     : Float → Float → Bool
  primNatToFloat    : Nat → Float
  primFloatPlus     : Float → Float → Float
  primFloatMinus    : Float → Float → Float
  primFloatTimes    : Float → Float → Float
  primFloatDiv      : Float → Float → Float
  primFloatSqrt     : Float → Float
  primRound         : Float → Int
  primFloor         : Float → Int
  primCeiling       : Float → Int
  primExp           : Float → Float
  primLog           : Float → Float
  primSin           : Float → Float
  primShowFloat     : Float → String


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive "natural" numbers
------------------------------------------------------------------------

{-# OPTIONS --without-K --guardedness --sized-types #-}

module Codata.Musical.Conat where

open import Codata.Musical.Notation
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- The type

data Coℕ : Set where
  zero : Coℕ
  suc  : (n : ∞ Coℕ) → Coℕ

module Coℕ-injective where

 suc-injective : ∀ {m n} → (Coℕ ∋ suc m) ≡ suc n → m ≡ n
 suc-injective P.refl = P.refl

------------------------------------------------------------------------
-- Some operations

pred : Coℕ → Coℕ
pred zero    = zero
pred (suc n) = ♭ n

fromℕ : ℕ → Coℕ
fromℕ zero    = zero
fromℕ (suc n) = suc (♯ fromℕ n)

fromℕ-injective : ∀ {m n} → fromℕ m ≡ fromℕ n → m ≡ n
fromℕ-injective {zero}  {zero}  eq = P.refl
fromℕ-injective {zero}  {suc n} ()
fromℕ-injective {suc m} {zero}  ()
fromℕ-injective {suc m} {suc n} eq = P.cong suc (fromℕ-injective (P.cong pred eq))

∞ℕ : Coℕ
∞ℕ = suc (♯ ∞ℕ)

infixl 6 _+_

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

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

data _≈_ : Coℕ → Coℕ → Set where
  zero :                                 zero  ≈ zero
  suc  : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n

module ≈-injective where

 suc-injective : ∀ {m n p q} → (suc m ≈ suc n ∋ suc p) ≡ suc q → p ≡ q
 suc-injective P.refl = P.refl

setoid : Setoid _ _
setoid = record
  { Carrier       = Coℕ
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {zero}  = zero
  refl {suc n} = suc (♯ refl)

  sym : Symmetric _≈_
  sym zero      = zero
  sym (suc m≈n) = suc (♯ sym (♭ m≈n))

  trans : Transitive _≈_
  trans zero      zero      = zero
  trans (suc m≈n) (suc n≈k) = suc (♯ trans (♭ m≈n) (♭ n≈k))

------------------------------------------------------------------------
-- Legacy

import Codata.Conat as C
open import Codata.Thunk
import Size

fromMusical : ∀ {i} → Coℕ → C.Conat i
fromMusical zero    = C.zero
fromMusical (suc n) = C.suc λ where .force → fromMusical (♭ n)

toMusical : C.Conat Size.∞ → Coℕ
toMusical C.zero    = zero
toMusical (C.suc n) = suc (♯ toMusical (n .force))


text:
module index where

-- A formalisation of Haskell B. Curry’s thesis Grundlagen der Kombinatorischen
-- Logik. See <https://www.jstor.org/stable/2370619> (part 1) and
-- <https://www.jstor.org/stable/2370716> (part 2).
import CombinatoryLogic.Equality
import CombinatoryLogic.Forest
import CombinatoryLogic.Semantics
import CombinatoryLogic.Syntax

-- A formalisation of the theory and problems presented in To Mock a Mockingbird
-- by Raymond Smullyan.
import Mockingbird.Forest
import Mockingbird.Forest.Base
import Mockingbird.Forest.Birds
import Mockingbird.Forest.Combination
import Mockingbird.Forest.Combination.Base
import Mockingbird.Forest.Combination.Properties
import Mockingbird.Forest.Combination.Vec
import Mockingbird.Forest.Combination.Vec.Base
import Mockingbird.Forest.Combination.Vec.Properties
import Mockingbird.Forest.Extensionality
import Mockingbird.Problems.Chapter09
import Mockingbird.Problems.Chapter10
import Mockingbird.Problems.Chapter11
import Mockingbird.Problems.Chapter12
import Mockingbird.Problems.Chapter13
import Mockingbird.Problems.Chapter14
import Mockingbird.Problems.Chapter15
import Mockingbird.Problems.Chapter16
import Mockingbird.Problems.Chapter17
import Mockingbird.Problems.Chapter18
import Mockingbird.Problems.Chapter19
import Mockingbird.Problems.Chapter20

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Membership predicate for fresh lists
------------------------------------------------------------------------

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

open import Relation.Binary

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

open import Level using (Level; _⊔_)
open import Data.List.Fresh
open import Data.List.Fresh.Relation.Unary.Any as Any using (Any)
open import Relation.Nullary

open Setoid S renaming (Carrier to A)

private
  variable
    r : Level

_∈_ : {R : Rel A r} → A → List# A R → Set _
x ∈ xs = Any (x ≈_) xs

_∉_ : {R : Rel A r} → A → List# A R → Set _
x ∉ xs = ¬ (x ∈ xs)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bijections on finite sets (i.e. permutations).
------------------------------------------------------------------------

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

module Data.Fin.Permutation where

open import Data.Empty using (⊥-elim)
open import Data.Fin
open import Data.Fin.Properties
import Data.Fin.Permutation.Components as PC
open import Data.Nat using (ℕ; suc; zero)
open import Data.Product using (proj₂)
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function.Equality using (_⟨$⟩_)
open import Function using (_∘_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; trans; sym; →-to-⟶; cong; cong₂)
open P.≡-Reasoning

------------------------------------------------------------------------
-- Types

-- A bijection between finite sets of potentially different sizes.
-- There only exist inhabitants of this type if in fact m = n, however
-- it is often easier to prove the existence of a bijection without
-- first proving that the sets have the same size. Indeed such a
-- bijection is a useful way to prove that the sets are in fact the same
-- size. See '↔-≡' below.

Permutation : ℕ → ℕ → Set
Permutation m n = Fin m ↔ Fin n

Permutation′ : ℕ → Set
Permutation′ n = Permutation n n

------------------------------------------------------------------------
-- Helper functions

permutation : ∀ {m n} (f : Fin m → Fin n) (g : Fin n → Fin m) →
              (→-to-⟶ g) InverseOf (→-to-⟶ f) → Permutation m n
permutation f g inv = record
  { to         = →-to-⟶ f
  ; from       = →-to-⟶ g
  ; inverse-of = inv
  }

_⟨$⟩ʳ_ : ∀ {m n} → Permutation m n → Fin m → Fin n
_⟨$⟩ʳ_ = _⟨$⟩_ ∘ Inverse.to

_⟨$⟩ˡ_ : ∀ {m n} → Permutation m n → Fin n → Fin m
_⟨$⟩ˡ_ = _⟨$⟩_ ∘ Inverse.from

inverseˡ : ∀ {m n} (π : Permutation m n) {i} → π ⟨$⟩ˡ (π ⟨$⟩ʳ i) ≡ i
inverseˡ π = Inverse.left-inverse-of π _

inverseʳ : ∀ {m n} (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡ i
inverseʳ π = Inverse.right-inverse-of π _

------------------------------------------------------------------------
-- Example permutations

-- Identity

id : ∀ {n} → Permutation′ n
id = Inverse.id

-- Transpose two indices

transpose : ∀ {n} → Fin n → Fin n → Permutation′ n
transpose i j = permutation (PC.transpose i j) (PC.transpose j i)
  record
  { left-inverse-of  = λ _ → PC.transpose-inverse _ _
  ; right-inverse-of = λ _ → PC.transpose-inverse _ _
  }

-- Reverse the order of indices

reverse : ∀ {n} → Permutation′ n
reverse = permutation PC.reverse PC.reverse
  record
  { left-inverse-of  = PC.reverse-involutive
  ; right-inverse-of = PC.reverse-involutive
  }

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

-- Composition

_∘ₚ_ : ∀ {m n o} → Permutation m n → Permutation n o → Permutation m o
π₁ ∘ₚ π₂ = π₂ Inverse.∘ π₁

-- Flip

flip : ∀ {m n} → Permutation m n → Permutation n m
flip = Inverse.sym

-- Element removal
--
-- `remove k [0 ↦ i₀, …, k ↦ iₖ, …, n ↦ iₙ]` yields
--
-- [0 ↦ i₀, …, k-1 ↦ iₖ₋₁, k ↦ iₖ₊₁, k+1 ↦ iₖ₊₂, …, n-1 ↦ iₙ]

remove : ∀ {m n} → Fin (suc m) →
         Permutation (suc m) (suc n) → Permutation m n
remove {m} {n} i π = permutation to from
  record
  { left-inverse-of  = left-inverse-of
  ; right-inverse-of = right-inverse-of
  }
  where
  πʳ = π ⟨$⟩ʳ_
  πˡ = π ⟨$⟩ˡ_

  permute-≢ : ∀ {i j} → i ≢ j → πʳ i ≢ πʳ j
  permute-≢ p = p ∘ (Inverse.injective π)

  to-punchOut : ∀ {j : Fin m} → πʳ i ≢ πʳ (punchIn i j)
  to-punchOut = permute-≢ (punchInᵢ≢i _ _ ∘ sym)

  from-punchOut : ∀ {j : Fin n} → i ≢ πˡ (punchIn (πʳ i) j)
  from-punchOut {j} p = punchInᵢ≢i (πʳ i) j (sym (begin
    πʳ i                        ≡⟨ cong πʳ p ⟩
    πʳ (πˡ (punchIn (πʳ i) j))  ≡⟨ inverseʳ π ⟩
    punchIn (πʳ i) j            ∎))

  to : Fin m → Fin n
  to j = punchOut (to-punchOut {j})

  from : Fin n → Fin m
  from j = punchOut {j = πˡ (punchIn (πʳ i) j)} from-punchOut

  left-inverse-of : ∀ j → from (to j) ≡ j
  left-inverse-of j = begin
    from (to j)                                                      ≡⟨⟩
    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut {i = πʳ i} _)) ⟩
    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _  ≡⟨ punchOut-cong i (inverseˡ π) ⟩
    punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
    j                                                                ∎

  right-inverse-of : ∀ j → to (from j) ≡ j
  right-inverse-of j = begin
    to (from j)                                                       ≡⟨⟩
    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut {i = i} _)) ⟩
    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
    j                                                                 ∎

------------------------------------------------------------------------
-- Other properties

module _ {m n} (π : Permutation (suc m) (suc n)) where
  private
    πʳ = π ⟨$⟩ʳ_
    πˡ = π ⟨$⟩ˡ_

  punchIn-permute : ∀ i j → πʳ (punchIn i j) ≡ punchIn (πʳ i) (remove i π ⟨$⟩ʳ j)
  punchIn-permute i j = begin
    πʳ (punchIn i j)                                           ≡⟨ sym (punchIn-punchOut {i = πʳ i} _) ⟩
    punchIn (πʳ i) (punchOut {i = πʳ i} {πʳ (punchIn i j)} _)  ≡⟨⟩
    punchIn (πʳ i) (remove i π ⟨$⟩ʳ j)                         ∎

  punchIn-permute′ : ∀ i j → πʳ (punchIn (πˡ i) j) ≡ punchIn i (remove (πˡ i) π ⟨$⟩ʳ j)
  punchIn-permute′ i j = begin
    πʳ (punchIn (πˡ i) j)                         ≡⟨ punchIn-permute _ _ ⟩
    punchIn (πʳ (πˡ i)) (remove (πˡ i) π ⟨$⟩ʳ j)  ≡⟨ cong₂ punchIn (inverseʳ π) refl ⟩
    punchIn i (remove (πˡ i) π ⟨$⟩ʳ j)            ∎

↔⇒≡ : ∀ {m n} → Permutation m n → m ≡ n
↔⇒≡ {zero}  {zero}  π = refl
↔⇒≡ {zero}  {suc n} π = contradiction (π ⟨$⟩ˡ zero) ¬Fin0
↔⇒≡ {suc m} {zero}  π = contradiction (π ⟨$⟩ʳ zero) ¬Fin0
↔⇒≡ {suc m} {suc n} π = cong suc (↔⇒≡ (remove zero π))

fromPermutation : ∀ {m n} → Permutation m n → Permutation′ m
fromPermutation π = P.subst (Permutation _) (sym (↔⇒≡ π)) π

refute : ∀ {m n} → m ≢ n → ¬ Permutation m n
refute m≢n π = contradiction (↔⇒≡ π) m≢n


text:
-- Andreas, 2016-01-27
-- After complaints of Wolfram Kahl and Aaron Stump
-- we decided it is imported to keep the rewrite behavior
-- that does not rewrite in rewrite terms.

open import Common.Equality

test : ∀{A : Set}{a : A}{f : A → A} (p : f a ≡ a) → f (f a) ≡ a
test p rewrite p = p

-- rewrite should not happen in p itself,
-- otherwise we get  p : a ≡ a  which is useless.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Morphism where

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

open import Prelude
open import Structure

module _ {A B : Set} (σᴬ : Struct A) (σᴮ : Struct B) where
  open Struct σᴬ renaming (ℜ to ℜᴬ ; 𝔉 to 𝔉ᴬ)
  open Struct σᴮ renaming (ℜ to ℜᴮ ; 𝔉 to 𝔉ᴮ)

  record Hom : Set where
    field
      f : A → B
      ℜ-f : {n : ℕ} → (aⁿ : A ^ n) → ℜᴬ aⁿ → ℜᴮ (𝔉ⁿ f n aⁿ)
      𝔉-f : {n : ℕ} → (aⁿ : A ^ n) → f (𝔉ᴬ aⁿ) ≡ 𝔉ᴮ (𝔉ⁿ f n aⁿ)

  record Embed : Set where
    field
      h : Hom
    open Hom h
    field
      f-inj : ∀ {x y} → f x ≡ f y → x ≡ y
      ℜ-f' : {n : ℕ} → (aⁿ : A ^ n) → ℜᴮ (𝔉ⁿ f n aⁿ) → ℜᴬ aⁿ

  record Iso : Set where
    field
      e : Embed
    open Embed e
    open Hom h
    field
      g : B → A
      g-inj : ∀ {x y} → g x ≡ g y → x ≡ y
      f-g : ∀ {x} → f (g x) ≡ x
      g-f : ∀ {x} → g (f x) ≡ x

module _ {A : Set} (σᴬ : Struct A) where
  Endo : Set
  Endo = Hom σᴬ σᴬ

  Auto : Set
  Auto = Iso σᴬ σᴬ

module Examples {A B : Set} (σᴬ : Struct A) (σᴮ : Struct B) (h : Hom σᴬ σᴮ) where
  open Struct σᴬ renaming (ℜ to ℜᴬ ; 𝔉 to 𝔉ᴬ)
  open Struct σᴮ renaming (ℜ to ℜᴮ ; 𝔉 to 𝔉ᴮ)
  open Hom h

  hrel : A → A → Set
  hrel x y = f x ≡ f y

  open import Relation.Binary

  hrel-equiv : IsEquivalence hrel
  hrel-equiv = record { refl = refl ; sym = sym ; trans = trans }

  module _ {x y : A} where
    hrel-cong : hrel x y → hrel (𝔉ᴬ (x , tt)) (𝔉ᴬ (y , tt))
    hrel-cong p = trans (𝔉-f (x , tt)) (sym (trans (𝔉-f (y , tt)) (sym (cong (λ b → 𝔉ᴮ (b , tt)) p))))

max_stars_repo_name: vikraman/agda-structures

max_issues_repo_name: vikraman/agda-structures

max_forks_repo_name: vikraman/agda-structures


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

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

module Numbers.Primes.IntegerFactorisation where
open TotalOrder ℕTotalOrder

-- Represent a factorisation into increasing factors
-- Note that 0 cannot be expressed this way.
record factorisationNonunit (minFactor : ℕ) (a : ℕ) : Set where
  inductive
  field
    1<a : 1 <N a
    firstFactor : ℕ
    firstFactorNontrivial : 1 <N firstFactor
    firstFactorBiggerMin : minFactor ≤N firstFactor
    firstFactorDivision : divisionAlgResult firstFactor a
    firstFactorDivides : divisionAlgResult.rem firstFactorDivision ≡ 0
    firstFactorPrime : Prime firstFactor
    otherFactorsNumber : ℕ
    otherFactors : ((divisionAlgResult.quot firstFactorDivision ≡ 1) && (otherFactorsNumber ≡ 0)) || (((1 <N divisionAlgResult.quot firstFactorDivision) && (factorisationNonunit firstFactor (divisionAlgResult.quot firstFactorDivision))))

private
  lemma : (p : ℕ) → p *N 1 +N 0 ≡ p
  lemma p rewrite Semiring.sumZeroRight ℕSemiring (p *N 1) | Semiring.productOneRight ℕSemiring p = refl

  lemma' : {a b : ℕ} → a *N zero +N 0 ≡ b → b ≡ zero
  lemma' {a} {b} pr rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | Semiring.productZeroRight ℕSemiring a = equalityCommutative pr

primeFactorisation : {p : ℕ} → (pr : Prime p) → factorisationNonunit 1 p
primeFactorisation {p} record { p>1 = p>1 ; pr = pr } = record {11 ; firstFactor = p ; firstFactorNontrivial = p>1 ; firstFactorBiggerMin = inl p>1 ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = lemma p  ; remIsSmall = zeroIsValidRem p ; quotSmall = inl (TotalOrder.<Transitive ℕTotalOrder (le zero refl) p>1) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = p>1 ; pr = pr} ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
  where
    proof : (s : ℕ) → s *N 1 +N 0 ≡ s
    proof s rewrite Semiring.sumZeroRight ℕSemiring (s *N 1) | multiplicationNIsCommutative s 1 | Semiring.sumZeroRight ℕSemiring s = refl

twoAsFact : factorisationNonunit 2 2
factorisationNonunit.1<a twoAsFact = succPreservesInequality (succIsPositive 0)
factorisationNonunit.firstFactor twoAsFact = 2
factorisationNonunit.firstFactorNontrivial twoAsFact = succPreservesInequality (succIsPositive 0)
factorisationNonunit.firstFactorBiggerMin twoAsFact = inr refl
factorisationNonunit.firstFactorDivision twoAsFact = record { quot = 1 ; rem = 0 ; remIsSmall = zeroIsValidRem 2 ; pr = refl ; quotSmall = inl (le 1 refl) }
factorisationNonunit.firstFactorDivides twoAsFact = refl
factorisationNonunit.firstFactorPrime twoAsFact = twoIsPrime
factorisationNonunit.otherFactorsNumber twoAsFact = 0
factorisationNonunit.otherFactors twoAsFact = inl record { fst = refl ; snd = refl }

fourFact : factorisationNonunit 1 4
factorisationNonunit.1<a fourFact = succPreservesInequality (succIsPositive 2)
factorisationNonunit.firstFactor fourFact = 2
factorisationNonunit.firstFactorNontrivial fourFact = succPreservesInequality (succIsPositive 0)
factorisationNonunit.firstFactorBiggerMin fourFact = inl (succPreservesInequality (succIsPositive 0))
factorisationNonunit.firstFactorDivision fourFact = record { quot = 2 ; rem = 0 ; remIsSmall = zeroIsValidRem 2 ; pr = refl ; quotSmall = inl (le 1 refl) }
factorisationNonunit.firstFactorDivides fourFact = refl
factorisationNonunit.firstFactorPrime fourFact = twoIsPrime
factorisationNonunit.otherFactorsNumber fourFact = 1
factorisationNonunit.otherFactors fourFact = inr record { fst = succPreservesInequality (succIsPositive 0) ; snd = twoAsFact }

lessLemma : {y : ℕ} → (1 <N y) → (zero <N y)
lessLemma {.(succ (x +N 1))} (le x refl) = succIsPositive (x +N 1)

canReduceFactorBound : {a i j : ℕ} → factorisationNonunit i a → j <N i → factorisationNonunit j a
canReduceFactorBound {a} {i} {j} record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inl ff<i ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors } j<i = record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inl (lessTransitive j<i ff<i) ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors }
canReduceFactorBound {a} {i} {j} record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inr ff=i ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors } j<i = record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = inl (identityOfIndiscernablesRight _<N_ j<i ff=i) ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors }

canReduceFactorBound' : {a i j : ℕ} → factorisationNonunit i a → j ≤N i → factorisationNonunit j a
canReduceFactorBound' {a} {i} {j} factA (inl x) = canReduceFactorBound factA x
canReduceFactorBound' {a} {i} {.i} factA (inr refl) = factA

canIncreaseFactorBound : {a i : ℕ} → (fact : factorisationNonunit 1 a) → (∀ x → 1 <N x → x <N i → x ∣ a → False) → (i ≤N factorisationNonunit.firstFactor fact) → factorisationNonunit i a
canIncreaseFactorBound {a} {i} record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors } noSmaller iSmallEnough = record { 1<a = 11 firstFactorPrime ; firstFactorBiggerMin = iSmallEnough ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = otherFactors }

-- Get the smallest prime factor of the number
everyNumberHasAPrimeFactor : {a : ℕ} → (1 <N a) → Sg ℕ (λ i → ((i ∣ a) && (1 <N i)) && ((Prime i) && (∀ x → x <N i → 1 <N x → x ∣ a → False)))
everyNumberHasAPrimeFactor {a} 1<a with compositeOrPrime a 1<a
everyNumberHasAPrimeFactor {a} 11 = n>1 ; divisor = divisor ; dividesN = dividesN ; divisorLessN = divisorLessN ; divisorNot1 = divisorNot1 ; divisorPrime = divisorPrime ; noSmallerDivisors = noSmallerDivisors } = ( divisor , record { fst = record { fst = dividesN ; snd = divisorNot1 } ; snd = record { fst = divisorPrime ; snd = noSmallerDivisors } } )
everyNumberHasAPrimeFactor {a} 1<a | inr x = (a , record { fst = record { fst = aDivA a ; snd = 1<a } ; snd = record { fst = x ; snd = λ y y<a 1<y y|a → irreflexive (<WellDefined (equalityCommutative (Prime.pr x y|a y<a (lessLemma 1<y))) refl 1<y) }} )

lemma2 : {a b c : ℕ} → 1 <N a → 0 <N b → a *N b +N 0 ≡ c → b <N c
lemma2 {zero} {b} {c} 1<a _ pr = exFalso (zeroNeverGreater 1<a)
lemma2 {succ zero} {b} {c} 1<a _ pr = exFalso (lessIrreflexive 1<a)
lemma2 {succ (succ a)} {zero} {zero} 1<a t pr = exFalso (lessIrreflexive t)
lemma2 {succ (succ a)} {zero} {succ c} 1<a t pr = succIsPositive c
lemma2 {succ (succ a)} {succ b} {c} 1<a t pr = le (b +N (a *N succ b)) go
  where
    assocLemm : (a b c : ℕ) → (a +N b) +N c ≡ (a +N c) +N b
    assocLemm a b c rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) | Semiring.commutative ℕSemiring b c | Semiring.+Associative ℕSemiring a c b = refl
    go : succ ((b +N a *N succ b) +N succ b) ≡ c
    go rewrite Semiring.sumZeroRight ℕSemiring (succ (b +N succ (b +N a *N succ b))) | equalityCommutative (assocLemm b (succ b) (a *N succ b)) | Semiring.+Associative ℕSemiring b (succ b) (a *N succ b) = pr

factorIntegerLemma : (x : ℕ) (indHyp : (y : ℕ) (y<x : y <N x) → ((y <N 2) || (factorisationNonunit 1 y))) → ((x <N 2) || (factorisationNonunit 1 x))
factorIntegerLemma zero indHyp = inl (succIsPositive 1)
factorIntegerLemma (succ zero) indHyp = inl (succPreservesInequality (succIsPositive 0))
factorIntegerLemma (succ (succ x)) indHyp with everyNumberHasAPrimeFactor {succ (succ x)} (succPreservesInequality (succIsPositive x))
factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | multiplicationNIsCommutative a 0 = exFalso (naughtE ssxDivA)
factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 11 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = ssxDivA ; remIsSmall = r ; quotSmall = inl (TotalOrder.<Transitive ℕTotalOrder (le zero refl) 11 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }

factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ (succ qu) ; rem = .0 ; pr = ssxDivA ; remIsSmall = remSmall } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 11 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = succ (succ qu) ; rem = 0 ; pr = ssxDivA ; remIsSmall = remSmall ; quotSmall = inl (TotalOrder.<Transitive ℕTotalOrder (le zero refl) 11 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inr record {fst = succPreservesInequality (succIsPositive qu) ; snd = factNonunit} ; otherFactorsNumber = succ (factorisationNonunit.otherFactorsNumber indHypRes') }
  where
    indHypRes : ((succ (succ qu)) <N 2) || factorisationNonunit 1 (succ (succ qu))
    indHypRes = indHyp (succ (succ qu)) (lemma2 {a} {succ (succ qu)} {succ (succ x)} 1<a (succIsPositive (succ qu)) ssxDivA)
    indHypRes' : factorisationNonunit 1 (succ (succ qu))
    indHypRes' with indHypRes
    indHypRes' | inl y = exFalso (zeroNeverGreater (canRemoveSuccFrom<N (canRemoveSuccFrom<N y)))
    indHypRes' | inr y = y
    z|ssx : (z : ℕ) → z ∣ succ (succ qu) → z ∣ succ (succ x)
    z|ssx z z|ssq = (divisibilityTransitive z|ssq (divides (record { quot = a ; rem = 0 ; pr = identityOfIndiscernablesLeft _≡_ ssxDivA (applyEquality (λ t → t +N 0) (multiplicationNIsCommutative a (succ (succ qu)))) ; remIsSmall = zeroIsValidRem (succ (succ qu)) ; quotSmall = inl (succIsPositive _) }) refl))
    factNonunit : factorisationNonunit a (succ (succ qu))
    factNonunit with totality a (factorisationNonunit.firstFactor indHypRes')
    factNonunit | inl (inl a<ff) = canIncreaseFactorBound indHypRes' (λ z 1<z z<a z|ssq → smallerFactors z z<a 1<z (z|ssx z z|ssq)) (inl a<ff)
    factNonunit | inl (inr ff<a) = exFalso (smallerFactors (factorisationNonunit.firstFactor indHypRes') ff<a (factorisationNonunit.firstFactorNontrivial indHypRes') (z|ssx (factorisationNonunit.firstFactor indHypRes') (divides (factorisationNonunit.firstFactorDivision indHypRes') (factorisationNonunit.firstFactorDivides indHypRes'))))
    factNonunit | inr ff=a = canIncreaseFactorBound indHypRes' (λ z 1<z z<a z|ssq → smallerFactors z z<a 1<z (divisibilityTransitive z|ssq (divides (record { quot = a ; rem = 0 ; pr = identityOfIndiscernablesLeft _≡_ ssxDivA (applyEquality (λ t → t +N 0) (multiplicationNIsCommutative a (succ (succ qu)))) ; remIsSmall = zeroIsValidRem (succ (succ qu)) ; quotSmall = inl (succIsPositive _) }) refl))) (inr ff=a)

factorInteger : (a : ℕ) → (1 <N a) → factorisationNonunit 1 a
factorInteger a 1<a with (rec <NWellfounded (λ n → (n <N 2) || (factorisationNonunit 1 n))) factorIntegerLemma
... | bl with bl a
factorInteger a 1<a | bl | inl x = exFalso (noIntegersBetweenXAndSuccX 1 1<a x)
factorInteger a 1<a | bl | inr x = x

lessTransLemma : {p i j : ℕ} → p <N i → i ≤N j → p <N j
lessTransLemma {p} {i} {j} p<i (inl x) = <Transitive p<i x
lessTransLemma {p} {i} {j} p<i (inr x) rewrite x = p<i

lemma4' : {quot rem b : ℕ} → (quot +N quot) +N rem ≡ succ b → quot <N succ b
lemma4' {zero} {rem} {b} pr = succIsPositive b
lemma4' {succ quot} {rem} {b} pr rewrite equalityCommutative (Semiring.+Associative ℕSemiring quot (succ quot) rem) = succPreservesInequality (le (quot +N rem) (succInjective (transitivity (applyEquality succ (Semiring.commutative ℕSemiring _ quot)) pr)))

lemma4 : {quot a rem b : ℕ} → (a *N quot +N rem ≡ succ b) → (1 <N a) → (quot <N succ b)
lemma4 {quot} {zero} {rem} {b} pr 1<a = exFalso (zeroNeverGreater 1<a)
lemma4 {quot} {succ zero} {rem} {b} pr 1<a = exFalso (lessIrreflexive 1<a)
lemma4 {quot} {succ (succ zero)} {rem} {b} pr 1<a rewrite Semiring.sumZeroRight ℕSemiring quot = lemma4' pr
lemma4 {quot} {succ (succ (succ a))} {rem} {b} pr 1<a = lemma4 {quot} {succ (succ a)} {quot +N rem} {b} p' (succPreservesInequality (succIsPositive a))
  where
    p' : (quot +N (quot +N a *N quot)) +N (quot +N rem) ≡ succ b
    p' rewrite Semiring.commutative ℕSemiring quot (quot +N (quot +N a *N quot)) | Semiring.+Associative ℕSemiring (quot +N (quot +N a *N quot)) quot rem = pr

noSmallerFactors : {a i p : ℕ} → (factorisationNonunit i a) → (Prime p) → (p <N i) → (p ∣ a) → False
noSmallerFactors {a} {i} {p} factA pPrime p<i p|a with rec <NWellfounded (λ b → (factorisationNonunit i b) → p ∣ b → False)
... | indHyp = (indHyp prf) a factA p|a
  where
    prf : (x : ℕ) (ind : (y : ℕ) (y<x : y <N x) (factY : factorisationNonunit i y) (p|y : p ∣ y) → False) (factX : factorisationNonunit i x) (p|x : p ∣ x) → False
    prf x ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inl record { fst = quotFirstfact=1 ; snd = otherFactorsNumber }) } p|x = exFalso bad
      where
        x=firstFact : firstFactor *N 1 +N 0 ≡ x
        x=firstFact rewrite equalityCommutative firstFactorDivides | equalityCommutative quotFirstfact=1 = divisionAlgResult.pr firstFactorDivision
        x=firstFact' : firstFactor ≡ x
        x=firstFact' = transitivity (equalityCommutative (lemma firstFactor)) x=firstFact
        p|firstFact : p ∣ firstFactor
        p|firstFact rewrite x=firstFact' = p|x
        p=firstFact : p ≡ firstFactor
        p=firstFact = primeDivPrimeImpliesEqual pPrime firstFactorPrime p|firstFact
        i<=firstFactor : i ≤N p
        i<=firstFactor rewrite p=firstFact = firstFactorBiggerMin
        bad : False
        bad with i<=firstFactor
        ... | inl t = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder t p<i)
        ... | inr eq rewrite eq = TotalOrder.irreflexive ℕTotalOrder p<i
    prf zero ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inr otherFact) } p|x = zeroNeverGreater 1<a
    prf (succ x) ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inr otherFact) } p|x = ind (divisionAlgResult.quot firstFactorDivision) (lemma4 {divisionAlgResult.quot firstFactorDivision} {firstFactor} {divisionAlgResult.rem firstFactorDivision} {x} (divisionAlgResult.pr (firstFactorDivision)) (primesAreBiggerThanOne firstFactorPrime)) (canReduceFactorBound' (_&&_.snd otherFact) firstFactorBiggerMin) (p|q p|ffOrQ)
      where
        succXNotSmaller : succ x <N firstFactor → False
        succXNotSmaller = divisorIsSmaller {firstFactor} {x} (divides firstFactorDivision firstFactorDivides)
        succXNotSmaller' : firstFactor ≤N succ x
        succXNotSmaller' = notSmallerMeansGE succXNotSmaller
        inter : firstFactor *N (divisionAlgResult.quot firstFactorDivision) +N divisionAlgResult.rem firstFactorDivision ≡ (succ x)
        inter = divisionAlgResult.pr firstFactorDivision
        inter' : firstFactor *N (divisionAlgResult.quot firstFactorDivision) +N 0 ≡ (succ x)
        inter' rewrite equalityCommutative firstFactorDivides = inter
        inter'' : firstFactor *N (divisionAlgResult.quot firstFactorDivision) ≡ (succ x)
        inter'' rewrite equalityCommutative (Semiring.sumZeroRight ℕSemiring (firstFactor *N (divisionAlgResult.quot firstFactorDivision))) = inter'
        p|ff*q : p ∣ firstFactor *N (divisionAlgResult.quot firstFactorDivision)
        p|ff*q rewrite inter'' = p|x
        p|ffOrQ : (p ∣ firstFactor) || (p ∣ divisionAlgResult.quot firstFactorDivision)
        p|ffOrQ = primesArePrime pPrime p|ff*q
        p|ffIsFalse : (p ∣ firstFactor) → False
        p|ffIsFalse p|ff = lessIrreflexive (lessTransLemma p<i i<=p)
          where
            p=ff : p ≡ firstFactor
            p=ff = primeDivPrimeImpliesEqual pPrime firstFactorPrime p|ff
            i<=p : i ≤N p
            i<=p rewrite p=ff = firstFactorBiggerMin
        p|q : ((p ∣ firstFactor) || (p ∣ divisionAlgResult.quot firstFactorDivision)) → (p ∣ divisionAlgResult.quot firstFactorDivision)
        p|q (inl fls) = exFalso (p|ffIsFalse fls)
        p|q (inr res) = res

lemma3 : {a : ℕ} → a ≡ 0 → 1 <N a → False
lemma3 {a} a=0 pr rewrite a=0 = zeroNeverGreater pr

firstFactorUniqueLemma : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (factorisationNonunit.firstFactor f1 <N factorisationNonunit.firstFactor f2) → False
firstFactorUniqueLemma {i} a 1<a f1 f2 ff1<ff2 = go
  where
    p1 = factorisationNonunit.firstFactor f1
    rem1 = divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f1)
    p2 = factorisationNonunit.firstFactor f2
    rem2 = divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2)
    p1<p2 : p1 <N p2
    p1<p2 = ff1<ff2
    a=p2rem2 : a ≡ p2 *N rem2
    a=p2rem2 with divisionAlgResult.pr (factorisationNonunit.firstFactorDivision f2)
    ... | ff rewrite factorisationNonunit.firstFactorDivides f2 | Semiring.sumZeroRight ℕSemiring (factorisationNonunit.firstFactor f2 *N divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2)) = equalityCommutative ff
    p1|second : (p1 ∣ p2) || (p1 ∣ rem2)
    p1|second = primesArePrime {p1} {p2} {rem2} (factorisationNonunit.firstFactorPrime f1) lem
      where
        lem : p1 ∣ (p2 *N rem2)
        lem = identityOfIndiscernablesRight _∣_ (divides (factorisationNonunit.firstFactorDivision f1) (factorisationNonunit.firstFactorDivides f1)) a=p2rem2
    p1|second' : ((p1 ∣ p2) || (p1 ∣ rem2)) → ((p1 ≡ p2) || (p1 ∣ rem2))
    p1|second' (inl x) = inl (primeDivPrimeImpliesEqual (factorisationNonunit.firstFactorPrime f1) (factorisationNonunit.firstFactorPrime f2) x)
    p1|second' (inr x) = inr x
    p1|second'' : (p1 ≡ p2) || (p1 ∣ rem2)
    p1|second'' = p1|second' p1|second
    go : False
    go with p1|second''
    go | inl x = irreflexive (<WellDefined x refl ff1<ff2)
    go | inr x with factorisationNonunit.otherFactors f2
    go | inr x | inl record { fst = rem2=1 ; snd = _ } rewrite rem2=1 = exFalso (oneIsNotPrime res)
      where
        1prime' : Prime p1 ≡ Prime 1
        1prime' = applyEquality Prime (oneHasNoDivisors x)
        res : Prime 1
        res rewrite equalityCommutative 1prime' = (factorisationNonunit.firstFactorPrime f1)
    go | inr x | inr p1|rem2 with factorisationNonunit.otherFactors f2
    go | inr x | inr p1|rem2 | inl record { fst = rem2=1 ; snd = _ } rewrite rem2=1 = exFalso (oneIsNotPrime res)
      where
        1prime' : Prime p1 ≡ Prime 1
        1prime' = applyEquality Prime (oneHasNoDivisors x)
        res : Prime 1
        res rewrite equalityCommutative 1prime' = (factorisationNonunit.firstFactorPrime f1)
    go | inr x | inr p1|rem2 | inr factorRem2 = noSmallerFactors (_&&_.snd factorRem2) (factorisationNonunit.firstFactorPrime f1) p1<p2 x

firstFactorUnique : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (factorisationNonunit.firstFactor f1 ≡ factorisationNonunit.firstFactor f2)
firstFactorUnique {i} a 1<a f1 f2 with totality (factorisationNonunit.firstFactor f1) (factorisationNonunit.firstFactor f2)
firstFactorUnique {i} a 1<a f1 f2 | inl (inl f1<f2) = exFalso (firstFactorUniqueLemma a 1<a f1 f2 f1<f2)
firstFactorUnique {i} a 1<a f1 f2 | inl (inr f2<f1) = exFalso (firstFactorUniqueLemma a 1<a f2 f1 f2<f1)
firstFactorUnique {i} a 1<a f1 f2 | inr x = x

factorListLemma : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2)) ≡ (divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f1))
factorListLemma {i} a 1<a f1 f2 with firstFactorUnique {i} a 1<a f1 f2
... | firstFactEqual = res
  where
    div1 : divisionAlgResult (factorisationNonunit.firstFactor f1) a
    div1 = factorisationNonunit.firstFactorDivision f1
    rem1=0 : divisionAlgResult.rem div1 ≡ 0
    rem1=0 = factorisationNonunit.firstFactorDivides f1
    pr1 : (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1) +N 0 ≡ a
    pr1 rewrite equalityCommutative rem1=0 = divisionAlgResult.pr div1
    pr1' : (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1) ≡ a
    pr1' rewrite equalityCommutative (Semiring.sumZeroRight ℕSemiring ((factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1))) = pr1
    div2 : divisionAlgResult (factorisationNonunit.firstFactor f2) a
    div2 = factorisationNonunit.firstFactorDivision f2
    rem2=0 : divisionAlgResult.rem div2 ≡ 0
    rem2=0 = factorisationNonunit.firstFactorDivides f2
    pr2 : (factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2) +N 0 ≡ a
    pr2 rewrite equalityCommutative rem2=0 = divisionAlgResult.pr div2
    pr2' : (factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2) ≡ a
    pr2' rewrite equalityCommutative (Semiring.sumZeroRight ℕSemiring ((factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2))) = pr2
    pr : (factorisationNonunit.firstFactor f2) *N (divisionAlgResult.quot div2) ≡ (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1)
    pr = transitivity pr2' (equalityCommutative pr1')
    pr' : (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div2) ≡ (factorisationNonunit.firstFactor f1) *N (divisionAlgResult.quot div1)
    pr' = identityOfIndiscernablesLeft _≡_ pr (applyEquality (λ t → t *N divisionAlgResult.quot div2) (equalityCommutative firstFactEqual))
    positive : zero <N factorisationNonunit.firstFactor f1
    positive = lessTransitive (succIsPositive 0) (factorisationNonunit.firstFactorNontrivial f1)
    res : divisionAlgResult.quot div2 ≡ divisionAlgResult.quot div1
    res = productCancelsLeft (factorisationNonunit.firstFactor f1) (divisionAlgResult.quot div2) (divisionAlgResult.quot div1) positive pr'

factorListSameLength : {i : ℕ} → (a : ℕ) → (1 <N a) → (f1 : factorisationNonunit i a) → (f2 : factorisationNonunit i a) → (divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f1) ≡ 1) → divisionAlgResult.quot (factorisationNonunit.firstFactorDivision f2) ≡ 1
factorListSameLength {i} a 1<a f1 f2 quot=1 with firstFactorUnique {i} a 1<a f1 f2
... | firstFactEqual with factorListLemma {i} a 1<a f1 f2
... | eq = transitivity eq quot=1


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Streams
------------------------------------------------------------------------

module Data.Stream where

open import Coinduction
open import Data.Colist using (Colist; []; _∷_)
open import Data.Vec    using (Vec;    []; _∷_)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

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

{-# IMPORT Data.FFI #-}
{-# COMPILED_DATA Stream Data.FFI.AgdaStream Data.FFI.Cons #-}

------------------------------------------------------------------------
-- Some operations

head : ∀ {A} → Stream A → A
head (x ∷ xs) = x

tail : ∀ {A} → Stream A → Stream A
tail (x ∷ xs) = ♭ xs

map : ∀ {A B} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

zipWith : ∀ {A B C} →
          (A → B → C) → Stream A → Stream B → Stream C
zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys)

take : ∀ {A} n → Stream A → Vec A n
take zero    xs       = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

drop : ∀ {A} → ℕ → Stream A → Stream A
drop zero    xs       = xs
drop (suc n) (x ∷ xs) = drop n (♭ xs)

repeat : ∀ {A} → A → Stream A
repeat x = x ∷ ♯ repeat x

iterate : ∀ {A} → (A → A) → A → Stream A
iterate f x = x ∷ ♯ iterate f (f x)

-- Interleaves the two streams.

infixr 5 _⋎_

_⋎_ : ∀ {A} → Stream A → Stream A → Stream A
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)

mutual

  -- Takes every other element from the stream, starting with the
  -- first one.

  evens : ∀ {A} → Stream A → Stream A
  evens (x ∷ xs) = x ∷ ♯ odds (♭ xs)

  -- Takes every other element from the stream, starting with the
  -- second one.

  odds : ∀ {A} → Stream A → Stream A
  odds (x ∷ xs) = evens (♭ xs)

toColist : ∀ {A} → Stream A → Colist A
toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs)

lookup : ∀ {A} → ℕ → Stream A → A
lookup zero    (x ∷ xs) = x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

infixr 5 _++_

_++_ : ∀ {A} → Colist A → Stream A → Stream A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

------------------------------------------------------------------------
-- Equality and other relations

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {A} : Stream A → Stream A → Set where
  _∷_ : ∀ {x y xs ys}
        (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys

-- x ∈ xs means that x is a member of xs.

infix 4 _∈_

data _∈_ {A} : A → Stream A → Set where
  here  : ∀ {x   xs}                   → x ∈ x ∷ xs
  there : ∀ {x y xs} (x∈xs : x ∈ ♭ xs) → x ∈ y ∷ xs

-- xs ⊑ ys means that xs is a prefix of ys.

infix 4 _⊑_

data _⊑_ {A} : Colist A → Stream A → Set where
  []  : ∀ {ys}                            → []     ⊑ ys
  _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys

------------------------------------------------------------------------
-- Some proofs

setoid : Set → Setoid _ _
setoid A = record
  { Carrier       = Stream A
  ; _≈_           = _≈_ {A}
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {_ ∷ _} = P.refl ∷ ♯ refl

  sym : Symmetric _≈_
  sym (x≡ ∷ xs≈) = P.sym x≡ ∷ ♯ sym (♭ xs≈)

  trans : Transitive _≈_
  trans (x≡ ∷ xs≈) (y≡ ∷ ys≈) = P.trans x≡ y≡ ∷ ♯ trans (♭ xs≈) (♭ ys≈)

head-cong : ∀ {A} {xs ys : Stream A} → xs ≈ ys → head xs ≡ head ys
head-cong (x≡ ∷ _) = x≡

tail-cong : ∀ {A} {xs ys : Stream A} → xs ≈ ys → tail xs ≈ tail ys
tail-cong (_ ∷ xs≈) = ♭ xs≈

map-cong : ∀ {A B} (f : A → B) {xs ys} →
           xs ≈ ys → map f xs ≈ map f ys
map-cong f (x≡ ∷ xs≈) = P.cong f x≡ ∷ ♯ map-cong f (♭ xs≈)

zipWith-cong : ∀ {A B C} (_∙_ : A → B → C) {xs xs′ ys ys′} →
               xs ≈ xs′ → ys ≈ ys′ →
               zipWith _∙_ xs ys ≈ zipWith _∙_ xs′ ys′
zipWith-cong _∙_ (x≡ ∷ xs≈) (y≡ ∷ ys≈) =
  P.cong₂ _∙_ x≡ y≡ ∷ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈)

infixr 5 _⋎-cong_

_⋎-cong_ : ∀ {A} {xs xs′ ys ys′ : Stream A} →
           xs ≈ xs′ → ys ≈ ys′ → xs ⋎ ys ≈ xs′ ⋎ ys′
(x ∷ xs≈) ⋎-cong ys≈ = x ∷ ♯ (ys≈ ⋎-cong ♭ xs≈)


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.BinNat where

open import Cubical.Data.BinNat.BinNat public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import Categories.Category
open import Categories.Functor hiding (id)

-- Limit of a Cone over a Functor F : J → C
module Categories.Diagram.Limit
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

private
  module C = Category C
  module J = Category J
open C
open HomReasoning
open Functor F

open import Level
open import Data.Product using (proj₂)

open import Categories.Category.Construction.Cones F renaming (Cone⇒ to _⇨_)
open import Categories.Object.Terminal as T hiding (up-to-iso; transport-by-iso)
open import Categories.Morphism.Reasoning C
open import Categories.Morphism C
open import Categories.Morphism Cones as MC using () renaming (_≅_ to _⇔_)

private
  variable
    K K′  : Cone
    A B   : J.Obj
    X Y Z : Obj
    q     : K ⇨ K′

-- A Limit is a Terminal object in the category of Cones
--   (This could be unpacked...)
record Limit : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    terminal : Terminal Cones

  module terminal = Terminal terminal

  open terminal using () renaming (⊤ to limit) public
  open Cone limit hiding (apex) renaming (N to apex; ψ to proj; commute to limit-commute) public

  rep-cone : ∀ K → K ⇨ limit
  rep-cone K = terminal.! {K}

  rep : ∀ K → Cone.N K ⇒ apex
  rep K = arr
    where open _⇨_ (rep-cone K)

  unrep : X ⇒ apex → Cone
  unrep f = record {
    apex        = record
      { ψ       = λ A → proj A ∘ f
      ; commute = λ g → pullˡ (limit-commute g)
      }
    }

  conify : (f : X ⇒ apex) → unrep f ⇨ limit
  conify f = record
    { arr     = f
    ; commute = refl
    }

  commute : proj A ∘ rep K ≈ Cone.ψ K A
  commute {K = K} = _⇨_.commute (rep-cone K)

  unrep-cone : (K ⇨ limit) → Cone
  unrep-cone f = unrep (_⇨_.arr f)

  g-η : ∀ {f : X ⇒ apex} → rep (unrep f) ≈ f
  g-η {f = f} = terminal.!-unique (conify f)

  η-cone : Cones [ rep-cone limit ≈ Category.id Cones ]
  η-cone = terminal.⊤-id (rep-cone limit)

  η : rep limit ≈ id
  η = η-cone

  rep-cone∘ : Cones [ Cones [ rep-cone K ∘ q ] ≈ rep-cone K′ ]
  rep-cone∘ {K = K} {q = q} = Equiv.sym (terminal.!-unique (Cones [ rep-cone K ∘ q ]))

  rep∘ : ∀ {q : K′ ⇨ K} → rep K ∘ _⇨_.arr q ≈ rep K′
  rep∘ {q = q} = rep-cone∘ {q = q}

  rep-cone-self-id : Cones [ rep-cone limit ≈ Cones.id ]
  rep-cone-self-id = terminal.!-unique Cones.id

  rep-self-id : rep limit ≈ id
  rep-self-id = rep-cone-self-id

open Limit

up-to-iso-cone : (L₁ L₂ : Limit) → limit L₁ ⇔ limit L₂
up-to-iso-cone L₁ L₂ = T.up-to-iso Cones (terminal L₁) (terminal L₂)

up-to-iso : (L₁ L₂ : Limit) → apex L₁ ≅ apex L₂
up-to-iso L₁ L₂ = iso-cone⇒iso-apex (up-to-iso-cone L₁ L₂)

transport-by-iso-cone : (L : Limit) → limit L ⇔ K → Limit
transport-by-iso-cone L L⇿K = record
  { terminal = T.transport-by-iso Cones (terminal L) L⇿K
  }

transport-by-iso : (L : Limit) → apex L ≅ X → Limit
transport-by-iso L L≅X = transport-by-iso-cone L (proj₂ p)
  where p = cone-resp-iso (limit L) L≅X

module _ (X : Obj) (apex₁ : Apex X) (apex₂ : Apex X) (L : Limit) where
  private
    module apex₁ = Apex apex₁
    module apex₂ = Apex apex₂
    module L = Limit L

    K₁ : Cone
    K₁ = record { apex = apex₁ }
    module K₁ = Cone K₁

    K₂ : Cone
    K₂ = record { apex = apex₂ }
    module K₂ = Cone K₂

  ψ-≈⇒rep-≈ : (∀ A → apex₁.ψ A ≈ apex₂.ψ A) → L.rep K₁ ≈ L.rep K₂
  ψ-≈⇒rep-≈ ∀eq = trans (L.terminal.!-unique K₁⇒limit) identityʳ
    where K₁⇒K₂ : K₁ ⇨ K₂
          K₁⇒K₂ = record
            { arr     = id
            ; commute = λ {X} → trans identityʳ (sym (∀eq X))
            }

          K₁⇒limit : K₁ ⇨ L.limit
          K₁⇒limit = Cones [ L.terminal.! ∘ K₁⇒K₂ ]

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Data.Product using ( _,_ )
open import Data.Empty using ( ⊥ )
open import FRP.LTL.ISet.Core using ( ISet ; [_] ; _,_ )

module FRP.LTL.ISet.Empty where

F : ISet
F = [ (λ i → ⊥) , (λ i j i~j → λ ()) , (λ i j i⊑j → λ ()) ]

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module ReducingConstructorsInWith where

data ⊤ : Set where
  tt : ⊤

module RegExps where

  data RegExp : Set where
    _│_ : RegExp -> RegExp -> RegExp

open module R = RegExps

bypassable : (re : RegExp) -> ⊤
bypassable (re₁ │ re₂) with bypassable re₁
bypassable (re₁ │ re₂) | m  = m


text:
module MonoidalCat where

open import Library hiding (_×_)
open import Categories
open import Categories.Products
open import Functors
open import Naturals

record Monoidal {l}{m} : Set (lsuc (l ⊔ m)) where
  field C : Cat {l}{m}
  open Cat C
  open Fun
  open NatI
  field ⊗ : Fun (C × C) C
        I : Obj

  I⊗- : Fun C C
  I⊗- = functor
    (\ A -> OMap ⊗ (I , A))
    (\ f -> HMap ⊗ (iden , f))
    (fid ⊗)
    (trans (cong (\f -> HMap ⊗ (f , _)) (sym idl)) (fcomp ⊗))

  field λ'  : NatI I⊗- (IdF C)

  -⊗I : Fun C C
  -⊗I = functor
    (\ A -> OMap ⊗ (A , I))
    (\ f -> HMap ⊗ (f , iden))
    (fid ⊗)
    (trans (cong (\f -> HMap ⊗ (_ , f)) (sym idl)) (fcomp ⊗))

  field ρ  : NatI -⊗I (IdF C)

  [-⊗-]⊗- : Fun (C × C × C) C
  [-⊗-]⊗- = functor
    (λ {(X , Y , Z) → OMap ⊗ (OMap ⊗ (X , Y) , Z)})
    (λ {(f , g , h) → HMap ⊗ (HMap ⊗ (f , g) , h)})
    (trans (cong (\f -> HMap ⊗ (f , _)) (fid ⊗) ) (fid ⊗))
    (trans (cong (\f -> HMap ⊗ (f , _)) (fcomp ⊗)) (fcomp ⊗))

  -⊗[-⊗-] : Fun (C × C × C) C
  -⊗[-⊗-] = functor
    (λ {(X , Y , Z) → OMap ⊗ (X , OMap ⊗ (Y , Z))})
    (λ {(f , g , h) → HMap ⊗ (f , HMap ⊗ (g , h))})
    (trans (cong (\f -> HMap ⊗ (_ , f)) (fid ⊗) ) (fid ⊗))
    (trans (cong (\f -> HMap ⊗ (_ , f)) (fcomp ⊗)) (fcomp ⊗))

  field α : NatI [-⊗-]⊗- -⊗[-⊗-]

        triangle : ∀{A B} ->
          comp (HMap ⊗ (iden {A} , (cmp λ' {B}))) (cmp α {A , I , B})
          ≅  HMap ⊗ (cmp ρ {A} , iden {B})

        square : ∀{A B C D} ->
          comp (HMap ⊗ (iden {A} , cmp α {B , C , D}))
               (comp (cmp α {A , OMap ⊗ (B , C) , D})
                     (HMap ⊗ (cmp α {A , B , C} , iden {D})))
          ≅
          comp (cmp α {A , B , OMap ⊗ (C , D)})
               (cmp α {OMap ⊗ (A , B) , C , D})

record MonoidalFun {a b c d}(M : Monoidal {a}{b})(M' : Monoidal {c}{d})
  : Set (a ⊔ b ⊔ c ⊔ d) where
  open Monoidal
  open Cat

  field F : Fun (C M) (C M')

  open Fun

  field e : Hom (C M') (I M') (OMap F (I M))

  F-⊗'F- : Fun (C M × C M) (C M')
  F-⊗'F- = functor
    (\ {(A , B) -> OMap (⊗ M') (OMap F A , OMap F B)})
    (\ {(f , g) -> HMap (⊗ M') (HMap F f , HMap F g)})
    (trans (cong₂ (\f g -> HMap (⊗ M') (f , g)) (fid F) (fid F)) (fid (⊗ M')))
    (trans (cong₂ (\f g -> HMap (⊗ M') (f , g))
           (fcomp F) (fcomp F)) (fcomp (⊗ M')))

  F[-⊗-] : Fun (C M × C M) (C M')
  F[-⊗-] = functor
    (λ { (A , B) → OMap F (OMap (⊗ M) (A , B)) })
    ((λ { (f , g) → HMap F (HMap (⊗ M) (f , g)) }))
    (trans (cong (HMap F) (fid (⊗ M))) (fid F))
    (trans (cong (HMap F) (fcomp (⊗ M))) (fcomp F))

  field m : NatT F-⊗'F- F[-⊗-]

  field square1 : ∀{A} ->
          NatI.cmp (ρ M') {OMap F A}
          ≅
          comp (C M') (HMap F (NatI.cmp (ρ M) {A}))
                      (comp (C M') (NatT.cmp m {A , I M})
                                   (HMap (⊗ M') (iden (C M') {OMap F A} , e)))

        square2 : ∀{B} ->
          NatI.cmp (λ' M') {OMap F B}
          ≅
          comp (C M') (HMap F (NatI.cmp (λ' M) {B}))
                      (comp (C M') (NatT.cmp m {I M , B})
                                   (HMap (⊗ M') (e , iden (C M') {OMap F B})))

        hexagon : ∀{A B B'} ->
           comp (C M') (HMap F (NatI.cmp (α M) {A , B , B'}))
                       (comp (C M') (NatT.cmp m {OMap (⊗ M) (A , B) , B'})
                                    (HMap (⊗ M') (NatT.cmp m {A , B} ,
                                                  iden (C M') {OMap F B'})))
           ≅
           comp (C M') (NatT.cmp m {A , OMap (⊗ M) (B , B')})
                       (comp (C M') (HMap (⊗ M') (iden (C M') {OMap F A} ,
                                                  NatT.cmp m {B , B'}))
                                    (NatI.cmp (α M') {OMap F A ,
                                                      OMap F B ,
                                                      OMap F B'}))

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads