Zulip Chat Archive

Stream: general

Topic: tfae bug


view this post on Zulip Patrick Massot (Oct 05 2018 at 06:59):

Minimized from the open maps thread:

example (α : Type) (P Q R : α  Prop) : tfae [ x, P x,  x, Q x,  x, R x] :=
begin
  tfae_have : 1  3, by sorry,
  tfae_have : 3  1, by sorry,
  tfae_have : 3  2, by sorry,
  tfae_finish,
end

fails with: exact tactic failed, type mismatch, given expression has type (∀ (x : α), Q x) ↔ ∀ (x : α), R x but is expected to have type (∀ (x : α), Q x) ↔ ∀ (x : α), P x

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:02):

I'm on it

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:03):

Note that removing the forall hides the issue

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:03):

Does it? That's odd

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:06):

maybe not

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:06):

I changed many times what I tried

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:06):

And also, undo in VScode vim extension is completely crazy, you never know how many steps you will go back

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:09):

Wow, I see completely random behavior

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:09):

I have a series of test cases, restarting Lean server changes the set of failing tests randomly

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:09):

Heisenbugs!

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:11):

A Heisenbug in a theorem prover — the irony

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:11):

My test file is

import tactic.tfae

example (P Q R : Prop) : tfae [P, Q, R] :=
begin
  tfae_have : 1  2, by sorry,
  tfae_have : 2  1, by sorry,
  tfae_have : 3  1, by sorry,
  tfae_finish,
end
example (P Q R : Prop) : tfae [P, Q, R] :=
begin
  tfae_have : 1  2, by sorry,
  tfae_have : 2  1, by sorry,
  tfae_have : 1  3, by sorry,
  tfae_finish,
end
example (α : Type) (P Q R : α  Prop) : tfae [ x, P x,  x, Q x,  x, R x] :=
begin
  tfae_have : 1  2, by sorry,
  tfae_have : 2  1, by sorry,
  tfae_have : 1  3, by sorry,
  tfae_finish,
end
example (α : Type) (P Q R : α  Prop) : tfae [ x, P x,  x, Q x,  x, R x] :=
begin
  tfae_have : 1  2, by sorry,
  tfae_have : 2  1, by sorry,
  tfae_have : 3  1, by sorry,
  tfae_finish,
end

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:11):

Creating and deleting a line between two examples also changes what works

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:12):

Can anyone see that, or is it only my computer going crazy?

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:13):

I can reproduce

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:13):

Creating and deleting lines changes what works nondeterministically.

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:14):

I guess meta-land allows non-deterministic algorithms

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:14):

I don't get non-deterministic behavior with that code. I'm in emacs.

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:15):

Right... we need a tactic that will first toss a coin to decide if it will actually help you :upside_down:

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:15):

I have such tactics

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:15):

we see that

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:15):

@Simon Hudon Do you get any errors at all with that code (apart from the sorries)?

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:15):

Yes, it fails deterministically

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:16):

@Patrick Massot I'll remember that

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 07:17):

And also, undo in VScode vim extension is completely crazy, you never know how many steps you will go back

This annoys me to no end as well. However it seems that VS code's built-in undo (cmd+z on mac, ctrl+z on other systems) works independently and seems to function properly.

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:49):

Ok now I see the non deterministic behavior. That looks weird. I think it's because some vertices are being ignored and because they are stored in a hash table and their hash code probably depends on the memory address of the expressions which changes from run to run.

view this post on Zulip Mario Carneiro (Oct 05 2018 at 07:50):

is this because of ref?

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:51):

I don't think so

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:51):

I'm only using expr as a key in hash tables

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:52):

In the mean time, I'd like to sorry this tfae and move on. How to you actually use a tfae statement? I don't see anything in the docs

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:54):

That's a correct use of tfae.

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 07:54):

tfae.out is probably what you want. It's mentioned obliquely in the docs: "In data/list/basic.leanthere are propositions of the form..."

