解决平等/不平等的目标，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代码

回答

相关问题