Add a new example: zagier.v

Co-authored-by: Laurent Théry <[email protected]>
math-comp · Sep 27, 2021 · 4713df8 · 4713df8
1 parent 6bb61a3
commit 4713df8
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/Make.test-suite b/Make.test-suite
@@ -1,4 +1,5 @@
 examples/boolean.v
 examples/divmod.v
+examples/zagier.v
 
 -I .
diff --git a/examples/zagier.v b/examples/zagier.v
@@ -0,0 +1,17 @@
+From mathcomp Require Import all_ssreflect zify.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Lemma zagierK x y z : 0 < x -> 0 < z -> 
+  let zagier t :=
+    let: (x, y, z) := t in
+    if x < y - z then (x + z.*2, z, y - z - x)
+    else if x < y.*2 then (y.*2 - x, y, x + z - y)
+    else (x - y.*2, x + z - y, y) in
+  zagier (zagier (x, y, z)) = (x, y, z).
+Proof.
+move=> xP zP /=.
+repeat case: leqP => *; congr (_,_,_); lia.
+Qed.