## Stream: Coq users

### Topic: ✔ Proof of a small scenario

#### Julin S (Jun 09 2022 at 11:22):

Suppose a guy has a baby.

Talking from the point of view of this guy,

• Everyone loves my baby (baby is so adorable).
• But my baby loves only me.

I once saw a proof online where it was possible to derive that 'I am my baby' from these assumptions.

I recreated that proof in Coq and it looks like this:

``````Section baby.
Variable Person : Set.
Variable loves : Person -> Person -> Prop.

Axiom mybaby me : Person.
Axiom everyoneLovesMybaby : forall person:Person,
loves person mybaby.
Axiom mybabyLovesOnlyMe : forall person:Person,
loves mybaby person -> person = me.
Theorem mybabyIsMe : mybaby = me.
Proof.
exact (mybabyLovesOnlyMe mybaby (everyoneLovesMybaby mybaby)).
Qed.
End baby.
``````

I suppose this was provable because of some fault in the way the axioms were formulated?

Is there any way by which we can prove that `me ≠ mybaby` while still holding true to the essence of this scenario?

Maybe if we modify `mybabyLovesOnlyMe` to

``````Axiom mybabyLovesOnlyMe : forall person:Person,
person <> mybaby -> loves mybaby person -> person = me.
``````

Can it help?

#### Li-yao (Jun 09 2022 at 11:31):

That allows you not to prove `mybabe = me` but won't allow you to prove the negation. When you introduce axioms there is always the risk of introducing a contradiction, in which case everything is provable. The alternative is to instantiate the axioms. Then you can show `mybabe <> me` in that specific model.

#### Julin S (Jun 09 2022 at 11:45):

Which instance of the axioms could be helpful?

#### Julin S (Jun 09 2022 at 11:45):

And what could be the 'least intrusive' hypothesis that we can add to the set of axioms to make `mybaby <> me` provable?

#### Gaëtan Gilbert (Jun 09 2022 at 11:46):

just adding it as an axiom may be least intrusive

#### Li-yao (Jun 09 2022 at 12:00):

There's a post-apocalyptic model where it's only you and your baby left in the world.

#### Gaëtan Gilbert (Jun 09 2022 at 12:06):

ah `Variant person := me | baby`

#### Julin S (Jun 09 2022 at 12:14):

Hadn't known about `Variant`.

#### Julin S (Jun 09 2022 at 12:14):

Like a stripped down version of `Inductive`, is it?

yup

#### Olivier Laurent (Jun 09 2022 at 12:18):

It seems you can derive `loves mybaby me` only because `me = mybaby`, while it seems to be part of the scenario anyway.
You could then consider an anti-narcissistic world:

``````Section baby.
Variable Person : Set.
Variable loves : Person -> Person -> Prop.

Axiom antiNarcissistic : forall person1 person2,
loves person1 person2 -> person1 <> person2.

Axiom mybaby me : Person.
Axiom everyoneLovesMybaby : forall person:Person,
person <> mybaby -> loves person mybaby.
Axiom mybabyLovesMe : loves mybaby me.
Axiom mybabyLovesOnlyMe : forall person:Person,
loves mybaby person -> person = me.
Theorem mybabyIsNotMe : mybaby <> me.
Proof. apply antiNarcissistic, mybabyLovesMe. Qed.
End baby.
``````

Thanks!

#### Notification Bot (Jun 10 2022 at 03:21):

Julin S has marked this topic as resolved.

Last updated: Jun 20 2024 at 12:02 UTC