Skip to content

Instantly share code, notes, and snippets.

@gallais

gallais/sum_of_pow.v

Last active August 29, 2015 14:05
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gallais/f687b7b14ba11e0a342d to your computer and use it in GitHub Desktop.
Save gallais/f687b7b14ba11e0a342d to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sum_of_pow.v
Require Import NArith.
Fixpoint sum_of (f : nat -> nat) (n : nat) : nat :=
match n with
| O => f O
| S m => f (S m) + sum_of f m
end.
Lemma sum_of_pow : forall n,
S (sum_of (NPeano.pow 2) n) = NPeano.pow 2 (S n).
intro n; induction n.
- reflexivity.
- simpl sum_of ; rewrite plus_n_Sm, IHn.
simpl ; repeat rewrite <- plus_n_O ; reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment