Stream: MetaCoq

Topic: Proving a reified proposition with Program

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:

• every inhabitant `t` of `ind` is of the form `C(a1,...,an)`, where `C` is a constructor of `ind`
• If `C(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: Jul 24 2024 at 12:02 UTC