symcc: refactor a couple more places to rely on higher level primitives#909
Conversation
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
| | .set ts _ => ts.elts.mapUnion₁ (λ ⟨t, _⟩ => t.entityUIDs) | ||
| | .record ats => ats.toList.mapUnion₃ (λ ⟨(_, t), _⟩ => t.entityUIDs) | ||
| | .app _ ts _ => ts.mapUnion₁ (λ ⟨t, _⟩ => t.entityUIDs) | ||
| decreasing_by |
There was a problem hiding this comment.
Have you looked into way to automate termination proofs better? I tried adding some of the sizeOf theorems to @[simp], but that didn't seem to help much.
Or, more specifically, why does this now need an explicit termination proofs?
There was a problem hiding this comment.
I was thinking about automating termination proofs with a Kiro/Claude skill. We could have Kiro write the skill itself by asking it to look at all of the existing termination proofs and write itself some advice for the future for things to try or use.
@[simp] is not smart enough to know when to apply some of these lemmas, as they aren't just rewrites.
This now needs explicit termination proofs because there's a mismatch between the _ property in the function, and the property that Lean needs in order to convince itself of termination. For example in the .set case, the _ property now tells us that t \in ts.elts. But we actually need something more like t \in ts in order for the automatic termination checker to work, since ts is the structural thing that the function recurses on. Which isn't to say that mapUnion₁ isn't still helpful -- it gives us a starting prop from which we can derive the property we actually need, unfortunately manually.
It does seem like this should be amenable to better automation, but I'm not immediately sure what/how. We could try adding @[grind] to some of the SizeOf lemmas and seeing if some combination of grind and omega works. Unfortunately both grind and omega have to be terminal
There was a problem hiding this comment.
In this PR in Concretizer/Lit.lean I wrote one of the termination proofs using calc. Perhaps this is a style we prefer or that is more automatable. Or perhaps it's more automatable to just put all the lemmas we need into the context with have and let omega figure it out, which is our more typical practice in this codebase.
|
|
||
| @[simp] | ||
| public theorem find?_mapOnValues {α β γ} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) (m : Map α β) (k : α) : | ||
| (m.find? k).map f = (m.mapOnValues f).find? k |
There was a problem hiding this comment.
Does this help simp?
There was a problem hiding this comment.
Yes. Switching the direction ensures that the simpler form (which we prefer to reason about) is on the RHS. The (m.mapOnValues f).find? form is harder to reason about because it applies find? to an opaquely-constructed Map (seeing as mapOnValues is an opaque definition, for files complying with the module system).
3 participants
Refactors a couple more places to rely on higher level primitives instead of destructuring
Sets andMaps -- particularly in Concretizer.lean and Interpretation.lean. Introduces a few new lemmas aboutSets andMaps, and adds@[simp]to a couple of existing ones.In Term/Same.lean, Kiro completely rewrote one of the proofs to rely on higher-level lemmas instead of destructuring
Maps and reasoning about Lists.