sf/IndPrinciples.v at master · pzzp/sf · GitHub

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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
Check nat_ind.

Theorem mult_0_r':
  forall n: nat, n * 0 = 0.
Proof.
  apply nat_ind.
  - reflexivity.
  - simpl. intros n H. apply H.
Qed.

Theorem plus_one_r': forall n: nat, n + 1 = S n.
Proof.
  apply nat_ind.
  - reflexivity.
  - intros n H.
    simpl. f_equal. apply H.
Qed.


Inductive time : Type :=
  | day
  | night.
Check time_ind.


Inductive ExSet: Type :=
| con1: bool -> ExSet
| con2: nat -> ExSet -> ExSet.

Check ExSet_ind.

Inductive list (X:Type) : Type :=
        | nil : list X
        | cons : X -> list X -> list X.

Check list_ind.

(*
forall (X: Type) (P: tree X -> Prop),
  (forall x: X, P (leaf x)) ->
  (forall t1: tree X, P t1) ->
  forall t2: tree X, P t2 ->
  P (node t1 t2)) ->
  (forall (t: tree X), P t)
*)
Inductive tree (X:Type) : Type :=
  | leaf (x : X)
  | node (t1 t2 : tree X).
Check tree_ind.


Inductive mytype (X: Type) : Type :=
| constr1: X -> mytype X
| constr2: nat -> mytype X
| constr3: mytype X -> nat -> mytype X.
Check mytype_ind.

Inductive foo (X Y: Type) : Type :=
| bar: X -> foo X Y
| baz: Y -> foo X Y
| quux: (nat->foo X Y) -> foo X Y.
Check foo_ind.


Inductive foo' (X: Type): Type :=
| c1 (l: list X) (f: foo' X)
| c2.

Definition P_m0r : nat->Prop :=
  fun n => n * 0 = 0.

Check foo'_ind.
Theorem mult_0_r'' : forall n:nat,
  P_m0r n.
Proof.
  apply nat_ind.
  - (* n = O *) reflexivity.
  - (* n = S n' *)
    (* 请注意目前的证明状态！ *)
    intros n IHn.
    unfold P_m0r in IHn. unfold P_m0r. simpl. apply IHn.
Qed.

Theorem plus_comm' : forall n m : nat,
  n + m = m + n.
Proof.
  induction n as [| n'].
  - (* n = O *) intros m. rewrite <- plus_n_O. reflexivity.
  - (* n = S n' *) intros m. simpl. rewrite -> IHn'.
    rewrite <- plus_n_Sm. reflexivity.
Qed.