Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Proving False with negative inductive types in Coq

The third chapter of CPDT briefly discusses why negative inductive types are forbidden in Coq. If we had

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

then we could easily define a function

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

so that the term uhoh (Abs uhoh) would be non-terminating, with which "we would be able to prove every theorem".

I understand the non-termination part, but I don't get how we can prove anything with it. How would one prove False using term as defined above?

like image 393
user287393 Avatar asked Jul 05 '15 01:07

user287393


1 Answers

Reading your question made me realize that I didn't quite understand Adam's argument either. But inconsistency in this case results quite easily from Cantor's usual diagonal argument (a never-ending source of paradoxes and puzzles in logic). Consider the following assumptions:

Section Diag.

Variable T : Type.

Variable test : T -> bool.

Variables x y : T.

Hypothesis xT : test x = true.
Hypothesis yF : test y = false.

Variable g : (T -> T) -> T.
Variable g_inv : T -> (T -> T).

Hypothesis gK : forall f, g_inv (g f) = f.

Definition kaboom (t : T) : T :=
  if test (g_inv t t) then y else x.

Lemma kaboom1 : forall t, kaboom t <> g_inv t t.
Proof.
  intros t H.
  unfold kaboom in H.
  destruct (test (g_inv t t)) eqn:E; congruence.
Qed.

Lemma kaboom2 : False.
Proof.
  assert (H := @kaboom1 (g kaboom)).
  rewrite -> gK in H.
  congruence.
Qed.

End Diag.

This is a generic development that could be instantiated with the term type defined in CPDT: T would be term, x and y would be two elements of term that we can test discriminate between (e.g. App (Abs id) (Abs id) and Abs id). The key point is the last assumption: we assume that we have an invertible function g : (T -> T) -> T which, in your example, would be Abs. Using that function, we play the usual diagonalization trick: we define a function kaboom that is by construction different from every function T -> T, including itself. The contradiction results from that.

like image 165
Arthur Azevedo De Amorim Avatar answered Oct 16 '22 10:10

Arthur Azevedo De Amorim