Как использовать принуждение с sig в ​​coq - PullRequest
Новая
       109

Как использовать принуждение с sig в ​​coq

0 голосов
/ 28 января 2020

У меня есть код вроде 

Definition even := {n : nat | exists k, n = k + k}.

Definition even_to_nat (e : even) : nat.
Admitted.

Coercion even_to_nat : even >-> nat.

Example Ex : forall n : even, exists k, k + k = n.
Admitted.

Example Ex2 : forall k, exists n : even, k + k = n.
Admitted.

Как мне удалить Admitted в этом случае?

Кроме того, почему 

Example Ex' : forall n : even, exists k, n = k + k

не работает даже с принуждением? Есть ли хороший способ удалить такие ошибки?

1 Ответ

0 голосов
/ 28 января 2020

Это определение для функции even_to_nat, написанное в Gallina: 

Definition even := {n : nat | exists k, n = k + k}.

Definition even_to_nat (e : even) : nat :=
  match e with
  | exist _ n _ => n
  end.

Coercion even_to_nat : even >-> nat.

Это соответствует шаблону на e, чтобы получить упакованное натуральное число n.

This является эквивалентной реализацией, использующей тактику: 

Definition even_to_nat_tac (e : even) : nat.
destruct e.
auto.
Defined.

Шаблон destruct tacti c по существу совпадает с e. Затем auto автоматически использует натуральное число внутри, чтобы завершить sh определение.

Вот реализация Gallina вашего первого примера: 

Example Ex : forall n : even, exists k, k + k = n :=
  fun n => match n with
  | exist _ n (ex_intro _ k eq) => ex_intro (fun k => k + k = n) k (eq_sym eq)
  end.

По сути, шаблон соответствует n, извлекает k и доказательство того, что n = k + k, затем использует eq_sym, чтобы перевернуть равенство.

Вот реализация для Ex2: 

Example Ex2 : forall k, exists n : even, k + k = n :=
  fun k =>
  let n := k + k in
  let exists_k := ex_intro (fun k => n = k + k) k eq_refl in
  let even_nat := exist (fun n => exists k, n = k + k) n exists_k in
  ex_intro (fun n => k + k = even_to_nat n) even_nat eq_refl.

exists_k - это доказательство, содержащееся внутри четного числа с указанием exists k, n + n = k. even_nat - четное число, удовлетворяющее условию exists n, k + k = n, где n, очевидно, k + k. Наконец-то я живу нужного типа. Кажется, я не могу использовать здесь принуждения, поэтому я явно использую even_to_nat.

В качестве альтернативы, принуждение работает, если я добавляю аннотацию типа: 

Example Ex2 : forall k, exists n : even, k + k = n :=
  fun k =>
  let n := k + k in
  let exists_k := ex_intro (fun k => n = k + k) k eq_refl in
  let even_nat := exist (fun n => exists k, n = k + k) n exists_k in
  ex_intro (fun (n : even) => k + k = n) even_nat eq_refl.

Для вашего Ex' пример, см. предупреждение в этом примере из документации по принуждению . С учетом принуждения Coercion bool_in_nat : bool >-> nat.:

Обратите внимание, что проверка (true = O) завершится неудачей. Это «нормальное» поведение принуждений. Чтобы проверить true = O, приведение ищется от nat к bool. Там нет ни одного.

Вы можете только принуждать правую часть типа равенства, а не левую.

...