text:
------------------------------------------------------------------------------
-- LTC-PCF terms properties
------------------------------------------------------------------------------

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

module LTC-PCF.Base.Properties where

open import LTC-PCF.Base

------------------------------------------------------------------------------
-- Congruence properties

·-leftCong : ∀ {m n o} → m ≡ n → m · o ≡ n · o
·-leftCong refl = refl

·-rightCong : ∀ {m n o} → n ≡ o → m · n ≡ m · o
·-rightCong refl = refl

succCong : ∀ {m n} → m ≡ n → succ₁ m ≡ succ₁ n
succCong refl = refl

predCong : ∀ {m n} → m ≡ n → pred₁ m ≡ pred₁ n
predCong refl = refl

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

S≢0 : ∀ {n} → succ₁ n ≢ zero
S≢0 S≡0 = 0≢S (sym S≡0)

-- We added Common.Relation.Binary.PropositionalEquality.cong, so this
-- theorem is not necessary.
-- x≡y→Sx≡Sy : ∀ {m n} → m ≡ n → succ₁ m ≡
-- succ₁ n x≡y→Sx≡Sy refl = refl

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module README where

-- Formalization for "Decidability of Conversion for Setoid Type Theory"
-- Git repository: https://github.com/CoqHott/logrel-mltt/

------------------
-- INTRODUCTION --
------------------

-- A minimal library necessary for formalization:

-- The empty type and its elimination rule.
import Tools.Empty

-- The unit type.
import Tools.Unit

-- Sum type.
import Tools.Sum

-- Product type.
import Tools.Product

-- Identity function and composition.
import Tools.Function

-- Negation and decidability type.
import Tools.Nullary

-- Propositional equality and its properties.
import Tools.PropositionalEquality

-- Natural numbers and decidability of equality.
import Tools.Nat

-- Lists definition
import Tools.List

---------------------------
-- LANGUAGE INTRODUCTION --
---------------------------

-- Syntax and semantics of weakening and substitution.
import Definition.Untyped

-- Propositional equality properties: Equalities between expressions,
-- weakenings, substitutions and their combined composition.
-- (These lemmas are not in the paper.)
import Definition.Untyped.Properties

-- Judgements: Typing rules, conversion, reduction rules
-- and well-formed substitutions and respective equality.
import Definition.Typed

-- Well-formed context extraction and reduction properties.
import Definition.Typed.Properties

-- Well-formed weakening and its properties.
import Definition.Typed.Weakening

------------------------------
-- KRIPKE LOGICAL RELATIONS --
------------------------------

-- Generic equality relation definition.
import Definition.Typed.EqualityRelation

-- The judgemental instance of the generic equality.
import Definition.Typed.EqRelInstance

-- Logical relations definitions.
import Definition.LogicalRelation

-- Properties of logical relation:

-- Reflexivity of the logical relation.
import Definition.LogicalRelation.Properties.Reflexivity

-- Escape lemma for the logical relation.
import Definition.LogicalRelation.Properties.Escape

-- Shape view of two or more types.
import Definition.LogicalRelation.ShapeView

-- Proof irrelevance for the logical relation.
import Definition.LogicalRelation.Irrelevance

-- Weakening of logical relation judgements.
import Definition.LogicalRelation.Weakening

-- Conversion of the logical relation.
import Definition.LogicalRelation.Properties.Conversion

-- Symmetry of the logical relation.
import Definition.LogicalRelation.Properties.Symmetry

-- Transitvity of the logical relation.
import Definition.LogicalRelation.Properties.Transitivity

-- Neutral introduction in the logical relation.
import Definition.LogicalRelation.Properties.Neutral

-- Weak head expansion of the logical relation.
import Definition.LogicalRelation.Properties.Reduction

-- Application in the logical relation.
import Definition.LogicalRelation.Application

-- Validity judgements definitions
import Definition.LogicalRelation.Substitution

-- Properties of validity judgements:

-- Proof irrelevance for the validity judgements.
import Definition.LogicalRelation.Substitution.Irrelevance

-- Properties about valid substitutions:
-- * Substitution well-formedness.
-- * Substitution weakening.
-- * Substitution lifting.
-- * Identity substitution.
-- * Reflexivity, symmetry and transitivity of substitution equality.
import Definition.LogicalRelation.Substitution.Properties

-- Single term substitution of validity judgements.
import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

-- The fundamental theorem.
import Definition.LogicalRelation.Fundamental

-- Certain cases of the fundamental theorem

-- Validity of the universes
import Definition.LogicalRelation.Substitution.Introductions.Universe

-- Validity of the empty type and its eliminator
import Definition.LogicalRelation.Substitution.Introductions.Empty
import Definition.LogicalRelation.Substitution.Introductions.Emptyrec

-- Validity of natural numbers and its eliminator
import Definition.LogicalRelation.Substitution.Introductions.Nat
import Definition.LogicalRelation.Substitution.Introductions.Natrec

-- Validity of Π-types, abstractions and applications
import Definition.LogicalRelation.Substitution.Introductions.Pi
import Definition.LogicalRelation.Substitution.Introductions.Application
import Definition.LogicalRelation.Substitution.Introductions.Lambda

-- Validity of ∃-types, pairs and projections
import Definition.LogicalRelation.Substitution.Introductions.Sigma
import Definition.LogicalRelation.Substitution.Introductions.Pair
import Definition.LogicalRelation.Substitution.Introductions.Fst
import Definition.LogicalRelation.Substitution.Introductions.Snd

-- Validity of type casting and proof-irrelevant transport
import Definition.LogicalRelation.Substitution.Introductions.Castlemmas
import Definition.LogicalRelation.Substitution.Introductions.Cast
import Definition.LogicalRelation.Substitution.Introductions.CastPi
import Definition.LogicalRelation.Substitution.Introductions.Transp

-- Validity of identity types, and reflexivity
import Definition.LogicalRelation.Substitution.Introductions.Idlemmas
import Definition.LogicalRelation.Substitution.Introductions.IdUniv
import Definition.LogicalRelation.Substitution.Introductions.IdNat
import Definition.LogicalRelation.Substitution.Introductions.IdPi
import Definition.LogicalRelation.Substitution.Introductions.IdUPiPi
import Definition.LogicalRelation.Substitution.Introductions.IdRefl

-- Reducibility of well-formedness.
import Definition.LogicalRelation.Fundamental.Reducibility

-- Consequences of the fundamental theorem:

-- Consistency (no proof of False in the empty context) implies
-- canonicity of the system.
import Definition.Typed.Consequences.Canonicity

-- Injectivity of Π-types.
import Definition.Typed.Consequences.Injectivity

-- Syntactic validitiy of the system.
import Definition.Typed.Consequences.Syntactic

-- All types and terms fully reduce to WHNF.
import Definition.Typed.Consequences.Reduction

-- Strong equality of types.
import Definition.Typed.Consequences.Equality

-- Syntactic inequality of types.
import Definition.Typed.Consequences.Inequality

-- Substitution in judgements and substitution composition.
import Definition.Typed.Consequences.Substitution

-- Uniqueness of the types of neutral terms.
import Definition.Typed.Consequences.NeTypeEq

-- Consistency (0 is not judgementally equal to 1) of the type theory.
import Definition.Typed.Consequences.Consistency

-- Types can only belong to one universe (because of annotations)
-- also various inequalities for conversion
import Definition.Typed.Consequences.PiNorm
import Definition.Typed.Consequences.RelevanceUnicity

-- Terms can only admit one type
import Definition.Typed.Consequences.TypeUnicity

-- Various inversion results
import Definition.Typed.Consequences.TypeUnicity

------------------
-- DECIDABILITY --
------------------

-- Conversion algorithm definition.
import Definition.Conversion

-- Properties of conversion algorithm:

-- Context equality and its properties:
-- * Context conversion of typing judgements.
-- * Context conversion of reductions and algorithmic equality.
-- * Reflexivity and symmetry of context equality.
import Definition.Conversion.Stability

-- Soundness of the conversion algorithm.
import Definition.Conversion.Soundness

-- Results around normalisation of reflexive terms
import Definition.Conversion.FullReduction

-- Conversion property of algorithmic equality.
import Definition.Conversion.Conversion

-- Decidability of the conversion algorithm.
import Definition.Conversion.Decidable

-- Symmetry of the conversion algorithm.
import Definition.Conversion.Symmetry

-- Transitivity of the conversion algorithm.
import Definition.Conversion.Transitivity

-- Weakening of the conversion algorithm.
import Definition.Conversion.Weakening

-- WHNF and neutral lifting of the conversion algorithm.
import Definition.Conversion.Lift

-- Generic equality relation instance for the conversion algorithm.
import Definition.Conversion.EqRelInstance

-- Completeness of conversion algorithm.
import Definition.Conversion.Consequences.Completeness

-- Decidability of judgemental conversion.
import Definition.Conversion.HelperDecidable
import Definition.Typed.Decidable

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
open import Data.Nat using (suc)

open import Substitution using (rename-subst-commute; subst-commute)
open import DeBruijn

infix 3 _—→_

data _—→_ : ∀ {n} → Term n → Term n → Set where

  —→-ξₗ : ∀ {n} {M M′ N : Term n}
    → M —→ M′
      ---------------
    → M · N —→ M′ · N

  —→-ξᵣ : ∀ {n} {M N N′ : Term n}
    → N —→ N′
      ---------------
    → M · N —→ M · N′

  —→-ƛ : ∀ {n} {M M′ : Term (suc n)}
    → M —→ M′
      -----------
    → ƛ M —→ ƛ M′

  —→-β : ∀ {n} {M : Term (suc n)} {N : Term n}
      --------------------
    → (ƛ M) · N —→ M [ N ]

infix  3 _—↠_
infixr 3 _—→⟨_⟩_
infix  4 _∎

data _—↠_ : ∀ {n} → Term n → Term n → Set where

  _∎ : ∀ {n} (M : Term n)
      ------
    → M —↠ M

  _—→⟨_⟩_ : ∀ {n} {L N : Term n} (M : Term n)
    → M —→ L
    → L —↠ N
      ------
    → M —↠ N

—↠-trans : ∀ {n} {M L N : Term n}
  → M —↠ L
  → L —↠ N
    ------
  → M —↠ N
—↠-trans (M ∎)                 M—↠M = M—↠M
—↠-trans (M —→⟨ M—→L′ ⟩ L′—↠L) L—↠N = M —→⟨ M—→L′ ⟩ (—↠-trans L′—↠L L—↠N )

—↠-congₗ : ∀ {n} {M M′ R : Term n}
  → M —↠ M′
    ---------------
  → M · R —↠ M′ · R
—↠-congₗ {M = M}{R = R} (M ∎)                = M · R ∎
—↠-congₗ {M = M}{R = R} (M —→⟨ M—→L ⟩ L—↠M′) = M · R —→⟨ —→-ξₗ M—→L ⟩ —↠-congₗ L—↠M′

—↠-congᵣ : ∀ {n} {M M′ L : Term n}
  → M —↠ M′
    ---------------
  → L · M —↠ L · M′
—↠-congᵣ {M = M}{L = L} (M ∎)                = L · M ∎
—↠-congᵣ {M = M}{L = L} (M —→⟨ M—→L ⟩ L—↠M′) = L · M —→⟨ —→-ξᵣ M—→L ⟩ —↠-congᵣ L—↠M′

—↠-cong-ƛ : ∀ {n} {M M′ : Term (suc n)}
  → M —↠ M′
    -----------
  → ƛ M —↠ ƛ M′
—↠-cong-ƛ (M ∎)                = ƛ M ∎
—↠-cong-ƛ (M —→⟨ M—→L ⟩ L—↠N′) = ƛ M —→⟨ —→-ƛ M—→L ⟩ —↠-cong-ƛ L—↠N′

—↠-cong : ∀ {n} {M M′ N N′ : Term n}
  → M —↠ M′
  → N —↠ N′
    ----------------
  → M · N —↠ M′ · N′
—↠-cong M—↠M′ N—↠N′ = —↠-trans (—↠-congₗ M—↠M′) (—↠-congᵣ N—↠N′)

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
------------------------------------------------------------------------
-- Instantiates the ring solver with two copies of the same ring
------------------------------------------------------------------------

open import Algebra.RingSolver.AlmostCommutativeRing

module Algebra.RingSolver.Simple (r : AlmostCommutativeRing) where

open AlmostCommutativeRing r
import Algebra.RingSolver as R
open R rawRing r (-raw-almostCommutative⟶ r) public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Literals where

module Definition where
      module Natural where open import Light.Literals.Definition.Natural public
      module Negative where open import Light.Literals.Definition.Negative public

module Natural where open import Light.Literals.Natural public
module Level where open import Light.Literals.Level public
module Integer where open import Light.Literals.Integer public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Eq.LogicalTheory where

open import Prelude
open import T
open import DynTheory
open import SubstTheory
open import Contexts
open import Eq.Defs
open import Eq.KleeneTheoryEarly

-- Closed equivalence is contained in open
closed-logical-imp-open : ∀{A} → LogicalEq A ⊆ OLogicalEq [] A
closed-logical-imp-open {A} {e} {e'} leq {γ} {γ'} η =
  ID.coe2 (LogicalEq A) (symm (closed-subst γ e)) (symm (closed-subst γ' e')) leq

-- Theory about logical equivalence

