Complexity of proof terms generated by the inversion tactic

[greenrd]

If I use Proof. ... Defined. to build a term, and I use inversion in
the proof, the generated proof term can be quite complicated. If I use
"info inversion" to see what tactics are being used in that proof step,
the output is quite long. So it looks like it would be a lot of work
for me to understand how the inversion tactic works in this particular
situation.

Is there any way, apart from using the simple inversion tactic, to make
the proof terms less complicated for a proof involving inversion? Or at
least, in some sense easier to work with in a subsequent proof
involving that definition?
--
Robin

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Adam Chlipala-3]

Robin Green wrote:
> Is there any way, apart from using the simple inversion tactic, to make
> the proof terms less complicated for a proof involving inversion? Or at
> least, in some sense easier to work with in a subsequent proof
> involving that definition?
>  

My advice is never to reason after-the-fact about terms built with
tactics.  If you really need after-the-fact reasoning, implement the
inversion lemma yourself with a literal proof term.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Conor McBride-2]

Hi Robin

On 4 Jul 2009, at 02:57, Robin Green wrote:

> If I use Proof. ... Defined. to build a term, and I use inversion in
> the proof, the generated proof term can be quite complicated. If I use
> "info inversion" to see what tactics are being used in that proof  
> step,
> the output is quite long. So it looks like it would be a lot of work
> for me to understand how the inversion tactic works in this particular
> situation.
>
> Is there any way, apart from using the simple inversion tactic, to  
> make
> the proof terms less complicated for a proof involving inversion? Or  
> at
> least, in some sense easier to work with in a subsequent proof
> involving that definition?

James McKinna and I have a technique which helps in this situation,
which we use in Epigram. After all, Epigram programs really are
proof terms built with inversion, but the system never shows you
the gory mess! Here's the plan. (I write (xs : Xs) for a telecope of
Pi-binders.)

Suppose you're thinking of writing some function.

  f : (xs : Xs) -> T[xs]

Before you start, declare a "phantom" inductive family

  Compute_f : (xs : Xs) -> Set
  return_f : (xs : Xs)(t : T[xs]) -> Compute_f xs

and define the function which unpacks it, behaving like this.

  call_f : (xs : Xs) -> Compute_f xs -> T[xs]
  call_f xs (return_f xs t) = t

Now do your tactic-driven programming to develop

  compute_f : (xs : Xs) -> Compute_f xs

You'll find that you'll need return_f to return a value and
call_f to appeal to an inductive hypothesis. Each return_f
will look a bit like one line of a functional program.

Once you've done this, you'll see that you can define f by

  f xs = call xs (compute_f xs)

And that's it!

Things to note

(1) The computational behaviour of these things is like
pattern matching: if compute_f ps = return_f ... e, then
f ps = e.
(2) The revolting mess of elimination which survives
evaluation on open terms is always inside a call_f, and
you can see what it means by looking at *which* call_f.
E.g.

  plus (S x) y ---> S (call_plus x y (nat_rec ... x))

Whenever you see (call_plus x y ugly), you know that's
(plus x y). You don't need to notice that the ugly
thing itself is really some function application.

I hope that's made some sense. Usually when I try to
explain this, it appears to be utterly pointless. But
truth to tell, I haven't folded a definition since 1998.

Hope this helps

Conor

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[roconnor]

On Sat, 4 Jul 2009, Robin Green wrote:

> If I use Proof. ... Defined. to build a term, and I use inversion in
> the proof, the generated proof term can be quite complicated. If I use
> "info inversion" to see what tactics are being used in that proof step,
> the output is quite long. So it looks like it would be a lot of work
> for me to understand how the inversion tactic works in this particular
> situation.
>
> Is there any way, apart from using the simple inversion tactic, to make
> the proof terms less complicated for a proof involving inversion? Or at
> least, in some sense easier to work with in a subsequent proof
> involving that definition?

I'm not sure why no one mentioned this, but you can write:

Derive Inversion MyInversionLemma ...

to automatically generate a new lemma called "MyInversionLemma". Then you
can use this lemma in your proof.

Check the manual for how to use "Derive Inversion".

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club