I'm not sure if this even makes sense, but could one show/automate in MetaCoq that single-constructor (non-recursive) `Inductive`

can be rewritten to an equivalent non-`Inductive`

definition? (I guess this mainly is interesting for things living in `Prop`

)

at least naively, one might sometimes want both the `Inductive`

version and non-`Inductive`

without having to write code and do the `<->`

proof.

By turning it into a telescope of `exists`

s? I think that makes sense, yes, and just generating the equivalence proof should also not be too hard

Proving that the resulting definition is well-typed might be tricky, but doable

Proving that the generated equivalence proof is indeed an equivalence proof might be hard, not sure (but also not necessary - if it works it works)

OK, good to know, thanks!

If I'd have to get something working quickly, I would do the generation of the definition in MetaCoq, generate the theorem statement in MetaCoq, and then generate the proof of the theorem in Ltac)

If I remember correctly, there is some support for things like this in Coq-HoTT (where a lot of theorems are proven for Σ-types, but you want to use records in practice, so there is infrastructure to go back and forth between the two). Have you looked into it?

Yeah, that's more or less the (proof relevant) version of the tactic I had in mind. MetaCoq then could come in to generate the nested Sigma type automatically

```
From Coq Require Import List.
Import ListNotations.
From MetaCoq.Template Require Import All Loader.
From MetaCoq.Utils Require Import bytestring.
Import MCMonadNotation.
Open Scope bs.
Fixpoint generate_sigma (ctx : context) :=
match ctx with
[] => <% unit %>
| [c] =>
c.(decl_type)
| c :: ctx =>
tApp <% sigT %>
[c.(decl_type); tLambda c.(decl_name) c.(decl_type) (generate_sigma ctx)]
end.
Definition sigmaify {A} (a : A) :=
p <- tmQuoteRec a ;;
match p.2 with
| tInd ind _ => match lookup_inductive p.1 ind with
Some (mind, oind) => match oind.(ind_ctors) with
| [c] => tmUnquoteTyped Type (generate_sigma (MCList.rev (fst (decompose_prod_assum [] c.(cstr_type))))) >>= tmPrint
| _ => tmFail "not a record"
end
| _ => tmFail "error"
end
| _ => tmFail "not a record"
end.
Record test := { proj1 : nat ; proj2 : proj1 = 0 ; proj3 : exists x y, x = proj1 /\ y = proj2 }.
MetaCoq Run (sigmaify test).
```

(does the wrong thing if the record has parameters, but not hard to fix. The number of parameters is stored in `mind.(ind_npars)`

Last updated: Jul 23 2024 at 20:01 UTC