Canonical forms lemma
This article is about proving an object language lemma. For the notion of canonical form within LF itself, see canonical form.
In a standard proofs of TODO, the progress theorem requires canonical forms lemmas about the values in a language. These lemmas are usually in the form “If e is a value and ⊦ e : T, then e is of some form appropriate for T”. A specific example would be “If e is a value and ⊦ e : T1 → T2, then e is of the form λx:T1.e’”.
Depending on the complexity of the type system, there are two general ways to state and prove these lemmas. In some cases, STELF’s input coverage can give you the canonical forms lemma for free. In other cases, you must state and prove canonical forms explicitly using equality.
Canonical forms lemmas for free
Section titled “Canonical forms lemmas for free”If there is only one rule through which the canonical form at a particular type can be derived, then STELF’s input coverage is actually strong enough to give you canonical forms for free via TODO.
Consider the following language:
%sort tp %.%term tp/unit tp %.%term tp/arrow %pi tp %-> tp %-> tp %.%sort exp %.%term exp/unit exp %.%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.%term exp/app %pi exp %-> exp %-> exp %.%sort of {_ exp} {_ tp} %.%term of/unit of exp/unit tp/unit %.%term of/lam %pi (of (exp/lam T1 E) (tp/arrow T1 T2)) %<- ({x} %pi (of x T1) %-> (of (E x) T2)) %.%term of/app %pi (of (exp/app E1 E2) T2) %<- (of E2 T1) %<- (of E1 (tp/arrow T1 T2)) %.%sort val {_ exp} %.%term val/unit val exp/unit %.%term val/lam val (exp/lam _ _) %.%sort step {_ exp} {_ exp} %.%term step/app-1 %pi (step (exp/app E1 E2) (exp/app E1' E2)) %<- (step E1 E1') %.%term step/app-2 %pi (step (exp/app E1 E2) (exp/app E1 E2')) %<- (step E2 E2') %<- (val E1) %.%term step/app-beta %pi (step (exp/app (exp/lam _ E) E2) (E E2)) %<- (val E2) %.%sort notstuck {_ exp} %.%term notstuck/val %pi (notstuck E) %<- (val E) %.%term notstuck/step %pi (notstuck E) %<- (step E E') %.To prove progress for this language, we use an output factoring lemma that collects the post-inductive-call reasoning in the application case:
%sort progress-exp/app {_ notstuck E1} {_ notstuck E2} {_ of E1 (tp/arrow _ _)} {_ notstuck (exp/app E1 E2)} %.%mode progress-exp/app %in %in %in %out %.%term _ progress-exp/app (notstuck/step S) _ _ (notstuck/step (step/app-1 S)) %.%term _ progress-exp/app (notstuck/val V) (notstuck/step S) _ (notstuck/step (step/app-2 V S)) %.%term _ progress-exp/app (notstuck/val val/lam) (notstuck/val V2) (of/lam _) (notstuck/step (step/app-beta V2)) %.%worlds () (progress-exp/app _ _ _ _) %.%total {} (progress-exp/app _ _ _ _) %.In the final case, we use inversion to assert that E1 is a value in the form of a lambda. Because we also pass in a typing derivation that says E1 is of an arrow type, STELF’s input coverage verifies that the only time E1 is a value and has an arrow type is when it is a lambda. Because the type system is simple enough that STELF can figure out that the only values of arrow type are lambdas, we get canonical forms “for free”.
It is then simple to complete the proof of progress:
%sort progress {_ of E T} {_ notstuck E} %.%mode progress %in %out %.%term _ progress of/unit (notstuck/val val/unit) %.%term _ progress (of/lam _) (notstuck/val val/lam) %.%term _ %pi (progress (of/app D1 D2) NS) %<- (progress D1 NS1) %<- (progress D2 NS2) %<- (progress-exp/app NS1 NS2 D1 NS) %.%worlds () (progress _ _) %.%total (D1) (progress D1 _) %.Canonical forms lemmas stated using equality
Section titled “Canonical forms lemmas stated using equality”Some languages do not have the luxury of having exactly one rule through which a canonical form could be derived. This is common for languages with re-typing rules that make use of subtyping/type equality. In such languages, canonical forms lemmas must be explicitly stated and proven. The conclusion of the lemma “e is of the form …” can be stated in a straightforward way using shallow equality. This example makes use of output factoring and reasoning from equality.
For example, we extend the above language with a trivial notion of subtyping. It is equivalent to syntactic equality on types. The purpose of this tutorial is to illustrate how to state/prove canonical forms lemmas when subtyping/equality are part of the type system, and this trivial notion is enough to motivate the discussion.
%sort tp-sub {_ tp} {_ tp} %.%term tp-sub/unit tp-sub tp/unit tp/unit %.%term tp-sub/arrow %pi (tp-sub (tp/arrow T1 T2) (tp/arrow T3 T4)) %<- (tp-sub T2 T4) %<- (tp-sub T3 T1) %.%term of/sub %pi (of E1 T2) %<- (tp-sub T1 T2) %<- (of E1 T1) %.Now, we state and prove the canonical forms lemma explicitly. In the theorem statement, we use the syntactic equality judgement as an output in order to state “E1 is of the form (exp/lam T E)”.
%sort seq-exp {_ exp} {_ exp} %.%term seq-exp/i seq-exp E E %.%sort cfl-tp/arrow {_ val E1} {_ of E1 (tp/arrow _ _)} {_ seq-exp E1 (exp/lam T E)} %.%mode cfl-tp/arrow %in %in %out %.%term _ cfl-tp/arrow val/lam (of/lam _) seq-exp/i %.%term _ %pi (cfl-tp/arrow V (of/sub D1 (tp-sub/arrow _ _)) DQ) %<- (cfl-tp/arrow V D1 DQ) %.%worlds () (cfl-tp/arrow _ _ _) %.%total (D1) (cfl-tp/arrow _ D1 _) %.Next, we define a helper lemma for showing that (exp/app E1 E2) is notstuck when E1 is of the form (exp/lam T E) and E2 is a value. We use this lemma because we get the derivation of (seq-exp E1 (exp/lam T E)) as the output of the canonical forms lemma. If we were to try to invert the derivation as an output, we would cause STELF’s coverage checker to fail. So instead, we call a helper lemma with the equality derivation as an input. Because the derivation is an input, we can safely apply inversion on it.
%sort progress-exp/app-beta {_ seq-exp E1 (exp/lam T E)} {_ val E2} {_ notstuck (exp/app E1 E2)} %.%mode progress-exp/app-beta %in %in %out %.%term _ progress-exp/app-beta seq-exp/i V (notstuck/step (step/app-beta V)) %.%worlds () (progress-exp/app-beta _ _ _) %.%total {} (progress-exp/app-beta _ _ _) %.Next, we prove the output factoring lemma:
%sort progress-exp/app {_ notstuck E1} {_ notstuck E2} {_ of E1 (tp/arrow _ _)} {_ notstuck (exp/app E1 E2)} %.%mode progress-exp/app %in %in %in %out %.%term _ progress-exp/app (notstuck/step S) _ _ (notstuck/step (step/app-1 S)) %.%term _ progress-exp/app (notstuck/val V) (notstuck/step S) _ (notstuck/step (step/app-2 V S)) %.Because there is more than one way to derive that a value that has an arrow type, we must use the canonical forms lemma we have just proven. To make use of the equality we get out of the canonical forms lemma, we call the special helper lemma progress-exp/app-beta.
%term _ %pi (progress-exp/app (notstuck/val V) (notstuck/val V2) D1 NS) %<- (cfl-tp/arrow V D1 DQ) %<- (progress-exp/app-beta DQ V2 NS) %.%worlds () (progress-exp/app _ _ _ _) %.%total {} (progress-exp/app _ _ _ _) %.Finally, we prove the overall progress theorem as before.
%sort progress {_ of E T} {_ notstuck E} %.%mode progress %in %out %.%term _ progress of/unit (notstuck/val val/unit) %.%term _ progress (of/lam _) (notstuck/val val/lam) %.%term _ %pi (progress (of/app D1 D2) NS) %<- (progress D1 NS1) %<- (progress D2 NS2) %<- (progress-exp/app NS1 NS2 D1 NS) %.%term _ %pi (progress (of/sub D1 _) NS) %<- (progress D1 NS) %.%worlds () (progress _ _) %.%total (D1) (progress D1 _) %.