Объекты доказательства в типе удостоверения
Я читаю фонд программного обеспечения, и они определяют равенство как
Inductive eq {X:Type} : X -> X -> Prop :=
| eq_refl : forall x, eq x x.
Notation "x == y" := (eq x y)
(at level 70, no associativity)
: type_scope.
Я смог доказать equality__leibniz_equality с помощью тактики
Lemma equality__leibniz_equality : forall (X : Type) (x y: X),
x == y -> forall P:X->Prop, P x -> P y.
Proof.
intros X x y H P evP. destruct H. apply evP.
Qed.
Однако я также хотел построить объект доказательства. Вот что я пробовал:
Definition equality__leibniz_equality' : forall (X : Type) (x y: X),
x == y -> forall P:X->Prop, P x -> P y :=
fun (X:Type) (x y: X) (H: x==y) (P:X->Prop) (evP: P x) =>
match H with
| eq_refl a => evP
end.
В то время как destruct H сработало в моем первом доказательстве, потому что тактика сразу заменила y на x, однако сопоставление с образцом eq_refl a, похоже, не имеет подобного эффекта, так что кажется, что информация о том, что x=y=a потеряна, и я застрял. Есть ли способ построить объект доказательства?
Ответы 2
Definition equality__leibniz_equality' : forall (X : Type) (x y: X),
x == y -> forall P:X->Prop, P x -> P y :=
fun (X:Type) (x y: X) (H: x==y) (P:X->Prop) =>
match H with
| eq_refl a => fun evP => evP
end.
Лучшее определение eq, которое делает ваше определение успешным:
Inductive eq {X:Type} (x : X) : X -> Prop :=
| eq_refl : eq x x.
Вы можете использовать Print, чтобы посмотреть определение любого идентификатора. Или завершите доказательство Defined вместо Qed, чтобы вычислить его, или разверните его в другом доказательстве.
Также может быть интересно посмотреть на принципы исключения, созданные Coq, и поиграть с Check. С вашим определением:
Check eq_ind.
(*
eq_ind
: forall (X : Type) (P : X -> X -> Prop),
(forall x : X, P x x) -> forall y y0 : X, eq y y0 -> P y y0
*)
Check fun (X: Type)(Q: X -> Prop) =>
eq_ind _ (fun x y => Q x -> Q y) (fun x Hx => Hx).
fun (X : Type) (Q : X -> Prop) =>
eq_ind X (fun x y : X => Q x -> Q y) (fun (x : X) (Hx : Q x) => Hx)
: forall (X : Type) (Q : X -> Prop) (y y0 : X), eq y y0 -> Q y -> Q y0
Вы также можете сравнить эту версию eq с Logic.eq Кока (см. ответ Ли-яо Ся), запросив тип Logic.eq_ind. Обратите внимание, что в вашем определении нет ни eq_rec, ни eq_rect (в отличие от Logic.eq)