Beginner issue with 'Could not prove termination of this recursive call'

[alex4482]

Hello. I am new to F* and i have some code in Haskell that i am trying to 'translate' to F* (dont ask why). I read and skimmed and read again parts of the tutorial webside but i saw that some parts are not yet written.
Anyway, this is a function i wrote and tested on the tutorial website verifier. It's purpose is to receive a list of 'literals' (a literal is a type i defined, Var string | NotVar string, where the string is the name of the 'literal', Var means it's positive, NotVar means it's negative) and if i find 2 literals in the list, one positive and one negative, but with the same 'name', remove them.
But it keeps giving me the error 'Could not prove termination of this recursive call'. And i dont know what to change to prove termination.

Sorry i am not sure how to indent the lines for readability.

let rec removeLiteralsWithBothPolarities literals : Tot (res: list literal {subset res literals}) (decreases literals) =
match literals with
| [] -> []
| lit :: otherLiterals -> let negatedLit = negateLit lit in
let doesContain = contains negatedLit otherLiterals in
if doesContain
then
removeLiteralsWithBothPolarities (List.Tot.filter (fun (x: literal) -> not (x = negatedLit || x = lit)) otherLiterals)
else
let newOtherLiterals = removeLiteralsWithBothPolarities otherLiterals in
lit :: newOtherLiterals

[nikswamy]

This section of the tutorial provides an introduction to termination proofs: http://fstar-lang.org/tutorial/book/part1/part1_termination.html#proofs-of-termination

This part shows one example of non-structural recursion: http://fstar-lang.org/tutorial/book/part1/part1_quicksort.html#proving-sort-correct

More advanced topics about termination are here: http://fstar-lang.org/tutorial/book/part2/part2_well_founded.html#well-founded-relations-and-termination

For your example:

When you write decreases literals you're telling F* that this function is structurally recursive on literals, i.e., every recursive call is on a strict sub-term of the parameter literals. That's not true here, in particular in the first recursive call in the then branch. What is actually decreasing on each recursive call?

I'll let you think about the answer but if you're stuck, please ask again.

[alex4482]

hi. Thanks a lot for replying so fast. I have read the introduction to termination proofs and seen some of the examples.
I forgot to add a NOT in the code when i copied it, in the then branch, and i added it now.

From my understanding, the 'filter' bit that i wrote should remove all elements from the list that are NEITHER equal to 'negatedLit' NOR 'lit'. Hope i got that right.

And I know for certain that there is at least one 'negatedLit' in the list, so i should have the guarantee that the list is decreasing. I have been trying for 2 days to rewrite that function to work but to no avail, thinking that was missing some syntax elements or didnt understand this behavior enough.

[nikswamy]

i should have the guarantee that the list is decreasing

I think you mean that the length of the list is decreasing. you'll have to prove that filter's output list is no longer than its input.

[nikswamy]

let literal = bool
let negateLit = not
module L = FStar.List.Tot
let rec filter_length (#a:_) (f:a -> bool) (l:list a)
  : Lemma (L.length (L.filter f l) <= L.length l)
  = admit() (* prove this *)

let rec removeLiteralsWithBothPolarities literals
  : Tot (res: list literal (* { subset res literals } ... I'll leave that to you *))
        (decreases (L.length literals))
  = match literals with
    | [] -> []
    | lit :: otherLiterals ->
      let negatedLit = negateLit lit in
      let doesContain = L.contains negatedLit otherLiterals in
      if doesContain
      then let fil =(fun (x: literal) -> (x = negatedLit || x = lit)) in
           filter_length fil otherLiterals;
           removeLiteralsWithBothPolarities
             (L.filter fil otherLiterals)
      else
        let newOtherLiterals = removeLiteralsWithBothPolarities otherLiterals in
        lit :: newOtherLiterals

[alex4482]

WOOW I DIDNT THINK I HAD TO PUT 'decreases (L.length literals)'

well i hope i can manage to make it work after reading your code. THANKS A LOT.
But while trying other approaches i found another error i have no ideea how to interpret.

This is the function. (my own version of the above 'filter')
let rec removeLiteralFromList (func: literal -> bool) (literals: list literal {L.length literals > 0})
: Tot (res: list literal {L.length res < L.length literals && L.subset res literals}) =
if L.tl literals = []
then []
else
let head = L.hd literals in
let tail = L.tl literals in
if func head
then removeLiteralFromList func tail
else head :: removeLiteralFromList func tail

And here is the error:
Subtyping check failed; expected type res:
Prims.list OtherFunctions.literal
{ length res < length literals &&
.subset res literals }; got type res:
Prims.list OtherFunctions.literal
{ length res < length tail &&
Fsubset res tail }:

Do i have to make a Lemma and use that 'admit' to prove that 'tail is part of literals'?

[hacklex]

Keep in mind that every admit() and assume are both axioms.

One wrong fact assumption easily leads to proving False, which means full logical collapse, aka "every possible statement is true".

So, no, never use admit() in the final version of your code.

assumes and admits are merely debugging tools used for:

• Sliding admit() down your proof to find where is the first statement FStar is not fine with
• Skipping trivial details to finish the big picture of your system -- and you're supposed to fill the admitted gaps with actual proofs later
• providing mocks to test your library