Certified Programming with Dependent Types: src/Subset.v comparison

comparison src/Subset.v @ 77:d07c77659c20

Templatizing Subset

author	Adam Chlipala <adamc@hcoop.net>
date	Fri, 03 Oct 2008 15:27:39 -0400
parents	82a2189fa283
children	15e2b3485dc4

comparison

equal deleted inserted replaced

-:82a2189fa283
+:d07c77659c20
 refine (fun n =>
 match n return (n > 0 -> {m : nat | n = S m}) with
 | O => fun _ => False_rec _ _
 | S n' => fun _ => exist _ n' _
 end).
+(* begin thide *)
 (** We build [pred_strong4] using tactic-based proving, beginning with a [Definition] command that ends in a period before a definition is given.  Such a command enters the interactive proving mode, with the type given for the new identifier as our proof goal.  We do most of the work with the [refine] tactic, to which we pass a partial "proof" of the type we are trying to prove.  There may be some pieces left to fill in, indicated by underscores.  Any underscore that Coq cannot reconstruct with type inference is added as a proof subgoal.  In this case, we have two subgoals:
 [[
 2 subgoals
 refine (fun n =>
 match n return (n > 0 -> {m : nat | n = S m}) with
 | O => fun _ => False_rec _ _
 | S n' => fun _ => exist _ n' _
 end); crush.
+(* end thide *)
 Defined.
 (** We end the "proof" with [Defined] instead of [Qed], so that the definition we constructed remains visible.  This contrasts to the case of ending a proof with [Qed], where the details of the proof are hidden afterward.  Let us see what our proof script constructed. *)
 Print pred_strong4.
 (** %\smallskip%
 We can build "smart" versions of the usual boolean operators and put them to good use in certified programming.  For instance, here is a [sumbool] version of boolean "or." *)
+(* begin thide *)
 Notation "x || y" := (if x then Yes else Reduce y) (at level 50).
 (** Let us use it for building a function that decides list membership.  We need to assume the existence of an equality decision procedure for the type of list elements. *)
 Section In_dec.
 End In_dec.
 (** [In_dec] has a reasonable extraction to OCaml. *)
 Extraction In_dec.
+(* end thide *)
 (** %\begin{verbatim}
 (** val in_dec : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 list -> bool **)
 let rec in_dec a_eq_dec x = function
 -> hasType e2 TBool
 -> hasType (And e1 e2) TBool.
 (** It will be helpful to have a function for comparing two types.  We build one using [decide equality]. *)
+(* begin thide *)
 Definition eq_type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}.
 decide equality.
 Defined.
 (** Another notation complements the monadic notation for [maybe] that we defined earlier.  Sometimes we want to be to include "assertions" in our procedures.  That is, we want to run a decision procedure and fail if it fails; otherwise, we want to continue, with the proof that it produced made available to us.  This infix notation captures that, for a procedure that returns an arbitrary two-constructor type. *)
 Notation "e1 ;; e2" := (if e1 then e2 else ??)
 (right associativity, at level 60).
 (** With that notation defined, we can implement a [typeCheck] function, whose code is only more complex than what we would write in ML because it needs to include some extra type annotations.  Every [[[e]]] expression adds a [hasType] proof obligation, and [crush] makes short work of them when we add [hasType]'s constructors as hints. *)
+(* end thide *)
 Definition typeCheck (e : exp) : {{t | hasType e t}}.
+(* begin thide *)
 Hint Constructors hasType.
 refine (fix F (e : exp) : {{t | hasType e t}} :=
 match e return {{t | hasType e t}} with
 | Nat _ => [[TNat]]
 t2 <- F e2;
 eq_type_dec t1 TBool;;
 eq_type_dec t2 TBool;;
 [[TBool]]
 end); crush.
+(* end thide *)
 Defined.
 (** Despite manipulating proofs, our type checker is easy to run. *)
 Eval simpl in typeCheck (Nat 0).
 (** %\smallskip%
 We can adapt this implementation to use [sumor], so that we know our type-checker only fails on ill-typed inputs.  First, we define an analogue to the "assertion" notation. *)
+(* begin thide *)
 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
 (right associativity, at level 60).
 (** Next, we prove a helpful lemma, which states that a given expression can have at most one type. *)
 induction 1; inversion 1; crush.
 Qed.
 (** Now we can define the type-checker.  Its type expresses that it only fails on untypable expressions. *)
+(* end thide *)
 Definition typeCheck' (e : exp) : {t : type | hasType e t} + {forall t, ~hasType e t}.
+(* begin thide *)
 Hint Constructors hasType.
 (** We register all of the typing rules as hints. *)
 Hint Resolve hasType_det.
 (** [hasType_det] will also be useful for proving proof obligations with contradictory contexts.  Since its statement includes [forall]-bound variables that do not appear in its conclusion, only [eauto] will apply this hint. *)
 eq_type_dec t2 TBool;;;
 [[[TBool]]]
 end); clear F; crush' tt hasType; eauto.
 (** We clear [F], the local name for the recursive function, to avoid strange proofs that refer to recursive calls that we never make.  The [crush] variant [crush'] helps us by performing automatic inversion on instances of the predicates specified in its second argument.  Once we throw in [eauto] to apply [hasType_det] for us, we have discharged all the subgoals. *)
+(* end thide *)
 Defined.
 (** The short implementation here hides just how time-saving automation is.  Every use of one of the notations adds a proof obligation, giving us 12 in total.  Most of these obligations require multiple inversions and either uses of [hasType_det] or applications of [hasType] rules.
 The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *)

Mercurial > cpdt > repo

comparison src/Subset.v @ 77:d07c77659c20