# Zulip Chat Archive

## Stream: maths

### Topic: golfing `Ico` union

#### Yury G. Kudryashov (Jul 25 2020 at 02:25):

I have the following goal:

```
example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c := sorry
```

I know how to prove this using lots of `by_cases`

and `Ico_union_Ico`

. Is there any easier way?

#### Floris van Doorn (Jul 25 2020 at 07:47):

Here it is for decidable linear orders. I think `Ico_union_Ico`

is the most general lemma that "merges" the union of two `Ico`

s (I do have some nonterminal simps in my proof).

After doing all this, I'm not sure if this was actually easier than doing it directly, but `Ico_union_Ico`

is probably also useful for a bunch of other things.

```
lemma Ico_union_Ico' {α} [decidable_linear_order α] {a b c d : α}
(h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) :
Ico a c ∪ Ico b d = Ico a d :=
begin
apply subset.antisymm, apply union_subset; apply Ico_subset_Ico; {refl <|> assumption},
rw ← Ico_union_Ico_eq_Ico h1 (le_trans h2 h3), apply union_subset_union_left,
apply Ico_subset_Ico, refl, assumption
end
lemma Ico_union_Ico {α} [decidable_linear_order α] {a b c d : α}
(h1 : min a b ≤ max c d) (h2 : min c d ≤ max a b) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
begin
cases le_total a b with h3 h3; cases le_total c d with h4 h4; simp [h3, h4] at h1 h2 ⊢,
{ cases le_total a c with h5 h5; cases le_total b d with h6 h6; simp [h5, h6],
{ apply Ico_union_Ico'; assumption },
{ apply union_eq_self_of_subset_right, apply Ico_subset_Ico; assumption },
{ apply union_eq_self_of_subset_left, apply Ico_subset_Ico; assumption },
{ rw union_comm, apply Ico_union_Ico'; assumption },
},
{ simp [h1, h2] },
{ simp [h1, h2] },
{ rw Ico_eq_empty, simp * }
end
lemma Ico_union_Ico_same {α} [decidable_linear_order α] {a b c : α} :
Ico a b ∪ Ico b c = Ico (min a b) (max b c) :=
Ico_union_Ico (le_trans (min_le_right _ _) (le_max_left _ _))
(le_trans (min_le_left _ _) (le_max_right _ _))
example {α} [decidable_linear_order α] (a b c : α) :
Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
begin
rw [Ico_union_Ico_same, Ico_union_Ico, union_comm (Ico b a), Ico_union_Ico_same, Ico_union_Ico],
{ simp only [max_left_comm, min_left_comm, min_comm, max_comm] },
all_goals { simp, finish },
end
```

#### Kevin Buzzard (Jul 25 2020 at 08:15):

I think the proof should be: WLOG a<=b<=c; linarith.

#### Kevin Buzzard (Jul 25 2020 at 08:16):

The theorem statement is S3-invariant.

#### Kevin Buzzard (Jul 25 2020 at 08:35):

Aah I see, you still have to do a case split on X<b

#### Kevin Buzzard (Jul 25 2020 at 09:15):

```
import tactic
import data.real.basic
open set
lemma Ico_union_Ico {a b c d : ℝ}
(h1 : min a b ≤ max c d) (h2 : min c d ≤ max a b) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
begin
ext x,
split,
all_goals {intro h},
all_goals {try {cases h with h3 h4}},
all_goals {unfold min max Ico at *},
-- split_ifs at * leads to a weird state with multiple copies of variables :-(
all_goals {try {split_ifs at h1}},
all_goals {try {split_ifs at h2}},
all_goals {try {split_ifs at h3}},
all_goals {try {split_ifs at h4}},
all_goals {try {split_ifs}},
all_goals {try {split}},
-- 144 goals at this point
all_goals {try {cases h3}},
all_goals {try {cases h4}},
all_goals {try {linarith}},
all_goals {try {left, split; linarith}},
all_goals {try {right, split; linarith}},
-- two left
all_goals {by_cases h5 : x < b},
all_goals {try {left, split; linarith}},
all_goals {try {right, split; linarith}},
/-
abcdx: ℝ
h: a ≤ b
h_1: c ≤ d
h1: a ≤ d
h_2: c ≤ d
h2: c ≤ b
h_3: ¬a ≤ c
h3: c ≤ x
h_4: ¬b ≤ d
h4: x < b
h5: x < b
⊢ x ∈ {x : ℝ | a ≤ x ∧ x < b} ∪ {x : ℝ | c ≤ x ∧ x < d}
-/
sorry
end
```

If you do `split_ifs at *`

you can end up with five variables called a sometimes. I was using semicolons but all_goals is clearer. I got from 1 goal to 160 and then back down to 1 but I didn't quite finish and now I have to go :-/ Do I need one more case split? Why do I need case splits? Is there something that linarith doesn't know? Would like to diagnose but have family duties

#### Kenny Lau (Jul 25 2020 at 09:18):

@Kevin Buzzard what's the maths proof that isn't "draw a picture"?

#### Kevin Buzzard (Jul 25 2020 at 09:21):

I just posted it: get the tactics to draw the picture

#### Kevin Buzzard (Jul 25 2020 at 09:52):

Why can't I close my last goal? c<a<=d<b

#### Jasmin Blanchette (Jul 25 2020 at 11:02):

Because no hammer?

Screen-Shot-2020-07-25-at-13.01.42.png

#### Jasmin Blanchette (Jul 25 2020 at 11:03):

(In turn, because excruciatingly low Lean 3 metaprogramming framework.)

#### Kevin Buzzard (Jul 25 2020 at 11:22):

Yeah that's the correct proof

#### Kevin Buzzard (Jul 25 2020 at 11:22):

"It's obvious"

#### Floris van Doorn (Jul 25 2020 at 16:09):

Yes, we do miss sledgehammer in Lean.

However, many of your conjunctions should be disjunctions: you only know

```
h1 : a ≤ c ∨ b ≤ c ∨ a ≤ d ∨ b ≤ d,
h2 : c ≤ a ∨ d ≤ a ∨ c ≤ b ∨ d ≤ b
```

#### Floris van Doorn (Jul 25 2020 at 16:09):

@Jasmin Blanchette

#### Floris van Doorn (Jul 25 2020 at 16:10):

Oh sorry, you responded to Kevin, you were not golfing my lemma. My bad.

#### Floris van Doorn (Jul 25 2020 at 16:11):

Does sledgehammer solve the complete lemma by itself?

#### Patrick Massot (Jul 25 2020 at 16:23):

The screenshot suggests we miss `auto`

or `force`

, not really sledgehammer (unless you consider these to be part of sledgehammer).

#### Yury G. Kudryashov (Jul 25 2020 at 17:07):

I came up with the following (for a `decidable_linear_order`

):

```
lemma Ico_union_Ico_union_Ico_cycle :
Ico a b ∪ Ico b c ∪ Ico c a = Ico (min a (min b c)) (max a (max b c)) :=
ext $ λ x, by simp [iff_def, or_imp_distrib, lt_or_le] { contextual := tt };
simp [← or_assoc, or_comm, lt_or_le]
```

#### Patrick Massot (Jul 25 2020 at 17:12):

It would be really nice to have a tactic doing this is a pretty general context.

#### Jasmin Blanchette (Jul 25 2020 at 18:16):

@Floris: I can't test easily without knowing what `Ico`

is.

#### Reid Barton (Jul 25 2020 at 18:20):

#### Jasmin Blanchette (Jul 25 2020 at 18:25):

@Patrick Massot another proof is possible with Isabelle's `simp`

+ `linarith`

.

#### Mario Carneiro (Jul 25 2020 at 18:51):

Here's a more basic proof along the lines of floris's first proof:

