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

0
votes

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:

  • the extractions are the same for all proofs that rely on PEP, including the one above
  • the extractions for Scheme and Haskell seem to do completely different things

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.

2
coqdependent-type
Your question regarding extraction is ill-posed. Coq's extraction assumes a non-informative Prop, so any type that lives in Prop gets extracted to something akin to the unit type. In particular, your lemma disj_syll gets extracted to the unit value. (Because of cumulativity, this value looks like a recursive function in Scheme and OCaml, but it is still meant to be understood as a singleton.) As a consequence, you are not exercising the extraction of PEP, you are just seeing how Coq's extraction encodes non-informative types. - Guillaume Melquiond
Thanks!! That was a silly mistake. Now I'm trying to re-do the example in Set using parallel definitions of or and False and (after 5 minutes) I haven't been able to prove disjuntive syllogism. - Max Heiber
The proof should be exactly the same as in the Prop case: Lemma disj_syll A B : or' A B -> (B -> false') -> A. Proof. intros [J|J] K. easy. contradiction. Defined. - Guillaume Melquiond

2 Answers

3
votes

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.

3
votes

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.