The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

(* a small workaround: *)
Set Implicit Arguments.

Inductive Xsig (A: Type) (P: A -> Prop): Type :=
| Xexists: forall a, P a -> Xsig P
| XunivN: (forall a, P a -> False) -> Xsig P.

Inductive Xsum (A: Type) (P: A -> Prop) (R: Prop): Type :=
| Xleft: forall a, P a -> Xsum P R
| Xright: R -> Xsum P R.

Notation "{{ a : A | P }}" :=
   (Xsig (fun a : A => P))
   (at level 0, a at level 99).

Notation "{ a : A | P } + R" :=
   (Xsum (fun a : A => P) R)
   (at level 0, a at level 99).

Lemma cast1: forall A (L: A -> Prop) (R: Prop),
      (R -> forall a, L a -> False) ->
      {a: A | L a}+R ->
      {{a: A | L a}}.
Proof.
 intros.
 destruct X as [a La|r].
  now left with a.
 right; now apply H.
Qed.

Lemma cast2: forall A (L: A -> Prop) (R: Prop),
      ((forall a, L a -> False) -> R) ->
      {{a: A | L a}} ->
      {a: A | L a}+R.
Proof.
 intros.
 destruct X as [a La|r].
  now left with a.
 right; now apply H.
Qed.

Require Import List.
Definition myhead1 (A : Set) (l : list A) :
 { a : A | exists ls : list A, l = a::ls} + (l = nil).
Proof.
 destruct l as [|h t]; [right|left with h].
  split.
 eexists; split.
Defined.

Definition myhead2 (A : Set) (l : list A) :
 {{ a : A | exists ls : list A, l = a::ls}}.
Proof.
 intros A l.
 refine (cast1 _ _ (myhead1 l)).
 intros; subst; destruct H0; discriminate.
Qed.

>
> 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.
>
>

I am not conviced, your "strong specification" is really more interesting,
excepted in the domain of decidability (but in this domain, {P}+{~P} is
used from a long time).

About your ...+{True} which is not very strog, what do you think of
{{a:A | True}} or {{a:A | False}}?

It is the responsabilty of the programmer to make meaningfull specification.

-- 
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay