feat: Elementarized tactics with motives, congruence, and absurdity #72

aniva · 2024-04-13T19:43:04-07:00

aniva commented

2024-04-13 19:43:04 -07:00

This implements a one-step solution for the problem in aniva/Trillium#124.

The motivated apply tactic places all used motives in let motive: Motive := _ bindings with the necessary metavariables. This resolves the problem of non-elementarity of applying motive-based symbols.
The noConfuse tactic uses .noConfusion on an existing impossible equality
The congruence tactics (congruenceArg, congruenceFun, and congruence) apply the congrArg, congrFun, and congr lemmata via a conduit type.
Improves metavariable printing handling of delay assigned metavariables. An extra (:subst ...) sexp represents a delayed assigned mvar whose pending mvar is not assigned in any way. Also starts the gradual shift from sexp to raw Expr objects in the FFI, but sexp's will remain for the foreseeable future.

This implements a one-step solution for the problem in https://git.leni.sh/aniva/Trillium/pulls/124. 1. The motivated apply tactic places all used motives in `let motive: Motive := _` bindings with the necessary metavariables. This resolves the problem of non-elementarity of applying motive-based symbols. 2. The `noConfuse` tactic uses `.noConfusion` on an existing impossible equality 3. The congruence tactics (`congruenceArg`, `congruenceFun`, and `congruence`) apply the `congrArg`, `congrFun`, and `congr` lemmata via a conduit type. 4. Improves metavariable printing handling of delay assigned metavariables. An extra `(:subst ...)` sexp represents a delayed assigned mvar whose pending mvar is not assigned in any way. Also starts the gradual shift from sexp to raw `Expr` objects in the FFI, but sexp's will remain for the foreseeable future.

aniva added the

labels 2024-04-13 19:43:04 -07:00

aniva self-assigned this 2024-04-13 19:43:04 -07:00

aniva added 1 commit 2024-04-13 19:43:04 -07:00

b954f12526

refactor: Move all tactic operations to the bottom

aniva added 1 commit 2024-04-14 15:41:15 -07:00

75b4648ba9

feat: mapply stub

aniva added 1 commit 2024-04-15 12:47:19 -07:00

dbd54f7679

feat: Implement the mapply tactic

aniva added 1 commit 2024-04-15 12:56:40 -07:00

7aa7e6d7e9

feat: Library interface for mapply

aniva commented

2024-04-15 13:03:31 -07:00

Waiting for this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Elaborator.20and.20.40/near/433364676

aniva commented

2024-04-16 15:37:57 -07:00

MWE to reproduce the implicit lambda problem:

import Lean
open Lean

def parseTerm (s: String): CoreM Syntax := do
  match Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := s)
    (fileName := "<stdin>") with
  | .ok s => return s
  | .error e => throwError e

def termElabM : Elab.TermElabM Unit := do
  let expr := "Nat.brecOn"
  let expr  ← Elab.Term.elabTerm (← parseTerm expr) (expectedType? := .none)
  let type ← Meta.inferType expr
  IO.println s!"{← Meta.ppExpr expr}"
  IO.println s!"  : {← Meta.ppExpr type}"

  let unassigned ← Elab.Term.collectUnassignedMVars type
  for mvarId in unassigned do
    let mvarType ← Meta.inferType mvarId
    IO.println s!"{← Meta.ppExpr mvarId}: {← Meta.ppExpr mvarType}"

