Embedding Example: Curry-Howard

We define propositional terms as a recursive type Prop:

let prop_INDUCT,prop_RECURSION = define_type
                                   "Prop = Truth
                                    | Product Prop Prop
                                    | Implies Prop Prop";;    

We also add some syntax sugar. Namely, we set --> as the infix operator for implication (Implies) and % as the infix operator for conjunction (Product):

parse_as_infix("-->",(13,"right"));;
override_interface("-->",`Implies`);;
parse_as_infix("%",(14,"right"));;
override_interface("%",`Product`);;

First we introduce an infix operator for logical consequence, i.e. the “turnstile”.

parse_as_infix("|=",(11,"right"));;

We then provide an inductive definition for the operator based on the inference rules. Each line (conjunct) in the definition corresponds to one inference rule, in the following order:

1. Identity (ID)
2. Weakening (W)
3. Contraction (C)
4. Cut (Cut)
5. Conjunction Right (RX)
6. Conjunction Left1 (L1X)
7. Conjunction Left2 (L2X)
8. Implication Left (L-->)
9. Implication Right (R-->)

 0: let propRULES,propINDUCT,propCASES = new_inductive_definition 
 1: `(!a. ' a |= a) /\
 2: (!G a c. (G |= c) ==> (G ^ ' a |= c)) /\
 3: (!G a c. (G ^ ' a ^ ' a |= c) ==> (G ^ ' a |= c)) /\
 4: (!G D a c. (G |= a) /\ (D ^ ' a |= c) ==> (G ^ D |= c)) /\
 5: (!G D a b. (G |= a) /\ (D |= b) ==> (G ^ D |= a % b)) /\
 6: (!G a b c. (G ^ ' a |= c) ==> (G ^ ' (a % b) |= c)) /\
 7: (!G a b c. (G ^ ' b |= c) ==> (G ^ ' (a % b) |= c)) /\
 8: (!G D a b c. (G ^ ' b |= c) /\ (D |= a) ==> (G ^ D ^ ' (a --> b) |= c)) /\
 9: (!G a b. (G ^ ' a |= b) ==> (G |= (a --> b)))
10: ` ;;

We now break up the definition into the individual rules. We also do some pre-processing to get them ready to be used as (embedded) “meta-rules”. We keep unprocessed, primed versions of the rules as well, to demonstrate how a proof would work out using vanilla HOL Light.

let [pID;
     pW; pC; pCut; 
     pX_R; pX_L1; pX_L2;
     pI_L; pI_R
    ] = 
  map (MIMP_RULE o SPEC_ALL o REWRITE_RULE[IMP_CONJ]) 
    (CONJUNCTS propRULES);;

let [pID';
     pW'; pC'; pCut'; 
     pX_R'; pX_L1'; pX_L2';
     pI_L'; pI_R'
    ] = (CONJUNCTS propRULES);;

Set the goal:

g `mempty |= X % Y --> Y % X` ;;

Warning: Free variables in goal: X, Y
val it : goalstack = 1 subgoal (1 total)

`mempty |= X % Y --> Y % X`

Apply R-->:

