Adding Spanish translation

Verbose/Spanish/All.lean

@@ -0,0 +1,11 @@
+import Verbose.Tactics.Notations
+import Verbose.Spanish.Assume
+import Verbose.Spanish.By
+import Verbose.Spanish.Calc
+import Verbose.Spanish.Claim
+import Verbose.Spanish.Fix
+import Verbose.Spanish.Lets
+import Verbose.Spanish.Since
+import Verbose.Spanish.We
+import Verbose.Spanish.Widget
+import Verbose.Spanish.Statements

Verbose/Spanish/Assume.lean

@@ -0,0 +1,179 @@
+import Verbose.Spanish.Common
+import Verbose.Spanish.Fix
+
+open Lean Elab Tactic
+
+setLang es
+
+syntax "Supongamos₁ " colGt assumeDecl : tactic
+elab_rules : tactic
+  | `(tactic| Supongamos₁ $x:ident) => Assume1 (introduced.bare x x.getId)
+
+elab_rules : tactic
+  | `(tactic| Supongamos₁ $x:ident : $type) =>
+    Assume1 (introduced.typed (mkNullNode #[x, type]) x.getId type)
+
+
+elab_rules : tactic
+  | `(tactic| Supongamos₁ ( $decl:assumeDecl )) => do evalTactic (← `(tactic| Supongamos₁ $decl:assumeDecl))
+
+
+namespace Verbose.Named
+scoped syntax "Supongamos " (colGt assumeDecl)+ : tactic
+scoped syntax "Supongamos " ("para una contradicción " <|> "por contradicción ") (colGt assumeDecl) : tactic
+
+scoped macro_rules
+  | `(tactic| Supongamos $decl:assumeDecl) => `(tactic| Supongamos₁ $decl)
+  | `(tactic| Supongamos $decl:assumeDecl $decls:assumeDecl*) => `(tactic| Supongamos₁ $decl; Supongamos $decls:assumeDecl*)
+
+scoped elab_rules : tactic
+  | `(tactic| Supongamos para una contradicción $x:ident : $type) => forContradiction x.getId type
+
+example (P Q : Prop) : P → Q → True := by
+  Supongamos hP (hQ : Q)
+  trivial
+
+example (P Q : Prop) : P → Q → True := by
+  Supongamos hP (hQ : Q)
+  trivial
+
+example (n : Nat) : 0 < n → True := by
+  Supongamos hn
+  trivial
+
+example : ∀ n > 0, true := by
+  success_if_fail_with_msg "Aquí no puedes introducir una hipótesis."
+    Supongamos n
+  intro n
+  Supongamos H : n > 0
+  trivial
+
+
+example (P Q : Prop) (h : ¬ Q → ¬ P) : P → Q := by
+  Supongamos hP
+  Supongamos para  una contradicción hnQ :¬ Q
+  exact h hnQ hP
+
+example (P Q : Prop) (h : ¬ Q → ¬ P) : P → Q := by
+  Supongamos hP
+  Supongamos para una contradicción hnQ : ¬ Q
+  exact h hnQ hP
+
+
+example (P Q : Prop) (h : ¬ Q → ¬ P) : P → Q := by
+  Supongamos hP
+  Supongamos por contradicción hnQ : ¬ Q
+  exact h hnQ hP
+
+
+example (P Q : Prop) (h : Q → ¬ P) : P → ¬ Q := by
+  Supongamos hP
+  Supongamos hnQ : Q
+  exact h hnQ hP
+
+example : ∀ n > 0, n = n := by
+  Supongamos para  una contradicción H : ∃ n > 0, n ≠ n
+  tauto
+
+private def foo_bar (P : Nat → Prop) := ∀ x, P x
+
+example (P : Nat → Prop) (h : ¬ ∃ x, ¬ P x) : foo_bar P := by
+  success_if_fail_with_msg
+    "Para proceder por contradicción, debes suponer la negación del objetivo."
+    Supongamos para  una contradicción H : ∃ x, ¬ P x
+  unfold foo_bar
+  Supongamos para  una contradicción H : ∃ x, ¬ P x
+  exact h H
+
+configureUnfoldableDefs foo_bar
+
+example (P : Nat → Prop) (h : ¬ ∃ x, ¬ P x) : foo_bar P := by
+  Supongamos para  una contradicción H : ∃ x, ¬ P x
+  exact h H
+
+example : 0 ≠ 1 := by
+  success_if_fail_with_msg
+    "El objetivo ya es una negación, proceder por contradicción no cambia nada. En su lugar, puedes asumir directamente 0 = 1."
+    Supongamos para  una contradicción h : 0 = 1
+  norm_num
+
+example : 0 ≠ 1 := by
+  Supongamos h : 0 = 1
+  norm_num at h
+
+allowProvingNegationsByContradiction
+
+example : 0 ≠ 1 := by
+  Supongamos para  una contradicción h : 0 = 1
+  norm_num at h
+
+-- Check type ascriptions are not needed
+example : ¬ (2 : ℝ) * -42 = 2 * 42 := by
+  Supongamos hyp : 2 * -42 = 2 * 42
+  linarith
+end Verbose.Named
+
+namespace Verbose.NameLess
+syntax "Supongamos que " (colGt term) : tactic
+syntax "Supongamos que " (colGt term AndES term) : tactic
+syntax "Supongamos que " (colGt term ", " term AndES term) : tactic
+syntax "Supongamos " ("para una contradicción que " <|> "por contradicción que ") (colGt term) : tactic
+
+elab_rules : tactic
+  | `(tactic| Supongamos que $t) => withMainContext do
+     let e ← elabTerm t none
+     let name ← mk_hyp_name t e
+     Assume1 (introduced.typed (mkNullNode #[t]) name t)
+  | `(tactic| Supongamos que $t $_and:AndES $s) => withMainContext do
+     let e ← elabTerm t none
+     let name ← mk_hyp_name t e
+     Assume1 (introduced.typed (mkNullNode #[t]) name t)
+     let e ← elabTerm s none
+     let name ← mk_hyp_name s e
+     Assume1 (introduced.typed (mkNullNode #[s]) name s)
+  | `(tactic| Supongamos que $t, $s $_and:AndES $r) => withMainContext do
+     let e ← elabTerm t none
+     let name ← mk_hyp_name t e
+     Assume1 (introduced.typed (mkNullNode #[t]) name t)
+     let e ← elabTerm s none
+     let name ← mk_hyp_name s e
+     Assume1 (introduced.typed (mkNullNode #[s]) name s)
+     let e ← elabTerm r none
+     let name ← mk_hyp_name r e
+     Assume1 (introduced.typed (mkNullNode #[r]) name r)
+
+
+elab_rules : tactic
+  | `(tactic| Supongamos para una contradicción que $t) => withMainContext do
+    let e ← elabTerm t none
+    let name ← mk_hyp_name t e
+    forContradiction name t
+
+example : ∀ n > 0, n = n := by
+  Supongamos por contradicción que ∃ n > 0, n ≠ n
+  tauto
+
+example : ∀ n > 0, n = n := by
+  Supongamos para una contradicción que ∃ n > 0, n ≠ n
+  tauto
+
+example (P : Prop) : P → True := by
+/-   success_if_fail_with_msg "El término
+  True
+ no es igual por definición a
+  P"
+    Supongamos que True -/
+  Supongamos que P
+  success_if_fail_with_msg "Aquí no puedes introducir una hipótesis."
+    Supongamos que True
+  trivial
+
+example (P Q : Prop) : P → Q → True := by
+  Supongamos que P ,y Q
+  trivial
+
+example (P Q R : Prop) : P → Q → R → True := by
+  Supongamos que P, Q ,y R
+  trivial
+
+end Verbose.NameLess

Verbose/Spanish/By.lean

@@ -0,0 +1,135 @@
+import Verbose.Tactics.By
+import Verbose.Spanish.Common
+
+open Lean Verbose.Spanish
+
+
+elab "Por " e:maybeAppliedES (" tenemos " <|> " obtenemos ") colGt news:newStuffES : tactic => do
+obtainTac (← maybeAppliedESToTerm e) (newStuffESToArray news)
+
+elab "Por " e:maybeAppliedES " podemos elegir " colGt news:newStuffES : tactic => do
+chooseTac (← maybeAppliedESToTerm e) (newStuffESToArray news)
+
+elab "Por " e:maybeAppliedES " basta probar " "que "? colGt arg:term : tactic => do
+bySufficesTac (← maybeAppliedESToTerm e) #[arg]
+
+elab "Por " e:maybeAppliedES " basta probar " "que "? colGt args:sepBy1(term, ",", AndES) : tactic => do
+bySufficesTac (← maybeAppliedESToTerm e) args.getElems
+
+elab "hipótesis" : tactic => assumption'
+
+macro "hipótesis" : term => `(by hipótesis)
+
+lemma le_le_of_abs_le {α : Type*} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} : |a| ≤ b → -b ≤ a ∧ a ≤ b := abs_le.1
+
+lemma le_le_of_max_le {α : Type*} [LinearOrder α] {a b c : α} : max a b ≤ c → a ≤ c ∧ b ≤ c :=
+max_le_iff.1
+
+implement_endpoint (lang := es) cannotGet : CoreM String := pure "Imposible de deducir."
+
+implement_endpoint (lang := es) theName : CoreM String := pure "El nombre"
+
+implement_endpoint (lang := es) needName : CoreM String :=
+pure "Tienes que asignar un nombre al objeto elegido."
+
+implement_endpoint (lang := es) wrongNbGoals : CoreM String :=
+pure s!"No hay suficientes afirmaciones a verificar."
+
+implement_endpoint (lang := es) doesNotApply (fact : Format) : CoreM String :=
+pure s!"No se puede aplicar {fact}."
+
+implement_endpoint (lang := es) couldNotInferImplVal (val : Name) : CoreM String :=
+pure s!"No se ha podido inferir el valor implicito de {val}."
+
+implement_endpoint (lang := es) alsoNeedCheck (fact : Format) : CoreM String :=
+pure s!"También tienes que verificar {fact}"
+
+configureAnonymousFactSplittingLemmas le_le_of_abs_le le_le_of_max_le
+
+setLang es
+
+example (P : Nat → Prop) (h : ∀ n, P n) : P 0 := by
+  Por h aplicado a 0 tenemos h₀
+  exact h₀
+
+example (P : Nat → Nat → Prop) (h : ∀ n k, P n (k+1)) : P 0 1 := by
+  Por h aplicado a 0 ,e 0 obtenemos (h₀ : P 0 1)
+  exact h₀
+
+example (n : Nat) (h : ∃ k, n = 2*k) : True := by
+  Por h obtenemos k tal que (H : n = 2*k)
+  trivial
+
+example (n : Nat) (h : ∃ k, n = 2*k) : True := by
+  Por h tenemos k tal que H
+  trivial
+
+example (P Q : Prop) (h : P ∧ Q)  : Q := by
+  Por h tenemos (hP : P) (hQ : Q)
+  exact hQ
+
+example (x : ℝ) (h : |x| ≤ 3) : True := by
+  Por h tenemos (h₁ : -3 ≤ x) (h₂ : x ≤ 3)
+  trivial
+
+example (n p q : ℕ) (h : n ≥ max p q) : True := by
+  Por h tenemos (h₁ : n ≥ p) (h₂ : n ≥ q)
+  trivial
+
+noncomputable example (f : ℕ → ℕ) (h : ∀ y, ∃ x, f x = y) : ℕ → ℕ := by
+  Por h podemos elegir g tal que (H : ∀ (y : ℕ), f (g y) = y)
+  exact g
+
+noncomputable example (f : ℕ → ℕ) (A : Set ℕ) (h : ∀ y, ∃ x ∈ A, f x = y) : ℕ → ℕ := by
+  Por h podemos elegir g tal que (H : ∀ (y : ℕ), g y ∈ A) ,e (H' : ∀ (y : ℕ), f (g y) = y)
+  exact g
+
+noncomputable example (f : ℕ → ℕ) (A : Set ℕ) (h : ∀ y, ∃ x ∈ A, f x = y) : ℕ → ℕ := by
+  Por h podemos elegir g tal que (H : ∀ (y : ℕ), g y + 0 ∈ A) ,e (H' : ∀ (y : ℕ), f (g y) = y)
+  exact g
+
+example (P Q : Prop) (h : P → Q) (h' : P) : Q := by
+  Por h basta probar que  P
+  exact h'
+
+example (P Q : Prop) (h : P → Q) (h' : P) : Q := by
+  Por h basta probar que  P
+  exact h'
+
+example (P Q : Prop) (h : P → Q) (h' : P) : Q := by
+  Por h basta probar que  P
+  exact hipótesis
+
+example (P Q R : Prop) (h : P → R → Q) (hP : P) (hR : R) : Q := by
+  Por h basta probar que  P ,e R
+  exact hP
+  exact hR
+
+set_option linter.unusedVariables false in
+example (P Q : Prop) (h : ∀ n : ℕ, P → Q) (h' : P) : Q := by
+  success_if_fail_with_msg "No se puede aplicar h 0 1."
+    Por h aplicado a 0 ,e 1 basta probar que  P
+  Por h aplicado a 0 basta probar que  P
+  exact h'
+
+example (Q : Prop) (h : ∀ n : ℤ, n > 0 → Q)  : Q := by
+  Por h aplicado a 1 basta probar que  1 > 0
+  norm_num
+
+example (Q : Prop) (h : ∀ n : ℤ, n > 0 → Q)  : Q := by
+  Por h basta probar que  1 > 0
+  norm_num
+
+example {P Q R : ℕ → Prop} {n k l : ℕ} (h : ∀ k l, P k → Q l → R n) (hk : P k) (hl : Q l) :
+    R n := by
+  success_if_fail_with_msg "También tienes que verificar Q ?l"
+    Por h basta probar que  P k
+  Por h basta probar que  P k ,e Q l
+  exact hk
+  exact hl
+
+set_option linter.unusedVariables false in
+example (n : Nat) (h : ∃ n : Nat, n = n) : True := by
+  success_if_fail_with_msg "El nombre n ya está en uso"
+    Por h tenemos n tal que H
+  trivial