Coq: Model subtype check on decoding, IDL-Soundness, Transitive Coher…

…ence (#171)

A revamp of the Coq development:

 * It models the subtype-checking on decoding (#168). Looks good
 * It connects MiniCandid to the IDL-Soundness theorem. The main work here is the subtyping-compositonality lemma.
   ```
   If t1 <: t2 and s1 in t1 <: s2 in t2 then s1 <: s2.
   ```
   With this in place, instantiating the “canonical subtyping” proof there works nicely.
 * It proves transitive coherence with regard to the relaxed relation as per #173
 * Mild coqdoc’ifiacation. I’d like to eventually render these to HTML and host them somewhere.
   It’s very annoying that Github Action artifacts, even if they are HTML, are not directly accessible with the browser.
   Maybe setup Github pages?
   
It is still a Mini-Candid with a limited set of types, but I think it has all the interesting ones to cover the corner cases. Even adding vectors adds a lot of technical noise with little additional insight (see #154.)

coq/IDLSoundness.v

@@ -1,13 +1,16 @@
-(* This formalizes
+(**
+
+This theory formalizes
    https://github.com/dfinity/candid/blob/master/spec/IDL-Soundness.md
- *)
+
+*)
 
 Require Import Coq.Lists.List.
 Import ListNotations.
 
 Require Import Coq.Sets.Ensembles.
 (* Odd that this is needed, see
-   https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd
+https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd
 *)
 Arguments In {U}.
 Arguments Add {U}.
@@ -23,16 +26,21 @@ Set Bullet Behavior "Strict Subproofs".
 
 Section IDL.
 
-  (* An abstract theory of IDLs is parametrized as follows: *)
-
-  (* Argument or result types *)
+  (**
+  
+  * The Abstract IDL theory
+  
+  An abstract theory of IDLs is parametrized as follows:
+  *)
+
+  (** The type of (argument or result types) *)
   Variable T : Set.
 
-  (* A service type is a pair of types *)
+  (** A service type is a pair of types (argument and results) *)
   Definition S : Set := (T * T).
   Notation "t1 --> t2" := (t1, t2) (at level 80, no associativity).
 
-  (* The prediates of the theory *)
+  (** The theory has to define the following predicates *)
   Variable decodesAt : T -> T -> Prop.
   Notation "t1 <: t2" := (decodesAt t1 t2) (at level 70, no associativity).
 
@@ -46,10 +54,10 @@ Section IDL.
   Variable hostSubtypeOf : S -> S -> Prop.
   Notation "s1 <<: s2" := (hostSubtypeOf s1 s2) (at level 70, no associativity).
 
-  (* Service Identifiers *)
+  (** This is generic in the set of service identifiers *)
   Variable I : Set.
 
-  (* Judgements *)
+  (** ** Judgements *)
   Inductive Assertion : Set :=
     | HasType : I -> S -> Assertion
     | HasRef : I -> I -> S -> Assertion.
@@ -108,17 +116,19 @@ Section IDL.
 
   Definition StateSound (st : State) : Prop :=
     forall A t1 t2 B, CanSend st A t1 t2 B ->  t1 <: t2.
+
+  (** The final soundness proposition *)
 
   Definition IDLSound : Prop :=
     forall s, clos_refl_trans _ step Empty_set s -> StateSound s.
 
-  (* Now we continue with the soundness proof for canonical subtyping.
+  (** * Canonical subtyping *)
 
-     We do so by just adding more hypotheses to this Section.
-     This is fine for now; when we actually want to instantiate this proof
-     with an actual IDL, we may want to revisit this, and maybe
-     modularize this development.
-   *)
+  (**
+  We continue with the soundness proof for canonical subtyping.
+
+  We do so by just adding more hypotheses to this Section.
+  *)
 
   Hypothesis decodesAt_refl: reflexive _ decodesAt.
   Hypothesis decodesAt_trans: transitive _ decodesAt.
@@ -137,7 +147,7 @@ Section IDL.
   Hypothesis host_subtyping_sound:
    forall s1 s2, s1 <<: s2 -> s1 <:: s2.
 
-  (*
+  (**
   Now the actual proofs. When I was writing these, my Coq has become
   pretty rusty, so these are rather manual proofs, with little
   automation. The style is heavily influenced by the explicit Isar-style