Timeline for Uniqueness of proofs for inductively defined predicates
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 5 at 16:53 | comment | added | JoJoModding |
Yes it's equivalent to UIP: you can build a Hedberg Function by converting to a <= b /\ b <= a given a = b and if <= is unique (and since /\ preserves uniqueness), so is the equality coming out of converting back.
|
|
| Jul 5 at 11:22 | comment | added | Pavel Shuhray | @JoJoModding thank you, it seems like what I need. The proof uses UIP on nat (the result is similat to UIP so it is expected) | |
| Jul 5 at 10:44 | comment | added | Naïm Favier |
In any case UIP on nat is provable by Hedberg's theorem, since nat has decidable equality (see Meven's link).
|
|
| Jul 5 at 10:19 | comment | added | JoJoModding |
As far as I am aware, the general proof requires UIP on nat. See chapter 29.4 here for a human-readable proof. (Or perhaps that was for lt not le..)
|
|
| Jul 5 at 10:16 | comment | added | Naïm Favier |
It seems harder than I thought to prove the specific case le_n' n = le_n n without using the general fact, because everything under the sun is apparently opaque in Coq. But the general fact really should just be a matter of generalising the theorem to $\forall n\ m. (p : n \leq m) \to (e : n = m) \to p =_e \text{le_n}\ n$ and applying the induction principle for $\leq$, obtaining a contradiction ($n = \text{S}\ n$) in the case of $\text{le_S}$. I don't know how easy this is to express in Coq, but it would be completely trivial in Agda for example.
|
|
| Jul 5 at 10:09 | comment | added | Meven Lennon-Bertrand♦ | It is definitely provable, see lemma le_unique in the standard library. Whether we can make a reasonably readable proof of this fact is another question. | |
| Jul 5 at 9:56 | comment | added | Vladimir Ivanov |
Please, show your proof next time. I don't see that Goal le_n' 0 = ln_n 0. can be proved (this is the base of proof by induction).
|
|
| Jul 5 at 9:46 | comment | added | Naïm Favier |
Those are clearly equal by induction on n. In general, you should be able to use the full induction principle for <= to show that every proof of n <= n is equal to le_n n. (I realise the burden of proof is on me; currently trying to remember enough about Coq syntax to formalise this.)
|
|
| Jul 5 at 9:40 | comment | added | Vladimir Ivanov |
Another proof might look like this: Lemma le_n' n : n <= n. Proof. induction n; [reflexivity | apply le_n_S, IHn]. Qed. There is no proof of Theorem Th' n : le_n' n = le_n n..
|
|
| Jul 5 at 9:01 | comment | added | Naïm Favier |
Th should be provable without assuming proof irrelevance.
|
|
| S Jul 5 at 9:00 | review | First answers | |||
| Jul 8 at 9:49 | |||||
| S Jul 5 at 9:00 | history | answered | Vladimir Ivanov | CC BY-SA 4.0 |