Merge branch 'ctx-overhaul' into alectryon

Makefile

@@ -11,8 +11,9 @@ doc:
 		--frontend coq+rst \
 		--coq-driver sertop \
 		--webpage-style windowed \
+		--long-line-threshold 100 \
 		-Q _build/default/theories OGS \
-		theories/**/*.v
+		theories/*.v theories/**/*.v
 
 serve:
 	python3 -m http.server -d docs

theories/Ctx/Abstract.v

@@ -18,58 +18,66 @@ Nicolas Pouillard.
 Theory
 ------
 
-Categorically, it very simple. Contexts are represented by a set `C`, a distinguished
-element `∅` and a binary operation `- +▶ -`. Additionally it has a map representing
-variable `𝓋 : C → 𝒜` where `𝒜` is a sufficiently well-behaved category, typically a
+Categorically, it very simple. Contexts are represented by a set ``C``, a distinguished
+element ``∅`` and a binary operation ``- +▶ -``. Additionally it has a map representing
+variable ``𝐯 : C → 𝐀`` where ``𝐀`` is a sufficiently well-behaved category, typically a
 presheaf category. We then ask that
 
-- `𝓋 ∅ ≈ ⊥`, where `⊥` is the initial object in `𝒜` and
-- `𝓋 (Γ +▶ Δ) ≈ 𝓋 Γ + 𝓋 Δ` where `+` is the coproduct in `𝒜`.
+- ``𝐯 ∅ ≈ ⊥``, where ``⊥`` is the initial object in ``𝐀`` and
+- ``𝐯 (Γ +▶ Δ) ≈ 𝐯 Γ + 𝐯 Δ`` where `+` is the coproduct in ``𝐀``.
 
-Our category of contexts is basically the image of `𝓋`, which has the structure of a
-commutative monoid. Then, given a family `𝒳 : C → 𝒜`, it is easy to define
-assignments as::
+Our category of contexts is basically the image of ``𝐯``, which has the structure of a
+commutative monoid. Then, given a family ``X : C → 𝐀``, it is easy to define
+assignments as:
 
-  Γ =[𝒳]> Δ ≔ 𝒜[ 𝓋 Γ , 𝒳 Δ ]
+.. code::
 
-And renamings as::
+  Γ =[X]> Δ ≔ 𝐀[ 𝐯 Γ , X Δ ]
 
-  Γ ⊆ Δ ≔ Γ =[ 𝓋 ]> Δ
-        ≔ 𝒜[ 𝓋 Γ , 𝓋 Δ ]
+And renamings as:
 
-Assuming `𝒜` is (co-)powered over `Set`, the substitution tensor product and substitution
-internal hom in `C → 𝒜` are given by:: 
+.. code::
 
-  ( 𝒳 ⊗ 𝒴 ) Γ ≔ ∫^Δ  𝒳 Δ × (Δ =[ 𝒴 ]> Γ)
-  ⟦ 𝒳 , 𝒴 ⟧ Γ ≔ ∫_Δ  (Γ =[ 𝒳 ]> Δ) → 𝒴 Δ
+  Γ ⊆ Δ ≔ Γ =[ 𝐯 ]> Δ
+        ≔ 𝐀[ 𝐯 Γ , 𝐯 Δ ]
 
-More generally, given a category `ℬ` (co-)powered over `Set` we can define the the
+Assuming ``𝐀`` is (co-)powered over ``Set``, the substitution tensor product and substitution
+internal hom in ``C → 𝐀`` are given by:
+
+.. code::
+
+  ( X ⊗ Y ) Γ ≔ ∫^Δ  X Δ × (Δ =[ Y ]> Γ)
+  ⟦ X , Y ⟧ Γ ≔ ∫_Δ  (Γ =[ X ]> Δ) → Y Δ
+
+More generally, given a category ``𝐁`` (co-)powered over ``Set`` we can define the the
 following functors, generalizing the substitution tensor and hom to heretogeneous
