Induction (help!)

[Achim Schneider]

PR Stanley <prstanley@...> wrote:

> Hi
> One of you chaps mentioned the Nat data type
> data Nat = Zero | Succ Nat
>
> Let's have
> add :: Nat -> Nat -> Nat
> add Zero n = n
> add (Succ m)n = Succ (add m n)
>
> Prove
> add m Zero = m
>
> I'm on the verge of giving up on this. :-(
>

The important point is to learn to regard an infinite number of
terms as one term, and how to mess with it without allowing individual
terms to escape or dangle around.

--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Brent Yorgey]

On Wed, May 7, 2008 at 8:01 PM, PR Stanley <prstanley@...> wrote:

So, when you apply the function to the first element in the set - e.g. Zero or Nil in the case of lists - you're actually testing to see the function works. Then in the inductive step you base everything on the assumption that p holds for some n and of course if that's true then p must hold for Succ n but you have to prove this by taking Succ from n and thus going bakc to its predecessor which is also the hypothesis p(n).
So, to reiterate
assumption: if hypothesis then conclusion
       if p(n) then p(Succ n)
proof of assumption if p(Succ n) = Succ(p(n)) then we've won. If pn+1) = p(n) + p(1) then we have liftoff!
I'm not going to go any further in case I'm once again on the wrong track.
Cheers
Paul

You've got the right idea.  I should point out that it doesn't make sense to say p(Succ n) = Succ(p(n)),  p(x) represents some statement that is either true or false, so it doesn't make sense to say Succ(p(n)).  But I think you are on the right track.

-Brent
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[PR Stanley]

You've got the right idea.
        Paul: At long last! :-)
        I should point out that it doesn't make sense to say p(Succ n) =
Succ(p(n)),  p(x) represents some statement that is either true or
false, so it doesn't make sense to say Succ(p(n)). .
        Paul: okay, da capo: We prove/test through case analysis
that the predicate p holds true for the first/starting case/element
in the sequence. When dealing with natural numbers this could be 0 or
1. We try the formula with 0 and if it returns the desired result we
move onto the next stage. If the formula doesn't work with 0 and so
the predicate does not hold true for the base case then we've proved
that it's a nonstarter.

In the inductive step we'll make a couple of assumptions: we'll
imagine that p(j). We'll also assume that p holds true for the
successor of j - p(j+1).
Then with the help of rules and the protocol available to us we'll
try to establish whether the formula (f) gives us f(j) = f(j+1) - f(1)
So, we know that the predicate holds for 0 or at least one element.
By the way, could we have 3 or 4 or any element other than 0? Anyway,
p(0). Then we set out to find out if p holds for the successor of 0
followed by the successor of the successor of 0 and so forth.
However, rather than laboriously applying p to every natural number
we innstead try to find out if f(j+1) - f(1) will take us back to
fj). I think this was the bit I wasn't getting. The assumptions in
the inductive step and the algebraic procedures are not to prove the
formula or premise per se. That's sort of been done with the base
case. Rather, they help us to illustrate that f remains consistent
while allowing for any random element to be succeeded or broken down
a successive step at a time until we reach the base/starting element/value.
Okay so far?

Cheers
Paul

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Daniel Fischer-4]

Am Freitag, 9. Mai 2008 00:04 schrieb PR Stanley:

> You've got the right idea.
> Paul: At long last! :-)
> I should point out that it doesn't make sense to say p(Succ n) =
> Succ(p(n)),  p(x) represents some statement that is either true or
> false, so it doesn't make sense to say Succ(p(n)). .
> Paul: okay, da capo: We prove/test through case analysis
> that the predicate p holds true for the first/starting case/element
> in the sequence. When dealing with natural numbers this could be 0 or
> 1. We try the formula with 0 and if it returns the desired result we
> move onto the next stage. If the formula doesn't work with 0 and so
> the predicate does not hold true for the base case then we've proved
> that it's a nonstarter.

Well, it might hold for all n >= 3. But you're right, if p doesn't hold for
the base case, then it doesn't hold for _all_ cases.
>
> In the inductive step we'll make a couple of assumptions: we'll
> imagine that p(j). We'll also assume that p holds true for the
> successor of j - p(j+1).

No. In the induction step, we prove that
IF p(j) holds, THEN p(j+1) holds, too.
p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
follows.
Then we have proved
(*) p(j) implies p(j+1), for all j.

If we already have established the base case, p(0), we have
p(0) and (p(0) implies p(1)) - the latter is a special case of (*) - from that
follows p(1).
Then we have
p(1) and (p(1) implies p(2), again a special case of (*), therefore p(2).
Now we have p(2) and (p(2) implies p(3)), hence p(3) and so on.


> Then with the help of rules and the protocol available to us we'll
> try to establish whether the formula (f) gives us f(j) = f(j+1) - f(1)
> So, we know that the predicate holds for 0 or at least one element.
> By the way, could we have 3 or 4 or any element other than 0?

Sure, anything. Start with proving p(1073) and the induction proves p(n) for
all n >= 1073, it does not say anything about n <= 1072.

> Anyway,
> p(0). Then we set out to find out if p holds for the successor of 0
> followed by the successor of the successor of 0 and so forth.
> However, rather than laboriously applying p to every natural number
> we innstead try to find out if f(j+1) - f(1) will take us back to
> fj). I think this was the bit I wasn't getting. The assumptions in
> the inductive step and the algebraic procedures are not to prove the
> formula or premise per se. That's sort of been done with the base
> case. Rather, they help us to illustrate that f remains consistent
> while allowing for any random element to be succeeded or broken down
> a successive step at a time until we reach the base/starting element/value.
> Okay so far?

Not quite, but close.
>
> Cheers
> Paul
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Ryan Ingram]

On 5/8/08, Daniel Fischer <daniel.is.fischer@...> wrote:
> No. In the induction step, we prove that
> IF p(j) holds, THEN p(j+1) holds, too.
> p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
> follows.
> Then we have proved
> (*) p(j) implies p(j+1), for all j.

To formalize this, you can work in a system of logic with the following rules:

Variable introduction:
   x is not free in L,
   L |- t is a type
   proves
   L, x :: t |- x :: t     --- this is a proof of "x has type t"

Forall introduction (removing the above assumption)
   L, x :: t |- p
   proves
   L |- forall x :: t. p

Assumption of a proposition:
   L, p |- p    --- no pre-requisites

Impication introduction ("Deduction"; if P then Q)
   L, p |- q
   proves
   L |- p => q

The part to the left of the |- is an "environment"; it represents
assumptions you have made up to this point.   The part to the right is
a statement which is "true" in that environment; the L just represents
"any environment".

For example, in the first rule, we say that if we know that t is a
type, and we haven't assumed anything about x yet, we can assume that
x is a member of that type.  Then in the second rule, if we've proved
some proposition "p" once we've assumed that x is something of type t,
we can say that p holds for -all- x of type t; we didn't assume
anything about that x besides its type.

Induction corresponds to adding the following rule to the logic:

L |- p(0)
L |- forall x :: Nat, p(x) => p(x+1)
proves
L |- forall x :: Nat, p(x)

A "true" statement is one that holds with no environment:
|- p

Now, if you are proving something by induction, you had to prove that
second line; and the only way to do so is by making some assumptions.
A skeleton of a proof:

axiom
|- Nat is a type

variable introduction
x :: Nat |- x :: Nat

proposition introduction
x :: Nat, p(x) |- p(x)

... some proof using p(x) here ...
x :: Nat, p(x) |- p(x+1)

deduction
x :: Nat |- p(x) => p(x+1)

forall introduction
|- forall x :: Nat, p(x) => p(x+1)

... some proof of p(0) here ...
|- p(0)

induction
|- forall x :: Nat, p(x)

Every proof by induction looks basically like this; you just need to
fill in the "... some proof here..." parts.

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[PR Stanley]

        Paul: okay, da capo: We prove/test through case analysis
 > that the predicate p holds true for the first/starting case/element
 > in the sequence. When dealing with natural numbers this could be 0 or
 > 1. We try the formula with 0 and if it returns the desired result we
 > move onto the next stage. If the formula doesn't work with 0 and so
 > the predicate does not hold true for the base case then we've proved
 > that it's a nonstarter.

        Well, it might hold for all n >= 3. But you're right, if p doesn't hold for
