Can you help with this experimental expander?

Stream: new members

[Mr Proof]

Just messing about with Lean and printing out some symbolic expressions. Then I tried to implement a recursive function to expand the expressions. Suffice it to say, this didn't work due to when expanding the expressions, the output can be different types. Any tips to proceed?

I think I also need some way to tell it that a type is symbolic and has the method expandable implemented.

import Mathlib

structure Symbolic where
    name:String

structure SymbolicSum (α β:Type) where
    first:α
    second:β

structure SymbolicProduct (α β:Type) where
    first:α
    second:β

structure SymbolicFunc(α:Type) where
    name:String
    member:α

def Symbolic.add {α β:Type}(a:α)(b:β):SymbolicSum α β := ⟨a,b⟩
def Symbolic.mul {α β:Type}(a:α)(b:β):SymbolicProduct  α β := ⟨a,b⟩
def Symbolic.func {α:Type}(f:String)(a:α):SymbolicFunc α := ⟨f,a⟩


def x:Symbolic := ⟨"x"⟩
def y:Symbolic := ⟨"y"⟩
def z:Symbolic := ⟨"z"⟩

instance  : Repr (Symbolic) := { reprPrec := fun q _ => s!"{q.name}" }
instance [Repr α] [Repr β]  : Repr (SymbolicSum α β) := { reprPrec := fun q _ => s!"({repr q.first}+{repr q.second})" }
instance [Repr α] [Repr β]  : Repr (SymbolicProduct α β) := { reprPrec := fun q _ => s!"({repr q.first}*{repr q.second})" }
instance [Repr α]  : Repr (SymbolicFunc α) := { reprPrec := fun q _ => s!"{q.name}({repr q.member})" }

/- This prints symbolic expressions to the output window -/

#eval Symbolic.func "√" (Symbolic.mul (Symbolic.add (Symbolic.add 3 y) z) (Symbolic.add x (5+15) ) )
#eval Symbolic.add (Symbolic.func "sin" (Symbolic.add (Symbolic.func "√" 3) 5)) 15


/- Trying to do a recursive expand function. Didn't work :( -/





def Symbolic.expand (A:Symbolic):=A
def SymbolicSum.expand {α β:Type}(A:SymbolicSum α β):=SymbolicSum.mk A.first.expand A.second.expand
def SymbolicFunc.expand {α:Type}(A:SymbolicFunc α):= SymbolicFunc.mk A.name A.member.expand
def SymbolicProduct.expand  {α β:Type} (A:SymbolicProduct α β):=
match α,β with
| _, SymbolicSum => SymbolicSum.mk (SymbolicProduct.mk A.first.expand A.second.first.expand) (SymbolicProduct.mk A.first.expand A.second.second.expand )
| SymbolicSum, _ => SymbolicSum.mk (SymbolicProduct.mk A.first.first.expand  A.second.expand ) (SymbolicProduct.mk A.first.second.expand  A.second.expand  )
| _ , _ => SymbolicProduct.mk A.first.expand A.second.expand

#eval (Symbolic.add x y).expand

[Mr Proof]

I did a different approach here. But his time I can't get the #eval to work due to it not liking the [Repr] in the repr definition:

import Mathlib

inductive Symb
| var : String -> Symb
| sum : Symb → Symb → Symb
| prod: Symb → Symb → Symb
| foo: String → Symb → Symb
| num: Nat -> Symb

def Symb.add (a:Symb)(b:Symb):Symb := Symb.sum a b
def Symb.mul (a:Symb)(b:Symb):Symb := Symb.prod a b
def Symb.func (f:String)(a:Symb):Symb := Symb.foo f a

def w:= Symb.var "w"
def x:= Symb.var "x"
def y:= Symb.var "y"
def z:= Symb.var "z"

/-- can't get this to work-/
instance [Repr Symb] : Repr Symb :=
 { reprPrec := fun q _ =>
 match q with
 | Symb.var name=> name
 | Symb.sum a b =>s!"({repr a}+{repr b})"
 | Symb.prod a b => s!"({repr a}*{repr b})"
 | Symb.foo f b => s!"{f}({repr b})"
 | _ => s!"error"
}


#check x
#eval x

def P:=Symb.func "√" (Symb.mul (Symb.add (Symb.add (Symb.num 3) y) z) (Symb.add x (Symb.num 5) ) )
def Q:=Symb.add (Symb.func "sin" (Symb.add (Symb.func "√" (Symb.num 3)) (Symb.num 5))) (Symb.num 15)
#reduce P
#reduce Q
#eval P
#eval Q



def Symb.expand (A:Symb):=
match A with
| Symb.var _ => A
| Symb.sum a b => Symb.sum (a.expand) (b.expand)
| Symb.prod (Symb.sum a b) c=> Symb.sum (Symb.prod a.expand c.expand ) (Symb.prod b.expand c.expand)
| Symb.prod a (Symb.sum b c)=> Symb.sum (Symb.prod a.expand b.expand ) (Symb.prod a.expand c.expand)
| Symb.prod a b => Symb.prod (a.expand) (b.expand)
| Symb.foo f m => Symb.foo f m.expand
| _ => A


#reduce (Symb.mul (Symb.add x y) (Symb.add w z)).expand
#eval (Symb.add x y).expand