Re: [Hol-info] some questions about the proving process in HOL4

2015-12-15 Thread Ramana Kumar 
As Thomas said, the key is rewriting (or simplification). I suggested to
use fs, not STRIP_ASSUME_TAC.

On 16 December 2015 at 01:14, 康漫 <956066...@qq.com> wrote:

>   Thank everyone!
>   This problem has been resolved. I added following steps:
>
>   e (ASM_REWRITE_TAC [*TAKE_0*]) ;
>   e (ONCE_ASM_REWRITE_TAC [boolTheory.EQ_SYM_EQ]) ;
>   e (PROVE_TAC[listTheory.LENGTH_NIL]);
>   Thanks!
>
> -- Original --
> *From: * "hol-info-request";;
> *Date: * Tue, Dec 15, 2015 08:48 PM
> *To: * "hol-info";
> *Subject: * hol-info Digest, Vol 115, Issue 7
>
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
>
> You can reach the person managing the list at
> hol-info-ow...@lists.sourceforge.net
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of hol-info digest..."
>
>
> Today's Topics:
>
>1. Re: [SPAM] some questions about the proving process in HOL4
>   (Jeremy Dawson)
>2. [SPAM] Re: some questions about the proving process in HOL4 ( ?? )
>
>
> --
>
> Message: 1
> Date: Tue, 15 Dec 2015 14:54:48 +1100
> From: Jeremy Dawson 
> Subject: Re: [Hol-info] [SPAM] some questions about the proving
> process in HOL4
> To: 
> Message-ID: <566f8f08.9050...@anu.edu.au>
> Content-Type: text/plain; charset="windows-1252"; format=flowed
>
> Hi Ada,
>
> You need to search for suitable theorems.
>
> In this case
>
>  > apropos ``TAKE 0`` ;
> <>
> val it =
> [(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)),
>
> so from the initial goal
>
> e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
>
> e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ;
>
> This should work but doesn't - when all else fails, look at the types:
> show_types := true ;
> and you see that they are different.
> Do it this way instead.
>
> e (ASM_REWRITE_TAC [listTheory.TAKE_0, listTheory.LENGTH_EQ_NUM_compute]) ;
>
> then you're almost there.
>
> If you didn't have the theorem TAKE_0 you would have to use the
> definition of TAKE, namely listTheory.TAKE_def, and use
> Cases_on `p`
>
> Cheers,
>
> Jeremy
>
>
>
> On 15/12/15 14:27, Ada wrote:
> > Hey guys,
> >
> > I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> > which can get the first n elements in a list.
> > When I was proving one property of TAKE, I find an interesting thing. As
> > follows:
> > - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> > - e (REPEAT STRIP_TAC);
> > OK..
> > 1 subgoal:
> >> val it =
> >  TAKE 0 p = p
> >  
> >LENGTH p = 0
> >   : proof
> > - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> > OK..
> > 1 subgoal:
> >  > val it =
> >  TAKE 0 p = p
> >  
> >0.  LENGTH p = 0
> >1.  !l. (LENGTH l = 0) <=> (l = [])
> >2.  !l n.
> >  (LENGTH l = NUMERAL (BIT1 n)) <=>
> >  ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
> >3.  !l n.
> >  (LENGTH l = NUMERAL (BIT2 n)) <=>
> >  ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
> >4.  !l n1 n2.
> >  (LENGTH l = n1 + n2) <=>
> >  ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++
> l2)
> >   : proof
> > The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> > have already been in assumption list, so I think it is natural to get
> > "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove
> > that. Could anyone prove it?
> > Thanks! --Wish.
> >
> >
> >
> --
> >
> >
> >
> > ___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>
>
> --
>
> Message: 2
> Date: Tue, 15 Dec 2015 20:48:18 +0800
> From: " ?? " <956066...@qq.com>
> Subject: [Hol-info] [SPAM] Re: some questions about the proving
> process in HOL4
> To: " hol-info " 
> Message-ID: 
> Content-Type: text/plain; charset="gb18030"
>
>
> Hi,Ramana,Thanks for your reply!
>after I used listTheory.LENGTH_NIL, I get that:
>  - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL);
> OK..
> 1 subgoal:
> > val it =
>  first 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>  : proof
>  Then Which tactic could be

Re: [Hol-info] [SPAM] Re: some questions about the proving process in HOL4

2015-12-15 Thread Thomas Tuerk 
Hi Ada,

there are many ways to do it. But essentially what you want is rewriting.

Bird's eye view:

You want to prove

``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``

STEP 1 : You show that "p" is "[]" with theorem LENGTH_NIL.
STEP 2 : You use the theorem TAKE_0 to simplify "TAKE 0 p" to "[]"
STEP 3 : You combine STEP 1 and STEP 2


