解決平等/不平等的目標，COQ代碼

Val.shru（Val.and一（Vint的B））（Vint的C）= Vint的？ 3434/\？3434 <> d
Val.shru（Val.and一個（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.

感謝，

來源

2016-09-14 saeed M

你有一個引理指出形狀的任何條款'Val.shru foo'可以改寫成一個'Vint酒吧'？這裏的主要問題是，你需要展示'e'來證明你的目標的左手邊。 – Vinz

如果你可以構造（在下面的例子中i0）int類型的值，那麼這個引理不成立：

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.

來源

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 –

我該如何擺脫目標中的存在數字？ –

解決平等/不平等的目標，COQ代碼

回答

相關問題