rearranging equations

Stream: general

[Matthew Pocock]

I have the equation 2 * j = 3 * (1 + 2 * i) + 1 as an intermediate goal, and I would like to rewrite it in terms of j=... as I need the j to plug into an existential. I'm having trouble even simplifying the rhs to 4+2i. From there, I should be able to divide through by 2, to get j = 2+i, assuming my high-school algebra isn't too rusty. I have had a quick scan through the mathematics in lean book, but haven't been able to find anything to help me so far.

[Scott Morrison]

If you post a #mwe you will get much better help!

[Matthew Pocock]

Scott Morrison said:

If you post a #mwe you will get much better help!

import Mathlib.Tactic.LibrarySearch

variable (n : Nat)
variable (a b c : Nat)
variable (i j k : Nat)

def is_even a := ∃ b, 2*b = a

def is_odd a := ∃ b, 1 + 2*b = a

def collatz := if n % 2 == 0 then n / 2 else 3 * n + 1

theorem collatz_odd_to_even : is_odd n -> is_even (collatz n) := by
    simp [is_odd, is_even, collatz]
    intro i                                 -- odd generator
    intro hn                                -- collatz argument
    subst hn                                -- expand i for n
    refine Exists.intro j ?h                -- break up the existential
    refine Iff.mpr eq_ite_iff ?h.a          -- rewrite the if/else
    simp [Nat.add_mul_mod_self_left 1 2 i]  -- and leave us with the odd case

I am not sure if this is the nicest way to approach this problem. j=2+ishould be the existential witness that completes the proof.

[Adam Topaz]

It's unclear to me why you want the j at all here.

[Adam Topaz]

It seems that you should rather use i.

[Adam Topaz]

Well, not i exactly, but at least some expression involving i.

[Adam Topaz]

Ungolfed Spoiler!

import Mathlib.Data.Nat.Basic

variable (n : Nat)
variable (a b c : Nat)
variable (i j k : Nat)

def is_even a := ∃ b, 2*b = a

def is_odd a := ∃ b, 1 + 2*b = a

def collatz := if n % 2 == 0 then n / 2 else 3 * n + 1

theorem collatz_odd_to_even : is_odd n -> is_even (collatz n) := by
    simp [is_odd, is_even, collatz]
    intro i                                 -- odd generator
    intro hn                                -- collatz argument
    subst hn                                -- expand i for n
    refine Exists.intro (3 * i + 2) ?h
    refine Iff.mpr eq_ite_iff ?h.a          -- rewrite the if/else
    simp [Nat.add_mul_mod_self_left 1 2 i]  -- and leave us with the odd case
    simp [mul_add, add_comm 3, ← mul_assoc]

[Adam Topaz]

Golfed spoiler

theorem collatz_odd_to_even : is_odd n -> is_even (collatz n) := by
  rintro ⟨i, rfl⟩
  use 3 * i + 2
  simp [collatz, mul_add, add_comm 3, ← mul_assoc]

[Matthew Pocock]

Thank you. I'll try to understand both proofs :D

[Matthew Pocock]

Adam Topaz said:

  rintro ⟨i, rfl⟩
  use 3 * i + 2

Is there something that I need to import to get the use tactic? My session says that it is an unknown tactic.

In the rintro tactic, is rfl being used as a name for the introduced goal, or is it immediately applying the rfl tactic to whatever fits into that slot in the constructor? I haven't seen targets used "in place" like that before.

[Alex J. Best]

import Mathlib.Tactic should be enough to get you all "standard" tactics

[Alex J. Best]

The rfl is like a keyword for rintro and it tells rintro to automatically substitute the introduced equality instead of returning it as a new hypothesis

[Matthew Pocock]

Alex J. Best said:

The rfl is like a keyword for rintro and it tells rintro to automatically substitute the introduced equality instead of returning it as a new hypothesis

Thanks. That import has got it working. Cheers!

[Matthew Pocock]

Do I need to have in mind that 3*i+2 is the value I'm looking for, or can I use a tactic that will summon this term somehow? Perhaps this is the difference between an interactive proof assistant and a fully automated solver.