creating your own tactics & manipulating the expression tree

Stream: new members

[Dean Young]

Hi all,

Suppose I have a setup like this:

variable { X : Type}
variable { Y : Type}
variable { Z : Type}
def A : Type := X → Y → Z
def B : Type := X → Y → Z

How might I refer to the expression trees of A and B in tactic mode? I expect it would be something like EXP(A).1.1.

What I'm looking for is a "complete" tactic language, I guess - as powerful as it would ever need to be.

Secondly, how do I create my own tactics? I have only used tactics.

[Alex J. Best]

I recommend reading https://leanprover-community.github.io/extras/tactic_writing.html, and watching the videos linked there. Be aware that the way tactics are written is somewhat different in lean 4, but understanding the basic concepts of how expressions are formed should be pretty transferable. You can always go to the definition of an existing tactic and study how it works.

[Eric Wieser]

You can get the expression tree of the name A as `(A)

[Eric Wieser]

A simple test might look like

run_cmd do
  let the_expr := `(A),
  tactic.trace the_expr.to_raw_fmt

[Dean Young]

Where can I find the documentation behind expression trees in Lean 4? I want to be able to access the branches of the tree and to know how many branches there are at the top node, and the height, for instance.

variable { X : Type}
variable { Y : Type}
variable { Z : Type}
def A : Type := X → Y → Z
def B : Type := X → Y → Z
let C := `(A)
let first_branch := sorry
let second_branch := sorry
let height := sorry
let how_many_daughters := sorry

[Alex J. Best]

docs4#Lean.Expr is the main type of expressions, I don't know of specific functions like height, I'm not sure how actually useful they are in practice. And the branching really depends on the sort of object at the top, e.g. a constant doesn't branch, a function application branches twice etc. The inductive type here controls the structure rather than being an arbitrary tree

[Eric Wieser]

I think that Q(...) is the lean 4 replacement for `(...)

[Eric Wieser]

And you can't just put let at the top level of a lean file like that