# Zulip Chat Archive

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

?

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

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

what does it do?

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

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