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

comparison src/Subset.v @ 297:b441010125d4

Everything compiles in Coq 8.3pl1

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 14 Jan 2011 14:39:12 -0500
parents	1b6c81e51799
children	7b38729be069

comparison

equal deleted inserted replaced

-:559ec7328410
+:b441010125d4
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
 *
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 | S n' -> n'
 </pre>#
 We have managed to reach a type that is, in a formal sense, the most expressive possible for [pred].  Any other implementation of the same type must have the same input-output behavior.  However, there is still room for improvement in making this kind of code easier to write.  Here is a version that takes advantage of tactic-based theorem proving.  We switch back to passing a separate proof argument instead of using a subset type for the function's input, because this leads to cleaner code. *)
-Definition pred_strong4 (n : nat) : n > 0 -> {m : nat | n = S m}.
+Definition pred_strong4 : forall n : nat, n > 0 -> {m : nat | n = S m}.
 refine (fun n =>
 match n with
 | O => fun _ => False_rec _ _
 | S n' => fun _ => exist _ n' _
 end).
 We are almost done with the ideal implementation of dependent predecessor.  We can use Coq's syntax extension facility to arrive at code with almost no complexity beyond a Haskell or ML program with a complete specification in a comment. *)
 Notation "!" := (False_rec _ _).
 Notation "[ e ]" := (exist _ e _).
-Definition pred_strong5 (n : nat) : n > 0 -> {m : nat | n = S m}.
+Definition pred_strong5 : forall n : nat, n > 0 -> {m : nat | n = S m}.
 refine (fun n =>
 match n with
 | O => fun _ => !
 | S n' => fun _ => [n']
 end); crush.
 (** The [Reduce] notation is notable because it demonstrates how [if] is overloaded in Coq.  The [if] form actually works when the test expression has any two-constructor inductive type.  Moreover, in the [then] and [else] branches, the appropriate constructor arguments are bound.  This is important when working with [sumbool]s, when we want to have the proof stored in the test expression available when proving the proof obligations generated in the appropriate branch.
 Now we can write [eq_nat_dec], which compares two natural numbers, returning either a proof of their equality or a proof of their inequality. *)
-Definition eq_nat_dec (n m : nat) : {n = m} + {n <> m}.
+Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}.
 refine (fix f (n m : nat) : {n = m} + {n <> m} :=
 match n, m with
 | O, O => Yes
 | S n', S m' => Reduce (f n' m')
 | _, _ => No
 Notation "??" := (Unknown _).
 Notation "[[ x ]]" := (Found _ x _).
 (** Now our next version of [pred] is trivial to write. *)
-Definition pred_strong7 (n : nat) : {{m | n = S m}}.
+Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
 refine (fun n =>
 match n with
 | O => ??
 | S n' => [[n']]
 end); trivial.
 Notation "!!" := (inright _ _).
 Notation "[[[ x ]]]" := (inleft _ [x]).
 (** Now we are ready to give the final version of possibly-failing predecessor.  The [sumor]-based type that we use is maximally expressive; any implementation of the type has the same input-output behavior. *)
-Definition pred_strong8 (n : nat) : {m : nat | n = S m} + {n = 0}.
+Definition pred_strong8 : forall n : nat, {m : nat | n = S m} + {n = 0}.
 refine (fun n =>
 match n with
 | O => !!
 | S n' => [[[n']]]
 end); trivial.
 (** The meaning of [x <- e1; e2] is: First run [e1].  If it fails to find an answer, then announce failure for our derived computation, too.  If [e1] %\textit{%#<i>#does#</i>#%}% find an answer, pass that answer on to [e2] to find the final result.  The variable [x] can be considered bound in [e2].
 This notation is very helpful for composing richly-typed procedures.  For instance, here is a very simple implementation of a function to take the predecessors of two naturals at once. *)
-Definition doublePred (n1 n2 : nat) : {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
+Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
 refine (fun n1 n2 =>
 m1 <- pred_strong7 n1;
 m2 <- pred_strong7 n2;
 [[(m1, m2)]]); tauto.
 Defined.
 end)
 (right associativity, at level 60).
 (** printing * $\times$ *)
-Definition doublePred' (n1 n2 : nat)
+Definition doublePred' : forall n1 n2 : nat,
-: {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
+{p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
 + {n1 = 0 \/ n2 = 0}.
 refine (fun n1 n2 =>
 m1 <-- pred_strong8 n1;
 m2 <-- pred_strong8 n2;
 [[[(m1, m2)]]]); tauto.
 (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}}.
+Definition typeCheck : forall e : exp, {{t | hasType e t}}.
 (* begin thide *)
 Hint Constructors hasType.
 refine (fix F (e : exp) : {{t | hasType e t}} :=
 match e with
 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}.
+Definition typeCheck' : forall 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.

Mercurial > cpdt > repo

comparison src/Subset.v @ 297:b441010125d4