def main : IO Unit := do
  let options: Options := {}
  let options := options.setNat `pp.deepTerms.threshold 100
  let options := options.setNat `pp.proofs.threshold 100
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  let termElabContext: Elab.Term.Context :=  {
    heedElabAsElim := false,
    declName? := `sandbox,
    errToSorry := false
  }
  let coreM := Meta.MetaM.run' <| Elab.Term.TermElabM.run' (ctx := termElabContext) termElabM
  let coreContext: Lean.Core.Context := {
    options,
    currNamespace := `Example
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0] }
  }
  match ← (coreM.run' coreContext { env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok _ => return ()

MWE to reproduce the implicit lambda problem: ```lean import Lean open Lean def parseTerm (s: String): CoreM Syntax := do match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) (fileName := "<stdin>") with | .ok s => return s | .error e => throwError e def termElabM : Elab.TermElabM Unit := do let expr := "Nat.brecOn" let expr ← Elab.Term.elabTerm (← parseTerm expr) (expectedType? := .none) let type ← Meta.inferType expr IO.println s!"{← Meta.ppExpr expr}" IO.println s!" : {← Meta.ppExpr type}" let unassigned ← Elab.Term.collectUnassignedMVars type for mvarId in unassigned do let mvarType ← Meta.inferType mvarId IO.println s!"{← Meta.ppExpr mvarId}: {← Meta.ppExpr mvarType}" def main : IO Unit := do let options: Options := {} let options := options.setNat `pp.deepTerms.threshold 100 let options := options.setNat `pp.proofs.threshold 100 let env: Environment ← importModules (imports := #[`Init]) (opts := {}) (trustLevel := 1) let termElabContext: Elab.Term.Context := { heedElabAsElim := false, declName? := `sandbox, errToSorry := false } let coreM := Meta.MetaM.run' <| Elab.Term.TermElabM.run' (ctx := termElabContext) termElabM let coreContext: Lean.Core.Context := { options, currNamespace := `Example openDecls := [], -- No 'open' directives needed fileName := "<stdin>", fileMap := { source := "", positions := #[0] } } match ← (coreM.run' coreContext { env }).toBaseIO with | .error exception => IO.println s!"{← exception.toMessageData.toString}" | .ok _ => return () ```

aniva added 2 commits 2024-04-19 12:37:43 -07:00

fec13ddb51

chore: Code cleanup

398b1c39ed

refactor: Common tactic execute function

aniva added 1 commit 2024-04-20 13:10:15 -07:00

4a92e655f6

test: Tactic test stub

aniva added 1 commit 2024-04-22 00:12:08 -07:00

3812aa56ec

feat: Phantom var in mapply

aniva commented

2024-04-22 00:25:03 -07:00

I think the metavariables generated by mapply don't have to be syntheticOpaque, since no isDefEq operation is contained in it, but we'll see if this is a problem.

I think the metavariables generated by `mapply` don't have to be `syntheticOpaque`, since no `isDefEq` operation is contained in it, but we'll see if this is a problem.

aniva added 2 commits 2024-04-22 10:02:28 -07:00

feff62a3c5

fix: Remove determination of major

6ffb227cd6

feat: Conduit modus ponens

aniva added 1 commit 2024-05-04 23:37:15 -07:00

4cff6677d2

chore: Lean version bump to 4.8.0-rc1

aniva added 1 commit 2024-05-05 00:43:52 -07:00

63417ef179

fix: Motive extra arguments not instiantiated

aniva added 1 commit 2024-05-05 10:37:04 -07:00

1e1995255a

test: mapply captures dependent types

aniva added 2 commits 2024-05-05 13:26:03 -07:00

cf1289f159

feat: NoConfuse tactic

2937675044

feat: Library interface for calling no_confuse

aniva added 1 commit 2024-05-05 13:26:56 -07:00

679871cbc6

fix: NoConfuse arg name

aniva added 1 commit 2024-05-06 22:20:46 -07:00

aa106f7591

feat: Do not filter mvars from mapply

aniva added 1 commit 2024-05-06 22:39:34 -07:00

69ec70ffbe

feat: Do not explicitly show delay assigned mvar

aniva added 1 commit 2024-05-08 12:41:44 -07:00

66a5dfcf3c

feat: Diagnostics command for FFI users

aniva added 1 commit 2024-05-08 20:51:50 -07:00

e58dbc66a9

fix: Consistent naming in library functions

aniva added 1 commit 2024-05-09 14:03:07 -07:00

0b88f6708e

test: Delayed mvar assignment for mapply

aniva commented

2024-05-10 14:38:38 -07:00

This breaks current metavariable resolution schema because the motive variable is delay assigned. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Force.20instantiate.20delay.20assigned.20metavariable/near/438042381

import Lean

open Lean Meta

/--
Instantiate metavariables, including partially assigned delayed assignment metavariables.
-/
def semiInstantiateMVars (e : Expr) : MetaM Expr := do
  Meta.transform (← instantiateMVars e)
    (pre := fun e => e.withApp fun f args => do
      if let .mvar mvarId := f then
        if let some decl ← getDelayedMVarAssignment? mvarId then
          if args.size ≥ decl.fvars.size then
            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
            if !pending.isMVar then
              return .visit <| (← mkLambdaFVars decl.fvars pending).beta args
      return .continue)

elab "check " t:term : tactic => Elab.Tactic.withMainContext do
  let mut e ← Elab.Tactic.elabTerm t none
  if e.isFVar then
    if let some val ← e.fvarId!.getValue? then
      e := val
  logInfo m!"{e}"

elab "check' " t:term : tactic => Elab.Tactic.withMainContext do
  let mut e ← Elab.Tactic.elabTerm t none
  if e.isFVar then
    if let some val ← e.fvarId!.getValue? then
      e := val
  let e' ← semiInstantiateMVars e
  logInfo m!"{e'}"

example : True := by
  let h : ∀ x y : Nat, 1 + x = 1 + y := fun x y => ?foo
  case' foo => refine congrArg _ ?_
  rotate_left
  check h   -- fun x y ↦ ?m.4924 x y
  check' h  -- fun x y ↦ congrArg (HAdd.hAdd 1) (?m.4955 x y)
  trivial

This breaks current metavariable resolution schema because the motive variable is delay assigned. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Force.20instantiate.20delay.20assigned.20metavariable/near/438042381 ```lean import Lean open Lean Meta /-- Instantiate metavariables, including partially assigned delayed assignment metavariables. -/ def semiInstantiateMVars (e : Expr) : MetaM Expr := do Meta.transform (← instantiateMVars e) (pre := fun e => e.withApp fun f args => do if let .mvar mvarId := f then if let some decl ← getDelayedMVarAssignment? mvarId then if args.size ≥ decl.fvars.size then let pending ← instantiateMVars (.mvar decl.mvarIdPending) if !pending.isMVar then return .visit <| (← mkLambdaFVars decl.fvars pending).beta args return .continue) elab "check " t:term : tactic => Elab.Tactic.withMainContext do let mut e ← Elab.Tactic.elabTerm t none if e.isFVar then if let some val ← e.fvarId!.getValue? then e := val logInfo m!"{e}" elab "check' " t:term : tactic => Elab.Tactic.withMainContext do let mut e ← Elab.Tactic.elabTerm t none if e.isFVar then if let some val ← e.fvarId!.getValue? then e := val let e' ← semiInstantiateMVars e logInfo m!"{e'}" example : True := by let h : ∀ x y : Nat, 1 + x = 1 + y := fun x y => ?foo case' foo => refine congrArg _ ?_ rotate_left check h -- fun x y ↦ ?m.4924 x y check' h -- fun x y ↦ congrArg (HAdd.hAdd 1) (?m.4955 x y) trivial ```

aniva changed title from ~~feat: Motivated apply (mapply) tactic~~ to feat: Elementarized tactics with motives, congruence, and absurdity

2024-05-10 14:39:09 -07:00

aniva commented

2024-05-11 15:37:45 -07:00

There are currently 3 solutions to this issue:

Add value dependency to the current handling of traces
Use a partial delaboration function like above
When producing sexp, use a similar method as https://github.com/leanprover/lean4/pull/3494/files#diff-ed9bb7a43b23e8712218804e75e7080ce53c49c0449d322fb172092eca9331e0. This feature may be merged into mainline Lean.

There are currently 3 solutions to this issue: 1. Add value dependency to the current handling of traces 2. Use a partial delaboration function like above 3. When producing sexp, use a similar method as https://github.com/leanprover/lean4/pull/3494/files#diff-ed9bb7a43b23e8712218804e75e7080ce53c49c0449d322fb172092eca9331e0. This feature may be merged into mainline Lean.

aniva added 2 commits 2024-05-12 22:33:53 -07:00

03ecb6cf19

feat: Partial instantiate metavariables

c04b363de7

feat: Handle delay assigned mvars

aniva commented

2024-05-13 12:42:49 -07:00

I've decided to go with method (3). This requires a new abstraction in the sexp layer. Maybe the sexp should just be removed.

aniva added 1 commit 2024-05-13 13:49:35 -07:00

f813d4a8dd

refactor: Delayed mvar instantiation function

aniva added 1 commit 2024-05-13 13:59:05 -07:00