如何用局部变量实例化变量（？8758）？

Question

我目前的证明状态：

 ...
 qu := 1 : Z
 ============================
  (array_at_ tint sh 0 100 (eval_id _busybits rho) *
   array_at tint sh (fun x : Z => Vint (Int.repr (keys m x))) 0 100
     (eval_id _keys rho) *
   array_at tint sh (fun x : Z => Vint (Int.repr (values m x))) 0 100
     (eval_id _values rho))%logic
  |-- !!(offset_val (Int.repr (sizeof tint * ?8758)) (eval_id _busybits rho) =
         force_val
           (sem_add_pi tint (eval_id _busybits rho) (eval_id _index rho)) /\
         0 <= ?8758 /\ ?8758 < 100 /\ Vint (Int.repr 1) = Vint (Int.repr 1))

我可以用任何整数实例化变量 ?8758:

instantiate (2:=1).

  (array_at_ tint sh 0 100 (eval_id _busybits rho) *
   array_at tint sh (fun x : Z => Vint (Int.repr (keys m x))) 0 100
     (eval_id _keys rho) *
   array_at tint sh (fun x : Z => Vint (Int.repr (values m x))) 0 100
     (eval_id _values rho))%logic
  |-- !!(offset_val (Int.repr (sizeof tint * 1)) (eval_id _busybits rho) =
         force_val
           (sem_add_pi tint (eval_id _busybits rho) (eval_id _index rho)) /\
         0 <= 1 /\ 1 < 100 /\ Vint (Int.repr 1) = Vint (Int.repr 1))

但是当我尝试用局部变量实例化它时：

instantiate (2:=qu).

我收到一条错误消息：

Toplevel input, characters 38-40:
Error: Instance is not well-typed in the environment of ?8758

为什么我不能用变量实例化它？

编辑：

instantiate (2:=1%Z).

工作方式与 (2:=1) 相同。

存在主义：（回应@Vinz）

Show Existentials.

Existential 1 =
?9091 : [Espec : OracleKind
         sh : share
         m : ArrMapZ
         key : Z
         val : Z
         vkey : Values.val
         vval : Values.val
         H : repr key vkey
         H0 : repr val vval
         H4 : writable_share sh
         Struct_env := abbreviate : type_id_env.type_id_env
         bbarg : name _busybits
         ksarg : name _keys
         valsarg : name _values
         karg : name _key
         startloc : name _start
         indexloc : name _index
         startloc0 : Values.val
         indexloc0 : Values.val
         Delta := abbreviate : tycontext
         MORE_COMMANDS := abbreviate : statement
         rho : environ
         H5 : None <> find_empty m (loop key) 99
         H1 : isptr (eval_id _busybits rho)
         H2 : isptr (eval_id _keys rho)
         H3 : isptr (eval_id _values rho)
         POSTCONDITION := abbreviate : ret_assert
         H6 : Vint
                (Int.repr
                   match find_empty m (loop key) 99 with
                   | Some x => x
                   | None => -1
                   end) = eval_id _index rho
         qu := 1 : Z
        |- (array_at_ tint sh 0 100 (eval_id _busybits rho) *
            array_at tint sh (fun x : Z => Vint (Int.repr (keys m x))) 0 100
              (eval_id _keys rho) *
            array_at tint sh (fun x : Z => Vint (Int.repr (values m x))) 0
              100 (eval_id _values rho))%logic
           |-- !!(offset_val (Int.repr (sizeof tint * ?8758))
                    (eval_id _busybits rho) =
                  force_val
                    (sem_add_pi tint (eval_id _busybits rho)
                       (eval_id _index rho)) /\
                  0 <= ?8758 /\ ?8758 < 100 /\ ?8759 = Vint (Int.repr 1))] 
