Stream: Beginner Questions

Topic: ✔ Failure to apply induction on a theorem

Mathias Fleury (Sep 04 2022 at 15:30):

Simpler version: always use ==>

Mathias Fleury (Sep 04 2022 at 15:30):

Only exception: when you work under \forall

Notification Bot (Sep 04 2022 at 16:02):

Alex Weisberger has marked this topic as resolved.

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.

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.

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

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:

Mathias Fleury (Sep 05 2022 at 11:10):

ah sorry I misunderstood you then…

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 ∀

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”.

Mathias Fleury (Sep 05 2022 at 18:03):

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

Last updated: Dec 21 2024 at 12:33 UTC