rewriting 'forall x: Nat. exists y: Nat. y == x' to true

[jgroote]

Issue migrated from trac ticket # 1299

component: Data: Enumerator Library | priority: minor

2014-07-22 15:37:09: @wiegerw created the issue

---

The rewriter was able to rewrite the expression forall x: Nat. exists y: Nat. y == x to true. But in revision 12986 the name generation for the enumerator has changed, and now rewriting this expression does not work anymore.

It should be investigated whether the previous behavior of the enumerator should be restored.

[jgroote]

2016-11-17 14:05:27: @wiegerw changed type from defect to feature request

[jgroote]

2016-11-24 19:24:31: @wiegerw changed status from new to accepted

[jgroote]

2016-11-24 19:24:31: @wiegerw

[jgroote]

I believe that this problem essentially boils down to the question how to enumerate the solutions for x that satisfy x=c for some expression c. The current enumerator cannot handle this, as it enumerates based on the constructors of a sort. But one could conceive an enumerator that also takes equalities into account. I believe that this is a valid and natural enhancement of an enumerator, and I suggest that we leave it open, but only give it a low priority, and certainly not address it in the release of summer 2018.