Syntax Tricks in Lean 4

Meet.lean

import Lean.Meta.Reduce
import Lean.Parser.Term
import Lean.Expr
import Lean.Elab
open Lean

axiom I  : Type
axiom i₀ : I
axiom i₁ : I

axiom meet : I → I → I

open Expr

partial def eval (e : Expr) : MetaM Expr :=
do match (← Meta.reduceAll e) with
| app (app (const ``meet _ _) (const ``i₀ _ _) _) _ _ => return (mkConst ``i₀)
| app (app (const ``meet _ _) _ _) (const ``i₀ _ _) _ => return (mkConst ``i₀)

| app (app (const ``meet _ _) (const ``i₁ _ _) _) e _ => eval e
| app (app (const ``meet _ _) e _) (const ``i₁ _ _) _ => eval e

| app f x _ => return mkApp (← eval f) (← eval x)
| lam .. => Meta.lambdaTelescope e fun xs b => do Meta.mkLambdaFVars (← Array.mapM eval xs) (← eval b)
| forallE .. => Meta.forallTelescope e fun xs b => do Meta.mkForallFVars (← Array.mapM eval xs) (← eval b)
| proj n i s .. => return mkProj n i (← eval s)
| e' => return e'

@[commandParser] def cubicalDef :=
leading_parser "cubical " >> "def " >> Parser.ident >> " : " >>
               Parser.termParser >> " := " >> Parser.termParser

@[commandElab «cubicalDef»] def elabCubicalDef : Elab.Command.CommandElab :=
λ stx => match stx.getArgs with
| #[_, _, ident, _, tstx, _, estx] => do
  let name := Syntax.getId ident
  let τ ← Elab.Command.liftTermElabM name (do
    let t ← Elab.Term.elabTerm tstx none
    Lean.Meta.liftMetaM (eval t >>= Meta.instantiateMVars))

  let ε ← Elab.Command.liftTermElabM name (do
    let e ← Elab.Term.elabTerm estx (some τ)
    Lean.Meta.liftMetaM (Meta.instantiateMVars e))

  addDecl (Declaration.defnDecl {
    name := name, levelParams := [],
    hints := mkReducibilityHintsRegularEx 0,
    safety := DefinitionSafety.safe,
    type := τ, value := ε
  })
| _ => throwError "something went wrong"

cubical def test₁ : ∀ i, Eq (meet i₁ i) i  := λ i => Eq.refl i
cubical def test₂ : ∀ i, Eq (meet i i₁) i  := λ i => Eq.refl i
cubical def test₃ : ∀ i, Eq (meet i₀ i) i₀ := λ i => Eq.refl i₀
cubical def test₄ : ∀ i, Eq (meet i i₀) i₀ := λ i => Eq.refl i₀