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

open import LogicalFormulae
open import Semirings.Definition

module Semirings.Solver {a : _} {A : Set a} {Zero One : A} {_+_ : A → A → A} {_*_ : A → A → A} (S : Semiring Zero One _+_ _*_) (comm : (a b : A) → a * b ≡ b * a) where

open Semiring S

-- You can see how to use the solver in LectureNotes/NumbersAndSets/Lecture1.agda.

data Expr : Set a where
  const : A → Expr
  zero : Expr
  succ : Expr → Expr
  plus : Expr → Expr → Expr
  times : Expr → Expr → Expr

-- TODO: do this in distinct phases. (Work out what those phases are.)
-- Expose those phases to the user so that they can choose which tactics to use.
-- Phases:
--  * In any expression which is all sums, extract all consts out to the front
--  * In any expression which is all sums, extract all the succs to the front

eval : Expr → A
eval (const k) = k
eval zero = Zero
eval (succ e) = One + (eval e)
eval (plus x y) = (eval x) + (eval y)
eval (times x y) = (eval x) * (eval y)

simplePlus : Expr → Expr → Expr
simplePlus (const x) (const y) = plus (const x) (const y)
simplePlus (const x) zero = const x
simplePlus (const x) (succ b) = succ (plus (const x) b)
simplePlus (const x) (plus a b) = plus (const x) (plus a b)
simplePlus (const x) (times a b) = plus (const x) (times a b)
simplePlus zero b = b
simplePlus (succ a) (const x) = succ (plus (const x) a)
simplePlus (succ a) zero = succ a
simplePlus (succ a) (succ b) = succ (succ (plus a b))
simplePlus (succ a) (plus b c) = succ (plus a (plus b c))
simplePlus (succ a) (times b c) = succ (plus a (times b c))
simplePlus (plus a b) (const x) = plus (const x) (plus a b)
simplePlus (plus a b) zero = plus a b
simplePlus (plus a b) (succ c) = succ (plus a (plus b c))
simplePlus (plus a b) (plus c d) = plus a (plus b (plus c d))
simplePlus (plus a b) (times c d) = plus a (plus b (times c d))
simplePlus (times a b) (const x) = plus (const x) (times a b)
simplePlus (times a b) zero = times a b
simplePlus (times a b) (succ c) = succ (plus (times a b) c)
simplePlus (times a b) (plus c d) = plus (times a b) (plus c d)
simplePlus (times a b) (times c d) = plus (times a b) (times c d)

private
  lemma : (a b c : A) → a + (b + c) ≡ b + (a + c)
  lemma a b c rewrite commutative a (b + c) | equalityCommutative (+Associative b c a) = applyEquality (b +_) (commutative _ _)

simplePlusIsPlus : (a b : Expr) → eval (simplePlus a b) ≡ eval (plus a b)
simplePlusIsPlus (const x) (const x₁) = refl
simplePlusIsPlus (const x) zero rewrite Semiring.sumZeroRight S x = refl
simplePlusIsPlus (const x) (succ b) = lemma One x (eval b)
simplePlusIsPlus (const x) (plus b c) = refl
simplePlusIsPlus (const x) (times b c) = refl
simplePlusIsPlus zero b = equalityCommutative (sumZeroLeft (eval b))
simplePlusIsPlus (succ a) (const x) rewrite lemma One x (eval a) = commutative x _
simplePlusIsPlus (succ a) zero = equalityCommutative (sumZeroRight _)
simplePlusIsPlus (succ a) (succ b) rewrite lemma (One + eval a) One (eval b) = applyEquality (One +_) (+Associative One _ _)
simplePlusIsPlus (succ a) (plus b c) = +Associative _ _ _
simplePlusIsPlus (succ a) (times b c) = +Associative _ _ _
simplePlusIsPlus (plus a b) (const x) = commutative x _
simplePlusIsPlus (plus a b) zero = equalityCommutative (sumZeroRight _)
simplePlusIsPlus (plus a b) (succ c) rewrite lemma (eval a + eval b) One (eval c) = applyEquality (One +_) (+Associative _ _ _)
simplePlusIsPlus (plus a b) (plus c d) = +Associative (eval a) _ _
simplePlusIsPlus (plus a b) (times c d) = +Associative _ _ _
simplePlusIsPlus (times a b) (const x) = commutative x _
simplePlusIsPlus (times a b) zero = equalityCommutative (sumZeroRight _)
simplePlusIsPlus (times a b) (succ c) rewrite lemma One (eval a * eval b) (eval c) = refl
simplePlusIsPlus (times a b) (plus c d) = refl
simplePlusIsPlus (times a b) (times c d) = refl

simplify : Expr → Expr
simplify (const k) = const k
simplify zero = zero
simplify (succ e) = succ (simplify e)
simplify (plus (const k) (const x)) = simplePlus (const k) (const x)
simplify (plus (const k) zero) = simplify (const k)
simplify (plus (const k) (succ expr)) = succ (simplify (plus (const k) expr))
simplify (plus (const k) (plus x y)) = simplePlus (const k) (simplify (plus x y))
simplify (plus (const k) (times x y)) = simplePlus (const k) (simplify (times x y))
simplify (plus zero expr2) = simplify expr2
simplify (plus (succ expr1) expr2) = succ (simplify (plus expr1 expr2))
simplify (plus (plus expr1 expr3) zero) = simplify (plus expr1 expr3)
simplify (plus (plus expr1 expr3) (const k)) = simplePlus (const k) (simplify (plus expr1 expr3))
simplify (plus (plus expr1 expr3) (succ expr2)) = succ (simplePlus (simplify (plus expr1 expr3)) (simplify expr2))
simplify (plus (plus expr1 expr3) (plus expr2 expr4)) = simplePlus (simplify (plus expr1 expr3)) (simplify (plus expr2 expr4))
simplify (plus (plus expr1 expr3) (times expr2 expr4)) = simplePlus (simplify (plus expr1 expr3)) (simplify (times expr2 expr4))
simplify (plus (times expr1 expr3) (const k)) = simplePlus (const k) (simplify (times expr1 expr3))
simplify (plus (times expr1 expr3) zero) = times (simplify expr1) (simplify expr3)
simplify (plus (times expr1 expr3) (succ expr2)) = succ (simplePlus (simplify (times expr1 expr3)) (simplify expr2))
simplify (plus (times expr1 expr3) (plus expr2 expr4)) = simplePlus (simplify (times expr1 expr3)) (simplify (plus expr2 expr4))
simplify (plus (times expr1 expr3) (times expr2 expr4)) = simplePlus (simplify (times expr1 expr3)) (simplify (times expr2 expr4))
simplify (times (const k) (const x)) = times (const k) (const x)
simplify (times (const k) zero) = zero
simplify (times (const k) (succ zero)) = const k
simplify (times (const k) (succ (const y))) = simplePlus (const k) (times (const k) (const y))
simplify (times (const k) (succ (plus a b))) = simplePlus (const k) (simplify (times (const k) (plus a b)))
simplify (times (const k) (succ (times a b))) = simplePlus (const k) (simplify (times (const k) (times a b)))
simplify (times (const k) (succ (succ x))) = simplePlus (const k) (simplify (times (const k) (succ x)))
simplify (times (const k) (plus expr2 expr3)) = simplePlus (simplify (times (const k) (expr2))) (simplify (times (const k) expr3))
simplify (times (const k) (times expr2 expr3)) = times (const k) (simplify (times expr2 expr3))
simplify (times zero expr2) = zero
simplify (times (succ zero) expr2) = simplify expr2
simplify (times (succ (succ expr1)) expr2) = simplePlus (simplify expr2) (simplify (times (succ expr1) expr2))
simplify (times (succ (plus expr1 expr3)) (const k)) = times (const k) (simplify (succ (plus expr1 expr3)))
simplify (times (succ (plus expr1 expr3)) zero) = zero
simplify (times (succ (plus expr1 expr3)) (succ expr2)) = succ (simplePlus (simplify (times expr1 expr2)) (simplePlus (simplify (times expr3 expr2)) (simplePlus expr2 (simplify (plus expr1 expr3)))))
simplify (times (succ (plus expr1 expr3)) (plus expr2 expr4)) = times (simplify (succ (plus expr1 expr3))) (simplify (plus expr2 expr4))
simplify (times (succ (plus expr1 expr3)) (times expr2 expr4)) = times (simplify (succ (plus expr1 expr3))) (simplify (times expr2 expr4))
simplify (times (succ (const k)) (const x)) = simplePlus (const x) (times (const k) (const x))
simplify (times (succ (const k)) zero) = zero
simplify (times (succ (const k)) (succ (const x))) = succ (simplePlus (const k) (simplePlus (const x) (simplify (times (const k) (const x)))))
simplify (times (succ (const k)) (succ zero)) = succ (const k)
simplify (times (succ (const k)) (succ (succ expr2))) = succ (simplePlus (const k) (simplePlus (simplify (succ expr2)) (simplify (times (const k) (succ (expr2))))))
simplify (times (succ (const k)) (succ (plus expr2 expr3))) = succ (simplePlus (const k) (simplePlus (simplify (plus expr2 expr3)) (simplify (times (const k) (plus expr2 expr3)))))
simplify (times (succ (const k)) (succ (times expr2 expr3))) = succ (simplePlus (const k) (simplePlus (simplify (times expr2 expr3)) (simplify (times (const k) (times expr2 expr3)))))
simplify (times (succ (const k)) (plus expr2 expr3)) = simplePlus (simplify (plus expr2 expr3)) (simplify (times (const k) (plus expr2 expr3)))
simplify (times (succ (const k)) (times expr2 expr3)) = simplePlus (simplify (times expr2 expr3)) (simplify (times (const k) (times expr2 expr3)))
simplify (times (succ (times expr1 expr3)) (const x)) = times (const x) (simplify (succ (times expr1 expr3)))
simplify (times (succ (times expr1 expr3)) zero) = zero
simplify (times (succ (times expr1 expr3)) (succ expr2)) = succ (simplePlus (simplify expr2) (plus (simplify (times expr1 expr3)) (simplify (times (times expr1 expr3) expr2))))
simplify (times (succ (times expr1 expr3)) (plus expr2 expr4)) = simplePlus (simplify (plus expr2 expr4)) (simplify (times (times expr1 expr3) (plus expr2 expr4)))
simplify (times (succ (times expr1 expr3)) (times expr2 expr4)) = simplePlus (simplify (times expr2 expr4)) (simplify (times (times expr1 expr3) (times expr2 expr4)))
simplify (times (plus expr1 expr3) zero) = zero
simplify (times (plus expr1 expr3) (succ expr2)) = simplePlus (simplify (plus expr1 expr3)) (simplify (times (plus expr1 expr3) expr2))
simplify (times (plus expr1 expr3) (const x)) = times (const x) (simplify (plus expr1 expr3))
simplify (times (plus expr1 expr3) (plus expr2 expr4)) = simplePlus (simplify (times expr1 expr2)) (simplePlus (simplify (times expr3 expr2)) (simplePlus (simplify (times expr1 expr4)) (simplify (times expr3 expr4))))
simplify (times (plus expr1 expr3) (times expr2 expr4)) = simplePlus (simplify (times expr1 (times expr2 expr4))) (simplify (times expr3 (times expr2 expr4)))
simplify (times (times expr1 expr3) zero) = zero
simplify (times (times expr1 expr3) (succ expr2)) = simplePlus (simplify (times expr1 expr3)) (simplify (times (times expr1 expr3) expr2))
simplify (times (times expr1 expr3) (plus expr2 expr4)) = simplePlus (simplify (times (times expr1 expr3) expr2)) (simplify (times (times expr1 expr3) expr4))
simplify (times (times expr1 expr3) (times expr2 expr4)) = times (simplify expr1) (simplify (times expr3 (times expr2 expr4)))
simplify (times (times expr1 expr3) (const x)) = times (simplify (times expr1 expr3)) (const x)

equalPlus : {a b c d : A} → (a ≡ c) → (b ≡ d) → (a + b) ≡ (c + d)
equalPlus refl refl = refl

equalTimes : {a b c d : A} → (a ≡ c) → (b ≡ d) → (a * b) ≡ (c * d)
equalTimes refl refl = refl

otherDist : {a b c : A} → (a * b) + (c * b) ≡ (a + c) * b
otherDist = transitivity (equalPlus (comm _ _) (comm _ _)) (transitivity (equalityCommutative (+DistributesOver* _ _ _)) (comm _ _))

