Thank you Michael,
Great suggestions, Just solved.
Cheers.
On Fri, May 2, 2014 at 2:47 PM, Michael Norrish <
[email protected]> wrote:
> Some options:
>
> METIS_TAC[]
> works because first-ordering reasoning with equality is certainly
> able to find simple substitutions like this one
>
> SRW_TAC[][]
> works because SRW_TAC[][] eliminates simple equalities in the
> assumptions, whether they are oriented var = expression or
> expression = var. It will eliminate both assumption 3 and 4.
>
> REV_FULL_SIMP_TAC(srw_ss()) []
> works because it will rewrite assumption 4 with assumption 3
>
> Q.PAT_ASSUM `SUC n = winner` (SUBST_ALL_TAC o SYM) THEN
> ASM_SIMP_TAC (srw_ss()) []
>
> works by getting the equation from the assumptions, flipping it,
> and then substituting it throughout the goal. The simplifier then
> spots that the goal is the same as one of the assumptions. You
> could omit the call to SYM, and then assumption 4 would become
> `Count winner v = max`
>
> ...
>
>
> Michael
>
>
> On 02/05/14 13:42, masoume tajvidi wrote:
> > Hi,
>
> > While proving a lemma, I get to this step:
>
> > Count winner v = max
> > ------------------------------------
> > 0. ((winner' = winner) ∧ (max' = max)) ∧ winner ≠ 0 ⇒
> > (Count winner v = max)
> > 1. Max_vote n v = (winner',max')
> > 2. Count (SUC n) v > max'
> > 3. SUC n = winner
> > 4. Count (SUC n) v = max
> > 5. winner ≠ 0
>
> > I think by using Assumptions 3 and 4 we could easily prove the goal.
> > But I do not know what Tactic to use?
>
> > I have tried DECIDE_TAC, RES_TAC, SUBST1_ALL_TAC, but no success!
>
> > this is all I got:
>
> > (**********my theory to be proved************)
> > val Max_vote_eq_lem = store_thm ("Max_vote_eq_lem",
> > ``! n v winner max.(( Max_vote n v= (winner , max )) /\ ~(winner=0))
> > ==>( Count winner v = max)``
>
> > REPEAT GEN_TAC THEN
> > Induct_on `n` THENL [
> > FULL_SIMP_TAC (srw_ss())[Max_vote] THEN
> > REPEAT STRIP_TAC THEN
> > POP_ASSUM (ASSUME_TAC o GSYM) THEN
> > RES_TAC ,
> > FULL_SIMP_TAC (srw_ss())[Max_vote, Count] THEN
> > LET_ELIM_TAC ] THEN
> > POP_ASSUM MP_TAC THEN
> > POP_ASSUM MP_TAC THEN
> > REPEAT IF_CASES_TAC THEN
> > FULL_SIMP_TAC (srw_ss())[Max_vote, Count] THEN
> > REPEAT STRIP_TAC
> > ...)
>
> > (*************** my functions: ************************)
>
>
> > val Count= Define `(Count c ([])= 0)
> > /\ ( Count c (h::l) = if h=c then Count c (l) +1
> > else Count c (l))`
>
> > val Max_vote = Define `
> > (Max_vote 0 v= (0,0)) /\
> > ( Max_vote c v =
> > let (winner, max)= Max_vote (c-1) v in
> > (if Count c v > max then ( c , Count c v)
> > else if Count c v =max then (0,Count c v)
> > else Max_vote (c-1) v )) `
>
> > Thank you,
> > Masoumeh
>
>
> >
> ------------------------------------------------------------------------------
> > "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
> > Instantly run your Selenium tests across 300+ browser/OS combos. Get
> > unparalleled scalability from the best Selenium testing platform
> available.
> > Simple to use. Nothing to install. Get started now for free."
> > http://p.sf.net/sfu/SauceLabs
>
>
>
> > _______________________________________________
> > hol-info mailing list
> > [email protected]
> > https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
> ------------------------------------------------------------------------------
> "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
> Instantly run your Selenium tests across 300+ browser/OS combos. Get
> unparalleled scalability from the best Selenium testing platform available.
> Simple to use. Nothing to install. Get started now for free."
> http://p.sf.net/sfu/SauceLabs
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
"Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
Instantly run your Selenium tests across 300+ browser/OS combos. Get
unparalleled scalability from the best Selenium testing platform available.
Simple to use. Nothing to install. Get started now for free."
http://p.sf.net/sfu/SauceLabs
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