the base case, then it doesn't hold for _all_ cases.
        Paul: I don't understand the point you're contending. We've chosen 0
as our base case and if p(0) doesn't hold then nothing else will for
our proof. Granted, you may want to start from 3 or 4 as your base
case but we're not doing that here and for all we know forall n >= 3
p(n) but this isn't relevant to our proof, surely.
 >
        Paul: In the inductive step we'll make a couple of assumptions: we'll
 > imagine that p(j). We'll also assume that p holds true for the
 > successor of j - p(j+1).

        Daniel: No. In the induction step, we prove that
IF p(j) holds, THEN p(j+1) holds, too.
p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
follows.
Then we have proved
(*) p(j) implies p(j+1), for all j.
        Paul: No, you haven't proved anything! I'm sorry but your assertion
fails to make much sense.

        Daniel: If we already have established the base case, p(0), we have
p(0) and (p(0) implies p(1)) - the latter is a special case of (*) - from that
follows p(1).
Then we have
p(1) and (p(1) implies p(2), again a special case of (*), therefore p(2).
Now we have p(2) and (p(2) implies p(3)), hence p(3) and so on.

        Paul: Then with the help of rules and the protocol available to us we'll
 > try to establish whether the formula (f) gives us f(j) = f(j+1) - f(1)
 > So, we know that the predicate holds for 0 or at least one element.
 > By the way, could we have 3 or 4 or any element other than 0?

        Daniel: Sure, anything. Start with proving p(1073) and the induction
proves p(n) for
all n >= 1073, it does not say anything about n <= 1072.

        Paul: p(0). Then we set out to find out if p holds for the successor of 0
 > followed by the successor of the successor of 0 and so forth.
 > However, rather than laboriously applying p to every natural number
 > we innstead try to find out if f(j+1) - f(1) will take us back to
 > fj). I think this was the bit I wasn't getting. The assumptions in
 > the inductive step and the algebraic procedures are not to prove the
 > formula or premise per se. That's sort of been done with the base
 > case. Rather, they help us to illustrate that f remains consistent
 > while allowing for any random element to be succeeded or broken down
 > a successive step at a time until we reach the base/starting element/value.
 > Okay so far?

Cheers,
Paul

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Daniel Fischer-4]

Am Freitag, 9. Mai 2008 13:50 schrieb PR Stanley:

> Paul: okay, da capo: We prove/test through case analysis
>
>  > that the predicate p holds true for the first/starting case/element
>  > in the sequence. When dealing with natural numbers this could be 0 or
>  > 1. We try the formula with 0 and if it returns the desired result we
>  > move onto the next stage. If the formula doesn't work with 0 and so
>  > the predicate does not hold true for the base case then we've proved
>  > that it's a nonstarter.
>
> Well, it might hold for all n >= 3. But you're right, if p doesn't hold
> for the base case, then it doesn't hold for _all_ cases.
> Paul: I don't understand the point you're contending. We've chosen 0
> as our base case and if p(0) doesn't hold then nothing else will for
> our proof. Granted, you may want to start from 3 or 4 as your base
> case but we're not doing that here and for all we know forall n >= 3
> p(n) but this isn't relevant to our proof, surely.

Right. I only wanted to say that we might have chosen the wrong base case for
the proposition. If p(0) doesn't hold, then obviously [for all n. p(n)]
doesn't hold. But [for all n. p(n) implies p(n+1)] could still be true, and
in that case, if e.g. p(3) holds, then [for all n >= 3. p(n)] holds.
So if the base case fails, still a large portion of the proposition might be
saved, but if the induction step fails, that is not so.

>
> Paul: In the inductive step we'll make a couple of assumptions: we'll
>
>  > imagine that p(j). We'll also assume that p holds true for the
>  > successor of j - p(j+1).
>
> Daniel: No. In the induction step, we prove that
> IF p(j) holds, THEN p(j+1) holds, too.
> p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
> follows.
> Then we have proved
> (*) p(j) implies p(j+1), for all j.
> Paul: No, you haven't proved anything! I'm sorry but your assertion
> fails to make much sense.

