>> Did a quick experiment with Kenji, and we could easily prove your >> lemma using assert_norm: >> … > > Wonderful, thanks! Works like a charm. > This might be a useful addition to the tutorial :) Or did I miss it?
Added this to the wiki for now: https://github.com/FStarLang/FStar/wiki/Using-SMT-fuel-and-the-normalizer#using-the-f-normalizer >> On Mon, May 15, 2017 at 4:03 PM, Catalin Hritcu >> <catalin.hri...@gmail.com> wrote: >>> Reminds be of an issue I filed really long time ago: >>> https://github.com/FStarLang/FStar/issues/121 >>> >>> >>> On Mon, May 15, 2017 at 4:00 PM, Clément Pit-Claudel via fstar-club >>> <fstar-club@lists.gforge.inria.fr> wrote: >>>> Hi all, >>>> >>>> I'm having trouble with the (simplified) example below. Is there a subtle >>>> type-inference-related reason for the unfolding lemma to be unprovable? >>>> >>>> Thanks! >>>> Clément. >>>> >>>> module Scratch >>>> >>>> open FStar.List >>>> >>>> assume val pairs_with_sum (n: nat) : list (p: (nat * nat){fst p + snd >>>> p == n}) >>>> >>>> assume val product (#a #b: Type) (l1: list a) (l2: list b) : list (a * >>>> b) >>>> >>>> type bin_tree = >>>> | Leaf >>>> | Branch of bin_tree * bin_tree >>>> >>>> let rec size bt : nat = >>>> match bt with >>>> | Leaf -> 0 >>>> | Branch(l, r) -> 1 + size l + size r >>>> >>>> let rec trees_of_size (s: nat) : list bin_tree = >>>> if s = 0 then >>>> [Leaf] >>>> else >>>> List.Tot.concatMap #(p: (nat * nat){(fst p) + (snd p) == s - 1}) >>>> (fun (s1, s2) -> List.Tot.map Branch (product (trees_of_size s1) >>>> (trees_of_size s2))) >>>> (pairs_with_sum (s - 1)) >>>> >>>> let unfold_tos (s: nat) : >>>> Lemma (trees_of_size s == >>>> (if s = 0 then >>>> [Leaf] >>>> else >>>> List.Tot.concatMap #(p: (nat * nat){(fst p) + (snd p) == s >>>> - 1}) >>>> (fun (s1, s2) -> List.Tot.map Branch (product >>>> (trees_of_size s1) (trees_of_size s2))) >>>> (pairs_with_sum (s - 1)))) = () >>>> _______________________________________________ >>>> 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
