Как я могу использовать аргументы типа в ltac? - PullRequest
Новая
       36

Как я могу использовать аргументы типа в ltac?

1 голос
/ 01 апреля 2019

Я пытаюсь написать следующую функцию: 

Ltac restore_dims :=
  repeat match goal with
  | [ |- context[@Mmult ?m ?n ?o ?A ?B]] => let Matrix m' n' := type of A in 
                                           let Matrix n'' o' := type of B in 
                                           replace m with m' by easy
         end.

То есть я хочу использовать информацию о типах A и B (которые являются матрицами с 2-мя аргументами измерения) в моем Ltac. Возможно ли это, и если да, то как?

(В идеале это заменит m на m', а также на n и o для всех матричных продуктов в моей цели.)

1 Ответ

4 голосов
/ 02 апреля 2019

Вы можете выполнить синтаксическое сопоставление type of A для извлечения аргументов. 

Ltac restore_dims :=
  repeat match goal with
  | [ |- context[@Mmult ?m ?n ?o ?A ?B]] =>
        match type of A with
        |  Matrix ?m' ?n' => replace m with m' by easy
        end;
        match type of B with
        |  Matrix ?n'' ?o' => replace n with n'' by easy
          (* or whatever you wanted to do with n'' and o' *)
        end
  end.

Если вы думаете, что m и m' будут конвертируемыми, а не просто равными, и вам нужны хорошие термины доказательства, рассмотрите возможность использования тактики change вместо replace, например. change n'' with n. Это ничего не добавит к условному термину, поэтому с ним легче работать.

...