в Изабель, какой формат цели требуется для совместной монетизации - PullRequest
Новая
       5

в Изабель, какой формат цели требуется для совместной монетизации

2 голосов
/ 05 февраля 2020

Привет, я новичок, пытающийся научиться использовать коиндукцию в Изабель. Я смотрю на HOL / Datatype_Examples / Process.thy (Андрей Попеску) 2012. Начиная с 2019 года, Изабель значительно улучшилась (и не благодаря личным навыкам), я упростила доказательства, но до сих пор не могу понять, почему они решили сделать первый шаг.

Рабочее упрощенное доказательство: 

lemma solution_PROC[simp]: "solution sys (PROC p) = p"
proof-
  {fix q assume "q = solution sys (PROC p)" (* How did they know to do this! *)
   hence "p = q"
   proof (coinduct rule: process.coinduct)
     case (Eq_process process process')
     then show ?case
       by simp 
   qed
 }
  thus ?thesis by metis
qed

Мой неудачный наивный подход был: 

lemma solution_PROCFail: " p  = solution sys (PROC p)"
proof (coinduct rule: process.coinduct) (* look up  process.coinduct and 
            you can see the extra goal forced by the misalignment*)  
  case Eq_process
  then show ?thesis  (* cannot solve*)
qed

Два вопроса:

  1. is синтаксис {fix q принимает «q = solution sys (PRO C p)» .....} старый синтаксис для локальной леммы?

И что более важно 2. Как я узнаю когда попробовать эту технику?

большое спасибо Дэвид

1 Ответ

1 голос
/ 06 февраля 2020

  1. Синтаксис эквивалентен 

    have ‹p = q› if ‹q = solution sys (PROC p)› for q
  using that by (coinduct rule: process.coinduct) simp

в 

{fix q assume "q = solution sys (PROC p)" (* How did they know to do this! *)
   hence "p = q"
   proof (coinduct rule: process.coinduct)
     case (Eq_process process process')
     then show ?case
       by simp 
   qed
 }

{} открывает новый блок (с переменными локалей и предположения локали), и предположить вводит локальное предположение. Блок экспортирует теорему вида ?q2 = solution sys (PROC p) ⟹ p = ?q2.

Вероятно, вам следует прочитать руководство по Isar (например, «Конкретная семантика, а не isar-ref»), чтобы узнать об этих очень полезных конструкциях.

Идея состоит в том, что вам нужно предположение, которое включает в себя предикатный предикат. Я бы описал эту технику как стандартный обходной путь в Изабель, так как (со) индукция иногда теряет связи между переменными. 

lemma solution_PROCFail: " p  = solution sys (PROC p)"
proof (coinduct rule: process.coinduct) (* look up  process.coinduct and 
        you can see the extra goal forced by the misalignment*)  
  case Eq_process
  then show ?thesis  (* cannot solve*)
qed

терпит неудачу, потому что случай / show генерируется мусор (это происходит, посмотрите на панель состояний).

...