Supposons que j'ai une somme comme a + (b + (c + d)), que je souhaite transformer en a + b + c + d pour appliquer un lemme.Coq: Supprimer toutes les parenthèses (imbriquées) d'une somme
Le faire manuellement avec Nat.add_assoc est extrêmement fastidieux. Y a-t-il un moyen plus intelligent?
Le facile, mais pas gentil "comme je voudrais utiliser est replace (a + (b + (c + d)))) with (a + b + c + d) by now omega
Vous pouvez utiliser le repeat tactique, qui répète une tactique jusqu'à ce qu'il ne peut pas être appliqué plus:
repeat rewrite Nat.add_assoc.
ou plus concise Version:
rewrite !Nat.add_assoc.
Il fonctionne même que la variante avec repeat.
L'inconvénient de cette approche est qu'elle se réécrit partout dans le but. Donc, vous pourriez vouloir sélectionner une partie de votre formule pour faire les réécritures sur elle seulement.
Pourquoi n'est-ce pas agréable? En outre, vous pouvez également faire 'par auto avec *'. –
Si vous avez déjà regardé le terme de sortie créé par 'omega', vous comprendrez. La plupart du temps c'est trop compliqué, et une petite preuve utilisant la réécriture sera beaucoup plus petite. Mais c'est une question d'opinion personnelle;) – Vinz
'par omega' fonctionnerait aussi bien; et 'by ring' résout également le problème. Le premier a besoin d'un module "Omega" à importer; ce dernier - 'Arith'. –