Adding Spanish translation

[navimath]

This PR translates the widget, help and error messages and adapts custom tactics to the Spanish language, see the list of (most of) translated commands:

• Help -> Ayuda
• Suppose -> Supongamos
• such that -> tal que
• Every tactic beginning by "We " has been translated to its proper Spanish conjugation, e.g,
  • We proceed -> Procedemos / Procedamos (two possible ways)
• By -> Por
• Using -> Usando
• Applied to -> Aplicado a
• Since -> Como
• Fix -> Sea

Calc has not been translated since it can be interpreted as in "Cálculo".

However, to avoid problems with the infamous translation of "and" (since in Spanish is just "y" which would clash with the variable name), I took the decision of naming it as "yy". This tool has been built for student to use Lean4 as a "personal teacher" for learning how to write proofs so they can do it by themselves on paper later. I find that the commands should resemble as much as possible to the one they will use on paper even if other Spanish native alternatives are possible (con, además, junto con, también). Another possibility would be some variant of "y_" that would enhance readibility but I find it more costly of writing.

Finally, I am afraid that this translation may be sometimes too literal and I would like the opinion of other Spanish speakers before merging, mostly in the Calc tactic with the addition of the syntax "pues" and "por", e.g:

-- In example.lean 
  Calc |u n - l| ≤ ε/2  por hN aplicado a n usando que n ≥ N
       _         < ε    pues ε > 0

I do not know if students will fine clear the difference between por (justify a calc step) and pues (using a fact), honestly I am not really sure I get it either but I saw the other translations difference between these two as well (car and puisque for French, from and since for English)

I would like your feedback on this translation before merging.

[pepamontero]

I’ve left a few suggestions focused on Spanish natural phrasing.

This is not a complete review, but rather a collection of smaller issues I noticed while reading. Most of them are minor wording improvements to make the Spanish sound more natural and consistent with standard mathematical usage.

I'm happy to take another pass if you find this helpful, or discuss any of the suggestions.

[pepamontero]

Hemos estado mirando un poco más en grupo durante nuestra reunión de MadLean (@madlean-hub), te dejo dos comentarios muy pequeños jajaja.

Hemos estado hablando del tema de la "y", definitivamente poner "yy" es un poco raro, hemos pensado que en el caso de intro quizás sería más fácil poner solo comas? También podría haber una forma de diferenciar la y de variable de la y de and porque la y siempre va sin comas alrededor (a y b versus. x, y, z y w), pero habría que cambiar probablemente cosas del repo original (no sólo el lenguaje) e igual habría que preguntar primero. No se si te parece complicarse mucho la vida.

También creemos que al archivo de calc le falta un poco de revisión, pero es un poco difícil verlo en la sintaxis aparte (se ve mucho más claro cuando lees un ejemplo completo). Igual se podría intentar escribir más ejemplos para ver.

[pepamontero]

Aquí quizás quedaría mejor "Se tiene" o "Tenemos".

[navimath]

Creo que entraría en conflicto con la sintaxis "Por h se tiene x", tengo que ver si es posible. De todas formas, aunque estoy de acuerdo que Hecho/Afirmación puede sonar raro ya que corta el ritmo de la lectura, creo que tiene sentido al escribirlo por que estas enunciando una afirmación que va a parte de la demostración. No sé tampoco si Se tiene funcionaria mejor.

Intentaré escribir más ejemplos y os comento.

[pepamontero]

Aquí hemos pensado que quizás se podría poner "desarrollando" en lugar de "por cálculo".

[navimath]

Hemos estado mirando un poco más en grupo durante nuestra reunión de MadLean (@madlean-hub), te dejo dos comentarios muy pequeños jajaja.

Hemos estado hablando del tema de la "y", definitivamente poner "yy" es un poco raro, hemos pensado que en el caso de intro quizás sería más fácil poner solo comas? También podría haber una forma de diferenciar la y de variable de la y de and porque la y siempre va sin comas alrededor (a y b versus. x, y, z y w), pero habría que cambiar probablemente cosas del repo original (no sólo el lenguaje) e igual habría que preguntar primero. No se si te parece complicarse mucho la vida.

Este tema es complicado pero la idea que proponéis no es mala. De todas formas, en el repositorio original alguien ya preguntó por algo parecido y Patrick dijo que no cree que fuese posible. Igual no se barajó esta solución así que voy a proponérsela a ver si él sabe por dónde empezar y cómo hacerlo de forma que no cambie los otros idiomas.

También creemos que al archivo de calc le falta un poco de revisión, pero es un poco difícil verlo en la sintaxis aparte (se ve mucho más claro cuando lees un ejemplo completo). Igual se podría intentar escribir más ejemplos para ver.

Siendo honestos, con ese archivo hice un apaño por que tiene muchos conectores de implicación (por, ya que, pues) que puse un poco como pude (y que a decir verdad tampoco entiendo cuándo toca poner uno u otro). La cosa es que la traducción del inglés al francés me dio la misma impresión (ya le preguntaré a Patrick). Al final no le di mucha importancia ya que en la mayoría de casos se usa "por", pero habría que revisarlo para que sea coherente.

Estaría bien poder usar la misma palabra (por) y que Lean entienda cual es la "táctica" por el contexto pero no lo tengo claro. Lo pruebo y os confirmo.

Intentaré ver eso primero y hacer algunos ejemplos más para pasarooslos.

[pepamontero]

Genial, gracias por responder tan rápido! Es muy buen trabajo y yo creo que con algo de tiempo puede salir algo muy chulo. Cualquier cosa nos dices, si te viene bien que miremos algo en concreto hacemos algún hueco; como no estamos super metidos en el proyecto tampoco sabemos bien cuáles son las cosas más importantes. Pero nos encantará ayudar :)

[navimath]

Hola @pepamontero, he estado unos días fuera y con el proyecto un poco de lado. He cambiado el archivo Calc.lean, ahora debería ser más intuitivo, os pido que mireis si podeis los ejemplos dentro del mismo archivo y los del archivo Examples.lean. Respecto al problema de la yy he estado dandole vueltas pero no entiendo muy bien lo que propusisteis, ¿me podrías dar algún ejemplo? En el caso de que lo entendiese bien no sé si sería posible hacerlo ya que yy es parte de la sintaxis de la táctica, y hacer que las variables tengan que llevar una coma después de ser nombradas llevaría muchisimos cambios incluso puede que en el propio Lean (?, a coger con pinzas esto último ya que estoy lejos de ser ningún experto del lenguaje).

PD: También he corregido el logo de "Victoria!", ahora incluye las dos exclamaciones :)