andrejbauer

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

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