# Re: [Hol-info] HOL difficulty with this subgoal

```Thanks qspecl_then and friends are great! Sometimes it is easier to be more
specific.```
```
Haitao

On Wed, Mar 6, 2019 at 1:46 AM <michael.norr...@data61.csiro.au> wrote:

> If you really need to instantiate a theorem by hand, using Q.SPEC_THEN and
> Q.ISPEC_THEN is usually better.  The first is also available under the name
> qspec_then.
>
>
>
> E.g., you can do
>
>
>
>   qspec_then `a` mp_tac mytheorem
>
>
>
> If you need to do lots of specialisations you can use the list forms:
>
>
>
>   qspecl_then [`a`, `b`, `c`] mp_tac mytheorem
>
>
>
> If you want to specialise an assumption (rather than mytheorem), use
> first_x_assum or similar to pull that assumption out of the assumptions:
>
>
>
>   first_x_assum (qspecl_then [`a+6`, `f b`] mp_tac)
>
>
>
> The big advantage of Q.SPEC_THEN and friends is that the arguments are
> parsed in the context of the goal (so something like `f b` above will
> ensure that f and b get the right types rather than `’a->’b` and `’a`).
>
>
>
> Michael
>
>
>
> *From: *Haitao Zhang <zhtp...@gmail.com>
> *Date: *Wednesday, 6 March 2019 at 18:42
> *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] HOL difficulty with this subgoal
>
>
>
> I should also add that simp [..] would take a step in the wrong direction
> as I have an equality on the assumptions list that I used earlier in the
> other direction (through SYM). simp_tac does not do anything as assumptions
> are required. And as I can see now the step does not actually depend on
> FUNSET_ID as there is already a fact proved using it in the assumptions. I
> was using FUNSET_ID in the earlier solution because I was manually
> instantiating the antecedent (instead of searching for it among the
> assumptions).
>
>
>
> Haitao
>
>
>
>
>
> On Tue, Mar 5, 2019 at 11:30 PM Haitao Zhang <zhtp...@gmail.com> wrote:
>
> Sorry Michael I cut and pasted the wrong goal for some reason. Here is the
> corrected one:
>
>
>
>    scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) =
>    sce A ((λ(x :mor). x) a)
>    ------------------------------------
>      0.  homset (A :mor -> bool)
>      4.  (A :mor -> bool) (a :mor)
>
>
> It doesn't depend on scr. I also found out that writing out in this non
> beta-reduced form I can solve it with irule SC_EV >> asm_simp_tac bool_ss
> [], but not in the beta reduced form. metis_tac and prove_tac still fails
> on both (beta-reduced or not reduced).
>
>
>
> Sorry for the confusion.
>
>
>
> Haitao
>
>
>
>
>
> On Tue, Mar 5, 2019 at 10:07 PM <michael.norr...@data61.csiro.au> wrote:
>
> What did simp[FUNSET_ID, SC_EV] do to this goal, if anything?
>
>
>
> I’d expect it to change the goal to
>
>
>
>    sce A a = scr A c sce A a
>
>
>
> (You haven’t shown us any assumptions/theorems about scr.)
>
>
>
> Michael
>
>
>
> *From: *Haitao Zhang <zhtp...@gmail.com>
> *Date: *Wednesday, 6 March 2019 at 16:57
> *To: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *[Hol-info] HOL difficulty with this subgoal
>
>
>
> I had great difficulty to have HOL prove the following subgoal (I turned
> on typing for debugging, ``\$c`` is a composition operator like ``\$o``):
>
>
>
>    scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) = scr A c sce A a
>    ------------------------------------
>      0.  homset (A :mor -> bool)
>      4.  (A :mor -> bool) (a :mor)
>
>
>
> Which should be directly derived from two theorems below and assumptions
> 0,4 (I removed other ones to reduce clutter) :
>
>
>
> > FUNSET_ID;
> val it = ⊢ ∀(A :α -> bool). FUNSET A A (λ(x :α). x): thm
>
> > SC_EV;
> val it =
>    ⊢ ∀(A :mor -> bool) (B :mor -> bool) (f :mor -> mor) (a :mor).
>          homset A ⇒
>          homset B ⇒
>          FUNSET A B f ⇒
>          A a ⇒
>          (scf A B f c sce A a = sce B (f a)): thm
>
>
>
> Eventually I need to manually instantiate everything to solve it:
>
>
>
> > e (mp_tac (BETA_RULE (MATCH_MP ((UNDISCH o UNDISCH o SPEC ``a:mor`` o
> SPEC ``\x.(x:mor)`` o Q.SPEC `A` o Q.SPEC `A`) SC_EV) (ISPEC
> ``A:mor->bool`` FUNSET_ID))) >> asm_simp_tac bool_ss []);
>
>
>
> It seems the main obstacle was "ground const vs. polymorphic const" based
> on the error messages I got during various trials. It was important that I
> spelled out all type correctly for it to work.
>
>
>
> Haitao
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
```
```_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
```