applying one expr to another

Stream: new members

[Lucas Allen]

Buenos días, Giving two expressions t s I want to be able to treat s like it's a goal, apply t to it, and get the list of goals that apply t generates. To do this I have

meta def test3 (t s : expr) : tactic (list expr) :=
do set_goals [s],
   apply t,
   get_goals

meta def test3_works (t s : expr) : tactic unit :=
do l ← test3 t s,
   trace l

variables c d : Prop
#eval test3_works `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) `(c ↔ d)

Unfortunately, I get a red squiggle under the ↔ in (c ↔ d) with the error "failed to synthesize type class instance for
c d : Prop ⊢ reflected (c ↔ d)". I've seen reflected before, but I have no idea what it is.

Does test3 actually do what I want? And if so, how might I test it? Is it even possible to test?

[Fox Thomson]

Your problem is not related to test3 or iff. I think an expression being reflected refers to it being free of any local context so '(c ↔ d) is not reflected as it refers to c and d. '(∀ {c d : Prop} c ↔ d) would be reflected. In order to fix this you can change c and d to exprand use pre-expresions ''(%%c ↔ %%d) like in this:

meta def test3 (t : expr) (s : pexpr) : tactic (list expr) :=
do (λ x : expr, [x]) <$> to_expr s >>= set_goals,
   apply t,
   get_goals

meta def test3_works (t : expr) (s : pexpr) : tactic unit :=
do l ← test3 t s,
   trace l

variables c d : expr

#eval test3_works `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) ``(%%c ↔ %%d)

Unfortunately this was as far as I got, lean gives the cryptic error cannot evaluate function: 0 arguments given but expected 2

[Lucas Allen]

I see, thanks. I've gotten the error "cannot evaluate function: 0 arguments given but expected 2" before as well and I have no idea what it means.

[Lucas Allen]

It gives the impression that there are some arguments missing, but I don't know what they could be.

[Reid Barton]

Apparently that error happens when you try to #eval something involving a variable:

variables (n : ℕ)
#eval n   -- error: cannot evaluate function: 0 arguments given but expected 1

[Reid Barton]

In this case that error makes sense because ``(%%c ↔ %%d) means iff applied to the expressions c and d.

[Reid Barton]

For testing purposes I guess you might prefer constants c d : Prop together with ``(c ↔ d), although then you will encounter a new error.

[Lucas Allen]

I'm not at my Lean machine atm, I'll check it out later. Are %%c and %%d variables?

[Reid Barton]

they are splices

[Reid Barton]

like if c : exprand d : expr both represent the expression x, then ``(%%c ↔ %%d) is the expression x ↔ x

[Lucas Allen]

My understanding was that splices were like _s but you can use the name later.

[Reid Barton]

I don't understand what that would mean. It sounds more like metavariables...?

[Reid Barton]

%%c can also be called an antiquotation

[Reid Barton]

As an extreme example, ``(%%c) = c.

[Lucas Allen]

Hmmm, maybe my understanding is wrong. Can't you do things like (%%c ↔ %%d)) ← get_some_expr, and then use c and d later?

[Lucas Allen]

Is this explained in some docs somewhere?

[Reid Barton]

That's the same thing but in a pattern position.

[Lucas Allen]

Right.

[Lucas Allen]

I tried

meta constants x y : expr
#eval test3_works `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) `(%%x ↔ %%y)

And got a red squiggle under #eval with the error "code generation failed, VM does not have code for 'y'".

I feel like I'm trying to do something for which Lean is not intended. I'm going to go away and think about what I've learned and what I want to do.

[Reid Barton]

This is still the same underlying issue--you're asking Lean to do something that doesn't make sense. You might like to consider the following exercises.

Why does this fail? (What do you expect to happen?)

variables (n : nat)
#eval n

Why does this fail?

constant (n : nat)
#eval n

Why does this fail?

meta constant (e : expr)
#eval trace e

Why does this fail?

meta constant (e : expr)
#eval trace ``(%%e)

Then: Why does this fail?

variable (n : nat)
#eval trace ``(n)

Why does this not fail?

constant (n : nat)
#eval trace ``(n)

[Lucas Allen]

The code

variables (n : ℕ)
#eval n

gives the error "cannot evaluate function: 0 arguments given but expected 1". I guess this is because #eval does computation, so it wants the variable n to be assigned to something.

constant (n : nat)
#eval n

gives "code generation failed, VM does not have code for 'm'". I'm guessing this is because #eval doesn't know what to do with constants.

meta constant (e : expr)
#eval trace e

gives "code generation failed, VM does not have code for 'e'" which I'd wager is for the exact same reason as the last example.

meta constant (e : expr)
#eval trace ``(%%e)

gives the same error I think because ``(%%e) is just e.

variable (n : nat)
#eval trace ``(n)

gives a red squiggle under the n with the error "unexpected local in quotation expression". This suggests to me that when a variable is declared a local constant is added to the environment or something. Whereas for

constant (n : nat)
#eval trace ``(n)

Lean stores n as a constant. So do double backticks work on constants and not local constants or something?

[Lucas Allen]

So this

meta constants x y : expr
#eval test3_works `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) `(%%x ↔ %%y)

fails because x and y are not set to anything. Right?

[Mario Carneiro]

So do double backticks work on constants and not local constants or something?

This has to do with the difference between double and triple backtick. A double backtick pre-expression is name-resolved in the empty context at the point of the tactic itself, which is to say, you can reference constants and definitions defined previous to the tactic call, but not local constants (which wouldn't make any sense anyway because lean wants an expr not a nat at that point; but this is what %%e is doing).

When you use triple backtick, all the resolution is put off until it is explicitly elaborated using to_expr. This approach allows you to resolve local constants as long as the to_expr tactic is called inside a begin ... end block that has n in the context.

[Mario Carneiro]

So this fails because x and y are not set to anything. Right?

It fails for the same reasons as examples 2 and 3. The VM can't evaluate constants (unless they have been specifically defined as intrinsics in the C++ code)

[Lucas Allen]

Ohh...

variable (n : nat)
#eval trace ```(n)

works.

[Mario Carneiro]

You should think of that as being morally equivalent to trace "n"

[Mario Carneiro]

it doesn't require n in the context at all

[Lucas Allen]

I'm not sure I completely understand what's happening. But I think I is learning.

[Lucas Allen]

Yeah, so

#eval trace ```(t)

works without variable t : nat.

[Mario Carneiro]

open tactic

meta def tac := to_expr ```(t) >>= trace

#eval tac -- unknown identifier 't'

example (t : nat) : true := by {tac, trivial} -- t

[Mario Carneiro]

or to be slightly more interesting:

open tactic

meta def tac := to_expr ```(t) >>= infer_type >>= trace

#eval tac -- unknown identifier 't'

example (t : nat) : true := by {tac, trivial} -- ℕ

[Mario Carneiro]

which should make it clear that in the latter case tac really has picked up the variable t : nat in the context