Coq: Как ссылаться на типы, сгенерированные конкретным конструктором? - PullRequest
Новая
       5

Coq: Как ссылаться на типы, сгенерированные конкретным конструктором?

0 голосов
/ 03 октября 2018

Например, если я определю функцию от nat до nat, это будет 

Definition plusfive(a:nat): nat := a + 5.

Однако я хотел бы определить функцию, аргументами которой являются nats, построенные с использованием конструктора "S" (т.е.ненулевой) это можно напрямую указать как тип?что-то вроде 

Definition plusfive(a: nat.S): nat := a + 5.

(я знаю, что для этого случая я мог бы также добавить аргумент с доказательством того, что a не равен нулю, но мне интересно, можно ли напрямую назвать тип на основеКонструктор 'S').

1 Ответ

0 голосов
/ 04 октября 2018

Функции должны быть завершены, поэтому вам придется использовать некоторый подтип вместо nat или добавить аргумент, уменьшающий пространство ввода, например (H: a<>0)

Definition plusfive(a:nat) (H:a<>0) :=
  match a as e return a=e -> _ with
  | S _ => fun _  => a + 5
  | _   => fun H0 => match (H H0) with end
  end eq_refl.

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

Require Import Nat.
Print div.

div = 
fun x y : nat => match y with
                 | 0 => y
                 | S y' => fst (divmod x y' 0 y')
                 end
     : nat -> nat -> nat

Итак, Compute (div 1 0). дает вам 0.

Приятно то, что вы можете использовать div в выраженияхнапрямую, без чередования доказательств того, что знаменатель ненулевой.Доказательство того, что выражение является правильным, затем выполняется после того, как оно было определено, а не одновременно.

...