Rational number equality

Stream: new members

[Anders Skovsted Buch]

Here is another silly thing I can't find an answer to:

import data.rat
example : 2 * 3 = 6 := by ring
example : rat.mul (rat.mk 3 2) 2 = 3 := sorry
#eval rat.mul (rat.mk 3 2) 2 -- works, evaluates to 3

I expected that by ring would work, but apparently not. What is a proof without using tactics?

Also, is there a good reference for how to construct proofs without using tactics? Sure, tactics are great, but the focus on tactics in the documentation I have read makes it difficult to figure out what is really going on and what to do when the tactics I know about don't apply.

[Alex J. Best]

Mostly tactics like ring and norm_num (which is more appropriate for this goal) are designed to operate using the polymorphic multiplication and division operations, so that may be why they don't work here. Mathlib prefers to use * over explicit rat.mul, also many lemmas are stated in this way too.
The reason people quickly switch to tactics is that the term mode proofs very quickly become painful, especially for this sort of thing, the first few chapters of #tpil are quite term-mode-y though I think.
What specific proof do you have in mind to formalize this example, on paper, in detail? You'll probably want to state some general lemmas and then combine those to prove your example

[Reid Barton]

Likewise you're not really intended to use rat.mk directly.

[Junyan Xu]

Yeah, you probably want

import tactic.ring
example : (3 * 2 : ℚ) = 6 := by ring