Pudding's Dinning Hall
0%

SF-Tactics

Posted on Edited on

Tactics（上）

在写SF练习答案的时候顺便水点博客
答案只能保证正确，不保证是最简单的
不写主观题

练习：2 星, standard, optional (silly_ex)

1
2
3
4
5
6
7
Theorem silly_ex :
     (forall n, evenb n = true -> oddb (S n) = true) ->
     evenb 4 = true ->
     oddb 3 = true.
Proof.
  intros eq1 eq2.
  apply eq1. apply eq2.  Qed.

练习：3 星, standard (apply_exercise1)

1
2
3
4
5
6
7
8
9
10
11
12
Theorem rev_exercise1 : forall (l l' : list nat),
     l = rev l' ->
     l' = rev l.
Proof.
  intros l l' eq1.
  rewrite -> eq1.
  Search rev.
  symmetry.
  apply (rev_involutive nat).
  (* rev_involutive: 
        forall (X : Type) (l : list X), rev (rev l) = l *)
  Qed.

上文第9行的 nat 可加可不加，coq 可以自动推断 Type 是 nat。

练习：3 星, standard, optional (apply_with_exercise)

1
2
3
4
5
6
7
8
Example trans_eq_exercise : forall (n m o p : nat),
     m = (minustwo o) ->
     (n + p) = m ->
     (n + p) = (minustwo o).
Proof.
  intros n m o p eq1 eq2.
  apply trans_eq with (m).
  apply eq2. apply eq1. Qed.

练习：3 星, standard (injection_ex3)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.
Proof.
  intros X x y z l j.
  intros H1 H2.
  injection H1 as H1' H1''.
  rewrite H1'.
  rewrite <- H1'' in H2.
  injection H2 as H2'.
  symmetry.
  apply H2'.
  Qed.

另一种实现（使用apply with（实际上写起来没什么差别）：

1
2
3
4
5
6
7
8
9
10
11
12
13
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.
Proof.
  intros X x y z l j.
  intros H1 H2.
  injection H1 as H1' H1''.
  rewrite <- H1'' in H2.
  injection H2 as H2'.
  apply trans_eq with (z).
  apply H1'. symmetry. apply H2'.
  Qed.

练习：1 星, standard (discriminate_ex3)

1
2
3
4
5
6
7
8
9
Example discriminate_ex3 :
  forall (X : Type) (x y z : X) (l j : list X),
    x :: y :: l = [] ->
    x = z.
Proof.
  intros X x y z l j.
  intros H.
  discriminate H.
  Qed.

练习：2 星, standard (eqb_true)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Theorem eqb_true : forall n m,
    n =? m = true -> n = m.
Proof.
  intros n.
  induction n as [].
  - destruct m as[].
  ++ reflexivity.
  ++ discriminate.
  - destruct m as[|m'].
  ++ discriminate.
  ++ intros H.
    f_equal.
    simpl in H.
    apply IHn in H.
    apply H.
  Qed.

主要是我一开始没看懂上面例题在做什么，intros m n 之后最后一个结论证不出来，应该只intro n，之后 m 是 forall m，所以可以随意取值（应该是这个道理？）。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n'].
  - destruct m as[].
    simpl. reflexivity.
    discriminate.
  - destruct m as[].
    discriminate.
    intros eq.
    simpl in eq.
    apply S_injective' in eq.
    rewrite <-plus_n_Sm in eq.
    rewrite <-plus_n_Sm in eq.
    apply S_injective' in eq.
    f_equal.
    apply IHn' in eq.
    apply eq.
  Qed.

主要就是使用前面的S_injective证明 Sn 单射之后把 S (n' + S n') 转化为 n' + S n' 再用 plus_n_Sm 就行。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
     length l = n ->
     nth_error l n = None.
Proof.
  intros n X l.
  generalize dependent l.
  induction n as [].
  - destruct l.
    reflexivity.
    discriminate.
  - destruct l.
    discriminate.
    intros H.
    simpl.
    simpl in H.
    apply S_injective in H.
    apply IHn in H.
    apply H.
  Qed.

练习：3 星, standard, optional (combine_split)

这个是直接抄的群友的答案，，，主要就是没想到destruct结构

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros X Y l.
  unfold combine. 
  induction l as [| n l' IHl'].
  - simpl. intros.
    injection H as H1 H2.
    rewrite <- H1.
    reflexivity.
  - simpl. intros.
    destruct n as [x y].
    destruct (split l') as [lx ly].
    injection H as H1 H2.
    rewrite <- H1.
    rewrite <- H2.
    f_equal.
    apply IHl'.
    reflexivity.
  Qed.

练习：2 星, standard (destruct_eqn_practice)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
Theorem bool_fn_applied_thrice :
  forall (f : bool -> bool) (b : bool),
  f (f (f b)) = f b.
Proof.
  intros.
  destruct b eqn:Eb.
  -destruct (f b) eqn:Efb.
  --rewrite Eb in Efb.
    rewrite Efb.
    rewrite Efb.
    apply Efb.
  --rewrite Eb in Efb.
    rewrite Efb.
    destruct (f false) eqn:Eft.
    + apply Efb.
    + apply Eft.
  -destruct (f b) eqn:Efb.
  --rewrite Eb in Efb.
    rewrite Efb.
    destruct (f true) eqn:Eft.
    + apply Eft.
    + apply Efb.
  --rewrite Eb in Efb.
    rewrite Efb.
    rewrite Efb.
    apply Efb.
  Qed.

这题对我来说有个大坑，即应用f_equal tactics 时并不会判断函数是否是单射函数（现在想想也正常，coq应该做不到判断函数单射？），如果无脑用的话然后就会出现要求证明 false = true 😂