# Embedding Example: Curry-Howard

## Table of Contents

## 1 Introduction

### 1.1 Loading the library

The library can be loaded with a simple command:

loads ("embed/sequent.ml");;

This includes a small theory of multisets.

### 1.2 Multiset notation

In an attempt to declutter multiset expressions, we adopt the following HOL Light notation:

`mempty`

: empty multiset- Single quote
`'`

: singleton multiset - e.g.`' 5`

is`{5}`

. - Hat
`^`

: multiset sum (munion) - e.g.`' 5 ^ ' 5 ^ ' 6`

is`{5,5,6}`

.

## 2 A Simple Logic

We embed a simple propositional logic, limited to conjunction and implication.

We will then try to prove a simple object-level theorem using vanilla HOL Light and our library.

### 2.1 Embedding

#### 2.1.1 Type Declaration

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`);;

#### 2.1.2 Inference rules

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:

- Identity (
`ID`

) - Weakening (
`W`

) - Contraction (
`C`

) - Cut (
`Cut`

) - Conjunction Right (
`RX`

) - Conjunction Left1 (
`L1X`

) - Conjunction Left2 (
`L2X`

) - Implication Left (
`L-->`

) - 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);;

### 2.2 Proofs

#### 2.2.1 Vanilla HOL Light

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

#### 2.2.2 Using our library

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

#### 2.2.3 Explicit Instantiation

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.

## 3 Curry-Howard

### 3.1 Embedding

#### 3.1.1 Lambda Terms

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]);;

#### 3.1.2 Type Annotations

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()`

.

#### 3.1.3 Inference Rules

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:

- Identity (
`ID`

) - Weakening (
`W`

) - Contraction (
`C`

) - Cut (
`Cut`

) - Conjunction Right (
`RX`

) - Conjunction Left1 (
`L1X`

) - Conjunction Left2 (
`L2X`

) - Implication Left (
`L-->`

) - 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!

### 3.2 Proofs

#### 3.2.1 A Construction Proof

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.

#### 3.2.2 A Type-checking Proof

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();;

#### 3.2.3 Proving and Reusing Lemmas

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.