View AgdaSolver.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- 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 |
View Set2Bool.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
View Epimorphism.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View Queue.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 _⊕_ |
View Primrec.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View Corey.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View finite.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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). |
View doubleNegationInitialAlgebra.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- empty type | |
data 𝟘 : Set where | |
absurd : {A : Set} → 𝟘 → A | |
absurd () | |
-- booleans | |
data 𝟚 : Set where | |
false true : 𝟚 |
View finite_subsets_and_LEM.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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. |
View UniverseInjection.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
NewerOlder