Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear all,

I'm trying to help improving the wiki. I wrote a tentative gotchas.md page
however I don't know how to contribute it. Specifically, I'm able to make a
clone of
   https://github.com/math-comp/wiki/wiki
On my laptop. But since it's not a classical github repo I can't make a pull
request. Is there a good solution which doesn't require a write access ?

By the way, I've attached a patch for my changes.

Cheers,

Florent
diff --git a/Home.md b/Home.md
index 2e03ad0..a5a6dfc 100644
--- a/Home.md
+++ b/Home.md
@@ -6,5 +6,5 @@ An umbrella/show-case to foster MC related projects and MC 
itself.
 
 - [[Tutorials, teaching material|tutorials]]
 - [[Installation using OPAM|install-opam]]
-- Gotchas
+- [[Gotchas|gotchas]]
 - [[Good practices|good practices]]
diff --git a/gotchas.md b/gotchas.md
new file mode 100644
index 0000000..f81cae3
--- /dev/null
+++ b/gotchas.md
@@ -0,0 +1,51 @@
+# SSReflect tactical gotchas
+
+### Boolean reflexion
+
+- proving a
+
+  ```reflect A B```
+
+  lemma
+
+  ```
+  apply (ifP idP).
+  ```
+
+- This works with more complicated reflexion lemmas, for example:
+
+  ```
+  reflect (forall s1, s1 \in P1 -> ...) [forall (x | x \in E), ...]
+  ```
+
+  is proved using:
+
+  ```
+  apply (iffP forall_inP)
+  ```
+
+- proving the equality of two booleans:
+
+  ```
+  apply/idP/idP.
+  ```
+
+### congr in hypothesis:
+
+- My goal is of the form
+
+  ```
+  a = b -> P
+  ```
+
+  I'd like to transform it as
+
+  ```
+  f a = f b -> P
+  ```
+
+  This is achieved by
+
+  ```
+  move/(congr1 f).
+  ```