andrejbauer

{- 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

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

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

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

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

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

(** 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

-- empty type
data 𝟘 : Set where

absurd : {A : Set} → 𝟘 → A
absurd ()

-- booleans
data 𝟚 : Set where
  false true : 𝟚

andrejbauer

(* 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

-- 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