tfae bug

Stream: general

[Patrick Massot]

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

[Simon Hudon]

I'm on it

[Patrick Massot]

Note that removing the forall hides the issue

[Simon Hudon]

Does it? That's odd

[Patrick Massot]

maybe not

[Patrick Massot]

I changed many times what I tried

[Patrick Massot]

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

[Patrick Massot]

Wow, I see completely random behavior

[Patrick Massot]

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

[Johan Commelin]

Heisenbugs!

[Johan Commelin]

A Heisenbug in a theorem prover — the irony

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

I can reproduce

[Johan Commelin]

Creating and deleting lines changes what works nondeterministically.

[Patrick Massot]

I guess meta-land allows non-deterministic algorithms

[Simon Hudon]

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

[Johan Commelin]

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

[Simon Hudon]

I have such tactics

[Patrick Massot]

we see that

[Johan Commelin]

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

[Simon Hudon]

Yes, it fails deterministically

[Simon Hudon]

@Patrick Massot I'll remember that

[Bryan Gin-ge Chen]

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.

[Simon Hudon]

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.

[Mario Carneiro]

is this because of ref?

[Simon Hudon]

I don't think so

[Simon Hudon]

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

[Patrick Massot]

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

[Simon Hudon]

That's a correct use of tfae.

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

and use those numbers in tfae.out

[Simon Hudon]

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

[Patrick Massot]

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

[Simon Hudon]

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.

[Patrick Massot]

Can you fix my example above?

[Simon Hudon]

rw tfae.out (eqvs ) 0 1,

[Patrick Massot]

doesn't work

[Simon Hudon]

What error do you get?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

Thanks. It's somehow disappointing

[Patrick Massot]

Arg, I'm super late

[Johan Commelin]

Oooh, that's disappointing indeed.

[Johan Commelin]

Would something like erw be able to deal with this?

[Simon Hudon]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

But it is too verbose.

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

@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:

[Simon Hudon]

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.

[Patrick Massot]

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