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
|
le_n: forall n : nat, n <= n
le_0_n: forall n : nat, 0 <= n
le_S: forall n m : nat, n <= m -> n <= S m
le_n_S: forall n m : nat, n <= m -> S n <= S m
le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
le_S_n: forall n m : nat, S n <= S m -> n <= m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
min_r: forall n m : nat, m <= n -> Nat.min n m = m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
le_ind:
forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall n0 : nat, n <= n0 -> P n0
false: bool
true: bool
is_true: bool -> Prop
negb: bool -> bool
eq_true: bool -> Prop
implb: bool -> bool -> bool
orb: bool -> bool -> bool
andb: bool -> bool -> bool
xorb: bool -> bool -> bool
Nat.even: nat -> bool
Nat.odd: nat -> bool
BoolSpec: Prop -> Prop -> bool -> Prop
Nat.eqb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Nat.ltb: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
eq_true_rec:
forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
eq_true_ind:
forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
eq_true_rect_r:
forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
eq_true_rec_r:
forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
eq_true_rect:
forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
eq_true_ind_r:
forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
andb_true_intro:
forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
BoolSpec_ind:
forall (P Q : Prop) (P0 : bool -> Prop),
(P -> P0 true) ->
(Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
bool_choice:
forall (S : Set) (R1 R2 : S -> Prop),
(forall x : S, {R1 x} + {R2 x}) ->
{f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
mult_n_O: forall n : nat, 0 = n * 0
plus_O_n: forall n : nat, 0 + n = n
plus_n_O: forall n : nat, n = n + 0
n_Sn: forall n : nat, n <> S n
pred_Sn: forall n : nat, n = Nat.pred (S n)
O_S: forall n : nat, 0 <> S n
f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
eq_S: forall x y : nat, x = y -> S x = S y
eq_add_S: forall n m : nat, S n = S m -> n = m
min_r: forall n m : nat, m <= n -> Nat.min n m = m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
not_eq_S: forall n m : nat, n <> m -> S n <> S m
mult_n_Sm: forall n m : nat, n * m + n = n * S m
f_equal2_plus:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
f_equal2_mult:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
f_equal2_nat:
forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
andb_true_intro:
forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
bool_choice:
forall (S : Set) (R1 R2 : S -> Prop),
(forall x : S, {R1 x} + {R2 x}) ->
{f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
andb_true_intro:
forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h: n <> newdef n
h: n <> newdef n
h': newdef n <> n
The command has indeed failed with message:
No such goal.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
h: P n
h': ~ P n
h: P n
h': ~ P n
h: P n
h': ~ P n
h: P n
h: P n
|