```
lemma Ico_union_Ico {α} [decidable_linear_order α] {a b c d : α}
(h1 : min a b ≤ max c d) (h2 : min c d ≤ max a b) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
begin
apply subset.antisymm,
{ apply union_subset; apply Ico_subset_Ico; simp [le_refl] },
rintro x ⟨h3, h4⟩; simp at h3 h4 ⊢,
cases h3; cases h4; simp [h3, h4]; by_contra hn; push_neg at hn; cases hn with h5 h6,
{ exact not_le_of_lt (lt_min h6 h4) (le_trans h2 (max_le h3 h5)) },
{ exact not_le_of_lt (lt_min h5 h4) (le_trans h1 (max_le h3 h6)) }
end
```

I tried `linarith`

on the last two goals but it didn't work, does it not do proofs in pure inequality structures?

#### Gabriel Ebner (Jul 25 2020 at 19:17):

Golfed:

```
lemma Ico_Ico_Ico {α} [linear_order α] (a b c : α) :
Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
by ext; split; finish using [lt_of_le_of_lt, lt_of_lt_of_le, lt_irrefl] {max_ematch_rounds := 2}
```

(Please don't run the profiler on this.)

#### Gabriel Ebner (Jul 25 2020 at 19:52):

Slightly faster (five seconds):

```
lemma Ico_Ico_Ico {α} [linear_order α] (a b c : α) :
Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
by ext; simp; super with lt_irrefl lt_of_lt_of_le lt_of_le_of_lt le_or_lt {timeout := 50000}
```

This should be acceptably fast in :four_leaf_clover:.

#### Patrick Massot (Jul 25 2020 at 20:56):

Jasmin Blanchette said:

Patrick Massot another proof is possible with Isabelle's

`simp`

+`linarith`

.

We want all of this :grinning:

#### Yury G. Kudryashov (Jul 25 2020 at 23:58):

Note that we can't use Lean `linarith`

because we have only `(decidable_)linear_order`

, no `ordered_field`

.

#### Yury G. Kudryashov (Jul 25 2020 at 23:59):

BTW, @Jasmin Blanchette what does Isabelle say in this context (`linear_order`

only)?

#### Sebastien Gouezel (Jul 26 2020 at 07:33):

```
lemma auto_is_strong:
fixes a b c::"'a::linorder"
shows "{a ..< b} ∪ {b ..< c} ∪ {c ..< a} = {b ..< a} ∪ {c ..< b} ∪ {a ..< c}"
by auto
```

#### Sebastien Gouezel (Jul 26 2020 at 07:34):

(takes less than 1/10s)

#### Sebastien Gouezel (Jul 26 2020 at 07:36):

I guess `auto`

will use some `simp`

lemmas that will depend on the order of the points, then split automatically on case disjunction, then use some version of linarith that works in linear orders, but I don't know how to ask details about the proof.

#### Sebastien Gouezel (Jul 26 2020 at 08:00):

In fact, I don't think it uses any fancy version of linarith. Probably it only applies `lt_of_le`

, `lt_trans`

a few times (at most 5, say), see all the consequences it gets from this, and then sees if the goal is in there (but in a more efficient way called a tableau prover). Essentially what Gabriel did with its `super`

invocation, in fact. Except that it is really fast in Isabelle, and completely automatic.

#### Jasmin Blanchette (Jul 26 2020 at 08:26):

@Jannis Limperg I hope you are paying attention. ;)

#### Kenny Lau (Jul 26 2020 at 08:29):

```
import data.set.intervals.basic
open set
example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
begin
cases le_total a b with hab hba; cases le_total b c with hbc hcb,
{ rw [Ico_eq_empty hab, Ico_eq_empty hbc, Ico_eq_empty (le_trans hab hbc),
empty_union, empty_union, union_empty, Ico_union_Ico_eq_Ico hab hbc] },
{ cases le_total a c with hac hca,
{ rw [Ico_eq_empty hac, Ico_eq_empty hcb, Ico_eq_empty hab,
empty_union, union_empty, union_empty, union_comm, Ico_union_Ico_eq_Ico hac hcb] },
{ rw [Ico_eq_empty hca, Ico_eq_empty hcb, Ico_eq_empty hab,
empty_union, union_empty, union_empty, union_comm, Ico_union_Ico_eq_Ico hca hab] } },
{ cases le_total a c with hac hca,
{ rw [Ico_eq_empty hac, Ico_eq_empty hbc, Ico_eq_empty hba,
empty_union, union_empty, union_empty, Ico_union_Ico_eq_Ico hba hac] },
{ rw [Ico_eq_empty hca, Ico_eq_empty hbc, Ico_eq_empty hba,
empty_union, union_empty, union_empty, Ico_union_Ico_eq_Ico hbc hca] } },
{ rw [Ico_eq_empty hcb, Ico_eq_empty hba, Ico_eq_empty (le_trans hcb hba),
empty_union, empty_union, union_empty, union_comm, Ico_union_Ico_eq_Ico hcb hba] }
end
```

