The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Birgit Fruth wrote:
> Thank you both. This helped a lot.
>
> But is there a possibility to give a value to a matching construct 
> like I use in "autotree", too? I'd like to use it for Lemma 
> "always_q_autotree".
> Or have you a suggestion how I can get rid of these dependencies in 
> the arguments?
> I' ve search already in the Coq'Art book, but I couldn't find something.
>
> I have to do this at university and I really want to learn Coq but 
> there's no one here, who has experience with Coq (but some who'd like 
> to have). So I would be grateful if you could help me again. Thanks 
> for your help!
>
> Birgit
Dear Birgit,

I don't know whether you can get rid of these dependencies in the 
arguments.  For now, I suggest you accept the
extra burden of having to give some of the arguments to help the system 
reduce the dependencies or to
define an extra lemma that is specialized for your automaton:

Definition Atomic_tree_intro' := Atomic_tree_intro A0.

and then use the new definiton for all the proofs you want to do about 
your specific automaton.

Concerning your "always_q_autotree", the proof can be done, but you need 
to use a decomposition lemma
instead of unfold: this is a general rule of thumb when reasoning about 
co-recursive functions.  After your
unfold, the pattern-matching construct is still not exposed: it is 
inside a cofix construct.

You do have a decomposition lemma in your file, so use it!

Yves