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.

Sign up for GitHub

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

Add a subset_mem lemma to make mem_subset more complete #3199

Merged
merged 3 commits into from
Feb 19, 2024
Merged

Add a subset_mem lemma to make mem_subset more complete #3199

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f28e378
Add a subset_mem lemma to make mem_subset more complete
chandradeepdey Jan 30, 2024
594cd68
Merge remote-tracking branch 'upstream/master' into subset
chandradeepdey Feb 19, 2024
6cfe3be
Merge mem_subset and subset_mem into one
chandradeepdey Feb 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 12 additions & 2 deletions ulib/FStar.List.Tot.Properties.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -596,13 +596,23 @@ let rec partition_count_forall #a f l= match l with

let rec mem_subset (#a: eqtype) (la lb: list a)
: Lemma (requires (forall x. mem x la ==> mem x lb))
(ensures (subset la lb)) =
(ensures (subset la lb))
[SMTPat (subset la lb)] =
match la with
| [] -> ()
| hd :: tl -> mem_subset tl lb

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)] =
Copy link
Collaborator

@aseemr aseemr Feb 17, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(If you prefer, I can also do this change in your branch, let me know.)

Copy link
Contributor Author

@chandradeepdey chandradeepdey Feb 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks again!

match la with
| [] -> ()
| hd :: tl -> subset_mem tl lb

(* NOTE: This is implied by mem_subset above, kept for compatibility *)
let subset_reflexive (#a: eqtype) (l: list a)
: Lemma (subset l l) [SMTPat (subset l l)] = mem_subset l l
: Lemma (subset l l) = ()

(** Correctness of quicksort **)

Expand Down
Loading