blob: a9821b027f362796b5c85e5aba12947aa5c14d2b (
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
|
(* A few tests of the syntax of clauses and of the interpretation of change *)
Goal let a := 0+0 in a=a.
intro.
change 0 in (value of a).
change ((fun A:Type => A) nat) in (type of a).
Abort.
Goal forall x, 2 + S x = 1 + S x.
intro.
change (?u + S x) with (S (u + x)).
Abort.
(* Check the combination of at, with and in (see bug #2146) *)
Goal 3=3 -> 3=3. intro H.
change 3 at 2 with (1+2).
change 3 at 2 with (1+2) in H |-.
change 3 with (1+2) in H at 1 |- * at 1.
(* Now check that there are no more 3's *)
change 3 with (1+2) in * || reflexivity.
Qed.
(* Note: the following is invalid and must fail
change 3 at 1 with (1+2) at 3.
change 3 at 1 with (1+2) in *.
change 3 at 1 with (1+2) in H at 2 |-.
change 3 at 1 with (1+2) at 3.
change 3 at 1 with (1+2) in H |- *.
change 3 at 1 with (1+2) in H, H|-.
change 3 at 1.
*)
(* Test that pretyping checks allowed elimination sorts *)
Goal True.
Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
Fail change True with
match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
Abort.
(* Check absence of loop in identity substitution (was failing up to
Sep 2014, see #3641) *)
Goal True.
change ?x with x.
Abort.
(* Check typability after change of type subterms *)
Goal nat = nat :> Set.
Fail change nat with (@id Type nat). (* would otherwise be ill-typed *)
Abort.
(* Check typing env for rhs is the correct one *)
Goal forall n, let x := n in id (fun n => n + x) 0 = 0.
intros.
unfold x.
(* check that n in 0+n is not interpreted as the n from "fun n" *)
change n with (0+n).
Abort.
(* Check non-collision of non-normalized defined evars with pattern variables *)
Goal exists x, 1=1 -> x=1/\x=1.
eexists ?[n]; intros; split.
eassumption.
match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
match goal with |- 0+1=1 => trivial end.
Qed.
|
