Hi Clément,
Did a quick experiment with Kenji, and we could easily prove your
lemma using assert_norm:
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)))) =
assert_norm (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))))
In general, leaving these kind of unification problems to the SMT
solver is quite shady, since our SMT encoding is in no way complete.
Hopefully tactics will soon provide more elegant way to solve this :)
Catalin
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
