Решая равенство / неравенство в цели, код Coq

Question

Как я могу доказать, что эти два утверждения равны:

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

Концепция довольно проста, но застряла в поиске правильной тактики для ее решения. Это на самом деле лемма, которую я собираюсь доказать:

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.

Спасибо,

Answer 1

Если вы можете построить значение типа int (i0 в приведенном ниже примере), то эта лемма не выполняется:

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.

Есть как минимум две причины:

• Val.and а также Val.shru вернуть Vundef для всех аргументов, которые не являются Vint (это пример принципа GIGO);
• также вы не можете сдвинуть биты слишком далеко в C - результат не определен (это о Val.shru).

Что касается модифицированной леммы, которую вы упомянули в своем комментарии, просто reflexivity сделал бы:

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.