dec_trivial Q

Stream: new members

[Cedric Holle]

I can not dec_trivial equalities and inequalities among rationals.

import data.rat
lemma good : (-1 : ℚ) ≠ (1 :ℚ) := by dec_trivial -- works

lemma  bad : (5 : ℚ) ≠ (1 :ℚ) := by dec_trivial -- doesn't work

[Yury G. Kudryashov]

I guess, @Mario Carneiro and @Gabriel Ebner should know how dec_trivial works.

[Kyle Miller]

I think there's been two threads over the last month and a half that mention this. If I were to hazard a guess, it's that there's well-founded recursion in some of the definitions, which dec_trivial can't evaluate.

[Yakov Pechersky]

nat.div is via wf, iirc. Cedric, are you OK with using norm_num?

[Yury G. Kudryashov]

Why do we need division to compare two rational numbers?

[Yury G. Kudryashov]

Or we use it in bit0/bit1 (I guess, yes)?

[Kyle Miller]

I see that the decidable eq is from

instance : decidable_eq ℚ := by tactic.mk_dec_eq_instance

A few months ago I had an instance created by that tactic where dec_trivial didn't work, and, after rewriting it manually, it did (or so I remember...)

[Yury G. Kudryashov]

I tried, it doesn't help.

[Gabriel Ebner]

Yakov Pechersky said:

nat.div is via wf, iirc. Cedric, are you OK with using norm_num?

nat.div and nat.mod are both implemented using structural recursion now (as of a couple of months ago)

[Gabriel Ebner]

But nat.gcd isn't.

[Kyle Miller]

The decidable_eq instance uses nat.coprime, and this fails:

example : nat.coprime 5 3 := by dec_trivial

[Yury G. Kudryashov]

The actual issue @Cedric Holle minimized to this question was about some 4x4 matrices. @Cedric Holle , you should post an example of what you actually want to prove to a new topic.

[Kevin Buzzard]

@Cedric Holle why do you even want to use this primitive tactic when we have norm_num which was designed to solve goals of this form (and which would even prove that (-100000000000000000000 : Q) != -2000000000000000) when dec_trivial could well time out).

[Yury G. Kudryashov]

I guess, I'm responsible for this attempt.