comparison src/InductiveTypes.v @ 33:8b34dade70e1

Reflexive Types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 10 Sep 2008 12:54:51 -0400
parents 77e1a7eda0b8
children d44274542f8b
comparison
equal deleted inserted replaced
32:77e1a7eda0b8 33:8b34dade70e1
548 (fun ol : odd_list => forall el : even_list, 548 (fun ol : odd_list => forall el : even_list,
549 olength (oapp ol el) = plus (olength ol) (elength el))); crush. 549 olength (oapp ol el) = plus (olength ol) (elength el))); crush.
550 Qed. 550 Qed.
551 551
552 (** We simply need to specify two predicates, one for each of the mutually inductive types. In general, it would not be a good idea to assume that a proof assistant could infer extra predicates, so this way of applying mutual induction is about as straightforward as we could hope for. *) 552 (** We simply need to specify two predicates, one for each of the mutually inductive types. In general, it would not be a good idea to assume that a proof assistant could infer extra predicates, so this way of applying mutual induction is about as straightforward as we could hope for. *)
553
554
555 (** * Reflexive Types *)
556
557 (** A kind of inductive type called a %\textit{%#<i>#reflexive type#</i>#%}% is defined in terms of functions that have the type being defined as their range. One very useful class of examples is in modeling variable binders. For instance, here is a type for encoding the syntax of a subset of first-order logic: *)
558
559 Inductive formula : Set :=
560 | Eq : nat -> nat -> formula
561 | And : formula -> formula -> formula
562 | Forall : (nat -> formula) -> formula.
563
564 (** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of "variables" in our type, by using Coq functions to encode quantification. For instance, here is the encoding of [forall x : nat, x = x]: *)
565
566 Example forall_refl : formula := Forall (fun x => Eq x x).
567
568 (** We can write recursive functions over reflexive types quite naturally. Here is one translating our formulas into native Coq propositions. *)
569
570 Fixpoint formulaDenote (f : formula) : Prop :=
571 match f with
572 | Eq n1 n2 => n1 = n2
573 | And f1 f2 => formulaDenote f1 /\ formulaDenote f2
574 | Forall f' => forall n : nat, formulaDenote (f' n)
575 end.
576
577 (** We can also encode a trivial formula transformation that swaps the order of equality and conjunction operands. *)
578
579 Fixpoint swapper (f : formula) : formula :=
580 match f with
581 | Eq n1 n2 => Eq n2 n1
582 | And f1 f2 => And (swapper f2) (swapper f1)
583 | Forall f' => Forall (fun n => swapper (f' n))
584 end.
585
586 (** It is helpful to prove that this transformation does not make true formulas false. *)
587
588 Theorem swapper_preserves_truth : forall f, formulaDenote f -> formulaDenote (swapper f).
589 induction f; crush.
590 Qed.
591
592 (** We can take a look at the induction principle behind this proof. *)
593
594 Check formula_ind.
595 (** [[
596
597 formula_ind
598 : forall P : formula -> Prop,
599 (forall n n0 : nat, P (Eq n n0)) ->
600 (forall f0 : formula,
601 P f0 -> forall f1 : formula, P f1 -> P (And f0 f1)) ->
602 (forall f1 : nat -> formula,
603 (forall n : nat, P (f1 n)) -> P (Forall f1)) ->
604 forall f2 : formula, P f2
605 ]] *)
606
607 (** Focusing on the [Forall] case, which comes third, we see that we are allowed to assume that the theorem holds %\textit{%#<i>#for any application of the argument function [f1]#</i>#%}%. That is, Coq induction principles do not follow a simple rule that the textual representations of induction variables must get shorter in appeals to induction hypotheses. Luckily for us, the people behind the metatheory of Coq have verified that this flexibility does not introduce unsoundness.
608
609 %\medskip%
610
611 Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in Haskell and ML. This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes. In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness. Reflexive types provide our first good example of such a case.
612
613 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of lambda calculus. Indeed, the function-based representation technique that we just used, called %\textit{%#<i>#higher-order abstract syntax (HOAS)#</i>#%}%, is the representation of choice for lambda calculi in Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *)
614
615 (** [[
616
617 Inductive term : Set :=
618 | App : term -> term -> term
619 | Abs : (term -> term) -> term.
620
621 [[
622 Error: Non strictly positive occurrence of "term" in "(term -> term) -> term"
623 ]]
624
625 We have run afoul of the %\textit{%#<i>#strict positivity requirement#</i>#%}% for inductive definitions, which says that the type being defined may not occur to the left of an arrow in the type of a constructor argument. It is important that the type of a constructor is viewed in terms of a series of arguments and a result, since obviously we need recursive occurrences to the lefts of the outermost arrows if we are to have recursive occurrences at all.
626
627 Why must Coq enforce this restriction? Imagine that our last definition had been accepted, allowing us to write this function:
628
629 [[
630 Definition uhoh (t : term) : term :=
631 match t with
632 | Abs f => f t
633 | _ => t
634 end.
635
636 Using an informal idea of Coq's semantics, it is easy to verify that the application [uhoh (Abs uhoh)] will run forever. This would be a mere curiosity in OCaml and Haskell, where non-termination is commonplace, though the fact that we have a non-terminating program without explicit recursive function definitions is unusual.
637
638 For Coq, however, this would be a disaster. The possibility of writing such a function would destroy all our confidence that proving a theorem means anything. Since Coq combines programs and proofs in one language, we would be able to prove every theorem with an infinite loop.
639
640 Nonetheless, the basic insight of HOAS is a very useful one, and there are ways to realize most benefits of HOAS in Coq. We will study a particular technique of this kind in the later chapters on programming language syntax and semantics. *)