summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress/Progress.lean
blob: ba63f09d967282d67aba9b9aa84e49115fcd1f91 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
import Lean
import Base.Arith
import Base.Progress.Base
import Base.Primitives -- TODO: remove?

namespace Progress

open Lean Elab Term Meta Tactic
open Utils

-- TODO: the scalar types annoyingly often get reduced when we use the progress
-- tactic. We should find a way of controling reduction. For now we use rewriting
-- lemmas to make sure the goal remains clean, but this complexifies proof terms.
-- It seems there used to be a `fold` tactic.
theorem scalar_isize_eq : Primitives.Scalar .Isize = Primitives.Isize := by rfl
theorem scalar_i8_eq    : Primitives.Scalar .I8 = Primitives.I8 := by rfl
theorem scalar_i16_eq   : Primitives.Scalar .I16 = Primitives.I16 := by rfl
theorem scalar_i32_eq   : Primitives.Scalar .I32 = Primitives.I32 := by rfl
theorem scalar_i64_eq   : Primitives.Scalar .I64 = Primitives.I64 := by rfl
theorem scalar_i128_eq  : Primitives.Scalar .I128 = Primitives.I128 := by rfl
theorem scalar_usize_eq : Primitives.Scalar .Usize = Primitives.Usize := by rfl
theorem scalar_u8_eq    : Primitives.Scalar .U8 = Primitives.U8 := by rfl
theorem scalar_u16_eq   : Primitives.Scalar .U16 = Primitives.U16 := by rfl
theorem scalar_u32_eq   : Primitives.Scalar .U32 = Primitives.U32 := by rfl
theorem scalar_u64_eq   : Primitives.Scalar .U64 = Primitives.U64 := by rfl
theorem scalar_u128_eq  : Primitives.Scalar .U128 = Primitives.U128 := by rfl
def scalar_eqs := [
  ``scalar_isize_eq, ``scalar_i8_eq, ``scalar_i16_eq, ``scalar_i32_eq, ``scalar_i64_eq, ``scalar_i128_eq,
  ``scalar_usize_eq, ``scalar_u8_eq, ``scalar_u16_eq, ``scalar_u32_eq, ``scalar_u64_eq, ``scalar_u128_eq
]

inductive TheoremOrLocal where
| Theorem (thName : Name)
| Local (asm : LocalDecl)

instance : ToMessageData TheoremOrLocal where
  toMessageData := λ x => match x with | .Theorem thName => m!"{thName}" | .Local asm => m!"{asm.userName}"

/- Type to propagate the errors of `progressWith`.
   We need this because we use the exceptions to backtrack, when trying to
   use the assumptions for instance. When there is actually an error we want
   to propagate to the user, we return it. -/
inductive ProgressError
| Ok
| Error (msg : MessageData)
deriving Inhabited