#### Kevin Buzzard (Jul 26 2020 at 08:29):

Yury G. Kudryashov said:

I know how to prove this using lots of

`by_cases`

and`Ico_union_Ico`

. Is there any easier way?

#### Kevin Buzzard (Jul 26 2020 at 08:30):

So what is `auto`

?

#### Sebastien Gouezel (Jul 26 2020 at 09:02):

From https://people.mpi-inf.mpg.de/~jblanche/frocos2011-dis-proof.pdf:

On the user level, the simplifier is eclipsed by auto, a proof method that interleaves simplification with a small amount of proof search. It is impossible to describe suc-cinctly what auto does due to its heuristic, ad hoc nature. Its great strength is its ability to discharge the easy parts of a goal and leave the user with the more difficult ones. This helps the user to quickly focus on the core of a problem.Strengthened versions of auto perform more sophisticated proof search, while still interleaving it with simplification. The search is based on tableau methods [39]. These methods are often useful, but since search is involved, not only are they slower than the simplifier and auto, they are endgame provers that do not provide any hints when they fail to prove the goal

@Jasmin Blanchette , do you know of a reference describing a little bit more of the internals of `auto`

? I think I miss it in Lean even more than sledgehammer...

#### Mario Carneiro (Jul 26 2020 at 09:10):

I've read descriptions of `auto`

like that several times before and it's indistinguishable from "auto is magic"

#### Mario Carneiro (Jul 26 2020 at 09:11):

and as a user it also is difficult to demystify by watching it work

#### Sebastien Gouezel (Jul 26 2020 at 09:32):

Apparently (see the code at http://isabelle.in.tum.de/repos/isabelle/file/f3e1144a1cec/src/Provers/clasimp.ML), it combines blast (https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/blast.pdf) with the simplifier.

#### Patrick Massot (Jul 26 2020 at 09:46):

Mario Carneiro said:

I've read descriptions of

`auto`

like that several times before and it's indistinguishable from "auto is magic"

This sounds like the holy grail of interactive theorem proving: a tactic that proves obvious goals without any need to understand how it works.

#### Mario Carneiro (Jul 26 2020 at 09:48):

I generally have a bad experience with "magic" tactics. If it actually solves all goals I care about, well that's great, but that's also a pipe dream. Unless I understand the failure modes, I won't be able to use it effectively

#### Mario Carneiro (Jul 26 2020 at 09:49):

I remember working in isabelle during a tutorial, this was my number one complaint - everything was "by auto" and I didn't even understand what the syntax of tactic proofs was (and of course I can't ask isabelle to show me the proof either). It was very unsatisfying

#### Jasmin Blanchette (Jul 26 2020 at 09:50):

`auto`

isn't that magic. It's really simplifier + some intro and elim rules, some applied aggressively, some not (with backtracking). From its output, which is similar to the simplifier's except that you can get multiple subgols, you can usually tell "oh, I forgot to register commutativity of `foo`

as a `simp`

rule".

#### Sebastien Gouezel (Jul 26 2020 at 09:50):

`auto`

is not a closing tactic: it takes care of what it can, and leaves you with the remaining goals. And you can tweak it like `(auto simp: foo bar intro: foo' bar')`

telling it to add `foo`

and `bar`

to the simpset during this run, and to apply the lemmas `foo'`

and `bar'`

whenever it can. When you are used to it, it is incredibly efficient.

#### Jasmin Blanchette (Jul 26 2020 at 09:51):

