Created
January 2, 2016 20:49
-
-
Save aspiwack/ffbe713c062a9a413e9e to your computer and use it in GitHub Desktop.
A proof of ∀ A, A∨¬A explained with continuation
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
(** To give a direct proof of the constructive result that [forall | |
A:Prop, ~~(A\/~A)], it is useful to see [~A] as meaning a | |
"continuation of [A]". That is, [~A] is a computation that takes an | |
[A] and "returns".*) | |
(** Here is a first proof by forward chaining. *) | |
Lemma Proof₁ : forall A:Prop, ~~(A\/~A). | |
Proof. | |
intros A k₀. | |
(** We have [k₀:~(A\/~A)]. That is [k₀] is a continuation of either | |
an [A] or a [~A]. The conclusion is [False], i.e. unreachable, | |
so we must build a computation that returns. *) | |
pose proof ((fun x:A => k₀ (or_introl x)) : ~A) as k₁. | |
(** In other words, [k₀] is both a continuation [k₁] of [A]. *) | |
pose proof ((fun k:~A => k₀ (or_intror k)) : ~~A) as k₂. | |
(** And a continuation [k₂] of [~A]: a continuation of a | |
continuation of [A]. *) | |
exact (k₂ k₁). | |
(** Since [k₁:~A] and [k₂] returns on a [~A], we can return. *) | |
Qed. | |
(** Here is a backward chaining version of the same proof. *) | |
Lemma Proof₂ : forall A:Prop, ~~(A\/~A). | |
Proof. | |
intros A k₀. | |
(** We have [k₀:~(A\/~A)]. That is [k₀] is a continuation of either | |
an [A] or a [~A]. The conclusion is [False], i.e. unreachable, | |
so we must build a computation that returns. *) | |
apply k₀. right. | |
(** The only way to return is to use [k₀], so we must provide an | |
[A\/~A]. We have no [A] available, but we have computations, so | |
we shall provide a [~A]. *) | |
intros x. | |
(** In other word, a computation that returns from an [x:A]. *) | |
apply k₀. left. | |
(** The only way to return is to use [k₀], so we must provide an | |
[A\/~A]. We have now have an [A] available, so we shall provide | |
an [A]. *) | |
exact x. | |
(** [x:A]. *) | |
Qed. | |
(** The forward chaining [Proof₂] contains β-redexes. *) | |
Print Proof₁. | |
(* Proof₁ = | |
fun (A : Prop) (k₀ : ~ (A \/ ~ A)) => | |
(fun k₁ : ~ A => | |
(fun k₂ : ~ ~ A => k₂ k₁) ((fun k : ~ A => k₀ (or_intror k)):~ ~ A)) | |
((fun x : A => k₀ (or_introl x)):~ A) | |
: forall A : Prop, ~ ~ (A \/ ~ A) *) | |
(** By reducing these β-redexes we can obtain a simple, concise proof | |
term for [forall A, ~~(A\/~A)], which may look more confortable to | |
someone well-versed in the arcanas of [call/cc] and similar | |
programming constructs. *) | |
Lemma Proof₁' : forall A, ~~(A\/~A). | |
Proof. | |
exact (fun A k₀ => k₀ (or_intror (fun x:A => k₀ (or_introl x)))). | |
Qed. | |
(** [Proof₁'] is, incidentally, the same proof term as [Proof₂]. *) | |
Print Proof₂. | |
(* Proof₂ = | |
fun (A : Prop) (k₀ : ~ (A \/ ~ A)) => | |
k₀ (or_intror (fun x : A => k₀ (or_introl x))) | |
: forall A : Prop, ~ ~ (A \/ ~ A) *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment