feat: progress with a term #281

RaitoBezarius · 2024-07-03T15:52:43Z

progress with X where X can now be a full term, e.g. X := (@SomeSpec.XYZ T U).

TODO:

diagnose what happens with as and some failures
add unit tests

Signed-off-by: Ryan Lahfa [email protected]

`progress with X` where X can now be a full term, e.g. `X := (@SomeSpec.XYZ T U)`. Signed-off-by: Raito Bezarius <[email protected]>

RaitoBezarius · 2024-07-08T12:14:36Z

@sonmarcho I think this is almost ready, there might be still some vague TODOs, but it feels feature-complete, I will take it for a walk and try to come up with proper interesting unit tests.

The case:

progress with (_: T)

fails because Lean complains about inability to synthesize the placeholder, I wonder if I should try to fix it in the code by modifying the calls to synthesization and allow failure and create for each failure a new metavar and leave it as a new goal to be assigned by the user (which I feel like is the solution to fix that usecase).

sonmarcho · 2024-07-09T08:00:29Z

@sonmarcho I think this is almost ready, there might be still some vague TODOs, but it feels feature-complete, I will take it for a walk and try to come up with proper interesting unit tests.

The case:
progress with (_: T)
fails because Lean complains about inability to synthesize the placeholder, I wonder if I should try to fix it in the code by modifying the calls to synthesization and allow failure and create for each failure a new metavar and leave it as a new goal to be assigned by the user (which I feel like is the solution to fix that usecase).

We might do something like this in the future. I don't see the point of doing this for regular function calls, because then you should always call progress with a precise lemma in mind (or an instantiated lemma, hence the need for terms instead of ids). However, we might want to give the possibility of writing a specification when considering if then else expressions like below, where we would open two goals: one to prove that the expression in the let-binding has the proper spec, and another for after we evaluated the if then else.

let x <- if b then 0 else 1 -- We can't use a lemma here
let y <- f x

sonmarcho · 2024-07-09T08:08:48Z

backends/lean/Base/Progress/Progress.lean

      -- Try the theorems one by one
      for pspec in pspecs do
-        if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return pspec
+        -- TODO: convert pspec into an Expr.


What it this TODO?

sonmarcho · 2024-07-09T08:11:42Z

backends/lean/Base/Progress/Progress.lean

@@ -219,7 +209,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do
   Return true if it succeeded. -/
 def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)


I think we should rename this function to tryApply, because it doesn't perform a lookup anymore.
Also, it might make sense to move the match over the option (and the comments printed in the trace are not valid anymore I believe).

sonmarcho · 2024-07-09T08:12:36Z

backends/lean/Base/Progress/Progress.lean

+      -- Either, it's a local declaration or a theorem, either it's a term
+      -- for which we need to find a declaration
+
+      if id.isIdent then


I don't think we really need this case disjunction. Shouldn't it be performed by Lean's elaboration (i.e., isn't the else branch enough)?

Hm, if I do that, something like:

set_option trace.Progress true in example {x: U32} (f : Result U32 → Result Unit) (h : ∀ (x: U32), ∀ (y: U32), f (x + y) = .ok ()): f (.ok x) = ok () := by have : ∀ x, f x = .ok () := by sorry progress with this

won't work because this elaborated := sorryAx ?m.something true and the metavariable will create an obscure failure of progress here.

(tbh, the current code does not work neither, it fails by not finding this in the context)

Ok, this is good to know (and worth commenting in the code ;) )

Wouldn't this be a blocker though for the PR? I'm trying to make this work but I'm just diving into how the whole thing is supposed to work

What I meant is that the fact that we need the case disjunction is good to know and should be documented. But of course, we need to make the elaboration work, generally speaking.

sonmarcho · 2024-07-09T08:12:53Z

backends/lean/Base/Progress/Progress.lean

    stxArgs := stxArgs.setArg 1 withArg
  let tac := mkNode `Progress.progress #[mkAtom "progress", stxArgs]
+  -- if stats.usedTheorem.isInaccesisble then
+  --  logInfo "{...} is inaccessible, if you want to actually use the suggestion, please use `rename_i ...`"


Please remove all commented code (note however that printing such a comment would be useful, if it is possible).

RaitoBezarius · 2024-07-09T14:46:42Z

backends/lean/Base/Progress/Progress.lean

@@ -268,17 +258,17 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
  match withTh with
  | some th => do
    match ← progressWith fExpr th keep ids splitPost asmTac with
-    | .Ok => return th
+    | .Ok => return (← exprToSyntax th)


Hm, I'm not so sure this is the right way to transform an expression to syntax for progress?

Does it generate spurious syntax?

Yeah, just dump a metavariable I think

I'm not sure I understand in which situations it dumps a metavariable: could you clarify a bit?
But if exprToSyntax doesn't work there is likely a simple way of getting the name of the theorem and transforming it to syntax.

feat: progress can receives terms in its with argument

f078764

`progress with X` where X can now be a full term, e.g. `X := (@SomeSpec.XYZ T U)`. Signed-off-by: Raito Bezarius <[email protected]>

RaitoBezarius force-pushed the progress-with-terms branch from 4dcfcd3 to f078764 Compare July 8, 2024 12:12

RaitoBezarius marked this pull request as ready for review July 8, 2024 12:13

sonmarcho reviewed Jul 9, 2024

View reviewed changes

RaitoBezarius commented Jul 9, 2024

View reviewed changes

sonmarcho mentioned this pull request Aug 27, 2024

Improve the progress tactic #315

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: progress with a term #281

feat: progress with a term #281

RaitoBezarius commented Jul 3, 2024 •

edited

Loading

RaitoBezarius commented Jul 8, 2024

sonmarcho commented Jul 9, 2024

sonmarcho Jul 9, 2024

sonmarcho Jul 9, 2024

sonmarcho Jul 9, 2024

RaitoBezarius Jul 9, 2024

RaitoBezarius Jul 9, 2024

sonmarcho Jul 11, 2024

RaitoBezarius Jul 11, 2024

sonmarcho Jul 11, 2024

sonmarcho Jul 9, 2024

RaitoBezarius Jul 9, 2024

sonmarcho Jul 11, 2024

RaitoBezarius Jul 11, 2024

sonmarcho Jul 11, 2024 •

edited

Loading

		@@ -219,7 +209,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do
		Return true if it succeeded. -/
		def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)

feat: progress with a term #281

Are you sure you want to change the base?

feat: progress with a term #281

Conversation

RaitoBezarius commented Jul 3, 2024 • edited Loading

RaitoBezarius commented Jul 8, 2024

sonmarcho commented Jul 9, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sonmarcho Jul 11, 2024 • edited Loading

Choose a reason for hiding this comment

RaitoBezarius commented Jul 3, 2024 •

edited

Loading

sonmarcho Jul 11, 2024 •

edited

Loading