Обобщая набор доказательств в coq - PullRequest
Новая
       13

Обобщая набор доказательств в coq

0 голосов
/ 08 ноября 2018

Я пытаюсь завершить первую лабораторную часть курса 6.826 MIT, но я не уверен насчет комментария над одним из упражнений, который говорит, что я могу решить кучу примеров, используя одно и то же доказательство. вот что я имею в виду: 

(* A `nattree` is a tree of natural numbers, where every internal
   node has an associated number and leaves are empty. There are
   two constructors, L (empty leaf) and I (internal node).
   I's arguments are: left-subtree, number, right-subtree. *)
Inductive nattree : Set :=
  | L : nattree                                (* Leaf *)
  | I : nattree -> nat -> nattree -> nattree.  (* Internal nodes *)

(* Some example nattrees. *)
Definition empty_nattree := L.
Definition singleton_nattree := I L 0 L.
Definition right_nattree := I L 0 (I L 1 (I L 2 (I L 3 L))).
Definition left_nattree := I (I (I (I L 0 L) 1 L) 2 L) 3 L.
Definition balanced_nattree := I (I L 0 (I L 1 L)) 2 (I L 3 L).
Definition unsorted_nattree := I (I L 3 (I L 1 L)) 0 (I L 2 L).

(* EXERCISE: Complete this proposition, which should be `True`
   iff `x` is located somewhere in `t` (even if `t` is unsorted,
   i.e., not a valid binary search tree). *)
Function btree_in (x:nat) (t:nattree) : Prop :=
  match t with
    | L => False
    | I l n r => n = x \/ btree_in x l \/ btree_in x r
  end.

(* EXERCISE: Complete these examples, which show `btree_in` works.
   Hint: The same proof will work for every example.
   End each example with `Qed.`. *)
Example btree_in_ex1 : ~ btree_in 0 empty_nattree.
  simpl. auto.
Qed.
Example btree_in_ex2 : btree_in 0 singleton_nattree.
  simpl. auto.
Qed.
Example btree_in_ex3 : btree_in 2 right_nattree.
  simpl. right. auto.
Qed.
Example btree_in_ex4 : btree_in 2 left_nattree.
  simpl. right. auto.
Qed.
Example btree_in_ex5 : btree_in 2 balanced_nattree.
  simpl. auto.
Qed.
Example btree_in_ex6 : btree_in 2 unsorted_nattree.
  simpl. auto.
Qed.
Example btree_in_ex7 : ~ btree_in 10 balanced_nattree.
  simpl. intros G. destruct G. inversion H. destruct H. destruct H. inversion H. 
  destruct H. inversion H. destruct H. inversion H. destruct H. inversion H.  
  destruct H. destruct H. inversion H. destruct H. inversion H. destruct H.
Qed.
Example btree_in_ex8 : btree_in 3 unsorted_nattree.
  simpl. auto.
Qed.

Код под комментариями EXERCISE был выполнен как упражнение (хотя ex7 требовал некоторого поиска в Google ...), подсказка для второго упражнения говорит: «Подсказка: одно и то же доказательство будет работать для каждого примера». но я не уверен, как написать доказательство для каждого, которое не относится к конкретному случаю.

Материал курса, о котором идет речь, можно найти здесь: http://6826.csail.mit.edu/2017/lab/lab0.html

Как новичок в Coq, я был бы признателен за то, что меня направили в правильном направлении, а не просто дали решение. Если есть какая-то особая тактика, которая может быть полезна здесь, и я, возможно, упускаю ее, было бы хорошо указать на это ...

1 Ответ

0 голосов
/ 08 ноября 2018

Я думаю, что вы просто упускаете тактику intuition, которая intro гипотез, когда он видит A -> B, разворачивается ~P до P -> False и intro, разбивает / \ s и/ s в гипотезах разбивает / \ s в цели на несколько подцелей и использует auto для поиска в обеих ветвях \/ s в цели.Это может показаться большим, но обратите внимание, что это все базовые стратегии из логики (кроме вызова auto).

После того, как вы выполнили упрощение для каждого из этих упражнений, вы увидите, что оно соответствует этой формеи тогда intuition будет работать.

...