On 2017-05-16 12:26, Catalin Hritcu wrote: > Hi Clément, > > 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? Clément. > 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
