Доказательство со списком в Coq - PullRequest
Новая
       6

Доказательство со списком в Coq

0 голосов
/ 04 декабря 2018

Я пытаюсь что-то доказать в CoqIDE (для школы).Я блокирую на шаг, вот это 

`Print length. (* la longueur de listes *)


Lemma mystere A:  forall l : list A, length l = 0 <-> l = nil.
intros.
destruct l.
* split.
- intros.
reflexivity.
- intros. 
simpl.
reflexivity.
* split.
- intros.
???? <- I have tried many things, but without success..
Admitted.
`

Спасибо, ребята, за ваше внимание!

1 Ответ

0 голосов
/ 04 декабря 2018

В вашем контексте есть гипотеза 

H : length (a :: l) = 0

Это абсурд, потому что length (a :: l) является преемником.Вы можете увидеть это, запустив simpl in * или simpl in H, что приведет к 

H : S (length l) = 0

Если вы сейчас запустите 

Search (S _) 0.

, вторая запись (после H) будет 

O_S: forall n : nat, 0 <> S n

Таким образом, мы можем запустить symmetry in H, чтобы получить гипотезу, которая лучше соответствует O_S. 

H : 0 = S (length l)

Поскольку a <> b - это просто a = b -> False, теперь мы можем запуститьapply O_S in H чтобы получить 

H : False

И теперь мы фактически закончили.Мы можем закончить доказательство с помощью exfalso; assumption, или exfalso; exact H, или easy, или now trivial (или now idtac), или case H, или destruct H, или elim H или с refine match H with end, или с induction H, или с refine (False_rect _ H), или tauto.Все это в основном означает одно и то же (хотя некоторые из них, такие как easy и tauto, также могут решать другие задачи).

...