## Stream: new members

### Topic: using the dec_trivial tactic

#### Julian Sutherland (Dec 29 2022 at 10:33):

I have an instanced of decidable for a given Prop:

instance has_no_rational_root_dec (n e : ℕ) : decidable (∀ q : ℚ, q^e ≠ ↑n)


From here, I thought that I would then simply be able to do:

example : ∀ q : ℚ, q^2 ≠ ↑2 :=  dec_trivial


to show that the square root of 2 is irrational (the appropriate infered typeclass is has_no_rational_root_dec 2 2). However, I get the following error:

exact tactic failed, type mismatch, given expression has type
true
but is expected to have type
as_true (∀ (q : ℚ), q ^ 2 ≠ ↑2)
state:
⊢ as_true (∀ (q : ℚ), q ^ 2 ≠ ↑2)


Can anyone advise on what I'm doing wrong? :smile:

#### Reid Barton (Dec 29 2022 at 10:36):

Does your decidable instance use axioms? If you use LEM, for instance, this clearly can't work.

#### Reid Barton (Dec 29 2022 at 10:36):

Specifically, has_no_rational_root_dec 2 2 needs to reduce to a constructor application

#### Reid Barton (Dec 29 2022 at 10:37):

A common mistake is not using docs#decidable_of_iff

#### Julian Sutherland (Dec 29 2022 at 11:26):

@Reid Barton Thank you for your advice!

I have now eliminated any used of the rw tactic in all of the relevant decidable instances as well as anything that appears to be non-constructive. In particular, I had a use of not_not.symm, which I have now replaced with the use of decidable.not_not.

The relevant decidable instances are now as follows:

instance neg_dec_of_dec : ∀ (p : Prop) (inst : decidable p), decidable (¬ p) :=
begin
intros p inst,
have h := (@decidable.not_not p inst).2,
cases inst with h' h',
{
exact is_true h',
},
{
apply is_false,
exact h h',
},
end

instance is_perfect_pow_dec (n e : ℕ) : decidable (is_perfect_pow n e) :=
decidable_of_iff _ (iff.symm $is_pp_equiv_lemma n e) instance has_no_rational_root_dec (n e : ℕ) : decidable (∀ q : ℚ, q^e ≠ ↑n) := begin have h₁: (¬∃ (m : ℕ), m ^ e = n) ↔ (¬∃ (m : ℕ), n = m^e), { split, repeat { rintros h ⟨m, h'⟩, apply h, use m, exact eq.symm h', }, }, apply @decidable_of_iff _ _ (rootn_not_pn_irr e n) ( @decidable_of_iff _ _ h₁ ( neg_dec_of_dec _ (is_perfect_pow_dec n e) ) ), end  where in a particular: theorem rootn_not_pn_irr : ∀ e n : ℕ, (¬ (∃ m : ℕ, n = m^e) ↔ ∀ q : ℚ, q^e ≠ n)  and lemma is_pp_equiv_lemma (n e : ℕ) : is_perfect_pow n e ↔ (floor_root e n)^e = n  However, despite these changes, the problem still persists... #### Reid Barton (Dec 29 2022 at 11:28): And floor_root? #### Julian Sutherland (Dec 29 2022 at 11:30): @Reid Barton Yes sorry, the type of floor_root is as follows: floor_root : ℕ → ℕ → ℕ  #### Reid Barton (Dec 29 2022 at 11:30): It's okay to use axioms (like propext) inside the proof argument of decidable_of_iff--it's just the data part that needs to be able to reduce #### Reid Barton (Dec 29 2022 at 11:30): Yes and does it reduce (e.g. #reduce floor_root 2 2)? #### Julian Sutherland (Dec 29 2022 at 11:37): @Reid Barton It appears that lean diverges when I run either of: #reduce floor_root 2 2 #reduce has_no_rational_root_dec 2 2  However if I run: #eval floor_root 2 2 #eval has_no_rational_root_dec 2 2  I get: 1  and tt  respectively, as expected. #### Julian Sutherland (Dec 29 2022 at 11:39): and furthermore, if I run: #eval has_no_rational_root_dec 4 2  I get ff. It appears to be working as expected. #### Reid Barton (Dec 29 2022 at 11:40): Yeah #eval is more powerful. #### Reid Barton (Dec 29 2022 at 11:40): Can you give a MWE containing floor_root? (it doesn't seem to exist in mathlib) #### Julian Sutherland (Dec 29 2022 at 11:44): @Reid Barton Of course, thanks for helping! floor_root's definition is a bit convoluted: def floor_root_helper (e : ℕ) (h : e ≥ 1) (n : ℕ) : ∀ (m : ℕ), m ^ e ≤ n → ℕ | m h' := if h₁ : (n < (m + 1) ^ e) then m else have n - (m + 1) ^ e < n - m ^ e := floor_root_helper_termination_lemma e n m h (by linarith), floor_root_helper (m + 1) (by linarith) using_well_founded { rel_tac := λ _ _, [exact ⟨_, measure_wf$ λ ⟨m, _⟩, n - m ^ e⟩] }

