syntax error when creating a variant of apply_rules

Stream: new members

[Joseph Corneli]

I get an error why I try to apply my new tactic, below. This seems strange to me because I did little more than a copy and paste job to define the tactic. Clearly I have made some mistake along the way. Lean expects a pexpr but gets something else.

import topology.basic analysis.complex.exponential
import tactic.core
open real set

open tactic

meta def refine_list_expr : list expr → tactic unit
| []     := fail "no matching rule"
| (h::t) := do (refine ``(%%h _ _)) <|> refine_list_expr t

meta def apply_rules_with_refine (hs : list pexpr) (n : nat) : tactic unit :=
do l ← build_list_expr_for_apply hs,
   iterate_at_most_on_subgoals n (assumption <|> refine_list_expr l <|> apply_list_expr l)

open interactive interactive.types
meta def apply_rules_with_refine_interactive (hs : parse pexpr_list_or_texpr) (n : nat := 50) : tactic unit :=
apply_rules_with_refine hs n

-- * sin(sin(x)) and friends are continuous on ℝ

lemma continuous_sin' : continuous (λ x : ℝ, sin x) :=
by apply_rules [continuous.comp, continuous_sin] 3

#print continuous_sin'

lemma continuous_sin_sin : continuous (λ x : ℝ, sin(sin x)) :=
by apply_rules_with_refine_interactive [continuous.comp, continuous_sin] 30

[Joseph Corneli]

type mismatch at application
  list.cons continuous.comp
term
  continuous.comp
has type
  continuous ?m_5 → continuous ?m_8 → continuous (?m_8 ∘ ?m_5) : Prop
but is expected to have type
  pexpr : Type

[Joseph Corneli]

OK, here I've added some more namespace decorations etc. and this gets me past the "syntax error". Still sorting out the actual logic of the tactic but that's another story!

import topology.basic analysis.complex.exponential
import tactic.core data.list.defs
open real set

----------------------
/- Attempt to use `refine` alongside `apply` -/
namespace sin_sin
open tactic
meta def refine_list_expr : list expr → tactic unit
| []     := do {trace "fail", fail "no matching rule"}
| (h::t) := do {trace "refine, initial target:",
                tactic.target >>= tactic.trace,
                (refine ``(%%h _ _)),
                trace "refine, subsequent target:",
                tactic.target >>= tactic.trace,
                trace "refine, rule applied:",
                trace h <|> refine_list_expr t }

meta def apply_rules_with_refine (hs : list pexpr) (n : nat) : tactic unit :=
do l ← build_list_expr_for_apply hs,
   iterate_at_most_on_subgoals n ((trace "A" >> assumption) <|>
                                  (trace "R" >> refine_list_expr l) <|>
                                  (trace "E" >> apply_list_expr l))
end sin_sin
----------------------

namespace tactic
namespace interactive
open lean
open lean.parser
open interactive interactive.types expr

meta def apply_rules_with_refine_interactive (hs : parse pexpr_list_or_texpr) (n : nat := 50) : tactic unit :=
sin_sin.apply_rules_with_refine hs n

end interactive
end tactic

-- * sin(sin(x)) and friends are continuous on ℝ

-- this works but it's boring!
lemma continuous_sin' : continuous (λ x : ℝ, sin x) :=
by apply_rules [continuous_sin] 1
#print continuous_sin'

lemma continuous_sin_sin : continuous (λ x : ℝ, sin(sin x)) :=
begin
apply_rules_with_refine_interactive [continuous.comp, continuous_sin] 6
end

open real

-- Note, with latest version of mathlib, this proof is slightly different from earlier versions
lemma continuous_sin_sin_sin : continuous (λ x : ℝ, sin (sin (sin x))) :=
begin
refine continuous.comp _ _,
apply continuous_sin,
refine continuous.comp _ _,
apply continuous_sin,
refine continuous.comp _ _,
apply continuous_sin,
exact continuous_id,
end

#print continuous_sin_sin_sin