0

I'm proving this lemma:

Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.

Lemma test: forall (val1 val2: int), ((Vint val1) <> (Vint val2)) -> (Some (Val.cmp Ceq (Vint val1) (Vint val2)) = Some Vfalse).
Proof.

Admitted.

I've tried unfolding not, Val.cmp, ... and using rewrite over H but didn't go anywhere. Any help is appreciated.

Thanks

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
saeed M
  • 21
  • 7

1 Answers1

1

The original theorem that you had was false, unfortunately. The problem was that Val.cmp returns Vundef if one of the compared values is not an integer. Check the definition of cmp and cmp_bool here.

The new theorem that you have is true, but is not stated in a very useful form. It is better to state it like this:

forall val1 val2, val1 <> val2 -> Val.cmp Ceq (Vint val1) (Vint val2) = Vfalse

Having the Vint and Some constructors around the equalities does not change the truth value of your theorem, but makes it harder to apply in most concrete settings. This result should follow by unfolding Val.cmp, Val.cmp_bool, and Int.cmp, and rewriting with Int.eq_false.

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • good point. I made an edit to the lemma. Can you look at it again? – saeed M Oct 01 '16 at 23:45
  • `val1` and `val2` aren't of type `int`. They are of type `val`. So I can't use Int.eq_false. – saeed M Oct 02 '16 at 00:04
  • No, `val1` and `val2` _are_ of type `int` in the statement that I wrote down. It is `Vint val1` and `Vint val2` that are of type `val`. – Arthur Azevedo De Amorim Oct 02 '16 at 00:06
  • I meant in the one that I need to prove are of type `val`. – saeed M Oct 02 '16 at 00:07
  • Your `test` lemma is also quantifying over `val1` and `val2` of type `int`... Maybe you wanted to prove something else? – Arthur Azevedo De Amorim Oct 02 '16 at 00:09
  • `VAL1` and `VAL2` here `VAL1 <> VAL2` are of type `val`. The unequality is over type `val` not `int`. – saeed M Oct 02 '16 at 00:13
  • I think you're referring to the fact that your statement says `Vint val1 <> Vint val2` instead of `val1 <> val2`, as I had on mine. If that's the case, all you have to do is use the `Vint val1 <> Vint val2` hypothesis to prove `val1 <> val2`, as needed by `Int.eq_false`. You can probably do it with `assert (val1 <> val2). { congruence. }`, after introducing `Vint val1 <> Vint val2`. – Arthur Azevedo De Amorim Oct 02 '16 at 00:19