The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday 09 October 2010 02:04:51 Stéphane Lescuyer wrote:
> > 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.

I think that's the workaround I already used in my proof.  That really 
reduces 
the usefulness of refine, though.

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

As I already noted, that would tend to get cumbersome if g is defined by 
cases.  
My specification of the first g, if it had required holes, would be something 
like:

forall x:X, {y:X | f (Some x) = Some y \/ (f (Some x) = None /\ y = a)}

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

Well, my primary interest in coq is in formalizing mathematical proofs and 
not 
in computability, so I don't hesitate to use things like 
constructive_definite_description, functional_extensionality, 
proof_irrelevance, etc.  On the other hand, as a specialist in algebraic 
geometry, I *am* interested in which results can be proved in a topos, i.e. 
without classic or choice.  And the statement that every surjective function 
has a right inverse as above is essentially equivalent to choice.  (Although 
I 
did prove a finite_choice without assuming choice, so the two are equivalent 
modulo c_d_description for finite codomains.)  But you could replace 
"bijective" with "invertible" in the definition of FiniteT -- I already 
proved 
they're equivalent modulo c_d_description and the proof of finite_inj_surj 
would probably become CIC axiom-free.

Inductive invertible {X Y:Type} (f:X->Y) : Prop :=
  | inverse_func_intro : forall g:Y->X,
    (forall x:X, g (f x) = x) -> (forall y:Y, f (g y) = y) ->
    invertible f.

Actually, it might not be a bad idea to make that replacement in any case -- 
it would save me a lot of applications of bijective_equiv_invertible, and in 
proving things like "FiniteT X -> FiniteT Y -> FiniteT (X+Y)" I was 
essentially constructing inverse functions to "option (X + Y) -> X + option 
Y" 
piecemeal anyway.  I'd just have to make the inverses explicit, which is a 
good thing.
-- 
Daniel Schepler