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
|
Set Implicit Arguments.
Module NonPrim.
Local Set Nonrecursive Elimination Schemes.
Record prodwithlet (A B : Type) : Type :=
pair' { fst : A; fst' := fst; snd : B }.
Definition letreclet (p : prodwithlet nat nat) :=
let (x, x', y) := p in x + y.
Definition pletreclet (p : prodwithlet nat nat) :=
let 'pair' x x' y := p in x + y + x'.
Definition pletreclet2 (p : prodwithlet nat nat) :=
let 'pair' x y := p in x + y.
Check (pair 0 0).
End NonPrim.
Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Local Set Nonrecursive Elimination Schemes.
Local Set Primitive Projections.
Record prod (A B : Type) : Type :=
pair { fst : A; snd : B }.
Print prod_rect.
(* What I really want: *)
Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
(p : prod A B) : P p
:= u (fst p) (snd p).
Definition conv : @prod_rect = @prod_rect'.
Proof. reflexivity. Defined.
Definition imposs :=
(fun A B P f (p : prod A B) => match p as p0 return P p0 with
| {| fst := x ; snd := x0 |} => f x x0
end).
Definition letrec (p : prod nat nat) :=
let (x, y) := p in x + y.
Eval compute in letrec (pair 1 5).
Goal forall p : prod nat nat, letrec p = fst p + snd p.
Proof.
reflexivity.
Undo.
intros p.
case p. simpl. unfold letrec. simpl. reflexivity.
Defined.
Eval compute in conv. (* = eq_refl
: prod_rect = prod_rect' *)
Check eq_refl : @prod_rect = @prod_rect'. (* Toplevel input, characters 6-13:
Error:
The term "eq_refl" has type "prod_rect = prod_rect"
while it is expected to have type "prod_rect = prod_rect'"
(cannot unify "prod_rect" and "prod_rect'"). *)
Record sigma (A : Type) (B : A -> Type) : Type :=
dpair { pi1 : A ; pi2 : B pi1 }.
|
