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

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

1 голос
/ 26 апреля 2020

Я пытаюсь доказать симметрию пропозициональной идентичности с принципом индукции явно в Coq, но не могу сделать это с принципом индукции, как я могу в agda. Я не знаю, как локально объявить переменную в Coq, и при этом я не знаю, как развернуть определение, как вы можете видеть ниже. Как я могу получить доказательство, похожее на приведенное ниже агд? Применить правильные аргументы? Как я могу локально утверждать D и d с помощью тактики (есть где или (пусть a = b in) tacti c?) Применить (Id_ind A x (для всех: A, Id A xa -> Prop)).

Вот код агды, который я пытаюсь эмулировать 

data I (A : Set) (a : A) : A → Set where
r : I A a a

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

refl-I : {A : Set} → (x : A) → I A x x
refl-I x = r

symm-I : {A : Set} → (x y : A) → I A x y → I A y x
symm-I {A} x y p = J2 D d x y p
  where
    D : (x y : A) → I A x y → Set
    D x y p = I A y x
    d : (a : A) → D a a r
    d a = r

Несмотря на то, что coq и agda J не равны, они предположительно взаимозаменяемы.

1 Ответ

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

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

Это должно работать, поскольку теперь D можно развернуть. 

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

(* trivial with induction *)
Theorem symId {A} {x y} : Id A x y -> Id A y x.
Proof.
  intros.
  induction H.
  apply refl.
Qed.

Check Id_ind.
(* Id_ind *)
(*      : forall (A : Type) (x : A) (P : forall a : A, Id A x a -> Prop), *)
(*        P x (refl A x) -> forall (y : A) (i : Id A x y), P y i *)

Theorem D {A} (x y : A) : Id A x y -> Prop.
Proof.
  intros.
  apply (Id A y x).
Defined.

Theorem d {A} (x : A) : D x x (refl A x).
Proof.
  apply refl.
Qed.

Что касается других ваших вопросов. Вы можете явно использовать индукцию двумя способами. Одним из них является использование Id_rect, Id_rec или Id_ind (они автоматически объявляются при определении Id). Например, 

Definition Id_sym {A: Type} {x y: A}: Id A x y -> Id A y x :=
Id_ind A x (fun y' _ => Id A y' x) (refl A x) y.

(использование некоторых неявных аргументов может облегчить чтение).

В конечном итоге это преобразуется в оператор сопоставления, так что вы также можете использовать его. 

Definition Id_sym' {A: Type} {x y: A} (p: Id A x y): Id A y x :=
  match p with
  | refl _ _ => refl _ _
  end.

Чтобы объявить локальную переменную в определении, вы можете использовать форму let var := term in term. Например, Id_sym выше можно переписать как 

Definition Id_sym'' {A: Type} {x y: A}: Id A x y -> Id A y x :=
let P := (fun y' _ => Id A y' x) in
Id_ind A x P (refl A x) y.
...