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
|
Set Implicit Arguments.
Module NonPrim.
Unset Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
End NonPrim.
Module Prim.
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
End Prim.
Goal (forall x : NonPrim.prod Set Set, let (a, b) := x in a = a)
/\ (forall x : Prim.prod Set Set, let (a, b) := x in a = a).
Show. (* (forall x : NonPrim.prod Set Set, let (a, _) := x in a = a) /\
(forall x : Prim.prod Set Set,
let a := Prim.fst x in let b := Prim.snd x in a = a) *)
Set Printing All.
Show. (* and
(forall x : NonPrim.prod Set Set,
match x return Prop with
| NonPrim.pair a _ => @eq Set a a
end)
(forall x : Prim.prod Set Set,
let a := @Prim.fst Set Set x in
let b := @Prim.snd Set Set x in @eq Set a a) *)
Unset Printing All.
Abort.
Goal (forall x : NonPrim.prod Set Set, match x with NonPrim.pair a b => a = a end)
/\ (forall x : Prim.prod Set Set, match x with Prim.pair a b => a = a end).
Show. (* (forall x : NonPrim.prod Set Set,
match x with
| {| NonPrim.fst := a |} => a = a
end) /\ (forall x : Prim.prod Set Set, Prim.fst x = Prim.fst x) *)
(** Wrong: [match] should generate unfolded things *)
Set Printing All.
Show. (* and
(forall x : NonPrim.prod Set Set,
match x return Prop with
| NonPrim.pair a _ => @eq Set a a
end)
(forall x : Prim.prod Set Set,
@eq Set (@Prim.fst Set Set x) (@Prim.fst Set Set x)) *)
Unset Printing All.
Abort.
Goal (forall x : NonPrim.prod Set Set, let (a, b) := x in a = a /\ b = b)
/\ (forall x : Prim.prod Set Set, let (a, b) := x in a = a /\ b = b).
Show. (* (forall x : NonPrim.prod Set Set, let (a, b) := x in a = a /\ b = b) /\
(forall x : Prim.prod Set Set,
let a := Prim.fst x in let b := Prim.snd x in a = a /\ b = b) *)
(** Understandably different, maybe, but should still be unfolded *)
Set Printing All.
Show. (* and
(forall x : NonPrim.prod Set Set,
match x return Prop with
| NonPrim.pair a b => and (@eq Set a a) (@eq Set b b)
end)
(forall x : Prim.prod Set Set,
let a := @Prim.fst Set Set x in
let b := @Prim.snd Set Set x in and (@eq Set a a) (@eq Set b b)) *)
Unset Printing All.
Abort.
Goal (forall x : NonPrim.prod Set Set, match x with NonPrim.pair a b => a = a /\ b = b end)
/\ (forall x : Prim.prod Set Set, match x with Prim.pair a b => a = a /\ b = b end).
Show. (* (forall x : NonPrim.prod Set Set,
match x with
| {| NonPrim.fst := a; NonPrim.snd := b |} => a = a /\ b = b
end) /\
(forall x : Prim.prod Set Set,
Prim.fst x = Prim.fst x /\ Prim.snd x = Prim.snd x) *)
Set Printing All.
Show.
set(foo:=forall x : Prim.prod Set Set, match x return Set with
| Prim.pair fst _ => fst
end).
(* and
(forall x : NonPrim.prod Set Set,
match x return Prop with
| NonPrim.pair a b => and (@eq Set a a) (@eq Set b b)
end)
(forall x : Prim.prod Set Set,
and (@eq Set (@Prim.fst Set Set x) (@Prim.fst Set Set x))
(@eq Set (@Prim.snd Set Set x) (@Prim.snd Set Set x))) *)
Unset Printing All.
Abort.
|
