blob: 8334322c99d065220759923b54072b9e7344bb89 (
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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
(* Nijmegen expects redefinition of sorts *)
Definition CProp := Prop.
Record test : CProp := {n : nat ; m : bool ; _ : n <> 0 }.
Require Import Program.
Require Import List.
Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
Implicit Arguments vector [].
Coercion vec_list : vector >-> list.
Hint Rewrite @vec_len : datatypes.
Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *).
Obligation Tactic := crush.
Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.
Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) :=
{| vec_list := cons a (vec_list v) |}.
Hint Rewrite map_length rev_length : datatypes.
Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n :=
{| vec_list := map f v |}.
Program Definition vreverse {A n} (v : vector A n) : vector A n :=
{| vec_list := rev v |}.
Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B :=
match v, w with
| nil, nil => nil
| cons f fs, cons x xs => cons (f x) (va_list fs xs)
| _, _ => nil
end.
Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n :=
{| vec_list := va_list v w |}.
Next Obligation.
destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
subst n. revert w Hw. induction v ; destruct w ; crush.
rewrite IHv ; auto.
Qed.
(* Correct type inference of record notation. Initial example by Spiwack. *)
Inductive Machin := {
Bazar : option Machin
}.
Definition bli : Machin :=
{| Bazar := Some ({| Bazar := None |}:Machin) |}.
Definition bli' : option (option Machin) :=
Some (Some {| Bazar := None |} ).
Definition bli'' : Machin :=
{| Bazar := Some {| Bazar := None |} |}.
Definition bli''' := {| Bazar := Some {| Bazar := None |} |}.
(** Correctly use scoping information *)
Require Import ZArith.
Record Foo := { bar : Z }.
Definition foo := {| bar := 0 |}.
(** Notations inside records *)
Require Import Relation_Definitions.
Record DecidableOrder : Type :=
{ A : Type
; le : relation A where "x <= y" := (le x y)
; le_refl : reflexive _ le
; le_antisym : antisymmetric _ le
; le_trans : transitive _ le
; le_total : forall x y, {x <= y}+{y <= x}
}.
(* Test syntactic sugar suggested by wish report #2138 *)
Record R : Type := {
P (A : Type) : Prop := exists x : A -> A, x = x;
Q A : P A -> P A
}.
|