There are plenty of ways to do it. Essentially, you want to use
LENGTH_NIL and TAKE_0 as rewrites. This can (rather verbosely) be done
via e.g.

val thm1 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
 REWRITE_TAC[LENGTH_NIL, TAKE_0] THEN
 REPEAT STRIP_TAC THEN
 ASM_REWRITE_TAC[])

However, a simple call to the simplifier is sufficient (it uses the
antecedent of the implication automatically and list_ss contains TAKE_0)

val thm2 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
  SIMP_TAC list_ss [LENGTH_NIL])


One could also use first order automatic reasoners, but this is a bit
much here.

val thm3 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
  REPEAT STRIP_TAC THEN
  `p = []` by PROVE_TAC[LENGTH_NIL] THEN
  ASM_REWRITE_TAC[TAKE_0])

val thm4 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
  PROVE_TAC [TAKE_0, LENGTH_NIL])


There are plenty more ways for doing it. The core operation is rewriting
here. So, perhaps have a look at the rewrite tactics and the simplifier.

Best

Thomas Tuerk



On 15.12.2015 13:48, 康漫 wrote:
>   Hi,Ramana,Thanks for your reply!
>   after I used listTheory.LENGTH_NIL, I get that:
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL);
> OK..
> 1 subgoal:
>> val it =
> first 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>  : proof
> Then Which tactic could be used to prove the goal? I tried many
> times , but it failed.
> Thanks! -Wish
> 
> 
> --
> 
> Message: 3
> Date: Tue, 15 Dec 2015 11:27:35 +0800
> From: " Ada " 
> Subject: [Hol-info] [SPAM] some questions about the proving process in
> HOL4
> To: " hol-info " 
> Message-ID: 
> Content-Type: text/plain; charset="iso-8859-1"
> 
> Hey guys,
>  
> I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
>  When I was proving one property of TAKE, I find an interesting thing.
> As follows:
>  - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
>> val it =
>  TAKE 0 p = p
> 
>   LENGTH p = 0
>  : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
>> val it =
>  TAKE 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>   2.  !l n.
> (LENGTH l = NUMERAL (BIT1 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
>   3.  !l n.
> (LENGTH l = NUMERAL (BIT2 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
>   4.  !l n1 n2.
> (LENGTH l = n1 + n2) <=>
> ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
>  : proof
>  The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove
> that. Could anyone prove it?
>  
>  Thanks! --Wish.
> -- next part --
> An HTML attachment was scrubbed...
> 
> --
> 
> Message: 4
> Date: Tue, 15 Dec 2015 14:34:44 +1100
> From: Ramana Kumar 
> Subject: Re: [Hol-info] [SPAM] some questions about the proving
> process in HOL4
> To: Ada 
> Cc: hol-info 
> Message-ID:
>

[Hol-info] [SPAM] Re: some questions about the proving process in HOL4

2015-12-15 Thread ???? 
Hi,Ramana,Thanks for your reply!
   after I used listTheory.LENGTH_NIL, I get that:
 - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL);
OK..
1 subgoal:
> val it =
 first 0 p = p

  0.  LENGTH p = 0
  1.  !l. (LENGTH l = 0) <=> (l = [])
 : proof
 Then Which tactic could be used to prove the goal? I tried many times , 
but it failed.
 Thanks! -Wish
  

 

--

Message: 3
Date: Tue, 15 Dec 2015 11:27:35 +0800
From: " Ada " 
Subject: [Hol-info] [SPAM] some questions about the proving process in
HOL4
To: " hol-info " 
Message-ID: 
Content-Type: text/plain; charset="iso-8859-1"

Hey guys,
 
I am learning to use HOL4. There is  a function named "TAKE" in HOL4, which can 
get the first n elements in a list. 
 When I was proving one property of TAKE, I find an interesting thing. As 
follows:
 - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
- e (REPEAT STRIP_TAC);
OK..
1 subgoal:
> val it =
 TAKE 0 p = p

  LENGTH p = 0
 : proof
- e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
OK..
1 subgoal:
> val it =
 TAKE 0 p = p

  0.  LENGTH p = 0
  1.  !l. (LENGTH l = 0) <=> (l = [])
  2.  !l n.
(LENGTH l = NUMERAL (BIT1 n)) <=>
?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
  3.  !l n.
(LENGTH l = NUMERAL (BIT2 n)) <=>
?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
  4.  !l n1 n2.
(LENGTH l = n1 + n2) <=>
?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
 : proof
 The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])" have 
already been in assumption list, so I think it is natural to get "p=[]", then 
"TAKE 0 [] = []". But I tried many times , I can't prove that. Could anyone 
prove it?
  
 Thanks! --Wish.
-- next part --
An HTML attachment was scrubbed...

--

Message: 4
Date: Tue, 15 Dec 2015 14:34:44 +1100
From: Ramana Kumar 
Subject: Re: [Hol-info] [SPAM] some questions about the proving
process in HOL4
To: Ada 
Cc: hol-info 
Message-ID:

Re: [Hol-info] some questions about the proving process in HOL4

2015-12-15 Thread ???? 
Thank everyone!
   This problem has been resolved. I added following steps:
   
   e (ASM_REWRITE_TAC [TAKE_0]) ;
   e (ONCE_ASM_REWRITE_TAC [boolTheory.EQ_SYM_EQ]) ;
   e (PROVE_TAC[listTheory.LENGTH_NIL]);
Thanks!

 

 -- Original --
  From:  "hol-info-request";;
 Date:  Tue, Dec 15, 2015 08:48 PM
 To:  "hol-info"; 
 
 Subject:  hol-info Digest, Vol 115, Issue 7

 

Send hol-info mailing list submissions to
hol-info@lists.sourceforge.net

To subscribe or unsubscribe via the World Wide Web, visit
https://lists.sourceforge.net/lists/listinfo/hol-info
or, via email, send a message with subject or body 'help' to
hol-info-requ...@lists.sourceforge.net

You can reach the person managing the list at
hol-info-ow...@lists.sourceforge.net

When replying, please edit your Subject line so it is more specific
than "Re: Contents of hol-info digest..."


Today's Topics:

   1. Re: [SPAM] some questions about the proving process in HOL4
  (Jeremy Dawson)
   2. [SPAM] Re: some questions about the proving process in HOL4 ( ?? )


--

Message: 1
Date: Tue, 15 Dec 2015 14:54:48 +1100
From: Jeremy Dawson 
Subject: Re: [Hol-info] [SPAM] some questions about the proving
process in HOL4
To: 
Message-ID: <566f8f08.9050...@anu.edu.au>
Content-Type: text/plain; charset="windows-1252"; format=flowed

Hi Ada,

You need to search for suitable theorems.

In this case

 > apropos ``TAKE 0`` ;
<>
val it =
[(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)),

so from the initial goal

e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);