simplifyPreserves : (a : Expr) → eval (simplify a) ≡ eval a
simplifyPreserves (const x) = refl
simplifyPreserves zero = refl
simplifyPreserves (succ a) = applyEquality (One +_) (simplifyPreserves a)
simplifyPreserves (plus (const x) (const y)) = refl
simplifyPreserves (plus (const x) zero) = equalityCommutative (sumZeroRight x)
simplifyPreserves (plus (const x) (succ b)) = transitivity (transitivity (applyEquality (One +_) (transitivity (simplifyPreserves (plus (const x) b)) (commutative x (eval b)))) (+Associative One (eval b) x)) (commutative (One + eval b) x)
simplifyPreserves (plus (const x) (plus b c)) = transitivity (simplePlusIsPlus (const x) (simplify (plus b c))) (applyEquality (x +_) (simplifyPreserves (plus b c)))
simplifyPreserves (plus (const x) (times b c)) = transitivity (simplePlusIsPlus (const x) (simplify (times b c))) (applyEquality (x +_) (simplifyPreserves (times b c)))
simplifyPreserves (plus zero a) = transitivity (simplifyPreserves a) (equalityCommutative (sumZeroLeft (eval a)))
simplifyPreserves (plus (succ a) b) = transitivity (applyEquality (One +_) (simplifyPreserves (plus a b))) (+Associative One (eval a) (eval b))
simplifyPreserves (plus (plus a b) (const x)) = transitivity (simplePlusIsPlus (const x) (simplify (plus a b))) (transitivity (commutative x (eval (simplify (plus a b)))) (applyEquality (_+ x) (simplifyPreserves (plus a b))))
simplifyPreserves (plus (plus a b) zero) = transitivity (simplifyPreserves (plus a b)) (equalityCommutative (sumZeroRight _))
simplifyPreserves (plus (plus a b) (succ c)) = transitivity (applyEquality (One +_) (simplePlusIsPlus (simplify (plus a b)) (simplify c))) (transitivity (+Associative One _ _) (transitivity (applyEquality (_+ eval (simplify c)) (commutative One _)) (transitivity (equalityCommutative (+Associative _ _ _)) (transitivity (applyEquality (_+ (One + eval (simplify c))) (simplifyPreserves (plus a b))) (applyEquality (λ i → (eval a + eval b) + (One + i)) (simplifyPreserves c))))))
simplifyPreserves (plus (plus a b) (plus c d)) = transitivity (simplePlusIsPlus (simplify (plus a b)) (simplify (plus c d))) (transitivity (applyEquality (_+ eval (simplify (plus c d))) (simplifyPreserves (plus a b))) (applyEquality ((eval a + eval b) +_) (simplifyPreserves (plus c d))))
simplifyPreserves (plus (plus a b) (times c d)) = transitivity (simplePlusIsPlus (simplify (plus a b)) (simplify (times c d))) (transitivity (applyEquality (_+ eval (simplify (times c d))) (simplifyPreserves (plus a b))) (applyEquality ((eval a + eval b) +_) (simplifyPreserves (times c d))))
simplifyPreserves (plus (times a b) (const x)) = transitivity (simplePlusIsPlus (const x) (simplify (times a b))) (transitivity (commutative x _) (applyEquality (_+ x) (simplifyPreserves (times a b))))
simplifyPreserves (plus (times a b) zero) = transitivity (transitivity (applyEquality (_* eval (simplify b)) (simplifyPreserves a)) (applyEquality ((eval a) *_) (simplifyPreserves b))) (equalityCommutative (sumZeroRight _))
simplifyPreserves (plus (times a b) (succ c)) = transitivity (transitivity (applyEquality (One +_) (transitivity (simplePlusIsPlus (simplify (times a b)) (simplify c)) (transitivity (transitivity (applyEquality (eval (simplify (times a b)) +_) (simplifyPreserves c)) (applyEquality (_+ eval c) (simplifyPreserves (times a b)))) (commutative _ (eval c))))) (+Associative One (eval c) _)) (commutative _ (eval a * eval b))
simplifyPreserves (plus (times a b) (plus c d)) = transitivity (simplePlusIsPlus (simplify (times a b)) (simplify (plus c d))) (transitivity (applyEquality (_+ eval (simplify (plus c d))) (simplifyPreserves (times a b))) (applyEquality ((eval a * eval b) +_) (simplifyPreserves (plus c d))))
simplifyPreserves (plus (times a b) (times c d)) = transitivity (simplePlusIsPlus (simplify (times a b)) (simplify (times c d))) (transitivity (applyEquality (_+ eval (simplify (times c d))) (simplifyPreserves (times a b))) (applyEquality ((eval a * eval b) +_) (simplifyPreserves (times c d))))
simplifyPreserves (times (const x) (const y)) = refl
simplifyPreserves (times (const x) zero) = equalityCommutative (productZeroRight x)
simplifyPreserves (times (const x) (succ (const y))) = transitivity (applyEquality (_+ (x * y)) (equalityCommutative (productOneRight _))) (equalityCommutative (+DistributesOver* x One y))
simplifyPreserves (times (const x) (succ zero)) = equalityCommutative (transitivity (applyEquality (x *_) (sumZeroRight One)) (productOneRight x))
simplifyPreserves (times (const x) (succ (succ b))) = transitivity (simplePlusIsPlus (const x) (simplify (times (const x) (succ b)))) (transitivity (equalPlus (equalityCommutative (productOneRight _)) (simplifyPreserves (times (const x) (succ b)))) (equalityCommutative (+DistributesOver* x One _)))
simplifyPreserves (times (const x) (succ (plus b c))) = transitivity (simplePlusIsPlus (const x) (simplePlus (simplify (times (const x) b)) (simplify (times (const x) c)))) (transitivity (equalPlus (equalityCommutative (productOneRight _)) (transitivity (simplePlusIsPlus (simplify (times (const x) b)) (simplify (times (const x) c))) (transitivity (equalPlus (simplifyPreserves (times (const x) b)) (simplifyPreserves (times (const x) c))) (equalityCommutative (+DistributesOver* x (eval b) (eval c)))))) (equalityCommutative (+DistributesOver* x One _)))
simplifyPreserves (times (const x) (succ (times b c))) = transitivity (equalPlus (equalityCommutative (productOneRight x)) (applyEquality (x *_) (simplifyPreserves (times b c)))) (equalityCommutative (+DistributesOver* x One _))
simplifyPreserves (times (const x) (plus b c)) = transitivity (simplePlusIsPlus (simplify (times (const x) b)) (simplify (times (const x) c))) (transitivity (transitivity (applyEquality (eval (simplify (times (const x) b)) +_) (simplifyPreserves (times (const x) c))) (applyEquality (_+ (x * eval c)) (simplifyPreserves (times (const x) b)))) (equalityCommutative (+DistributesOver* x (eval b) (eval c))))
simplifyPreserves (times (const x) (times b c)) = applyEquality (x *_) (simplifyPreserves (times b c))
simplifyPreserves (times zero b) = equalityCommutative (productZeroLeft (eval b))
simplifyPreserves (times (succ (const x)) (const y)) = transitivity (transitivity (equalPlus (equalityCommutative (productOneRight y)) (comm x y)) (equalityCommutative (+DistributesOver* y One x))) (comm y _)
simplifyPreserves (times (succ (const x)) zero) = equalityCommutative (productZeroRight _)
simplifyPreserves (times (succ (const x)) (succ (const y))) = transitivity (transitivity (transitivity (+Associative One x _) (applyEquality ((One + x) +_) (transitivity (equalPlus (equalityCommutative (productOneRight y)) (comm x y)) (equalityCommutative (+DistributesOver* y One x))))) (equalPlus (equalityCommutative (productOneRight (One + x))) (comm _ _))) (equalityCommutative (+DistributesOver* _ _ _))
simplifyPreserves (times (succ (const x)) (succ zero)) = equalityCommutative (transitivity (applyEquality ((One + x) *_) (sumZeroRight One)) (productOneRight _))
simplifyPreserves (times (succ (const x)) (succ (succ b))) = transitivity (applyEquality (One +_) (simplePlusIsPlus (const x) (simplePlus (succ (simplify b)) (simplify (times (const x) (succ b)))))) (transitivity (applyEquality (λ i → One + (x + i)) (simplePlusIsPlus (succ (simplify b)) (simplify (times (const x) (succ b))))) (transitivity (applyEquality (λ i → One + (x + ((One + i) + eval (simplify (times (const x) (succ b)))))) (simplifyPreserves b)) (transitivity (applyEquality (λ i → One + (x + ((One + eval b) + i))) (simplifyPreserves (times (const x) (succ b)))) (transitivity (transitivity (+Associative One x _) (equalPlus (equalityCommutative (productOneRight _)) (transitivity (transitivity (transitivity (applyEquality ((One + eval b) +_) (+DistributesOver* x One (eval b))) (transitivity (transitivity (equalityCommutative (+Associative One (eval b) _)) (transitivity (applyEquality (One +_) (transitivity (+Associative (eval b) _ _) (transitivity (equalPlus (transitivity (commutative _ _) (equalPlus (productOneRight x) (equalityCommutative (productOneRight _)))) (comm x _)) (equalityCommutative (+Associative x _ _))))) (+Associative One x _))) (applyEquality ((One + x) +_) (equalityCommutative (+DistributesOver* (eval b) One x))))) (equalPlus (equalityCommutative (productOneRight _)) (comm (eval b) _))) (equalityCommutative (+DistributesOver* (One + x) One _))))) (equalityCommutative (+DistributesOver* (One + x) One _))))))
simplifyPreserves (times (succ (const x)) (succ (plus b c))) = transitivity (transitivity (transitivity (applyEquality (One +_) (simplePlusIsPlus (const x) (simplePlus (simplify (plus b c)) (simplePlus (simplify (times (const x) b)) (simplify (times (const x) c)))))) (transitivity (+Associative One x _) (applyEquality ((One + x) +_) (transitivity (simplePlusIsPlus (simplify (plus b c)) (simplePlus (simplify (times (const x) b)) (simplify (times (const x) c)))) (transitivity (equalPlus (simplifyPreserves (plus b c)) (simplePlusIsPlus (simplify (times (const x) b)) (simplify (times (const x) c)))) (transitivity (transitivity (transitivity (transitivity (equalityCommutative (+Associative _ _ _ )) (transitivity (applyEquality (eval b +_) (transitivity (applyEquality (eval c +_) (equalPlus (simplifyPreserves (times (const x) b)) (simplifyPreserves (times (const x) c)))) (transitivity (+Associative (eval c) _ _) (transitivity (applyEquality (_+ (x * eval c)) (commutative _ _)) (equalityCommutative (+Associative _ _ _)))))) (+Associative _ _ _))) (equalPlus (equalPlus (equalityCommutative (productOneRight (eval b))) (comm _ _)) (equalPlus (equalityCommutative (productOneRight (eval c))) (comm x _)))) (equalPlus (equalityCommutative (+DistributesOver* (eval b) One x)) (equalityCommutative (+DistributesOver* (eval c) One x)))) (equalPlus (comm _ _) (comm _ _)))))))) (equalPlus (equalityCommutative (productOneRight _)) (equalityCommutative (+DistributesOver* (One + x) _ _)))) (equalityCommutative (+DistributesOver* (One + x) _ _))
simplifyPreserves (times (succ (const x)) (succ (times b c))) = transitivity (transitivity (applyEquality (One +_) (simplePlusIsPlus (const x) (simplePlus (simplify (times b c)) (times (const x) (simplify (times b c)))))) (transitivity (+Associative One x _) (equalPlus (equalityCommutative (productOneRight _)) (transitivity (simplePlusIsPlus (simplify (times b c)) (times (const x) (simplify (times b c)))) (transitivity (transitivity (equalPlus (transitivity (simplifyPreserves (times b c)) (equalityCommutative (productOneRight _))) (transitivity (comm _ _) (applyEquality (_* x) (simplifyPreserves (times b c))))) (equalityCommutative (+DistributesOver* _ One x))) (comm _ _)))))) (equalityCommutative (+DistributesOver* _ _ _))
simplifyPreserves (times (succ (const x)) (plus b c)) = transitivity (simplePlusIsPlus (simplify (plus b c)) (simplePlus (simplify (times (const x) b)) (simplify (times (const x) c)))) (transitivity (transitivity (equalPlus (transitivity (simplifyPreserves (plus b c)) (equalityCommutative (productOneRight _))) (transitivity (simplePlusIsPlus (simplify (times (const x) b)) (simplify (times (const x) c))) (transitivity (transitivity (equalPlus (simplifyPreserves (times (const x) b)) (simplifyPreserves (times (const x) c))) (equalityCommutative (+DistributesOver* x _ _))) (comm x _)))) (equalityCommutative (+DistributesOver* _ One x))) (comm _ _))
simplifyPreserves (times (succ (const x)) (times b c)) = transitivity (simplePlusIsPlus (simplify (times b c)) (times (const x) (simplify (times b c)))) (transitivity (transitivity (equalPlus (transitivity (simplifyPreserves (times b c)) (equalityCommutative (productOneRight _))) (transitivity (comm x _) (applyEquality (_* x) (simplifyPreserves (times b c))))) (equalityCommutative (+DistributesOver* _ One x))) (comm _ _))
simplifyPreserves (times (succ zero) b) = transitivity (simplifyPreserves b) (transitivity (equalityCommutative (productOneLeft (eval b))) (applyEquality (_* eval b) (equalityCommutative (sumZeroRight One))))
simplifyPreserves (times (succ (succ a)) b) = transitivity (simplePlusIsPlus (simplify b) (simplify (times (succ a) b))) (transitivity (equalPlus (simplifyPreserves b) (simplifyPreserves (times (succ a) b))) (transitivity (transitivity (equalPlus (equalityCommutative (productOneRight _)) (comm _ _)) (equalityCommutative (+DistributesOver* (eval b) One _))) (comm (eval b) _)))
simplifyPreserves (times (succ (plus a b)) (const x)) = transitivity (comm x _) (applyEquality (λ i → (One + i) * x) (simplifyPreserves (plus a b)))
simplifyPreserves (times (succ (plus a b)) zero) = equalityCommutative (productZeroRight _)
simplifyPreserves (times (succ (plus a b)) (succ c)) = transitivity (transitivity (transitivity (applyEquality (One +_) (transitivity (simplePlusIsPlus (simplify (times a c)) (simplePlus (simplify (times b c)) (simplePlus c (simplify (plus a b))))) (transitivity (transitivity (equalPlus (simplifyPreserves (times a c)) (simplePlusIsPlus (simplify (times b c)) (simplePlus c (simplify (plus a b))))) (transitivity (+Associative _ _ _) (transitivity (transitivity (equalPlus (transitivity (equalPlus (comm _ _) (transitivity (simplifyPreserves (times b c)) (comm _ _))) (equalityCommutative (+DistributesOver* _ _ _))) (transitivity (simplePlusIsPlus c (simplify (plus a b))) (transitivity (commutative _ _) (equalPlus (simplifyPreserves (plus a b)) (equalityCommutative (productOneRight _)))))) (commutative _ _)) (equalityCommutative (+Associative _ _ _))))) (applyEquality ((eval a + eval b) +_) (equalityCommutative (+DistributesOver* _ One _)))))) (+Associative One _ _)) (equalPlus (equalityCommutative (productOneRight _)) (comm _ _))) (equalityCommutative (+DistributesOver* _ _ _))
simplifyPreserves (times (succ (plus a b)) (plus c d)) = equalTimes (applyEquality (One +_) (simplifyPreserves (plus a b))) (simplifyPreserves (plus c d))
simplifyPreserves (times (succ (plus a b)) (times c d)) = equalTimes (applyEquality (One +_) (simplifyPreserves (plus a b))) (simplifyPreserves (times c d))
simplifyPreserves (times (succ (times a b)) (const x)) = transitivity (comm x _) (applyEquality (λ i → (One + i) * x) (simplifyPreserves (times a b)))
simplifyPreserves (times (succ (times a b)) zero) = equalityCommutative (productZeroRight _)
simplifyPreserves (times (succ (times a b)) (succ c)) = transitivity (transitivity (transitivity (applyEquality (One +_) (transitivity (simplePlusIsPlus (simplify c) (plus (simplify (times a b)) (simplify (times (times a b) c)))) (transitivity (transitivity (transitivity (equalPlus (transitivity (simplifyPreserves c) (equalityCommutative (productOneRight _))) (transitivity (commutative _ _) (equalPlus (transitivity (simplifyPreserves (times (times a b) c)) (comm _ _)) (simplifyPreserves (times a b))))) (+Associative _ _ _)) (applyEquality (_+ (eval a * eval b)) (equalityCommutative (+DistributesOver* _ One _)))) (commutative _ _)))) (+Associative One _ _)) (equalPlus (equalityCommutative (productOneRight _)) (comm _ _))) (equalityCommutative (+DistributesOver* _ One _))
simplifyPreserves (times (succ (times a b)) (plus c d)) = transitivity (simplePlusIsPlus (simplify (plus c d)) (simplePlus (simplify (times (times a b) c)) (simplify (times (times a b) d)))) (transitivity (equalPlus (simplifyPreserves (plus c d)) (simplePlusIsPlus (simplify (times (times a b) c)) (simplify (times (times a b) d)))) (transitivity (transitivity (equalPlus (equalityCommutative (productOneRight _)) (transitivity (transitivity (equalPlus (simplifyPreserves (times (times a b) c)) (simplifyPreserves (times (times a b) d))) (equalityCommutative (+DistributesOver* _ _ _))) (comm _ _))) (equalityCommutative (+DistributesOver* _ One _))) (comm _ _)))
simplifyPreserves (times (succ (times a b)) (times c d)) = transitivity (simplePlusIsPlus (simplify (times c d)) (times (simplify a) (simplify (times b (times c d))))) (transitivity (equalPlus (simplifyPreserves (times c d)) (equalTimes (simplifyPreserves a) (simplifyPreserves (times b (times c d))))) (transitivity (transitivity (equalPlus (equalityCommutative (productOneRight _)) (transitivity (*Associative (eval a) _ _) (comm _ _))) (equalityCommutative (+DistributesOver* _ One _))) (comm _ _)))
simplifyPreserves (times (plus a b) (const x)) = transitivity (comm x _) (applyEquality (_* x) (simplifyPreserves (plus a b)))
simplifyPreserves (times (plus a b) zero) = equalityCommutative (productZeroRight _)
simplifyPreserves (times (plus a b) (succ c)) = transitivity (simplePlusIsPlus (simplify (plus a b)) (simplify (times (plus a b) c))) (transitivity (applyEquality ((eval (simplify (plus a b))) +_) (simplifyPreserves (times (plus a b) c))) (transitivity (applyEquality (_+ ((eval a + eval b) * eval c)) (simplifyPreserves (plus a b))) (transitivity (equalPlus (equalityCommutative (productOneRight _)) refl) (equalityCommutative (+DistributesOver* _ One (eval c))))))
simplifyPreserves (times (plus a b) (plus c d)) = transitivity (simplePlusIsPlus (simplify (times a c)) (simplePlus (simplify (times b c)) (simplePlus (simplify (times a d)) (simplify (times b d))))) (transitivity (transitivity (transitivity (transitivity (equalPlus (transitivity (simplifyPreserves (times a c)) (comm _ _)) (transitivity (simplePlusIsPlus (simplify (times b c)) (simplePlus (simplify (times a d)) (simplify (times b d)))) (equalPlus (transitivity (simplifyPreserves (times b c)) (comm _ _)) (transitivity (simplePlusIsPlus (simplify (times a d)) (simplify (times b d))) (equalPlus (transitivity (simplifyPreserves (times a d)) (comm _ _)) (transitivity (simplifyPreserves (times b d)) (comm _ _))))))) (+Associative _ _ _)) (equalPlus (equalityCommutative (+DistributesOver* (eval c) (eval a) _)) (equalityCommutative (+DistributesOver* (eval d) (eval a) _)))) (equalPlus (comm (eval c) _) (comm (eval d) _))) (equalityCommutative (+DistributesOver* _ (eval c) (eval d))))
simplifyPreserves (times (plus a b) (times c d)) = transitivity (simplePlusIsPlus (simplify (times a (times c d))) (simplify (times b (times c d)))) (transitivity (equalPlus (simplifyPreserves (times a (times c d))) (simplifyPreserves (times b (times c d)))) (transitivity (equalPlus (comm (eval a) _) (comm (eval b) _)) (transitivity (equalityCommutative (+DistributesOver* _ (eval a) (eval b))) (comm _ _))))
simplifyPreserves (times (times a b) (const x)) = applyEquality (_* x) (simplifyPreserves (times a b))
simplifyPreserves (times (times a b) zero) = equalityCommutative (productZeroRight _)
simplifyPreserves (times (times a b) (succ c)) = transitivity (simplePlusIsPlus (simplify (times a b)) (simplify (times (times a b) c))) (transitivity (equalPlus (simplifyPreserves (times a b)) (simplifyPreserves (times (times a b) c))) (transitivity (applyEquality (_+ ((eval a * eval b) * eval c)) (equalityCommutative (productOneRight _))) (equalityCommutative (+DistributesOver* _ One (eval c)))))
simplifyPreserves (times (times a b) (plus c d)) = transitivity (simplePlusIsPlus (simplify (times (times a b) c)) (simplify (times (times a b) d))) (transitivity (equalPlus (simplifyPreserves (times (times a b) c)) (simplifyPreserves (times (times a b) d))) (equalityCommutative (+DistributesOver* _ _ _)))
simplifyPreserves (times (times a b) (times c d)) = transitivity (equalTimes (simplifyPreserves a) (simplifyPreserves (times b (times c d)))) (*Associative (eval a) (eval b) _)

