Я хотел бы написать метод Eisbach с той же функциональностью следующего Ltac в Coq - PullRequest
Новая
       19

Я хотел бы написать метод Eisbach с той же функциональностью следующего Ltac в Coq

1 голос
/ 03 мая 2019

Я не знаю, как оценивать термин, используя определяемые пользователем функции как часть кода метода Эйсбаха, а также как сопоставлять его с термином.Ниже приведено (упрощенное) определение Coq Ltac, которое я хотел бы написать как метод Эйсбаха в Изабель / HOL: 

fun f:: 'a => 'a list := .....

Ltac apply_R :=
match goal with
|  |- ( ... H ...) => let L := eval cbv in f(H)
                      in match L with
                       | nil => apply R; simpl; intuition
                       | _ =>  idtac
                       end
end.
...