Stream: Beginner Questions

Topic: show


view this post on Zulip 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"])

view this post on Zulip Manuel Eberl (Apr 14 2021 at 11:23):

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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Apr 14 2021 at 11:51):

the induction tactic might be having a problem with a goal shaped shows X and Y

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Apr 14 2021 at 11:55):

do the induction rules in question have the right number of conclusions?

view this post on Zulip 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)

view this post on Zulip Lukas Stevens (Apr 14 2021 at 12:00):

The problem is the and.

view this post on Zulip 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)

view this post on Zulip Lukas Stevens (Apr 14 2021 at 12:11):

Because the induction rule probably does not consume/eliminate "atom (x::var) ♯ Γ"

view this post on Zulip 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))"

view this post on Zulip Jan van Brügge (Apr 14 2021 at 12:15):

I guess it can't be helped

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Apr 14 2021 at 13:19):

But induct/induction normally work without consuming all the facts as well, right?

view this post on Zulip 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"?

view this post on Zulip 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)

view this post on Zulip Jakub Kądziołka (Apr 14 2021 at 13:27):

(also, paste your code inside

 ```isabelle
 ...
 ```

to make it look nice and preserve indentation)

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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].......

view this post on Zulip Jakub Kądziołka (Apr 14 2021 at 13:37):

why would it automatically assume x \<in> G?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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}

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip zibo yang (Apr 14 2021 at 14:54):

what is the difference between unfolding and using

view this post on Zulip 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: Aug 13 2022 at 05:18 UTC