I have a function
Definition fo_prop_of_cons (Sigma : global_env) (ind: term)
which outputs the reification of the fact that, if
ind is a inductive declared in the global environment
indis of the form
Cis a constructor of
C'are two constructors of
In all the other cases (e.g.,
ind is not an inductive in
Sigma), my function outputs the reification of
For instance, if
ind is the inductive associated to reification of
nat is declared in
Sigma), then the output will be the refication of the formula
(forall (x : nat), (x = O) \/ (exists k, x = S k)) /\ (forall (x : nat), S x <> O) /\ (forall (x y:nat), S x = S y -> x = y)
ind is associated to the reification of
list nat, I'll obtain the reification of:
(forall (l : list nat), l = nil \/ (exists (x : nat) (l0: list nat), l = x :: l0 )) /\ (forall (x : nat), (l : list nat), x :: l <> nil) /\ (forall (x x' : nat) (l l' : list nat), x :: l = x' :: l' -> (x = x') /\ (l = l'))
Actually, the name of the function means that it quotes first-order predicates satisfied by the constructors of an inductive (actually, it works with mutual inductive blocks, but it does not handle parameters/indices yet). I have several questions related to this:
1) How do I prove the following property?
Theorem fo_prop_ind_proved : forall (Sigma : global_env_ext) (Gam: context) (ind: term) , Sigma ;;; Gam |- fo_prop_of_cons Sigma.1 ind : Prop_reif.
Prop_reif is the reification of
I don't know if the typing of inductives is fully taken cared of in
MetaCoq now, but I don't want to write a reified proof of this fact. Is there a nice way to handle with the TemplateMonad (using the
2) Is it possible to ignore MetaCoq altogether and write
fo_prop_of_cons in Ltac/ssreflect? (I guess it should be possible in OCaml...)
2) In Ltac/ssreflect I would assume not. Probably in ocaml yes.
1) Do you need to know it's well-typed? Can't you just unquote the term and let the Coq type checker do it on its own?
(Or rather do you need to prove it's well-typed?)
Otherwise you can indeed use
tmLemma to prove somthing using an obligation.
@Théo Winterhalter Do I need to know that it is well-typed? Good question. I'll try to use
tmLemma first to see , but it is possible that yes, I just need to prove that
fo_prop_of_cons ind holds case-wise but that it is unnecessary to have a generic proof of this fact.
Btw, is the typing of inductives fully reified in MetaCoq now? (positivity condition, etc)
Not the positivity condition, I think there is something, but it's not complete. cc @Matthieu Sozeau
Positivity is formalized now, yes. Only it disallows nested inductive types for now.
I would hope you don't have to prove injectivity of type constructors etc... in MetaCoq (at least it's probably going to be a consequent proof endeavor), but can rely on injection/congruence tactics to discharge each instance of the lemmas.
Well, actually, I'm ok with anything which efficiently proves the injectivity of the type constructor. But I think it was necessary to use MetaCoq (or OCaml) for the statement of the injectivity to be automated. I guess I'll need to modify a few things so that I obtain a tactic morally equivalent to "Unquote (fo_prop_of_cons ind)" . Once it is done, it won't be difficult to prove it.
To give a little context, I'm doing this while working SMTCoq Project. SMTCoq takes a Coq goal
G to a statement
G' which is understandable by a SMTSolver. This SMT solver (hopefully) outputs a certifcate
C telling us that
G' holds. Then SMTCoq tries to convert
C into a Coq proof term
G. Of course,
C' needs to be a first-order formula.
For now, when we convert formulae using inductives, the SMTsolver doesn't know that the constructors are injective, and related statements. The idea would be to obtain a tactic that (1) scan the goal
G to list all the constructors appearing in it (2) asserting the "first order" properties of all these constructors and (3) proving it (on may imagine some variants, e.g. the possibility for the user to specify the constructors they want to be scrutinized). Thus, along with
G one could send to the SMTsolver useful information on the inductives that it would otherwise not "guess"/take into account.
Yes, I agree with you, you need a metalanguage to generate the statement, and MetaCoq should fit perfectly here
Last updated: Dec 07 2023 at 17:01 UTC