The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 25 Nov 2010 11:51:18 +0100,
Frank Staals 
<f.staals AT student.tue.nl>
 a écrit :

> Hey everyone,
> 
> Is there a way to automatically bind/attach a lemma to a definition ?
> I will try to explain what I mean with that with a concrete example: 
> Suppose I have a stream defintion s:
> 
> CoFixpoint s : Stream A := x :: xs.

???

That doesn't mean anything:

I can assume that A is a Type, but
AFAIK "::" is for lists (not Streams)
I do not know what are x and xs (are they already been declared).
What is the aim of defining a (co)fixpoint which is not involved in its
definition?

So did you meant that your minimalistic file would be:

"
Require Import Streams.

Parameter A: Type.
Parameter x: A.
CoFixpoint s : Stream A := Cons x s.
"
> 
> Now I want coq to automatically generate the following lemmas:
> 
> Lemma s_hd : A := hd s = x.
> Lemma s_tl : Stream A : tl s = xs.
>

Again your syntax is not clear.
Do you mean that you want generalization on A and x
(assuming that I well corrected the previous part):

"
Require Import Streams.

Section S.
 Parameter A: Type.
 Parameter x: A.
 CoFixpoint s : Stream A := Cons x s.

 Lemma s_hd: hd s = x.
 Proof.
  admit.
 Qed.

 Lemma s_tl: tl s = xs.
 Proof.
  admit.
 Qed.
End S.
"
or do you not require coinduction at all?
"
Require Import Streams.

Section S.
 Parameter A: Type.
 Parameter x: A.
 Parameter xs: Stream A.
 Definition s : Stream A := Cons x s.

 Lemma s_hd: hd s = x.
 Proof.
  admit.
 Qed.

 Lemma s_tl: tl s = xs.
 Proof.
  admit.
 Qed.
End S.
"
or do you want some decomposition lemmas:
"
Require Import Streams.

Lemma s_hd: forall (s: Stream A), {x: A|hd s = x}.
Proof.
 admit.
Qed.

Lemma s_tl: forall (s: Stream A), {xs: Stream A|tl s = xs}.
Proof.
 admit.
Qed.
"

 
> Obviously I would have to prove these lemmas. But assume that I have
> the tactics 'prove_hd' and 'prove_tl' that can prove the above lemmas
> fully automatically for any s,x and xs.
> 
> So an example of this which is already in Coq is the generation of a
> new inductive type: Coq automatically generates the induction
> principle.

I may be wrong, but I do not consider this generation a good idea
nowadays (I believe it is here for more historical reasons, when we
were on CoC, and there was no inductive types),
since it tends to produce unreadable "lisp-like" proof terms (IMO);
often bigger than using "match … as … in … return … with … end".
Furthermore they sometimes pollute your environnement, particulary when
you have mutual inductives (in these cases, automatically generated
induction principles are often useless).

In the previous situations, I cannot see why how and why "s" could think
of generating lemmas involving "hd" and "tl" which are not explicitly
involved in its definition.

So maybe you wanted something like:

"
CoInductive RichStream (A: Type): Type :=
{hd: A;
 tl: RichStream A
}.

Lemma s_hd: forall A (x: A) (xs: RichStream A), {|hd:=x; tl:=xs|}.(hd A)
= x.
Proof.
 now simpl.
Qed.

Lemma s_tl: forall A (x: A) (xs: RichStream A), {|hd:=x; tl:=xs|}.(tl A)
=
xs.
Proof.
 now simpl.
Qed.

Section Example.
 Variable A: Type.
 Variable x: A.
 CoFixpoint s : RichStream A := {|hd:=x; tl:=s|}.
End Example.
"

For sad reasons, Records cannot be used inside of mutual inductive
types, but as you can see, it can be used for at least this case.

Using "Set Implicit Arguments." will make all that even more convenient.
(you then could write "s.(tl)" instead of "s.(tl A)").

So, if you have only one constructor, we could do such things.

Now consider the following definition:

Parameters blue yellow green: Type.

CoInductive green_stream :=
| EverGreen: green -> green_stream -> green_stream
| Sun_and_Sky: yellow -> blue -> green_stream.

In this case the compounds cannot be guessed:

You have not these functions:
Definition green_: green_stream -> green := ….
Definition blue_: green_stream -> blue := ….
Definition yellow_: green_stream -> yellow := ….

(for example when "blue := False" and "green := True",
what would return
"CoFixpoint EverGreenForEver := EverGreen I EverGreenForever.
 Eval compute in (blue_ EverGreenForEver).
")

All you could do (IMO) would be to generate:
Definition EverGreen_green
: forall gs, (exists g s, gs = EverGreen g s) -> green :=….
or
Definition EverGreen_green
: green_stream -> option green := ….
or
Definition EverGreen_green
: forall gs, {g:green | exists s, EverGreen g s = gs} := ….
and so on;

or have some (awful?) structure
CoInductive green_stream :=
| EverGreen: immediate_green -> green_stream
| Sun_and_Sky: mixture -> green_stream
with immediate_green :=
{ green_: green;
  gnext: green_stream
}
with mixture :=
{ yellow_: yellow;
  blue_: blue;
  bynext: green_stream
}.
which could simplify the previous definitions.

In my opinion, too many things would be generated.

I do not know if "Function" and "Program" can manage coinductive types,
(if I well remember they require measure, so it shouldn't be the case);
if not, maybe would it be a good idea to extend it for your purpouse.
> 
> I can imagine that the above is not directly possible on the already 
> existing definition of Stream (because what I am asking should
> basically be a property of everything of type Stream). So I would
> also be content with having to define a new 'RichStream' type which
> has these properties. Such that I would have to define my stream
> using:
> 
> CoFixpoint s: RichStream A := x :: xs.
> 
> instead.
> 
> Would something like this be possible ?
> 
> Regards,
> 

One last thing, you can use simply sigma types

For instance:

Record Cons_spec (A: Type) (x: A) (xs: Stream A): Type :=
{ s: Stream A;
  s_hd: hd s = x;
  s_tl: tl s = xs
}.

Definition ConsRich: forall A x xs, Cons_spec A x xs
 := {|s := Cons x xs; s_hd := _; s_tl := _|}.
Proof.
 abstract prove_hd. (* since you tell you have such tactic *)
 abstract prove_tl. (* since you tell you have such tactic *)
Defined.

Now you have the following:
(ConsRich A x xs).(s_hd A x xs): hd (ConsRich A x xs).(s A x xs) = x
and
(ConsRich A x xs).(s_tl A x xs): tl (ConsRich A x xs).(s A x xs) = xs

or with implicit arguments
(ConsRich x xs).(s_hd): hd (ConsRich x xs).(s) = x
and
(ConsRich x xs).(s_tl): tl (ConsRich x xs).(s) = xs

It may seem heavy to deploy, but you may gain some time if you do not
remember the name of your lemmas, since:

Check ConsRich. will inform that the type is Cons_spec;
Print Cons_spec. will give you the name of your lemmas.
It may be better than "SearchAbout tl." if you have a lot of lemmas
involving tl.

I hope I gave you some good idea(s)
Regards