blob: 5b87e877bfd1ef9dbf276f4b9d77a6d54e86d353 (
plain)
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
|
Require Import TestSuite.admit.
(* Check that inversion of names of mutual inductive fixpoints works *)
(* (cf bug #1031) *)
Inductive tree : Set :=
| node : nat -> forest -> tree
with forest : Set :=
| leaf : forest
| cons : tree -> forest -> forest
.
Definition copy_of_compute_size_forest :=
fix copy_of_compute_size_forest (f:forest) : nat :=
match f with
| leaf => 1
| cons t f0 => copy_of_compute_size_forest f0 + copy_of_compute_size_tree t
end
with copy_of_compute_size_tree (t:tree) : nat :=
match t with
| node _ f => 1 + copy_of_compute_size_forest f
end for copy_of_compute_size_forest
.
Eval simpl in (copy_of_compute_size_forest leaf).
(* Another interesting case: Hrec has to occurrences: one cannot be folded
back to f while the second can. *)
Parameter g : (nat->nat)->nat->nat->nat.
Definition f (n n':nat) :=
nat_rec (fun _ => nat -> nat)
(fun x => x)
(fun k Hrec => g Hrec (Hrec k))
n n'.
Goal forall a b, f (S a) b = b.
intros.
simpl.
admit.
Qed. (* Qed will fail if simpl performs eta-expansion *)
(* Yet another example. *)
Require Import List.
Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i.
simpl.
admit.
Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *)
(* Check that maximally inserted arguments do not break interpretation
of references in simpl, vm_compute etc. *)
Arguments fst {A} {B} p.
Goal fst (0,0) = 0.
simpl fst.
Fail set (fst _).
Abort.
Goal fst (0,0) = 0.
vm_compute fst.
Fail set (fst _).
Abort.
Goal let f x := x + 0 in f 0 = 0.
intro.
vm_compute f.
Fail set (f _).
Abort.
(* This is a change wrt 8.4 (waiting to know if it breaks script a lot or not)*)
Goal 0+0=0.
Fail simpl @eq.
Abort.
(* Check reference by notation in simpl *)
Goal 0+0 = 0.
simpl "+".
Fail set (_ + _).
Abort.
(* Check occurrences *)
Record box A := Box { unbox : A }.
Goal unbox _ (unbox _ (unbox _ (Box _ (Box _ (Box _ True))))) =
unbox _ (unbox _ (unbox _ (Box _ (Box _ (Box _ True))))).
simpl (unbox _ (unbox _ _)) at 1.
match goal with |- True = unbox _ (unbox _ (unbox _ (Box _ (Box _ (Box _ True))))) => idtac end.
Undo 2.
Fail simpl (unbox _ (unbox _ _)) at 5.
simpl (unbox _ (unbox _ _)) at 1 4.
match goal with |- True = unbox _ (Box _ True) => idtac end.
Undo 2.
Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *)
simpl (unbox _ (unbox _ _)) at 2 4.
match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end.
Abort.
(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *)
Goal 2=1+1.
match goal with |- (_ = ?c) => simpl c end.
match goal with |- 2 = 2 => idtac end. (* Check that it reduced *)
Abort.
|
