A question about correctness of proofs

Stream: general

[Victor Liu]

Hi there. I've recently encountered a predicament while trying to write proofs in Lean 4, although this is probably more general to just the language and applies to formal proof verifiers.

I was proving a statement of the following. I had a hypothesis to restrict the domain of the function. Something like:

example (h : x ∈ Ω) : ContinuousAt h x := by
  sorry

What ended up happening was that I accidentally proved the result without using the hypothesis. Seemingly, this works because

$$\text{False} \Rightarrow \text{True}$$

holds. In reality, h is not continuous outside of Ω since it is not even defined there.

My question is:

1. How do we deal with restricting domain of functions in a manner that such cases do not happen?
2. This case was maybe a translational error since the conversion from the actual statement to Lean 4 was not entirely accurate. However, based on the fact that False can imply anything, can we actually rely on the correctness of Lean 4 proofs? How would we check for such as mistake?

[Yury G. Kudryashov]

Could you please provide an #mwe?

[Yury G. Kudryashov]

It's hard to discuss questions about logic without a very specific example.

[Victor Liu]

Yury G. Kudryashov said:

Could you please provide an #mwe?

Well I discarded it but I can give a pretty trivial example, suppose

$$h(x)=x$$

is defined for

$$\Omega = [0,1]$$

You can prove that h is continuous on all real numbers by using the theorem that the identity is continuous. However, this does not make use of the hypothesis. I'll try to make a minimum working example.

[Victor Liu]

Okay, here's a somewhat trivial working example:

import Mathlib

open Set

open Function

open Topology
-- Define the variables for Banach space X
variable {X : Type*}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
-- Define a subset of X
variable (Ω : Set X)
-- This function maps the subset Ω to another space
noncomputable def f' : X → X → X := fun _ ↦ (fun x ↦ x)

-- Here, f should only be continuous for x ∈ Ω since it is only defined on Ω. However, we can prove its continuity for all of X.
theorem f_continuous (x : X) (hx : x ∈ Ω) : Continuous (f' x) := by
  apply continuous_id
/-
unused variable `hx`
note: this linter can be disabled with `set_option linter.unusedVariables false`
-/

[Kim Morrison]

I'm not understanding what you're asking. So far, the correct advice is to follow the linter and delete the irrelevant hypothesis hx.

[Victor Liu]

Kim Morrison said:

I'm not understanding what you're asking. So far, the correct advice is to follow the linter and delete the irrelevant hypothesis hx.

I think this case is probably me not being familiar enough for the language and creating a discrepancy during translation to Lean 4. However, my intention is to create a function of Banach spaces X, Y so that

$$f : \Omega \to Y$$

is continuously differentiable, hence its derivative

$$f' : \Omega \to X \to Y$$

is such that $f'(x)$ at each $x \in \Omega$ a continuous linear map between X and Y. However, in this setting, it was possible to prove that $f'(x)$ is continuous for all $x \in X$, not just $\Omega$.

[Luigi Massacci]

How is f' defined outside of Omega?

[Victor Liu]

My example may not be the best to illustrate as you could argue I probably just didn't express my constraints in the correct way. Nonetheless, there is the possibility that you could accidentally create a statement of

$$\text{False} \implies \text{False}$$

leading to no errors.

[Victor Liu]

Luigi Massacci said:

How is f' defined outside of Omega?

It is not

[Luigi Massacci]

Victor Liu said:

Luigi Massacci said:

How is f' defined outside of Omega?

It is not

Maybe not on paper, but in lean it must be

[Victor Liu]

Yes, that's why I am saying that my example might not be the best as I am not that familiar with the language and it is because I defined it as f: X → X

[Victor Liu]

But there certainly exist examples where you can construct similar arguments like this

Victor Liu said:

My example may not be the best to illustrate as you could argue I probably just didn't express my constraints in the correct way. Nonetheless, there is the possibility that you could accidentally create a statement of

$$\text{False} \implies \text{False}$$

leading to no errors.

[Eric Wieser]

If you insist that it is not defined outside Ω, then you can write f : Ω -> X

[Luigi Massacci]

Well, because it's a logically sound argument?

[Luigi Massacci]

So why should it trigger an error?

[Victor Liu]

Well it shouldn't, but does that imply that every hypothesis must always be used?

[Luigi Massacci]

No?

[Eric Wieser]

Luigi Massacci said:

Well, because it's a logically sound argument?

(this argument is docs#False.elim, and says $\mathit{False} \implies X$ is always fine)

[Victor Liu]

Eric Wieser said:

If you insist that it is not defined outside Ω, then you can write f : Ω -> X

Yeah, I was looking for something like that but I wasn't sure if I could get it to work because I was creating many errors while dealing with derivatives. Could you help me change these definitions to more suitable ones?

variable (f : X → Y) (hf : ContDiffOn ℝ 1 f Ω)
         (hf' : ∀ x ∈ Ω, HasFDerivAt f (f' x : X →L[ℝ] Y) x)
-- Define f' as a mapping
variable (f' : X → X ≃L[ℝ] Y)
         (hf' : ∀ x ∈ Ω, HasFDerivAt f (f' x : X →L[ℝ] Y) x)

[Victor Liu]

If I directly change hf' to

         (hf' : ∀ x ∈ Ω, HasFDerivAt f (f' x : X →L[ℝ] Y) x)

I get errors:

application type mismatch
  ContDiffOn ℝ 1 f Ω
argument
  Ω
has type
  Set X : Type u_1
but is expected to have type
  Set ↑Ω : Type u_1

application type mismatch
  f' x
argument
  x
has type
  X : Type u_1
but is expected to have type
  ↑Ω : Type u_1

And if I try ContDiff, I also face errors:

variable (f : Ω → Y) (hf : ContDiff ℝ 1 f)
/-
failed to synthesize
  NormedAddCommGroup ↑Ω
-/

(and many others)

image.png

[Luigi Massacci]

Just to be sure, have you looked at #mil yet?

[Victor Liu]

I did indeed, you can see my progress on GitHub:
https://github.com/victorliu5296/mathematics_in_lean

[Victor Liu]

I did the chapters 1 and 2, 10 and 11 carefully, I might have to revisit the others in more detail. However, I felt like as the chapters went on, they felt somewhat incomplete and hard to follow, so I learnt as I went by reading the documentation at https://leanprover-community.github.io/mathlib4_docs/.

[Victor Liu]

I'll go read chapters # 4. Sets and Functions and # 9. Topology then

[Damiano Testa]

I may be misunderstanding what the issue is, but it seems like you are asking "how do I make sure that the statement that I formalised is the statement that I intended to formalise?".

There is never a guarantee of this, but by

• getting familiar with what the definitions in mathlib mean,
• learning how they differ from their informal analogues and
• proving lots of related results to make sure that they still satisfy your intuition,

you can develop some confidence that you are doing the correct thing.