Need help for proving List membership theorem

Stream: new members

[Mikaël Mayer]

Hello, I'm new to Lean4, and I'm struggling to do something that I thought would be simple. Even ChatGPT and Claude answered things that did not work and many times in a row.

Basically, I have the following code.

https://live.lean-lang.org/#codez=JYOwJgrgxgLsBuBTABAUQB4AcBOyBcyAKgJ6YoDuAFotogFDLIA+yIAhgLYoAUU+yAZRjZQAcwCUDZsmGIUybogCMyRACZ+GHJLphEAM2T7aiAGptsAZ0Was2cfwAywSzEHCx+ALxSObGFCUqsjkwDCUUiwAdOxcrMheAHzIANogALqRyFGyKAA2Bm4iopRuSUYm5lbIBfpuANT1FXJVlsjFpXS6Bs2WQdzo/EIiIBIKKARa9vwAQgD2c3neUoOAkEQKxi0WbYg6dOGIc7QcvZQA+rn4Upt9yIPcOSY1he3AJTAOPow3QYO1boByIlOd1e728yAARsQpJZgBxMKkfgAaZpmbbpIA

inductive Expr : Type where
  | name (c : String)
  | tree  (e1 e2 : Expr)

def freeVars(e : Expr) : List String :=
  match e with
  | .name n => [n]
  | .tree left right => freeVars left ++ freeVars right

def fresh (x : String) (e : Expr) : Bool :=
  x ∉ (freeVars e)

theorem fresh_tree :
  fresh x (.tree left right) =
  fresh x left ∧ fresh x right := by
  simp [fresh, freeVars]

and I can't find a way to complete the proof.
If you could recommend extensions that can also help me find tactics that can apply, I'm pretty clueless as well. I tried using calc, Bool.decide_eq_true, etc.

[Bryan Gin-ge Chen]

Looks like you're just missing parentheses in fresh_tree:

inductive Expr : Type where
  | name (c : String)
  | tree  (e1 e2 : Expr)

def freeVars(e : Expr) : List String :=
  match e with
  | .name n => [n]
  | .tree left right => freeVars left ++ freeVars right

def fresh (x : String) (e : Expr) : Bool :=
  x ∉ (freeVars e)

theorem fresh_tree :
  fresh x (.tree left right) =
  (fresh x left ∧ fresh x right) := by
  simp [fresh, freeVars] -- No goals

[Patrick Massot]

Note also your issue with parentheses would go away if you used the idiomatic ↔ instead of an equality of propositions.

[Notification Bot]

This topic was moved here from #lean4 > Need help for proving List membership theorem by Patrick Massot.

[Mikaël Mayer]

This is excellent feedback thank you so much !

[Kenny Lau]

and also Prop instead of Bool.