Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

[<Mic...@da...>]

Make the assumption the left-hand-side of an implication (moving it out of the assumptions), rewrite with the identity that says that

  ((P /\ Q) ==> R) <=> (P ==> (Q ==> R))

and then move all the implications’ left-hand-sides back into the assumptions.

In HOL4 you could use something like

  th |> DISCH_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH_ALL

The use of the _ALL functions makes this a bit fragile, but it will work in your case.

You might also find that the discharged theorem works directly as a conditional rewrite (I don’t know what the HOL Light tools is for this).

My HOL4-informed advice would be to avoid working with theorems that have assumptions like this: the machinery copes better with theorems that are just implications.  (Of course, goals can have assumptions and the machinery copes very well with those, but that is a different matter.)

Michael

From: Dylan Melville <dyl...@gm...>
Date: Tuesday, 28 August 2018 at 22:48
To: "Norrish, Michael (Data61, Acton)" <Mic...@da...>, "hol...@li..." <hol...@li...>
Subject: Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

That's what I figured. How can I separate the assumptions of second_b13_complete?

On Mon, Aug 27, 2018, 10:32 PM <Mic...@da...<mailto:Mic...@da...>> wrote:
The assumption of the rewrite theorem is not present in the assumptions of the goal and so you get an invalid tactic.

Strictly speaking this is not REWRITE_TAC failing but e.   Indeed, you should find that REWRITE_TAC [second_b13_complete] applied to the goal works just fine.

Michael

From: Dylan Melville <dyl...@gm...<mailto:dyl...@gm...>>
Date: Tuesday, 28 August 2018 at 11:45
To: "hol...@li...<mailto:hol...@li...>" <hol...@li...<mailto:hol...@li...>>
Subject: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

VERSION: HOL Light QE (augmentation of HOL Light, very similar)

Hello all. Today I’ve been having 2 issues with HOL. The first is that although the documentation for REWRITE_TAC says that the tactic has no failure conditions, when I use the following command:

# e (REWRITE_TAC[second_b13_complete]);;

Where second_b13_complete is:

# second_b13_complete;;
val it : thm =
  isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\
  ~isFreeIn (QuoVar "n" (TyBase "num")) f
  |- (\n. (\P. P n) (eval (f) to (num->bool))) =
     (\P n. P n) (eval (f) to (num->bool))

When used with the following goal already declared:

# p();;
val it : goalstack = 1 subgoal (1 total)

  0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`]
  1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`]
  2 [`isPeano f`]

`(eval (f) to (num->bool)) 0 /\
 (\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool)))
 ==> (\P. P = (\x. T)) (\n. (\P. P n) (eval (f) to (num->bool)))`

Results in the following error:

# e (REWRITE_TAC[first_b13_complete]);;
Exception: Failure "VALID: Invalid tactic”.

Which is confusing, since not only is the tactic supposed to have no failure conditions, but the bolded sections of the theorem and the goal are matched properly, and the two conjuncted antecedents of the theorem are assumptions 0 and 1 of the goal. So, is the reason that the tactic application fails that antecedents of the theorem are conjuncted? If so, is there a command I’m missing that can transform the theorem to the proper form?

Thanks in advance.

Dylan Melville | McMaster University, Math and Computer Science