feat: contractive and nonexp tactics - #558
Conversation
|
This is sweet! I think we should wait until #550 is merged though, since it is still a debated question how this new parameter is going to be inferred, and this will probably change your tactic. |
MackieLoeffel
left a comment
MackieLoeffel
left a comment
There was a problem hiding this comment.
Thanks for the PR and sorry for the delay in reviewing. I slightly cleaned up the PR and moved around some files. Overall the PR looks nice, but I tried using nonexp and contractive in more places in the repo and ran into some problems. See the comments below.
|
|
||
| meta partial def contractiveMain (goal : MVarId) (guarded : Bool) : TacticM Unit := do | ||
| if ← goal.isAssigned then return | ||
| trace[NonExp] "Goal: {← goal.getType}" |
There was a problem hiding this comment.
I tried using the tactic and it failed without giving any information. So I added some rudimentary tracing to the tactic, but it is currently not great. For example, it does not show what instances were tried or which step succeeded. Can you add better tracing information?
| refine ((equiv_iff.mpr le_upd_unfold).dist).trans ?_ | ||
| refine .trans ?_ ((equiv_iff.mpr le_upd_unfold).dist).symm | ||
| -- TODO: Why does nonexp not work here? | ||
| refine forall_ne (fun i => ?_) |
There was a problem hiding this comment.
I tried using nonexp here and it failed. Do you know why?
In general, I think it would be good to make a pass over the repo and use nonexp and contractive for all NonExpansive and Contractive obligations.
| (fun a => NextContractive.distLater_dist (fun m hm => h m hm a))⟩ | ||
| Contractive (saved_pred_own (GF := GF) (A := A) γ dq) where | ||
| distLater_dist := -- TODO: Why does by contractive not work here? | ||
| fun {_ _ _} h => saved_anything_ne γ dq |>.ne |
There was a problem hiding this comment.
I tried using by contractive here and it failed. Do you know why?
| ne := by nonexp | ||
|
|
||
| /- `nonexp` should also work when directly called on a NonExpansive goal -/ | ||
| example : NonExpansive (fun x : α => x) := by nonexp |
There was a problem hiding this comment.
I think nonexp should also work when directly called on a NonExpansive goal. Otherwise, it will be very confusing for the users. Same for contractive. Can you make this work?
| contractiveSetup | ||
| contractiveMain (← getMainGoal) false | ||
|
|
||
| elab "nonexp" : tactic => do |
There was a problem hiding this comment.
Do we actually need two different tactics for nonexp and contractive or can they be unified into a single tactic?
| if ← tryStep (contractiveMain · guarded) distLaterStep goal then return | ||
|
|
||
| -- applies a non-expansive lemma | ||
| if ← tryStep (contractiveMain · guarded) nonexpStep goal then return |
There was a problem hiding this comment.
This implementation is based on backtracking between the different options. Do we actually need the backtracking or can we just stick with the first case that works?
3 participants
Description
Implements
contractiveandnonexptactics to automatically solveOFE.ContractiveandOFE.NonExpansivegoals, respectively.Closes #123
Checklist
authorssection of any appropriate files