The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

By the way there are other way to achieve your goal, like this one:

Record sig_ {A: Type} (P: A -> Prop): Type := {
 ν: A;
 π: P ν
}.

Notation "{ x : T 'st' Π }" :=
 (sig_ (fun (x: T) =>  Π))
 (x at level 99, format "'[' {  x  :  T  '/' 'st'  Π  } ']'").
Notation "{ x 'st' Π }" := {x:_ st Π}
 (x at level 99, format "'[' {  x  '/' 'st'  Π  } ']'").
Notation "{ x '&' Π }" :=
 (sig_ (fun (_: x) => Π))
 (x at level 99, format "'[' {  x  '/' '&'  Π  } ']'").
Notation "{: x :}" := {|ν:=x|}.

Definition case_opt {A: Type} (o: option A)
: {unit & None = o}+{p st Some p = o}.
refine (
 match o with
 | Some a => inr _ {:a (*we are equal to some constant*):}
 | None => inl _ {:tt (*we are equal to None*):}
 end
).
Proof. (*we are equal to some constant*)
 split.
Proof. (*we are equal to None*)
 split.
Defined.

Definition f optA:=
  match case_opt optA with
  | inr v => Some (g (ν v) (π v))
  | inl _ => None  
  end.

Of course case_opt can be defined without tactics (but I prefer to
use it for the proof parts),
and you can use ascii notations instead (or no notation at all, if you
prefer).

The idea is to redefine a "specified" version of "match … with … end"
for option types.
sig_ is completely isomorphic to sig, but I don't remember if the
projections are defined for this type; and these notations are not all
defined in the standard library.

Le Wed, 13 Jul 2011 15:37:46 +0200,
Pierre Courtieu 
<Pierre.Courtieu AT cnam.fr>
 a écrit :

> Hi,
> The x inside the return is actually bound by the "as x" occurring
> just before.
> 
> Indeed (eq_refl optA) is the proof of optA=optA. but the return clause
> does not specify the type of the match, it specifies the type "scheme"
> of each of its branches. The type of the match is computed by applying
> the scheme to the matched term (ie optA), which gives ((fun x=> optA=x
> => nat) optA) i.e. optA=optA -> nat.
> 
> Indeed if you remove the refl_equal:
> 
> Variable A:Set.
> Definition f (optA : option A) :=
> (match optA as x return optA = x -> nat with
>  | Some a => (fun p => O)
>  | None => (fun p => 1)
> end).
> 
> Check f.
> 
> you obtain that f is of type optA=optA -> nat.
> 
> Hope this helps,
> Pierre
> 
> 2011/7/13 Marco Servetto 
> <marco.servetto AT gmail.com>:
> > Hi, thank you, the return "trik" works with minor twiking.
> > However it really leave me in the total misunderstanding of why it
> > works:
> >
> > I was thinking (eq_refl optA) to produce a proof for optA=optA, not
> > for optA=x, moreover x looks out of
> > scope outside the parenthesis of the match... may be I have to study
> > what exactly the return does.
> >
> >> Definition f (optA : option A) :=
> >> (match optA as x return optA = x -> nat with
> >>  | Some a => (fun p => O)
> >>  | None => (fun p => 1)
> >> end) (eq_refl optA).
> >
> > And again,  thank you all!
> > Marco.
> >
> >
>