Ваша интуиция в отношении bool_ind верна, но размышление о том, почему bool_ind означает то, что вы сказали, может помочь прояснить два других. Мы знаем это
bool_ind : forall P : bool -> Prop,
P true ->
P false ->
forall b : bool,
P b
Если мы прочитаем это как логическую формулу, мы получим то же чтение, что и вы:
- For every predicate
P on booleans,
- If
P true holds, and
- Если выполняется
P false, то
- For every boolean
b,
Но это не просто логическая формула, это тип. В частности, это (зависимый) тип функции. И как тип функции он говорит (если вы позволите мне придумывать имена для безымянных аргументов и результата):
- Given a value
P : bool -> Prop,
- A value
Pt : P true,
- Значение
Pf : P false и
- A value
b : bool,
- We can construct a value
Pb : P b.
(Конечно, это каррированная функция, поэтому есть и другие способы разбить тип на прозу, но для наших целей это наиболее ясный.)
Самое важное здесь то, что заставляет Coq работать как средство доказательства теорем, будучи языком программирования (или наоборот), — это Соответствие Карри-Ховарда: типы — это предложения, а значения — доказательства этих утверждений. Например, тип простой функции -> соответствует импликации, а тип зависимой функции forall соответствует универсальной квантификации. (Обозначение довольно наводит на размышления :-)) Итак, в Coq, чтобы доказать, что φ → ψ, мы должны построить значение типа φ -> ψ: функцию, которая принимает значение типа φ (или, другими словами, доказательство предложения φ) и использует его для построения значения типа ψ (доказательство предложения ψ).
В Coq мы можем думать обо всех типах таким образом, живут ли эти типы в Set, Type или Prop. (Поэтому, когда вы говорите: «Похоже, что P true (которое является Set для bool rec и Type для bool_rect) обрабатывается как пропозициональное значение», вы правы!) Например, давайте рассмотрим, как мы реализуем bool_ind сами. Мы начнем с перечисления всех параметров функции вместе с типом возвращаемого значения:
Definition bool_ind' (P : bool -> Prop)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
Все идет нормально. На данный момент мы хотели бы вернуть что-то типа P b, но мы не знаем, что такое b. Итак, как всегда в таких ситуациях, мы сопоставляем шаблоны:
match b with
Сейчас два случая. Во-первых, b может быть true. В этом случае мы должны захотеть вернуть что-то типа P true, и, к счастью, у нас есть такое значение: Pt.
| true => Pt
Случай false аналогичен:
| false => Pf
end.
Обратите внимание, что когда мы реализуем bool_ind', это выглядит не очень «защищенным», а скорее очень «программным». Конечно, благодаря переписке Карри-Ховарда, это одно и то же. Но обратите внимание, что для двух других функций будет достаточно той же самой реализации:
Definition bool_rec' (P : bool -> Set)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
Definition bool_rect' (P : bool -> Type)
(Pt : P true)
(Pf : P false)
(b : bool)
: P b :=
match b with
| true => Pt
| false => Pf
end.
Глядя на это вычислительное определение, вы видите еще один взгляд на bool_ind, bool_rec и bool_rect: они инкапсулируют то, что вам нужно знать, чтобы говорить о каждом значении bool. Но в любом случае мы упаковываем эту информацию: если я знаю что-то для true и что-то для false, то я знаю это для всех bool.
Определение функций bool_{ind,rec,rect} абстрагируется от обычного способа написания функций на логических значениях: один аргумент соответствует истинной ветви, а другой — ложной. Или, другими словами: эти функции — всего лишь if операторов. В языке с независимой типизацией они могут иметь более простой тип forall S : Set, S -> S -> bool -> S:
Definition bool_simple_rec (S : Set) (St : P) (Sf : P) (b : bool) : S :=
match b with
| true => St
| false => Sf
end.
Однако, поскольку типы могут зависеть от значений, мы должны везде пропускать b через типы. Однако, если окажется, что мы этого не хотим, мы можем использовать нашу более общую функцию и сказать:
Definition bool_simple_rec' (S : Set) : S -> S -> bool -> S :=
bool_rec (fun _ => S).
Никто никогда не говорил, что наш P : bool -> Set должен использовать bool!
Все эти функции намного интереснее для рекурсивных типов. Например, Coq имеет следующий тип натуральных чисел:
Inductive nat : Set := O : nat | S : nat -> nat.
И у нас есть
nat_ind : forall P : nat -> Prop,
P O ->
(forall n' : nat, P n' -> P (S n')) ->
forall n : nat,
P n
Вместе с соответствующими nat_rec и nat_rect. (Упражнение для читателя: реализуйте эти функции напрямую.)
На первый взгляд, это всего лишь принцип математической индукции. Однако именно так мы пишем рекурсивные функции на nats; это одно и то же. В общем, рекурсивные функции над nat выглядят следующим образом:
fix f n => match n with
| O => ...
| S n' => ... f n' ...
end
Рука совпадения, следующая за O (базовый случай), является просто значением типа P O. Ветвь совпадения, следующая за S n' (рекурсивный случай), — это то, что передается в функцию типа forall n' : nat, P n' -> P (S n'): n' совпадают, а значение P n' является результатом рекурсивного вызова f n'.
Тогда другой способ думать об эквивалентности между функциями _rec и _ind — и тот, который, как мне кажется, более понятен для бесконечных типов, чем для bool, — состоит в том, что это то же самое, что и эквивалентность между математическим indдействием (которое происходит в Prop) и (структурным ) recursion (что происходит в Set и Type).
Давайте попрактикуемся и воспользуемся этими функциями. Мы определим простую функцию, которая преобразует логические значения в натуральные числа, и сделаем это как напрямую, так и с помощью bool_rec. Самый простой способ написать эту функцию — использовать сопоставление с образцом:
Definition bool_to_nat_match (b : bool) : nat :=
match b with
| true => 1
| false => 0
end.
Альтернативное определение
Definition bool_to_nat_rec : bool -> nat :=
bool_rec (fun _ => nat) 1 0.
И эти две функции одинаковы:
Goal bool_to_nat_match = bool_to_nat_rec.
Proof. reflexivity. Qed.
(Примечание: эти функции синтаксически равны. Это более сильное условие, чем просто выполнение одного и того же.)
Здесь P : bool -> Set равно fun _ => nat; он дает нам возвращаемый тип, который не зависит от аргумента. Наше Pt : P true равно 1, что нужно вычислить, когда нам дано true; аналогично, наш Pf : P false это 0.
Если мы хотим использовать зависимость, мы должны создать полезный тип данных. Как насчет
Inductive has_if (A : Type) : bool -> Type :=
| has : A -> has_if A true
| lacks : has_if A false.
При таком определении has_if A true изоморфно A, а has_if A false изоморфно unit. Тогда у нас может быть функция, которая сохраняет свой первый аргумент тогда и только тогда, когда ей передается true.
Definition keep_if_match' (A : Type) (a : A) (b : bool) : has_if A b :=
match b with
| true => has A a
| false => lacks A
end.
Альтернативное определение
Definition keep_if_rect (A : Type) (a : A) : forall b : bool, has_if A b :=
bool_rect (has_if A) (has A a) (lacks A).
И они снова те же:
Goal keep_if_match = keep_if_rect.
Proof. reflexivity. Qed.
Здесь возвращаемый тип функции зависит от аргумента b, поэтому наш P : bool -> Type действительно что-то делает.
Вот более интересный пример с использованием натуральных чисел и списков с индексом длины. Если вы не видели индексированные по длине списки, также называемые векторами, то это именно то, что написано на жестяной банке; vec A n — это список n As.
Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A O
| vcons : forall n, A -> vec A n -> vec A (S n).
Arguments vnil {A}.
Arguments vcons {A n} _ _.
(Машина Arguments обрабатывает неявные аргументы.) Теперь мы хотим создать список n копий некоторого конкретного элемента, поэтому мы можем написать это с фиксированной точкой:
Fixpoint vreplicate_fix {A : Type} (n : nat) (a : A) : vec A n :=
match n with
| O => vnil
| S n' => vcons a (vreplicate_fix n' a)
end.
В качестве альтернативы мы можем использовать nat_rect:
Definition vreplicate_rect {A : Type} (n : nat) (a : A) : vec A n :=
nat_rect (vec A) vnil (fun n' v => vcons a v) n.
Обратите внимание, что поскольку nat_rect фиксирует шаблон рекурсии, vreplicate_rect сама по себе не является фиксированной точкой. Следует отметить третий аргумент nat_rect:
fun n' v => vcons a v
v концептуально является результатом рекурсивного вызова vreplicate_rect n' a; nat_rect абстрагирует этот шаблон рекурсии, поэтому нам не нужно вызывать его напрямую. n' действительно тот же n', что и vreplicate_fix, но теперь кажется, что нам не нужно упоминать его явно. Почему это передается? Это станет ясно, если мы выпишем наши типы:
fun (n' : nat) (v : vec A n') => vcons a v : vec A (S n')
Нам нужно n', чтобы мы знали, какой тип имеет v и, следовательно, какой тип имеет результат.
Давайте посмотрим на эти функции в действии:
Eval simpl in vreplicate_fix 0 tt.
Eval simpl in vreplicate_rect 0 tt.
(* both => = vnil : vec unit 0 *)
Eval simpl in vreplicate_fix 3 true.
Eval simpl in vreplicate_rect 3 true.
(* both => = vcons true (vcons true (vcons true vnil)) : vec bool 3 *)
И действительно, они одинаковы:
(* Note: these two functions do the same thing, but are not syntactically
equal; the former is a fixpoint, the latter is a function which returns a
fixpoint. This sort of equality is all you generally need in practice. *)
Goal forall (A : Type) (a : A) (n : nat),
vreplicate_fix n a = vreplicate_rect n a.
Proof. induction n; [|simpl; rewrite IHn]; reflexivity. Qed.
Выше я изложил упражнение по повторной реализации nat_rect и друзей. Вот ответ:
Fixpoint nat_rect' (P : nat -> Type)
(base_case : P 0)
(recurse : forall n', P n' -> P (S n'))
(n : nat)
: P n :=
match n with
| O => base_case
| S n' => recurse n' (nat_rect' P base_case recurse n')
end.
Надеюсь, это проясняет, как nat_rect абстрагирует шаблон рекурсии и почему он достаточно общий.
person
Antal Spector-Zabusky
schedule
23.06.2013
