More suffices advice stuff

[HalflingHelper]

This goes back to the issue we discussed previously about suffices not showing the @ <> annotation.

The example below prompts:

/home/calvin/Documents/Programming/343/deduce/exercise.pf:17.5-17.33: 
suffices to prove:
        0 = foldr([], 0, +)

But I need to provide 0 = foldr(@[]<Nat>, 0, operator+) . The operator thing is new and I don't see it being an issue for what is covered in the course (and maybe something fixed with a better parser anyway). It's weird though that the TermInst fix didn't work for this case...

// I'm doing a bunch of a exercises as a way to hopefully find
// things we can improve

import List
import Nat

function sum(List<Nat>) -> Nat {
  sum(empty) = 0
  sum(node(n, ns)) = n + sum(ns)
}


theorem foldr_eq_sum : all ls : List<Nat>. sum(ls) = foldr(ls, 0, operator+)
proof
  induction List<Nat>
  case empty {
    suffices ? by definition sum
    ?
  }
  case node(a, d) {
    ?
  }
end

[jsiek]

Thank you! I'll look into this today.

[jsiek]

I've fixed the issue with operator +.

[jsiek]

The problem with [] is tricky... I think it's an interaction with the TermInst on foldr, which is causing the type checker to think it doesn't need to make the TermInst on [] explicit. But the TermInst on foldr doesn't get printed...

[HalflingHelper]

I see you made a change that at least fixes the issue, event though it's less concise - would it be worth looking into adding additional logic to reduce, and changing inference there?

For example adding this case to reduce() in TermInst annotates vars only when we reduce in suffices. Could we do a bit more to only setting inferred to False ?

case Var(loc2, TypeInst(), name):
        return TermInst(self.location, self.typeof, subject_red,
                        self.type_args, False)

(This is still more verbose than necessary, for example when using definition length on the goal length(node(1, node(1, empty))) we get 1 + length(node(1, @empty<Nat>)))

This doesn't change any of the existing error messages we test for though, except for the one you added for this foldr example.

[jsiek]

I just thought of yet another fix and pushed it. For the above example, the result is that [] gets the TermInst instead of foldr. The way it happens is that the term generated from the case pattern of the induction is type checked an extra time in synthesis mode which causes the TermInst to become explicit (not inferred).

[jsiek]

I think this new fix causes less verbosity in other situations.

[HalflingHelper]

It seems like your fix doesn't work for this scenario

theorem l1 : length(node(1, empty)) = 1
proof
  suffices ? by definition length 
  ?
end

/home/calvin/Documents/Programming/343/deduce/exercise.pf:10.3-10.34: 
suffices to prove:
        1 + length([]) = 1
/home/calvin/Documents/Programming/343/deduce/exercise.pf:11.3-11.4: incomplete proof
Goal:
        1 + length([]) = 1
Advice:
        To prove this equality, one of these statements might help:
                definition
                rewrite
                equations

Givens:

[HalflingHelper]

An option that can replace what you did, and also catches this length case is setting inferred to false when substituting a TermInst that is a direct argument of a Call that is also a TermInst

[jsiek]

Good, I was vaguely worried about this. This example shows that the "fix" needs to be applied to many more places. Basically, anywhere that we do substitution.

[jsiek]

I see what you're saying about substituting a TermInst. I think that leads to a simpler solution that what I was doing with type_synth_term.