Zulip Chat Archive

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

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

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