Индукция пути с использованием eq_rect - PullRequest
Новая
       9

Индукция пути с использованием eq_rect

0 голосов
/ 02 сентября 2018

Согласно Теории гомотопического типа (стр. 49), это принцип полной индукции для равенства: 

Definition path_induction (A : Type) (C : forall x y : A, (x = y) -> Type)
           (c : forall x : A, C x x eq_refl) (x y : A) (prEq : x = y)
  : C x y prEq :=
  match prEq with
  | eq_refl => c x
  end.

Я не очень разбираюсь в HoTT, но вижу, что индукция пути сильнее, чем eq_rect: 

Lemma path_ind_stronger : forall (A : Type) (x y : A) (P : A -> Type)
                            (prX : P x) (prEq : x = y),
    eq_rect x P prX y prEq =
    path_induction A (fun x y pr => P x -> P y) (fun x pr => pr) x y prEq prX.
Proof.
  intros. destruct prEq. reflexivity.
Qed.

И наоборот, мне не удалось построить path_induction из eq_rect. Является ли это возможным ? Если нет, то каков правильный принцип индукции для равенства? Я думал, что эти принципы были механически получены из определений типа Inductive.

EDIT

Благодаря ответу ниже полный принцип индукции по равенству может быть сгенерирован 

Scheme eq_rect_full := Induction for eq Sort Prop.

Тогда получаем обратное, 

Lemma eq_rect_full_works : forall (A : Type) (C : forall x y : A, (x = y) -> Prop)
                             (c : forall x : A, C x x eq_refl) (x y : A)
                             (prEq : x = y),
    path_induction A C c x y prEq
    = eq_rect_full A x (fun y => C x y) (c x) y prEq.
Proof.
  intros. destruct prEq. reflexivity.
Qed.

1 Ответ

0 голосов
/ 02 сентября 2018

Я думаю, что вы имеете в виду тот факт, что тип результата path_induction упоминает путь, который разрушается, в то время как тип eq_rect - нет. Это упущение является значением по умолчанию для индуктивных предложений (в отличие от того, что происходит с Type), потому что дополнительный аргумент обычно не используется в разработках, не имеющих отношения к доказательствам. Тем не менее, вы можете указать Coq генерировать более полные принципы индукции с помощью команды Scheme: https://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html?highlight=minimality. (вариант Minimality по умолчанию используется для предложений.)

...