Prove Expr.typeCheck_complete for full language with Var, Lam, App

[Copilot]

• Explore and understand the codebase and the issue
• Restore Vec type in Tibi/Util.lean
• Restore full intrinsically-typed Expr ctx ty (with Ty, Locals, Var, Lam, App) in Tibi/Syntax/Expr.lean
• Create Tibi/Semantics/Env.lean with Env environment type
• Update Tibi/Semantics.lean to use indexed Expr ctx ty and ty.interp
• Restore full HasType and typeCheck (for Var, Lam, App) in Tibi/Typing.lean
• Update Tibi/Interpreter.lean for new indexed Expr ctx ty
• Update Tibi/Compiler.lean for new indexed Expr ctx ty; add -- TODO to unimplemented cases
• Update Tibi/Parser.lean to return Expr .nil .int
• Update Tibi/Top.lean for new types
• Update README.md syntax section to include Var/Lam/App (marked as not yet implemented in parser)
• Update Tibi/Props/Typing.lean
• Update Tibi/Props/Compiler.lean
• CI passing

Original prompt

---

This section details on the original issue you should resolve

<issue_title>prove Expr.typeCheck_complete</issue_title>
<issue_description>

tibi/Tibi/Props/Typing.lean

Line 35 in 58ea612

-- TODO prove Expr.typeCheck_complete

namespace Tibi

theorem HasType.det : HasType e t₁ → HasType e t₂ → t₁ = t₂
| .Int64 ..,  .Int64 ..    => rfl
| .Var,       .Var         => rfl
| .Lam h,     .Lam h'      => by rw [h.det h']
| .App h₁ h₂, .App h₁' h₂' => h₂.det h₂' ▸ h₁.det h₁' |> Typ.Fn.inj |>.right

/--
Reference: [A Certified Type Checker \- Lean Documentation Overview](https://lean-lang.org/lean4/doc/examples/tc.lean.html)
-/
theorem Expr.typeCheck_correct {e : Expr ctx ty}
  (ht : HasType e t)
  (h : e.typeCheck ≠ .unknown)
: e.typeCheck = .found t ht
:= by
  revert h
  match e.typeCheck with
  | .found ty' h₁' => intro ; have := ht.det h₁' ; subst this ; rfl
  | .unknown       => intros; contradiction
/-
Try this: (match e.typeCheck with
  | Maybe.found ty' h₁' => fun h =>
    let_fun this := HasType.det ht h₁';
    Eq.ndrec (motive := fun ty' =>
      ∀ (h₁' : HasType e ty'), Maybe.found ty' h₁' ≠ Maybe.unknown → Maybe.found ty' h₁' = Maybe.found t ht)
      (fun h₁' h => Eq.refl (Maybe.found t h₁')) this h₁' h
  | Maybe.unknown => fun h => absurd (Eq.refl Maybe.unknown) h)
  h
-/

-- TODO prove Expr.typeCheck_complete
/-
theorem Expr.typeCheck_complete {e : Expr ctx ty}
: e.typeCheck = .unknown → ¬HasType e t
:= by
  induction e with simp [Expr.typeCheck]
  | Const n =>
      intro h ht
      match ht with
      | .Int64 hLt hGe =>
          have := h hGe hLt
          contradiction
  | Lam e ih =>
      match h : e.typeCheck with
      | .found t' ht' => intro ; contradiction
      | .unknown =>
          have : ¬HasType e t := ih h
          intro _ ht'
          match ht' with
          | .Lam h' =>
              sorry
  | App e₁ e₂ ih₁ ih₂ => sorry
-/

-- TODO prove : Decidable (HasType e t)
/-
instance (e : Expr ctx ty) (t : Typ) : Decidable (HasType e t) :=
  match h : e.typeCheck with
  | .found t' ht' =>

