Proof context dependence #2900
Replies: 2 comments
-
When you're working against the interface of FStar.Seq.Properties.fsti, the only thing you know about map_seq are the properties made visible in the interface. In particular, the definition of the map_seq is not visible. Whereas, if you put this in the implementation of the module, then all the definitions are visible and the lemma is provable. Does that make sense? This chapter explains more about interfaces. http://fstar-lang.org/tutorial/book/part3/part3.html#modularity-with-interfaces-and-typeclasses |
Beta Was this translation helpful? Give feedback.
0 replies
-
Nik, that is one of the things I considered and it's clear now, thanks.
This is small potatoes but actually it was really cool to test via
proof (normalization)!
So three questions:
1) I should check in the tests under tests/printable?
2) Some tests can't run with just normalization as this shows.
There does not seem to be a unit test for executable tests.
Should there be? I know it's not as important in a proof
oriented PL but it's still needed a bit.
Should I make one? And write a section on "Test by Proof
(and when that won't work)"? and perhaps a default
simple benchmarking framework?
3) Many PL's have concrete lists, vectors or arrays (one adjustable length)
and make their use abstract under a collections (or sequence) interface.
There is small loss of ease of proof without proof by normalization. But
lots of duplication without functors in the module system.
The only proof oriented module system I have played with is in Coq
and when I was last using it, it was quite buggy. Anyone know of
a good one?
4) Attempting to compare and understand list's normalization with
sequence's, it was clear that I could not trace by steps. A good
thing for learning. So a compute_some : nat -> ? would be helpful.
But mostly, more flesh on the bones of the tactics section.
5) Guido had to show me
instance printable_ref #a #p (d : printable a) : printable (x:a{p x}) =...
a paragraph in the typeclass section would show you how to
get an instance for a refined type.
When I know 1, I can setup a pull for Printables.
Thanks, B
…On Fri, Apr 28, 2023, 8:53 PM nikswamy ***@***.***> wrote:
When you're working against the interface of FStar.Seq.Properties.fsti,
the only thing you know about map_seq are the properties made visible in
the interface. In particular, the *definition* of the map_seq is not
visible. Whereas, if you put this in the implementation of the module, then
all the definitions are visible and the lemma is provable. Does that make
sense?
This chapter explains more about interfaces.
http://fstar-lang.org/tutorial/book/part3/part3.html#modularity-with-interfaces-and-typeclasses
—
Reply to this email directly, view it on GitHub
<#2900 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACKMDK22KLLAUBG77JJZ7XDXDSGCBANCNFSM6AAAAAAXP47VP4>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
I've been playing with a clean Printable and writing proof tests for it to check it and understand more about proofs.
I was a bit surprised to find code context dependence ( -1 parsing in let assignments but not body with the same type)
but now I seem to found some possible proof context dependence that I can't suss out.
let map_of_empty_list_is_empty_list (#a #b:eqtype) (f: a -> b):
Lemma (requires true)
(ensures (FStar.List.Tot.Base.map f ([] <: list a)) = ([] <: list b))
= ()
proves as expected, but do it again with sequences
let map_seq_of_empty_is_empty (#a #b:eqtype) (f: a -> b):
Lemma (requires true)
(ensures (map_seq f (empty <: seq a)) = (empty <: seq b))
= ()
and it won't prove.
But the odd thing is drop it at the end of FStar.Seq.Properties.fst and it proves,
but it won't prove at the end of the fsti file!
I did a wee bit o source scraping and can see that they both have the same
set of lemmas (as you would expect). z3 options aren't needed to prove this
(and it's not missing a pop-options).
Anyone have any ideas how to suss this out?
Beta Was this translation helpful? Give feedback.
All reactions