The Coq mailing list

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

Hello Dmitry,

Thanks for reference to convoy pattern, I forgot about it.
As for first part of question, in my particular case things are more complex,
so it is pretty difficult to do everything by hands, so I looked for automated
way to do it (something like "dependent refine" tactic).

Sincerely,
Kirill Taran

On Sun, May 11, 2014 at 2:48 PM, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

> So, I want to have proof of subgoal 1 when I prove subgoal 2. Is it
> possible?

Parameter X Y : Prop.
Parameter callx : X -> bool.
Parameter cally : Y -> bool.

Example first : bool.
refine (andb (callx _) (cally _)).
(* here Coq focuses on goal X *)
Admitted.

Example second : bool.
refine (let y := _ in andb (callx _) (cally y)).
(* here Coq lets me construct term of type Y *)
admit.  (* pretend we've constructed it *)
(* here:
1 subgoal
y : Y
_____________(1/1)
X
*)

  There is one problem left: even if one takes concrete
X, Y, and provide real value, it won't be present in
hypotheses.  There'll be "y : nat" (for example), but
without value, unlike when "pose (y := 123)" is issued.

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

  Here you can use "convoy pattern" described in CPDT.