def progressWith (fExpr : Expr) (th : TheoremOrLocal)
  (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)
  (asmTac : TacticM Unit) : TacticM ProgressError := do
  /- Apply the theorem
     We try to match the theorem with the goal
     In order to do so, we introduce meta-variables for all the parameters
     (i.e., quantified variables and assumpions), and unify those with the goal.
     Remark: we do not introduce meta-variables for the quantified variables
     which don't appear in the function arguments (we want to let them
     quantified).
     We also make sure that all the meta variables which appear in the
     function arguments have been instantiated
   -/
  let env  getEnv
  let thTy  do
    match th with
    | .Theorem thName =>
      let thDecl := env.constants.find! thName
      -- We have to introduce fresh meta-variables for the universes already
      let ul : List (Name × Level) 
        thDecl.levelParams.mapM (λ x => do pure (x,  mkFreshLevelMVar))
      let ulMap : HashMap Name Level := HashMap.ofList ul
      let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x)
      pure thTy
    | .Local asmDecl => pure asmDecl.type
  trace[Progress] "Looked up theorem/assumption type: {thTy}"
  -- TODO: the tactic fails if we uncomment withNewMCtxDepth
  -- withNewMCtxDepth do
  let (mvars, binders, thExBody)  forallMetaTelescope thTy
  trace[Progress] "After stripping foralls: {thExBody}"
  -- Introduce the existentially quantified variables and the post-condition
  -- in the context
  let thBody 
    existsTelescope thExBody.consumeMData fun _evars thBody => do
    trace[Progress] "After stripping existentials: {thBody}"
    let (thBody, _)  optSplitConj thBody
    trace[Progress] "After splitting the conjunction: {thBody}"
    let (thBody, _)  destEq thBody
    trace[Progress] "After splitting equality: {thBody}"
    -- There shouldn't be any existential variables in thBody
    pure thBody.consumeMData
  -- Match the body with the target
  trace[Progress] "Matching:\n- body:\n{thBody}\n- target:\n{fExpr}"
  let ok  isDefEq thBody fExpr
  if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}"
  let mgoal  Tactic.getMainGoal
  postprocessAppMVars `progress mgoal mvars binders true true
  Term.synthesizeSyntheticMVarsNoPostponing
  let thBody  instantiateMVars thBody
  trace[Progress] "thBody (after instantiation): {thBody}"
  -- Add the instantiated theorem to the assumptions (we apply it on the metavariables).
  let th  do
    match th with
    | .Theorem thName => mkAppOptM thName (mvars.map some)
    | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
  let asmName  do match keep with | none => mkFreshAnonPropUserName | some n => do pure n
  let thTy  inferType th
  let thAsm  Utils.addDeclTac asmName th thTy (asLet := false)
  withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
  let ngoal  getMainGoal
  trace[Progress] "current goal: {ngoal}"
  trace[Progress] "current goal: {← ngoal.isAssigned}"
  -- The assumption should be of the shape:
  -- `∃ x1 ... xn, f args = ... ∧ ...`
  -- We introduce the existentially quantified variables and split the top-most
  -- conjunction if there is one. We use the provided `ids` list to name the
  -- introduced variables.
  let res  splitAllExistsTac thAsm ids.toList fun h ids => do
    -- Split the conjunctions.
    -- For the conjunctions, we split according once to separate the equality `f ... = .ret ...`
    -- from the postcondition, if there is, then continue to split the postcondition if there
    -- are remaining ids.
    let splitEqAndPost (k : Expr  Option Expr  List (Option Name)  TacticM ProgressError) : TacticM ProgressError := do
      if  isConj ( inferType h) then do
        let hName := ( h.fvarId!.getDecl).userName
        let (optIds, ids)  do
          match ids with
          | [] => do pure (some (hName,  mkFreshAnonPropUserName), [])
          | none :: ids => do pure (some (hName,  mkFreshAnonPropUserName), ids)
          | some id :: ids => do pure (some (hName, id), ids)
        splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids)
      else k h none ids
    -- Simplify the target by using the equality and some monad simplifications,
    -- then continue splitting the post-condition
    splitEqAndPost fun hEq hPost ids => do
    trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
    tryTac (
      simpAt true []
             [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
             [hEq.fvarId!] (.targets #[] true))
    -- TODO: remove this (some types get unfolded too much: we "fold" them back)
    tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
    -- Clear the equality, unless the user requests not to do so
    let mgoal  do
      if keep.isSome then getMainGoal
      else do
        let mgoal  getMainGoal
        mgoal.tryClearMany #[hEq.fvarId!]
    setGoals (mgoal :: ( getUnsolvedGoals))
    trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}"
    -- Continue splitting following the post following the user's instructions
    match hPost with
    | none =>
      -- Sanity check
      if ¬ ids.isEmpty then
        return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
      else return .Ok
    | some hPost => do
      let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids0 : List (Option Name)) : TacticM ProgressError := do
        match ids0 with
        | [] =>
          /- We used all the user provided ids.
             Split the remaining conjunctions by using fresh ids if the user
             instructed to fully split the post-condition, otherwise stop -/
          if splitPost then
            splitFullConjTac true hPost (λ _ => pure .Ok)
          else pure .Ok
        | nid :: ids => do
          trace[Progress] "Splitting post: {← inferType hPost}"
          -- Split
          let nid  do
            match nid with
            | none => mkFreshAnonPropUserName
            | some nid => pure nid
          trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
          if  isConj ( inferType hPost) then
            splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
          else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
      let curPostId := ( hPost.fvarId!.getDecl).userName
      splitPostWithIds curPostId hPost ids
  match res with
  | .Error _ => return res -- Can we get there? We're using "return"
  | .Ok =>
    -- Update the set of goals
    let curGoals  getUnsolvedGoals
    let newGoals := mvars.map Expr.mvarId!
    let newGoals  newGoals.filterM fun mvar => not <$> mvar.isAssigned
    trace[Progress] "new goals: {newGoals}"
    setGoals newGoals.toList
    allGoals asmTac
    let newGoals  getUnsolvedGoals
    setGoals (newGoals ++ curGoals)
    trace[Progress] "progress: replaced the goals"
    --
    pure .Ok

-- Small utility: if `args` is not empty, return the name of the app in the first
-- arg, if it is a const.
def getFirstArgAppName (args : Array Expr) : MetaM (Option Name) := do
  if args.size = 0 then pure none
  else
    (args.get! 0).withApp fun f _ => do
    if f.isConst then pure (some f.constName)
    else pure none

def getFirstArg (args : Array Expr) : Option Expr := do
  if args.size = 0 then none
  else some (args.get! 0)

/- Helper: try to lookup a theorem and apply it, or continue with another tactic
   if it fails -/
def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)
  (asmTac : TacticM Unit) (fExpr : Expr)
  (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
  let res  do
    match th with
    | none =>
      trace[Progress] "Could not find a {kind}"
      pure none
    | some th => do
      trace[Progress] "Lookuped up {kind}: {th}"
      -- Apply the theorem
      let res  do
        try
          let res  progressWith fExpr th keep ids splitPost asmTac
          pure (some res)
        catch _ => none
  match res with
  | some .Ok => return ()
  | some (.Error msg) => throwError msg
  | none => x

-- The array of ids are identifiers to use when introducing fresh variables
def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal)
  (ids : Array (Option Name)) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Unit := do
  withMainContext do
  -- Retrieve the goal
  let mgoal  Tactic.getMainGoal
  let goalTy  mgoal.getType
  trace[Progress] "goal: {goalTy}"
  -- Dive into the goal to lookup the theorem
  let (fExpr, fName, args)  do
    withPSpec goalTy fun desc =>
    -- TODO: check that no quantified variables in the arguments
    pure (desc.fExpr, desc.fName, desc.args)
  trace[Progress] "Function: {fName}"
  -- If the user provided a theorem/assumption: use it.
  -- Otherwise, lookup one.
  match withTh with
  | some th => do
    match  progressWith fExpr th keep ids splitPost asmTac with
    | .Ok => return ()
    | .Error msg => throwError msg
  | none =>
    -- Try all the assumptions one by one and if it fails try to lookup a theorem.
    let ctx  Lean.MonadLCtx.getLCtx
    let decls  ctx.getDecls
    for decl in decls.reverse do
      trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
      let res  do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
      match res with
      | .Ok => return ()
      | .Error msg => throwError msg
    -- It failed: try to lookup a theorem
    -- TODO: use a list of theorems, and try them one by one?
    trace[Progress] "No assumption succeeded: trying to lookup a theorem"
    let pspec  do
      let thName  pspecAttr.find? fName
      pure (thName.map fun th => .Theorem th)
    tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec do
    -- It failed: try to lookup a *class* expr spec theorem (those are more
    -- specific than class spec theorems)
    trace[Progress] "Failed using a pspec theorem: trying to lookup a pspec class expr theorem"
    let pspecClassExpr  do
      match getFirstArg args with
      | none => pure none
      | some arg => do
        trace[Progress] "Using: f:{fName}, arg: {arg}"
        let thName  pspecClassExprAttr.find? fName arg
        pure (thName.map fun th => .Theorem th)
    tryLookupApply keep ids splitPost asmTac fExpr "pspec class expr theorem" pspecClassExpr do
    -- It failed: try to lookup a *class* spec theorem
    trace[Progress] "Failed using a pspec class expr theorem: trying to lookup a pspec class theorem"
    let pspecClass  do
      match  getFirstArgAppName args with
      | none => pure none
      | some argName => do
        trace[Progress] "Using: f: {fName}, arg: {argName}"
        let thName  pspecClassAttr.find? fName argName
        pure (thName.map fun th => .Theorem th)
    tryLookupApply keep ids splitPost asmTac fExpr "pspec class theorem" pspecClass do
    trace[Progress] "Failed using a pspec class theorem: trying to use a recursive assumption"
    -- Try a recursive call - we try the assumptions of kind "auxDecl"
    let ctx  Lean.MonadLCtx.getLCtx
    let decls  ctx.getAllDecls
    let decls := decls.filter (λ decl => match decl.kind with
      | .default | .implDetail => false | .auxDecl => true)
    for decl in decls.reverse do
      trace[Progress] "Trying recursive assumption: {decl.userName} : {decl.type}"
      let res  do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
      match res with
      | .Ok => return ()
      | .Error msg => throwError msg
    -- Nothing worked: failed
    throwError "Progress failed"

syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?

def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
  let args := args.raw
  -- Process the arguments to retrieve the identifiers to use
  trace[Progress] "Progress arguments: {args}"
  let (keepArg, withArg, asArgs) 
    match args.getArgs.toList with
    | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs)
    | _ => throwError "Unexpected: invalid arguments"
  let keep : Option Name  do
    trace[Progress] "Keep arg: {keepArg}"
    let args := keepArg.getArgs
    if args.size > 0 then do
      trace[Progress] "Keep args: {args}"
      let arg := args.get! 1
      trace[Progress] "Keep arg: {arg}"
      if arg.isIdent then pure (some arg.getId)
      else do pure (some ( mkFreshAnonPropUserName))
    else do pure none
  trace[Progress] "Keep: {keep}"
  let withArg  do
    let withArg := withArg.getArgs
    if withArg.size > 0 then
      let id := withArg.get! 1
      trace[Progress] "With arg: {id}"
      -- Attempt to lookup a local declaration
      match ( getLCtx).findFromUserName? id.getId with
      | some decl => do
        trace[Progress] "With arg: local decl"
        pure (some (.Local decl))
      | none => do
        -- Not a local declaration: should be a theorem
        trace[Progress] "With arg: theorem"
        addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
        let cs  resolveGlobalConstWithInfos id
        match cs with
        | [] => throwError "Could not find theorem {id}"
        | id :: _ =>
          pure (some (.Theorem id))
    else pure none
  let ids :=
    let args := asArgs.getArgs
    if args.size > 2 then
      let args := (args.get! 2).getSepArgs
      args.map (λ s => if s.isIdent then some s.getId else none)
    else #[]
  trace[Progress] "User-provided ids: {ids}"
  let splitPost : Bool :=
    let args := asArgs.getArgs
    args.size > 3  (args.get! 3).getArgs.size > 0
  trace[Progress] "Split post: {splitPost}"
  /- For scalarTac we have a fast track: if the goal is not a linear
     arithmetic goal, we skip (note that otherwise, scalarTac would try
     to prove a contradiction) -/
  let scalarTac : TacticM Unit := do
    if  Arith.goalIsLinearInt then
      -- Also: we don't try to split the goal if it is a conjunction
      -- (it shouldn't be)
      Arith.scalarTac false
    else
      throwError "Not a linear arithmetic goal"
  progressAsmsOrLookupTheorem keep withArg ids splitPost (
    withMainContext do
    trace[Progress] "trying to solve assumption: {← getMainGoal}"
    firstTac [assumptionTac, scalarTac])
  trace[Diverge] "Progress done"

elab "progress" args:progressArgs : tactic =>
  evalProgress args

namespace Test
  open Primitives Result

  -- Show the traces
  -- set_option trace.Progress true
  -- set_option pp.rawOnError true

  -- The following commands display the databases of theorems
  -- #eval showStoredPSpec
  -- #eval showStoredPSpecClass
  -- #eval showStoredPSpecExprClass
  open alloc.vec

  example {ty} {x y : Scalar ty}
    (hmin : Scalar.min ty  x.val + y.val)
    (hmax : x.val + y.val  Scalar.max ty) :
     z, x + y = ret z  z.val = x.val + y.val := by
    progress keep _ as  z, h1 .. 
    simp [*, h1]

  example {ty} {x y : Scalar ty}
    (hmin : Scalar.min ty  x.val + y.val)
    (hmax : x.val + y.val  Scalar.max ty) :
     z, x + y = ret z  z.val = x.val + y.val := by
    progress keep h with Scalar.add_spec as  z 
    simp [*, h]

  example {x y : U32}
    (hmax : x.val + y.val  U32.max) :
     z, x + y = ret z  z.val = x.val + y.val := by
    progress keep _ as  z, h1 .. 
    simp [*, h1]

  /- Checking that universe instantiation works: the original spec uses
     `α : Type u` where u is quantified, while here we use `α : Type 0` -/
  example {α : Type} (v: Vec α) (i: Usize) (x : α)
    (hbounds : i.val < v.length) :
     nv, v.update_usize i x = ret nv 
    nv.val = v.val.update i.val x := by
    progress
    simp [*]

end Test

end Progress