apply_rules example

Stream: maths

[Joseph Corneli]

I thought this might be a clever way to automate simple continuity proofs, but it's not working except on the very simplest case. I would be looking to recover a proof like this, which seems reasonably similar to the example for apply_rules in the docs.

theorem continuous_sin_sin_sin : continuous (λ (x : ℝ), sin (sin (sin x))) :=
continuous.comp (continuous.comp continuous_sin continuous_sin) continuous_sin

Here's what I tried:

import topology.basic data.set.intervals analysis.complex.exponential
open real set

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

@[user_attribute]
meta def cts_rules : user_attribute :=
{ name := `cts_rules,
  descr := "lemmas usable to prove continuity" }

attribute [cts_rules] continuous.comp continuous_sin

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

#print continuous_sin'

lemma continuous_sin_sin : continuous (λ x : ℝ, sin(sin x)) :=
by apply_rules [cts_rules] 6

lemma continuous_sin_sin_sin : continuous (λ x : ℝ, sin (sin (sin x))) :=
begin
refine continuous.comp _ _,
refine continuous.comp _ _,
apply continuous_sin,
apply continuous_sin,
apply continuous_sin,
end

#print continuous_sin_sin_sin

[Joseph Corneli]

I guess apply_rules doesn't know how to do the equivalent of refine, is that correct?

[Joseph Corneli]

Digging into the code, I guess the name apply_rules says it all.

meta def apply_list_expr : list expr → tactic unit
| []     := fail "no matching rule"
| (h::t) := do interactive.concat_tags (apply h) <|> apply_list_expr t

[Reid Barton]

This example has come up before. One problem is that apply is not smart enough to insert the right number of _s to make apply continuous.comp work. If I recall correctly it is related to the fact that continuous f is itself a Pi-type (for all $U$, if $U$ is open then ...). Another problem is that blindly applying continuous.comp is not a good idea either--even if the function we're trying to prove continuous is not visibly a composition, applying continuous.comp will succeed in writing it as the composition of itself and the identity.

[Jesse Michael Han]

i wonder why marking continuous.comp and continuous_sin as simp doesn't cause them to trigger when trying to prove continuous (sin \circ sin) with simp

[Chris Hughes]

marking continuous.comp with simp has no effect, because it has proof assumptions. I think it might have an effect if you use simp * at * and there is a local constant of type continuous sin.

[Jesse Michael Han]

i'm puzzled because we solved a similar problem (generating Boolean-valued congruence lemmas) in flypitch in exactly this way, where the simp lemmas also had proof assumptions (you can see where they're used in the source code as change B_ext _, simp)

in that case, there are multiple operations (binary inf and sup, indexed Inf and Sup) and simp seems to know how to break apart the expressions and recursively fulfill the new proof obligations

[Chris Hughes]

I'm confused. Everywhere change B_ext _, simp is used that I saw, the only simp lemma used was bSet.B_ext_mem_right which has no assumptions to prove.

[Joseph Corneli]

I suppose each of the problems Reid mentioned could be tackled head on.

Each lemma here always has the same number of underscores, so that could be preprogrammed rather then guessed.

I suppose there must be some way to tell if a function is a composition, so that the application of continuous.comp can be constrained.

[Jesse Michael Han]

@Chris Hughes that's odd---was that from squeeze_simp? on my machine, if i squeeze_simp the change B_ext _, simp in theorem bSet_axiom_of_infinity' (line 1750), i get

simp only [bSet.subst_congr_inf,
 bSet.subst_congr_supr,
 bSet.subst_congr_const,
 bSet.mem,
 bSet.B_ext_mem_left,
 forall_true_iff]

(subst_congr and B_ext are unfortunately synonymous prefixes)

[Jesse Michael Han]

@Joseph Corneli maybe there's a meta way to query Lean for the number of explicit arguments for a lemma?

[Joseph Corneli]

I've tried making a (simple) variant of apply_rules that can also do refine, but I've run into an unexpected syntax problem. I don't want to detract from a wider and more interesting discussion with a "debug my code" discussion, but might get another thread going, because I'm likely to stay stuck.

[Chris Hughes]

Chris Hughes that's odd---was that from squeeze_simp? on my machine, if i squeeze_simp the change B_ext _, simp in theorem bSet_axiom_of_infinity' (line 1750), i get

simp only [bSet.subst_congr_inf,
 bSet.subst_congr_supr,
 bSet.subst_congr_const,
 bSet.mem,
 bSet.B_ext_mem_left,
 forall_true_iff]

(subst_congr and B_ext are unfortunately synonymous prefixes)

I didn't look at that one. I'm confused about that. set_option trace.simplify.rewrite true seems to be rewriting things that aren't even in the goal.

[Jesse Michael Han]

maybe simp is suited to do this kind of reasoning when the operations (inf, sup, +, -) are lifted pointwise from the codomain, but actual function composition is confusing it somehow

[Mario Carneiro]

I don't want to detract from a wider and more interesting discussion with a "debug my code" discussion

you clearly have different views on what is interesting than me

[Joseph Corneli]

I posted the code in the new members list.

[Joseph Corneli]

... and here's some revised code that looks very close to working. @Mario Carneiro it gets up to an application of exact but for some reason that fails and accordingly the goal doesn't close.

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 (format!"REFINE: {h}"),
                pure() <|> refine_list_expr t }

meta def exact_list_expr : list expr → tactic unit
| []     := do {trace "fail", fail "no matching rule"}
| (h::t) := do {trace "exact, initial target:",
                tactic.target >>= tactic.trace,
                trace (format!"EXACT: {h}"),
                -- Some problem here...
                exact h,
                trace "exact, final target:",
                tactic.target >>= tactic.trace,
                return () <|> exact_list_expr t }

meta def apply_list_expr : list expr → tactic unit
| []     := fail "no matching rule"
| (h::t) := do { trace "apply, initial target:",
                 tactic.target >>= tactic.trace,
                 trace (format!"APPLY: {h}") ,
                 interactive.concat_tags (apply h), pure() <|> apply_list_expr t }

open nat

meta def iterate_at_most_on_all_goals' : nat → tactic unit → tactic unit
| 0        tac := trace "maximal iterations reached"
| (succ n) tac := tactic.all_goals $ (do tac, trace (format!"{n}"), iterate_at_most_on_all_goals' n tac) <|> skip

meta def iterate_at_most_on_subgoals' : nat → tactic unit → tactic unit
| 0        tac := trace "maximal iterations reached"
| (succ n) tac := focus1 (do tac, trace (format!"{n}"), iterate_at_most_on_all_goals' n tac)

meta def apply_rules_with_refine (apps : list pexpr) (refs : list pexpr) (exas : list pexpr) (n : nat) : tactic unit :=
do a ← build_list_expr_for_apply apps,
   r ← build_list_expr_for_apply refs,
   e ← build_list_expr_for_apply exas,
   iterate_at_most_on_subgoals' n (assumption <|>
                                  -- guess: we can refine iff the expression is a lambda?
                                  -- oh, but we need to peel off the "continuous" part
                                  (do t ← tactic.target,
                                        let a := expr.app_arg t,
                                        if expr.is_lambda a then refine_list_expr r
                                        else fail "can't refine") <|>
                                  (sin_sin.apply_list_expr a) <|>
                                  (sin_sin.exact_list_expr e))

end sin_sin
----------------------

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

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

end interactive
end tactic

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

open real

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

#print continuous_sin_sin

-- 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

[Joseph Corneli]

You'll see I separated out the rules for apply, refine, and exact, and that here there's just one rule available for each such step. So obvs. this is preliminary to anything more general.

[Joseph Corneli]

Is there a way to run sorry inside of a tactic, so I can at least get it to print out a proof with a hole in it as opposed to ⁇ :question:

[Joseph Corneli]

Naively substituting in sorry I get this error:

don't know how to synthesize placeholder
context:
exact_list_expr : list expr → tactic unit,
h : expr,
t : list expr,
_x _x _x _x : unit
⊢ Type

That seems a bit suspicious, i.e., _x _x _x _x looks weird.

[Mario Carneiro]

tactic.admit

[Joseph Corneli]

Ah, tactic.admit, I just found it. But impressively it doesn't work.

[Joseph Corneli]

The trace commands are like this:

$  lean refine_rules.lean
refine, initial target:
continuous (λ (x : ℝ), sin (sin x))
REFINE: continuous.comp.{?_mlocal._fresh.13.928650 ?_mlocal._fresh.13.928651 ?_mlocal._fresh.13.928652}
29
apply, initial target:
continuous sin
APPLY: real.continuous_sin
28
refine, initial target:
continuous (λ (x : ℝ), sin x)
REFINE: continuous.comp.{?_mlocal._fresh.13.928650 ?_mlocal._fresh.13.928651 ?_mlocal._fresh.13.928652}
28
apply, initial target:
continuous sin
APPLY: real.continuous_sin
27
refine, initial target:
continuous (λ (x : ℝ), x)
apply, initial target:
continuous (λ (x : ℝ), x)
APPLY: real.continuous_sin
exact, initial target:
continuous (λ (x : ℝ), x)
EXACT: continuous_id.{?_mlocal._fresh.13.928653}
exact, final target:
/Users/joe/my_playground_tidy2/src/refine_rules.lean:87:0: error: tactic failed, there are unsolved goals
state:
⊢ continuous (λ (x : ℝ), x)
theorem continuous_sin_sin : continuous (λ (x : ℝ), sin (sin x)) :=
⁇

[Joseph Corneli]

So it seems to claim there's no target in the last step, but then there are unsolved goals at the end of the run.

[Joseph Corneli]

Oh, maybe this is the difference between pure and return?

[Joseph Corneli]

:fingers_crossed:

[Joseph Corneli]

Nope, that's not the problem.

[Joseph Corneli]

The steps exactly match those of my interactive proof:

lemma continuous_sin_sin' : continuous (λ x : ℝ, sin (sin x)) :=
begin
refine continuous.comp _ _,
apply continuous_sin,
refine continuous.comp _ _,
apply continuous_sin,
exact continuous_id,
end

... well, almost exactly. There's an extra apply but it doesn't change the target.

[Mario Carneiro]

maybe that extra apply made a new subgoal

[Mario Carneiro]

for example if it was continuous.comp and lean said "aha, composition with identity"

[Patrick Massot]

for example if it was continuous.comp and lean said "aha, composition with identity"

If only Lean could stop saying that...

[Mario Carneiro]

there is an easy way to make that happen: take off that dang @[reducible] on comp

[Mario Carneiro]

however in that case this won't match at all because the input is continuous (λ x : ℝ, sin (sin x)) instead of continuous (sin ∘ sin)

[Patrick Massot]

About apply and continuity, would it be evil to change the definition of continuity so that it's no longer a forall? It would feel weird, and many proofs we already have would need to start with a rewrite to get back to the forall definition. But having automatic proofs of continuity of the kind Joe is hoping would be a huge progress (and Isabelle have them). Our stupid manual proofs are very visible in the perfectoid project. They generate many many lines that don't exist in real world

[Mario Carneiro]

an easy way to make it not a forall without really changing anything is to wrap it in a structure

[Mario Carneiro]

with luck you just have to add a few anonymous constructors in places

[Patrick Massot]

This would bring no mathematical benefit. With a different mathematical definition we would at least get some simpler proofs

[Mario Carneiro]

?

[Mario Carneiro]

The current definition is certainly the best one

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L428 could become the definition

[Mario Carneiro]

I want to disturb that as little as possible

[Patrick Massot]

No one would recognize it but it's not a forall

[Mario Carneiro]

Well okay when you put it like that... but it's defeq to the obvious definition

[Patrick Massot]

So apply would fail as well?

[Mario Carneiro]

the usual definition is a forall

[Mario Carneiro]

this one is just a le which unfolds to a forall

[Patrick Massot]

By the way, is the order relation on topological_space and uniform_space open for debate? Currently we have incompatibility with the order on filters, as seen in https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L147-L148 and https://github.com/leanprover-community/mathlib/blob/master/src/topology/uniform_space/basic.lean#L472, generating things like https://github.com/leanprover-community/mathlib/blob/master/src/topology/uniform_space/basic.lean#L542 and generating a push-forward which is right-adjoint to pull-back

[Patrick Massot]

this one is just a le which unfolds to a forall

I understand that, my question is: is this enough to hide from the apply bug?

[Patrick Massot]

As far as I can see, real world never write $t_1 \leq t_2$ for topologies $t_1$ and $t_2$ but write sentences randomly using either the "finer than" or "coarser than" relation

[Mario Carneiro]

you can't hide from the apply bug

[Mario Carneiro]

seriously, it can see through irreducible and theorems, it's crazy

[Joseph Corneli]

Got the example working, thanks to @Chris Hughes for suggesting to use @continuous_id ℝ _.

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 goals:",
                gs ← get_goals,
                mmap infer_type gs >>= trace,
                (refine ``(%%h _ _)),
                --trace "refine, subsequent target:",
                --tactic.target >>= tactic.trace,
                trace (format!" REFINE: {h}"),
                trace "refine, final goals:",
                gs ← get_goals,
                mmap infer_type gs >>= trace,
                pure() <|> refine_list_expr t }

meta def exact_list_expr : list expr → tactic unit
| []     := do {trace "fail", fail "no matching rule"}
| (h::t) := do {trace "exact, initial goals:",
                gs ← get_goals,
                mmap infer_type gs >>= trace,
                trace (format!" EXACT: {h}"),
                -- Some problem here...
                exact h,
                trace "exact, final goals:",
                gs ← get_goals,
                mmap infer_type gs >>= trace,
                pure() <|> exact_list_expr t }

meta def apply_list_expr : list expr → tactic unit
| []     := fail "no matching rule"
| (h::t) := do { trace "apply, initial goals:",
                 gs ← get_goals,
                 mmap infer_type gs >>= trace,
                 trace (format!" APPLY: {h}") ,
                 interactive.concat_tags (apply h),
                 trace "apply, final goals:",
                 gs ← get_goals,
                 mmap infer_type gs >>= trace,
                 pure() <|> apply_list_expr t }

open nat

meta def iterate_at_most_on_all_goals' : nat → tactic unit → tactic unit
| 0        tac := trace "All goals: maximal iterations reached"
| (succ n) tac := tactic.all_goals $ (do tac, trace (format!"All goals:{n}"), iterate_at_most_on_all_goals' n tac) <|> skip

meta def iterate_at_most_on_subgoals' : nat → tactic unit → tactic unit
| 0        tac := trace "Subgoals: maximal iterations reached"
| (succ n) tac := focus1 (do tac, trace (format!"Subgoals:{n}"), iterate_at_most_on_all_goals' n tac)

meta def apply_rules_with_refine (apps : list pexpr) (refs : list pexpr) (exas : list pexpr) (n : nat) : tactic unit :=
do a ← build_list_expr_for_apply apps,
   r ← build_list_expr_for_apply refs,
   e ← build_list_expr_for_apply exas,
   iterate_at_most_on_subgoals' n (assumption
                                    <|> (do t ← tactic.target,
                                          let a := expr.app_arg t,
                                          if (band (expr.is_lambda a)
                                                   (bnot (eq a `(λ (x : ℝ), x))))
                                          then refine_list_expr r
                                          else fail "can't refine")
                                    <|> (sin_sin.apply_list_expr a)),
   sin_sin.exact_list_expr e,
   -- trace "context at the end of the run:",
   -- tactic.local_context >>= tactic.trace,
   -- trace "target at the end of the run:",
   -- tactic.target >>= tactic.trace,
   pure()

