Proving that if an element normalizes in at most n steps then it normalizes in at most (n+1) steps.

Of course, the above is trivial IRL. However, if "at most n steps" is formalized indirectly in Coq, the proof can be nontrivial.


Module Termination.


Parameter T : Set.


Parameter R : T -> T -> Prop.


Fixpoint terminates (n : nat) (gamma : T) : Prop :=
  match n with
    | O => False
    | S n' =>
      forall gamma' : T,
        (R gamma gamma' -> terminates n' gamma')
  end.

The proposition "terminates n gamma" means that gamma reduces to a normal form in at most (n-1) steps. The "at most" part of the definition is very implicit in the way the second case is written. Proving that this is actually the case:

Theorem terminates_monotone : forall n gamma,

  terminates n gamma -> terminates (S n) gamma.

i.e. that if gamma normalizes in at most (n-1) steps then it normalizes in at most n steps, is not trivial and it shows why it pays to think about a proof before jumping into it. Here is the proof I came up with:

  induction n.

  inversion 1.

  intros.

  simpl.

  intros.

  simpl in H.

  specialize (H gamma' H0).

  specialize (IHn gamma' H).

  simpl in IHn.

  specialize (IHn gamma'0 H1).

  assumption.

Qed.

End Termination.

after some scribbling on paper. As an open question, how can we make the proof more automatic by making use of Ltac? The "intelligent" parts of the proof seem to be the choice of "n" as an induction parameter and the specializations of the different hypothesis, so these would probably need to be kept (or brute-forced).

COQ: Proving the duality between forall and exists

I recently needed to prove the following theorem in Coq:

Module ForallExists.

Theorem forall_exists : forall D, forall P : D -> Prop,

~ (forall x : D, P x) <-> (exists x : D, ~ P x).

That is, if a property does not hold for all of the elements, then there must be an element for which the property does not hold. I don't think this is provable in Coq without classical reasoning (if I'm wrong, please correct me).

So I added classical reasoning:

Require Import Classical.

and then I went on to construct its proof:

1 subgoal

============================

forall (D : Type) (P : D -> Prop),

~ (forall x : D, P x) <-> (exists x : D, ~ P x)

The first thing I did was to split the equivalence proof into proofs of the two implications:

split.

2 subgoals

D : Type

P : D -> Prop

============================

~ (forall x : D, P x) -> exists x : D, ~ P x

subgoal 2 is:

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

The first implication is the one which requires classical reasoning. After introducing the antecedent into the hypothesis:

intro.

2 subgoals

D : Type

P : D -> Prop

H : ~ (forall x : D, P x)

============================

exists x : D, ~ P x

subgoal 2 is:

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

we want to continue by contradiction on whether such an x really exists. This is called Peirce's law

Check Peirce.

Peirce

: forall P : Prop, ((P -> False) -> P) -> P

and it comes with the Classical module. That is, if we can prove that the negation ~P of P (~P is shorthand for P -> False) implies P, then we can deduce P.

apply Peirce.

intros.

2 subgoals

D : Type

P : D -> Prop

H : ~ (forall x : D, P x)

H0 : (exists x : D, ~ P x) -> False

============================

exists x : D, ~ P x

subgoal 2 is:

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

As H and H0 are contradictory, we will continue by proving False using H.

exfalso.

apply H.

intros.

2 subgoals

D : Type

P : D -> Prop

H : ~ (forall x : D, P x)

H0 : (exists x : D, ~ P x) -> False

x : D

============================

P x

subgoal 2 is:

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

That is, it remains to be shown that P x holds (for arbitrary x). Again we reason using Peirce's law.

apply Peirce.

intros.

2 subgoals

D : Type

P : D -> Prop

H : ~ (forall x : D, P x)

H0 : (exists x : D, ~ P x) -> False

x : D

H1 : P x -> False

============================

P x

subgoal 2 is:

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

As H0 and H1 are contradictory, we change the goal with False and prove the contradiction.

exfalso.

apply H0.

2 subgoals

D : Type

P : D -> Prop

H : ~ (forall x : D, P x)

H0 : (exists x : D, ~ P x) -> False

x : D

H1 : P x -> False

============================

exists x0 : D, ~ P x0

subgoal 2 is:

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

The required x0 is easy to produce (it is sufficient to use x).

exists x.

assumption.

1 subgoal

D : Type

P : D -> Prop

============================

(exists x : D, ~ P x) -> ~ (forall x : D, P x)

and we are left with the second implication. This one is easier and we do not need classical reasoning for it.

intros.

unfold not.

intros.

1 subgoal

D : Type

P : D -> Prop

H : exists x : D, ~ P x

H0 : forall x : D, P x

============================

False

We first introduce everything into the hypothesis and next we produce a witness for H:

elim H.

intros.

1 subgoal

D : Type

P : D -> Prop

H : exists x : D, ~ P x

H0 : forall x : D, P x

x : D

H1 : ~ P x

============================

False

The rest is routine, as it is easy to derive the contradiction.

assert (P x).

apply H0.

contradiction.

Proof completed.

Qed.

End ForallExists.