-settings::
+settings:
+
+.. code::
 
-  ( - ⊗ - ) : (C → ℬ) → (C → 𝒜) → (C → ℬ)
-  ( 𝒳 ⊗ 𝒴 ) Γ ≔ ∫^Δ  𝒳 Δ × (Δ =[ 𝒴 ]> Γ)
+  ( - ⊗ - ) : (C → 𝐁) → (C → 𝐀) → (C → 𝐁)
+  ( X ⊗ Y ) Γ ≔ ∫^Δ  X Δ × (Δ =[ Y ]> Γ)
 
-  ⟦ - , - ⟧ : (C → 𝒜) → (C → ℬ) → (C → ℬ)
-  ⟦ 𝒳 , 𝒴 ⟧ Γ ≔ ∫_Δ  (Γ =[ 𝒳 ]> Δ) → 𝒴 Δ
+  ⟦ - , - ⟧ : (C → 𝐀) → (C → 𝐁) → (C → 𝐁)
+  ⟦ X , Y ⟧ Γ ≔ ∫_Δ  (Γ =[ X ]> Δ) → Y Δ
 
 Concretely
 ----------  
 
-We here apply the above theory to the case where `𝓐` is the family category `T → Set` for
-some set `T`. Taking `T` to the set of types of some object language, families `C → 𝒜`, ie
-`C → T → Set`, model nicely well-scoped and well-typed families. To capture non-typed
-syntactic categories, indexed only by a scope, we develop the special case where `ℬ` is
-just `Set`.
+We here apply the above theory to the case where ``𝐀`` is the family category ``T → Set``
+for some set ``T``. Taking ``T`` to the set of types of some object language, families
+``C → 𝐀``, ie ``C → T → Set``, model nicely well-scoped and well-typed families. To
+capture non-typed syntactic categories, indexed only by a scope, we develop the special
+case where ``𝐁`` is just ``Set``.
 
 We then instanciate this abstract structure with the usual lists and DeBruijn indices,
-but also with two useful instances: the direct sum, where the notion of variables `𝓋` is
-the pointwise coproduct and the subset, where the notion of variables is preserved.
+but also with two useful instances: the direct sum, where the notion of variables ``𝐯``
+is the pointwise coproduct and the subset, where the notion of variables is preserved.
 
 In further work we wish to tacle this in more generality, notable treating the case for
-the idiomatic presentation of well-scoped untyped syntax where `𝒜` is `Set`, `C` is `ℕ`
-and `𝓋` is `Fin`. Currently, we do treat untyped syntax, but using the non-idiomatic
-"unityped" presentation.
+the idiomatic presentation of well-scoped untyped syntax where ``𝐀`` is ``Set``, ``C``
+is ``ℕ`` and ``𝐯`` is ``Fin``. Currently, we do treat untyped syntax, but using the
+non-idiomatic "unityped" presentation.
 
 .. coq:: none
 |*)

theories/Ctx/Assignment.v

@@ -1,3 +1,13 @@
+(*|
+Assignments
+===========
+
+In this file we define assignments for a given abstract context structure. We also define
+several combinators based on them: the internal substitution hom, filled operations,
+copairing, etc.
+
+.. coq:: none
+|*)
 From OGS Require Import Prelude.
 From OGS.Utils Require Import Psh Rel.
 From OGS.Ctx Require Import Abstract Family.
@@ -19,18 +29,23 @@ Section with_param.
   Context {T C : Type} {CC : context T C} {CL : context_laws T C}.
 
 (*|
-Assignment
-------------
+Definition of assignments
+-------------------------
 
 We distinguish assignments, mapping variables in a context to terms, from
 substitutions, applying an assignment to a term. Assignments are intrinsically
 typed, mapping variables of a context Γ to open terms with variables in Δ.
+
+.. coq::
+   :name: asgn
 |*)
   Definition assignment (F : Fam₁ T C) (Γ Δ : C) := forall x, Γ ∋ x -> F Δ x.
 
   Notation "Γ =[ F ]> Δ" := (assignment F Γ%ctx Δ%ctx).
