Quantifiers and ⇔

The last stretch of core.alg is the quantifiers, ∀ and ∃. They follow the same build one / use one pattern as the connectives, with one twist: their rules carry a motive — a predicate T → Prop naming the property you’re quantifying. We’ll work over an abstract sort T and an abstract predicate P : T → Prop, so nothing is hidden.

For all: ∀

To prove ∀ x. P(x), prove P(x) for a fresh, arbitrary x. forall_intro hands you that eigenvariable — one premise, so then, and the then carries x into its context. The one property we can prove of every element with no assumptions is that it equals itself:

import core(forall_intro, refl);

sort T : Sort;

lemma everything_is_itself
  ⊢ ∀ (x : T) st x = x;
proof
  by forall_intro(T, _ = _) then x : T ⊢ x = x; by refl(T, x);
qed;

Here the motive _ = _ is the predicate λ (x : T) st x = x (that _ sugar from Induction and friends). Because x was introduced fresh, proving x = x for it counts as proving it for everyone.

To use a ∀, instantiate it at a specific term. forall_elim takes ∀ y. P(y) and a point a and yields P(a). This time the motive is the abstract P itself, and the universal fact is a lemma parameter:

import core(forall_elim);

sort T : Sort;

lemma at_a_point(P : T → Prop, a : T, all := ∀ (y : T) st P(y))
  ⊢ P(a);
proof
  by forall_elim(T, P, a)
  then all := ∀ (y : T) st P(y) ⊢ ∀ (y : T) st P(y);
  by all;
qed;

The third argument, a, is the point you’re instantiating at; the then goal is the universal statement you’re drawing it from, discharged by all. The then restates all because a continuation carries its whole context — Algae does no implicit weakening, so a dropped hypothesis is an error.

There exists: ∃

Building a ∃ means producing a witness. exists_intro takes a term a and a proof that the property holds of that term:

import core(exists_intro);

sort T : Sort;

lemma there_is_one(P : T → Prop, a : T, pa := P(a))
  ⊢ ∃ (x : T) st P(x);
proof
  by exists_intro(T, P, a) then pa := P(a) ⊢ P(a); by pa;
qed;

We offered a as the witness, so the leftover goal is the property at a — P(a) — which our assumption pa supplies.

Using a ∃ is the dual of using a ∨: you get a witness but you don’t get to know which one, so whatever you conclude must hold no matter who it is. exists_elim hands you a fresh x and the hypothesis witness := P(x) (named, as always, after the rule’s premise), and asks you to reach your goal from there — two premises, cases. To show it really gives you something usable, we unpack an existential and immediately repack it:

import core(exists_intro, exists_elim);

sort T : Sort;

lemma repack(P : T → Prop, ex := ∃ (x : T) st P(x))
  ⊢ ∃ (x : T) st P(x);
proof
  by exists_elim(T, P, ∃ (x : T) st P(x)) cases
    case ex := ∃ (x : T) st P(x) ⊢ ∃ (x : T) st P(x);
      by ex;
    qed;
    case ex := ∃ (x : T) st P(x), x : T, witness := P(x) ⊢ ∃ (x : T) st P(x);
      by exists_intro(T, P, x)
      then ex := ∃ (x : T) st P(x), x : T, witness := P(x) ⊢ P(x);
      by witness;
    qed;
  qed;
qed;

The second branch pulls out the witness x and the proof witness := P(x), then feeds them straight back into exists_intro. Trivial as a theorem, but it shows the exact shape every real exists_elim proof has.

Your turn

Combine the two moves: from ∀ y. P(y) — P holds everywhere — produce a proof that ∃ x. P(x).

import core(forall_elim, exists_intro);

sort T : Sort;

lemma somewhere(P : T → Prop, a : T, all := ∀ (y : T) st P(y))
  ⊢ ∃ (x : T) st P(x);
proof
  by wip(?goal);
wip;

Hint

Witness the existential at a first: by exists_intro(T, P, a) leaves P(a) to prove. Get it by instantiating the universal with forall_elim(T, P, a), whose then goal is ∀ (y : T) st P(y), closed by all. Carry all := ∀ (y : T) st P(y) in both then contexts.

If and only if: ⇔

A biconditional is just two implications bundled together, and its rules say exactly that. biconditional_intro asks for both directions — A ⇒ B and B ⇒ A — so two premises, cases, each closed by an assumed implication:

import core(biconditional_intro);

lemma equivalent(A B : Prop, fwd := A ⇒ B, bwd := B ⇒ A)
  ⊢ A ⇔ B;
proof
  by biconditional_intro(A, B) cases
    case fwd := A ⇒ B, bwd := B ⇒ A ⊢ A ⇒ B; by fwd; qed;
    case fwd := A ⇒ B, bwd := B ⇒ A ⊢ B ⇒ A; by bwd; qed;
  qed;
qed;

Going the other way, biconditional_elim_left extracts A ⇒ B from A ⇔ B (and biconditional_elim_right extracts B ⇒ A) — one premise each, so then. Between them you can take a ⇔ apart into whichever implication you need, then finish with implication_elim from The logical toolkit.

That’s all of core. Next we leave pure logic behind and start reasoning about data.