I am having an issue using Induct_on on a Hol_reln called Gm.
If I try to use it on a trivial goal it works, e.g.
> g `!Γ A. Gm Γ A ==> Gm Γ A`;
…
> e (Induct_on `Gm`);
OK..
1 subgoal:
val it =
(∀A. Gm {|A|} A) ∧ …
but if I use on a useful goal such as:
g `!Γ Γ' A. Gm Γ A ==> Gm (Γ' + Γ)
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 am
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)
wrot
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 to
.
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
, 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 data
