Вопросы Теги

Как упростить индуктивный предикат с помощью оценки?

Способ иметь отдельную реализацию выглядит следующим образом. 

//inner_foo.h

template <typename T>
struct Foo
{
    void doSomething(T param);
};


//foo.tpp
#include "inner_foo.h"
template <typename T>
void Foo<T>::doSomething(T param)
{
    //implementation
}


//foo.h
#include <foo.tpp>

//main.cpp
#include <foo.h>

inner_foo имеет форвардные объявления. foo.tpp имеет реализацию и включает inner_foo.h; и foo.h будет иметь только одну строку, чтобы включить foo.tpp.

Во время компиляции содержимое foo.h копируется в foo.tpp, а затем весь файл копируется в foo.h после который он компилирует. Таким образом, ограничений нет, и именование согласовано в обмен на один дополнительный файл.

Я делаю это, потому что статические анализаторы для кода разбиваются, когда он не видит передовые объявления класса в * .tpp. Это раздражает при написании кода в любой среде IDE или с помощью YouCompleteMe или других.

1
задан Denis 3 March 2019 в 16:59
поделиться

1 ответ

Команда code_pred генерирует уравнения для class_roles, по одному для каждого выведенного режима, и values использует их. Теорема class_roles.equation показывает их все. Если вы хотите использовать их для доказательства своей леммы, вы должны сначала преобразовать цель или утверждение леммы так, чтобы появилась одна из сгенерированных констант class_role_.... Делать это вручную довольно громоздко.

Вы получите гораздо лучшую автоматизацию, если позволите компилятору предикатов выполнить это преобразование за вас. Поскольку лемма содержит универсально квантифицированные переменные (assoc1, assoc2, from и role), я рекомендую определить отрицание леммы как индуктивный предикат, так как отрицание превращает универсальный квантор в экзистенциальный, который моделируется свободной переменной в предположениях. Затем вы можете использовать метод доказательства eval для выполнения тяжелой работы: 

inductive foo where
  "foo" if 
  "class_roles associations Employee assoc1 from role"
  "class_roles associations Employee assoc2 from role"
  "assoc1 ≠ assoc2"

code_pred foo .

lemma class_roles_unique:
  assumes "class_roles associations Employee assoc1 from role"
    and "class_roles associations Employee assoc2 from role"
  shows "assoc1 = assoc2"
proof -
  have "¬ foo" by eval
  with assms show ?thesis by(simp add: foo.simps)
qed

Обратите внимание, что eval использует генерацию и оценку кода в PolyML, поэтому он вычисляет результат, а не доказывает его. То есть оценка не проверяется ядром Изабель. Связанный метод доказательства code_simp проходит через ядро, но он не работает "из коробки" в этом примере, потому что настройка кода для String.asciis_of_literals отсутствует в Isabelle2018.

Следующие леммы обеспечивают отсутствующие уравнения кода для литеральных строк, но code_simp очень медленны с литеральными строками (normalization немного быстрее, но также не проверяется ядром Изабель). 

definition dup_bit :: "bool ⇒ integer ⇒ integer" where
 "dup_bit b i = i + i + (if b then 1 else 0)"

lemma dup_bit_code [code]:
  "dup_bit True 0 = 1"
  "dup_bit False 0 = 0"
  "dup_bit True (Code_Numeral.Pos n) = Code_Numeral.Pos (num.Bit1 n)"
  "dup_bit False (Code_Numeral.Pos n) = Code_Numeral.Pos (num.Bit0 n)"
  "dup_bit True (Code_Numeral.Neg n) = - Code_Numeral.sub (num.Bit0 n) Num.One"
  "dup_bit False (Code_Numeral.Neg n) = Code_Numeral.Neg (num.Bit0 n)"
  by(simp_all add: dup_bit_def Code_Numeral.sub_def nat_of_num_add num_eq_iff)
    (metis diff_numeral_special(1) numeral_Bit0 numeral_plus_numeral sub_num_simps(2))

fun integer_of_bits :: "bool list ⇒ integer" where
  "integer_of_bits [] = 0"
| "integer_of_bits (b # bs) = dup_bit b (integer_of_bits bs)"

lemma asciis_of_literal_code [code]: 
  "String.asciis_of_literal (STR '''') = []"
  "String.asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) =
     integer_of_bits [b0, b1, b2, b3, b4, b5, b6] # String.asciis_of_literal s"
  including literal.lifting by(transfer; simp add: dup_bit_def; fail)+
0
ответ дан Andreas Lochbihler 3 March 2019 в 16:59
поделиться