passing types

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

I would like to use docs#tactic.interactive.nontriviality inside a `[ tac ]-block. In my case, I have to specify an argument to nontriviality. In tactic mode, I would like to do nontriviality R, where R is a type. I can get my hands on the expr representing R, but I do not know how to pass this expr as a parse texpr? to nontriviality.

Can anyone help me?

[Damiano Testa]

here is a somewhat minimized example:

import data.polynomial.degree

open expr tactic
setup_tactic_parser

meta def single_term_proof (e : expr) : tactic unit :=
match e with
| `(polynomial.X) := do val ← to_expr ``(polynomial.nat_degree) tt ff,
                      let degX := expr.mk_app val [e],
                      e_eq ← mk_app `eq [degX, `(1)],
                      n ← get_unused_name,
                      assert n e_eq,
-- up to here, I should have produced a goal `(X : R[X]).nat_degree = 1`,
-- except I do not have access to `R` yet
                      rx ← infer_type e,
-- the 0-th arg of `rx` is `R`
                      let ris := (rx.get_app_args.nth 0).get_or_else `(0),
                      let pris := pexpr.of_expr ris,
                      let ar : parse texpr? := pris,
                    `[ --nontriviality ar,  <--- what should I place here?
                       exact polynomial.nat_degree_X ]
| _ := skip
end

[Eric Wieser]

Can you use docs#tactic.nontriviality_by_assumption to avoid needing the interactive version?

[Eric Wieser]

(as nontriviality_by_assumption ris)

[Damiano Testa]

Yes, it works! Thanks a lot!

[Damiano Testa]

I am still curious as to whether it is possible to pass on arguments as I had in mind, but this does solve this instance of my problem.

[Eric Wieser]

I would guess you need a %% antiquotation of some kind, but I've not tried

[Eric Wieser]

At any rate, it's probably better to stay out of interactive mode rather than go back and forth and fight the parser

[Damiano Testa]

I agree with the going back and forth. I have a follow-up question. In what is below, why do I need two assumption? Can I change something and get Lean to not need them?

import data.polynomial.degree

open expr tactic
setup_tactic_parser

meta def single_term_proof (e : expr) : tactic unit :=
match e with
| `(polynomial.X) := do val ← to_expr ``(polynomial.nat_degree) tt ff,
                      let degX := expr.mk_app val [e],
                      e_eq ← mk_app `eq [degX, `(1)],
                      n ← get_unused_name "pX1",
                      rx ← infer_type e,
                      let ris := (rx.get_app_args.nth 0).get_or_else `(0),
                      assert n e_eq,
                      nontriviality_by_assumption ris,
                      proof ← to_expr ``(polynomial.nat_degree_X),
                      tactic.exact proof,
                      assumption,  -- one of these assumptions is proving `e_eq`,
                      assumption   -- the other is closing a `non-trivial` goal?
| _ := skip
end

meta def quick : tactic unit :=
do `(polynomial.nat_degree %%x = %%one) ← target,
                      single_term_proof x

example {R : Type*} [hh : semiring R] (h : (0 : R) ≠ 1) :
  (polynomial.X : polynomial R).nat_degree = 1 :=
by quick

[Damiano Testa]

As I commented, I think that one of the two I actually need, since I want to use the recently proved e_eq to close the goal. But the other seems to be a weird nontrivial R goal, when nontrivial R is in context. I tried changing the to_expr [...] to to_expr [...] tt ff as per a suggestion of Kyle's, but this time it did not seem to help.

[Damiano Testa]

Here is what the goal state if I remove the two assumptions:

example {R : Type*} [hh : semiring R] (h : (0 : R) ≠ 1) :
  (polynomial.X : polynomial R).nat_degree = 1 :=
by {quick,  }

2 goals
R: Type ?
hh: semiring R
h: 0 ≠ 1
_inst: nontrivial R
⊢ nontrivial R

R: Type ?
hh: semiring R
h: 0 ≠ 1
pX1: polynomial.X.nat_degree = 1
⊢ polynomial.X.nat_degree = 1

[Damiano Testa]

I feel like the first one should have been closed by the nontriviality step, but I think that I did not pass on the correct metavariable information.

[Eric Wieser]

Note you can match against `(@polynomial.X %%R %%inst) to get R directly

[Eric Wieser]

That is to say, this works:

import data.polynomial.degree

open expr tactic
setup_tactic_parser

meta def single_term_proof (e : expr) : tactic unit :=
match e with
| `(@polynomial.X %%R %%inst) := do
    nontriviality_by_assumption R,
    tactic.interactive.exact ``(polynomial.nat_degree_X)
| _ := tactic.trace "oops"
end

meta def quick : tactic unit :=
do `(polynomial.nat_degree %%x = %%one) ← target,
                      single_term_proof x

example {R : Type*} [hh : semiring R] (h : (0 : R) ≠ 1) :
  (polynomial.X : polynomial R).nat_degree = 1 :=
by quick

[Eric Wieser]

Confusingly, you do want to use docs#tactic.interactive.exact here; you just don't want to use it from within interactive mode

[Eric Wieser]

(parse texpr is just pexpr with some extra instructions for the interactive parser)

[Damiano Testa]

Eric, thank you so much! I had gotten to my twisty code by trying to get Lean to understand what I was saying and really the issue is that I do not know the language!

I'll try to add more matches to single_term_proof and make it work in more situations!

Thanks again!

[Damiano Testa]

Also, even though I had seen these annotations a few times and I also know about Mario's cheatsheet, I still find it hard to navigate among `, %%, `(), ``(),....

[Eric Wieser]

I probably couldn't have written that from scratch, I'm also not familiar with the difference between those symbols.
Deleting and modifying code you don't understand is much easier than writing it from scratch!

[Yakov Pechersky]

`name, `(expr), ``(pexpr), %%inline-an-expr

In this case, you're matching on an expr, so you use \`(). In it, you match exactly in the terms you want. You store the expr for the term that is the ring type under the variable R via the match. The exact tactic expects a pexpr, which is like an expr but not yet fully elaborated. This makes sense because we want to rely on the exact tactic to figure out which ring our lemma is about and the instances. You could form the explicit expr by saying `(@polynomial.nat_degree_X %%R ... ) but you'd have to supply all the instances. In norm_num, this is usually done by carrying an instance_cache around and using it to form exprs instead of writing them out manually.

[Damiano Testa]

Yakov, thanks a lot for the explanation! Even though I know about the @<lemma> to supply all the arguments, it had not dawned on me until the answers that I got here, how useful this is in meta mode! Even if I could get Eric's suggestion to work (and I think that it is better in the current situation), I am really grateful for your comments!

[Scott Morrison]

Going back to the original question, Lean 3 does not have antiquotations for `[...] blocks, and so you have to rely on there being a non-interactive version of the tactic available.

[Damiano Testa]

Scott, thank you for the information! It's good to know when you should stop looking for something that just isn't there! :smile: