Termination of recursive function with inductive type

[VincentCheval]

Hello,

I have simplified my problem into the following: Imagine you have a type of trees where each node can have multiple sons and are labeled by an integer (the multiple sons are represented by the list tree in the type tree. The leaves are not labeled. It's not very elegant in this simplified version by I would need something similar in my real code.

module Test

type tree =
  | Leaf : tree
  | Node : int -> list tree -> tree

val size: t:tree -> Tot nat (decreases t)
let rec size t = match t with
  | Leaf -> 1
  | Node n l_sons-> List.Tot.fold_left (fun acc son -> size son + acc) 1 l_sons

It gives the following error:

Subtyping check failed; expected type (list _7_235:tree{(%[_7_235] << %[t])}); got type (list tree)

The use of List.Tot.fold_left looks a bit overkill but it's a simplified code ^^.

Typically, he does not understand that the variable l_sons should be of type (list t':tree{(%[t'] << %[t])}). However according to your tutorial, the order << works with inductive types. Hence, F* should understand that %[l_sons] << %[t]. And since l_sons is a list of trees define inductively, we should have that l_sons is of type (list t':tree{(%[t'] << %[t])}). I try to give clues to F* to make this reasoning but I mainly get syntax errors when I try something. The only solution I found was to drop the List.Tot.fold_left and to rewrite a sub-function for it. In that case, F* seems to deduce correctly the relation above without much help.

val size: t:tree -> Tot nat (decreases t)
val sub_size: l_sons:list tree -> Tot nat (decreases l_sons)
let rec size t = match t with
  | Leaf  -> 1
  | Node _ l_sons -> sub_size l_sons

and sub_size l_sons = match l_sons with
  | [] -> 1
  | t::tl -> size t + sub_size tl

In that case it works but I would prefer being able to reuse existing functions rather than rewriting everything every time.

Could someone give me a tip on how make the first code work ?

Thanks a lot ! Vincent

[VincentCheval]

I tried also the following code:

module Test

type tree =
  | Leaf : tree
  | Node : int -> list tree -> tree

val size: t:tree -> Tot nat (decreases t)
let rec size t = match t with
  | Leaf -> 1
  | Node n (l_sons:list (t':tree{ %[t'] << %[t]})) ->
      List.Tot.fold_left (fun acc son -> (size son) + acc) 1 l_sons

It does not give me syntax errors but it does not type check either. Would it be possible to indicate inside the declaration of the type tree that the trees in the nodes are smaller according to the relation << ? Something like:

type (t:tree) =
  | Leaf : tree
  | Node : int -> list (t':tree{ %[t'] << %[t]}) -> tree

The previous code gives me a syntax error but it's just to give my intuition.

Thanks again 😊 Vincent

[catalin-hritcu]

This seems like a common source of pain. Please have a look at treeMap here: https://github.com/FStarLang/FStar/blob/master/examples/termination/termination.fst#L110 The main problem here is that even if F* can prove a property p for all elements of a list, that's not enough for it to give the list type list (x:'a{p}).

[VincentCheval]

It's working like magic 😊 I would have never come up with what you wrote in termination.fst ! Thanks a lot of the help. It's very pleasing to always receive very quick answer.

[VincentCheval]

Hello again,

Continuing on my previous problem, I think I found a bug. I used the code that you showed me, that is:

val list_subterm_ordering_coercion:
  l:list 'a
  -> bound:'b{Precedes l bound}
  -> Tot (m:list 'a{l==m /\ (forall (x:'a). List.Tot.mem x m ==> Precedes x bound)})

let rec list_subterm_ordering_coercion l bound = match l with
  | [] -> []
  | hd::tl ->
    hd::list_subterm_ordering_coercion tl bound

(* WARNING: pattern does not contain all quantified variables. *)
val list_subterm_ordering_lemma:
  l:list 'a
  -> bound:'b
  -> x:'a
  -> Lemma (requires (l << bound))
          (ensures (FStar.List.Tot.mem x l ==> x << bound))
          [SMTPat (FStar.List.Tot.mem x l); SMTPatT (x << bound)]

let rec list_subterm_ordering_lemma l bound x = match l with
  | [] -> ()
  | hd::tl -> list_subterm_ordering_lemma tl bound x

