Zulip Chat Archive

Stream: general

Topic: backticks - literals inside expr


view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:38):

I'm trying to make a variant of one of the tactics in tactic_writing.md. This example from the documentation works fine:

meta def trace_goal_is_eq : tactic unit :=
do { `(%%l = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between " ++ (to_string l) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

My proposed variant would pattern-match a quadratic ax2+bx+cax^2+bx+c on the left hand side. I tried this:

meta def trace_goal_is_quad_eq : tactic unit :=
do { `(%%A * x^2 + %%B * x + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "x^2 "
                     ++ (to_string B) ++ "x "
                     ++ (to_string C) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

Here I get the error:

unknown identifier ’x’
invalid quotation, unsupported macro ’sorry’

I also tried this:

meta def trace_goal_is_quad_eq' : tactic unit :=
do { `(%%A * %%x ^ 2 + %%B * %%y + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "x^2 "
                     ++ (to_string B) ++ "x "
                     ++ (to_string C) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

equation compiler failed, maximum number of steps (2048) exceeded (possible solution: use ’set_option eqn_compiler.max_steps <new-threshold>’) (use ’set_option trace.eqn_compiler.elim_match true’ for additional details)

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:41):

If I remove the ^2, the tactic definition is accepted.

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:44):

But this isn't accepted:

meta def trace_goal_is_quad_eq'' : tactic unit :=
do { `(%%A * %%x ^ %%e + %%B * %%y + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "x^2 "
                     ++ (to_string B) ++ "x "
                     ++ (to_string C) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:48):

Curiously, this works:

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:48):

meta def trace_goal_is_quad_eq : tactic unit :=
do { `(%%A * nat.pow %%n %%x + %%B * %%y + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "x^2 "
                     ++ (to_string B) ++ "x "
                     ++ (to_string C) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:48):

ah!

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:49):

(But you have to manually write out the pow)

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:49):

From that, it seems * and + are acceptable as "sugar" inside of such expressions, and ^ is not...? Is there a place to find the list of sugared variants?

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:50):

Anyway thanks for helping me get going here @Keeley Hoek

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:50):

I don't think it's so simple, because this compiles as well:

meta def trace_goal_is_quad_eq'' : tactic unit :=
do { `(%%A * %%x ^ %%e + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "x^2 "
                     ++ (to_string C) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:51):

:queasy:

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:52):

Ohk, I think I'm understanding. This is just a guess, but: I think the equation compiler might be doing something crazy like making a pattern for all the possible had_add, etc... instances which it knows about. Or maybe there are just somehow a lot of cases.
Regardless,

set_option eqn_compiler.max_steps 10000

really does make your original code work...

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:52):

:O

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:53):

"When in doubt follow the instructions" ???

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:53):

"And when making wild guesses follow the instructions more"? :D set_option trace.eqn_compiler.elim_match true lets you see what's actually happening

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:54):

It really is just a massive case bash on all of the expr constructors

view this post on Zulip Joseph Corneli (Apr 10 2019 at 11:56):

I'mma let you finish but

