Hi Liu,
I don't know EXTENCE_TAC. I would have used EXISTS_TAC. This shound not
depend on whether "a" is a record type or not. So something like:
Q.EXISTS_TAC `EL n A`
It might be worth looking at REFINE_TAC to partially instantiate the
record and quantifier heuristics (QI_ss) to split the quantifier
automatically and introduce a record.
Cheers
Thomas
On 17.04.2017 08:54, Liu Gengyang wrote:
> Hi,
>
> I have a question as follow:
>
> load "realLib";
> open listTheory;
>
> Datatype `coordinate = <|x_axis: real; y_axis: real; z_axis: real|>`;
> val A = ``A: coordinate list``;
>
> g `^A <> [] ==> !n. ?a. a.x_axis <= (EL n A).x_axis`;
>
> - e(RW_TAC list_ss []);
> OK..
> 1 subgoal:
> > val it =
>
> ?a. a.x_axis <= (EL n A).x_axis
> ------------------------------------
> A <> []
> : proof
>
> Now I want to use EXTENCE_TAC to instantiate "a", but I don't know how
> to do it, because "a" is a record type. Could anyone help me?
>
> Thanks,
>
> Liu
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
