← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/complexity/injection.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/complexity/injection.v
 
1
(* This example, submitted by A. Appel, checks the efficiency of
 
2
   injection (see bug #1173) *)
 
3
(* Expected time < 1.50s *)
 
4
 
 
5
Set Implicit Arguments.
 
6
 
 
7
Record joinable (t: Type) : Type := Joinable {
 
8
   is_empty: t -> Prop;
 
9
   join: t -> t -> t -> Prop;
 
10
   join_com: forall a b c, join a b c -> join b a c;
 
11
   join_empty: forall e a b, is_empty e -> join e a b -> a=b;
 
12
   exists_empty: forall a, exists e, is_empty e /\ join e a a;
 
13
   join_empty2: forall a b c, join a b c ->  is_empty c -> is_empty a;
 
14
   join_empty3: forall e a, join e a a -> is_empty e;
 
15
   join_assoc: forall a b c d e, join a b d -> join d c e ->
 
16
                    exists f, join b c f /\ join a f e;
 
17
   join_eq: forall x y z z', join x y z -> join x y z' -> z = z';
 
18
   cancellation: forall a1 a2 b c, join a1 b c -> join a2 b c -> a1=a2
 
19
}.
 
20
 
 
21
Record joinmap (key: Type) (t: Type) (j : joinable t) : Type
 
22
 := Joinmap {
 
23
    jm_t : Type;
 
24
    jm_j : joinable jm_t;
 
25
    lookup: jm_t -> key -> t;
 
26
    prim : forall (f: key -> t) (e: t),
 
27
                  (forall k, j.(join) e (f k) (f k)) ->
 
28
                  jm_t;
 
29
    join_rule: forall s1 s2 s,
 
30
                jm_j.(join) s1 s2 s <->
 
31
                forall x, j.(join) (lookup s1 x) (lookup s2 x) (lookup s x);
 
32
    empty_rule: forall e x, jm_j.(is_empty) e -> j.(is_empty) (lookup e x);
 
33
    prim_rule: forall f e pf k, lookup (prim f e pf) k = f k;
 
34
    ext: forall s1 s2,
 
35
        (forall x, lookup s1 x = lookup s2 x) <-> s1 = s2;
 
36
    can_join: forall s1 s2,
 
37
            (forall x, exists v,
 
38
                j.(join) (lookup s1 x) (lookup s2 x) v) ->
 
39
            exists s3, jm_j.(join) s1 s2 s3;
 
40
    can_split: forall s1 s3,
 
41
            (forall x, exists v,
 
42
                j.(join) (lookup s1 x) v (lookup s3 x)) ->
 
43
            exists s2, jm_j.(join) s1 s2 s3
 
44
}.
 
45
 
 
46
Parameter mkJoinmap :   forall (key: Type) (t: Type) (j: joinable t), 
 
47
joinmap key j.
 
48
 
 
49
Parameter ADMIT: forall p: Prop, p.
 
50
Implicit Arguments ADMIT [p].    
 
51
 
 
52
Module Share.
 
53
Parameter jb : joinable bool.
 
54
Definition jm: joinmap nat jb := mkJoinmap nat jb.
 
55
Definition t := jm.(jm_t).
 
56
Definition j := jm.(jm_j).
 
57
Parameter nonempty: t -> Prop.
 
58
End Share.
 
59
 
 
60
Section Own.
 
61
 
 
62
Variable inv : Type.
 
63
 
 
64
Inductive own : Type :=
 
65
  | NO
 
66
  | VAL' : forall sh, Share.nonempty sh -> own
 
67
  | LK : forall sh, Share.nonempty sh -> Share.t -> inv -> own
 
68
  | CT : forall sh, Share.nonempty sh -> own
 
69
  | FUN: forall sh, Share.nonempty sh -> inv -> own.
 
70
 
 
71
Definition own_join (a b c: own) : Prop :=
 
72
 match a , b , c with
 
73
  | NO , _ , _ =>  b=c
 
74
  | _ , NO , _ =>  a=c
 
75
  | VAL' sa _ , VAL' sb _, VAL' sc _ => Share.j.(join) sa sb sc
 
76
  | LK sa pa ha fa, LK sb pb hb fb, LK sc pc hc fc =>
 
77
      Share.j.(join) sa sb sc /\
 
78
      Share.j.(join) ha hb hc /\
 
79
      fa=fc /\
 
80
      fb=fc
 
81
  | CT sa pa , CT sb pb, CT sc pc => Share.j.(join) sa sb sc
 
82
  | FUN sa pa fa, FUN sb pb fb, FUN sc pc fc =>
 
83
        Share.j.(join) sa sb sc /\ fa=fc /\ fb=fc
 
84
  | _ , _ , _ => False
 
85
 end.
 
86
 
 
87
Definition own_is_empty (a: own) := a=NO.
 
88
 
 
89
Definition jown : joinable own :=
 
90
  Joinable own_is_empty own_join
 
91
     ADMIT ADMIT  ADMIT  ADMIT  ADMIT  ADMIT  ADMIT  ADMIT .
 
92
End Own.
 
93
  
 
94
Fixpoint sinv (n: nat) : Type :=
 
95
  match n with
 
96
   | O => unit
 
97
   | S n => prodT (sinv n) (own (sinv n) -> unit -> Prop)
 
98
 end.
 
99
 
 
100
Parameter address: Set.
 
101
 
 
102
Definition jm (n: nat) := mkJoinmap address (jown (sinv n)).
 
103
 
 
104
Definition worldfun (n: nat) := (jm n).(jm_t).
 
105
 
 
106
Inductive world : Type :=
 
107
  mk_world: forall n, worldfun n -> world.
 
108
 
 
109
Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 ->
 
110
         n1 = n2.
 
111
Proof.
 
112
intros.
 
113
Time injection H.