Пошаговое упрощение в coq?

Question

Есть ли способ упростить один шаг за раз?

Скажи у тебя f1 (f2 x) оба из которых могут быть упрощены в свою очередь через один simplМожно ли упростить f2 x В качестве первого шага рассмотрим промежуточный результат, а затем упростим f1?

Возьмем для примера теорему:

Theorem pred_length : forall n : nat, forall l : list nat,
  pred (length (n :: l)) = length l.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

simpl тактика упрощает Nat.pred (length (n :: l)) в length l, Есть ли способ разбить это на два этапа упрощения, то есть:

Nat.pred (length (n :: l)) --> Nat.pred (S (length l)) --> length l

Answer 1

Вы также можете использовать simpl для конкретного шаблона.

Theorem pred_length : forall n : nat, forall l : list nat,
  pred (length (n :: l)) = length l.
Proof.
 intros.
 simpl length.
 simpl pred.
 reflexivity.
Qed.

В случае, если у вас есть несколько вхождений шаблона как length что может быть упрощено, вы можете дополнительно ограничить результат упрощения, указав позицию этого вхождения (слева направо), например simpl length at 1 или же simpl length at 2 для первого или второго случая.

Answer 2

Мы можем включить упрощение для pred выключите, упростите его аргумент и включите его снова:

Theorem pred_length : forall n : nat, forall l : list nat,
  pred (length (n :: l)) = length l.
Proof.
  intros.
  Arguments pred : simpl never.    (* do not unfold pred *)
  simpl.
  Arguments pred : simpl nomatch.  (* unfold if extra simplification is possible *)
  simpl.
  reflexivity.
Qed.

См. §8.7.4 Справочного руководства для получения более подробной информации.