Email Gateway (Aug 17 2022 at 14:46): Email Gateway (Aug 17 2022 at 14:46):From: Dimitrios Vytiniotis <dimitriv@cis.upenn.edu>
Hello all, I am puzzled over the first issue and need
some advice on the second.
First issue
===========================================================
I have an inductive relation and some of the inference rules
use meta-level quantifiers on the premises.
I found that more convenient because at use sites it is easier
for me to instantiate these things than when using object-level
quantifiers.
I very often in my development use the style:
lemma blabla: ...
by(induct X, auto elim: MyRelation.elims)
And although I feel it should work, I get back the error:
*** exception TERM raised: dest_Trueprop
This is a bit annoying, because I did not encounter these problems
when the premises of the rules contained just object level forall's.
Additionally I have noticed that if I prove an inversion theorem
using (inductive_cases) and use that theorem instead of MyRelation.elims
things tend to (but not always) work more smoothly.
Is there more information on this? Should I send over more information?
I have not been able to figure out when exactly these errors occur but
any information would be valuable.
Second issue (advice)
=======================================================
I have a datatype which has only one constructor that takes a pair.
Values of this datatype are paired with naturals and
contained in a list. I have very often
found out that when I do induction on the list to prove a theorem,
in the inductive case I often have to do
a "by(cases "x", cases "snd x", blast)"
which I hate but want to do it in a one-line step because it is
a very ``obvious'' fact for the reader of the proof. How do I do
this elegantly (e.g with a single tactic like
(cases_deep_break "x", auto) or similar)
thanks!
-d
Email Gateway (Aug 17 2022 at 14:46):From: Lawrence Paulson <lp15@cam.ac.uk>
This looks like a bug. Please send me a theory file, preferably the
smallest possible that causes this behaviour.
Larry Paulson
Email Gateway (Aug 17 2022 at 14:46):From: Makarius <makarius@sketis.net>
On Fri, 16 Jun 2006, Dimitrios Vytiniotis wrote:
I have a datatype which has only one constructor that takes a pair.
Values of this datatype are paired with naturals and contained in a
list. I have very often found out that when I do induction on the list
to prove a theorem, in the inductive case I often have to do a "by(cases
"x", cases "snd x", blast)"
This is how to provide your own cases rule for that specific type scheme:
datatype ('a, 'b) foo = Foo "'a * 'b"
lemma nat_foo_cases [cases type]:
"(!!(n::nat) a b. x = (n, Foo (a, b)) ==> C) ==> C"
by (cases x, cases "snd x") auto
lemma
fixes foos :: "(nat * ('a, 'b) foo) list"
shows "P foos"
proof (induct foos)
case Nil
show ?case sorry
next
case (Cons x xs)
show ?case
apply (cases x)
sorry
qed
How do I do this elegantly (e.g with a single tactic like
(cases_deep_break "x", auto) or similar)
As a rule of thumb, it is better to derive rules of the Pure framework (as
above) rather than do ML hacking with methods/tactics.
Makarius
Email Gateway (Aug 17 2022 at 14:46):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Dimitrios Vytiniotis wrote:
Dimitrios,
I don't know if the following would help, but of the following,
case_tac_frees does case_tac for all free variables
and case_tac_params does it for all parameters, ie, variables
in a subgoal quantified by !!
fun case_tacs (str :: strs) sg state =
((case_tac str THEN_ALL_NEW case_tacs strs) sg state
handle _ => case_tacs strs sg state)
| case_tacs [] sg state = all_tac state ;
fun case_tac_frees sg state =
let val tm = nth (prems_of state, sg-1) ;
fun freename (Free (name, ty)) = name ;
in case_tacs (map freename (term_frees tm)) sg state end ;
fun case_tac_params sg state =
let val tm = nth (prems_of state, sg-1) ;
val params = (strip_qnt_vars "all" tm) ;
in case_tacs (map fst params) sg state end ;
Alternatively you can just construct your own "exhaust" theorem
(for example, case_tac "x" where x is a list seems to be equivalent to
(res_inst_tac [("y", "x")] list.exhaust))
Regards,
Jeremy
Email Gateway (Aug 17 2022 at 14:46):From: Makarius <makarius@sketis.net>
On Fri, 16 Jun 2006, Dimitrios Vytiniotis wrote:
I have an inductive relation and some of the inference rules
use meta-level quantifiers on the premises.
I found that more convenient because at use sites it is easier for me to
instantiate these things than when using object-level quantifiers.
Very good. This is usually the way to do it, because the resulting rules
can be used natively, without having to walk through object-logic
connectives.
lemma blabla: ...
by(induct X, auto elim: MyRelation.elims)
Just note that the initial induct and terminal auto method are normally
separated like this:
by (induct X) (auto ...)
The difference shows up when there are facts being used for the first
part. These are usually irrelevant for the second, so don't pass them to
auto in the first place.
And although I feel it should work, I get back the error:
*** exception TERM raised: dest_Trueprop
Is this caused by induct or auto? Sometimes a meta-level quantifier gets
a more general type than expected (e.g. 'a::{}). Then certain tools fail
to internalize a problem into the object-logic.
Makarius
Email Gateway (Aug 17 2022 at 14:46):From: Dimitrios Vytiniotis <dimitriv@cis.upenn.edu>
Thanks Jeremy, Makarius for the advice. Useful to know.
For the dest_Trueprop issue, it is the 'auto' step that causes
the TERM exception. To be concrete I have put a small theory file at:
http://www.cis.upenn.edu/~dimitriv/poplmark/Simple.thy
which demonstrates what is happening
thanks!
-d
Makarius wrote:
Email Gateway (Aug 17 2022 at 14:46):From: Brian Huffman <brianh@csee.ogi.edu>
Looking at the source for auto_tac (in Provers/clasimp.ML), I found that auto
makes calls to the simp, safe, and blast tactics. It appears that the problem
in your example lies in the blast tactic. If you make Typing.elims and
Val.elims into safe elimination rules (with "auto elim!:" instead of "auto
elim:") then auto no longer fails, because the elimination rules are used by
safe instead of blast. But if you replace auto with repeated calls to blast,
the third subgoal produces the same dest_Trueprop error. I'm not an expert on
how blast works, but it seems to me that there could be a bug in the blast
tactic.
Last updated: Nov 21 2024 at 12:39 UTC