semax_func_cons - не применяется тактика

Question

Я пытаюсь собрать доказательства для моих двух функций в доказательство для всей программы:

... 
Definition Vprog : varspecs := nil. 
Definition Gprog : funspecs := get_spec :: set_spec :: nil. 

Lemma body_get: semax_body Vprog Gprog f_get get_spec. 
Proof. 
... 
Qed. 

Lemma body_set: semax_body Vprog Gprog f_set set_spec. 
Proof. 
... 
Qed. 

Existing Instance NullExtension.Espec. 


Theorem all_funcs_correct: 
    semax_func Vprog Gprog (prog_funct prog) Gprog. 
Proof. 
semax_func_skipn. 
semax_func_cons body_get. 

Перед применением semax_func_cons тактики, у меня есть следующие цели:

1 subgoals, subgoal 1 (ID 3951) 

    ============================ 
    semax_func Vprog [get_spec; set_spec] 
    [(_get, Internal f_get); (_set, Internal f_set)] 
    [(_get, 
     WITH x : share * Z * (Z -> val) * val * val PRE [ 
     (_key, tint), (_rez, tint), (_arr, tptr tint)] 
     (let (p, varr) := x in 
     let (p0, vk) := p in 
     let (p1, arr) := p0 in 
     let (sh, k) := p1 in 
     PROP (0 <= k < 100; forall i : Z, 0 <= i < 100 -> is_int (arr i); 
     repr k vk) 
     LOCAL (`(eq vk) (eval_id _key); `(eq varr) (eval_id _arr); 
     `isptr (eval_id _arr)) 
     SEP (`(array_at tint sh arr 0 100) (eval_id _arr))) POST [tint] 
     (let (p, varr) := x in 
     let (p0, _) := p in 
     let (p1, arr) := p0 in 
     let (sh, k) := p1 in 
     `(array_at tint sh arr 0 100 varr) && local (`(eq (arr k)) retval))); 
    set_spec] 

Так что кажется разумным устранить f_get с моей проверенной леммой body_get. Почему тактика терпит неудачу?

Сообщение не помогает:

Toplevel input, characters 0-24: 
Error: No applicable tactic. 

Answer 1

Проблема заключается в спецификации списка аргументов.

• Он должен содержать только аргументы функции (не местные жителей)

• Он должен иметь аргументы в том же порядке, как и в функции C прототипе.

BTW, порядок функций в Gprog должен быть таким же, как порядок определений функций в c-файле.