Zulip Chat Archive

Stream: new members

Topic: Rational number equality

Anders Skovsted Buch (Feb 17 2023 at 18:20):

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 (Feb 17 2023 at 18:38):

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 (Feb 17 2023 at 18:39):

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

Junyan Xu (Feb 18 2023 at 18:15):

Yeah, you probably want

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

Last updated: Dec 20 2023 at 11:08 UTC