comparison src/Universes.v @ 230:9dbcd6bad488

Axioms
author Adam Chlipala <adamc@hcoop.net>
date Mon, 23 Nov 2009 11:33:22 -0500
parents 2bb1642f597c
children bc0f515a929f
comparison
equal deleted inserted replaced
229:2bb1642f597c 230:9dbcd6bad488
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import DepList. 11 Require Import DepList Tactics.
12 12
13 Set Implicit Arguments. 13 Set Implicit Arguments.
14 (* end hide *) 14 (* end hide *)
15 15
16 16
339 is not allowed on a predicate in sort Type 339 is not allowed on a predicate in sort Type
340 because proofs can be eliminated only to build proofs. 340 because proofs can be eliminated only to build proofs.
341 341
342 ]] 342 ]]
343 343
344 In formal Coq parlance, "elimination" means "pattern-matching." The typing rules of Gallina forbid us from pattern-matching on a discriminee whose types belongs to [Prop], whenever the result type of the [match] has a type besides [Prop]. This is a sort of "information flow" policy, where the type system ensures that the details of proofs can never have any effect on parts of a development that are not also marked as proofs. 344 In formal Coq parlance, "elimination" means "pattern-matching." The typing rules of Gallina forbid us from pattern-matching on a discriminee whose type belongs to [Prop], whenever the result type of the [match] has a type besides [Prop]. This is a sort of "information flow" policy, where the type system ensures that the details of proofs can never have any effect on parts of a development that are not also marked as proofs.
345 345
346 This restriction matches informal practice. We think of programs and proofs as clearly separated, and, outside of constructive logic, the idea of computing with proofs is ill-formed. The distinction also has practical importance in Coq, where it affects the behavior of extraction. 346 This restriction matches informal practice. We think of programs and proofs as clearly separated, and, outside of constructive logic, the idea of computing with proofs is ill-formed. The distinction also has practical importance in Coq, where it affects the behavior of extraction.
347 347
348 Recall that extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction %\textit{%#<i>#erases#</i>#%}% proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *) 348 Recall that extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction %\textit{%#<i>#erases#</i>#%}% proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *)
349 349
388 forall P Q : Prop, P \/ Q -> Q \/ P 388 forall P Q : Prop, P \/ Q -> Q \/ P
389 : Prop 389 : Prop
390 390
391 ]] 391 ]]
392 392
393 We see that it is possible to define a [Prop] that quantifies over other [Prop]s. This is fortunate, as we start wanting that ability even for such basic purposes as stating propositional tautologies. In the next section of this chapter, we will see some reasons why unrestricted impredicativity is undesirable. The impredicativity of [Prop] interacts crucially with the elimination restriction to avoid those pitfalls. *) 393 We see that it is possible to define a [Prop] that quantifies over other [Prop]s. This is fortunate, as we start wanting that ability even for such basic purposes as stating propositional tautologies. In the next section of this chapter, we will see some reasons why unrestricted impredicativity is undesirable. The impredicativity of [Prop] interacts crucially with the elimination restriction to avoid those pitfalls.
394
395 Impredicativity also allows us to implement a version of our earlier [exp] type that does not suffer from the weakness that we found. *)
396
397 Inductive expP : Type -> Prop :=
398 | ConstP : forall T, T -> expP T
399 | PairP : forall T1 T2, expP T1 -> expP T2 -> expP (T1 * T2)
400 | EqP : forall T, expP T -> expP T -> expP bool.
401
402 Check ConstP 0.
403 (** %\vspace{-.15in}% [[
404 ConstP 0
405 : expP nat
406 ]] *)
407
408 Check PairP (ConstP 0) (ConstP tt).
409 (** %\vspace{-.15in}% [[
410 PairP (ConstP 0) (ConstP tt)
411 : expP (nat * unit)
412 ]] *)
413
414 Check EqP (ConstP Set) (ConstP Type).
415 (** %\vspace{-.15in}% [[
416 EqP (ConstP Set) (ConstP Type)
417 : expP bool
418 ]] *)
419
420 Check ConstP (ConstP O).
421 (** %\vspace{-.15in}% [[
422 ConstP (ConstP 0)
423 : expP (expP nat)
424
425 ]]
426
427 In this case, our victory is really a shallow one. As we have marked [expP] as a family of proofs, we cannot deconstruct our expressions in the usual programmatic ways, which makes them almost useless for the usual purposes. Impredicative quantification is much more useful in defining inductive families that we really think of as judgments. For instance, this code defines a notion of equality that is strictly stronger than the base equality [=]. *)
428
429 Inductive eqPlus : forall T, T -> T -> Prop :=
430 | Base : forall T (x : T), eqPlus x x
431 | Func : forall dom ran (f1 f2 : dom -> ran),
432 (forall x : dom, eqPlus (f1 x) (f2 x))
433 -> eqPlus f1 f2.
434
435 Check (Base 0).
436 (** %\vspace{-.15in}% [[
437 Base 0
438 : eqPlus 0 0
439 ]] *)
440
441 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)).
442 (** %\vspace{-.15in}% [[
443 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n)
444 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n)
445 ]] *)
446
447 Check (Base (Base 1)).
448 (** %\vspace{-.15in}% [[
449 Base (Base 1)
450 : eqPlus (Base 1) (Base 1)
451 ]] *)
452
453
454 (** * Axioms *)
455
456 (** While the specific logic Gallina is hardcoded into Coq's implementation, it is possible to add certain logical rules in a controlled way. In other words, Coq may be used to reason about many different refinements of Gallina where strictly more theorems are provable. We achieve this by asserting %\textit{%#<i>#axioms#</i>#%}% without proof.
457
458 We will motivate the idea by touring through some standard axioms, as enumerated in Coq's online FAQ. I will add additional commentary as appropriate. *)
459
460 (** ** The Basics *)
461
462 (* One simple example of a useful axiom is the law of the excluded middle. *)
463
464 Require Import Classical_Prop.
465 Print classic.
466 (** %\vspace{-.15in}% [[
467 *** [ classic : forall P : Prop, P \/ ~ P ]
468
469 ]]
470
471 In the implementation of module [Classical_Prop], this axiom was defined with the command *)
472
473 Axiom classic : forall P : Prop, P \/ ~ P.
474
475 (** An [Axiom] may be declared with any type, in any of the universes. There is a synonym [Parameter] for [Axiom], and that synonym is often clearer for assertions not of type [Prop]. For instance, we can assert the existence of objects with certain properties. *)
476
477 Parameter n : nat.
478 Axiom positive : n > 0.
479 Reset n.
480
481 (** This kind of "axiomatic presentation" of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming.
482
483 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
484
485 Axiom not_classic : exists P : Prop, ~ (P \/ ~ P).
486
487 Theorem uhoh : False.
488 generalize classic not_classic; firstorder.
489 Qed.
490
491 Theorem uhoh_again : 1 + 1 = 3.
492 destruct uhoh.
493 Qed.
494
495 Reset not_classic.
496
497 (** On the subject of the law of the excluded middle itself, this axiom is usually quite harmless, and many practical Coq developments assume it. It has been proved metatheoretically to be consistent with CIC. Here, "proved metatheoretically" means that someone proved on paper that excluded middle holds in a %\textit{%#<i>#model#</i>#%}% of CIC in set theory. All of the other axioms that we will survey in this section hold in the same model, so they are all consistent together.
498
499 Recall that Coq implements %\textit{%#<i>#constructive#</i>#%}% logic by default, where excluded middle is not provable. Proofs in constructive logic can be thought of as programs. A [forall] quantifier denotes a dependent function type, and a disjunction denotes a variant type. In such a setting, excluded middle could be interpreted as a decision procedure for arbitrary propositions, which computability theory tells us cannot exist. Thus, constructive logic with excluded middle can no longer be associated with our usual notion of programming.
500
501 Given all this, why is it all right to assert excluded middle as an axiom? I do not want to go into the technical details, but the intuitive justification is that the elimination restriction for [Prop] prevents us from treating proofs as programs. An excluded middle axiom that quantified over [Set] instead of [Prop] %\textit{%#<i>#would#</i>#%}% be problematic. If a development used that axiom, we would not be able to extract the code to OCaml (soundly) without implementing a genuine universal decision procedure. In contrast, values whose types belong to [Prop] are always erased by extraction, so we sidestep the axiom's algorithmic consequences.
502
503 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on. *)
504
505 Theorem t1 : forall P : Prop, P -> ~ ~ P.
506 tauto.
507 Qed.
508
509 Print Assumptions t1.
510 (** %\vspace{-.15in}% [[
511 Closed under the global context
512 ]] *)
513
514 Theorem t2 : forall P : Prop, ~ ~ P -> P.
515 (** [[
516 tauto.
517
518 Error: tauto failed.
519
520 ]] *)
521
522 intro P; destruct (classic P); tauto.
523 Qed.
524
525 Print Assumptions t2.
526 (** %\vspace{-.15in}% [[
527 Axioms:
528 classic : forall P : Prop, P \/ ~ P
529
530 ]]
531
532 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable propositions. *)
533
534 Theorem classic_nat_eq : forall n m : nat, n = m \/ n <> m.
535 induction n; destruct m; intuition; generalize (IHn m); intuition.
536 Qed.
537
538 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m.
539 intros n m; destruct (classic_nat_eq n m); tauto.
540 Qed.
541
542 Print Assumptions t2'.
543 (** %\vspace{-.15in}% [[
544 Closed under the global context
545 ]]
546
547 %\bigskip%
548
549 Mainstream mathematical practice assumes excluded middle, so it can be useful to have it available in Coq developments, though it is also nice to know that a theorem is proved in a simpler formal system than classical logic. There is a similar story for %\textit{%#<i>#proof irrelevance#</i>#%}%, which simplifies proof issues that would not even arise in mainstream math. *)
550
551 Require Import ProofIrrelevance.
552 Print proof_irrelevance.
553 (** %\vspace{-.15in}% [[
554 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
555
556 ]]
557
558 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, without this axiom, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 6. *)
559
560 (* begin hide *)
561 Lemma zgtz : 0 > 0 -> False.
562 crush.
563 Qed.
564 (* end hide *)
565
566 Definition pred_strong1 (n : nat) : n > 0 -> nat :=
567 match n with
568 | O => fun pf : 0 > 0 => match zgtz pf with end
569 | S n' => fun _ => n'
570 end.
571
572 (** We might want to prove that different proofs of [n > 0] do not lead to different results from our richly-typed predecessor function. *)
573
574 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
575 destruct n; crush.
576 Qed.
577
578 (** The proof script is simple, but it involved peeking into the definition of [pred_strong1]. For more complicated function definitions, it can be considerably more work to prove that they do not discriminate on details of proof arguments. This can seem like a shame, since the [Prop] elimination restriction makes it impossible to write any function that does otherwise. Unfortunately, this fact is only true metatheoretically, unless we assert an axiom like [proof_irrelevance]. With that axiom, we can prove our theorem without consulting the definition of [pred_strong1]. *)
579
580 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
581 intros; f_equal; apply proof_irrelevance.
582 Qed.
583
584
585 (** %\bigskip%
586
587 In the chapter on equality, we already discussed some axioms that are related to proof irrelevance. In particular, Coq's standard library includes this axiom: *)
588
589 Require Import Eqdep.
590 Import Eq_rect_eq.
591 Print eq_rect_eq.
592 (** %\vspace{-.15in}% [[
593 *** [ eq_rect_eq :
594 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
595 x = eq_rect p Q x p h ]
596
597 ]]
598
599 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. *)
600
601 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x.
602 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [
603 symmetry; apply eq_rect_eq
604 | exact (match pf as pf' return match pf' in _ = y return x = y with
605 | refl_equal => refl_equal x
606 end = pf' with
607 | refl_equal => refl_equal _
608 end) ].
609 Qed.
610
611 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
612 intros; generalize pf1 pf2; subst; intros;
613 match goal with
614 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
615 end.
616 Qed.
617
618 (** These corollaries are special cases of proof irrelevance. Many developments only need proof irrelevance for equality, so there is no need to assert full irrelevance for them.
619
620 Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions. For instance, [UIP] is provable whenever the type [A] has a decidable equality operation. The module [Eqdep_dec] of the standard library contains a proof. A similar phenomenon applies to other notable cases, including less-than proofs. Thus, it is often possible to use proof irrelevance without asserting axioms.
621
622 %\bigskip%
623
624 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *)
625
626 Require Import FunctionalExtensionality.
627 Print functional_extensionality_dep.
628 (** %\vspace{-.15in}% [[
629 *** [ functional_extensionality_dep :
630 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
631 (forall x : A, f x = g x) -> f = g ]
632
633 ]]
634
635 This axiom says that two functions are equal if they map equal inputs to equal outputs. Such facts are not provable in general in CIC, but it is consistent to assume that they are.
636
637 A simple corollary shows that the same property applies to predicates. In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *)
638
639 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x),
640 (forall x : A, f x = g x) -> f = g.
641 intros; apply functional_extensionality_dep; assumption.
642 Qed.
643
644
645 (** ** Axioms of Choice *)
646
647 (** Some Coq axioms are also points of contention in mainstream math. The most prominent example is the axiom of choice. In fact, there are multiple versions that we might consider, and, considered in isolation, none of these versions means quite what it means in classical set theory.
648
649 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *)
650
651 Require Import ConstructiveEpsilon.
652 Check constructive_definite_description.
653 (** %\vspace{-.15in}% [[
654 constructive_definite_description
655 : forall (A : Set) (f : A -> nat) (g : nat -> A),
656 (forall x : A, g (f x) = x) ->
657 forall P : A -> Prop,
658 (forall x : A, {P x} + {~ P x}) ->
659 (exists! x : A, P x) -> {x : A | P x}
660 ]] *)
661
662 Print Assumptions constructive_definite_description.
663 (** %\vspace{-.15in}% [[
664 Closed under the global context
665
666 ]]
667
668 This function transforms a decidable predicate [P] into a function that produces an element satisfying [P] from a proof that such an element exists. The functions [f] and [g], plus an associated injectivity property, are used to express the idea that the set [A] is countable. Under these conditions, a simple brute force algorithm gets the job done: we just enumerate all elements of [A], stopping when we find one satisfying [P]. The existence proof, specified in terms of %\textit{%#<i>#unique#</i>#%}% existence [exists!], guarantees termination. The definition of this operator in Coq uses some interesting techniques, as seen in the implementation of the [ConstructiveEpsilon] module.
669
670 Countable choice is provable in set theory without appealing to the general axiom of choice. To support the more general principle in Coq, we must also add an axiom. Here is a functional version of the axiom of unique choice. *)
671
672 Require Import ClassicalUniqueChoice.
673 Check dependent_unique_choice.
674 (** %\vspace{-.15in}% [[
675 dependent_unique_choice
676 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
677 (forall x : A, exists! y : B x, R x y) ->
678 exists f : forall x : A, B x, forall x : A, R x (f x)
679
680 ]]
681
682 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *)
683
684 Require Import ClassicalChoice.
685 Check choice.
686 (** %\vspace{-.15in}% [[
687 choice
688 : forall (A B : Type) (R : A -> B -> Prop),
689 (forall x : A, exists y : B, R x y) ->
690 exists f : A -> B, forall x : A, R x (f x)
691
692 ]]
693
694 This principle is proved as a theorem, based on the unique choice axiom and an additional axiom of relational choice from the [RelationalChoice] module.
695
696 In set theory, the axiom of choice is a fundamental philosophical commitment one makes about the universe of sets. In Coq, the choice axioms say something weaker. For instance, consider the simple restatement of the [choice] axiom where we replace existential quantification by its Curry-Howard analogue, subset types. *)
697
698 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B | R x y})
699 : {f : A -> B | forall x : A, R x (f x)} :=
700 exist (fun f => forall x : A, R x (f x))
701 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)).
702
703 (** Via the Curry-Howard correspondence, this "axiom" can be taken to have the same meaning as the original. It is implemented trivially as a transformation not much deeper than uncurrying. Thus, we see that the utility of the axioms that we mentioned earlier comes in their usage to build programs from proofs. Normal set theory has no explicit proofs, so the meaning of the usual axiom of choice is subtlely different. In Gallina, the axioms implement a controlled relaxation of the restrictions on information flow from proofs to programs.
704
705 However, when we combine an axiom of choice with the law of the excluded middle, the idea of "choice" becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of "programs," but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This truly is more than repackaging a function with a different type.
706
707 %\bigskip%
708
709 The Coq tools support a command-line flag %\texttt{%#<tt>#-impredicative-set#</tt>#%}%, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This contrasts with [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop].
710
711 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, this can lead to inconsistency. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *)
712
713 (** ** Axioms and Computation *)
714
715 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of %\textit{%#<i>#computational equivalence#</i>#%}% is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *)
716
717 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
718 match pf with
719 | refl_equal => v
720 end.
721
722 (** Computation over programs that use [cast] can proceed smoothly. *)
723
724 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
725 (** [[
726 = 13
727 : nat
728 ]] *)
729
730 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
731
732 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
733 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
734 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
735 Qed.
736
737 Eval compute in (cast t3 (fun _ => First)) 12.
738 (** [[
739 = match t3 in (_ = P) return P with
740 | refl_equal => fun n : nat => First
741 end 12
742 : fin (12 + 1)
743
744 ]]
745
746 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *)
747
748 Reset t3.
749
750 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
751 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
752 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
753 Defined.
754
755 Eval compute in (cast t3 (fun _ => First)) 12.
756 (** [[
757 = match
758 match
759 match
760 functional_extensionality
761 ....
762
763 ]]
764
765 We elide most of the details. A very unwieldy tree of nested matches on equality proofs appears. This time evaluation really %\textit{%#<i>#is#</i>#%}% stuck on a use of an axiom.
766
767 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
768
769 Lemma plus1 : forall n, S n = n + 1.
770 induction n; simpl; intuition.
771 Defined.
772
773 Theorem t4 : forall n, fin (S n) = fin (n + 1).
774 intro; f_equal; apply plus1.
775 Defined.
776
777 Eval compute in cast (t4 13) First.
778 (** %\vspace{-.15in}% [[
779 = First
780 : fin (13 + 1)
781 ]] *)