my first not-entirely trivial thing

Stream: general

[Matthew Pocock]

Thanks for all the helpful answers to my questions these past few days. I've written my first not entirely trivial proof that I can solve two linear equations. Where the equations produce whole number outputs for whole number inputs, the solutions should generate all whole number solutions, but I've not proved this yet. Constructive criticism welcomed.

-- A linear equation of the form y=mx+c
structure LF :=
    (m : ℕ)
    (c : ℚ)
    (m_gt_zero : 0 < m)

-- Perhaps there's a typeclass for this?
def LF.app (lf : LF) (n : ℚ) : ℚ := lf.m * n + lf.c

-- parameterised solutions to lf1,2
def solutions (lf₁ lf₂ : LF) : LF×LF :=
    let mgcd := Nat.gcd lf₁.m lf₂.m
    let lfL := {
        m := lf₂.m / mgcd
        c := lf₂.c / lf₁.m
        m_gt_zero := by
            have gz := Nat.div_gcd_pos_of_pos_right lf₁.m lf₂.m_gt_zero
            simp
            assumption
    }
    let lfR := {
        m := lf₁.m / mgcd
        c := lf₁.c / lf₂.m
        m_gt_zero := by
            have gz := Nat.div_gcd_pos_of_pos_left lf₂.m lf₁.m_gt_zero
            simp
            assumption
    }
    ⟨ lfL, lfR ⟩

-- prove that they are, in fact, solutions
theorem solutions_valid (lf₁ lf₂ : LF) : (⟨sL, sR⟩ = solutions lf₁ lf₂) →
        ∀ n , lf₁.app (sL.app n) = lf₂.app (sR.app n) := by
    simp [solutions]
    rintro hsL hsR n
    simp [LF.app, hsL, hsR]
    have lf₁nz : (lf₁.m : ℚ) ≠ 0 := Iff.mpr Nat.cast_ne_zero $ Nat.pos_iff_ne_zero.mp lf₁.m_gt_zero
    have lf₂nz : (lf₂.m : ℚ) ≠ 0 := Iff.mpr Nat.cast_ne_zero $ Nat.pos_iff_ne_zero.mp lf₂.m_gt_zero

    simp [mul_add]
    simp [mul_div_cancel' lf₂.c lf₁nz, mul_div_cancel' lf₁.c lf₂nz]
    simp [Nat.gcd_dvd_left, Nat.gcd_dvd_right]
    ring

[Henrik Böving]

You might be able to use docs#CoeFun for your LF.app although I am not quite sure if that is idiomatic.

And with respect to your proof. We usually try to use simp only as the last tactic to prove a goal (in your case there is only one goal, if you do e.g. a cases you would want to use simp only at the end of the cases arms). That's because we want to guarantee proof stability. Say that we add a lemma to the default simp rules via @[simp] a call to simp in the middle of your proof could turn your goal into something entirely different now which ends up either failing right away at the next tactic step or the much more annoying variant: ends up failing after a couple of tactic steps and you cant instantly see what's wrong.

For this reason we usually try to use simp only when we are not in terminal position. If you want to turn a simp call into a simp only one (after all as we just learned simp can involve arbitrary additional lemmas) you can use the mathlib tactic simp? instead of simp which will print the corresponding simp only call that you can then replace the simp? with.

[Matthew Pocock]

Henrik Böving said:

You might be able to use docs#CoeFun for your LF.app although I am not quite sure if that is idiomatic.

I did try something like this but couldn't encourage it to summon the correct bounds. I was probably syntaxing wrongly.

For this reason we usually try to use simp only when we are not in terminal position. If you want to turn a simp call into a simp only one (after all as we just learned simp can involve arbitrary additional lemmas) you can use the mathlib tactic simp? instead of simp which will print the corresponding simp only call that you can then replace the simp? with.

Brill :D