e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ;

This should work but doesn't - when all else fails, look at the types:
show_types := true ;
and you see that they are different.
Do it this way instead.

e (ASM_REWRITE_TAC [listTheory.TAKE_0, listTheory.LENGTH_EQ_NUM_compute]) ;

then you're almost there.

If you didn't have the theorem TAKE_0 you would have to use the 
definition of TAKE, namely listTheory.TAKE_def, and use
Cases_on `p`

Cheers,

Jeremy



On 15/12/15 14:27, Ada wrote:
> Hey guys,
>
> I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
> When I was proving one property of TAKE, I find an interesting thing. As
> follows:
> - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
>> val it =
>  TAKE 0 p = p
>  
>LENGTH p = 0
>   : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
>  > val it =
>  TAKE 0 p = p
>  
>0.  LENGTH p = 0
>1.  !l. (LENGTH l = 0) <=> (l = [])
>2.  !l n.
>  (LENGTH l = NUMERAL (BIT1 n)) <=>
>  ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
>3.  !l n.
>  (LENGTH l = NUMERAL (BIT2 n)) <=>
>  ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
>4.  !l n1 n2.
>  (LENGTH l = n1 + n2) <=>
>  ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
>   : proof
> The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove
> that. Could anyone prove it?
> Thanks! --Wish.
>
>
> --
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>



--

Message: 2
Date: Tue, 15 Dec 2015 20:48:18 +0800
From: " ?? " <956066...@qq.com>
Subject: [Hol-info] [SPAM] Re: some questions about the proving
process in HOL4
To: " hol-info " 
Message-ID: 
Content-Type: text/plain; charset="gb18030"

Hi,Ramana,Thanks for your reply!
   after I used listTheory.LENGTH_NIL, I get that:
 - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL);
OK..
1 subgoal:
> val it =
 first 0 p = p

  0.  LENGTH p = 0
  1.  !l. (LENGTH l = 0) <=> (l = [])
 : proof
 Then Which tactic could be used to prove the goal? I tried many times , 
but it failed.
 Thanks! -Wish
  

 

--

Message: 3
Date: Tue, 15 Dec 2015 11:27:35 +0800
From: " Ada " 
Subject: [Hol-info] [SPAM] some questions about the proving process in
HOL4
To: " hol-info " 
Message-ID: 
Content-Type: text/plain; charset="iso-8859-1"

Hey guys,
 
I