But indeed, it would be nice if `auto`

had some detailed output, or at least existed in some `squeeze_auto`

fashion.

#### Jasmin Blanchette (Jul 26 2020 at 09:51):

And if `auto`

were ever reproduced in Lean, it would have to have better output.

#### Jasmin Blanchette (Jul 26 2020 at 09:52):

As for the reference: I'm not aware of any.

#### Mario Carneiro (Jul 26 2020 at 09:53):

how important is heuristic instantiation for `auto`

?

#### Mario Carneiro (Jul 26 2020 at 09:54):

Does it differ in any important way from `tidy`

? If it's just "case on or, split on and, simp" then `tidy`

does that already

#### Sebastien Gouezel (Jul 26 2020 at 09:55):

`auto`

does backtracking.

#### Mario Carneiro (Jul 26 2020 at 09:57):

what do you get in an `auto`

failure if it backtracks?

#### Sebastien Gouezel (Jul 26 2020 at 10:15):

Auto does several things:

- it applies the simplifier (always).
- there are some lemmas that it will always apply if they make sense. No backtracking involved. Typically you are left with several subgoals afterwards.
- there are somme lemmas that it will apply if after applying them it is able to prove the goal (or the part of the goal it is working on). Here backtracking happens.

This means that on some subgoals it will try to find a proof and if it doesn't it will just leave you the subgoal untouched. Other subgoals will be solved thanks to backtracking and proof search. Typically, in the end you will just be left with the nontrivial remaining subgoals, a.k.a., the interesting part of the proof.

#### Sebastien Gouezel (Jul 26 2020 at 10:17):

(NB: this is what I understood from playing quite some time with Isabelle, I have never looked at auto's inner workings)

#### Kenny Lau (Jul 26 2020 at 10:19):

then how do you do all that in 1/10 s?

#### Sebastien Gouezel (Jul 26 2020 at 10:20):

That's Isabelle and simple type theory (no unification, no implicit parameters, and so on).

#### Mario Carneiro (Jul 26 2020 at 10:26):

so what are intro and elim rules and how do they contribute to that overall structure?

#### Mario Carneiro (Jul 26 2020 at 10:27):

I understand that these have to be annotated in the library, yes?

#### Sebastien Gouezel (Jul 26 2020 at 10:29):

Yes. You have `intro!`

lemmas (i.e., lemmas tagged with this attribute in the library), which are lemmas that auto should always apply when they make sense, and `intro`

(or `intro?`

) lemmas that will only be applied in the middle of a proof search process with backtracking. And elim I never really understood :-)

#### Sebastien Gouezel (Jul 26 2020 at 10:32):

Note that the `intro!`

lemmas are not equivalences in general, so maybe a statement that was provable is not provable any more after applying `auto`

. But when a lemma is the right thing to do like 95% of the time, it is a good idea to mark it at `intro!`

(and of course the intro set can be tweaked in an invocation of auto).

#### Mario Carneiro (Jul 26 2020 at 10:33):

Does `simplify`

have its own annotation e.g. `simp`

? Or does it reuse `intro`

and `elim`

in some way

#### Sebastien Gouezel (Jul 26 2020 at 10:35):

You also have `simp`

tags, yes. You have 3 different kinds of lemmas, the simp ones, the intro ones, and the elim ones.

#### Mario Carneiro (Jul 26 2020 at 10:36):

Lean also has `intro`

and `intro!`

attributes, but no one knows what they do :)

#### Sebastien Gouezel (Jul 26 2020 at 10:43):

Probably they don't do anything for now because we don't have auto, but they have been planned a long way ahead!

#### Patrick Massot (Jul 26 2020 at 10:44):

That's not true.

#### Patrick Massot (Jul 26 2020 at 10:44):

I know what they do.

#### Patrick Massot (Jul 26 2020 at 10:45):

https://github.com/leanprover-community/lean/blob/master/library/init/meta/backward.lean

#### Mario Carneiro (Jul 26 2020 at 10:46):

we should give `back_chaining`

an interactive front end and try using it

#### Sebastien Gouezel (Jul 26 2020 at 10:47):

