Re: [Hol-info] How to do this kind of induction?

[Chun Tian (binghe)]

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 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” 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) 
> > mailto:binghe.l...@gmail.com>> ha scritto:
> >
> > 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
> >
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to do this kind of induction?

[Konrad Slind]

... 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 = 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” 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) <
>> binghe.l...@gmail.com> ha scritto:
>> >
>> > 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
>> >
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to do this kind of induction?

[Konrad Slind]

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” 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) <
> binghe.l...@gmail.com> ha scritto:
> >
> > 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
> >
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to do this kind of induction?

[Chun Tian (binghe)]

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 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
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] How to do this kind of induction?

[Chun Tian (binghe)]

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
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info