Что нужно сделать, когда Simpl не сокращает все необходимые шаги? - PullRequest
Новая
       14

Что нужно сделать, когда Simpl не сокращает все необходимые шаги?

1 голос
/ 27 апреля 2019

Следующий пример взят из главы «Поли» из книги «Основы программного обеспечения». 

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
intros.
induction l.
- simpl. reflexivity.
- simpl.

1 subgoal
X : Type
x : X
l : list X
IHl : fold_length l = length l
______________________________________(1/1)
fold_length (x :: l) = S (length l)

Я ожидал, что это упростит шаг с левой стороны.Это, безусловно, должно быть в состоянии. 

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
intros.
induction l.
- simpl. reflexivity.
- simpl. rewrite <- IHl. simpl.

1 subgoal
X : Type
x : X
l : list X
IHl : fold_length l = length l
______________________________________(1/1)
fold_length (x :: l) = S (fold_length l)

Во время выполнения тестов у меня была проблема, из-за которой simpl отказывался бы погружаться, но reflexivity добился цели, поэтому я попыталсято же самое здесь, и доказательство прошло успешно.

Заметьте, что нельзя ожидать, что рефлексивность пройдет, учитывая состояние цели, но это так.В этом примере это сработало, но заставило меня выполнить переписывание в направлении, противоположном тому, что я изначально планировал.

Возможно ли иметь больший контроль над simpl, чтобы он выполнял желаемые сокращения?

1 Ответ

3 голосов
/ 27 апреля 2019

Для целей этого ответа я предполагаю, что определение fold является чем-то вроде 

Fixpoint fold {A B: Type} (f: A -> B -> B) (u: list A) (b: B): B :=
match u with
| [] => b
| x :: v => f x (fold f v b)
end.

(в основном fold_right из стандартной библиотеки). Если ваше определение существенно отличается, рекомендованная мною тактика может не сработать.

Проблема здесь заключается в поведении simpl с константами, которые необходимо развернуть, прежде чем их можно упростить. С документация :

Обратите внимание, что упрощенные могут разворачиваться только прозрачные константы, чье имя может быть повторно использовано в рекурсивных вызовах. Например, константа, определенная с помощью plus ': = plus, может быть развернута и повторно использована в рекурсивных вызовах, но такая константа, как succ: = plus (S O), никогда не раскрывается.

Это немного сложно понять, поэтому давайте рассмотрим пример. 

Definition add_5 (n: nat) := n + 5.

Goal forall n: nat, add_5 (S n) = S (add_5 n).
Proof.
  intro n.
  simpl.
  unfold add_5; simpl.
  exact eq_refl.
Qed.

Вы увидите, что первый вызов simpl ничего не сделал, хотя add_5 (S n) можно было бы упростить до S (n + 5). Однако, если я unfold add_5 первый, он работает отлично. Я думаю, что проблема в том, что plus_5 не является напрямую Fixpoint. Хотя plus_5 (S n) эквивалентно S (plus_5 n), на самом деле это не его определение. Так что Coq не признает, что его «имя может быть повторно использовано в рекурсивных вызовах». Nat.add (то есть "+") определяется непосредственно как рекурсивный Fixpoint, поэтому simpl упрощает его.

Поведение simpl можно немного изменить (см. Документацию снова). Как упоминает Антон в комментариях, вы можете использовать народную команду Arguments для изменения, когда simpl пытается упростить. Arguments fold_length _ _ /. сообщает Coq, что fold_length следует развернуть, если указано как минимум два аргумента (наклонная черта разделяет обязательные аргументы слева и ненужные аргументы справа). [Sup] 1 [\ sup]

Более простая тактика, если вы не хотите иметь с ней дело, это cbn, которая работает здесь по умолчанию и работает лучше в целом. Цитирование из документации :

Тактика cbn считается более принципиальной, быстрой и предсказуемой заменой упрощенной.

Ни simpl с Arguments и косой чертой, ни cbn не уменьшают цель до того, что вы хотите в вашем случае, так как она развернется fold_length, но не перевернет ее. Вы можете распознать, что вызов fold - это всего лишь fold_length l, и перекомпилировать его с fold (fold_length l).

Другая возможность в вашем случае - использовать тактику change. Казалось, вы уже знали, что fold_length (a :: l) должен был упростить до S (fold_length l). Если это так, вы можете использовать change (fold_length (a :: l)) with (S (fold_length l))., и Coq попытается преобразовать одно в другое (используя только основные правила преобразования, а не равенства, как rewrite делает).

После того, как вы достигли цели S (fold_length l) = S (length l), используя любую из вышеперечисленных тактик, вы можете использовать rewrite -> IHl., как вы и хотели.

  1. Я думал, что косые черты только simpl раскрывают вещи меньше , поэтому я не упоминал об этом раньше. Я не уверен, какое значение по умолчанию на самом деле, так как при расположении косой черты в любом месте simpl раскрывается fold_length.
...