WikiSort.ru - Программирование

Ассоциативность композиции функций

Доказательство «на бумаге» ассоциативности композиции функций:

${\displaystyle (f\circ g)\circ h}$

${\displaystyle =\lambda x.(f\circ g)(h~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.(\lambda y.f(g~y))(h~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.(f(g(h~x)))}$ ; β-эквивалентность

${\displaystyle f\circ (g\circ h)}$

${\displaystyle =\lambda x.f((g\circ h)~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.f((\lambda y.g(h~y))~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.f(g(h~x))}$ ; β-эквивалентность

По транзитивности равенства:

${\displaystyle (f\circ g)\circ h=f\circ (g\circ h)}$

Доказательство в Coq:

 Definition cf := fun t0 t1 t2 : Type
   => fun (f : t1 -> t2) (g : t0 -> t1) => fun x => f (g x).
 Implicit Arguments cf [t0 t1 t2].
 Notation "f @ g" := (cf f g) (at level 65, left associativity).
 
 Definition cf_assoc := fun (t0 t1 t2 t3 : Type)
   (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1)
   => (refl_equal _) : (f @ g) @ h = f @ (g @ h).

cf — определение композиции функций. Notation вводит инфиксное обозначение @ для композиции функций.

cf_assoc — собственно доказательство. Coq основан на изоморфизме Карри — Ховарда, поэтому доказательство есть терм лямбда-исчисления.

fun … => … в Coq обозначает лямбда-абстракцию. Функциям даются имена f, g, h, а их областям определения и областям значений даются имена t0, t1, t2, t3.

Кроме лямбда-абстракции доказательство состоит из refl_equal — аксиомы рефлексивности равенства. Нам нужно привести левую и правую части равенства с помощью βδ-редукций к одному выражению. Coq сам выполняет βδ-редукцию, поэтому доказательство практически пустое.

Чтобы понять роль refl_equal, выполните Check (refl_equal 2). Coq покажет автоматически выведенный тип этого терма, а именно, 2 = 2. Но в доказательстве cf_assoc аргумент refl_equal заменён на подчёркивание. Coq сам может вывести этот аргумент (см. «Вывод значений аргументов из типов»). Это сокращает объём доказательства. Выполнив Print cf_assoc., можно убедиться, что Coq вывел терм (f @ g) @ h вместо подчёркивания.

Коммутативность умножения в арифметике Пеано

Тип натуральных чисел определён в стандартной библиотеке индуктивно:

 Inductive nat : Set :=
   | O : nat
   | S : nat -> nat.

Конструкторы ${\displaystyle O}$ и ${\displaystyle S}$ суть ноль и функция, возвращающая следующее число.

Необходимо доказать, что ${\displaystyle n\cdot m=m\cdot n}$ . Доказательство коммутативности в арифметике Пеано строится с помощью математической индукции по одному из множителей.

 Require Import Coq.Arith.Plus.
 
 Definition mult_comm : forall n m, n * m = m * n.
 Proof.
 intros. elim n.
 auto with arith.
 intros. simpl in |- *. elim mult_n_Sm. elim H. apply plus_comm.
 Qed.

 Definition mult_comm := fun n:nat
 => fix rec (m : nat)
 : n * m = m * n
 := match m as m return n * m = m * n with
   | O => sym_eq (mult_n_O _)
   | S pm => match rec pm in _ = dep return _ = n + dep
     with refl_equal =>
       match mult_n_Sm _ _ in _ = dep return dep = _
       with refl_equal => plus_comm _ _ end
     end
   end.

 Definition mult_comm := fun n:nat
 => nat_ind (fun m => n * m = m * n)
   (sym_eq (mult_n_O _))
   (fun _ rec =>
     eq_ind _ (fun dep => _ = n + dep)
     (eq_ind _ (fun dep => dep = _)
       (plus_comm _ _) _ (mult_n_Sm _ _))
     _ rec).

Коммутативность умножения в кольце Гротендика

Это пример использования специализированной тактики ring. Она выполняет преобразования формул, построенных из операций полукольца или кольца.

Кольцо Гротендика конструируется из полукольца следующим образом. int_bipart — носитель кольца — есть вторая декартова степень nat — носителя полукольца.

 Record int_bipart : Set := {pneg : nat; ppos : nat}.

Record не только конструирует декартово произведение множеств, но и генерирует левую (названа pneg) и правую (названа ppos) проекции. Значение ${\displaystyle i}$ из множества int_bipart можно понимать как решение уравнения ${\displaystyle x+(pneg~i)=(ppos~j)}$ , где ${\displaystyle x}$  — неизвестная величина. Если ${\displaystyle (pneg~i)>(ppos~j)}$ , то решение является отрицательным числом.

Сложение в кольце определено как покомпонентное сложение, то есть pneg левого слагаемого складывается с pneg правого слагаемого, ppos левого слагаемого складывается с ppos правого слагаемого.

 Notation "a !+ b" := (Peano.plus a b) (at level 50, left associativity).
 Definition plus a b := Build_int_bipart
   (pneg a !+ pneg b) (ppos a !+ ppos b).
 Notation "a + b" := (plus a b).

Мы обозначаем сложение в полукольце как «!+» и сложение в кольце как «+».

Умножение определяется так: в часть pneg (это первый аргумент Build_int_bipart) идут произведения разных компонент, в часть ppos (это второй аргумент Build_int_bipart) идут произведения одинаковых компонент.

 Notation "a !* b" := (Peano.mult a b) (at level 40, left associativity).
 Definition mult a b := Build_int_bipart
   (pneg a !* ppos b !+ ppos a !* pneg b)
   (pneg a !* pneg b !+ ppos a !* ppos b).
 Notation "a * b" := (mult a b) (at level 40, left associativity).

Мы обозначаем умножение в полукольце как «!*» и умножение в кольце как «*».

Сначала докажем лемму «если оба компонента int_bipart равны, то int_bipart равны».

 Definition int_bipart_eq_part
   : forall an bn, an = bn -> forall ap bp, ap = bp
   -> Build_int_bipart an ap = Build_int_bipart bn bp.
 Proof.
 refine (fun _ _ eqn _ _ eqp => _).
 refine (eq_ind _ (fun n => _ = Build_int_bipart n _) _ _ eqn).
 refine (f_equal _ eqp).
 Qed.

Теперь докажем коммутативность умножения в кольце, то есть n * m = m * n.

 Require Import ArithRing.
 
 Definition mult_comm : forall n m, n * m = m * n.
 Proof.
 refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
 Qed.

Нужно доказать равенство двух int_bipart. Лемма int_bipart_eq_part разбивает нашу цель на две подцели. Первая подцель есть равенство компонент pneg, вторая подцель есть равенство компонент ppos. Увидеть эти подцели можно, если сразу после Proof. выполнить refine (fun n m => int_bipart_eq_part _ _ _ _ _ _). «;» между refine и (simpl; ring) означает, что комбинированная тактика (simpl; ring) доказывает все подцели, генерируемые тактикой refine.

Чтобы доказать «на бумаге», нужно последовательно применить свойства операций полукольца:

${\displaystyle (pneg~n)\cdot (ppos~m)+(ppos~n)\cdot (pneg~m)}$

${\displaystyle =(ppos~m)\cdot (pneg~n)+(ppos~n)\cdot (pneg~m)}$ ; коммутативность умножения

${\displaystyle =(ppos~m)\cdot (pneg~n)+(pneg~m)\cdot (ppos~n)}$ ; коммутативность умножения

${\displaystyle =(pneg~m)\cdot (ppos~n)+(ppos~m)\cdot (pneg~n)}$ ; коммутативность сложения

${\displaystyle (pneg~n)\cdot (pneg~m)+(ppos~n)\cdot (ppos~m)}$

${\displaystyle =(pneg~m)\cdot (pneg~n)+(ppos~n)\cdot (ppos~m)}$ ; коммутативность умножения

${\displaystyle =(pneg~m)\cdot (pneg~n)+(ppos~m)\cdot (ppos~n)}$ ; коммутативность умножения

Тактика ring генерирует все эти преобразования автоматически.