Re: [Hol-info] How to reduce these lambda equations to F?

2017-08-07 Thread Chun Tian (binghe)
Thanks!Actually I was ever taught (by Thomas) to use FUN_EQ_THM to convert 
relation equations (R = R’) into provable forms (!x y. R x y = R’ x y), but 
when I was facing lambda functions I didn’t realize they’re essentially the 
same thing.   (Using PAT_X_ASSUM I can precisely target on any single 
assumptions, thus other assumptions won’t be affected)

And I found that, once I got ``!x. x = prefix (label l) x``, actually the 
`distinct` theorems generated by Datatype will directly lead it to False, no 
need to call the “size” theorems and use arithmetic stuff, although the latter 
idea also works.

—Chun

> Il giorno 07 ago 2017, alle ore 01:33, michael.norr...@data61.csiro.au ha 
> scritto:
> 
> I would use
> 
>   fs[FUN_EQ_THM]
> 
> to expand the assumptions to
> 
>   !x. x = prefix (label l) x
> 
> and
> 
>   !x. x = p
> 
> respectively.
> 
> Of course, this is a blunt weapon, so you may not wish to use it if other 
> assumptions are disrupted too much.
> 
> Michael
> 
> On 5/8/17, 04:25, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>This is the first time I met the following goal, in which one of the 
> assumptions should be able to reduce to F (then the goal is resolved):
> 
>R (λt. t)
>
>  4.  (λt. t) = (λt. prefix (label l) t)
> 
>The lambda function has the type of ``CCS -> CCS``, which CCS is my 
> datatype defined by HOL’s Define command.  “prefix” is an constructor of CCS 
> datatype.I *know* the equation doesn’t hold, because the whatever input 
> arguments, the resulting CCS on both side must have different “size”, simply 
> because one is the sub-expression of the other.   But how can I actually 
> reduce it to F?
> 
>The other case is a little different:
> 
>R (λt. t)
>
>  4.  (λt. t) = (λt. p)
> 
>The assumption "(λt. t) = (λt. p)” hold for only one case: when input of 
> lambda function is exactly “p”.  For all other cases the left side doesn’t 
> equal to the right side.  But from the view of two functions, they’re 
> obviously not identical. But how can I actually reduce it to F?
> 
>Regards,
> 
>Chun Tian
> 
> 
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


Re: [Hol-info] How to reduce these lambda equations to F?

2017-08-06 Thread Michael.Norrish
I would use 

   fs[FUN_EQ_THM]

to expand the assumptions to

   !x. x = prefix (label l) x

and

   !x. x = p

respectively.

Of course, this is a blunt weapon, so you may not wish to use it if other 
assumptions are disrupted too much. 

Michael

On 5/8/17, 04:25, "Chun Tian (binghe)"  wrote:

Hi,

This is the first time I met the following goal, in which one of the 
assumptions should be able to reduce to F (then the goal is resolved):

R (λt. t)

  4.  (λt. t) = (λt. prefix (label l) t)

The lambda function has the type of ``CCS -> CCS``, which CCS is my 
datatype defined by HOL’s Define command.  “prefix” is an constructor of CCS 
datatype.I *know* the equation doesn’t hold, because the whatever input 
arguments, the resulting CCS on both side must have different “size”, simply 
because one is the sub-expression of the other.   But how can I actually reduce 
it to F?

The other case is a little different:

R (λt. t)

  4.  (λt. t) = (λt. p)

The assumption "(λt. t) = (λt. p)” hold for only one case: when input of 
lambda function is exactly “p”.  For all other cases the left side doesn’t 
equal to the right side.  But from the view of two functions, they’re obviously 
not identical. But how can I actually reduce it to F?

Regards,

Chun Tian



--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


Re: [Hol-info] How to reduce these lambda equations to F?

2017-08-05 Thread Chun Tian (binghe)
Hi Thomas,

Thanks! Now I got your points:

