Stream: MetaCoq

Topic: Equivalence of single-constructor inductives with definition


view this post on Zulip Karl Palmskog (Nov 02 2023 at 11:55):

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)

view this post on Zulip Karl Palmskog (Nov 02 2023 at 11:57):

at least naively, one might sometimes want both the Inductive version and non-Inductive without having to write code and do the <-> proof.

view this post on Zulip Yannick Forster (Nov 02 2023 at 11:58):

By turning it into a telescope of existss? I think that makes sense, yes, and just generating the equivalence proof should also not be too hard

view this post on Zulip Yannick Forster (Nov 02 2023 at 11:58):

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

view this post on Zulip Yannick Forster (Nov 02 2023 at 11:58):

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)

view this post on Zulip Karl Palmskog (Nov 02 2023 at 12:00):

OK, good to know, thanks!

view this post on Zulip Yannick Forster (Nov 02 2023 at 12:00):

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)

view this post on Zulip Meven Lennon-Bertrand (Nov 02 2023 at 12:21):

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?

view this post on Zulip Gaëtan Gilbert (Nov 02 2023 at 12:32):

https://github.com/HoTT/Coq-HoTT/blob/45af5465b467c0ae9386a2869af73864e8815ea4/theories/Basics/Tactics.v#L707

view this post on Zulip Yannick Forster (Nov 02 2023 at 12:39):

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

view this post on Zulip Yannick Forster (Nov 02 2023 at 12:49):

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

view this post on Zulip Yannick Forster (Nov 02 2023 at 12:58):

(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