Jonathan Lindegaard Starup (Oct 31 2024 at 12:31): Jonathan Lindegaard Starup (Oct 31 2024 at 12:31):I often find myself in situations exemplified here
lemma
assumes z: ‹example []›
assumes imp: ‹⋀xs ys. (example xs ⟹ example ys ⟹ example (xs @ ys))›
shows ‹example (take 0 [1])›
proof-
have simpl: ‹take 0 [1] = [] @ []› by simp
show ?thesis unfolding simpl
proof(rule imp; rule z) qed
qed
I have an implication i want to use (conclusion example (xs @ ys)) and a goal example (take 0 [1]). I want to apply the implication with rule but the terms no not match. What i'd want is a way for the pattern match to succeed, but also give me the obligation to prove that take 0 [1] = ?xs @ ?ys.
Is there such a way to use rule or do you have some other smart way to write proofs in these kinds of situations?
irvin (Oct 31 2024 at 15:41):urule might be able to do something like
lemma simpl[uhint]: ‹take 0 [1] = [] @ []› by simp
lemma
assumes z: ‹example []›
assumes imp: ‹⋀xs ys. (example xs ⟹ example ys ⟹ example (xs @ ys))›
shows ‹example (take 0 [1])›
apply(urule imp)
by (fact z)+
its available in the afp and I think you need to import
ML_Unification.ML_Unification_HOL_Setup
ML_Unification.Unify_Resolve_Tactics
Jan van Brügge (Oct 31 2024 at 15:53):Depending on your goal, just unfolding the simp rules might also work:
lemma
assumes z: ‹example []›
assumes imp: ‹⋀xs ys. (example xs ⟹ example ys ⟹ example (xs @ ys))›
shows ‹example (take 0 [1])›
unfolding take.simps by (rule imp; rule z)
irvin said:
urule might be able to do something like
lemma simpl[uhint]: ‹take 0 [1] = [] @ []› by simp lemma assumes z: ‹example []› assumes imp: ‹⋀xs ys. (example xs ⟹ example ys ⟹ example (xs @ ys))› shows ‹example (take 0 [1])› apply(urule imp) by (fact z)+
Here's the code-golf version:
lemma
assumes ‹example []›
assumes ‹⋀xs ys. (example xs ⟹ example ys ⟹ example (xs @ ys))›
shows ‹example (take 0 [1])›
by (urule (rr) assms) (*resolves with assumptions repeatedly*)
urule apparently seems to be able unify "take 0 [1} = []" so (urule z) works
Kevin Kappelmann (Oct 31 2024 at 16:10):Here's a "funny" way to prove it:
lemma
assumes [uhint]: ‹example []›
shows ‹example (take 0 [1])›
by (urule TrueI)
Since, at the end of the day, all true propositions are just equal to True... :upside_down:
Jonathan Lindegaard Starup (Oct 31 2024 at 18:37):I've tried looking up urule but can't find anything. Is there a place to read about it?
An alternative solution is to phrase my lemmas with .. ==> zs = xs @ ys ==> example zs instead, to make rule work, but that's also a bit tedious.
irvin (Oct 31 2024 at 18:56):I dont think there any documentation on urule and the only public work which uses it is the transport library
irvin (Oct 31 2024 at 18:58):Im not sure how to intuitively explain it. There are some examples here also https://www.isa-afp.org/sessions/ml_unification/#E_Unification_Examples
Last updated: Dec 21 2024 at 16:20 UTC