def floor_root : ℕ → ℕ → ℕ
| e n :=
if h : e ≥ 1
then floor_root_helper e h n 0
begin
have h₁ : 0 ^ e = 0,
cases e,
{
exfalso,
simp at h,
exact h,
},
{
cases e,
{
simp,
},
{
rw pow_succ,
simp,
},
},
rw h₁,
exact zero_le _,
end
else 1


where in particular:

lemma floor_root_helper_termination_lemma :
∀ e n m : ℕ, e ≥ 1 →  n ≥ (m + 1) ^ e →
n - (m + 1) ^ e < n - m ^ e


#### Kevin Buzzard (Dec 29 2022 at 11:45):

(Results provided by #eval aren't certified by the kernel)

#### Reid Barton (Dec 29 2022 at 11:45):

I think things defined by well-founded recursion just don't reduce

#### Julian Sutherland (Dec 29 2022 at 11:49):

@Kevin Buzzard I see, which I guess is probably helping it be more permissive here.

@Reid Barton I see, so the only solution here would be to find some definition of floor_root that works purely by structural induction? Out of curiosity, do you know why this is the case? It seems somehow surprising as the proof of well-foundedness is not required to compute the result of the function.

#### Reid Barton (Dec 29 2022 at 11:50):

It is required though, because the definition is really by induction on that proof

#### Reid Barton (Dec 29 2022 at 11:50):

Or rather, it is required for the term to reduce

#### Patrick Johnson (Dec 29 2022 at 11:54):

Simpler floor_root:

def floor_root' (e n : ℕ) : ℕ → ℕ
| 0 := 0
| (k+1) := if k ^ e ≤ n then k else floor_root' k

def floor_root (e n : ℕ) : ℕ := floor_root' e n n


#### Julian Sutherland (Dec 29 2022 at 11:59):

@Reid Barton I think I'm missing something here, my understanding is that the proofs of well-foundedness here are only needed to guarantee that the reduction will converge, other than this, due to Prop erasure, they have no run-time existence? I'm not so familar with the exact difference between #eval and #reduce in this context.

@Patrick Johnson Thank you very much, with this simpler definition of floor_root using structural induction, the dec_trivial tactic now works! :tada:

#### Reid Barton (Dec 29 2022 at 12:03):

dec_trivial isn't a tactic

#### Julian Sutherland (Dec 29 2022 at 12:04):

@Reid Barton Yup, my bad! :smile:

#### Reid Barton (Dec 29 2022 at 12:04):

It works by reducing a decidability instance, so it is all happening in the kernel

#### Reid Barton (Dec 29 2022 at 12:04):

i.e., there is no "run-time"; everything is happening with terms

#### Reid Barton (Dec 29 2022 at 12:05):

If you look at the term that comes out of a well-founded recursion proof (probably a bad idea in general) then it will be of the form acc.rec applied to the proof of accessibility

#### Reid Barton (Dec 29 2022 at 12:08):

In theory, this could still reduce if the proof of accessibility also reduces to constructors but I think Lean doesn't do this

#### Patrick Johnson (Dec 29 2022 at 12:08):

Technically, it is a tactic: tactic#dec_trivial. There is also term-mode dec_trivial, which is essentially docs#of_as_true.

#### Julian Sutherland (Dec 29 2022 at 12:10):

@Reid Barton Understood, thanks for explaining this to me :)

One last question if it's acceptable to go a little "off-topic", the instance neg_dec_of_dec above, it feels like there has to be a better way of doing that. Any suggestions? :smile:

#### Reid Barton (Dec 29 2022 at 12:10):

I would think that it must already exist in mathlib...

#### Julian Sutherland (Dec 29 2022 at 12:11):

@Reid Barton I would have thought so too, but have been able to find it, at least within mathlib3...

#### Yaël Dillies (Dec 29 2022 at 12:12):

It should be called docs#not.decidable

Bingo!

#### Julian Sutherland (Dec 29 2022 at 12:16):

@Yaël Dillies Thanks, that's perfect, I could have sworn I tried library_search before trying to prove this manually, but apparently not!

#### Kevin Buzzard (Dec 29 2022 at 13:36):

library_search can be hit and miss with definitions. It's really designed for theorems.

#### Yaël Dillies (Dec 29 2022 at 19:29):

Did you try library_search before or after the intros p inst line? Introducing all variables before calling library_search` helps a lot.

Last updated: Dec 20 2023 at 11:08 UTC