Stream: Beginner Questions

Topic: ✔ Failure to apply induction on a theorem


view this post on Zulip Mathias Fleury (Sep 04 2022 at 15:30):

Simpler version: always use ==>

view this post on Zulip Mathias Fleury (Sep 04 2022 at 15:30):

Only exception: when you work under \forall

view this post on Zulip Notification Bot (Sep 04 2022 at 16:02):

Alex Weisberger has marked this topic as resolved.

view this post on Zulip Wolfgang Jeltsch (Sep 04 2022 at 17:12):

Mathias Fleury said:

Only exception: when you work under \forall

But then, when do you work under ∀? You can and usually should use ⋀ instead. You have to use ⟶ and ∀ only where you have to use bool, which typically is in a definition.

view this post on Zulip Alex Weisberger (Sep 05 2022 at 00:50):

What about expressing this as:

theorem "⟦beval1 t t'; beval1 t t''⟧ ⟹ t' = t''"

This seems to work as well, and for me is a little more clear because the premises are clearly grouped together.

view this post on Zulip Mathias Fleury (Sep 05 2022 at 04:24):

Wolfgang Jeltsch said:
You have to use ⟶ and ∀ only where you have to use bool, which typically is in a definition.

This is what i meant with \forall…

Wolfgang Jeltsch said:
But then, when do you work under ∀? You can and usually should use ⋀ instead.

I don't agree: all tactics and compositon work on ==> and !! (induction, rule, OF, of, ...). Hence the default choice for theorems should always be the Pure symbols

view this post on Zulip Wolfgang Jeltsch (Sep 05 2022 at 11:09):

Mathias Fleury said:

Wolfgang Jeltsch said:
But then, when do you work under ∀? You can and usually should use ⋀ instead.

I don't agree: all tactics and compositon work on ==> and !! (induction, rule, OF, of, ...). Hence the default choice for theorems should always be the Pure symbols

Isn’t this what I said above? :wink:

view this post on Zulip Mathias Fleury (Sep 05 2022 at 11:10):

ah sorry I misunderstood you then…

view this post on Zulip Mathias Fleury (Sep 05 2022 at 11:10):

I thought that your You can and usually should use ⋀ instead was meant in general, and not only below ∀

view this post on Zulip Wolfgang Jeltsch (Sep 05 2022 at 17:09):

Mathias Fleury said:

I thought that your You can and usually should use ⋀ instead was meant in general, and not only below ∀

Of course, it was meant in general, and that’s what you’re saying as well, right? I mean, is the same as !!, a pure symbol, and you’re saying, “Hence the default choice for theorems should always be the Pure symbols”.

view this post on Zulip Mathias Fleury (Sep 05 2022 at 18:03):

I find ‹⋀∧› and ⋀∧ too hard to distinguish


Last updated: Mar 28 2024 at 16:17 UTC