?

Log in

No account? Create an account
coq затык - Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

coq затык [Nov. 17th, 2010|09:51 pm]
Программирование с зависимыми типами

ru_deptypes

[zelych]
Подскажите, пожалуйста.
Вот у меня есть индуктивный предикат:
  Inductive last (a: A): list A -> Prop :=
  | last_one: last a (a :: nil)
  | last_many: forall (l: list A) (x: A), last a l -> last a (x :: l).

Очевидно?, что last a nil быть не может. Как тогда доказать что-нибудь типа такого?
  Lemma last_nil: forall (a: A), last a nil -> False.

Спасибо.
LinkReply

Comments:
[User Picture]From: mr_aleph
2010-11-17 07:56 pm (UTC)
intros a b.
inversion_clear b.
(Reply) (Thread)
[User Picture]From: zelych
2010-11-18 07:44 am (UTC)
Спасибо!
Забавно, что в coq'art задачка про last на странице 213, а inversion вводится на 246-й.
(Reply) (Parent) (Thread)
[User Picture]From: mr_aleph
2010-11-18 06:40 pm (UTC)
да не за что, я если честно поступил как макака (monkey see - monkey do) ;-)

пошел скачал Coq, давно хотел посмотреть что за зверь, потом в туториале на их сайте нашел слова индуктивный предикат...

(Reply) (Parent) (Thread)
[User Picture]From: zelych
2010-11-18 06:50 pm (UTC)
Хы. Неплохое начало. Индуктивные предикаты -- это уже почти середина coq'art.
(Reply) (Parent) (Thread)
[User Picture]From: mr_aleph
2010-11-18 08:47 pm (UTC)
для меня это скорее, конец, я "повертел очками так и сяк", куда их приложить не сообразил и убрал в комод =)
(Reply) (Parent) (Thread)