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*

```
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.
```

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

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

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

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

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

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

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?

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

but also `Program`

lets you write the much nicer:

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

by default `Program`

has a few extra smarts, but `Unset Transparent Obligations. Unset Program Cases. Obligation Tactic := idtac.`

disable the most annoying ones.

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 *)
```

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

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.

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...

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`

.

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`

.

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

any sorts

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: Jun 18 2024 at 00:02 UTC