Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Interaction between clausal simplifier and spurious hypothesis #14

Open
Bronsa opened this issue Sep 4, 2019 · 0 comments

Comments

@Bronsa
Copy link
Member

commented Sep 4, 2019

Whenever you have an explicit equality hypothesis between a variable and a non-variable term that doesn't contain it, that leads to an 'explicit substitution' that eliminates the variable - that's so that we have minimal hypotheses before an induction.
In certain cases, this can lead to Imandra removing "manual" destructor elimination, and thus failing to automatically prove a goal by induction.

A key takeaway is, if you have a goal that is going to be proved by induction, always try to make it as strong as possible. As much as possible, you never want to have spurious hypotheses in something you're proving by induction, because then your inductive hypotheses are weaker.

@Bronsa Bronsa added the doc topic label Sep 4, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.