Utiliser eq_refl pour obtenir une hypothèse "x = x"

2017-10-18 7 views 0 likes

En résumé, est-ce possible? J'essaie de prouver que l'annulation fonctionne dans un groupe.Utiliser eq_refl pour obtenir une hypothèse "x = x"

J'ai

a, b, x : G 
H: a <+> x = b <+> x

et je voudrais prouver

a = b

Mon idée était d'obtenir une hypothèse

H2: a <+> x <+> i x = a <+> x <+> i x

(i est la fonction inverse).

J'ai essayé

pose proof eq_refl (a <+> x <+> i x) as H.

mais cela ne semble pas fonctionner.

Source

2017-10-18 Mark Butler

Répondre

Si votre objectif ressemble vraiment à ce que vous avez posté, alors votre tactique devrait échouer car elle réutilise le nom H. Si ce n'est pas le problème, il serait utile de savoir quel message d'erreur Coq affiche.

Source

2017-10-18 18:20:19

En outre, le terme de preuve manque de parenthèses autour d'elle. –

@AntonTrunov Je pense que ce n'est pas un problème, en fait: j'ai juste couru un extrait similaire sur ma machine, et cela a fonctionné. –

Oh, oui, vous avez raison - je l'ai confondu avec 'specialize', ce qui nécessite parens –

Utiliser eq_refl pour obtenir une hypothèse "x = x"

Répondre

Questions connexes