From fee07c2ffb9a0e0862f48faab848070763280cfd Mon Sep 17 00:00:00 2001 From: Carlo Angiuli Date: Fri, 2 Aug 2024 10:08:26 -0500 Subject: [PATCH] Fix Lecture 2 solution of Zadd, thanks to Dever Kemme Nash. --- 2024-07-Minneapolis/2_Coq/coq_solutions.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/2024-07-Minneapolis/2_Coq/coq_solutions.v b/2024-07-Minneapolis/2_Coq/coq_solutions.v index 47d3db7..9eb1722 100644 --- 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 *)