Verifications and uses in HLF

From The Twelf Project

This example can only be run in the Hybrid LF implementation of Twelf created by Jason Reed as part of his Ph.D. Thesis, "A Hybrid Logical Framework." It shouldn't be suprising that the little box to the right says "Status: %% ABORT %%," in other words. The example on verifications and uses with zippers has essentially the same content but actually works in non-HLF extended Twelf.

This code is primarily here so it can be referenced by a blog post by Rob.

%hlf.

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 -> @type.

atm : hyp A -> (use A -o use (a Q)) -> verif (a Q).
⊃I  : (hyp A1 -> verif A2) -> verif (A1 ⊃ A2).
⊃E  : use (A1 ⊃ A2) -o verif A1 -> use A2.
∧I  : verif A1 -> verif A2 -> verif (A1 ∧ A2).
∧E1 : use (B1 ∧ B2) -o use B1.
∧E2 : use (B1 ∧ B2) -o use B2.

%block bl_hyp : some {A : prop} block {x : hyp A e}.
%block bl_use : some {A : prop} block {α}{x : use A α}.
%worlds (bl_atom | bl_hyp | bl_use) (verif _ _) (use _ _) (hyp _ _).

Global completeness

eta : {A} ({B} hyp B -> (use B -o use A) -> verif A) -> type.
%mode eta +A -B.

- : eta (a Q) ([B][x : hyp B][r : use B -o use (a Q)] 
          atm x ([u :^ (use B)] r ^ u)).
- : eta (A1 ⊃ A2) ([B][x : hyp B][r : use B -o use (A1 ⊃ A2)] 
          ⊃I ([y : hyp A1] N2 B x ([u :^ (use B)]
            ⊃E ^ (r ^ u) (N1 A1 y ([u :^ (use A1)] u)))))
     <- eta A1 ([B] N1 B : hyp B -> (use B -o use A1) -> verif A1)
     <- eta A2 ([B] N2 B : hyp B -> (use B -o use A2) -> verif A2).
- : eta (A1 ∧ A2) ([B][x : hyp B][r : use B -o use (A1 ∧ A2)]
          ∧I (N1 B x ([u :^ (use B)] ∧E1 ^ (r ^ u))) 
             (N2 B x ([u :^ (use B)] ∧E2 ^ (r ^ u))))
     <- eta A1 ([B] N1 B : hyp B -> (use B -o use A1) -> verif A1)
     <- eta A2 ([B] N2 B : hyp B -> (use B -o use A2) -> verif A2).

%worlds (bl_atom | bl_hyp | bl_use) (eta _ _).
%total A (eta A _).

%solve s : {q}{r}{s} eta (a q ⊃ a r ⊃ a s) (X q r s).
%solve s : {q}{r}{s} eta ((a q ⊃ a r) ⊃ a s) (X q r s).

Global soundness

hsubst_n  : {A}    verif A -> (hyp A -> verif B)        -> verif B -> type.
hsubst_rr : {A}    verif A -> (hyp A -> use C -o use B) -> (use C -o use B) -> type.
hsubst_rn : {A}{B} verif A -> (hyp A -> use A -o use 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 : hyp A] ⊃I [y : hyp B1] M x y) (⊃I [y : hyp B1] N y)
     <- {y : hyp B1} hsubst_n A M0 ([x : hyp A] M x y) (N y : verif B2).
- : hsubst_n A M0 ([x : hyp A] ∧I (M1 x) (M2 x)) (∧I N1 N2)
     <- hsubst_n A M0 M1 (N1 : verif B1)
     <- hsubst_n A M0 M2 (N2 : verif B2).
- : hsubst_n A M0 ([x : hyp A] atm x ([u :^ (use A)] R x ^ u)) N
     <- hsubst_rn A (a Q) M0 R (N : verif (a Q)).
- : hsubst_n A M0 ([x : hyp A] atm Y (R x)) (atm Y R')
     <- hsubst_rr A M0 R (R' : use C -o use (a Q)).

- : hsubst_rr A M0 ([x : hyp A][u :^ (use C)] ⊃E ^ (R x ^ u) (M x)) 
          ([u :^ (use C)] ⊃E ^ (R' ^ u) N)        
     <- hsubst_rr A M0 R (R' : use C -o use (B1 ⊃ B2)) 
     <- hsubst_n A M0 M (N : verif B1).
- : hsubst_rr A M0 ([x : hyp A][u :^ (use C)] ∧E1 ^ (R x ^ u)) 
          ([u :^ (use C)] ∧E1 ^ (R' ^ u))
     <- hsubst_rr A M0 R (R' : use C -o use (B1 ∧ B2)).
- : hsubst_rr A M0 ([x : hyp A][u :^ (use C)] ∧E2 ^ (R x ^ u)) 
          ([u :^ (use C)] ∧E2 ^ (R' ^ u))
     <- hsubst_rr A M0 R (R' : use C -o use (B1 ∧ B2)).
- : hsubst_rr A M0 ([x : hyp A][u :^ (use C)] u) ([u :^ (use C)] u).

- : hsubst_rn A B2 M0 ([x : hyp A][u :^ (use A)] ⊃E ^ (R x ^ u) (M x)) N'
     <- hsubst_rn A (B1 ⊃ B2) M0 R ((⊃I [y : hyp B1] N y) : verif (B1 ⊃ B2))
     <- hsubst_n A M0 M (M' : verif B1)
     <- hsubst_n B1 M' N (N' : verif B2).
- : hsubst_rn A B1 M0 ([x : hyp A][u :^ (use A)] ∧E1 ^ (R x ^ u)) N1
     <- hsubst_rn A (B1 ∧ B2) M0 R (∧I N1 N2 : verif (B1 ∧ B2)).
- : hsubst_rn A B2 M0 ([x : hyp A][u :^ (use A)] ∧E2 ^ (R x ^ u)) N2
     <- hsubst_rn A (B1 ∧ B2) M0 R (∧I N1 N2 : verif (B1 ∧ B2)).
- : hsubst_rn A A M0 ([x : hyp A][u :^ (use A)] u) 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 _).