Coq export for symbol with definition defined with tactics

[NotBad4U]

Hi, I would like to export in Coq format symbol that has been defined with tactics like the symbol test_export2 below:

symbol Prop : TYPE;
builtin "Prop" ≔ Prop;

injective symbol π : Prop → TYPE; // `p
builtin "P" ≔ π;

constant symbol ⊤: Prop;
builtin "True" ≔ ⊤;

constant symbol ⊥: Prop;
builtin "False" ≔ ⊥;

symbol trivial : π ⊤;

symbol test_export : π (⊤) ≔ trivial;

symbol test_export2 : π (⊤) ≔
begin
  refine trivial
end;

But when I run the command lambdapi export -v 0 -o stt_coq Test.lp I get the error:

Axiom Prop : Type.
Axiom π : Prop -> Type.
Axiom ⊤ : Prop.
Axiom ⊥ : Prop.
Axiom trivial : π ⊤.
Definition test_export := trivial.
Uncaught [File "src/export/coq.ml", line 318, characters 17-23: Assertion failed].

[fblanqui]

Hi Alessio. The exports to Coq are purely syntactic currently: they are done after parsing and before elaboration. So they do not handle proofs (I should update the doc). For this reason, they are very efficient. I see 2 solutions to overcome this problem:

• Develop a translation after elaboration.
• Translate Lambdapi tactics to Coq tactics.

[NotBad4U]

What do you consider the easiest to do in a short time?

Translate Lambdapi tactics to Coq tactics.

The Lambdapi tactic is very similar to the Coq tactic so it should be a direct translation no?

I am interested in developing this feature. My goal is to be able to export my SMT proof in Coq 😄.

PS: Maybe the person in charge of Vodk in your team is interested in this feature?

[fblanqui]

The translation of tactics should be very easy to experiment (you just need to add a few lines in export/coq.ml). If it works, it will be interesting as it will keep the translation very efficient (linear in the size of files). But it may be the case that the semantics of lambdapi and coq tactics are slightly different, in which case you would need to define coq tactics implementing lambdapi ones. The translation after elaboration should not be too difficult either but longer as you need to create a new file to translate a signature and terms instead of an ast and p_terms, but you can follow and reuse what is done in the files dk.ml, xtc.ml or hrs.ml.