The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday, January 20, 2012 03:02:30 AM AUGER Cédric wrote:
> By the way, I remember that some months (year?) ago, you said that
> you never had problems with the "inversion" tactic. Did you changed
> your mind, or do you just want to write terms to compute without using
> the tactic system?

I still don't have problems with using "inversion" -- but I do have problems 
with using tactics to construct data parts of definitions.  (Although, these 
definitions came out of some experiments I've been doing lately, to see how 
to 
unfold the results of the inversion tactic to eliminate the intermediate 
equality propositions.)  Plus, if I try using "dependent inversion" to 
outline 
the skeleton before writing it out in full, that sometimes generates 
intermediate JMeq statements.  And I think sometimes it uses the JMeq_eq 
axiom 
internally -- and that can destroy the possibility of directly computing 
using 
the resulting definitions.  I get similar problems if I try using the Program 
system to write a definition without all the type casts and let it generate 
type casts and equality obligations.

Overall, the resulting term involving vectorS_inv isn't *that* ugly, so I 
think I'd rather put up with that than write 2^n notation declarations, or 
use 
what you suggested.  On the other hand, it could be nice to define one 
alternative notation to allow me to drop "as _".

So I guess my previous message stated things a bit backwards: in fact, I had 
the desire to write vectorS_match expressions, and have a back end which 
would 
easily simplify when applied to a vector_cons expression.  A plus would be to 
have the expressions have nice Ocaml extractions (i.e. having "assert false" 
in the invalid cases, rather than some expression involving Obj.magic).  I 
already had a vectorS_inv function satisfying the first criterion some time 
ago, and I think I may have already posted that version.  It was only 
yesterday that I had an inspiration on how to refine it to satisfy the second 
criterion as well.

In case you're interested, and you can't read the mess of vectorS_inv which 
involves several "convoys" of P and Pcons through matches, the basic idea was:

Definition vector_tl {X:Type} {n:nat} (v:vector X (S n)) : vector X n :=
match v in (vector _ m) return
  (match m with
  | 0 => unit
  | S m' => vector X m'
  end) with
| vector_nil => tt
| vector_cons _ _ t => t
end.

This satisfies the first criterion but not the second.  (The Vector_nil case 
extracts to "Obj.magic ()".)

To make the extraction nicer, rewrite instead:

Definition vector_tl {X:Type} {n:nat} (v:vector X (S n)) : vector X n :=
match v in (vector _ m) return
  (match m return Prop with
  | 0 => False
  | S _ => True
  end ->
  match m return Type with
  | 0 => Empty_set
  | S m' => vector X m'
  end) with
| vector_nil => False_rect Empty_set
| vector_cons _ _ t => fun _:True => t
end I.

So, we provide a context Prop which in the correct case reduces to True, and 
is ignored.  But in the incorrect case, it reduces to False, allowing us to 
"raise an exception" instead of returning a garbage value.  Then in the 
extraction, that context Prop is eliminated; and since the incorrect case 
extracts to "assert false", I guess somehow the extraction process realizes 
that the different return type of empty_set vs. 'a1 vector doesn't matter, so 
no Obj.magic is needed.
-- 
Daniel Schepler