A proof of ∀ A, A∨¬A explained with continuation

wem.coq

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