end sin_sin
----------------------

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

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

end interactive
end tactic

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

open real

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

#print continuous_sin_sin

[Joseph Corneli]

And @Mario Carneiro thanks for the advice on printing goals, that helped me debug it properly.

[Joseph Corneli]

And I appreciate the comment from @Patrick Massot -- this is only a small step towards a more full automation; a reimplementation of Hanne Gottliebsen's cts tactic from PVS would be impressive :-)

[Mario Carneiro]

what does it do?

[Mario Carneiro]

I mean precisely

[Joseph Corneli]

Much as this example, but for a broader class of functions. So, it would automate continuity proofs for many compositions. It runs into trouble with examples like 1/(cos x + 2).

[Joseph Corneli]

... Compositions, and combinations under arithmetic operations.

[Johan Commelin]

Can we write a tactic that determines whether some expression is a composition or not?

[Johan Commelin]

By inspecting it syntactically

[Mario Carneiro]

yes, that's how this should be done

[Reid Barton]

My continuity tactic does this in a different way

[Reid Barton]

But it waited forever for backwards_reasoning

[Joseph Corneli]

Ah, I had initially set off to write this example with tidy using apply_rules inside, I didn't realise that you could feed individual rules into tidy quite so straightforwardly.

[Joseph Corneli]

@Mario Carneiro I think Reid's tactic is pretty much equivalent to the cts tactic I mentioned. Again it wouldn't do 1/(cos x + 2). The idea I was pursuing in some other threads was to get a bound cos x + 2 > 0 using an SMT solver.

[Mario Carneiro]

why not just spit out a subgoal for it? Proving cos x + 2 != 0 seems out of scope for a continuity prover

[Joseph Corneli]

Well, proving things to be non-zero is needed in order to apply continuous_inv. So, the check would play a similar role to the conditions in Reid's apply_continuous.comp.

[Mario Carneiro]

right, that's why it is a subgoal

[Mario Carneiro]

it's a tactic, you don't have to prove everything