Hi Arun, the error message could be better, but it is saying that your list is a list of pairs of something (that is ?u4 * ?u5) when it should be a list of strings. The problem is that list literals in F*, as in OCaml and F#, separate their elements by ';' instead of ','. If you fix that, you won't get this mysterious error, but instead the proof will still fail like this:
T.fst(8,8-8,14): (Error 19) assertion failed; The solver found a (partial) counterexample, try to spell your proof in more detail or increase fuel/ifuel (see also T.fst(8,26-8,73)) It fails since `String.concat` is an assumed function in F* (it has no definition, nor any interesting specification), and our SMT encoding does not state anything about it beyond its type. To my knowledge we have not really done much reasoning on programs manipulating strings. Some related F* issues are: https://github.com/FStarLang/FStar/issues/548 https://github.com/FStarLang/FStar/issues/657 So, sadly, I don't think your assertion is currently provable in F*... but it should be in the future Best, Guido On Fri, 4 Oct 2019 at 14:24, P Arun Babu via fstar-club <fstar-club@lists.gforge.inria.fr> wrote: > > Dear all, > > I am new to Fstar and theorem provers. > > Is there some way to prove a program which looks like this: > > ---------------------------------------------------------------- > module T > > let canWrite (f:string) = > match f with > | "demo/tempfile" -> true > | _ -> false > > let _ = assert (forall x. canWrite(String.concat "/" ["temp", x]) = false) > > ---------------------------------------------------------------- > I get: > > (Warning 271) Pattern uses these theory symbols or terms that should > not be in an smt pattern: Prims.op_Subtraction 1 (see also > /home/arun/.opam/default/lib/fstar/FStar.UInt.fst(671,8-671,51)) > > ... lots of warnings ..., and finally: > > T.fst(8,59-8,63): (Error 54) (*?u4*) _ * (*?u5*) _ is not a subtype of > the expected type Prims.string > 1 error was reported (see above) > > > Thank you and regards, > Arun > _______________________________________________ > fstar-club mailing list > fstar-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/fstar-club _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
