How to have constraint on inductively defined type

Stream: lean4

[Xubai Wang]

For example, I want to have an expression on real

inductive Expr
| const : Real -> Expr
| add : Real -> Real -> Expr
| mul : Real -> Real -> Expr
| neg : Real -> Expr
| inv : (e : Expr) -> r  ≠  0 -> Expr

How to do the r ≠ 0 part in the inv arm?

[Xubai Wang]

I mean, Expr type must be defined before we have any Eq instance on it. But it seems that only mutually inductive type is allowed in mutual block, so there is no way to define such an instance?

[James Gallicchio]

(do you mean (e : Expr) -> e ≠ 0 -> Expr?)

[Xubai Wang]

Oh, yes. editted.

[James Gallicchio]

I think the way I was recommended to do this before is to separate concerns -- define your inductive type, without constraining valid values, and then define a predicate for valid values.

inductive Expr
| const : Real -> Expr
| add : Expr -> Expr -> Expr
| mul : Expr -> Expr -> Expr
| neg : Expr -> Expr
| inv : Expr -> Expr

def eval : Expr -> Real := sorry

def validExpr : Expr -> Prop
| .const _ => True
| .add e₁ e₂ => validExpr e₁ ∧ validExpr e₂
| .mul e₁ e₂ => validExpr e₁ ∧ validExpr e₂
| .neg e => validExpr e
| .inv e => eval e ≠ 0 ∧ validExpr e

[James Gallicchio]

and then, you can write functions which take (e : Expr) -> validExpr e -> ... and match on both simultaneously, which gives you a proof that eval e ≠ 0 in the .inv e case

[Xubai Wang]

Thanks! That's exactly what I need.

[Xubai Wang]

I also have another question. The original use of this is to have symbolic computation on real, while mathlib3 already have some applications, e.g. the docs#deriv simplifier:

example (x : ℝ) : deriv (λ x, cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) :=
by { simp, ring }

But I just couldn't figure out how it is done. Is this simpilfier achieved on meta level? And can we extend it to automatic symbolic computation?