Блог

Используя ssreflect, я влюбился в его стиль активного управления связующими элементами в цель и из нее. Однако у меня возникли проблемы с поиском того, что я хочу получить из его документации.

В частности, я не могу найти тактику ssreflect для этой inversion тактики.

Я понимаю, что могу очень хорошо использовать inversion тактику. Тем не менее, он следует традиционному стилю coq при использовании привязок, где мне трудно указать правильные имена для каждой ветви, поскольку она «скрыта» от представления с несколькими целями. Между тем, тактика ssreflect всегда сбрасывает связующие в цель, чтобы я мог связать имена с теми, кто похож move .

Например, применяя инверсию вкл Forall2 R l m , я получаю

 x0: A
y0: B
l0: list A
l': list B
H3: R x y
H5: Forall2 R l m
H0: x0 = x
H1: l0 = l
H2: y0 = y
H4: l' = m
 

какие имена мне не нравятся, и отслеживать и указывать их было бы болезненно, поскольку привязки скрыты за второй ветвью (просто первая ветвь l = m = [] ).

Что я могу использовать, если я хочу инвертировать индуктивный тип в стиле ssreflect? Может elim использоваться для какой-то инверсии?