Open mww-aws opened 10 months ago
@mww-aws This is a very involved issue. At first glance, I believe to fully fix this we need to implement (1) Support for complicated dependent types (at least for recursors), or support for obtaining definitional equality for functions whose body contain match
(2) Translation from higher-order logic to first-order logic.
At this point it's unclear to me how exactly I should implement support for these two features because there are a lot of design choices to make. I'll look more into this issue after Jan 7th next year.
If it's ok to you, you can manually prove the four definitional equalities related to Zone.MinArea1
, and supply them to auto
.
O.k., I can prove those. How would I submit them to auto? Could you give a concrete example, then I can generalize.
The cases x
is indeed not necessary in these examples.
Okay, fixed. Now a more complex lemdb example is recorded in https://github.com/leanprover-community/lean-auto/blob/main/Test/LemDBTest.lean and the no-lemdb example is recorded in https://github.com/leanprover-community/lean-auto/blob/main/Test/SmtTranslation/MatchWorkaround.lean
I have a trivial Lean spec:
I can't seem to prove it by auto because it is not expanding the definition of MinArea1:
I have tried a couple of things like asking lean-auto to unfold Zone.MinArea1: auto u[Zone.MinArea1] but this leads to an error:
lamTerm2STerm :: Unexpected head term Auto.Embedding.Lam.LamTerm.lam (.atom 1) (.app (.base (.nat)) (.base (.icst (.iofNat))) (.base (.ncst (.natVal 10000))))
Can you tell me how to complete this proof properly? Also, is it possible to get lean-auto to handle the cases part?