Bugs in TIP-to-Isabelle translation

[moajohansson]

Omar Montano Rivas has tested the TIP-to-Isabelle translation and found a number of bugs:

He also wishes to have a pass which translates properties to Isabelle with Frees instead of Vars (i.e. x not ?x).

-- Variable names are not translated properly to Isabelle/HOL as they sometimes clash with the ASCII representation of HOL constants. e.g. 'EX'
, 'o', etc. For example, the following definition is not accepted by the Isabelle outer syntax parser. The culprit is the name of the variable 'o' in the last equation of the definition. A potential solution would be to just rename the variable 'o' to some new fresh variable.

fun minus :: "Nat => Nat => Integer" where
"minus (Z) (Z) = P Z"
| "minus (Z) (S n) = N n"
| "minus (S m) (Z) = P (S m)"
| "minus (S m) (S o) = minus m o"

-- Identifiers in SMT files such as '1' are not properly translated into Isabelle/HOL. e.g.

fun 1 :: "Nat" where
"1 = S Z"

A potential solution would be to use the definition command using a proper identifier. e.g.

definition id1 :: "Nat" ("1") where
[simp]: "id1 = S Z"

Here we use the fresh identifier 'id1' and add it to Isabelle/HOL's simpset to simulate the fun command. An alternative would be to use a syntax translation.

-- Constants with non-functional type are not properly translated to Isabelle/HOL as fun does not support the definition of functions with atomic type (Probably a syntax translation or the definition command would be more suitable). e.g.

fun one :: "Nat" where
"one = S Z"

I think the previous suggested solution would work here.

-- A harder problem to fix is that some definition translations, can not be proved to terminate automatically by fun such as:

fun interleave :: "'a list => 'a list => 'a list" where
"interleave (nil2) y = y"
| "interleave (cons2 z xs) y = cons2 z (interleave y xs)"

Here it occurs to me to make a call to 'isabelle_process' to see if fun can handle the definition. If not, the definition can be phrased with the 'function' command to give it a try to the size_change automatic method, which in this case solves the pending goals.

function (sequential) interleave :: "'a list => 'a list => 'a list" where
"interleave (nil2) y = y"
| "interleave (cons2 z xs) y = cons2 z (interleave y xs)"
by pat_completeness auto
termination by size_change

Of course this will not work in all cases such as:

function (sequential) weirdconcat :: "('a list) list => 'a list" where
"weirdconcat (nil2) = nil2"
| "weirdconcat (cons2 (nil2) xss) = weirdconcat xss"
| "weirdconcat (cons2 (cons2 z xs) xss) =
cons2 z (weirdconcat (cons2 xs xss))"
by pat_completeness auto
termination by size_change

The 'relation' method can be used for such cases but I think it would be more difficult to come up with the decreasing measure automatically. One last think that can be done and will work on most cases is to use partiality. For example, if lexicographic order and size_change fail, instead making the translation like this:

fun m :: "int => int" where
"m x = (if x > 100 then x - 10 else m (m (x + 11)))"

theorem x0 :
"!! (n :: int) . ((n <= 100) ==> ((m n) = 91))"
by induct_auto_astar

We can do it with the equivalent (where m is partial and terminates under n ("m_dom n" holds)):

function m :: "int => int" where
"m x = (if x > 100 then x - 10 else m (m (x + 11)))"
by pat_completeness auto

theorem x0 :
"!! (n :: int) . m_dom n ⟹ ((n <= 100) ==> ((m n) = 91))"

-- Other problem is not produced by the translator itself but by the smt2 file. e.g. the file tip2015/list_z_elem.smt2 only contains "(check-sat)". This can be just me not downloading an updated version of the repository.

-- Another one is not the fault of the translator because Isabelle does not support non-linear datatypes. e.g polyrec_seq_index.smt2 file produces.

datatype 'a list = nil2 | cons2 "'a" "'a list"
datatype ('a, 'b) Pair = Pair2 "'a" "'b"
datatype 'a Maybe = Nothing | Just "'a"
datatype 'a Seq = Nil2 | Cons2 "'a" "(('a, ('a Maybe)) Pair) Seq"

-- I can see the translator uses partiality to some extend with the file propositional_AndCommutative.smt2 but some errors are produced. My first guess is that non-constructor patterns are used in definitions:

e.g.

models ( p q) y = models2 q (models p y)"

[danr]

Thanks! Here are my comments:

-- Variable names are not translated properly to Isabelle/HOL as they sometimes clash with the ASCII representation of HOL constants. e.g. 'EX'
, 'o', etc. For example, the following definition is not accepted by the Isabelle outer syntax parser. The culprit is the name of the variable 'o' in the last equation of the definition. A potential solution would be to just rename the variable 'o' to some new fresh variable.

fun minus :: "Nat => Nat => Integer" where
"minus (Z) (Z) = P Z"
| "minus (Z) (S n) = N n"
| "minus (S m) (Z) = P (S m)"
| "minus (S m) (S o) = minus m o"

You can change this in the keyword list

tools/tip-lib/src/Tip/Pretty/Isabelle.hs

Line 230 in 27784ac

isabelleKeywords :: [String]

-- Identifiers in SMT files such as '1' are not properly translated into Isabelle/HOL. e.g.

fun 1 :: "Nat" where
"1 = S Z"

A potential solution would be to use the definition command using a proper identifier. e.g.

definition id1 :: "Nat" ("1") where
[simp]: "id1 = S Z"

Here we use the fresh identifier 'id1' and add it to Isabelle/HOL's simpset to simulate the fun command. An alternative would be to use a syntax translation.

There is some code to dodge funky identifiers in the why3 pretty printer. It could be adapted for Isabelle:

tools/tip-lib/src/Tip/Pretty/Why3.hs

Line 22 in 27784ac

instance PrettyVar a => PrettyVar (Why3Var a) where

-- Constants with non-functional type are not properly translated to Isabelle/HOL as fun does not support the definition of functions with atomic type (Probably a syntax translation or the definition command would be more suitable). e.g.

fun one :: "Nat" where
"one = S Z"

I think the previous suggested solution would work here.

Just change fun to it to definition here then:

tools/tip-lib/src/Tip/Pretty/Isabelle.hs

Line 119 in 27784ac

where (header,termination) | null fns = ("fun",empty)

-- Other problem is not produced by the translator itself but by the smt2 file. e.g. the file tip2015/list_z_elem.smt2 only contains "(check-sat)". This can be just me not downloading an updated version of the repository.

This is an error in the benchmarks
https://github.com/tip-org/benchmarks/blob/master/benchmarks/tip2015/list_z_elem.smt2

-- I can see the translator uses partiality to some extend with the file propositional_AndCommutative.smt2 but some errors are produced. My first guess is that non-constructor patterns are used in definitions:

e.g.

models ( p q) y = models2 q (models p y)"

This is an error in the handling of identifiers. The identifier is simply a &, which is renamed
to an empty string.
https://github.com/tip-org/benchmarks/blob/master/benchmarks/tip2015/propositional_AndCommutative.smt2#L69

Using the method talked about earlier about the "why3 renamer" would help here.

[moajohansson]

There is now an option to remove the explicit top-level forall quantifiers in Isabelle, and one to leave them in. See:
tip --isabelle
tip --isabelle-explicit-forall

[Warbo]

I've also run into some of these issues.

I've managed to avoid the name clashes because I'm already hex-encoding all names prior to translation: this lets me decode back to exactly the same name after processing, rather than mangling special characters :)

Regarding Moa/Omar's function/size_change idea, I've tried this on every failing definition from the whole TIP benchmark and found that interleave is the only one it works for. In particular, the following functions (and all their alpha-equivalent copies) can't be show to terminate by fun or size_change:

tip2015/sort_MSortBU2Count.smt2merging - bu2
tip2015/tree_Flatten3.smt2 - flatten3
tip2015/tree_Flatten1.smt2 - flatten1
tip2015/sort_HSortCount.smt2 - hmerging
tip2015/sort_BubSortCount.smt2 - bubsort
tip2015/mccarthy91_M1.smt2 - m
tip2015/list_weird_concat_map_bind.smt2 - weird_concat
tip2015/mod_same.smt2 - mod2
tip2015/sort_BSortCount.smt2 - bmerge
tip2015/sort_HSortCount.smt2 - toList
tip2015/sort_QSortCount.smt2 - qsort

The suggestion about changing fun to definition for nullary values works fine for all such values.

[Warbo]

Another problem I've come across is let expressions not being translated correctly. For example, the ssort function from tip2015/sort_SSortCount.smt2:

(define-fun-rec ssort ((x (list CustomInt))) (list CustomInt) (match x (case nil (as nil (list CustomInt))) (case (cons y ys) (let ((m (ssort_minimum y ys))) (cons m (ssort (delete m x)))))))

