I am working on some exercises on Idris proofs and I keep running into the same problem in various exercises. I first describe the problem in general, and then I give a concrete example:
theorem: (some variables) -> (hypothesis using those variables) -> (proof goal)
Now suppose that I want to give the proof using case-splitting, and that in some cases the assignment of the variables makes the hypothesis false. This means that the situation can never occur, so the proof can continue. But how to tell this to Idris?
For example:
andb_true_elim_2 : (b, c: Bool) -> (b && c = True) -> c = True
andb_true_elim_2 True c prf = prf -- This is OK!
andb_true_elim_2 False c prf = ?hole -- This is the problem
As b is false, b && c = True evaluates to False = True, which is impossible, so there will never be a valid value for prf that reaches this case, so it is irrelevant.
How does one solve these kind of problems?
Thanks!
If you try to pattern match the proof with Refl, Idris will see that the it's impossible. You can then use the impossible keyword to tell Idris to not worry about it.
andb_true_elim_2 : (b, c: Bool) -> (b && c = True) -> c = True
andb_true_elim_2 True c prf = prf
andb_true_elim_2 False c Refl impossible