Reasoning from false

STELF’s coverage checker often rules out contradictory cases for you (see, for example, the proof of determinacy for the simply typed λ-calculus). However, you will sometimes need to reason from contradictory assumptions yourself. You can do this by declaring an uninhabited type, proving that certain assumptions are contradictory, and then writing lemmas that conclude anything from a term of the uninhabited type.

The uninhabited type

%sort uninhabited %.
%freeze uninhabited %.

Freezing the intentionally uninhabited type (which is also sometimes called void, false, or absurd) is not strictly necessary, but it clarifies the programmer’s intent—STELF will signal an error if any later part of the signature introduces a term of this type.

Proving contradictions

We use some simple judgements on natural numbers to illustrate proving contradictions.

%sort nat %.
%term nat/z nat %.
%term nat/s %pi nat %-> nat %.
%sort nat-less {_ nat} {_ nat} %.
%term nat-less/z nat-less nat/z (nat/s N) %.
%term nat-less/s %pi (nat-less (nat/s N1) (nat/s N2)) %<- (nat-less N1 N2) %.
%sort nat-plus {_ nat} {_ nat} {_ nat} %.
%term nat-plus/z nat-plus nat/z N N %.
%term nat-plus/s %pi (nat-plus (nat/s N1) N2 (nat/s N3)) %<- (nat-plus N1 N2 N3) %.

Contradiction by coverage checking

First, we prove that no number is less than zero:

(options removed from twelftag: check=“true”)

%sort nat-less-z-uninhabited {_ nat-less N nat/z} {_ uninhabited} %.
%mode nat-less-z-uninhabited %in %out %.
%worlds () (nat-less-z-uninhabited _ _) %.
%total {} (nat-less-z-uninhabited _ _) %.

The coverage checker accepts this proof without any cases because there are no rules for deriving nat-less _ nat/z. This is the simplest way to create a contradiction.

Inductive contradictions

Some contradictions require an inductive argument. For example, we can prove that if N1 < N2 then there is no N3 such that N2 + N3 = N1.

(options removed from twelftag: check=“true”)

%sort nat-less-plus-uninhabited {_ nat-less N1 N2} {_ nat-plus N2 N3 N1} {_ uninhabited} %.
%mode nat-less-plus-uninhabited %in %in %out %.
%term _
  %pi (nat-less-plus-uninhabited (nat-less/s NL) (nat-plus/s NP) DU)
  %<- (nat-less-plus-uninhabited NL NP DU) %.
%worlds () (nat-less-plus-uninhabited _ _ _) %.
%total (D1) (nat-less-plus-uninhabited D1 _ _) %.

In this theorem, the coverage checker rules out all cases but the one where the first input is of the form

nat-less N1 N2 ------------------------------nat-less/s nat-less (nat/s N1) (nat/s N2)

and the second input is of the form

nat-plus N2 N3 N1 ----------------------------------nat-plus/s nat-plus (nat/s N2) N3 (nat/s N1)

To show that this remaining case is contradictory. we apply the inductive hypothesis on the subderivations to derive uninhabited, and then return the resulting derivation of uninhabited to meet our proof obligations.

With this theorem, the coverage checker rules out all the base cases, so we are able to return a term of type uninhabited in the one remaining case by writing a loop.

Reasoning from contradiction

Once you have a contradiction, it is easy to write a lemma that reasons from it. For example, from uninhabited we can conclude that any two numbers are nat-less:

(options removed from twelftag: check=“true”)

%sort uninhabited-nat-less {N1 nat} {N2 nat} {_ uninhabited} {_ nat-less N1 N2} %.
%mode uninhabited-nat-less %in %in %in %out %.
%worlds () (uninhabited-nat-less _ _ _ _) %.
%total {} (uninhabited-nat-less _ _ _ _) %.

This proof requires no cases because any case would involve a canonical form of type uninhabited.

This lemma could be used in a proof that requires coming up with a derivation of some less-than fact in contradictory circumstances.

For an example where reasoning from contradiction is necessary, see the tutorial on hereditary substitution for the STLC.