Складывать только приложения - PullRequest
Новая
       6

Складывать только приложения

0 голосов
/ 30 июня 2018

Тактика fold заменяет все вхождения одного термина другим, поэтому fold (id f) пытается заменить все вхождения f на (id f).

Однако я хочу сбросить f, только если это происходит в контексте (f [ ]), а не если оно происходит в контексте ([ ] f). В частности repeat myfold (id f), не должен зацикливаться.

Есть ли общий способ сделать этот тип фолда? Лучшее, что у меня есть сейчас, это 

repeat match goal with
| |- context [(f ?x)] => change (f x) with ((id f) x)
end

Но вышесказанное не работает для контекстов вида forall x, f x = f x.

1 Ответ

0 голосов
/ 02 июля 2018

Вы можете использовать промежуточное значение, не содержащее f. Что-то вроде 

let f' := fresh in
pose (id f) as f';
change f with f'
change (id f') with f'; (* undo the change in locations where we've already added id *)
subst f'.

Редактировать

Если вы действительно хотите просто сложить вещи в аппликативных контекстах, вы можете использовать три промежуточных значения, например: 

(* Copyright 2018 Google LLC.
   SPDX-License-Identifier: Apache-2.0 *)
Ltac myfold_id f :=
  let id_f := fresh in
  let id_f_good := fresh in
  let f' := fresh in
  pose (id f) as id_f;
  pose (id f) as id_f_good;
  pose f as f';
  repeat (change f with id_f at 1;
          lazymatch goal with
          | [ |- context[id_f _] ] => change id_f with id_f_good
          | _ => change id_f with f'
          end);
  subst id_f id_f_good f'.
Goal let f := id in (f = f, f 0) = (f = f, f 0).
Proof.
  intro f.
  (* (f = f, f 0) = (f = f, f 0) *)
  myfold_id f.
  (* (f = f, id f 0) = (f = f, id f 0) *)
...