+(*|
+.. coq:: none
+|*)
   Bind Scope asgn_scope with assignment.
-
 (*|
 Pointwise equality of assignments.
 |*)
@@ -44,24 +59,28 @@ Pointwise equality of assignments.
     - intros u h ? ? i; symmetry; now apply (H _ i).
     - intros u v w h1 h2 ? i; transitivity (v _ i); [ now apply h1 | now apply h2 ].
   Qed.
-
 (*|
 Internal hom functors. The monoidal product for substitution is a bit cumbersome as
 it is expressed as a coend, that is, a quotient. Following the formalization by
 Dima Szamozvancev, we instead prefer to express everything in terms of its adjoint,
 the internal hom.
 
-For example the monoidal multiplication map will not be typed `X ⊗ X ⇒ X` but
-`X ⇒ ⟦ X , X ⟧`.
+For example the monoidal multiplication map will not be typed ``X ⊗ X ⇒ X`` but
+``X ⇒ ⟦ X , X ⟧``.
 
 It is an end, that is, a subset, which are far more easy to work with as they can
 simply be encoded as a record pairing an element and a proof. The proof part is not
 written here but encoded later on.
 
 The real one is ⟦-,-⟧₁, but in fact we can define an analogue to this bifunctor
-for any functor category `ctx → C`, which we do here for Fam₀ and Fam₂ (unsorted and
+for any functor category ``ctx → C``, which we do here for Fam₀ and Fam₂ (unsorted and
 bisorted, scoped families). This will be helpful to define what it means to
 substitute other kinds of syntactic objects.
+
+See `Ctx/Abstract.v <Abstract.html>`_ for more details on the theory.
+
+.. coq::
+   :name: ihom
 |*)
   Definition internal_hom₀ : Fam₁ T C -> Fam₀ T C -> Fam₀ T C
     := fun F G Γ => forall Δ, Γ =[F]> Δ -> G Δ.
@@ -73,11 +92,12 @@ substitute other kinds of syntactic objects.
   Notation "⟦ F , G ⟧₀" := (internal_hom₀ F G).
   Notation "⟦ F , G ⟧₁" := (internal_hom₁ F G).
   Notation "⟦ F , G ⟧₂" := (internal_hom₂ F G).
-
+(*|
+.. coq:: none
+|*)
   #[global] Arguments internal_hom₀ _ _ _ /.
   #[global] Arguments internal_hom₁ _ _ _ _ /.
   #[global] Arguments internal_hom₂ _ _ _ _ _ /.
-
 (*|
 Experimental. The left action on maps of the internal hom bifunctor.
 |*)
@@ -90,53 +110,66 @@ Experimental. The left action on maps of the internal hom bifunctor.
   Definition hom_precomp₂ {F1 F2 : Fam₁ T C} {G} (m : F1 ⇒₁ F2)
     : ⟦ F2 , G ⟧₂ ⇒₂ ⟦ F1 , G ⟧₂
     := fun _ _ _ f _ a => f _ (fun _ i => m _ _ (a _ i)).
-
+(*|
+.. coq:: none
+|*)
   #[global] Arguments hom_precomp₀ _ _ _ _ _ _ /.
   #[global] Arguments hom_precomp₁ _ _ _ _ _ _ _ /.
   #[global] Arguments hom_precomp₂ _ _ _ _ _ _ _ _ /.
-
 (*|
 Constructing a sorted family of operations from O with arguments taken from the family F.
+
+.. coq::
+   :name: filledop
 |*)
   Record filled_op (O : Oper T C) (F : Fam₁ T C) (Γ : C) (t : T) :=
     OFill { fill_op : O t ; fill_args : o_dom fill_op =[F]> Γ }.
-
+  Notation "S # F" := (filled_op S F).
+(*|
+.. coq:: none
+|*)
   Derive NoConfusion NoConfusionHom for filled_op.
   #[global] Arguments OFill {O F Γ t} o a%asgn : rename.
   #[global] Arguments fill_op {O F Γ t} _.
   #[global] Arguments fill_args {O F Γ t} _ _ /.
-  Notation "S # F" := (filled_op S F).
-
 (*|
 We can forget the arguments and get back a bare operation.
 |*)
   Definition forget_args {O : Oper T C} {F} : (O # F) ⇒₁ ⦉ O ⦊
     := fun _ _ => fill_op.
-
 (*|
 The empty assignment.
+
+.. coq::
+   :name: asgnempty
 |*)
   Definition a_empty {F Γ} : ∅ =[F]> Γ
     := fun _ i => match c_view_emp i with end.
-
 (*|
 The copairing of assignments.
+
+.. coq::
+   :name: asgncat
 |*)
   Definition a_cat {F Γ1 Γ2 Δ} (u : Γ1 =[F]> Δ) (v : Γ2 =[F]> Δ) : (Γ1 +▶ Γ2) =[F]> Δ
     := fun t i => match c_view_cat i with
                | Vcat_l i => u _ i
                | Vcat_r j => v _ j
                end.
+(*|
+.. coq:: none
+|*)
   #[global] Arguments a_cat _ _ _ _ _ _ _ _ /.
-
 (*|
 A kind relaxed of pointwise mapping.
 |*)
   Definition a_map {F G : Fam₁ T C} {Γ Δ1 Δ2} (u : Γ =[F]> Δ1) (f : forall x, F Δ1 x -> G Δ2 x)
     : Γ =[G]> Δ2
     := fun _ i => f _ (u _ i) .
+(*|
+.. coq:: none
+|*)
   #[global] Arguments a_map _ _ _ _ _ _ _ _ /.
-
 (*|
 Copairing respects pointwise equality.
 |*)
@@ -147,7 +180,9 @@ Copairing respects pointwise equality.
     destruct (c_view_cat a0); [ now apply Hu | now apply Hv ].
   Qed.
 End with_param.
-
+(*|
+Registering all the notations...
+|*)
 #[global] Notation "Γ =[ F ]> Δ" := (assignment F Γ%ctx Δ%ctx).
 #[global] Bind Scope asgn_scope with assignment.
 

theories/Ctx/Covering.v

@@ -1,3 +1,16 @@
+(*|
+Covering for free contexts
+==========================
+
+In `Ctx/Ctx.v <Ctx.html>`_ we have instanciated the relevant part of the abstract interface
+for concrete contexts. Here we tackle the rest of the structure. Basically, we need to
+provide case-splitting for deciding if a variable ``i : (Γ +▶ Δ) ∋ x`` is in ``Γ`` or in
+``Δ``. We could do this directly but we prove a slight generalization, going through the
+definition of coverings, a ternary relationship on concrete contexts witnessing that a
+context is *covered* by the two others (respecting order).
+
+.. coq:: none
+|*)
 From OGS Require Import Prelude.
 From OGS.Utils Require Import Psh Rel.
 From OGS.Ctx Require Import All Ctx.
@@ -11,9 +24,11 @@ Reserved Notation "[ u , H , v ]" (at level 9).
 Section with_param.
   Context {X : Type} {F : Fam₁ X (ctx X)}.
 (*|
-Covering:
----------
-Predicate for splitting a context into a disjoint union
+A covering
+----------
+
+This inductive family provides proofs that some context ``zs`` is obtained by "zipping"
+together two other contexts ``xs`` and ``ys``.
 |*)
   Inductive cover : ctx X -> ctx X -> ctx X -> Type :=
   | CNil : ∅ₓ ⊎ ∅ₓ  ≡ ∅ₓ
@@ -25,7 +40,7 @@ Predicate for splitting a context into a disjoint union
 |*)
   Derive Signature NoConfusion NoConfusionHom for cover.
 (*|
-.. coq::
+Basic useful coverings.
 |*)
   Equations cover_nil_r xs : xs ⊎ ∅ₓ ≡ xs :=
     cover_nil_r ∅ₓ        := CNil ;
@@ -36,12 +51,16 @@ Predicate for splitting a context into a disjoint union
     cover_nil_l ∅ₓ        := CNil ;
     cover_nil_l (xs ▶ₓ _) := CRight (cover_nil_l xs) .
   #[global] Arguments cover_nil_l {xs}.
-
+(*|
+This is the crucial one: the concatenation is covered by its two components.
+|*)
   Equations cover_cat {xs} ys : xs ⊎ ys ≡ (xs +▶ ys) :=
     cover_cat ∅ₓ        := cover_nil_r ;
     cover_cat (ys ▶ₓ _) := CRight (cover_cat ys) .
   #[global] Arguments cover_cat {xs ys}.
-
+(*|
+A covering gives us two injective renamings, left embedding and right embedding.
+|*)
   Equations r_cover_l {xs ys zs} : xs ⊎ ys ≡ zs -> xs ⊆ zs :=
     r_cover_l (CLeft c)  _ top     := top ;
     r_cover_l (CLeft c)  _ (pop i) := pop (r_cover_l c _ i) ;
@@ -51,7 +70,9 @@ Predicate for splitting a context into a disjoint union
     r_cover_r (CLeft c)  _ i       := pop (r_cover_r c _ i) ;
     r_cover_r (CRight c) _ top     := top ;
     r_cover_r (CRight c) _ (pop i) := pop (r_cover_r c _ i) .
-
+(*|
+Injectivity.
+|*)
   Lemma r_cover_l_inj {xs ys zs} (p : xs ⊎ ys ≡ zs) [x] (i j : xs ∋ x)
     (H : r_cover_l p _ i = r_cover_l p _ j) : i = j .
   Proof.
@@ -74,7 +95,9 @@ Predicate for splitting a context into a disjoint union
       apply noConfusion_inv in H.
       f_equal; now apply IHp.
   Qed.
-
+(*|
+The two embeddings have disjoint images.
+|*)
   Lemma r_cover_disj {xs ys zs} (p : xs ⊎ ys ≡ zs) [a] (i : xs ∋ a) (j : ys ∋ a)
     (H : r_cover_l p _ i = r_cover_r p _ j) : T0.
   Proof.
@@ -89,14 +112,19 @@ Predicate for splitting a context into a disjoint union
       + apply noConfusion_inv in H; cbn in H.
         exact (IHp i v H).
   Qed.
-
+(*|
+Now we can start proving that the copairing of the two embeddings has non-empty fibers,
+ie, we can case split.
+|*)
   Variant cover_view {xs ys zs} (p : xs ⊎ ys ≡ zs) [z] : zs ∋ z -> Type :=
   | Vcov_l  (i : xs ∋ z) : cover_view p (r_cover_l p _ i)
   | Vcov_r (j : ys ∋ z) : cover_view p (r_cover_r p _ j)
   .
   #[global] Arguments Vcov_l {xs ys zs p z}.
   #[global] Arguments Vcov_r {xs ys zs p z}.
-
+(*|
+Indeed!
+|*)
   Lemma view_cover {xs ys zs} (p : xs ⊎ ys ≡ zs) [z] (i : zs ∋ z) : cover_view p i.
   Proof.
     revert xs ys p; induction zs; intros xs ys p; dependent elimination i.
@@ -106,7 +134,7 @@ Predicate for splitting a context into a disjoint union
       * destruct (IHzs v _ _ c0); [ exact (Vcov_l i) | exact (Vcov_r (pop j)) ].
   Qed.
 (*|
-Finishing the instanciation of the abstract interface for `ctx X`.
+Finishing the instanciation of the abstract interface for ``ctx X``.
 |*)
   #[global] Instance free_context_cat_wkn : context_cat_wkn X (ctx X) :=
     {| r_cat_l _ _ := r_cover_l cover_cat ;