The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have two related questions:

Given a record like

  Record foo := { bar : Type }.

(or a more complicated one with arguments and multiple fields, or possibly even any inductive type with one constructor which lives in [Type]),

First, would it break CIC (or cause any other problems) if [f : foo] were made convertible with [Build_foo (bar f) : foo]?  (Is this properly named "eta conversion of records", or is it called something else?)  I suspect it wouldn't cause any problems, because I can always do something like

  let t := fresh in destruct f as [ t ];

    change (Build_foo (bar (Build_foo t))) with (Build_foo t) in *;

      set (f := Build_foo t) in *;

        clearbody f; clear t.

in any proof in which I want [f] and [Build_foo (bar f)] to be convertible.  Admittedly, this adds an extra [match] in the proof/construction, but I don't think this is a big deal, because I think we can always "get rid "of the match by [destruct f] in any proof/construction (that is, after [intros], we can always move the match up to top level, I think).

However, I'm not completely confident in my argument, because I know that allowing this kind of match-less conversion on inductive types not in [Type] (such as [@eq]) leads to ill-typed terms and being able to prove proof irrelevance.

Second: Assuming that this would not cause problems, are there any plans to add this to Coq?

Thanks.

-Jason