Skip to content

Instantly share code, notes, and snippets.

View andrejbauer's full-sized avatar

Andrej Bauer andrejbauer

View GitHub Profile
andrejbauer / LaTeX.inputplugin
Last active April 24, 2024 12:59
LaTeX symbols input method for MacOS
ENCODE: Unicode
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
alpha α
andrejbauer / MPimpliesPost.v
Created December 3, 2023 09:26
Markov's principle implies Post's theorem, constructively.
(* Post's theorem in computability theory states that a subset S ⊆ ℕ is
decidable if both S and its complement ℕ \ S are semidecidable.
Just how much classical logic is needed to prove the theorem, though?
In this note we show that Markov's principle suffices.
Rather than working with subsets of ℕ we work synthetically, with
semidecidable and decidable truth values. (This is more general than
the traditional Post's theorem.)
andrejbauer / ZF.v
Created November 8, 2023 00:56
Minimalist formalization of first-order signatures, logic, theories and models. As an example, we formalize a small fragment of ZF set theory.
A formalization of first-order logic, theories and their models.
As an example we formalize the language of ZF set theory and a a small fragment of ZF.
(* A signature is given by function symbols, relation symbols, and their arities. *)
Structure Signature :=
{ funSym : Type (* names of function symbols *)
; funArity : funSym -> Type (* arities of function symbols *)
; relSym : Type (* names of relation symbols *)
andrejbauer / example.agda
Last active April 20, 2023 08:30
Inductive trees in various proof assistants
open import Data.Nat
open import Data.Product
module example where
data SimpleTree (A : Set) : Set where
empty : SimpleTree A
leaf : A -> SimpleTree A
node : A -> SimpleTree A -> SimpleTree A -> SimpleTree A
andrejbauer / wlem.agda
Last active June 19, 2023 04:40
A formal proof that weak excluded middle holds from the familiar facts about real numbers.
Weak excluded middle states that for every propostiion P, either ¬¬P or ¬P holds.
We give a proof of weak excluded middle, relying just on basic facts about real numbers,
which we carefully state, in order to make the dependence on them transparent.
Some people might doubt the formalization. To convince yourself that there is no cheating, you should:
* Carefully read the facts listed in the RealFacts below to see that these are all
just familiar facts about the real numbers.
andrejbauer / AgdaSolver.agda
Last active April 22, 2024 18:20
How to use Agda ring solvers to prove equations?
{- 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
I welcome improvements and additions to this file.
This file works with Agda and standard-library-1.7.1
andrejbauer / Set2Bool.v
Created May 25, 2022 22:08
A proof in Coq that `Set -> bool` is not equal to `Set`.
Require Import Setoid.
Definition coerce {A B : Type} : A = B -> A -> B.
intros [] a.
exact a.
Lemma coerce_coerce {A B : Type} (e : A = B) (b : B) :
coerce e (coerce (eq_sym e) b) = b.
andrejbauer / Epimorphism.agda
Last active January 26, 2023 20:44
A setoid satisfies choice if, and only if its equivalence relation is equality.
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 / Queue.agda
Last active September 1, 2021 23:23
An implementation of infinite queues fashioned after the von Neuman ordinals
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 / Primrec.agda
Created July 6, 2021 10:21
Primitive recursive functions in 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