Is it like `apply_rules`

?

#### Mario Carneiro (Jul 26 2020 at 10:47):

pretty sure

#### Patrick Massot (Jul 26 2020 at 10:47):

Yes, it's Leo's version of apply_rules.

#### Patrick Massot (Jul 26 2020 at 10:48):

But it's clearly an experiment that was mostly abandonned.

#### Mario Carneiro (Jul 26 2020 at 10:48):

does it do things?

#### Sebastien Gouezel (Jul 26 2020 at 10:48):

I've done `apply_rules`

because I was longing for auto and I couldn't do anything smarter, but I'm pretty sure Leo's version is much better!

#### Mario Carneiro (Jul 26 2020 at 10:49):

the problem with relying on leo's tactics is that they don't get maintenance because no one knows the code

#### Mario Carneiro (Jul 26 2020 at 10:49):

the smt/eblast stuff died for basically that reason

#### Mario Carneiro (Jul 26 2020 at 10:50):

honestly `simp`

has held up pretty well all things considered

#### Mario Carneiro (Jul 26 2020 at 10:52):

but if you are okay with using them as is then I don't see why we can't give a nice front end to the tactic and see if it's any good

#### Mario Carneiro (Jul 26 2020 at 10:56):

It passes the basic test:

```
example {n : ℕ} : n ≤ n ⊔ n ⊔ n :=
by apply_rules [le_sup_left_of_le, le_refl]
example {n : ℕ} : n ≤ n ⊔ n ⊔ n :=
by do
[`le_sup_left_of_le, `le_refl].mmap tactic.mk_const >>=
tactic.back_chaining_using
```

#### Kenny Lau (Jul 26 2020 at 10:59):

we don't need more powerful tactics; we need more basic tactics and more creative proofs:

