The Coq mailing list

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

Le Wed, 28 Jul 2010 16:44:31 +0200,
Jean-Marie Madiot 
<madiot AT gmail.com>
 a écrit :

> Hello all,
> 
> I'm currently using the Record syntactic sugar and I was wondering if
> it is possible to build a record instance from an existing one while
> modifying only a few fields. To be clear, I have a record with many
> fields, like this:
> 
>  Record rec := rec_cons {
>    rec1 : nat;
>    rec2 : nat;
>    rec3 : nat;
>    recdots : nat
>  }.
> 
> (* and I built an instance of rec: *)
> 
>  Definition r : rec := rec_cons 1 2 3 4.
>  Definition r2 : rec := {| rec1 := 1; rec2 := 2; rec3 := 3; recdots
> := 4 |}. (* same thing *)
> 
> (* now I want to make an instance based on r but modifying only one
> field, like that: *)
> 
>  Definition r' : rec := {| r with rec2 := 20 |}.
> 
> But it does not work like that. (This is inspired from the ocaml
> syntax). Is there another way? I know I can do such a thing by
> defining my own function depending on my record type and which field I
> want to alter -- and even setting up a notation for it -- but since
> records are already just syntactic sugar, maybe it is possible to have
> something more general?
> 
> Or maybe it interferes with the existing notation system?
> 
> Regards,
> 
> Jean-Marie

I hoped that someone more competent than me, replied to you;
but it is not the case.
For what you whish, the only way I see to do it in coq would be with
an automatic code generation scheme; as it is the case with inductive
structures; when you declare a structure, induction principles are
automatically generated (unless, you disable this functionnality).

By hacking coq, it should be possible to have another automatic
generation; say when the type has only one constructor, generate field
modifiers.

(*Inductive prod (A B: Type) := pair A -> B -> prod A B.*)
Record prod (A B: Type) := {| pi1: A; pi2: B |}.
>> currently autogenerated:
prod_rect = 
fun (A B : Type) (P : prod A B -> Type)
  (f : forall (a : A) (b : B), P (pair a b)) (x : prod A B) =>
match x as x0 return (P x0) with
| pair x0 x1 => f x0 x1
end
     : forall (A B : Type) (P : prod A B -> Type),
       (forall a b, P (pair a b)) -> forall (x : prod A B), P x.
>> idem for prod_rec and prod_ind
>> could be autogenerated:
change_pi1 =
fun (A B : Type) (p: prod A B) (a : A) =>
match p with
| {| pi2 := b|} => {| pi1 := a; pi2 := b |}
end

change_pi2 =
fun (A B : Type) (p: prod A B) (b : B) =>
match p with
| {| pi1 := a|} => {| pi1 := a; pi2 := b |}
end
===============================================================

Yet it is not the case.
note that:
* to deal with dependent types complicates the story
  Record nat_sum {A: Type} (P: nat -> A -> Prop)
                           (Q: nat -> Prop)
                           (R: A -> Prop):
         Prop :=
  {| witness: A;
     index: nat;
     proof_p: P index witness;
     proof_q: Q index;
     proof_r: R witness
  |}.

  should generate only two modifiers:
 change_witness: forall A (P: nat -> A -> Prop) Q R (ns: nat_sum P Q R),
                 forall w, P ns.(index) w -> R w -> nat_sum P Q R
 change_index: forall A (P: nat -> A -> Prop) Q R (ns: nat_sum P Q R),
               forall i, P i ns.(witness) -> Q i -> nat_sum P Q R
 which may be tricky to understand.
* direct autogeneration of notations is possible, but it is not in the
  spirit of coq implementation (notation are mainly used for function
  application; so a notation here would rather rely on change_xxx
  autogenerated functions).
* to modify many fields, you will have to chain these functions;
  generating 2**n functions to modifiy all the possible sets of fields
  is not smart.
* having a primitive to do field modifications without performing a
  pattern matching would imply modifications of the coq kernel,
  which I think is not wishable.
* I think always generating these functions will pollute even more coq
  internal environnement.
  Think of bool_ind, bool_rec and bool_rect, which are never used,
  as it is not recursive,
  and eq_rec, eq_ind and eq_rect which are used every time you perform
  a rewrite or subst and pollute the proof term.
  (with a notation: "a = b" := (eq _ b a) and "rewrite H" := (case H),
   the proof terms would often really be nicer).
* More generally, I think that Coq really lacks some meta-facilities.
  Allowing things such as:
  "Meta change_generation (r: coq_record) :=
        for f in (coq_field r)
        <<Definition change_>>(coq_name f)<< (r: >> (coq_type r) <<)
        (f:>> (coq_type f) <<): >> (coq_type r) << := match ..."
  and then:

  "Record coord := {| abs: positive; ord: positive|}.
   change_generation coord. (* generates change_abs and change_ord *)
  "
  would be rather cool, and you gain a lot of control on the coq
  environnement.
  I have already wished such a feature, for example for tactics
  (which are meta-functions, but Ltac is not enough powerfull).
====================================================================
My conclusion is that you can't do it without patching your coq version.
As you said yourself, you can always define these functions and
notations for that, but you have to do it for each structure.
If you think that this feature should really be part of coq, send a
request feature to the bug tracking system.

Another awful solution would be to manage the "meta" part yourself, eg:

Definition make_record: list (string * Type) : Type :=
 some_awfully_coded_map_from_fields_to_types

so that you can yourself generate your own field modifiers

and all subjacent functions; unless you have a good ideas of
improvement, it will cost a lot of time, performance and readability.