text:
-- Andreas, 2018-06-30, issue #3147 reported by bafain
-- Pattern linearity ignored for as-patterns

-- {-# OPTIONS -v tc.lhs.top:30 #-}
-- {-# OPTIONS -v tc.lhs.linear:100 #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

f : Nat → Nat
f zero      = zero
f x@(suc x) = x    -- rhs context:
                   -- x : Nat
                   -- x : Nat

-- Should fail during lhs-checking

f-id-1 : f 1 ≡ 1
f-id-1 = refl

f-pre-1 : f 1 ≡ 0
f-pre-1 = refl

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Literals used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Literal where

import Data.Char as Char
import Data.Float as Float
import Data.Nat as ℕ
open import Data.String as String using (String)
import Data.Word as Word
import Reflection.Meta as Meta
import Reflection.Name as Name
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors

open import Agda.Builtin.Reflection public
  using ( Literal )
open Literal public

------------------------------------------------------------------------
-- Decidable equality

meta-injective : ∀ {x y} → meta x ≡ meta y → x ≡ y
meta-injective refl = refl

nat-injective : ∀ {x y} → nat x ≡ nat y → x ≡ y
nat-injective refl = refl

word64-injective : ∀ {x y} → word64 x ≡ word64 y → x ≡ y
word64-injective refl = refl

float-injective : ∀ {x y} → float x ≡ float y → x ≡ y
float-injective refl = refl

char-injective : ∀ {x y} → char x ≡ char y → x ≡ y
char-injective refl = refl

string-injective : ∀ {x y} → string x ≡ string y → x ≡ y
string-injective refl = refl

name-injective : ∀ {x y} → name x ≡ name y → x ≡ y
name-injective refl = refl

infix 4 _≟_
_≟_ : DecidableEquality Literal
nat x ≟ nat x₁ = Dec.map′ (cong nat) nat-injective (x ℕ.≟ x₁)
nat x ≟ word64 x₁ = no (λ ())
nat x ≟ float x₁ = no (λ ())
nat x ≟ char x₁ = no (λ ())
nat x ≟ string x₁ = no (λ ())
nat x ≟ name x₁ = no (λ ())
nat x ≟ meta x₁ = no (λ ())
word64 x ≟ word64 x₁ = Dec.map′ (cong word64) word64-injective (x Word.≟ x₁)
word64 x ≟ nat x₁ = no (λ ())
word64 x ≟ float x₁ = no (λ ())
word64 x ≟ char x₁ = no (λ ())
word64 x ≟ string x₁ = no (λ ())
word64 x ≟ name x₁ = no (λ ())
word64 x ≟ meta x₁ = no (λ ())
float x ≟ nat x₁ = no (λ ())
float x ≟ word64 x₁ = no (λ ())
float x ≟ float x₁ = Dec.map′ (cong float) float-injective (x Float.≟ x₁)
float x ≟ char x₁ = no (λ ())
float x ≟ string x₁ = no (λ ())
float x ≟ name x₁ = no (λ ())
float x ≟ meta x₁ = no (λ ())
char x ≟ nat x₁ = no (λ ())
char x ≟ word64 x₁ = no (λ ())
char x ≟ float x₁ = no (λ ())
char x ≟ char x₁ = Dec.map′ (cong char) char-injective (x Char.≟ x₁)
char x ≟ string x₁ = no (λ ())
char x ≟ name x₁ = no (λ ())
char x ≟ meta x₁ = no (λ ())
string x ≟ nat x₁ = no (λ ())
string x ≟ word64 x₁ = no (λ ())
string x ≟ float x₁ = no (λ ())
string x ≟ char x₁ = no (λ ())
string x ≟ string x₁ = Dec.map′ (cong string) string-injective (x String.≟ x₁)
string x ≟ name x₁ = no (λ ())
string x ≟ meta x₁ = no (λ ())
name x ≟ nat x₁ = no (λ ())
name x ≟ word64 x₁ = no (λ ())
name x ≟ float x₁ = no (λ ())
name x ≟ char x₁ = no (λ ())
name x ≟ string x₁ = no (λ ())
name x ≟ name x₁ = Dec.map′ (cong name) name-injective (x Name.≟ x₁)
name x ≟ meta x₁ = no (λ ())
meta x ≟ nat x₁ = no (λ ())
meta x ≟ word64 x₁ = no (λ ())
meta x ≟ float x₁ = no (λ ())
meta x ≟ char x₁ = no (λ ())
meta x ≟ string x₁ = no (λ ())
meta x ≟ name x₁ = no (λ ())
meta x ≟ meta x₁ = Dec.map′ (cong meta) meta-injective (x Meta.≟ x₁)

ext: agda


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Cat.Facts.Initial where

open import Cats.Category
open import Cats.Category.Cat using (Cat)
open import Cats.Category.Zero using (Zero)
open import Cats.Functor

Absurd : ∀ {lo la l≈ lo′ la′ l≈′} (C : Category lo′ la′ l≈′)
  → Functor (Zero lo la l≈) C
Absurd C = record
  { fobj = λ()
  ; fmap = λ{}
  ; fmap-resp = λ{}
  ; fmap-id = λ{}
  ; fmap-∘ = λ{}
  }

instance
  hasInitial : ∀ {lo la l≈} → HasInitial (Cat lo la l≈)
  hasInitial {lo} {la} {l≈} = record
    { ⊥ = Zero lo la l≈
    ; isInitial = λ X → record
      { arr = Absurd X
      ; unique = λ x → record
        { iso = λ{}
        ; forth-natural = λ{}
        }
      }
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

open import lib.Basics
open import lib.types.Bool
open import lib.types.Coproduct
open import lib.types.Truncation
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Fin
open import lib.types.Nat
open import lib.types.Empty
open import lib.NConnected
open import lib.NType2
open import lib.Equivalence2

{- Some miscellaneous lemmas about coproducts. -}
module Util.Coproducts where

⊔-fmap-is-equiv : {i j i' j' : ULevel} {A : Type i} {B : Type j} {A' : Type i'} {B' : Type j'}
  (f : A → A') (g : B → B') (f-eq : is-equiv f) (g-eq : is-equiv g) → is-equiv (⊔-fmap f g)

⊔-fmap-is-equiv f g f-eq g-eq =
  record { g = ⊔-fmap Feq.g Geq.g
         ; f-g = Coprod-elim (λ a → ap inl (Feq.f-g a)) λ b → ap inr (Geq.f-g b)
         ; g-f = Coprod-elim (λ a → ap inl (Feq.g-f a)) (λ b → ap inr (Geq.g-f b))
         ; adj = Coprod-elim (λ a → ∘-ap (⊔-fmap f g) inl _ ∙ ap-∘ _ _ _ ∙ ap (ap inl) (Feq.adj a))
                             λ b →  ∘-ap (⊔-fmap f g) _ _ ∙ ap-∘ _ _ _ ∙ ap (ap inr) (Geq.adj b)  }
  where
    module Feq = is-equiv f-eq
    module Geq = is-equiv g-eq

⊔-emap : {i i' j j' : ULevel} {A : Type i} {A' : Type i'} {B : Type j} {B' : Type j'}
  (e : A ≃ A') (e' : B ≃ B') → (A ⊔ B ≃ A' ⊔ B')

⊔-emap {A = A} {A' = A'} {B = B} {B' = B'} e e' = (f , record { g = g ; f-g = f-g ; g-f = g-f ; adj = adj })
  where
    f : A ⊔ B → A' ⊔ B'
    f = ⊔-fmap (–> e) (–> e')

    g : A' ⊔ B' → A ⊔ B
    g = ⊔-fmap (<– e) (<– e')

    f-g : (z : A' ⊔ B') → (f (g z) == z)
    f-g (inl x) = ap inl (<–-inv-r e x)
    f-g (inr x) = ap inr (<–-inv-r e' x)

    g-f : (z : A ⊔ B) → (g (f z) == z)
    g-f (inl x) = ap inl (<–-inv-l e x)
    g-f (inr x) = ap inr (<–-inv-l e' x)

    adj : (a : A ⊔ B) → ap f (g-f a) == f-g (f a)
    adj (inl a) =
      ap f (g-f (inl a))
        =⟨ idp ⟩
      ap f (ap inl (<–-inv-l e a))
        =⟨ ∘-ap f inl _ ⟩
      ap (f ∘ inl) (<–-inv-l e a)
        =⟨ idp ⟩
      ap (inl ∘ –> e) ((<–-inv-l e a))
        =⟨ ap-∘ inl (–> e) _ ⟩
      ap inl (ap (–> e) (<–-inv-l e a))
        =⟨ ap (ap inl) (<–-inv-adj e a) ⟩
      ap inl (<–-inv-r e (–> e a))
        =⟨ idp ⟩
      f-g (f (inl a))
        =∎
    adj (inr b) =
      ap f (g-f (inr b))
        =⟨ idp ⟩
      ap f (ap inr (<–-inv-l e' b))
        =⟨ ∘-ap f inr _ ⟩
      ap (f ∘ inr) (<–-inv-l e' b)
        =⟨ idp ⟩
      ap (inr ∘ –> e') ((<–-inv-l e' b))
        =⟨ ap-∘ inr (–> e') _ ⟩
      ap inr (ap (–> e') (<–-inv-l e' b))
        =⟨ ap (ap inr) (<–-inv-adj e' b) ⟩
      ap inr (<–-inv-r e' (–> e' b))
        =⟨ idp ⟩
      f-g (f (inr b))
        =∎

⊔-cancel-l : {i j : ULevel} {A : Type i} {B : Type j} → (A ⊔ B) → (¬ A) → B
⊔-cancel-l (inl a) na = ⊥-elim (na a)
⊔-cancel-l (inr b) _ = b

⊔-cancel-r : {i j : ULevel} {A : Type i} {B : Type j} → (A ⊔ B) → (¬ B) → A
⊔-cancel-r (inl a) _ = a
⊔-cancel-r (inr b) nb = ⊥-elim (nb b)

⊔-assoc : {i j k : ULevel} {A : Type i} {B : Type j} {C : Type k} → (A ⊔ B) ⊔ C ≃ A ⊔ B ⊔ C
⊔-assoc {A = A} {B = B} {C = C} = f , record { g = g ; f-g = f-g ; g-f = g-f ; adj = adj }
  where
    f : (A ⊔ B) ⊔ C → A ⊔ B ⊔ C
    f (inl (inl x)) = inl x
    f (inl (inr x)) = inr (inl x)
    f (inr x) = inr (inr x)

    g : A ⊔ B ⊔ C → (A ⊔ B) ⊔ C
    g (inl x) = inl (inl x)
    g (inr (inl x)) = inl (inr x)
    g (inr (inr x)) = inr x

    f-g : (z : A ⊔ B ⊔ C) → (f (g z) == z)
    f-g (inl x) = idp
    f-g (inr (inl x)) = idp
    f-g (inr (inr x)) = idp

    g-f : (z : (A ⊔ B) ⊔ C) → (g (f z) == z)
    g-f (inl (inl x)) = idp
    g-f (inl (inr x)) = idp
    g-f (inr x) = idp

    adj : (a : (A ⊔ B) ⊔ C) → ap f (g-f a) == f-g (f a)
    adj (inl (inl x)) = idp
    adj (inl (inr x)) = idp
    adj (inr x) = idp

⊔-sym : {i j : ULevel} {A : Type i} {B : Type j} → (A ⊔ B) ≃ (B ⊔ A)
⊔-sym = (λ {(inl a) → inr a ; (inr b) → inl b} ) ,
  record { g = λ { (inl b) → inr b ; (inr a) → inl a}
         ; f-g = λ { (inl x) → idp ; (inr x) → idp}
         ; g-f = λ { (inl x) → idp ; (inr x) → idp}
         ; adj = λ { (inl x) → idp ; (inr x) → idp} }

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
module left-kan-extensions where

open import functor

-- The left-kan extension of G along J.
record left-kan (G : Set → Set) (J : Set → Set) (pG : Functor G) (pJ : Functor J) : Set₁ where
  field
    lan : Set → Set
    pLan : Functor lan

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Powerset

open import Cubical.Data.Sigma
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing.Base

private
  variable
    ℓ : Level

module Units (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 private R = fst R'

 inverseUniqueness : (r : R) → isProp (Σ[ r' ∈ R ] r · r' ≡ 1r)
 inverseUniqueness r (r' , rr'≡1) (r'' , rr''≡1) = Σ≡Prop (λ _ → is-set _ _) path
  where
  path : r' ≡ r''
  path = r'             ≡⟨ sym (·Rid _) ⟩
         r' · 1r        ≡⟨ cong (r' ·_) (sym rr''≡1) ⟩
         r' · (r · r'') ≡⟨ ·Assoc _ _ _ ⟩
         (r' · r) · r'' ≡⟨ cong (_· r'') (·Comm _ _) ⟩
         (r · r') · r'' ≡⟨ cong (_· r'') rr'≡1 ⟩
         1r · r''       ≡⟨ ·Lid _ ⟩
         r''            ∎

 Rˣ : ℙ R
 Rˣ r = (Σ[ r' ∈ R ] r · r' ≡ 1r) , inverseUniqueness r

 -- some notation using instance arguments
 _⁻¹ : (r : R) → ⦃ r ∈ Rˣ ⦄ → R
 _⁻¹ r ⦃ r∈Rˣ ⦄ = r∈Rˣ .fst

 infix 9 _⁻¹

 -- some results about inverses
 ·-rinv : (r : R) ⦃ r∈Rˣ : r ∈ Rˣ ⦄ → r · r ⁻¹ ≡ 1r
 ·-rinv r ⦃ r∈Rˣ ⦄ = r∈Rˣ .snd

 ·-linv : (r : R) ⦃ r∈Rˣ : r ∈ Rˣ ⦄ → r ⁻¹ · r ≡ 1r
 ·-linv r ⦃ r∈Rˣ ⦄ = ·Comm _ _ ∙ r∈Rˣ .snd

 RˣMultClosed : (r r' : R) ⦃ r∈Rˣ : r ∈ Rˣ ⦄ ⦃ r'∈Rˣ : r' ∈ Rˣ ⦄
              → (r · r') ∈ Rˣ
 RˣMultClosed r r' = (r ⁻¹ · r' ⁻¹) , path
  where
  path : r · r' · (r ⁻¹ · r' ⁻¹) ≡ 1r
  path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ cong (_· (r ⁻¹ · r' ⁻¹)) (·Comm _ _) ⟩
         r' · r · (r ⁻¹ · r' ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
         r' · r · r ⁻¹ · r' ⁻¹   ≡⟨ cong (_· r' ⁻¹) (sym (·Assoc _ _ _)) ⟩
         r' · (r · r ⁻¹) · r' ⁻¹ ≡⟨ cong (λ x → r' · x · r' ⁻¹) (·-rinv _) ⟩
         r' · 1r · r' ⁻¹         ≡⟨ cong (_· r' ⁻¹) (·Rid _) ⟩
         r' · r' ⁻¹              ≡⟨ ·-rinv _ ⟩
         1r ∎

 RˣContainsOne : 1r ∈ Rˣ
 RˣContainsOne = 1r , ·Lid _

 RˣInvClosed : (r : R) ⦃ _ : r ∈ Rˣ ⦄ → r ⁻¹ ∈ Rˣ
 RˣInvClosed r = r , ·-linv _

 UnitsAreNotZeroDivisors : (r : R) ⦃ _ : r ∈ Rˣ ⦄
                         → ∀ r' → r' · r ≡ 0r → r' ≡ 0r
 UnitsAreNotZeroDivisors r r' p = r'              ≡⟨ sym (·Rid _) ⟩
                                  r' · 1r         ≡⟨ cong (r' ·_) (sym (·-rinv _)) ⟩
                                  r' · (r · r ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
                                  r' · r · r ⁻¹   ≡⟨ cong (_· r ⁻¹) p ⟩
                                  0r · r ⁻¹       ≡⟨ 0LeftAnnihilates _ ⟩
                                  0r ∎

 -- laws keeping the instance arguments
 1⁻¹≡1 : ⦃ 1∈Rˣ' : 1r ∈ Rˣ ⦄ → 1r ⁻¹ ≡ 1r
 1⁻¹≡1 ⦃ 1∈Rˣ' ⦄ = (sym (·Lid _)) ∙ 1∈Rˣ' .snd

 ⁻¹-dist-· : (r r' : R) ⦃ r∈Rˣ : r ∈ Rˣ ⦄ ⦃ r'∈Rˣ : r' ∈ Rˣ ⦄ ⦃ rr'∈Rˣ : (r · r') ∈ Rˣ ⦄
           → (r · r') ⁻¹ ≡ r ⁻¹ · r' ⁻¹
 ⁻¹-dist-· r r' ⦃ r∈Rˣ ⦄ ⦃ r'∈Rˣ ⦄ ⦃ rr'∈Rˣ ⦄ =
                 sym path ∙∙ cong (r ⁻¹ · r' ⁻¹ ·_) (rr'∈Rˣ .snd) ∙∙ (·Rid _)
  where
  path : r ⁻¹ · r' ⁻¹ · (r · r' · (r · r') ⁻¹) ≡ (r · r') ⁻¹
  path = r ⁻¹ · r' ⁻¹ · (r · r' · (r · r') ⁻¹)
       ≡⟨ ·Assoc _ _ _ ⟩
         r ⁻¹ · r' ⁻¹ · (r · r') · (r · r') ⁻¹
       ≡⟨ cong (λ x → r ⁻¹ · r' ⁻¹ · x · (r · r') ⁻¹) (·Comm _ _) ⟩
         r ⁻¹ · r' ⁻¹ · (r' · r) · (r · r') ⁻¹
       ≡⟨ cong (_· (r · r') ⁻¹) (sym (·Assoc _ _ _)) ⟩
         r ⁻¹ · (r' ⁻¹ · (r' · r)) · (r · r') ⁻¹
       ≡⟨ cong (λ x → r ⁻¹ · x · (r · r') ⁻¹) (·Assoc _ _ _) ⟩
         r ⁻¹ · (r' ⁻¹ · r' · r) · (r · r') ⁻¹
       ≡⟨ cong (λ x → r ⁻¹ · (x · r) · (r · r') ⁻¹) (·-linv _) ⟩
         r ⁻¹ · (1r · r) · (r · r') ⁻¹
       ≡⟨ cong (λ x → r ⁻¹ · x · (r · r') ⁻¹) (·Lid _) ⟩
         r ⁻¹ · r · (r · r') ⁻¹
       ≡⟨ cong (_· (r · r') ⁻¹) (·-linv _) ⟩
         1r · (r · r') ⁻¹
       ≡⟨ ·Lid _ ⟩
         (r · r') ⁻¹ ∎

 unitCong : {r r' : R} → r ≡ r' → ⦃ r∈Rˣ : r ∈ Rˣ ⦄ ⦃ r'∈Rˣ : r' ∈ Rˣ ⦄ → r ⁻¹ ≡ r' ⁻¹
 unitCong {r = r} {r' = r'} p ⦃ r∈Rˣ ⦄ ⦃ r'∈Rˣ ⦄ =
          PathPΣ (inverseUniqueness r' (r ⁻¹ , subst (λ x → x · r ⁻¹ ≡ 1r) p (r∈Rˣ .snd)) r'∈Rˣ) .fst

 ⁻¹-eq-elim : {r r' r'' : R} ⦃ r∈Rˣ : r ∈ Rˣ ⦄ → r' ≡ r'' · r → r' · r ⁻¹ ≡ r''
 ⁻¹-eq-elim {r = r} {r'' = r''} p = cong (_· r ⁻¹) p
                                  ∙ sym (·Assoc _ _ _)
                                  ∙ cong (r'' ·_) (·-rinv _)
                                  ∙ ·Rid _

-- some convenient notation
_ˣ : (R' : CommRing ℓ) → ℙ (R' .fst)
R' ˣ = Units.Rˣ R'

module CommRingHoms where
  open RingHoms

  idCommRingHom : (R : CommRing ℓ) → CommRingHom R R
  idCommRingHom R = idRingHom (CommRing→Ring R)

  compCommRingHom : (R S T : CommRing ℓ)
                  → CommRingHom R S → CommRingHom S T → CommRingHom R T
  compCommRingHom R S T = compRingHom {R = CommRing→Ring R} {CommRing→Ring S} {CommRing→Ring T}

  compIdCommRingHom : {R S : CommRing ℓ} (f : CommRingHom R S) → compCommRingHom R R S (idCommRingHom R) f ≡ f
  compIdCommRingHom = compIdRingHom

  idCompCommRingHom : {R S : CommRing ℓ} (f : CommRingHom R S) → compCommRingHom R S S f (idCommRingHom S) ≡ f
  idCompCommRingHom = idCompRingHom

  compAssocCommRingHom : {R S T U : CommRing ℓ} (f : CommRingHom R S) (g : CommRingHom S T) (h : CommRingHom T U) →
                         compCommRingHom R T U (compCommRingHom R S T f g) h ≡
                         compCommRingHom R S U f (compCommRingHom S T U g h)
  compAssocCommRingHom = compAssocRingHom

module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
 open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv)
 private A = fst A'
 open CommRingStr (snd A') renaming (_·_ to _·A_ ; 1r to 1a)
 open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv)
 open CommRingStr (snd B') renaming  ( _·_ to _·B_ ; 1r to 1b
                                     ; ·Lid to ·B-lid ; ·Rid to ·B-rid
                                     ; ·Assoc to ·B-assoc)

 private
   f = fst φ
 open IsRingHom (φ .snd)

 RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ
 RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1)

 φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄
               → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
 φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
  f (r ⁻¹ᵃ)                         ≡⟨ sym (·B-rid _) ⟩
  f (r ⁻¹ᵃ) ·B 1b                   ≡⟨ cong (f (r ⁻¹ᵃ) ·B_) (sym (·B-rinv _)) ⟩
  f (r ⁻¹ᵃ) ·B ((f r) ·B (f r) ⁻¹ᵇ) ≡⟨ ·B-assoc _ _ _ ⟩
  f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ   ≡⟨ cong (_·B (f r) ⁻¹ᵇ) (sym (pres· _ _)) ⟩
  f (r ⁻¹ᵃ ·A r) ·B (f r) ⁻¹ᵇ       ≡⟨ cong (λ x → f x ·B (f r) ⁻¹ᵇ) (·A-linv _) ⟩
  f 1a ·B (f r) ⁻¹ᵇ                 ≡⟨ cong (_·B (f r) ⁻¹ᵇ) (pres1) ⟩
  1b ·B (f r) ⁻¹ᵇ                   ≡⟨ ·B-lid _ ⟩
  (f r) ⁻¹ᵇ                         ∎

module Exponentiation (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 private R = fst R'

 -- introduce exponentiation
 _^_ : R → ℕ → R
 f ^ zero = 1r
 f ^ suc n = f · (f ^ n)

 infix 9 _^_

 -- and prove some laws
 1ⁿ≡1 : (n : ℕ) → 1r ^ n ≡ 1r
 1ⁿ≡1 zero = refl
 1ⁿ≡1 (suc n) = ·Lid _ ∙ 1ⁿ≡1 n

 ·-of-^-is-^-of-+ : (f : R) (m n : ℕ) → (f ^ m) · (f ^ n) ≡ f ^ (m +ℕ n)
 ·-of-^-is-^-of-+ f zero n = ·Lid _
 ·-of-^-is-^-of-+ f (suc m) n = sym (·Assoc _ _ _) ∙ cong (f ·_) (·-of-^-is-^-of-+ f m n)

 ^-ldist-· : (f g : R) (n : ℕ) → (f · g) ^ n ≡ (f ^ n) · (g ^ n)
 ^-ldist-· f g zero = sym (·Lid 1r)
 ^-ldist-· f g (suc n) = path
  where
  path : f · g · ((f · g) ^ n) ≡ f · (f ^ n) · (g · (g ^ n))
  path = f · g · ((f · g) ^ n)       ≡⟨ cong (f · g ·_) (^-ldist-· f g n) ⟩
         f · g · ((f ^ n) · (g ^ n)) ≡⟨ ·Assoc _ _ _ ⟩
         f · g · (f ^ n) · (g ^ n)   ≡⟨ cong (_· (g ^ n)) (sym (·Assoc _ _ _)) ⟩
         f · (g · (f ^ n)) · (g ^ n) ≡⟨ cong (λ r → (f · r) · (g ^ n)) (·Comm _ _) ⟩
         f · ((f ^ n) · g) · (g ^ n) ≡⟨ cong (_· (g ^ n)) (·Assoc _ _ _) ⟩
         f · (f ^ n) · g · (g ^ n)   ≡⟨ sym (·Assoc _ _ _) ⟩
         f · (f ^ n) · (g · (g ^ n)) ∎

 ^-rdist-·ℕ : (f : R) (n m : ℕ) → f ^ (n ·ℕ m) ≡ (f ^ n) ^ m
 ^-rdist-·ℕ f zero m = sym (1ⁿ≡1 m)
 ^-rdist-·ℕ f (suc n) m =  sym (·-of-^-is-^-of-+ f m (n ·ℕ m))
                        ∙∙ cong (f ^ m ·_) (^-rdist-·ℕ f n m)
                        ∙∙ sym  (^-ldist-· f (f ^ n) m)

-- like in Ring.Properties we provide helpful lemmas here
module CommRingTheory (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 private R = fst R'

 ·CommAssocl : (x y z : R) → x · (y · z) ≡ y · (x · z)
 ·CommAssocl x y z = ·Assoc x y z ∙∙ cong (_· z) (·Comm x y) ∙∙ sym (·Assoc y x z)

 ·CommAssocr : (x y z : R) → x · y · z ≡ x · z · y
 ·CommAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·Comm y z) ∙∙ ·Assoc x z y

 ·CommAssocr2 : (x y z : R) → x · y · z ≡ z · y · x
 ·CommAssocr2 x y z = ·CommAssocr _ _ _ ∙∙ cong (_· y) (·Comm _ _) ∙∙ ·CommAssocr _ _ _

 ·CommAssocSwap : (x y z w : R) → (x · y) · (z · w) ≡ (x · z) · (y · w)
 ·CommAssocSwap x y z w =
   ·Assoc (x · y) z w ∙∙ cong (_· w) (·CommAssocr x y z) ∙∙ sym (·Assoc (x · z) y w)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An implementation of the ring solver that requires you to manually
-- pass the equation you wish to solve.
------------------------------------------------------------------------

-- You'll probably want to use `Tactic.RingSolver` instead which uses
-- reflection to automatically extract the equation.

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

open import Tactic.RingSolver.Core.AlmostCommutativeRing

module Tactic.RingSolver.NonReflective
  {ℓ₁ ℓ₂} (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
  (let open AlmostCommutativeRing ring)
  where

open import Algebra.Morphism
open import Function
open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
open import Data.Maybe.Base
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base using (ℕ)
open import Data.Product
open import Data.Vec hiding (_⊛_)
open import Data.Vec.N-ary

open import Tactic.RingSolver.Core.Polynomial.Parameters
open import Tactic.RingSolver.Core.Expression public

module Ops where
  zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x
  zero-homo x _ with 0≟ x
  zero-homo x _  | just p = p
  zero-homo x () | nothing

  homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
  homo = record
    { from = record
      { rawRing = AlmostCommutativeRing.rawRing ring
      ; isZero  = λ x → is-just (0≟ x)
      }
    ; to = record
      { isAlmostCommutativeRing = record
          { isCommutativeSemiring = isCommutativeSemiring
          ; -‿cong       = -‿cong
          ; -‿*-distribˡ = -‿*-distribˡ
          ; -‿+-comm     = -‿+-comm
          }
      }
    ; morphism      = -raw-almostCommutative⟶ ring
    ; Zero-C⟶Zero-R = zero-homo
    }
  open Eval rawRing id public

  open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)

  norm : ∀ {n} → Expr Carrier n → Poly n
  norm (Κ x)   = κ x
  norm (Ι x)   = ι x
  norm (x ⊕ y) = norm x ⊞ norm y
  norm (x ⊗ y) = norm x ⊠ norm y
  norm (⊝ x)   = ⊟ norm x
  norm (x ⊛ i) = norm x ⊡ i

  ⟦_⇓⟧ : ∀ {n} → Expr Carrier n → Vec Carrier n → Carrier
  ⟦ expr ⇓⟧ = ⟦ norm expr ⟧ₚ where

    open import Tactic.RingSolver.Core.Polynomial.Semantics homo
      renaming (⟦_⟧ to ⟦_⟧ₚ)

  correct : ∀ {n} (expr : Expr Carrier n) ρ → ⟦ expr ⇓⟧ ρ ≈ ⟦ expr ⟧ ρ
  correct {n = n} = go
    where
    open import Tactic.RingSolver.Core.Polynomial.Homomorphism homo

    go : ∀ (expr : Expr Carrier n) ρ → ⟦ expr ⇓⟧ ρ ≈ ⟦ expr ⟧ ρ
    go (Κ x)   ρ = κ-hom x ρ
    go (Ι x)   ρ = ι-hom x ρ
    go (x ⊕ y) ρ = ⊞-hom (norm x) (norm y) ρ ⟨ trans ⟩ (go x ρ ⟨ +-cong ⟩ go y ρ)
    go (x ⊗ y) ρ = ⊠-hom (norm x) (norm y) ρ ⟨ trans ⟩ (go x ρ ⟨ *-cong ⟩ go y ρ)
    go (⊝ x)   ρ = ⊟-hom (norm x) ρ   ⟨ trans ⟩ -‿cong (go x ρ)
    go (x ⊛ i) ρ = ⊡-hom (norm x) i ρ ⟨ trans ⟩ pow-cong i (go x ρ)

  open import Relation.Binary.Reflection setoid Ι ⟦_⟧ ⟦_⇓⟧ correct public

solve : ∀ (n : ℕ) →
        (f : N-ary n (Expr Carrier n) (Expr Carrier n × Expr Carrier n)) →
        Eqʰ n _≈_ (curryⁿ (Ops.⟦_⇓⟧ (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⇓⟧ (proj₂ (Ops.close n f)))) →
        Eq  n _≈_ (curryⁿ (Ops.⟦_⟧  (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⟧  (proj₂ (Ops.close n f))))
solve = Ops.solve
{-# INLINE solve #-}

_⊜_ : ∀ (n : ℕ) →
      Expr Carrier n →
      Expr Carrier n →
      Expr Carrier n × Expr Carrier n
_⊜_ _ = _,_
{-# INLINE _⊜_ #-}


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

open import OscarPrelude
open import Problem
open import IsLiteralProblem

record LiteralProblem : Set
 where
  constructor ⟨_⟩
  field
    {problem} : Problem
    isLiteralProblem : IsLiteralProblem problem

open LiteralProblem public

instance EqLiteralProblem : Eq LiteralProblem
EqLiteralProblem = {!!}

open import 𝓐ssertion

instance 𝓐ssertionLiteralProblem : 𝓐ssertion LiteralProblem
𝓐ssertionLiteralProblem = record {}

open import HasSatisfaction

instance HasSatisfactionLiteralProblem : HasSatisfaction LiteralProblem
HasSatisfaction._⊨_ HasSatisfactionLiteralProblem I 𝔓 = I ⊨ problem 𝔓

open import HasDecidableValidation

instance HasDecidableValidationLiteralProblem : HasDecidableValidation LiteralProblem
HasDecidableValidationLiteralProblem = {!!}


text:
module LC.Subst.Var where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary

--------------------------------------------------------------------------------
-- variable binding

data Binding : ℕ → ℕ → Set where
  Free  : ∀ {n x} → (n≤x : n ≤ x) → Binding n x
  Bound : ∀ {n x} → (n>x : n > x) → Binding n x

inspectBinding : ∀ n x → Binding n x
inspectBinding n x with n ≤? x
... | yes p = Free p
... | no ¬p = Bound (≰⇒> ¬p)

--------------------------------------------------------------------------------
-- lifiting variables

lift-var : (n i x : ℕ) → ℕ
lift-var n i x with inspectBinding n x
... | Free  _ = i + x      -- free
... | Bound _ =     x      -- bound

--------------------------------------------------------------------------------
-- properties of lift-var

open import Relation.Binary.PropositionalEquality hiding ([_])

module EQ where
    open ≡-Reasoning

    twist : ∀ l m n → l + (m + n) ≡ m + (l + n)
    twist l m n =
        begin
            l + (m + n)
        ≡⟨ sym (+-assoc l m n) ⟩
            l + m + n
        ≡⟨ cong (_+ n) (+-comm l m) ⟩
            m + l + n
        ≡⟨ +-assoc m l n ⟩
            m + (l + n)
        ∎

    l+m+n≡m+x : ∀ l m n x → l + n ≡ x → l + m + n ≡ m + x
    l+m+n≡m+x l m n x l+n≡x =
        begin
            l + m + n
        ≡⟨ +-assoc l m n ⟩
            l + (m + n)
        ≡⟨ twist l m n ⟩
            m + (l + n)
        ≡⟨ cong (m +_) l+n≡x ⟩
            m + x
        ∎

module INEQ where
    open ≤-Reasoning

    m+n≰x+m : ∀ {m n x} → n ≰ x → m + n > x + m
    m+n≰x+m {m} {n} {x} n≰x = begin
            suc x + m
        ≡⟨ +-comm (suc x) m ⟩
            m + suc x
        ≤⟨ +-monoʳ-≤ m (≰⇒> n≰x) ⟩
            m + n
        ∎

    m+n≤x+m : ∀ {m n x} → n ≤ x → m + n ≤ x + m
    m+n≤x+m {m} {n} {x} n≤x = begin
            m + n
        ≤⟨ +-monoʳ-≤ m n≤x ⟩
            m + x
        ≡⟨ +-comm m x ⟩
            x + m
        ∎
    l+n≤n+i+x : ∀ l n i x → l ≤ x → l + n ≤ n + i + x
    l+n≤n+i+x l n i x l≤x =
        begin
            l + n
        ≤⟨ +-monoˡ-≤ n l≤x ⟩
            x + n
        ≤⟨ m≤n+m (x + n) i ⟩
            i + (x + n)
        ≡⟨ cong (i +_) (+-comm x n) ⟩
            i + (n + x)
        ≡⟨ sym (+-assoc i n x) ⟩
            i + n + x
        ≡⟨ cong (_+ x) (+-comm i n) ⟩
            n + i + x
        ∎

    l+m+n≤m+x : ∀ l m n x → l + n ≤ x → l + m + n ≤ m + x
    l+m+n≤m+x l m n x l+n≤x =
        begin
            l + m + n
        ≡⟨ +-assoc l m n ⟩
            l + (m + n)
        ≡⟨ EQ.twist l m n ⟩
            m + (l + n)
        ≤⟨ +-monoʳ-≤ m l+n≤x ⟩
            m + x
        ∎

    l+m+n>m+x : ∀ l m n x → l + n > x → l + m + n > m + x
    l+m+n>m+x l m n x l+n>x =
        begin
            suc m + x
        ≡⟨ sym (+-suc m x) ⟩
            m + suc x
        ≤⟨ +-monoʳ-≤ m l+n>x ⟩
            m + (l + n)
        ≡⟨ EQ.twist m l n ⟩
            l + (m + n)
        ≡⟨ sym (+-assoc l m n) ⟩
            l + m + n
        ∎

    l+m+n>x : ∀ l m n x → l > x → l + m + n > x
    l+m+n>x l m n x l>x =
        begin
            suc x
        ≤⟨ l>x ⟩
            l
        ≤⟨ m≤m+n l m ⟩
            l + m
        ≤⟨ m≤m+n (l + m) n ⟩
            l + m + n
        ∎

open import Relation.Nullary.Negation using (contradiction)
open ≡-Reasoning

lift-var-≤ : ∀ {n i x} → n ≤ x → lift-var n i x ≡ i + x
lift-var-≤ {n} {i} {x} n≤x with inspectBinding n x
... | Free  ≤x = refl
... | Bound >x = contradiction n≤x (<⇒≱ >x)

lift-var-> : ∀ {n i x} → n > x → lift-var n i x ≡ x
lift-var-> {n} {i} {x} n>x with inspectBinding n x
... | Free  ≤x = contradiction n>x (≤⇒≯ ≤x)
... | Bound >x = refl

-- lift-var-+ : ∀ n i x m → lift-var (m + n) i (x + m) ≡ lift-var n i x + m
-- lift-var-+ n i x m with inspectBinding n x
-- ... | Bound >x  =
--         lift-var (m + n) i (x + m)
--     ≡⟨ lift-var-> (INEQ.m+n≰x+m (<⇒≱ >x)) ⟩
--         x + m
--     ∎
-- ... | Free  ≤x  =
--         lift-var (m + n) i (x + m)
--     ≡⟨ lift-var-≤ {m + n} {i} {x + m} (INEQ.m+n≤x+m ≤x)  ⟩
--         i + (x + m)
--     ≡⟨ sym (+-assoc i x m) ⟩
--         i + x + m
--     ∎

--             lift-var (l + n) i
--        ∙ --------------------------> ∙
--        |                             |
--        |                             |
--   lift-var l m                  lift-var l m
--        |                             |
--        ∨                             ∨
--        ∙ --------------------------> ∙
--            lift-var (l + m + n) i

lift-var-lift-var : ∀ l m n i x → lift-var l m (lift-var (l + n) i x) ≡ lift-var (l + m + n) i (lift-var l m x)
lift-var-lift-var l m n i x with inspectBinding l x | inspectBinding (l + n) x
... | Free l≤x | Free l+n≤x =
        lift-var l m (i + x)
    ≡⟨ lift-var-≤ (≤-trans l≤x (m≤n+m x i)) ⟩
        m + (i + x)
    ≡⟨ EQ.twist m i x ⟩
        i + (m + x)
    ≡⟨ sym (lift-var-≤ (INEQ.l+m+n≤m+x l m n x l+n≤x)) ⟩
        lift-var (l + m + n) i (m + x)
    ∎
... | Free l≤x | Bound l+n>x =
        lift-var l m x
    ≡⟨ lift-var-≤ l≤x ⟩
        m + x
    ≡⟨ sym (lift-var-> (INEQ.l+m+n>m+x l m n x l+n>x)) ⟩
        lift-var (l + m + n) i (m + x)
    ∎
... | Bound l>x | Free l+n≤x = contradiction (≤-trans (m≤m+n l n) l+n≤x) (<⇒≱ l>x)
... | Bound l>x | Bound l+n>x =
        lift-var l m x
    ≡⟨ lift-var-> l>x ⟩
        x
    ≡⟨ sym (lift-var-> (INEQ.l+m+n>x l m n x l>x)) ⟩
        lift-var (l + m + n) i x
    ∎

--             lift-var l (n + i)
--        ∙ --------------------------> ∙
--        |                             |
--        |                             |
--   lift-var l (n + m + i)      lift-var (l + n) m
--        |                             |
--        ∨                             ∨
--        ∙ --------------------------> ∙
--

lift-var-lemma : ∀ l m n i x → lift-var l (n + m + i) x ≡ lift-var (l + n) m (lift-var l (n + i) x)
lift-var-lemma l m n i x with inspectBinding l x
... | Free n≤x =
  begin
      n + m + i + x
  ≡⟨ cong (λ w → w + i + x) (+-comm n m) ⟩
      m + n + i + x
  ≡⟨ +-assoc (m + n) i x ⟩
      m + n + (i + x)
  ≡⟨ +-assoc m n (i + x) ⟩
    m + (n + (i + x))
  ≡⟨ cong (m +_) (sym (+-assoc n i x)) ⟩
      m + (n + i + x)
  ≡⟨ sym (lift-var-≤ {l + n} {m} {n + i + x} (INEQ.l+n≤n+i+x l n i x n≤x)) ⟩
      lift-var (l + n) m (n + i + x)
  ∎
... | Bound n>x =
  begin
      x
  ≡⟨ sym (lift-var-> {l + n} {m} {x} (≤-trans n>x (m≤m+n l n))) ⟩
      lift-var (l + n) m x
  ∎

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


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

module WithoutK4 where

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

foo : (f : {A : Set} → A → A) {A : Set} (x y : A) →
      x ≡ f y → f y ≡ x
foo f .(f y) y refl = refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- {-# OPTIONS --safe #-}
module Time where

open import Map
open import Relation.Binary.PropositionalEquality
open import Data.String using (String)
open import Data.Nat
open import Data.Nat.Base using (_≤_)
open import Data.Bool using (true ; false)
open import Data.Bool.Base using (if_then_else_)
open import Data.Maybe using (Maybe; just; nothing)
open import Agda.Builtin.Unit
open import Data.Empty
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_)
open import Data.List
open import Data.Nat.Properties
open import Language
open import Function.Base using (_$_)

max : ∀ (m n : ℕ) → ℕ
max m n with (m ≤? n)
... | false Relation.Nullary.because _ = m
... | true Relation.Nullary.because _ = n

taeval : (Γ : (String → ℕ)) → (Aexp {ℕ}) → ℕ
taeval Γ (a +` a₁) = taeval Γ a + taeval Γ a₁ + (Γ "+")
taeval Γ (a -` a₁) = taeval Γ a + taeval Γ a₁ + (Γ "-")
taeval Γ (a *` a₁) = taeval Γ a + taeval Γ a₁ + (Γ "*")
taeval Γ (Avar x) = 1           -- Just look up in memory assuming 1
                                -- clock cycle
taeval Γ (Anum x) = 1           -- Just look up in mem is 1 clock cycle

tbeval : (Γ : (String → ℕ)) → (Bexp {ℕ}) → ℕ
tbeval Γ TRUE = Γ "TRUE"
tbeval Γ FALSE = Γ "FALSE"
tbeval Γ (x1 <` x2) = aeval Γ x1 + aeval Γ x2 + (Γ "<")
tbeval Γ (x1 >` x2) = aeval Γ x1 + aeval Γ x2 + (Γ ">")
tbeval Γ (x1 ≤` x2) = aeval Γ x1 + aeval Γ x2 + (Γ "≤")
tbeval Γ (x1 ≥` x2) = aeval Γ x1 + aeval Γ x2 + (Γ "≥")
tbeval Γ (x1 ≡` x2) = aeval Γ x1 + aeval Γ x2 + (Γ "≡")
tbeval Γ (¬` b) = tbeval Γ b + (Γ "NOT")
tbeval Γ (b &&` b₁) = tbeval Γ b + tbeval Γ b₁ + (Γ "AND")
tbeval Γ (b ||` b₁) = tbeval Γ b + tbeval Γ b₁ + (Γ "OR")

-- Making the tuple type needed to hold the program
data TProgTuple {A : Set} : Set where
  _,_,_,_ : (a : ATuple) → (r : RTuple) → (c : Cmd {A}) → (cmt : ℕ) → TProgTuple

-- Getting stuff from the TProgTuple
getProgCmdT : {A : Set} → (p : Maybe (TProgTuple {A})) → Cmd {A}
getProgCmdT (just (_ , _ , c , _)) = c
getProgCmdT nothing = SKIP       -- Dangerous

getProgArgsT : {A : Set} → (p : Maybe (TProgTuple {A})) → ATuple
getProgArgsT (just (a , _ , _ , _)) = a
getProgArgsT nothing = Arg "VOID"

getProgRetsT : {A : Set} → (p : Maybe (TProgTuple {A})) → RTuple
getProgRetsT (just (_ , r , _ , _)) = r
getProgRetsT nothing = Ret "VOID"

getProgTimeT : {A : Set} → (p : Maybe (TProgTuple {A})) → ℕ
getProgTimeT (just (_ , _ , _ , t)) = t
getProgTimeT nothing = 0

data _,_=[_]=>ᴬ_  (Γ : (String → ℕ)) : ℕ → (ATuple) → ℕ → Set where

  hd : ∀ (W : ℕ) → ∀ (v : String) →
       Γ , W =[ Arg v ]=>ᴬ (W + (Γ "arg-copy"))

  tl : (l r : ATuple) → (W W' W'' : ℕ) →
       (Γ , W =[ l ]=>ᴬ (W + W')) → (Γ , W + W' =[ r ]=>ᴬ (W + W' + W'')) →
        -----------------------------------------------------------
        Γ , W =[ (l ,` r) ]=>ᴬ (W + W' + W'')

numargs : ∀ (args : ATuple) → ℕ
numargs (Arg v) = 1
numargs (args ,` args₁) = numargs args + numargs args₁

-- soundness theorem for arg copy
args-sound : ∀ (Γ : (String → ℕ)) → ∀ (args : ATuple) → (W W' : ℕ)
             → (Γ , W =[ args ]=>ᴬ W')
             → (W + numargs args * (Γ "arg-copy")) ≡ W'
args-sound Γ .(Arg v) W .(W + Γ "arg-copy") (hd .W v)
  rewrite +-comm (Γ "arg-copy") 0 = refl
args-sound Γ .(l ,` r) W .(W + W' + W'') (tl l r .W W' W'' cmd cmd₁)
  with (Γ "arg-copy") in eq
... | u rewrite *-distribʳ-+ u (numargs l) (numargs r)
    | +-comm W (((numargs l) * u) + ((numargs r) * u))
    | +-comm ((numargs l) * u) ((numargs r) * u)
    | +-assoc ((numargs r) * u) ((numargs l) * u) W
    | +-comm ((numargs l) * u) W
    | +-comm ((numargs r) * u) (W + ((numargs l) * u))
    with args-sound Γ l W (W + W') cmd
... | j with args-sound Γ r (W + W') (W + W' + W'') cmd₁
... | k with +-cancelˡ-≡ W j | +-cancelˡ-≡ (W + W') k | eq
... | refl | refl | refl = refl

data _,_=[_]=>ᴿ_  (Γ : (String →  ℕ)) : ℕ → RTuple → ℕ  → Set where
  hd : ∀ (W : ℕ) → ∀ (v : String) →
       Γ , W =[ Ret v ]=>ᴿ (W + (Γ "ret-copy"))

  tl : (l r : RTuple) → (W W' W'' : ℕ) →
       (Γ , W =[ l ]=>ᴿ (W + W')) → (Γ , W + W' =[ r ]=>ᴿ (W + W' + W'')) →
        -----------------------------------------------------------
        Γ , W =[ (l ,` r) ]=>ᴿ (W + W' + W'')

numrets : ∀ (rets : RTuple) → ℕ
numrets (Ret v) = 1
numrets (rets ,` rets₁) = numrets rets + numrets rets₁

-- soundness theorem for ret copy
rets-sound : ∀ (Γ : (String → ℕ)) → ∀ (rets : RTuple) → (W W' : ℕ)
             → Γ , W =[ rets ]=>ᴿ W'
             → (W + numrets rets * (Γ "ret-copy")) ≡ W'
rets-sound Γ .(Ret v) W .(W + Γ "ret-copy") (hd .W v)
  rewrite +-comm (Γ "ret-copy") 0 = refl
rets-sound Γ .(l ,` r) W .(W + W' + W'') (tl l r .W W' W'' cmd cmd₁)
  with (Γ "ret-copy") in eq
... | u rewrite *-distribʳ-+ u (numrets l) (numrets r)
    | +-comm W (((numrets l) * u) + ((numrets r) * u))
    | +-comm ((numrets l) * u) ((numrets r) * u)
    | +-assoc ((numrets r) * u) ((numrets l) * u) W
    | +-comm ((numrets l) * u) W
    | +-comm ((numrets r) * u) (W + ((numrets l) * u))
    with rets-sound Γ l W (W + W') cmd
... | j with rets-sound Γ r (W + W') (W + W' + W'') cmd₁
... | k with +-cancelˡ-≡ W j | +-cancelˡ-≡ (W + W') k | eq
... | refl | refl | refl = refl

mutual
-- Semantics of time from here
 data _,_,_=[_]=>_ (Γ : (String → Maybe (TProgTuple {ℕ}))) (st : String → ℕ) :
           ℕ → Cmd {ℕ} → ℕ → Set where
  TSKIP : ∀ (W : ℕ) → Γ , st , W =[ SKIP ]=> (W + 0)

  TASSIGN : ∀ (X : String) → ∀ (n : ℕ) → ∀ (e : Aexp {ℕ})
           → ∀ (W : ℕ) →
           ---------------------------------
           Γ , st ,  W =[ (Var X := e) ]=> (W + (taeval st e) + (st "store"))

  TSEQ : ∀ (c1 c2 : Cmd {ℕ})
        → ∀ (W W' W'' : ℕ)
        → Γ , st , W =[ c1 ]=> (W + W')
        → Γ , st , (W + W') =[ c2 ]=> (W + (W' + W'')) →
        --------------------------------------------
        Γ , st ,  W =[ c1 ; c2 ]=> (W + (W' + W''))

  -- XXX: Hack, st contains both exec time and state!
  TIFT : (n1 : ℕ) → (b : Bexp {ℕ}) →
        (t e : Cmd {ℕ}) → ∀ (W W' W'' : ℕ)
        → (beval st b ≡ true)
        → Γ , st , W =[ t ]=> (W + W')
        → Γ , st , W =[ e ]=> (W + W'')
        → Γ , st , W =[ (IF b THEN t ELSE e END) ]=>
          (W + W' + (tbeval st b))

  TIFE : (n1 : ℕ) → (b : Bexp {ℕ}) →
        (t e : Cmd {ℕ}) → ∀ (W W' W'' : ℕ)
        → (beval st b ≡ false)
        → Γ , st , W =[ t ]=> (W + W')
        → Γ , st , W =[ e ]=> (W + W'')
        → Γ , st , W =[ (IF b THEN t ELSE e END) ]=>
          (W +  W'' + (tbeval st b))

  TLF :  (b : Bexp {ℕ}) → (c : Cmd {ℕ}) →
        beval st b ≡ false →
        ∀ (W : ℕ) →
        -----------------------------------------------------------
        Γ , st , W =[ (WHILE b DO c END) ]=>
        (W + 0 + (tbeval st b))

  TLT :  (b : Bexp {ℕ}) → (c : Cmd {ℕ}) →
        beval st b ≡ true → ∀ (W W' : ℕ) →
        -----------------------------------------------------------
        Γ , st , W =[ c ]=> (W + W') →
        Γ , st , W =[ (WHILE b DO c END) ]=>
        (W + ((st "loop-count") * (W' + (tbeval st b))) + (tbeval st b))

 -- CEX : ∀ (f : FuncCall {ℕ}) → ∀ (st st' : (String → ℕ))
 --       → Γ , st =[ f ]=>ᶠ st'
 --       -----------------------------------------------------------
 --       → Γ , st =[ EXEC f ]=> st'

 data _,_,_=[_]=>ᶠ_ (Γ : String → (Maybe (TProgTuple {ℕ})))
                    (st : String → ℕ) :
                    ℕ → FuncCall {ℕ} → ℕ → Set where

  Base : ∀ (fname : String) →        -- name of the function
         ∀ (W W' W'' W''' : ℕ)

         -- time to put args on function stack
         → st , W =[ getProgArgsT (Γ fname) ]=>ᴬ (W + W')

         -- Proof that WCET is what we have in the tuple
         → (wcet-is : (getProgTimeT (Γ fname)) ≡ W'')
         -- time to run the function
         → Γ , st , (W + W') =[ getProgCmdT (Γ fname) ]=> (W + W' + W'')

         -- copying ret values back on caller' stack
         → st , (W + W' + W'')
              =[ getProgRetsT (Γ fname) ]=>ᴿ (W + W' + W'' + W''')

         -----------------------------------------------------------
         → Γ , st , W =[ < getProgRetsT (Γ fname) >:=
             fname < getProgArgsT (Γ fname) > ]=>ᶠ (W + W' + W'' + W''')

  PAR : ∀ (l r : FuncCall {ℕ}) → ∀ (W X1 X2 : ℕ)
        → Γ , st , W =[ l ]=>ᶠ (W + X1)
        → Γ , st , W =[ r ]=>ᶠ (W + X2)
        -----------------------------------------------------------
        → Γ , st , W =[ l ||` r ]=>ᶠ (W + (max X1 X2) + ((2 * (st "fork"))
                                        + (2 * (st "join"))))

-- Soundness theorem for SKIP WCET rule
skip-sound : (Γ : String → Maybe (TProgTuple {ℕ}))
           → (Γᵗ : String → ℕ)  -- map of labels to execution times
           → ∀ (W W' X : ℕ) → (cmd : Γ , Γᵗ , W =[ SKIP ]=> W')
           → (W ≡ X) → (W' ≡ X)
skip-sound Γ Γᵗ W .(W + 0) .W (TSKIP .W) refl rewrite +-comm W 0 = refl

-- Soundness theorem for Assign WCET rule
assign-sound : (Γ : String → Maybe (TProgTuple {ℕ}))
             → (Γᵗ : (String → ℕ))
             → (S : String) → (e : Aexp {ℕ})
             → (W W' : ℕ) → (cmd : Γ , Γᵗ , W =[ Var S := e ]=> W')
             → (W' ≡ W + (taeval Γᵗ e) + (Γᵗ "store"))
assign-sound Γ Γᵗ S e W .(W + taeval Γᵗ e + Γᵗ "store") (TASSIGN .S n .e .W)
  = refl

-- Deterministic exec
Δ-exec : (Γ : String → Maybe (TProgTuple {ℕ}))
         → (Γᵗ : String → ℕ)
         → ∀ (W W' W'' : ℕ) → (c1 : Cmd {ℕ})
         → (Γ , Γᵗ , W =[ c1 ]=> W')
         → (Γ , Γᵗ , W =[ c1 ]=> W'')
         → W' ≡ W''
Δ-exec Γ Γᵗ W .(W + taeval Γᵗ e + Γᵗ "store")
  .(W + taeval Γᵗ e + Γᵗ "store") (Var X := e) (TASSIGN .X n₁ .e .W)
  (TASSIGN .X n .e .W) = refl
Δ-exec Γ Γᵗ W .(W + 0) .(W + 0) .SKIP (TSKIP .W) (TSKIP .W) = refl
Δ-exec Γ Γᵗ W .(W + (W' + W''')) .(W + (W'' + W''''))
 .(c1 ; c2) (TSEQ c1 c2 .W W' W''' p1 p3) (TSEQ .c1 .c2 .W W'' W'''' p2 p4)
 with Δ-exec Γ Γᵗ W (W + W') (W + W'') c1 p1 p2
... | r with +-cancelˡ-≡ W r
... | refl
 with Δ-exec Γ Γᵗ (W + W') (W + (W' + W''')) (W + (W' + W'''')) c2 p3 p4
... | rr with +-cancelˡ-≡ W rr
... | rm with +-cancelˡ-≡ W' rm
... | refl = refl
Δ-exec Γ Γᵗ W .(W + 0 + tbeval Γᵗ b)
  .(W + 0 + tbeval Γᵗ b) WHILE b DO c END (TLF .b .c x .W)
  (TLF .b .c x₁ .W) = refl
Δ-exec Γ Γᵗ W .(W + Γᵗ "loop-count" * (W' + tbeval Γᵗ b) + _)
  .(W + 0 + tbeval Γᵗ b) WHILE b DO c END (TLT .b .c x .W W' x₂)
  (TLF .b .c x₁ .W) = ⊥-elim (contradiction-lemma b Γᵗ x x₁)
Δ-exec Γ Γᵗ W .(W + 0 + tbeval Γᵗ b)
  .(W + Γᵗ "loop-count" * (W'' + tbeval Γᵗ b) + _) WHILE b DO c END
  (TLF .b .c x .W) (TLT .b .c x₁ .W W'' x₂)
  = ⊥-elim (contradiction-lemma b Γᵗ x₁ x)
Δ-exec Γ Γᵗ W .(W + Γᵗ "loop-count" * (W' + tbeval Γᵗ b) + _)
  .(W + Γᵗ "loop-count" * (W'' + tbeval Γᵗ b) + _) WHILE b DO c END
  (TLT .b .c x .W W' x₃) (TLT .b .c x₁ .W W'' x₂)
  with Δ-exec Γ Γᵗ W (W + W') (W + W'') c x₃ x₂
... | l with +-cancelˡ-≡ W l
... | refl = refl
Δ-exec Γ Γᵗ W .(W + W' + tbeval Γᵗ b)
  .(W + W'' + tbeval Γᵗ b) IF b THEN t ELSE e END
  (TIFT n2 .b .t .e .W W' W'''' x x₄ x₅)
  (TIFT n1 .b .t .e .W W'' W''' x₁ x₂ x₃)
  with Δ-exec Γ Γᵗ W (W + W') (W + W'') t x₄ x₂
... | y with +-cancelˡ-≡ W y
... | refl = refl
Δ-exec Γ Γᵗ W .(W + W'''' + tbeval Γᵗ b)
  .(W + W'' + tbeval Γᵗ b) IF b THEN t ELSE e END
  (TIFE n2 .b .t .e .W W' W'''' x x₄ x₅)
  (TIFT n1 .b .t .e .W W'' W''' x₁ x₂ x₃)
  = ⊥-elim (contradiction-lemma b Γᵗ x₁ x)
Δ-exec Γ Γᵗ W .(W + W' + tbeval Γᵗ b)
  .(W + W''' + tbeval Γᵗ b) IF b THEN t ELSE e END
  (TIFT n2 .b .t .e .W W' W'''' x x₄ x₅)
  (TIFE n1 .b .t .e .W W'' W''' x₁ x₂ x₃)
  = ⊥-elim (contradiction-lemma b Γᵗ x x₁)
Δ-exec Γ Γᵗ W .(W + W'''' + tbeval Γᵗ b)
  .(W + W''' + tbeval Γᵗ b) IF b THEN t ELSE e END
  (TIFE n2 .b .t .e .W W' W'''' x x₄ x₅)
  (TIFE n1 .b .t .e .W W'' W''' x₁ x₂ x₃)
  with Δ-exec Γ Γᵗ W (W + W''') (W + W'''') e x₃ x₅
... | y with +-cancelˡ-≡ W y
... | refl = refl

-- Deterministic execution of a function
Δ-exec-func : (Γ : String → Maybe (TProgTuple {ℕ}))
              → (Γᵗ : String → ℕ) → (l : FuncCall {ℕ})
              → (W W' W'' : ℕ)
              → Γ , Γᵗ , W =[ l ]=>ᶠ W'
              → Γ , Γᵗ , W =[ l ]=>ᶠ W''
              → W' ≡ W''
Δ-exec-func Γ Γᵗ
  .(< getProgRetsT (Γ fname) >:= fname < getProgArgsT (Γ fname) >) W
  .(W + W' + getProgTimeT (Γ fname) + W'''')
  .(W + W'' + getProgTimeT (Γ fname) + W'''''')
  (Base fname .W W' .(getProgTimeT (Γ fname)) W'''' x refl x₁ x₂)
  (Base .fname .W W'' .(getProgTimeT (Γ fname)) W'''''' x₃ refl x₄ x₅)
  with args-sound Γᵗ (getProgArgsT (Γ fname)) W (W + W') x
  | args-sound Γᵗ (getProgArgsT (Γ fname)) W (W + W'') x₃
  | rets-sound Γᵗ (getProgRetsT (Γ fname)) (W + W' + getProgTimeT (Γ fname))
    (W + W' + getProgTimeT (Γ fname) + W'''') x₂
  | rets-sound Γᵗ (getProgRetsT (Γ fname)) (W + W'' + getProgTimeT (Γ fname))
    (W + W'' + getProgTimeT (Γ fname) + W'''''') x₅
... | l | l1 | r1 | r2
  with +-cancelˡ-≡ W l | +-cancelˡ-≡ W l1
... | refl | refl with +-cancelˡ-≡
  (W + numargs (getProgArgsT (Γ fname)) * Γᵗ "arg-copy"
  + getProgTimeT (Γ fname)) r2
... | refl with +-cancelˡ-≡
  (W + numargs (getProgArgsT (Γ fname)) * Γᵗ "arg-copy"
  + getProgTimeT (Γ fname)) r1
... | refl = refl
Δ-exec-func Γ Γᵗ .(l ||` r) W
  .(W + max X1 X2 + (2 * Γᵗ "fork" + 2 * Γᵗ "join"))
  .(W + max X3 X4 + (2 * Γᵗ "fork" + 2 * Γᵗ "join"))
  (PAR l r .W X1 X2 e1 e3) (PAR .l .r .W X3 X4 e2 e4)
  with Δ-exec-func Γ Γᵗ l W (W + X1) (W + X3) e1 e2
  | Δ-exec-func Γ Γᵗ r W (W + X2) (W + X4) e3 e4
... | m | y with +-cancelˡ-≡ W m | +-cancelˡ-≡ W y
... | refl | refl = refl

skip-cancel : ∀ (Γ : String → Maybe (TProgTuple {ℕ}))
               → (Γᵗ : String → ℕ)
               → ∀ (W1 W2 X1 X2 : ℕ)
               → (Γ , Γᵗ , W1 =[ SKIP ]=> (W1 + X1))
               → (Γ , Γᵗ , W2 =[ SKIP ]=> (W2 + X2))
               → X1 ≡ X2
skip-cancel Γ Γᵗ W1 W2 X1 X2 p1 p2 with (W1 + X1) in eq1
skip-cancel Γ Γᵗ W1 W2 X1 X2 (TSKIP .W1) p2 | .(W1 + 0)
  with +-cancelˡ-≡ W1 eq1
skip-cancel Γ Γᵗ W1 W2 X1 X2 (TSKIP .W1) p2 | .(W1 + 0) | refl
  with (W2 + X2) in eq2
skip-cancel Γ Γᵗ W1 W2 _ X2 (TSKIP .W1) (TSKIP .W2)
  | .(W1 + _) | refl | .(W2 + 0) with +-cancelˡ-≡ W2 eq2
... | refl = refl

assign-cancel : ∀ (Γ : String → Maybe (TProgTuple {ℕ}))
               → (Γᵗ : String → ℕ)
               → ∀ (W1 W2 X1 X2 : ℕ)
               → (S : String) → (e : Aexp {ℕ})
               → (Γ , Γᵗ , W1 =[ Var S := e ]=> (W1 + X1))
               → (Γ , Γᵗ , W2 =[ Var S := e ]=> (W2 + X2))
               → X1 ≡ X2
assign-cancel Γ Γᵗ W1 W2 X1 X2 S e cmd1 cmd2 with (W1 + X1) in eq1
  | (W2 + X2) in eq2
assign-cancel Γ Γᵗ W1 W2 X1 X2 S e (TASSIGN .S n .e .W1)
  (TASSIGN .S n₁ .e .W2) | .(W1 + taeval Γᵗ e + Γᵗ "store")
  | .(W2 + taeval Γᵗ e + Γᵗ "store")
  rewrite +-assoc W1 (taeval Γᵗ e) (Γᵗ "store")
  | +-assoc W2 (taeval Γᵗ e) (Γᵗ "store")
  with +-cancelˡ-≡ W1 eq1 | +-cancelˡ-≡ W2 eq2
... | refl | refl = refl

loop-cancel : ∀ (Γ : String → Maybe (TProgTuple {ℕ}))
               → (Γᵗ : String → ℕ)
               → ∀ (W1 W2 X1 X2 : ℕ)
               → (b : Bexp {ℕ})
               → (c : Cmd {ℕ})
               → (Γ , Γᵗ , W1 =[ (WHILE b DO c END) ]=> (W1 + X1))
               → (Γ , Γᵗ , W2 =[ (WHILE b DO c END) ]=> (W2 + X2))
               → X1 ≡ X2
ife-cancel : ∀ (Γ : String → Maybe (TProgTuple {ℕ}))
               → (Γᵗ : String → ℕ)
               → ∀ (W1 W2 X1 X2 : ℕ)
               → (b : Bexp {ℕ})
               → (t e : Cmd {ℕ})
               → (Γ , Γᵗ , W1 =[ ( IF b THEN t ELSE e END ) ]=> (W1 + X1))
               → (Γ , Γᵗ , W2 =[ ( IF b THEN t ELSE e END ) ]=> (W2 + X2))
               → X1 ≡ X2
seq-cancel : ∀ (Γ : String → Maybe (TProgTuple {ℕ}))
               → (Γᵗ : String → ℕ)
               → ∀ (W1 W2 X1 X2 : ℕ)
               → (c1 c2 : Cmd {ℕ})
               → (Γ , Γᵗ , W1 =[ ( c1 ; c2) ]=> (W1 + X1))
               → (Γ , Γᵗ , W2 =[ ( c1 ; c2) ]=> (W2 + X2))
               → X1 ≡ X2

-- The general case of cancellation.
eq-cancel : ∀ (Γ : String → Maybe (TProgTuple {ℕ}))
               → (Γᵗ : String → ℕ)
               → ∀ (c : Cmd {ℕ})
               → ∀ (W1 W2 X1 X2 : ℕ)
               → (Γ , Γᵗ , W1 =[ c ]=> (W1 + X1))
               → (Γ , Γᵗ , W2 =[ c ]=> (W2 + X2))
               → X1 ≡ X2

loop-cancel Γ Γᵗ W1 W2 X1 X2 b c cmd1 cmd2
  with (W1 + X1) in eq1 | (W2 + X2) in eq2
loop-cancel Γ Γᵗ W1 W2 X1 X2 b c (TLF .b .c x .W1)
  (TLF .b .c x₁ .W2) | .(W1 + 0 + tbeval Γᵗ b) | .(W2 + 0 + tbeval Γᵗ b)
  rewrite +-assoc W1 0 (tbeval Γᵗ b) | +-assoc W2 0 (tbeval Γᵗ b)
  with +-cancelˡ-≡ W1 eq1 | +-cancelˡ-≡ W2 eq2
... | refl | refl = refl
loop-cancel Γ Γᵗ W1 W2 X1 X2 b c (TLF .b .c x .W1)
  (TLT .b .c x₁ .W2 W' cmd2) | .(W1 + 0 + tbeval Γᵗ b)
  | .(W2 + Γᵗ "loop-count" * (W' + tbeval Γᵗ b) + tbeval Γᵗ b)
  = ⊥-elim (contradiction-lemma b Γᵗ x₁ x)
loop-cancel Γ Γᵗ W1 W2 X1 X2 b c (TLT .b .c x .W1 W' cmd1)
  (TLF .b .c x₁ .W2)
  | .(W1 + Γᵗ "loop-count" * (W' + tbeval Γᵗ b) + tbeval Γᵗ b)
  | .(W2 + 0 + tbeval Γᵗ b) = ⊥-elim (contradiction-lemma b Γᵗ x x₁)
loop-cancel Γ Γᵗ W1 W2 X1 X2 b c (TLT .b .c x .W1 W' cmd1)
  (TLT .b .c x₁ .W2 W'' cmd2)
  | .(W1 + Γᵗ "loop-count" * (W' + tbeval Γᵗ b) + tbeval Γᵗ b)
  | .(W2 + Γᵗ "loop-count" * (W'' + tbeval Γᵗ b) + tbeval Γᵗ b)
  with eq-cancel Γ Γᵗ c W1 W2 W' W'' cmd1 cmd2
... | refl with (Γᵗ "loop-count") | (tbeval Γᵗ b)
... | LC | BC rewrite +-assoc W2 (LC * (W' + BC)) BC
    | +-assoc W1 (LC * (W' + BC)) BC
    with +-cancelˡ-≡ W2 eq2 | +-cancelˡ-≡ W1 eq1
... | refl | refl = refl

ife-cancel Γ Γᵗ W1 W2 X1 X2 b t e p1 p2 with (W1 + X1) in eq1
  | (W2 + X2) in eq2
ife-cancel Γ Γᵗ W1 W2 X1 X2 b t e (TIFT n1 .b .t .e .W1 W' W'' x p1 p3)
  (TIFT n2 .b .t .e .W2 W''' W'''' x₁ p2 p4) | .(W1 + W' + tbeval Γᵗ b)
  | .(W2 + W''' + tbeval Γᵗ b) with eq-cancel Γ Γᵗ t W1 W2 W' W''' p1 p2
... | refl rewrite +-assoc W2 W' (tbeval Γᵗ b) | +-assoc W1 W' (tbeval Γᵗ b)
  with +-cancelˡ-≡ W2 eq2 | +-cancelˡ-≡ W1 eq1
... | refl | refl = refl
ife-cancel Γ Γᵗ W1 W2 X1 X2 b t e (TIFT n1 .b .t .e .W1 W' W'' x p1 p3)
  (TIFE n2 .b .t .e .W2 W''' W'''' x₁ p2 p4) | .(W1 + W' + tbeval Γᵗ b)
  | .(W2 + W'''' + tbeval Γᵗ b) = ⊥-elim (contradiction-lemma b Γᵗ x x₁)
ife-cancel Γ Γᵗ W1 W2 X1 X2 b t e (TIFE n1 .b .t .e .W1 W' W'' x p1 p3)
  (TIFT n2 .b .t .e .W2 W''' W'''' x₁ p2 p4) | .(W1 + W'' + tbeval Γᵗ b)
  | .(W2 + W''' + tbeval Γᵗ b) = ⊥-elim (contradiction-lemma b Γᵗ x₁ x)
ife-cancel Γ Γᵗ W1 W2 X1 X2 b t e (TIFE n1 .b .t .e .W1 W' W'' x p1 p3)
  (TIFE n2 .b .t .e .W2 W''' W'''' x₁ p2 p4) | .(W1 + W'' + tbeval Γᵗ b)
  | .(W2 + W'''' + tbeval Γᵗ b) rewrite +-assoc W1 W'' (tbeval Γᵗ b)
  | +-assoc W2 W'''' (tbeval Γᵗ b) with +-cancelˡ-≡ W2 eq2
  | +-cancelˡ-≡ W1 eq1 | eq-cancel Γ Γᵗ e W1 W2 W'' W'''' p3 p4
... | refl | refl | refl = refl

seq-cancel Γ Γᵗ W1 W2 X1 X2 c1 c2 p1 p2 with (W1 + X1) in eq1
  | (W2 + X2) in eq2
seq-cancel Γ Γᵗ W1 W2 X1 X2 c1 c2 (TSEQ .c1 .c2 .W1 W' W'' p1 p3)
  (TSEQ .c1 .c2 .W2 W''' W'''' p2 p4)
  | .(W1 + (W' + W'')) | .(W2 + (W''' + W''''))
  rewrite +-cancelˡ-≡ W1 eq1 | +-cancelˡ-≡ W2 eq2
  with eq-cancel Γ Γᵗ c1 W1 W2 W' W''' p1 p2
... | refl
  rewrite
     +-comm W'''  W''
     | +-comm W1 (W'' + W''') | +-assoc W'' W'''  W1 | +-comm W''' W1
     | +-comm W'' (W1 + W''') | +-comm W'''  W'''' | +-comm W2 (W'''' + W''')
     | +-assoc W'''' W'''  W2 | +-comm W''' W2 | +-comm W'''' (W2 + W''')
   with (W1 + W''') | (W2 + W''')
... | l | m
   with eq-cancel Γ Γᵗ c2 l m W'' W'''' p3 p4
... | refl  = refl

eq-cancel Γ Γᵗ SKIP W1 W2 X1 X2 p1 p2 = skip-cancel Γ Γᵗ W1 W2 X1 X2 p1 p2
eq-cancel Γ Γᵗ (Var x := r) W1 W2 X1 X2 p1 p2
  = assign-cancel Γ Γᵗ W1 W2 X1 X2 x r p1 p2
eq-cancel Γ Γᵗ (c ; c₁) W1 W2 X1 X2 p1 p2
  = seq-cancel Γ Γᵗ W1 W2 X1 X2 c c₁ p1 p2
eq-cancel Γ Γᵗ IF b THEN c ELSE c₁ END W1 W2 X1 X2 p1 p2
  = ife-cancel Γ Γᵗ W1 W2 X1 X2 b c c₁ p1 p2
eq-cancel Γ Γᵗ WHILE b DO c END W1 W2 X1 X2 p1 p2
  = loop-cancel Γ Γᵗ W1 W2 X1 X2 b c p1 p2

-- TODO: The function call case and concurrency cases will go here

-- Soundness theorem for Seq WCET rule
seq-sound : (Γ : String → Maybe (TProgTuple {ℕ}))
            → (Γᵗ : String → ℕ)
            → (c1 c2 : Cmd {ℕ})
            → (W X1 X2 W' : ℕ)
            → (cmd : Γ , Γᵗ , W =[ c1 ; c2 ]=> W')
            → (p1 : Γ , Γᵗ , W =[ c1 ]=> (W + X1))
            → (p2 : Γ , Γᵗ , W =[ c2 ]=> (W + X2))
            → (W' ≡ W + (X1 + X2))
seq-sound Γ Γᵗ c1 c2 W X1 X2 .(W + (W' + W''))
  (TSEQ .c1 .c2 .W W' W'' cmd cmd₁) p1 p2
  with Δ-exec Γ Γᵗ W (W + W') (W + X1) c1 cmd p1
... | q with +-cancelˡ-≡ W q
... | refl rewrite +-comm W (X1 + W'') | +-comm X1 W'' | +-assoc W'' X1 W
    | +-comm X1 W | +-comm W'' (W + X1) | +-comm X1 X2 | +-comm W (X2 + X1)
    | +-assoc X2 X1 W | +-comm X2 (X1 + W) | +-comm X1 W with (W + X1)
... | rl with eq-cancel Γ Γᵗ c2 rl W W'' X2 cmd₁ p2
... | refl = refl

-- Helping lemma for ife
plus-≤ : ∀ (m n p : ℕ) → (m ≤ n) → (m + p) ≤ (n + p)
plus-≤ .zero n p z≤n = m≤n+m p n
plus-≤ .(suc _) .(suc _) p (s≤s {m} {n} q) with plus-≤ m n p q
... | H0 = s≤s H0

≤-rela1 : ∀ (m n : ℕ) → ¬ (m ≤ n) → (n < m)
≤-rela1 zero n p = ⊥-elim (p z≤n)
≤-rela1 (suc m) zero p = s≤s z≤n
≤-rela1 (suc m) (suc n) p = s≤s (≤-rela1 m n (λ z → p (s≤s z)))

≤-rela2 : ∀ (m n : ℕ) → (suc n ≤ m) → (n ≤ m)
≤-rela2 m n p with n≤1+n n
... | q = ≤-trans q p

-- if-helper
if-helper : ∀ (X1 X2 : ℕ) → (X1 ≤ max X1 X2)
if-helper X1 X2 with (X1 ≤? X2)
... | false Relation.Nullary.because proof = ≤′⇒≤ ≤′-refl
... | true Relation.Nullary.because Relation.Nullary.ofʸ p = p

if-helper2 : ∀ (X1 X2 : ℕ) → (X2 ≤ max X1 X2)
if-helper2 X1 X2 with (X1 ≤? X2)
if-helper2 X1 X2 | false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p
  with ≤-rela1 X1 X2 (¬p)
... | q = ≤-rela2 X1 X2 q
if-helper2 X1 X2 | true Relation.Nullary.because _ = ≤′⇒≤ ≤′-refl

-- Soundness theorem for If-else WCET rule
ife-sound : (Γ : String → Maybe (TProgTuple {ℕ}))
            → (Γᵗ : String → ℕ)
            → (t e : Cmd {ℕ})
            → (b : Bexp {ℕ})
            → (W X1 X2 W' : ℕ)
            → (tcmd : Γ , Γᵗ , W =[ t ]=> (W + X1))
            → (ecmd : Γ , Γᵗ , W =[ e ]=> (W + X2))
            → (cmd : Γ , Γᵗ , W =[ (IF b THEN t ELSE e END) ]=> W')
            → (W' ≤ W + (max X1 X2) + (tbeval Γᵗ b))
ife-sound Γ Γᵗ t e b W X1 X2 .(W + W' + tbeval Γᵗ b) tcmd ecmd
  (TIFT n1 .b .t .e .W W' W'' x cmd cmd₁)
  with Δ-exec Γ Γᵗ W (W + W') (W + X1) t cmd tcmd
... | l with +-cancelˡ-≡ W l
... | refl rewrite +-assoc W X1 (tbeval Γᵗ b) | +-comm W (X1 + (tbeval Γᵗ b))
    | +-assoc X1 (tbeval Γᵗ b) W with (tbeval Γᵗ b)
... | Y with max X1 X2 in eq
... | M rewrite +-assoc W M Y | +-comm W (M + Y) | +-assoc M Y W
    with (Y + W)
... | L with if-helper X1 X2 | eq
... | T | refl = plus-≤ X1 M L T
ife-sound Γ Γᵗ t e b W X1 X2 .(W + W'' + tbeval Γᵗ b) tcmd ecmd
  (TIFE n1 .b .t .e .W W' W'' x cmd cmd₁)
  with (tbeval Γᵗ b) | Δ-exec Γ Γᵗ W (W + W'') (W + X2) e cmd₁ ecmd
... | Y | l with +-cancelˡ-≡ W l
... | refl with max X1 X2 in eq
... | M rewrite +-assoc W X2 Y | +-assoc W M Y | +-comm W (X2 + Y)
    | +-comm W (M + Y) | +-assoc X2 Y W | +-assoc M Y W with (Y + W)
... | L with if-helper2 X1 X2 | eq
... | T | refl = plus-≤ X2 M L T

-- Helper for loop
loop-helper : ∀ (l g : ℕ) → (l ≤′ (g + l))
loop-helper l zero = ≤′-refl
loop-helper l (suc g) = ≤′-step (loop-helper l g)

-- XXX: Using well founded recursion here
loop-sound-≤′ : (Γ : String → Maybe (TProgTuple {ℕ}))
            → (Γᵗ : String → ℕ)
            → (c : Cmd {ℕ})
            → (b : Bexp {ℕ})
            → (W W' X1 : ℕ)
            → (Γ , Γᵗ , W =[ c ]=> (W + X1))
            → (cmd : Γ , Γᵗ , W =[ (WHILE b DO c END) ]=> W')
            → W' ≤′
              W + ((Γᵗ "loop-count") * (X1 + (tbeval Γᵗ b))) + (tbeval Γᵗ b)
loop-sound-≤′ Γ Γᵗ c b W .(W + 0 + tbeval Γᵗ b) X1 cmd (TLF .b .c x .W)
  with (Γᵗ "loop-count")
... | zero = ≤′-refl
... | suc m rewrite +-comm W 0
    with (tbeval Γᵗ b)
... | q
    with (X1 + q + m * (X1 + q))
... | t rewrite +-comm W t | +-assoc t W q with (W + q)
... | l = loop-helper l t
loop-sound-≤′  Γ Γᵗ c b W
  .(W + Γᵗ "loop-count" * (W' + tbeval Γᵗ b) + tbeval Γᵗ b) X1 cmd
  (TLT .b .c x .W W' cmd1)
  with Δ-exec Γ Γᵗ W (W + W') (W + X1) c cmd1 cmd
... | r with +-cancelˡ-≡ W r
... | refl = ≤′-refl

-- The general case
loop-sound : (Γ : String → Maybe (TProgTuple {ℕ}))
            → (Γᵗ : String → ℕ)
            → (c : Cmd {ℕ})
            → (b : Bexp {ℕ})
            → (W W' X1 : ℕ)
            → (Γ , Γᵗ , W =[ c ]=> (W + X1))
            → (cmd : Γ , Γᵗ , W =[ (WHILE b DO c END) ]=> W')
            → W' ≤
              W + ((Γᵗ "loop-count") * (X1 + (tbeval Γᵗ b))) + (tbeval Γᵗ b)
loop-sound Γ Γᵗ c b W W' X1 c2 cmd =
  ≤′⇒≤ (loop-sound-≤′ Γ Γᵗ c b W W' X1 c2 cmd)

-- The soundness theorem for a single function call
func-sound : (Γ : String → Maybe (TProgTuple {ℕ})) → ∀ (Γᵗ : String → ℕ)
             → ∀ (fname : String) → ∀ (W W' : ℕ)
             → Γ , Γᵗ , W =[ < getProgRetsT (Γ fname) >:=
                             fname < getProgArgsT (Γ fname) > ]=>ᶠ W'
             → W' ≡ (W +
                       ((numargs $ getProgArgsT $ (Γ fname)) * (Γᵗ "arg-copy"))
                    + (getProgTimeT (Γ fname))
                    + ((numrets $ getProgRetsT $ (Γ fname)) * (Γᵗ "ret-copy")))
func-sound Γ Γᵗ fname W .(W + W' + getProgTimeT (Γ fname) + W''')
  (Base .fname .W W' .(getProgTimeT (Γ fname)) W''' x refl x₁ x₂)
  with args-sound Γᵗ (getProgArgsT (Γ fname)) W (W + W') x
       | rets-sound Γᵗ (getProgRetsT (Γ fname))
         (W + W' + getProgTimeT (Γ fname))
         (W + W' + getProgTimeT (Γ fname) + W''') x₂
... | l | m with +-cancelˡ-≡ W l
... | refl
  with +-cancelˡ-≡ (W + numargs (getProgArgsT (Γ fname)) * Γᵗ "arg-copy"
                   + getProgTimeT (Γ fname)) m
... | refl = refl

-- The soundness theorem for PAR (||`) execution of threads
par-sound : (Γ : String → Maybe (TProgTuple {ℕ})) → ∀ (Γᵗ : String → ℕ)
            → (l r : FuncCall {ℕ}) → (W W' X1 X2 : ℕ)
            → Γ , Γᵗ , W =[ l ||` r ]=>ᶠ W'
            → Γ , Γᵗ , W =[ l ]=>ᶠ (W + X1)
            → Γ , Γᵗ , W =[ r ]=>ᶠ (W + X2)
            → W' ≡ W + (max X1 X2) + 2 * ((Γᵗ "fork") + (Γᵗ "join"))
par-sound Γ Γᵗ l r W .(W + max X3 X4 + (2 * Γᵗ "fork" + 2 * Γᵗ "join"))
  X1 X2 (PAR .l .r .W X3 X4 pare pare₁) parl parr
  with (Γᵗ "fork") | (Γᵗ "join")
... | tf | tj rewrite *-distribˡ-+ 2 tf tj
    | +-assoc tf tj 0 | +-comm tj 0 | +-comm tf 0
    | +-assoc tf tj (tf + tj) | +-comm tj (tf + tj)
    | +-assoc tf tj tj | +-comm tf (tf + (tj + tj))
    | +-comm tf (tj + tj) with (tf + tf + (tj + tj))
... | m with Δ-exec-func Γ Γᵗ l W (W + X1) (W + X3) parl pare
... | q with Δ-exec-func Γ Γᵗ r W (W + X2) (W + X4) parr pare₁
... | q2 with +-cancelˡ-≡ W q | +-cancelˡ-≡ W q2
... | refl | refl = refl


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Lattice.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Semilattice

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsLattice {L : Type ℓ}
                 (0l 1l : L) (_∨l_ _∧l_ : L → L → L) : Type ℓ where

  constructor islattice

  field
   joinSemilattice : IsSemilattice 0l _∨l_
   meetSemilattice : IsSemilattice 1l _∧l_
   absorb : (x y : L) → (x ∨l (x ∧l y) ≡ x)
                      × (x ∧l (x ∨l y) ≡ x)

  open IsSemilattice joinSemilattice public
   renaming
     ( assoc to ∨lAssoc
     ; identity to ∨lIdentity
     ; lid to ∨lLid
     ; rid to ∨lRid
     ; comm to ∨lComm
     ; idem to ∨lIdem
     ; isCommMonoid to ∨lIsCommMonoid
     ; isMonoid to ∨lIsMonoid
     ; isSemigroup to ∨lIsSemigroup )

  open IsSemilattice meetSemilattice public
   renaming
     ( assoc to ∧lAssoc
     ; identity to ∧lIdentity
     ; lid to ∧lLid
     ; rid to ∧lRid
     ; comm to ∧lComm
     ; idem to ∧lIdem
     ; isCommMonoid to ∧lIsCommMonoid
     ; isMonoid to ∧lIsMonoid
     ; isSemigroup to ∧lIsSemigroup )
   hiding
     ( is-set )

  ∨lAbsorb∧l : (x y : L) → x ∨l (x ∧l y) ≡ x
  ∨lAbsorb∧l x y = absorb x y .fst

  ∧lAbsorb∨l : (x y : L) → x ∧l (x ∨l y) ≡ x
  ∧lAbsorb∨l x y = absorb x y .snd

record LatticeStr (A : Type ℓ)  : Type (ℓ-suc ℓ) where

  constructor latticestr

  field
    0l : A
    1l : A
    _∨l_ : A → A → A
    _∧l_ : A → A → A
    isLattice : IsLattice 0l 1l _∨l_ _∧l_

  infix 7 _∨l_
  infix 6 _∧l_

  open IsLattice isLattice public

Lattice : ∀ ℓ → Type (ℓ-suc ℓ)
Lattice ℓ = TypeWithStr ℓ LatticeStr

isSetLattice : (L : Lattice ℓ) → isSet ⟨ L ⟩
isSetLattice L = L .snd .LatticeStr.is-set

makeIsLattice : {L : Type ℓ} {0l 1l : L} {_∨l_ _∧l_ : L → L → L}
             (is-setL : isSet L)
             (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
             (∨l-rid : (x : L) → x ∨l 0l ≡ x)
             (∨l-lid : (x : L) → 0l ∨l x ≡ x)
             (∨l-comm : (x y : L) → x ∨l y ≡ y ∨l x)
             (∧l-assoc : (x y z : L) → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l z)
             (∧l-rid : (x : L) → x ∧l 1l ≡ x)
             (∧l-lid : (x : L) → 1l ∧l x ≡ x)
             (∧l-comm : (x y : L) → x ∧l y ≡ y ∧l x)
             (∨l-absorb-∧l : (x y : L) → x ∨l (x ∧l y) ≡ x)
             (∧l-absorb-∨l : (x y : L) → x ∧l (x ∨l y) ≡ x)
           → IsLattice 0l 1l _∨l_ _∧l_
makeIsLattice {0l = 0l} {1l = 1l} {_∨l_ = _∨l_} {_∧l_ = _∧l_}
              is-setL ∨l-assoc ∨l-rid ∨l-lid ∨l-comm
                      ∧l-assoc ∧l-rid ∧l-lid ∧l-comm ∨l-absorb-∧l ∧l-absorb-∨l =
     islattice (makeIsSemilattice is-setL ∨l-assoc ∨l-rid ∨l-lid ∨l-comm ∨l-idem)
               (makeIsSemilattice is-setL ∧l-assoc ∧l-rid ∧l-lid ∧l-comm ∧l-idem)
               λ x y → ∨l-absorb-∧l x y , ∧l-absorb-∨l x y
 where
 ∨l-idem : ∀ x → x ∨l x ≡ x
 ∨l-idem x = cong (x ∨l_) (sym (∧l-rid _)) ∙ ∨l-absorb-∧l _ _

 ∧l-idem : ∀ x → x ∧l x ≡ x
 ∧l-idem x = cong (x ∧l_) (sym (∨l-rid _)) ∙ ∧l-absorb-∨l _ _

makeLattice : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L)
             (is-setL : isSet L)
             (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
             (∨l-rid : (x : L) → x ∨l 0l ≡ x)
             (∨l-lid : (x : L) → 0l ∨l x ≡ x)
             (∨l-comm : (x y : L) → x ∨l y ≡ y ∨l x)
             (∨l-idem : (x : L) → x ∨l x ≡ x)
             (∧l-assoc : (x y z : L) → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l z)
             (∧l-rid : (x : L) → x ∧l 1l ≡ x)
             (∧l-lid : (x : L) → 1l ∧l x ≡ x)
             (∧l-comm : (x y : L) → x ∧l y ≡ y ∧l x)
             (∧l-idem : (x : L) → x ∧l x ≡ x)
             (∨l-absorb-∧l : (x y : L) → x ∨l (x ∧l y) ≡ x)
             (∧l-absorb-∨l : (x y : L) → x ∧l (x ∨l y) ≡ x)
           → Lattice ℓ
makeLattice 0l 1l _∨l_ _∧l_ is-setL ∨l-assoc ∨l-rid ∨l-lid ∨l-comm ∨l-idem
            ∧l-assoc ∧l-rid ∧l-lid ∧l-comm ∧l-idem ∨l-absorb-∧l ∧l-absorb-∨l =
   _ , latticestr 0l 1l _∨l_ _∧l_
   (makeIsLattice is-setL ∨l-assoc ∨l-rid ∨l-lid ∨l-comm
                          ∧l-assoc ∧l-rid ∧l-lid ∧l-comm ∨l-absorb-∧l ∧l-absorb-∨l)

record IsLatticeHom {A : Type ℓ} {B : Type ℓ'} (L : LatticeStr A) (f : A → B) (M : LatticeStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module L = LatticeStr L
    module M = LatticeStr M

  field
    pres0 : f L.0l ≡ M.0l
    pres1 : f L.1l ≡ M.1l
    pres∨l : (x y : A) → f (x L.∨l y) ≡ f x M.∨l f y
    pres∧l : (x y : A) → f (x L.∧l y) ≡ f x M.∧l f y

unquoteDecl IsLatticeHomIsoΣ = declareRecordIsoΣ IsLatticeHomIsoΣ (quote IsLatticeHom)

LatticeHom : (L : Lattice ℓ) (M : Lattice ℓ') → Type (ℓ-max ℓ ℓ')
LatticeHom L M = Σ[ f ∈ (⟨ L ⟩ → ⟨ M ⟩) ] IsLatticeHom (L .snd) f (M .snd)

IsLatticeEquiv : {A : Type ℓ} {B : Type ℓ'} (M : LatticeStr A) (e : A ≃ B) (N : LatticeStr B)
  → Type (ℓ-max ℓ ℓ')
IsLatticeEquiv M e N = IsLatticeHom M (e .fst) N

LatticeEquiv : (L : Lattice ℓ) (M : Lattice ℓ') → Type (ℓ-max ℓ ℓ')
LatticeEquiv L M = Σ[ e ∈ (⟨ L ⟩ ≃ ⟨ M ⟩) ] IsLatticeEquiv (L .snd) e (M .snd)

isPropIsLattice : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L)
             → isProp (IsLattice 0l 1l _∨l_ _∧l_)
isPropIsLattice 0l 1l _∨l_ _∧l_ (islattice LJ LM LA) (islattice MJ MM MA) =
  λ i → islattice (isPropIsSemilattice _ _ LJ MJ i)
                  (isPropIsSemilattice _ _ LM MM i)
                  (isPropAbsorb LA MA i)
  where
  isSetL : isSet _
  isSetL = LJ .IsSemilattice.isCommMonoid .IsCommMonoid.isMonoid
              .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropAbsorb : isProp ((x y : _) → (x ∨l (x ∧l y) ≡ x) × (x ∧l (x ∨l y) ≡ x))
  isPropAbsorb = isPropΠ2 λ _ _ → isProp× (isSetL _ _) (isSetL _ _)

isPropIsLatticeHom : {A : Type ℓ} {B : Type ℓ'} (R : LatticeStr A) (f : A → B) (S : LatticeStr B)
                   → isProp (IsLatticeHom R f S)
isPropIsLatticeHom R f S = isOfHLevelRetractFromIso 1 IsLatticeHomIsoΣ
                           (isProp×3 (isSetLattice (_ , S) _ _)
                                     (isSetLattice (_ , S) _ _)
                                     (isPropΠ2 λ _ _ → isSetLattice (_ , S) _ _)
                                     (isPropΠ2 λ _ _ → isSetLattice (_ , S) _ _))

𝒮ᴰ-Lattice : DUARel (𝒮-Univ ℓ) LatticeStr ℓ
𝒮ᴰ-Lattice =
  𝒮ᴰ-Record (𝒮-Univ _) IsLatticeEquiv
    (fields:
      data[ 0l ∣ null ∣ pres0 ]
      data[ 1l ∣ null ∣ pres1 ]
      data[ _∨l_ ∣ bin ∣ pres∨l ]
      data[ _∧l_ ∣ bin ∣ pres∧l ]
      prop[ isLattice ∣ (λ _ _ → isPropIsLattice _ _ _ _) ])
 where
  open LatticeStr
  open IsLatticeHom

  -- faster with some sharing
  null = autoDUARel (𝒮-Univ _) (λ A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

LatticePath : (L M : Lattice ℓ) → LatticeEquiv L M ≃ (L ≡ M)
LatticePath = ∫ 𝒮ᴰ-Lattice .UARel.ua

Lattice→JoinSemilattice : Lattice ℓ → Semilattice ℓ
Lattice→JoinSemilattice (A , latticestr _ _ _ _ L) = semilattice _ _ _ (L .IsLattice.joinSemilattice )

Lattice→MeetSemilattice : Lattice ℓ → Semilattice ℓ
Lattice→MeetSemilattice (A , latticestr _ _ _ _ L) = semilattice _ _ _ (L .IsLattice.meetSemilattice )


text:
Extensionality of a function of two arguments

\begin{code}
extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
\end{code}

Isomorphism of all and exists.
\begin{code}
¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃ (λ (x : A) → B x)) ≃ ∀ (x : A) → ¬ B x
¬∃∀ =
  record
    { to   =  λ { ¬∃bx x bx → ¬∃bx (x , bx) }
    ; fro  =  λ { ∀¬bx (x , bx) → ∀¬bx x bx }
    ; invˡ =  λ { ¬∃bx → extensionality (λ { (x , bx) → refl }) }
    ; invʳ =  λ { ∀¬bx → refl }
    }
\end{code}


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

_ : 10_000 * 100_000 ≡ 1_000_000_000
_ = refl

max_stars_repo_name: strake/agda

max_issues_repo_name: strake/agda


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Unit where

open import Agda.Builtin.Unit public renaming (⊤ to Unit; tt to unit)


text:
------------------------------------------------------------------------
-- Spheres
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- This module follows the HoTT book rather closely.

import Equality.Path as P

module Sphere
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equality.Tactic equality-with-J
import Equivalence equality-with-J as Equiv
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Nat equality-with-J as Nat
open import Pointed-type equality-with-J
open import Suspension eq as Suspension

private
  variable
    a b : Level
    A B : Type a
    C   : Pointed-type a
    x   : A
    n   : ℕ

-- Spheres.

𝕊[_-1] : ℕ → Type
𝕊[ zero  -1] = ⊥
𝕊[ suc n -1] = Susp 𝕊[ n -1]

-- Spheres with non-negative dimensions.

𝕊 : ℕ → Type
𝕊 n = 𝕊[ 1 + n -1]

-- The booleans are isomorphic to the 0-dimensional sphere.

Bool↔𝕊⁰ : Bool ↔ 𝕊 0
Bool↔𝕊⁰ = Bool↔Susp-⊥

-- Based maps from spheres with non-negative dimensions (using north
-- as the point) are isomorphic to iterated loop spaces.

𝕊→ᴮ↔ : ∀ n → (𝕊 n , north) →ᴮ C ↔ proj₁ (Ω[ n ] C)
𝕊→ᴮ↔ {C = C} = lemma zero
  where
  lemma : ∀ m n → (𝕊 n , north) →ᴮ Ω[ m ] C ↔ proj₁ (Ω[ m + n ] C)
  lemma m zero =
    (𝕊 0 , north) →ᴮ Ω[ m ] C  ↝⟨ Σ-cong (→-cong ext (inverse Bool↔𝕊⁰) F.id) (λ _ → F.id) ⟩
    (Bool , true) →ᴮ Ω[ m ] C  ↝⟨ Bool→ᴮ↔ ext ⟩
    proj₁ (Ω[ m ] C)           ↝⟨ ≡⇒↝ _ $ cong (λ n → proj₁ (Ω[ n ] C)) $ sym $ Nat.+-right-identity {n = m} ⟩□
    proj₁ (Ω[ m + 0 ] C)       □

  lemma m (suc n) =
    (𝕊 (suc n) , north) →ᴮ Ω[ m ] C  ↝⟨ Susp→ᴮ↔ ⟩
    (𝕊 n , north) →ᴮ Ω[ suc m ] C    ↝⟨ lemma (suc m) n ⟩
    proj₁ (Ω[ suc m + n ] C)         ↝⟨ ≡⇒↝ _ $ cong (λ n → proj₁ (Ω[ n ] C)) $ Nat.suc+≡+suc m ⟩□
    proj₁ (Ω[ m + suc n ] C)         □

-- A corollary.

+↔∀contractible𝕊→ᴮ :
  H-level (1 + n) A ↔
  (∀ x → Contractible ((𝕊 n , north) →ᴮ (A , x)))
+↔∀contractible𝕊→ᴮ {n = n} {A = A} =
  H-level (1 + n) A                                ↔⟨ _↔_.to (Equiv.⇔↔≃ ext (H-level-propositional ext _)
                                                                            (Π-closure ext 1 λ _ →
                                                                             H-level-propositional ext _))
                                                             (+⇔∀contractible-Ω[] _) ⟩
  (∀ x → Contractible (proj₁ $ Ω[ n ] (A , x)))    ↝⟨ (∀-cong ext λ _ → H-level-cong ext 0 (inverse $ 𝕊→ᴮ↔ _)) ⟩□
  (∀ x → Contractible ((𝕊 n , north) →ᴮ (A , x)))  □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --universe-polymorphism #-}

-- Level suc is not a constructor, and doesn't behave as one
-- for unification.
module LevelUnification where

open import Imports.Level

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

sym : ∀ a b (A : Set (suc a))(B : Set (suc b))(x : A)(y : B) → x ≡ y → y ≡ x
sym a .a A .A x .x refl = refl


text:
{-
  Mathematical Foundations of Programming (G54FOP)
  Nicolai Kraus
  Lecture 6, 15 Feb 2018
-}

module lec6FOP where

{- We import everything we have done last week.
   "open" means we can use all definitions directly -}
open import lec3FOP

{- Hint: middle mouse click or alt-.
   [press alt/meta, then .]
   jumps to the definition that the cursor is on -}

-- Reduce in one step
-- (these are the simplification rules)
data _→1_ : Expr → Expr → Set where
  izz : iz z →1 t
  izs : {e : Expr} → iz (s e) →1 f
  ift : {e₂ e₃ : Expr} → (if t then e₂ else e₃) →1 e₂
  iff : {e₂ e₃ : Expr} → (if f then e₂ else e₃) →1 e₃
  ps  : {e : Expr} → p (s e) →1 e
  pz  : p z →1 z

-- include structural rules
data _↝_ : Expr → Expr → Set where  -- type: \leadsto
  from→1   : {e₁ e₂ : Expr} → (e₁ →1 e₂) → (e₁ ↝ e₂)
  inside-s : {e₁ e₂ : Expr} → (e₁ ↝ e₂) → (s e₁ ↝ s e₂)
  inside-p : {e₁ e₂ : Expr} → (e₁ ↝ e₂) → (p e₁ ↝ p e₂)
  inside-iz : ∀ {e₁} {e₂} → (e₁ ↝ e₂) → (iz e₁ ↝ iz e₂)
  inside-ite1 : ∀ {e₁ e₁' e₂ e₃} → (e₁ ↝ e₁')
    → (if e₁ then e₂ else e₃) ↝ (if e₁' then e₂ else e₃)
  inside-ite2 : ∀ {e₁ e₂ e₂' e₃} → (e₂ ↝ e₂')
    → (if e₁ then e₂ else e₃) ↝ (if e₁ then e₂' else e₃)
  inside-ite3 : ∀ {e₁ e₂ e₃ e₃'} → (e₃ ↝ e₃')
    → (if e₁ then e₂ else e₃) ↝ (if e₁ then e₂ else e₃')

data _↝*_ : Expr → Expr → Set where
  start : ∀ {e} → e ↝* e
  step  : ∀ {e₁ e₂ e₃} → (e₁ ↝ e₂) → (e₂ ↝* e₃)
          → (e₁ ↝* e₃)

-- compose two reduction sequences
compose : {e₁ e₂ e₃ : Expr} → (e₁ ↝* e₂)
          → (e₂ ↝* e₃)
          → (e₁ ↝* e₃)
compose start s₂ = s₂
compose (step x s₁) s₂ = step x (compose s₁ s₂)

open import Data.Empty renaming (⊥ to ∅)  -- \emptyset

-- define what it means to be a normal form
is-normal : Expr → Set
is-normal e = (e₁ : Expr) → (e →1 e₁) → ∅

{- Exercises:
   1. (easy) Show that the expression "t" is
      in normal form. This means: fill the whole
      (replace the question mark) in
        t-nf : is-normal t
        t-nf = ?

   2. (medium) Show that, if "e" is a normal form,
      then so is "s e".

   3. (hard) Show that "is-normal" is a
      decidable predicate on Expr.
      This means writing a function
      which takes an expression and tells us
      whether the expression is a normal form
      or not. The naive version would be
         Expr → Bool
      but we can do much better: we can take an
      expression "e" and either return a *proof*
      that "e" is a normal form, or return an
      example of how it can be reduced.
      Such an example would consist of an expression
      "reduct" and a proof of "e ↝ reduct"; we
      will learn later how this can be expressed,
      but a good way of implementing it is as follows:
-}

record can-red (e : Expr) : Set where
  field
    reduct  : Expr
    redstep : e ↝ reduct

{- Ex 3, continued: We can import Data.Sum to get the
   definition of ⊎ (type: \u+), a disjoint sum (it's
   Either in Haskell). Check out how ⊎ is defined in
   the library, it's really simple! -}

open import Data.Sum

{- Ex3, continued: Now, fill in the ? in the following
   function; probably, you will want more auxiliary
   lemma. Caveat: I have not done this myself.

decide-nf : (e : Expr) → (is-normal e) ⊎ can-red e
decide-nf e = {!!}

-}


text:
module Structure.Function.Ordering where

import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Type

module _ {ℓₒ₁ ℓₒ₂ ℓₗ₁ ℓₗ₂} {T₁ : Type{ℓₒ₁}} {T₂ : Type{ℓₒ₂}} (_≤₁_ : T₁ → T₁ → Type{ℓₗ₁}) (_≤₂_ : T₂ → T₂ → Type{ℓₗ₂}) where
  record Increasing (f : T₁ → T₂) : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : ∀{a b : T₁} → (a ≤₁ b) → (f(a) ≤₂ f(b))

  record Decreasing (f : T₁ → T₂) : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : ∀{a b : T₁} → (a ≤₁ b) → (f(b) ≤₂ f(a))

  Monotone : (T₁ → T₂) → Stmt
  Monotone(f) = (Increasing(f) ∨ Decreasing(f))

  record UpperBoundPointOf (f : T₁ → T₂) (p : T₁) : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : ∀{x} → (f(x) ≤₂ f(p))

  UpperBounded : (T₁ → T₂) → Stmt
  UpperBounded(f) = ∃(UpperBoundPointOf(f))

  record LowerBoundPointOf (f : T₁ → T₂) (p : T₁) : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : ∀{x} → (f(p) ≤₂ f(x))

  LowerBounded : (T₁ → T₂) → Stmt
  LowerBounded(f) = ∃(LowerBoundPointOf(f))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Issue498: Underapplied projection-like functions did not evaluate correctly.
module Issue498 where

data ⊤ : Set where
  tt : ⊤

data C : ⊤ → Set where
  c : C tt

data C₂ : ⊤ → ⊤ → Set where
  c : C₂ tt tt

module NoParams where

  f₁ : ∀ a → C a → ⊤
  f₁ a x = tt

  f₁′ : ∀ a → C a → ⊤
  f₁′ = f₁

  check₁ : ∀ a x → C (f₁′ a x)
  check₁ s x = c

  f₂ : ∀ a b → C₂ a b → ⊤
  f₂ a b x = tt

  f₂′ : ∀ a b → C₂ a b → ⊤
  f₂′ a = f₂ a

  check₂ : ∀ a b x → C (f₂′ a b x)
  check₂ a b x = c

  f₃ : ∀ a {b} → C₂ a b → ⊤
  f₃ a x = tt

  f₃′ : ∀ a {b} → C₂ a b → ⊤
  f₃′ = f₃

  data Is-f₃ : (∀ a {b} → C₂ a b → ⊤) → Set where
    is-f₃ : Is-f₃ (λ a {b} x → tt)

  check₃ : Is-f₃ f₃′
  check₃ = is-f₃

module SomeParams (X Y : Set) where

  f₁ : ∀ a → C a → ⊤
  f₁ a x = tt

  f₁′ : ∀ a → C a → ⊤
  f₁′ = f₁

  check₁ : ∀ a x → C (f₁′ a x)
  check₁ s x = c

  f₂ : ∀ a b → C₂ a b → ⊤
  f₂ a b x = tt

  f₂′ : ∀ a b → C₂ a b → ⊤
  f₂′ a = f₂ a

  check₂ : ∀ a b x → C (f₂′ a b x)
  check₂ a b x = c

check₃ : ∀ {X Y} a x → C (SomeParams.f₁′ X Y a x)
check₃ a x = c

check₄ : ∀ {X Y} a b x → C (SomeParams.f₂′ X Y a b x)
check₄ a b x = c

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
module huffman-tree where

open import lib

data huffman-tree : Set where
  ht-leaf : string → ℕ → huffman-tree
  ht-node : ℕ → huffman-tree → huffman-tree → huffman-tree

-- get the frequency out of a Huffman tree
ht-frequency : huffman-tree → ℕ
ht-frequency (ht-leaf _ f) = f
ht-frequency (ht-node f _ _) = f

-- lower frequency nodes are considered smaller
ht-compare : huffman-tree → huffman-tree → 𝔹
ht-compare h1 h2 = (ht-frequency h1) < (ht-frequency h2)

{- return (just s) if Huffman tree is an ht-leaf with string s;
   otherwise, return nothing (this is a constructor for the maybe type -- see maybe.agda in the IAL) -}
ht-string : huffman-tree → maybe string
ht-string (ht-leaf s f) = just s
ht-string _ = nothing

-- several helper functions for ht-to-string (defined at the bottom)
private
  -- helper function for ht-to-stringh
  ht-declare-node : huffman-tree → ℕ → string × string
  ht-declare-node h n =
    let cur = "n" ^ (ℕ-to-string n) in
      cur , (cur ^ " [label = \"" ^ (help (ht-string h)) ^ (ℕ-to-string (ht-frequency h)) ^ "\"];\n")
    where help : maybe string → string
          help (just s) = s ^ " , "
          help nothing = ""

  -- helper function for ht-to-stringh
  ht-attach : maybe string → string → string
  ht-attach nothing _ = ""
  ht-attach (just c) c' = c ^ " -> " ^ c' ^ ";\n"

  ht-to-stringh : huffman-tree → ℕ → maybe string → ℕ × string
  ht-to-stringh h n prev with ht-declare-node h n
  ht-to-stringh (ht-leaf _ _) n prev | c , s = suc n , (ht-attach prev c) ^ s
  ht-to-stringh (ht-node _ h1 h2) n prev | c , s with ht-to-stringh h1 (suc n) (just c)
  ht-to-stringh (ht-node _ h1 h2) _ prev | c , s | n , s1 with ht-to-stringh h2 n (just c)
  ht-to-stringh (ht-node _ h1 h2) _ prev | c , s | _ , s1 | n , s2 = n , (ht-attach prev c) ^ s ^ s1 ^ s2

{- turn a Huffman tree into a string in Graphviz format
   (you can render the output .gv file at http://sandbox.kidstrythisathome.com/erdos/) -}
ht-to-string : huffman-tree → string
ht-to-string h with ht-to-stringh h 0 nothing
ht-to-string h | _ , s = "digraph h {\nnode [shape = plaintext];\n" ^ s ^ "}"

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
-- Andreas, 2014-12-02, issue reported by Jesper Cockx

open import Common.Equality

mutual
  Type : Set
  type : Type

  data Term : Type → Set where
    set : Term type
  Type = Term type
  type = set

mutual
  weakenType : Type → Type → Type
  weaken : (ty ty' : Type) → Term ty → Term (weakenType ty' ty)

  weakenType ty ty' = subst Term {!!} (weaken type {!!} ty)
  weaken ty ty' t = {!!}

data Test : Type → Set where
  test : Test (weakenType type type)

-- Checking the constructor declaration was looping.
-- Termination checker should complain.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Intuitionistic propositional logic, vector-based de Bruijn approach, initial encoding

module Vi.Ip where

open import Lib using (Nat; suc; _+_; Fin; fin; Vec; _,_; proj; VMem; mem)

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Nat -> Set
Cx n = Vec Ty n

isTrue : forall {tn} -> Ty -> Fin tn -> Cx tn -> Set
isTrue a i tc = VMem a i tc

-- Terms

module Ip where
  infixl 1 _$_
  infixr 0 lam=>_
  data Tm {tn} (tc : Cx tn) : Ty -> Set where
    var    : forall {a i}   -> isTrue a i tc             -> Tm tc a
    lam=>_ : forall {a b}   -> Tm (tc , a) b             -> Tm tc (a => b)
    _$_    : forall {a b}   -> Tm tc (a => b) -> Tm tc a -> Tm tc b
    pair'  : forall {a b}   -> Tm tc a        -> Tm tc b -> Tm tc (a && b)
    fst    : forall {a b}   -> Tm tc (a && b)            -> Tm tc a
    snd    : forall {a b}   -> Tm tc (a && b)            -> Tm tc b
    left   : forall {a b}   -> Tm tc a                   -> Tm tc (a || b)
    right  : forall {a b}   -> Tm tc b                   -> Tm tc (a || b)
    case'  : forall {a b c} -> Tm tc (a || b) -> Tm (tc , a) c -> Tm (tc , b) c -> Tm tc c
    abort  : forall {a}     -> Tm tc FALSE               -> Tm tc a

  syntax pair' x y    = [ x , y ]
  syntax case' xy x y = case xy => x => y

  v : forall {tn} (k : Nat) {tc : Cx (suc (k + tn))} -> Tm tc (proj tc (fin k))
  v i = var (mem i)

  Thm : Ty -> Set
  Thm a = forall {tn} {tc : Cx tn} -> Tm tc a
open Ip public

-- Example theorems

t1 : forall {a b} -> Thm (a => NOT a => b)
t1 =
  lam=>
    lam=> abort (v 0 $ v 1)

t2 : forall {a b} -> Thm (NOT a => a => b)
t2 =
  lam=>
    lam=> abort (v 1 $ v 0)

t3 : forall {a} -> Thm (a => NOT (NOT a))
t3 =
  lam=>
    lam=> v 0 $ v 1

t4 : forall {a} -> Thm (NOT a <=> NOT (NOT (NOT a)))
t4 =
  [ lam=>
      lam=> v 0 $ v 1
  , lam=>
      lam=> v 1 $ (lam=> v 0 $ v 1)
  ]

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Selective.Libraries.ReceiveSublist where

open import Selective.ActorMonad public
open import Prelude

accept-sublist-unwrapped : (xs ys zs : InboxShape) → ∀{MT} → MT ∈ (xs ++ ys ++ zs) → Bool
accept-sublist-unwrapped [] [] zs p = false
accept-sublist-unwrapped [] (y ∷ ys) zs Z = true
accept-sublist-unwrapped [] (y ∷ ys) zs (S p) = accept-sublist-unwrapped [] ys zs p
accept-sublist-unwrapped (x ∷ xs) ys zs Z = false
accept-sublist-unwrapped (x ∷ xs) ys zs (S p) = accept-sublist-unwrapped xs ys zs p

accept-sublist : (xs ys zs : InboxShape) → MessageFilter (xs ++ ys ++ zs)
accept-sublist xs ys zs (Msg received-message-type received-fields) = accept-sublist-unwrapped xs ys zs received-message-type

record AcceptSublistDependent (IS : InboxShape) (accepted-type : MessageType) : Set₁ where
  field
    accepted-which : accepted-type ∈ IS
    fields : All receive-field-content accepted-type

receive-sublist : {i : Size} →
                  {Γ : TypingContext} →
                  (xs ys zs : InboxShape) →
                  ∞ActorM i (xs ++ ys ++ zs)
                            (Message ys)
                            Γ
                            (add-references Γ)
receive-sublist xs ys zs = do
    record { msg = Msg {MT} p f ; msg-ok = msg-ok } ← selective-receive (accept-sublist xs ys zs)
    let record {accepted-which = aw ; fields = fields } = rewrap-message xs ys zs p f msg-ok
    return₁ (Msg {MT = MT} aw fields)
  where
    rewrap-message : ∀{MT} →
                     (xs ys zs : InboxShape) →
                     (p : MT ∈ (xs ++ ys ++ zs)) →
                     All receive-field-content MT →
                     (accept-sublist-unwrapped xs ys zs p) ≡ true →
                     AcceptSublistDependent ys MT
    rewrap-message [] [] zs p f ()
    rewrap-message [] (x ∷ ys) zs Z f q = record { accepted-which = Z ; fields = f }
    rewrap-message [] (x ∷ ys) zs (S p) f q =
      let
        rec = rewrap-message [] ys zs p f q
        open AcceptSublistDependent
      in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields }
    rewrap-message (x ∷ xs) ys zs Z f ()
    rewrap-message (x ∷ xs) ys zs (S p) f q = rewrap-message xs ys zs p f q

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module x where

open import Level

private
  variable
    a b c d e f ℓ p q r : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e
    F : Set f

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

infixr 4 _,_
infixr 2 _^_

record _^_ (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B
open _^_

swap : A ^ B → B ^ A
swap (a , b) = b , a

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

infixr 1 _v_

data _v_ (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : (x : A) → A v B
  inr : (y : B) → A v B

cases : ∀ {A : Set a} {B : Set b} {C : Set c}
      → (A v B) → (A → C) → (B → C)
      → C
cases (inl q) f g = f q
cases (inr r) f g = g r

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

data ⊥ : Set where

⊥-elim : ∀ {A : Set a} → ⊥ → A
⊥-elim = λ ()

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

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

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

-- 4.1
assoc-^ : (A ^ B) ^ C  → A ^ (B ^ C)
assoc-^  ((a , b) , c) = a , (b , c)

-- 4.2
e4-2 : (¬ A v B) → (A → B)
e4-2 (inl ¬a) = λ a → ⊥-elim (¬a a)
e4-2 (inr  b) = λ _ → b

{- not provable
e4-2' : (A → B) → (¬ A v B)
e4-2' a→b = {!!}
-}

-- 4.3
e4-3 : (A v ¬ A) → (¬ ¬ A → A)
e4-3 (inl  a) = λ   _ → a
e4-3 (inr ¬a) = λ ¬¬a → ⊥-elim (¬¬a ¬a)

e4-3' : (A → ¬ ¬ A)
e4-3' = λ a ¬¬a → ¬¬a a

-- 4.4 -- this is similar to v elimination by cases
e4-4 : ((A ^ B) → C) → A → (B → C)
e4-4 a^b→c a = λ b → a^b→c (a , b)

-- 4.5
e4-5 : (A → (B → C)) → ((A ^ B) → C)
e4-5 a→b→c = λ (a , b) → a→b→c a b

e4-5' : ((A ^ B) → C) → (A → (B → C))
e4-5' a^b→c = λ a → λ b → a^b→c (a , b)

-- 4.6
e4-6 : A → (B v C) → ((A ^ B) v (A ^ C))
e4-6 a (inl b) = inl (a , b)
e4-6 a (inr c) = inr (a , c)

-- 4.7
e4-7 : (A → C) → (B → D) → ((A ^ B) → (C ^ D))
e4-7 a→c b→d = λ (a , b) → (a→c a , b→d b)

-- section 4.5.2

-- function composition
_∘_ : (B → C) → (A → B) → (A → C)
_∘_ b→c a→b = λ a -> b→c (a→b a)

srl : (A → B) → (¬ B → ¬ A)
srl a→b = λ ¬b a → ¬b (a→b a)

-- section 4.5.3
idA^A : (A ^ A) → (A ^ A)
idA^A (a , a') = (a' , a)

-- section 4.5.5 Conjunction and disjunction

s455 : ((A v B) → C) → ((A → C) ^ (B → C))
s455 = λ avb→c → (avb→c ∘ inl , avb→c ∘ inr)

s455' : ((A → C) ^ (B → C)) → ((A v B) → C)
s455' (a→c , b→c) = λ { (inl a) → a→c a
                      ; (inr b) → b→c b }

dm : ¬ (A v B) → (¬ A ^ ¬ B)
dm notAvB = (notAvB ∘ inl , notAvB ∘ inr)

dm' : (¬ A v ¬ B) → ¬ (A ^ B)
dm' (inl ¬a) = λ (a , _) → ¬a a
dm' (inr ¬b) = λ (_ , b) → ¬b b

-- 4.8
e4-8a : A → ¬ ¬ A
e4-8a a = λ ¬a → ¬a a

e4-8b : (B v C) → ¬ (¬ B ^ ¬ C)
e4-8b (inl b) = λ (¬b ,  _) → ¬b b
e4-8b (inr c) = λ ( _ , ¬c) → ¬c c

e4-8c : (A → B) → ((A → C) → (A → (B ^ C)))
e4-8c a→b = λ a→c → λ a → (a→b a , a→c a)

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
-- Andreas, 2021-04-22, issue #5339
-- Allow constructors of the same name in `constructor` block.

module _ where

module Works where

  interleaved mutual
    data Nat : Set
    data Fin : Nat → Set
    data _ where
      zero : Nat
    data _ where
      suc  : Nat → Nat
      zero : ∀ {n} → Fin (suc n)
    data _ where
      suc : ∀ {n} (i : Fin n) → Fin (suc n)

interleaved mutual
  data Nat : Set
  data Fin : Nat → Set
  data _ where
    zero : Nat
    suc  : Nat → Nat
    zero : ∀ {n} → Fin (suc n)
    suc  : ∀ {n} (i : Fin n) → Fin (suc n)

-- `data _ where` block should be accepted despite duplicate constructor names.

wkFin : ∀{n} → Fin n → Fin (suc n)
wkFin zero    = zero
wkFin (suc i) = suc (wkFin i)


text:
------------------------------------------------------------------------
-- IO
------------------------------------------------------------------------

{-# OPTIONS --no-termination-check #-}

module IO where

open import Coinduction
open import Data.Unit
open import Data.String
open import Data.Colist
import Foreign.Haskell as Haskell
import IO.Primitive as Prim

------------------------------------------------------------------------
-- The IO monad

-- One cannot write "infinitely large" computations with the
-- postulated IO monad in IO.Primitive without turning off the
-- termination checker (or going via the FFI, or perhaps abusing
-- something else). The following coinductive deep embedding is
-- introduced to avoid this problem. Possible non-termination is
-- isolated to the run function below.

infixl 1 _>>=_ _>>_

data IO : Set → Set₁ where
  lift   : ∀ {A} (m : Prim.IO A) → IO A
  return : ∀ {A} (x : A) → IO A
  _>>=_  : ∀ {A B} (m : ∞₁ (IO A)) (f : (x : A) → ∞₁ (IO B)) → IO B
  _>>_   : ∀ {A B} (m₁ : ∞₁ (IO A)) (m₂ : ∞₁ (IO B)) → IO B

-- The use of abstract ensures that the run function will not be
-- unfolded infinitely by the type checker.

abstract

  run : ∀ {A} → IO A → Prim.IO A
  run (lift m)   = m
  run (return x) = Prim.return x
  run (m  >>= f) = Prim._>>=_ (run (♭₁ m )) λ x → run (♭₁ (f x))
  run (m₁ >> m₂) = Prim._>>=_ (run (♭₁ m₁)) λ _ → run (♭₁ m₂)

------------------------------------------------------------------------
-- Utilities

-- Because IO A lives in Set₁ I hesitate to define sequence, which
-- would require defining a Set₁ variant of Colist.

mapM : ∀ {A B} → (A → IO B) → Colist A → IO (Colist B)
mapM f []       = return []
mapM f (x ∷ xs) = ♯₁ f x               >>= λ y  →
                  ♯₁ (♯₁ mapM f (♭ xs) >>= λ ys →
                  ♯₁ return (y ∷ ♯ ys))

-- The reason for not defining mapM′ in terms of mapM is efficiency
-- (the unused results could cause unnecessary memory use).

mapM′ : ∀ {A B} → (A → IO B) → Colist A → IO ⊤
mapM′ f []       = return _
mapM′ f (x ∷ xs) = ♯₁ f x >> ♯₁ mapM′ f (♭ xs)

------------------------------------------------------------------------
-- Simple lazy IO (UTF8-based)

getContents : IO Costring
getContents =
  ♯₁ lift Prim.getContents >>= λ s →
  ♯₁ return (Haskell.toColist s)

readFile : String → IO Costring
readFile f =
  ♯₁ lift (Prim.readFile f) >>= λ s →
  ♯₁ return (Haskell.toColist s)

writeFile∞ : String → Costring → IO ⊤
writeFile∞ f s =
  ♯₁ lift (Prim.writeFile f (Haskell.fromColist s)) >>
  ♯₁ return _

writeFile : String → String → IO ⊤
writeFile f s = writeFile∞ f (toCostring s)

putStr∞ : Costring → IO ⊤
putStr∞ s =
  ♯₁ lift (Prim.putStr (Haskell.fromColist s)) >>
  ♯₁ return _

putStr : String → IO ⊤
putStr s = putStr∞ (toCostring s)

putStrLn∞ : Costring → IO ⊤
putStrLn∞ s =
  ♯₁ lift (Prim.putStrLn (Haskell.fromColist s)) >>
  ♯₁ return _

putStrLn : String → IO ⊤
putStrLn s = putStrLn∞ (toCostring s)

max_issues_repo_name: larrytheliquid/Lemmachine


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Integers.RingStructure.Ring
open import Rings.IntegralDomains.Definition

module Numbers.Integers.RingStructure.IntegralDomain where

intDom : (a b : ℤ) → a *Z b ≡ nonneg 0 → (a ≡ nonneg 0 → False) → (b ≡ nonneg 0)
intDom (nonneg zero) (nonneg b) x a!=0 = exFalso (a!=0 x)
intDom (nonneg (succ a)) (nonneg zero) a!=0 _ = refl
intDom (nonneg zero) (negSucc b) pr a!=0 = exFalso (a!=0 pr)
intDom (negSucc a) (nonneg zero) _ _ = refl

ℤIntDom : IntegralDomain ℤRing
IntegralDomain.intDom ℤIntDom {a} {b} = intDom a b
IntegralDomain.nontrivial ℤIntDom ()