(** Following are modules with the various [stack] implementations. First [NatStack] defines the stack of naturals that looks and behaves as expected. Second, [StackPoly] implements a polymorphic stack using and explicit type variable, [T], for the type in the stack. Third, [StackInfer] allows Coq to infer the content type [T] used in [pop]. Finally, [StackArg] introduces implicit arguments for the content type [T] used in [top] and [size]. The [StackDep] uses proofs as arguments to values. When I introduced polymorphism you should notice the definitions of [top] are commented out. The reason for this is we don't know what to return when finding [top] of [empty]. This module fixes this using dependent typing. Take a peek and see if you can grock what's going on. This is reasonably advanced, so don't stress if it's not clear what's happening. Remember, types are theorems and values associated with types are proofs. The final model, [StackSubset], uses subset types to accomplish require verification that a stack is nonempty before calling [top] or [pop]. The proof is embedded in stack values as a theorem and associated proof of that theorem. *) (** Stack of natural numbers *) Require Import Omega. Module Natstack. (** A stack of natural numbers *) Inductive natstack : Type := | empty : natstack | push : nat -> natstack -> natstack. Definition pop(s:natstack):natstack := match s with | empty => empty | push n' s' => s' end. (** The definition of [top] has a major problem. Do you see it? *) Definition top(s:natstack):nat := match s with | empty => 0 | push n' s' => n' end. Fixpoint size(s:natstack):nat := match s with | empty => 0 | push _ s' => 1+(size s') end. (** Some sanity checks just to make sure we're on the right track *) Eval compute in push 0 empty. Eval compute in push 0 (push 1 empty). Eval compute in pop (push 0 (push 1 empty)). Eval compute in top (push 0 (push 1 empty)). Eval compute in size (push 0 (push 1 empty)). (** Sanity checks in the form of proofs. These will fail if functions return unexpected values and serve as regression tests. *) Example ex1: pop (push 1 empty) = empty. Proof. reflexivity. Qed. Example ex2: top (push 0 (push 1 empty)) = 0. Proof. reflexivity. Qed. (** Now a theorem. Any [natstack] is equivalent to pushing [top s] onto [pop s]. Makes good sense. Cannot be proved! *) Theorem congr: forall s, push (top s) (pop s) = s. Proof. induction s. simpl. Abort. (** We wind up with [push 0 empty = empty] which is clearly false. This is the major error in [pop]. Specifically, [pop empty] should be undefined, not the magic number 0. *) (** A different way. We will now say that [push] of [top s] on [pop s] is [s] if [s] is not empty. *) Theorem congr: forall s, s<>empty -> push (top s) (pop s) = s. Proof. intros s. intros H. induction s. contradiction. reflexivity. Qed. (** This pops out nicely. The [empty] induction case falls out becase [empty<>empty] appears in the hypotheses. That is inconsistent and discharges that case. *) (** Proof that [size] of [push] is bigger than the original stack. We use [apply] as a demonstration of applying a theorem. There are other and better ways to do it. *) Theorem bigger: forall s x, size (push x s) >= size s. Proof. intros s x. simpl. apply le_S. reflexivity. Qed. End Natstack. (** Stack of anything. Why is [top] commented out? How would you fix it? *) Module StackPoly. (** The type and constructors are parameterized over [T:Type] where [T] is the type contained in the stack. Stackness does not depend on what is contained in the stack. *) Inductive stack(T:Type) : Type := | empty : stack T | push : T -> stack T -> stack T. (** [empty] and [push] both have an extra parameter that will be [T]. However, we do not pattern match on types, so [_] is used. *) Definition pop(T:Type)(s:stack T):stack T := match s with | empty _ => empty T | push _ n' s' => s' end. (* Definition top(T:Type)(s:stack T):T := match s with | empty _ => | push _ n' s' => n' end. *) Fixpoint size(T:Type)(s:stack T):nat := match s with | empty _ => 0 | push _ _ s' => 1+(size _ s') end. Eval compute in push nat 0 (empty nat). Eval compute in push nat 0 (push nat 1 (empty nat)). Eval compute in pop nat (push nat 0 (push nat 1 (empty nat))). Eval compute in size nat (push nat 0 (push nat 1 (empty nat))). End StackPoly. (** Polymorphic stack where observers infer the stack content type. *) Module StackInfer. (** The [stack] type definition remains the same with the [T] parameter used for content type *) Inductive stack(T:Type) : Type := | empty : stack T | push : T -> stack T -> stack T. (** The type parameter for [pop] uses braces, [{T:Type}], rather than parens. This tells Coq that it needs to infer the parameter [T] rather than expect it from the user. *) Definition pop{T:Type}(s:stack T):stack T := match s with | empty _ => empty T | push _ n' s' => s' end. (* Definition top(T:Type)(s:stack T):T := match s with | empty _ => | push _ n' s' => n' end. *) Fixpoint size{T:Type}(s:stack T):nat := match s with | empty _ => 0 | push _ _ s' => 1+(size s') end. Eval compute in push nat 0 (empty nat). Eval compute in push nat 0 (push nat 1 (empty nat)). (** The last two examples demonstrate inference. [pop] and [size] do not specify values for [T]. Instead, Coq infers that value. Still not quite what we want, but getting closer. *) Eval compute in pop (push nat 0 (push nat 1 (empty nat))). Eval compute in size (push nat 0 (push nat 1 (empty nat))). End StackInfer. (** Fully polymorphic stack implmenetation where constructors and observers infer types for stack contents. *) Module StackArg. (** Still type stack type does not change. *) Inductive stack(T:Type) : Type := | empty : stack T | push : T -> stack T -> stack T. (** The [Arguments] directive tells Coq after the fact what variables should be inferred. In the definition above, [T] is specified manually for [empty] and [push]. After calls to [Argument], [T] will be inferred by Coq. *) Arguments empty {T}. Arguments push {T} _ _. Definition pop{T:Type}(s:stack T):stack T := match s with | empty => empty | push n' s' => s' end. (* Definition top(T:Type)(s:stack T):T := match s with | empty _ => | push _ n' s' => n' end. *) Fixpoint size{T:Type}(s:stack T):nat := match s with | empty => 0 | push _ s' => 1+(size s') end. (** Now usage of polymorphic stack functions looks like we expect. No need to specify type of the stack contents in function or constructors calls. *) Eval compute in push 0 empty. Eval compute in push 0 (push 1 empty). Eval compute in pop (push 0 (push 1 empty)). (* Eval compute in top nat (push nat 0 (push nat 1 (empty nat))). *) Eval compute in size (push 0 (push 1 empty)). End StackArg. Module StackOption. (** Lets deal with the return values of [pop] and [top] over [empty] using the [option] type. [option] allows returning a value or a non-value. It has two constructors, [None] and [Some x]. [None] is returned when no value can be calculated. Like [pop empty]. [Some x] is returned when [x] is the value to be returned. Using [option] has the effect of making [pop] and [top] total. *) Inductive stack(T:Type) : Type := | empty : stack T | push : T -> stack T -> stack T. Arguments empty {T}. Arguments push {T} _ _. (** [pop empty] returns [None] indicating no value. [pop (push ...)] returns [Some v] when [v] is the result of the operation. A [match] in the calling function easily manages the two return values. (You will see this later.) *) Definition pop{T:Type}(s:stack T):(option (stack T)) := match s with | empty => None | push n' s' => Some s' end. Definition top{T:Type}(s:stack T):(option T) := match s with | empty => None | push n' s' => Some n' end. Fixpoint size{T:Type}(s:stack T):nat := match s with | empty => 0 | push _ s' => 1+(size s') end. (** Note the return value for the 3rd example *) Eval compute in push 0 empty. Eval compute in push 0 (push 1 empty). Eval compute in pop empty. Eval compute in pop (push 0 (push 1 empty)). Eval compute in top (push 0 (push 1 empty)). Eval compute in size (push 0 (push 1 empty)). End StackOption. (** Dependently typed stack with [top] included again. How and why? The [Eval] examples might give you a hint. Remember that proofs are values. *) Module StackDep. Inductive stack(T:Type) : Type := | empty : stack T | push : T -> stack T -> stack T. Arguments empty {T}. Arguments push {T} _ _. (** [pop] taks a [stack T] and returns a function that produces a [stack T]. The domain of that function is [s <> empty]. Remembering that types are theorems and values are proofs, the function accepts a proof of [s <> empty] and produces a [stack T]. Thus, to get the stack associated with the result of [pop] you need to prove the argument stat is not empty. *) Definition pop{T:Type}(s:stack T) : s <> empty -> (stack T) := match s with | empty => (fun p:empty<>empty => empty) | push x t => (fun p:push x t <> empty => t) end. (** [top] returns the same kind of thing as [pop]. Given a proof that the input stack is non-empty, the returned value will give you the top of the stack. *) Definition top{T:Type}{e:T}(s:stack T) : s <> empty -> T := match s with | empty => (fun p:empty<>empty => e) | push x t => (fun p:push x t <> empty => x) end. Eval compute in top (push 1 empty). Eval compute in top empty. Theorem push_ne_empty: forall T:Type, forall x s, push (T:=T) x s <> empty. Proof. intros. unfold not. intros. discriminate. Qed. Eval compute in (top (push 1 empty)) (push_ne_empty _ 1 empty). Eval compute in (top empty). End StackDep.