val move_refinement:
  #a:Type
  -> #p:(a -> Type)
  -> l:list a{forall z. FStar.List.Tot.mem z l ==> p z}
  -> Tot (list (x:a{p x}))

let rec move_refinement (a:Type) (p:(a -> Type)) l = match l with
  | [] -> []
  | hd::tl -> hd::move_refinement #a #p tl

And then I wanted to show that the length of the list return by move_refinement #a #p l is the same as l. For that, I followed what you wrote for mapT_lemma in Star.ListProperties.fst:

val lemma_move_refinement_length:
  #a:Type
  -> #p:(a -> Type)
  -> l:list a{forall z. FStar.List.Tot.mem z l ==> p z}
  -> Lemma (requires (True))
          (ensures ((FStar.List.Tot.length l) = (FStar.List.Tot.length (move_refinement #a #p l))))
          [SMTPat (move_refinement #a #p l)]

let rec lemma_move_refinement_length (a:Type) (p:(a -> Type)) l = match l with
  | [] -> ()
  | hd::tl -> lemma_move_refinement_length #a #p tl

But then F* gives me the following error:

Version/Proof_tools.fst(51,0-53,51): post-condition at /Users/vincentcheval/Documents/Recherche/Outils/APKISS/Fstar Version/Proof_tools.fst(48,20-48,97)

I checked on the github and I found one of your post explaining that you manage to solve that using refinements instead of requires and ensures. So I changed the code into:

val lemma_move_refinement_length:
  #a:Type
  -> #p:(a -> Type)
  -> l:list a{forall z. FStar.List.Tot.mem z l ==> p z}
  -> GTot (u:unit{ List.Tot.length (move_refinement #a #p l) = List.Tot.length l})

let rec lemma_move_refinement_length (a:Type) (p:(a -> Type)) l = match l with
  | [] -> ()
  | hd::tl -> lemma_move_refinement_length #a #p tl

But then F* gives me a stranger error:

/Users/vincentcheval/Documents/Recherche/Outils/APKISS/Fstar Version/Proof_tools.fst(52,14-52,51): Subtyping check failed; expected type u:unit{((length (move_refinement l)) = (length l))}; got type u:unit{((length (move_refinement tl)) = (length tl))}

I don't really get how he cannot infer from u:unit{((length (move_refinement tl)) = (length tl))} that u:unit{((length (move_refinement l)) = (length l))}

What is what you meant when you said you used refinement ?

Thanks for the help

Vincent

[catalin-hritcu]

I checked on the github and I found one of your post explaining that you manage to solve that using refinements instead of requires and ensures.

Could you remind me which post you're talking about here?

[VincentCheval]

This one: https://github.com/FStarLang/FStar/issues/155

[catalin-hritcu]

Since #155 is already closed I think we can safely assume that problem is fixed.

I don't really get how he cannot infer from u:unit{((length (move_refinement tl)) = (length tl))} that u:unit{((length (move_refinement l)) = (length l))}

I would also expect this to work, since: length (move_refinement (hd::tl)) = length (hd::move_refinement tl) = 1+length (move_refinement tl) Could you please try adding assertions about these 2 equalities and check that they can be proved?

Another thing I would try would be proving the equality you want directly in the type of move_refinement. Something like this:

val move_refinement:
  #a:Type
  -> #p:(a -> Type)
  -> l:list a{forall z. FStar.List.Tot.mem z l ==> p z}
  -> Tot (l':(list (x:a{p x})){l' = l})

Hope this helps.

[VincentCheval]

So with the following declaration

val lemma_move_refinement_length:
  #a:Type
  -> #p:(a -> Type)
  -> l:list a{forall z. FStar.List.Tot.mem z l ==> p z}
  -> Tot (u:unit{ List.Tot.length (move_refinement #a #p l) = List.Tot.length l})

I ran the two assertions (1) and (2)

1) I obtain the error Proof_tools.fst(53,6-53,109): assertion failed with the following implementation

let rec lemma_move_refinement_length (a:Type) (p:(a -> Type)) l = match l with
  | [] -> ()
  | hd::tl ->
      assert (FStar.List.Tot.length (hd::move_refinement tl) = 1+ FStar.List.Tot.length (move_refinement tl));
      lemma_move_refinement_length #a #p tl

2) I obtain two errors Proof_tools.fst(50,66-55,43): Patterns are incomplete and Proof_tools.fst(53,6-53,112): assertion failed with the implementation of the other assert:

let rec lemma_move_refinement_length (a:Type) (p:(a -> Type)) l = match l with
  | [] -> ()
  | hd::tl ->
      assert (FStar.List.Tot.length (move_refinement (hd::tl)) = FStar.List.Tot.length (hd::move_refinement tl));
      lemma_move_refinement_length #a #p tl

With your second solution I obtain two errors once again. The code is as follows:

val move_refinement:
  #a:Type
  -> #p:(a -> Type)
  -> l:list a{forall z. FStar.List.Tot.mem z l ==> p z}
  -> Tot (l':(list (x:a{p x})){ l = l' })

let rec move_refinement (a:Type) (p:(a -> Type)) l = match l with
  | [] -> []
  | hd::tl -> hd::(move_refinement #a #p tl)

I have the errors Proof_tools.fst(36,32-36,33): Subtyping check failed; expected type (U24576 a p l l'); got type l:(list a){(forall (z). ((mem z l) ==> (p z)))} and Proof_tools.fst(39,10-39,12): Subtyping check failed; expected type l':(list x:a{(p x)}){(l = l')}; got type (list x:a{(p x)}). The character 36,32-36,33 corresponds to the l in the line -> Tot (l':(list (x:a{p x})){ l = l' }). The characters 39,10-39-12 corresponds to the second [] in the line | [] -> []

Thanks for the help 😊

Vincent

[catalin-hritcu]

There are a couple of F* problems here. First, the nil case failing is a bug I've filed separately as #466. For the cons case the equalities above should be provable, and in fact they are provable as lemmas. Moreover, calling these lemmas makes the whole proof go through:

val eq1 :   #a:Type
  -> #p:(a -> Type)
  -> hd:a{p hd} -> tl:(list a){forall z. mem z tl ==> p z} ->
     Lemma (requires True)
            (ensures (length (move_refinement #a #p (hd::tl)) =
                      length (hd::move_refinement #a #p tl)))
let eq1 hd tl = ()

val eq2 :   #a:Type
  -> #p:(a -> Type)
  -> hd:a{p hd} -> tl:(list a){forall z. mem z tl ==> p z} ->
     Lemma (requires True)
            (ensures (length (hd::move_refinement #a #p tl) =
                      1+length (move_refinement #a #p tl)))
let eq2 hd tl = ()

val lemma_move_refinement_length:
  #a:Type
  -> #p:(a -> Type)
  -> l:(list a){forall z. mem z l ==> p z}
  -> Lemma (requires (True))
           (ensures ((length l) = (length (move_refinement #a #p l))))
let rec lemma_move_refinement_length (a:Type) (p:(a -> Type)) l =
  match l with
  | [] -> admit()
  | hd::tl ->
     (* for some obscure reasons these assertions fail *)
     (* assert(length (hd::move_refinement #a #p tl) = *)
     (*      1+length (move_refinement #a #p tl)); *)
     (* assert(length (hd::move_refinement #a #p tl) = *)
     (*                  1+length (move_refinement #a #p tl)); *)
     (* but we can still call lemmas to make this work*)
     eq1 #a #p hd tl;
     eq2 #a #p hd tl;
     lemma_move_refinement_length #a #p tl

Still it's a complete mystery why the asserts would fail. They're supposed to help the SMT solver instantiate the forall z. mem z tl ==> p z quantifier in the refinement on l.

[vkanne-msft]

Can reproduce still

$ fstar examples/bug-reports/bug463a.fst
.\examples/bug-reports/bug463a.fst(7,14-7,22) : Error
Identifier not found: [Precedes]

$ fstar examples/bug-reports/bug463b.fst
.\examples/bug-reports/bug463b.fst(11,25-11,26) : Error
Inconsistent implicit argument annotation on argument a#245

[s-zanella]

@vkanne-msft: Those errors are unrelated to the original issue. After fixing them, the examples now typecheck, so this seems fixed now.

Closing.