The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

> So for the first refinement creating a local definition of g, it created a
> transparent definition and I was able to complete the proof of that case. 
>  But
> for the second refinement, I was left with an opaque "g : X -> X" which was
> useless.  In both cases, g is just an auxiliary function to use in the
> inductive hypothesis, and wouldn't be of much interest outside the proof.
Yes if some part of the let contained proofs, then it is made opaque,
that's why [g] is transparent in the first case and opaque in the
second.
I see two workarounds to this:
- you say that defining g outside the proof wouldn't make much sense,
and you're right, but you can prove the "hole" in g as an intermediate
result in the proof and then you don't need refine anymore. In your
case, you need to know that [f (Some x) <> None] for all x:

  (* case f None = None *)
  assert (Habs : forall x, f (Some x) = None -> False).
  intros; assert (Some x = None). apply Hinj; congruence. discriminate.
  set (g := fun x => match f (Some x) as a return f (Some x) = a -> X with
                       | Some x' => fun _ => x'
                       | None => fun abs => False_rect _ (Habs x abs)
                     end (refl_equal _)).
  (* - extra part which I suggest *)
  assert (gdef : forall x, f (Some x) = Some (g x)).
  intro x; unfold g; set (Z := Habs x); clearbody Z.
  destruct (f (Some x)); auto; contradiction (Z (refl_equal _)).
  clearbody g.

  You can thus introduce the function g without holes, with set or
pose, and since reasoning with the definition of g will be slightly
awkward (because of the dependent elimination), I suggest that you
prove an indirect definition of g right away, once and for all, and
make g opaque afterwards.

- the second workaround is just to use refine to introduce not only g,
but g along with its specification, ie. g with what I called gdef
above, so basically you introduce {g | forall x, f (Some x) = Some (g
x)} instead of simply g and then you don't care about what g looks
like. Refine might not allow very complex holes though...

Hope this helps,

Stéphane

PS: with your definition of surjectivity, unless I'm mistaken, there
is no hope of proving the theorem for the bij case in axiom-free CIC
because you won't be able to build the inverse of a bijective
function. Using "Definition surjective f := forall y, {x | f x = y}."
would make it possible.

-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06