Zulip Chat Archive

Stream: new members

Topic: dec_trivial Q


Cedric Holle (Feb 18 2022 at 17:31):

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 (Feb 18 2022 at 17:47):

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

Kyle Miller (Feb 18 2022 at 17:52):

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 (Feb 18 2022 at 17:54):

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

Yury G. Kudryashov (Feb 18 2022 at 17:56):

Why do we need division to compare two rational numbers?

Yury G. Kudryashov (Feb 18 2022 at 17:56):

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

Kyle Miller (Feb 18 2022 at 17:59):

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 (Feb 18 2022 at 18:02):

I tried, it doesn't help.

Gabriel Ebner (Feb 18 2022 at 18:02):

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 (Feb 18 2022 at 18:02):

But nat.gcd isn't.

Kyle Miller (Feb 18 2022 at 18:03):

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

example : nat.coprime 5 3 := by dec_trivial

Yury G. Kudryashov (Feb 18 2022 at 18:26):

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 (Feb 18 2022 at 18:35):

@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 (Feb 18 2022 at 19:01):

I guess, I'm responsible for this attempt.


Last updated: Dec 20 2023 at 11:08 UTC