On 5/9/08, Daniel Fischer <[EMAIL PROTECTED]> 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe