Merge pull request #629 from stepchowfun/readme-wordsmithing

Wordsmith the admissibility graph README

Author: stepchowfun

proofs/admissibility_graph/README.md

@@ -20,11 +20,11 @@ To make those informal descriptions more precise, the following axioms determine
    - If some `Z` is allowed to depend on `X`, then `Z` is also allowed to depend on `Y`.
 4. No other dependencies are allowed.
 
-The *transpose* of an admissibility graph is the graph formed by swapping the edge types—`X trusts Y` becomes `X exports Y` and vice versa.
+The *transpose* of an admissibility graph is the graph formed by swapping the edge types; `X trusts Y` becomes `X exports Y` and vice versa.
 
 ## Wooden admissibility graphs
 
-If `X trusts Y` or `X exports Y`, we say `X` is a *parent* of `Y` and `Y` is a *child* of `X`. An important special case which enables additional reasoning power at the expense of flexibility is to limit each node to having at most one parent. The resulting structure is called a *wooden admissibility graph*.
+If `X trusts Y` or `X exports Y`, we say `X` is a *parent* of `Y` and `Y` is a *child* of `X`. An important special case which enables additional reasoning power at the expense of flexibility is to limit each node to having at most one parent. The resulting structure is called a *wooden admissibility graph*, and it enjoys the *encapsulation* and *sandboxing* theorems below.
 
 ## Closure concepts
 
@@ -42,9 +42,9 @@ This development contains verified proofs of the following theorems:
 
 **Theorem (reflection).** Given two admissibility graphs with the same nodes that have matching edges between all pairs of *distinct* nodes, then they allow the same dependencies. In other words, nothing is gained by having a node trust or export itself.
 
-**Theorem (admission).** `X` is allowed to depend on `Y` [iff](https://en.wikipedia.org/wiki/If_and_only_if) there some `U` is trusting of `X` and some `V` is exporting `Y` and `U` = `V` or there is an edge `U trusts V` or `V exports U`.
+**Theorem (admission).** `X` is allowed to depend on `Y` iff there some `U` is trusting of `X` and some `V` is exporting `Y` and `U` = `V` or there is an edge `U trusts V` or `V exports U`.
 
-**Theorem (transposition).** Given an admissibility graph `G`, `G` allows `X` to depend on `Y` iff the transpose of `G` allows `Y` to depend on `X`.
+**Theorem (duality).** Given an admissibility graph `G`, `G` allows `X` to depend on `Y` iff the transpose of `G` allows `Y` to depend on `X`.
 
 **Theorem (encapsulation).** In a wooden admissibility graph, if `X` is a parent of `Y` and `Z` is allowed to depend on `Y`, then either `X` is an ancestor of `Z` or (`X exports Y` and `Z` is allowed to depend on `X`).
 

proofs/admissibility_graph/admissibility_graph.v

@@ -182,14 +182,14 @@ Qed.
   of the dependencies allowed by the original graph.
 *)
 
-Theorem transposition :
+Theorem duality :
   forall (Node : Type) (g : AdmissibilityGraph Node) n1 n2,
   Allowed g n1 n2 <-> Allowed (transpose g) n2 n1.
 Proof.
   split; clean; induction H; esearch.
 Qed.
 
-#[export] Hint Resolve transposition : main.
+#[export] Hint Resolve duality : main.
 
 (*
   If a node trusts or exports another node, we say the former node is a
@@ -434,19 +434,19 @@ Proof.
     destruct H2.
     clear H3.
     feed H2.
-    + apply -> transposition.
+    + apply -> duality.
       search.
     + clean.
       rewrite <- transpose_exporting in H2.
       repeat (destruct H2; search).
-      apply transposition in H3.
+      apply duality in H3.
       search.
   - pose proof (childIngress Node (transpose g) n1 n2 n3).
     feed H2; [ apply -> transpose_wooden; search | idtac ].
     feed H2; [ apply -> transpose_parent_child; search | idtac ].
     destruct H2.
     clear H2.
-    apply transposition in H3; search.
+    apply duality in H3; search.
 Qed.
 
 #[export] Hint Resolve childEgress : main.
@@ -469,12 +469,12 @@ Proof.
   pose proof (encapsulation Node (transpose g) n1 n2 n3).
   feed H2; [ apply -> transpose_wooden; search | idtac ].
   feed H2; [ apply -> transpose_parent_child; search | idtac ].
-  feed H2; [ apply -> transposition; search | idtac ].
+  feed H2; [ apply -> duality; search | idtac ].
   destruct H2.
   - apply transpose_ancestor in H2.
     search.
   - clean.
-    apply transposition in H3.
+    apply duality in H3.
     search.
 Qed.