On 27 May 2012, at 08:20, Bill Richter wrote:
> John, I'm over 400 lines now formalizing my Hilbert axiom paper
> http://www.math.northwestern.edu/~richter/hilbert.pdf (code below) and
> proved that being on the same side of a line defines an equivalence
> relation. This is really a lot of fun, and my son likes it too: the
> formalized mathematical proofs become more "concrete".
>
> I know you're real busy, but I have three questions. My first 6 lemmas
> here are all set-theory, and I wonder if I'm going about it the right
> way. Also, I couldn't figure out how to define an equivalence
> relation. It seems that there ought to be a way to define function
> ER: point#point->bool ---> bool
> (or something) testing if a relation is an equivalence relation.
HOL effectively lets you define the class of all equivalence relations. Thus:
let refl_def = new_definition
`Refl R = !x:'a. R x x`;;
let symm_def = new_definition
`Symm R = !x y:'a. R x y ==> R y x`;;
let trans_def = new_definition
`Trans R = !x y z:'a. R x y /\ R y z ==> R x z`;;
let equiv_rel_def = new_definition
`EquivRel R = (Refl R /\ Symm R /\ Trans R)`;;
(Here the fact that HOL is polymorphic is giving you much more expressivity in
practice than raw ZF set theory would give.)
After the above definitions, type_of`EquivRel` will evaluate to something like
`:(?83981->?83981->bool)->bool` where ?83981 is a type variable that can be
instantiated to any other type. In your case you can write `equiv_rel (\A B.
(A, B) same_side l)` to assert that the relationship of being on the same side
of the line l is an equivalence relation. However, you are going to need to do
something a bit trickier, since your axioms seem to be loose about whether `(A,
B) same_side l` holds if A or B is on the line l. So you will either need to
strengthen your axioms so that `(\A B. (A, B) same_side l)`becomes an
equivalence relation on the set of all points or generalise the above
definitions to the notion of an equivalence relation on a subset:
let refl_on_def = new_definition
`ReflOn R P = !x:'a. P x ==> R x x`;;
let symm_on_def = new_definition
`SymmOn R P = !x y:'a. P x /\ P y /\ R x y ==> R y x`;;
let trans_on_def = new_definition
`TransOn R P = !x y z:'a. P x /\ P y /\ P z /\ R x y /\ R y z ==> R x z`;;
let equiv_rel_on_def = new_definition
`EquivRelOn R P = (ReflOn R P /\ SymmOn R P /\ TransOn R P)`;;
So you can write `EquivRelOn (\A B. (A, B) same_side l) l`. (Given a free
choice, I would strengthen the axioms as it will simplify the proofs.)
> Below you can see my partly successful effort. Also, my axiom B3 is
> bulkier than I'd like. I want to say that exactly one of three things
> is true, so I wrote
> a \/ b \/ c /\ ~(a /\ b) /\ ~(a /\ c) /\ ~(b /\ c).
> Is there a nice HOL Light way to say this?
>
Well you could define a function on lists of truth values and use that. Thus:
let all_false_def = new_recursive_definition list_RECURSION
` (AllFalse [] = T)
/\ (AllFalse (CONS b bs) = (~b /\ AllFalse bs)) `;;
let one_true_def = new_recursive_definition list_RECURSION
` (OneTrue [] = F)
/\ (OneTrue (CONS b bs) = ((b /\ AllFalse bs) \/ (~b /\ OneTrue bs))) `;;
And then you can say things like `OneTrue [A = B; B = C; A = C]`. But I
suspect this won't make life any simpler for you because to reason with this
notation, you will probably just end up rewriting with the definitions as in:
REWRITE_CONV[one_true_def; all_false_def] `OneTrue [A = B; B = C; A = C]`;;
which returns:
|- OneTrue [A = B; B = C; A = C] <=>
A = B /\ ~(B = C) /\ ~(A = C) \/
~(A = B) /\ (B = C /\ ~(A = C) \/ ~(B = C) /\ A = C)
and so doesn't help with reducing the number of cases. John's "Without Loss Of
Generality" paper may give you some ideas
(http://www.cl.cam.ac.uk/~jrh13/papers/wlog.html) if case explosion is a big
problem for you, but I don't know how well that fits in with miz3.
Regards,
Rob.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
