EECS 755

Software Requirements Modeling and Analysis

Index
Blog

Subtraction

Someone in class today asked about closure of subtraction over nat in Coq. Actually, that wasn’t the question but it’s close enough for jazz. I commented that 0 - 1 = 0 in Coq to a number of well-deserved snickers. Turns out it’s true. To make subtraction closed over nat, subtraction results that would be negative are all 0. So it goes.