Zulip Chat Archive

Stream: maths

Topic: golfing `Ico` union


view this post on Zulip 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?

view this post on Zulip 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 Icos (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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:15):

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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:16):

The theorem statement is S3-invariant.

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:35):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 25 2020 at 09:18):

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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 09:21):

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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 09:52):

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

view this post on Zulip Jasmin Blanchette (Jul 25 2020 at 11:02):

Because no hammer?
Screen-Shot-2020-07-25-at-13.01.42.png

view this post on Zulip Jasmin Blanchette (Jul 25 2020 at 11:03):

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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:22):

Yeah that's the correct proof

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:22):

"It's obvious"

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Jul 25 2020 at 16:09):

@Jasmin Blanchette

view this post on Zulip Floris van Doorn (Jul 25 2020 at 16:10):

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

view this post on Zulip Floris van Doorn (Jul 25 2020 at 16:11):

Does sledgehammer solve the complete lemma by itself?

view this post on Zulip 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).

view this post on Zulip 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]

view this post on Zulip Patrick Massot (Jul 25 2020 at 17:12):

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

view this post on Zulip Jasmin Blanchette (Jul 25 2020 at 18:16):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:20):

src#set.Ico

view this post on Zulip Jasmin Blanchette (Jul 25 2020 at 18:25):

@Patrick Massot another proof is possible with Isabelle's simp + linarith.

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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:.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 23:59):

BTW, @Jasmin Blanchette what does Isabelle say in this context (linear_order only)?

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Jul 26 2020 at 07:34):

(takes less than 1/10s)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jul 26 2020 at 08:26):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 08:30):

So what is auto?

view this post on Zulip 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...

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Jul 26 2020 at 09:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jul 26 2020 at 09:51):

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

view this post on Zulip Jasmin Blanchette (Jul 26 2020 at 09:52):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 09:53):

how important is heuristic instantiation for auto?

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Jul 26 2020 at 09:55):

auto does backtracking.

view this post on Zulip Mario Carneiro (Jul 26 2020 at 09:57):

what do you get in an auto failure if it backtracks?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 26 2020 at 10:19):

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

view this post on Zulip Sebastien Gouezel (Jul 26 2020 at 10:20):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:26):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:27):

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

view this post on Zulip 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 :-)

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:36):

Lean also has intro and intro! attributes, but no one knows what they do :)

view this post on Zulip 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!

view this post on Zulip Patrick Massot (Jul 26 2020 at 10:44):

That's not true.

view this post on Zulip Patrick Massot (Jul 26 2020 at 10:44):

I know what they do.

view this post on Zulip Patrick Massot (Jul 26 2020 at 10:45):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:46):

we should give back_chaining an interactive front end and try using it

view this post on Zulip Sebastien Gouezel (Jul 26 2020 at 10:47):

Is it like apply_rules?

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:47):

pretty sure

view this post on Zulip Patrick Massot (Jul 26 2020 at 10:47):

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

view this post on Zulip Patrick Massot (Jul 26 2020 at 10:48):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:48):

does it do things?

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:49):

the smt/eblast stuff died for basically that reason

view this post on Zulip Mario Carneiro (Jul 26 2020 at 10:50):

honestly simp has held up pretty well all things considered

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip 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))

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:38):

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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jul 26 2020 at 11:40):

Don't forget the elim set.

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:43):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:43):

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

view this post on Zulip 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 simps, without loss of generality.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Jul 26 2020 at 15:51):

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

view this post on Zulip Jasmin Blanchette (Jul 26 2020 at 15:53):

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

view this post on Zulip Jasmin Blanchette (Jul 26 2020 at 15:53):

Search for "safe" and "unsafe" throughout.

view this post on Zulip 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.

view this post on Zulip 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