blob: 3efca5d99330e14e67c50709a8912af21a040812 (
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
|
Require Import Equality.
Parameter NameSet : Set.
Parameter SignedName : Set.
Parameter SignedName_compare : forall (x y : SignedName), comparison.
Parameter pu_type : NameSet -> NameSet -> Type.
Parameter pu_nameOf : forall {from to : NameSet}, pu_type from to -> SignedName.
Parameter commute : forall {from mid1 mid2 to : NameSet},
pu_type from mid1 -> pu_type mid1 to
-> pu_type from mid2 -> pu_type mid2 to -> Prop.
Program Definition castPatchFrom {from from' to : NameSet}
(HeqFrom : from = from')
(p : pu_type from to)
: pu_type from' to
:= p.
Class PatchUniverse : Type := mkPatchUniverse {
commutable : forall {from mid1 to : NameSet},
pu_type from mid1 -> pu_type mid1 to -> Prop
:= fun {from mid1 to : NameSet}
(p : pu_type from mid1) (q : pu_type mid1 to) =>
exists mid2 : NameSet,
exists q' : pu_type from mid2,
exists p' : pu_type mid2 to,
commute p q q' p';
commutable_dec : forall {from mid to : NameSet}
(p : pu_type from mid)
(q : pu_type mid to),
{mid2 : NameSet &
{ q' : pu_type from mid2 &
{ p' : pu_type mid2 to &
commute p q q' p' }}}
+ {~(commutable p q)}
}.
Inductive SequenceBase (pu : PatchUniverse)
: NameSet -> NameSet -> Type
:= Nil : forall {cxt : NameSet},
SequenceBase pu cxt cxt
| Cons : forall {from mid to : NameSet}
(p : pu_type from mid)
(qs : SequenceBase pu mid to),
SequenceBase pu from to.
Implicit Arguments Nil [pu cxt].
Implicit Arguments Cons [pu from mid to].
Program Fixpoint insertBase {pu : PatchUniverse}
{from mid to : NameSet}
(p : pu_type from mid)
(qs : SequenceBase pu mid to)
: SequenceBase pu from to
:= match qs with
| Nil => Cons p Nil
| Cons q qs' =>
match SignedName_compare (pu_nameOf p) (pu_nameOf q) with
| Lt => Cons p qs
| _ => match commutable_dec p (castPatchFrom _ q) with
| inleft (existT _ _ (existT _ q' (existT _ p' _))) => Cons q'
(insertBase p' qs')
| inright _ => Cons p qs
end
end
end.
Lemma insertBaseConsLt {pu : PatchUniverse}
{o op opq opqr : NameSet}
(p : pu_type o op)
(q : pu_type op opq)
(rs : SequenceBase pu opq opqr)
(p_Lt_q : SignedName_compare (pu_nameOf p) (pu_nameOf q)
= Lt)
: insertBase p (Cons q rs) = Cons p (Cons q rs).
Proof.
vm_compute.
|