[eqn_compiler.elim_match] depth [1]
match trace_goal_is_quad_eq'' : tactic unit[]
   :=
    (tactic.target >>=
         λ (_p : expr),
           (λ (_a : expr),
              expr.cases_on _a (λ (a : ), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                (λ (a : level), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                (λ (a : name) (a_1 : list level), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                (λ (a a_1 : name) (a_2 : expr), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                (λ (a a_1 : name) (a_2 : binder_info) (a_3 : expr),
                   id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                (λ (a a_1 : expr),
                   expr.cases_on a (λ (a : ), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                     (λ (a : level), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                     (λ (a_a : name) (a_a_1 : list level),
                        id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                     (λ (a_a a_a_1 : name) (a_a_2 : expr),
                        id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                     (λ (a_a a_a_1 : name) (a_a_2 : binder_info) (a_a_3 : expr),
                        id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                     (λ (a_a a_a_1 : expr),
                        expr.cases_on a_a
                          (λ (a_a : ), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                          (λ (a_a : level), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                          (λ (a_a_a : name) (a_a_a_1 : list level),
                             id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                          (λ (a_a_a a_a_a_1 : name) (a_a_a_2 : expr),
                             id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                          (λ (a_a_a a_a_a_1 : name) (a_a_a_2 : binder_info) (a_a_a_3 : expr),
                             id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                          (λ (a_a_a a_a_a_1 : expr),
                             expr.cases_on a_a_a
                               (λ (a_a_a : ), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                               (λ (a_a_a : level), id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                               (λ (a_a_a_a : name) (a_a_a_a_1 : list level),
                                  ite (a_a_a_a = name.mk_string "eq" name.anonymous)
                                    (expr.cases_on a_a_1
                                       (λ (a_a_1 : ),
                                          id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                       (λ (a_a_1 : level),
                                          id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                       (λ (a_a_1_a : name) (a_a_1_a_1 : list level),
                                          id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                       (λ (a_a_1_a a_a_1_a_1 : name) (a_a_1_a_2 : expr),
                                          id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                       (λ (a_a_1_a a_a_1_a_1 : name) (a_a_1_a_2 : binder_info) (a_a_1_a_3 : expr),
                                          id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                       (λ (a_a_1_a a_a_1_a_1 : expr),
                                          expr.cases_on a_a_1_a
                                            (λ (a_a_1_a : ),
                                               id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                            (λ (a_a_1_a : level),
                                               id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                            (λ (a_a_1_a_a : name) (a_a_1_a_a_1 : list level),
                                               id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                            (λ (a_a_1_a_a a_a_1_a_a_1 : name) (a_a_1_a_a_2 : expr),
                                               id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                            (λ (a_a_1_a_a a_a_1_a_a_1 : name) (a_a_1_a_a_2 : binder_info)
                                             (a_a_1_a_a_3 : expr),
                                               id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                            (λ (a_a_1_a_a a_a_1_a_a_1 : expr),
                                               expr.cases_on a_a_1_a_a
                                                 (λ (a_a_1_a_a : ),
                                                    id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                                 (λ (a_a_1_a_a : level),
                                                    id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                                 (λ (a_a_1_a_a_a : name) (a_a_1_a_a_a_1 : list level),
                                                    id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                                 (λ (a_a_1_a_a_a a_a_1_a_a_a_1 : name) (a_a_1_a_a_a_2 : expr),
                                                    id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                                 (λ (a_a_1_a_a_a a_a_1_a_a_a_1 : name) (a_a_1_a_a_a_2 : binder_info)
                                                  (a_a_1_a_a_a_3 : expr),
                                                    id_rhs (tactic unit) (match_failed interaction_monad.monad_fail))
                                                 (λ (a_a_1_a_a_a a_a_1_a_a_a_1 : expr),
                                                    expr.cases_on a_a_1_a_a_a (λ (a_a_1_a_a_a : ),  )
                                                      (λ (a_a_1_a_a_a : level), id_rhs  )
                                                      (λ (a_a_1_a_a_a_a : name) (a_a_1_a_a_a_a_1 : list level),
                                                         id_rhs (tactic unit)
                                                           (match_failed interaction_monad.monad_fail))
                                                      (λ (a_a_1_a_a_a_a a_a_1_a_a_a_a_1 : name)
                                                       (a_a_1_a_a_a_a_2 : expr),
                                                         id_rhs (tactic unit)
                                                           (match_failed interaction_monad.monad_fail))
                                                      (λ (a_a_1_a_a_a_a a_a_1_a_a_a_a_1 : name)
                                                       (a_a_1_a_a_a_a_2 : binder_info) (a_a_1_a_a_a_a_3 : expr),
                                                         id_rhs (tactic unit)
                                                           (match_failed interaction_monad.monad_fail))
                                                      (λ (a_a_1_a_a_a_a a_a_1_a_a_a_a_1 : expr),
                                                           (λ (a_a_1_a_a_a_a_a a_a_1_a_a_a_a_a_1 : ), )
                                                           (λ (a_a_1_a_a_a_a_a : name)
                                                            (a_a_1_a_a_a_a_a_1 : binder_info)
                                                            (a_a_1_a_a_a_a_a_2 a_a_1_a_a_a_a_a_3 : expr),  )
                                                           (λ (a_a_1_a_a_a_a_a : name)
                                                            (a_a_1_a_a_a_a_a_1 : binder_info)
                                                            (a_a_1_a_a_a_a_a_2 a_a_1_a_a_a_a_a_3 : expr),
                                                              id_rhs  )
                                                           (λ (a_a_1_a_a_a_a_a : name)
                                                            (a_a_1_a_a_a_a_a_1 a_a_1_a_a_a_a_a_2 a_a_1_a_a_a_a_a_3 :
                                                              expr),
                                                              id_rhs (tactic unit)
                                                                (match_failed interaction_monad.monad_fail))
                                                           (λ (a_a_1_a_a_a_a_a : macro_def)
                                                            (a_a_1_a_a_a_a_a_1 : list expr),
                                                              id_rhs (tactic unit)
                                                                (match_failed interaction_monad.monad_fail)))
                                                      (λ (a_a_1_a_a_a_a : name) (a_a_1_a_a_a_a_1 : binder_info)
                                                       (a_a_1_a_a_a_a_2 a_a_1_a_a_a_a_3 : expr),
                                                         id_rhs (tactic unit)
                                                           (match_failed interaction_monad.monad_fail))
                                                      (λ (a_a_1_a_a_a_a : name) (a_a_1_a_a_a_a_1 : binder_info)
                                                       (a_a_1_a_a_a_a_2 a_a_1_a_a_a_a_3 : expr),
                                                         id_rhs (

view this post on Zulip Keeley Hoek (Apr 10 2019 at 11:57):

aaaaaaaaaaaaaaaaaaaaaaa indeed

view this post on Zulip Simon Hudon (Apr 10 2019 at 14:30):

Can you try:

meta def trace_goal_is_quad_eq'' : tactic unit :=
do { `(%%A * %%x ^ (2 : nat) + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "x^2 "
                     ++ (to_string C) ++ " and " ++ (to_string r) }
   <|> tactic.trace "Goal is not an equality"

view this post on Zulip Joseph Corneli (Apr 10 2019 at 14:57):

@Simon Hudon that one gives me

equation compiler failed, maximum number of steps (2048) exceeded (possible solution: use 'set_option eqn_compiler.max_steps <new-threshold>') (use 'set_option trace.eqn_compiler.elim_match true' for additional details)

view this post on Zulip Joseph Corneli (Apr 10 2019 at 14:58):

I was able to take it apart to this level:

meta def trace_goal_is_quad_eq'' : tactic unit :=
do { `(%%A*%%Q + %%B*%%L + %%C = %%r)  tactic.target,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ (to_string A) ++ "/-quadratic part...-/ "
                     ++ (to_string Q) ++ "/-...--AND-/ "
                     ++ (to_string B) ++ "/-linear part...-/ "
                     ++ (to_string L) ++ "/-...--AND-/ "
                     ++ (to_string C) ++ "/-constant part-/ "
   }
   <|> tactic.trace "Goal is not an equality"

view this post on Zulip Joseph Corneli (Apr 10 2019 at 15:00):

That gave me this debug message:

Goal is equality between the quadratic a/-quadratic part...-/ has_pow.pow.{0 0} real nat (monoid.has_pow.{0} real real.monoid) x (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one))/-...--AND-/ b/-linear part...-/ x/-...--AND-/ c/-constant part-/

when applied via

example (a b c : ) :  (x:), a*x^2+b*x+c = a*(x + (1/(2*a))* b)^2 + (c-b^2/(4*a)) :=
begin
  intro,
  trace_goal_is_quad_eq'',
end

view this post on Zulip Simon Hudon (Apr 10 2019 at 15:01):

Is 2 supposed to be a natural number or a real number?

view this post on Zulip Joseph Corneli (Apr 10 2019 at 15:02):

Personally I think natural is the right choice.

view this post on Zulip Kevin Buzzard (Apr 10 2019 at 15:04):

this might not be true if a=0

view this post on Zulip Joseph Corneli (Apr 10 2019 at 15:06):

Oops! Even if a=1, though, the parsing might still be tricky. I'll set up a variant like that and test it.

view this post on Zulip Mario Carneiro (Apr 11 2019 at 00:17):

A simple way to avoid the threshold is to break the pattern match down:

open tactic
meta def trace_goal_is_quad_eq'' : tactic unit :=
do { `(%%e₁ = %%r)  target,
     `(%%A * %%x ^ %%e + %%B * %%y + %%C)  return e₁,
     guard (x = y),
     guard (e = `(2:)),
     pA  pp A, pB  pp B, pC  pp C, pr  pp r,
     tactic.trace $ "Goal is equality between the quadratic "
                     ++ pA ++ " x^2 + "
                     ++ pB ++ " x + "
                     ++ pC ++ " and " ++ pr }
   <|> tactic.trace "Goal is not an equality"
example (a b c : ) :  (x:), a*x^2+b*x+c = a*(x + (1/(2*a))* b)^2 + (c-b^2/(4*a)) :=
begin
  intro,
  trace_goal_is_quad_eq'',
end

view this post on Zulip Mario Carneiro (Apr 11 2019 at 00:23):

But I think this kind of parsing is probably not a good idea in any case. It's very brittle


Last updated: May 16 2021 at 05:21 UTC