Add a subset_mem lemma to make mem_subset more complete #3199
Conversation
- Mirrors TSet - reflexivity is now implied thanks to the SMTPat in mem_subset, kept the function for compatibility but removed the SMTPat
chandradeepdey
changed the title
ulib/FStar.List.Tot.Properties.fst
Outdated
| let rec subset_mem (#a: eqtype) (la lb: list a) | ||
| : Lemma (requires (subset la lb)) | ||
| (ensures (forall x. mem x la ==> mem x lb)) | ||
| [SMTPat (subset la lb)] = |
There was a problem hiding this comment.
Hi @chandradeepdey, this pattern is not optimal for the lemma, since it is not goal-directed. Usually, we pick patterns that mention terms in the goals (i.e., ensures) so that Z3 instantiates the lemma when it needs to prove the postcondition.
Rest of the changes look good to me. Do you absolutely need this smtpat? E.g., could you remove the pattern, and invoke the lemma manually?
There was a problem hiding this comment.
(If you prefer, I can also do this change in your branch, let me know.)
There was a problem hiding this comment.
Oh, okay. What I wanted was subset la lb <==> (forall x. mem x la ==> mem x lb) to be put in the context whenever subset la lb is mentioned.
I was using mem_subset to send a subset as a function argument. I don't need this new one, but thought it would be useful to have the reverse, i.e. get the information out of a function parameter.
Sure, you can make changes.
There was a problem hiding this comment.
Thanks again!
|
@aseemr How about this? |
kept the function for compatibility but removed the SMTPat