, 16 January 2019 at 16:36
To: Konrad Slind
Cc: hol-info
Subject: Re: [Hol-info] Confused about Induct_on
Hi Konrad and Chun,
When I change the goal to ∀A Γ. Gm Γ A ⇒ ∀Γ'. Gm Γ' A, I still get errors with
both Induct_on and HO_MATCH_MP_TAC (“not registered in the types database
.
Michael
From: Alexander Cox
Date: Wednesday, 16 January 2019 at 16:36
To: Konrad Slind
Cc: hol-info
Subject: Re: [Hol-info] Confused about Induct_on
Hi Konrad and Chun,
When I change the goal to ∀A Γ. Gm Γ A ⇒ ∀Γ'. Gm Γ' A, I still get errors with
both Induct_on and HO_MATCH_MP_TAC
Hi Konrad and Chun,
When I change the goal to ∀A Γ. Gm Γ A ⇒ ∀Γ'. Gm Γ' A, I still get errors with
both Induct_on and HO_MATCH_MP_TAC (“not registered in the types database”, “at
HolKernel.ho_match_term: at ??.failwith: term_pmatch” respectively).
It appears (to me) that Gm_ind wants Γ and A
I suspect that the order of quantification in the goal is important, since
that controls how the induction predicate is instantiated. So try
!Gamma A. Gm Gamma A ==> !Gamma'.
since that makes it explicit for the machinery.
Konrad.
On Tue, Jan 15, 2019 at 1:30 AM Chun Tian (binghe)
Hi,
I think you should use HO_MATCH_MP_TAC (together with your induction theorem of
“Gm”, of the form ``!Gm. X ==> P Gm``) in this case. I only use Induct and
Induct_on on simple variables like your Γ Γ’ A.
—Chun
> Il giorno 15 gen 2019, alle ore 14:49, Alexander Cox ha
> scritto:
>
> I
