The Coq mailing list

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

Arnaud,

This looks like really good feature.
In my current goal I need to restructure the whole function definition
in pretty unconvinient way to prove things without it, so I'll try it.

Sincerely,
Kirill Taran

On Mon, May 12, 2014 at 12:13 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Quick reply: for dependent subgoals, you can try the trunk.

Goal False.
Proof.
  refine (let x:=(_:~~False) in _).

(* 2 subgoals:  |- ~~False      x:=?4:~~False |- False *)

On 11 May 2014 15:51, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Also, finally I succeed with my initial problem.

Brief plot of my solution:

Definition complex_function : C -> C.
  (* "context" of my function body *)
  refine (Fix my_order_wf (fun _ => C)
    (fun x (call : forall y, y <<< x -> C) =>
       match x as x_ return (x = x_) -> C with
       | ... => fun xEq =>
         match x' as x'_ return (x' = x'_) -> C with
         | ... => fun x'Eq => _
         end eq_refl
       end eq_refl
    ));

  (* some bindings instead of "let" in code *)
  pose (x'   := ...);

  (* proof of correctness for first call: *)
  assert (call_1 :  x' <<< x) by
    (...).

  pose (x''  := call ... call_1);
  destruct ... as ... eqn:...;
  
  assert (call_2 : ... <<< x) by
    (...);

  pose (x''' := call ... call_2);
  destruct ... as ... eqn:...;
    
  refine (* result *).
Qed.

In fact it very resembles imperative programming:
"small" steps of manual assigning of values to variables, destructing, etc.
mixed with some "big" steps of refine.

Convoy pattern is used inside first "big" step for providing "context",
because I think it would be too dirty to refine manually Fix part (with pose and destruct).

Sincerely,
Kirill Taran

On Sun, May 11, 2014 at 4:39 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

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.