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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
(* This example, submitted by A. Appel, checks the efficiency of
injection (see bug #1173) *)
(* Expected time < 1.50s *)
Set Implicit Arguments.
Record joinable (t: Type) : Type := Joinable {
is_empty: t -> Prop;
join: t -> t -> t -> Prop;
join_com: forall a b c, join a b c -> join b a c;
join_empty: forall e a b, is_empty e -> join e a b -> a=b;
exists_empty: forall a, exists e, is_empty e /\ join e a a;
join_empty2: forall a b c, join a b c -> is_empty c -> is_empty a;
join_empty3: forall e a, join e a a -> is_empty e;
join_assoc: forall a b c d e, join a b d -> join d c e ->
exists f, join b c f /\ join a f e;
join_eq: forall x y z z', join x y z -> join x y z' -> z = z';
cancellation: forall a1 a2 b c, join a1 b c -> join a2 b c -> a1=a2
}.
Record joinmap (key: Type) (t: Type) (j : joinable t) : Type
:= Joinmap {
jm_t : Type;
jm_j : joinable jm_t;
lookup: jm_t -> key -> t;
prim : forall (f: key -> t) (e: t),
(forall k, j.(join) e (f k) (f k)) ->
jm_t;
join_rule: forall s1 s2 s,
jm_j.(join) s1 s2 s <->
forall x, j.(join) (lookup s1 x) (lookup s2 x) (lookup s x);
empty_rule: forall e x, jm_j.(is_empty) e -> j.(is_empty) (lookup e x);
prim_rule: forall f e pf k, lookup (prim f e pf) k = f k;
ext: forall s1 s2,
(forall x, lookup s1 x = lookup s2 x) <-> s1 = s2;
can_join: forall s1 s2,
(forall x, exists v,
j.(join) (lookup s1 x) (lookup s2 x) v) ->
exists s3, jm_j.(join) s1 s2 s3;
can_split: forall s1 s3,
(forall x, exists v,
j.(join) (lookup s1 x) v (lookup s3 x)) ->
exists s2, jm_j.(join) s1 s2 s3
}.
Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t),
joinmap key j.
Parameter ADMIT: forall p: Prop, p.
Arguments ADMIT [p].
Module Share.
Parameter jb : joinable bool.
Definition jm: joinmap nat jb := mkJoinmap nat jb.
Definition t := jm.(jm_t).
Definition j := jm.(jm_j).
Parameter nonempty: t -> Prop.
End Share.
Section Own.
Variable inv : Type.
Inductive own : Type :=
| NO
| VAL' : forall sh, Share.nonempty sh -> own
| LK : forall sh, Share.nonempty sh -> Share.t -> inv -> own
| CT : forall sh, Share.nonempty sh -> own
| FUN: forall sh, Share.nonempty sh -> inv -> own.
Definition own_join (a b c: own) : Prop :=
match a , b , c with
| NO , _ , _ => b=c
| _ , NO , _ => a=c
| @VAL' sa _, @VAL' sb _, @VAL' sc _ => Share.j.(join) sa sb sc
| @LK sa pa ha fa, @LK sb pb hb fb, @LK sc pc hc fc =>
Share.j.(join) sa sb sc /\
Share.j.(join) ha hb hc /\
fa=fc /\
fb=fc
| @CT sa pa , @CT sb pb, @CT sc pc => Share.j.(join) sa sb sc
| @FUN sa pa fa, @FUN sb pb fb, @FUN sc pc fc =>
Share.j.(join) sa sb sc /\ fa=fc /\ fb=fc
| _ , _ , _ => False
end.
Definition own_is_empty (a: own) := a=NO.
Definition jown : joinable own :=
Joinable own_is_empty own_join
ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT .
End Own.
Fixpoint sinv (n: nat) : Type :=
match n with
| O => unit
| S n => prodT (sinv n) (own (sinv n) -> unit -> Prop)
end.
Parameter address: Set.
Definition jm (n: nat) := mkJoinmap address (jown (sinv n)).
Definition worldfun (n: nat) := (jm n).(jm_t).
Inductive world : Type :=
mk_world: forall n, worldfun n -> world.
Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 ->
n1 = n2.
Proof.
intros.
Timeout 10 Time injection H.
|
