Как определить пользовательский принцип индукции в coq? - PullRequest
Новая
       95

Как определить пользовательский принцип индукции в coq?

2 голосов
/ 27 апреля 2020

Это своего рода продолжение предыдущего вопроса , который я задал, но сейчас я просто пытаюсь реализовать свой собственный принцип индукции для типа равенства, что я не знаю, как это сделать. без какого-либо сопоставления с образцом. Я избегаю использования индуктивной тактики c в приведенном ниже определении, поскольку это, очевидно, приводит к некоторой головоломке «курица против яйца». Есть ли какой-нибудь возможный способ сделать это с помощью некоторых базовых c тактик , кроме indction, а также с помощью ванильного определения J2: = ...? 

(* define a similair induction principle from this agda code*)
J2 : {A : Set} → (D : (x y : A) → (I A x y) →  Set)
  →  (d : (a : A) → (D a a r )) → (x y : A) → (p : I A x y) → D x y p
J2 D d x .x r = d x

Theorem J2 {A} :
  forall (D : forall (x y : A), Id A x y -> Prop), 
  forall (d : forall (a : A), (D a a (refl A a))),
  forall (x y : A) (p : Id A x y), D x y p.
Proof.
  intros.
  inversion p.
  subst.
  apply D y.

Это приводит к следующей ошибке, и я не уверен, как указать, что p должно быть refl без индукции tacti c. 

1 subgoal (ID 34)

  A : Type
  D : forall x y : A, Id A x y -> Prop
  d : forall a : A, D a a (refl A a)
  y : A
  p : Id A y y
  ============================
  D y y p

, что приводит к следующей ошибке. 

Error:
In environment
A : Type
D : forall x y : A, Id A x y -> Prop
d : forall a : A, D a a (refl A a)
y : A
p : Id A y y
Unable to unify "D y y (refl A y)" with "D y y p".

Наконец, несколько сопутствующая ошибка, когда я пытаюсь написать apply d in y, я получаю следующую ошибку: 

Error:
Unable to apply lemma of type "forall a : A, D a a (refl A a)"
on hypothesis of type "A".

Почему проверка типов не устраивает?

Ответы [ 2 ]

2 голосов
/ 27 апреля 2020

Есть ли какой-нибудь возможный способ сделать это с помощью некоторых базовых c тактик, кроме индукции, а также с помощью ванильного определения J2: = ...?

Позвольте мне ответить на вторую часть вашего вопроса: 

Inductive Id (A : Type) (x : A) : A -> Type :=
  | refl : Id A x x.

Definition J2 {A} :
  forall
    (D : forall (x y : A), Id A x y -> Prop)
    (d : forall (a : A), (D a a (refl A a)))
    (x y : A) (p : Id A x y),
    D x y p
:=
  fun D d x y p =>
    match p in Id _ _ y
            return D x y p
    with
    | refl _ _ => d x
    end.
2 голосов
/ 27 апреля 2020

Вместо inversion p используйте destruct p, что делает сопоставление с образцом простым способом.

inversion предназначено только для работы с предположениями, термины доказательства которых не используются в цели. Здесь p используется в цели.

...