search

math-comp / mcb

Mathematical Components (the Book)
Other
139 stars 25 forks source link

§5.6: case: (x1 =P x2) pushes x1 <> x2 instead of x1 != x2 into the second subgoal #57

Closed mituharu closed 6 years ago

mituharu commented 6 years ago

the branch corresponding to \C{ReflectT} has the hypothesis \C{x1 = x2} and the branch corrsponding to \C{ReflectF} has its negation \C{x1 != x2}.

Besides the typo "corrsponding", the negation of x1 = x2 is actually x1 <> x2. Because the notation <> hasn't been mentioned so far, some additional explanation would be necessary.

Also, the line below in the subsequent example does not type check because undup_uniq ss is not of type bool.

Check (ss != [::]) && s1 \in ss && undup_uniq ss.

gares commented 6 years ago

thanks for reporting!

anton-trunov commented 6 years ago

Perhaps the following was meant:

Check (ss != [::]) && (s1 \in ss) && uniq (undup ss).
mituharu commented 6 years ago

That's also what I thought first. But it was originally three commands (eeb16fd076f15c5fc4bf8ef4f24d596f692b105c) :

Check (ss == [::]) || s1 \in ss. Check uniq ss. Check undup_uniq ss.

And the last one itself makes sense and is consistent with the preceding sentence:

... , as well as apply the list operations and theorems on objects of type \C{(seq (seq T))} when \C{T} is an \C{eqType}.