## Stream: maths

### Topic: apply_rules example

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


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

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


#### 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 $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 (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

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

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

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

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

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

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

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

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

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

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

#### Joseph Corneli (May 17 2019 at 18:26):

I posted the code in the new members list.

#### 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  #### 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. #### 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: #### 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. #### Mario Carneiro (May 21 2019 at 11:57): tactic.admit #### Joseph Corneli (May 21 2019 at 11:58): Ah, tactic.admit, I just found it. But impressively it doesn't work. #### 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)) :=
⁇


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

#### Joseph Corneli (May 21 2019 at 12:02):

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

#### Joseph Corneli (May 21 2019 at 12:02):

:fingers_crossed:

#### Joseph Corneli (May 21 2019 at 12:03):

Nope, that's not the problem.

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

#### Mario Carneiro (May 21 2019 at 12:13):

maybe that extra apply made a new subgoal

#### Mario Carneiro (May 21 2019 at 12:13):

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

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

#### Mario Carneiro (May 21 2019 at 13:11):

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

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

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

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

#### Mario Carneiro (May 21 2019 at 13:13):

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

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

?

#### Mario Carneiro (May 21 2019 at 13:17):

The current definition is certainly the best one

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

#### Mario Carneiro (May 21 2019 at 13:18):

I want to disturb that as little as possible

#### Patrick Massot (May 21 2019 at 13:18):

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

#### Mario Carneiro (May 21 2019 at 13:18):

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

#### Patrick Massot (May 21 2019 at 13:19):

So apply would fail as well?

#### Mario Carneiro (May 21 2019 at 13:19):

the usual definition is a forall

#### Mario Carneiro (May 21 2019 at 13:20):

this one is just a le which unfolds to a forall

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

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

#### Patrick Massot (May 21 2019 at 13:24):

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 (May 21 2019 at 13:25):

you can't hide from the apply bug

#### Mario Carneiro (May 21 2019 at 13:26):

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

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


#### Joseph Corneli (May 21 2019 at 13:33):

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

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

what does it do?

I mean precisely

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

#### Joseph Corneli (May 21 2019 at 13:42):

... Compositions, and combinations under arithmetic operations.

#### Johan Commelin (May 21 2019 at 13:49):

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

#### Johan Commelin (May 21 2019 at 13:49):

By inspecting it syntactically

#### Mario Carneiro (May 21 2019 at 13:51):

yes, that's how this should be done

#### Reid Barton (May 21 2019 at 13:52):

My continuity tactic does this in a different way

#### Reid Barton (May 21 2019 at 13:52):

But it waited forever for backwards_reasoning

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

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

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

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

#### Mario Carneiro (May 21 2019 at 14:08):

right, that's why it is a subgoal

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