search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

let comment (p : Type) = () is useful while working on proofs #3602

Closed briangmilnes closed 1 week ago

briangmilnes commented 2 weeks ago

A small addition to prims would be: let comment (p : Type) = ()

because while you are working on proofs you want to if ... then (assert or assume(P); term) ...

and check if it's needed without deleting it. So you can change it to comment. Or ignore or such.

nikswamy commented 2 weeks ago

Why not just make it a real comment with // or (* ... *)?

briangmilnes commented 2 weeks ago

It's just faster and clearer than commenting, which I do otherwise. It would be nice too to have a comment(lemma...) that did not apply the lemma.

Just a nice little flourish.

On Mon, Nov 4, 2024 at 3:39 PM nikswamy @.***> wrote:

Why not just make it a real comment with // or ( ... )?

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/3602#issuecomment-2455924230, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK43OALW74HVW2I7IALZ67ZQVAVCNFSM6AAAAABRE6XO6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJVHEZDIMRTGA . You are receiving this because you authored the thread.Message ID: @.***>

briangmilnes commented 2 weeks ago

I should say it lets you show the intermediate asserts that you don't need in the final proofs.

On Mon, Nov 4, 2024 at 6:00 PM Brian Milnes @.***> wrote:

It's just faster and clearer than commenting, which I do otherwise. It would be nice too to have a comment(lemma...) that did not apply the lemma.

Just a nice little flourish.

On Mon, Nov 4, 2024 at 3:39 PM nikswamy @.***> wrote:

Why not just make it a real comment with // or ( ... )?

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/3602#issuecomment-2455924230, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK43OALW74HVW2I7IALZ67ZQVAVCNFSM6AAAAABRE6XO6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJVHEZDIMRTGA . You are receiving this because you authored the thread.Message ID: @.***>

briangmilnes commented 2 weeks ago

