Lekhani Ray (Jul 02 2022 at 12:30): Lekhani Ray (Jul 02 2022 at 12:30):Hello!
I have a question about definite descriptions: Do we need to prove the existence AND uniqueness of a function where we are using definite descriptions (THE)
For example, if I have
begin
definition
plus where "plus = (THE f. ∀ x y. f x zero = x ∧ f x (suc y) = suc (f x y))"
definition
times where "times = (THE g. ∀ x y. g x zero = zero ∧ g x (suc y) = plus (g x y) x)"
end
Do I need to prove existence and uniqueness in order to be able to use plus and times anywhere?
Manuel Eberl (Jul 02 2022 at 13:26):To use it not really, but to prove any properties about it: yes.
Manuel Eberl (Jul 02 2022 at 13:27):Yes. There's also the SOME operator, which only requires existence, but not uniqueness.
Manuel Eberl (Jul 02 2022 at 13:27):Not sure what zero and suc is in your case, but if you can use literally anything other than description operators then you should.
Manuel Eberl (Jul 02 2022 at 13:28):Like, the function package.
Manuel Eberl (Jul 02 2022 at 13:30):Judging from the other thread you opened, it seems that you have some sort of induction principle for your suc and zero. With that, it should be able to use the function package.
Manuel Eberl (Jul 02 2022 at 13:31):But you're probably also going to need distinctness, i.e. that zero ≠ suc x and suc x = suc y ⟹ x = y.
Manuel Eberl (Jul 02 2022 at 13:32):It might be easiest to actually define a function that converts your values into nat and back again and then just define plus and times in terms of the respective operations on nat.
Manuel Eberl (Jul 02 2022 at 13:33):(and derive the recursive equations above as derived theorems)
Manuel Eberl (Jul 02 2022 at 13:34):Or you could define a primitive recursion operator like rec_nat for your values and use that to define everything else.
Manuel Eberl (Jul 02 2022 at 13:34):Then you only have to do the annoying work once. But I think the "conversion to nat" function is the conceptually and practically easiest one.
Last updated: Feb 01 2025 at 20:19 UTC