Hi,
thanks, I should really again the Euclid's Theorem tutorial. I fixed `i` and
directly do induction on `j`, then it also worked with some cases analysis.
—Chun
> Il giorno 05 gen 2019, alle ore 22:20, Konrad Slind
> ha scritto:
>
> There is discussion of something like this in the
... also meant to mention that "Induct_on" and "completeInduct_on" have
online documentation.
On Sat, Jan 5, 2019 at 3:20 PM Konrad Slind wrote:
> There is discussion of something like this in the Euclid's Theorem
> tutorial. You can do Induct_on `j - i` or do the trick where you prove ?k.
> j
There is discussion of something like this in the Euclid's Theorem
tutorial. You can do Induct_on `j - i` or do the trick where you prove ?k.
j = i + SUC k, eliminate j, and then induct on k.
Konrad.
On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe)
wrote:
> sorry, "i ≤ j” should be “i < j”
sorry, "i ≤ j” should be “i < j” actually:
∀i j. i < j ⇒ f (SUC i) ⊆ f j
0. ∀n. f n ⊆ f (SUC n)
1. ∀n. 0 < n ⇒ f 0 ⊆ f n
> Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe)
> ha scritto:
>
> Hi,
>
> I have the following goal to
Hi,
I have the following goal to prove: (f : num -> ‘a set)
∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
0. ∀n. f n ⊆ f (SUC n)
but how can I do the induction on … e.g. `j - i`?
—Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
