5.3 Equational reasoning (1)

　HOL Lightにおいて等式は，数学におけるそれよりも特に基本的です．例えば，Iffは=記号にしても構いません．ただし，結合の強さと向き，typeの推量機能のため，時に括弧が必要です．

`p /\ x = 1 <=> q`;;
val it : term = `p /\ x = 1 <=> q`
`p /\ x = 1 = q`;;
val it : term = `p /\ (x <=> 1 = q)`
`p /\ (x = 1) = q`;;
val it : term = `p /\ (x = 1 <=> q)`
`(p /\ x = 1) = q`;;
val it : term = `p /\ x = 1 <=> q``

　順序対から等式を作る，逆に分解する，等式の左辺，右辺を参照する関数は，次の通りです．

let eq12 = mk_eq(`1`,`2`);;
val eq12 : term = `1 = 2`
dest_eq eq12;;
val it : term * term = (`1`, `2`)
lhs eq12;;
val it : term = `1`
rhs eq12;;
val it : term = `2`

　また，反射律，対称律，推移律という同値関係についての関数は，既に述べたREFLを含め，次の通りですが，引数のtypeの違いに注意してください．

REFL;;
val it : term -> thm =
SYM;;
val it : thm -> thm =
TRANS;;
val it : thm -> thm -> thm =

例えば

REFL `x` ;;
Warning: inventing type variables
val it : thm = |- x = x
REFL `x:num` ;;
val it : thm = |- x = x
REFL `x:bool` ;;
val it : thm = |- x <=> x

そして

SYM (ARITH_RULE `1+1=2`);;
val it : thm = |- 2 = 1 + 1
TRANS (ARITH_RULE `1+1=2`) (ARITH_RULE `2=0+2`);;
val it : thm = |- 1 + 1 = 0 + 2

となります．