Trivial proof without grind

[Julin S]

Hi.

I recently came across a snippet like this:

```
full_adder: THEORY
BEGIN
  a, b, cin: VAR bit

  % Auto-convert bit to nat when needed
  CONVERSION+ b2n

  fa_cout(a, b, cin) : bit =
    (a AND b) OR (b AND cin) OR (a AND cin)

  fa_sum(a, b, cin) : bit =
    (a XOR b) XOR cin

  fa_correct: LEMMA
    fa_sum(a, b, cin) = a + b + cin - 2 * fa_cout(a, b, cin)
END full_adder
```

(I suppose it has something to do with this: https://link.springer.com/content/pdf/10.1007/3-540-59047-1_53.pdf)

I was trying to prove the lemma without using `grind`.

How would we go about that?

I was just trying to get a hang of pvs rules.

I suppose we would need case analysis at some point?
Can `case` help?

[Paolo Masci]

Yes, after removing the universal quantifier (skeep) and expanding the relevant definitions, you can use (lift-if) to bring conditional statements to the top-level and then (split) to perform case analysis.

In each branch, you will probably need to use (flatten) and (assert) to perform simplifications and check if a branch is closed (i.e., proved).

Hope this helps. Feel free to post your solution here if you want to share it!

Paolo