Re: [Hol-info] How to eliminate existential quantifier in a goal about list?

[Thomas Tuerk]

Hi Liu,

you have realLib open. "0" can be parsed as either a real or a num.
That's why you get the warning that two resolutions are possible. The
"EXISTS_TAC ``0``" fails, because ``0`` is parsed as a real, while you
need a num. An explicit type annotation does the trick: So use

e (EXISTS_TAC ``0:num``);

Cheers

Thomas


--
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

[Hol-info] How to eliminate existential quantifier in a goal about list?

[Liu Gengyang]

Hi，


I have a question about eliminating the existential quantifier.As follows,


load "realLib";
open listTheory;


Datatype `coordinate = <|x_axis: real; y_axis: real; z_axis: real|>`;
val p = ``p: coordinate list``;
(*goal1*)
g `^p <> [] ==> ?c:coordinate. MEM c ^p`;
e (RW_TAC list_ss [MEM_EL]);
e (EXISTS_TAC ``0``);


And there is a error message:more than one resolution of overloading was 
possible.I don't know what mean about it.


Furthermore, if p is a num list, there is not such error.That is:


val p = ``p: num list``;
(*goal2*)
g `^p <> [] ==> ?a:num. MEM a ^p`;
e (RW_TAC list_ss [MEM_EL]);
e (EXISTS_TAC ``0``);
e (Cases_on `p` THEN RW_TAC list_ss []);


More strange is that if I prove goal2 first, it can be proved, otherwise, it 
can't be proved, and also prompt "message:more than one resolution of 
overloading was possible" after e (EXISTS_TAC ``0``).


I just want to prove that there is a element existencing in a list, but now I 
don't know how to do it. 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