Like this: let not_subset_lstl_impl_not_subset (#e: eqtype) (lsa: (listset e){~(isempty lsa)}) (lsb: listset e) : Lemma (requires ~(subset (lstl lsa) lsb)) (ensures ~(subset lsa lsb)) [SMTPat (~(subset (lstl lsa) lsb)); SMTPat (~(subset lsa lsb))] = introduce subset lsa lsb ==> False with pf_subset_lsa_lsb . begin comment(~(subset (lstl lsa) lsb)); comment(~(forall e'. mem e' (lstl lsa) ==> mem e' lsb)); comment(~(forall e'. mem' e' (lstl lsa) ==> mem' e' lsb)); comment(exists e'. ~(mem e' (lstl lsa) ==> mem e' lsb)); comment(exists e'. mem' e' (lstl lsa) /\ not(mem' e' lsb)); eliminate exists e'. mem' e' (lstl lsa) /\ not(mem' e' lsb) returns ~(subset lsa lsb) with pf_mem_e'_lstl_lsa_and_not_mem_e'_lsb . begin comment(mem' e' (lstl lsa)); assert(mem' e' lsa); assert(not(mem' e' lsb)); () end end

On Mon, Nov 4, 2024 at 6:21 PM Brian Milnes @.***> wrote:

I should say it lets you show the intermediate asserts that you don't need in the final proofs.

On Mon, Nov 4, 2024 at 6:00 PM Brian Milnes @.***> wrote:

It's just faster and clearer than commenting, which I do otherwise. It would be nice too to have a comment(lemma...) that did not apply the lemma.

Just a nice little flourish.

On Mon, Nov 4, 2024 at 3:39 PM nikswamy @.***> wrote:

Why not just make it a real comment with // or ( ... )?

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/3602#issuecomment-2455924230, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK43OALW74HVW2I7IALZ67ZQVAVCNFSM6AAAAABRE6XO6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJVHEZDIMRTGA . You are receiving this because you authored the thread.Message ID: @.***>

briangmilnes commented 2 weeks ago

Nik,

The advantage here is both typographical and for changes. If you put that in the editor it and it reads right and gets type checked. So if you change something you see it. My comment though is getting into the proof state which is interesting.

If you // it out it's a different color, different fonts and just plain ugly. Proofs should be beautiful in my mind.

Do you like the idea or not?

-B

On Mon, Nov 4, 2024 at 6:24 PM Brian Milnes @.***> wrote:

Like this: let not_subset_lstl_impl_not_subset (#e: eqtype) (lsa: (listset e){~(isempty lsa)}) (lsb: listset e) : Lemma (requires ~(subset (lstl lsa) lsb)) (ensures ~(subset lsa lsb)) [SMTPat (~(subset (lstl lsa) lsb)); SMTPat (~(subset lsa lsb))] = introduce subset lsa lsb ==> False with pf_subset_lsa_lsb . begin comment(~(subset (lstl lsa) lsb)); comment(~(forall e'. mem e' (lstl lsa) ==> mem e' lsb)); comment(~(forall e'. mem' e' (lstl lsa) ==> mem' e' lsb)); comment(exists e'. ~(mem e' (lstl lsa) ==> mem e' lsb)); comment(exists e'. mem' e' (lstl lsa) /\ not(mem' e' lsb)); eliminate exists e'. mem' e' (lstl lsa) /\ not(mem' e' lsb) returns ~(subset lsa lsb) with pf_mem_e'_lstl_lsa_and_not_mem_e'_lsb . begin comment(mem' e' (lstl lsa)); assert(mem' e' lsa); assert(not(mem' e' lsb)); () end end

On Mon, Nov 4, 2024 at 6:21 PM Brian Milnes @.***> wrote:

I should say it lets you show the intermediate asserts that you don't need in the final proofs.

On Mon, Nov 4, 2024 at 6:00 PM Brian Milnes @.***> wrote:

It's just faster and clearer than commenting, which I do otherwise. It would be nice too to have a comment(lemma...) that did not apply the lemma.

Just a nice little flourish.

On Mon, Nov 4, 2024 at 3:39 PM nikswamy @.***> wrote:

Why not just make it a real comment with // or ( ... )?

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/3602#issuecomment-2455924230, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK43OALW74HVW2I7IALZ67ZQVAVCNFSM6AAAAABRE6XO6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJVHEZDIMRTGA . You are receiving this because you authored the thread.Message ID: @.***>

nikswamy commented 2 weeks ago

I'm not in favor of having this in prims. If you like this style, then you could use your own let comments p = () definition.

briangmilnes commented 2 weeks ago

But somehow p is being processed in the proof, so I can't really do that. Is there someway to ensure that p is just parsed, type checked but not used in the proof? A tactic perhaps?

On Tue, Nov 5, 2024 at 11:06 AM nikswamy @.***> wrote:

I'm not in favor of having this in prims. If you like this style, then you could use your own let comments p = () definition.

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/3602#issuecomment-2457952553, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK7NHAXLVZOA47HYTPLZ7EJM7AVCNFSM6AAAAABRE6XO6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJXHE2TENJVGM . You are receiving this because you authored the thread.Message ID: @.***>

briangmilnes commented 2 weeks ago

Ah let comment p = assert(True) is doing the job. It type checks p, puts trivial True in the goal stack, and prints nicely. You don't find //p printing in red in different fonts ugly enough to fix? I wonder how many of the 940 asserts in ulib are needed in the proof versus being commentable.

On Tue, Nov 5, 2024 at 11:16 AM Brian Milnes @.***> wrote:

But somehow p is being processed in the proof, so I can't really do that. Is there someway to ensure that p is just parsed, type checked but not used in the proof? A tactic perhaps?

On Tue, Nov 5, 2024 at 11:06 AM nikswamy @.***> wrote:

I'm not in favor of having this in prims. If you like this style, then you could use your own let comments p = () definition.

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/3602#issuecomment-2457952553, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK7NHAXLVZOA47HYTPLZ7EJM7AVCNFSM6AAAAABRE6XO6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJXHE2TENJVGM . You are receiving this because you authored the thread.Message ID: @.***>

nikswamy commented 1 week ago

Glad that you have a style that works for you. I don't want to suggest that this is a recommended style by including it in prims.