Не удается переписать подтермы в Coq

Question

У меня есть доказательство в Coq, где одна из гипотез является:

H : m = pred q * n + (r + n) 

И у меня есть доказанная лемма, которая гласит:

Lemma suma_conmutativa: forall m, forall n, m + n = n + m. 

Где + является нотацией для функция называется сума, что я определил:

Fixpoint suma (m:nat) (n:nat) : nat := 
match m with 
    | 0 => n 
    | S k => S (suma k n) 
end. 
Notation "m + n" := (suma m n). 

по какой-то причине, когда я пытаюсь переписать suma_conmutativa with r n in H я получаю следующее сообщение об ошибке:

Error: Found no subterm matching "r + n" in H. 

Однако, очевидно, что подтерм согласуется с r + n в H. Почему это не может найти Coq?

спасибо.

Answer 1

Я не специалист по обозначениям в Coq, но вот как я понимаю вашу проблему.

Coq заменяет первое вхождение + на suma. suma связывает свои аргументы с областью nat_scope. Классическая нотация + связана с nat_scope и предпочтителен для второго появления +.

Решение, которое я предлагаю, состоит в том, чтобы связать ваши обозначения с nat_scope, чтобы полностью скрыть оригинальную нотацию. Это дает: Notation "m + n" := (suma m n) : nat_scope.