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
