在 coq 中推广一组证明

Question

我正在尝试完成 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 需要一些谷歌搜索......），第二个练习的提示说 'Hint: The same proof will work for every example.' 但我我不确定如何为每个不特定于该案例的证明编写证明。

相关课程 material 可在此处找到：http://6826.csail.mit.edu/2017/lab/lab0.html

作为 Coq 的初学者，我很高兴被引导到正确的方向，而不是仅仅得到一个解决方案。如果有一种特定的策略在这里很有用，我可能会遗漏，那么指出它会很好......

Answer 1

我认为你只是错过了 intuition 策略，当它看到 A -> B 时 intro 的假设，展开 ~P 到 P -> False 并且intro's that, split the /\s and /s in the hypotheses, breaking /\s in the goal into multiple subgoals, and use auto search to both branches of \/s in 假设目标。这可能看起来很多，但请注意，这些都是逻辑上的基本策略（除了调用 auto）。

在你运行简单地完成这些练习后，你会发现它适合这种形式，然后 intuition 就可以了。

在 coq 中推广一组证明

Generalising a set of proofs in coq

theorem-proving

coq