mathport:tags

Stream: lean4

[Daniel Selsam]

Mario Carneiro said:

Maybe a good next step would be to backport Expr.mdata to lean 3, so that we can have general annotations on things without affecting tactics (for the most part). Right now all the annotation support is wrapped up in MacroDef, which is opaque to lean

How about the following:

• We add a new inductive type tag4 to lean3 that can express lists, strings, names, numbers, bools, etc.
• We define:

@[reducible] def id_tag {α : Sort u} (tag : tag4) (a : α) : α := a

• Non-trivial tactics can wrap their proofs with id_tag, e.g. simp can tag its proof with tag.string "simp", possibly including options or named lemmas
• Mathport can replace the tag4 occurrences inside id_tag with Tag4 (note: this is not naive aligning due to strings&names, but would be like how we handle auto_param -> autoParam currently)
• For delaboration, we can then add special delaborators for terms whose app-fn head is id_tag, that get to look at the tag data

[Daniel Selsam]

It is fairly clean but I am not sure if it is actually necessary -- many tactics can probably be reverse-engineered from the proof terms. For example, we can detect norm_num in a number of ways: by inspecting the type or by detecting a norm_num lemma inside. For simp, the lemmas could be determined by sweeping the proof term.

[Daniel Selsam]

We don't need to decide this yet. I think the highest priority is to finalize numbers. Then we can write normNum and ring, and then start experimenting with lean4 on top of the auto-ported .oleans.