Как уничтожить / обобщить перезаписанные операторы соответствия программы

При использовании Program операторы соответствия переписываются в стиль "proof-passing". Это делает доказательства соответствия доступными в ветвях-что может быть критично.

Однако это также, по-видимому, затрудняет анализ конкретных случаев. Например: 
Require Import ZArith.

Open Scope Z_scope.

Program Definition test (x:Z) : option (x <= 100) :=
  match Z_le_gt_dec x 100 with
  | left bound => Some _
  | right bound => None
  end.

Lemma test_gt_100 : forall x:Z, x > 100 -> test x = None.
Proof.
  intros x bound.
  unfold test.

В этом месте обычно было бы destruct (Z_le_gt_dec x 100), и доказательство тогда легко. Однако переписанное совпадение дает такой контекст: 

x : Z
bound : x > 100
============================
 match
   Z_le_gt_dec x 100 as x0
   return (x0 = Z_le_gt_dec x 100 -> option (x <= 100))
 with
 | left bound0 =>
     fun Heq_anonymous : left bound0 = Z_le_gt_dec x 100 =>
     Some (test_obligation_1 x bound0 Heq_anonymous)
 | right bound0 => fun _ : right bound0 = Z_le_gt_dec x 100 => None
 end eq_refl = None

При этом разрушение завершается неудачей: 

Toplevel input, characters 20-48:
Error: Abstracting over the term "s" leads to a term
"fun s : {x <= 100} + {x > 100} =>
 match s as x0 return (x0 = s -> option (x <= 100)) with
 | left bound =>
     fun Heq_anonymous : left bound = s =>
     Some (test_obligation_1 x bound Heq_anonymous)
 | right bound => fun _ : right bound = s => None
 end eq_refl = None" which is ill-typed.

Двигаясь медленнее и стараясь просто generalize (Z_le_gt_dec x 100) показывает, почему: 

Toplevel input, characters 0-30:
Error: Illegal application (Type Error): 
The term "test_obligation_1" of type
 "forall x : Z,
  let filtered_var := Z_le_gt_dec x 100 in
  forall bound : x <= 100, left bound = filtered_var -> x <= 100"
cannot be applied to the terms
 "x" : "Z"
 "bound0" : "x <= 100"
 "Heq_anonymous" : "left bound0 = s"
The 3rd term has type "left bound0 = s" which should be coercible to
 "left bound0 = Z_le_gt_dec x 100".
Хотя это имеет некоторый смысл, я не знаю, что с этим делать.

(я поместил это в collacoq , Если это полезно. Не забудьте сначала выполнить только строку комментария, а затем дождаться загрузки всех библиотек, прежде чем импортировать ZArith.)

1 2
coq

1 ответ:

Проблема здесь в том, что вы зависите от конкретного термина равенства, абстрагирование над ним должно позволить вам продолжить. (Это-общая хорошая практика, чтобы заявить леммы, которые независимы от доказательств).

Вот ваш пример, используя ssreflect's rewrite. К сожалению, я не смог заставить одного Кок сделать правильный выбор рисунка.

Comments "pkgs: coq-reals".
From mathcomp Require Import ssreflect.
Require Import Coq.ZArith.ZArith.

Open Scope Z_scope.

Program Definition test (x:Z) : option (x <= 100) :=
  match Z_le_gt_dec x 100 with
  | left  bound => Some _
  | right bound => None
  end.

Lemma test_gt_100 : forall x:Z, x > 100 -> test x = None.
Proof.
intros x hb; unfold test.
assert (Z_le_gt_dec x 100 = right hb) as Hz. admit.
move: eq_refl; rewrite {1 3}Hz.
done.

[также в https://x80.org/collacoq/xareboqura.coq ]

С наилучшими пожеланиями, е.

EDIT: немного подробнее: на в начале аргументом соответствия является eq_refl : forall x, x = x, что нормально, так как функция внутри соответствия ожидает член типа Z.le .... = Z.le ..... Однако при выполнении перезаписи тип в аннотации соответствия будет иметь вид Z_le ... = right ..., но если аргумент все еще eq_refl, это приведет к плохо набранному термину, так как eq_refl никогда не может быть набран как Z.le ... = right ...!

Таким образом, мы модифицируем нашу цель так, что доказательство равенства не обязательно должно быть eq_refl, а затем переписываем.

Почему доказательство было сделано с помощью eq_refl в первую очередь? Это обычно делается, чтобы иметь хорошее поведение сокращения при наличии доказательств равенства.

Было бы интересно добавить поддержку доказательства неуместности к программе thou. (Я игнорирую, если они уже есть).
2