Impossible de réécrire sous-terme en Coq

Question

j'ai une preuve en Coq où l'une des hypothèses est:

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

et j'ai un lemme prouvé qui stipule:

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

Où + est la notation pour une fonction appelée Suma que je définissais:

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). 

pour une raison quelconque lorsque je tente de réécrire suma_conmutativa with r n in H je reçois l'erreur suivante: Cependant, il existe clairement un sous-terme correspondant à r + n dans H. Pourquoi Coq ne peut-il pas le trouver?

Merci.

Answer 1

Je ne suis pas un expert des notations en Coq, mais voici comment je comprends votre problème. Coq remplace la première occurrence de + par . suma lie ses arguments à la portée nat_scope. La notation classique + est liée à nat_scope et est préférée pour la deuxième occurrence de +.

La solution que je propose est de lier votre notation à nat_scope pour cacher complètement la notation originale. Cela donne: Notation "m + n" := (suma m n) : nat_scope.