e (MATCH_MP_TAC pI_R');;

val it : goalstack = 1 subgoal (1 total)

`mempty^' (X % Y) |= Y % X`

Now we want to apply contraction:

pC';;

val it : thm = |- !G a c. G^' a^' a |= c ==> G^' a |= c

We are lucky that, thanks to the empty multiset, the rule matches directly so that:

• G = mempty
• a = X % Y
• c = Y % X

e (MATCH_MP_TAC pC');;

val it : goalstack = 1 subgoal (1 total)

`mempty^' (X % Y)^' (X % Y) |= Y % X`

Now we want to apply RX:

pX_R';;

val it : thm = |- !G D a b. G |= a /\ D |= b ==> G^D |= a % b

This time we are not as lucky. We want the left-hand side of the turnstile in the goal to match the form G^D. If we apply the rule directly we will get the following match:

• G = mempty
• D = ' (X % Y)^' (X % Y)

The result is not what we want:

e (MATCH_MP_TAC pX_R');;

val it : goalstack = 1 subgoal (1 total)

`mempty |= Y /\ ' (X % Y)^' (X % Y) |= X`

So we backtrack. We can use the MUNION_EMPTY2 to get rid of the empty multiset:

b();;
MUNION_EMPTY2;;

val it : thm = |- (mempty^M) = M

So we use rewritting:

e (REWRITE_TAC[MUNION_EMPTY2]);;

val it : goalstack = 1 subgoal (1 total)

`' (X % Y)^' (X % Y) |= Y % X`

Now the rule will give us what we wanted:

e (MATCH_MP_TAC pX_R');;

val it : goalstack = 1 subgoal (1 total)

`' (X % Y) |= Y /\ ' (X % Y) |= X`

We use CONJ_TAC to break our conjunction to 2 subgoals:

e (CONJ_TAC);;

val it : goalstack = 2 subgoals (2 total)

`' (X % Y) |= X`

`' (X % Y) |= Y`

Now we want to use the L2X rule:

pX_L2';;

val it : thm = |- !G a b c. G^' b |= c ==> G^' (a % b) |= c

…but we can’t, because we have nothing to match to G:

e (MATCH_MP_TAC pX_L2');;

Exception: Failure "MATCH_MP_TAC: No match".

We need to add an empty multiset, so that G = mempty. One way to do this is by introducing the exact form that we want as a subgoal. We use rewritting with MUNION_EMPTY2 to prove that the new subgoal is equivalent to the original:

e (SUBGOAL_THEN (`mempty ^ '(X % Y) |= Y`)
     (fun th -> ACCEPT_TAC (REWRITE_RULE[MUNION_EMPTY2] th)));;

val it : goalstack = 1 subgoal (2 total)

`mempty^' (X % Y) |= Y`

Now we can use the rule:

e (MATCH_MP_TAC pX_L2');;

val it : goalstack = 1 subgoal (2 total)

`mempty^' Y |= Y`

Getting rid of the empty multiset again, as ID will not like it:

e (REWRITE_TAC[MUNION_EMPTY2]);;

val it : goalstack = 1 subgoal (2 total)

`' Y |= Y`

The identity rule completes this branch of the proof:

e (MATCH_ACCEPT_TAC pID);;

val it : goalstack = 1 subgoal (1 total)

`' (X % Y) |= X`

The second branch is symmetrical:

e (SUBGOAL_THEN (`mempty ^ '(X % Y) |= X`)
     (fun th -> ACCEPT_TAC (REWRITE_RULE[MUNION_EMPTY2] th)));;
e (MATCH_MP_TAC pX_L1' THEN REWRITE_TAC[MUNION_EMPTY2] THEN MATCH_ACCEPT_TAC pID);;

val it : goalstack = No subgoals

Our proof is complete, so we can reconstruct the theorem we just proved. This also validates the whole proof:

top_thm();;

val it : thm = |- mempty |= X % Y --> Y % X

We reset the goal to the initial state. This time we will use our library:

g `mempty |= X % Y --> Y % X` ;;

Warning: Free variables in goal: X, Y
val it : goalstack = 1 subgoal (1 total)

`mempty |= X % Y --> Y % X`

The sequence of the rules is exactly the same, starting with R-->.

The eseq command is an extension of e for our extended (embedded *seq*uent calculus) tactics.

The ruleseq tactic uses any embedded sequent calculus rule in a backwards reasoning step (as MATCH_MP_TAC does):

eseq (ruleseq pI_R);;

val it : goalstack = 1 subgoal (1 total)

`' (X % Y) |= Y % X`

No empty multisets appear this time. Now we can use C directly:

eseq (ruleseq pC);;

val it : goalstack = 1 subgoal (1 total)

`' (X % Y)^' (X % Y) |= Y % X`

Again, no empty multiset to clutter our goal. We can use RX and it will match directly:

eseq (ruleseq pX_R);;

val it : goalstack = 2 subgoals (2 total)

`' (X % Y) |= X`

`' (X % Y) |= Y`

Notice that the subgoals were also split automatically without explicit CONJ_TAC.

Even though we are in the same state as before, without an empty multiset to match G, we can apply L2X with no problems:

eseq (ruleseq pX_L2);;

val it : goalstack = 1 subgoal (2 total)

`' Y |= Y`

And finish it off with ID:

eseq (ruleseq pID);;

val it : goalstack = 1 subgoal (1 total)

`' (X % Y) |= X`

Symmetrically for the second branch:

eseq (ruleseq pX_L1);;
eseq (ruleseq pID);;

val it : goalstack = No subgoals

The proof validates fine, and we get the same theorem:

top_thm();;

val it : thm = |- mempty |= X % Y --> Y % X

Now, let’s revisit this goal:

g `' (X % Y)^' (X % Y) |= Y % X` ;;

Warning: Free variables in goal: X, Y
val it : goalstack = 1 subgoal (1 total)

`' (X % Y)^' (X % Y) |= Y % X`

In vanilla HOL Light we had an extra mempty lying around, so applying RX gave us the match G = mempty. Using our library there is no empty multiset to match to G.

The question is, what if we actually wanted G to be matched to an empty multiset and all of the rest of the context to go into D?

We can still do this by explicitly instantiating our rule, using rule_seqtac:

eseq (rule_seqtac [`D`,`' (X % Y)^' (X % Y)`] pX_R) ;;

Warning: inventing type variables
val it : goalstack = 2 subgoals (2 total)

`' (X % Y)^' (X % Y) |= X`

`mempty |= Y`

Note that we have provided no typing information for D, X, or Y, yet the system did not complain. It figured out and instantiated the types on its own.

We could also instantiate G to mempty. However, we do need to provide the type of mempty in that case, because it cannot be found in the goal and we can therefore not determine its type automatically:

b();;
eseq (rule_seqtac [`G`,`mempty:(Prop)multiset`] pX_R) ;;

Warning: inventing type variables
Warning: inventing type variables
val it : goalstack = 2 subgoals (2 total)

`' (X % Y)^' (X % Y) |= X`

`mempty |= Y`

Even though there was no mempty in the original goal, the system managed to apply the rule as we wanted.

We begin by defining the lambda terms as a recursive type Lambda:

let lamINDUCT,lamRECURSION = define_type
                               " Lambda = Var A
                                | App Lambda Lambda
                                | Prod (Lambda#Lambda)
                                | Lam A Lambda
                                ";; 

Our type is polymorphic to the type of the variable names. Typically this will be a string, but it alternative types may be used to facilitate substitutions, freshness conditions, etc.

We add @@ as an infix operator for function application (App):

parse_as_infix("@@",(10,"right"));; 
override_interface("@@",`App`);;

Normally projections would be primitively defined as part of the syntax. Cut elimination then yields their functionality. We are only working on shallow embeddings and object-level reasoning. We cannot perform cut elimination at this level. Because of this, we define projections as functions, so that they are more practical.

The definitions rely on FST and SND which are functions over pairs in HOL Light. Constant and function names in HOL Light are case sensitive, so we can use Fst and Snd:

let lamFst_DEF = new_recursive_definition lamRECURSION 
                   `Fst (Prod x :(A)Lambda) = FST x` ;; 

let lamFst = prove (`!x y. Fst (Prod (x,y)) = x`, REWRITE_TAC[lamFst_DEF;FST]);;


let lamSnd_DEF = new_recursive_definition lamRECURSION 
                   `Snd (Prod x :(A)Lambda) = SND x` ;; 

let lamSnd = prove (`!x y. Snd (Prod (x,y)) = y`, REWRITE_TAC[lamSnd_DEF;SND]);;

We want to be able to annotate lambda terms with propositions as types. We actually make this a little more general than that, so we can annotate any term with types:

let tmINDUCT,tmRECURSION = define_type "TTerm = Annotate A Prop";; 

Using a variable type A makes the defined TTerm polymorphic. For lambdas, the type will be ((A)Lambda)TTerm for some A (the type of variable names).

We add :: as an infix typing operator (we cannot use : because it is the HOL Light typing operator):

parse_as_infix("::",(16,"right"));;
override_interface("::",`Annotate`);;

In HOL Light, it is fairly easy to install a custom printer that hides the lambda terms from our proofs. This makes it easier to focus on the logical proof without worrying about the computational terms:

let chTermString tm =
  try 
    let c,args = strip_comb tm in
    let op = (fst o dest_const) c in
    if (String.equal op "Annotate") 
    then (string_of_term o hd o tl) args 
    else failwith ""
  with Failure _ -> failwith "Not a Curry-Howard term." ;;

let print_chTerm fmt = pp_print_string fmt o chTermString ;;

let hide_lam,show_lam =
  (fun () -> install_user_printer ("print_chTerm",print_chTerm)),
  (fun () -> try delete_user_printer "print_chTerm"
             with Failure _ -> failwith ("show_procs: " ^
                                           "Curry-Howard lambda terms are already being shown normally."));;

hide_lam();;

We can hide lambda terms using hide_lam() or re-enable them using show_lam().

As before, we introduce an infix operator for logical consequence, i.e. the “turnstile”. We use a different symbol so that both embedding can co-exist:

parse_as_infix("|==",(11,"right"));;

We introduce the inference rules in the same way and order as before:

1. Identity (ID)
2. Weakening (W)
3. Contraction (C)
4. Cut (Cut)
5. Conjunction Right (RX)
6. Conjunction Left1 (L1X)
7. Conjunction Left2 (L2X)
8. Implication Left (L-->)
9. Implication Right (R-->)

 0: let chRULES,chINDUCT,chCASES = new_inductive_definition 
 1: `(!a x. ' (x :: a) |== x :: a) /\
 2: (!G a c x z. (G |== z :: c) ==> (G ^ ' (x :: a) |== z :: c)) /\
 3: (!G a c x z. (G ^ '(x :: a) ^ '(x :: a) |== z :: c) ==> (G ^ ' (x :: a) |== z :: c)) /\
 4: (!G D a c x z. (G |== z :: a) /\ (D ^ ' (z :: a) |== x :: c) ==> (G ^ D |== x :: c)) /\
 5: (!G D a b x y. (G |== x :: a) /\ (D |== y :: b) ==> (G ^ D |== Prod (x,y) :: (a % b))) /\
 6: (!G a b c x z. (G ^ ' (Fst x :: a) |== (z :: c)) ==> (G ^ ' (x :: (a % b)) |== (z :: c))) /\
 7: (!G a b c x z. (G ^ ' (Snd x :: b) |== (z :: c)) ==> (G ^ ' (x :: (a % b)) |== (z :: c))) /\
 8: (!G D a b c f y z. (G ^ ' ((f @@ y) :: b) |== z :: c) /\ (D |== (y :: a)) ==> (G ^ D ^ ' (f :: (a --> b)) |== z :: c)) /\
 9: (!G a b x y. (G ^ ' (Var x :: a) |== (y :: b)) ==> (G |== Lam x y :: (a --> b)))
10: ` ;;

The only difference is that we use annotated terms (~TTerm~s) instead of propositions (~Prop~s), so we include the corresponding Curry-Howard terms in each rule.

As before, we break up and pre-process our rules, ready for use in our system:

let [chID;
     chW; chC; chCut; 
     chX_R; chX_L1; chX_L2;
     chI_L; chI_R
    ] = 
  map (MIMP_RULE o SPEC_ALL o REWRITE_RULE[IMP_CONJ]) 
    (CONJUNCTS chRULES);;

If we are doing construction proofs, it help to be able to instantiate variables of type Lambda easily using metavariables from the proof state. These shortcut methods greatly facilitate this:

let lamConstruct p st = 
  let construct m =
    if (String.equal p ((fst o dest_var) m)) 
    then instantiate (top_inst st) m
    else failwith "Not found!" in
  tryfind construct (top_metas st);;

let top_constr s = lamConstruct s (p());;

Finally, we mentioned earlier how we sometimes need to provide a typed mempty. Our types have started becoming quite verbose (and are still variable), so we write a quick function to make this easier:

let chEmpty ty = inst [ty,`:A`] `mempty:(((A)Lambda)TTerm)multiset` ;;

Now we are ready to do some proofs!

We revisit the same proof from before. Now we want to find which lambda term matches this particular type. We use existential quantification at the meta-level (HOL):

g `?P. mempty |== P :: (X % Y --> Y % X)` ;;

Warning: inventing type variables
Warning: Free variables in goal: X, Y
val it : goalstack = 1 subgoal (1 total)

`?P. mempty |== X % Y --> Y % X`

The META_EXISTS_TAC tactic gets rid of the the existential quantifier, but adds the variable P as a metavariable. This allows us to instantiate it as the proof progresses:

e (META_EXISTS_TAC);;

val it : goalstack = 1 subgoal (1 total)
Metas: `(P:(?125766)Lambda)`;

`mempty |== X % Y --> Y % X`

The rest of the proof progresses exactly as before. Especially given that we have hidden the lamdba terms, there is virtually no difference in the proof process:

eseq (ruleseq chI_R);;

val it : goalstack = 1 subgoal (1 total)
Metas: `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

`' X % Y |== Y % X`

eseq (ruleseq chC);; 

val it : goalstack = 1 subgoal (1 total)
Metas: `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

`' X % Y^' X % Y |== Y % X`

Do not be fooled, however. This is Curry-Howard in all its glory!

show_lam();;
p();;

val it : goalstack = 1 subgoal (1 total)
Metas: `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

`' (Var x0 :: (X % Y))^' (Var x0 :: (X % Y)) |== y0 :: (Y % X)`

eseq (ruleseq chX_R);;

val it : goalstack = 2 subgoals (2 total)
Metas: `(x2:(?125766)Lambda)`; `(y2:(?125766)Lambda)`; `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

`' (Var x0 :: (X % Y)) |== y2 :: X`

`' (Var x0 :: (X % Y)) |== x2 :: Y`

eseq (ruleseq chX_L2);; 

val it : goalstack = 1 subgoal (2 total)
Metas: `(x2:(?125766)Lambda)`; `(y2:(?125766)Lambda)`; `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

`' (Snd (Var x0) :: Y) |== x2 :: Y`

eseq (ruleseq chID);; 

val it : goalstack = 1 subgoal (1 total)
Metas: `(x2:(?125766)Lambda)`; `(y2:(?125766)Lambda)`; `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

`' (Var x0 :: (X % Y)) |== y2 :: X`

We can hide the lambda terms again at any point.

hide_lam();;
eseq (ruleseq chX_L1);;
eseq (ruleseq chID);;

val it : goalstack = No subgoals
Metas: `(x2:(?125766)Lambda)`; `(y2:(?125766)Lambda)`; `(x0:?125766)`; `(y0:(?125766)Lambda)`; `(P:(?125766)Lambda)`;

Our proof is complete and we can generate out theorem, though the existential quantifier makes is hardly usable. Validating the proof, however, is quite important, to ensure the delayed metavariable instantiation are still sound:

top_thm();;

val it : thm = |- ?P. mempty |== X % Y --> Y % X

What is more interesting is that we can instantiate the original metavariable P to construct our lamdba term:

top_constr "P";;

val it : term = `Lam x0 (Prod (Snd (Var x0),Fst (Var x0)))`

This is a direct translation of the proof we just performed into lambda calculus! It is a function that takes an argument x0 (assumed to be a product) and returns a product with x0’s elements flipped (Snd followed by Fst). This was all constructed automatically for us.

If we replace P in the previous goal with the term we constructed, we can start a type-checking proof, to prove that P does indeed have the right type:

g `mempty |== Lam x (Prod (Snd (Var x),Fst (Var x))) :: (X % Y --> Y % X)` ;;

Warning: inventing type variables
Warning: Free variables in goal: X, Y, x
val it : goalstack = 1 subgoal (1 total)

`mempty |== X % Y --> Y % X`

We can follow the exact same proof as before:

eseq (ruleseq chI_R);;
eseq (ruleseq chC);;
eseq (ruleseq chX_R);;
eseq (ruleseq chX_L2);;
eseq (ruleseq chID);;
eseq (ruleseq chX_L1);;
eseq (ruleseq chID);;

val it : goalstack = No subgoals

And once we are done, we can obtain a theorem, proving our type is correct:

show_lam();;
top_thm();;

val it : thm =
  |- mempty |== Lam x (Prod (Snd (Var x),Fst (Var x))) :: (X % Y --> Y % X)

hide_lam();;

So far, we have been looking at interactive proofs. Our tactics can be packaged in the traditional HOL Light style. However, we use our own, extended tacticals, which unfortunately cannot be infix (at least until we find a way to add this to camlp5).

Here is a packaged proof of commutativity of conjunction (without the implication this time):

let TIMES_COMM = prove_seq( `' (a :: (X % Y)) |== Prod (Snd a, Fst a) :: (Y % X)` ,
                            ETHENL 
                              (ETHEN (ruleseq chC) (ruleseq chX_R))
                              [
                                ETHEN (ruleseq chX_L2) (ruleseq chID);
                                ETHEN (ruleseq chX_L1) (ruleseq chID) ]
                   );;

Warning: inventing type variables
val TIMES_COMM : thm = |- ' (a :: (X % Y)) |== Prod (Snd a,Fst a) :: (Y % X)

Lemmas like this are only useful if we can employ them in other proofs. Given our convenient tactics, it would be nice if we could use lemmas like this to derive new inference rules.

In this particular case, we can construct an inference rule that commutes a conjunction on the right-hand side (and later on the left-hand side) of the sequent. The rule can be expressed like this:

`G |== a :: (X % Y) ===> G |== b :: (Y % X)`

The question is, what is the appropriate Curry-Howard translation for this rule? In other words, what should the lambda terms a and b be?

A construction proof can give the answer quite easily:

g `?a:(A)Lambda b. G |== a :: (X % Y) ===> G |== b :: (Y % X)` ;;
e (REPEAT META_EXISTS_TAC);;
e (MDISCH_TAC);;

val it : goalstack = 1 subgoal (1 total)
Metas: `(a:(A)Lambda)`; `(b:(A)Lambda)`;

  0 [`G |== X % Y`]

`G |== Y % X`

Note that MDISCH_TAC is an Isabelle Light tactic. It is the same as DISCH_TAC, but for our special meta-implication.

At this point we need to make smart use of Cut in order to apply our TIMES_COMM lemma. Doing this in vanilla HOL Light would be quite tedious. Our rule instantiation mechanics make it very easy:

eseq (drule_seqtac [`c`,`Y % X`;`D`,chEmpty `:A`] chCut);; (* cut! *)

Warning: inventing type variables
Warning: inventing type variables
val it : goalstack = 2 subgoals (2 total)
Metas: `(x0:(A)Lambda)`; `(a:(A)Lambda)`; `(b:(A)Lambda)`;

  0 [`G |== Y % X`]

`G |== Y % X`

`' X % Y |== Y % X`

Now the first (bottom) goal matches our lemma exactly, whereas the second one matches the assumption. Then we are done!

eseq (ruleseq TIMES_COMM);; (* Using the lemma we proved earlier *)
eseq (seqassumption);;
top_thm();;

val it : thm = |- ?a b. G |== X % Y ===> G |== Y % X

Based on this proof, a is just itself:

top_constr "a" ;; 

val it : term = `a`

And given that, b should be a with the elements swapped:

top_constr "b" ;; 

val it : term = `Prod (Snd a,Fst a)`

Replace the constructed a and b in the original goal, and package the proof:

let chTimesCommR = prove_seq (`G |== a:(A)Lambda :: (X % Y) ===>
                                         G |== Prod (Snd a,Fst a) :: (Y % X)` ,
                                       ETHENL ( ETHEN
                                                  (ETAC (MDISCH_TAC))
                                                  (drule_seqtac [`c`,`Y % X`;`D`,chEmpty `:A`] chCut) ) [
                                           ruleseq TIMES_COMM;
                                           seqassumption]);;

Warning: inventing type variables
Warning: inventing type variables
val chTimesCommR : thm = |- G |== X % Y ===> G |== Y % X

And voila! A brand new, derived inference rule!

Let’s do the same for the left-hand side. First construct our lambda terms:

g `?a:(A)Lambda b. G ^ ' (a :: (X % Y)) |== z :: C  ===> G ^ ' (b :: (Y % X)) |== z :: C` ;;
e (REPEAT META_EXISTS_TAC);;
e (MDISCH_TAC);;
eseq (rule_seqtac [`a`,`X % Y`;`G`,`' (b :: (Y % X))`] chCut);;
eseq (ruleseq TIMES_COMM);;
eseq (seqassumption);;
top_thm();;
top_constr "a";;

val it : term = `Prod (Snd b,Fst b)`

And then instantiate the rule and package the proof:

show_lam();;
let chTimesCommL = prove_seq (`G ^ ' (Prod (Snd a,Fst a) :: (X % Y)) |== z :: C  ===>
                                G ^ ' (a :: (Y % X)) |== z :: C` ,
                              ETHENL ( ETHEN
                                         (ETAC (MDISCH_TAC))
                                         (rule_seqtac [`a`,`X % Y`;`G`,`' (a :: (Y % X))`] chCut) ) [
                                  ruleseq TIMES_COMM;
                                  seqassumption]);;

Warning: inventing type variables
Warning: inventing type variables
Warning: inventing type variables
Warning: inventing type variables
val chTimesCommL : thm =
  |- G^' (Prod (Snd a,Fst a) :: (X % Y)) |== z :: C ===>
     G^' (a :: (Y % X)) |== z :: C

We can do the same without explicitly stating the computational terms we want to construct. This way, if we change anything in the correspondence, the lemma will still be proven:

let chTimesCommL = constr_prove (`?a b. G ^ ' (b :: (X % Y)) |== z :: C  ===>
                                   G ^ ' (a :: (Y % X)) |== z :: C` ,
                                 ETHENL ( ETHEN (SEQTAC MDISCH_TAC)
                                            (rule_seqtac [`a`,`X % Y`;`G`,`' (a :: (Y % X))`] chCut) ) 
                                   [
                                     ruleseq TIMES_COMM;
                                     seqassumption
                                   ]
                     );;

Warning: inventing type variables
Warning: inventing type variables
Warning: inventing type variables
Warning: inventing type variables
val chTimesCommL : thm =
  |- G^' (Prod (Snd a,Fst a) :: (X % Y)) |== z :: C ===>
     G^' (a :: (Y % X)) |== z :: C

Now that we have 2 new inference rules, let’s see them in action in a new proof:

hide_lam();;
g `? P. mempty |== P :: (((A % B) % C) --> (C % (B % A)))` ;;
e (REPEAT META_EXISTS_TAC);;
eseq (ruleseq chI_R);;

val it : goalstack = 1 subgoal (1 total)
Metas: `(x0:?126376)`; `(y0:(?126376)Lambda)`; `(P:(?126376)Lambda)`;

`' (A % B) % C |== C % B % A`

Let’s swap things on the right-hand side:

eseq (ruleseq chTimesCommR);;

val it : goalstack = 1 subgoal (1 total)
Metas: `(a1:(?126376)Lambda)`; `(x0:?126376)`; `(y0:(?126376)Lambda)`; `(P:(?126376)Lambda)`;

`' (A % B) % C |== (B % A) % C`

Keep going:

eseq (ruleseq chC);;
eseq (ruleseq chX_R);;

eseq (ruleseq chX_L1);;

val it : goalstack = 1 subgoal (2 total)
Metas: `(x3:(?126376)Lambda)`; `(y3:(?126376)Lambda)`; `(a1:(?126376)Lambda)`; `(x0:?126376)`; `(y0:(?126376)Lambda)`; `(P:(?126376)Lambda)`;

`' A % B |== B % A`

The perfect goal to use chTimesCommL:

eseq (ruleseq chTimesCommL);;

val it : goalstack = 1 subgoal (2 total)
Metas: `(x3:(?126376)Lambda)`; `(y3:(?126376)Lambda)`; `(a1:(?126376)Lambda)`; `(x0:?126376)`; `(y0:(?126376)Lambda)`; `(P:(?126376)Lambda)`;

`' B % A |== B % A`

The rest is straightforward:

eseq (ruleseq chID);;

eseq (ruleseq chX_L2);;
eseq (ruleseq chID);;

top_thm();;

val it : thm = |- ?P. mempty |== (A % B) % C --> C % B % A

And why not construct the lambda term for this slightly more complex type?

top_constr "P";; 

val it : term =
  `Lam x0
   (Prod
   (Snd (Prod (Prod (Snd (Fst (Var x0)),Fst (Fst (Var x0))),Snd (Var x0))),
    Fst (Prod (Prod (Snd (Fst (Var x0)),Fst (Fst (Var x0))),Snd (Var x0)))))`

Due to the (implicit) cuts, our constructed term can be reduced with rewritting:

REWRITE_CONV[lamFst;lamSnd] (top_constr "P");; 

val it : thm =
  |- Lam x0
     (Prod
     (Snd (Prod (Prod (Snd (Fst (Var x0)),Fst (Fst (Var x0))),Snd (Var x0))),
      Fst (Prod (Prod (Snd (Fst (Var x0)),Fst (Fst (Var x0))),Snd (Var x0))))) =
     Lam x0
     (Prod (Snd (Var x0),Prod (Snd (Fst (Var x0)),Fst (Fst (Var x0)))))

If Fst and Snd were primitive constructors, we would not be able to use rewritting like this, nor can we define a notion of cut elimination.

We could also define function application as a function in HOL instead of a primitive constructor. However, this would require a definition of variable substitution, which in turn would require managing bound variables. This is notoriously hard, especially with the limited features of HOL Light, and therefore beyond the scope of our tutorial. Other theorem provers (such as Isabelle or HOL4) which support appropriate mechanisms (Higher Order Abstract Syntax, de Bruijn indexes etc.) would be more suitable for this purpose.