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

Как я могу доказать, что эти два утверждения равны:Решая равенство/неравенство в цели, Кок код

Val.shru (Val.and а (Vint б)) (Vint с) = Vint? 3434/\? 3434 <> d
Val.shru (Val.and а (Vint б)) (Vint с) <> 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.

Спасибо,

источник

2016-09-14 saeed M

У вас есть лемма о том, что любой член формы 'Val.shru Foo' можно переписать в 'Vint bar'? Основная проблема здесь в том, что вам нужно выставить 'e' с равенством, чтобы доказать левую сторону вашей цели. – Vinz

Если вы можете построить значение типа 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 return 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.

источник

2016-09-14 08:54:46

Спасибо, ты прав. Я помещаю правильные ограничения на переменную сдвига и удостоверяюсь, что мы не возвращаем Vundef. Я развернулся и дошел до этого момента: –

H0: Vint (Int.shru (Int.and ab) c) <> Vint d ______________________________________ (1/1) Vint (Int.shru (Int.and ab) c) = Vint? 3443/\? 3443 <> d –

Как я могу как-то избавиться от экзистенциального числа в цели? –

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

ответ

Смежные вопросы