from_to_by_ : (x y : Expr) (pr : eval (simplify x) ≡ eval (simplify y)) → eval x ≡ eval y
from a to b by pr = transitivity (equalityCommutative (simplifyPreserves a)) (transitivity pr (simplifyPreserves b))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary.Indexed.Homogeneous

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

module Relation.Binary.Indexed.Homogeneous.Core where

open import Level using (Level; _⊔_)
open import Data.Product using (_×_)
open import Relation.Binary as B using (REL; Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.Indexed.Heterogeneous as I
open import Relation.Unary.Indexed using (IPred)

------------------------------------------------------------------------
-- Homegeneously indexed binary relations

-- Heterogeneous types

IREL : ∀ {i a b} {I : Set i} → (I → Set a) → (I → Set b) → (ℓ : Level) → Set _
IREL A B ℓ = ∀ {i} → REL (A i) (B i) ℓ

-- Homogeneous types

IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
IRel A = IREL A A

------------------------------------------------------------------------
-- Simple properties

module _ {i a} {I : Set i} (A : I → Set a) where

  syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_

  Implies : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ B.⇒ (_∼₂_ {i})

  Reflexive : ∀ {ℓ} → IRel A ℓ → Set _
  Reflexive _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})

  Symmetric : ∀ {ℓ} → IRel A ℓ → Set _
  Symmetric _∼_ = ∀ {i} → B.Symmetric (_∼_ {i})

  Transitive : ∀ {ℓ} → IRel A ℓ → Set _
  Transitive _∼_ = ∀ {i} → B.Transitive (_∼_ {i})

  Antisymmetric : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Antisymmetric _≈_ _∼_ = ∀ {i} → B.Antisymmetric _≈_ (_∼_ {i})

  Decidable : ∀ {ℓ} → IRel A ℓ → Set _
  Decidable _∼_ = ∀ {i} → B.Decidable (_∼_ {i})

  Respects : ∀ {ℓ₁ ℓ₂} → IPred A ℓ₁ → IRel A ℓ₂ → Set _
  Respects P _∼_ = ∀ {i} {x y : A i} → x ∼ y → P x → P y

  Respectsˡ : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Respectsˡ P _∼_  = ∀ {i} {x y z : A i} → x ∼ y → P x z → P y z

  Respectsʳ : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Respectsʳ P _∼_ = ∀ {i} {x y z : A i} → x ∼ y → P z x → P z y

  Respects₂ : ∀ {ℓ₁ ℓ₂} → IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Respects₂ P _∼_ = (Respectsʳ P _∼_) × (Respectsˡ P _∼_)

------------------------------------------------------------------------
-- Conversion between homogeneous and heterogeneously indexed relations

module _ {i a b} {I : Set i} {A : I → Set a} {B : I → Set b} where

  OverPath : ∀ {ℓ} → IREL A B ℓ → ∀ {i j} → i ≡ j → REL (A i) (B j) ℓ
  OverPath _∼_ refl = _∼_

  toHetIndexed : ∀ {ℓ} → IREL A B ℓ → I.IREL A B (i ⊔ ℓ)
  toHetIndexed _∼_ {i} {j} x y = (p : i ≡ j) → OverPath _∼_ p x y

  fromHetIndexed : ∀ {ℓ} → I.IREL A B ℓ → IREL A B ℓ
  fromHetIndexed _∼_ = _∼_

------------------------------------------------------------------------
-- Lifting to non-indexed binary relations

module _ {i a} {I : Set i} (A : I → Set a) where

  Lift : ∀ {ℓ} → IRel A ℓ → Rel (∀ i → A i) _
  Lift _∼_ x y = ∀ i → x i ∼ y i

ext: agda


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

open import Oscar.Class
open import Oscar.Class.Hmap
open import Oscar.Class.Leftunit
open import Oscar.Class.Reflexivity
open import Oscar.Class.Smap
open import Oscar.Class.Symmetry
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transitivity
open import Oscar.Class.Transleftidentity
open import Oscar.Data.Substitunction
open import Oscar.Data.Term
open import Oscar.Prelude

module Test.ProblemWithDerivation-4 where

postulate
  A : Set
  B : Set
  _~A~_ : A → A → Set
  _~B~_ : B → B → Set
  s1 : A → B
  f1 : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y

instance

  𝓢urjectivity1 : Smap.class _~A~_ _~B~_ s1 s1
  𝓢urjectivity1 .⋆ _ _ = f1

-- Oscar.Class.Hmap.Transleftidentity
instance

  -HmapFromTransleftidentitySymmetry : ∀
    {𝔵} {𝔛 : Ø 𝔵}
    {𝔞} {𝔄 : 𝔛 → Ø 𝔞}
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    (let _∼_ = Arrow 𝔄 𝔅)
    {ℓ̇} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ̇}
    {transitivity : Transitivity.type _∼_}
    {reflexivity : Reflexivity.type _∼_}
    {ℓ}
    ⦃ _ : Transleftidentity.class _∼_ _∼̇_ reflexivity transitivity ⦄
    ⦃ _ : ∀ {x y} → Symmetry.class (_∼̇_ {x} {y}) ⦄
    → ∀ {m n}
    → Hmap.class (λ (f : m ∼ n) (P : LeftExtensionṖroperty ℓ _∼_ _∼̇_ m) → π₀ (π₀ P) f)
                 (λ f P → π₀ (π₀ P) (transitivity f reflexivity))
  -HmapFromTransleftidentitySymmetry .⋆ _ (_ , P₁) = P₁ $ symmetry transleftidentity

test-before : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-before = smap

postulate
  XX : Set
  BB : XX → Set
  CC : XX → Set
  EQ : ∀ {x y} → Arrow BB BB x y → Arrow BB BB x y → Set

instance
  postulate
    -transleftidentity : Transleftidentity.class (Arrow BB BB) EQ magic magic
    -symmetry : ∀ {x y} → Symmetry.class (EQ {x} {y})

test-after : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-after = smap -- FIXME this was yellow when we used Symmetry instead of Sym. why?


text:
open import FRP.JS.Nat using ( ℕ ; suc ; _+_ ; _≟_ )
open import FRP.JS.RSet
open import FRP.JS.Time using ( Time ; epoch )
open import FRP.JS.Delay using ( _ms )
open import FRP.JS.Behaviour
open import FRP.JS.Event using ( ∅ )
open import FRP.JS.Bool using ( Bool ; not ; true )
open import FRP.JS.QUnit using ( TestSuite ; ok◇ ; test ; _,_ ; ε )

module FRP.JS.Test.Behaviour where

infixr 2 _≟*_

_≟*_ : ⟦ Beh ⟨ ℕ ⟩ ⇒ Beh ⟨ ℕ ⟩ ⇒ Beh ⟨ Bool ⟩ ⟧
_≟*_ = map2 _≟_

