Quelle injection.v Sprache: Coq

(* 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.
Abort.

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.