porting `Data.Nat.WithBot`

Stream: mathlib4

[Moritz Firsching]

https://github.com/leanprover-community/mathlib4/pull/1255

I'm trying to port data.nat.with_bot. The problem here seems to be that the tactic "tauto" is used. I thought because of https://github.com/leanprover-community/mathlib4/pull/1081 might be enough, but when I import Mathlib.Tactic.Tauto I the following error:

(deterministic) timeout at 'whnf', maximum number of heartbeats (1000000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

(after increasing the number of heartbeats).

So is there something wrong with tauto and should I wait until that tactic has been improved or is there some way to proceed with the port of that file?

[Ruben Van de Velde]

You can try to prove the goals manually

[Ruben Van de Velde]

Maybe show_term { tauto } on the mathlib3 side can help

[Moritz Firsching]

good idea!
show_term { tautology } is giving

Try this: exact {mp := λ (ᾰ : none + none = 0), option.no_confusion ᾰ,
 mpr := λ (ᾰ : none = 0 ∧ none = 0),
          ᾰ.dcases_on (λ (ᾰ_left ᾰ_right : none = 0), option.no_confusion ᾰ_left)}

[Kevin Buzzard]

Try doing a combination of cases and refl.

[Moritz Firsching]

I managed to make the ported file work, https://github.com/leanprover-community/mathlib4/pull/1255/files, but it is a bit ridiculous because there are things like this now:

  · refine' ⟨fun h => Option.noConfusion h, fun h => _⟩
    cases h with
    | inl hl => exact Option.noConfusion hl.1
    | inr hr => cases hr with
      | inl hrl => exact Option.noConfusion hrl.1
      | inr hrr => cases hrr with
        | inl hrrl => exact Option.noConfusion hrrl.1
        | inr hrrr => exact Option.noConfusion hrrr.1

I tried to use rcases instead, but couldn't get it to work. How can I make rcases it to keep splitting of the or's and then use exact Option.noConfusion h.1?

[Jannis Limperg]

You could also try to throw Aesop at the goals. It's not a complete replacement for tauto, but in practice it often works.

[Moritz Firsching]

That worked, thanks!