This gets translated to the following Isabelle (I've decoded and mangled the names for clarity):

fun tip2015sort_SSortCountsmt2ssort :: "int
                                                                                   grammarspackrat_unambigPackratsmt2list =>
                                                                                 int
                                                                                   grammarspackrat_unambigPackratsmt2list" where
"tip2015sort_SSortCountsmt2ssort
   (grammarspackrat_unambigPackratsmt2nil) =
   grammarspackrat_unambigPackratsmt2nil"
| "tip2015sort_SSortCountsmt2ssort
     (grammarspackrat_unambigPackratsmt2cons localy
                                                                                             localys) =
     let localm :: int =
       tip2015sort_SSortCountsmt2ssort_minimum
         localy localys
     in grammarspackrat_unambigPackratsmt2cons
          localm
          (tip2015sort_SSortCountsmt2ssort
             (tip2015list_SelectPermutationssmt2zdelete
                localm
                (grammarspackrat_unambigPackratsmt2cons
                   localy localys)))"

Loading a theory containing this definition (in isabelle console) gives me the following error:

*** Inner syntax error (line 1887 of "/home/chris/DELETEME/isa/C.thy")
*** at "let localm :: int = tip2015sort_SSortCountsmt2ssort_minimum localy
***      localys in grammarspackrat_unambigPackratsmt2cons localm (
***      tip2015sort_SSortCountsmt2ssort (
***      tip2015list_SelectPermutationssmt2zdelete localm (
***      grammarspackrat_unambigPackratsmt2cons localy localys ) ) )"
*** Failed to parse prop
*** At command "fun" (line 1877 of "/home/chris/DELETEME/isa/C.thy")
Exception- TOPLEVEL_ERROR raised

This affects the following definitions:

tip2015/sort_SSortCount.smt2 - ssort
isaplanner/prop_12.smt2 - map2
tip2015/sort_NMSortTDCount.smt2 - nmsorttd
tip2015/subst_SubstFreeNo.smt2 - subst
tip2015/sort_MSortTDCount.smt2 - msorttd

[moajohansson]

Hi Chris,

Thanks for reporting these bugs. The TIP -> Isabelle translator is not yet complete, and let-expressions were probably never supported (Airini who worked on this latest can confirm/comment on this). Also, it's probably not been tested towards the latest version of Isabelle (2016-2), although I'm not sure if that causes any of your problems.

Unfortunately, I do not have time to fix this myself right now (I'm on parental leave) and the project is currently short on other developers. If you want to add/fix these features (or anything else) yourself, you are most welcome, and we'd be happy to include such extensions and fixes. I'll try to answer any questions as best I can via email, bearing in mind that there might be a delay in response right now.

[Warbo]

Hi Moa, I'm not blocked by any of this stuff so there's no problem; I'm mostly commenting/raising these things so they're written down somewhere.

In particular, I'm not too knowledgeable about Isabelle or (Poly)ML, so I've mostly just been playing, for reproduction and comparisons :)

[Warbo]

I've just taken another look at these issues, and it looks like I can avoid all the problems I was hitting by doing the following:

• Alpha-rename all local variables before translation. I'm just naming them local-1, local-2, etc.
• Encode all definition names before translation. I'm just hex-encoding the ASCII, and prefixing with the word global. This makes it less obvious what the Isabelle is saying, but we can just send any definitions, output, error messages, etc. through a hex decoder to read them.
• Replace fun with definition, as mentioned above, for nullary definitions.
• Replace fun with function for all other definitions, and use sorry for the termination and exhaustiveness proofs. Isabelle seems to accept this, although any non-exhaustive definitions cause warnings to appear (on standard out rather than standard error! Gah!)
• The syntax errors I was getting for case and let seem to be fixed if we wrap those expressions in parentheses. Just goes to show that everyone should be using s-expressions after all ;)

I'm currently adding in parentheses with a post-processing script and a hard-coded list of affected names. Now that I know it works, I'm tempted to implement the fix here; although I'm currently pinned to an old revision, so it might not merge nicely.

[Warbo]

I've made a few commits with the changes I've made:

• https://github.com/Warbo/tools/tree/isabelle-nullary-defs uses definition instead of fun or function
• https://github.com/Warbo/tools/tree/isabelle-parentheses always puts parentheses around let and case
• https://github.com/Warbo/tools/tree/isabelle-sorry-proofs uses sorry for all proofs
• https://github.com/Warbo/tools/tree/tebenchmark-fixes includes all of the above

It looks like the only outstanding thing is the invalid type from polyrec, and the functions which depend on it. I'm stripping these out with a preprocessor before translation.

[Warbo]

Can confirm the generated code is accepted by Isabelle, as long as the polyrec stuff is stripped out (which (like everything) is easier to do when it's in s-expression form).

One thing to keep in mind is that Isabelle seems to be doing something in call-by-value order (evaluation? who knows...) when reading function definitions. I ran into this because I had a definition of division something like this:

customDivide x y = ifThenElse (y > x) zero (succ (customDivide (x - y) y))

The problem is that ifThenElse was a normal function; under call-by-need (i.e. translating to Haskell) this definition is fine; but it causes Isabelle to hang with 100% CPU. My guess is that it's trying to evaluate or something using call-by-value, in which case all arguments to ifThenElse will be evaluated first, including the recursive case, and hence this definition diverges.

I worked around this by using a (match (y > 0) (case True zero) (case False ...)) which seems to get delayed appropriately since Isabelle accepts it without issue.