A meta-translation inside Lean

Stream: general

[Farzad Jafarrahmani]

Hello everyone,

I've formalized a logic, let's call it L, in Lean. My goal is to translate a portion of Mathlib—specifically, a theory T—into L.

This means I want to write a program that can translate both the statements and proofs of theory T from Mathlib into the syntax of L, which is itself written in Lean.

First, does this question make sense, especially given that L is already defined within Lean's syntax?

If so, I would appreciate any suggestions on how to approach this.
Does this involve metaprogramming?

[Edward van de Meent]

i think this question makes sense: you have (presumably) defined a type of statements in your logic, and would like a way to turn a term in lean into a term or statement (in lean) in your logic.

indeed, since you (most likely) will need to inspect the lean term, metaprogramming will be necessary

[Farzad Jafarrahmani]

Thanks for your reply!

I was worried about how to distinguish these two terms—one of L and one of T—since both are ultimately represented using the same underlying type theory of lean.

Anyway, as you said, I think I need to inspect the Lean terms via metaprogramming to see what can be done.

[Andrés Goens]

Just for completeness sake: you can of course specify the translation manually without using metaprogramming as Lean functions (but then it will only work for the concrete fragment of Mathlib for which you define the translation.), i. e. if your T is fixed, you might get away without metaprogramming

[Farzad Jafarrahmani]

Thanks for your comment! 
Actually, my T is a fixed theory, let'say Mathlib.Geometry.Euclidean.
But I do not see how I can get away without metaprogramming. 
Nevertheless, I need to work with the lean terms for the statements and theorems in this fragment of Mathlib which is accessible via metaprogramming.
Am I missing something?