Stream: Coq users

Topic: Good practice for constructing elements of record types


view this post on Zulip Patrick Nicodemus (Jan 03 2022 at 20:39):

let's say i have a record type, idk something like

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jan 03 2022 at 22:16):

this is perfect, i see what's happening, thank you

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:11):

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

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:15):

I haven't checked out Program, i have no idea about that tool.

view this post on Zulip Karl Palmskog (Jan 04 2022 at 19:16):

https://coq.inria.fr/refman/addendum/program.html

view this post on Zulip 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?

view this post on Zulip 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>

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:43):

but also Program lets you write the much nicer:

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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 04 2022 at 19:57):

you can use a notation instead of a definition, eg

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

then you don't need to unfold:

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 20:26):

does this tactic depend on the Prop sort or could it be used with other sorts?

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 20:26):

any sorts

view this post on Zulip 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.


Last updated: Jan 27 2023 at 02:04 UTC