can't seem to specialise a universally quantified hypothesis

Stream: new members

[rzeta0]

The Mechanics of Proof introduces "for all" and uses the following example to show how a universally quantified hypothesis can be specialised:

example {a : ℝ} (h : ∀ x, a ≤ x ^ 2 - 2 * x) : a ≤ -1 :=
  calc
    a ≤ 1 ^ 2 - 2 * 1 := by apply h
    _ = -1 := by numbers

Here x has been chosen to be 1.

I'm having trouble specialising a more complicated hypotheses. Here is my goal state:

y : ℚ
hy : ∀ a ≥ 1, a ≤ 3 → (a - y) ^ 2 ≤ 1
x1 : 1 ≥ 1
x3 : 1 ≤ 3

This is the section of code that is not working, where i have chosen to specialise a to (1:ℚ)

have f1 := by
        calc
          ((1:ℚ) - y) ^ 2 ≤ 1 := by apply hy -- < -- error
          _ = 1^2 := by norm_num

The following is the error message:

unsolved goals
case a
y : ℚ
hy : ∀ a ≥ 1, a ≤ 3 → (a - y) ^ 2 ≤ 1
x1 : 1 ≥ 1
x3 : 1 ≤ 3
⊢ 1 ≥ 1

case a
y : ℚ
hy : ∀ a ≥ 1, a ≤ 3 → (a - y) ^ 2 ≤ 1
x1 : 1 ≥ 1
x3 : 1 ≤ 3
⊢ 1 ≤ 3

I suspect I need to somehow include x1 and x3 in the apply hy but I don't know how to do that.

Moving the cursor to later points in the hope the extant goals are available to resolve via a simple norm_num doesn't work.

---

The full code is below, but I hesitated to share it as it is too long, a beginner's first embarrassing draft solution.

example : ∃! x : ℚ, ∀ a, a ≥ 1 → a ≤ 3 → (a - x) ^ 2 ≤ 1 := by
  use 2
  dsimp
  constructor
  · intro a ha hb
    have ga: a-2 ≥ -1 := by addarith [ha]
    have gb: a-2 ≤ 1 := by addarith [hb]
    have gc:= by
      calc
        (a-2)^2 ≤ 1^2 := sq_le_sq' ga gb
        _ = 1 := by norm_num
    exact gc
  · intro y hy
    apply le_antisymm
    · have x1 : (1:ℚ) ≥ 1 := by norm_num
      have x3 : 1 ≤ (3:ℚ) := by norm_num
      have f1 := by
        calc
          ((1:ℚ) - y) ^ 2 ≤ 1 := by apply hy
          _ = 1^2 := by norm_num
      have f0 : (0 : ℚ ) ≤ 1 := by norm_num
      have f2: -1 ≤ 1-y ∧ 1-y ≤ 1 := by apply abs_le_of_sq_le_sq' f1 f0
      obtain ⟨ fa, fb ⟩ := f2
      addarith [fa]
    · have e1 := by
        calc
          ((3:ℚ) - y) ^ 2 ≤ 1 := by apply hy
          _ = 1^2 := by norm_num
      have e0 : (0 : ℚ ) ≤ 1 := by norm_num
      have e2: -1 ≤ 3-y ∧ 3-y ≤ 1 := by apply abs_le_of_sq_le_sq' e1 e0
      obtain ⟨ ea, eb ⟩ := e2
      addarith [eb]

[Ruben Van de Velde]

You can write hy 1 x1 x3

[Ruben Van de Velde]

After apply

[Kyle Miller]

Hint: when you apply a local hypothesis like hy, it is just like applying any other lemma. What you know about applying lemmas applies to applying local hypotheses.

[rzeta0]

Ruben Van de Velde said:

You can write hy 1 x1 x3

Chapter 4 of Mechanics of Proof introduces new syntax without explaining it - or requires us to find out ourselves.

Perhaps that's part of the educational challenge...

[rzeta0]

---

@Kyle Miller I have followed the Mechanics of Proof course and done every single exercise so far but I do feel I'm missing a proper guide or overview of how to apply lemmas/hypotheses.

I'm just guessing as I try:

• apply lemma
• apply lemma at
• := lemma
• := by apply lemma
• more?

I don't know the difference between the last two for example.

[Edward van de Meent]

:= lemma means "lemma is exactly the type i need". := by apply lemma means "you can fill in parameters to lemma (satisfying certain rules) to get a type that is exactly the type i need"

[Edward van de Meent]

for example, if the expected type is Nat -> Nat, and foo : (A:Type) -> A -> A, then := by apply foo works (because lean can figure out that only filling in (A := Nat) gives the right type), but := foo doesn't.

[rzeta0]

I don't know what Nat -> Nat means.

I definitely don't know what foo : (A:Type) -> A -> A means.

Perhaps an example can illustrate this?

[Kyle Miller]

I thought I've seen you write things like apply lemma arg1 arg2 before @rzeta0. Or at least exact lemma arg1 arg2?

[rzeta0]

aha - i didn't know parameters were written in the signature like that.

when I see X → Y it looks like functions mapping from domain X to co-domain Y

[Philippe Duchon]

Yes, Nat -> Nat is the type of mappings from Nat to Nat (natural number sequences).

And A -> A -> A is the type of mappings from A to A->A, or in other words (it's often way easier to think of them this way) functions that take two values of type A and return a single value of type A. This is the type of binary operations on A, like addition or multiplication in groups and rings.

[Edward van de Meent]

note that (A:Type) -> A -> A is different from A -> A -> A. in the first case, the type of the first parameter is Type, in the second case it is A.

[Edward van de Meent]

the (A:Type) -> ... notation allows you to give a name to the first parameter, to use it in the returntype.

[Edward van de Meent]

so (A:Type) -> A -> A is the type of functions which map a type into an endofunction on that type.

[Philippe Duchon]

Ah yes you're right, so it's a dependent type where the type of the second parameter depends on the value of the first parameter. Clearly I misread.