Re: [Hol-info] Confused about Induct_on

[Alexander Cox]

Ah, now I understand. For some reason I misread that as meaning the variables 
had to be in the quantification order of the induction theorem. Silly me.
It’s working now.

Thank you,
Alex

On 16 Jan 2019, at 16:51, michael.norr...@data61.csiro.au wrote:

As Konrad said, both ho_match_mp_tac and Induct_on (which calls the former) 
will require the order of the variables in the quantification to match the 
order they appear as arguments to the relation.  In your case Gm has the Gamma 
and then the A, but your quantification has A then Gamma.



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 (“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 always be the same, and I don’t 
know why. Gm_ind ends with …⇒ ∀a0 a1. Gm a0 a1 ⇒ Gm' a0 a1.

Thank you,
Alex

On 15 Jan 2019, at 19:07, Konrad Slind wrote:

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) 
mailto:binghe.l...@gmail.com>> wrote:

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 
> mailto:u6060...@anu.edu.au>> ha scritto:
>
> 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 (Γ' + Γ) A`;
> …
> e (Induct_on `Gm`);
> OK..
>
> Exception raised at BasicProvers.Induct_on:
> at BasicProvers.induct_on_type:
> Type: :(α formula -> num) -> α formula -> bool is not registered in the types 
> database
>
> Any ideas where I’m going wrong? Is the latter the goal in the wrong form? 
> Where should I look to figure this out?
>
> Thank you,
> Alex
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info

___
hol-info mailing list
hol-info@lists.sourceforge.net<mailto: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

Re: [Hol-info] Confused about Induct_on

[Alexander Cox]

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 always be the same, and I don’t 
know why. Gm_ind ends with …⇒ ∀a0 a1. Gm a0 a1 ⇒ Gm' a0 a1.

Thank you,
Alex

On 15 Jan 2019, at 19:07, Konrad Slind wrote:

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) 
mailto:binghe.l...@gmail.com>> wrote:
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 
> mailto:u6060...@anu.edu.au>> ha scritto:
>
> 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 (Γ' + Γ) A`;
> …
> e (Induct_on `Gm`);
> OK..
>
> Exception raised at BasicProvers.Induct_on:
> at BasicProvers.induct_on_type:
> Type: :(α formula -> num) -> α formula -> bool is not registered in the types 
> database
>
> Any ideas where I’m going wrong? Is the latter the goal in the wrong form? 
> Where should I look to figure this out?
>
> Thank you,
> Alex
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info

___
hol-info mailing list
hol-info@lists.sourceforge.net<mailto: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] Confused about Induct_on

[Alexander Cox]

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 (Γ' + Γ) A`;
…
e (Induct_on `Gm`);
OK..

Exception raised at BasicProvers.Induct_on:
at BasicProvers.induct_on_type:
Type: :(α formula -> num) -> α formula -> bool is not registered in the types 
database


Any ideas where I’m going wrong? Is the latter the goal in the wrong form? 
Where should I look to figure this out?

Thank you,
Alex
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Relations which build upon each other

[Alexander Cox]

Hello,

I’m doing a project on proof theory, and I’m trying to define the proof rules 
with Hol_reln. I am defining multiple proof systems which build upon each 
other, i.e. intuitionistic logic then classical logic. It seems natural to have 
something like:

var (Sys1_rules, …,…) = Hol_reln `…`;
var (Sys2_rules,…,…) = Hol_reln `!x. Sys1 x ==> Sys2 x /\ …`

But when I go to prove something which needs to use Sys2 rules then Sys1 rules, 
I don’t know how to get it to work, since the Sys1 rules don’t know mention 
Sys2 (nor should they). For example:

`Sys2 x` by metis_tac[Sys2_rules]
`Sys2 y` by metis_tac[Sys1_rules,Sys2_rules] (* Sys1 has no rules for Sys2, so 
this fails! *)

The obvious solution is to just keep them independent and have all the rules in 
each of them, but I thought I might be missing some elegant way of achieving 
this. Please let me know if there is such a trick.

Thank you,
Alex
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info