-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathnostutter.v
124 lines (106 loc) · 2.5 KB
/
nostutter.v
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
(* Import Nat. *)
Local Open Scope nat_scope.
Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Example test_nostutter_1: nostutter [3;1;4;1;5;6].
Proof.
repeat constructor; apply Nat.eqb_neq; auto.
Qed.
Example test_nostutter_1_1: nostutter [3;1;4;1;5;6].
Proof.
constructor; try (apply Nat.eqb_neq).
Abort.
Example test_nostutter_1_2: nostutter [3;1;4;1;5;6].
Proof.
(* [3;1;4;1;5;6] *)
constructor.
2: {apply Nat.eqb_neq. trivial. }
(* [1;4;1;5;6] *)
constructor.
2: {apply Nat.eqb_neq. simpl. reflexivity. }
(* [4;1;5;6] *)
constructor.
2: {apply Nat.eqb_neq. auto. }
(* [1;5;6] *)
constructor.
2: {apply Nat.eqb_neq. auto. }
(* [5;6] *)
constructor.
2: {apply Nat.eqb_neq. auto. }
(* [6], ns_one applied*)
constructor.
Qed.
(* do tactical *)
Example test_nostutter_1_3: nostutter [3;1;4;1;5;6].
Proof.
do 5 (constructor 3; [ | apply Nat.eqb_neq; auto ]).
constructor.
Qed.
Example test_nostutter_1_4: nostutter [3;1;4;1;5;6].
Proof.
do 5 (constructor 3; [ | auto using Nat.eqb_neq ]).
constructor.
Qed.
Example test_nostutter_1_5: nostutter [3;1;4;1;5;6].
Proof.
do 5 (constructor 3; auto using Nat.eqb_neq).
constructor.
Qed.
Hint Constructors nostutter.
Example test_nostutter_1_6: nostutter [3;1;4;1;5;6].
Proof.
auto 6 using Nat.eqb_neq.
Qed.
Example test_nostutter_1_7: nostutter [3;1;4;1;5;6].
Proof.
auto 6.
Qed.
(* test_nostutter_4 *)
Example test_nostutter_4: not (nostutter [3;1;1;4]).
Proof.
intro.
repeat match goal with
h: nostutter _ |- _ => inversion h; clear h; subst
end.
contradiction.
Qed.
(* unfold not in H5. *)
(* specialize (H5 eq_refl). *)
(* subst tactic *)
Lemma equality_commutes:
forall (a: bool) (b: bool), a = b -> b = a.
Proof.
intros.
subst a.
reflexivity.
Qed.
Example test_nostutter_4_3commands: not (nostutter [3;1;1;4]).
Proof.
intro.
inversion H.
clear H.
subst.
Abort.
Example test_nostutter_manual: not (nostutter [3;1;1;4]).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
unfold not in H2.
specialize (H2 eq_refl).
apply H2.
Qed.
Example test_nostutter_4_clear: not (nostutter [3;1;1;4]).
Proof.
intro.
repeat match goal with
H: nostutter _ |- _ => inversion_clear H
end.
contradiction.
Qed.