UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
381 stars 22 forks source link

How to refer to based path induction #30

Open marcbezem opened 5 years ago

marcbezem commented 5 years ago

Our E3 in 2.3 is based path induction, and this is fine. With p: a=b I see that E3 is sometimes referred to as "induction on b and p". I would prefer to say "(path) induction on p". For me the induction "on b" is at best confusing,but actually incorrect, in particular if the type of b is an inductive type.

DanGrayson commented 5 years ago

I've been saying "by induction on b and p", to make it clear that one reduces to a case where both b and p are something simpler: b is a and p is refl_a. But you're right that it could be confusingly interpreted to mean "by induction on b and induction on p", which is not intended.

marcbezem commented 5 years ago

In the early chapters, where it is important to be fully explicit, we could write (what we do already some other places): by path induction on $p$, which reduces to the case where $b\jdeq a$ and $p\jdeq\refl{a}$. Later we can simply write "by induction on $p$.

DanGrayson commented 5 years ago

Something like "by induction on (b,p)" would be unambiguous but ugly.

EgbertRijke commented 5 years ago

Would the ambiguity be removed if we explain right away (where path induction is introduced for the first time) what Marc said. Thus we add a sentence explaining the phrase "by (path) induction on p", and we could even add this phrase to the index so that it could be looked up. Then the ambiguity is removed because it is explained what is meant.

I would define it as follows: "When we say that to prove P(x,p) by (path) induction on p:a=x, it suffices to consider the case P(a,refl)". And avoid the judgmental equalities in Marc's statement.

I think Dan's phrasing also risks being interpreted slightly incorrectly, because typically when we write a pair (b,p) we intend it to be a term of a Sigma-type, which we don't want in this case.

marcbezem commented 5 years ago

I like Egbert's suggestion, and we can just implement this in E3. Here are some samples from intro-uf:

"This reduces us to the case where $b$ is $a$ and $p$ is $\refl a$, and our task is now to produce an element of $a=a$; we choose $\refl a$ for it." (I'm unsure if it is "us" who are reduced.)

"By induction on $q$ we are reduced to the case where $c$ is $b$ and $q$ is $\refl b$, and we are to produce an element of $a=b$. The element $p$ serves the purpose. " (Same remark on "we are reduced".)

"It suffices to prove $C(b,b',p)$ for all $b,b':\bool$ and $p: b=b'$. By induction on $p$ this reduces to $C(b,b,\refl{b})$, which is immediate by induction on $b:\bool$."

The above example has a symbolic C and a variable b. In cases in which C and/or b is a large expression, one may not like to repeat it.