linarith 追加

Examples/Linarith.lean

@@ -0,0 +1,10 @@
+import Mathlib.Tactic.Linarith
+
+import Std.Data.Rat
+
+variable (x y z : ℚ)
+
+-- ANCHOR: first
+example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0): 12 * y - 4 * z ≥ 0 := by
+  linarith
+-- ANCHOR_END: first

src/SUMMARY.md

@@ -25,6 +25,7 @@
 - [induction: 帰納法](./induction.md)
 - [intro: 含意→や全称∀を示す](./intro.md)
 - [left, right: 論理和∨を示す](./left_right.md)
+- [linarith: 線形不等式を示す](./linarith.md)
 - [rel: 不等式を使う](./rel.md)
 - [rfl: 定義そのまま](./rfl.md)
 - [ring: 環の等式を示す](./ring.md)

src/linarith.md

@@ -0,0 +1,9 @@
+# linarith
+
+needs: `import Mathlib.Tactic.Linarith`
+
+`linarith` は線形算術(linear arithmetic)からその名前があると考えられるタクティクです．ローカルコンテキストの仮定を読んで，線形な不等式を導くことができます．
+
+```lean
+{{#include ../Examples/Linarith.lean:first}}
+```