Skip to content

Instantly share code, notes, and snippets.

Avatar

Andrej Bauer andrejbauer

View GitHub Profile
@andrejbauer
andrejbauer / AgdaSolver.agda
Last active Sep 14, 2022
How to use Agda ring solvers to prove equations?
View AgdaSolver.agda
{- Here is a short demonstration on how to use Agda's solvers that automatically
prove equations. It seems quite impossible to find complete worked examples
of how Agda solvers are used.
Thanks go to @anormalform who helped out with these on Twitter, see
https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng
I welcome improvements and additions to this file.
This file works with Agda 2.6.2.2 and standard-library-1.7.1
@andrejbauer
andrejbauer / Set2Bool.v
Created May 25, 2022
A proof in Coq that `Set -> bool` is not equal to `Set`.
View Set2Bool.v
Require Import Setoid.
Definition coerce {A B : Type} : A = B -> A -> B.
Proof.
intros [] a.
exact a.
Defined.
Lemma coerce_coerce {A B : Type} (e : A = B) (b : B) :
coerce e (coerce (eq_sym e) b) = b.
@andrejbauer
andrejbauer / Epimorphism.agda
Last active Jan 10, 2022
A setoid satisfies choice if, and only if its equivalence relation is equality.
View Epimorphism.agda
open import Level
open import Relation.Binary
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)
module Epimorphism where
@andrejbauer
andrejbauer / Queue.agda
Last active Sep 1, 2021
An implementation of infinite queues fashioned after the von Neuman ordinals
View Queue.agda
open import Data.Nat
open import Data.Maybe
open import Data.Product
-- An implementation of infinite queues fashioned after the von Neuman ordinals
module Queue where
infixl 5 _⊕_
@andrejbauer
andrejbauer / Primrec.agda
Created Jul 6, 2021
Primitive recursive functions in Agda
View Primrec.agda
open import Data.Nat
open import Data.Fin as Fin
module Primrec where
-- The datatype of primitive recursive function
data PR : (k : ℕ) Set where
pr-zero : PR 0 -- zero
pr-succ : PR 1 -- successor
pr-proj : {k} (i : Fin k) PR k -- projection
@andrejbauer
andrejbauer / Corey.agda
Created Jun 1, 2021
The type of bit streams is uncountable.
View Corey.agda
open import Data.Bool
open import Data.Empty
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality
module Corey where
-- streams of bits
record Stream : Set where
@andrejbauer
andrejbauer / finite.v
Created Feb 5, 2021
The finite truth values are precisely the decidable truth values.
View finite.v
(** Prop is a complete lattice. We can ask which propositions are finite. *)
Definition directed (D : Prop -> Prop) :=
(exists p , D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\ (q -> r).
(** A proposition p is finite when it has the following property:
for any directed D, if p ≤ sup D then there is q ∈ D such that p ≤ q. *)
Definition finite (p : Prop) :=
forall D, directed D ->
(p -> exists q, D q /\ q) -> exists q, D q /\ (p -> q).
@andrejbauer
andrejbauer / doubleNegationInitialAlgebra.agda
Created Jan 4, 2021
The initial algebra for the functor X ↦ (X → ∅) → ∅ is ∅.
View doubleNegationInitialAlgebra.agda
-- empty type
data 𝟘 : Set where
absurd : {A : Set} 𝟘 A
absurd ()
-- booleans
data 𝟚 : Set where
false true : 𝟚
@andrejbauer
andrejbauer / finite_subsets_and_LEM.v
Created Nov 15, 2020
The proof that excluded middle follows if all subsets of a singleton set are finite.
View finite_subsets_and_LEM.v
(* If all subsets of a singleton set are finite, then excluded middle holds.*)
Require Import List.
(* We present the subsets of X as characteristic maps S : X -> Prop.
Thus to say that x : X is an element of S : Powerset X we write S x. *)
Definition Powerset X := X -> Prop.
(* Auxiliary relation "l lists the elements of S". *)
Definition lists {X} (l : list X) (S : Powerset X) :=
forall x, S x <-> In x l.
@andrejbauer
andrejbauer / UniverseInjection.agda
Last active Feb 28, 2021
Formalization of the fact that a dependent type theory with excluded middle cannot have a universe Set such that Set → Set injects into Set.
View UniverseInjection.agda
-- Counterexample by Chung Kil Hur, improved by Andrej Bauer
-- We show that it is inconsistent to have an injection I : (Set → Set) → Set and excluded middle.
-- Indeed, excluded middle and I together give a surjection J : Set → (Set → Set),
-- which by Lawvere's fixed point theorem begets a fixed point operator on Set.
-- However, negation does not have a fixed point.
module cantor where
-- generalities