ℕ.dt

module ℕ

syntax ℕ  = Zero
          | S(ℕ)


judgment sum = Sum(ℕ, ℕ, ℕ)

rule schema sum-zero for all objects (n : ℕ) :
|
|-------------------------------------- sum-zero
| Sum(Zero, n, n)


rule schema sum-suc for all objects (m : ℕ), (n : ℕ), (o : ℕ) :
| Sum(m, n, o)
|-------------------------------------- sum-s
| Sum(S(m), n, S(o))




theorem total : ∀ (n₁ : ℕ) (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(n₁, n₂, n₃)
∀ (n₁ : ℕ) (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(n₁, n₂, n₃)  by induction :

  case Zero -> 
    |
    |--------------------------------------------------------------------------------------------
    | --  let's prove the base case
    | --  ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( Zero , n₂ , n₃ )
    |
    | uni-n2 :  | for all (n2 : ℕ)
    |           |--------------------------------------------------------------------------------
    |           |
    |           | sz : Sum( Zero , n2 , n3 )  by rule sum-zero
    |           | ∃ (n₃ : ℕ) : Sum( Zero , n2 , n₃ )  by rule ∃-intro on sz
    |
    | result : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( Zero , n₂ , n₃ )  by rule ∀-intro on uni-n2


  case Suc(m) ->  

    | induction-hypothesis : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( m , n₂ , n₃ )
    |--------------------------------------------------------------------------------------------
    | --  let's prove the inductive case
    | --  { ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( m , n₂ , n₃ ) }
    | --    ==> { ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( S(m) , n₂ , n₃ ) }
    |
    | uni-n2b : | for all (N2 : ℕ)
    |           |--------------------------------------------------------------------------------
    |           |  
    |           | d1 : ∃ (n₃ : ℕ) : Sum( m , N2 , n₃ )  by rule ∀-elim on induction-hypothesis
    |           |
    |           | exn3 :  | p5 : Sum( m , N2 , n3 ) for some (n3 : ℕ)
    |           |         |----------------------------------------------------------------------
    |           |         |
    |           |         | sum-m+1 : Sum( S(m) , N2 , S(n3) )  by rule sum-s on p5
    |           |         | ∃ (n₃ : ℕ) : Sum( S(m) , N2 , n₃ )  by rule ∃-intro on sum-m+1
    |           |
    |           | ∃ (n₃ : ℕ) : Sum( S(m) , N2 , n₃ )  by rule ∃-elim on d1, exn3
    |
    | ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( S(m) , n₂ , n₃ )  by rule ∀-intro on uni-n2b




--
--  We can leave proving this theorem to the tool.
--
theorem n+0=n : ∀ (N : ℕ) : Sum(N, Zero, N)
prove ∀ (N : ℕ) : Sum(N, Zero, N)




--
--  We can leave proving this theorem to the tool.
--
theorem sum-s-rhs : ∀ (N1 : ℕ) (N2 : ℕ) (N3 : ℕ) : Sum(N1, N2, N3) ==> Sum(N1, Suc(N2), Suc(N3))
prove ∀ (N1 : ℕ) (N2 : ℕ) (N3 : ℕ) : Sum(N1, N2, N3) ==> Sum(N1, Suc(N2), Suc(N3))




--
--  This is the theorem from the paper, but proved completely manually.
--  The version from the paper is below.
--
theorem sum-total-comm-manual : ∀ (n₁, n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(n₁, n₂, n₃) ∧ Sum(n₂, n₁, n₃)

N+0=N : ∀ (N : ℕ) : Sum(N, Zero, N)  by theorem n+0=n

∀ (n₁ : ℕ) (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(n₁, n₂, n₃) ∧ Sum(n₂, n₁, n₃)  by induction :

  case Zero ->
    |
    |--------------------------------------------------------------------------
    |
    | 1 : | for any (N₂ : ℕ)
    |     |--------------------------------------------------------------------
    |     |
    |     | 2 : Sum(Zero, N₂, N₂)  by rule sum-zero
    |     | 3 : Sum(N₂, Zero, N₂)  by rule ∀-elim on N+0=N
    |     | 4 : Sum(Zero, N₂, N₂) ∧ Sum(N₂, Zero, N₂)  by rule ∧-intro on 2,3
    |     | 5 : ∃ (n₃ : ℕ) : Sum(Zero, N₂, n₃) ∧ Sum(N₂, Zero, n₃)  by rule ∃-intro on 4
    |
    | 2 : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(Zero, n₂, n₃) ∧ Sum(n₂, Zero, n₃)  by rule ∀-intro on 1

  case S(m) ->
    | ind-hyp : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(m, n₂, n₃) ∧ Sum(n₂, m, n₃)
    |----------------------------------------------------------------------------------------------
    |
    | 1 : | for any (N₂' : ℕ)
    |     |----------------------------------------------------------------------------------------
    |     |
    |     | ∃ (n₃ : ℕ) : Sum(S(m), N₂', n₃) ∧ Sum(N₂', S(m), n₃)  by case analysis on N₂' :
    |     |
    |     |   case Zero ->
    |     |     |
    |     |     |----------------------------------------------------------------------------------
    |     |     |
    |     |     | 1 : Sum(S(m), Zero, S(m))  by rule ∀-elim on N+0=N
    |     |     | 2 : Sum(Zero, S(m), S(m))  by rule sum-zero
    |     |     | 3 : Sum(S(m), Zero, S(m)) ∧ Sum(Zero, S(m), S(m))  by rule ∧-intro on 1, 2
    |     |     | 4 : ∃ (n₃ : ℕ) : Sum(S(m), Zero, n₃) ∧ Sum(Zero, S(m), n₃)  by rule ∃-intro on 3
    |     |
    |     |   case S(m') ->
    |     |     |
    |     |     |----------------------------------------------------------------------------------
    |     |     |
    |     |     | 1 : ∃ (n₃ : ℕ) : Sum(m, S(m'), n₃) ∧ Sum(S(m'), m, n₃)  by rule ∀-elim on ind-hyp
    |     |     | 2 : | p : Sum(m, S(m'), n₃') ∧ Sum(S(m'), m, n₃') for some (n₃' : ℕ)
    |     |     |     |----------------------------------------------------------------------------
    |     |     |     |
    |     |     |     | 3 : Sum(m, S(m'), n₃')  by rule ∧-elim on p
    |     |     |     | 4 : Sum(S(m'), m, n₃')  by rule ∧-elim on p
    |     |     |     | 5 : Sum(S(m), S(m'), S(n₃'))  by rule sum-suc on 3
    |     |     |     | 6 : ∀ (N1 : ℕ) (N₂ : ℕ) (n₃' : ℕ) : Sum(N1, N₂, n₃') ==> Sum(N1, S(N₂), S(n₃')) by theorem sum-s-rhs
    |     |     |     | 7 : Sum(S(m'), m, n₃') ==> Sum(S(m'), S(m), S(n₃'))  by rule ∀-elim on 6
    |     |     |     | 8 : Sum(S(m'), S(m), S(n₃'))  by rule ==>-elim on 7, 4
    |     |     |     | 9 : Sum(S(m), S(m'), S(n₃')) ∧ Sum(S(m'), S(m), S(n₃'))  by rule ∧-intro on 5, 8
    |     |     |     | 10 : ∃ (n₃ : ℕ) : Sum(S(m), S(m'), n₃) ∧ Sum(S(m'), S(m), n₃)  by rule ∃-intro on 9
    |     |     |
    |     |     | 9 : ∃ (n₃ : ℕ) : Sum(S(m), S(m'), n₃) ∧ Sum(S(m'), S(m), n₃)  by rule ∃-elim on 1, 2
    |
    | 2 : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum(S(m), n₂, n₃) ∧ Sum(n₂, S(m), n₃)  by rule ∀-intro on 1



--
--  This is the theorem from the paper.
--
theorem sum-total-comm : ∀ (n₁, n₂ : N) : ∃ (n₃ : N) : Sum(n₁, n₂, n₃) ∧ Sum(n₂, n₁, n₃)
∀ (n₁ : N) (n₂ : N) : ∃ (n₃ : N) : Sum(n₁, n₂, n₃) ∧ Sum(n₂, n₁, n₃) by induction :
case Zero ->
  |
  |----------------------------------------------------------------------------
  | a: prove ∀ (n₂ : N) : ∃ (n₃ : N) : Sum(Zero, n₂, n₃) ∧ Sum(n₂, Zero, n₃)

case S(m₁) ->
  | ind-hyp: ∀ (n₂ : N) : ∃ (n₃ : N) : Sum(m₁, n₂, n₃) ∧ Sum(n₂, m₁, n₃)
  |------------------------------------------------------------------------------------------------
  | b:  | for any (N₂ : N)
  |     |------------------------------------------------------------------------------------------
  |     | ∃ (n₃ : N) : Sum(S(m₁), N₂, n₃) ∧ Sum(N₂, S(m₁), n₃) by case analysis on N₂ :
  |     | case Zero ->
  |     |   |
  |     |   |------------------------------------------------------------------
  |     |   | c: prove ∃ (n₃ : N) : Sum(S(m₁), Zero, n₃) ∧ Sum(Zero, S(m₁), n₃)
  |     |
  |     | case S(m₂) ->
  |     |   |
  |     |   |--------------------------------------------------------------------------------------
  |     |   | d: ∃ (n₃ : N) : Sum(m₁, S(m₂), n₃) ∧ Sum(S(m₂), m₁, n₃) by rule ∀-elim on ind-hyp
  |     |   | e:  | p: Sum(m₁, S(m₂), N₃) ∧ Sum(S(m₂), m₁, N₃) for some (N₃ : N)
  |     |   |     |--------------------------------------------------------------------------------
  |     |   |     | f: Sum(m₁, S(m₂), N₃) by rule ∧-elim on p
  |     |   |     | g: Sum(S(m₂), m₁, N₃) by rule ∧-elim on p
  |     |   |     | h: Sum(S(m₁), S(m₂), S(N₃)) by rule sum-s on f
  |     |   |     | i: ∀ (n₁,n₂,n₃ : N): Sum(n₁, n₂, n₃) ==> Sum(n₁, S(n₂), S(n₃)) by theorem sum-s-rhs
  |     |   |     | j: Sum(S(m₂), m₁, N₃) ==> Sum(S(m₂), S(m₁), S(N₃)) by rule ∀-elim on i
  |     |   |     | k: Sum(S(m₂), S(m₁), S(N₃)) by rule ==>-elim on j, g
  |     |   |     | l: Sum(S(m₁), S(m₂), S(N₃)) ∧ Sum(S(m₂), S(m₁), S(N₃)) by rule ∧-intro on h, k
  |     |   |     | m: ∃ (n₃: N): Sum(S(m₁), S(m₂), n₃) ∧ Sum(S(m₂), S(m₁), n₃) by rule ∃-intro on l
  |     |   | n: ∃ (n₃ : N) : Sum(S(m₁), S(m₂), n₃) ∧ Sum(S(m₂), S(m₁), n₃) by rule ∃-elim on d, e
  | o: ∀ (n₂ : N) : ∃ (n₃ : N) : Sum(S(m₁), n₂, n₃) ∧ Sum(n₂, S(m₁), n₃) by rule ∀-intro on b