Stuck on first project -- de Bruijn indices

Stream: new members

[Joseph Junker]

Hi, I'm trying to get started using Lean by doing exercises with basic lambda calculi, but I've hit a roadblock pretty early. I'm trying to implement de Bruijn conversion for untyped lambda calculus terms and prove that the conversion is lossless. Here's where I'm at so far:

import Lean.Data.HashSet
import Lean.Data.HashMap

namespace LC

inductive LCTerm where
| var (name : String) : LCTerm
| abs (varName : String) (body: LCTerm) : LCTerm
| app (fn : LCTerm) (arg: LCTerm) : LCTerm
deriving Repr

inductive DBLCTerm where
| var (info : String) (n : Nat) : DBLCTerm
| abs (info : String) (body : DBLCTerm) : DBLCTerm
| app (fn : DBLCTerm) (arg : DBLCTerm) : DBLCTerm
deriving Repr

def freeVars (term : LCTerm) (bound : (Std.HashSet String)) : Std.HashSet String :=
  match term with
  | .var name => if bound.contains name then .empty else .ofList [name]
  | .abs name body => freeVars body (bound.insert name)
  | .app fn arg => .insertMany (freeVars fn bound) (freeVars arg bound)

abbrev Bindings := Lean.AssocList String Nat

def addBinding (bindings : Bindings) (name : String) : Bindings :=
  (bindings.mapVal (· + 1)).insert name 0

def freeBindings (term : LCTerm) : Bindings :=
  let vars := (freeVars term Std.HashSet.empty).toList
  vars.foldl (addBinding · ·) Lean.AssocList.empty

def removeNames (term : LCTerm) (bindings : Bindings) : Option DBLCTerm :=
  match term with
  | .var name =>
    match bindings.find? name with
    | .some value => .some (.var name value)
    | .none => .none
  | .abs varName body =>
    match removeNames body (addBinding bindings varName) with
    | .some value => .some (.abs varName value)
    | .none => .none
  | .app fn arg =>
    match removeNames fn bindings with
    | .none => .none
    | .some fn' => match removeNames arg bindings with
      | .none => .none
      | .some body' => .some (.app fn' body')

def totalRemoveNames (term : LCTerm) : (Bindings × DBLCTerm) :=
  let bindings := freeBindings term
  let converted := removeNames term bindings
  have h : converted.isSome = true := by
    induction term
    case var name => (
      have h' : (bindings.contains name) := by

    )

Using an AssocList lead to there being a ton of optional handling noise in removeNames, so I'm trying to prove that the result will always be a some when the initial bindings are complete. I can't seem to make any progress on this proof, though. My proof state is this:

name : String
bindings : Bindings := freeBindings (LCTerm.var name)
converted : Option DBLCTerm := removeNames (LCTerm.var name) bindings
⊢ Lean.AssocList.contains name bindings = true

I'm trying to unfold the definition of freeBindings inside of bindings, but unfold and simp won't make any progress.

I have two questions: How can I make progress on this proof? And given that what I have so far is really messy, is there an easier way to approach this?

[Johannes Tantow]

You can use simp[bindings] to replace the term by the let value in the goal and then unfold freeBindings inside the goal.

[Robin Arnez]

1. The correct import for HashMap and HashSet is in Std: Std.Data.HashSet and Std.Data.HashMap. The versions in Lean are deprecated in favour of the ones in Std which you were already using but I would just note that.
2. Lean.AssocList has no proof foundation. If you really want to have performant computable definitions, you can also use Std.HashMap or just List (String × Nat).
3. If you want this to just be a formalization problem, it would probably be easier to use things like String → Nat and Set String or String → Bool. While there are a lot of proofs on HashMap etc., there aren't e.g. for insertMany of two HashSets (you would probably use union here but that one also doesn't have sufficient proofs).

[Johannes Tantow]

While insertMany for inserting a hashset has no lemmas yet, there are (currently only in the release candidate) lemmas for insertMany for lists. You could use insertMany s1 s2.toList and use the lemmas for this.