blob: 9af719322f1ecd7c6b130cd87b27037598f78650 (
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
|
Set Primitive Projections.
Record R := C { p : nat }.
(* R is defined
p is defined *)
Unset Primitive Projections.
Record R' := C' { p' : nat }.
Fail Definition f := fix f (x : R) : nat := p x.
(** Not allowed to make fixpoint defs on (non-recursive) records
having eta *)
Fail Definition f := fix f (x : R') : nat := p' x.
(** Even without eta (R' is not primitive here), as long as they're
found to be BiFinite (non-recursive), we disallow it *)
(*
(* Subject reduction failure example, if we allowed fixpoints *)
Set Primitive Projections.
Record R := C { p : nat }.
Definition f := fix f (x : R) : nat := p x.
(* eta rule for R *)
Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x
:= v.
Definition goal := forall x, f x = p x.
(* when we compute the Rtr away typechecking will fail *)
Definition thing : goal := fun x =>
(Rtr (fun x => f x = p x) x (eq_refl _)).
Definition thing' := Eval compute in thing.
Fail Check (thing = thing').
(*
The command has indeed failed with message:
The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)"
and "f x = p x").
*)
Definition thing_refl := eq_refl thing.
Fail Definition thing_refl' := Eval compute in thing_refl.
(*
The command has indeed failed with message:
Illegal application:
The term "@eq_refl" of type "forall (A : Type) (x : A), x = x"
cannot be applied to the terms
"forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop"
"fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
which should be coercible to
"forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)".
*)
Definition more_refls : thing_refl = thing_refl.
Proof.
compute. reflexivity.
Fail Defined. Abort.
*)
|
