Coq: переписать с «forall» в гипотезе или цели - PullRequest
Новая
       9

Coq: переписать с «forall» в гипотезе или цели

0 голосов
/ 02 октября 2018

Я доказал «правильность» обратной функции на полиморфных Списках в Coq.Следующее доказательство работает отлично, но у меня есть несколько вопросов о том, как работает тактика rewrite .

Вот код: 

Require Export Coq.Lists.List.
Import ListNotations.

Fixpoint rev {T:Type} (l:list T) : list T :=
  match l with
  | nil    => nil
  | h :: t => rev t ++ [h]
  end.

(* Prove rev_acc equal to above naive implementation. *)
Fixpoint rev_acc {T:Type} (l acc:list T) : list T :=
  match l with
  | nil => acc
  | h :: t => rev_acc t (h::acc)
  end.

Theorem app_assoc : forall  (T:Type) (l1 l2 l3 : list T),
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
Admitted.

Theorem rev_acc_correct : forall (T:Type) (l k :list T),
  rev l ++ k = rev_acc l k.
Proof.
  intros T l.
  induction l as [ | h l' IHl' ].
  - reflexivity.
  - simpl. 
    intro k.
    (* Why is "intro k" required for "rewrite -> app_assoc" *)
    (* But "rewrite -> IHl'" works regardless of "intro k".  *)
    (* generalize (rev l'), [h], k. *)
    rewrite -> app_assoc.
    simpl.
    rewrite -> IHl'.
    reflexivity.
Qed.

В индуктивном шагедоказательство для rev_acc_correct , если я пропущу intro k , а затем переписать с помощью app_assoc , жалуется, что не может найти подходящий подтерм. 

Found no subterm matching "(?M1058 ++ ?M1059) ++ ?M1060" in the current goal.

Здесь я предполагаю, что ? перед именами заполнителей означают, что термины ограничены, в данном случае они имеют тип Список T для некоторого типа T ;и поскольку rev l ' и [h] в воротах являются экземплярами списка T , можно ожидать совпадения в воротах.

С другой стороны, переписывание с индуктивной гипотезой ( rewrite -> IHl ') вместо app_assoc проходит без необходимости intro k до этого.

Мне кажется, что такое поведение rewrite немного сбивает с толку, и руководство Coq не дает никаких подробностей.Я не хочу разбираться с реализацией, но мне нужно хорошее понимание того, что делает тактика перезаписи, особенно в отношении того, как работает сопоставление терминов.Любые ответы / рекомендации в этом направлении приветствуются.

1 Ответ

0 голосов
/ 02 октября 2018

Сложность этого переписывания состоит в том, что существует связующее (forall k), которое может усложнить ситуацию.Если вы просто хотите, чтобы все работало, используйте setoid_rewrite вместо rewrite, и он будет перезаписан под связывателями.

  • rewrite IHl' выглядит так, как будто это происходит под связывателем, но шаблонпереписывание на самом деле не включает связанную переменную, поэтому связывание на самом деле не важно.Вот что я имею в виду: цель - 

    forall k : list T, (rev l' ++ [h]) ++ k = rev_acc l' (h :: k)

    , что совпадает с (то есть равно): 

     (fun l : list T => forall k : list T, l ++ k = rev_acc l' (h :: k)) (rev l' ++ [h])

    , которое я получил, используя pattern (rev l' ++ [h]) в Ltac.Теперь ясно, что вы можете просто переписать применяемую деталь и игнорировать подшивку.Когда вы делаете rewrite IHl' Coq легко вычисляет, что IHl должен быть специализирован для [h], и перезапись продолжается.

  • rewrite app_assoc, с другой стороны, должна быть специализирована для трехсписки, в частности rev l', [h] и k.Он не может быть специализирован в текущем контексте, потому что переменная k ограничена только под forall.Вот почему шаблон (?x ++ ?y) ++ ?z не появляется в цели.

Так что вы на самом деле делаете?Конечно, вы можете ввести k, чтобы не было связывателя, но есть более простой и более общий метод: Coq имеет обобщенное переписывание, которое можно переписать под связывателями, которое вы можете использовать, вместо этого вызывая setoid_rewrite (см. Перезапись всвязующие вещества в справочном руководстве Coq).В руководстве говорится, что вам необходимо объявить морфизмы, но в этом случае все они были реализованы для forall, поэтому setoid_rewrite app_assoc просто сработает.

Обратите внимание, что вы всегда можете ввестиforall чтобы избавиться от связующего, setoid_rewrite может быть очень удобно, когда ваша цель - exists.Вместо использования eexists вы можете просто переписать под связыватель.

...