Silly Imp problem

Stream: new members

[Kevin Sullivan]

We've implemented a minimal imperative language following Pierce's Imp chapter. On line 28, the definition of cEval, we're getting this error: infer type failed, unknown variable _f_1. We're not familiar enough with Lean's implementation to know why we're seeing this. There is no variable _f_1 in our program.

inductive bvar : Type
| mk (n : ℕ)

def bvar_eq : bvar → bvar → bool
| (bvar.mk n1) (bvar.mk n2) := n1=n2

inductive bExpr : Type
| BLit (b: bool)
| BVar (v: bvar)

def benv := bvar → bool

def bEval : bExpr → benv → bool
| (bExpr.BLit b) i := b
| (bExpr.BVar v) i := i v

def init_benv : benv := λ v, ff

def update_benv : benv → bvar → bool → benv
| i v b := λ v2, if (bvar_eq v v2) then b else (i v2)

inductive bCmd : Type
| bAssm (v : bvar) (e : bExpr)
| bSeq (c1 c2 : bCmd)

def cEval : benv → bCmd → benv
| i0 c :=   match c with
            | (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
            | (bCmd.bSeq c1 c2) :=
                let i1 := (cEval i0 c1) in (cEval i1 c2)
            end

def myFirstProg := bCmd.bAssm (bvar.mk 0) (bExpr.BLit ff)

def newEnv := cEval init_benv myFirstProg

#eval newEnv (bvar.mk 0)

[Mario Carneiro]

The way you have written cEval makes me think you learned this from coq style. In lean you just write a definition with multiple cases

[Mario Carneiro]

def cEval : benv → bCmd → benv
| i0 (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
| i0 (bCmd.bSeq c1 c2) := cEval (cEval i0 c1) c2

[Mario Carneiro]

@Kevin Sullivan

[Mario Carneiro]

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

[Kevin Sullivan]

Mario Carneiro said:

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

Thanks, yeah. It is Coq-style but it seemed like a wrong response nonetheless, which is what prompted me to ask. Not sure if I should file an issue?

[Kevin Sullivan]

Kevin Sullivan said:

Mario Carneiro said:

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

Thanks, yeah. It is Coq-style but it seemed like a wrong response nonetheless, which is what prompted me to ask. Not sure if I should file an issue?

Lean Prover repo has been archived. Doesn't seem I can post an issue. I'm probably missing something, but maybe not. Let me know. Thanks.

[Yakov Pechersky]

The community version of Lean is at https://github.com/leanprover-community/lean

[Kevin Sullivan]

Yakov Pechersky said:

The community version of Lean is at https://github.com/leanprover-community/lean

Ah, yes, thanks.