tests : TestSuite
tests =
  ( test "≟*"
    ( ok◇ "[ 1 ] ≟* [ 1 ]" ([ 1 ] ≟* [ 1 ])
    , ok◇ "[ 1 ] ≟* [ 0 ]" (not* ([ 1 ] ≟* [ 0 ]))
    , ok◇ "[ 0 ] ≟* [ 1 ]" (not* ([ 0 ] ≟* [ 1 ])) )
  , test "map"
    ( ok◇ "map suc [ 0 ] ≟* [ 1 ]" (map suc [ 0 ] ≟* [ 1 ])
    , ok◇ "map suc [ 1 ] ≟* [ 1 ]" (not* (map suc [ 1 ] ≟* [ 1 ])) )
  , test "join"
    ( ok◇ "join (map [ suc ] [ 0 ] ) ≟* [ 1 ]" (join (map (λ n → [ suc n ]) [ 0 ]) ≟* [ 1 ])
    , ok◇ "join (map [ suc ] [ 1 ]) ≟* [ 1 ]" (not* (join (map (λ n → [ suc n ]) [ 1 ]) ≟* [ 1 ])) )
  , test "hold"
    ( ok◇ "hold 1 ∅ ≟* [ 1 ]" (hold 1 ∅ ≟* [ 1 ])
    , ok◇ "hold 0 ∅ ≟* [ 1 ]" (not* (hold 0 ∅ ≟* [ 1 ])) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Andreas, 2016-07-17 issue 2101

-- It should be possible to place a single function with a where block
-- inside `abstract`.

-- This will work if type signatures inside a where-block
-- are considered private, since in private type signatures,
-- abstract definitions are transparent.
-- (Unlike in public type signatures.)

record Wrap (A : Set) : Set where
  field unwrap : A

postulate
  P : ∀{A : Set} → A → Set

module AbstractPrivate (A : Set) where
  abstract
    B : Set
    B = Wrap A

    postulate
      b : B

    private -- this makes abstract defs transparent in type signatures
      postulate
        test : P (Wrap.unwrap b) -- should succeed

abstract

  unnamedWhere : (A : Set) → Set
  unnamedWhere A = A
    where  -- the following definitions are private!
    B : Set
    B = Wrap A

    postulate
      b : B
      test : P (Wrap.unwrap b) -- should succeed

  namedWherePrivate : (A : Set) → Set
  namedWherePrivate A = A
    module MP where
    B : Set
    B = Wrap A

    private
      postulate
        b : B
        test : P (Wrap.unwrap b) -- should succeed

  namedWhere : (A : Set) → Set
  namedWhere A = A
    module M where  -- the definitions in this module are not private!
    B : Set
    B = Wrap A

    postulate
      b : B
      test : P (Wrap.unwrap b) -- should fail!

access = M.b  -- should be in scope

outside : ∀ {A} → M.B A → A
outside = Wrap.unwrap  -- should fail and does so

--

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Nat as ℕ using (ℕ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List
open import Data.List.Relation.Unary.All as List
open import Relation.Binary.PropositionalEquality

module simple-let-temp-output where

abstract
  e1 : let x = ⊤ in let y = ⊥ in x × y
  e1 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  e2 : let y = # 1 in y Fin.≥ # 2
  e2 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

e3 : ℕ
e3 = let y = 1 ℕ.+ 1 in y

lamLet : ℕ → ℕ
lamLet x = let y = x in y

abstract
  forallLet : ∀ (x : Fin 2) → let y = x in y ≡ # 1
  forallLet = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  letForall : let y = # 1 in ∀ (x : Fin 2) → y ≡ x
  letForall = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  forallInLet : List.All (λ (x : Fin 2) → let y = x in y ≡ # 1) (# 1 ∷ [])
  forallInLet = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  letForallIn : let y = # 1 in List.All (λ (x : Fin 2) → y ≡ x) (# 1 ∷ [])
  letForallIn = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module Test where

open import Data.List
open import Data.List.Instance
open import Data.Nat
open import Category.FAM

f : List ℕ → List ℕ
f = fmap suc

max_stars_repo_name: banacorn/FAM

max_issues_repo_name: banacorn/FAM

max_forks_repo_name: banacorn/FAM


text:
------------------------------------------------------------------------
-- Simple queues, implemented in the usual way using two lists
-- (following Hood and Melville)
------------------------------------------------------------------------

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

open import Equality

module Queue.Simple {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Bijection eq using (_↔_)
open import Equality.Decision-procedures eq
open import List eq as L hiding (map)
open import Surjection eq using (_↠_)

private
  variable
    a     : Level
    A B   : Type a
    x     : A
    f     : A → B
    xs ys : List A

------------------------------------------------------------------------
-- Invariant

-- The queue invariant: if the first list is empty, then the second
-- list is empty.

Invariant : {A : Type a} → List A → List A → Type a
Invariant (_ ∷ _) _       = ↑ _ ⊤
Invariant []      []      = ↑ _ ⊤
Invariant []      (_ ∷ _) = ⊥

-- The invariant is propositional.

Invariant-propositional : Is-proposition (Invariant xs ys)
Invariant-propositional {xs = []}    {ys = []} _ _ = refl _
Invariant-propositional {xs = _ ∷ _}           _ _ = refl _

-- Some lemmas related to the invariant.

-[] : Invariant xs []
-[] {xs = []}    = _
-[] {xs = _ ∷ _} = _

map-map : Invariant xs ys → Invariant (L.map f xs) (L.map f ys)
map-map {xs = _ ∷ _}           _ = _
map-map {xs = []}    {ys = []} _ = _

------------------------------------------------------------------------
-- Queues

-- Queues.
--
-- Note that the invariant is erased.

record Queue (A : Type a) : Type a where
  constructor ⟨_,_⟩
  field
    front rear     : List A
    @0 {invariant} : Invariant front rear

open Queue public

-- A variant of ⟨_,_⟩ with three explicit arguments.

pattern ⟨_,_⟩[_] f r i =
  record { front     = f
         ; rear      = r
         ; invariant = i
         }

------------------------------------------------------------------------
-- Conversion functions

-- Converts queues to lists.

to-List : Queue A → List A
to-List q = front q ++ reverse (rear q)

-- Converts lists to queues.

from-List : List A → Queue A
from-List xs = ⟨ xs , [] ⟩[ -[] ]

-- The function from-List is a right inverse of to-List.

to-List-from-List : to-List (from-List xs) ≡ xs
to-List-from-List {xs = xs} =
  xs ++ []  ≡⟨ ++-right-identity _ ⟩∎
  xs        ∎

-- If the carrier type is inhabited, then the function from-List is
-- not, in general, a left inverse of to-List.

¬-from-List-to-List :
  A → ¬ ((q : Queue A) → from-List (to-List q) ≡ q)
¬-from-List-to-List {A = A} x hyp = not-equal equal
  where
  counter-example : Queue A
  counter-example = ⟨ x ∷ [] , x ∷ [] ⟩

  not-equal : from-List (to-List counter-example) ≢ counter-example
  not-equal eq = List.[]≢∷ (cong rear eq)

  equal : from-List (to-List counter-example) ≡ counter-example
  equal = hyp counter-example

------------------------------------------------------------------------
-- The representation is not unique

-- If the carrier type is inhabited, then two queues representing the
-- same list are not necessarily equal.

representation-not-unique :
  A → ¬ ({q₁ q₂ : Queue A} → to-List q₁ ≡ to-List q₂ → q₁ ≡ q₂)
representation-not-unique x hyp =
  ¬-from-List-to-List x λ q → hyp (
    to-List (from-List (to-List q))  ≡⟨ to-List-from-List ⟩∎
    to-List q                        ∎)

-- If the carrier type is inhabited, then the type
-- ∃ λ (q : Queue A) → to-List q ≡ xs is not, in general, a
-- proposition.

¬-Σ-Queue-propositional :
  A →
  ¬ ({xs : List A} →
     Is-proposition (∃ λ (q : Queue A) → to-List q ≡ xs))
¬-Σ-Queue-propositional x hyp =
  representation-not-unique x λ {q₁ q₂} eq →
  cong proj₁ (
    q₁ , eq      ≡⟨ hyp _ _ ⟩∎
    q₂ , refl _  ∎)

------------------------------------------------------------------------
-- Queue operations

-- Enqueues an element.

enqueue : A → Queue A → Queue A
enqueue x ⟨ []            , rear ⟩ = ⟨ x ∷ [] , rear     ⟩
enqueue x ⟨ front@(_ ∷ _) , rear ⟩ = ⟨ front  , x ∷ rear ⟩

to-List-enqueue : ∀ q → to-List (enqueue x q) ≡ to-List q ++ x ∷ []
to-List-enqueue         ⟨ []            , []   ⟩ = refl _
to-List-enqueue {x = x} ⟨ front@(_ ∷ _) , rear ⟩ =
  front ++ reverse (x ∷ rear)        ≡⟨ cong (front ++_) $ reverse-∷ rear ⟩
  front ++ reverse rear ++ x ∷ []    ≡⟨ ++-associative front _ _ ⟩∎
  (front ++ reverse rear) ++ x ∷ []  ∎

-- Dequeues an element, if possible.

dequeue : Queue A → Maybe (A × Queue A)
dequeue ⟨ [] , [] ⟩ = nothing

dequeue ⟨ x ∷ [] , rear ⟩ =
  just (x , ⟨ reverse rear , [] ⟩[ -[] ])

dequeue ⟨ x ∷ front@(_ ∷ _) , rear ⟩ =
  just (x , ⟨ front , rear ⟩)

to-List-dequeue :
  {A : Type a} (q : Queue A) →
  ⊎-map id (Σ-map id to-List) (dequeue q) ≡
  _↔_.to List↔Maybe[×List] (to-List q)
to-List-dequeue ⟨ [] , [] ⟩ = refl _

to-List-dequeue ⟨ x ∷ [] , rear ⟩ = cong (just ∘ (x ,_)) (
  reverse rear ++ []  ≡⟨ ++-right-identity _ ⟩∎
  reverse rear        ∎)

to-List-dequeue ⟨ _ ∷ _ ∷ _ , _ ⟩ = refl _

-- The "inverse" of the dequeue operation.

dequeue⁻¹ : Maybe (A × Queue A) → Queue A
dequeue⁻¹ nothing                       = ⟨ [] , [] ⟩
dequeue⁻¹ (just (x , ⟨ front , rear ⟩)) = ⟨ x ∷ front , rear ⟩

to-List-dequeue⁻¹ :
  (x : Maybe (A × Queue A)) →
  to-List (dequeue⁻¹ x) ≡
  _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id to-List) x)
to-List-dequeue⁻¹ nothing  = refl _
to-List-dequeue⁻¹ (just _) = refl _

-- A map function.

map : (A → B) → Queue A → Queue B
map f ⟨ front , rear ⟩[ inv ] =
  ⟨ L.map f front , L.map f rear ⟩[ map-map inv ]

to-List-map : ∀ q → to-List (map f q) ≡ L.map f (to-List q)
to-List-map {f = f} ⟨ front , rear ⟩ =
  L.map f front ++ reverse (L.map f rear)  ≡⟨ cong (L.map f front ++_) $ sym $ map-reverse rear ⟩
  L.map f front ++ L.map f (reverse rear)  ≡⟨ sym $ map-++ _ front _ ⟩∎
  L.map f (front ++ reverse rear)          ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Algebra.Construct.Free.Semilattice.Relation.Unary.All.Map where

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

private
  variable p : Level

map-◻ : ∀ {p} {P : A → Type p} → (∀ x → P x) → ∀ xs → ◻ P xs
map-◻ {A = A} {P = P} = λ f → ∥ map-◻′ f ∥⇓
  where
  map-◻′ : (∀ x → P x) → xs ∈𝒦 A ⇒∥ ◻ P xs ∥
  ∥ map-◻′ f ∥-prop {xs} = isProp-◻ {P = P} {xs = xs}
  ∥ map-◻′ f ∥[] = tt
  ∥ map-◻′ f ∥ x ∷ xs ⟨ Pxs ⟩ = ∣ f x ∣ , Pxs

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module LC.Reasoning where

open import LC.Base
open import LC.Reduction

open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties using (preorder)
open import Relation.Binary.Reasoning.Preorder (preorder _β→_)
open import Relation.Binary.Reasoning.Preorder (preorder _β→_) using (begin_; step-≡; _∎; _≡⟨⟩_) public

infixr 2 _→*⟨_⟩_
_→*⟨_⟩_ : ∀ (x : Term) {y z} → x β→* y → y IsRelatedTo z → x IsRelatedTo z
x →*⟨ P ⟩ y = x ∼⟨ P ⟩ y

infixr 2 _→⟨_⟩_
_→⟨_⟩_ : ∀ (x : Term) {y z} → x β→ y → y IsRelatedTo z → x IsRelatedTo z
x →⟨ P ⟩ y = x ∼⟨ return P ⟩ y

infixr 2 _→⟨⟩_
_→⟨⟩_ : ∀ (x : Term) {y} → x IsRelatedTo y → x IsRelatedTo y
x →⟨⟩ y = x ∼⟨ ε ⟩ y

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Machine-checked formalization of the theoretical results presented
-- in the paper:
--
--   Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, Klaus Ostermann.
--   A Theory of Changes for Higher-Order Languages:
--   Incrementalizing λ-Calculi by Static Differentiation.
--   To appear at PLDI, ACM 2014.
--
-- We claim that this formalization
--
--   (1) proves every lemma and theorem in Sec. 2 and 3 of the paper,
--   (2) formally specifies the interface between our incrementalization
--       framework and potential plugins, and
--   (3) shows that the plugin interface can be instantiated.
--
-- The first claim is the main reason for a machine-checked
-- proof: We want to be sure that we got the proofs right.
--
-- The second claim is about reusability and applicability: Only
-- a clearly defined interface allows other researchers to
-- provide plugins for our framework.
--
-- The third claim is to show that the plugin interface is
-- consistent: An inconsistent plugin interface would allow to
-- prove arbitrary results in the framework.
------------------------------------------------------------------------

module README where

-- We know two good ways to read this code base. You can either
-- use Emacs with agda2-mode to interact with the source files,
-- or you can use a web browser to view the pretty-printed and
-- hyperlinked source files. For Agda power users, we also
-- include basic setup information for your own machine.

-- IF YOU WANT TO USE A BROWSER
-- ============================
--
-- Start with *HTML* version of this readme. On the AEC
-- submission website (online or inside the VM), follow the link
-- "view the Agda code in their browser" to the file
-- agda/README.html.
--
-- The source code is syntax highlighted and hyperlinked. You can
-- click on module names to open the corresponding files, or you
-- can click on identifiers to jump to their definition. In
-- general, a Agda file with name `Foo/Bar/Baz.agda` contains a
-- module `Foo.Bar.Baz` and is shown in an HTML file
-- `Foo.Bar.Baz.html`.
--
-- Note that we also include the HTML files generated for our
-- transitive dependencies from the Agda standard library. This
-- allows you to follow hyperlinks to the Agda standard
-- library. It is the default behavior of `agda --html` which we
-- used to generate the HTML.
--
-- To get started, continue below on "Where to start reading?".

-- IF YOU WANT TO USE EMACS
-- ========================
--
-- Open this file in Emacs with agda2-mode installed. See below
-- for which Agda version you need to install. On the VM image,
-- everything is setup for you and you can just open this file in
-- Emacs.
--
--   C-c C-l   Load code. Type checks and syntax highlights. Use
--             this if the code is not syntax highlighted, or
--             after you changed something that you want to type
--             check.
--
--   M-.       Jump to definition of identifier at the point.
--   M-*       Jump back.
--
-- Note that README.agda imports Everything.agda which imports
-- every Agda file in our formalization. So if README.agda type
-- checks successfully, everything does. If you want to type
-- check everything from scratch, delete the *.agdai files to
-- disable separate compilation. You can use "find . -name
-- '*.agdai' | xargs rm" to do that.
--
-- More information on the Agda mode is available on the Agda wiki:
--
-- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
-- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations
--
-- To get started, continue below on "Where to start reading?".

-- IF YOU WANT TO USE YOUR OWN SETUP
-- =================================
--
-- To typecheck this formalization, you need to install the appropriate version
-- of Agda (2.4.0.*), the Agda standard library (version 0.8), generate
-- Everything.agda with the attached Haskell helper, and finally run Agda on
-- this file.
--
-- Given a Unix-like environment (including Cygwin), running the ./agdaCheck.sh
-- script and following instructions given on output will eventually generate
-- Everything.agda and proceed to type check everything on command line.
--
-- If you're not an Agda power user, it is probably easier to use
-- the VM image or look at the pretty-printed and hyperlinked
-- HTML files, see above.

-- WHERE TO START READING?
-- =======================
--
-- modules.pdf
--   The graph of dependencies between Agda modules.
--   Good if you want to get a broad overview.
--
-- README.agda
--   This file. A coarse-grained introduction to the Agda
--   formalization.  Good if you want to begin at the beginning
--   and understand the structure of our code.
--
-- PLDI14-List-of-Theorems.agda
--   Pointers to the Agda formalizations of all theorems, lemmas
--   or definitions in the PLDI paper. Good if you want to read
--   the paper and the Agda code side by side.
--
--   Here is an import of this file, so you can jump to it
--   directly (use M-. in Emacs or click the module name in the
--   Browser):

import PLDI14-List-of-Theorems

-- Everything.agda
--   Imports every Agda module in our formalization. Good if you
--   want to make sure you don't miss anything.
--
--   Again, here's is an import of this file so you can navigate
--   there:

import Everything

-- (This import is also important to ensure that if we typecheck
-- README.agda, we also typecheck every other file of our
-- formalization).

-- THE AGDA CODE
-- =============
--
-- The formalization has four parts:
--
--   1. A formalization of change structures. This lives in
--   Base.Change.Algebra. (What we call "change structure" in the
--   paper, we call "change algebra" in the Agda code. We changed
--   the name when writing the paper, and never got around to
--   updating the name in the Agda code).
--
--   2. Incrementalization framework for first-class functions,
--   with extension points for plugging in data types and their
--   incrementalization. This lives in the Parametric.*
--   hierarchy.
--
--   3. An example plugin that provides integers and bags
--   with negative multiplicity. This lives in the Nehemiah.*
--   hierarchy. (For some reason, we choose to call this
--   particular incarnation of the plugin Nehemiah).
--
--   4. Other material that is unrelated to the framework/plugin
--   distinction. This is all other files.

-- FORMALIZATION OF CHANGE STRUCTURES
-- ==================================
--
-- Section 2 of the paper, and Base.Change.Algebra in Agda.

import Base.Change.Algebra

-- INCREMENTALIZATION FRAMEWORK
-- ============================
--
-- Section 3 of the paper, and Parametric.* hierarchy in Agda.
--
-- The extension points are implemented as module parameters. See
-- detailed explanation in Parametric.Syntax.Type and
-- Parametric.Syntax.Term. Some extension points are for types,
-- some for values, and some for proof fragments. In Agda, these
-- three kinds of entities are unified anyway, so we can encode
-- all of them as module parameters.
--
-- Every module in the Parametric.* hierarchy adds at least one
-- extension point, so the module hierarchy of a plugin will
-- typically mirror the Parametric.* hierarchy, defining the
-- values for these extension points.
--
-- Firstly, we have the syntax of types and terms, the erased
-- change structure for function types and incrementalization as
-- a term-to-term transformation. The contents of these modules
-- formalizes Sec. 3.1 and 3.2 of the paper, except for the
-- second and third line of Figure 3, which is formalized further
-- below.

import Parametric.Syntax.Type   -- syntax of types
import Parametric.Syntax.Term   -- syntax of terms
import Parametric.Change.Type   -- simply-typed changes
import Parametric.Change.Derive -- incrementalization

-- Secondly, we define the usual denotational semantics of the
-- simply-typed lambda calculus in terms of total functions, and
-- the change semantics in terms of a change structure on total
-- functions. The contents of these modules formalize Sec. 3.3,
-- 3.4 and 3.5 of the paper.

import Parametric.Denotation.Value      -- standard values
import Parametric.Denotation.Evaluation -- standard evaluation
import Parametric.Change.Validity       -- dependently-typed changes
import Parametric.Change.Specification  -- change evaluation

-- Thirdly, we define terms that operate on simply-typed changes,
-- and connect them to their values. The concents of these
-- modules formalize the second and third line of Figure 3, as
-- well as the semantics of these lines.

import Parametric.Change.Term        -- terms that operate on simply-typed changes
import Parametric.Change.Value       -- the values of these terms
import Parametric.Change.Evaluation  -- connecting the terms and their values

-- Finally, we prove correctness by connecting the (syntactic)
-- incrementalization to the (semantic) change evaluation by a
-- logical relation, and a proof that the values of terms
-- produced by the incrementalization transformation are related
-- to the change values of the original terms. The contents of
-- these modules formalize Sec. 3.6.

import Parametric.Change.Implementation -- logical relation
import Parametric.Change.Correctness    -- main correctness proof

-- EXAMPLE PLUGIN
-- ==============
--
-- Sec. 3.7 in the paper, and the Nehemiah.* hierarchy in Agda.
--
-- The module structure of the plugin follows the structure of
-- the Parametric.* hierarchy.  For example, the extension point
-- defined in Parametric.Syntax.Term is instantiated in
-- Nehemiah.Syntax.Term.
--
-- As discussed in Sec. 3.7 of the paper, the point of this
-- plugin is not to speed up any real programs, but to show "that
-- the interface for proof plugins can be implemented". As a
-- first step towards proving correctness of the more complicated
-- plugin with integers, bags and finite maps we implement in
-- Scala, we choose to define plugin with integers and bags in
-- Agda. Instead of implementing bags (with negative
-- multiplicities, like in the paper) in Agda, though, we
-- postulate that a group of such bags exist. Note that integer
-- bags with integer multiplicities are actually the free group
-- given a singleton operation `Integer -> Bag`, so this should
-- be easy to formalize in principle.

-- Before we start with the plugin, we postulate an abstract data
-- type for integer bags.
import Postulate.Bag-Nehemiah

-- Firstly, we extend the syntax of types and terms, the erased
-- change structure for function types, and incrementalization as
-- a term-to-term transformation to account for the data types of
-- the Nehemiah language. The contents of these modules
-- instantiate the extension points in Sec. 3.1 and 3.2 of the
-- paper, except for the second and third line of Figure 3, which
-- is instantiated further below.

import Nehemiah.Syntax.Type
import Nehemiah.Syntax.Term
import Nehemiah.Change.Type
import Nehemiah.Change.Derive

-- Secondly, we extend the usual denotational semantics and the
-- change semantics to account for the data types of the Nehemiah
-- language. The contents of these modules instantiate the
-- extension points in Sec. 3.3, 3.4 and 3.5 of the paper.

import Nehemiah.Denotation.Value
import Nehemiah.Denotation.Evaluation
import Nehemiah.Change.Validity

-- Thirdly, we extend the terms that operate on simply-typed
-- changes, and the connection to their values to account for the
-- data types of the Nehemiah language. The concents of these
-- modules instantiate the extension points in the second and
-- third line of Figure 3.

import Nehemiah.Change.Term
import Nehemiah.Change.Value
import Nehemiah.Change.Evaluation

-- Finally, we extend the logical relation and the main
-- correctness proof to account for the data types in the
-- Nehemiah language. The contents of these modules instantiate
-- the extension points defined in Sec. 3.6.

import Nehemiah.Change.Implementation
import Nehemiah.Change.Correctness

-- OTHER MATERIAL
-- ==============
--
-- We postulate extensionality of Agda functions. This postulate
-- is well known to be compatible with Agda's type theory.

import Postulate.Extensionality

-- For historical reasons, we reexport Data.List.All from the
-- standard library under the name DependentList.

import Base.Data.DependentList

-- This module supports overloading the ⟦_⟧ notation based on
-- Agda's instance arguments.

import Base.Denotation.Notation

-- These modules implement contexts including typed de Bruijn
-- indices to represent bound variables, sets of bound variables,
-- and environments. These modules are parametric in the set of
-- types (that are stored in contexts) and the set of values
-- (that are stored in environments). So these modules are even
-- more parametric than the Parametric.* hierarchy.

import Base.Syntax.Context
import Base.Syntax.Vars
import Base.Denotation.Environment

-- This module contains some helper definitions to merge a
-- context of values and a context of changes.
import Base.Change.Context

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

data Id (A : Set) : Set where
  mkId : A → Id A

data Monad (M : Set → Set) : Set where

postulate
  return : ∀ {M} {{Mon : Monad M}} {A} → A → M A
  _>>=_  : ∀ {M} {{Mon : Monad M}} {A B} → M A → (A → M B) → M B
  State : (S A : Set) → Set

  instance
    MonadState : ∀ {S} → Monad (State S)
    MonadId : Monad Id

-- Yields
--   _M Nat == State Nat Nat,
-- which inert improvement solves by
--   _M x := State (_S x) (_A x)
--     with _S Nat == Nat
--          _A Nat == Nat
-- This allows instance search to pick the right instance.
rz : State Nat Nat
rz = return zero

postulate
  StateT : (S : Set) (M : Set → Set) (A : Set) → Set

  instance
    MonadStateT : ∀ {S M} → Monad M → Monad (StateT S M)

stateT₁ : ∀ {M} {{Mon : Monad M}} → StateT Nat M Nat
stateT₁ = return zero

stateT₂ : ∀ {M} {{Mon : Monad M}} → StateT Nat M Nat
stateT₂ = return zero >>= λ n → return (suc n)

postulate
  _<$_ : ∀ {A B M} {{Mon : Monad M}} → A → M B → M A

record ⊤ : Set where
  constructor tt

foo : Id ⊤
foo = _ <$ return zero

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- Simple recognisers
------------------------------------------------------------------------

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

-- The recognisers are parametrised on the alphabet.

module TotalRecognisers.Simple
         (Tok : Set)
         (_≟_ : Decidable (_≡_ {A = Tok}))
         -- The tokens must come with decidable equality.
         where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool hiding (_≟_)
import Data.Bool.Properties as Bool
private
  module BoolCS = CommutativeSemiring Bool.∧-∨-commutativeSemiring
open import Function
open import Data.List
open import Data.Product
open import Relation.Nullary

------------------------------------------------------------------------
-- Recogniser combinators

infixl 10 _·_
infixl  5 _∣_

mutual

  -- The index is true if the corresponding language contains the
  -- empty string (is nullable).

  data P : Bool → Set where
    fail  : P false
    empty : P true
    tok   : Tok → P false
    _∣_   : ∀ {n₁ n₂} → P n₁ →            P n₂ → P (n₁ ∨ n₂)
    _·_   : ∀ {n₁ n₂} → P n₁ → ∞⟨ not n₁ ⟩P n₂ → P (n₁ ∧ n₂)

  -- Coinductive if the index is true.

  ∞⟨_⟩P : Bool → Bool → Set
  ∞⟨ true  ⟩P n = ∞ (P n)
  ∞⟨ false ⟩P n =    P n

------------------------------------------------------------------------
-- Conditional coinduction helpers

delayed? : ∀ {b n} → ∞⟨ b ⟩P n → Bool
delayed? {b = b} _ = b

♭? : ∀ {b n} → ∞⟨ b ⟩P n → P n
♭? {true}  x = ♭ x
♭? {false} x =   x

♯? : ∀ {b n} → P n → ∞⟨ b ⟩P n
♯? {true}  x = ♯ x
♯? {false} x =   x

-- A lemma.

♭?♯? : ∀ b {n} {p : P n} → ♭? {b} (♯? p) ≡ p
♭?♯? true  = refl
♭?♯? false = refl

------------------------------------------------------------------------
-- Semantics

-- The semantics is defined inductively: s ∈ p iff the string s is
-- contained in the language defined by p.

infix 4 _∈_

data _∈_ : ∀ {n} → List Tok → P n → Set where
  empty   : [] ∈ empty
  tok     : ∀ {t} → [ t ] ∈ tok t
  ∣-left  : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
            s ∈ p₁ → s ∈ p₁ ∣ p₂
  ∣-right : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
            s ∈ p₂ → s ∈ p₁ ∣ p₂
  _·_     : ∀ {s₁ s₂ n₁ n₂} {p₁ : P n₁} {p₂ : ∞⟨ not n₁ ⟩P n₂} →
            s₁ ∈ p₁ → s₂ ∈ ♭? p₂ → s₁ ++ s₂ ∈ p₁ · p₂

-- A lemma.

cast : ∀ {n} {p p′ : P n} {s} → p ≡ p′ → s ∈ p → s ∈ p′
cast refl s∈ = s∈

------------------------------------------------------------------------
-- Nullability

-- The nullability index is correct.

⇒ : ∀ {n} {p : P n} → [] ∈ p → n ≡ true
⇒ pr = ⇒′ pr refl
  where
  ⇒′ : ∀ {n s} {p : P n} → s ∈ p → s ≡ [] → n ≡ true
  ⇒′ empty                   refl = refl
  ⇒′ tok                     ()
  ⇒′ (∣-left            pr₁) refl with ⇒ pr₁
  ⇒′ (∣-left            pr₁) refl | refl = refl
  ⇒′ (∣-right           pr₂) refl with ⇒ pr₂
  ⇒′ (∣-right {n₁ = n₁} pr₂) refl | refl = proj₂ BoolCS.zero n₁
  ⇒′ (_·_ {[]}    pr₁ pr₂)   refl = cong₂ _∧_ (⇒ pr₁) (⇒ pr₂)
  ⇒′ (_·_ {_ ∷ _} pr₁ pr₂)   ()

⇐ : ∀ {n} (p : P n) → n ≡ true → [] ∈ p
⇐ fail                         ()
⇐ empty                        refl = empty
⇐ (tok t)                      ()
⇐ (_∣_ {true}           p₁ p₂) refl = ∣-left            (⇐ p₁ refl)
⇐ (_∣_ {false} {true}   p₁ p₂) refl = ∣-right {p₁ = p₁} (⇐ p₂ refl)
⇐ (_∣_ {false} {false}  p₁ p₂) ()
⇐ (_·_ {true}  p₁ p₂)          refl = ⇐ p₁ refl · ⇐ p₂ refl
⇐ (_·_ {false} p₁ p₂)          ()

-- We can decide if the empty string belongs to a given language.

nullable? : ∀ {n} (p : P n) → Dec ([] ∈ p)
nullable? {true}  p = yes (⇐ p refl)
nullable? {false} p = no helper
  where
  helper : ¬ [] ∈ p
  helper []∈p with ⇒ []∈p
  ... | ()

------------------------------------------------------------------------
-- Derivative

-- D-nullable and D are placed in a mutual block to ensure that the
-- underscores in the definition of D-nullable can be solved by
-- constraints introduced in the body of D. The functions are not
-- actually mutually recursive.

mutual

  -- The index of the derivative. The right-hand sides (excluding
  -- t′ ≟ t and delayed? p₂) are inferable, but included here so that
  -- they can easily be inspected.

  D-nullable : ∀ {n} → Tok → P n → Bool
  D-nullable t fail      = false
  D-nullable t empty     = false
  D-nullable t (tok t′)  with t′ ≟ t
  D-nullable t (tok t′)  | yes t′≡t = true
  D-nullable t (tok t′)  | no  t′≢t = false
  D-nullable t (p₁ ∣ p₂) = D-nullable t p₁ ∨ D-nullable t p₂
  D-nullable t (p₁ · p₂) with delayed? p₂
  D-nullable t (p₁ · p₂) | true  = D-nullable t p₁ ∧ _
  D-nullable t (p₁ · p₂) | false = D-nullable t p₁ ∧ _ ∨ D-nullable t p₂

  -- D t p is the "derivative" of p with respect to t. It is specified
  -- by the equivalence s ∈ D t p ⇔ t ∷ s ∈ p (proved below).

  D : ∀ {n} (t : Tok) (p : P n) → P (D-nullable t p)
  D t fail      = fail
  D t empty     = fail
  D t (tok t′)  with t′ ≟ t
  D t (tok t′)  | yes t′≡t = empty
  D t (tok t′)  | no  t′≢t = fail
  D t (p₁ ∣ p₂) = D t p₁ ∣ D t p₂
  D t (p₁ · p₂) with delayed? p₂
  D t (p₁ · p₂) | true  = D t p₁ · ♯? (♭ p₂)
  D t (p₁ · p₂) | false = D t p₁ · ♯?    p₂ ∣ D t p₂

-- D is correct.

D-sound : ∀ {s n} {t} {p : P n} → s ∈ D t p → t ∷ s ∈ p
D-sound s∈ = D-sound′ _ _ s∈
  where
  D-sound′ : ∀ {s n} t (p : P n) → s ∈ D t p → t ∷ s ∈ p
  D-sound′ t fail                ()
  D-sound′ t empty               ()
  D-sound′ t (tok t′)            _                   with t′ ≟ t
  D-sound′ t (tok .t)            empty               | yes refl = tok
  D-sound′ t (tok t′)            ()                  | no  t′≢t
  D-sound′ t (p₁ ∣ p₂)           (∣-left  ∈₁)        = ∣-left            (D-sound′ t p₁ ∈₁)
  D-sound′ t (p₁ ∣ p₂)           (∣-right ∈₂)        = ∣-right {p₁ = p₁} (D-sound′ t p₂ ∈₂)
  D-sound′ t (_·_ {true}  p₁ p₂) (∣-left  (∈₁ · ∈₂)) = D-sound′ t p₁ ∈₁ · cast (♭?♯? (not (D-nullable t p₁))) ∈₂
  D-sound′ t (_·_ {true}  p₁ p₂) (∣-right ∈₂)        = ⇐ p₁ refl · D-sound′ t p₂ ∈₂
  D-sound′ t (_·_ {false} p₁ p₂) (∈₁ · ∈₂)           = D-sound′ t p₁ ∈₁ · cast (♭?♯? (not (D-nullable t p₁))) ∈₂

D-complete : ∀ {s n} {t} {p : P n} → t ∷ s ∈ p → s ∈ D t p
D-complete {t = t} t∷s∈ = D-complete′ _ t∷s∈ refl
  where
  D-complete′ : ∀ {s s′ n} (p : P n) → s′ ∈ p → s′ ≡ t ∷ s → s ∈ D t p
  D-complete′         fail     ()  refl
  D-complete′         empty    ()  refl
  D-complete′         (tok t′) _   refl with t′ ≟ t
  D-complete′         (tok .t) tok refl | yes refl = empty
  D-complete′ {[]}    (tok .t) tok refl | no  t′≢t with t′≢t refl
  D-complete′ {[]}    (tok .t) tok refl | no  t′≢t | ()
  D-complete′ (p₁ ∣ p₂)           (∣-left  ∈₁)         refl = ∣-left                    (D-complete ∈₁)
  D-complete′ (p₁ ∣ p₂)           (∣-right ∈₂)         refl = ∣-right {p₁ = D t p₁}     (D-complete ∈₂)
  D-complete′ (_·_ {true}  p₁ p₂) (_·_ {[]}     ∈₁ ∈₂) refl = ∣-right {p₁ = D t p₁ · _} (D-complete ∈₂)
  D-complete′ (_·_ {true}  p₁ p₂) (_·_ {._ ∷ _} ∈₁ ∈₂) refl = ∣-left (D-complete ∈₁ · cast (sym (♭?♯? (not (D-nullable t p₁)))) ∈₂)
  D-complete′ (_·_ {false} p₁ p₂) (_·_ {[]}     ∈₁ ∈₂) refl with ⇒ ∈₁
  D-complete′ (_·_ {false} p₁ p₂) (_·_ {[]}     ∈₁ ∈₂) refl | ()
  D-complete′ (_·_ {false} p₁ p₂) (_·_ {._ ∷ _} ∈₁ ∈₂) refl = D-complete ∈₁ · cast (sym (♭?♯? (not (D-nullable t p₁)))) ∈₂

------------------------------------------------------------------------
-- _∈_ is decidable

-- _∈?_ runs a recogniser. Note that the result is yes or no plus a
-- /proof/ verifying that the answer is correct.

infix 4 _∈?_

_∈?_ : ∀ {n} (s : List Tok) (p : P n) → Dec (s ∈ p)
[]    ∈? p = nullable? p
t ∷ s ∈? p with s ∈? D t p
t ∷ s ∈? p | yes s∈Dtp = yes (D-sound s∈Dtp)
t ∷ s ∈? p | no  s∉Dtp = no  (s∉Dtp ∘ D-complete)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Andreas, 2011-09-11
module Issue392 where
import Common.Irrelevance

-- Create an non-irrelevant record R1 (at least one field relevant).
record R1 : Set1 where
  field
    .f1 : Set
    f1' : Set

{- This creates a module with an relevant record parameter

   module R1 (r : R1) where
     .f1 : Set -- = R1.f1 r
     f1' : Set
-}

-- Create an irrelevant instance f2 of R1.
record R2 : Set2 where
  field
    .f2 : R1
    f3  : Set

-- This should not succeed.
  open R1 f2 public

{-
identifier f2 is declared irrelevant, so it cannot be used here
when checking that the expression f2 has type R1
-}


text:
module Generic.Lib.Equality.Heteroindexed where

open import Data.Product

open import Generic.Lib.Equality.Propositional

data [_]_≅_ {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : ∀ {j} -> A j -> Set where
  irefl : [ A ] x ≅ x

inds : ∀ {ι α} {I : Set ι} {A : I -> Set α} {i j} {x : A i} {y : A j}
     -> [ A ] x ≅ y -> i ≡ j
inds irefl = refl

homo : ∀ {ι α} {I : Set ι} {A : I -> Set α} {i} {x y : A i}
     -> [ A ] x ≅ y -> x ≡ y
homo irefl = refl

inds-homo : ∀ {ι α} {I : Set ι} {A : Set α} {i j : I} {x y : A}
          -> [_]_≅_ {i = i} (λ _ -> A) x {j} y -> i ≡ j × x ≡ y
inds-homo irefl = refl , refl

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module IndentedCheckingMessages where

import A.M

Foo : Set
Foo = Foo


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED, please use `Data.Record` directly.
------------------------------------------------------------------------

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

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)

module Record {ℓ} (Label : Set ℓ) (_≟_ : Decidable {A = Label} _≡_) where

{-# WARNING_ON_IMPORT
"Record was deprecated in v1.1.
Use Data.Record instead."
#-}

open import Data.Record Label _≟_ public


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

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

record Box (A : Set) : Set where
  constructor box
  field
    unbox : A
open Box

postulate
  A : Set
  a b : A

  f : (X : Set) → X → A
  g : (X : Set) → X

  rewf₁ : f (Box A) (box a) ≡ a
  rewf₂ : (X : Set) → f X (g X) ≡ b

  rewg : g (Box A) .unbox ≡ a

test = f (Box A) (g (Box A))

{-# REWRITE rewf₁ rewg #-}

rewg-contracted : g (Box A) ≡ box a
rewg-contracted = refl

foo : test ≡ a
foo = refl

{-# REWRITE rewf₂ #-}

bar : test ≡ b
bar = refl

fails : a ≡ b
fails = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Construction.Diagonal where

-- A variety of Diagonal functors

open import Level
open import Data.Product using (_,_)

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Product
open import Categories.Category.Construction.Functors
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation using (ntHelper)

import Categories.Functor.Power as Power

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

Δ : (C : Category o ℓ e) → Functor C (Product C C)
Δ C = record
  { F₀           = λ x → x , x
  ; F₁           = λ f → f , f
  ; identity     = refl , refl
  ; homomorphism = refl , refl
  ; F-resp-≈     = λ x → x , x
  }
  where
    open Category C
    open Equiv

Δ′ : (I : Set) → (C : Category o ℓ e) → Functor C (Power.Exp C I)
Δ′ I C = record
  { F₀           = λ x _ → x
  ; F₁           = λ f _ → f
  ; identity     = λ _ → refl
  ; homomorphism = λ _ → refl
  ; F-resp-≈     = λ x _ → x
  }
  where open Category.Equiv C

ΔF : {C : Category o ℓ e} (I : Category o′ ℓ′ e′) → Functor C (Functors I C)
ΔF {C = C} I = record
  { F₀           = const
  ; F₁           = λ f → ntHelper record { η = λ _ → f; commute = λ _ → C.identityʳ ○ ⟺ C.identityˡ }
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ x → x
  }
 where
   module C = Category C
   open C.Equiv
   open C.HomReasoning using (_○_; ⟺)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Data.NatMinusOne.Base where

open import Cubical.Core.Primitives
open import Cubical.Data.Nat

data ℕ₋₁ : Set where
  neg1 : ℕ₋₁
  suc  : (n : ℕ₋₁) → ℕ₋₁

_+₋₁_ : ℕ → ℕ₋₁ → ℕ₋₁
0 +₋₁ n = n
suc m +₋₁ n = suc (m +₋₁ n)

ℕ→ℕ₋₁ : ℕ → ℕ₋₁
ℕ→ℕ₋₁ n = suc (n +₋₁ neg1)

1+_ : ℕ₋₁ → ℕ
1+ neg1 = zero
1+ suc n = suc (1+ n)

-1+_ : ℕ → ℕ₋₁
-1+ zero = neg1
-1+ suc n = suc (-1+ n)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module fib1 where

data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

_+_ : ℕ -> ℕ ->  ℕ
n + Z   = n
n + S m = S (n + m)

one : ℕ
one = S Z

fib : ℕ -> ℕ
fib Z         = one
fib (S Z)     = one
fib (S (S n)) = fib n + fib (S n)

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.Eigen
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (_+ᵥ_ : V → V → V)
  (_⋅ₛᵥ_ : S → V → V)
  (_+ₛ_ _⋅ₛ_ : S → S → S)
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Syntax.Function

-- v is a eigenvector for the eigenvalue 𝜆 of the linear transformation f.
-- Multiplication by an eigenvalue can replace a linear transformation for certain vectors.
Eigenpair : (V → V) → S → V → Stmt
Eigenpair(f)(𝜆)(v) = ((v ≢ 𝟎ᵥ) ∧ (f(v) ≡ 𝜆 ⋅ₛᵥ v))

Eigenvector : (V → V) → V → Stmt
Eigenvector(f)(v) = ∃(𝜆 ↦ Eigenpair(f)(𝜆)(v))

Eigenvalue : (V → V) → S → Stmt
Eigenvalue(f)(𝜆) = ∃(v ↦ Eigenpair(f)(𝜆)(v))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Base
open import Homotopy.Truncation
open import Homotopy.Connected
open import Spaces.Suspension
open import Homotopy.PushoutDef
import Homotopy.PushoutUP as PushoutUP

-- In this file I prove that if [A] is n-connected and its (n+1)-truncation is
-- inhabited, then [suspension A] is (n+1)-connected.
--
-- The hypothesis that [τ (S n) A] is inhabited is not necessary, it can be
-- removed but it’s simpler to assume it

module Homotopy.ConnectedSuspension
  {i} (A : Set i) {n : ℕ₋₂} (p : is-connected n A) (x₀ : τ (S n) A) where

-- The (n+1)-truncation of the suspension is a pushout of the following diagram

τ-susp-diag : pushout-diag i
τ-susp-diag = diag τ (S n) unit , τ (S n) unit , τ (S n) A
              , τ-extend-nondep (λ _ → proj tt)
              , τ-extend-nondep (λ _ → proj tt)

module τ-susp-H = PushoutUP τ-susp-diag (is-truncated (S n))

import Homotopy.TruncationRightExact (S n) (suspension-diag A) as Exact

abstract
  trunc-cocone : τ-susp-H.cocone (τ (S n) (suspension A))
  trunc-cocone = Exact.cocone-τpushout

  trunc-is-pushout : τ-susp-H.is-pushout (τ (S n) (suspension A)) trunc-cocone
  trunc-is-pushout = Exact.τpushout-is-pushout

-- The previous diagram is equivalent to the following

susp-diag : pushout-diag i
susp-diag = suspension-diag (τ (S n) A)

module susp-H = PushoutUP susp-diag (is-truncated (S n))

-- To be moved
τ-unit-to-unit : τ (S n) (unit {i}) → unit {i}
τ-unit-to-unit _ = tt

abstract
  τ-unit-to-unit-is-equiv : is-equiv τ-unit-to-unit
  τ-unit-to-unit-is-equiv =
    iso-is-eq _ (λ _ → proj tt)
      (λ _ → refl)
      (τ-extend
         ⦃ λ _ → ≡-is-truncated (S n) (τ-is-truncated (S n) _) ⦄
        (λ _ → refl))

τ-unit-equiv-unit : τ (S n) unit ≃ unit
τ-unit-equiv-unit = (τ-unit-to-unit , τ-unit-to-unit-is-equiv)
-- / To be moved

abstract
  τ-susp-equal-susp : τ-susp-diag ≡ susp-diag
  τ-susp-equal-susp = pushout-diag-eq τ-unit-equiv-unit τ-unit-equiv-unit
                        (id-equiv _) (λ _ → refl) (λ _ → refl)

  -- But we prove by hand that the point is also a pushout of this diagram
  unit-cocone : susp-H.cocone unit
  unit-cocone = (id _ susp-H., id _ , cst refl)

  private
    factor-pushout : (E : Set i) → (susp-H.cocone E → (unit {i} → E))
    factor-pushout E c = susp-H.A→top c

    x : {E : Set i} → (susp-H.cocone E → E)
    x c = susp-H.A→top c tt

    y : {E : Set i} → (susp-H.cocone E → E)
    y c = susp-H.B→top c tt

    x≡y : {E : Set i} (c : susp-H.cocone E) → x c ≡ y c
    x≡y c = susp-H.h c x₀

    ττA-is-contr : is-contr (τ n (τ (S n) A))
    ττA-is-contr = equiv-types-truncated _ (τ-equiv-ττ n A) p

  susp-H-unit-is-pushout : susp-H.is-pushout unit unit-cocone
  susp-H-unit-is-pushout E ⦃ P-E ⦄ =
    iso-is-eq _
      (factor-pushout E)
      (λ c →
        susp-H.cocone-eq-raw _ refl (funext (λ _ → x≡y c))
          (app-is-inj x₀ ττA-is-contr (P-E _ _)
            (trans-Π2 _ (λ v _ → susp-H.A→top c tt ≡ v tt)
              (funext (λ r → susp-H.h c x₀)) _ _
              ∘ (trans-cst≡app _ (λ u → u tt) (funext (λ r → susp-H.h c x₀)) _
              ∘ happly (happly-funext (λ _ → susp-H.h c x₀)) tt))))
      (λ _ → refl)

-- Type of (S n)-truncated pushout-diagrams (this should probably be defined
-- more generally in Homotopy.PushoutDef or something)
truncated-diag : Set _
truncated-diag = Σ (pushout-diag i)
                 (λ d → (is-truncated (S n) (pushout-diag.A d))
                        × ((is-truncated (S n) (pushout-diag.B d))
                        × (is-truncated (S n) (pushout-diag.C d))))

τ-susp-trunc-diag : truncated-diag
τ-susp-trunc-diag = (τ-susp-diag , (τ-is-truncated (S n) _ ,
                                     (τ-is-truncated (S n) _ ,
                                      τ-is-truncated (S n) _)))

susp-trunc-diag : truncated-diag
susp-trunc-diag = (susp-diag , (unit-is-truncated-S#instance ,
                               (unit-is-truncated-S#instance ,
                                τ-is-truncated (S n) _)))

-- The two diagrams are equal as truncated diagrams
abstract
  τ-susp-trunc-equal-susp-trunc : τ-susp-trunc-diag ≡ susp-trunc-diag
  τ-susp-trunc-equal-susp-trunc = Σ-eq τ-susp-equal-susp
                (Σ-eq (π₁ (is-truncated-is-prop (S n) _ _))
                (Σ-eq (π₁ (is-truncated-is-prop (S n) _ _))
                (π₁ (is-truncated-is-prop (S n) _ _))))

new-cocone : (d : truncated-diag) → (Set i → Set i)
new-cocone (d , (_ , (_ , _))) =
  PushoutUP.cocone d (is-truncated (S n))

new-is-pushout : (d : truncated-diag)
  → ((D : Set i) ⦃ PD : is-truncated (S n) D ⦄
     (Dcocone : new-cocone d D) → Set _)
new-is-pushout (d , (_ , (_ , _))) =
  PushoutUP.is-pushout d (is-truncated (S n))

unit-new-cocone : (d : truncated-diag) → new-cocone d unit
unit-new-cocone d = ((λ _ → tt) PushoutUP., (λ _ → tt) , (λ _ → refl))

unit-is-pushout : (d : truncated-diag) → Set _
unit-is-pushout d = new-is-pushout d unit (unit-new-cocone d)

abstract
  unit-τ-is-pushout :
    τ-susp-H.is-pushout unit (unit-new-cocone τ-susp-trunc-diag)
  unit-τ-is-pushout =
    transport unit-is-pushout (! τ-susp-trunc-equal-susp-trunc)
              susp-H-unit-is-pushout

private
  unit-equiv-τSnΣA : unit {i} ≃ τ (S n) (suspension A)
  unit-equiv-τSnΣA =
    τ-susp-H.pushout-equiv-pushout
      unit   (unit-new-cocone τ-susp-trunc-diag) unit-τ-is-pushout
      (τ (S n) (suspension A)) trunc-cocone      trunc-is-pushout

abstract
  suspension-is-connected-S : is-connected (S n) (suspension A)
  suspension-is-connected-S =
    equiv-types-truncated _ unit-equiv-τSnΣA unit-is-contr

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.Bool
open import lib.types.FunctionSeq
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Suspension.Core
open import lib.types.Suspension.Trunc
open import lib.types.Truncation

module lib.types.Suspension.Flip where

module SuspFlip {i} {A : Type i} = SuspRec
  (south' A) north (! ∘ merid)

Susp-flip : ∀ {i} {A : Type i} → Susp A → Susp A
Susp-flip = SuspFlip.f

Susp-flip-σloop-seq : ∀ {i} (X : Ptd i) (x : de⊙ X)
  → ap Susp-flip (σloop X x) =-= ! (merid x) ∙ merid (pt X)
Susp-flip-σloop-seq X x =
  ap Susp-flip (merid x ∙ ! (merid (pt X)))
    =⟪ ap-∙ Susp-flip (merid x) (! (merid (pt X))) ⟫
  ap Susp-flip (merid x) ∙ ap Susp-flip (! (merid (pt X)))
    =⟪ ap2 _∙_
           (! (!-! (ap Susp-flip (merid x))) ∙ ap ! (r x))
           (ap-! Susp-flip (merid (pt X)) ∙ r (pt X)) ⟫
  ! (merid x) ∙ merid (pt X) ∎∎
  where
    r : (x : de⊙ X) → ! (ap Susp-flip (merid x)) == merid x
    r x = ap ! (SuspFlip.merid-β x) ∙ !-! (merid x)

Susp-flip-σloop : ∀ {i} (X : Ptd i) (x : de⊙ X)
  → ap Susp-flip (σloop X x) == ! (merid x) ∙ merid (pt X)
Susp-flip-σloop X x = ↯ (Susp-flip-σloop-seq X x)

Susp-flip-σloop-pt : ∀ {i} (X : Ptd i)
  → Susp-flip-σloop X (pt X) ◃∎
    =ₛ
    ap (ap Susp-flip) (!-inv-r (merid (pt X))) ◃∙
    ! (!-inv-l (merid (pt X))) ◃∎
Susp-flip-σloop-pt X =
  Susp-flip-σloop X (pt X) ◃∎
    =ₛ⟨ expand (Susp-flip-σloop-seq X (pt X)) ⟩
  Susp-flip-σloop-seq X (pt X)
    =ₛ⟨ coh Susp-flip (merid (pt X)) (merid (pt X))
            (ap ! (SuspFlip.merid-β (pt X)) ∙ !-! (merid (pt X))) ⟩
  ap (ap Susp-flip) (!-inv-r (merid (pt X))) ◃∙
  ! (!-inv-l (merid (pt X))) ◃∎ ∎ₛ
  where
  coh : ∀ {j k} {A : Type j} {B : Type k} (f : A → B)
    {a₀ a₁ : A} (p : a₀ == a₁)
    (q : f a₁ == f a₀)
    (r : ! (ap f p) == q)
    → ap-∙ f p (! p) ◃∙
      ap2 _∙_ (! (!-! (ap f p)) ∙ ap ! r) (ap-! f p ∙ r) ◃∎
      =ₛ
      ap (ap f) (!-inv-r p) ◃∙
      ! (!-inv-l q) ◃∎
  coh f p@idp q@.idp r@idp = =ₛ-in idp

maybe-Susp-flip : ∀ {i} {A : Type i} → Bool → Susp A → Susp A
maybe-Susp-flip true = Susp-flip
maybe-Susp-flip false = idf _

⊙Susp-flip : ∀ {i} (X : Ptd i) → ⊙Susp (de⊙ X) ⊙→ ⊙Susp (de⊙ X)
⊙Susp-flip X = (Susp-flip , ! (merid (pt X)))

⊙maybe-Susp-flip : ∀ {i} (X : Ptd i) → Bool → ⊙Susp (de⊙ X) ⊙→ ⊙Susp (de⊙ X)
⊙maybe-Susp-flip X true  = ⊙Susp-flip X
⊙maybe-Susp-flip X false = ⊙idf (⊙Susp (de⊙ X))

de⊙-⊙maybe-Susp-flip : ∀ {i} (X : Ptd i) (b : Bool)
  → fst (⊙maybe-Susp-flip X b) == maybe-Susp-flip b
de⊙-⊙maybe-Susp-flip X true  = idp
de⊙-⊙maybe-Susp-flip X false = idp

Susp-flip-flip : ∀ {i} {A : Type i} (sa : Susp A)
  → Susp-flip (Susp-flip sa) == sa
Susp-flip-flip =
  Susp-elim
    idp
    idp $ λ a → ↓-='-in' $
  ap (λ z → z) (merid a)
    =⟨ ap-idf (merid a) ⟩
  merid a
    =⟨ ! (!-! (merid a)) ⟩
  ! (! (merid a))
    =⟨ ap ! (! (SuspFlip.merid-β a)) ⟩
  ! (ap Susp-flip (merid a))
    =⟨ !-ap Susp-flip (merid a) ⟩
  ap Susp-flip (! (merid a))
    =⟨ ap (ap Susp-flip) (! (SuspFlip.merid-β a)) ⟩
  ap Susp-flip (ap Susp-flip (merid a))
    =⟨ ∘-ap Susp-flip Susp-flip (merid a) ⟩
  ap (Susp-flip ∘ Susp-flip) (merid a) =∎

⊙Susp-flip-flip : ∀ {i} {X : Ptd i}
  → ⊙Susp-flip X ◃⊙∘ ⊙Susp-flip X ◃⊙idf =⊙∘ ⊙idf-seq
⊙Susp-flip-flip {_} {X} =
  ⊙seq-λ= Susp-flip-flip $
  ap Susp-flip (! (merid (pt X))) ◃∙
  ! (merid (pt X)) ◃∎
    =ₛ₁⟨ 0 & 1 & ap-! Susp-flip (merid (pt X)) ⟩
  ! (ap Susp-flip (merid (pt X))) ◃∙
  ! (merid (pt X)) ◃∎
    =ₛ₁⟨ 0 & 1 & ap ! (SuspFlip.merid-β (pt X)) ⟩
  ! (! (merid (pt X))) ◃∙
  ! (merid (pt X)) ◃∎
    =ₛ₁⟨ !-inv-l (! (merid (pt X))) ⟩
  idp ◃∎ ∎ₛ

⊙maybe-Susp-flip-flip : ∀ {i} (X : Ptd i) (b c : Bool)
  → ⊙maybe-Susp-flip X b ◃⊙∘ ⊙maybe-Susp-flip X c ◃⊙idf
    =⊙∘
    ⊙maybe-Susp-flip X (xor b c) ◃⊙idf
⊙maybe-Susp-flip-flip X true  true  =
  ⊙Susp-flip X ◃⊙∘ ⊙Susp-flip X ◃⊙idf
    =⊙∘⟨ ⊙Susp-flip-flip ⟩
  ⊙idf-seq
    =⊙∘⟨ ⊙contract ⟩
  ⊙idf _ ◃⊙idf ∎⊙∘
⊙maybe-Susp-flip-flip X true  false = =⊙∘-in idp
⊙maybe-Susp-flip-flip X false true  = =⊙∘-in (⊙λ= (⊙∘-unit-l (⊙Susp-flip X)))
⊙maybe-Susp-flip-flip X false false = =⊙∘-in idp

Susp-flip-equiv : ∀ {i} {A : Type i} → Susp A ≃ Susp A
Susp-flip-equiv {A = A} =
  equiv Susp-flip Susp-flip Susp-flip-flip Susp-flip-flip

Susp-flip-natural : ∀ {i} {j} {A : Type i} {B : Type j} (f : A → B)
  → ∀ σ → Susp-flip (Susp-fmap f σ) == Susp-fmap f (Susp-flip σ)
Susp-flip-natural f = Susp-elim idp idp $ λ y → ↓-='-in' $
  ap (Susp-fmap f ∘ Susp-flip) (merid y)
    =⟨ ap-∘ (Susp-fmap f) Susp-flip (merid y) ⟩
  ap (Susp-fmap f) (ap Susp-flip (merid y))
    =⟨ ap (ap (Susp-fmap f)) (SuspFlip.merid-β y) ⟩
  ap (Susp-fmap f) (! (merid y))
    =⟨ ap-! (Susp-fmap f) (merid y) ⟩
  ! (ap (Susp-fmap f) (merid y))
    =⟨ ap ! (SuspFmap.merid-β f y) ⟩
  ! (merid (f y))
    =⟨ ! (SuspFlip.merid-β (f y)) ⟩
  ap Susp-flip (merid (f y))
    =⟨ ! (ap (ap Susp-flip) (SuspFmap.merid-β f y)) ⟩
  ap Susp-flip (ap (Susp-fmap f) (merid y))
    =⟨ ∘-ap Susp-flip (Susp-fmap f) (merid y) ⟩
  ap (Susp-flip ∘ Susp-fmap f) (merid y) =∎

⊙Susp-flip-natural : ∀ {i} {j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
  → ⊙Susp-flip Y ⊙∘ ⊙Susp-fmap (fst f) == ⊙Susp-fmap (fst f) ⊙∘ ⊙Susp-flip X
⊙Susp-flip-natural {_} {_} {X} {Y} f =
  pair= (λ= (Susp-flip-natural (fst f))) $
  ↓-app=cst-in $ ! $ =ₛ-out {t = ! (merid (pt Y)) ◃∎} $
  app= (λ= (Susp-flip-natural (fst f))) north ◃∙
  ap (Susp-fmap (fst f)) (! (merid (pt X))) ◃∙
  idp ◃∎
    =ₛ⟨ 2 & 1 & expand [] ⟩
  app= (λ= (Susp-flip-natural (fst f))) north ◃∙
  ap (Susp-fmap (fst f)) (! (merid (pt X))) ◃∎
    =ₛ₁⟨ 0 & 1 & app=-β (Susp-flip-natural (fst f)) north ⟩
  idp ◃∙
  ap (Susp-fmap (fst f)) (! (merid (pt X))) ◃∎
    =ₛ⟨ 0 & 1 & expand [] ⟩
  ap (Susp-fmap (fst f)) (! (merid (pt X))) ◃∎
    =ₛ₁⟨ ap-! (Susp-fmap (fst f)) (merid (pt X)) ⟩
  ! (ap (Susp-fmap (fst f)) (merid (pt X))) ◃∎
    =ₛ₁⟨ ap ! (SuspFmap.merid-β (fst f) (pt X)) ⟩
  ! (merid (fst f (pt X))) ◃∎
    =ₛ₁⟨ ap (! ∘ merid) (snd f) ⟩
  ! (merid (pt Y)) ◃∎ ∎ₛ

module _ {i} {A : Type i} where

  Susp-fmap-flip : (x : Susp (Susp A))
    → Susp-fmap Susp-flip x == Susp-flip x
  Susp-fmap-flip =
    Susp-elim
      {P = λ x → Susp-fmap Susp-flip x == Susp-flip x}
      (merid north)
      (! (merid south)) $ λ y →
    ↓-='-in-=ₛ $
    merid north ◃∙
    ap Susp-flip (merid y) ◃∎
      =ₛ₁⟨ 1 & 1 & SuspFlip.merid-β y ⟩
    merid north ◃∙
    ! (merid y) ◃∎
      =ₛ⟨ =ₛ-in {t = merid (Susp-flip y) ◃∙ ! (merid south) ◃∎} $
          Susp-elim
             {P = λ y → merid north ∙ ! (merid y) == merid (Susp-flip y) ∙ ! (merid south)}
             (!-inv-r (merid north) ∙ ! (!-inv-r (merid south)))
             idp
             (λ a → ↓-='-in-=ₛ $
               (!-inv-r (merid north) ∙ ! (!-inv-r (merid south))) ◃∙
               ap (λ z → merid (Susp-flip z) ∙ ! (merid south)) (merid a) ◃∎
                 =ₛ⟨ 0 & 1 & expand (!-inv-r (merid north) ◃∙ ! (!-inv-r (merid south)) ◃∎) ⟩
               !-inv-r (merid north) ◃∙
               ! (!-inv-r (merid south)) ◃∙
               ap (λ z → merid (Susp-flip z) ∙ ! (merid south)) (merid a) ◃∎
                 =ₛ₁⟨ 2 & 1 & ap-∘ (λ z' → merid z' ∙ ! (merid south)) Susp-flip (merid a) ⟩
               !-inv-r (merid north) ◃∙
               ! (!-inv-r (merid south)) ◃∙
               ap (λ z' → merid z' ∙ ! (merid south)) (ap Susp-flip (merid a)) ◃∎
                 =ₛ₁⟨ 2 & 1 & ap (ap (λ z' → merid z' ∙ ! (merid south)))
                                 (SuspFlip.merid-β a) ⟩
               !-inv-r (merid north) ◃∙
               ! (!-inv-r (merid south)) ◃∙
               ap (λ z' → merid z' ∙ ! (merid south)) (! (merid a)) ◃∎
                 =ₛ₁⟨ 2 & 1 & ap-∘ (_∙ ! (merid south)) merid (! (merid a)) ⟩
               !-inv-r (merid north) ◃∙
               ! (!-inv-r (merid south)) ◃∙
               ap (_∙ ! (merid south)) (ap merid (! (merid a))) ◃∎
                 =ₛ₁⟨ 2 & 1 & ap (ap (_∙ ! (merid south))) (ap-! merid (merid a)) ⟩
               !-inv-r (merid north) ◃∙
               ! (!-inv-r (merid south)) ◃∙
               ap (_∙ ! (merid south)) (! (ap merid (merid a))) ◃∎
                 =ₛ⟨ coh-helper (ap merid (merid a)) ⟩
               ap (λ q → merid north ∙ ! q) (ap merid (merid a)) ◃∎
                 =ₛ₁⟨ ∘-ap (λ q → merid north ∙ ! q) merid (merid a) ⟩
               ap (λ z → merid north ∙ ! (merid z)) (merid a) ◃∎
                 =ₛ⟨ 1 & 0 & contract ⟩
               ap (λ z → merid north ∙ ! (merid z)) (merid a) ◃∙ idp ◃∎ ∎ₛ)
             y ⟩
    merid (Susp-flip y) ◃∙
    ! (merid south) ◃∎
      =ₛ₁⟨ 0 & 1 & ! (SuspFmap.merid-β Susp-flip y) ⟩
    ap (Susp-fmap Susp-flip) (merid y) ◃∙
    ! (merid south) ◃∎ ∎ₛ
    where
      coh-helper : ∀ {j} {B : Type j}
        {b-north b-south : B}
        {merid₁ merid₂ : b-north == b-south}
        (p : merid₁ == merid₂)
        → !-inv-r merid₁ ◃∙
          ! (!-inv-r merid₂) ◃∙
          ap (_∙ ! merid₂) (! p) ◃∎
          =ₛ
          ap (λ q → merid₁ ∙ ! q) p ◃∎
      coh-helper {merid₁ = idp} {merid₂ = .idp} idp =
        =ₛ-in idp

  ⊙Susp-fmap-Susp-flip : ⊙Susp-fmap Susp-flip == ⊙Susp-flip (⊙Susp A)
  ⊙Susp-fmap-Susp-flip =
    ⊙λ=' Susp-fmap-flip (↓-idf=cst-in (! (!-inv-r (merid north))))

  ⊙Susp-fmap-maybe-Susp-flip : ∀ (b : Bool)
    → ⊙Susp-fmap (maybe-Susp-flip b) == ⊙maybe-Susp-flip (⊙Susp A) b
  ⊙Susp-fmap-maybe-Susp-flip true  = ⊙Susp-fmap-Susp-flip
  ⊙Susp-fmap-maybe-Susp-flip false = =⊙∘-out (⊙Susp-fmap-idf _)

⊙maybe-Susp-flip-natural : ∀ {i} {j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y) (b : Bool)
  → ⊙Susp-fmap (fst f) ⊙∘ ⊙maybe-Susp-flip X b ==
    ⊙maybe-Susp-flip Y b ⊙∘ ⊙Susp-fmap (fst f)
⊙maybe-Susp-flip-natural f true  = ! (⊙Susp-flip-natural f)
⊙maybe-Susp-flip-natural f false = ⊙λ= (⊙∘-unit-l (⊙Susp-fmap (fst f)))

module _ {i} (A : Type i) (m : ℕ₋₂) where

  Susp-Trunc-swap-Susp-flip :
    Susp-Trunc-swap A m ∘ Susp-flip ∼
    Trunc-fmap Susp-flip ∘ Susp-Trunc-swap A m
  Susp-Trunc-swap-Susp-flip =
    Susp-elim
      idp
      idp $
    Trunc-elim {{λ t → ↓-level (=-preserves-level Trunc-level)}} $ λ a →
    ↓-='-in' $
    ap (Trunc-fmap Susp-flip ∘ Susp-Trunc-swap A m) (merid [ a ])
      =⟨ ap-∘ (Trunc-fmap Susp-flip) (Susp-Trunc-swap A m) (merid [ a ]) ⟩
    ap (Trunc-fmap Susp-flip) (ap (Susp-Trunc-swap A m) (merid [ a ]))
      =⟨ ap (ap (Trunc-fmap Susp-flip)) (SuspTruncSwap.merid-β A m [ a ]) ⟩
    ap (Trunc-fmap Susp-flip) (ap [_] (merid a))
      =⟨ ∘-ap (Trunc-fmap Susp-flip) [_] (merid a) ⟩
    ap ([_] ∘ Susp-flip) (merid a)
      =⟨ ap-∘ [_] Susp-flip (merid a) ⟩
    ap [_] (ap Susp-flip (merid a))
      =⟨ ap (ap [_]) (SuspFlip.merid-β a) ⟩
    ap [_] (! (merid a))
      =⟨ ap-! [_] (merid a) ⟩
    ! (ap [_] (merid a))
      =⟨ ap ! (! (SuspTruncSwap.merid-β A m [ a ])) ⟩
    ! (ap (Susp-Trunc-swap A m) (merid [ a ]))
      =⟨ !-ap (Susp-Trunc-swap A m) (merid [ a ]) ⟩
    ap (Susp-Trunc-swap A m) (! (merid [ a ]))
      =⟨ ap (ap (Susp-Trunc-swap A m)) (! (SuspFlip.merid-β [ a ])) ⟩
    ap (Susp-Trunc-swap A m) (ap Susp-flip (merid [ a ]))
      =⟨ ∘-ap (Susp-Trunc-swap A m) Susp-flip (merid [ a ]) ⟩
    ap (Susp-Trunc-swap A m ∘ Susp-flip) (merid [ a ]) =∎

abstract
  ⊙Susp-Trunc-swap-⊙Susp-flip : ∀ {i} {X : Ptd i} (m : ℕ₋₂)
    → ⊙Susp-Trunc-swap (de⊙ X) m ◃⊙∘
      ⊙Susp-flip (⊙Trunc m X) ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙Susp-flip X) ◃⊙∘
      ⊙Susp-Trunc-swap (de⊙ X) m ◃⊙idf
  ⊙Susp-Trunc-swap-⊙Susp-flip {X = X} m =
    ⊙seq-λ= (Susp-Trunc-swap-Susp-flip (de⊙ X) m) $ !ₛ $
    idp ◃∙
    idp ◃∙
    ap [_] (! (merid (pt X))) ◃∎
      =ₛ⟨ 0 & 1 & expand [] ⟩
    idp ◃∙
    ap [_] (! (merid (pt X))) ◃∎
      =ₛ⟨ 0 & 1 & expand [] ⟩
    ap [_] (! (merid (pt X))) ◃∎
      =ₛ₁⟨ ap-! [_] (merid (pt X)) ⟩
    ! (ap [_] (merid (pt X))) ◃∎
      =ₛ₁⟨ ! $ ap ! $ SuspTruncSwap.merid-β (de⊙ X) m [ pt X ] ⟩
    ! (ap (Susp-Trunc-swap (de⊙ X) m) (merid [ pt X ])) ◃∎
      =ₛ₁⟨ !-ap (Susp-Trunc-swap (de⊙ X) m) (merid [ pt X ]) ⟩
    ap (Susp-Trunc-swap (de⊙ X) m) (! (merid [ pt X ])) ◃∎
      =ₛ⟨ 1 & 0 & contract ⟩
    ap (Susp-Trunc-swap (de⊙ X) m) (! (merid [ pt X ])) ◃∙
    idp ◃∎ ∎ₛ

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Oscar.Class.Congruity where

open import Oscar.Class.Extensionality
open import Oscar.Level

record Congruity {a} {A : Set a} {ℓ₁} (_≋₁_ : A → A → Set ℓ₁)
                 {b} {B : Set b} {ℓ₂} (_≋₂_ : B → B → Set ℓ₂)
       : Set (a ⊔ ℓ₁ ⊔ b ⊔ ℓ₂) where
  field
    congruity : ∀ (μ : A → B) {x y} → x ≋₁ y → μ x ≋₂ μ y

  instance ′extensionality : ∀ (μ : A → B) → Extensionality _≋₁_ (λ ⋆ → _≋₂_ ⋆) μ μ
  Extensionality.extensionality (′extensionality μ) = congruity μ

open Congruity ⦃ … ⦄ public -- hiding (′extensionality)


text:
-- 2014-07-27 Andreas, issue reported by phadei

module _ where

-- trait A { type T <: A }
record A (self : Set) (T : Set) : Set₁ where
  inductive
  field
    T⊂A : T → A T self

-- trait C extends A with B { type T <: C }
record C (self : Set) (T : Set) : Set₁ where
  inductive
  field
    a : A T self
    T⊂C : T → C T self

-- A with B { type T <: A with B { type T <: ... } }
record AB (self : Set) (T : Set) : Set₁ where
  field
    c : C T self

postulate
  Nat Bool : Set

-- Let's give Nat a A∧B trait, with T = Bool
Nat-AB : AB Nat Bool
Nat-AB = {!!}

-- WAS: Non-termination of type-checker (eta-expansion).

-- SHOULD BE: an unsolved meta.


text:
∙_ : Set₁ → Set₁
∙ X = X

Foo : Set
Foo = ∙ Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection

pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x

macro
  macaroo : Term → TC ⊤
  macaroo hole = unify hole (con (quote suc) (vArg unknown ∷ []))

test : Nat
test = macaroo

max_stars_repo_name: sseefried/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.RingAlgebras where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra

open import Cubical.Categories.Category

open Category
open AlgebraHoms

private
 variable
  ℓ ℓ' : Level

module _ (R : Ring ℓ) where
  AlgebrasCategory : Category (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
  ob AlgebrasCategory       = Algebra R _
  Hom[_,_] AlgebrasCategory = AlgebraHom
  id AlgebrasCategory {A}   = idAlgebraHom A
  _⋆_ AlgebrasCategory      = compAlgebraHom
  ⋆IdL AlgebrasCategory     = compIdAlgebraHom
  ⋆IdR AlgebrasCategory     = idCompAlgebraHom
  ⋆Assoc AlgebrasCategory   = compAssocAlgebraHom
  isSetHom AlgebrasCategory = isSetAlgebraHom _ _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Signature

module Program (Σ : Sig) (V : Set) where

open import Function
open import Data.Empty
open import Data.Unit
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Nat
open import Data.Fin
open import Data.List
open import Terms Σ

FinFam : Set → Set
FinFam X = ⨿ ℕ λ n → (Fin n → X)

dom : ∀{X} → FinFam X → Set
dom (n , _) = Fin n

get : ∀{X} (F : FinFam X) → dom F → X
get (_ , f) k = f k

domEmpty : ∀{X} → FinFam X → Set
domEmpty (zero  , _) = ⊤
domEmpty (suc _ , _) = ⊥

record Clause : Set where
  constructor _⊢_
  field
    body : FinFam (T V)
    head : T V
open Clause public

-- | A program consists of two finite sets of inductive and coinductive clauses.
Program : Set
Program = FinFam Clause × FinFam Clause

dom-μ : Program → Set
dom-μ = dom ∘ proj₁

dom-ν : Program → Set
dom-ν = dom ∘ proj₂

geth-μ : (P : Program) → dom-μ P → T V
geth-μ P = head ∘ get (proj₁ P)

getb-μ : (P : Program) → dom-μ P → FinFam (T V)
getb-μ P = body ∘ get (proj₁ P)

geth-ν : (P : Program) → dom-ν P → T V
geth-ν P = head ∘ get (proj₂ P)

getb-ν : (P : Program) → dom-ν P → FinFam (T V)
getb-ν P = body ∘ get (proj₂ P)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Andreas, 2017-04-24, issue #2552
-- Let bindings in top-level module telescope
-- make top-level interactive commands crash.

-- {-# OPTIONS -v interaction.top:20 #-}

open import Agda.Primitive

module _ (let foo = lzero) (A : Set) where

-- C-c C-n A

-- WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Interaction/BasicOps.hs:882

-- Should work now

-- Still problematic:

-- C-c C-n foo
-- Panic: unbound variable foo
-- when inferring the type of foo