Zulip Chat Archive
Stream: general
Topic: backticks - literals inside expr
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 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)
Joseph Corneli (Apr 10 2019 at 11:41):
If I remove the ^2, the tactic definition is accepted.
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"
Keeley Hoek (Apr 10 2019 at 11:48):
Curiously, this works:
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"
Joseph Corneli (Apr 10 2019 at 11:48):
ah!
Keeley Hoek (Apr 10 2019 at 11:49):
(But you have to manually write out the pow)
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?
Joseph Corneli (Apr 10 2019 at 11:50):
Anyway thanks for helping me get going here @Keeley Hoek
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"
Joseph Corneli (Apr 10 2019 at 11:51):
:queasy:
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...
Keeley Hoek (Apr 10 2019 at 11:52):
:O
Joseph Corneli (Apr 10 2019 at 11:53):
"When in doubt follow the instructions" ???
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
Keeley Hoek (Apr 10 2019 at 11:54):
It really is just a massive case bash on all of the expr constructors
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 (
Keeley Hoek (Apr 10 2019 at 11:57):
aaaaaaaaaaaaaaaaaaaaaaa indeed
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"
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)
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"
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
Simon Hudon (Apr 10 2019 at 15:01):
Is 2 supposed to be a natural number or a real number?
Joseph Corneli (Apr 10 2019 at 15:02):
Personally I think natural is the right choice.
Kevin Buzzard (Apr 10 2019 at 15:04):
this might not be true if a=0
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.
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
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: Dec 20 2023 at 11:08 UTC