Existential 2 =
?9089 : [Espec : OracleKind
         sh : share
         m : ArrMapZ
         key : Z
         val : Z
         vbb : Values.val
         vkeys : Values.val
         vvals : Values.val
         vkey : Values.val
         vval : Values.val
         H : repr key vkey
         H0 : repr val vval
         H1 : isptr vbb
         H2 : isptr vkeys
         H3 : isptr vvals
         H4 : writable_share sh
         Struct_env := abbreviate : type_id_env.type_id_env
         bbarg : name _busybits
         ksarg : name _keys
         valsarg : name _values
         karg : name _key
         startloc : name _start
         indexloc : name _index
         startloc0 : Values.val
         indexloc0 : Values.val
         vindex := Vint
                     (Int.repr
                        match find_empty m (loop key) 99 with
                        | Some x => x
                        | None => -1
                        end) : Values.val
         Delta := abbreviate : tycontext
         POSTCONDITION := abbreviate : ret_assert
         MORE_COMMANDS := abbreviate : statement
        |- semax Delta
             (PROP  (None <> find_empty m (loop key) 99)
              LOCAL  (`(eq vindex) (eval_id _index);
              `(eq vbb) (eval_id _busybits); `(eq vkeys) (eval_id _keys);
              `(eq vvals) (eval_id _values))
              SEP 
              (`(array_at tint sh
                   (upd
                      (fun x : Z =>
                       Vint (Int.repr (if busybits m x then 1 else 0))) 
                      ?8758 ?8759) 0 100)
                 (fun _ : lift_S (LiftEnviron mpred) => vbb);
              `(array_at tint sh (fun x : Z => Vint (Int.repr (keys m x))) 0
                  100 vkeys);
              `(array_at tint sh (fun x : Z => Vint (Int.repr (values m x)))
                  0 100 vvals)))
             (Ssequence
                (Sassign
                   (Ederef
                      (Ebinop Oadd (Etempvar _keys (tptr tint))
                         (Etempvar _index tint) (tptr tint)) tint)
                   (Etempvar _key tint)) MORE_COMMANDS) POSTCONDITION] 
Existential 3 =
?8759 : [Espec : OracleKind
         sh : share
         m : ArrMapZ
         key : Z
         val : Z
         vbb : Values.val
         vkeys : Values.val
         vvals : Values.val
         vkey : Values.val
         vval : Values.val
         H : repr key vkey
         H0 : repr val vval
         H1 : isptr vbb
         H2 : isptr vkeys
         H3 : isptr vvals
         H4 : writable_share sh
         Struct_env := abbreviate : type_id_env.type_id_env
         bbarg : name _busybits
         ksarg : name _keys
         valsarg : name _values
         karg : name _key
         startloc : name _start
         indexloc : name _index
         startloc0 : Values.val
         indexloc0 : Values.val
         vindex := Vint
                     (Int.repr
                        match find_empty m (loop key) 99 with
                        | Some x => x
                        | None => -1
                        end) : Values.val
         Delta := abbreviate : tycontext
         MORE_COMMANDS := abbreviate : statement |- 
        reptype tint] 
Existential 4 =
?8758 : [Espec : OracleKind
         sh : share
         m : ArrMapZ
         key : Z
         val : Z
         vbb : Values.val
         vkeys : Values.val
         vvals : Values.val
         vkey : Values.val
         vval : Values.val
         H : repr key vkey
         H0 : repr val vval
         H1 : isptr vbb
         H2 : isptr vkeys
         H3 : isptr vvals
         H4 : writable_share sh
         Struct_env := abbreviate : type_id_env.type_id_env
         bbarg : name _busybits
         ksarg : name _keys
         valsarg : name _values
         karg : name _key
         startloc : name _start
         indexloc : name _index
         startloc0 : Values.val
         indexloc0 : Values.val
         vindex := Vint
                     (Int.repr
                        match find_empty m (loop key) 99 with
                        | Some x => x
                        | None => -1
                        end) : Values.val
         Delta := abbreviate : tycontext
         MORE_COMMANDS := abbreviate : statement |- Z]

辅酶 8.4pl3

Answer 1

感谢您的反馈。我认为你的问题是你没有实例化正确的变量，但是你得到了实例化 ?8758 的副作用。如果您查看 Show Existentials 的输出，您会发现 ?8758 不是第二个变量而是第四个变量，而且第二个变量的类型令人毛骨悚然，而第四个变量的类型为 Z.

instantiate (4 := qu). 是否解决了您的问题？

Answer 2

我认为这里发生的是 qu 不在你的存在变量的上下文中。

你看，每次创建存在变量时，它都会继承当前上下文（a.k.a。环境）并且不能由包含不在该上下文中的变量的术语实例化。这是为了防止某些形式的循环推理，但我猜你的情况太严格了。

Goal forall P, exists x : False, P x -> False -> False.
Proof.
intros.
eexists.
intros H1 H2.
instantiate (1 := H2) in H1.
exact H2.
Qed.

您需要在创建存在之前定义qu。

如何用局部变量实例化变量（？8758）？

How to instantiate a variable (?8758) with a local variable?

coq

编辑：

存在主义：（回应@Vinz）