search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

how to provide lemma to hammer (not sauto)? #127

Closed brando90 closed 2 years ago

brando90 commented 2 years ago

I know hammer is meant mostly to find dependencies using classical atps -- but I was curious if it was possible to provide hammer extra lemmas directly if we want them. e.g. doing hammer use: LEMMA1. Or perhaps the only way to do it is to define a lemma externally first or with a have: .... by proof statement first then run hammer in the next proof?

lukaszcz commented 2 years ago

Yes, "hammer" will use anything that's in the context. You can add things to the context also with the "use" tactic. "hammer" doesn't accept any options.

brando90 commented 2 years ago

assert and have: also add things to the context afaik. No? funny there are 3 things for that use, have, assert in Coq...

On Mar 19, 2022, at 3:31 AM, Łukasz Czajka @.***> wrote:

Yes, "hammer" will use anything that's in the context. You can add things to the context also with the "use" tactic. "hammer" doesn't accept any options.

— Reply to this email directly, view it on GitHub https://github.com/lukaszcz/coqhammer/issues/127#issuecomment-1072968894, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAOE6LRTWBWGUF5676M5NKLVAWGHXANCNFSM5RC6IUQA. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub. You are receiving this because you authored the thread.

lukaszcz commented 2 years ago

"use" is a tactic from CoqHammer which also simplifies the added hypotheses

On Sat, 19 Mar 2022, 15:29 Brando Miranda, @.***> wrote:

assert and have: also add things to the context afaik. No? funny there are 3 things for that use, have, assert in Coq...

On Mar 19, 2022, at 3:31 AM, Łukasz Czajka @.***> wrote:

Yes, "hammer" will use anything that's in the context. You can add things to the context also with the "use" tactic. "hammer" doesn't accept any options.

— Reply to this email directly, view it on GitHub < https://github.com/lukaszcz/coqhammer/issues/127#issuecomment-1072968894>, or unsubscribe < https://github.com/notifications/unsubscribe-auth/AAOE6LRTWBWGUF5676M5NKLVAWGHXANCNFSM5RC6IUQA . Triage notifications on the go with GitHub Mobile for iOS < https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android < https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

You are receiving this because you authored the thread.

— Reply to this email directly, view it on GitHub https://github.com/lukaszcz/coqhammer/issues/127#issuecomment-1073019886, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKHZJNUQQK3NSZBALSU3VAXQEFANCNFSM5RC6IUQA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you modified the open/close state.Message ID: @.***>