Fix Lecture 2 solution of Zadd, thanks to Dever Kemme Nash.

UniMath · Aug 2, 2024 · fee07c2 · fee07c2
1 parent 184bbf9
commit fee07c2
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/2024-07-Minneapolis/2_Coq/coq_solutions.v b/2024-07-Minneapolis/2_Coq/coq_solutions.v
@@ -146,8 +146,11 @@ Definition Z : UU := coprod nat nat.
 Notation "⊹ x" := (inl x) (at level 20).
 Notation "─ x" := (inr x) (at level 40).
 
+Definition Z5 : Z := ⊹ 5.
 Definition Z1 : Z := ⊹ 1.
 Definition Z0 : Z := ⊹ 0.
+Definition Zn1 : Z := ─ 0.
+Definition Zn2 : Z := ─ 1.
 Definition Zn3 : Z := ─ 2.
 
 Definition Zcase (A : UU) (fpos : nat → A) (fneg : nat → A) : Z → A :=
@@ -164,12 +167,12 @@ Definition Zadd : Z -> Z -> Z :=
            Zcase Z
                  (λ posm : nat, ⊹ (posn + posm))
                  (λ negm : nat,
-                    myif posn ≥ negm then ⊹ (posn - negm)
+                    myif posn ≥ (S negm) then ⊹ (posn - S negm)
                                       else (─ (negm - posn))))
         (λ negn : nat,
            Zcase Z
                  (λ posm : nat,
-                    myif posm ≥ negn then ⊹ (posm - negn)
+                    myif posm ≥ (S negn) then ⊹ (posm - S negn)
                                       else (─ (negn - posm)))
                  (λ negm : nat, ─ (S negn + negm))).
 
@@ -181,3 +184,6 @@ Eval compute in Zadd Zn3 Z1.             (* ─ 1 *)
 Eval compute in Zadd Zn3 Zn3.            (* ─ 5 *)
 Eval compute in Zadd (Zadd Zn3 Zn3) Zn3. (* ─ 8 *)
 Eval compute in Zadd Z0 (negate (Zn3)).  (* ⊹ 3 *)
+Eval compute in Zadd Z0 Zn1.             (* ─ 0 *)
+Eval compute in Zadd Z1 Zn1.             (* ⊹ 0 *)
+Eval compute in Zadd Z5 Zn2.             (* ⊹ 3 *)