How to prove lemmas with partial functions?

Question

Could you suggest how to prove this simple lemma?

datatype val = BVal bool | IVal int

lemma the_unif:
"the (x :: val option) = the (y :: val option) ⟹ x = y"
  apply (induct x; induct y)
  apply simp

I'm trying to prove it by induction, but I stuck on case ⋀option. the None = the (Some option) ⟹ None = Some option.

option may be equal either to BVal x or to IVal x. It will never be equal to the None. So the assumption will always have false value in this cases.

UPDATE:

I can prove the following lemma:

lemma the_none_ne_the_some:
  "x ≠ the None ⟹ the None ≠ the (Some x)"
  by simp

So I guess, that the first lemma can be proven too.

The general lemma can't be proven, because it really doesn't hold:

lemma the_unif:
  "the x = the y ⟹ x = y"

A counterexample:

x = None
y = Some (the None)

But in the first lemma neither x, nor y can be equal to Some (the None). So I can't find a counterexample for the first lemma.

Oh, I've got it, I can prove the following lemma:

lemma the_unif:
  "x ≠ Some (the None) ⟹ y ≠ Some (the None) ⟹ the x = the y ⟹ x = y"
  by (induct x; induct y; simp)

But how to prove that x :: val option implies x ≠ Some (the None)?

UPDATE 2:

It seems that it is impossible to prove that:

lemma val_not_the_none:
  "x = BVal b ∨ x = IVal i ⟹ x ≠ the None"

But if the lemmas doesn't hold then they must have a counterexamples? Could you provide one?

larsrh larsrh · Accepted Answer · 2017-07-19T08:19:52

What you are trying to prove simply does not hold. the None is unspecified – in essence, there's nothing non-trivial you can prove about it. Hence, saying "it will never be equal to the None" is vacuous, because you don't know what the None is.

How to prove lemmas with partial functions?

1 Answers