```
import data.set.intervals.basic tactic
open set
meta def unions' : tactic unit :=
`[try { refl' <|> { apply subset_union_of_subset_left, unions' } <|> { apply subset_union_of_subset_right, unions' }}]
meta def unions : tactic unit :=
`[{ apply union_subset; unions } <|> unions']
example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
subset.antisymm (subset.trans (union_subset_union (union_subset_union
(@Ico_subset_Ico_union_Ico _ _ a c b) (@Ico_subset_Ico_union_Ico _ _ b a c)) (@Ico_subset_Ico_union_Ico _ _ c b a)) (by unions))
(subset.trans (union_subset_union (union_subset_union
(@Ico_subset_Ico_union_Ico _ _ b c a) (@Ico_subset_Ico_union_Ico _ _ c a b)) (@Ico_subset_Ico_union_Ico _ _ a b c)) (by unions))
```

#### Kenny Lau (Jul 26 2020 at 11:09):

turns out Lean is pretty smart:

```
import data.set.intervals.basic tactic
open set
meta def unions' : tactic unit :=
`[try { refl' <|> { apply subset_union_of_subset_left, unions' } <|> { apply subset_union_of_subset_right, unions' }}]
meta def unions : tactic unit :=
`[{ apply union_subset; unions } <|> unions']
example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
subset.antisymm (subset.trans (union_subset_union (union_subset_union
Ico_subset_Ico_union_Ico Ico_subset_Ico_union_Ico) Ico_subset_Ico_union_Ico) (by unions))
(subset.trans (union_subset_union (union_subset_union
Ico_subset_Ico_union_Ico Ico_subset_Ico_union_Ico) Ico_subset_Ico_union_Ico) (by unions))
```

#### Sebastien Gouezel (Jul 26 2020 at 11:24):

Kenny Lau said:

we don't need more powerful tactics

Come on Kenny! Would you complain if you had a tactic `auto`

which could close this lemma with `by auto`

in 1/10s?

#### Gabriel Ebner (Jul 26 2020 at 11:35):

Mario Carneiro said:

we should give

`back_chaining`

an interactive front end and try using it

I think `auto`

would be great to have. Note that `back_chaining`

only does a third of auto: namely applying the "intro" rules. My gut feeling is that most of the work of creating a Lean version of `auto`

would consist of judiciously adding `intro`

and `elim`

attributes. These sets require just as much care, effort, and curation as the simp set.

#### Mario Carneiro (Jul 26 2020 at 11:38):

It actually has a bit of the other parts of `auto`

as well, because the core tactic also includes a `pre_tactic`

and `leaf_tactic`

for interoperating with the backtracking search. If you put in `simp`

as the `pre_tactic`

it seems like you've got 2/3 of `auto`

#### Mario Carneiro (Jul 26 2020 at 11:38):

I definitely agree that it is important for us to start curating the `intro`

set

#### Mario Carneiro (Jul 26 2020 at 11:39):

I suspect that there is a chicken and egg problem with getting a good `intro`

set vs getting the `auto`

tactic working

#### Gabriel Ebner (Jul 26 2020 at 11:40):

Don't forget the `elim`

set.

#### Mario Carneiro (Jul 26 2020 at 11:40):

Do you know what that is? Sebastien didn't above

#### Gabriel Ebner (Jul 26 2020 at 11:42):

`intro`

lemmas are used with `apply`

, i.e. they only apply to the target of the goal. `elim`

lemmas are similar to `cases`

, they apply to the hypotheses.

#### Gabriel Ebner (Jul 26 2020 at 11:42):

E.g., if you have an assumption `∃ x, p x`

then you want to apply docs#exists.elim

#### Mario Carneiro (Jul 26 2020 at 11:43):

do you think we should use curated lemmas for that? Unlike isabelle we get most of that for free by using `cases`

#### Mario Carneiro (Jul 26 2020 at 11:43):

but maybe there are things like custom recursors we should be applying instead

#### Mario Carneiro (Jul 26 2020 at 11:43):

do you know examples of elim rules that are not just subsets of `cases`

behavior?

#### Jasmin Blanchette (Jul 26 2020 at 15:20):

I'd consider using the `intro!`

attribute globally for a unidirectional rule (i.e., one that doesn't preserve provability) a bug. The whole point is that these "safe" rules should be applied exhaustively, like `simp`

s, without loss of generality.

#### Mario Carneiro (Jul 26 2020 at 15:26):

An example of a unidirectional `intro!`

rule would be something like closure for division like `x \in real /\ y \in real /\ y != 0 -> x / y \in real`

for a hypothetical typing predicate for real division (maybe these are ZFC reals or something so that typing is a theorem)

#### Mario Carneiro (Jul 26 2020 at 15:27):

in fact even setting aside partial functions, something like `x \in real /\ y \in real -> x + y \in real`

might very well not be bidirectional

#### Sebastien Gouezel (Jul 26 2020 at 15:36):

For another example, if you want to prove `continuous (f + g)`

, it seems to me completely reasonable to apply `continuous.add`

and reduce it to the continuity of `f`

and `g`

, although of course you can have discontinuous functions whose sum is continuous, but this should never show up in real proofs.

#### Sebastien Gouezel (Jul 26 2020 at 15:37):

A rule that does preserve provability could instead be written as an iff and registered as a simp lemma, so to me the whole point of `intro!`

is for rules that don't preserve provability but are completely reasonable like the continuity example.

#### Jasmin Blanchette (Jul 26 2020 at 15:51):

I'd say that's the point of `intro`

.

#### Jasmin Blanchette (Jul 26 2020 at 15:53):

See e.g. http://www21.in.tum.de/~ballarin/fomus/part1/part1.pdf

#### Jasmin Blanchette (Jul 26 2020 at 15:53):

Search for "safe" and "unsafe" throughout.

#### Jannis Limperg (Aug 02 2020 at 21:52):

Jasmin Blanchette said:

Jannis Limperg I hope you are paying attention. ;)

I wasn't because I'm not subscribed to this stream, in which case I apparently don't even get notified if I'm @-mentioned. -.- Am now though.

#### Jalex Stark (Aug 03 2020 at 00:08):

When you @ someone who is not subscribed to the stream you're posting in, there should be a prompt to invite them to the stream

Last updated: May 10 2021 at 07:15 UTC