nat.slf

// 終端記号の定義
terminals z s

// 文法定義 n は z または s n
syntax
n ::= z
  | s n

// 公理
// judgment 名前 : 式
// それぞれの式は、--- の上に前提、下に結果が来る。結果は式とマッチする必要がある。
judgment sum: n + n = n

--------- sum-z
z + n = n

n1 + n2 = n3
-------------------- sum-s
(s n1) + n2 = (s n3)

// Warm-up theorem: 1 + n = s n
// theorem 定理名 : forallのリスト exists一つ
/*
theorem n_plus_1_equals_s_n : forall n exists (s z) + n = (s n).
  d1: (s z) + n = (s n) by unproved
end theorem
*/
/*
theorem n_plus_1_equals_s_n : forall n exists (s z) + n = (s n).
  d1: z + n = n             by unproved
  d2: (s z) + n = (s n)     by rule sum-s on d1 // sum-s に d1 を代入
end theorem
*/

theorem n_plus_1_equals_s_n : forall n exists (s z) + n = (s n).
  d1: z + n = n             by rule sum-z // sum-z の下とマッチ
  d2: (s z) + n = (s n)     by rule sum-s on d1 // sum-s に d1 を代入
end theorem

// n + 0 = n
// induction と case のサンプル

/*
theorem sum-z-rh: forall n exists n + z = n.
  d1: n + z = n by induction on n: // n で case に分ける
    case z is // n == z の場合
      d2: z + z = z by unproved
    end case
    case s n1 is // n == (s n1) の場合
      d4: (s n1) + z = (s n1) by unproved
    end case
  end induction
end theorem
*/
theorem sum-z-rh: forall n exists n + z = n.
  d1: n + z = n by induction on n: // n で case に分ける
    case z is // n == z の場合
      d2: z + z = z           by rule sum-z // sum-z の下とマッチ
    end case
    case s n1 is // n == (s n1) の場合
      d3: n1 + z = n1         by induction hypothesis on n1 // d1 の n に n1 を代入
      d4: (s n1) + z = (s n1) by rule sum-s on d3 // sum-s に d3 を代入
    end case
  end induction
end theorem

// n1 + n2 = n3 の時 n1 + (n2 + 1) = (n3 + 1)
/*
theorem sum-s-rh: forall d1: n1 + n2 = n3 exists n1 + (s n2) = (s n3).
  // d1 (jugment sum) にある rule で場合分けする。
  d2: n1 + (s n2) = s n3 by induction on d1:
    case rule // sum-z の場合
      
      ----------------- sum-z
      dzc: z + n = n // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      dz1: z + (s n) = (s n) by unproved
    end case
    case rule // sum-s の場合
      dsp: n1' + n2' = n3'
      -------------------- sum-s
      dsc: (s n1') + n2' = (s n3') // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      ds2: (s n1') + (s n2') = (s (s n3')) by unproved
    end case
  end induction
end theorem
*/

theorem sum-s-rh: forall d1: n1 + n2 = n3 exists n1 + (s n2) = (s n3).
  // d1 (jugment sum) にある rule で場合分けする。
  d2: n1 + (s n2) = s n3 by induction on d1:
    case rule // sum-z の場合
      
      ----------------- sum-z
      dzc: z + n = n // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      dz1: z + (s n) = (s n) by rule sum-z
    end case
    case rule // sum-s の場合
      dsp: n1' + n2' = n3'
      -------------------- sum-s
      dsc: (s n1') + n2' = (s n3') // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      // n1' + n2' = n3' より
      ds1: n1' + (s n2') = (s n3') by induction hypothesis on dsp
      // forall n1' + n2' = n3' exists (s n1') + n2' = (s n3') に n1' + (s n2') = (s n3') を代入
      ds2: (s n1') + (s n2') = (s (s n3')) by rule sum-s on ds1
    end case
  end induction
end theorem