The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

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.