Zulip Chat Archive

Stream: new members

Topic: creating your own tactics & manipulating the expression tree

Dean Young (Mar 07 2023 at 08:48):

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 (Mar 07 2023 at 10:45):

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 (Mar 07 2023 at 14:26):

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

Eric Wieser (Mar 07 2023 at 14:28):

A simple test might look like

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

Dean Young (Mar 07 2023 at 23:04):

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 (Mar 08 2023 at 10:18):

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 (Mar 08 2023 at 15:37):

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

Eric Wieser (Mar 08 2023 at 15:38):

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

Last updated: Dec 20 2023 at 11:08 UTC