Good practice for constructing elements of record types · Coq users

Record rec (A : Type) (a : A) (P  : A -> Type) :=
Build_rec { 
    field1 : exp(A, a, P)
    field2 : exp2(A,a, P, field1)
    field3 : exp3(A,a,P, field1, field2)
 }

so I want to construct an element of rec A a p, and I want to construct all the fields separately on their own as a sequence of separate lemmas. some of them are meant to be proof-irrelevant and i want to define them with a Qed style label rather than the defined keyword. and I don't want to use the abstract tactical if i can avoid it. What i'm wondering is, if there is an easy way to simply get the types exp(A, a, P), exp2(A,a,P, field1) etc from the definition of the record. I can always manually write

Definition data1 : exp(A, a, P) := ....
Proposition data2 : exp2(A, a, P, data1)
but like, if the expresssions are complicated then this is a lot to read, and i end up having to copy-and-paste a lot.
I am looking for some kind of construct that lets me write something like
Definition data1 : type_of field1 in rec A a P := ...
Proposition data2 : type_of field 2 in rec A a P with field1 := data1

Li-yao (Jan 03 2022 at 21:14):

Record Rec (A : Type) (P : A -> Prop) : Type :=
  { f1 : A
  ; f2 : P f1
  }.

Definition next_field_of {A : Type} {P : A -> Type} (_ : forall x : A, P x) : Type := A.

Definition g1 : next_field_of (@Build_Rec nat (gt 3)). Admitted.
Definition g2 : next_field_of (@Build_Rec nat (gt 3) g1). Admitted.

Patrick Nicodemus (Jan 03 2022 at 22:15):

ok this took me a minute to understand, my example was really bad for your question here lol

Patrick Nicodemus (Jan 03 2022 at 22:16):

Paolo Giarrusso (Jan 04 2022 at 19:11):

Have you considered using Program (with opaque obligations), instead of the abstract tactic?

Paolo Giarrusso (Jan 04 2022 at 19:13):

Otherwise, the intermediate definitions of next_field_of and especially g1 and g2 might interfere with any proofs about the concrete record.

Patrick Nicodemus (Jan 04 2022 at 19:15):

Karl Palmskog (Jan 04 2022 at 19:16):

Patrick Nicodemus (Jan 04 2022 at 19:17):

I can always just unfold next_field_of whenever it occurs in a proof, right? I see that this will add some kind of extra complication, is that what you mean?

Paolo Giarrusso (Jan 04 2022 at 19:42):

Yes that's what I meant; it's more annoying if your proof goes from auto to <unfold 10 things; auto>

Paolo Giarrusso (Jan 04 2022 at 19:43):

Program Definition foo : rec := {| field1 := …; field2 := … |}.
Next Obligation. <proof for field3>. Qed.

Paolo Giarrusso (Jan 04 2022 at 19:44):

by default Program has a few extra smarts, but Unset Transparent Obligations. Unset Program Cases. Obligation Tactic := idtac. disable the most annoying ones.

Gaëtan Gilbert (Jan 04 2022 at 19:57):

Notation next_field_of c := ltac:(let t := type of c in match t with forall _ : ?A, _ => exact A end).

Definition g1 : next_field_of (@Build_Rec nat (gt 3)).
(* 1 goal: nat *)

Paolo Giarrusso (Jan 04 2022 at 20:06):

I was more concerned about unfolding g1 and g2, as next_field_of seems less likely to get in the way.

Paolo Giarrusso (Jan 04 2022 at 20:07):

OTOH... @Patrick Nicodemus do you want separate definitions just to separate obligations (then Program is enough) or for other reasons? I inferred the former, but if you want the latter great.

Patrick Nicodemus (Jan 04 2022 at 20:12):

Um, i don't exactly know what an obligation is. I am doing pure mathematics and my reason for wanting to separate the functions, maps etc from the propositions and proofs is to improve compilation speed, prevent automatic solving tools from unfolding the proofs of theorems unnecessarily, communicate to the reader the difference between data of a construction and its properties...

Paolo Giarrusso (Jan 04 2022 at 20:23):

your last requirement makes sense and might not be satisfied by Program (subjective). For the first two, Next Obligation. <proof> Qed. will satisfy your 2nd requirement (and maybe the 1st), but not the 3rd, since the produced proof term will be similar to what you’d get from abstract.

Paolo Giarrusso (Jan 04 2022 at 20:25):

basically in my example you’d get a generated top-level symbol (with a name like foo_obligation1 with an qed-ed definition (that will never be unfolded), and foo’s body will mention, say, field3 := foo_obligation1.

Patrick Nicodemus (Jan 04 2022 at 20:26):

Paolo Giarrusso (Jan 04 2022 at 20:26):

Paolo Giarrusso (Jan 04 2022 at 20:28):

many (me included) advocate for using tactics in Qed-ed proofs in Prop, and proof terms elsewhere, with some exceptions — but that’s a proof engineering question, not something imposed by Program.

Stream: Coq users

Topic: Good practice for constructing elements of record types

Patrick Nicodemus (Jan 03 2022 at 20:39):