Sorry? The induction step consists of proving that
WHATEVER j is, IF p(j) holds, THEN p(j+1) holds, too.

If or when we have done that, it is tautological to say that we proved
(*) for all j. [p(j) implies p(j+1)].

In the notation used by Ryan Ingram yesterday, the induction step consists of
proving

L, j :: Nat |- p(j) => p(j+1)

typically, that is done via proving

L, j :: Nat, p(j) |- p(j+1)

, i.e. proving p(j+1) under the assumption p(j), which by the logical rule of
deduction/implication introduction is equivalent to

L, j :: Nat |- p(j) => p(j+1).

>
> Daniel: If we already have established the base case, p(0), we have
> p(0) and (p(0) implies p(1)) - the latter is a special case of (*) - from
> that follows p(1).
> Then we have
> p(1) and (p(1) implies p(2), again a special case of (*), therefore p(2).
> Now we have p(2) and (p(2) implies p(3)), hence p(3) and so on.
>
> Paul: Then with the help of rules and the protocol available to us we'll
>
>  > try to establish whether the formula (f) gives us f(j) = f(j+1) - f(1)
>  > So, we know that the predicate holds for 0 or at least one element.
>  > By the way, could we have 3 or 4 or any element other than 0?
>
> Daniel: Sure, anything. Start with proving p(1073) and the induction
> proves p(n) for
> all n >= 1073, it does not say anything about n <= 1072.
>
> Paul: p(0). Then we set out to find out if p holds for the successor of 0
>
>  > followed by the successor of the successor of 0 and so forth.
>  > However, rather than laboriously applying p to every natural number
>  > we innstead try to find out if f(j+1) - f(1) will take us back to
>  > fj). I think this was the bit I wasn't getting. The assumptions in
>  > the inductive step and the algebraic procedures are not to prove the
>  > formula or premise per se. That's sort of been done with the base
>  > case. Rather, they help us to illustrate that f remains consistent
>  > while allowing for any random element to be succeeded or broken down
>  > a successive step at a time until we reach the base/starting
>  > element/value. Okay so far?
>
> Cheers,
> Paul

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Ryan Ingram]

On 5/9/08, Daniel Fischer <daniel.is.fischer@...> wrote:
> Right. I only wanted to say that we might have chosen the wrong base case for
> the proposition. If p(0) doesn't hold, then obviously [for all n. p(n)]
> doesn't hold. But [for all n. p(n) implies p(n+1)] could still be true, and
> in that case, if e.g. p(3) holds, then [for all n >= 3. p(n)] holds.
> So if the base case fails, still a large portion of the proposition might be
> saved, but if the induction step fails, that is not so.

Note that this is reasonably trivial to translate into a regular
inductive proof:

let q(x) = p(x) OR (x < 3).
given forall y :: Nat, (y >= 3) => p(y) => p(y+1)
given p(3)

given x :: Nat, and q(x)
x < 2 or x == 2 or x > 2

case (x < 2):
    x+1 <= 2
    q(x+1) holds trivially; x+1 < 3.
case (x == 2)
    x+1 == 3
    p(3) holds (given)
    therefore q(3) holds
    therefore q(x+1) holds
case (x > 2)
    q(x) holds, so either p(x) holds or (x < 3).
    case (x < 3):
        x > 2 and x < 3 is a contradiction.
    case q(x) holds:
        forall y :: Nat, (y >= 3) => p(y) => p(y+1) (given)
        (x >= 3) => p(x) => p(x+1)  (instantiate with y <- x)
        (x >= 3) (since x > 2)
        p(x+1)  (derive from p(x) and x >= 3 and the instantiation)
        (x < 3) or p(x+1)
        therefore q(x+1)

so, forall x::Nat, q(x) => q(x+1).
p(0) is trivial (x < 3).

so, forall x::Nat, q(x)
which means forall x :: Nat, x >= 3 => p(x).

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe