The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 01/08/2013 13:44, Dmitry Grebeniuk a écrit :
> 1. Why the body is hidden?

I don't know.

> 2. How to "reveal" it?  I suspect I need to change the way I introduce
> ba', but I can't find the correct way to do it.

You can split the refine. For example:

refine (let ba := buf.(buf_arr) in _).
refine (
  let arr_ofs := ba.(arr_ofs) in
  let arr_len := ba.(arr_len) + sz in
  let file_ofs := ba.(file_ofs) in
  let H1 :
    arr_ofs >= 0 /\ arr_len >= 0 /\ arr_ofs + arr_len <= bs2
  := _ in
  let H2 : file_ofs mod block_size = arr_ofs := _ in
  _
).
(* Solve the first two goals *)
split.
destruct ba.
simpl.
spl.
assumption.
(**)
split.
simpl.
destruct ba.
simpl in *.
spl.
unfold arr_len0.
omega.
(**)
simpl in Hsz_fits.
subst ba.
destruct w as [ w0_file w0_buf W0buffile ]. simpl in *.
subst fil buf fil'.
destruct w0_buf; simpl in *.
spl.
unfold arr_len0, arr_ofs0.
omega.
(**)
destruct ba. simpl in *.
assumption.
(* Now we can build ba' without hole *)
refine (
      let ba' :=
        {| arr_ofs := ba.(arr_ofs)
         ; arr_len := ba.(arr_len) + sz
         ; file_ofs := ba.(file_ofs)
         ; Aarr := H1
         ; Aalign := H2
         |}
      in _
).
(* back to the original situation, with ba''s body explicit *)

I don't know if it helps; it might be that you'll be stuck later for the
very same reason than the monolithic refine was hiding ba''s body.


Cheers,

-- 
Stéphane