Trying To Understand How to Make a Simple Proof

[zicklag]

Hey there!

I'm trying to understand how to use Kind to verify a simple bool proof.

I see in the example.kind2 you have a proof like this:

Bool.not_not_theorem (a: Bool) : (Equal Bool a (Bool.not (Bool.not a)))
Bool.not_not_theorem Bool.true  = (Equal.refl Bool Bool.true)
Bool.not_not_theorem Bool.false = (Equal.refl Bool Bool.false)

Those statements proof that "not not a == a", but only for Bool.true and Bool.false ( which are currently the only bools ), but what if we had, for instance, forgotten to the third line in the codeblock above, and therefore forgot to prove that "not not false == false".

Is there a way to prove that "not not a == a" for all Bools?

Can we make sure that we've exhaustively proven the statement against every constructible Bool?

[algebraic-dev]

We cannot make sure that we've exhaustively proven some statement currently. I'm trying to work on a implementation of coverage checker for Kind2 but I'm not sure when we are going to have it working.

[zicklag]

OK, cool, thanks. 👍