Verifications and uses with zippers
From The Twelf Project
| This is Literate Twelf Code: here Status: %% OK %% Output: here. |
In the verifications and uses article we saw a typical presentation of a logic of verifications and uses, and in article on hereditary substitution with zippers we saw an attempt to clean up the "ugly part" of that proof by defining a zipper-like structure over terms. The reason that global soundness for this system did not hold is that Twelf could not verify (without the use of a structural metric) that a "zipped" use was the same size as an "unzipped" use, so termination checking failed when a recursive call was made on a term that had been unzipped.
In this article, we give a different solution. This system has something of the flavor of a spine form presentation; however, as we discussed in the hereditary substitution with zippers, it is still much closer to a natural deduction system - the analogue of the natural deduction term atm (⊃E (⊃E (⊃E (var x) N1) N2) N3) in the natural deduction system is atm x (⊃E (⊃E (⊃E end N1) N2) N3) in this version of "natural deduction" - the form of proofs stays the same with the exception that the head variable x has been pulled out into the front.
Propositions and rules
prop : type. atom : type. %block bl_atom : block {qp : atom}. a : atom -> prop. ⊃ : prop -> prop -> prop. %infix right 9 ⊃. ∧ : prop -> prop -> prop. %infix right 8 ∧. hyp : prop -> type. verif : prop -> type. use : prop -> prop -> type. %block bl_hyp : some {A : prop} block {x : hyp A}. end : use A A. atm : hyp A -> use A (a Q) -> verif (a Q). ⊃I : (hyp A -> verif B) -> verif (A ⊃ B). ⊃E : use A (B1 ⊃ B2) -> verif B1 -> use A B2. ∧I : verif A1 -> verif A2 -> verif (A1 ∧ A2). ∧E1 : use A (B1 ∧ B2) -> use A B1. ∧E2 : use A (B1 ∧ B2) -> use A B2.
Global completeness
Because we have changed the logic, the η-expansion theorem has changed somewhat. Recall that, in the pure system of verifications and uses, the statement of global completeness/η-expansion was that, for all A, we can verify the truth of A in any context where we can use the fact that A is true. In this system, however, we don't ever use A in a vacuum - we always take a hypothesis of B and then prove that, given B, we can use A. The eta expansion theorem reflects this: it says that, for any A, given an arbitrary B that we have hypothesized to be true and a proof that we can use A given B, we can prove A.
The structure of the η-expansion theorem's proof is then mostly unchanged from the system of verifications and uses.
eta : {A} ({B} hyp B -> use B A -> verif A) -> type. %mode eta +A -B. - : eta (a Q) ([B][x][r] atm x r). - : eta (A1 ⊃ A2) ([B][x][r] ⊃I [y] N2 B x (⊃E r (N1 A1 y end))) <- eta A1 ([B] N1 B : hyp B -> use B A1 -> verif A1) <- eta A2 ([B] N2 B : hyp B -> use B A2 -> verif A2). - : eta (A1 ∧ A2) ([B][x][r] ∧I (N1 B x (∧E1 r)) (N2 B x (∧E2 r))) <- eta A1 ([B] N1 B : hyp B -> use B A1 -> verif A1) <- eta A2 ([B] N2 B : hyp B -> use B A2 -> verif A2). %worlds (bl_atom | bl_hyp) (eta _ _). %total A (eta A _).
Let's see some examples of η-expansions:
%solve _ : {q1}{q2}{q3} eta (a q1 ⊃ a q2 ⊃ a q3) (X q1 q2 q3).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)%solve {q1:atom} {q2:atom} {q3:atom} eta (a q1 ⊃ a q2 ⊃ a q3) ([B:prop] [x:hyp B] [x1:use B (a q1 ⊃ a q2 ⊃ a q3)] X q1 q2 q3 B x x1). OK _ : {q1:atom} {q2:atom} {q3:atom} eta (a q1 ⊃ a q2 ⊃ a q3) ([B:prop] [x:hyp B] [x1:use B (a q1 ⊃ a q2 ⊃ a q3)] ⊃I ([y:hyp (a q1)] ⊃I ([y1:hyp (a q2)] atm x (⊃E (⊃E x1 (atm y end)) (atm y1 end))))) = [q1:atom] [q2:atom] [q3:atom] %-% (%-% %-% %-%) %-%.
%% OK %%
%solve _ : {q1}{q2}{q3} eta ((a q1 ⊃ a q2) ⊃ a q3) (X q1 q2 q3).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)%solve {q1:atom} {q2:atom} {q3:atom} eta ((a q1 ⊃ a q2) ⊃ a q3) ([B:prop] [x:hyp B] [x1:use B ((a q1 ⊃ a q2) ⊃ a q3)] X q1 q2 q3 B x x1). OK _ : {q1:atom} {q2:atom} {q3:atom} eta ((a q1 ⊃ a q2) ⊃ a q3) ([B:prop] [x:hyp B] [x1:use B ((a q1 ⊃ a q2) ⊃ a q3)] ⊃I ([y:hyp (a q1 ⊃ a q2)] atm x (⊃E x1 (⊃I ([y1:hyp (a q1)] atm y (⊃E end (atm y1 end))))))) = [q1:atom] [q2:atom] [q3:atom] %-% %-% (%-% %-% %-%).
%% OK %%
Global soundness
The real benefit of this modified natural deduction system is that we no longer need to take any detours to prove the hereditary substitution theorem: when we reach the atm case where we must verify an atomic proposition by using a proof of its truth, we know exactly what hypothesis we are using. If the hypothesis is the one we're substituting for, then we call out to the hsubst_rn theorem where we do repeated reductions, and if the hypothesis is not, we call out to the hsubst_rr theorem where the structure of the use stays essentially the same.
hsubst_n : {A} verif A -> (hyp A -> verif B) -> verif B -> type. hsubst_rr : {A} verif A -> (hyp A -> use C B) -> use C B -> type. hsubst_rn : {A}{B} verif A -> (hyp A -> use A B) -> verif B -> type. %mode hsubst_n +A +M0 +M -N. %mode hsubst_rr +A +M0 +R -R'. %mode hsubst_rn +A +B +M0 +R -N. - : hsubst_n A M0 ([x] ⊃I [y] M x y) (⊃I [y] N y) <- {y : hyp B1} hsubst_n A M0 ([x] M x y) (N y : verif B2). - : hsubst_n A M0 ([x] ∧I (M1 x) (M2 x)) (∧I N1 N2) <- hsubst_n A M0 ([x] M1 x) (N1 : verif B1) <- hsubst_n A M0 ([x] M2 x) (N2 : verif B2). - : hsubst_n A M0 ([x] atm x (R x)) N <- hsubst_rn A (a Q) M0 ([x] R x) N. - : hsubst_n A M0 ([x] atm Y (R x)) (atm Y R') <- hsubst_rr A M0 ([x] R x) R'. - : hsubst_rr A M0 ([x] ⊃E (R x) (M x)) (⊃E R' N) <- hsubst_rr A M0 ([x] R x) R' <- hsubst_n A M0 ([x] M x) N. - : hsubst_rr A M0 ([x] ∧E1 (R x)) (∧E1 R') <- hsubst_rr A M0 ([x] R x) R'. - : hsubst_rr A M0 ([x] ∧E2 (R x)) (∧E2 R') <- hsubst_rr A M0 ([x] R x) R'. - : hsubst_rr A M0 ([x] end) end. - : hsubst_rn A B2 M0 ([x] ⊃E (R x) (M x)) N' <- hsubst_rn A (B1 ⊃ B2) M0 ([x] R x) ((⊃I [y] N y) : verif (B1 ⊃ B2)) <- hsubst_n A M0 ([x] M x) (M' : verif B1) <- hsubst_n B1 M' ([y] N y) (N' : verif B2). - : hsubst_rn A B1 M0 ([x] ∧E1 (R x)) N1 <- hsubst_rn A (B1 ∧ B2) M0 ([x] R x) (∧I N1 N2 : verif (B1 ∧ B2)). - : hsubst_rn A B2 M0 ([x] ∧E2 (R x)) N2 <- hsubst_rn A _ M0 ([x] R x) (∧I N1 N2 : verif (B1 ∧ B2)). - : hsubst_rn A A M0 ([x] end) M0. %worlds (bl_atom | bl_hyp) (hsubst_n _ _ _ _) (hsubst_rr _ _ _ _) (hsubst_rn _ _ _ _ _). %reduces B <= A (hsubst_rn A B _ _ _). %total {(A B C) (M R S)} (hsubst_n A _ M _) (hsubst_rr B _ R _) (hsubst_rn C _ _ S _).
