Jan van Brügge (Apr 14 2021 at 11:12): Jan van Brügge (Apr 14 2021 at 11:12):What does "Rule has fewer conclusions than the arguments given" mean exactly? I am trying to mutually induct over a inductive, but somehow I am messing up. I even tried explicity instanciating the goals:
lemma fresh_in_context_term_var:
assumes "atom (x::var) ♯ Γ"
shows "Γ , Δ ⊢ e : τ ⟶ atom x ♯ e"
and "Alts Γ Δ T σs τ1 alts τ ⟶ atom x ♯ alts"
using assms proof (induction Γ Δ e τ and Γ Δ T σs τ1 alts τ rule: Tm_Alts.induct[of "λ_ _ e _. atom x ♯ e" "λ_ _ _ _ _ alts _. atom x ♯ alts"])
If possible, please post a full example (including all the relevant definitions, or at least dummies for the constants/notation used) so that people can try it out themselves.
Manuel Eberl (Apr 14 2021 at 11:24):In any case, I think instantiating the induction rule manually like this is only going to confuse the induction method. If you want to instantiate stuff by hand for debugging purposes, you can try applying the induction rule manually with e.g. rule.
Jan van Brügge (Apr 14 2021 at 11:30):I tried it first without instantiating, but with the same error. I pushed the code and this is the lemma: https://github.com/jvanbruegge/isabelle-lambda-calculus/blob/case-expressions/Typing.thy#L214
Jan van Brügge (Apr 14 2021 at 11:43):It works if I use proof (rule Tm_Alts.induct, goal_cases), but why not with the induction method?
Jan van Brügge (Apr 14 2021 at 11:50):lemma fresh_in_context_term_var:
assumes "atom (x::var) ♯ Γ"
shows "Γ , Δ ⊢ e : τ ⟹ atom x ♯ e"
and "Alts Γ Δ T σs τ1 alts τ ⟹ atom x ♯ alts"
proof -
have "(Γ , Δ ⊢ e : τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ e)) ∧ (Alts Γ Δ T σs τ1 alts τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ alts))"
proof (rule Tm_Alts.induct, goal_cases)
(* ... *)
qed
then show "Γ , Δ ⊢ e : τ ⟹ atom x ♯ e" and "Alts Γ Δ T σs τ1 alts τ ⟹ atom x ♯ alts" using assms by auto
qed
the induction tactic might be having a problem with a goal shaped shows X and Y
Jan van Brügge (Apr 14 2021 at 11:53):no, it works for other lemmas: https://github.com/jvanbruegge/isabelle-lambda-calculus/blob/case-expressions/Lemmas.thy#L178
Jakub Kądziołka (Apr 14 2021 at 11:55):do the induction rules in question have the right number of conclusions?
Jan van Brügge (Apr 14 2021 at 11:55):yes, it looks like this:
(?x1.0 , ?x2.0 ⊢ ?x3.0 : ?x4.0 ⟶ ?P1.0 ?x1.0 ?x2.0 ?x3.0 ?x4.0) ∧ (Alts ?x5.0 ?x6.0 ?x7.0 ?x8.0 ?x9.0 ?x10.0 ?x11.0 ⟶ ?P2.0 ?x5.0 ?x6.0 ?x7.0 ?x8.0 ?x9.0 ?x10.0 ?x11.0)
The problem is the and.
Jan van Brügge (Apr 14 2021 at 12:05):ok, this works, but as soon as I try to add using assms proof it fails again with "Failed to apply initial proof method"
lemma fresh_in_context_term_var:
assumes "atom (x::var) ♯ Γ"
shows "(Γ , Δ ⊢ e : τ ⟶ atom x ♯ e) ∧ (Alts Γ Δ T σs τ1 alts τ ⟶ atom x ♯ alts)"
proof (induction rule: Tm_Alts.induct)
Because the induction rule probably does not consume/eliminate "atom (x::var) ♯ Γ"
Jan van Brügge (Apr 14 2021 at 12:11):Yes, but formulating the goal like this is annoying to prove because of the extra implication
"(Γ , Δ ⊢ e : τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ e)) ∧ (Alts Γ Δ T σs τ1 alts τ ⟶ (atom x ♯ Γ ⟶ atom x ♯ alts))"
I guess it can't be helped
Lukas Stevens (Apr 14 2021 at 12:16):You could define a new induction rule that consumes the assumption and puts it into the hypothesis. Doesn't make sense for a one-off though.
Manuel Eberl (Apr 14 2021 at 13:19):But induct/induction normally work without consuming all the facts as well, right?
zibo yang (Apr 14 2021 at 13:20):section ‹Abelian Groups›
context abelian_group
begin
definition minus:: "'a ⇒ 'a ⇒ 'a" (infixl "‐" 70)
where "x ‐ y ≡ x ⋅ inverse y "
lemma vsdf:"x ⋅ y = 𝟭 ⟹ x = inverse y"
proof(unfold_locales,auto)
assume xg:"x ∈ G" and yg:"y ∈ G"" x ⋅ y = 𝟭"
from this have "y ⋅ x = 𝟭" by (simp add: commutative)
from this and xg and yg show"x = inverse y" by (simp add:inverse_equality)
qed
end (* abelian_group*)
can someone help me with why it indicates:
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(x ∈ G) ⟹
(y ∈ G) ⟹ (x ⋅ y = 𝟭) ⟹ x = local.inverse y
when I use "show" in the last line but it's ok if "show" is replaced by "have"?
Jakub Kądziołka (Apr 14 2021 at 13:25):(Note: if you're just interested in the group, you'll want comm_group instead. The abelian_group locale talks about the additive group of a ring)
Jakub Kądziołka (Apr 14 2021 at 13:27):(also, paste your code inside
```isabelle
...
```
to make it look nice and preserve indentation)
Jakub Kądziołka (Apr 14 2021 at 13:29):okay now that I've loaded up Isabelle with HOL-Algebra it seems that you're defining your own abelian_group locale. Leaving aside why you'd want to do that, there isn't really a good way to check the code out locally and poke around...
Jakub Kądziołka (Apr 14 2021 at 13:29):anyway, this error usually means that you assumed something that isn't part of the goal
Jakub Kądziołka (Apr 14 2021 at 13:31):you shouldn't need unfold_locales unless you're proving a statement with the shape locale_name some_object
Jakub Kądziołka (Apr 14 2021 at 13:32):fundamentally, the issue is that your xg and yg assumptions are unfounded, I think. You might be interested in how HOL-Algebra solves this problem: https://github.com/NieDzejkob/isabelle-math-contests/blob/master/NOTES.md#the-two-definitions-of-a-group
Jakub Kądziołka (Apr 14 2021 at 13:33):also, some Isar style tips: from this have = hence; from this and xg and yg show = with xg and yg show or with xg yg show
zibo yang (Apr 14 2021 at 13:36):I found something very interesting but strange is that: when I add [ x \<in > G; y \<in> G] into the lemma, it works. but why does Isabelle think it reasonable when I state nothing like [ x \<in > G; y \<in> G]? I always think when I state x \<cdot> y, it should indicate [ x \<in > G; y \<in> G].......
Jakub Kądziołka (Apr 14 2021 at 13:37):why would it automatically assume x \<in> G?
zibo yang (Apr 14 2021 at 13:41):because \<cdot> should be the type"G -> G -> G" when it was initialized, isabelle should infer x \<in> G
Jakub Kądziołka (Apr 14 2021 at 13:42):Every expression in Isabelle has some type, and if you don't specify it (for example with fixes a :: nat and S :: "nat set" in the lemma statement), the most general type will be inferred (in a lemma, based on its statement. For example a :: 'a and S :: 'a set, for any type variable 'a). However, G is not a type here, but a set — simply, a value of type 'something set. The multiplication is defined (like all functions in HOL) on an entire type, not just a set.
zibo yang (Apr 14 2021 at 13:46):ok. I am a bit clear with that. so it's the same reason why we need to clarify the type (1::nat) + 1?
Jakub Kądziołka (Apr 14 2021 at 13:47):yeah, kinda — inference will give both your 1s the type 'a with a sort constraint 'a::{plus, and_probably_something_else_I_forget}
Jakub Kądziołka (Apr 14 2021 at 13:48):BTW, are you creating your own algebra library because you're unaware of the existing one, or on purpose as practice?
zibo yang (Apr 14 2021 at 13:50):the situation is more closed to practice but I still wanna refer that lemma in another file
zibo yang (Apr 14 2021 at 14:54):what is the difference between unfolding and using
Jakub Kądziołka (Apr 14 2021 at 14:56):unfolding some_fact where some_fact is of the form A = B will replace all occurences of A with B in your goal before running the tactic. using will simply pass on the fact to the tactic. They have quite a similar effect if you're using, for example, by simp
Last updated: Dec 21 2024 at 16:20 UTC