The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello coq-club,

1) Is it possible to provide "dependencies" between subgoals of refine?

I am trying to define complex fixpoint via refine and combinator Fix for w.f. relations.
But I have two calls and second call uses results from first one.

For instance:
    Fix my_rel_wf (fun _ => nat)
        (fun x (call : forall y, y <<< x -> nat) =>
            match x with
            S x' => match (call x' __subgoal_1__) with

                    ... match (call y' __subgoal_2__) with
                        ...
                    end
            ...
            end
        end).
So, I want to have proof of subgoal 1 when I prove subgoal 2. Is it possible?

I guess that one workaround is to split one function into two mutual recursive functions,
but it takes some effort. And I am not sure that it is easy with Fix combinator.

2) Is it possible to propagate information from term, which is used to define function,
to subgoals?

For example, when I prove  subgoals I need to have hypothesis
which is result of pattern matching, e.g. that x = S x', but I haven't it.

Sincerely,
Kirill Taran