0

How can I prove that these two statements are equal:

  1. Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d

  2. Val.shru (Val.and a (Vint b)) (Vint c) <> d

The concept is pretty simple but stuck in finding the right tactic to solve it. This is actually the Lemma I'm going to prove:

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

Lemma val_remains_int:
forall (a : val) (b c d: int),
(Val.shru (Val.and a (Vint b)) (Vint c)) <> (Vint d) ->
(exists (e : int), (Val.shru (Val.and a (Vint b)) (Vint c)) = (Vint e) /\ e <> d).

Proof.
  intros.
  eexists.
  ...
Admitted.

Thanks,

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
saeed M
  • 21
  • 7
  • Do you have a lemma stating that any term of the shape `Val.shru foo` can be rewritten into a `Vint bar` ? The main issue here is that you need to exhibit `e` with the equality to prove the left hand side of your goal. – Vinz Sep 14 '16 at 07:10

1 Answers1

0

If you can construct a value of type int (i0 in the example below), then this lemma does not hold:

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

Variable i0 : int.

Fact counter_example_to_val_remains_int:
  ~ forall (a : val) (b c d: int),
      (Val.shru (Val.and a (Vint b)) (Vint c)) <> (Vint d) ->
      (exists (e : int),
          (Val.shru (Val.and a (Vint b)) (Vint c)) = (Vint e)
        /\ e <> d).
Proof.
  intro H.
  assert (Vundef <> Vint i0) as H0 by easy.
  specialize (H Vundef i0 i0 i0 H0); clear H0.
  simpl in H.
  destruct H as (? & contra & _).
  discriminate contra.
Qed.

There are at least two reasons:

  • Val.and and Val.shru return Vundef for all arguments that are not Vint (it's an instance of the GIGO principle);
  • also you can't shift bits too far in C -- the result is undefined (this one is about Val.shru).

As for the modified lemma you mentioned in your comment, simple reflexivity would do:

Lemma val_remains_int: forall a b c d: int,
    Vint (Int.shru (Int.and a b) c) <> Vint d ->
    exists (e : int), Vint (Int.shru (Int.and a b) c) = Vint e /\ e <> d.
Proof.
  intros a b c d Hneq.
  eexists. split.
  - reflexivity.
  - intro Heq. subst. auto.
Qed.
Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • Thanks, you're right. I put the right constraints over shift variable and make sure that we are not returning Vundef. I unfolded and got to this point: – saeed M Sep 15 '16 at 03:04
  • H0 : Vint (Int.shru (Int.and a b) c) <> Vint d ______________________________________(1/1) Vint (Int.shru (Int.and a b) c) = Vint ?3443 /\ ?3443 <> d – saeed M Sep 15 '16 at 03:06
  • How can I somehow get rid of the existential number in the goal? – saeed M Sep 15 '16 at 03:09