adamc@142: (* Copyright (c) 2008, Adam Chlipala
adamc@142:  * 
adamc@142:  * This work is licensed under a
adamc@142:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@142:  * Unported License.
adamc@142:  * The license text is available at:
adamc@142:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@142:  *)
adamc@142: 
adamc@142: (* begin hide *)
adamc@142: Require Import List.
adamc@142: 
adamc@142: Require Import Tactics MoreSpecif.
adamc@142: 
adamc@142: Set Implicit Arguments.
adamc@142: (* end hide *)
adamc@142: 
adamc@142: 
adamc@142: (** %\chapter{Proof by Reflection}% *)
adamc@142: 
adamc@142: (** The last chapter highlighted a very heuristic approach to proving.  In this chapter, we will study an alternative technique, %\textit{%#<i>#proof by reflection#</i>#%}%.  We will write, in Gallina, decision procedures with proofs of correctness, and we will appeal to these procedures in writing very short proofs.  Such a proof is checked by running the decision procedure.  The term %\textit{%#<i>#reflection#</i>#%}% applies because we will need to translate Gallina propositions into values of inductive types representing syntax, so that Gallina programs may analyze them. *)
adamc@142: 
adamc@142: 
adamc@142: (** * Proving Evenness *)
adamc@142: 
adamc@142: (** Proving that particular natural number constants are even is certainly something we would rather have happen automatically.  The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure. *)
adamc@142: 
adamc@142: Inductive isEven : nat -> Prop :=
adamc@142:   | Even_O : isEven O
adamc@142:   | Even_SS : forall n, isEven n -> isEven (S (S n)).
adamc@142: 
adamc@142: Ltac prove_even := repeat constructor.
adamc@142: 
adamc@142: Theorem even_256 : isEven 256.
adamc@142:   prove_even.
adamc@142: Qed.
adamc@142: 
adamc@142: Print even_256.
adamc@142: (** [[
adamc@142: 
adamc@142: even_256 = 
adamc@142: Even_SS
adamc@142:   (Even_SS
adamc@142:      (Even_SS
adamc@142:         (Even_SS
adamc@142:     ]]
adamc@142: 
adamc@142:     ...and so on.  This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even.  The final proof term has length linear in the input value.  This seems like a shame, since we could write a trivial and trustworthy program to verify evenness of constants.  The proof checker could simply call our program where needed.
adamc@142: 
adamc@142:     It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately.  Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.
adamc@142: 
adamc@142:     The techniques of proof by reflection address both complaints.  We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
adamc@142: 
adamc@142:     For this example, we begin by using a type from the [MoreSpecif] module to write a certified evenness checker. *)
adamc@142: 
adamc@142: Print partial.
adamc@142: (** [[
adamc@142: 
adamc@142: Inductive partial (P : Prop) : Set :=  Proved : P -> [P] | Uncertain : [P]
adamc@142:     ]] *)
adamc@142: 
adamc@142: (** A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
adamc@142: 
adamc@142: Open Local Scope partial_scope.
adamc@142: 
adamc@142: (** We bring into scope some notations for the [partial] type.  These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *)
adamc@142: 
adamc@142: Definition check_even (n : nat) : [isEven n].
adamc@142:   Hint Constructors isEven.
adamc@142: 
adamc@142:   refine (fix F (n : nat) : [isEven n] :=
adamc@142:     match n return [isEven n] with
adamc@142:       | 0 => Yes
adamc@142:       | 1 => No
adamc@142:       | S (S n') => Reduce (F n')
adamc@142:     end); auto.
adamc@142: Defined.
adamc@142: 
adamc@142: (** We can use dependent pattern-matching to write a function that performs a surprising feat.  When given a [partial P], this function [partialOut] returns a proof of [P] if the [partial] value contains a proof, and it returns a (useless) proof of [True] otherwise.  From the standpoint of ML and Haskell programming, it seems impossible to write such a type, but it is trivial with a [return] annotation. *)
adamc@142: 
adamc@142: Definition partialOut (P : Prop) (x : [P]) :=
adamc@142:   match x return (match x with
adamc@142:                     | Proved _ => P
adamc@142:                     | Uncertain => True
adamc@142:                   end) with
adamc@142:     | Proved pf => pf
adamc@142:     | Uncertain => I
adamc@142:   end.
adamc@142: 
adamc@142: (** It may seem strange to define a function like this.  However, it turns out to be very useful in writing a reflective verison of our earlier [prove_even] tactic: *)
adamc@142: 
adamc@142: Ltac prove_even_reflective :=
adamc@142:   match goal with
adamc@142:     | [ |- isEven ?N] => exact (partialOut (check_even N))
adamc@142:   end.
adamc@142: 
adamc@142: (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. *)
adamc@142: 
adamc@142: Theorem even_256' : isEven 256.
adamc@142:   prove_even_reflective.
adamc@142: Qed.
adamc@142: 
adamc@142: Print even_256'.
adamc@142: (** [[
adamc@142: 
adamc@142: even_256' = partialOut (check_even 256)
adamc@142:      : isEven 256
adamc@142:     ]]
adamc@142: 
adamc@142:     We can see a constant wrapper around the object of the proof.  For any even number, this form of proof will suffice.  What happens if we try the tactic with an odd number? *)
adamc@142: 
adamc@142: Theorem even_255 : isEven 255.
adamc@142:   (** [[
adamc@142: 
adamc@142:   prove_even_reflective.
adamc@142: 
adamc@142:   [[
adamc@142: 
adamc@142: User error: No matching clauses for match goal
adamc@142:   ]]
adamc@142: 
adamc@142:   Thankfully, the tactic fails.  To see more precisely what goes wrong, we can run manually the body of the [match].
adamc@142: 
adamc@142:   [[
adamc@142: 
adamc@142:   exact (partialOut (check_even 255)).
adamc@142: 
adamc@142:   [[
adamc@142: 
adamc@142:   Error: The term "partialOut (check_even 255)" has type
adamc@142:  "match check_even 255 with
adamc@142:   | Yes => isEven 255
adamc@142:   | No => True
adamc@142:   end" while it is expected to have type "isEven 255"
adamc@142:   ]]
adamc@142: 
adamc@142:   As usual, the type-checker performs no reductions to simplify error messages.  If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *)
adamc@142: Abort.