defeq sort and reassociation

Stream: lean4

[Tomas Skrivan]

I have a simple inductive type for expression with a single binary operation. I would like to write a function that reassociates and orders all terms in the expression. The trouble is that I want this function to work well with defeq.

The expression type:

inductive Expr where
| val (a : Nat) : Expr
| op (x y : Expr) : Expr

I want function def Expr.sort : Expr → Expr such that

example : (val 3 * (val 2 * val 1)).sort = val 1 * val 2 * val 3 := by rfl   -- The `by rfl` is important!

---

My attempt:
What is the problem with the Expr.sort function such that is causes troubl to rfl tacitc?

inductive Expr where
| val (a : Nat) : Expr
| op (x y : Expr) : Expr
deriving Inhabited

export Expr (val)

def Expr.sort : Expr → Expr
| val a => val a
| op x (val b) =>
  match x.sort with
  | val a =>
    if a ≤ b
    then op (val a) (val b)
    else op (val b) (val a)
  | op x (val a) =>
    if a ≤ b
    then op (op x (val a)) (val b)
    else op (op x (val b)).sort (val a)
  | _ => unreachable!
| op x (op y z) => (op (op x y) z).sort
decreasing_by sorry

instance : Mul Expr := ⟨λ x y => x.op y⟩

def Expr.toString : Expr → String
| val a => s!"{a}"
| op x y => s!"({x.toString} * {y.toString})"
instance : ToString Expr := ⟨λ e => e.toString⟩

-- check if it is working
#eval (val 3 * (val 2 * val 1)).sort

-- swapping works
example : (val 3 * val 2).sort = val 2 * val 3 := by rfl
example : (val 1 * val 3 * val 2).sort = val 1 * val 2 * val 3 := by rfl

-- left association does not work
example : (val 1 * (val 2 * val 3)).sort = val 1 * val 2 * val 3 := by rfl

[Tomas Skrivan]

I can do it using bubble sort on List but I would like to understand what is wrong with the function Expr.sort above

def List.bubblesort [LT α] [DecidableRel (. < . : α → α → Prop)] (l : List α) : {l' : List α // l.length = l'.length} :=
  match l with
  | [] => ⟨[], rfl⟩
  | x :: xs =>
    match bubblesort xs with
    | ⟨[], h⟩ => ⟨[x], by simp[h]⟩
    | ⟨y :: ys, h⟩ =>
      if y < x then
        have : Nat.succ (length ys) < Nat.succ (length xs) := by rw [h, List.length_cons]; apply Nat.lt_succ_self
        let ⟨zs, he⟩ := bubblesort (x :: ys)
        ⟨y :: zs, by simp[h, ← he]⟩
      else
        ⟨x :: y :: ys, by simp[h]⟩
termination_by _ => l.length

def Expr.vals : Expr → List Nat
| val a => [a]
| op x y => x.vals.append y.vals

def Expr.fromVals : List Nat → Expr
| [] => val 0
| [x] => val x
| x :: xs => op (fromVals xs) (val x)

def Expr.sort' (e : Expr) : Expr := Expr.fromVals e.vals.bubblesort.1.reverse


-- It works now!
example : (val 3 * (val 2 * val 1)).sort' = val 1 * val 2 * val 3 := by rfl

[Tomas Skrivan]

In my code I'm actually interested in doing this for expressions with one binary and one unary operations.

inductive Expr where
| val (a : Nat) : Expr
| foo (x : Expr) : Expr
| op  (x y : Expr) : Expr

But then one needs to define a bit more complicated ordering to define.

Effectively, I'm interested in finding a unique representative for each expression under assumption what op is commutative and associative operation and the function returning this representative should respect defeq.