Removing all clutter, this works (also paying the computational cost of the
_ghost_ `f`)
```
let rec flatten_tree (t: tree 'a) : list 'a =
match t with
| Leaf v -> [v]
| Branch subtrees ->
let rec f: l:list (tree 'a){l << t} -> list (t': tree 'a{t' << t}) =
function
| [] -> []
| t' :: ts -> t' :: f ts
in
List.Tot.flatten (List.Tot.map flatten_tree (f subtrees))
```
On Wed, Apr 12, 2017 at 12:57 PM, Catalin Hritcu <catalin.hri...@gmail.com>
wrote:
> >> I wonder if there's a different way to phrase this problem that would
> >> grant us as much flexibility as Coq without the modularity cost. I
> think
> >> the comment in the snippet Nik pointed to earlier
> >> (https://github.com/FStarLang/FStar/blob/master/examples/ter
> mination/termination.fst#L118)
> >> hints at something like this.
>
> Nik's trick directly works here, using the fact that `flatten_list` is
> polymorphic:
> ```
> let rec flatten_list (#a #b:Type) (l:(list b)) (f:(b -> list a)) : list a =
> match l with
> | [] -> []
> | hd::tl -> FStar.List.append (f hd) (flatten_list tl f)
>
> val list_subterm_ordering_lemma:
> #a:eqtype
> -> #b:Type
> -> l:list a
> -> bound:b
> -> x:a
> -> Lemma (requires (l << bound))
> (ensures (FStar.List.mem x l ==> x <<
> bound))
> [SMTPat (FStar.List.mem x l);
> SMTPatT (x << bound)]
> let rec list_subterm_ordering_lemma #a #b l bound x = match l with
> | [] -> ()
> | hd::tl -> list_subterm_ordering_lemma tl bound x
>
> val move_refinement: #a:eqtype
> -> #p:(a -> Type)
> -> l:list a{forall z. FStar.List.mem z l ==> p z}
> -> Tot (list (x:a{p x}))
> let rec move_refinement #a #p l = match l with
> | [] -> []
> | hd::tl -> hd::move_refinement #a #p tl
>
> let rec flatten_tree (#a:eqtype) (t:tree a) : list a =
> match t with
> | Leaf v -> [v]
> | Branch l -> let l = move_refinement #_ #(fun aa -> aa << t) l in
> flatten_list l flatten_tree
>
> ```
>
> The problem I see with Nik's trick is that adding "ghost" in a comment:
> ```
> let l = move_refinement #_ #(fun aa -> aa << v) l in (* ghost *)
> ```
> doesn't make something Ghost in F*, and in fact move_refinement would
> currently have a significant computational cost at the moment.
>
> Catalin
>
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
