## Stream: general

### Topic: tfae bug

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

I'm on it

#### Patrick Massot (Oct 05 2018 at 07:03):

Note that removing the forall hides the issue

#### Simon Hudon (Oct 05 2018 at 07:03):

Does it? That's odd

maybe not

#### Patrick Massot (Oct 05 2018 at 07:06):

I changed many times what I tried

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

#### Patrick Massot (Oct 05 2018 at 07:09):

Wow, I see completely random behavior

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

Heisenbugs!

#### Johan Commelin (Oct 05 2018 at 07:11):

A Heisenbug in a theorem prover — the irony

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


#### Patrick Massot (Oct 05 2018 at 07:11):

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

#### Patrick Massot (Oct 05 2018 at 07:12):

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

I can reproduce

#### Johan Commelin (Oct 05 2018 at 07:13):

Creating and deleting lines changes what works nondeterministically.

#### Patrick Massot (Oct 05 2018 at 07:14):

I guess meta-land allows non-deterministic algorithms

#### Simon Hudon (Oct 05 2018 at 07:14):

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

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

#### Simon Hudon (Oct 05 2018 at 07:15):

I have such tactics

we see that

#### Johan Commelin (Oct 05 2018 at 07:15):

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

#### Simon Hudon (Oct 05 2018 at 07:15):

Yes, it fails deterministically

#### Simon Hudon (Oct 05 2018 at 07:16):

@Patrick Massot I'll remember that

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

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

#### Mario Carneiro (Oct 05 2018 at 07:50):

is this because of ref?

I don't think so

#### Simon Hudon (Oct 05 2018 at 07:51):

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

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

#### Simon Hudon (Oct 05 2018 at 07:54):

That's a correct use of tfae.

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

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

#### Mario Carneiro (Oct 05 2018 at 07:56):

and use those numbers in tfae.out

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

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


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

#### Patrick Massot (Oct 05 2018 at 08:09):

Can you fix my example above?

#### Simon Hudon (Oct 05 2018 at 08:09):

 rw tfae.out (eqvs ) 0 1,

doesn't work

#### Simon Hudon (Oct 05 2018 at 08:10):

What error do you get?

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

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


#### Patrick Massot (Oct 05 2018 at 08:24):

Thanks. It's somehow disappointing

#### Patrick Massot (Oct 05 2018 at 08:24):

Arg, I'm super late

#### Johan Commelin (Oct 05 2018 at 08:26):

Oooh, that's disappointing indeed.

#### Johan Commelin (Oct 05 2018 at 08:29):

Would something like erw be able to deal with this?

#### 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?

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

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

#### Johan Commelin (Oct 05 2018 at 08:31):

But it is too verbose.

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

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

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

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

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