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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ "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
