From 08c220e468a875b6394cfb2e54b60aa6cfa11b6d Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 30 Nov 2020 17:46:55 +0100
Subject: [PATCH 01/25] Empty Coq setup

using the shiny new support in dune to build Coq projects:
https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory
---
 coq/.gitignore        |   3 +
 coq/IDLSoundness.v    |   0
 coq/default.nix       |   1 +
 coq/dune              |   5 ++
 coq/dune-project      |   2 +
 coq/nix/default.nix   |  51 +++++++++++++
 coq/nix/gitSource.nix | 110 ++++++++++++++++++++++++++
 coq/nix/sources.json  |  26 +++++++
 coq/nix/sources.nix   | 174 ++++++++++++++++++++++++++++++++++++++++++
 coq/shell.nix         |   1 +
 10 files changed, 373 insertions(+)
 create mode 100644 coq/.gitignore
 create mode 100644 coq/IDLSoundness.v
 create mode 100644 coq/default.nix
 create mode 100644 coq/dune
 create mode 100644 coq/dune-project
 create mode 100644 coq/nix/default.nix
 create mode 100644 coq/nix/gitSource.nix
 create mode 100644 coq/nix/sources.json
 create mode 100644 coq/nix/sources.nix
 create mode 100644 coq/shell.nix

diff --git a/coq/.gitignore b/coq/.gitignore
new file mode 100644
index 00000000..5f99793c
--- /dev/null
+++ b/coq/.gitignore
@@ -0,0 +1,3 @@
+result*
+_build
+.envrc
diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
new file mode 100644
index 00000000..e69de29b
diff --git a/coq/default.nix b/coq/default.nix
new file mode 100644
index 00000000..5204735f
--- /dev/null
+++ b/coq/default.nix
@@ -0,0 +1 @@
+(import ./nix {}).local
diff --git a/coq/dune b/coq/dune
new file mode 100644
index 00000000..cd6bb06c
--- /dev/null
+++ b/coq/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name "candid")
+ (synopsis "Coq for candid")
+ (modules "IDLSoundness")
+)
diff --git a/coq/dune-project b/coq/dune-project
new file mode 100644
index 00000000..343a574f
--- /dev/null
+++ b/coq/dune-project
@@ -0,0 +1,2 @@
+(lang dune 2.7)
+(using coq 0.1)
diff --git a/coq/nix/default.nix b/coq/nix/default.nix
new file mode 100644
index 00000000..96ebc25f
--- /dev/null
+++ b/coq/nix/default.nix
@@ -0,0 +1,51 @@
+{}:
+let
+  sources =  import ./sources.nix;
+
+  subpath = import ./gitSource.nix;
+
+  overlays = [
+    (pkgs: super: { local = {
+      # Fetch niv from nix/sources.json, newer than nixpkgs
+      niv = (import sources.niv {}).niv;
+
+      # the main product: building the theories
+      theories = pkgs.stdenv.mkDerivation {
+        name = "candid-coq";
+        src = subpath ./..;
+        buildInputs = [
+          pkgs.dune_2
+          pkgs.coq
+          pkgs.ocaml
+        ];
+        buildPhase = ''
+          dune build --display=short
+        '';
+        installPhase = ''
+          touch $out
+        '';
+      };
+
+      # a convenient shell setup
+      shell = pkgs.mkShell {
+        inputsFrom = [
+          pkgs.local.theories
+        ];
+        propagatedBuildInputs = [
+          pkgs.niv
+        ];
+
+        # allow building this as a derivation, so that CI can biuld and cache
+        # the dependencies of shell
+        phases = ["installPhase" "fixupPhase"];
+        installPhase = ''
+          mkdir $out
+        '';
+        preferLocalBuild = true;
+        allowSubstitutes = true;
+      };
+    };})
+  ];
+
+in import sources.nixpkgs { inherit overlays; }
+
diff --git a/coq/nix/gitSource.nix b/coq/nix/gitSource.nix
new file mode 100644
index 00000000..5e8323ba
--- /dev/null
+++ b/coq/nix/gitSource.nix
@@ -0,0 +1,110 @@
+# The function call
+#
+#   gitSource ./toplevel subpath
+#
+# creates a Nix store path of ./toplevel/subpath that includes only those files
+# tracked by git. More precisely: mentioned in the git index (i.e. git add is enough
+# to get them to be included, you do not have to commit).
+#
+# This is a whitelist-based alternative to manually listing files or using
+# nix-gitignore.
+
+# Internally, it works by calling git ls-files at evaluation time. To
+# avoid copying all of `.git` to the git store, it only copies the least amount
+# of files necessary for `git ls-files` to work; this is a bit fragile, but
+# very fast.
+
+with builtins;
+
+# We read the git index once, before getting the subdir parameter, so that it
+# is shared among multiple invocations of gitSource:
+
+let
+  filter_from_list = root: files:
+    let
+      all_paren_dirs = p:
+        if p == "." || p == "/"
+        then []
+        else [ p ] ++ all_paren_dirs (dirOf p);
+
+      whitelist_set = listToAttrs (
+        concatMap (p:
+          let full_path = toString (root + "/${p}"); in
+          map (p': { name = p'; value = true; }) (all_paren_dirs full_path)
+        ) files
+      );
+    in
+    p: t: hasAttr (toString p) whitelist_set;
+
+  has_prefix = prefix: s:
+    prefix == builtins.substring 0 (builtins.stringLength prefix) s;
+  has_suffix = suffix: s:
+    let x1 = builtins.stringLength suffix - builtins.stringLength s; in
+    x1 >= 0 && suffix == builtins.substring x1 (builtins.stringLength s) s;
+  remove_prefix = prefix: s:
+    builtins.substring
+      (builtins.stringLength prefix)
+      (builtins.stringLength s - builtins.stringLength prefix)
+      s;
+
+  lines = s: filter (x : x != [] && x != "") (split "\n" s);
+
+# On hydra, checkouts are always clean, and we don't want to do IFD
+  isHydra = (builtins.tryEval <src>).success;
+  not_dot_git = p: t: !(has_suffix ".git" p);
+in
+
+# unfortunately this is not completely self-contained,
+# we needs pkgs this to get git and lib.cleanSourceWith
+let nixpkgs = import ./. {}; in
+
+if !isHydra && builtins.pathExists ../../.git
+then
+  let
+
+    git_dir =
+      if builtins.pathExists ../../.git/index
+      then ../../.git
+      else # likely a git worktree, so follow the indirection
+        let
+          git_content = lines (readFile ./../../.git);
+          first_line = head git_content;
+          prefix = "gitdir: ";
+          ok = length git_content == 1 && has_prefix prefix first_line;
+        in
+          if ok
+          then /. + remove_prefix prefix first_line
+          else abort "gitSource.nix: Cannot parse ${toString ./../../.git}";
+
+    whitelist_file =
+      nixpkgs.runCommand "git-ls-files" {envVariable = true;} ''
+        cp ${git_dir + "/index"} index
+        echo "ref: refs/heads/master" > HEAD
+        mkdir objects refs
+        ${nixpkgs.git}/bin/git --git-dir . ls-files > $out
+      '';
+
+    whitelist = lines (readFile (whitelist_file.out));
+
+    filter = filter_from_list ../../. whitelist;
+  in
+    subdir: nixpkgs.lib.cleanSourceWith {
+      name = baseNameOf (toString subdir);
+      src = if isString subdir then (../../. + "/${subdir}") else subdir;
+      filter = filter;
+    }
+
+else
+  let warn_unless = b: m: x: if b then x else trace m x; in
+  # No .git directory found, we should warn the user.
+  # But when this repository is imported using something like
+  # `builtins.fetchGit` then the source is extracted to /nix/store without a
+  # .git directory, but in this case we know that it is clean, so do not warn
+  warn_unless
+    (isHydra || has_prefix "/nix/store" (toString ../.))
+    "gitSource.nix: ${toString ../../.} does not seem to be a git repository,\nassuming it is a clean checkout."
+    (subdir: nixpkgs.lib.cleanSourceWith {
+      name = baseNameOf (toString subdir);
+      src = if isString subdir then (../../. + "/${subdir}") else subdir;
+      filter = not_dot_git;
+    })
diff --git a/coq/nix/sources.json b/coq/nix/sources.json
new file mode 100644
index 00000000..f5e79a22
--- /dev/null
+++ b/coq/nix/sources.json
@@ -0,0 +1,26 @@
+{
+    "niv": {
+        "branch": "master",
+        "description": "Easy dependency management for Nix projects",
+        "homepage": "https://github.com/nmattia/niv",
+        "owner": "nmattia",
+        "repo": "niv",
+        "rev": "ba57d5a29b4e0f2085917010380ef3ddc3cf380f",
+        "sha256": "1kpsvc53x821cmjg1khvp1nz7906gczq8mp83664cr15h94sh8i4",
+        "type": "tarball",
+        "url": "https://github.com/nmattia/niv/archive/ba57d5a29b4e0f2085917010380ef3ddc3cf380f.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+    },
+    "nixpkgs": {
+        "branch": "nixos-20.09",
+        "description": "Nix Packages collection",
+        "homepage": "",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "ae47c79479a086e96e2977c61e538881913c0c08",
+        "sha256": "1yaa02zdbmd4j5lrhbynk5xdv6dkfhajlbsf5fkhx73hj9knmfgn",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/ae47c79479a086e96e2977c61e538881913c0c08.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+    }
+}
diff --git a/coq/nix/sources.nix b/coq/nix/sources.nix
new file mode 100644
index 00000000..1938409d
--- /dev/null
+++ b/coq/nix/sources.nix
@@ -0,0 +1,174 @@
+# This file has been generated by Niv.
+
+let
+
+  #
+  # The fetchers. fetch_<type> fetches specs of type <type>.
+  #
+
+  fetch_file = pkgs: name: spec:
+    let
+      name' = sanitizeName name + "-src";
+    in
+      if spec.builtin or true then
+        builtins_fetchurl { inherit (spec) url sha256; name = name'; }
+      else
+        pkgs.fetchurl { inherit (spec) url sha256; name = name'; };
+
+  fetch_tarball = pkgs: name: spec:
+    let
+      name' = sanitizeName name + "-src";
+    in
+      if spec.builtin or true then
+        builtins_fetchTarball { name = name'; inherit (spec) url sha256; }
+      else
+        pkgs.fetchzip { name = name'; inherit (spec) url sha256; };
+
+  fetch_git = name: spec:
+    let
+      ref =
+        if spec ? ref then spec.ref else
+          if spec ? branch then "refs/heads/${spec.branch}" else
+            if spec ? tag then "refs/tags/${spec.tag}" else
+              abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!";
+    in
+      builtins.fetchGit { url = spec.repo; inherit (spec) rev; inherit ref; };
+
+  fetch_local = spec: spec.path;
+
+  fetch_builtin-tarball = name: throw
+    ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`.
+        $ niv modify ${name} -a type=tarball -a builtin=true'';
+
+  fetch_builtin-url = name: throw
+    ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`.
+        $ niv modify ${name} -a type=file -a builtin=true'';
+
+  #
+  # Various helpers
+  #
+
+  # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695
+  sanitizeName = name:
+    (
+      concatMapStrings (s: if builtins.isList s then "-" else s)
+        (
+          builtins.split "[^[:alnum:]+._?=-]+"
+            ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name)
+        )
+    );
+
+  # The set of packages used when specs are fetched using non-builtins.
+  mkPkgs = sources: system:
+    let
+      sourcesNixpkgs =
+        import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; };
+      hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath;
+      hasThisAsNixpkgsPath = <nixpkgs> == ./.;
+    in
+      if builtins.hasAttr "nixpkgs" sources
+      then sourcesNixpkgs
+      else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then
+        import <nixpkgs> {}
+      else
+        abort
+          ''
+            Please specify either <nixpkgs> (through -I or NIX_PATH=nixpkgs=...) or
+            add a package called "nixpkgs" to your sources.json.
+          '';
+
+  # The actual fetching function.
+  fetch = pkgs: name: spec:
+
+    if ! builtins.hasAttr "type" spec then
+      abort "ERROR: niv spec ${name} does not have a 'type' attribute"
+    else if spec.type == "file" then fetch_file pkgs name spec
+    else if spec.type == "tarball" then fetch_tarball pkgs name spec
+    else if spec.type == "git" then fetch_git name spec
+    else if spec.type == "local" then fetch_local spec
+    else if spec.type == "builtin-tarball" then fetch_builtin-tarball name
+    else if spec.type == "builtin-url" then fetch_builtin-url name
+    else
+      abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}";
+
+  # If the environment variable NIV_OVERRIDE_${name} is set, then use
+  # the path directly as opposed to the fetched source.
+  replace = name: drv:
+    let
+      saneName = stringAsChars (c: if isNull (builtins.match "[a-zA-Z0-9]" c) then "_" else c) name;
+      ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}";
+    in
+      if ersatz == "" then drv else
+        # this turns the string into an actual Nix path (for both absolute and
+        # relative paths)
+        if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}";
+
+  # Ports of functions for older nix versions
+
+  # a Nix version of mapAttrs if the built-in doesn't exist
+  mapAttrs = builtins.mapAttrs or (
+    f: set: with builtins;
+    listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set))
+  );
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295
+  range = first: last: if first > last then [] else builtins.genList (n: first + n) (last - first + 1);
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257
+  stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1));
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269
+  stringAsChars = f: s: concatStrings (map f (stringToCharacters s));
+  concatMapStrings = f: list: concatStrings (map f list);
+  concatStrings = builtins.concatStringsSep "";
+
+  # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331
+  optionalAttrs = cond: as: if cond then as else {};
+
+  # fetchTarball version that is compatible between all the versions of Nix
+  builtins_fetchTarball = { url, name ? null, sha256 }@attrs:
+    let
+      inherit (builtins) lessThan nixVersion fetchTarball;
+    in
+      if lessThan nixVersion "1.12" then
+        fetchTarball ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; }))
+      else
+        fetchTarball attrs;
+
+  # fetchurl version that is compatible between all the versions of Nix
+  builtins_fetchurl = { url, name ? null, sha256 }@attrs:
+    let
+      inherit (builtins) lessThan nixVersion fetchurl;
+    in
+      if lessThan nixVersion "1.12" then
+        fetchurl ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; }))
+      else
+        fetchurl attrs;
+
+  # Create the final "sources" from the config
+  mkSources = config:
+    mapAttrs (
+      name: spec:
+        if builtins.hasAttr "outPath" spec
+        then abort
+          "The values in sources.json should not have an 'outPath' attribute"
+        else
+          spec // { outPath = replace name (fetch config.pkgs name spec); }
+    ) config.sources;
+
+  # The "config" used by the fetchers
+  mkConfig =
+    { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null
+    , sources ? if isNull sourcesFile then {} else builtins.fromJSON (builtins.readFile sourcesFile)
+    , system ? builtins.currentSystem
+    , pkgs ? mkPkgs sources system
+    }: rec {
+      # The sources, i.e. the attribute set of spec name to spec
+      inherit sources;
+
+      # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers
+      inherit pkgs;
+    };
+
+in
+mkSources (mkConfig {}) // { __functor = _: settings: mkSources (mkConfig settings); }
diff --git a/coq/shell.nix b/coq/shell.nix
new file mode 100644
index 00000000..b362a6aa
--- /dev/null
+++ b/coq/shell.nix
@@ -0,0 +1 @@
+(import ./nix {}).local.shell

From fcaeaa1cb69b356414b2f233f14c012a85bbd21c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 30 Nov 2020 19:03:43 +0100
Subject: [PATCH 02/25] Formalize IDL-Soundness

without the proof for canonical subtyping yet.
---
 coq/IDLSoundness.v  | 102 ++++++++++++++++++++++++++++++++++++++++++++
 coq/nix/default.nix |   3 ++
 2 files changed, 105 insertions(+)

diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index e69de29b..9cc67b10 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -0,0 +1,102 @@
+(* This tries to formalize 
+   https://github.com/dfinity/candid/blob/master/spec/IDL-Soundness.md
+ *)
+
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+(* Odd that this is needed, see
+   https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd
+*)
+Require Import Coq.Sets.Ensembles.
+Arguments In {U}.
+Arguments Add {U}.
+Arguments Empty_set {U}.
+
+Require Import Coq.Relations.Relation_Operators.
+
+Set Bullet Behavior "Strict Subproofs".
+ 
+Section IDL.
+
+  (* An abstract theory of IDLs is parametrized as follows: *)
+  
+  (* Argument or result types *)
+  Variable T : Set.
+  
+  (* A service type is a pair of types *)
+  Definition S : Set := (T * T).
+  Notation "t1 --> t2" := (t1, t2) (at level 80, no associativity).
+  
+  (* The prediates of the theory *)
+  Variable decodesAt : T -> T -> Prop.
+  Notation "t1 <: t2" := (decodesAt t1 t2) (at level 70, no associativity).
+  
+  Variable passesThrough : S -> T -> S -> T -> Prop.
+  Notation "s1 ∈ t1 <: s2 ∈ t2" := (passesThrough s1 t1 s2 t2)
+    (t1 at level 50, s2 at level 50, at level 70, no associativity).
+  
+  Variable evolves : S -> S -> Prop.
+  Notation "s1 ~> s2" := (evolves s1 s2) (at level 70, no associativity).
+  
+  Variable hostSubtyping : S -> S -> Prop.
+  Notation "s1 <<: s2" := (hostSubtyping s1 s2) (at level 70, no associativity).
+
+  (* Service Identifiers *)
+  Variable I : Set.
+
+  (* Judgements *)  
+  Inductive Assertion : Set :=
+    | HasType : I -> S -> Assertion
+    | HasRef : I -> I -> S -> Assertion.
+
+  Definition State := Ensemble Assertion.
+  
+  Definition FreshIn (i : I) (st : State) : Prop :=
+    (forall s, ~ In st (HasType i s)) /\
+    (forall i' s, ~ In st (HasRef i i' s)) /\
+    (forall i' s, ~ In st (HasRef i' i s)).
+  
+  Inductive CanSend : State -> I -> T -> T -> I -> Prop :=
+    | CanCall: forall st A B t1 t1' t2 t2',
+      In st (HasRef A B (t1 --> t1')) ->
+      In st (HasType B (t2 --> t2')) ->
+      CanSend st A t1 t2 B
+    | CanReply: forall st A B t1 t1' t2 t2',
+      In st (HasRef B A (t1 --> t1')) ->
+      In st (HasType A (t2 --> t2')) ->
+      CanSend st A t2' t1' B.
+      
+  Inductive step : State -> State -> Prop :=
+    | NewService :
+      forall (i : I) (s : S) st,
+      FreshIn i st ->
+      step st (Add st (HasType i s))
+    | EvolveService :
+      forall (i : I) (s1 s2 : S) st,
+      ~ In st (HasType i s1) ->
+      s1 ~> s2 ->
+      step (Add st (HasType i s1)) (Add st (HasType i s2))
+    | LearnService :
+      forall (i1 i2 : I) (s: S) st,
+      In st (HasType i1 s) ->
+      step st (Add st (HasRef i2 i1 s))
+    | TransmitService :
+      forall (A B C : I) (s1 s2 : S) (t1 t2 : T) st,
+      In st (HasRef A C s1) ->
+      CanSend st A t1 t2 B ->
+      (s1 ∈ t1 <: s2 ∈ t2) ->
+      step st (Add st (HasRef B C s2))
+    | HostSubtyping :
+      forall (A B : I) (s1 s2 : S) st,
+      s1 <<: s2 ->
+      step (Add st (HasRef A B s1)) (Add st (HasRef A B s2))
+    .
+
+  Definition StateSound (st : State) : Prop :=
+    forall A t1 t2 B, CanSend st A t1 t2 B ->  t1 <: t2.
+
+  Definition IDLSound : Prop :=
+    forall s, clos_refl_trans _ step Empty_set s -> StateSound s.
+
+End IDL.
\ No newline at end of file
diff --git a/coq/nix/default.nix b/coq/nix/default.nix
index 96ebc25f..46aac3f1 100644
--- a/coq/nix/default.nix
+++ b/coq/nix/default.nix
@@ -35,6 +35,9 @@ let
           pkgs.niv
         ];
 
+        # This helps with using GUI programs like coqide
+        LOCALE_ARCHIVE = pkgs.stdenv.lib.optionalString pkgs.stdenv.isLinux "${pkgs.glibcLocales}/lib/locale/locale-archive";
+
         # allow building this as a derivation, so that CI can biuld and cache
         # the dependencies of shell
         phases = ["installPhase" "fixupPhase"];

From f2a18681389334402572c296d074759426579de0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 30 Nov 2020 19:10:53 +0100
Subject: [PATCH 03/25] Try to add CI

---
 .github/workflows/coq.yml | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 .github/workflows/coq.yml

diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
new file mode 100644
index 00000000..3181f44a
--- /dev/null
+++ b/.github/workflows/coq.yml
@@ -0,0 +1,19 @@
+name: Coq
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: cachix/install-nix-action@v12
+      #- run: nix-build s coq
+      # The above would also build the shell, includling niv.
+      # This would be useful behaviour if our CI seeds some cache.
+      # Until then this would just be wasteful, so lets only
+      # build the Coq files:
+      - run: nix-build -A theories coq

From 29e29d516c2fbe47f25cc9de98ad9ab1ae0d257c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 1 Dec 2020 16:24:23 +0100
Subject: [PATCH 04/25] State assumptions of soundness proof

---
 coq/IDLSoundness.v | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index 9cc67b10..cb91f269 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -14,6 +14,7 @@ Arguments Add {U}.
 Arguments Empty_set {U}.
 
 Require Import Coq.Relations.Relation_Operators.
+Require Import Coq.Relations.Relation_Definitions.
 
 Set Bullet Behavior "Strict Subproofs".
  
@@ -98,5 +99,34 @@ Section IDL.
 
   Definition IDLSound : Prop :=
     forall s, clos_refl_trans _ step Empty_set s -> StateSound s.
+    
+   (* Now we continue with the soundness proof for canonical subtyping.
+      TODO: Modularize this development, instead of continuing in the same Section *)
+     
+    Hypothesis decodesAt_refl: reflexive _ decodesAt.
+    Hypothesis decodesAt_trans: transitive _ decodesAt.
+
+    Variable service_subtyping : S -> S -> Prop.
+    Notation "s1 <:: s2" := (service_subtyping s1 s2) (at level 70, no associativity).
+    Hypothesis service_subtype_sound:
+     forall t1 t1' t2 t2',
+       (t1 --> t1') <:: (t2 --> t2') ->
+       t1' <: t2' /\ t2 <: t1.
+
+    Hypothesis evolves_correctly:
+     forall s1 s2, s2 <:: s1 -> s1 ~> s2.
+    Hypothesis compositional:
+      forall t1 t2 s1 s2,
+      t1 <: t2 -> s1 ∈ t1 <: s2 ∈ t2 -> s1 <:: s2.
+    Hypothesis host_subtyping_sound:
+     forall s1 s2, s2 <<: s1 -> s1 <:: s2.
+    
+    Definition invariant (st : State) :=
+       forall A B s1 s2,
+       In st (HasType A s1) -> In st (HasRef B A s2) -> s1 <:: s2 .
+    
+    Lemma invariant_StateSound:
+      forall st, invariant st -> StateSound st.
+    Admitted.
 
 End IDL.
\ No newline at end of file

From e963b0bf2112acb0591e214d4d4853d373d1456a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 1 Dec 2020 17:56:46 +0100
Subject: [PATCH 05/25] Outline some of the proof

---
 coq/IDLSoundness.v | 78 +++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 77 insertions(+), 1 deletion(-)

diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index cb91f269..e8f2edf1 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -125,8 +125,84 @@ Section IDL.
        forall A B s1 s2,
        In st (HasType A s1) -> In st (HasRef B A s2) -> s1 <:: s2 .
     
-    Lemma invariant_StateSound:
+    Lemma invariant_implies_StateSound:
       forall st, invariant st -> StateSound st.
+    Proof.
+      intros st Hinvariant.
+      intros A t1 t2 B HCanSend.
+      destruct HCanSend.
+      * pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
+        apply service_subtype_sound in H1.
+        apply H1.
+      * pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
+        apply service_subtype_sound in H1.
+        apply H1.
+    Qed.
+
+    Lemma invariant_Add_HasType:
+      forall st A s1,
+      invariant st ->
+      (forall B s2, In st (HasRef B A s2) -> s1 <:: s2) ->
+      invariant (Add st (HasType A s1)).
+    Proof.
+       intros st A s1 Hinv HA.
+       intros A' B s1' s2 HHasType HHasRef.
+       inversion HHasType; clear HHasType; inversion HHasRef; clear HHasRef; subst.
+       * eapply Hinv; eassumption.
+       * inversion H1.
+       * inversion H; subst; clear H.
+         eapply HA; eassumption.
+       * inversion H; subst; clear H.
+         inversion H1; subst; clear H1.
+    Qed.
+
+    Lemma invariant_Add_HasRef:
+      forall st A B s2,
+      invariant st ->
+      (forall s1, In st (HasType B s1) -> s1 <:: s2) ->
+      invariant (Add st (HasRef A B s2)).
+    Proof.
+       intros st A B s2 Hinv HA.
+       intros A' B' s1' s2' HHasRef HHasType.
+       inversion HHasType; clear HHasType; inversion HHasRef; clear HHasRef; subst.
+       * eapply Hinv; eassumption.
+       * inversion H1.
+       * inversion H; subst; clear H.
+         eapply HA; eassumption.
+       * inversion H; subst; clear H.
+         inversion H1; subst; clear H1.
+    Qed.
+
+    Lemma invariant_is_invariant:
+      forall st1 st2, step st1 st2 -> invariant st1 -> invariant st2.
+    Proof.
+      intros st1 st2 Hstep Hinv.
+      induction Hstep.
+      * (* NewService *)
+        apply invariant_Add_HasType.
+        - apply Hinv.
+        - intros  B s2 HB.
+          eapply H in HB.
+          inversion HB.
+      * (* EvolveService *) 
+        admit.
+      * (* LearnService *)
+        apply invariant_Add_HasRef.
+        - apply Hinv.
+        - intros s2 HHasType.
+          (* Uniqueness of HasType, reflexivity *)
+          admit.
+      * (* TransmitService *) 
+        apply invariant_Add_HasRef.
+        - apply Hinv.
+        - intros s3 HC.
+        admit.
+      * (* HostSubtyping *)
+        apply invariant_Add_HasRef.
+        - admit.
+        - intros s3 HB.
+          admit.
     Admitted.
 
+
 End IDL.
\ No newline at end of file

From f1dd58ff81d73a9206cb1d7a664d1221c2e96287 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 3 Dec 2020 12:19:22 +0100
Subject: [PATCH 06/25] Finish IDL-Soundess proof

---
 coq/IDLSoundness.v | 431 ++++++++++++++++++++++++++++++++-------------
 1 file changed, 311 insertions(+), 120 deletions(-)

diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index e8f2edf1..35a055d4 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -1,63 +1,64 @@
-(* This tries to formalize 
+(* This 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
 *)
-Require Import Coq.Sets.Ensembles.
 Arguments In {U}.
 Arguments Add {U}.
 Arguments Empty_set {U}.
 
 Require Import Coq.Relations.Relation_Operators.
 Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Operators_Properties.
 
 Set Bullet Behavior "Strict Subproofs".
- 
+
 Section IDL.
 
   (* An abstract theory of IDLs is parametrized as follows: *)
-  
+
   (* Argument or result types *)
   Variable T : Set.
-  
+
   (* A service type is a pair of types *)
   Definition S : Set := (T * T).
   Notation "t1 --> t2" := (t1, t2) (at level 80, no associativity).
-  
+
   (* The prediates of the theory *)
   Variable decodesAt : T -> T -> Prop.
   Notation "t1 <: t2" := (decodesAt t1 t2) (at level 70, no associativity).
-  
+
   Variable passesThrough : S -> T -> S -> T -> Prop.
   Notation "s1 ∈ t1 <: s2 ∈ t2" := (passesThrough s1 t1 s2 t2)
     (t1 at level 50, s2 at level 50, at level 70, no associativity).
-  
+
   Variable evolves : S -> S -> Prop.
   Notation "s1 ~> s2" := (evolves s1 s2) (at level 70, no associativity).
-  
+
   Variable hostSubtyping : S -> S -> Prop.
   Notation "s1 <<: s2" := (hostSubtyping s1 s2) (at level 70, no associativity).
 
   (* Service Identifiers *)
   Variable I : Set.
 
-  (* Judgements *)  
+  (* Judgements *)
   Inductive Assertion : Set :=
     | HasType : I -> S -> Assertion
     | HasRef : I -> I -> S -> Assertion.
 
   Definition State := Ensemble Assertion.
-  
+
   Definition FreshIn (i : I) (st : State) : Prop :=
     (forall s, ~ In st (HasType i s)) /\
     (forall i' s, ~ In st (HasRef i i' s)) /\
     (forall i' s, ~ In st (HasRef i' i s)).
-  
+
   Inductive CanSend : State -> I -> T -> T -> I -> Prop :=
     | CanCall: forall st A B t1 t1' t2 t2',
       In st (HasRef A B (t1 --> t1')) ->
@@ -67,7 +68,7 @@ Section IDL.
       In st (HasRef B A (t1 --> t1')) ->
       In st (HasType A (t2 --> t2')) ->
       CanSend st A t2' t1' B.
-      
+
   Inductive step : State -> State -> Prop :=
     | NewService :
       forall (i : I) (s : S) st,
@@ -99,110 +100,300 @@ Section IDL.
 
   Definition IDLSound : Prop :=
     forall s, clos_refl_trans _ step Empty_set s -> StateSound s.
-    
-   (* Now we continue with the soundness proof for canonical subtyping.
-      TODO: Modularize this development, instead of continuing in the same Section *)
-     
-    Hypothesis decodesAt_refl: reflexive _ decodesAt.
-    Hypothesis decodesAt_trans: transitive _ decodesAt.
-
-    Variable service_subtyping : S -> S -> Prop.
-    Notation "s1 <:: s2" := (service_subtyping s1 s2) (at level 70, no associativity).
-    Hypothesis service_subtype_sound:
-     forall t1 t1' t2 t2',
-       (t1 --> t1') <:: (t2 --> t2') ->
-       t1' <: t2' /\ t2 <: t1.
-
-    Hypothesis evolves_correctly:
-     forall s1 s2, s2 <:: s1 -> s1 ~> s2.
-    Hypothesis compositional:
-      forall t1 t2 s1 s2,
-      t1 <: t2 -> s1 ∈ t1 <: s2 ∈ t2 -> s1 <:: s2.
-    Hypothesis host_subtyping_sound:
-     forall s1 s2, s2 <<: s1 -> s1 <:: s2.
-    
-    Definition invariant (st : State) :=
-       forall A B s1 s2,
-       In st (HasType A s1) -> In st (HasRef B A s2) -> s1 <:: s2 .
-    
-    Lemma invariant_implies_StateSound:
-      forall st, invariant st -> StateSound st.
-    Proof.
-      intros st Hinvariant.
-      intros A t1 t2 B HCanSend.
-      destruct HCanSend.
-      * pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
-        apply service_subtype_sound in H1.
-        apply H1.
-      * pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
-        apply service_subtype_sound in H1.
-        apply H1.
-    Qed.
-
-    Lemma invariant_Add_HasType:
-      forall st A s1,
-      invariant st ->
-      (forall B s2, In st (HasRef B A s2) -> s1 <:: s2) ->
-      invariant (Add st (HasType A s1)).
-    Proof.
-       intros st A s1 Hinv HA.
-       intros A' B s1' s2 HHasType HHasRef.
-       inversion HHasType; clear HHasType; inversion HHasRef; clear HHasRef; subst.
-       * eapply Hinv; eassumption.
-       * inversion H1.
-       * inversion H; subst; clear H.
-         eapply HA; eassumption.
-       * inversion H; subst; clear H.
-         inversion H1; subst; clear H1.
-    Qed.
-
-    Lemma invariant_Add_HasRef:
-      forall st A B s2,
-      invariant st ->
-      (forall s1, In st (HasType B s1) -> s1 <:: s2) ->
-      invariant (Add st (HasRef A B s2)).
-    Proof.
-       intros st A B s2 Hinv HA.
-       intros A' B' s1' s2' HHasRef HHasType.
-       inversion HHasType; clear HHasType; inversion HHasRef; clear HHasRef; subst.
-       * eapply Hinv; eassumption.
-       * inversion H1.
-       * inversion H; subst; clear H.
-         eapply HA; eassumption.
-       * inversion H; subst; clear H.
-         inversion H1; subst; clear H1.
-    Qed.
-
-    Lemma invariant_is_invariant:
-      forall st1 st2, step st1 st2 -> invariant st1 -> invariant st2.
-    Proof.
-      intros st1 st2 Hstep Hinv.
-      induction Hstep.
-      * (* NewService *)
-        apply invariant_Add_HasType.
-        - apply Hinv.
-        - intros  B s2 HB.
-          eapply H in HB.
-          inversion HB.
-      * (* EvolveService *) 
-        admit.
-      * (* LearnService *)
-        apply invariant_Add_HasRef.
-        - apply Hinv.
-        - intros s2 HHasType.
-          (* Uniqueness of HasType, reflexivity *)
-          admit.
-      * (* TransmitService *) 
-        apply invariant_Add_HasRef.
-        - apply Hinv.
-        - intros s3 HC.
-        admit.
-      * (* HostSubtyping *)
-        apply invariant_Add_HasRef.
-        - admit.
-        - intros s3 HB.
-          admit.
-    Admitted.
-
-
-End IDL.
\ No newline at end of file
+
+  (* Now we continue with the soundness proof for 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.
+   *)
+
+  Hypothesis decodesAt_refl: reflexive _ decodesAt.
+  Hypothesis decodesAt_trans: transitive _ decodesAt.
+
+  Variable service_subtyping : S -> S -> Prop.
+  Notation "s1 <:: s2" := (service_subtyping s1 s2) (at level 70, no associativity).
+  Hypothesis service_subtype_sound:
+   forall t1 t1' t2 t2',
+     (t1 --> t1') <:: (t2 --> t2') <->
+     t1' <: t2' /\ t2 <: t1.
+
+  Hypothesis evolves_correctly:
+   forall s1 s2, s1 ~> s2 -> s2 <:: s1.
+  Hypothesis compositional:
+    forall t1 t2 s1 s2,
+    t1 <: t2 -> s1 ∈ t1 <: s2 ∈ t2 -> s1 <:: s2.
+  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
+  proofs in Isabelle. But hey, it works, and may aid readiablity.
+  *)
+
+  Lemma service_subtype_refl: reflexive _ service_subtyping.
+  Proof.
+    intros [t1 t1'].
+    rewrite service_subtype_sound.
+    split; apply decodesAt_refl.
+  Qed.
+
+  Lemma service_subtype_trans: transitive _ service_subtyping.
+  Proof.
+    intros [t1 t1'] [t2 t2'] [t3 t3'] H1 H2.
+    rewrite service_subtype_sound in *.
+    destruct H1, H2.
+    split; eapply decodesAt_trans; eassumption.
+  Qed.
+
+
+  Definition unique (st : State) :=
+     forall A s1 s2,
+     In st (HasType A s1) -> In st (HasType A s2) -> s1 = s2.
+
+  Definition invariant (st : State) :=
+     forall A B s1 s2,
+     In st (HasType A s1) -> In st (HasRef B A s2) -> s1 <:: s2 .
+
+  Lemma invariant_implies_StateSound:
+    forall st, invariant st -> StateSound st.
+  Proof.
+    intros st Hinvariant.
+    intros A t1 t2 B HCanSend.
+    destruct HCanSend.
+    * pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
+      apply service_subtype_sound in H1.
+      apply H1.
+    * pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
+      apply service_subtype_sound in H1.
+      apply H1.
+  Qed.
+
+  Lemma invariant_Add_HasType:
+    forall st A s1,
+    invariant st ->
+    (forall B s2, In st (HasRef B A s2) -> s1 <:: s2) ->
+    invariant (Add st (HasType A s1)).
+  Proof.
+     intros st A s1 Hinv HA.
+     intros A' B s1' s2 HHasType HHasRef.
+     inversion HHasType; clear HHasType; inversion HHasRef; clear HHasRef; subst.
+     * eapply Hinv; eassumption.
+     * inversion H1.
+     * inversion H; subst; clear H.
+       eapply HA; eassumption.
+     * inversion H; subst; clear H.
+       inversion H1; subst; clear H1.
+  Qed.
+
+  Lemma invariant_Add_HasRef:
+    forall st A B s2,
+    invariant st ->
+    (forall s1, In st (HasType B s1) -> s1 <:: s2) ->
+    invariant (Add st (HasRef A B s2)).
+  Proof.
+    intros st A B s2 Hinv HA.
+    intros A' B' s1' s2' HHasRef HHasType.
+    inversion HHasType; clear HHasType; inversion HHasRef; clear HHasRef; subst.
+    * eapply Hinv; eassumption.
+    * inversion H1.
+    * inversion H; subst; clear H.
+      eapply HA; eassumption.
+    * inversion H; subst; clear H.
+      inversion H1; subst; clear H1.
+  Qed.
+
+  Lemma invariant_Add_HasType_elim:
+    forall st A s1,
+    invariant (Add st (HasType A s1)) ->
+    invariant st /\ (forall B s2, In st (HasRef B A s2) -> s1 <:: s2).
+  Proof.
+    intros st A s1 HInv.
+    split.
+    * intros A' B' s1' s2' HHasRef HHasType.
+      eapply HInv.
+      - apply Union_introl. eassumption.
+      - apply Union_introl. eassumption.
+    * intros B s2' HIn.
+      eapply HInv.
+      - apply Union_intror. constructor.
+      - apply Union_introl. eassumption.
+  Qed.
+
+  Lemma invariant_Add_HasRef_elim:
+    forall st A B s2,
+    invariant (Add st (HasRef A B s2)) ->
+    invariant st /\ (forall s1, In st (HasType B s1) -> s1 <:: s2).
+  Proof.
+    intros st A B s2 HInv.
+    split.
+    * intros A' B' s1' s2' HHasRef HHasType.
+      eapply HInv.
+      - apply Union_introl. eassumption.
+      - apply Union_introl. eassumption.
+    * intros s1' HIn.
+      eapply HInv.
+      - apply Union_introl. eassumption.
+      - apply Union_intror. constructor.
+  Qed.
+
+  Lemma invariant_Change_HasType:
+    forall st A s1 s2,
+    invariant (Add st (HasType A s1)) ->
+    (forall B s3, In st (HasRef B A s3) -> s1 <:: s3 -> s2 <:: s3) ->
+    invariant (Add st (HasType A s2)).
+  Proof.
+    intros st A s1 s2 Hinv Himp.
+    apply invariant_Add_HasType_elim in Hinv as [Hinv HA].
+    apply invariant_Add_HasType.
+    * apply Hinv.
+    * intros B s3 HHasRef.
+      eapply Himp.
+      - apply HHasRef.
+      - eapply HA. apply HHasRef.
+  Qed.
+
+  Lemma invariant_Change_HasRef:
+    forall st A B s1 s2,
+    invariant (Add st (HasRef A B s1)) ->
+    (forall s3, In st (HasType B s3) -> s3 <:: s1 -> s3 <:: s2) ->
+    invariant (Add st (HasRef A B s2)).
+  Proof.
+    intros st A B s1 s2 Hinv Himp.
+    apply invariant_Add_HasRef_elim in Hinv as [Hinv HA].
+    apply invariant_Add_HasRef.
+    * apply Hinv.
+    * intros s3 HHasType.
+      apply Himp.
+      - apply HHasType.
+      - apply HA. apply HHasType.
+  Qed.
+
+  Lemma unique_Add_HasRef:
+    forall st A B s,
+    unique (Add st (HasRef A B s)) <-> unique st.
+  Proof.
+    intros st A B s.
+    split; intro Huniq.
+    * intros A' s1' s2' HType1 HType2.
+      eapply Huniq.
+      - apply Union_introl. eassumption.
+      - apply Union_introl. eassumption.
+    * intros A' s1' s2' HType1 HType2.
+      inversion HType1; subst; clear HType1;
+      inversion HType2; subst; clear HType2.
+      - eapply Huniq; eassumption.
+      - inversion H0; subst; clear H0.
+      - inversion H; subst; clear H.
+      - inversion H; subst; clear H.
+  Qed.
+
+  Lemma step_preserves_unique:
+    forall st1 st2, step st1 st2 -> unique st1 -> unique st2.
+  Proof.
+    intros st1 st2 Hstep Huniq.
+    induction Hstep.
+    * (* NewService *)
+      intros A' s1' s2' HType1 HType2.
+      inversion HType1; subst; clear HType1;
+      inversion HType2; subst; clear HType2.
+      - eapply Huniq; eassumption.
+      - inversion H1; subst; clear H1.
+        eapply H in H0. inversion H0.
+      - inversion H0; subst; clear H0.
+        eapply H in H1. inversion H1.
+      - inversion H1; subst; clear H1;
+        inversion H0; subst; clear H0.
+        reflexivity.
+    * (* EvolveService *)
+      intros A' s1' s2' HType1 HType2.
+      inversion HType1; subst; clear HType1;
+      inversion HType2; subst; clear HType2.
+      - eapply Huniq.
+        + apply Union_introl. eassumption.
+        + apply Union_introl. eassumption.
+      - inversion H2; subst; clear H2.
+        replace s1' with s1 in *.
+        + tauto.
+        + eapply Huniq.
+          ** apply Union_intror. constructor.
+          ** apply Union_introl. assumption.
+      - inversion H1; subst; clear H1.
+        replace s2' with s1 in *.
+        + tauto.
+        + eapply Huniq.
+          ** apply Union_intror. constructor.
+          ** apply Union_introl. assumption.
+      - inversion H1; subst; clear H1;
+        inversion H2; subst; clear H0.
+        reflexivity.
+    * (* LearnService *)
+      rewrite unique_Add_HasRef in *.
+      assumption.
+    * (* TransmitService *)
+      rewrite unique_Add_HasRef in *.
+      assumption.
+    * (* HostSubtyping *)
+      rewrite unique_Add_HasRef in *.
+      assumption.
+  Qed.
+
+  Lemma step_preserves_invariant:
+    forall st1 st2, step st1 st2 -> unique st1 -> invariant st1 -> invariant st2.
+  Proof.
+    intros st1 st2 Hstep Huniq Hinv.
+    induction Hstep.
+    * (* NewService *)
+      apply invariant_Add_HasType.
+      - apply Hinv.
+      - intros  B s2 HB.
+        eapply H in HB.
+        inversion HB.
+    * (* EvolveService *)
+      eapply invariant_Change_HasType.
+      - apply Hinv.
+      - intros B s3 HB Hsub.
+        apply evolves_correctly in H0.
+        eapply service_subtype_trans; eassumption.
+    * (* LearnService *)
+      apply invariant_Add_HasRef.
+      - apply Hinv.
+      - intros s2 HHasType.
+        (* Uniqueness of HasType, reflexivity *)
+        replace s2 with s.
+        + apply service_subtype_refl.
+        + eapply Huniq; eassumption.
+    * (* TransmitService *)
+      apply invariant_Add_HasRef.
+      - apply Hinv.
+      - intros s3 HC.
+        assert (Hsub : s3 <:: s1) by apply (Hinv _ _ _ _ HC H).
+        assert (HSound : StateSound st) by (apply invariant_implies_StateSound; assumption).
+        assert (t1 <: t2) by (eapply HSound; apply H0).
+        assert (s1 <:: s2) by (eapply compositional;  eassumption).
+        eapply service_subtype_trans; eassumption.
+    * (* HostSubtyping *)
+      eapply invariant_Change_HasRef.
+      - apply Hinv.
+      - intros s3 HB Hsub.
+        apply host_subtyping_sound in H.
+        eapply service_subtype_trans; eassumption.
+  Qed.
+
+  Lemma canonical_soundness: IDLSound.
+  Proof.
+    intros st Hclos.
+    enough (unique st /\ invariant st) by (apply invariant_implies_StateSound; tauto).
+    induction Hclos using clos_refl_trans_ind_left.
+    - split.
+      * intros A s1 s2 Hin1 Hin2. inversion Hin1.
+      * intros A B s1 s2 Hin1 Hin2. inversion Hin1.
+    - inversion IHHclos. split.
+      * eapply step_preserves_unique; eassumption.
+      * eapply step_preserves_invariant; eassumption.
+  Qed.
+
+End IDL.

From 88551a3e84d8880c0c00dce0dcd2695ad614c083 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 3 Dec 2020 15:10:25 +0100
Subject: [PATCH 07/25] Small cleanup

---
 coq/IDLSoundness.v | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index 35a055d4..11fa79be 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -112,13 +112,12 @@ Section IDL.
   Hypothesis decodesAt_refl: reflexive _ decodesAt.
   Hypothesis decodesAt_trans: transitive _ decodesAt.
 
-  Variable service_subtyping : S -> S -> Prop.
+  Definition service_subtyping (s1 s2 : S) : Prop :=
+    let '(t1 --> t1') := s1 in
+    let '(t2 --> t2') := s2 in
+    t1' <: t2' /\ t2 <: t1.
   Notation "s1 <:: s2" := (service_subtyping s1 s2) (at level 70, no associativity).
-  Hypothesis service_subtype_sound:
-   forall t1 t1' t2 t2',
-     (t1 --> t1') <:: (t2 --> t2') <->
-     t1' <: t2' /\ t2 <: t1.
-
+  
   Hypothesis evolves_correctly:
    forall s1 s2, s1 ~> s2 -> s2 <:: s1.
   Hypothesis compositional:
@@ -137,14 +136,12 @@ Section IDL.
   Lemma service_subtype_refl: reflexive _ service_subtyping.
   Proof.
     intros [t1 t1'].
-    rewrite service_subtype_sound.
     split; apply decodesAt_refl.
   Qed.
 
   Lemma service_subtype_trans: transitive _ service_subtyping.
   Proof.
     intros [t1 t1'] [t2 t2'] [t3 t3'] H1 H2.
-    rewrite service_subtype_sound in *.
     destruct H1, H2.
     split; eapply decodesAt_trans; eassumption.
   Qed.
@@ -165,10 +162,8 @@ Section IDL.
     intros A t1 t2 B HCanSend.
     destruct HCanSend.
     * pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
-      apply service_subtype_sound in H1.
       apply H1.
     * pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
-      apply service_subtype_sound in H1.
       apply H1.
   Qed.
 

From b5ca271b85ea838631b7e0e60a8e957ab3413f9b Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 3 Dec 2020 18:15:59 +0100
Subject: [PATCH 08/25] Coq: MiniCandid

starting a bit on a Candid formalization, focusing on the
Opt-to-constituent rule.

Stuck at https://github.com/dfinity/candid/issues/146,
and worked around by adding restrictions to the compositional rule for
opt.
---
 coq/MiniCandid.v | 153 +++++++++++++++++++++++++++++++++++++++++++++++
 coq/dune         |   2 +-
 2 files changed, 154 insertions(+), 1 deletion(-)
 create mode 100644 coq/MiniCandid.v

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
new file mode 100644
index 00000000..1614a6dd
--- /dev/null
+++ b/coq/MiniCandid.v
@@ -0,0 +1,153 @@
+(*
+MiniCandid: A formalization of the core ideas of Candid
+*)
+
+Require Import Coq.ZArith.BinInt.
+
+Require Import Coq.Relations.Relation_Operators.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Operators_Properties.
+
+Set Bullet Behavior "Strict Subproofs".
+
+
+(* Types are coinductive (we do not want to model the graph structure explicilty) *)
+CoInductive T :=
+  | NatT: T
+  | IntT: T
+  | NullT : T
+  | OptT : T -> T.
+
+Inductive V :=
+  | NatV : nat -> V
+  | IntV : Z -> V
+  | NullV : V
+  | SomeV : V -> V.
+
+
+Definition is_not_opt_like_type (t : T) : Prop :=
+  match t with
+  | NullT => False
+  | OptT _ => False
+  | _ => True
+  end.
+
+Reserved Infix "<:" (at level 80, no associativity).
+CoInductive Subtype : T -> T -> Prop :=
+  | ReflST : forall t, t <: t
+  | NatIntST : NatT <: IntT
+  | NullOptST : forall t, NullT <: OptT t
+  | OptST :
+    forall t1 t2,
+    (* This additional restriction added to fix https://github.com/dfinity/candid/issues/146 *)
+    (is_not_opt_like_type t1 <-> is_not_opt_like_type t2) -> 
+    t1 <: t2 ->
+    OptT t1 <: OptT t2
+  | ConstituentOptST :
+    forall t1 t2,
+    is_not_opt_like_type t2 ->
+    t1 <: t2 -> t1 <: OptT t2
+where "t1 <: t2" := (Subtype t1 t2).
+
+
+Inductive HasType : V -> T -> Prop :=
+  | NatHT: forall n, NatV n :: NatT
+  | IntHT: forall n, IntV n :: IntT
+  | NullHT: NullV :: NullT
+  | NullOptHT: forall t, NullV :: OptT t
+  | OptHT: forall v t, v :: t -> SomeV v :: OptT t
+where "v :: t" := (HasType v t).
+
+Definition is_not_opt_like_value (v : V) : Prop :=
+  match v with
+  | NullV => False
+  | SomeV _ => False
+  | _ => True
+  end.
+
+
+Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity).
+Inductive Coerces : V -> V -> T -> Prop :=
+  | NatC: forall n, (NatV n ~> NatV n :: NatT)
+  | IntC: forall n, (IntV n ~> IntV n :: IntT)
+  | NatIntC: forall n i, i = Z.of_nat n -> (NatV n ~> IntV i :: IntT)
+  | NullC: NullV ~> NullV :: NullT
+  | NullOptC: forall t, NullV ~> NullV :: OptT t
+  | SomeOptC: forall v1 v2 t, v1 ~> v2 :: t -> SomeV v1 ~> SomeV v2 :: OptT t
+  | ConstituentOptC: forall v1 v2 t,
+    is_not_opt_like_value v1 ->
+    v1 ~> v2 :: t ->
+    v1 ~> SomeV v2 :: OptT t
+where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
+
+Theorem coercion_correctness:
+  forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
+Proof.
+  intros. induction H; constructor; assumption.
+Qed.
+
+Theorem coercion_roundtrip:
+  forall v t, v :: t -> v ~> v :: t.
+Proof.
+  intros. induction H; constructor; intuition.
+Qed.
+
+Theorem coercion_uniqueness:
+  forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2.
+Proof.
+  intros.
+  revert v2 H0.
+  induction H; intros v2' Hother;
+    try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence).
+Qed.
+
+Theorem soundness_of_subtyping:
+  forall t1 t2,
+  t1 <: t2 ->
+  forall v1, v1 :: t1 -> exists v2, v1 ~> v2 :: t2.
+Proof.
+  intros t1 t2 Hsub v HvT. revert t2 Hsub.
+  induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
+    try (eexists;constructor; fail).
+  * eexists. constructor. reflexivity. 
+  * inversion H0; subst; clear H0; simpl in H; inversion H.
+    - eexists. constructor; try constructor.
+    - eexists. constructor; try constructor; reflexivity.
+  * inversion H0; subst; clear H0; simpl in H; inversion H.
+    econstructor. econstructor. constructor. constructor.
+  * specialize (IHHvT t (ReflST _)).
+    destruct IHHvT as [v2 Hv2].
+    eexists; econstructor; try eassumption.
+  * specialize (IHHvT _ H1).
+    destruct IHHvT as [v2 Hv2].
+    eexists; econstructor; eassumption.
+  * inversion H0; subst; clear H0; simpl in H; inversion H.
+Qed.
+
+Theorem subtyping_refl: reflexive _ Subtype.
+Proof. intros x. apply ReflST. Qed.
+
+Lemma is_not_opt_like_type_contravariant:
+  forall t1 t2,
+     is_not_opt_like_type t1 -> t2 <: t1 -> is_not_opt_like_type t2.
+Proof. intros. destruct t1, t2; easy. Qed.
+
+Theorem subtyping_trans: transitive _ Subtype.
+Proof.
+  cofix Hyp.
+  intros t1 t2 t3 H1 H2.
+  inversion H1; subst; clear H1;
+  inversion H2; subst; clear H2;
+    try (constructor; easy).
+  * constructor. assumption.
+    eapply Hyp; [econstructor|assumption].
+  * constructor.
+    - intuition.
+    - eapply Hyp; eassumption.
+  * inversion H3; subst; clear H3; simpl in H0; contradiction.
+  * constructor.
+    - intuition.
+    - firstorder.
+  * inversion H3; subst; clear H3; try easy.
+Guarded.
+Qed.
\ No newline at end of file
diff --git a/coq/dune b/coq/dune
index cd6bb06c..984be181 100644
--- a/coq/dune
+++ b/coq/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name "candid")
  (synopsis "Coq for candid")
- (modules "IDLSoundness")
+ (modules IDLSoundness MiniCandid)
 )

From 0f7a32630cd3862936443c86666472ea253ac1ec Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 3 Dec 2020 18:30:34 +0100
Subject: [PATCH 09/25] Show that is_not_opt_like_type t <-> ~ (NullT <: t)

---
 coq/MiniCandid.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 1614a6dd..d0a51b51 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -80,6 +80,20 @@ Inductive Coerces : V -> V -> T -> Prop :=
     v1 ~> SomeV v2 :: OptT t
 where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
 
+(* The is_not_opt_like_type definition is only introduced because
+   Coq (and not only coq) does not like hyptheses like ~(null <: t)
+*)
+Lemma is_not_opt_like_type_correct:
+  forall t,
+  is_not_opt_like_type t <-> ~ (NullT <: t).
+Proof.
+  intros. destruct t; simpl; intuition.
+  * inversion H0.
+  * inversion H0.
+  * apply H. constructor.
+  * apply H. constructor.
+Qed.
+
 Theorem coercion_correctness:
   forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
 Proof.
@@ -149,5 +163,4 @@ Proof.
     - intuition.
     - firstorder.
   * inversion H3; subst; clear H3; try easy.
-Guarded.
 Qed.
\ No newline at end of file

From 40f45ab0a776284602553b3583c1df8244241953 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 4 Dec 2020 16:07:26 +0100
Subject: [PATCH 10/25] Play around with named cases

---
 coq/MiniCandid.v | 105 ++++++++++++++++++++++++++++++------------
 coq/NamedCases.v | 116 +++++++++++++++++++++++++++++++++++++++++++++++
 coq/_CoqProject  |   1 +
 coq/dune         |   2 +-
 4 files changed, 193 insertions(+), 31 deletions(-)
 create mode 100644 coq/NamedCases.v
 create mode 100644 coq/_CoqProject

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index d0a51b51..b0e6b577 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -9,7 +9,9 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Relations.Operators_Properties.
 
 Set Bullet Behavior "Strict Subproofs".
+Set Default Goal Selector "!".
 
+Require Import candid.NamedCases.
 
 (* Types are coinductive (we do not want to model the graph structure explicilty) *)
 CoInductive T :=
@@ -34,16 +36,24 @@ Definition is_not_opt_like_type (t : T) : Prop :=
 
 Reserved Infix "<:" (at level 80, no associativity).
 CoInductive Subtype : T -> T -> Prop :=
-  | ReflST : forall t, t <: t
-  | NatIntST : NatT <: IntT
-  | NullOptST : forall t, NullT <: OptT t
+  | ReflST :
+    forall Case_ReflSL : CaseName,
+    forall t, t <: t
+  | NatIntST :
+    forall Case_NatIntSL : CaseName,
+    NatT <: IntT
+  | NullOptST :
+    forall Case_NullOptST : CaseName,
+    forall t, NullT <: OptT t
   | OptST :
+    forall Case_OptST : CaseName,
     forall t1 t2,
     (* This additional restriction added to fix https://github.com/dfinity/candid/issues/146 *)
     (is_not_opt_like_type t1 <-> is_not_opt_like_type t2) -> 
     t1 <: t2 ->
     OptT t1 <: OptT t2
   | ConstituentOptST :
+    forall Case_ConstituentOptST : CaseName,
     forall t1 t2,
     is_not_opt_like_type t2 ->
     t1 <: t2 -> t1 <: OptT t2
@@ -51,11 +61,21 @@ where "t1 <: t2" := (Subtype t1 t2).
 
 
 Inductive HasType : V -> T -> Prop :=
-  | NatHT: forall n, NatV n :: NatT
-  | IntHT: forall n, IntV n :: IntT
-  | NullHT: NullV :: NullT
-  | NullOptHT: forall t, NullV :: OptT t
-  | OptHT: forall v t, v :: t -> SomeV v :: OptT t
+  | NatHT:
+    forall Case_NatHT : CaseName,
+    forall n, NatV n :: NatT
+  | IntHT:
+    forall Case_IntHT : CaseName,
+    forall n, IntV n :: IntT
+  | NullHT:
+    forall Case_NullHT : CaseName,
+    NullV :: NullT
+  | NullOptHT:
+    forall Case_NullOptHT : CaseName,
+    forall t, NullV :: OptT t
+  | OptHT:
+    forall Case_OptHT : CaseName,
+    forall v t, v :: t -> SomeV v :: OptT t
 where "v :: t" := (HasType v t).
 
 Definition is_not_opt_like_value (v : V) : Prop :=
@@ -68,13 +88,27 @@ Definition is_not_opt_like_value (v : V) : Prop :=
 
 Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity).
 Inductive Coerces : V -> V -> T -> Prop :=
-  | NatC: forall n, (NatV n ~> NatV n :: NatT)
-  | IntC: forall n, (IntV n ~> IntV n :: IntT)
-  | NatIntC: forall n i, i = Z.of_nat n -> (NatV n ~> IntV i :: IntT)
-  | NullC: NullV ~> NullV :: NullT
-  | NullOptC: forall t, NullV ~> NullV :: OptT t
-  | SomeOptC: forall v1 v2 t, v1 ~> v2 :: t -> SomeV v1 ~> SomeV v2 :: OptT t
-  | ConstituentOptC: forall v1 v2 t,
+  | NatC: 
+    forall Case_NatC : CaseName,
+    forall n, (NatV n ~> NatV n :: NatT)
+  | IntC:
+    forall Case_IntC : CaseName,
+    forall n, (IntV n ~> IntV n :: IntT)
+  | NatIntC:
+    forall Case_NatIntC : CaseName,
+    forall n i, i = Z.of_nat n -> (NatV n ~> IntV i :: IntT)
+  | NullC:
+    forall Case_NullC : CaseName,
+    NullV ~> NullV :: NullT
+  | NullOptC:
+    forall Case_NullOptC : CaseName,
+    forall t, NullV ~> NullV :: OptT t
+  | SomeOptC:
+    forall Case_SomeOptC : CaseName,
+    forall v1 v2 t, v1 ~> v2 :: t -> SomeV v1 ~> SomeV v2 :: OptT t
+  | ConstituentOptC:
+    forall Case_ConstituentC : CaseName,
+    forall v1 v2 t,
     is_not_opt_like_value v1 ->
     v1 ~> v2 :: t ->
     v1 ~> SomeV v2 :: OptT t
@@ -90,8 +124,8 @@ Proof.
   intros. destruct t; simpl; intuition.
   * inversion H0.
   * inversion H0.
-  * apply H. constructor.
-  * apply H. constructor.
+  * apply H. named_constructor.
+  * apply H. named_constructor.
 Qed.
 
 Theorem coercion_correctness:
@@ -122,14 +156,13 @@ Theorem soundness_of_subtyping:
 Proof.
   intros t1 t2 Hsub v HvT. revert t2 Hsub.
   induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
-    try (eexists;constructor; fail).
-  * eexists. constructor. reflexivity. 
+    try (eexists;constructor; try constructor; fail).
   * inversion H0; subst; clear H0; simpl in H; inversion H.
-    - eexists. constructor; try constructor.
-    - eexists. constructor; try constructor; reflexivity.
+    - eexists. named_constructor; [constructor|named_constructor].
+    - eexists. named_constructor; [constructor|named_constructor;reflexivity].
   * inversion H0; subst; clear H0; simpl in H; inversion H.
-    econstructor. econstructor. constructor. constructor.
-  * specialize (IHHvT t (ReflST _)).
+    econstructor. econstructor; named_constructor.
+  * specialize (IHHvT t (ReflST _ _)).
     destruct IHHvT as [v2 Hv2].
     eexists; econstructor; try eassumption.
   * specialize (IHHvT _ H1).
@@ -139,7 +172,7 @@ Proof.
 Qed.
 
 Theorem subtyping_refl: reflexive _ Subtype.
-Proof. intros x. apply ReflST. Qed.
+Proof. intros x. apply ReflST; constructor. Qed.
 
 Lemma is_not_opt_like_type_contravariant:
   forall t1 t2,
@@ -152,15 +185,27 @@ Proof.
   intros t1 t2 t3 H1 H2.
   inversion H1; subst; clear H1;
   inversion H2; subst; clear H2;
+    name_cases;
     try (constructor; easy).
-  * constructor. assumption.
-    eapply Hyp; [econstructor|assumption].
-  * constructor.
+  [Case_NatIntSL_Case_ConstituentOptST]: {
+    named_constructor.
+    - assumption.
+    - eapply Hyp; [named_econstructor | assumption].
+  }
+  [Case_OptST_Case_OptST0]: {
+    named_constructor.
     - intuition.
     - eapply Hyp; eassumption.
-  * inversion H3; subst; clear H3; simpl in H0; contradiction.
-  * constructor.
+  }
+  [Case_OptST_Case_ConstituentOptST]: {
+    inversion H3; subst; clear H3; simpl in H0; contradiction.
+  }
+  [Case_ConstituentOptST_Case_OptST]: {
+    named_constructor.
     - intuition.
     - firstorder.
-  * inversion H3; subst; clear H3; try easy.
+  }
+  [Case_ConstituentOptST_Case_ConstituentOptST0]: {
+    inversion H3; subst; clear H3; try easy.
+  }
 Qed.
\ No newline at end of file
diff --git a/coq/NamedCases.v b/coq/NamedCases.v
new file mode 100644
index 00000000..f7ee6565
--- /dev/null
+++ b/coq/NamedCases.v
@@ -0,0 +1,116 @@
+(** Fun stuff trying to emulate Isar-style case names *)
+
+From Ltac2 Require Import Ltac2.
+From Ltac2 Require Option.
+Set Default Proof Mode "Classic".
+
+Inductive CaseName := CaseNameI.
+
+Existing Class CaseName.
+Existing Instance CaseNameI.
+
+Require Import Coq.Strings.String.
+Import StringSyntax.
+
+(*
+Require Import candid.StringToIdent.
+*)
+
+Ltac2 strcpy := fun s1 s2 o =>
+    let rec go := fun n =>
+      match Int.lt n (String.length s2) with
+      | true => String.set s1 (Int.add o n) (String.get s2 n); go (Int.add n 1)
+      | false => ()
+      end
+    in go 0.
+Ltac2 concat := fun s1 s2 => 
+    let l := Int.add (Int.add (String.length s1) (String.length s2)) 1 in
+    let s := String.make l (Char.of_int 95) in
+    strcpy s s1 0;
+    strcpy s s2 (Int.add (String.length s1) 1);
+    s.
+Ltac2 rec combine_case_names () :=
+  repeat (lazy_match! goal with
+  | [ h1 : CaseName, h2 : CaseName |- _ ] =>
+    let h := concat (Ident.to_string h1) (Ident.to_string h2) in
+    (* Message.print (Message.of_string h); *)
+    let h := Option.get (Ident.of_string h) in
+    Std.clear [h1; h2];
+    assert ($h : CaseName) by apply CaseNameI
+  | [ |- _ ] => fail
+  end).
+
+Ltac name_cases := 
+  [> (
+    ltac2:(combine_case_names ());
+    lazymatch goal with
+    | [ H : CaseName |- _ ] => refine ?[H]; clear H
+    | _ => idtac "Could not find a CaseName assumption"; fail
+    end
+  )..].
+  
+  
+Ltac named_constructor :=
+  constructor; only 1: apply CaseNameI.
+Ltac named_econstructor :=
+  econstructor; only 1: apply CaseNameI.
+
+(* 
+Notation "''case'' x , t" := (forall x : CaseName, t)
+  (at level 10, x at level 1000, t at level 1000).
+*)
+
+Section Example.
+
+  Inductive Test :=
+    | Foo: forall foo : CaseName, Test
+    | Bar: forall bar : CaseName, Test.
+
+  Goal Test -> Test.
+    intros.
+    destruct H; name_cases.
+    [foo]: {
+      named_constructor.
+    }
+    [bar]: {
+      named_constructor.
+    }
+  Qed.
+  
+  Goal Test -> Test -> Test.
+    intros.
+    destruct H; destruct H0; name_cases.
+    [foo_foo0]: {
+      named_constructor.
+    }
+    [foo_bar]: {
+      named_constructor.
+    }
+    [bar_foo]: {
+      named_constructor.
+    }
+    [bar_bar0]: {
+      named_constructor.
+    }
+  Qed.
+
+
+  Goal Test -> Test -> Test -> Test.
+    intros.
+    destruct H; destruct H0; destruct H1; name_cases.
+    Show Existentials.
+    [foo_foo0_bar]: {
+      named_constructor.
+    }
+    [foo_bar_foo0]: {
+      named_constructor.
+    }
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+    * named_constructor.
+  Qed.
+
+End Example.
\ No newline at end of file
diff --git a/coq/_CoqProject b/coq/_CoqProject
new file mode 100644
index 00000000..4919bd1f
--- /dev/null
+++ b/coq/_CoqProject
@@ -0,0 +1 @@
+-Q ./_build/default candid
diff --git a/coq/dune b/coq/dune
index 984be181..58a8bbb6 100644
--- a/coq/dune
+++ b/coq/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name "candid")
  (synopsis "Coq for candid")
- (modules IDLSoundness MiniCandid)
+ (modules IDLSoundness MiniCandid NamedCases)
 )

From d1d72b10515d96315ad60b1d1f3feec9d77758a1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 4 Dec 2020 17:18:37 +0100
Subject: [PATCH 11/25] Add VoidT

---
 coq/MiniCandid.v | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index b0e6b577..20a5fcb5 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -18,7 +18,9 @@ CoInductive T :=
   | NatT: T
   | IntT: T
   | NullT : T
-  | OptT : T -> T.
+  | OptT : T -> T
+  | VoidT : T
+  .
 
 Inductive V :=
   | NatV : nat -> V
@@ -57,9 +59,11 @@ CoInductive Subtype : T -> T -> Prop :=
     forall t1 t2,
     is_not_opt_like_type t2 ->
     t1 <: t2 -> t1 <: OptT t2
+  | VoidST :
+    forall Case_VoidST : CaseName,
+    forall t, VoidT <: t
 where "t1 <: t2" := (Subtype t1 t2).
 
-
 Inductive HasType : V -> T -> Prop :=
   | NatHT:
     forall Case_NatHT : CaseName,
@@ -122,10 +126,9 @@ Lemma is_not_opt_like_type_correct:
   is_not_opt_like_type t <-> ~ (NullT <: t).
 Proof.
   intros. destruct t; simpl; intuition.
-  * inversion H0.
-  * inversion H0.
-  * apply H. named_constructor.
-  * apply H. named_constructor.
+  all: try inversion H0.
+  * apply H; named_constructor.
+  * apply H; named_constructor.
 Qed.
 
 Theorem coercion_correctness:

From 091c951d7f0ebc7080cbada73b2d8c10260e7ae1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 4 Dec 2020 17:27:30 +0100
Subject: [PATCH 12/25] Add ReservedT

---
 coq/MiniCandid.v | 52 ++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 42 insertions(+), 10 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 20a5fcb5..de86b7ad 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -20,19 +20,22 @@ CoInductive T :=
   | NullT : T
   | OptT : T -> T
   | VoidT : T
+  | ReservedT : T
   .
 
 Inductive V :=
   | NatV : nat -> V
   | IntV : Z -> V
   | NullV : V
-  | SomeV : V -> V.
-
+  | SomeV : V -> V
+  | ReservedV : V
+  .
 
 Definition is_not_opt_like_type (t : T) : Prop :=
   match t with
   | NullT => False
   | OptT _ => False
+  | ReservedT => False
   | _ => True
   end.
 
@@ -62,6 +65,9 @@ CoInductive Subtype : T -> T -> Prop :=
   | VoidST :
     forall Case_VoidST : CaseName,
     forall t, VoidT <: t
+  | ReservedST :
+    forall Case_ReservedST : CaseName,
+    forall t, t <: ReservedT
 where "t1 <: t2" := (Subtype t1 t2).
 
 Inductive HasType : V -> T -> Prop :=
@@ -80,12 +86,16 @@ Inductive HasType : V -> T -> Prop :=
   | OptHT:
     forall Case_OptHT : CaseName,
     forall v t, v :: t -> SomeV v :: OptT t
+  | ReservedHT:
+    forall Case_ReservedHT : CaseName,
+    ReservedV :: ReservedT
 where "v :: t" := (HasType v t).
 
 Definition is_not_opt_like_value (v : V) : Prop :=
   match v with
   | NullV => False
   | SomeV _ => False
+  | ReservedV => False
   | _ => True
   end.
 
@@ -116,6 +126,10 @@ Inductive Coerces : V -> V -> T -> Prop :=
     is_not_opt_like_value v1 ->
     v1 ~> v2 :: t ->
     v1 ~> SomeV v2 :: OptT t
+  | ReservedC:
+    forall Case_ReservedC : CaseName,
+    forall v1,
+    v1 ~> ReservedV :: ReservedT
 where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
 
 (* The is_not_opt_like_type definition is only introduced because
@@ -129,6 +143,7 @@ Proof.
   all: try inversion H0.
   * apply H; named_constructor.
   * apply H; named_constructor.
+  * apply H; named_constructor.
 Qed.
 
 Theorem coercion_correctness:
@@ -159,19 +174,33 @@ Theorem soundness_of_subtyping:
 Proof.
   intros t1 t2 Hsub v HvT. revert t2 Hsub.
   induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
+    name_cases;
     try (eexists;constructor; try constructor; fail).
-  * inversion H0; subst; clear H0; simpl in H; inversion H.
+  [Case_NatHT_Case_ConstituentOptST]: {
+    inversion H0; subst; clear H0; simpl in H; inversion H.
     - eexists. named_constructor; [constructor|named_constructor].
     - eexists. named_constructor; [constructor|named_constructor;reflexivity].
-  * inversion H0; subst; clear H0; simpl in H; inversion H.
-    econstructor. econstructor; named_constructor.
-  * specialize (IHHvT t (ReflST _ _)).
+  }
+  [Case_IntHT_Case_ConstituentOptST]: {
+    inversion H0; subst; clear H0; simpl in H; inversion H.
+    econstructor. named_econstructor; named_constructor.
+  }
+  [Case_OptHT_Case_ReflSL]: {
+    specialize (IHHvT t (ReflST _ _)).
     destruct IHHvT as [v2 Hv2].
-    eexists; econstructor; try eassumption.
-  * specialize (IHHvT _ H1).
+    eexists. named_econstructor; try eassumption.
+  }
+  [Case_OptHT_Case_OptST]: {
+    specialize (IHHvT _ H1).
     destruct IHHvT as [v2 Hv2].
-    eexists; econstructor; eassumption.
-  * inversion H0; subst; clear H0; simpl in H; inversion H.
+    eexists; named_econstructor; eassumption.
+  }
+  [Case_OptHT_Case_ConstituentOptST]: {
+    inversion H0; subst; clear H0; simpl in H; inversion H.
+  }
+  [Case_ReservedHT_Case_ConstituentOptST]: {
+    inversion H0; subst; clear H0; simpl in H; inversion H.
+  }
 Qed.
 
 Theorem subtyping_refl: reflexive _ Subtype.
@@ -211,4 +240,7 @@ Proof.
   [Case_ConstituentOptST_Case_ConstituentOptST0]: {
     inversion H3; subst; clear H3; try easy.
   }
+  [Case_ReservedST_Case_ConstituentOptST]: {
+    inversion H0; subst; clear H0; inversion H.
+  }
 Qed.
\ No newline at end of file

From 614b112ba1ef98d0e0b651a7adccca940143debe Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 4 Dec 2020 17:31:34 +0100
Subject: [PATCH 13/25] Make named_constructor more strict

---
 coq/MiniCandid.v | 2 +-
 coq/NamedCases.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index de86b7ad..a57b7bd7 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -183,7 +183,7 @@ Proof.
   }
   [Case_IntHT_Case_ConstituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
-    econstructor. named_econstructor; named_constructor.
+    econstructor. named_econstructor; [constructor|named_constructor].
   }
   [Case_OptHT_Case_ReflSL]: {
     specialize (IHHvT t (ReflST _ _)).
diff --git a/coq/NamedCases.v b/coq/NamedCases.v
index f7ee6565..d4c88c29 100644
--- a/coq/NamedCases.v
+++ b/coq/NamedCases.v
@@ -51,9 +51,9 @@ Ltac name_cases :=
   
   
 Ltac named_constructor :=
-  constructor; only 1: apply CaseNameI.
+  constructor;[ apply CaseNameI | idtac .. ].
 Ltac named_econstructor :=
-  econstructor; only 1: apply CaseNameI.
+  econstructor;[ apply CaseNameI | idtac .. ].
 
 (* 
 Notation "''case'' x , t" := (forall x : CaseName, t)

From f50f0decef5e12ab7bc78089e33f0eb80bb2da9d Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 4 Dec 2020 17:34:11 +0100
Subject: [PATCH 14/25] Simplify

---
 coq/MiniCandid.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index a57b7bd7..a11a47ce 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -140,10 +140,7 @@ Lemma is_not_opt_like_type_correct:
   is_not_opt_like_type t <-> ~ (NullT <: t).
 Proof.
   intros. destruct t; simpl; intuition.
-  all: try inversion H0.
-  * apply H; named_constructor.
-  * apply H; named_constructor.
-  * apply H; named_constructor.
+  all: try inversion H0; (apply H; named_constructor).
 Qed.
 
 Theorem coercion_correctness:

From ebd6081c026a0c2797da8a378c821f99e55130dd Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 4 Dec 2020 18:52:43 +0100
Subject: [PATCH 15/25] Prettier case names

---
 coq/MiniCandid.v | 80 ++++++++++++++++++++++++++----------------------
 coq/NamedCases.v | 24 ++++++++-------
 2 files changed, 56 insertions(+), 48 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index a11a47ce..09aece0d 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -11,7 +11,9 @@ Require Import Coq.Relations.Operators_Properties.
 Set Bullet Behavior "Strict Subproofs".
 Set Default Goal Selector "!".
 
+(* Loads the idiosyncratic CaseNames extension *)
 Require Import candid.NamedCases.
+Set Printing Goal Names. (* Coqide doesn’t use it yet, will be in 8.13 *)
 
 (* Types are coinductive (we do not want to model the graph structure explicilty) *)
 CoInductive T :=
@@ -31,6 +33,8 @@ Inductive V :=
   | ReservedV : V
   .
 
+(* This is a stand in for `~(null <: t)` in places
+where <: is not allowed yet. *)
 Definition is_not_opt_like_type (t : T) : Prop :=
   match t with
   | NullT => False
@@ -42,52 +46,52 @@ Definition is_not_opt_like_type (t : T) : Prop :=
 Reserved Infix "<:" (at level 80, no associativity).
 CoInductive Subtype : T -> T -> Prop :=
   | ReflST :
-    forall Case_ReflSL : CaseName,
+    case reflSL,
     forall t, t <: t
   | NatIntST :
-    forall Case_NatIntSL : CaseName,
+    case natIntSL,
     NatT <: IntT
   | NullOptST :
-    forall Case_NullOptST : CaseName,
+    case nullOptST,
     forall t, NullT <: OptT t
   | OptST :
-    forall Case_OptST : CaseName,
+    case optST,
     forall t1 t2,
     (* This additional restriction added to fix https://github.com/dfinity/candid/issues/146 *)
     (is_not_opt_like_type t1 <-> is_not_opt_like_type t2) -> 
     t1 <: t2 ->
     OptT t1 <: OptT t2
   | ConstituentOptST :
-    forall Case_ConstituentOptST : CaseName,
+    case constituentOptST,
     forall t1 t2,
     is_not_opt_like_type t2 ->
     t1 <: t2 -> t1 <: OptT t2
   | VoidST :
-    forall Case_VoidST : CaseName,
+    case voidST,
     forall t, VoidT <: t
   | ReservedST :
-    forall Case_ReservedST : CaseName,
+    case reservedST,
     forall t, t <: ReservedT
 where "t1 <: t2" := (Subtype t1 t2).
 
 Inductive HasType : V -> T -> Prop :=
   | NatHT:
-    forall Case_NatHT : CaseName,
+    case natHT,
     forall n, NatV n :: NatT
   | IntHT:
-    forall Case_IntHT : CaseName,
+    case intHT,
     forall n, IntV n :: IntT
   | NullHT:
-    forall Case_NullHT : CaseName,
+    case nullHT,
     NullV :: NullT
   | NullOptHT:
-    forall Case_NullOptHT : CaseName,
+    case nullOptHT,
     forall t, NullV :: OptT t
   | OptHT:
-    forall Case_OptHT : CaseName,
+    case optHT,
     forall v t, v :: t -> SomeV v :: OptT t
   | ReservedHT:
-    forall Case_ReservedHT : CaseName,
+    case reservedHT,
     ReservedV :: ReservedT
 where "v :: t" := (HasType v t).
 
@@ -103,31 +107,33 @@ Definition is_not_opt_like_value (v : V) : Prop :=
 Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity).
 Inductive Coerces : V -> V -> T -> Prop :=
   | NatC: 
-    forall Case_NatC : CaseName,
-    forall n, (NatV n ~> NatV n :: NatT)
+    case natC,
+    forall n, NatV n ~> NatV n :: NatT
   | IntC:
-    forall Case_IntC : CaseName,
-    forall n, (IntV n ~> IntV n :: IntT)
+    case intC,
+    forall n, IntV n ~> IntV n :: IntT
   | NatIntC:
-    forall Case_NatIntC : CaseName,
+    case natIntC,
     forall n i, i = Z.of_nat n -> (NatV n ~> IntV i :: IntT)
   | NullC:
-    forall Case_NullC : CaseName,
+    case nullC,
     NullV ~> NullV :: NullT
   | NullOptC:
-    forall Case_NullOptC : CaseName,
+    case nullOptC,
     forall t, NullV ~> NullV :: OptT t
   | SomeOptC:
-    forall Case_SomeOptC : CaseName,
-    forall v1 v2 t, v1 ~> v2 :: t -> SomeV v1 ~> SomeV v2 :: OptT t
+    case someOptC,
+    forall v1 v2 t,
+    v1 ~> v2 :: t ->
+    SomeV v1 ~> SomeV v2 :: OptT t
   | ConstituentOptC:
-    forall Case_ConstituentC : CaseName,
+    case constituentC,
     forall v1 v2 t,
     is_not_opt_like_value v1 ->
     v1 ~> v2 :: t ->
     v1 ~> SomeV v2 :: OptT t
   | ReservedC:
-    forall Case_ReservedC : CaseName,
+    case reservedC,
     forall v1,
     v1 ~> ReservedV :: ReservedT
 where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
@@ -173,29 +179,29 @@ Proof.
   induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
     name_cases;
     try (eexists;constructor; try constructor; fail).
-  [Case_NatHT_Case_ConstituentOptST]: {
+  [natHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
     - eexists. named_constructor; [constructor|named_constructor].
     - eexists. named_constructor; [constructor|named_constructor;reflexivity].
   }
-  [Case_IntHT_Case_ConstituentOptST]: {
+  [intHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
     econstructor. named_econstructor; [constructor|named_constructor].
   }
-  [Case_OptHT_Case_ReflSL]: {
+  [optHT_reflSL]: {
     specialize (IHHvT t (ReflST _ _)).
     destruct IHHvT as [v2 Hv2].
     eexists. named_econstructor; try eassumption.
   }
-  [Case_OptHT_Case_OptST]: {
+  [optHT_optST]: {
     specialize (IHHvT _ H1).
     destruct IHHvT as [v2 Hv2].
     eexists; named_econstructor; eassumption.
   }
-  [Case_OptHT_Case_ConstituentOptST]: {
+  [optHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
   }
-  [Case_ReservedHT_Case_ConstituentOptST]: {
+  [reservedHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
   }
 Qed.
@@ -216,28 +222,28 @@ Proof.
   inversion H2; subst; clear H2;
     name_cases;
     try (constructor; easy).
-  [Case_NatIntSL_Case_ConstituentOptST]: {
+  [natIntSL_constituentOptST]: {
     named_constructor.
     - assumption.
     - eapply Hyp; [named_econstructor | assumption].
   }
-  [Case_OptST_Case_OptST0]: {
+  [optST_optST0]: {
     named_constructor.
     - intuition.
     - eapply Hyp; eassumption.
   }
-  [Case_OptST_Case_ConstituentOptST]: {
+  [optST_constituentOptST]: {
     inversion H3; subst; clear H3; simpl in H0; contradiction.
   }
-  [Case_ConstituentOptST_Case_OptST]: {
+  [constituentOptST_optST]: {
     named_constructor.
     - intuition.
     - firstorder.
   }
-  [Case_ConstituentOptST_Case_ConstituentOptST0]: {
+  [constituentOptST_constituentOptST0]: {
     inversion H3; subst; clear H3; try easy.
   }
-  [Case_ReservedST_Case_ConstituentOptST]: {
+  [reservedST_constituentOptST]: {
     inversion H0; subst; clear H0; inversion H.
   }
-Qed.
\ No newline at end of file
+Qed.
diff --git a/coq/NamedCases.v b/coq/NamedCases.v
index d4c88c29..1e132fee 100644
--- a/coq/NamedCases.v
+++ b/coq/NamedCases.v
@@ -12,10 +12,8 @@ Existing Instance CaseNameI.
 Require Import Coq.Strings.String.
 Import StringSyntax.
 
-(*
-Require Import candid.StringToIdent.
-*)
 
+(* Horribly manual string manipulations *)
 Ltac2 strcpy := fun s1 s2 o =>
     let rec go := fun n =>
       match Int.lt n (String.length s2) with
@@ -29,6 +27,9 @@ Ltac2 concat := fun s1 s2 =>
     strcpy s s1 0;
     strcpy s s2 (Int.add (String.length s1) 1);
     s.
+
+(* Combines the names of hyptheses of type CaseName *)
+(* Writen in Ltac2 because I could not mangle identifier names in Ltac1 *)
 Ltac2 rec combine_case_names () :=
   repeat (lazy_match! goal with
   | [ h1 : CaseName, h2 : CaseName |- _ ] =>
@@ -40,6 +41,8 @@ Ltac2 rec combine_case_names () :=
   | [ |- _ ] => fail
   end).
 
+(* Removes all CaseName hypotheses, and renames the goal based on their names *)
+(* Writen in Ltac1 because I could not figure ou thow to use refine in Ltac2 *)
 Ltac name_cases := 
   [> (
     ltac2:(combine_case_names ());
@@ -48,23 +51,22 @@ Ltac name_cases :=
     | _ => idtac "Could not find a CaseName assumption"; fail
     end
   )..].
-  
-  
+
+(* To be used instead of constructor when the first assumption is 
+   one of those CaseName assumptions *)
 Ltac named_constructor :=
   constructor;[ apply CaseNameI | idtac .. ].
 Ltac named_econstructor :=
   econstructor;[ apply CaseNameI | idtac .. ].
 
-(* 
-Notation "''case'' x , t" := (forall x : CaseName, t)
-  (at level 10, x at level 1000, t at level 1000).
-*)
+Notation "'case' x , t" := (forall x : CaseName, t)
+  (at level 200).
 
 Section Example.
 
   Inductive Test :=
-    | Foo: forall foo : CaseName, Test
-    | Bar: forall bar : CaseName, Test.
+    | Foo: case foo, Test
+    | Bar: case bar, Test.
 
   Goal Test -> Test.
     intros.

From 1ee30446fa760d749c574ca1df6d6d3341dcee46 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 5 Dec 2020 18:06:05 +0100
Subject: [PATCH 16/25] A little bit of cleanup

---
 coq/NamedCases.v | 67 ++++++++++++++++++++++++++++--------------------
 1 file changed, 39 insertions(+), 28 deletions(-)

diff --git a/coq/NamedCases.v b/coq/NamedCases.v
index 1e132fee..9d480cec 100644
--- a/coq/NamedCases.v
+++ b/coq/NamedCases.v
@@ -13,44 +13,50 @@ Require Import Coq.Strings.String.
 Import StringSyntax.
 
 
-(* Horribly manual string manipulations *)
-Ltac2 strcpy := fun s1 s2 o =>
+Ltac2 name_cases () :=
+  (* Horribly manual string manipulations. Does this mean I should
+     go to the Ocaml level?
+  *)
+  let strcpy s1 s2 o :=
     let rec go := fun n =>
       match Int.lt n (String.length s2) with
       | true => String.set s1 (Int.add o n) (String.get s2 n); go (Int.add n 1)
       | false => ()
       end
-    in go 0.
-Ltac2 concat := fun s1 s2 => 
+    in go 0
+  in
+  let concat := fun s1 s2 => 
     let l := Int.add (Int.add (String.length s1) (String.length s2)) 1 in
     let s := String.make l (Char.of_int 95) in
     strcpy s s1 0;
     strcpy s s2 (Int.add (String.length s1) 1);
-    s.
-
-(* Combines the names of hyptheses of type CaseName *)
-(* Writen in Ltac2 because I could not mangle identifier names in Ltac1 *)
-Ltac2 rec combine_case_names () :=
-  repeat (lazy_match! goal with
-  | [ h1 : CaseName, h2 : CaseName |- _ ] =>
-    let h := concat (Ident.to_string h1) (Ident.to_string h2) in
-    (* Message.print (Message.of_string h); *)
-    let h := Option.get (Ident.of_string h) in
-    Std.clear [h1; h2];
-    assert ($h : CaseName) by apply CaseNameI
-  | [ |- _ ] => fail
-  end).
+    s
+  in
+  Control.enter (let rec go () :=
+    lazy_match! goal with
+    | [ h1 : CaseName, h2 : CaseName |- _ ] =>
+      (* Multiple case names? Combine them (and recurse) *)
+      let h := concat (Ident.to_string h1) (Ident.to_string h2) in
+      Std.clear [h1; h2];
+      let h := Option.get (Ident.of_string h) in
+      assert ($h := CaseNameI);
+      go ()
+    | [ _ : CaseName |- _ ] =>
+      (* A single case name? Set current goal name accordigly. *)
+      ltac1:(
+        (* How to do this in ltac2? *)
+        lazymatch goal with
+        | [ H : CaseName |- _ ] => refine ?[H]; clear H
+        end
+      )
+    | [ |- _ ] =>
+      Control.backtrack_tactic_failure "Did not find any CaseName hypotheses"
+    end
+  in go).
 
 (* Removes all CaseName hypotheses, and renames the goal based on their names *)
 (* Writen in Ltac1 because I could not figure ou thow to use refine in Ltac2 *)
-Ltac name_cases := 
-  [> (
-    ltac2:(combine_case_names ());
-    lazymatch goal with
-    | [ H : CaseName |- _ ] => refine ?[H]; clear H
-    | _ => idtac "Could not find a CaseName assumption"; fail
-    end
-  )..].
+Ltac name_cases := ltac2:(name_cases ()).
 
 (* To be used instead of constructor when the first assumption is 
    one of those CaseName assumptions *)
@@ -67,7 +73,7 @@ Section Example.
   Inductive Test :=
     | Foo: case foo, Test
     | Bar: case bar, Test.
-
+  
   Goal Test -> Test.
     intros.
     destruct H; name_cases.
@@ -82,6 +88,7 @@ Section Example.
   Goal Test -> Test -> Test.
     intros.
     destruct H; destruct H0; name_cases.
+    Show Existentials.
     [foo_foo0]: {
       named_constructor.
     }
@@ -100,7 +107,6 @@ Section Example.
   Goal Test -> Test -> Test -> Test.
     intros.
     destruct H; destruct H0; destruct H1; name_cases.
-    Show Existentials.
     [foo_foo0_bar]: {
       named_constructor.
     }
@@ -115,4 +121,9 @@ Section Example.
     * named_constructor.
   Qed.
 
+  Goal True.
+    (* The tactic fails if it does not find case names *)
+    Fail name_cases.
+  Abort.
+
 End Example.
\ No newline at end of file

From 5ffd78d479e69688306683e525c6fb7c8937cac5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 5 Dec 2020 21:11:08 +0100
Subject: [PATCH 17/25] Use NamedCases in IDLSoundness

---
 coq/IDLSoundness.v | 63 ++++++++++++++++++++++++++++++++--------------
 1 file changed, 44 insertions(+), 19 deletions(-)

diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v
index 11fa79be..c1d617be 100644
--- a/coq/IDLSoundness.v
+++ b/coq/IDLSoundness.v
@@ -17,6 +17,8 @@ Require Import Coq.Relations.Relation_Operators.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Relations.Operators_Properties.
 
+Require Import candid.NamedCases.
+
 Set Bullet Behavior "Strict Subproofs".
 
 Section IDL.
@@ -41,8 +43,8 @@ Section IDL.
   Variable evolves : S -> S -> Prop.
   Notation "s1 ~> s2" := (evolves s1 s2) (at level 70, no associativity).
 
-  Variable hostSubtyping : S -> S -> Prop.
-  Notation "s1 <<: s2" := (hostSubtyping s1 s2) (at level 70, no associativity).
+  Variable hostSubtypeOf : S -> S -> Prop.
+  Notation "s1 <<: s2" := (hostSubtypeOf s1 s2) (at level 70, no associativity).
 
   (* Service Identifiers *)
   Variable I : Set.
@@ -60,36 +62,45 @@ Section IDL.
     (forall i' s, ~ In st (HasRef i' i s)).
 
   Inductive CanSend : State -> I -> T -> T -> I -> Prop :=
-    | CanCall: forall st A B t1 t1' t2 t2',
+    | CanCall:
+      case canCall,
+      forall st A B t1 t1' t2 t2',
       In st (HasRef A B (t1 --> t1')) ->
       In st (HasType B (t2 --> t2')) ->
       CanSend st A t1 t2 B
-    | CanReply: forall st A B t1 t1' t2 t2',
+    | CanReply:
+      case canReply,
+      forall st A B t1 t1' t2 t2',
       In st (HasRef B A (t1 --> t1')) ->
       In st (HasType A (t2 --> t2')) ->
       CanSend st A t2' t1' B.
 
   Inductive step : State -> State -> Prop :=
     | NewService :
+      case newService,
       forall (i : I) (s : S) st,
       FreshIn i st ->
       step st (Add st (HasType i s))
     | EvolveService :
+      case evolveService,
       forall (i : I) (s1 s2 : S) st,
       ~ In st (HasType i s1) ->
       s1 ~> s2 ->
       step (Add st (HasType i s1)) (Add st (HasType i s2))
     | LearnService :
+      case learnService,
       forall (i1 i2 : I) (s: S) st,
       In st (HasType i1 s) ->
       step st (Add st (HasRef i2 i1 s))
     | TransmitService :
+      case transmitService,
       forall (A B C : I) (s1 s2 : S) (t1 t2 : T) st,
       In st (HasRef A C s1) ->
       CanSend st A t1 t2 B ->
       (s1 ∈ t1 <: s2 ∈ t2) ->
       step st (Add st (HasRef B C s2))
     | HostSubtyping :
+      case hostSubtyping,
       forall (A B : I) (s1 s2 : S) st,
       s1 <<: s2 ->
       step (Add st (HasRef A B s1)) (Add st (HasRef A B s2))
@@ -160,11 +171,15 @@ Section IDL.
   Proof.
     intros st Hinvariant.
     intros A t1 t2 B HCanSend.
-    destruct HCanSend.
-    * pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
+    destruct HCanSend; name_cases.
+    [canCall]: {
+      pose proof (Hinvariant B A (t2 --> t2') (t1 --> t1') H0 H) as H1.
       apply H1.
-    * pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
+    }
+    [canReply]: {
+      pose proof (Hinvariant A B (t2 --> t2') (t1 --> t1') H0 H) as H1.
       apply H1.
+    }
   Qed.
 
   Lemma invariant_Add_HasType:
@@ -290,8 +305,8 @@ Section IDL.
     forall st1 st2, step st1 st2 -> unique st1 -> unique st2.
   Proof.
     intros st1 st2 Hstep Huniq.
-    induction Hstep.
-    * (* NewService *)
+    induction Hstep; name_cases.
+    [newService]: {
       intros A' s1' s2' HType1 HType2.
       inversion HType1; subst; clear HType1;
       inversion HType2; subst; clear HType2.
@@ -303,7 +318,8 @@ Section IDL.
       - inversion H1; subst; clear H1;
         inversion H0; subst; clear H0.
         reflexivity.
-    * (* EvolveService *)
+    }
+    [evolveService]: {
       intros A' s1' s2' HType1 HType2.
       inversion HType1; subst; clear HType1;
       inversion HType2; subst; clear HType2.
@@ -325,35 +341,41 @@ Section IDL.
       - inversion H1; subst; clear H1;
         inversion H2; subst; clear H0.
         reflexivity.
-    * (* LearnService *)
+    }
+    [learnService]: {
       rewrite unique_Add_HasRef in *.
       assumption.
-    * (* TransmitService *)
+    }
+    [transmitService]: {
       rewrite unique_Add_HasRef in *.
       assumption.
-    * (* HostSubtyping *)
+    }
+    [hostSubtyping]: {
       rewrite unique_Add_HasRef in *.
       assumption.
+    }
   Qed.
 
   Lemma step_preserves_invariant:
     forall st1 st2, step st1 st2 -> unique st1 -> invariant st1 -> invariant st2.
   Proof.
     intros st1 st2 Hstep Huniq Hinv.
-    induction Hstep.
-    * (* NewService *)
+    induction Hstep; name_cases.
+    [newService]: {
       apply invariant_Add_HasType.
       - apply Hinv.
       - intros  B s2 HB.
         eapply H in HB.
         inversion HB.
-    * (* EvolveService *)
+    }
+    [evolveService]: {
       eapply invariant_Change_HasType.
       - apply Hinv.
       - intros B s3 HB Hsub.
         apply evolves_correctly in H0.
         eapply service_subtype_trans; eassumption.
-    * (* LearnService *)
+    }
+    [learnService]: {
       apply invariant_Add_HasRef.
       - apply Hinv.
       - intros s2 HHasType.
@@ -361,7 +383,8 @@ Section IDL.
         replace s2 with s.
         + apply service_subtype_refl.
         + eapply Huniq; eassumption.
-    * (* TransmitService *)
+    }
+    [transmitService]: {
       apply invariant_Add_HasRef.
       - apply Hinv.
       - intros s3 HC.
@@ -370,12 +393,14 @@ Section IDL.
         assert (t1 <: t2) by (eapply HSound; apply H0).
         assert (s1 <:: s2) by (eapply compositional;  eassumption).
         eapply service_subtype_trans; eassumption.
-    * (* HostSubtyping *)
+    }
+    [hostSubtyping]: {
       eapply invariant_Change_HasRef.
       - apply Hinv.
       - intros s3 HB Hsub.
         apply host_subtyping_sound in H.
         eapply service_subtype_trans; eassumption.
+    }
   Qed.
 
   Lemma canonical_soundness: IDLSound.

From db700e2ef5328fde5ffb3ce25c3c09a4aaf47aa0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 9 Dec 2020 16:30:37 +0100
Subject: [PATCH 18/25] Towards the opportunistic subtyping

---
 coq/MiniCandid.v | 253 +++++++++++++++++++++++++++++++++++++++--------
 coq/NamedCases.v | 181 +++++++++++++++++++++++++++++----
 2 files changed, 372 insertions(+), 62 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 09aece0d..23a90d0d 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -3,6 +3,7 @@ MiniCandid: A formalization of the core ideas of Candid
 *)
 
 Require Import Coq.ZArith.BinInt.
+Require Import Coq.Init.Datatypes.
 
 Require Import Coq.Relations.Relation_Operators.
 Require Import Coq.Relations.Relation_Definitions.
@@ -35,13 +36,51 @@ Inductive V :=
 
 (* This is a stand in for `~(null <: t)` in places
 where <: is not allowed yet. *)
-Definition is_not_opt_like_type (t : T) : Prop :=
+Definition is_opt_like_type (t : T) : bool :=
   match t with
-  | NullT => False
-  | OptT _ => False
-  | ReservedT => False
-  | _ => True
+  | NullT => true
+  | OptT _ => true
+  | ReservedT => true
+  | _ => false
   end.
+  
+Definition is_not_opt_like_value (v : V) : Prop :=
+match v with
+| NullV => False
+| SomeV _ => False
+| ReservedV => False
+| _ => True
+end.
+
+(* The boring, non-subtyping typing relation. *)
+Inductive HasType : V -> T -> Prop :=
+  | NatHT:
+    case natHT,
+    forall n, NatV n :: NatT
+  | IntHT:
+    case intHT,
+    forall n, IntV n :: IntT
+  | NullHT:
+    case nullHT,
+    NullV :: NullT
+  | NullOptHT:
+    case nullOptHT,
+    forall t, NullV :: OptT t
+  | OptHT:
+    case optHT,
+    forall v t, v :: t -> SomeV v :: OptT t
+  | ReservedHT:
+    case reservedHT,
+    ReservedV :: ReservedT
+where "v :: t" := (HasType v t).
+
+
+Module NoOpportunisticDecoding.
+
+(*
+This is the variant without `t <: opt t'`, where
+things can be simple and inductive.
+*)
 
 Reserved Infix "<:" (at level 80, no associativity).
 CoInductive Subtype : T -> T -> Prop :=
@@ -58,13 +97,13 @@ CoInductive Subtype : T -> T -> Prop :=
     case optST,
     forall t1 t2,
     (* This additional restriction added to fix https://github.com/dfinity/candid/issues/146 *)
-    (is_not_opt_like_type t1 <-> is_not_opt_like_type t2) -> 
+    (is_opt_like_type t1 = is_opt_like_type t2) -> 
     t1 <: t2 ->
     OptT t1 <: OptT t2
   | ConstituentOptST :
     case constituentOptST,
     forall t1 t2,
-    is_not_opt_like_type t2 ->
+    is_opt_like_type t2 = false ->
     t1 <: t2 -> t1 <: OptT t2
   | VoidST :
     case voidST,
@@ -74,34 +113,6 @@ CoInductive Subtype : T -> T -> Prop :=
     forall t, t <: ReservedT
 where "t1 <: t2" := (Subtype t1 t2).
 
-Inductive HasType : V -> T -> Prop :=
-  | NatHT:
-    case natHT,
-    forall n, NatV n :: NatT
-  | IntHT:
-    case intHT,
-    forall n, IntV n :: IntT
-  | NullHT:
-    case nullHT,
-    NullV :: NullT
-  | NullOptHT:
-    case nullOptHT,
-    forall t, NullV :: OptT t
-  | OptHT:
-    case optHT,
-    forall v t, v :: t -> SomeV v :: OptT t
-  | ReservedHT:
-    case reservedHT,
-    ReservedV :: ReservedT
-where "v :: t" := (HasType v t).
-
-Definition is_not_opt_like_value (v : V) : Prop :=
-  match v with
-  | NullV => False
-  | SomeV _ => False
-  | ReservedV => False
-  | _ => True
-  end.
 
 
 Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity).
@@ -143,10 +154,11 @@ where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
 *)
 Lemma is_not_opt_like_type_correct:
   forall t,
-  is_not_opt_like_type t <-> ~ (NullT <: t).
+  is_opt_like_type t = true <-> NullT <: t.
 Proof.
   intros. destruct t; simpl; intuition.
-  all: try inversion H0; (apply H; named_constructor).
+  all: try inversion H.
+  all: try named_constructor.
 Qed.
 
 Theorem coercion_correctness:
@@ -211,7 +223,7 @@ Proof. intros x. apply ReflST; constructor. Qed.
 
 Lemma is_not_opt_like_type_contravariant:
   forall t1 t2,
-     is_not_opt_like_type t1 -> t2 <: t1 -> is_not_opt_like_type t2.
+     is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false.
 Proof. intros. destruct t1, t2; easy. Qed.
 
 Theorem subtyping_trans: transitive _ Subtype.
@@ -229,15 +241,15 @@ Proof.
   }
   [optST_optST0]: {
     named_constructor.
-    - intuition.
+    - congruence.
     - eapply Hyp; eassumption.
   }
   [optST_constituentOptST]: {
-    inversion H3; subst; clear H3; simpl in H0; contradiction.
+    inversion H3; subst; clear H3; simpl in H1; congruence.
   }
   [constituentOptST_optST]: {
     named_constructor.
-    - intuition.
+    - congruence.
     - firstorder.
   }
   [constituentOptST_constituentOptST0]: {
@@ -247,3 +259,162 @@ Proof.
     inversion H0; subst; clear H0; inversion H.
   }
 Qed.
+
+End NoOpportunisticDecoding.
+
+
+Module OpportunisticDecoding.
+(*
+This is the variant with `t <: opt t'.
+*)
+
+Reserved Infix "<:" (at level 80, no associativity).
+CoInductive Subtype : T -> T -> Prop :=
+  | ReflST :
+    case reflSL,
+    forall t, t <: t
+  | NatIntST :
+    case natIntSL,
+    NatT <: IntT
+  | OptST :
+    case optST,
+    forall t1 t2,
+    t1 <: OptT t2
+  | VoidST :
+    case voidST,
+    forall t, VoidT <: t
+  | ReservedST :
+    case reservedST,
+    forall t, t <: ReservedT
+where "t1 <: t2" := (Subtype t1 t2).
+
+(*
+The coercion relation is not strictly positive, so we have to implement
+it as a function that recurses on the value. This is essentially
+coercion function, and we can separately try to prove that it corresponds
+to the relation.
+ *)
+
+
+Require Import FunInd.
+Function coerce (n : nat) (v1 : V) (t : T) : option V :=
+  match n with  | 0 => None (* out of fuel *) | S n => 
+    match v1, t with
+    | NatV n, NatT => Some (NatV n)
+    | IntV n, IntT => Some (IntV n)
+    | NatV n, IntT => Some (IntV (Z.of_nat n))
+    | NullV, NullT => Some NullV
+    | NullV, OptT t => Some NullV
+    | SomeV v, OptT t => option_map SomeV (coerce n v t)
+    | ReservedV, OptT t => Some NullV
+    | v, OptT t =>
+      if is_opt_like_type t
+      then None
+      else option_map SomeV (coerce n v t)
+    | v, ReservedT => Some ReservedV
+    | v, t => None
+    end
+  end.
+  
+Definition Coerces (v1 v2 : V) (t : T) : Prop :=
+  exists n, coerce n v1 t = Some v2.
+Notation "v1 ~> v2 :: t" := (Coerces v1 v2 t) (at level 80, v2 at level 50, no associativity).
+
+(* TODO: derive intro and elim rules *)
+
+(* The is_not_opt_like_type definition is only introduced because
+   Coq (and not only coq) does not like hyptheses like ~(null <: t)
+*)
+Lemma is_not_opt_like_type_correct:
+  forall t,
+  is_opt_like_type t = true <-> NullT <: t.
+Proof.
+  intros. destruct t; simpl; intuition.
+  all: try inversion H.
+  all: try named_constructor.
+Qed.
+
+Theorem coercion_correctness:
+  forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
+Proof.
+  intros.
+  inversion H as [n Hcoerce]; clear H.
+  revert v1 v2 t Hcoerce.
+  induction n; intros v1 v2 t Hcoerce;
+    functional inversion Hcoerce; subst;
+    try (named_constructor; fail).
+  * destruct (coerce n v t1) eqn:Heq; simpl in H0; inversion H0; subst; clear H0.
+    specialize (IHn _ _ _ Heq).
+    named_constructor; assumption. 
+  * destruct (coerce n v1 t1) eqn:Heq; simpl in H0; inversion H0; subst; clear H0.
+    specialize (IHn _ _ _ Heq).
+    named_constructor; assumption. 
+Qed.
+
+Theorem coercion_roundtrip:
+  forall v t, v :: t -> v ~> v :: t.
+Proof.
+  intros. induction H; 
+    try (exists 1; reflexivity).
+  * destruct IHHasType as [n Hcoerce].
+    exists (S n). simpl. rewrite Hcoerce. reflexivity.
+Qed.
+
+Theorem coercion_uniqueness:
+  forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2.
+Proof.
+  intros.
+  revert v2 H0.
+  induction H; intros v2' Hother;
+    try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence).
+  * destruct Hother as [n Hother].
+    admit.
+Admitted.
+
+Theorem soundness_of_subtyping:
+  forall t1 t2,
+  t1 <: t2 ->
+  forall v1, v1 :: t1 -> exists v2, v1 ~> v2 :: t2.
+Proof.
+  intros t1 t2 Hsub v HvT. revert t2 Hsub.
+  induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
+    name_cases;
+    try (eexists;constructor; try constructor; fail).
+  [natHT_optST]: {
+    admit.
+  }
+  [intHT_optST]: {
+    admit.
+  }
+  [optHT_reflSL]: {
+    specialize (IHHvT t (ReflST _ _)).
+    destruct IHHvT as [v2 Hv2].
+    eexists. named_econstructor; try eassumption.
+  }
+  [optHT_optST]: {
+    admit.
+  }
+  [reservedHT_optST]: {
+    admit.
+  }
+Admitted.
+
+Theorem subtyping_refl: reflexive _ Subtype.
+Proof. intros x. apply ReflST; constructor. Qed.
+
+Lemma is_not_opt_like_type_contravariant:
+  forall t1 t2,
+     is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false.
+Proof. intros. destruct t1, t2; easy. Qed.
+
+Theorem subtyping_trans: transitive _ Subtype.
+Proof.
+  cofix Hyp.
+  intros t1 t2 t3 H1 H2.
+  inversion H1; subst; clear H1;
+  inversion H2; subst; clear H2;
+    name_cases;
+    try (constructor; easy).
+Qed.
+
+End OpportunisticDecoding.
\ No newline at end of file
diff --git a/coq/NamedCases.v b/coq/NamedCases.v
index 9d480cec..fa706bac 100644
--- a/coq/NamedCases.v
+++ b/coq/NamedCases.v
@@ -1,19 +1,14 @@
 (** Fun stuff trying to emulate Isar-style case names *)
 
-From Ltac2 Require Import Ltac2.
-From Ltac2 Require Option.
-Set Default Proof Mode "Classic".
-
 Inductive CaseName := CaseNameI.
 
 Existing Class CaseName.
 Existing Instance CaseNameI.
 
-Require Import Coq.Strings.String.
-Import StringSyntax.
-
-
-Ltac2 name_cases () :=
+From Ltac2 Require Import Ltac2.
+From Ltac2 Require Option.
+Set Default Proof Mode "Classic".
+Ltac name_cases := ltac2:(
   (* Horribly manual string manipulations. Does this mean I should
      go to the Ocaml level?
   *)
@@ -52,21 +47,16 @@ Ltac2 name_cases () :=
     | [ |- _ ] =>
       Control.backtrack_tactic_failure "Did not find any CaseName hypotheses"
     end
-  in go).
-
-(* Removes all CaseName hypotheses, and renames the goal based on their names *)
-(* Writen in Ltac1 because I could not figure ou thow to use refine in Ltac2 *)
-Ltac name_cases := ltac2:(name_cases ()).
+  in go)
+).
 
 (* To be used instead of constructor when the first assumption is 
    one of those CaseName assumptions *)
-Ltac named_constructor :=
-  constructor;[ apply CaseNameI | idtac .. ].
-Ltac named_econstructor :=
-  econstructor;[ apply CaseNameI | idtac .. ].
+Ltac clear_names := try exact CaseNameI.
+Ltac named_constructor  := constructor; [ exact CaseNameI | idtac .. ].
+Ltac named_econstructor := econstructor; [ exact CaseNameI | idtac .. ].
 
-Notation "'case' x , t" := (forall x : CaseName, t)
-  (at level 200).
+Notation "'case' x , t" := (forall {x : CaseName}, t) (at level 200).
 
 Section Example.
 
@@ -126,4 +116,153 @@ Section Example.
     Fail name_cases.
   Abort.
 
-End Example.
\ No newline at end of file
+End Example.
+
+Require Import Coq.Lists.List.
+Section Example2.
+  (* From https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html *)
+
+ Import ListNotations.
+
+ Inductive reg_exp (T : Type) : Type :=
+  | EmptySet
+  | EmptyStr
+  | Char (t : T)
+  | App (r1 r2 : reg_exp T)
+  | Union (r1 r2 : reg_exp T)
+  | Star (r : reg_exp T).
+  Arguments EmptySet {T}.
+  Arguments EmptyStr {T}.
+  Arguments Char {T} _.
+  Arguments App {T} _ _.
+  Arguments Union {T} _ _.
+  Arguments Star {T} _.
+ 
+  Reserved Notation "s =~ re" (at level 80).
+  Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
+    | MEmpty:
+      case empty,
+      [] =~ EmptyStr
+    | MChar:
+      case char,
+      forall x,
+      [x] =~ (Char x)
+    | MApp:
+      case app,
+      forall s1 re1 s2 re2
+      (H1 : s1 =~ re1)
+      (H2 : s2 =~ re2),
+      (s1 ++ s2) =~ (App re1 re2)
+    | MUnionL:
+      case unionL,
+      forall s1 re1 re2
+      (H1 : s1 =~ re1),
+      s1 =~ (Union re1 re2)
+    | MUnionR:
+      case unionR,
+      forall re1 s2 re2
+      (H2 : s2 =~ re2),
+      s2 =~ (Union re1 re2)
+    | MStar0:
+      case star0,
+      forall re,
+      [] =~ (Star re)
+    | MStarApp:
+      case starApp,
+      forall s1 s2 re
+      (H1 : s1 =~ re)
+      (H2 : s2 =~ (Star re)),
+      (s1 ++ s2) =~ (Star re)
+    where "s =~ re" := (exp_match s re).
+  
+  Lemma star_app0: forall T (s1 s2 : list T) (re : reg_exp T),
+    s1 =~ Star re ->
+    s2 =~ Star re ->
+    s1 ++ s2 =~ Star re.
+  Proof.
+    intros T s1 s2 re H1.
+    remember (Star re) as re'.
+     generalize dependent s2.
+    induction H1.
+    - (* MEmpty *) discriminate.
+    - (* MChar *) discriminate.
+    - (* MApp *) discriminate.
+    - (* MUnionL *) discriminate.
+    - (* MUnionR *) discriminate.
+    - (* MStar0 *)
+      injection Heqre' as Heqre''. intros s H. apply H.
+    - (* MStarApp *)
+      injection Heqre' as Heqre''.
+      intros s3 H1. rewrite <- app_assoc.
+      apply MStarApp.
+      + trivial.
+      + apply H1_.
+      + apply IHexp_match2.
+        * rewrite Heqre''. reflexivity.
+        * apply H1.
+  Qed.
+
+  Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
+    s1 =~ Star re ->
+    s2 =~ Star re ->
+    s1 ++ s2 =~ Star re.
+  Proof.
+    intros T s1 s2 re H1.
+    remember (Star re) as re'.
+     generalize dependent s2.
+    induction H1; name_cases; try discriminate.
+    [starApp]: {
+      injection Heqre' as Heqre''.
+      intros s3 H1. rewrite <- app_assoc.
+      apply MStarApp; clear_names.
+      + apply H1_.
+      + apply IHexp_match2.
+        * rewrite Heqre''. reflexivity.
+        * apply H1.
+     }
+    [star0]: {
+      injection Heqre' as Heqre''. intros s H. apply H.
+    }
+  Qed.
+  
+  Inductive Palindrome {T} : list T -> Prop :=
+  | EmptyPalin:
+    case emptyP,
+    Palindrome []
+  | SingletonPalin:
+    case singletonP,
+    forall x,
+    Palindrome [x]
+  | GrowPalin:
+    case growP,
+    forall l x,
+    Palindrome l -> Palindrome ([x] ++ l ++ [x])
+  .
+  
+  Lemma palindrome_star_of_two:
+    forall T (s : list T) a b,
+    Palindrome s -> s =~ Star (App (Char a) (Char b)) ->
+    s = [] \/ a = b.
+  Proof.
+    intros T s x y  HPalin HRe.
+    induction HPalin; inversion HRe; name_cases.
+    Show Existentials.
+    [emptyP_star0]: {
+      left. reflexivity.
+    }
+    [emptyP_starApp]: {
+       left. reflexivity.
+    }
+    [singletonP_starApp]: {
+      inversion HRe; clear HRe.
+      inversion H5; clear H5.
+      inversion H10; clear H10.
+      inversion H11; clear H11.
+      subst.
+      inversion H3.
+    }
+    [growP_starApp]: {
+      admit.
+    }
+  Admitted.
+End Example2.   

From e8f24eed54ce9da11f24dc102af667b2fe46ba6f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 10 Dec 2020 01:12:33 +0100
Subject: [PATCH 19/25] Conclude the proof for opportunistic decoding

---
 coq/MiniCandid.v | 110 +++++++++++++++++++++++++----------------------
 1 file changed, 58 insertions(+), 52 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 23a90d0d..3f718a9e 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -262,6 +262,7 @@ Qed.
 
 End NoOpportunisticDecoding.
 
+Require Import FunInd.
 
 Module OpportunisticDecoding.
 (*
@@ -295,29 +296,38 @@ coercion function, and we can separately try to prove that it corresponds
 to the relation.
  *)
 
-
-Require Import FunInd.
-Function coerce (n : nat) (v1 : V) (t : T) : option V :=
-  match n with  | 0 => None (* out of fuel *) | S n => 
-    match v1, t with
-    | NatV n, NatT => Some (NatV n)
-    | IntV n, IntT => Some (IntV n)
-    | NatV n, IntT => Some (IntV (Z.of_nat n))
-    | NullV, NullT => Some NullV
-    | NullV, OptT t => Some NullV
-    | SomeV v, OptT t => option_map SomeV (coerce n v t)
-    | ReservedV, OptT t => Some NullV
-    | v, OptT t =>
-      if is_opt_like_type t
-      then None
-      else option_map SomeV (coerce n v t)
-    | v, ReservedT => Some ReservedV
-    | v, t => None
-    end
+Definition recover x := match x with
+  | None => Some NullV
+  | Some x => Some (SomeV x)
+ end.
+
+Function coerce (v1 : V) (t : T) : option V :=
+  match v1, t with
+  | NatV n, NatT => Some (NatV n)
+  | IntV n, IntT => Some (IntV n)
+  | NatV n, IntT => Some (IntV (Z.of_nat n))
+  | NullV, NullT => Some NullV
+  | SomeV v, OptT t => recover (coerce v t)
+  
+  (* This is the rule we would like to have, but 
+     in order to please the termination checker,
+     we have to duplicate all non-opt rules as opt-rules
+  | v, OptT t =>
+    if is_opt_like_type t
+    then None
+    else option_map SomeV (coerce n v t)
+  *)
+  | NatV n, OptT NatT => recover (Some (NatV n))
+  | IntV n, OptT IntT => recover (Some (IntV n))
+  | NatV n, OptT IntT => recover (Some (IntV (Z.of_nat n)))
+  (* OptT never fails (this subsumes NullV and ReservedV) *)
+  | v, OptT _ => Some NullV
+
+  | v, ReservedT => Some ReservedV
+  | v, t => None
   end.
   
-Definition Coerces (v1 v2 : V) (t : T) : Prop :=
-  exists n, coerce n v1 t = Some v2.
+Definition Coerces (v1 v2 : V) (t : T) : Prop := coerce v1 t = Some v2.
 Notation "v1 ~> v2 :: t" := (Coerces v1 v2 t) (at level 80, v2 at level 50, no associativity).
 
 (* TODO: derive intro and elim rules *)
@@ -338,38 +348,34 @@ Theorem coercion_correctness:
   forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
 Proof.
   intros.
-  inversion H as [n Hcoerce]; clear H.
-  revert v1 v2 t Hcoerce.
-  induction n; intros v1 v2 t Hcoerce;
-    functional inversion Hcoerce; subst;
-    try (named_constructor; fail).
-  * destruct (coerce n v t1) eqn:Heq; simpl in H0; inversion H0; subst; clear H0.
-    specialize (IHn _ _ _ Heq).
-    named_constructor; assumption. 
-  * destruct (coerce n v1 t1) eqn:Heq; simpl in H0; inversion H0; subst; clear H0.
-    specialize (IHn _ _ _ Heq).
-    named_constructor; assumption. 
+  revert v2 t H.
+  induction v1;
+  intros v2 t Hcoerce;
+    unfold Coerces in Hcoerce;
+    functional inversion Hcoerce; simpl in *; subst; clear Hcoerce;
+    try (named_constructor; named_constructor; fail).
+  * destruct (coerce v1 t1) eqn:Heq; simpl in *; inversion H0; subst; clear H0.
+    - specialize (IHv1 _ _ Heq).
+      named_constructor; assumption. 
+    - named_constructor.
 Qed.
 
 Theorem coercion_roundtrip:
   forall v t, v :: t -> v ~> v :: t.
 Proof.
-  intros. induction H; 
-    try (exists 1; reflexivity).
-  * destruct IHHasType as [n Hcoerce].
-    exists (S n). simpl. rewrite Hcoerce. reflexivity.
+  intros.
+  induction H; try reflexivity.
+  * unfold Coerces in *. simpl. rewrite IHHasType. reflexivity.
 Qed.
 
 Theorem coercion_uniqueness:
   forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2.
 Proof.
-  intros.
-  revert v2 H0.
-  induction H; intros v2' Hother;
-    try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence).
-  * destruct Hother as [n Hother].
-    admit.
-Admitted.
+  intro v.
+  induction v; intros v1 v2 t Heq1 Heq;
+    unfold Coerces in *;
+    congruence.
+Qed.
 
 Theorem soundness_of_subtyping:
   forall t1 t2,
@@ -379,25 +385,25 @@ Proof.
   intros t1 t2 Hsub v HvT. revert t2 Hsub.
   induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub;
     name_cases;
-    try (eexists;constructor; try constructor; fail).
+    try (eexists;reflexivity).
+  Show Existentials.
   [natHT_optST]: {
-    admit.
+    destruct t2; eexists; reflexivity.
   }
   [intHT_optST]: {
-    admit.
+    destruct t2; eexists; reflexivity.
   }
   [optHT_reflSL]: {
     specialize (IHHvT t (ReflST _ _)).
     destruct IHHvT as [v2 Hv2].
-    eexists. named_econstructor; try eassumption.
+    eexists. unfold Coerces in *. simpl. rewrite Hv2. reflexivity.
   }
   [optHT_optST]: {
-    admit.
-  }
-  [reservedHT_optST]: {
-    admit.
+    (* specialize (IHHvT t2 (ReflST _ _)).*)
+    unfold Coerces. simpl.
+    destruct (coerce v t2) eqn:Heq; eexists; reflexivity.
   }
-Admitted.
+Qed.
 
 Theorem subtyping_refl: reflexive _ Subtype.
 Proof. intros x. apply ReflST; constructor. Qed.

From 9c8d3fd03deff7a8f8419372bbccf35d66c38153 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 11 Dec 2020 11:20:37 +0100
Subject: [PATCH 20/25] Move NamedCasesDemo into own file

---
 coq/NamedCases.v     | 149 --------------------------------
 coq/NamedCasesDemo.v | 201 +++++++++++++++++++++++++++++++++++++++++++
 coq/dune             |   2 +-
 3 files changed, 202 insertions(+), 150 deletions(-)
 create mode 100644 coq/NamedCasesDemo.v

diff --git a/coq/NamedCases.v b/coq/NamedCases.v
index fa706bac..685ad714 100644
--- a/coq/NamedCases.v
+++ b/coq/NamedCases.v
@@ -117,152 +117,3 @@ Section Example.
   Abort.
 
 End Example.
-
-Require Import Coq.Lists.List.
-Section Example2.
-  (* From https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html *)
-
- Import ListNotations.
-
- Inductive reg_exp (T : Type) : Type :=
-  | EmptySet
-  | EmptyStr
-  | Char (t : T)
-  | App (r1 r2 : reg_exp T)
-  | Union (r1 r2 : reg_exp T)
-  | Star (r : reg_exp T).
-  Arguments EmptySet {T}.
-  Arguments EmptyStr {T}.
-  Arguments Char {T} _.
-  Arguments App {T} _ _.
-  Arguments Union {T} _ _.
-  Arguments Star {T} _.
- 
-  Reserved Notation "s =~ re" (at level 80).
-  Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
-    | MEmpty:
-      case empty,
-      [] =~ EmptyStr
-    | MChar:
-      case char,
-      forall x,
-      [x] =~ (Char x)
-    | MApp:
-      case app,
-      forall s1 re1 s2 re2
-      (H1 : s1 =~ re1)
-      (H2 : s2 =~ re2),
-      (s1 ++ s2) =~ (App re1 re2)
-    | MUnionL:
-      case unionL,
-      forall s1 re1 re2
-      (H1 : s1 =~ re1),
-      s1 =~ (Union re1 re2)
-    | MUnionR:
-      case unionR,
-      forall re1 s2 re2
-      (H2 : s2 =~ re2),
-      s2 =~ (Union re1 re2)
-    | MStar0:
-      case star0,
-      forall re,
-      [] =~ (Star re)
-    | MStarApp:
-      case starApp,
-      forall s1 s2 re
-      (H1 : s1 =~ re)
-      (H2 : s2 =~ (Star re)),
-      (s1 ++ s2) =~ (Star re)
-    where "s =~ re" := (exp_match s re).
-  
-  Lemma star_app0: forall T (s1 s2 : list T) (re : reg_exp T),
-    s1 =~ Star re ->
-    s2 =~ Star re ->
-    s1 ++ s2 =~ Star re.
-  Proof.
-    intros T s1 s2 re H1.
-    remember (Star re) as re'.
-     generalize dependent s2.
-    induction H1.
-    - (* MEmpty *) discriminate.
-    - (* MChar *) discriminate.
-    - (* MApp *) discriminate.
-    - (* MUnionL *) discriminate.
-    - (* MUnionR *) discriminate.
-    - (* MStar0 *)
-      injection Heqre' as Heqre''. intros s H. apply H.
-    - (* MStarApp *)
-      injection Heqre' as Heqre''.
-      intros s3 H1. rewrite <- app_assoc.
-      apply MStarApp.
-      + trivial.
-      + apply H1_.
-      + apply IHexp_match2.
-        * rewrite Heqre''. reflexivity.
-        * apply H1.
-  Qed.
-
-  Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
-    s1 =~ Star re ->
-    s2 =~ Star re ->
-    s1 ++ s2 =~ Star re.
-  Proof.
-    intros T s1 s2 re H1.
-    remember (Star re) as re'.
-     generalize dependent s2.
-    induction H1; name_cases; try discriminate.
-    [starApp]: {
-      injection Heqre' as Heqre''.
-      intros s3 H1. rewrite <- app_assoc.
-      apply MStarApp; clear_names.
-      + apply H1_.
-      + apply IHexp_match2.
-        * rewrite Heqre''. reflexivity.
-        * apply H1.
-     }
-    [star0]: {
-      injection Heqre' as Heqre''. intros s H. apply H.
-    }
-  Qed.
-  
-  Inductive Palindrome {T} : list T -> Prop :=
-  | EmptyPalin:
-    case emptyP,
-    Palindrome []
-  | SingletonPalin:
-    case singletonP,
-    forall x,
-    Palindrome [x]
-  | GrowPalin:
-    case growP,
-    forall l x,
-    Palindrome l -> Palindrome ([x] ++ l ++ [x])
-  .
-  
-  Lemma palindrome_star_of_two:
-    forall T (s : list T) a b,
-    Palindrome s -> s =~ Star (App (Char a) (Char b)) ->
-    s = [] \/ a = b.
-  Proof.
-    intros T s x y  HPalin HRe.
-    induction HPalin; inversion HRe; name_cases.
-    Show Existentials.
-    [emptyP_star0]: {
-      left. reflexivity.
-    }
-    [emptyP_starApp]: {
-       left. reflexivity.
-    }
-    [singletonP_starApp]: {
-      inversion HRe; clear HRe.
-      inversion H5; clear H5.
-      inversion H10; clear H10.
-      inversion H11; clear H11.
-      subst.
-      inversion H3.
-    }
-    [growP_starApp]: {
-      admit.
-    }
-  Admitted.
-End Example2.   
diff --git a/coq/NamedCasesDemo.v b/coq/NamedCasesDemo.v
new file mode 100644
index 00000000..6f0faf20
--- /dev/null
+++ b/coq/NamedCasesDemo.v
@@ -0,0 +1,201 @@
+(*
+A demo of the NamedCases machinery.
+
+This builds on an example from
+https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html
+and is also explained in
+https://www.joachim-breitner.de/blog/777-Named_goals_in_Coq
+*)
+
+Require Import candid.NamedCases.
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+Inductive reg_exp (T : Type) : Type :=
+| EmptySet
+| EmptyStr
+| Char (t : T)
+| App (r1 r2 : reg_exp T)
+| Union (r1 r2 : reg_exp T)
+| Star (r : reg_exp T).
+Arguments EmptySet {T}.
+Arguments EmptyStr {T}.
+Arguments Char {T} _.
+Arguments App {T} _ _.
+Arguments Union {T} _ _.
+Arguments Star {T} _.
+
+Reserved Notation "s =~ re" (at level 80).
+Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
+  | MEmpty:
+    case empty,
+    [] =~ EmptyStr
+  | MChar:
+    case char,
+    forall x,
+    [x] =~ (Char x)
+  | MApp:
+    case app,
+    forall s1 re1 s2 re2
+    (H1 : s1 =~ re1)
+    (H2 : s2 =~ re2),
+    (s1 ++ s2) =~ (App re1 re2)
+  | MUnionL:
+    case unionL,
+    forall s1 re1 re2
+    (H1 : s1 =~ re1),
+    s1 =~ (Union re1 re2)
+  | MUnionR:
+    case unionR,
+    forall re1 s2 re2
+    (H2 : s2 =~ re2),
+    s2 =~ (Union re1 re2)
+  | MStar0:
+    case star0,
+    forall re,
+    [] =~ (Star re)
+  | MStarApp:
+    case starApp,
+    forall s1 s2 re
+    (H1 : s1 =~ re)
+    (H2 : s2 =~ (Star re)),
+    (s1 ++ s2) =~ (Star re)
+  where "s =~ re" := (exp_match s re).
+
+Lemma star_app0: forall T (s1 s2 : list T) (re : reg_exp T),
+  s1 =~ Star re ->
+  s2 =~ Star re ->
+  s1 ++ s2 =~ Star re.
+Proof.
+  intros T s1 s2 re H1.
+  remember (Star re) as re'.
+   generalize dependent s2.
+  induction H1.
+  - (* MEmpty *) discriminate.
+  - (* MChar *) discriminate.
+  - (* MApp *) discriminate.
+  - (* MUnionL *) discriminate.
+  - (* MUnionR *) discriminate.
+  - (* MStar0 *)
+    injection Heqre' as Heqre''. intros s H. apply H.
+  - (* MStarApp *)
+    injection Heqre' as Heqre''.
+    intros s3 H1. rewrite <- app_assoc.
+    apply MStarApp.
+    + trivial.
+    + apply H1_.
+    + apply IHexp_match2.
+      * rewrite Heqre''. reflexivity.
+      * apply H1.
+Qed.
+
+Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
+  s1 =~ Star re ->
+  s2 =~ Star re ->
+  s1 ++ s2 =~ Star re.
+Proof.
+  intros T s1 s2 re H1.
+  remember (Star re) as re'.
+   generalize dependent s2.
+  induction H1; name_cases; try discriminate.
+  [starApp]: {
+    injection Heqre' as Heqre''.
+    intros s3 H1. rewrite <- app_assoc.
+    apply MStarApp; clear_names.
+    + apply H1_.
+    + apply IHexp_match2.
+      * rewrite Heqre''. reflexivity.
+      * apply H1.
+   }
+  [star0]: {
+    injection Heqre' as Heqre''. intros s H. apply H.
+  }
+Qed.
+
+Inductive Palindrome {T} : list T -> Prop :=
+| EmptyPalin:
+  case emptyP,
+  Palindrome []
+| SingletonPalin:
+  case singletonP,
+  forall x,
+  Palindrome [x]
+| GrowPalin:
+  case growP,
+  forall l x,
+  Palindrome l -> Palindrome ([x] ++ l ++ [x])
+.
+
+Lemma snoc_app_right:
+  forall T (s : list T) re,
+  s =~ Star re ->
+  s = [] \/ (exists s1 s2, s = s1 ++ s2 /\ s1 =~ Star re /\ s2 =~ re).
+Proof.
+  intros T s re H.
+  remember (Star re) as re'.
+  rewrite Heqre'.
+  revert re Heqre'.
+  induction H;
+    intros re' Heq;
+    inversion Heq; subst; clear Heq;
+    name_cases;
+    try (left; reflexivity).
+  [starApp]: {
+    clear IHexp_match1.
+    specialize (IHexp_match2 re' eq_refl).
+    destruct IHexp_match2.
+    - subst.
+      right.
+      exists []. eexists s1.
+      repeat split; try assumption.
+      rewrite app_nil_r. reflexivity.
+    - right.
+      inversion H1 as [s3 [s4 [He1 [Hre1 Hre2]]]]; subst; clear H1.
+      exists (s1 ++ s3). exists s4.
+      repeat split; try assumption.
+      + rewrite app_assoc. reflexivity.
+      + named_constructor; assumption.
+   }
+Qed.
+
+Lemma app_char_char:
+  forall T (x y : T) s,
+  s =~ App (Char x) (Char y) -> s = [x;y].
+Proof.
+  intros.
+  inversion H; subst; clear H.
+  inversion H3; subst; clear H3;
+  inversion H4; subst; clear H4;
+  reflexivity.
+Qed.
+
+Lemma palindrome_star_of_two:
+  forall T (s : list T) a b,
+  Palindrome s -> s =~ Star (App (Char a) (Char b)) ->
+  s = [] \/ a = b.
+Proof.
+  intros T s x y  HPalin HRe.
+  inversion HPalin; inversion HRe; subst; clear HRe; name_cases;
+    try intuition congruence.
+  [singletonP_starApp]: {
+    apply app_char_char in H2; subst.
+    inversion H0.
+  }
+  [growP_starApp]: {
+    right.
+    apply app_char_char in H2; subst.
+    eapply snoc_app_right in H4.
+    inversion H4; subst; clear H4.
+    * rewrite app_nil_r in H3. destruct l; inversion H3; subst; try reflexivity.
+      symmetry in H4.
+      apply app_eq_nil in H4.
+      intuition congruence.
+    * inversion H0 as [s3 [s4 [He1 [Hre1 Hre2]]]]; subst; clear H0.
+      apply app_char_char in Hre2; subst.
+      simpl in H3.
+      inversion H3; subst; clear H3.
+      apply (f_equal (@rev T)) in H2; simpl in *.
+      repeat rewrite ! rev_app_distr in H2; simpl in *.
+      congruence.
+  }
+Qed.
\ No newline at end of file
diff --git a/coq/dune b/coq/dune
index 58a8bbb6..98d3331c 100644
--- a/coq/dune
+++ b/coq/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name "candid")
  (synopsis "Coq for candid")
- (modules IDLSoundness MiniCandid NamedCases)
+ (modules IDLSoundness MiniCandid NamedCases NamedCasesDemo)
 )

From 72cb55c9d1c06b2085ea0dfe7fb48f4dab4243b8 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 11 Dec 2020 17:27:21 +0100
Subject: [PATCH 21/25] Wrap up the proofs

---
 coq/MiniCandid.v | 168 ++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 144 insertions(+), 24 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 3f718a9e..b23d2bc9 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -2,6 +2,8 @@
 MiniCandid: A formalization of the core ideas of Candid
 *)
 
+Require Import FunInd.
+
 Require Import Coq.ZArith.BinInt.
 Require Import Coq.Init.Datatypes.
 
@@ -34,8 +36,7 @@ Inductive V :=
   | ReservedV : V
   .
 
-(* This is a stand in for `~(null <: t)` in places
-where <: is not allowed yet. *)
+(* This is a stand in for `null <: t` in places where <: is not allowed yet. *)
 Definition is_opt_like_type (t : T) : bool :=
   match t with
   | NullT => true
@@ -43,7 +44,8 @@ Definition is_opt_like_type (t : T) : bool :=
   | ReservedT => true
   | _ => false
   end.
-  
+
+
 Definition is_not_opt_like_value (v : V) : Prop :=
 match v with
 | NullV => False
@@ -78,8 +80,8 @@ where "v :: t" := (HasType v t).
 Module NoOpportunisticDecoding.
 
 (*
-This is the variant without `t <: opt t'`, where
-things can be simple and inductive.
+This is the variant without `t <: opt t'`, but with `t <: opt t`.
+Here things are simple and inductive.
 *)
 
 Reserved Infix "<:" (at level 80, no associativity).
@@ -114,7 +116,6 @@ CoInductive Subtype : T -> T -> Prop :=
 where "t1 <: t2" := (Subtype t1 t2).
 
 
-
 Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity).
 Inductive Coerces : V -> V -> T -> Prop :=
   | NatC: 
@@ -149,10 +150,7 @@ Inductive Coerces : V -> V -> T -> Prop :=
     v1 ~> ReservedV :: ReservedT
 where "v1 ~> v2 :: t" := (Coerces v1 v2 t).
 
-(* The is_not_opt_like_type definition is only introduced because
-   Coq (and not only coq) does not like hyptheses like ~(null <: t)
-*)
-Lemma is_not_opt_like_type_correct:
+Lemma is_opt_like_type_correct:
   forall t,
   is_opt_like_type t = true <-> NullT <: t.
 Proof.
@@ -262,11 +260,9 @@ Qed.
 
 End NoOpportunisticDecoding.
 
-Require Import FunInd.
-
 Module OpportunisticDecoding.
 (*
-This is the variant with `t <: opt t'.
+This is the variant with the opportunistic `t <: opt t'` rule.
 *)
 
 Reserved Infix "<:" (at level 80, no associativity).
@@ -290,10 +286,11 @@ CoInductive Subtype : T -> T -> Prop :=
 where "t1 <: t2" := (Subtype t1 t2).
 
 (*
-The coercion relation is not strictly positive, so we have to implement
-it as a function that recurses on the value. This is essentially
-coercion function, and we can separately try to prove that it corresponds
-to the relation.
+The coercion relation is not strictly positive, and thus can’t be an inductive
+relations, so we have to implement it as a function that recurses on the value.
+
+This is essentially coercion function, and we can separately try to prove that
+it corresponds to the relation.
  *)
 
 Definition recover x := match x with
@@ -311,7 +308,7 @@ Function coerce (v1 : V) (t : T) : option V :=
   
   (* This is the rule we would like to have, but 
      in order to please the termination checker,
-     we have to duplicate all non-opt rules as opt-rules
+     we have to duplicate all non-opt rules in their opt variant
   | v, OptT t =>
     if is_opt_like_type t
     then None
@@ -330,12 +327,136 @@ Function coerce (v1 : V) (t : T) : option V :=
 Definition Coerces (v1 v2 : V) (t : T) : Prop := coerce v1 t = Some v2.
 Notation "v1 ~> v2 :: t" := (Coerces v1 v2 t) (at level 80, v2 at level 50, no associativity).
 
-(* TODO: derive intro and elim rules *)
+(*
+Now we can prove that this indeed implements the inductive relation in the spec:
+*)
+
+Lemma NatC: forall n, NatV n ~> NatV n :: NatT.
+Proof. intros. reflexivity. Qed.
+
+Lemma IntC: forall n, IntV n ~> IntV n :: IntT.
+Proof. intros. reflexivity. Qed.
+
+Lemma NatIntC: forall n i, i = Z.of_nat n -> NatV n ~> IntV i :: IntT.
+Proof. intros. subst. reflexivity. Qed.
+
+Lemma NullC: NullV ~> NullV :: NullT.
+Proof. intros. reflexivity. Qed.
+
+Lemma NullOptC: forall t, NullV ~> NullV :: OptT t.
+Proof. intros. reflexivity. Qed.
+
+Lemma SomeOptC: forall v1 v2 t,
+    v1 ~> v2 :: t ->
+    SomeV v1 ~> SomeV v2 :: OptT t.
+Proof. unfold Coerces. intros. simpl. rewrite H. reflexivity. Qed.
+
+Lemma OpportunisticOptC:
+    forall v1 t,
+    ~ (exists v2, v1 ~> v2 :: t) ->
+    SomeV v1 ~> NullV :: OptT t.
+Proof.
+  unfold Coerces. simpl. intros.
+  destruct (coerce v1 t).
+  * contradiction H. eexists. reflexivity.
+  * reflexivity.
+Qed.
+
+Lemma ReservedOptC:
+  forall t, ReservedV ~> NullV :: OptT t.
+Proof. intros. reflexivity. Qed.
 
-(* The is_not_opt_like_type definition is only introduced because
-   Coq (and not only coq) does not like hyptheses like ~(null <: t)
+Lemma ConstituentOptC:
+    forall v1 v2 t,
+    is_not_opt_like_value v1 ->
+    is_opt_like_type t = false ->
+    v1 ~> v2 :: t ->
+    v1 ~> SomeV v2 :: OptT t.
+Proof.
+  unfold Coerces. simpl. intros.
+  destruct v1, t; simpl in *; try contradiction; try congruence.
+Qed.
+
+Lemma OpportunisticConstituentOptC:
+    forall v1 t,
+    is_not_opt_like_value v1 ->
+    is_opt_like_type t = false ->
+    ~ (exists v2, v1 ~> v2 :: t) ->
+    v1 ~> NullV :: OptT t.
+Proof.
+  unfold Coerces. simpl. intros.
+  destruct v1, t; simpl in *; try contradiction; try congruence;
+    contradiction H1; eexists; reflexivity.
+Qed.
+
+
+Lemma ReservedC: forall v, v ~> ReservedV :: ReservedT.
+Proof. unfold Coerces. intros. destruct v; reflexivity. Qed.
+
+(*
+Now the induction theorem. As always, ugly and bit.
+Note that negative assumptions don’t give you a P predicate.
 *)
-Lemma is_not_opt_like_type_correct:
+
+Lemma Coerces_ind:
+  forall P,
+  (case natC, forall n, P (NatV n) (NatV n) NatT) ->
+  (case intC, forall n, P (IntV n) (IntV n) IntT) ->
+  (case natIntC, forall n, P (NatV n) (IntV (Z.of_nat n)) IntT) ->
+  (case nullC, P NullV NullV NullT) ->
+  (case nullOptC, forall t, P NullV  NullV (OptT t)) ->
+  (case someOptC, forall v1 v2 t,
+    v1 ~> v2 :: t -> P v1 v2 t -> P (SomeV v1) (SomeV v2) (OptT t)) ->
+  (case opportunisticOptC,
+      forall v1 t, ~ (exists v2, v1 ~> v2 :: t) -> P (SomeV v1) NullV (OptT t)) ->
+  (case reservedOptC,
+    forall t, P ReservedV NullV (OptT t)) ->
+  (case constituentOptC,
+    forall v1 v2 t,
+    is_not_opt_like_value v1 ->
+    is_opt_like_type t = false ->
+    v1 ~> v2 :: t ->
+    P v1 v2 t -> 
+    P v1 (SomeV v2) (OptT t)) ->
+  (case opportunisticConstituentOptC,
+    forall v1 t,
+    is_not_opt_like_value v1 ->
+    is_opt_like_type t = true \/
+    ~ (exists v2, v1 ~> v2 :: t) ->
+    P v1 NullV (OptT t)) ->
+  (case reservedC, forall v, P v ReservedV ReservedT) ->
+  (forall v1 v2 t, v1 ~> v2 :: t -> P v1 v2 t).
+Proof.
+  unfold Coerces.
+  intros P NatC IntC NatIntC NullC NullOptC SomeOptC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC ReservedC v1.
+  induction v1; intros v2 t Hcoerces; destruct t.
+  all: try (inversion Hcoerces; subst; clear Hcoerces; intuition; fail). 
+  all: simpl in Hcoerces.
+  * destruct t;
+    inversion Hcoerces; subst; clear Hcoerces.
+    + apply ConstituentOptC; clear_names; simpl; intuition.
+    + apply ConstituentOptC; clear_names; simpl; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy.
+      right; intros [? ?]; congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
+  * destruct t;
+    inversion Hcoerces; subst; clear Hcoerces.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
+    + apply ConstituentOptC; clear_names; simpl; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy.
+      right; intros [? ?]; congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
+  * destruct (coerce v1 t) eqn:Heq; simpl in Hcoerces; inversion Hcoerces; subst; clear Hcoerces.
+    + apply SomeOptC; clear_names; intuition.
+    + apply OpportunisticOptC; clear_names.
+      intros [v2 H]. congruence.
+Qed.
+
+Lemma is_opt_like_type_correct:
   forall t,
   is_opt_like_type t = true <-> NullT <: t.
 Proof.
@@ -399,7 +520,6 @@ Proof.
     eexists. unfold Coerces in *. simpl. rewrite Hv2. reflexivity.
   }
   [optHT_optST]: {
-    (* specialize (IHHvT t2 (ReflST _ _)).*)
     unfold Coerces. simpl.
     destruct (coerce v t2) eqn:Heq; eexists; reflexivity.
   }
@@ -410,7 +530,7 @@ Proof. intros x. apply ReflST; constructor. Qed.
 
 Lemma is_not_opt_like_type_contravariant:
   forall t1 t2,
-     is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false.
+  is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false.
 Proof. intros. destruct t1, t2; easy. Qed.
 
 Theorem subtyping_trans: transitive _ Subtype.

From 458551d4cd7d1a0c4781beea4fcc68f2fffbee47 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 11 Dec 2020 17:39:12 +0100
Subject: [PATCH 22/25] Introduce does-not-coerce relation

---
 coq/MiniCandid.v | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index b23d2bc9..f8f58508 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -327,6 +327,9 @@ Function coerce (v1 : V) (t : T) : option V :=
 Definition Coerces (v1 v2 : V) (t : T) : Prop := coerce v1 t = Some v2.
 Notation "v1 ~> v2 :: t" := (Coerces v1 v2 t) (at level 80, v2 at level 50, no associativity).
 
+Definition DoesNotCoerce (v1 : V) (t : T) : Prop := coerce v1 t = None.
+Notation "v1 ~/> :: t" := (DoesNotCoerce v1 t) (at level 80, no associativity).
+
 (*
 Now we can prove that this indeed implements the inductive relation in the spec:
 *)
@@ -408,7 +411,7 @@ Lemma Coerces_ind:
   (case someOptC, forall v1 v2 t,
     v1 ~> v2 :: t -> P v1 v2 t -> P (SomeV v1) (SomeV v2) (OptT t)) ->
   (case opportunisticOptC,
-      forall v1 t, ~ (exists v2, v1 ~> v2 :: t) -> P (SomeV v1) NullV (OptT t)) ->
+      forall v1 t, v1 ~/> :: t -> P (SomeV v1) NullV (OptT t)) ->
   (case reservedOptC,
     forall t, P ReservedV NullV (OptT t)) ->
   (case constituentOptC,
@@ -421,13 +424,12 @@ Lemma Coerces_ind:
   (case opportunisticConstituentOptC,
     forall v1 t,
     is_not_opt_like_value v1 ->
-    is_opt_like_type t = true \/
-    ~ (exists v2, v1 ~> v2 :: t) ->
+    is_opt_like_type t = true \/ v1 ~/> :: t ->
     P v1 NullV (OptT t)) ->
   (case reservedC, forall v, P v ReservedV ReservedT) ->
   (forall v1 v2 t, v1 ~> v2 :: t -> P v1 v2 t).
 Proof.
-  unfold Coerces.
+  unfold Coerces. unfold DoesNotCoerce.
   intros P NatC IntC NatIntC NullC NullOptC SomeOptC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC ReservedC v1.
   induction v1; intros v2 t Hcoerces; destruct t.
   all: try (inversion Hcoerces; subst; clear Hcoerces; intuition; fail). 
@@ -438,8 +440,7 @@ Proof.
     + apply ConstituentOptC; clear_names; simpl; intuition.
     + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
     + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy.
-      right; intros [? ?]; congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
     + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
   * destruct t;
     inversion Hcoerces; subst; clear Hcoerces.
@@ -447,13 +448,11 @@ Proof.
     + apply ConstituentOptC; clear_names; simpl; intuition.
     + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
     + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy.
-      right; intros [? ?]; congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
     + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
   * destruct (coerce v1 t) eqn:Heq; simpl in Hcoerces; inversion Hcoerces; subst; clear Hcoerces.
     + apply SomeOptC; clear_names; intuition.
-    + apply OpportunisticOptC; clear_names.
-      intros [v2 H]. congruence.
+    + apply OpportunisticOptC; clear_names; easy.
 Qed.
 
 Lemma is_opt_like_type_correct:

From 2d9af918a637f709a2d0cb596ea150a6af93761f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 11 Dec 2020 17:50:21 +0100
Subject: [PATCH 23/25] Use does-not-coerce relation more

---
 coq/MiniCandid.v | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index f8f58508..dbf40c2c 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -356,13 +356,11 @@ Proof. unfold Coerces. intros. simpl. rewrite H. reflexivity. Qed.
 
 Lemma OpportunisticOptC:
     forall v1 t,
-    ~ (exists v2, v1 ~> v2 :: t) ->
+    v1 ~/> :: t ->
     SomeV v1 ~> NullV :: OptT t.
 Proof.
-  unfold Coerces. simpl. intros.
-  destruct (coerce v1 t).
-  * contradiction H. eexists. reflexivity.
-  * reflexivity.
+  unfold Coerces; unfold DoesNotCoerce. simpl. intros.
+  rewrite H; reflexivity.
 Qed.
 
 Lemma ReservedOptC:
@@ -384,15 +382,13 @@ Lemma OpportunisticConstituentOptC:
     forall v1 t,
     is_not_opt_like_value v1 ->
     is_opt_like_type t = false ->
-    ~ (exists v2, v1 ~> v2 :: t) ->
+    v1 ~/> :: t ->
     v1 ~> NullV :: OptT t.
 Proof.
-  unfold Coerces. simpl. intros.
-  destruct v1, t; simpl in *; try contradiction; try congruence;
-    contradiction H1; eexists; reflexivity.
+  unfold Coerces; unfold DoesNotCoerce. simpl. intros.
+  destruct v1, t; simpl in *; try contradiction; try congruence.
 Qed.
 
-
 Lemma ReservedC: forall v, v ~> ReservedV :: ReservedT.
 Proof. unfold Coerces. intros. destruct v; reflexivity. Qed.
 

From 13595fd2f4a1ae15564abf28585c1cbbbee12854 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 11 Dec 2020 18:29:49 +0100
Subject: [PATCH 24/25] Simpler, faster tactics

---
 coq/MiniCandid.v | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index dbf40c2c..6d111c31 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -434,19 +434,20 @@ Proof.
     inversion Hcoerces; subst; clear Hcoerces.
     + apply ConstituentOptC; clear_names; simpl; intuition.
     + apply ConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition.
   * destruct t;
     inversion Hcoerces; subst; clear Hcoerces.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
     + apply ConstituentOptC; clear_names; simpl; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; firstorder congruence.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-    + apply OpportunisticConstituentOptC; clear_names; simpl; try easy; intuition.
-  * destruct (coerce v1 t) eqn:Heq; simpl in Hcoerces; inversion Hcoerces; subst; clear Hcoerces.
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
+    + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. 
+  * destruct (coerce v1 t) eqn:Heq; simpl in Hcoerces;
+    inversion Hcoerces; subst; clear Hcoerces.
     + apply SomeOptC; clear_names; intuition.
     + apply OpportunisticOptC; clear_names; easy.
 Qed.

From 419a7a5dca8b3cb5a901ce9d8ad6f78ea563a12c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 20 Dec 2020 23:53:41 +0100
Subject: [PATCH 25/25] Coq: Add vec
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

only to `NoOpportunisticDecoding` so far. Dealing with data structures
(even simple ones like lists) in Coq can be a pain, and the ugilness of
these proves have greatly increased, so keeping this on a branch for
now. Maybe I’ll find the right sweet spot later.
---
 coq/MiniCandid.v | 135 ++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 127 insertions(+), 8 deletions(-)

diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 6d111c31..5a3e732d 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -4,8 +4,11 @@ MiniCandid: A formalization of the core ideas of Candid
 
 Require Import FunInd.
 
+Require Import Psatz.
+
 Require Import Coq.ZArith.BinInt.
 Require Import Coq.Init.Datatypes.
+Require Import Coq.Lists.List.
 
 Require Import Coq.Relations.Relation_Operators.
 Require Import Coq.Relations.Relation_Definitions.
@@ -24,6 +27,7 @@ CoInductive T :=
   | IntT: T
   | NullT : T
   | OptT : T -> T
+  | VecT : T -> T
   | VoidT : T
   | ReservedT : T
   .
@@ -33,6 +37,7 @@ Inductive V :=
   | IntV : Z -> V
   | NullV : V
   | SomeV : V -> V
+  | VecV : list V -> V
   | ReservedV : V
   .
 
@@ -71,6 +76,9 @@ Inductive HasType : V -> T -> Prop :=
   | OptHT:
     case optHT,
     forall v t, v :: t -> SomeV v :: OptT t
+  | VecHT:
+    case vecHT,
+    forall vs t, (forall n, n < length vs -> nth n vs NullV :: t) -> VecV vs :: VecT t
   | ReservedHT:
     case reservedHT,
     ReservedV :: ReservedT
@@ -87,10 +95,10 @@ Here things are simple and inductive.
 Reserved Infix "<:" (at level 80, no associativity).
 CoInductive Subtype : T -> T -> Prop :=
   | ReflST :
-    case reflSL,
+    case reflST,
     forall t, t <: t
   | NatIntST :
-    case natIntSL,
+    case natIntST,
     NatT <: IntT
   | NullOptST :
     case nullOptST,
@@ -107,6 +115,11 @@ CoInductive Subtype : T -> T -> Prop :=
     forall t1 t2,
     is_opt_like_type t2 = false ->
     t1 <: t2 -> t1 <: OptT t2
+  | VecST :
+    case vecST,
+    forall t1 t2,
+    t1 <: t2 ->
+    VecT t1 <: VecT t2
   | VoidST :
     case voidST,
     forall t, VoidT <: t
@@ -144,6 +157,12 @@ Inductive Coerces : V -> V -> T -> Prop :=
     is_not_opt_like_value v1 ->
     v1 ~> v2 :: t ->
     v1 ~> SomeV v2 :: OptT t
+  | VecC:
+    case vecC,
+    forall vs1 vs2 t,
+    length vs1 = length vs2 ->
+    (forall n, n < length vs1 -> nth n vs1 NullV ~> nth n vs2 NullV :: t) ->
+    VecV vs1 ~> VecV vs2 :: VecT t
   | ReservedC:
     case reservedC,
     forall v1,
@@ -162,13 +181,36 @@ Qed.
 Theorem coercion_correctness:
   forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t.
 Proof.
-  intros. induction H; constructor; assumption.
+  intros. induction H; try (named_constructor; assumption); name_cases.
+  [vecC]: {
+    named_constructor.
+    intros.
+    apply H1. lia.
+  }
 Qed.
 
 Theorem coercion_roundtrip:
   forall v t, v :: t -> v ~> v :: t.
 Proof.
-  intros. induction H; constructor; intuition.
+  intros. induction H; try (constructor; intuition); name_cases.
+Qed.
+
+Lemma nths_ext:
+  forall A (l1 l2 : list A) d,
+  length l1 = length l2 ->
+  (forall n, n < length l1 -> nth n l1 d = nth n l2 d) ->
+  l1 = l2.
+Proof.
+  intros A l1. induction l1; intros l2 d Heq Hnth.
+  * destruct l2; inversion Heq. reflexivity.
+  * destruct l2; inversion Heq.
+    f_equal.
+    - specialize (Hnth 0 ltac:(simpl;lia)).
+      simpl in Hnth. assumption.
+    - eapply IHl1; try assumption.
+      intros n Hle.
+      specialize (Hnth (S n) ltac:(simpl;lia)).
+      simpl in Hnth. eassumption.
 Qed.
 
 Theorem coercion_uniqueness:
@@ -177,7 +219,16 @@ Proof.
   intros.
   revert v2 H0.
   induction H; intros v2' Hother;
-    try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence).
+    try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence);
+    name_cases.
+  [vecC]: {
+    inversion Hother; subst; clear Hother.
+    apply f_equal.
+    eapply nths_ext; try congruence.
+    intros n Hle.
+    apply H1; try congruence.
+    apply H6; congruence.
+  }
 Qed.
 
 Theorem soundness_of_subtyping:
@@ -196,9 +247,9 @@ Proof.
   }
   [intHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
-    econstructor. named_econstructor; [constructor|named_constructor].
+    eexists. named_econstructor; [constructor|named_constructor].
   }
-  [optHT_reflSL]: {
+  [optHT_reflST]: {
     specialize (IHHvT t (ReflST _ _)).
     destruct IHHvT as [v2 Hv2].
     eexists. named_econstructor; try eassumption.
@@ -211,6 +262,64 @@ Proof.
   [optHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
   }
+  [vecHT_vecST]: {
+    clear H.
+    assert (Hv2 : forall n : nat, n < length vs -> exists v2 : V, nth n vs NullV ~> v2 :: t2) by intuition.
+    clear H0 H2.
+    induction vs.
+    * exists (VecV nil). named_constructor; try reflexivity. intuition. simpl in H. lia.
+    * lapply IHvs.
+      - intros. destruct H as [v2 HC].
+        inversion HC; subst; clear HC.
+        destruct (Hv2 0 ltac:(simpl;lia)) as [va HCa].
+        exists (VecV (va :: vs2)).
+        named_constructor.
+        + simpl; congruence.
+        + intros. simpl in H.
+          destruct n.
+          ** apply HCa.
+          ** apply H3. lia.
+     - intros.
+       specialize (Hv2 (S n) ltac:(simpl;lia)).
+       firstorder.
+  }
+  [vecHT_reflST]: {
+    eexists. named_constructor. 
+    * reflexivity.
+    * intros.
+      apply coercion_roundtrip.
+      apply H.
+      assumption.
+  }
+  [vecHT_constituentOptST]: {
+    inversion H2; subst; clear H2; simpl in H1; inversion H1.
+    * eexists.
+      named_constructor; try reflexivity.
+      named_constructor; try reflexivity.
+      intros. apply coercion_roundtrip. apply H. assumption.
+    * enough (exists v2 : V, VecV vs ~> v2 :: VecT t0)
+        by (destruct H2; eexists; named_constructor; try reflexivity; apply H2).
+      assert (Hv2 : forall n : nat, n < length vs -> exists v2 : V, nth n vs NullV ~> v2 :: t0) by intuition.
+      clear H H0 H1 vecST H4 t.
+      {
+      induction vs.
+      * exists (VecV nil). named_constructor; try reflexivity. intuition. simpl in H. lia.
+      * lapply IHvs.
+        - intros. destruct H as [v2 HC].
+          inversion HC; subst; clear HC.
+          destruct (Hv2 0 ltac:(simpl;lia)) as [va HCa].
+          exists (VecV (va :: vs2)).
+          named_constructor.
+          + simpl; congruence.
+          + intros. simpl in H.
+            destruct n.
+            ** apply HCa.
+            ** apply H3. lia.
+       - intros.
+         specialize (Hv2 (S n) ltac:(simpl;lia)).
+         firstorder.
+       }
+  }
   [reservedHT_constituentOptST]: {
     inversion H0; subst; clear H0; simpl in H; inversion H.
   }
@@ -232,7 +341,7 @@ Proof.
   inversion H2; subst; clear H2;
     name_cases;
     try (constructor; easy).
-  [natIntSL_constituentOptST]: {
+  [natIntST_constituentOptST]: {
     named_constructor.
     - assumption.
     - eapply Hyp; [named_econstructor | assumption].
@@ -256,6 +365,16 @@ Proof.
   [reservedST_constituentOptST]: {
     inversion H0; subst; clear H0; inversion H.
   }
+  [vecST_vecST0]: {
+    named_constructor.
+    eapply Hyp; eassumption.
+  }
+  [vecST_constituentOptST]: {
+    named_constructor; try assumption.
+    inversion H1; subst; clear H1; try easy.
+    - named_constructor; assumption.
+    - named_constructor. eapply Hyp; eassumption.
+  }
 Qed.
 
 End NoOpportunisticDecoding.