The Coq mailing list

[Tim Reed <tim.reed AT gmail.com>]

Hi all,

I am familiarizing myself with the sig type and I was wondering if
it would be wise to have a stronger notion of a signature. The 
way I've been using it is to use a proposition that establishes a
relation between a function's inputs and the acceptable output 
and use the sig and sumor types to describe the specification of 
the intended behavior and error cases for the function. 

For instance:

Definition myhead (A : Set) (l : list A) : 
  { a : A | exists ls : list A, l = cons a ls} + {l = nil}.

This is a simple example. In more complicated examples, I find 
myself using propositions for the "inright" type of the sumor that 
are not the logical complement of the proposition used in my sig 
type for the "inleft" type of the sumor. 

I would really like to have a strong specification so that I know
that I've covered all of the cases for a function's inputs and output
and not allow for any possibility that a function's result can be 
described by both the inleft and the inright sides of the sumor. For 
instance, the following is not a very strong specification:

Definition myhead2 (A : Set) (l : list A) :
  { a : A | exists ls : list A, l = cons a ls} + {True}. 

A trivial program that always provides the "I" constructor would
satisfy this specification.

I'm considering adopting a new signature type defined as: 

Definition strong_sig (A : Type) (P : A -> Prop) := 
   sig P + {forall a : A, ~ P a}.
Implicit Arguments strong_sig [A].
Notation "{{ a : A | P }}" := 
   (strong_sig (fun a : A => P)) 
   (at level 0, a at level 99).

With this type, I think I can be sure that when I prove a program 
specification is realizable that I will then be forced to prove that for
every possible function input its output is in exactly one of the inleft
or inright cases, but not both.  For instance:

Definition myhead3 (A : Set) (l : list A) : 
  {{ a : A | exists ls : list A, l = cons a ls}}.

This specification should be easy since the inright type expands to 
"forall a : A, ~ exists ls : list A, l = cons a ls" and this error case 
arises when we know that l = nil. 

But, I think this type and its notation is a more compact and stronger
way to specify what a function does. 

Any comments? Has this path been explored and found to have
pitfalls? 

Regards,
Tim.