Add documentation for CClosure.to_constr and

overhaul documentation for esubst lifts

Author: yannl35133

kernel/cClosure.ml

@@ -504,7 +504,20 @@ let subst_context e ctx =
   in
   snd @@ subst_context ctx
 
-(* The inverse of mk_clos: move back to constr *)
+(** The inverse of mk_clos: move back to constr
+    Assuming [Γ ⊢ lfts : Δ] and [Δ ⊢ v],
+    we get [Γ ⊢ to_constr lfts v]
+
+    Crucially, in the case of [FLIFT]s which are the sole reason
+    why lifts are needed here, we have the following:
+    assuming [Γ ⊢ lfts : Δ, Δ'] and [Δ, Δ' ⊢ FLIFT(|Δ'|, v)] (i.e. [Δ ⊢ v])
+    we get [Γ ⊢ el_shft n lfts : Δ]; so [Γ ⊢ to_constr (el_shftn n lfts) v]
+
+    In cases like [FCLOS(t, σ)] where substitutions happen,
+    we have [Γ ⊢ lfts : Δ], [Δ ⊢ σ : Ξ] and [Ξ ⊢ v]
+    so we compute [Γ ⊢ comp_subs lfts σ : Ξ]
+    where [comp_subs lfts σ] returns a constr substitution,
+    that can be applied to [v] *)
 let rec to_constr lfts v =
   match v.term with
     | FRel i -> mkRel (reloc_rel i lfts)

kernel/esubst.ml

@@ -19,8 +19,8 @@ open Util
 (*********************)
 
 (* Explicit lifts and basic operations *)
-(* Invariant to preserve in this module: no lift contains two consecutive
-    [ELSHFT] nor two consecutive [ELLFT]. *)
+(* Invariant to preserve in this module: no lift contains an [ELLFT] of [ELID],
+    two consecutive [ELLFT] or two consecutive [ELSHFT]. *)
 
 (* Terminology comes from substitution calculi (see e.g. Hardin et al.).
    That is, what is called a lift in Rocq is made of what is called in
@@ -29,9 +29,15 @@ open Util
    can be iterated as represented in the type [lift] *)
 type lift =
   | ELID
-  | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
-  | ELLFT of int * lift  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
-                         (*                 i.e under n binders *)
+  (** [id] in substitution calculi; for all [Γ], [Γ ⊢ ELID : Γ] *)
+
+  | ELSHFT of lift * int
+  (** [↑^n ∘ σ] in substitution calculi (i.e. a shift of [n], then [σ]);
+      assuming [Γ ⊢ σ : Δ, Ξ] and [n = |Ξ|], then [Γ ⊢ ELSHFT (σ, n) : Δ] *)
+
+  | ELLFT of int * lift
+  (** [⇑^n(σ)] in substitution calculi (i.e. [σ] under [n] binders);
+      assuming [Γ ⊢ σ : Δ] and [n = |Ξ|], then [Γ, Ξ ⊢ ELLFT (n, σ) : Δ, Ξ] *)
 
 let el_id = ELID
 
@@ -268,21 +274,35 @@ let rec lift_subst mk e s = match s with
 module Internal =
 struct
 
-type weakening = LIFT of int * weakening | WEAK of int * weakening | ID
-(* More intuitive representation for weakenings
-   Instead of using ELSHFT (s ⟼ ↑^n ∘ s), uses WEAK (s ⟼ s ∘ ↑^n) *)
+(** More intuitive representation for weakenings
+    Instead of using ELSHFT (s ⟼ ↑^n ∘ s), uses WEAK (s ⟼ s ∘ ↑^n) *)
+type weakening =
+  | ID
+  (** [id] in substitution calculi; for all [Γ], [Γ ⊢ ID : Γ] *)
+
+  | LIFT of int * weakening
+  (** [⇑^n(σ)] in substitution calculi (i.e. [σ] under [n] binders);
+      assuming [Γ ⊢ σ : Δ] and [n = |Ξ|], then [Γ, Ξ ⊢ LIFT (n, σ) : Δ, Ξ] *)
+
+  | WEAK of int * weakening
+  (** [σ ∘ ↑^n] in substitution calculi (i.e. [σ], then a shift of [n]);
+      assuming [Γ ⊢ σ : Δ] and [n = |Ξ|], then [Γ, Ξ ⊢ WEAK (n, σ) : Δ] *)
 
 (* compose a relocation of magnitude n *)
 let weak n = function
   | WEAK (k, w) -> WEAK (k+n, w)
   | w           -> WEAK (n, w)
+
+(** Assuming [Γ ⊢ σ : Δ] and [|Ξ| = n], then [Γ, Ξ ⊢ weak n σ : Δ] *)
 let weak n w = if Int.equal n 0 then w else weak n w
 
 (* cross n binders *)
 let lift n = function
   | ID          -> ID
   | LIFT (k, w) -> LIFT (n+k, w)
   | w           -> LIFT (n, w)
+
+(** Assuming [Γ ⊢ σ : Δ] and [|Ξ| = n], then [Γ, Ξ ⊢ lift n σ : Δ, Ξ] *)
 let lift n w = if Int.equal n 0 then w else lift n w
 
 let rec weakening_of_lift pending =

kernel/esubst.mli

@@ -13,13 +13,14 @@
 (** {6 Explicit substitutions } *)
 (** Explicit substitutions for some type of terms ['a].
 
-    Assuming terms enjoy a notion of typability Γ ⊢ t : A, where Γ is a
-    telescope and A a type, substitutions can be typed as Γ ⊢ σ : Δ, where
-    as a first approximation σ is a list of terms u₁; ...; uₙ s.t.
-    Δ := (x₁ : A₁), ..., (xₙ : Aₙ) and Γ ⊢ uᵢ : Aᵢ{u₁...uᵢ₋₁} for all 1 ≤ i ≤ n.
+    Assuming terms enjoy a notion of typability [Γ ⊢ t : A], where [Γ] is a
+    telescope and [A] a type, substitutions can be typed as [Γ ⊢ σ : Δ], where
+    as a first approximation [σ] is a list of terms [[u₁; ...; uₙ]] s.t.
+    [Δ := (x₁ : A₁), ..., (xₙ : Aₙ)] and [Γ ⊢ uᵢ : Aᵢ{u₁...uᵢ₋₁}]
+    for all [1 ≤ i ≤ n].
 
     Substitutions can be applied to terms as follows, and furthermore
-    if Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ t{σ} : A{σ}.
+    if [Γ ⊢ σ : Δ] and [Δ ⊢ t : A], then [Γ ⊢ t{σ} : A{σ}].
 
     We make the typing rules explicit below, but we omit the explicit De Bruijn
     fidgetting and leave relocations implicit in terms and types.
@@ -29,79 +30,82 @@ type 'a subs
 
 (** Derived constructors granting basic invariants *)
 
-(** Assuming |Γ| = n, Γ ⊢ subs_id n : Γ *)
+(** Assuming [|Γ| = n], [Γ ⊢ subs_id n : Γ] *)
 val subs_id : int -> 'a subs
 
-(** Assuming Γ ⊢ σ : Δ and Γ ⊢ t : A{σ}, then Γ ⊢ subs_cons t σ : Δ, A *)
+(** Assuming [Γ ⊢ σ : Δ] and [Γ ⊢ t : A{σ}], then [Γ ⊢ subs_cons t σ : Δ, A] *)
 val subs_cons: 'a -> 'a subs -> 'a subs
 
-(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_shft (n, σ) : Δ *)
+(** Assuming [Γ ⊢ σ : Δ] and [|Ξ| = n], then [Γ, Ξ ⊢ subs_shft (n, σ) : Δ] *)
 val subs_shft: int * 'a subs -> 'a subs
 
-(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ *)
+(** Assuming [Γ ⊢ σ : Δ] and [|Ξ| = n], then [Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ] *)
 val subs_liftn: int -> 'a subs -> 'a subs
 
 (** Unary variant of {!subst_liftn}. *)
 val subs_lift: 'a subs -> 'a subs
 
 (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
-    [subs]. The result is either (Inl(lams,v)) when the variable is
-    substituted by value [v] under [lams] binders (i.e. v *has* to be
-    shifted by [lams]), or (Inr (k',p)) when the variable k is just relocated
-    as k'; p is None if the variable points inside subs and Some(k) if the
-    variable points k bindings beyond subs (cf argument of ESID).
+    [subs]. The result is either [Inl (lams, v)] when the variable is
+    substituted by value [v] under [lams] binders (i.e. [v] *has* to be
+    shifted by [lams]), or [Inr (k', p)] when the variable [k] is just
+    relocated as [k']; [p] is [None] if the variable points inside [subs]
+    and [Some k] if the variable points [k] bindings beyond [subs]
+    (cf argument of [ESID]).
 *)
 val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
 
 (** Tests whether a substitution behaves like the identity *)
 val is_subs_id: 'a subs -> bool
 
-(** {6 Compact representation } *)
+(** {6 Compact representation} *)
 (** Compact representation of explicit relocations
-    - [ELSHFT(l,n)] == lift of [n], then apply [lift l].
-    - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders.
+    - [ELID]: identity relocation [id]
+    - [ELSHFT (σ, n)]: shift of [n], then [σ]; [↑^n ∘ σ] in sigma calculi
+    - [ELLFT (n, σ)]: apply [σ] to de Bruijn > [n], i.e under [n] binders;
+      [⇑^n(σ)] in sigma calculi
 
-    Invariant ensured by the private flag: no lift contains two consecutive
-    [ELSHFT] nor two consecutive [ELLFT].
+    Invariant ensured by the private flag: no lift contains an [ELLFT] of [ELID],
+    two consecutive [ELLFT] or two consecutive [ELSHFT].
 
     Relocations are a particular kind of substitutions that only contain
-    variables. In particular, [el_*] enjoys the same typing rules as the
+    variables. In particular, [el_*] enjoys similar typing rules as the
     equivalent substitution function [subs_*].
 *)
 type lift = private
   | ELID
   | ELSHFT of lift * int
   | ELLFT of int * lift
 
-(** For arbitrary Γ: Γ ⊢ el_id : Γ *)
+(** For arbitrary Γ, [Γ ⊢ el_id : Γ] *)
 val el_id : lift
 
-(** Assuming Γ ⊢ σ : Δ₁, Δ₂ and |Δ₂| = n, then Γ ⊢ el_shft n σ : Δ₁ *)
+(** Assuming [Γ ⊢ σ : Δ, Ξ] and [|Ξ| = n], then [Γ ⊢ el_shft n σ : Δ] *)
 val el_shft : int -> lift -> lift
 
-(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ el_liftn n σ : Δ, Ξ *)
+(** Assuming [Γ ⊢ σ : Δ] and [|Ξ| = n], then [Γ, Ξ ⊢ el_liftn n σ : Δ, Ξ] *)
 val el_liftn : int -> lift -> lift
 
 (** Unary variant of {!el_liftn}. *)
 val el_lift : lift -> lift
 
-(** Assuming Γ₁, A, Γ₂ ⊢ σ : Δ₁, A, Δ₂ and Δ₁, A, Δ₂ ⊢ n : A,
-    then Γ₁, A, Γ₂ ⊢ reloc_rel n σ : A *)
+(** Assuming [Γ₁, A, Γ₂ ⊢ σ : Δ₁, A, Δ₂] and [Δ₁, A, Δ₂ ⊢ n : A],
+    then [Γ₁, A, Γ₂ ⊢ reloc_rel n σ : A] *)
 val reloc_rel : int -> lift -> int
 
 val is_lift_id : lift -> bool
 
 (** Lift applied to substitution: [lift_subst mk_clos el s] computes a
-    substitution equivalent to applying el then s. Argument
-    mk_clos is used when a closure has to be created, i.e. when
-    el is applied on an element of s.
+    substitution equivalent to applying [el] then [s]. Argument
+    [mk_clos] is used when a closure has to be created, i.e. when
+    [el] is applied on an element of [s].
 
-    That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ.
+    That is, if [Γ ⊢ e : Δ] and [Δ ⊢ σ : Ξ], then [Γ ⊢ lift_subst mk e σ : Ξ].
 *)
 val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs
 
+(** Structural equality for lifts *)
 val eq_lift : lift -> lift -> bool
-(** Equality for lifts *)
 
 (** Debugging utilities *)
 module Internal :