expr

Stream: general

[Scott Morrison]

Does anyone know the behaviour of meta constant expr.replace : expr → (expr → nat → option expr) → expr?

[Scott Morrison]

(I have an expression that has a single mvar somewhere in it; I would like to replace that with an expr.var 0.)

[Simon Hudon]

You could try implementing it as e.replace $ λ e' _, if e'.is_mvar then expr.var 0 else none

[Simon Hudon]

It might not work if replace does not proceed recursively but your attempt should help us decide what to do next.

[Mario Carneiro]

you should probably use the n variable though

[Mario Carneiro]

e.replace $ λ e' n, if e'.is_mvar then expr.var n else none

[Simon Hudon]

Ooooooh! Is that what it's for? That's so cool!

[Scott Morrison]

Neat!

[Scott Morrison]

Do you guys have an expr.is_mvar that I'm missing?

[Mario Carneiro]

no, looks like you will have to roll your own

[Simon Hudon]

I thought it was in mathlib

[Simon Hudon]

Ah! In tactic.basic, there it is called is_meta_var

[Scott Morrison]

Thanks.

[Mario Carneiro]

should we be more regular in the naming there?

[Simon Hudon]

Probably, yes

[Chris Hughes]

Is there any documentation anywhere on what all the constructors to expr mean?

[Simon Hudon]

Not that I know of. It would be worth writing. What do you want to know?

[Scott Morrison]

I would love to have a paragraph on each. I have to re-remember the order of arguments to expr.pi every time I see it.

[Chris Hughes]

Essentially what Scott's talking about. What each of the arguments to each constructor represents.

[Scott Morrison]

Didn't Ed Ayers write this at some point? He had a draft of some docs on meta stuff, but I think it was never PR'd.

[Chris Hughes]

Are expr tts allowed to contain metavariables?

[Edward Ayers]

yes

[Edward Ayers]

as far as I understand, expr tt means that the expression has been typechecked and fully elaborated.

[Edward Ayers]

meta inductive expr (elaborated : bool := tt)
/- A bound variable with a de-Bruijn index. -/
| var      {} : nat → expr
/- A type universe: `Sort u` -/
| sort     {} : level → expr
/- A global constant. These include definitions, constants and inductive type stuff present in the environment as well as hard-coded definitions. -/
| const    {} : name → list level → expr
/- [WARNING] Do not trust the types for `mvar` and `local_const`,
they are sometimes dummy values. Use `tactic.infer_type` instead. -/
/- An `mvar` is a 'hole' yet to be filled in by the elaborator or tactic state. -/
| mvar        (pretty : name)  (unique : name)  (type : expr) : expr
/- A local constant. For example, if our tactic state was `h : P ⊢ Q`, `h` would be a local constant. -/
| local_const (pretty : name) (unique : name) (bi : binder_info) (type : expr) : expr
/- Function application. -/
| app         : expr → expr → expr
/- Lambda abstraction. eg ```(λ a : α, x)`` -/
| lam        (var_name : name) (bi : binder_info) (var_type : expr) (body : expr) : expr
/- Pi type constructor. eg ```(Π a : α, x)`` and ```(α → β)`` -/
| pi         (var_name : name) (bi : binder_info) (var_type : expr) (body : expr) : expr
/- An explicit let binding.-/
| elet       (var_name : name) (type : expr) (assignment : expr) (body : expr) : expr
/- A macro, see the docstring for `macro_def`.
  The list of expressions are local constants and metavariables that the macro depends on.
  -/
| macro       : macro_def → list expr → expr

[Edward Ayers]

@Scott Morrison yeah I should PR it at some point.

[Edward Ayers]

I build Lean from source with extra docstrings.

[Edward Ayers]

binder_info is only used by the elaborator.

[Chris Hughes]

Thanks for this.

[Chris Hughes]

What does tactic.generalize do?

[Simon Hudon]

If you have ⊢ x + 1 ≤ y + 2, generalize ``(y + 2) `z will turn the goal into ⊢ x + 1 ≤ z

[Chris Hughes]

Okay thanks.

[Simon Hudon]

The interactive version offers more options like adding an assumption h : y + 2 = z

[Mario Carneiro]

@Edward Ayers An expr tt may not actually have been typechecked, but it is presumed to at least have the structure to be typechecked

[Edward Ayers]

Ok so does expr tt just mean that there are no placeholders?

[Gabriel Ebner]

Well, technically yes since "placeholder" is the name used for the macro that represents the _ syntactical form. But both expr ff and expr tt can have metavariables.

[Gabriel Ebner]

The big difference between expr ff and expr tt is whether implicit arguments are present. For example the equality x = x is represented in expr ff as app (app (const `eq _) x) x while in expr tt it is represented as app (app (app (const `eq _) t) x) x (one more argument).

[Edward Ayers]

What is the difference between implicit and strict_implicit?

[Edward Ayers]

For binder_info

[Gabriel Ebner]

default = (x : α), implicit = {x : α}, strict_implicit = ⦃x : α⦄, inst_implicit = [x : α], I believe aux_decl is used as a tag for the _match hypotheses but I could be completely mistaken.

[Gabriel Ebner]

The difference between {} and ⦃⦄ is how implicit arguments are treated that are not followed by explicit arguments. {} arguments are applied eagerly, while ⦃⦄ arguments are left partially applied:

def foo {x : ℕ} : ℕ := x
def bar ⦃x : ℕ⦄ : ℕ := x
#check foo -- foo : ℕ
#check bar -- bar : Π ⦃x : ℕ⦄, ℕ

[Edward Ayers]

In C++ it says that aux_decl is "used to mark local constants representing recursive functions
in recursive equations and match statements."

[Mario Carneiro]

aux_decl is used for _match, _fun_match, _let_match and the self reference that appears in recursive pattern matching

[Mario Carneiro]

these are not real local constants, but rather trigger recursive compilation when used

[Chris Hughes]

If pexpr and expr are more or less the exact same inductive type how are they different? Is it just because in practice we never define them from constructors ourselves and always use the inbuilt functions which treat pexpr and expr differently even though the type doesn't force them to?

[Floris van Doorn]

As Gabriel said above, the same term is represented differently as an pexpr than as an expr. Moreover, for both structures there are some constants such as expr.mk_sorry, pexpr.mk_placeholder and pexpr.mk_explicit which only exist in one of the two variants, but not the other. These are not represented by the inductive structure. But mk_placeholder and mk_explicit will be used (for example) by the tactic to_expr.

[Chris Hughes]

Is there an easy way of printing an expr in terms of the constructors of expr?

[Rob Lewis]

expr.to_raw_fmt

[Chris Hughes]

Thanks

[Chris Hughes]

If I'm writing a tactic and I have e : expr, which is a proof of equality, how would I do rw e at * say, or simp [e] at * as part of a tactic?

[Keeley Hoek]

You can rw another arbitrary expr using rewrite_core. I would have to read the tactic.interactive.rw definition to see how it replaces local hypotheses, too, but that's the idea.

For simp you need to call mk_simp_set and then add your lemma to it. Then you need to pass that data to the built-in function tactic.simplify.

[Scott Morrison]

often a cheap way to do these sorts of things is using tactic quotations, e.g. `[simp at *]

[Scott Morrison]

I'm guessing you can use antiquotations, and write something like `[simp [%%e] at *].