Prove Mathemetical Function is Bijective

Stream: new members

[Chase Wilson]

Hey y'all, I'm trying to prove that this mathematical function is bijective, but I'm really new to theorum proving so I'm honestly just flailing trying to figure things out. So far I have this code, which is incomplete and errors out

import data.int.basic
import tactic.suggest

-- fn next(i: NonZeroU64) -> NonZeroU64 {
--     let i = i.get();
--     let n = (i << 1) ^ (i >> 63 ^ i >> 62 ^ i >> 60 ^ i >> 59) & 1;
--
--     // Safety: I hope I got the math right
--     unsafe { NonZeroU64::new_unchecked(n) }
-- }
namespace prove_prng

open int function

infixr ` << ` : 50 := int.shiftl
infixr ` >> ` := int.shiftr
infixr ` ⊕ ` := int.lxor
infixr ` & ` : 60 := int.land

def prng (i : ℤ) : ℤ :=
  (i << 1) ⊕ ((i >> 63) ⊕ (i >> 62) ⊕ (i >> 60) ⊕ (i >> 59)) & 1

#eval prng 100
#eval prng 0

theorem injective_prng : injective @prng :=
begin
  assume x₁ x₂,
  assume H : prng x₁ = prng x₂,
  repeat { rw [prng] at H },
  induction x₁ using int.induction_on,
  induction x₂ using int.induction_on,
  { trivial },
  { apply int.zero_shiftr -- Error occurs here
  , apply int.zero_shiftl }
  -- There's more cases since I applied induction twice
end
  -- Also tried this:
  -- assume x₁ x₂,
  -- assume H : prng x₁ = prng x₂,
  -- show x₁ = x₂,
  --   from H

theorem surjective_prng : surjective @prng :=
  sorry

theorem bijective_prng : bijective @prng :=
  and.intro injective_prng surjective_prng

end prove_prng

The error it produces is this:

invalid apply tactic, failed to unify
  0 = ↑x₂_i + 1
with
  0 >> ?m_1 = 0
state:
case hz, hp
x₂_i : ℕ,
x₂_ᾰ :
  (0 << 1 ⊕ (0 >> 63 ⊕ 0 >> 62 ⊕ 0 >> 60 ⊕ 0 >> 59) & 1) =
    (↑x₂_i << 1 ⊕ (↑x₂_i >> 63 ⊕ ↑x₂_i >> 62 ⊕ ↑x₂_i >> 60 ⊕ ↑x₂_i >> 59) & 1) →
  0 = ↑x₂_i,
H :
  (0 << 1 ⊕ (0 >> 63 ⊕ 0 >> 62 ⊕ 0 >> 60 ⊕ 0 >> 59) & 1) =
    (↑x₂_i + 1 << 1 ⊕
       (↑x₂_i + 1 >> 63 ⊕ ↑x₂_i + 1 >> 62 ⊕ ↑x₂_i + 1 >> 60 ⊕ ↑x₂_i + 1 >> 59) & 1)
⊢ 0 = ↑x₂_i + 1

But honestly, I don't even know if I'm heading in the right direction, any advice?

[Eric Rodriguez]

what do you want your tactic state to be? apply basically means "if my goal is B, and I have A → B, then A suffices".

[Chase Wilson]

For lack of a better term, I want to "execute the function on the state", I want to remove all the instances of zero being bitshifted in favor of a literal zero

[Patrick Johnson]

You probably want simp_rw [int.zero_shiftr, int.zero_shiftl] at * instead of apply int.zero_shiftr, apply int.zero_shiftl

[Chase Wilson]

Ahh, thanks! And another thing, I'd like to do this with a representation of 64bit integers but I think int is an unbounded integer, fin looks like what I want (bounded integers) but I can't find bitwise operations over it

[Johan Commelin]

Yeah, you'll probably have to implement them yourself

[Chase Wilson]

Drat, thank you!

[Chase Wilson]

How would I remove duplicate terms from each side of the equation, turning x + 1 = y + 1 into x = y?

[Johan Commelin]

congr

[Yakov Pechersky]

You can also use the fact that addition is injective. Do you have x + 1 = y + 1 as a goal or as hypothesis?

[Patrick Johnson]

or use docs#add_left_inj

[Chase Wilson]

Currently it's a hypothesis

[Yakov Pechersky]

Right, so congr won't work on a hypothesis. Because that would mean that 1 / 0 = 2 / 0 would imply 1 = 2.

[Martin Dvořák]

Fun fact: the term 1 / 0 = 2 / 0 reduces to true.

[Patrick Johnson]

Implementing unsigned 64-bit integers and bitwise operations on them is not that hard:

import data.list
import tactic
open list

structure uint64_t : Type :=
(bits : list bool)
(h : bits.length = 64)

def zero : uint64_t :=
{ bits := repeat ff 64,
  h := by rw length_repeat }

def not' (a : uint64_t) : uint64_t :=
{ bits := a.1.map bnot,
  h := by rw [←a.2, length_map] }

def and' (a b : uint64_t) : uint64_t :=
{ bits := zip_with band a.1 b.1,
  h := by rw [←(_ : min a.1.length b.1.length = 64),
  length_zip_with]; rw [a.2, b.2, min_self] }

def or' (a b : uint64_t) : uint64_t :=
not' (and' (not' a) (not' b))

[Yaël Dillies]

Just use vector bool 64