using the dec_trivial tactic

Stream: new members

[Julian Sutherland]

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]

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

[Reid Barton]

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

[Reid Barton]

A common mistake is not using docs#decidable_of_iff

[Julian Sutherland]

@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]

And floor_root?

[Julian Sutherland]

@Reid Barton Yes sorry, the type of floor_root is as follows:

floor_root : ℕ → ℕ → ℕ

[Reid Barton]

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]

Yes and does it reduce (e.g. #reduce floor_root 2 2)?

[Julian Sutherland]

@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]

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]

Yeah #eval is more powerful.

[Reid Barton]

Can you give a MWE containing floor_root? (it doesn't seem to exist in mathlib)

[Julian Sutherland]

@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]

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

[Reid Barton]

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

[Julian Sutherland]

@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]

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

[Reid Barton]

Or rather, it is required for the term to reduce

[Patrick Johnson]

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]

@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_trivial isn't a tactic

[Julian Sutherland]

@Reid Barton Yup, my bad! :smile:

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Julian Sutherland]

@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]

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

[Julian Sutherland]

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

[Yaël Dillies]

It should be called docs#not.decidable

[Yaël Dillies]

Bingo!

[Julian Sutherland]

@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]

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

[Yaël Dillies]

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