-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathScopeSystem.v
127 lines (104 loc) · 4.59 KB
/
ScopeSystem.v
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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
Require Import HoTT.
Require Import Auxiliary.Coproduct.
(* A _Scope_ abstract the kind of scopes that contexts and bindings can have.
There are several motivations for this:
- firstly, it allows the same code to simultaneously cover both syntax with
de Bruijn indices and syntax with named variables — those will be two
examples of scope systems.
- secondly, it abstracts just the properties of both those settings that are
really needed in the definition of substitution etc., hence giving a clean
and robust interface.
- thirdly, it is written with an eye towards possible later generalisation
to infinitary settings, where genuinely different scope systems might occur.
*)
(** A record describing scopes that can be used for contexts and bindings.
\cref{def:scope-system} *)
Record scope_system :=
{ scope_carrier :> Type
; scope_position : scope_carrier -> Type
(* each scope has some positions; maybe should map to sets *)
; scope_empty : scope_carrier (* the empty *)
; scope_is_empty : is_empty (scope_position scope_empty)
(* the empty scope binds nothing *)
; scope_sum : scope_carrier -> scope_carrier -> scope_carrier
(* the sum of two scopes *)
; scope_is_sum
(* the positions in the sum are the sum of positions *)
: forall γ δ : scope_carrier,
Coproduct.is_coproduct
(scope_position (scope_sum γ δ)) (scope_position γ) (scope_position δ)
; scope_extend : scope_carrier -> scope_carrier
(* a scope extended by one more more position *)
; scope_is_extend
: forall γ : scope_carrier,
Coproduct.is_plusone (scope_position (scope_extend γ)) (scope_position γ)
}.
Global Arguments scope_sum {_} _ _.
Global Arguments scope_is_sum {_ _ _}.
Global Arguments scope_is_empty {_}.
Coercion scope_position : scope_carrier >-> Sortclass.
Section Associativities.
(** Lemmas on associativity, unitality, etc of sums of scopes.*)
(* TODO: these could be upstreamed to [Coproduct], perhaps?
If that makes them less convenient to apply, then they can at least be deduced
here from general lemmas about coproducts. *)
Context {σ : scope_system}.
(* use this and [fmap1], [fmap2] where they’ve previously been given inline, e.g. in [rename], [instantiate_rename]. *)
Lemma fmap_scope_sum {γ γ' δ δ' : σ} (f : γ -> γ') (g : δ -> δ')
: (scope_sum γ δ) -> (scope_sum γ' δ').
Proof.
refine (coproduct_rect scope_is_sum _ _ _).
- intros; apply (coproduct_inj1 (scope_is_sum)); auto.
- intros; apply (coproduct_inj2 (scope_is_sum)); auto.
Defined.
Lemma fmap1_scope_sum {γ γ' δ : σ} (f : γ -> γ')
: (scope_sum γ δ) -> (scope_sum γ' δ).
Proof.
exact (fmap_scope_sum f idmap).
Defined.
Lemma fmap2_scope_sum {γ δ δ' : σ} (g : δ -> δ')
: (scope_sum γ δ) -> (scope_sum γ δ').
Proof.
exact (fmap_scope_sum idmap g).
Defined.
Definition scope_sum_empty_inl_is_equiv (γ : σ)
: IsEquiv (coproduct_inj1 scope_is_sum
: γ -> scope_sum γ (scope_empty _)).
Proof.
apply coproduct_empty_inj1_is_equiv, scope_is_empty.
Defined.
Definition scope_sum_empty_inl (γ : σ)
: γ <~> scope_sum γ (scope_empty _)
:= Build_Equiv _ _ _ (scope_sum_empty_inl_is_equiv γ).
Definition scope_sum_empty_inr_is_equiv (γ : σ)
: IsEquiv (coproduct_inj2 scope_is_sum
: γ -> scope_sum (scope_empty _) γ).
Proof.
apply coproduct_empty_inj2_is_equiv, scope_is_empty.
Defined.
Definition scope_sum_empty_inr (γ : σ)
: γ <~> scope_sum (scope_empty _) γ
:= Build_Equiv _ _ _ (scope_sum_empty_inr_is_equiv γ).
Definition scope_assoc_ltor {γ δ κ : scope_carrier σ}
: scope_sum (scope_sum γ δ) κ -> scope_sum γ (scope_sum δ κ).
Proof.
simple refine (Coproduct.assoc_ltor _ _ _ _);
try apply scope_is_sum; try apply scope_is_sum.
Defined.
Definition scope_assoc_rtol {γ δ κ : scope_carrier σ}
: scope_sum γ (scope_sum δ κ) -> scope_sum (scope_sum γ δ) κ.
Proof.
simple refine (Coproduct.assoc_rtol _ _ _ _);
try apply scope_is_sum; try apply scope_is_sum.
Defined.
Definition scope_assoc (γ δ κ : scope_carrier σ)
: scope_sum γ (scope_sum δ κ) <~> scope_sum (scope_sum γ δ) κ.
Proof.
simple refine (equiv_adjointify scope_assoc_rtol scope_assoc_ltor _ _);
unfold pointwise_paths.
- apply Coproduct.assoc_ltortol; apply scope_is_sum.
- apply Coproduct.assoc_rtoltor; apply scope_is_sum.
Defined.
Instance scope_assoc_is_equiv {γ δ κ} : IsEquiv (scope_assoc γ δ κ)
:= equiv_isequiv (scope_assoc _ _ _).
End Associativities.