view this post on Zulip Mario Carneiro (Oct 05 2018 at 07:54):

you state follow up equivalences you are interested in and refer to the elements of the list by their index

view this post on Zulip Mario Carneiro (Oct 05 2018 at 07:56):

and use those numbers in tfae.out

view this post on Zulip Simon Hudon (Oct 05 2018 at 07:56):

With one added oddity: the indices are 1 ≤ i ≤ xs.length rather than 0 ≤ i < xs.length

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:05):

I can't use it, probably because of parameters. Compare:

import tactic.tfae
open list
constants (α : Type) (P Q R : α  Prop)

lemma eqv (x : α) : P x  Q x :=
sorry

example (x : α) (h : P x) : P x :=
begin
  rw eqv at *,
  assumption
end

lemma eqvs (x : α): tfae [P x, Q x, R x] :=
sorry

example (x : α) (h : P x) : P x :=
begin
  rw tfae.out (eqvs ) 1 2,
  assumption
end

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:08):

Sorry, my comment was misleading: the indices start at 1 in the proof, not when you use the theorem.

Now that I'm saying, I think we should remove that oddity.

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:09):

Can you fix my example above?

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:09):

rw tfae.out (eqvs ) 0 1,

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:10):

doesn't work

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:10):

What error do you get?

view this post on Zulip Mario Carneiro (Oct 05 2018 at 08:18):

Sorry I wasn't clear. You can't use it directly as a rewrite rule, you have to restate the theorem and prove it by tfae.out

view this post on Zulip Mario Carneiro (Oct 05 2018 at 08:19):

theorem eqvs_PQ (x : α) : P x ↔ Q x := (eqvs x).out 0 1
theorem eqvs_PR (x : α) : P x ↔ R x := (eqvs x).out 0 2

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:24):

Thanks. It's somehow disappointing

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:24):

Arg, I'm super late

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:26):

Oooh, that's disappointing indeed.

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:29):

Would something like erw be able to deal with this?

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:30):

What if you could do: from_tfae h : eqvs 0 1 first to add an assumption h with the right equivalence?

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:30):

We need a rw on steroids. One that will use more power to do the job. Like simp it should dive into binders etc, so that we no longer need to do the conv dance. And it should also unpack this stuff from tfae.out so that it can just use it to rw.

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:31):

@Simon Hudon Yes, you could just do have : P → Q := tfae.out 0 1 and then rw this.

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:31):

But it is too verbose.

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:32):

Yes. It's confusing... mathematicians keep complaining that proofs are too compact and unreadable in term mode. Otoh we love the brevity of informal maths...

view this post on Zulip Patrick Massot (Oct 06 2018 at 16:31):

And also, undo in VScode vim extension is completely crazy, you never know how many steps you will go back

This annoys me to no end as well. However it seems that VS code's built-in undo (cmd+z on mac, ctrl+z on other systems) works independently and seems to function properly.

@Bryan Gin-ge Chen Gabriel just told me to use the trick described in https://github.com/VSCodeVim/Vim/issues/1490#issuecomment-352167221

view this post on Zulip Johan Commelin (Nov 18 2018 at 18:18):

@Simon Hudon How are things going with tfae? Is there something blocking progress? I'm currently stating 5 equivalent conditions for a presheaf to be a sheaf. I think tfae could increase the user experience :smiley:

view this post on Zulip Simon Hudon (Nov 18 2018 at 18:23):

I haven't fixed the bug yet, I was under the impression that it didn't always manifest and tfae has been merged so you should be able to use it and cross your fingers.

view this post on Zulip Patrick Massot (Nov 19 2018 at 21:52):

I can still see the bug using the latest mathlib.

import tactic.tfae

example (P Q R : Prop) : tfae [P, Q, R] :=
begin
  tfae_have : 1  2, by sorry,
  tfae_have : 2  1, by sorry,
  tfae_have : 3  1, by sorry,
  tfae_finish,
end

doesn't work here


Last updated: May 17 2021 at 21:12 UTC