Add forall versions of memP_map_intro and memP_map_elim

[chandradeepdey]

[chandradeepdey]

Sec2.HIFC.fst fails, is it problematic to have SMTPats for this kind of forall exists lemmas?

[chandradeepdey]

Adding an SMTPat to memP_map_intro and/or memP_map_elim also causes errors, gave up on SMTPats and just added the forall lemma that I wanted.

[aseemr]

Thanks @chandradeepdey . An alternate proof for the two lemmas would be using forall introduction, rather than repeating the induction. For example,

let memP_map_intro_forall (#a #b: Type) (f: (a -> Tot b)) (l: list a)
    : Lemma (forall x. memP x l ==> memP (f x) (map f l)) =

    introduce forall x. memP x l ==> memP (f x) (map f l)
    with memP_map_intro f x l

(See https://www.fstar-lang.org/tutorial/book/part2/part2_logical_connectives.html#constructive-classical-connectives for more on classical connectives.)

This way is a bit more modular. What do you think?

[chandradeepdey]

Thanks @chandradeepdey . An alternate proof for the two lemmas would be using forall introduction, rather than repeating the induction. For example,

let memP_map_intro_forall (#a #b: Type) (f: (a -> Tot b)) (l: list a)
    : Lemma (forall x. memP x l ==> memP (f x) (map f l)) =

    introduce forall x. memP x l ==> memP (f x) (map f l)
    with memP_map_intro f x l

(See https://www.fstar-lang.org/tutorial/book/part2/part2_logical_connectives.html#constructive-classical-connectives for more on classical connectives.)

This way is a bit more modular. What do you think?

Thanks! I was wondering whether there were other ways than writing the same thing again. But I still don't understand why the SMTPat caused issues the first time around. I thought it was the hints and tried regenerating them, but then that itself failed.

PS: Sorry about the rebase, I realised the mistake after doing it 😅

[chandradeepdey]

Closing this. I think the SMTPat here is a bad idea based on what Nik said on Slack. Without the SMTPat, this change just adds one line that needs to be invoked with one more line in the user code. Seems useless.