1. ``(λt. t) = (λt. p)`` cannot reduce to F unless the underlying type 
has at least two distinct values (for datatypes with at least two constructors, 
it’s easily provable by cases analysis, I think).
2. To prove two lambda-functions, say f and g are not identical, it’s 
enough to choose one special value x and shows that f(x) <> g(x). And this fact 
depends on theorems but beta-conversion.

Now I think I can resolve both cases.

Regards,

Chun

> Il giorno 04 ago 2017, alle ore 21:38, Thomas Tuerk  
> ha scritto:
> 
> Hi Chun,
> 
> via a subgoal, you can introduce an assumption for a concrete argument. This 
> should be what you need. I'm thinking of something like
> 
> First show that a CCS q exists with "q <> p"
> `?q. q <> p` by ...
> 
> Then use this new q as an argument)
> `(\t. t) q = (\t. p) q` by PROVE_TAC[]
> Now you are done by BETA reduction and contradicting assumptions.
> 
> Best
> 
> Thomas
> 
> 
> On 04.08.2017 20:22, Chun Tian (binghe) wrote:
>> Hi,
>> 
>> This is the first time I met the following goal, in which one of the 
>> assumptions should be able to reduce to F (then the goal is resolved):
>> 
>> R (λt. t)
>> 
>>   4.  (λt. t) = (λt. prefix (label l) t)
>> 
>> The lambda function has the type of ``CCS -> CCS``, which CCS is my datatype 
>> defined by HOL’s Define command.  “prefix” is an constructor of CCS 
>> datatype.I *know* the equation doesn’t hold, because the whatever input 
>> arguments, the resulting CCS on both side must have different “size”, simply 
>> because one is the sub-expression of the other.   But how can I actually 
>> reduce it to F?
>> 
>> The other case is a little different:
>> 
>> R (λt. t)
>> 
>>   4.  (λt. t) = (λt. p)
>> 
>> The assumption "(λt. t) = (λt. p)” hold for only one case: when input of 
>> lambda function is exactly “p”.  For all other cases the left side doesn’t 
>> equal to the right side.  But from the view of two functions, they’re 
>> obviously not identical. But how can I actually reduce it to F?
>> 
>> Regards,
>> 
>> Chun Tian
>> 
>> 
>> 
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org!
>> http://sdm.link/slashdot
>> 
>> 
>> ___
>> hol-info mailing list
>> 
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! 
> http://sdm.link/slashdot___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


Re: [Hol-info] How to reduce these lambda equations to F?

2017-08-04 Thread Thomas Tuerk
Hi Chun,

via a subgoal, you can introduce an assumption for a concrete argument.
This should be what you need. I'm thinking of something like

First show that a CCS q exists with "q <> p"

`?q. q <> p` by ...

Then use this new q as an argument)

`(\t. t) q = (\t. p) q` by PROVE_TAC[]

Now you are done by BETA reduction and contradicting assumptions.

Best

Thomas



On 04.08.2017 20:22, Chun Tian (binghe) wrote:
> Hi,
>
> This is the first time I met the following goal, in which one of the 
> assumptions should be able to reduce to F (then the goal is resolved):
>
> R (λt. t)
> 
>   4.  (λt. t) = (λt. prefix (label l) t)
>
> The lambda function has the type of ``CCS -> CCS``, which CCS is my datatype 
> defined by HOL’s Define command.  “prefix” is an constructor of CCS datatype. 
>I *know* the equation doesn’t hold, because the whatever input arguments, 
> the resulting CCS on both side must have different “size”, simply because one 
> is the sub-expression of the other.   But how can I actually reduce it to F?
>
> The other case is a little different:
>
> R (λt. t)
> 
>   4.  (λt. t) = (λt. p)
>
> The assumption "(λt. t) = (λt. p)” hold for only one case: when input of 
> lambda function is exactly “p”.  For all other cases the left side doesn’t 
> equal to the right side.  But from the view of two functions, they’re 
> obviously not identical. But how can I actually reduce it to F?
>
> Regards,
>
> Chun Tian
>
>
>
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info