(* We are going to prove some properties of list operations in hol. *)
(* There is already an excelleent built-in type list in hol, but we *)
(* don't want to use that because it has all the theorems that we *)
(* want to prove built-in. *)
let list2ind, list2rec = define_type "list2 = nil | const X list2";;
(* Note that we have defined a polymorphic type, because the type of X *)
(* was not specified. *)
(* This is quite risky, because dealing with type variables has proven *)
(* itself problematic in the past. *)
(* Now list2rec = |- !f0 f1.
?fn. fn nil = f0 /\ (!a0 a1. fn (const a0 a1) = f1 a0 a1 (fn a1)))
*)
(* We define append, and reverse *)
(* The definition of append: *)
(* The built-in function is called APPEND, so we can *)
(* safely call it append. *)
(* The @-symbol denotes the eps operator. I will explain it in the *)
(* lecture. *)
let lambda_append =
` \ ( app : (X)list2 -> (X)list2 -> (X)list2 ).
( app nil = ( \li. li )) /\
( ! el li. ( app ( const el li )) =
( \li2 . ( const el ( app li li2 ))))`;;
let defappend =
( mk_binder "@" ( (bndvar lambda_append),(body lambda_append)));;
let defappend = ( mk_eq ( `append:(X)list2 -> (X)list2 -> (X)list2`,
defappend ));;
(* This is somewhat of a disappointment. The types should have *)
(* been unified automatically. *)
let defappend = define defappend;;
(* We want to prove the characteristic axioms of append: *)
let app = ISPEC ` \ (x:(X)list2). x ` list2rec ;;
let t = bndvar( rand ( concl app ));;
(* t is not used in the proof, but it allows to see the type *)
(* variable. *)
let app = ISPEC ` ( \ (e:X) (l:(X)list2)
(f:((X)list2 -> (X)list2)).
( \li2. ( const e ( f li2 ))))` app;;
(* X is a type variable. So it is possible to insert type variables. *)
(* ISPEC is willing to instantiate type variables in the theorem, *)
(* but it refuses to instantiate type variables in the term. *)
let app = CONV_RULE ( TOP_DEPTH_CONV BETA_CONV ) app;;
(* This does some beta-reductions in app. *)
(* This is app2 with ?fn replaced by append. *)
g ( mk_icomb (lambda_append,
`append:(X)list2 -> (X)list2 -> (X)list2` ));;
(* Believe it or not, but the declaration *)
(* (X)list2 -> (X)list2 -> (X) list2 *)
(* is essential for provability. Strange *)
e( REWRITE_TAC [ defappend ] );;
e( CONV_TAC ( TOP_DEPTH_CONV BETA_CONV ));;
let sel = ISPEC lambda_append SELECT_AX;;
let sel = CONV_RULE ( TOP_DEPTH_CONV BETA_CONV ) sel;;
e( CHOOSE_TAC app );;
(* Now we need to instantiate variable x in sel with the right type, *)
(* which is extremely difficult. We will need to extract it *)
(* from the goal. *)
let gg = top_goal( );;
let pp,cc = gg;;
let [pp] = pp;;
let pp = ( rand ( rator pp ));;
let pp = ( rand ( rator pp ));;
let tt = ( rator pp );;
let sel = ( ISPEC `fn:(X)list2 -> (X)list2 -> (X)list2` sel );;
let sel = ( UNDISCH sel );;
e( ASSUME_TAC sel );;
e( ASM_REWRITE_TAC [] );;
let ap_thm = top_thm( );;
(* Next step is to prove the usual defining properties of append: *)
g ` ( ! (l1:(X)list2) . ( append nil l1 ) = l1 ) /\
( ! (e:X) l1 l2. ( append ( const e l1 ) l2 ) =
( const e ( append l1 l2 ))) `;;
e( CONJ_TAC );;
let aa = CONV_RULE ( TOP_DEPTH_CONV BETA_CONV ) ap_thm;;
e( ASM_REWRITE_TAC [aa] );;
e( ASM_REWRITE_TAC [aa] );;
let standappend = top_thm( );;
(* Next comes the definition of reverse: *)
let lambda_reverse =
` \ ( rev : (X)list2 -> (X)list2 ).
( rev nil = nil ) /\
( ! el li. ( rev ( const el li )) =
( append ( rev li ) ( const el nil )))`;;
let defreverse =
( mk_binder "@" ( (bndvar lambda_reverse),(body lambda_reverse )));;
let defreverse = ( mk_eq ( `reverse:(X)list2 -> (X)list2 `, defreverse ));;
(* See above. My disappointment did not become less. *)
let defreverse = define defreverse;;
(* We build up a goal stating that reverse satifies lambda_reverse *)
let rev = ISPEC ` ( nil :(X)list2 ) ` list2rec ;;
let rev = ISPEC ` ( \ (e:X) (l:(X)list2) (r: (X)list2 ).
( append r ( const e nil )))` rev;;
let rev = CONV_RULE ( TOP_DEPTH_CONV BETA_CONV ) rev;;
g( mk_icomb ( lambda_reverse, `reverse:(X)list2 -> (X)list2 ` ));;
(* and prove the goal: *)
e( REWRITE_TAC [ defreverse ] );;
e( CONV_TAC ( TOP_DEPTH_CONV BETA_CONV ));;
e( CHOOSE_TAC rev );;
let sel = ISPEC lambda_reverse SELECT_AX;;
let sel = CONV_RULE ( TOP_DEPTH_CONV BETA_CONV ) sel;;
let sel = ( ISPEC `fn:(X)list2 -> (X)list2` sel );;
let sel = ( UNDISCH sel );;
e( ASSUME_TAC sel );;
e( ASM_REWRITE_TAC [] );;
let rev_thm = top_thm( );;
(* Now we can prove the standard axioms of reverse: *)
(* This is very easy: *)
let standreverse = ( CONV_RULE ( TOP_DEPTH_CONV BETA_CONV ) rev_thm );;
(* Let's do some little theorems: *)
(* Associativity of append: *)
g ` ! ( l1: (X)list2 ) ( l2: (X)list2 ) ( l3: (X)list2 ).
( append l1 ( append l2 l3 )) = ( append ( append l1 l2 ) l3 ) `;;
(* It is proven by induction on l1. *)
(* Instantiate list2ind with *)
(* lambda l1 all l2, l3: *)
(* ( append l1 ( append l2 l3 )) = ( append ( append l1 l2 ) l3 ) *)
(* beta-reduce the result, and use it to prove the current goal. *)
e( MATCH_MP_TAC ( CONV_RULE ( TOP_DEPTH_CONV BETA_CONV )
( ISPEC `\ ( l1:(X)list2 ). ! ( l2: (X)list2 ) ( l3: (X)list2 ).
( append l1 ( append l2 l3 )) = ( append ( append l1 l2 ) l3 ) `
list2ind )));;
(* The present goal is a conjunction, resulting from the premiss of *)
(* list2ind after instantiation. *)
e( CONJ_TAC THEN ( REPEAT STRIP_TAC ) THEN
( ASM_REWRITE_TAC [ standappend ] ));;
let assocappend = top_thm( );;
(* ( append l nil ) = l. *)
g ` ! ( l: (X) list2 ). ( append l nil ) = l `;;
(* By induction on l: *)
e( MATCH_MP_TAC ( CONV_RULE ( TOP_DEPTH_CONV BETA_CONV )
( ISPEC ` \ ( l:(X)list2 ). ( append l nil ) = l ` list2ind )));;
e( CONJ_TAC THEN ( REPEAT STRIP_TAC ) THEN
( ASM_REWRITE_TAC [ standappend ] ));;
(* We add the result to standappend, because it is so fundamental: *)
let standappend = ( CONJ standappend ( top_thm( ) ));;
(* reverse permutes with append: *)
g ` ! ( l1: (X) list2 ) ( l2: (X) list2 ).
( reverse ( append l1 l2 )) = ( append ( reverse l2 ) ( reverse l1 )) `;;
(* This is proven by induction on l1. *)
e( MATCH_MP_TAC ( CONV_RULE ( TOP_DEPTH_CONV BETA_CONV )
( ISPEC ` \ ( l1:(X)list2 ). ! ( l2:(X)list2 ).
( reverse ( append l1 l2 )) = ( append ( reverse l2 ) ( reverse l1))`
list2ind )));;
e( CONJ_TAC THEN ( REPEAT STRIP_TAC ) THEN
( ASM_REWRITE_TAC [ assocappend;standappend; standreverse ] ));;
let revappend = top_thm( );;
g ` ! ( l: (X)list2 ). ( reverse ( reverse l )) = l `;;
(* induction? *)
e( MATCH_MP_TAC ( CONV_RULE ( TOP_DEPTH_CONV BETA_CONV )
( ISPEC ` \ ( l:(X)list2 ).
( reverse ( reverse l )) = l ` list2ind )));;
e( CONJ_TAC THEN ( REPEAT STRIP_TAC ) THEN
( ASM_REWRITE_TAC [ assocappend; standappend;
standreverse; revappend ] ));;
let revrev = top_thm( );;