Индукция для типа данных с параметрами неоднородного типа приводит к некорректным терминам - PullRequest
Новая
       24

Индукция для типа данных с параметрами неоднородного типа приводит к некорректным терминам

4 голосов
/ 08 июля 2019

Я работаю над формализацией свободных селективных аппликативных функторов в Coq, но борюсь с доказательствами по индукции для индуктивных типов данных с неоднородными параметрами типа.

Позвольте мне дать немноговведения в тип данных, с которым я имею дело.В Haskell мы кодируем свободные селективные функторы как GADT: 

data Select f a where
    Pure   :: a -> Select f a
    Select :: Select f (Either a b) -> f (a -> b) -> Select f b

Важнейшей вещью здесь является переменная экзистенциального типа b во втором конструкторе данных.

Мы можем перевести это определениеto Coq: 

Inductive Select (F : Type -> Type) (A : Set) : Set :=
    Pure   : A -> Select F A
  | MkSelect : forall (B : Set), Select F (B + A) -> F (B -> A) -> Select F A.

В качестве примечания я использую опцию -impredicative-set для его кодирования.

Coq генерирует следующий принцип индукции для этого типа данных: 

Select_ind :
  forall (F : Type -> Type) (P : forall A : Set, Select F A -> Prop),
  (forall (A : Set) (a : A), P A (Pure a)) ->
  (forall (A B : Set) (s : Select F (B + A)), P (B + A)%type s ->
     forall f0 : F (B -> A), P A (MkSelect s f0)) ->
  forall (A : Set) (s : Select F A), P A s

Здесь интересным является предикат P : forall A : Set, Select F A -> Prop, который параметризуется не только в выражении, но и в параметре типа выражения.Как я понимаю, принцип индукции имеет эту конкретную форму из-за первого аргумента конструктора MkSelect типа Select F (B + A).

Теперь я хотел бы доказать утверждения, подобные третьему Прикладному закону для определенноготип данных: 

Theorem Select_Applicative_law3
        `{FunctorLaws F} :
  forall (A B : Set) (u : Select F (A -> B)) (y : A),
  u <*> pure y = pure (fun f => f y) <*> u.

Которые содержат значения типа Select F (A -> B), то есть выражения, содержащие функции.Однако вызов induction для переменных таких типов приводит к неправильному типу терминов.Рассмотрим упрощенный пример равенства, которое может быть тривиально доказано с помощью reflexivity, но не может быть доказано с помощью induction: 

Lemma Select_induction_fail `{Functor F} :
  forall (A B : Set) (a : A) (x : Select F (A -> B)),
    Select_map (fun f => f a) x = Select_map (fun f => f a) x.
Proof.
  induction x.

Coq жалуется на ошибку: 

Error: Abstracting over the terms "P" and "x" leads to a term
fun (P0 : Set) (x0 : Select F P0) =>
  Select_map (fun f : P0 => f a) x0 = Select_map (fun f : P0 => f a) x0
which is ill-typed.
Reason is: Illegal application (Non-functional construction):
The expression "f" of type "P0" cannot be applied to the term
 "a" : "A"

Здесь Coq не может создать предикат, абстрагированный от переменной типа, потому что приложение с обратными функциями из оператора становится не типизированным.

Мой вопрос: как мне использовать индукцию для моего типа данных?Я не вижу способа, как изменить принцип индукции таким образом, чтобы предикат не абстрагировал тип.Я пытался использовать dependent induction, но он выдвигал индуктивную гипотезу, ограниченную равенствами, подобными (A -> B -> C) = (X + (A -> B -> C)), которые, я думаю, было бы невозможно создать.

Пожалуйста, посмотрите полный пример на GitHub: https://github.com/tuura/selective-theory-coq/blob/impredicative-set/src/Control/Selective/RigidImpredSetMinimal.v

1 Ответ

1 голос
/ 09 июля 2019

Доказательства по индукции мотивированы рекурсивными определениями. Чтобы узнать, к чему применять индукцию, ищите Fixpoint s.

Ваши Fixpoint наиболее вероятно работают с терминами, индексированными переменными одного типа Select F A, именно здесь вы хотите использовать индукцию, а не на верхнем уровне цели.

A Fixpoint для терминов, индексированных по типам функций A -> B, бесполезен, так как никакие подтермы любого термина Select не индексируются по типам функций. По той же причине induction бесполезен на таких условиях.

Здесь я думаю, что дисциплина сильного типа на самом деле заставляет вас все проработать на бумаге, прежде чем пытаться что-то делать в Coq (что, на мой взгляд, хорошо). Попробуйте сделать доказательство на бумаге, даже не беспокоясь о типах; явно запишите предикаты, которые вы хотите доказать по индукции. Вот шаблон, чтобы понять, что я имею в виду:

По индукции на u покажем 

 u <*> pure x = pure (fun f => f x) <*> u

    (* Dummy induction predicate for the sake of example. *)
    (* Find the right one. *)
    (* It may use quantifiers... *)

  1. Базовый корпус (набор u = Pure f). Доказать: 

    Pure f <*> pure x = pure (fun f => f x) <*> Pure f

  2. Шаг индукции (установите u = MkSelect v h). Доказать: 

    MkSelect v h <*> pure x = pure (fun f => f x) <*> MkSelect v h

    при условии гипотезы индукции для подтермы v (set u = v): 

    v <*> pure x = pure (fun f => f x) <*> v

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

Если вам действительно нужно использовать Coq для проведения исследования, есть хитрость, заключающаяся в удалении параметра проблемного типа (и всех терминов, которые от него зависят). В зависимости от вашего знакомства с Coq, этот совет может оказаться более запутанным, чем что-либо. Так что будьте осторожны.

Термины будут по-прежнему иметь ту же рекурсивную структуру. Имейте в виду, что доказательство также должно следовать той же структуре, потому что смысл состоит в том, чтобы добавить больше типов сверху, поэтому вам следует избегать ярлыков, которые полагаются на отсутствие типов, если вы можете. 

(* Replace all A and B by unit. *)
Inductive Select_ (F : unit -> Type) : Set :=
| Pure_ : unit -> Select_ F
| MkSelect_ : Select_ F -> F tt -> Select_ F
.

Arguments Pure_ {F}.
Arguments MkSelect_ {F}.

(* Example translating Select_map. The Functor f constraint gets replaced with a dummy function argument. *)
                                        (*      forall A B, (A -> B) -> (F A -> F B) *)
Fixpoint Select_map_ {F : unit -> Type} (fmap : forall t,   unit     -> (F t -> F t)) (f : unit -> unit) (v : Select_ F) : Select_ F :=
  match v with
  | Pure_ a => Pure_ (f a)
  | MkSelect_ w h => MkSelect_ (Select_map_ fmap f w) (fmap _ tt h)
  end.

Этим вы можете попытаться доказать эту урезанную версию законов функторов, например: 

Select_map_ fmap f (Select_map_ fmap g v) = Select_map_ fmap (fun x => f (g x)) v

(* Original theorem:

Select_map f (Select_map g v) = Select_map (fun x => f (g x)) v

*)

Дело в том, что удаление параметра позволяет избежать связанных с этим проблем печати, поэтому вы можете наивно использовать индукцию, чтобы увидеть, как все (не) работает.

...