Pierre Vial (Sep 29 2020 at 07:31): Pierre Vial (Sep 29 2020 at 07:31):Hello folks!
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 Sigma, then:
t of ind is of the form C(a1,...,an), where C is a constructor of indC(a1,...,an)=C'(a'1,...a'n') where C and C' are two constructors of ind, then C=C', n=n' and ai=a'i for all i. In all the other cases (e.g., ind is not an inductive in Sigma), my function outputs the reification of True.
For instance, if ind is the inductive associated to reification of nat (and 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)
If 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.
where Prop_reif is the reification of Prop?
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 obligation mechanism)?
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...)
Théo Winterhalter (Sep 29 2020 at 09:03):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?
Théo Winterhalter (Sep 29 2020 at 09:03):(Or rather do you need to prove it's well-typed?)
Théo Winterhalter (Sep 29 2020 at 09:05):Otherwise you can indeed use tmLemma to prove somthing using an obligation.
Pierre Vial (Sep 29 2020 at 09:12):@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)
Théo Winterhalter (Sep 29 2020 at 09:35):Not the positivity condition, I think there is something, but it's not complete. cc @Matthieu Sozeau
Matthieu Sozeau (Sep 29 2020 at 09:55):Positivity is formalized now, yes. Only it disallows nested inductive types for now.
Matthieu Sozeau (Sep 29 2020 at 09:59):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.
Pierre Vial (Sep 29 2020 at 12:49):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, reifies 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 P proving 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.
Matthieu Sozeau (Sep 30 2020 at 08:01):Yes, I agree with you, you need a metalanguage to generate the statement, and MetaCoq should fit perfectly here
Last updated: May 31 2023 at 04:01 UTC