John and Ramana, thanks again! It turns out that my problem was entirely
caused by my abstraction definition union replacement for UNION. This now
works (as part of 4200 lines of code formalizing Euclid up to Prop I.26, the
Alternate Interior Angles thm), since I switched back to UNION:
let SegmentSymmetry_THM = thm `;
let A B be point;
thus seg A B = seg B A
by Segment_DEF, IntervalSymmetry_THM, SET_RULE`;;
[...] solved at 173
val SegmentSymmetry_THM : thm = |- !A B. seg A B = seg B A
Below is an actual report (not of a bug) that indicates SET_RULE gets confused
by anything that's not defined in sets.ml. Everything works with UNION, but
nothing works with union. John wrote
Although [SET_RULE] can certainly prove `{A,B,C} = {B,A,C}` etc. as
a standalone goal, SET_RULE would not, for example, give you even
such simple generalizations as `P {A,B,C} ==> P {B,A,C}`.
I think my report below is an example of this.
It would be an interesting (and not necessarily easy) project to
extend its abilities like this. But it might be much easier to take
a more focused approach to dealing with this kind of permutation
(e.g. something akin to Brand's transformation, which is explained
a bit in my book).
Interesting! I think we're talking about general directions of improving miz3.
My hazy idea is that your holby.ml prover for miz3 "by" justifications ought
to do for sets everything that's analogous to what MESON already does for FOL.
I would tend to think your focused approach to permutations isn't general
enough, but I'm no expert. I did read some of your book, the Mizar-like
section, and it seemed to me that you said something really important: neither
of the following approaches is very good:
1) get the computer to go prove the theorem;
2) tell the the computer exactly how to go prove the theorem;
and the winning strategy is to combine (1) & (2). I liked that a lot, even
though right now I'm working almost entirely in (2), and I think it follows
logically that you want miz3 to be as powerful as possible, while the Mizar
folks seemed to desire Mizar to be relatively weak. If you could comment, it
might be helpful, as this matter came up while you were gone.
--
Best,
Bill
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
timeout := 50;;
SET_RULE `X = Y ==> {a, b} UNION X = {b, a} UNION Y `;;
let DoubletonSymmetry_THM = thm `;
let a b be A;
thus {a, b} = {b, a}
by SET_RULE`;;
let DoubletonXSymmetry_THM = thm `;
let a b be A;
let X be A->bool;
thus {a, b} UNION X = {b, a} UNION X
by SET_RULE`;;
let DoubletonPlusSymmetry_THM = thm `;
let a b be A;
let X Y be A->bool;
assume X = Y [H1];
thus {a, b} UNION X = {b, a} UNION Y
by SET_RULE, H1`;;
parse_as_infix("union",(16, "right"));;
let union = new_definition
`∀ s t:A->bool. s union t = λ x. x ∈ s ∨ x ∈ t`;;
SET_RULE `X = Y ==> {a, b} union X = {b, a} union Y `;;
let DoubletonXunionSymmetry_THM = thm `;
let a b be A;
let X be A->bool;
thus {a, b} union X = {b, a} union X
by SET_RULE`;;
let DoubletonPlusunionSymmetry_THM = thm `;
let a b be A;
let X Y be A->bool;
assume X = Y [H1];
thus {a, b} union X = {b, a} union Y
by SET_RULE, H1`;;
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
