/- Clara L"oh 2021 -/

import tactic   -- standard proof tactics
open finset     -- for range operator
open_locale big_operators -- to enable ∑ notation

open classical  -- we want to work in classical logic

/-
# A simple induction proof
-/

-- we define geometric sums (at base 2) ...
def geometric_sum
  : nat → nat
| 0            := 1 
| (nat.succ n) := geometric_sum n + 2^(n+1)

-- ... and show how they can be computed
lemma geometric_sum_eval
      (n : nat)
    : geometric_sum n = 2^(n+1) - 1
:= 
begin
  -- we prove this claim by induction (over the natural number argument n);
  -- here, m is the variable used in the induction step 
  -- and ind_hyp is the induction hypothesis used in the induction step
  induction n with m ind_hyp,

  -- base case: 0
  case nat.zero : {simp[geometric_sum]},

  -- induction step: m -> m+1
  case nat.succ : 
  begin
    calc geometric_sum (m+1) = geometric_sum m + 2^(m+1) : by {simp[geometric_sum]}
                        ...  = 2^(m+1) - 1 + 2^(m+1)     : by {simp[ind_hyp]}
                        ...  = 2^(m+1) + 2^(m+1) - 1     : by {omega}
                        ...  = 2 * 2^(m+1) - 1           : by {ring}
                        ...  = 2^(m+2) - 1               : by {ring},
  end
end      

-- computing some examples:
#eval geometric_sum 0
#eval geometric_sum 5


/-
# Using the ∑ notation
-/

-- and another simple sum, 
-- using the sum operator from mathlib (big_operators)
def one_sum 
  : nat → nat
:= λ n : nat, 
   ∑ (i : nat) in range n, 1

lemma one_sum_eval
      (n : nat)
    : (one_sum n = n)
:=
begin
  -- we prove this claim by induction (over the natural number argument n)
  induction n with m ind_hyp,

  -- base case: 0 
  case nat.zero : {simp[one_sum]},

  -- induction step: m -> m+1
  case nat.succ : 
  begin
    calc one_sum (m+1) = ∑ (i : nat) in range (m+1), 1   : by {simp[one_sum]}
                   ... = (∑ (i : nat) in range m, 1) + 1 : by {simp}
                   ... = m + 1                           : by {simp[ind_hyp]},
  end
  /-
  unfold one_sum,
  -- found by library_search :)
  by {exact sum_range_induction (λ (k : ℕ), 1) (λ (n : ℕ), n) rfl (congr_fun rfl) n},
  -/  
end