weird behavior of `unfold`

Stream: new members

[Vasily Ilin]

I am playing the complex number game, and came across this paradoxical behavior.

lemma I_ne_zero : (I : ℂ) ≠ 0 :=
begin
  intro h,
  rw ext_iff at h,
  unfold I at h,
  simp * at h,
end

leaves me with

h: false
⊢ false

in infoview. But deleting unfold I get

lemma I_ne_zero : (I : ℂ) ≠ 0 :=
begin
  intro h,
  rw ext_iff at h,
  simp * at h,
end

with

h: true
⊢ false

in infoview. What's going on here? Why does h flip from false to true?

[Kevin Buzzard]

#backticks

[Kevin Buzzard]

If you want my guess, simp * at h can't figure out how to simplify h without the unfold, but rather than fail the simplifier decides that it will use h to simplify h, and ends up simplifying it to true.

[Kevin Buzzard]

yeah:

example (P : Prop) (hP : P) : false :=
begin
  simp * at hP, -- `hP : true`
  sorry,
end

[Vasily Ilin]

But that's completely wrong, no? Mathematically speaking the truth value of h is false, no matter what

[Kevin Buzzard]

But h implies h, so because we have h as an assumption we can also reduce h to true

[Kevin Buzzard]

2+2=5 is false, but if you assume that 2+2=5 you can reduce the equation to 5=5

[Vasily Ilin]

I feel uneasy about this but I understand what you are saying

[Kevin Buzzard]

example (P Q : Prop) (hP : P) (hPQ : P ↔ Q) : false :=
begin
  simp [hP] at hPQ, -- `hPQ : Q`
  sorry,
end

[Kevin Buzzard]

Here's another way of thinking about it: you are using a logical machine to do computations but right now you have a false assumption, and explicitly asking the machine to use the false assumption clearly has the consequence that the machine can say anything it wants and find some logical way to justify it.

[Kevin Buzzard]

In the example above, of course if we know P then we can reduce P <-> Q to Q -- that's just basic logic. But if P is false and Q is true we have "reduced a false statement to a true statement" on the face of it -- but only by assuming a false statement along the way.

[Yaël Dillies]

Simplifying h by h sounds like a wrong turn, though. Do we ever want to do that?

[Kevin Buzzard]

I agree that it's hard to imagine that it can ever be useful. Perhaps it was a last resort (note that it didn't happen when unfolding I first).

[Arthur Paulino]

Your code is not an #mwe (it's missing some declarations/imports), but notice that failing to simplify h to false and having it being simplified to true instead is a loss of information, if we can think like this.

example {a b : nat} : a + b = b + a :=
begin
  have h : a + b = b + a := sorry, -- exact h would work after this!
  simp [h] at h,                   -- but now I have `h : true` :(
  sorry,
end

It's a loss of information because it's a trivial type, easily proven by trivial, even:

example : true := by trivial

In the case where you succeeded to simplify h to false, try using squeeze_simp * at h instead and you should be able to see what was used to achieve that

[Vasily Ilin]

Are you saying that it's a loss of information because nothing follows from true and everything follows from false?

[Vasily Ilin]

I thought that unfold does not actually do anything, just makes something easier to read. This example made me realize it's more complicated than that

[Arthur Paulino]

Well, technically speaking true follows from true, but you can't go much further than that I believe

[Kevin Buzzard]

As Yael says, this is arguably a bug in simp, because simp [h] at h shouldn't really just simplify h to true if it can't think of anything better to do. But logically it's fine.

[Arthur Paulino]

Vasily Ilin said:

I thought that unfold does not actually do anything, just makes something easier to read. This example made me realize it's more complicated than that

Sorry if I speak too CS'ish, but for the computer, what we see written differently may represent very different types

[Damiano Testa]

Another way of saying the same thing is that with simp [h] at h you are instructing lean to use h in its simplifications.

Maybe, it would have appeared less weird if the assumption have been something more complicated. Suppose that P A : Prop. Using simp [h] on

if h then P else Q

should (untested) produce P. The actual truth values of P or Q is irrelevant: you have provided the assertion that h can be assumed true throughout.

If you are happy with this, you can now apply the previous reduction in the case where P = h.

[Kyle Miller]

Kevin Buzzard said:

As Yael says, this is arguably a bug in simp, because simp [h] at h shouldn't really just simplify h to true if it can't think of anything better to do. But logically it's fine.

Maybe the bug is that simp isn't keeping around every assumption it's used at the end. One way to think about it is that simp is deriving true from h and then deleting the original h. For example, if we've got h : P and then simp [h] at h, we might expect to see h_1 : P and h : true instead.

We see simp keep around original assumptions if they're part of complicated dependent types elsewhere.

[Kyle Miller]

Vasily Ilin said:

But that's completely wrong, no? Mathematically speaking the truth value of h is false, no matter what

Maybe you'll feel more at ease about it seeing what simp is effectively doing here:

example {P : Prop} (h : P) : false :=
begin
  -- simp [h] at h,
  have old_h := h,
  simp [old_h] at h,
  clear old_h,
  -- now h : true (but it's a different h from what we started with)
end