direct proof

Stream: new members

[Esteban Estupinan]

hi, i m trying this tutorial, https://github.com/leanprover-community/tutorials , there are many examples of direct proofs using backward and forward reasonning. Personally I see more convenient proving with backward reasonning. I ask you, is posible using backwards in any direct proof, or this just works when exists explicit implications somewhere in the hypothesis like in this sample?

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

def non_increasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≥ f x₂

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) :=
begin
  unfold non_decreasing at hf,
  unfold non_decreasing at hg,
  unfold non_decreasing,
  -- Let x₁ and x₂ be real numbers such that x₁ ≤ x₂
  intros x₁ x₂ h,
  -- We need to prove (g ∘ f) x₁ ≤ (g ∘ f) x₂.
  -- Since g is non-decreasing, it suffices to prove f x₁ ≤ f x₂
  apply hg,
  -- which follows from our assumption on f
  apply hf,
  -- and on x₁ and x₂
  exact h,
end

this is easy, but I m trying use backwards in another theorems and here is the problem because is not easy for me to find the implications within the hypotheses

[Scott Morrison]

(An aside: note that the unfolds here are not actually needed. intros will go right through a definition looking for binders.)

[Scott Morrison]

I'm not sure what to say about your general question. Some results are easier to prove "forwards" than "backwards", others vice versa, and most deserve many changes of direction?

[Scott Morrison]

Perhaps you have a particular example to show us?

[Esteban Estupinan]

According to the examples that I have seen in the tutorial, backward reasoning can be applied when there are implications within the hypothesis itself, theorems or definitions such as the example above. My question is, do all definitions in math hide implications? if so, how can the implicit implications be discovered? I ask this because it makes it easier for me to work backwards than forwards

[Kevin Buzzard]

maths goes forwards and backwards and it's impossible to make definitive statements about whether it's generally easier to go forwards or backwards. Maths is a maze.

[Esteban Estupinan]

ok, theorems are implications or biconditional, axioms or definitions can rewritten as implications or implicit implications, all axioms are implications or not?

[Kevin Buzzard]

You cannot attempt to classify mathematics in this way, despite the dreams of computer scientists to do this. Mathematics is anything which follows the rules of mathematics.

[Eric Wieser]

all axioms are implications or not?

Well true.intro is not an implication, and could be seen as an "axiom" that there is a proof of true

[Esteban Estupinan]

its ok thank you for your answers

[Esteban Estupinan]

hi all, it is interesting to manipulate a theorem as a function that receives as input the assumptions and returns the proof itself as output, I don't know who wrote this idea but I really appreciate it, it has helped me a lot in understanding the theorems.

import data.real.basic

Let's see how we could use this lemma. It is already in the core library, under the name `add_le_add_right`:

  add_le_add_right {a b : ℝ} (hab : a ≤ b) (c : ℝ) : a + c ≤ b + c

This can be read as: "add_le_add_right is a function that will take as input real numbers a and b, an
assumption `hab` claiming a ≤ b and a real number c, and will output a proof of a + c ≤ b + c".

In addition, recall that curly braces around a b mean Lean will figure out those arguments unless we
insist to help. This is because they can be deduced from the next argument `hab`.
So it will be sufficient to feed `hab` and c to this function.
-/

example {a b : ℝ}  (ha : 0 ≤ a) : b ≤ a + b :=
begin
  calc b = 0 + b : by ring
     ... ≤ a + b : by exact add_le_add_right ha b,
end

/-
In the second line of the above proof, we need to prove 0 + b ≤ a + b.
The proof after the colon says: this is exactly lemma `add_le_add_right` applied to ha and b.

following this same idea, please someone help me to interpret a theorem
imagen.png
imagen.png
the inputs from theorem 2.8 are included in theorem 2.20, but what in t2.20 use t2.8 to prove or say (fi) function is linear?, because t2.8 should have as output literal a and b of t2.8 and "linear" is another assumption not a conclusion, thanks for your answers

[Alex J. Best]

Your theorem 2.8 is the statement that the map $\Phi (T)= [T]^\gamma_\beta$ is linear as a function of $T$ broken up into two pieces, part a and b, together they imply linearity of $\Phi$. The assumptions to 2.8 also include that $T,U$ are linear which I guess is what is confusing you, but those are the inputs not the outputs as you say.