Added conclude by contradiction construction

Verbose/English/We.lean

@@ -1,3 +1,4 @@
+import Verbose.Tactics.Since
 import Verbose.Tactics.We
 import Verbose.English.Common
 
@@ -78,6 +79,14 @@ pure "Specifying the rewriting result is possible only when rewriting in a singl
 implement_endpoint (lang := en) cannotContrapose : CoreM String :=
 pure "Cannot contrapose: the main goal is not an implication."
 
+namespace Verbose.Contradicting
+
+scoped elab "We" "conclude by contradicting" facts:facts : tactic => do
+  let factsT := factsToArray facts
+  sinceConcludeTac (← `(term| False)) factsT
+
+end Verbose.Contradicting
+
 example (P Q : Prop) (h : P ∨ Q) : True := by
   We proceed using h
   . intro _hP
@@ -376,3 +385,7 @@ is not definitionally equal to target
     We reformulate h as 2 = 3
   We reformulate h as 2 = 2
   trivial
+
+open Verbose.Contradicting in
+example (p : Prop) (_ : p) (_ : ¬ p) : False := by
+  We conclude by contradicting p and ¬ p

Verbose/French/We.lean

@@ -1,3 +1,4 @@
+import Verbose.Tactics.Since
 import Verbose.Tactics.We
 import Verbose.French.Common
 
@@ -87,6 +88,14 @@ pure "On ne peut spécifier le résultat de la réécriture que lorsqu’on ne r
 implement_endpoint (lang := fr) cannotContrapose : CoreM String :=
 pure "Il est impossible de contraposer car le but n’est pas une implication."
 
+namespace Verbose.Contradicting
+
+scoped elab "On" "conclut par contradiction avec " facts:factsFR : tactic => do
+  let factsT := factsFRToArray facts
+  sinceConcludeTac (← `(term| False)) factsT
+
+end Verbose.Contradicting
+
 setLang fr
 
 example (P Q : Prop) (h : P ∨ Q) : True := by
@@ -387,3 +396,7 @@ is not definitionally equal to target
     On reformule l'hypothèse h en 2 = 3
   On reformule l'hypothèse h en 2 = 2
   trivial
+
+open Verbose.Contradicting in
+example (p : Prop) (_ : p) (_ : ¬ p) : False := by
+  On conclut par contradiction avec p et ¬ p

basic-configuration.md

@@ -153,3 +153,10 @@ configureDataProviders {
   ℕ : [mkSelf, NumbersDefault] }
 ```
 This is hopefully easy to understand and modify.
+
+## Scoped notation
+
+Some phrases are scoped to namespaces. Examples include: `Verbose.NameLess` with
+phrases that do not refer to hypotheses by name, `Verbose.Named` with phrases
+that do refer to hypothesis by name and `Verbose.Contradicting` for extra phrases around contradiction.
+Using `open Verbose.NameLess` or equivalent makes these accessible for exercises.