```</issue_description>

## Comments on the Issue (you are @copilot in this section)

<comments>
</comments>

• Fixes prove Expr.typeCheck_complete #6

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

[nahcnuj]

@copilot
Fix failure

[Copilot]

@copilot
Fix failure

Fixed in 85630ab. There were three CI errors:

1. Props/Typing.lean — Lam case: simp only [Expr.typeCheck, ih] was used in term mode (no by), causing "unknown identifier 'simp'". Added by to switch to tactic mode.

2. Props/Typing.lean — App case: simp only [Expr.typeCheck, ihf, ihv] was evaluating dom = dom to True via Lean's built-in DecidableEq evaluation (even with only), so dif_pos rfl which proves dite (dom = dom) ... mismatched the goal dite True .... Changed to full simp [Expr.typeCheck, ihf, ihv] which handles the True branch and proof-term equality (rfl ▸ hv = hv) automatically.

3. Props/Compiler.lean: v had polymorphic type ty.interp but Wasm.Num.Int64 requires Tibi.Int64 = Wasm.Value.Int64. Added {e : Expr ctx .int} explicit parameter so v : .int.interp = Tibi.Int64. Also removed the impossible .Var pattern (can't have Var x : Expr ctx .int since Var x : Expr ctx (.cls ty ty)).

[nahcnuj]

@copilot
Fix failure

[Copilot]

@copilot
Fix failure

Fixed in 3ed9b48. The previous fix placed {e : Expr ctx .int} as a before-colon parameter, which meant equation-style patterns had no way to bind n from .Const n. The fix moves {e : Expr ctx .int} into the → type chain (matching the original {e : Expr} → style), so the pattern .Const n explicitly binds n. Also added the matching e position to the .App case pattern.

[nahcnuj]

@copilot
Fix failure

[Copilot]

@copilot
Fix failure

Fixed in e8938c0. There were two errors in Props/Compiler.lean:

1. Const case (line 12, unsolved goals with hLt✝/hGe✝): The previous code bound hLt, hGe from HasType.Int64 to build the expected instrs, but v was Int64.mk ⟨n, hLt✝, hGe✝⟩ from Eval.Const — a different pair of proof terms. Fix: bind hLt, hGe from Eval.Const instead (using _ for the HasType proofs), so both v and the constructed instrs use the same proofs.

2. App case (line 19, metavariable in v's type): Pattern .App _ _, .App _ _, .App _ _ tried to deconstruct Eval.App, leaving dom as a metavariable ?m in v : (?m.cls Ty.int).interp. Fix: use _ for both the HasType and Eval arguments — only hc is needed to derive the contradiction via simp [Expr.compile].

[nahcnuj]

@copilot
rebase main and then fix failure

[Copilot]

@copilot
rebase main and then fix failure

Fixed in aba9c0c. The CI failure was Props/Compiler.lean:13: don't know how to synthesize implicit argument 'ctx' for (Expr.Const n).compile — since n : Int alone gives Lean no way to infer ctx. Adding an explicit type annotation (Expr.Const n : Expr ctx .int).compile fixes the elaboration.

Regarding the rebase: I'm not able to perform git rebase (force push isn't available in this environment), so I applied the fix directly on the current branch.

[Copilot]

Pull request overview

This PR restores an intrinsically-typed expression language (Expr ctx ty) with variables and functions, threads indices through typing/semantics/interpreter/compiler, and updates the typing proofs to include typeCheck_complete for the expanded language.

Changes:

• Reintroduced Vec, added Env, and restored indexed syntax (Ty, Locals, Expr) with Var/Lam/App.
• Updated Typing, Semantics, Interpreter, Compiler, Parser, and Top to use the new indexed Expr.
• Expanded typing metatheory proofs (typeCheck_correct, typeCheck_complete, decidability, and type_safe) for the new constructors.

Reviewed changes

Copilot reviewed 11 out of 11 changed files in this pull request and generated 9 comments.

Show a summary per file

File	Description
Tibi/Util.lean	Adds Vec to support indexed contexts.
Tibi/Syntax/Expr.lean	Restores indexed Ty, Locals, and Expr with Var/Lam/App.
Tibi/Semantics/Env.lean	Introduces Env and lookup for Locals.
Tibi/Semantics.lean	Updates Eval relation to indexed expressions and adds Var/Lam/App cases.
Tibi/Typing.lean	Restores Typ, HasType, and Expr.typeCheck for the full syntax.
Tibi/Interpreter.lean	Updates evaluator to accept an environment and indexed expressions.
Tibi/Compiler.lean	Updates compiler signature to indexed expressions; adds Unimplemented error cases.
Tibi/Parser.lean	Narrows parser result type to Expr .nil .int.
Tibi/Top.lean	Updates REPL/run pipeline to use new evaluator/compiler signatures.
Tibi/Props/Typing.lean	Updates typing proofs (correctness/completeness/decidability/type safety) for new constructors.
Tibi/Props/Compiler.lean	Adjusts compiler correctness proof to the new indexed Expr.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The new type_safe cases for .Lam and .App are proved by ⟨_, rfl⟩, which is only possible because the current Eval.Lam/Eval.App constructors always produce an .ok result and don’t model the real failure modes of application/body evaluation. Once Eval is fixed to depend on Env/argument evaluation, these cases will likely need nontrivial proofs that propagate the IHs rather than finishing by reflexivity.

Suggested change

	| .Lam _, .Lam .. => ⟨_, rfl⟩
	| .App _ _, .App .. => ⟨_, rfl⟩
	| .Lam _, hEval =>
	-- Use the structure of the evaluation derivation for lambdas
	cases hEval with
	| Lam .. => exact ⟨_, rfl⟩
	| .App _ _, hEval =>
	-- Use the structure of the evaluation derivation for applications
	cases hEval with
	| App .. => exact ⟨_, rfl⟩

[Copilot]

HasType.Lam hard-codes the parameter type as Typ.Var 0, but this repository already has Ty.toTyp; using .Var 0 makes lambda types unrelated to the actual dom index on Expr (.fn dom ran) and effectively prevents well-typed applications of lambdas (since no expression can synthesize Typ.Var 0). Define the lambda type using the dom from the expression indices (e.g., Typ.Fn dom.toTyp t) so Lam/App interact consistently.

[Copilot]

Eval is not parameterized by an environment, but the Var constructor introduces an env : Env ctx anyway. This makes Eval (.Var x) ... provable for arbitrary environments and loses the intended dependence on runtime state, which will undermine determinism and later safety/correctness proofs. Consider changing the relation to Eval (env : Env ctx) (e : Expr ctx ty) : Except EvalError ty.interp → Prop (or similar) and thread env through all constructors.

Suggested change

	inductive Eval : (Expr ctx ty) → Except EvalError ty.interp → Prop
	| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size)
	: Eval (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
	| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)
	: Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
	| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size)
	: Eval (.Const n) (.error <| .OutOfBounds_Int64 n)
	| Var (x : Locals k ctx ty) (env : Env ctx)
	: Eval (.Var x) (.ok <| env.lookup x)
	| Lam (d : Eval e (.ok v))
	: Eval (.Lam e) (.ok <| fun _ => v)
	| App (d₁ : Eval e₁ (.ok v₁)) (d₂ : Eval e₂ (.ok v₂))
	: Eval (.App (.Lam e₁) e₂) (.ok <| v₁)
	inductive Eval (env : Env ctx) : (Expr ctx ty) → Except EvalError ty.interp → Prop
	| Const {n : Int} (hLt : n < Int64.size) (hGe : n >= -Int64.size)
	: Eval env (.Const n) (.ok <| Int64.mk ⟨n, hLt, hGe⟩)
	| ConstErr_lt {n : Int} (h : ¬ n < Int64.size)
	: Eval env (.Const n) (.error <| .OutOfBounds_Int64 n)
	| ConstErr_ge {n : Int} (h : ¬ n >= -Int64.size)
	: Eval env (.Const n) (.error <| .OutOfBounds_Int64 n)
	| Var (x : Locals k ctx ty)
	: Eval env (.Var x) (.ok <| env.lookup x)
	| Lam (d : Eval env e (.ok v))
	: Eval env (.Lam e) (.ok <| fun _ => v)
	| App (d₁ : Eval env e₁ (.ok v₁)) (d₂ : Eval env e₂ (.ok v₂))
	: Eval env (.App (.Lam e₁) e₂) (.ok <| v₁)

[Copilot]

The Lam/App rules currently ignore the argument: Lam returns fun _ => v after evaluating the body once, and App returns v₁ without relating it to the argument value (it even requires d₂ but never uses v₂). This makes function semantics incorrect (every lambda becomes a constant function) and makes App unrelated to substitution/application. Rework these constructors to model closures/application (likely using an explicit Env parameter and evaluating the body under an extended environment for the given argument).

Suggested change

	| Lam (d : Eval e (.ok v))
	: Eval (.Lam e) (.ok <| fun _ => v)
	| App (d₁ : Eval e₁ (.ok v₁)) (d₂ : Eval e₂ (.ok v₂))
	: Eval (.App (.Lam e₁) e₂) (.ok <| v₁)
	| Lam {e v} (d : ∀ a, Eval e (.ok (v a)))
	: Eval (.Lam e) (.ok v)
	| App (d₁ : Eval e₁ (.ok v₁)) (d₂ : Eval e₂ (.ok v₂))
	: Eval (.App (.Lam e₁) e₂) (.ok <| v₁ v₂)

[Copilot]

Env.lean redefines the global :: notation (previously Vec.cons) to mean Env.cons. Since notation isn’t type-directed, importing Tibi.Semantics.Env will overwrite Vec’s :: and can break/obscure code that constructs Vec contexts elsewhere. Consider using a different notation for environments (or a scoped notation) to avoid clobbering Vec’s constructor syntax.

Suggested change

	infix:67 " :: " => Env.cons
	scoped infixr:67 " :: " => Env.cons

[Copilot]

Expr.typeCheck’s Lam branch returns Fn (Var 0) t, which does not reflect the lambda’s indexed domain type (dom) and will not line up with Ty.toTyp/App’s argument-type equality check. This will cause typeCheck to return .unknown for applications that should type-check. Use the domain dom from the expression indices when constructing the function type.

[Copilot]

The Lam evaluation path computes v by evaluating the body once with the specific input x, then returns the constant function fun _ => v. That makes lambda values independent of the argument (i.e., not a real closure). If Ty.interp (fn a b) is a → b, Lam should return a function that (for each argument) evaluates the body under the extended environment for that argument.

Suggested change

	| _, .Lam e', x =>
	match e'.eval (x :: env) x with
	| .found (.ok v) h => .found (.ok <| fun _ => v) <| .Lam h
	| .unknown => .unknown
	| _, .Lam _ , _ =>
	.unknown

[Copilot]

App evaluation is currently hard-coded to the very specific shape (.int, App (dom := .int) (.Lam e₁) e₂, _) and falls back to .unknown for other well-typed applications (e.g. non-int domains or when the function expression is not syntactically a Lam). Since Expr.App is part of the core language and Ty.interp (fn a b) is a function type, eval should evaluate the function expression to a value and apply it uniformly for all domains/results, not only this special case.

[Copilot]

This branch ends with simp [Expr.compile] at hc, which only rewrites the hypothesis hc and does not close the goal. If the intent is to discharge the case by contradiction (since Expr.compile is .error on App), you likely need to derive False from hc and then eliminate it (e.g., by cases hc after simplification).

Suggested change

	| .App _ _, _, _, hc => by simp [Expr.compile] at hc
	| .App _ _, _, _, hc => by
	simp [Expr.compile] at hc
	cases hc

[nahcnuj]

SyntaxとしてはVar, Lam, Appまで受け付けるようにした、という理解で良いですか？
READMEに構文定義を書いているのでそちらもアップデートしてください。

[Copilot]

SyntaxとしてはVar, Lam, Appまで受け付けるようにした、という理解で良いですか？
READMEに構文定義を書いているのでそちらもアップデートしてください...

Yes, that understanding is correct — Expr ctx ty now includes Var, Lam, and App as abstract syntax constructors. The parser (Parser.lean) currently only handles integer literals; support for variables, lambdas, and applications is not yet implemented there.

Updated the README syntax section in 329808f to include all three constructs, each marked with (* ... -- not yet implemented in parser *).