[Hol-info] list computations
I just wrote a fairly manual 48-line proof of the following. Is there some decision procedure, simpset, or tactic I could use to automate it that I'm not aware of? The theorems in srw_ss() seem not to play very well together on this kind of stuff. TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] list computations
Note quite sure how you got to 48 lines. I think only a single call to SRW_TAC (or lcsymtacs.lrw) is needed. val thm = Q.prove( `TAKE (LENGTH bvs + 1) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st`, lrw [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_DROP, rich_listTheory.EL_APPEND2, rich_listTheory.EL_CONS, arithmeticTheory.PRE_SUB1] ) Anthony On 27 Feb 2013, at 17:58, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote: I just wrote a fairly manual 48-line proof of the following. Is there some decision procedure, simpset, or tactic I could use to automate it that I'm not aware of? The theorems in srw_ss() seem not to play very well together on this kind of stuff. TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] list computations
Thanks! The secret sauce seems to be EL_APPEND2, and possibly whatever is in lrw. (And I should use LIST_EQ_REWRITE more often too.) This should make a lot of my subgoal proofs much shorter :) On Wed, Feb 27, 2013 at 7:02 PM, Anthony Fox ac...@cam.ac.uk wrote: Note quite sure how you got to 48 lines. I think only a single call to SRW_TAC (or lcsymtacs.lrw) is needed. val thm = Q.prove( `TAKE (LENGTH bvs + 1) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st`, lrw [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_DROP, rich_listTheory.EL_APPEND2, rich_listTheory.EL_CONS, arithmeticTheory.PRE_SUB1] ) Anthony On 27 Feb 2013, at 17:58, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote: I just wrote a fairly manual 48-line proof of the following. Is there some decision procedure, simpset, or tactic I could use to automate it that I'm not aware of? The theorems in srw_ss() seem not to play very well together on this kind of stuff. TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] list computations
Hi, I think, it is even simpler: SIMP_TAC list_ss [rich_listTheory.DROP_APPEND2] Best Thomas On Wed, 2013-02-27 at 22:10 +, Ramana Kumar wrote: Thanks! The secret sauce seems to be EL_APPEND2, and possibly whatever is in lrw. (And I should use LIST_EQ_REWRITE more often too.) This should make a lot of my subgoal proofs much shorter :) On Wed, Feb 27, 2013 at 7:02 PM, Anthony Fox ac...@cam.ac.uk wrote: Note quite sure how you got to 48 lines. I think only a single call to SRW_TAC (or lcsymtacs.lrw) is needed. val thm = Q.prove( `TAKE (LENGTH bvs + 1) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ h:: (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st`, lrw [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_DROP, rich_listTheory.EL_APPEND2, rich_listTheory.EL_CONS, arithmeticTheory.PRE_SUB1] ) Anthony On 27 Feb 2013, at 17:58, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote: I just wrote a fairly manual 48-line proof of the following. Is there some decision procedure, simpset, or tactic I could use to automate it that I'm not aware of? The theorems in srw_ss() seem not to play very well together on this kind of stuff. TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4))) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) = TAKE (LENGTH bvs + 1) (REVERSE bvs ++ Block 3 [CodePtr a; bve]:: (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
