The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday 08 October 2010 01:58:51 Stéphane Lescuyer wrote:
> > I second Cedric's answer, you should try refine or Program. Note that
> > there is probably a nicer way to do wha
> 
> Sorry, premature sending :)
> 
> So I was saying, unless this is really what you want to do, you should
> maybe try and rethink what you're doing in order to avoid mixing
> definitions and proofs.
> A final note: you can use refine and still have proofs opaque, by
> using the abstract tactic: abstract (<tactic>) applies tactic, which
> should solve the current goal, and saves it as an opaque lemma. The
> downside is you need to prove every subgoal in one tactic, or one
> chain of tactic. If you have trouble with that particular point, ask
> Adam Chlipala :)
> 
> S.

Thanks for all the replies, it looks like the "refine" tactic is pretty much 
exactly what I was asking for, at least for definitions...

Definition inclusion_fun {X:Type} (S T:Ensemble X) (_:Included _ S T)
  (x:{x:X | In _ S x}) : {x:X | In _ T x}.
intros.
refine (match x with
  | exist x0 _ => exist _ x0 _
end).
auto with sets.
Defined.

Unfortunately, it looks like if I try to do a "refine (let g := fun ... in 
_)" 
with holes, the g becomes opaque when filling out the body of the let.  To 
give 
extracts of some recent work I've done:

Definition injective {X Y:Type} (f:X->Y) :=
  forall x1 x2:X, f x1 = f x2 -> x1 = x2.
Definition surjective {X Y:Type} (f:X->Y) :=
  forall y:Y, exists x:X, f x = y.
Definition bijective {X Y:Type} (f:X->Y) :=
  injective f /\ surjective f.

Inductive FiniteT : Type->Prop :=
  | empty_finite : FiniteT False
  | add_finite : forall X:Type, FiniteT X -> FiniteT (option X)
  | bij_finite : forall (X Y:Type) (f:X->Y),
    FiniteT X -> bijective f -> FiniteT Y.

Lemma finite_inj_surj: forall (X:Type) (f:X->X),
  FiniteT X -> injective f -> surjective f.
Proof.
intros.
revert f H0.
induction H.

(* case False *)
intros; red; intro.
induction y.

(* case option X, assuming true for X *)
intros.
(* remember (f None) as f0; destruct f0 *)
refine ((match (f None) as f0 return (f None = f0 -> _) with
  | Some a => fun (Heqf0:_) => _
  | None => fun (Heqf0:_) => _
end) (refl_equal _)).

(* case f None = Some a *)
(* pose (g := ...) *)
refine (let g := fun (x:X) => match f (Some x) with
  | Some y => y
  | None => a
end in _).
assert (surjective g).
apply IHFiniteT.
(* ... finish the proof of this case *)
admit.
admit.

(* case f None = None *)
refine (let g := fun (x:X) =>
(match f (Some x) as fx return (f (Some x) = fx -> _) with
  | Some y => fun _ => y
  | None => fun (Heqfx:_) => False_rect _ _
end) (refl_equal _) in _).
rewrite <- Heqf0 in Heqfx.
apply H0 in Heqfx.
discriminate Heqfx.

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