logical-sym : ∀{A} → Symmetric (LogicalEq A)
logical-sym {nat} eq = kleene-sym eq
logical-sym {A ⇒ B} equiv = λ e₁ e₁' x → logical-sym {B}
                                          (equiv e₁' e₁ (logical-sym {A} x))

logical-trans : ∀{A} → Transitive (LogicalEq A)
logical-trans {nat} eq1 eq2 = kleene-trans eq1 eq2
logical-trans {A ⇒ B} {e} {e'} {e''} eq1 eq2 =
   λ e₁ e₁' x → logical-trans (eq1 e₁ e₁ (logical-trans x (logical-sym x))) (eq2 e₁ e₁' x)

logicalγ-sym : ∀{Γ} → Symmetric (LogicalEqΓ Γ)
logicalγ-sym η n = logical-sym (η n)
logicalγ-trans : ∀{Γ} → Transitive (LogicalEqΓ Γ)
logicalγ-trans η η' n = logical-trans (η n) (η' n)

-- Open logical theory
ological-sym : ∀{Γ} {A} → Symmetric (OLogicalEq Γ A)
ological-sym eq η = logical-sym (eq (logicalγ-sym η))

-- This uses the trick where, despite not having reflexivity yet,
-- we show that some element x is reflexive by using symmetry and
-- transitivity on a proof of x ~ y that we have.
-- I find this trick hilarious.
ological-trans : ∀{Γ} {A} → Transitive (OLogicalEq Γ A)
ological-trans eq eq' η = logical-trans (eq η)
                          (eq' (logicalγ-trans (logicalγ-sym η) η))

logical-converse-evaluation-1 : ∀{A} {e e' d : TCExp A} →
                                e ~ e' :: A →
                                d ~>* e →
                                d ~ e' :: A
logical-converse-evaluation-1 {nat} eq eval = kleene-converse-evaluation eq eval
logical-converse-evaluation-1 {A ⇒ B} eq eval =
  λ e₁ e₁' x → logical-converse-evaluation-1 (eq e₁ e₁' x)
               (eval-compat step-app-l eval)

logical-converse-evaluation : ∀{A} {e e' d d' : TCExp A} →
                              e ~ e' :: A →
                              d ~>* e →
                              d' ~>* e' →
                              d ~ d' :: A
logical-converse-evaluation eq eval1 eval2 with logical-converse-evaluation-1 eq eval1
... | eq1 with logical-converse-evaluation-1 (logical-sym eq1) eval2
... | eq2 = logical-sym eq2

-- This is the hard one.
ological-refl : ∀{Γ} {A} → (e : TExp Γ A) → Γ ⊢ e ~ e :: A
ological-refl (var x) η = η x
ological-refl {Γ} {A ⇒ B} (Λ e) {γ = γ} {γ' = γ'} η = lam-case
  where lam-case : (e₁ e₁' : TExp [] A) → LogicalEq A e₁ e₁' →
                    LogicalEq B (Λ (ssubst (liftγ γ) e) $ e₁) (Λ (ssubst (liftγ γ') e) $ e₁')
        lam-case e₁ e₁' arg-eq with ological-refl e (extendLogicalEQΓ η arg-eq)
        ... | equiv with combine-subst-noob γ e e₁ | combine-subst-noob γ' e e₁'
        ... | eq1 | eq2 with ID.coe2 (LogicalEq B) eq1 eq2 equiv
        ... | equiv' = logical-converse-evaluation equiv'
                       (eval-step step-beta) (eval-step step-beta)
ological-refl (e $ e') η with ological-refl e η | ological-refl e' η
... | eq-e | eq-e' = eq-e _ _ eq-e'
ological-refl zero η = kleeneq zero val-zero eval-refl eval-refl
ological-refl (suc e) η with ological-refl e η
... | kleeneq n val S1 S2 = kleeneq (suc n) (val-suc val)
                            (eval-compat step-suc S1) (eval-compat step-suc S2)
ological-refl {Γ} {A} (rec e e0 es) {γ = γ} {γ' = γ'} η with ological-refl e η
... | kleeneq n val E1 E2 = logical-converse-evaluation (inner val)
                            (eval-compat step-rec E1) (eval-compat step-rec E2)
  where inner : {n : TNat} (val : TVal n) →
                ((rec n (ssubst γ e0) (ssubst (liftγ γ) es)) ~
                 (rec n (ssubst γ' e0) (ssubst (liftγ γ') es)) :: A)
        inner val-zero = logical-converse-evaluation (ological-refl e0 η)
                         (eval-step step-rec-z) (eval-step step-rec-z)
        inner (val-suc val) with ological-refl es (extendLogicalEQΓ η (inner val))
        ... | equiv with combine-subst-noob γ es _ | combine-subst-noob γ' es _
        ... | eq1 | eq2 with ID.coe2 (LogicalEq A) eq1 eq2 equiv
        ... | equiv' = logical-converse-evaluation equiv'
                       (eval-step (step-rec-s val)) (eval-step (step-rec-s val))

ological-refl' : ∀{Γ} {A} → Reflexive (OLogicalEq Γ A)
ological-refl' {x = x} = ological-refl x

-- Extend it back to closed terms and to substitutions
logical-refl : ∀{A} → Reflexive (LogicalEq A)
logical-refl {x = e} with ological-refl e (emptyLogicalEqΓ {γ = emptyγ} {γ' = emptyγ})
... | leq = ID.coe2 (LogicalEq _) (subid e) (subid e) leq

logicalγ-refl : ∀{Γ} → Reflexive (LogicalEqΓ Γ)
logicalγ-refl n = logical-refl

logical-is-equivalence : ∀{A : TTp} → IsEquivalence (LogicalEq A)
logical-is-equivalence = record { refl_ = logical-refl
                                ; sym_ = logical-sym
                                ; trans_ = logical-trans }
logicalγ-is-equivalence : ∀{Γ : Ctx} → IsEquivalence (LogicalEqΓ Γ)
logicalγ-is-equivalence = record { refl_ = λ {γ} → logicalγ-refl {_} {γ}
                                 ; sym_ = logicalγ-sym
                                 ; trans_ = logicalγ-trans }

-- I do not understand why these need to be eta expanded
ological-is-equivalence : ∀{Γ : Ctx} {A : TTp} → IsEquivalence (OLogicalEq Γ A)
ological-is-equivalence = record { refl_ = λ {e} → ological-refl' {_} {_} {e}
                                 ; sym_ = λ {e e'} → ological-sym {_} {_} {e} {e'}
                                 ; trans_ = λ {e e' e''} → ological-trans {_} {_} {e} {e'} {e''}}

-- This is basically the same proof as reflexivity...?
-- That's weird.
ological-is-congruence : Congruence OLogicalEq
ological-is-congruence leq ∘ η = leq η
ological-is-congruence leq (e₁ e$ C) η with ological-is-congruence leq C η | ological-refl e₁ η
... | equiv-rhs | equiv-lhs = equiv-lhs _ _ equiv-rhs
ological-is-congruence leq (C $e e₂) η with ological-is-congruence leq C η | ological-refl e₂ η
... | equiv-lhs | equiv-rhs = equiv-lhs _ _ equiv-rhs
ological-is-congruence {e = e} {e' = e'} leq (Λ C) {γ = γ} {γ' = γ'} η = body
  where -- I feel like I shouldn't have to give so much type information here.
        body : (e₁ e₁' : TExp [] _) →
                LogicalEq _ e₁ e₁' →
                LogicalEq _ (Λ (ssubst (liftγ _) (C < e >)) $ e₁)
               (Λ (ssubst (liftγ _) (C < e' >)) $ e₁')
        body e₁ e₁' arg-eq with ological-is-congruence {e = e} {e' = e'} leq C (extendLogicalEQΓ η arg-eq)
        ... | equiv with combine-subst-noob γ (C < e >) e₁ | combine-subst-noob γ' (C < e' >) e₁'
        ... | eq1 | eq2 with ID.coe2 (LogicalEq _) eq1 eq2 equiv
        ... | equiv' = logical-converse-evaluation equiv'
                       (eval-step step-beta) (eval-step step-beta)
ological-is-congruence leq (suc C) η with ological-is-congruence leq C η
... | kleeneq n val S1 S2 = kleeneq (suc n) (val-suc val)
                            (eval-compat step-suc S1) (eval-compat step-suc S2)
-- Is there a way to abstract out all the shit in these three bits?
ological-is-congruence {e = e} {e' = e'} leq {A' = A'} (rec1 C e0 es) {γ = γ} {γ' = γ'} η
  with ological-is-congruence leq C η
... | kleeneq n val E1 E2 = logical-converse-evaluation (inner val)
                            (eval-compat step-rec E1) (eval-compat step-rec E2)
  where inner : {n : TNat} (val : TVal n) →
                ((rec n (ssubst γ e0) (ssubst (liftγ γ) es)) ~
                 (rec n (ssubst γ' e0) (ssubst (liftγ γ') es)) :: A')
        inner val-zero = logical-converse-evaluation (ological-refl e0 η)
                         (eval-step step-rec-z) (eval-step step-rec-z)
        inner (val-suc val) with ological-refl es (extendLogicalEQΓ η (inner val))
        ... | equiv with combine-subst-noob γ es _ | combine-subst-noob γ' es _
        ... | eq1 | eq2 with ID.coe2 (LogicalEq A') eq1 eq2 equiv
        ... | equiv' = logical-converse-evaluation equiv'
                       (eval-step (step-rec-s val)) (eval-step (step-rec-s val))

ological-is-congruence {e = e} {e' = e'} leq {A' = A'} (rec2 en C es) {γ = γ} {γ' = γ'} η
  with ological-refl en η
... | kleeneq n val E1 E2 = logical-converse-evaluation (inner val)
                            (eval-compat step-rec E1) (eval-compat step-rec E2)
  where inner : {n : TNat} (val : TVal n) →
                ((rec n (ssubst γ (C < e >)) (ssubst (liftγ γ) es)) ~
                 (rec n (ssubst γ' (C < e' >)) (ssubst (liftγ γ') es)) :: A')
        inner val-zero = logical-converse-evaluation (ological-is-congruence leq C η)
                         (eval-step step-rec-z) (eval-step step-rec-z)
        inner (val-suc val) with ological-refl es (extendLogicalEQΓ η (inner val))
        ... | equiv with combine-subst-noob γ es _ | combine-subst-noob γ' es _
        ... | eq1 | eq2 with ID.coe2 (LogicalEq A') eq1 eq2 equiv
        ... | equiv' = logical-converse-evaluation equiv'
                       (eval-step (step-rec-s val)) (eval-step (step-rec-s val))

ological-is-congruence {e = e} {e' = e'} leq {A' = A'} (rec3 en e0 C) {γ = γ} {γ' = γ'} η
  with ological-refl en η
... | kleeneq n val E1 E2 = logical-converse-evaluation (inner val)
                            (eval-compat step-rec E1) (eval-compat step-rec E2)
  where inner : {n : TNat} (val : TVal n) →
                ((rec n (ssubst γ e0) (ssubst (liftγ γ) (C < e >))) ~
                 (rec n (ssubst γ' e0) (ssubst (liftγ γ') (C < e' >))) :: A')
        inner val-zero = logical-converse-evaluation (ological-refl e0 η)
                         (eval-step step-rec-z) (eval-step step-rec-z)
        inner (val-suc val) with ological-is-congruence leq C (extendLogicalEQΓ η (inner val))
        ... | equiv with combine-subst-noob γ (C < e >) _ | combine-subst-noob γ' (C < e' >) _
        ... | eq1 | eq2 with ID.coe2 (LogicalEq A') eq1 eq2 equiv
        ... | equiv' = logical-converse-evaluation equiv'
                       (eval-step (step-rec-s val)) (eval-step (step-rec-s val))

ological-consistent : Consistent OLogicalEq
ological-consistent leq with leq (emptyLogicalEqΓ {γ = emptyγ} {γ' = emptyγ})
... | keq = ID.coe2 KleeneEq (subid _) (subid _) keq

ological-equiv-nat-val : (e : TNat) → Σ[ n :: TNat ] (TVal n × ([] ⊢ e ~ n :: nat))
ological-equiv-nat-val e with ological-consistent {e = e} {e' = e} (ological-refl e)
... | kleeneq n val E1 E2 = n , (val , (closed-logical-imp-open (kleeneq n val E1 eval-refl)))

log-is-con-congruence : IsConsistentCongruence OLogicalEq
log-is-con-congruence = record { equiv = ological-is-equivalence
                               ; cong = ological-is-congruence
                               ; consistent = ological-consistent
                               }

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
-- Pattern matching on a datatype in Prop is disallowed

{-# OPTIONS --enable-prop #-}

open import Agda.Builtin.Bool

data TestProp : Prop where
  p₁ p₂ : TestProp

toBool : TestProp → Bool
toBool p₁ = true
toBool p₂ = false

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

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

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.DirectSum.DirectSumFun.Base

private variable
  ℓ : Level

open GroupTheory
open AbGroupStr

-----------------------------------------------------------------------------
-- AbGroup Properties

module DSF-properties
  (G : ℕ → Type ℓ)
  (Gstr : (n : ℕ) → AbGroupStr (G n))
  where

  private
    GG : ℕ → Group ℓ
    GG n = AbGroup→Group ((G n) , (Gstr n))

  isSet⊕Fun : isSet (⊕Fun G Gstr)
  isSet⊕Fun = isSetΣSndProp (isSetΠ (λ n → is-set (Gstr n))) (λ _ → squash₁)

  -- Object
  0⊕Fun : ⊕Fun G Gstr
  0⊕Fun = (λ n → 0g (Gstr n)) , ∣ (0 , λ n p → refl) ∣₁

  _+⊕Fun_ : ⊕Fun G Gstr → ⊕Fun G Gstr → ⊕Fun G Gstr
  _+⊕Fun_ (f , Anf) (g , Ang) = f+g , Anf+g Anf Ang
    where
    f+g = λ n → Gstr n ._+_ (f n) (g n)
    Anf+g : AlmostNullP G Gstr f → AlmostNullP G Gstr g → AlmostNullP G Gstr f+g
    Anf+g = PT.rec2 squash₁
            (λ { (k , nf) → λ { (l , ng) →
               ∣ ((k +n l) ,
                 (λ n p → cong₂ ((Gstr n)._+_) (nf n (<-+k-trans p)) (ng n (<-k+-trans p))
                           ∙ +IdR (Gstr n) (0g (Gstr n)))) ∣₁ } })

  Inv⊕Fun : ⊕Fun G Gstr → ⊕Fun G Gstr
  Inv⊕Fun (f , Anf) = f- , Anf- Anf
    where
    f- = λ n → (Gstr n).-_ (f n)
    Anf- : AlmostNullP G Gstr f → AlmostNullP G Gstr f-
    Anf- = PT.rec squash₁
           (λ { (k , nf) →
              ∣ (k , λ n p → cong ((Gstr n).-_) (nf n p) ∙ inv1g (GG n)) ∣₁})

  -- AbGroup Properties
  +⊕FunAssoc : (x y z : ⊕Fun G Gstr) → x +⊕Fun (y +⊕Fun z) ≡ (x +⊕Fun y) +⊕Fun z
  +⊕FunAssoc (f , Anf) (g , Ang) (h , Anh) =
             ΣPathTransport→PathΣ _ _
             (funExt (λ n → Gstr n .+Assoc _ _ _) , (squash₁ _ _))

  +⊕FunRid : (x : ⊕Fun G Gstr) → x +⊕Fun 0⊕Fun ≡ x
  +⊕FunRid (f , Anf) = ΣPathTransport→PathΣ _ _
                       ((funExt (λ n → +IdR (Gstr n) _)) , squash₁ _ _)

  +⊕FunInvR : (x : ⊕Fun G Gstr) → x +⊕Fun Inv⊕Fun x ≡ 0⊕Fun
  +⊕FunInvR (f , Anf) = ΣPathTransport→PathΣ _ _
                        ((funExt (λ n → +InvR (Gstr n) _)) , (squash₁ _ _))

  +⊕FunComm : (x y : ⊕Fun G Gstr) →  x +⊕Fun y ≡ y +⊕Fun x
  +⊕FunComm (f , Anf) (g , Ang) = ΣPathTransport→PathΣ _ _
                                  ((funExt (λ n → Gstr n .+Comm _ _)) , (squash₁ _ _))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --safe #-}
module Issue2487-2 where

import Issue2487.A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module MakeTracks where

open import Data.Fin        using (Fin; #_; toℕ)
open import Data.List       using (List; _∷_; []; map; concat; _++_; replicate; zip; length; take; drop)
open import Data.Nat        using (_*_; ℕ; suc; _+_)
open import Data.Nat.Show   using (show)
open import Data.Product    using (_,_; uncurry)
open import Data.Vec        using (fromList; toList; Vec; _∷_; []; lookup) renaming (replicate to rep; zip to vzip; map to vmap; concat to vconcat; _++_ to _+v_)

open import Instruments
open import Interval
open import Note
open import Pitch
open import MidiEvent
open import Util            using (fins')
open import Transformation

velocity : Velocity
velocity = # 60

makeTrack : InstrumentNumber-1 → ℕ → Channel-1 → List Note → MidiTrack
makeTrack inst tempo n notes = track (show (suc (toℕ n))) inst n tempo (notes→events velocity notes)

makeTracks : {k : Fin maxChannels} → Vec InstrumentNumber-1 maxChannels → ℕ → Vec (List Note) (toℕ k) → Vec MidiTrack (toℕ k)
makeTracks {k} insts tempo lines =
  vmap (λ (i , ns) → makeTrack (lookup insts i) tempo i ns)
       (vzip (fins' maxChannels k) lines)

makeTrackList : {k : Fin maxChannels} → Vec InstrumentNumber-1 maxChannels → ℕ → Vec (List Note) (toℕ k) → List MidiTrack
makeTrackList insts tempo lines = toList (makeTracks insts tempo lines)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Oscar.Data.Term.ThickAndThin {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Class.ThickAndThin
open import Oscar.Data.Term FunctionName
import Oscar.Data.Term.ThickAndThin.internal FunctionName as ⋆

instance ThickAndThinTerm : ThickAndThin Term
ThickAndThin.thin ThickAndThinTerm = ⋆.thin
ThickAndThin.thin-injective ThickAndThinTerm = ⋆.thin-injective
ThickAndThin.thick ThickAndThinTerm = ⋆.thick
ThickAndThin.thick∘thin=id ThickAndThinTerm = {!!}
ThickAndThin.check ThickAndThinTerm = {!!}
ThickAndThin.thin-check-id ThickAndThinTerm = {!!}

instance ThickAndThinTerms : ∀ {N} → ThickAndThin (Terms N)
ThickAndThin.thin ThickAndThinTerms x = ⋆.thins x
ThickAndThin.thin-injective ThickAndThinTerms y = ⋆.thins-injective y
ThickAndThin.thick ThickAndThinTerms = ⋆.thicks
ThickAndThin.thick∘thin=id ThickAndThinTerms = {!!}
ThickAndThin.check ThickAndThinTerms = {!!}
ThickAndThin.thin-check-id ThickAndThinTerms = {!!}

open import Oscar.Data.Fin
open import Oscar.Data.Fin.ThickAndThin
open import Oscar.Data.Maybe.properties
open import Oscar.Data.Nat

_for_ : ∀ {n} → Term n → Fin (suc n) → suc n ⊸ n
(t' for x) y = maybe i t' ((check x y))


text:
open import dynamics-core

module focus-formation where
  -- every ε is an evaluation context -- trivially, here, since we don't
  -- include any of the premises in red brackets about finality
  focus-formation : ∀{d d' ε} → d == ε ⟦ d' ⟧ → ε evalctx
  focus-formation (FHPlus1 sub) = ECPlus1 (focus-formation sub)
  focus-formation (FHPlus2 sub) = ECPlus2 (focus-formation sub)
  focus-formation FHOuter = ECDot
  focus-formation (FHAp1 sub) = ECAp1 (focus-formation sub)
  focus-formation (FHAp2 sub) = ECAp2 (focus-formation sub)
  focus-formation (FHInl sub) = ECInl (focus-formation sub)
  focus-formation (FHInr sub) = ECInr (focus-formation sub)
  focus-formation (FHCase sub) = ECCase (focus-formation sub)
  focus-formation (FHFst sub) = ECFst
  focus-formation (FHSnd sub) = ECSnd
  focus-formation (FHPair1 sub) = ECPair1 (focus-formation sub)
  focus-formation (FHPair2 sub) = ECPair2 (focus-formation sub)
  focus-formation (FHNEHole sub) = ECNEHole (focus-formation sub)
  focus-formation (FHCast sub) = ECCast (focus-formation sub)
  focus-formation (FHFailedCast x) = ECFailedCast (focus-formation x)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{- This file describes properties of computable relations. -}

open import bool
open import level
open import eq
open import product
open import product-thms

module bool-relations {ℓ : level}{A : Set ℓ} (_≤A_ : A → A → 𝔹) where

reflexive : Set (ℓ)
reflexive = ∀ {a : A} → a ≤A a ≡ tt

transitive : Set (ℓ)
transitive = ∀ {a b c : A} → a ≤A b ≡ tt → b ≤A c ≡ tt → a ≤A c ≡ tt

total : Set ℓ
total = ∀ {a b : A} → a ≤A b ≡ ff → b ≤A a ≡ tt

total-reflexive : total → reflexive
total-reflexive tot {a} with keep (a ≤A a)
total-reflexive tot {a} | tt , p = p
total-reflexive tot {a} | ff , p = tot p

_iso𝔹_ : A → A → 𝔹
d iso𝔹 d' = d ≤A d' && d' ≤A d

iso𝔹-intro : ∀{x y : A} → x ≤A y ≡ tt → y ≤A x ≡ tt → x iso𝔹 y ≡ tt
iso𝔹-intro p1 p2 rewrite p1 | p2 = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import lib.Basics
open import lib.types.Truncation
open import lib.types.Groupoid
open import lib.types.PathSet

module lib.types.FundamentalGroupoid {i} (A : Type i) where

  fundamental-groupoid : Groupoid
  fundamental-groupoid = record
    { El = A
    ; Arr = _=₀_ {A = A}
    ; Arr-level = λ _ _ → Trunc-level
    ; groupoid-struct = record
      { id = idp₀
      ; inv = !₀
      ; comp = _∙₀_
      ; unit-l = ∙₀-unit-l
      ; unit-r = ∙₀-unit-r
      ; assoc = ∙₀-assoc
      ; inv-l = !₀-inv-l
      ; inv-r = !₀-inv-r
      }
    }

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module _ where

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

module Vars (A : Set) where
  variable
    x : A

-- Was
--   An internal error has occurred. Please report this as a bug.
--   Location of the error: src/full/Agda/TypeChecking/Reduce/Fast.hs:148
-- Should be
--   Cannot use generalized variable from let-opened module
record R : Set₁ where
  field
    A : Set
  open Vars A
  field
    f : x ≡ x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Logic where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Relation.Nullary.Decidable
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Agda.Primitive
{-# FOREIGN AGDA2HS
import Data.Nat
#-}

---- Equational reasoning
useEq : {x y : Bool} -> x ≡ y -> .(IsTrue x) -> IsTrue y
useEq {true} {true} eq is = IsTrue.itsTrue

useEqFalse : {x y : Bool} -> x ≡ y -> .(IsFalse x) -> IsFalse y
useEqFalse {false} {false} eq is = IsFalse.itsFalse

isTrueToEquiv : {c : Bool} -> IsTrue c -> c ≡ true
isTrueToEquiv {true} p = refl

isFalseToEquiv : {c : Bool} -> IsFalse c -> c ≡ false
isFalseToEquiv {false} p = refl

-- symmetry of equality
sym : {u : Level} {A : Set u} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

-- transitivity of equality
trans : {u : Level} {A : Set u} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

-- congruence of equality
cong : {u v : Level} {A : Set u} {B : Set v} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

cong2 : {A B T : Set} {a1 a2 : A} {b1 b2 : B} → (f : A → B -> T) → a1 ≡ a2 -> b1 ≡ b2 → f a1 b1 ≡ f a2 b2
cong2 f refl refl = refl

cong3 : {A B C T : Set} {a1 a2 : A} {b1 b2 : B} {c1 c2 : C} → (f : A → B -> C -> T) → a1 ≡ a2 -> b1 ≡ b2 -> c1 ≡ c2 → f a1 b1 c1 ≡ f a2 b2 c2
cong3 f refl refl refl = refl

cong4 : {A B C D T : Set} {a1 a2 : A} {b1 b2 : B} {c1 c2 : C} {d1 d2 : D} → (f : A → B -> C -> D -> T) → a1 ≡ a2 -> b1 ≡ b2 → c1 ≡ c2 -> d1 ≡ d2 -> f a1 b1 c1 d1 ≡ f a2 b2 c2 d2
cong4 f refl refl refl refl = refl

begin_ : {u : Level} {A : Set u} → {x y : A} → x ≡ y → x ≡ y
begin p = p

_end : {u : Level} {A : Set u} → (x : A) → x ≡ x
x end = refl

_=⟨_⟩_ : {u : Level} {A : Set u} → (x : A) → {y z : A}
       → x ≡ y → y ≡ z → x ≡ z
x =⟨ p ⟩ q = trans p q

_=⟨⟩_ : {u : Level} {A : Set u} → (x : A) → {y : A} → x ≡ y → x ≡ y
x =⟨⟩ q = x =⟨ refl ⟩ q

infix   1  begin_
infix   3  _end
infixr  2  _=⟨_⟩_
infixr  2  _=⟨⟩_

---- General purpose proofs

propZeroImpliesLtOne : (x : Nat) -> IsFalse (x == 0) -> IsFalse (x < 1)
propZeroImpliesLtOne Z notZ = notZ
propZeroImpliesLtOne (S x) notZ = IsFalse.itsFalse

propFnIf : {a b : Set} -> {c : Bool} {x y : a} (f : a -> b) -> (if c then f x else f y) ≡ f (if c then x else y)
propFnIf {c = false} f = refl
propFnIf {c = true} f = refl

propMaxSuc : (x y : Nat) -> max (S x) (S y) ≡ S (max x y)
propMaxSuc Z Z = refl
propMaxSuc Z (S y) = refl
propMaxSuc (S x) Z = refl
propMaxSuc (S x) (S y) =
  begin
    max (S $ S x) (S $ S y)
  =⟨⟩
    (if x < y then (S $ S y) else (S $ S x))
  =⟨ propFnIf S ⟩
    (S $ (if x < y then (S y) else (S x)))
  =⟨⟩
    S (max (S x) (S y))
  end

propMaxRefl : (x y : Nat) -> max x y ≡ max y x
propMaxRefl Z Z = refl
propMaxRefl Z (S y) = refl
propMaxRefl (S x) Z = refl
propMaxRefl (S x) (S y) =
  begin
    max (S x) (S y)
  =⟨ propMaxSuc x y ⟩
    S (max x y)
  =⟨ cong S (propMaxRefl x y) ⟩
    S (max y x)
  =⟨ sym $ propMaxSuc y x ⟩
    max (S y) (S x)
  end

propIsTrueCombine2 : {a b : Bool} -> IsTrue a -> IsTrue b -> IsTrue (a && b)
propIsTrueCombine2 {true} {true} ta tb = IsTrue.itsTrue

propIsTrueCombine4 : {a b c d : Bool} -> IsTrue a -> IsTrue b -> IsTrue c -> IsTrue d -> IsTrue ((a && b) && (c && d))
propIsTrueCombine4 {true} {true} {true} {true} ta tb tc td = IsTrue.itsTrue

propIsTrueCombine4Alt : {a b c d : Bool} -> IsTrue a -> IsTrue b -> IsTrue c -> IsTrue d -> IsTrue (a && b && c && d)
propIsTrueCombine4Alt {true} {true} {true} {true} ta tb tc td = IsTrue.itsTrue

andRefl : (a b : Bool) -> (a && b) ≡ (b && a)
andRefl false false = refl
andRefl false true = refl
andRefl true false = refl
andRefl true true = refl

orFst : {a b : Bool} -> IsTrue a -> IsTrue (a || b)
orFst {true} {b} ap = IsTrue.itsTrue

andFst : {a b : Bool} -> IsTrue (a && b) -> IsTrue a
andFst {true} {true} ab = IsTrue.itsTrue

andSnd : {a b : Bool} -> IsTrue (a && b) -> IsTrue b
andSnd {true} {true} ab = IsTrue.itsTrue

andSndI : {a b : Bool} -> .(IsTrue (a && b)) -> IsTrue b
andSndI {true} {true} ab = IsTrue.itsTrue

and1 : {a b c d : Bool} -> IsTrue (a && b && c && d) -> IsTrue a
and1 {true} {true} {true} {true} abcd = IsTrue.itsTrue

and2 : {a b c d : Bool} -> IsTrue (a && b && c && d) -> IsTrue b
and2 {true} {true} {true} {true} abcd = IsTrue.itsTrue

and3 : {a b c d : Bool} -> IsTrue (a && b && c && d) -> IsTrue c
and3 {true} {true} {true} {true} abcd = IsTrue.itsTrue

and4 : {a b c d : Bool} -> IsTrue (a && b && c && d) -> IsTrue d
and4 {true} {true} {true} {true} abcd = IsTrue.itsTrue

andCombine : {a b : Bool} -> IsTrue a -> IsTrue b -> IsTrue (a && b)
andCombine {true} {true} ta tb = IsTrue.itsTrue

boolAndTrue : (a : Bool) -> (a && true) ≡ a
boolAndTrue false = refl
boolAndTrue true = refl

ifTrue : {u : Level} {t : Set u} {a b : t} (c : Bool) -> IsTrue c -> (if c then a else b) ≡ a
ifTrue true tc = refl

ifFalse : {t : Set} {a b : t} (c : Bool) -> IsFalse c -> (if c then a else b) ≡ b
ifFalse false fc = refl

infix -2 ifc_then_else_
ifc_then_else_ : {u : Level} {a : Set u} → (c : Bool) → ({{IsTrue c}} → a) → ({{IsFalse c}} → a) → a
ifc false then x else y = y {{IsFalse.itsFalse}}
ifc true then x else y = x {{IsTrue.itsTrue}}
{-# COMPILE AGDA2HS ifc_then_else_ #-}

ifcTrue : {u : Level} {t : Set u} -> (c : Bool) {a : {{.(IsTrue c)}} -> t} {b : {{.(IsFalse c)}} -> t} -> .(ct : IsTrue c) -> (ifc c then (λ {{p}} -> a) else (λ {{p}} -> b)) ≡ (a {{ct}})
ifcTrue true {a} {b} ct = refl

ifcFalse : {u : Level} {t : Set u} -> (c : Bool) {a : {{.(IsTrue c)}} -> t} {b : {{.(IsFalse c)}} -> t} -> .(ct : IsFalse c) -> (ifc c then (λ {{p}} -> a) else (λ {{p}} -> b)) ≡ (b {{ct}})
ifcFalse false {a} {b} ct = refl

propFnIfc : {a b : Set} -> (c : Bool) {x : {{IsTrue c}} -> a} {y : {{IsFalse c}} -> a} (f : a -> b)
  -> (ifc c then f x else f y) ≡ f (ifc c then x else y)
propFnIfc false f = refl
propFnIfc true f = refl

propFnDistributeIfc2 : {a b : Set} -> (c1 c2 : Bool) {w x y z : a} (f : a -> b)
  -> f (ifc c1 then (ifc c2 then w else x) else (ifc c2 then y else z))
  ≡ (ifc c1 then (ifc c2 then f w else f x) else (ifc c2 then f y else f z))
propFnDistributeIfc2 false false f = refl
propFnDistributeIfc2 false true f = refl
propFnDistributeIfc2 true false f = refl
propFnDistributeIfc2 true true f = refl

propIfcBranchesSame : {t : Set} -> {c : Bool} (v : t)
  -> (ifc c then v else v) ≡ v
propIfcBranchesSame {c = false} v = refl
propIfcBranchesSame {c = true} v = refl

propIfBranchesSame : {t : Set} -> {c : Bool} (v : t)
  -> (if c then v else v) ≡ v
propIfBranchesSame {c = false} v = refl
propIfBranchesSame {c = true} v = refl

ifToIfc : {t : Set} {c : Bool} {a b : t} -> (if c then a else b) ≡ (ifc c then a else b)
ifToIfc {c = false} = refl
ifToIfc {c = true} = refl

ifTrueMap : {t : Set} -> {c : Bool} {a a2 b : t} -> (IsTrue c -> a ≡ a2) -> (if c then a else b) ≡ (if c then a2 else b)
ifTrueMap {c = false} aa2 = refl
ifTrueMap {c = true} {a} {a2} aa2 =
  begin
    a
  =⟨ aa2 IsTrue.itsTrue ⟩
    a2
  end

ifcTrueMap : {t : Set} -> {c : Bool} {a a2 b : t} -> (IsTrue c -> a ≡ a2) -> (ifc c then a else b) ≡ (ifc c then a2 else b)
ifcTrueMap {c = false} aa2 = refl
ifcTrueMap {c = true} {a} {a2} aa2 =
  begin
    a
  =⟨ aa2 IsTrue.itsTrue ⟩
    a2
  end

ifTrueNested : {t : Set} -> {c1 c2 : Bool} {a b c : t} -> (c1 ≡ c2) -> (if c1 then (if c2 then a else b) else c) ≡ (if c1 then a else c)
ifTrueNested {t} {false} {false} {a} {b} {c} c1eqc2 = refl
ifTrueNested {t} {true} {true} {a} {b} {c} c1eqc2 = refl

ifFalseNested : {t : Set} -> {c1 c2 : Bool} {a b c : t} -> (c1 ≡ c2) -> (if c1 then a else (if c2 then b else c)) ≡ (if c1 then a else c)
ifFalseNested {t} {false} {false} {a} {b} {c} c1eqc2 = refl
ifFalseNested {t} {true} {true} {a} {b} {c} c1eqc2 = refl

---- Useful functions

div : Nat -> (divisor : Nat) -> {≢0 : False (divisor ≟ 0)} -> Nat
div a b {p} = _/_ a b {p}
-- Does not need compile, since it is already defined in haskell

mod : Nat -> (divisor : Nat) -> {≢0 : False (divisor ≟ 0)} -> Nat
mod a b {p} = _%_ a b {p}
-- Does not need compile, since it is already defined in haskell

addLte : (a b c : Nat) -> IsTrue (c == a + b) -> IsTrue (a <= c)
addLte Z Z Z abc = IsTrue.itsTrue
addLte Z (S b) (S c) abc = IsTrue.itsTrue
addLte (S a) Z (S c) abc = addLte a Z c abc
addLte (S a) (S b) (S c) abc = addLte a (S b) c abc

0+n : (n : Nat) -> IsTrue (n == 0 + n)
0+n Z = IsTrue.itsTrue
0+n (S n) = 0+n n

addSuc : (a b c : Nat) -> IsTrue (c == a + S b) -> IsTrue (c == S a + b)
addSuc Z Z (S c) abc = abc
addSuc Z (S b) (S c) abc = abc
addSuc (S a) Z (S c) abc = addSuc a Z c abc
addSuc (S a) (S b) (S c) abc = addSuc a (S b) c abc

--  m = k + j  ==>  mod-helper k m n j = (n + k) mod (1 + m).
modHelperLt : (k m n j : Nat)
  -> IsTrue (m == k + j)
  -> IsTrue (mod-helper k m n j <= m)
modHelperLt k m  Z    j     i1 = addLte k j m i1
modHelperLt k m (S n)  Z    i1 = modHelperLt 0 m n m (0+n m)
modHelperLt k m (S n) (S j) i1 = modHelperLt (S k) m n j (addSuc k j m i1)

lteToLt : (a b : Nat) -> (a <= b) ≡ (a < S b)
lteToLt Z Z = refl
lteToLt Z (S b) = refl
lteToLt (S a) Z = refl
lteToLt (S a) (S b) = lteToLt a b

modLt : (a b : Nat) {≢0 : False (b ≟ 0)} -> IsTrue ((mod a b {≢0}) < b)
modLt a b@(S bs) =
  let
    pgoal : IsTrue (mod a b <= bs)
    pgoal = modHelperLt 0 bs a bs (0+n bs)
  in useEq (lteToLt (mod a b) bs) pgoal

pow : Nat -> Nat -> Nat
pow b Z = 1
pow b (S e) = b * pow b e
{-# COMPILE AGDA2HS pow #-}

mul_not_zero : {a b : Nat} -> IsFalse (a == 0) -> IsFalse (b == 0) -> IsFalse (a * b == 0)
mul_not_zero {S a} {S b} az bz = IsFalse.itsFalse

pow_not_zero : (n : Nat) -> IsFalse (pow 2 n == 0)
pow_not_zero Z = IsFalse.itsFalse
pow_not_zero (S sn) = mul_not_zero {2} {pow 2 sn} IsFalse.itsFalse (pow_not_zero sn)

false_convert : (n : Nat) -> IsFalse (n == 0) -> False (n ≟ 0)
false_convert (S n) if = tt

pow_not_zero_cv : (n : Nat) -> False (pow 2 n ≟ 0)
pow_not_zero_cv n = false_convert (pow 2 n) $ pow_not_zero n

zeroLteAny : (a : Nat) -> IsTrue (0 <= a)
zeroLteAny Z = IsTrue.itsTrue
zeroLteAny (S a) = IsTrue.itsTrue

lteSum : (a b s : Nat) -> (a <= b) ≡ (s + a <= s + b)
lteSum a b Z = refl
lteSum a b (S s) = lteSum a b s

lteSumOne : (a b s : Nat) -> IsTrue (a <= b) -> IsTrue (a <= s + b)
lteSumOne a b Z ab = ab
lteSumOne Z b (S n) ab = IsTrue.itsTrue
lteSumOne (S Z) Z (S Z) ab = IsTrue.itsTrue
lteSumOne (S (S n)) Z (S Z) ab = ab
lteSumOne (S n₁) (S n) (S Z) ab = lteSumOne n₁ n 1 ab
lteSumOne (S n₁) b (S (S n)) ab = lteSumOne n₁ (n + b) 1 (lteSumOne (S n₁) b (S n) ab)

anyGteZero : (a : Nat) -> IsTrue (a >= 0)
anyGteZero Z = IsTrue.itsTrue
anyGteZero (S a) = IsTrue.itsTrue

{-# TERMINATING #-}
log2up : Nat -> Nat
-- UNSAFE: This terminates since x/2 always decreases if x > 1
log2up 0 = 0
log2up 1 = 0
log2up (S (S x)) = S (log2up (div (S (S (S x))) 2))
{-# COMPILE AGDA2HS log2up #-}

divHelperReduce : (x a b c : Nat) -> div-helper (S x) a b c ≡ S (div-helper x a b c)
divHelperReduce x a Z c = refl
divHelperReduce x a (S b) Z =
  begin
    div-helper (S (S x)) a b a
  =⟨ divHelperReduce (S x) a b a ⟩
    S (div-helper (S x) a b a)
  end
divHelperReduce x a (S b) (S c) = divHelperReduce x a b c

div2Reduce : (x : Nat) -> div (2 + x) 2 ≡ S (div x 2)
div2Reduce Z = refl
div2Reduce x@(S sx) =
  begin
    div (2 + x) 2
  =⟨⟩
    div-helper 1 1 sx 0
  =⟨ divHelperReduce 0 1 sx 0 ⟩
    S (div-helper 0 1 sx 0)
  =⟨⟩
    S (div x 2)
  end

isTrueEquiv : {b : Bool} -> IsTrue b -> true ≡ b
isTrueEquiv {true} t = refl

plusGteOne : (a b : Nat) -> IsTrue (a >= 1) -> IsTrue (a + b >= 1)
plusGteOne (S a) b p = anyGteZero (a + b)

multGteOne : (a b : Nat) -> IsTrue (a >= 1) -> IsTrue (b >= 1) -> IsTrue (a * b >= 1)
multGteOne (S a) (S b) pa pb = plusGteOne (S b) (a * (S b)) pb

powGteOne : (n : Nat) -> IsTrue (pow 2 n >= 1)
powGteOne Z = IsTrue.itsTrue
powGteOne (S n) = multGteOne 2 (pow 2 n) IsTrue.itsTrue (powGteOne n)

add-assoc : (a b c : Nat) → (a + b) + c ≡ a + (b + c)
add-assoc Z b c = refl
add-assoc (S a) b c = cong S (add-assoc a b c)

add-n-zero : (n : Nat) → n + Z ≡ n
add-n-zero Z = refl
add-n-zero (S n) = cong S (add-n-zero n)

add-n-suc : (m n : Nat) → m + (S n) ≡ S (m + n)
add-n-suc Z n = refl
add-n-suc (S m) n = cong S (add-n-suc m n)

add-comm : (m n : Nat) → m + n ≡ n + m
add-comm m Z = add-n-zero m
add-comm m (S n) =
  begin
    m + (S n)
  =⟨ add-n-suc m n ⟩
    S (m + n)
  =⟨ cong S (add-comm m n) ⟩
    (S n) + m
  end

mul-n-zero : (a : Nat) -> a * Z ≡ Z
mul-n-zero Z = refl
mul-n-zero (S a) = mul-n-zero a

mul-n-suc : (a b : Nat) -> a * (S b) ≡ a + a * b
mul-n-suc Z b = refl
mul-n-suc (S a) b =
  begin
    (S a) * (S b)
  =⟨⟩
    (S b) + a * (S b)
  =⟨ cong (λ q -> (S b) + q) (mul-n-suc a b) ⟩
    S (b + (a + a * b))
  =⟨ cong S (sym $ add-assoc b a (a * b)) ⟩
    S ((b + a) + a * b)
  =⟨ cong (λ q -> S (q + a * b)) (add-comm b a) ⟩
    S ((a + b) + a * b)
  =⟨ cong S (add-assoc a b (a * b)) ⟩
    S (a + (b + a * b) )
  =⟨⟩
    (S a) + (S a) * b
  end

mul-comm : (a b : Nat) -> a * b ≡ b * a
mul-comm a Z = mul-n-zero a
mul-comm a (S b) =
  begin
    a * (S b)
  =⟨ mul-n-suc a b ⟩
    a + a * b
  =⟨ cong (λ q -> a + q) (mul-comm a b) ⟩
    (S b) * a
  end

gteDouble : (a b : Nat) -> (a >= b) ≡ (a + a >= b + b)
gteDouble Z Z = refl
gteDouble Z (S b) = refl
gteDouble (S a) Z = refl
gteDouble (S a) (S b) =
  begin
    a >= b
  =⟨ gteDouble a b ⟩
    (S a) + a >= (S b) + b
  =⟨ cong (λ q -> q >= (S b) + b) (add-comm (S a) a) ⟩
    a + S a >= S b + b
  =⟨ cong (λ q -> a + S a >= q) (add-comm (S b) b) ⟩
    a + S a >= b + S b
  end

gteMultBoth : (a b : Nat) -> (a >= b) ≡ (2 * a >= 2 * b)
gteMultBoth a b =
  begin
    a >= b
  =⟨ gteDouble a b ⟩
    a + a >= b + b
  =⟨ cong (λ q -> a + q >= b + b) (sym $ add-comm a 0) ⟩
    a + (a + 0) >= b + b
  =⟨ cong (λ q -> a + (a + 0) >= b + q) (sym $ add-comm b 0) ⟩
    a + (a + 0) >= b + (b + 0)
  end

gteTransitive : (a b c : Nat) -> IsTrue (a >= b) -> IsTrue (b >= c) -> IsTrue (a >= c)
gteTransitive Z Z Z ab bc = IsTrue.itsTrue
gteTransitive (S a) Z Z ab bc = IsTrue.itsTrue
gteTransitive (S a) (S b) Z ab bc = IsTrue.itsTrue
gteTransitive (S a) (S b) (S c) ab bc = gteTransitive a b c ab bc

mul-div : (x : Nat) -> IsTrue (2 * (div (1 + x) 2) >= x)
mul-div Z = IsTrue.itsTrue
mul-div (S Z) = IsTrue.itsTrue
mul-div (S (S x)) =
  let
    p1 : IsTrue (2 + 2 * (div (1 + x) 2) >= 2 + x)
    p1 = mul-div x

    p2 : IsTrue (S (div (1 + x) 2) * 2 >= 2 + x)
    p2 = useEq (cong (λ q -> 2 + q >= 2 + x) (mul-comm 2 (div (1 + x) 2))) p1

    p3 : IsTrue (2 * S (div (1 + x) 2) >= 2 + x)
    p3 = useEq (cong (λ q -> q >= 2 + x) (mul-comm (S (div (1 + x) 2)) 2)) p2

    goal : IsTrue (2 * (div (3 + x) 2) >= 2 + x)
    goal = useEq (cong (λ q -> 2 * q >= 2 + x) (sym $ div2Reduce (1 + x))) p3
  in goal

log2upPow : (a b : Nat) -> .(IsTrue (a >= log2up b)) -> IsTrue (pow 2 a >= b)
log2upPow Z Z p = IsTrue.itsTrue
log2upPow Z (S Z) p = IsTrue.itsTrue
log2upPow (S a) Z p = anyGteZero (pow 2 (S a))
log2upPow (S a) (S Z) p = useEq
  (begin
    (S a) >= 0
  =⟨ isTrueEquiv $ anyGteZero (S a) ⟩
    true
  =⟨ isTrueEquiv $ powGteOne (S a) ⟩
    pow 2 (S a) >= 1
  end) p
log2upPow (S a) (S (S b)) p =
  let
    p1 : IsTrue (  pow 2 a >= div (3 + b) 2  )
    p1 = log2upPow a (div (3 + b) 2) p

    p2 : IsTrue (  pow 2 (S a) >= 2 * (div (3 + b) 2)  )
    p2 = useEq (gteMultBoth (pow 2 a) (div (3 + b) 2)) p1
  in gteTransitive (pow 2 (S a)) (2 * (div (3 + b) 2)) (2 + b) p2 ((mul-div (2 + b)))

eqToGte : (a b : Nat) -> IsTrue (a == b) -> IsTrue (a >= b)
eqToGte Z b ab = ab
eqToGte (S a) (S b) ab = eqToGte a b ab

gteInvert : (a b : Nat) -> IsTrue (a >= b) -> IsTrue (b <= a)
gteInvert Z Z ab = IsTrue.itsTrue
gteInvert (S a) Z ab = IsTrue.itsTrue
gteInvert (S a) (S b) ab = gteInvert a b ab

ltLteTransitive : (a b c : Nat) -> IsTrue (a < b) -> IsTrue (b <= c) -> IsTrue (a < c)
ltLteTransitive Z (S b) (S c) ab bc = IsTrue.itsTrue
ltLteTransitive (S a) (S b) (S c) ab bc = ltLteTransitive a b c ab bc

lteTransitive : (a b c : Nat) -> IsTrue (a <= b) -> IsTrue (b <= c) -> IsTrue (a <= c)
lteTransitive Z Z c ab bc = bc
lteTransitive Z (S b) (S c) ab bc = IsTrue.itsTrue
lteTransitive (S a) (S b) (S c) ab bc = lteTransitive a b c ab bc

incrLte : (a b : Nat) -> IsTrue (a <= b) -> IsTrue (a <= S b)
incrLte Z Z altb = IsTrue.itsTrue
incrLte Z (S b) altb = IsTrue.itsTrue
incrLte (S a) (S b) altb = incrLte a b altb

natPlusMinNat : (x : Nat) -> {{p : IsFalse (x < 1)}} -> x ≡ (S (x - 1))
natPlusMinNat (S x) = refl

transformLteRight : {a b c : Nat} -> b ≡ c -> IsTrue (a <= b) -> IsTrue (a <= c)
transformLteRight {a} {b} {.b} refl ab = ab

lteSelf : (v : Nat) -> IsTrue (v <= v)
lteSelf Z = IsTrue.itsTrue
lteSelf (S v) = lteSelf v

falseToNotTrue : {b : Bool} -> IsFalse (b) -> IsTrue (not b)
falseToNotTrue {false} if = IsTrue.itsTrue

notFalseToTrue : {b : Bool} -> IsFalse (not b) -> IsTrue b
notFalseToTrue {true} if = IsTrue.itsTrue

trueToNotFalse : {b : Bool} -> IsTrue (b) -> IsFalse (not b)
trueToNotFalse {true} if = IsFalse.itsFalse

notTrueToFalse : {b : Bool} -> IsTrue (not b) -> IsFalse (b)
notTrueToFalse {false} if = IsFalse.itsFalse

-- Law of reflexivity for equality
postulate
  eqReflexivity : {t : Set} {{eqT : Eq t}} (v : t) -> IsTrue (v == v)
  eqToEquiv : {t : Set} {{eqT : Eq t}} (a b : t) -> IsTrue (a == b) -> a ≡ b

botToAny : {t : Set} -> ⊥ -> t
botToAny ()

max4 : (a b c d : Nat) -> Nat
max4 a b c d = max (max a b) (max c d)
{-# COMPILE AGDA2HS max4 #-}

sub : (a b : Nat) -> {{ .( IsTrue (b <= a) ) }} -> Nat
sub a Z {{ab}} = a
sub (S a) (S b) {{ab}} = sub a b
{-# COMPILE AGDA2HS sub #-}

diff : (a b : Nat) -> Nat
diff a Z = a
diff Z b = b
diff (S a) (S b) = diff a b
{-# COMPILE AGDA2HS diff #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module Languages.ILL.Intermediate where

open import Utils.HaskellTypes
open import Utils.HaskellFunctions
open import Languages.ILL.TypeSyntax

{-# IMPORT Languages.ILL.Intermediate #-}

data IPattern : Set where
  PTriv : IPattern
  PVar : String → IPattern
  PTensor : IPattern → IPattern → IPattern
{-# COMPILED_DATA IPattern Languages.ILL.Intermediate.IPattern
                           Languages.ILL.Intermediate.PTriv
                           Languages.ILL.Intermediate.PVar
                           Languages.ILL.Intermediate.PTensor #-}

data ITerm : Set where
  Var : String → ITerm
  Triv : ITerm
  TTensor : ITerm → ITerm → ITerm
  Lam : String → Type → ITerm → ITerm
  Let : ITerm → Type → IPattern → ITerm → ITerm
  App : ITerm → ITerm → ITerm
  Promote : List (Triple ITerm String Type) → ITerm → ITerm
  Discard : ITerm → ITerm → ITerm
  Copy : ITerm → String → String → ITerm → ITerm
  Derelict : ITerm → ITerm
{-# COMPILED_DATA ITerm Languages.ILL.Intermediate.ITerm
                        Languages.ILL.Intermediate.Var
                        Languages.ILL.Intermediate.Triv
                        Languages.ILL.Intermediate.TTensor
                        Languages.ILL.Intermediate.Lam
                        Languages.ILL.Intermediate.Let
                        Languages.ILL.Intermediate.App
                        Languages.ILL.Intermediate.Promote
                        Languages.ILL.Intermediate.Discard
                        Languages.ILL.Intermediate.Copy
                        Languages.ILL.Intermediate.Derelict #-}

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
open import Level using (0ℓ)
open import Function using (_$_; _∘_)

open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (False; True)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary
  using (Reflexive; Transitive; Trans; Antisymmetric; Asymmetric; Irreflexive; Decidable; Total; IsPreorder; IsPartialOrder; IsTotalOrder; TotalOrder; _Preserves₂_⟶_⟶_; Trichotomous; Tri; Irrelevant; Connex)
open Tri
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; trans; cong; resp₂; module ≡-Reasoning)
  renaming (isEquivalence to ≡-isEquivalence)
open import Relation.Binary.PropositionalEquality.WithK using (≡-erase)

open import Data.Bool using (T)
open import Data.Bool.Properties using (T?)
open import Data.Unit using (tt)

open import Data.List using (List)
open List
open import Data.Sum using (_⊎_)
open _⊎_

module AKS.Nat.Properties where

open import Data.Nat.Properties using (+-assoc; +-suc; +-comm; *-identityʳ; +-identityʳ; m+n≡0⇒m≡0; +-cancelʳ-≡; +-cancelˡ-≡; 1+n≢0; suc-injective) public
open import Data.Nat.Properties using (n∸n≡0; ∸-+-assoc) public
open import Data.Nat.Properties using (*-comm; *-1-commutativeMonoid) public

open import Polynomial.Simple.AlmostCommutativeRing using (AlmostCommutativeRing)
open import Polynomial.Simple.AlmostCommutativeRing.Instances using (module Nat)
open import Polynomial.Simple.Reflection using (solveOver)
open Nat.Reflection using (∀⟨_⟩)

open import AKS.Nat.Base using (ℕ; _+_; _*_; _∸_; lte; _≤_; _≥_; _≰_; _≱_; _<_; _≮_; _>_; _≯_; _<ᵇ_; _≟_; ℕ⁺; ℕ+; ⟅_⇓⟆; ⟅_⇑⟆; pred)
open ℕ
open import Algebra.Definitions {A = ℕ} _≡_ using (_DistributesOverˡ_)

≢⇒¬≟ : ∀ {n m} → n ≢ m → False (n ≟ m)
≢⇒¬≟ {n} {m} n≢m with n ≟ m
... | yes n≡m = contradiction n≡m n≢m
... | no _ = tt

¬≟⇒≢ : ∀ {n m} → False (n ≟ m) → n ≢ m
¬≟⇒≢ {n} {m} ¬n≟m n≡m with n ≟ m
... | no n≢m = contradiction n≡m n≢m

ℕ→ℕ⁺→ℕ : ∀ n {n≢0} → ⟅ ⟅ n ⇑⟆ {n≢0} ⇓⟆ ≡ n
ℕ→ℕ⁺→ℕ (suc n) {n≢0} = refl

⟅⇓⟆-injective : ∀ {n m} → pred ⟅ n ⇓⟆ ≡ pred ⟅ m ⇓⟆ → n ≡ m
⟅⇓⟆-injective {ℕ+ n} {ℕ+ m} refl = refl

n≢0∧m≢0⇒n*m≢0 : ∀ {n m} → n ≢ 0 → m ≢ 0 → n * m ≢ 0
n≢0∧m≢0⇒n*m≢0 {zero} {m} n≢0 m≢0 = contradiction refl n≢0
n≢0∧m≢0⇒n*m≢0 {suc n} {zero} n≢0 m≢0 = contradiction refl m≢0
n≢0∧m≢0⇒n*m≢0 {suc n} {suc m} n≢0 m≢0 ()

suc-injective-≡ : ∀ {n m} → suc n ≡ suc m → n ≡ m
suc-injective-≡ refl = refl

------------ _≤_ --------------

0≤n : ∀ {n} → 0 ≤ n
0≤n {n} = lte n refl

≤-refl : Reflexive _≤_
≤-refl {x} = lte 0 (≡-erase ∀⟨ x ∷ [] ⟩)

≤-reflexive : ∀ {n m} → n ≡ m → n ≤ m
≤-reflexive refl = ≤-refl

≤-trans : Transitive _≤_
≤-trans {x} (lte k₁ refl) (lte k₂ refl) = lte (k₁ + k₂) (≡-erase ∀⟨ x ∷ k₁ ∷ k₂ ∷ [] ⟩)

n+m≡n⇒m≡0 : ∀ {n m} → n + m ≡ n → m ≡ 0
n+m≡n⇒m≡0 {n} {m} n+m≡n = m≡0
  where
  open ≡-Reasoning
  m≡0 : m ≡ 0
  m≡0 = +-cancelˡ-≡ n $ begin
    n + m ≡⟨ n+m≡n ⟩
    n ≡⟨ sym (+-identityʳ n) ⟩
    n + 0 ∎

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym {x} {y} (lte k₁ x+k₁≡y) (lte k₂ y+k₂≡x) = ≡-erase (+-cancelʳ-≡ x y x+k₁≡y+k₁)
  where
  open ≡-Reasoning

  k₁+k₂≡0 : k₁ + k₂ ≡ 0
  k₁+k₂≡0 = n+m≡n⇒m≡0 $ begin
    x + (k₁ + k₂) ≡⟨ sym (+-assoc x k₁ k₂) ⟩
    (x + k₁) + k₂ ≡⟨ cong (λ t → t + k₂) x+k₁≡y ⟩
    y + k₂ ≡⟨ y+k₂≡x ⟩
    x ∎

  x+k₁≡y+k₁ : x + k₁ ≡ y + k₁
  x+k₁≡y+k₁ = begin
    x + k₁ ≡⟨ x+k₁≡y ⟩
    y      ≡⟨ sym (+-identityʳ y) ⟩
    y + 0  ≡⟨ cong (λ t → y + t) (sym (m+n≡0⇒m≡0 k₁ k₁+k₂≡0)) ⟩
    y + k₁ ∎

suc-mono-≤ : ∀ {n m} → n ≤ m → suc n ≤ suc m
suc-mono-≤ (lte k₁ refl) = lte k₁ refl

suc-injective-≤ : ∀ {n m} → suc n ≤ suc m → n ≤ m
suc-injective-≤ (lte k refl) = lte k refl

m≤m+n : ∀ {m n} → m ≤ m + n
m≤m+n {m} {n} = lte n refl

m≤n+m : ∀ {m n} → m ≤ n + m
m≤n+m {m} {n} = lte n (+-comm m n)

≤-erase : ∀ {n m} → n ≤ m → n ≤ m
≤-erase (lte k ≤-proof) = lte k (≡-erase ≤-proof)

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

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

------------ _<_ --------------

<-trans : Transitive _<_
<-trans {x} (lte k₁ refl) (lte k₂ refl) = lte (suc (k₁ + k₂)) (≡-erase ∀⟨ x ∷ k₁ ∷ k₂ ∷ [] ⟩)

<-≤-trans : Trans _<_ _≤_ _<_
<-≤-trans x<y y≤z = ≤-trans x<y y≤z

≤-<-trans : Trans _≤_ _<_ _<_
≤-<-trans {x} (lte k₁ refl) (lte k₂ refl) = lte (k₁ + k₂) (≡-erase ∀⟨ x ∷ k₁ ∷ k₂ ∷ [] ⟩)

n≮n : ∀ {n} → n ≮ n
n≮n {n} (lte k n+1+k≡n) rewrite sym (+-suc n k) = 1+n≢0 (n+m≡n⇒m≡0 n+1+k≡n)

<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl x<x = n≮n x<x

<-asym : Asymmetric _<_
<-asym x<y y<x = n≮n (<-trans x<y y<x)

<⇒≯ : ∀ {n m} → n < m → n ≯ m
<⇒≯ n<m n>m = <-asym n<m n>m

n<1+n : ∀ {n} → n < 1 + n
n<1+n = ≤-refl

0<1+n : ∀ {n} → 0 < 1 + n
0<1+n {n} = lte n refl

n≮0 : ∀ {n} → n ≮ 0
n≮0 ()

suc-mono-< : ∀ {n m} → n < m → suc n < suc m
suc-mono-< (lte k₁ refl) = lte k₁ refl

+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+-mono-≤ {x} {_} {u} (lte k refl) (lte m refl) = lte (k + m) (≡-erase (solveOver (x ∷ u ∷ k ∷ m ∷ []) Nat.ring))

+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+-mono-< {x} {_} {u} (lte k refl) (lte m refl) = lte (suc (k + m)) (≡-erase (solveOver (x ∷ u ∷ k ∷ m ∷ []) Nat.ring))

private
  a+b∸a≡b+[a∸a] : ∀ a b → a + b ∸ a ≡ b + (a ∸ a)
  a+b∸a≡b+[a∸a] zero b = sym (+-identityʳ b)
  a+b∸a≡b+[a∸a] (suc a) b = a+b∸a≡b+[a∸a] a b

m+[n∸m]≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
m+[n∸m]≡n {m} {n} (lte k refl) = begin
  m + (m + k ∸ m)   ≡⟨ cong (λ x → m + x) (a+b∸a≡b+[a∸a] m k) ⟩
  m + (k + (m ∸ m)) ≡⟨ cong (λ x → m + (k + x)) (n∸n≡0 m) ⟩
  m + (k + 0)       ≡⟨ cong (λ x → m + x) (+-identityʳ k) ⟩
  m + k ∎
  where
  open ≡-Reasoning

[n∸m]+m≡n : ∀ {m n} → m ≤ n → (n ∸ m) + m ≡ n
[n∸m]+m≡n {m} {n} rewrite +-comm (n ∸ m) m = m+[n∸m]≡n

m<n⇒n∸m≢0 : ∀ {m n} → m < n → n ∸ m ≢ 0
m<n⇒n∸m≢0 {zero} {n} m<n n∸m≡0 = <-irrefl (sym n∸m≡0) m<n
m<n⇒n∸m≢0 {suc m} {suc n} m<n n∸m≡0 = m<n⇒n∸m≢0 (suc-injective-≤ m<n) n∸m≡0

∸-mono-<ˡ : ∀ {x b t} → x ≤ b → b < t → b ∸ x < t ∸ x
∸-mono-<ˡ {x} (lte k₁ refl) (lte k₂ refl) = lte k₂ (≡-erase ≤-proof)
  where
  open ≡-Reasoning
  lemma₁ : ∀ a → 1 + (k₁ + a) + k₂ ≡ 1 + k₁ + k₂ + a
  lemma₁ a = ∀⟨ a ∷ k₁ ∷ k₂ ∷ [] ⟩
  lemma₂ : x + (1 + k₁ + k₂) ≡ 1 + (x + k₁ + k₂)
  lemma₂ = ∀⟨ x ∷ k₁ ∷ k₂ ∷ [] ⟩
  ≤-proof : suc (x + k₁ ∸ x) + k₂ ≡ suc (x + k₁) + k₂ ∸ x
  ≤-proof = begin
    suc (x + k₁ ∸ x) + k₂ ≡⟨ cong (λ t → suc t + k₂) (a+b∸a≡b+[a∸a] x k₁) ⟩
    suc (k₁ + (x ∸ x)) + k₂ ≡⟨ lemma₁ (x ∸ x) ⟩
    suc k₁ + k₂ + (x ∸ x) ≡⟨ sym (a+b∸a≡b+[a∸a] x (suc k₁ + k₂)) ⟩
    x + (suc k₁ + k₂) ∸ x ≡⟨ cong (λ t → t ∸ x) lemma₂ ⟩
    suc (x + k₁) + k₂ ∸ x ∎

∸-mono-<ʳ : ∀ {x b t} → t ≤ x → b < t → x ∸ t < x ∸ b
∸-mono-<ʳ {b = b} (lte k₁ refl) (lte k₂ refl) = lte k₂ (≡-erase ≤-proof)
  where
  open ≡-Reasoning
  LHS : suc (suc b + k₂ + k₁ ∸ (suc b + k₂) + k₂) ≡ suc (k₂ + k₁)
  LHS = cong suc $ begin
    suc b + k₂ + k₁ ∸ (suc b + k₂) + k₂ ≡⟨ cong (λ t → t + k₂) (sym (∸-+-assoc (b + k₂ + k₁) b k₂)) ⟩
    suc b + k₂ + k₁ ∸ suc b ∸ k₂ + k₂ ≡⟨ cong (λ t → t ∸ suc b ∸ k₂ + k₂) (+-assoc (suc b) k₂ k₁) ⟩
    suc b + (k₂ + k₁) ∸ suc b ∸ k₂ + k₂ ≡⟨ cong (λ t →  t ∸ k₂ + k₂) (a+b∸a≡b+[a∸a] (suc b) (k₂ + k₁)) ⟩
    k₂ + k₁ + (suc b ∸ suc b) ∸ k₂ + k₂ ≡⟨ cong (λ t → k₂ + k₁ + t ∸ k₂ + k₂) (n∸n≡0 (suc b)) ⟩
    k₂ + k₁ + 0 ∸ k₂ + k₂ ≡⟨  cong (λ t → t ∸ k₂ + k₂) (+-identityʳ (k₂ + k₁)) ⟩
    k₂ + k₁ ∸ k₂ + k₂ ≡⟨ cong (λ t → t + k₂) (a+b∸a≡b+[a∸a] k₂ k₁) ⟩
    k₁ + (k₂ ∸ k₂) + k₂ ≡⟨ cong (λ t → k₁ + t + k₂) (n∸n≡0 k₂) ⟩
    k₁ + 0 + k₂ ≡⟨ cong (λ t → t + k₂) (+-identityʳ k₁) ⟩
    k₁ + k₂ ≡⟨ +-comm k₁ k₂ ⟩
    k₂ + k₁ ∎
  lemma₁ : 1 + (b + k₂ + k₁) ≡ b + (1 + (k₂ + k₁))
  lemma₁ = ∀⟨ b ∷ k₂ ∷ k₁ ∷ [] ⟩
  RHS : suc (b + k₂ + k₁) ∸ b ≡ suc (k₂ + k₁)
  RHS = begin
    suc (b + k₂ + k₁) ∸ b ≡⟨ cong (λ t → t ∸ b) lemma₁ ⟩
    b + suc (k₂ + k₁) ∸ b ≡⟨ a+b∸a≡b+[a∸a] b (suc (k₂ + k₁)) ⟩
    suc (k₂ + k₁) + (b ∸ b) ≡⟨ cong (λ t → suc (k₂ + k₁) + t) (n∸n≡0 b) ⟩
    suc (k₂ + k₁) + 0 ≡⟨ +-identityʳ (suc (k₂ + k₁)) ⟩
    suc (k₂ + k₁) ∎
  ≤-proof : suc (suc b + k₂ + k₁ ∸ (suc b + k₂) + k₂) ≡ suc (b + k₂ + k₁) ∸ b
  ≤-proof = trans LHS (sym RHS)

∸-mono-≤ˡ : ∀ {x b t} → x ≤ b → b ≤ t → b ∸ x ≤ t ∸ x
∸-mono-≤ˡ {x} {b} {t} (lte k₁ refl) (lte k₂ refl) = lte k₂ ≤-proof
  where
  open ≡-Reasoning
  lemma₁ : ∀ a → k₁ + a + k₂ ≡ k₁ + k₂ + a
  lemma₁ a = ∀⟨ a ∷ k₁ ∷ k₂ ∷ [] ⟩
  ≤-proof : x + k₁ ∸ x + k₂ ≡ x + k₁ + k₂ ∸ x
  ≤-proof = begin
    x + k₁ ∸ x + k₂   ≡⟨ cong (λ t → t + k₂) (a+b∸a≡b+[a∸a] x k₁) ⟩
    k₁ + (x ∸ x) + k₂ ≡⟨ lemma₁ (x ∸ x) ⟩
    k₁ + k₂ + (x ∸ x) ≡⟨ sym (a+b∸a≡b+[a∸a] x (k₁ + k₂)) ⟩
    x + (k₁ + k₂) ∸ x ≡⟨ cong (λ t → t ∸ x) (sym (+-assoc x k₁ k₂)) ⟩
    x + k₁ + k₂ ∸ x   ∎

*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
*-mono-< {x} {_} {u} (lte k refl) (lte m refl) =
  lte (k * m + k * u + k + m * x + m + u + x) (≡-erase ∀⟨ x ∷ u ∷ k ∷ m ∷ [] ⟩)

*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
*-mono-≤ {x} {_} {u} (lte k refl) (lte m refl) = lte (k * m + k * u + m * x) (≡-erase ∀⟨ x ∷ u ∷ k ∷ m ∷ [] ⟩)

+-lower-≤ : ∀ x {n m} → n + x ≤ m → n ≤ m
+-lower-≤ x {n} {m} (lte q refl) = lte (x + q) (sym (+-assoc n x q))

<⇒≤ : ∀ {n m} → n < m → n ≤ m
<⇒≤ {n} (lte k refl) = lte (suc k) (≡-erase (+-suc n k))

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

n≤m⇒n<m⊎n≡m : ∀ {n m} → n ≤ m → n < m ⊎ n ≡ m
n≤m⇒n<m⊎n≡m {n} (lte zero ≤-proof) rewrite ≡-erase (+-identityʳ n) = inj₂ ≤-proof
n≤m⇒n<m⊎n≡m {n} (lte (suc k) ≤-proof) rewrite ≡-erase (+-suc n k) = inj₁ (lte k ≤-proof)

≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤∧≢⇒< m≤n m≢n with n≤m⇒n<m⊎n≡m m≤n
... | inj₁ m<n = m<n
... | inj₂ m≡n = contradiction m≡n m≢n

≮⇒≥ : ∀ {m n} → m ≮ n → m ≥ n
≮⇒≥ {_} {zero} m≮n = 0≤n
≮⇒≥ {zero} {suc n} m≮n = contradiction 0<1+n m≮n
≮⇒≥ {suc m} {suc n} m≮n = suc-mono-≤ (≮⇒≥ (m≮n ∘ suc-mono-<))

<⇒≱ : ∀ {m n} → m < n → m ≱ n
<⇒≱ {m} {n} m<n m≥n with n≤m⇒n<m⊎n≡m m≥n
... | inj₁ m>n = <-asym m<n m>n
... | inj₂ m≡n = <-irrefl (sym m≡n) m<n

<ᵇ⇒< : ∀ m n → T (m <ᵇ n) → m < n
<ᵇ⇒< zero    (suc n) m<n = 0<1+n
<ᵇ⇒< (suc m) (suc n) m<n = suc-mono-< (<ᵇ⇒< m n m<n)

<⇒<ᵇ : ∀ m n → m < n → T (m <ᵇ n)
<⇒<ᵇ zero (suc n) m<n = tt
<⇒<ᵇ (suc m) (suc n) m<n = <⇒<ᵇ m n (suc-injective-≤ m<n)

0≢⇒0< : ∀ {n} → 0 ≢ n → 0 < n
0≢⇒0< {zero} 0≢n = contradiction refl 0≢n
0≢⇒0< {suc n} 0≢n = 0<1+n

-- TODO change to does/proof
<-cmp : Trichotomous _≡_ _<_
<-cmp m n with m ≟ n | T? (m <ᵇ n)
... | yes m≡n | _       = tri≈ (<-irrefl m≡n) m≡n (<-irrefl (sym m≡n))
... | no  m≢n | yes m<n = tri< (<ᵇ⇒< m n m<n) m≢n (<⇒≯ (<ᵇ⇒< m n m<n))
... | no  m≢n | no  m≮n = tri> (m≮n ∘ <⇒<ᵇ m n) m≢n (≤∧≢⇒< (≮⇒≥ (m≮n ∘ <⇒<ᵇ m n)) (m≢n ∘ sym))

_<?_ : Decidable _<_
a <? b with <-cmp a b
... | tri< a<b _ _ = yes a<b
... | tri≈ _ refl _ = no λ a<b → n≮n a<b
... | tri> _ _ a>b = no λ a<b → <-asym a>b a<b

<-≤-connex : Connex _<_ _≤_
<-≤-connex m n with <-cmp m n
... | tri< n<m _ _  = inj₁ n<m
... | tri≈ _ refl _ = inj₂ ≤-refl
... | tri> _ _ n>m  = inj₂ (<⇒≤ n>m)

<-irrelevant : Irrelevant _<_
<-irrelevant {x} (lte k₁ 1+x+k₁≡y) (lte k₂ 1+x+k₂≡y) with +-cancelˡ-≡ (1 + x) (trans 1+x+k₁≡y (sym 1+x+k₂≡y))
<-irrelevant {x} (lte k₁ refl) (lte .k₁ refl) | refl = refl

≤-total : Total _≤_
≤-total n m with <-cmp n m
... | tri< n<m _ _  = inj₁ (<⇒≤ n<m)
... | tri≈ _ refl _ = inj₁ ≤-refl
... | tri> _ _ n>m  = inj₂ (<⇒≤ n>m)

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

≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record { isTotalOrder = ≤-isTotalOrder }

open import Algebra.Construct.NaturalChoice.Max ≤-totalOrder public

+-distribˡ-⊔ : _+_ DistributesOverˡ _⊔_
+-distribˡ-⊔ x y z with ≤-total z y
+-distribˡ-⊔ x y z | inj₁ z≤y with ≤-total (x + z) (x + y)
+-distribˡ-⊔ x y z | inj₁ z≤y | inj₁ x+z≤x+y = refl
+-distribˡ-⊔ x y z | inj₁ z≤y | inj₂ x+y≤x+z = ≤-antisym x+y≤x+z (+-mono-≤ ≤-refl z≤y)
+-distribˡ-⊔ x y z | inj₂ y≤z with ≤-total (x + z) (x + y)
+-distribˡ-⊔ x y z | inj₂ y≤z | inj₁ x+z≤x+y = ≤-antisym x+z≤x+y (+-mono-≤ ≤-refl y≤z)
+-distribˡ-⊔ x y z | inj₂ y≤z | inj₂ x+y≤x+z = refl

⊔-least-≤ : ∀ n m o → n ≤ o → m ≤ o → n ⊔ m ≤ o
⊔-least-≤ n m o n≤o m≤o with ≤-total m n
... | inj₁ _ = n≤o
... | inj₂ _ = m≤o

⊔-least-< : ∀ n m o → n < o → m < o → n ⊔ m < o
⊔-least-< n m o n<o m<o with ≤-total m n
... | inj₁ _ = n<o
... | inj₂ _ = m<o

m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n
m≤n⇒m⊔n≡n {m} {n} m≤n with ≤-total n m
... | inj₁ n≤m = ≤-antisym m≤n n≤m
... | inj₂ _   = refl

auto-≤ : ∀ {n m} {{ pf : True (n + (m ∸ n) ≟ m) }} → n ≤ m
auto-≤ {n} {m} with n + (m ∸ n) ≟ m
... | yes pf = lte (m ∸ n) pf

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
module localInstances where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Bool
open import Common.String
open import Common.List

record Eq (A : Set) : Set where
  field eq : A → A → Bool

strlen : String → ℕ
strlen s = length (stringToList s)

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y

open Eq {{...}}

instance
  eqℕ : Eq ℕ
  eqℕ = record { eq = λ x x' → x == x' }

eqString₁ : String → String → Bool
eqString₁ s₁ s₂ = strEq s₁ s₂

eqString₂ : String → String → Bool
eqString₂ s₁ s₂ = eq (strlen s₁) (strlen s₂)

testWhere : Bool → Bool
testWhere lengthEq = if eq "abcd" "dcba" then false else true
  where
    instance
      eqLocal : Eq String
      eqLocal = record { eq = if lengthEq then eqString₂ else eqString₁ }

testLet : Bool → Bool
testLet lengthEq =
  let instance
        eqLocal : Eq String
        eqLocal = record { eq = if lengthEq then eqString₂ else eqString₁ }
  in if eq "abcd" "dcba" then false else true

test1 : Bool
test1 = testWhere true

test2 : Bool
test2 = testLet true


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

open import lib.Base
open import lib.PathGroupoid

module lib.PathFunctor where

{- Nondependent stuff -}
module _ {i j} {A : Type i} {B : Type j} (f : A → B) where

  !-ap : {x y : A} (p : x == y)
    → ! (ap f p) == ap f (! p)
  !-ap idp = idp

  ap-! : {x y : A} (p : x == y)
    → ap f (! p) == ! (ap f p)
  ap-! idp = idp

  ∙-ap : {x y z : A} (p : x == y) (q : y == z)
    → ap f p ∙ ap f q == ap f (p ∙ q)
  ∙-ap idp q = idp

  ap-∙ : {x y z : A} (p : x == y) (q : y == z)
    → ap f (p ∙ q) == ap f p ∙ ap f q
  ap-∙ idp q = idp

  ∙∙-ap : {x y z w : A} (p : x == y) (q : y == z) (r : z == w)
    → ap f p ∙ ap f q ∙ ap f r == ap f (p ∙ q ∙ r)
  ∙∙-ap idp idp r = idp

  ap-∙∙ : {x y z w : A} (p : x == y) (q : y == z) (r : z == w)
    → ap f (p ∙ q ∙ r) == ap f p ∙ ap f q ∙ ap f r
  ap-∙∙ idp idp r = idp

  ap-∙∙∙ : {x y z w t : A} (p : x == y) (q : y == z) (r : z == w) (s : w == t)
    → ap f (p ∙ q ∙ r ∙ s) == ap f p ∙ ap f q ∙ ap f r ∙ ap f s
  ap-∙∙∙ idp idp idp s = idp

  ∙'-ap : {x y z : A} (p : x == y) (q : y == z)
    → ap f p ∙' ap f q == ap f (p ∙' q)
  ∙'-ap p idp = idp

  ap-∙' : {x y z : A} (p : x == y) (q : y == z)
    → ap f (p ∙' q) == ap f p ∙' ap f q
  ap-∙' p idp = idp

{- Dependent stuff -}
module _ {i j} {A : Type i} {B : A → Type j} (f : Π A B) where

  apd-∙ : {x y z : A} (p : x == y) (q : y == z)
    → apd f (p ∙ q) == apd f p ∙ᵈ apd f q
  apd-∙ idp idp = idp

  apd-∙' : {x y z : A} (p : x == y) (q : y == z)
    → apd f (p ∙' q) == apd f p ∙'ᵈ apd f q
  apd-∙' idp idp = idp

  apd-! : {x y : A} (p : x == y)
    → apd f (! p) == !ᵈ (apd f p)
  apd-! idp = idp

{- Over stuff -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (f : {a : A} → B a → C a) where

  ap↓-◃ : {x y z : A} {u : B x} {v : B y} {w : B z}
    {p : x == y} {p' : y == z} (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
    → ap↓ f (q ◃ r) == ap↓ f q ◃ ap↓ f r
  ap↓-◃ {p = idp} {p' = idp} idp idp = idp

  ap↓-▹! : {x y z : A} {u : B x} {v : B y} {w : B z}
    {p : x == y} {p' : z == y} (q : u == v [ B ↓ p ]) (r : w == v [ B ↓ p' ])
    → ap↓ f (q ▹! r) == ap↓ f q ▹! ap↓ f r
  ap↓-▹! {p = idp} {p' = idp} idp idp = idp

{- Fuse and unfuse -}
∘-ap : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  {x y : A} (p : x == y) → ap g (ap f p) == ap (g ∘ f) p
∘-ap f g idp = idp

ap-∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  {x y : A} (p : x == y) → ap (g ∘ f) p == ap g (ap f p)
ap-∘ f g idp = idp

ap-cst : ∀ {i j} {A : Type i} {B : Type j} (b : B) {x y : A} (p : x == y)
  → ap (cst b) p == idp
ap-cst b idp = idp

ap-idf : ∀ {i} {A : Type i} {u v : A} (p : u == v) → ap (idf A) p == p
ap-idf idp = idp

{- Functoriality of [coe] -}
coe-∙ : ∀ {i} {A B C : Type i} (p : A == B) (q : B == C) (a : A)
  → coe (p ∙ q) a == coe q (coe p a)
coe-∙ idp q a = idp

coe-! : ∀ {i} {A B : Type i} (p : A == B) (b : B) → coe (! p) b == coe! p b
coe-! idp b = idp

coe!-inv-r : ∀ {i} {A B : Type i} (p : A == B) (b : B)
  → coe p (coe! p b) == b
coe!-inv-r idp b = idp

coe!-inv-l : ∀ {i} {A B : Type i} (p : A == B) (a : A)
  → coe! p (coe p a) == a
coe!-inv-l idp a = idp

coe-inv-adj : ∀ {i} {A B : Type i} (p : A == B) (a : A) →
  ap (coe p) (coe!-inv-l p a) == coe!-inv-r p (coe p a)
coe-inv-adj idp a = idp

coe!-inv-adj : ∀ {i} {A B : Type i} (p : A == B) (b : B) →
  ap (coe! p) (coe!-inv-r p b) == coe!-inv-l p (coe! p b)
coe!-inv-adj idp b = idp

coe-ap-! : ∀ {i j} {A : Type i} (P : A → Type j) {a b : A} (p : a == b)
  (x : P b)
  → coe (ap P (! p)) x == coe! (ap P p) x
coe-ap-! P idp x = idp

{- Functoriality of transport -}
transp-∙ : ∀ {i j} {A : Type i} {B : A → Type j} {x y z : A}
  (p : x == y) (q : y == z) (b : B x)
  → transport B (p ∙ q) b == transport B q (transport B p b)
transp-∙ idp _ _ = idp

transp-∙' : ∀ {i j} {A : Type i} {B : A → Type j} {x y z : A}
  (p : x == y) (q : y == z) (b : B x)
  → transport B (p ∙' q) b == transport B q (transport B p b)
transp-∙' _ idp _ = idp

{- Naturality of homotopies -}

-- One should use [↓-='-out] and [apd] together, or even lib.cubical,
-- for homotopy naturality.

{- for functions with two arguments -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B → C) where

  ap2 : {x y : A} {w z : B}
    → (x == y) → (w == z) → f x w == f y z
  ap2 idp idp = idp

  ap2-out : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 p q == ap (λ u → f u w) p ∙ ap (λ v → f y v) q
  ap2-out idp idp = idp

  ap2-idp-l : {x : A} {w z : B} (q : w == z)
    → ap2 (idp {a = x}) q == ap (f x) q
  ap2-idp-l idp = idp

  ap2-idp-r : {x y : A} {w : B} (p : x == y)
    → ap2 p (idp {a = w}) == ap (λ z → f z w) p
  ap2-idp-r idp = idp

{- ap2 lemmas -}
module _ {i j} {A : Type i} {B : Type j} where

  ap2-fst : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 (curry fst) p q == p
  ap2-fst idp idp = idp

  ap2-snd : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 (curry snd) p q == q
  ap2-snd idp idp = idp

  ap-ap2 : ∀ {k l} {C : Type k} {D : Type l}
    (g : C → D) (f : A → B → C) {x y : A} {w z : B}
    (p : x == y) (q : w == z)
    → ap g (ap2 f p q) == ap2 (λ a b → g (f a b)) p q
  ap-ap2 g f idp idp = idp

  ap2-ap-l : ∀ {k l} {C : Type k} {D : Type l}
    (g : B → C → D) (f : A → B) {x y : A} {w z : C}
    (p : x == y) (q : w == z)
    → ap2 g (ap f p) q == ap2 (λ a c → g (f a) c) p q
  ap2-ap-l g f idp idp = idp

  ap2-ap-r : ∀ {k l} {C : Type k} {D : Type l}
    (g : A → C → D) (f : B → C) {x y : A} {w z : B}
    (p : x == y) (q : w == z)
    → ap2 g p (ap f q) == ap2 (λ a b → g a (f b)) p q
  ap2-ap-r g f idp idp = idp

  ap2-diag : (f : A → A → B)
    {x y : A} (p : x == y)
    → ap2 f p p == ap (λ x → f x x) p
  ap2-diag f idp = idp

-- unsure where this belongs
transp-cst=idf : ∀ {i} {A : Type i} {a x y : A} (p : x == y) (q : a == x)
  → transport (λ x → a == x) p q == q ∙ p
transp-cst=idf idp q = ! (∙-unit-r q)

{- for functions with more arguments -}
module _ {i₀ i₁ i₂ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂}
  {B : Type j} (f : A₀ → A₁ → A₂ → B) where

  ap3 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → f x₀ x₁ x₂ == f y₀ y₁ y₂
  ap3 idp idp idp = idp

module _ {i₀ i₁ i₂ i₃ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂} {A₃ : Type i₃}
  {B : Type j} (f : A₀ → A₁ → A₂ → A₃ → B) where

  ap4 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂} {x₃ y₃ : A₃}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → (x₃ == y₃) → f x₀ x₁ x₂ x₃ == f y₀ y₁ y₂ y₃
  ap4 idp idp idp idp = idp

module _ {i₀ i₁ i₂ i₃ i₄ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂} {A₃ : Type i₃}
  {A₄ : Type i₄} {B : Type j} (f : A₀ → A₁ → A₂ → A₃ → A₄ → B) where

  ap5 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂} {x₃ y₃ : A₃} {x₄ y₄ : A₄}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → (x₃ == y₃) → (x₄ == y₄)
    → f x₀ x₁ x₂ x₃ x₄ == f y₀ y₁ y₂ y₃ y₄
  ap5 idp idp idp idp idp = idp

module _ {i₀ i₁ i₂ i₃ i₄ i₅ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂} {A₃ : Type i₃}
  {A₄ : Type i₄} {A₅ : Type i₅} {B : Type j} (f : A₀ → A₁ → A₂ → A₃ → A₄ → A₅ → B) where

  ap6 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂} {x₃ y₃ : A₃} {x₄ y₄ : A₄} {x₅ y₅ : A₅}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → (x₃ == y₃) → (x₄ == y₄) → (x₅ == y₅)
    → f x₀ x₁ x₂ x₃ x₄ x₅ == f y₀ y₁ y₂ y₃ y₄ y₅
  ap6 idp idp idp idp idp idp = idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

record R : Set where
  constructor mkR
  field
    f : Nat

data Box : Set → Set₁ where
  box : (A : Set) → Box A

data D (A : Set) : Set₁ where
  c : Box A → R → D A

postulate
  r   : R
  dr  : ∀ {A} → D A
  rew : ∀ {A} {x} → c {A} (box A) (mkR x) ≡ dr
{-# REWRITE rew #-}

test : c {Bool} (box Bool) r ≡ dr
test = refl


text:
{-# OPTIONS -v tc.unquote:30 #-}
open import Common.Prelude
open import Common.Reflection
open import Agda.Builtin.Sigma

data Box : Bool → Set where
  box : (b : Bool) → Box b

works : (b : Bool) → Box b → Bool
works b (box .b) = unquote (give (var 0 []))

works₂ : (b : Bool) → Box b → Bool
unquoteDef works₂ = defineFun works₂ (clause
  ( ("b" , arg (argInfo visible relevant) unknown) ∷ [])
  ( arg (argInfo visible relevant) (var 0)
  ∷ arg (argInfo visible relevant) (con (quote box)
        (arg (argInfo visible relevant) (dot unknown) ∷ []))
  ∷ [])
  (var 0 []) ∷ [])

works₃ : (b : Bool) → Box b → (x y : Bool) → Bool
unquoteDef works₃ = defineFun works₃ (clause
  ( ("y" , arg (argInfo visible relevant) unknown)
  ∷ ("x" , arg (argInfo visible relevant) unknown)
  ∷ ("b" , arg (argInfo visible relevant) unknown)
  ∷ [])
  ( arg (argInfo visible relevant) (var 2)
  ∷ arg (argInfo visible relevant) (con (quote box)
        (arg (argInfo visible relevant) (dot unknown) ∷ []))
  ∷ arg (argInfo visible relevant) (var 1)
  ∷ arg (argInfo visible relevant) (var 0)
  ∷ [])
  (var 2 []) ∷ [])

max_forks_repo_name: shlevy/agda


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

open import zf
open import logic
open _∧_
open _∨_
open Bool

import OD
open import Relation.Nullary
open import Data.Empty
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
import BAlgbra
open BAlgbra O
open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom
import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

import ODC
open ODC O

open import filter

record Toplogy  ( L : HOD ) : Set (suc n) where
   field
       OS    : HOD
       OS⊆PL :  OS ⊆ Power L
       o∪ : { P : HOD }  →  P  ⊆ OS           → OS ∋ Union P
       o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q  → OS ∋ (p ∩ q)

open Toplogy

record _covers_ ( P q : HOD  ) : Set (suc n) where
   field
       cover   : {x : HOD} → q ∋ x → HOD
       P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
       isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x

-- Base
-- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that
-- W ⊆ U ∩ V and x ∈ W .

data genTop (P : HOD) : HOD → Set (suc n) where
   gi : {x : HOD} → P ∋ x → genTop P x
   g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
   g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)

-- Limit point

record LP ( L S x : HOD ) (top : Toplogy L) (S⊆PL :  S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
   field
      neip   : {y : HOD} → OS top ∋ y → y ∋ x → HOD
      isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x )

-- Finite Intersection Property

data Finite-∩ (S : HOD) : HOD → Set (suc n) where
   fin-∩e : {x : HOD} → S ∋ x → Finite-∩ S x
   fin-∩  : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)

record FIP  ( L P : HOD ) : Set (suc n) where
   field
       fipS⊆PL :  P ⊆ Power L
       fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ )

-- Compact

data Finite-∪ (S : HOD) : HOD → Set (suc n) where
   fin-∪e : {x : HOD} → S ∋ x → Finite-∪ S x
   fin-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)

record Compact  ( L P : HOD ) : Set (suc n) where
   field
       finCover        : {X y : HOD} → X covers P         → P ∋ y →  HOD
       isFinCover      : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y
       isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y )

-- FIP is Compact

FIP→Compact : {L P : HOD} → Tolopogy L → FIP L P → Compact L P
FIP→Compact = ?

Compact→FIP : {L P : HOD} → Tolopogy L → Compact L P → FIP L P
Compact→FIP = ?

-- Product Topology

_Top⊗_ : {P Q : HOD} → Topology P → Tolopogy Q → Topology ( P ⊗ Q )
_Top⊗_ = ?

-- existence of Ultra Filter

-- Ultra Filter has limit point

-- FIP is UFL

-- Product of UFL has limit point (Tychonoff)

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where all elements satisfy a given property
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.All where

open import Category.Applicative
open import Category.Monad
open import Data.Empty using (⊥)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product as Prod
  using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
open import Function
open import Level
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary hiding (_∈_)
open import Relation.Binary.PropositionalEquality as P

private
  variable
    a b p q r : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Definitions

-- Given a predicate P, then All P xs means that every element in xs
-- satisfies P. See `Relation.Unary` for an explanation of predicates.

infixr 5 _∷_

data All {A : Set a} (P : Pred A p) : Pred (List A) (a ⊔ p) where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

-- All P xs is a finite map from indices x ∈ xs to content P x.
-- Relation pxs [ i ]= px states that, in map pxs, key i : x ∈ xs points to value px.

infix 4 _[_]=_

data _[_]=_ {A : Set a} {P : Pred A p} :
            ∀ {x xs} → All P xs → x ∈ xs → P x → Set (a ⊔ p) where

  here  : ∀ {x xs} {px : P x} {pxs : All P xs} →
          px ∷ pxs [ here refl ]= px

  there : ∀ {x xs y} {px : P x} {pxs : All P xs} {py : P y} {i : x ∈ xs} →
          pxs [ i ]= px →
          py ∷ pxs [ there i ]= px

-- A list is empty if having an element is impossible.

Null : Pred (List A) _
Null = All (λ _ → ⊥)

------------------------------------------------------------------------
-- Operations on All

module _ {P : Pred A p} where

  uncons : ∀ {x xs} → All P (x ∷ xs) → P x × All P xs
  uncons (px ∷ pxs) = px , pxs

  head : ∀ {x xs} → All P (x ∷ xs) → P x
  head = proj₁ ∘ uncons

  tail : ∀ {x xs} → All P (x ∷ xs) → All P xs
  tail = proj₂ ∘ uncons

  tabulate : ∀ {xs} → (∀ {x} → x ∈ xs → P x) → All P xs
  tabulate {xs = []}     hyp = []
  tabulate {xs = x ∷ xs} hyp = hyp (here refl) ∷ tabulate (hyp ∘ there)

  reduce : (f : ∀ {x} → P x → B) → ∀ {xs} → All P xs → List B
  reduce f []         = []
  reduce f (px ∷ pxs) = f px ∷ reduce f pxs

  construct : (f : B → ∃ P) (xs : List B) → ∃ (All P)
  construct f []       = [] , []
  construct f (x ∷ xs) = Prod.zip _∷_ _∷_ (f x) (construct f xs)

  fromList : (xs : List (∃ P)) → All P (List.map proj₁ xs)
  fromList []              = []
  fromList ((x , p) ∷ xps) = p ∷ fromList xps

  toList : ∀ {xs} → All P xs → List (∃ P)
  toList pxs = reduce (λ {x} px → x , px) pxs

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

  map : P ⊆ Q → All P ⊆ All Q
  map g []         = []
  map g (px ∷ pxs) = g px ∷ map g pxs

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

  zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
  zipWith f ([] , [])             = []
  zipWith f (px ∷ pxs , qx ∷ qxs) = f (px , qx) ∷ zipWith f (pxs , qxs)

  unzipWith : R ⊆ P ∩ Q → All R ⊆ All P ∩ All Q
  unzipWith f []         = [] , []
  unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (f rx) (unzipWith f rxs)

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

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

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

self : ∀ {xs : List A} → All (const A) xs
self = tabulate (λ {x} _ → x)

------------------------------------------------------------------------
-- (weak) updateAt

module _ {P : Pred A p} where

  infixl 6 _[_]%=_ _[_]≔_

  updateAt : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
  updateAt () f []
  updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
  updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs

  _[_]%=_ : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
  pxs [ i ]%= f = updateAt i f pxs

  _[_]≔_ : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
  pxs [ i ]≔ px = pxs [ i ]%= const px

------------------------------------------------------------------------
-- Traversable-like functions

module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
         {F : Set (a ⊔ p) → Set (a ⊔ p)}
         (App : RawApplicative F)
         where

  open RawApplicative App

  sequenceA : All (F ∘′ P) ⊆ F ∘′ All P
  sequenceA []       = pure []
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs

  mapA : ∀ {Q : Pred A q} → (Q ⊆ F ∘′ P) → All Q ⊆ (F ∘′ All P)
  mapA f = sequenceA ∘′ map f

  forA : ∀ {Q : Pred A q} {xs} → All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
  forA qxs f = mapA f qxs

module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
         {M : Set (a ⊔ p) → Set (a ⊔ p)}
         (Mon : RawMonad M)
         where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : All (M ∘′ P) ⊆ M ∘′ All P
  sequenceM = sequenceA p App

  mapM : ∀ {Q : Pred A q} → (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
  mapM = mapA p App

  forM : ∀ {Q : Pred A q} {xs} → All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
  forM = forA p App

------------------------------------------------------------------------
-- Generalised lookup based on a proof of Any

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

  lookupAny : ∀ {xs} → All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i)
  lookupAny (px ∷ pxs) (here qx) = px , qx
  lookupAny (px ∷ pxs) (there i) = lookupAny pxs i

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

  lookupWith : ∀[ P ⇒ Q ⇒ R ] → ∀ {xs} → All P xs → (i : Any Q xs) →
               R (Any.lookup i)
  lookupWith f pxs i = Prod.uncurry f (lookupAny pxs i)

module _ {P : Pred A p} where

  lookup : ∀ {xs} → All P xs → (∀ {x} → x ∈ xs → P x)
  lookup pxs = lookupWith (λ { px refl → px }) pxs

------------------------------------------------------------------------
-- Properties of predicates preserved by All

module _ {P : Pred A p} where

  all : Decidable P → Decidable (All P)
  all p []       = yes []
  all p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all p xs)

  universal : Universal P → Universal (All P)
  universal u []       = []
  universal u (x ∷ xs) = u x ∷ universal u xs

  irrelevant : Irrelevant P → Irrelevant (All P)
  irrelevant irr []           []           = P.refl
  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
    P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)

  satisfiable : Satisfiable (All P)
  satisfiable = [] , []