Mul_pos and coercions

Stream: new members

[Christian Kolker]

In the following code, I would like to use mul_pos to close my goal. I suspect that my coerced n is messing with my mul_pos application or maybe I am not calling it correctly.

    have x : j - h > 0 , simp,
    exact k,
    have p := archimedean_R (j - h),
    have t := p(x), cases t with n hn,
    cases hn with v hv,
    have v1 : 0 < ↑n , linarith,
    have g : 0 < (j - h - 1 / ↑n), linarith,
    have s : 0 < ↑n * (j - h - 1 / ↑n),
     ```

[Alex J. Best]

What is the actual example / lemma you are trying to prove? As is we can't really tell what the goal state is. A full file with the imports will let people help you more easily

[Christian Kolker]

My goal is 0 < ↑n * (j - h - 1 / ↑n),

[Christian Kolker]

I am messing around with a level from the real number game, here it is

import tactic

/-
# Chapter 1 : Sets

## Level 10

As a final test of your ability in working with sets, prove that the set of rational
numbers is dense in the reals.

This proof will, among other things, rely on several new axioms that appear
in the left side bar.
Note that you may need to change the type of some quantities from rationals to reals.
Lean doesn't necessarily consider the rational $2$ to be the same at the real number $2$.
Some of the axioms on the left make working with the casts from rationals to reals easier.
-/


/- Axiom : inv_prod_self :
∀ n : ℕ, 0 < n → (1/n : ℝ) * (n : ℝ ) = 1
-/

/- Axiom : inv_prod_other :
∀ (m : ℤ), ∀ (n : ℕ), 0 < n → (1/n : ℝ) * (m : ℝ) = (m/n : ℝ)
-/

/- Axiom : archimedean_R : ∀ x : ℝ, 0 < x → ∃ n : ℕ, 0 < n ∧ (1/n : ℝ) < x
-/

/- Axiom : has_ceiling : ∀ x : ℝ,  ∃ m : ℤ, ((m-1) : ℝ) ≤ x ∧ x < (m:ℝ)
-/

-- one way to prove ℚ dense in ℝ
def dense_in_R (A : set ℝ) := ∀ (x y : ℝ), x < y → ∃ a ∈ A, a ∈ set.Ioo x y
def embedded_rationals : set ℝ := { x | ∃ r : ℚ, x = ↑r }
-- begin hide
axiom archimedean_R : ∀ x : ℝ, 0 < x → ∃ n : ℕ, 0 < n ∧ (1/n : ℝ) < x
-- we might want to prove these below. Made into axioms just for ease.
-- the problem is that the proofs are too hard for this level, IMO (DS)
axiom has_ceiling : ∀ x : ℝ,  ∃ m : ℤ, ((m-1) : ℝ) ≤ x ∧ x < (m:ℝ)
axiom inv_prod_self : ∀ n : ℕ, 0 < n → (1/n : ℝ) * (n : ℝ ) = 1
axiom inv_prod_other : ∀ (m : ℤ), ∀ (n : ℕ), 0 < n → (1/n : ℝ) * (m : ℝ) = (m/n : ℝ)
-- end hide

/- Lemma
Rationals are dense in the reals.
-/
theorem rat_dense_in_R : dense_in_R embedded_rationals :=
begin
    intros h j k,
    have x : j - h > 0 , simp,
    exact k,
    have p := archimedean_R (j - h),
    have t := p(x), cases t with n hn,
    cases hn with v hv,
    have v1 : 0 < ↑n , linarith,
    have g : 0 < (j - h - 1 / ↑n), linarith,
    have s : 0 < ↑n * (j - h - 1 / ↑n),

[Christian Kolker]

By the way, I just used finish and it cleared my goal. is there any way to see what finish did exactly to clear my goal?

[Alex J. Best]

Unfortunately the internals of finish are such that the proof produced isn't really human readable.

[Alex J. Best]

This works for your first goal:

theorem rat_dense_in_R : dense_in_R embedded_rationals :=
begin
    intros h j k,
    have x : j - h > 0 , simp,
    exact k,
    have p := archimedean_R (j - h),
    have t := p(x), cases t with n hn,
    cases hn with v hv,
    have v1 : 0 < (n : ℝ), simp, exact v, -- this line changed
    have g : 0 < (j - h - 1 / ↑n), linarith,
    have s : 0 < ↑n * (j - h - 1 / ↑n),
    exact mul_pos v1 g,
end

[Alex J. Best]

When you just specify a coercion with the up arrow, but don't say what to lean by default thinks you want to coerce nat to nat, its much better to always put the type ascription like I did here, telling lean you want to coerce to a real in this case.

[Christian Kolker]

Thank you Alex, this helps a lot!