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 typing in the presence of let-in in inductive arity *)
Inductive I : let a := 1 in a=a -> let b := 2 in Type := C : I (eq_refl).
Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl end = eq_refl.
intro.
match goal with |- ?c => let x := eval cbv in c in change x end.
Abort.
Check forall x:I eq_refl, match x in I x return x = x with C => eq_refl end = eq_refl.
(* This is bug #3210 *)
Inductive I' : let X := Set in X :=
| C' : I'.
Definition foo (x : I') : bool :=
match x with
C' => true
end.
(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *)
Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type :=
E2 : I2 A nat.
Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
E2 _ => (0,0,(0,0))
end.
(* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
Inductive IND : forall X:Type, let Y:=X in Type :=
CONSTR : IND True.
Definition F (x:IND True) (A:Type) :=
(* This failed in 8.5beta2 though it should have been accepted *)
match x in IND X Y return Y with
CONSTR => Logic.I
end.
Theorem paradox : False.
(* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
Fail Proof (F C False).
Abort.
(* Another bug found in November 2015 (a substitution was wrongly
reversed at pretyping level) *)
Inductive Ind (A:Type) :
let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type :=
Constr : Ind A nat.
Check fun x:Ind bool nat =>
match x in Ind _ X Y Z return Z with
| Constr _ => (true,0)
end.
(* A vm_compute bug (the type of constructors was not supposed to
contain local definitions before proper parameters) *)
Inductive Ind2 (b:=1) (c:nat) : Type :=
Constr2 : Ind2 c.
Eval vm_compute in Constr2 2.
(* A bug introduced in ade2363 (similar to #5322 and #5324). This
commit started to see that some List.rev was wrong in the "var"
case of a pattern-matching problem but it failed to see that a
transformation from a list of arguments into a substitution was
still needed. *)
(* The order of real arguments was made wrong by ade2363 in the "var"
case of the compilation of "match" *)
Inductive IND2 : forall X Y:Type, Type :=
CONSTR2 : IND2 unit Empty_set.
Check fun x:IND2 bool nat =>
match x in IND2 a b return a with
| y => _
end = true.
(* From January 2017, using the proper function to turn arguments into
a substitution up to a context possibly containing let-ins, so that
the following, which was wrong also before ade2363, now works
correctly *)
Check fun x:Ind bool nat =>
match x in Ind _ X Y Z return Z with
| y => (true,0)
end.
|
