Normalizing a synthetic integer type

Stream: new members

[Brandon Brown]

I've created my own synthetic integer type (i.e. not derived from the natural numbers type). The problem with this version of the integers is that there are many redundant ways of encoding the same integer. I want to have a normalization function that takes an arbitrary integer of this type and reduces it to a normal or canonical form of either succ (succ (succ ... zero ) ) or pred (pred (pred ... zero)). I'm finding this difficult to do in a pure functional way as someone novice at both Lean and functional programming in general. Any hints? [Lean3].

inductive Int
| zero : Int
| succ : Int → Int
| pred : Int → Int

open Int
-- This function can deal with integers encoded with alternating (succ (pred ...) ) but not forms like pred (pred (succ (succ zero )))
def norm : Int → Int
| zero := zero
| (succ (pred a)) := norm a
| (pred (succ a)) := norm a
| (succ a) := succ (norm a)
| (pred a) := pred (norm a)

#reduce norm $ succ $ pred $ succ $ pred $ zero -- zero
#reduce norm $ succ $ succ $ succ $ pred $ pred $ zero -- zero.pred.succ.succ

[Eric Rodriguez]

this feels like the bracketing problem with DFAs (well formed bracketed expressions aren't a regular language). Not sure if the eqn compiler can do something powerful than a DFA? maybe with a fuel parameter, or well-founded recursion?

[Kevin Buzzard]

Just to be clear -- this is not the integers, because succ(pred(0)) isn't equal to 0. Do you want to put an equivalence relation on this type and work with equivalence classes? Then you could get the integers on the nose.

[Kevin Buzzard]

Once you have the actual integers, then you can define simp lemmas such as cl(succ(pred(x))=cl(x) and then the simplifier will be able to do the reduction for you.

[Kevin Buzzard]

I doubt the equation compiler can match on subterms, so it won't be able to get to succ(succ(succ....(succ(pred(zero)))..) for an arbitrarily long string because it's matching from the left and it can only have finitely many rules. But the simplifier can do this -- but only with equalities and <->s, so that's why I'm suggesting that you pass to the equivalence classes first.

[Yakov Pechersky]

The fixed point of norm would work.

[Kevin Buzzard]

but norm as it stands won't change s(s(p(0))) to s(0), so what exactly do you mean by this?

[Johan Commelin]

You can define a function Int -> nat that counts the number of succ and preds in a term. Now iterate norm that many times on the term.

[Eric Rodriguez]

don't the last two lines fix that Kevin?

[Johan Commelin]

@Eric Rodriguez

#reduce norm $ succ $ succ $ succ $ pred $ pred $ zero -- zero.pred.succ.succ

[Kevin Buzzard]

You're right, it's better than I thought, but it's still not good enough. Maybe there is a trick then?

[Yakov Pechersky]

Johan is right:

import logic.function.iterate

@[derive decidable_eq]
inductive Int
| zero : Int
| succ : Int → Int
| pred : Int → Int

open Int

def rearr : Int → Int
| (pred (succ a)) := succ (rearr (pred a))
| a := a

def norm : Int → Int
| (succ (succ a)) := succ (norm (succ a))
| (pred (pred a)) := pred (norm (pred a))
| (succ (pred a)) := (norm a)
| (pred (succ a)) := (norm a)
| a := a

def count : Int -> int
| zero := 0
| (succ a) := 1 + count a
| (pred a) := -1 + count a

def count' : Int -> nat
| zero := 0
| (succ a) := 1 + count' a
| (pred a) := 1 + count' a

#reduce let x := succ $ succ $ succ $ pred $ pred $ zero in norm^[count' x] x -- zero.succ

[Eric Rodriguez]

the iteration operator is cool, i hadn't seen that before

[Johan Commelin]

Of course it is mighty inefficient (-;

[Kevin Buzzard]

I see, you have to apply norm more than once!

[Yakov Pechersky]

Exercise for the reader: define a well_founded relation that will allow you to take the fixpoint of norm, so you don't have to rely on count'.

[Mario Carneiro]

I think this is a more elegant single pass solution:

def up : Int → Int
| (pred a) := a
| a := succ a

def down : Int → Int
| (succ a) := a
| a := pred a

def norm_aux : Int → Int → Int
| acc (succ a) := norm_aux (up acc) a
| acc (pred a) := norm_aux (down acc) a
| acc zero := acc

def norm := norm_aux zero

#reduce norm $ succ $ pred $ succ $ pred $ zero -- zero
#reduce norm $ succ $ succ $ succ $ pred $ pred $ zero -- zero.succ

[Mario Carneiro]

The secret is that acc is actually an int in disguise: it is always either succ^n zero or pred^n zero because we consistently head-normalize it

[Mario Carneiro]

and this is linear time to boot

[Brandon Brown]

Thanks, everyone!

[Brandon Brown]

So if I use @Mario Carneiro 's norm function, then I can define a subtype like def Int2 : Type := { x : Int // (norm x) = x } Would this be a suitable alternative to creating a quotient type? I'd have to prove the idempotence of norm

[Mario Carneiro]

Yes, that would work. There are a couple ways you could express that proposition: it is also the set of Int values accessible by applying up and down to zero (it is easy to prove that norm produces elements in that subset), as well as the set of values of the form succ^n zero or pred^n zero (which would be a good starting point for proving isomorphism to int)

[Mario Carneiro]

If I label the conditions as (P1) norm x = x (P2) inductively generated by up,down,zero (P3) succ^n zero or pred^n zero, then there are the following lemmas:

• P2 (norm x), and more generally P2 acc -> P2 (norm_aux acc x) (by induction on x), therefore P1 -> P2
• P3 x -> P3 (up x), P3 (down x) (by cases), therefore P2 -> P3
• norm (succ^n zero) = succ^n zero (by induction on n) and similarly for pred, therefore P3 -> P1

[Mario Carneiro]

Therefore norm is idempotent because P2 (norm x) so by P1 norm (norm x) = norm x

[Kevin Buzzard]

You need more than idempotence of norm, you need to prove that norm gives rise to a set of representatives for the equivalence relation, i.e. a related to b iff norm(a)=norm(b) and a related to norm(a).

[Mario Carneiro]

Here, there is no explicit equivalence relation, it is just norm a = norm b. So the claim that norm a is related to a is just norm (norm a) = norm a, and a related to b iff norm a = norm b is true by definition

[Brandon Brown]

Yeah on the surface this seems easier than making a setoid and quotient.

[Eric Wieser]

Is it always possible to replace a quotient type with a subtype in this way?

[Eric Wieser]

Oh, I guess that's {x // (quot.mk r x).out = x}, and docs#quot.out is essentially the proof the answer is yes

[Kevin Buzzard]

It's non-computable but yes

[Kevin Buzzard]

You choose an element in each equivalence class

[Brandon Brown]

I've been banging my head on this for a long time and I am just not competent enough yet to solve this in any reasonable amount of time. Hoping someone can help. I'm trying to prove is_norm (norm i) using the norm function @Mario Carneiro made
By staring at the definition, clearly norm i produces a b_int of the form succ^n zero or pred^n zero (but I dont know how to prove it) and both of these can be proven to be in normal form according to is_norm.

MWE in Lean4:

inductive b_int : Type
| zero : b_int
| succ : b_int → b_int
| pred : b_int → b_int

open b_int

def is_norm (a : b_int) : Bool :=
match a with
| zero => true
| succ (pred a) => false
| pred (succ a) => false
| succ a => is_norm a
| pred a => is_norm a

def int := {x : b_int // is_norm x}

def up : b_int → b_int
| (pred a) => a
| a => succ a

def down : b_int → b_int
| (succ a) => a
| a => pred a

-- 1st arg is constructed, 2nd is input
def norm_aux : b_int → b_int → b_int :=
  fun a b =>
  match b with
  | zero => a
  | succ b => norm_aux (up a) b
  | pred b => norm_aux (down a) b

def norm : b_int → b_int := norm_aux zero

#reduce norm zero.pred.pred.succ.succ.succ.pred.pred.pred -- pred (pred zero)
#reduce is_norm $ norm zero.pred.pred.succ.succ.succ.pred.pred.pred -- true

theorem is_norm_norm (i : b_int) : is_norm (norm i) = true := sorry

[Mario Carneiro]

I sketched this proof above. Prove these lemmas:

theorem is_norm_up : is_norm a -> is_norm (up a) := sorry
theorem is_norm_down : is_norm a -> is_norm (down a) := sorry
theorem is_norm_norm_aux : is_norm a -> is_norm (norm_aux a b) := sorry
theorem is_norm_norm : is_norm (norm a) := sorry

[Brandon Brown]

Thanks, @Mario Carneiro ! I proved the first 3 lemmas, now working on is_norm_norm

theorem is_norm_up : is_norm a -> is_norm (up a) := by
  intros h1
  induction a with
  | zero => rfl;
  | succ a h2 =>
    show is_norm (succ (succ a)) = true;
    assumption;
  | pred a h3 =>
    show is_norm (a) = true;
    cases a with
    | zero => rfl;
    | succ a =>
      contradiction;
    | pred a =>
      assumption;

theorem is_norm_down : is_norm a -> is_norm (down a) := by
  intros h1
  induction a with
  | zero => rfl;
  | succ a h2 =>
    show is_norm (a) = true;
    cases a with
    | zero => rfl;
    | succ a =>
      assumption
    | pred a =>
      contradiction;
  | pred a h3 =>
    show is_norm (pred (pred a)) = true;
    assumption


theorem norm_i_succ : norm (i.succ) = norm_aux zero.succ i := rfl
theorem norm_i : norm i = norm_aux zero i := rfl
theorem norm_aux_succ_i : norm_aux zero (succ i) = norm_aux zero.succ i := rfl
theorem norm_aux_succ_eq_up : norm_aux a (succ i) = norm_aux (up a) i := rfl
theorem norm_aux_pred_eq_down : norm_aux a (pred i) = norm_aux (down a) i := rfl

theorem is_norm_norm_aux : is_norm a -> is_norm (norm_aux a b) :=
  fun h1 =>
  match a with
  | zero =>
    match b with
    | zero => rfl
    | succ b => by
      rw [norm_aux_succ_eq_up];
      have h2 : is_norm (up zero) from is_norm_up h1
      exact is_norm_norm_aux h2
    | pred b => by
      rw [norm_aux_pred_eq_down];
      have h2 : is_norm (down zero) from is_norm_down h1
      exact is_norm_norm_aux h2
  | succ a =>
    match b,h1 with
    | zero, h1 => by
      exact is_norm_up h1
    | succ b, h1 => by
      rw [norm_aux_succ_eq_up];
      show is_norm (norm_aux (succ (succ a)) b)
      exact is_norm_norm_aux h1
    | pred b, h1 => by
      rw [norm_aux_pred_eq_down]
      have h2 : is_norm (down (succ a)) from is_norm_down h1
      exact is_norm_norm_aux h2
  | pred a =>
    match b,h1 with
    | zero, h1 => by
      exact is_norm_down h1
    | succ b, h1 => by
      rw [norm_aux_succ_eq_up];
      have h2 : is_norm (up (pred a)) from is_norm_up h1
      exact is_norm_norm_aux h2
    | pred b, h1 => by
      rw [norm_aux_pred_eq_down]
      have h2 : is_norm (down (pred a)) from is_norm_down h1
      exact is_norm_norm_aux h2

[Mario Carneiro]

Your proof of is_norm_norm_aux is suspiciously long. It should be: induction on b generalizing a, and then apply h, IH (is_norm_up h) and IH (is_norm_down h) in the three cases

[Brandon Brown]

Yes... this is indeed quite a bit shorter , thanks again

theorem is_norm_norm_aux : is_norm a -> is_norm (norm_aux a b) := by
  intro h1
  induction b generalizing a with
  | zero => exact h1
  | succ b h2 =>
    show is_norm (norm_aux (up a) b)
    have h3 : is_norm (up a) from is_norm_up h1
    exact h2 h3
  | pred b h2 =>
    show is_norm (norm_aux (down a) b)
    have h3 : is_norm (down a) from is_norm_down h1
    exact h2 h3

[Brandon Brown]

And it's done

theorem is_norm_norm : is_norm (norm a) :=
  match a with
  | zero => rfl
  | succ a => by
    have h1 : is_norm (zero) from rfl
    exact is_norm_norm_aux h1
  | pred b => by
    have h1 : is_norm (zero) from rfl
    exact is_norm_norm_aux h1

[Brandon Brown]

Thank you very much for the guidance @Mario Carneiro . I can finally sleep in peace (thinking about this has been keeping me up at night).

[Mario Carneiro]

for the last proof, you don't need a match at all

[Mario Carneiro]

is_norm_norm_aux rfl

[Brandon Brown]

Oh right, even better. I really need to work on simplicity

[Kevin Buzzard]

I think long proofs is fine when you're just learning. You need to experience the "goals accomplished" triumph :-)