On Fri, 23 Nov 2012, Alexey Solovyev wrote:
>> * Page 15:
>> move: {1}x a transforms the goal into !x1 a. a + x1 = x + 3, where
>> x1 is an automatically generated name.
>>
>> How does that compare to SSReflect by Gonthier? It is one of the very
>> few points where SSReflect and Isar agree, to have generated names
>> never intrude the proof text implicitly. Does that actually
>> happen above for HOL Light, or is it just the text confusing me?
>>
> I'm not sure how this is done in SSReflect/Coq since I rarely used this
> construction in my SSReflect/Coq proofs (in SSReflect/HOL Light, I'm not
> using it often either). The SSReflect manual shows a similar example with a
> similar outcome (see http://hal.inria.fr/inria-00258384, pages 27-28). I
> agree that this is not a good way to interfere with the proof. Usually, this
> construction is immediately followed by the introduction tactical => which
> replaces auto-generated names with user-provided names.
OK, I see the following on page 28 of the SSReflect/Coq manual:
forall n n0 : nat, n = n0 -> G.
where the name n0 is picked by the Coq display function, and assuming n
appeared only in G.
I shall probably ask Gonthier about it the next time I see him.
On the other hand, in rare situations even Isar violates its own
principles about intrusion of generated names into the proof, notably in
certain induction proofs.
Makarius
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
