what is the name of applying an inequality called?

Stream: new members

[rzeta0]

Consider the following:

$$\begin{align}b&=a^{2}&&\text{given fact}\tag{1.1}\\a&\geq2&&\text{given fact} \tag{1.2}\\&\notag&&\\b&=a^{2}&&\text{using fact 1.1}\notag\\&\geq(2)^{2}&&\text{***** using fact 1.2}\notag\\&=4&&\text{using arithmetic}\notag\end{align}$$

My question is: what is the name of given to the step where we apply an inequality. It is not mere "substitution".

(In lean this would be a rel tactic)

[Giacomo Stevanato]

To me it seems you're applying the monotonicity of exponentiation to get a^2 >= 2^2 (the lemma should be Nat.pow_le_pow_left) and then substituting a^2 with b

[rzeta0]

Hi @Giacomo Stevanato - thanks for replying.

Does the rel tactic do any work to establish whether the mapping is monotonic?

Not all exponential mappings are monotonic eg $(x-1)(x-3)$ is not monotonic.

I did try to experiment myself to find out but that ran into a maths error rather than exploring rel.

[Giacomo Stevanato]

rzeta0 said:

Does the rel tactic do any work to establish whether the mapping is monotonic?

I don't know in details how rel works, but AFAIK all tactics in the end boil down to producing lean code that is supposedly well typed (but will still be checked by the compiler).

rzeta0 said:

Not all exponential mappings are monotonic eg $(x−1)(x−3)$ is not monotonic.

I would say that's a polynomial, not an exponentiation. But still, I don't think rel knows about the concept of exponentiation or the fact that it's monotonic. Instead it knows that there are a bunch of lemmas in the Mathlib library that it can try to piece together with your assumptions to prove your statement.

---

By the way you can use #print your_proof to see the output of the tactic. For example:

import Mathlib

def proof (h1 : b = a ^ 2) (h2 : a ≥ 2) : b ≥ 4 := calc
  b = a ^ 2 := h1
  a ^ 2 ≥ 2 ^ 2 := by rel[h1, h2]

#print proof

This prints:

def proof : ∀ {b a : ℕ}, b = a ^ 2 → a ≥ 2 → b ≥ 4 :=
fun {b a} h1 h2 => Trans.trans h1 (pow_le_pow_left' h2 2)

Showing that it is indeed using that lemma I mentioned.

[rzeta0]

thanks for writing this explanation - I find it difficult so I will print it out and read it several times tomorrow to see if it sinks in.