CODEWITHSUNDEEP
coqdependent-type
Max Heiber
Max Heiber

Reputation: 15492

Would giving up on 'ex falso' change anything w.r.t. dependently-typed programming in Coq?

Coq seems to assume ex falso quodlibet / the principle of explosion (PEP).

The induction principle generated from a data type definition with no constructors is PEP:

False_ind = 
fun (P : Prop) (f : False) => match f return P with
                              end
     : forall P : Prop, False -> P

This principal seems to be necessary for proving things like disjunctive syllogism:

Lemma disj_syll : forall (A B: Prop), A \/ B -> (not B) -> A.
Proof.
intros.
destruct H.
- (* prove A from A *) assumption.
- (* prove A from B and ~B *) contradiction.
Qed.

So that's what PEP buys us in terms of proving. But what about programming?

I can't figure out what it would mean to drop PEP and am really confused by the program extraction output.

As far as I can tell:

Scheme:

(load "macros_extr.scm")
(define __ (lambda (_) __))
(define disj_syll __)

Haskell:

module Disj_syll where
import qualified Prelude

__ :: any
__ = Prelude.error "Logical or arity value used"

disj_syll :: ()
disj_syll =  __

What is going on?

I'm asking this question because the connection between proofs and programs (Propositions-as-Types / Curry-Howard Isomorphism) seems well-understood for the logical connectives generally, but PEP is an axiom in Heyting and Kolmogorov's formalizations of intuitionistic logic (Kolmogorov and Brouwer on constructive implication and the Ex Falso rule, Van Dalen 2004). It's hard for me to see what the computational content of such an axiom is, especially when it says "Given that you have constructed the unconstructable, you now get (for free!) a construction of anything you choose to imagine)." I don't know how to write a program to do such a thing, and Coq's program extraction doesn't seem to have a consistent perspective on the matter either.

Upvotes: 0

Views: 385

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

Would giving up on 'ex falso' change anything w.r.t. dependently-typed programming in Coq?

Yes, it would. Let us consider the hello-world of dependently typed programming, namely length-indexed lists (a.k.a. vectors). It is defined in the standard library, but let me give it here for context.

Inductive vec (A : Type) : nat -> Type :=
  | vnil : vec A 0
  | vcons n : A -> vec A n -> vec A (S n).

Now, we might want to provide the analogue of the head function on regular (non-indexed) lists. There is many approaches to deal with the case of the empty list as the input of head for lists. But for vectors it is especially easy to ask for non-empty input: we put this restriction in the type of the input v : vec A (S n), where S n ensures that the length of the input vector is not zero.

Here is a stub for this function:

Fixpoint head {A n} (v : vec A (S n)) : A :=
  match v with
  | vnil _ => _
  | vcons _ n hd tl => hd
  end.

But what do we return in case of the empty input? Coq won't let us simply omit vnil constructor in the pattern-matching expression. Here we can use the principle of explosion to solve the issue. Here is one possible way to fill in the blank above:

Fixpoint head {A n} (v : vec A (S n)) : A :=
  match v in vec _ len
        return (len = S n -> A)
  with
  | vnil _ => fun contra => False_rect _ (O_S _ contra)
  | vcons _ n hd tl => fun _ => hd
  end eq_refl.

This solution uses the so-called "convoy pattern" which is described in several Stackoverflow answers and in the CPDT book by Adam Chlipala. It also uses the standard O_S lemma (of type forall n : nat, 0 <> S n), so (O_S _ contra) has type type False.

Upvotes: 3

perthmad
perthmad

Reputation: 291

The standard computational interpretation for PEP is just the program crashing, since it requires a logically impossible premise. In the Scheme code, crashing is represented by the program looping, and in Haskell, this is a toplevel exception. But in both cases we know this is dead code and should never be reached, except if Coq is inconsistent itself.

Note that Coq is consistent with alternative computational interpretations of PEP, though. One can apply a variant of Friedman's A-translation to Coq to replace crashing by raising recoverable exceptions. See the Exceptional model for more details.

Upvotes: 3

Related Questions