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
