1
Tenir compte de la preuve partielle suivante:Coq: supprimer constructeur des deux côtés du but
Theorem test : forall (n m : nat),
n = m -> S n = S m.
Proof.
intros n m H.
exécution jusqu'à ce point me donne ce qui suit:
1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
S n = S m
je voudrais supprimer les S s de l'objectif, l'obtention de l'objectif n = m. Y a-t-il une tactique qui fait cela?
La question actuelle semble être une copie de [this] (http://stackoverflow.com/q/37490891/2747511) question et [this one] (http://stackoverflow.com/q/13749403/2747511). –
Finalement, vous pourriez trouver intéressant de noter qu'il s'agit essentiellement d'une instruction 'match', mais d'un formulaire avancé qui utilise une annotation' return' pour laisser le système de type Coq "lancer" le type 'S n = S n'' S n = S m'. Essayez 'apply (appliquez H dans (_ = n2) return (S _ = S n2) avec eq_refl => eq_refl end). – larsr