The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

Adam, Guillaume:  thanks for the quick responses. This is a nice trick to 
learn---thanks!

But, it isn't exactly what I am looking for. 

Say I want to write this function (using the same definitions of A, B and foo 
as below):

Definition bar (a:A) (b:B a) : (B a * unit) := 
  (b, match a with 
        | One => foo b 
        | Two => tt
      end).

Using the trick, I can transform it like so:

Definition bar2 (a:A) : (B a) -> (B a * unit) := 
  match a as a0 return (B a0 -> (B a0 * unit)) with 
    | One => fun b => (b, foo b) 
    | Two => fun b => (b, tt)
  end.

I really would like to maintain the syntactic structure of bar, and this 
trick destroys the structure.
So, any other suggestions?

Thanks!
-Nik
 

> -----Original Message-----
> From: Adam Chlipala 
> [mailto:adam AT chlipala.net]
> Sent: Tuesday, November 09, 2010 2:18 PM
> To: Nikhil Swamy
> Cc: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Equality-witnessing coercions?
> 
> Nikhil Swamy wrote:
> >
> >
> > The example below illustrates what I'd like to accomplish.
> >
> > Inductive A : Type :=
> >
> > | One : A
> >
> > | Two : A.
> >
> > Inductive B : A -> Type := .
> >
> > Definition foo (b: B One) := tt.
> >
> > Definition bar (a:A) (b:B a) : unit :=
> >
> > match a with
> >
> > | One => foo b (* some way to coerce b's type to (B One)? *)
> >
> > | Two => tt
> >
> > end.
> >
> 
> A simple rearrangement of the function definition gets this to go through.
> What looks like magic actually works because this change makes it possible 
> to
> use an inferred [return] clause to express the dependency between [a] and
> [b].
> 
> Definition bar (a:A) : B a -> unit :=
> match a with
> | One => foo
> | Two => fun _ => tt
> end.
> 
> This and other dependent typing "tricks" are one of the main subjects of
> CPDT (http://adam.chlipala.net/cpdt/).