Zulip Chat Archive

Stream: maths

Topic: apply_rules example


view this post on Zulip Joseph Corneli (May 17 2019 at 15:45):

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

view this post on Zulip Joseph Corneli (May 17 2019 at 15:47):

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

view this post on Zulip Joseph Corneli (May 17 2019 at 16:01):

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

view this post on Zulip Reid Barton (May 17 2019 at 16:13):

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 UU, if UU 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.

view this post on Zulip Jesse Michael Han (May 17 2019 at 16:54):

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

view this post on Zulip Chris Hughes (May 17 2019 at 16:56):

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.

view this post on Zulip Jesse Michael Han (May 17 2019 at 17:06):

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

view this post on Zulip Chris Hughes (May 17 2019 at 17:31):

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.

view this post on Zulip Joseph Corneli (May 17 2019 at 17:34):

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.

view this post on Zulip Jesse Michael Han (May 17 2019 at 17:52):

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

view this post on Zulip Jesse Michael Han (May 17 2019 at 17:54):

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

view this post on Zulip Joseph Corneli (May 17 2019 at 18:05):

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.

view this post on Zulip Chris Hughes (May 17 2019 at 18:05):

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.

view this post on Zulip Jesse Michael Han (May 17 2019 at 18:08):

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

view this post on Zulip Mario Carneiro (May 17 2019 at 18:14):

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

view this post on Zulip Joseph Corneli (May 17 2019 at 18:26):

I posted the code in the new members list.

view this post on Zulip Joseph Corneli (May 20 2019 at 13:47):

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

view this post on Zulip Joseph Corneli (May 20 2019 at 13:50):

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.

view this post on Zulip Joseph Corneli (May 21 2019 at 11:51):

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:

view this post on Zulip Joseph Corneli (May 21 2019 at 11:51):

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.

view this post on Zulip Mario Carneiro (May 21 2019 at 11:57):

tactic.admit

view this post on Zulip Joseph Corneli (May 21 2019 at 11:58):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 11:59):

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)) :=
⁇

view this post on Zulip Joseph Corneli (May 21 2019 at 12:00):

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.

view this post on Zulip Joseph Corneli (May 21 2019 at 12:02):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 12:02):

:fingers_crossed:

view this post on Zulip Joseph Corneli (May 21 2019 at 12:03):

Nope, that's not the problem.

view this post on Zulip Joseph Corneli (May 21 2019 at 12:10):

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.

view this post on Zulip Mario Carneiro (May 21 2019 at 12:13):

maybe that extra apply made a new subgoal

view this post on Zulip Mario Carneiro (May 21 2019 at 12:13):

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

view this post on Zulip Patrick Massot (May 21 2019 at 13:09):

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

If only Lean could stop saying that...

view this post on Zulip Mario Carneiro (May 21 2019 at 13:11):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:12):

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

view this post on Zulip Patrick Massot (May 21 2019 at 13:12):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:13):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:13):

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

view this post on Zulip Patrick Massot (May 21 2019 at 13:17):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:17):

?

view this post on Zulip Mario Carneiro (May 21 2019 at 13:17):

The current definition is certainly the best one

view this post on Zulip Patrick Massot (May 21 2019 at 13:18):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:18):

I want to disturb that as little as possible

view this post on Zulip Patrick Massot (May 21 2019 at 13:18):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:18):

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

view this post on Zulip Patrick Massot (May 21 2019 at 13:19):

So apply would fail as well?

view this post on Zulip Mario Carneiro (May 21 2019 at 13:19):

the usual definition is a forall

view this post on Zulip Mario Carneiro (May 21 2019 at 13:20):

this one is just a le which unfolds to a forall

view this post on Zulip Patrick Massot (May 21 2019 at 13:22):

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

view this post on Zulip Patrick Massot (May 21 2019 at 13:23):

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?

view this post on Zulip Patrick Massot (May 21 2019 at 13:24):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:25):

you can't hide from the apply bug

view this post on Zulip Mario Carneiro (May 21 2019 at 13:26):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 13:32):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 13:33):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 13:36):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 13:36):

what does it do?

view this post on Zulip Mario Carneiro (May 21 2019 at 13:37):

I mean precisely

view this post on Zulip Joseph Corneli (May 21 2019 at 13:42):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 13:42):

... Compositions, and combinations under arithmetic operations.

view this post on Zulip Johan Commelin (May 21 2019 at 13:49):

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

view this post on Zulip Johan Commelin (May 21 2019 at 13:49):

By inspecting it syntactically

view this post on Zulip Mario Carneiro (May 21 2019 at 13:51):

yes, that's how this should be done

view this post on Zulip Reid Barton (May 21 2019 at 13:52):

My continuity tactic does this in a different way

view this post on Zulip Reid Barton (May 21 2019 at 13:52):

But it waited forever for backwards_reasoning

view this post on Zulip Joseph Corneli (May 21 2019 at 13:55):

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.

view this post on Zulip Joseph Corneli (May 21 2019 at 14:01):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 14:02):

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

view this post on Zulip Joseph Corneli (May 21 2019 at 14:07):

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.

view this post on Zulip Mario Carneiro (May 21 2019 at 14:08):

right, that's why it is a subgoal

view this post on Zulip Mario Carneiro (May 21 2019 at 14:08):

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


Last updated: May 11 2021 at 15:12 UTC