The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

So recently I had this discussion with some friends about what love is.

And one of my friends said: Well, there is no unconditional love.
Another replied: That's not true! You just have to love unconditionally 
first, then you can expect to be loved unconditionally back!
So I said: But that's impossible. If you and your partner both have that 
condition, nobody will ever get any loving done. In computer science, we 
call this a deadlock.

That friend didn't buy it, so I decided to formalize the proof that if 
unconditional love only starts after the other person somehow loves you, 
then either you love the other person unconditionally from the start 
(from the beginning of time, so to speak) or you never will.

Of course you shouldn't take this too seriously on a philosophical level 
as love works differently (the fact that people fall in love proves 
this), but I just thought this is kinda funny and stupid and maybe you 
would find this funny too. Or maybe it's just my young undergrad humor 
acting up. If so, you can just ignore this (sorry for the spam!).
For all other cases, I attached a proof of 135 lines that love doesn't 
exist.

Kind regards,

Jonas
Inductive person := A | B.
Definition point_in_time := nat.
Variable loves : person -> person -> point_in_time -> Prop.
(* loves a b t if a loves b at the point in time t *)
 
Definition lovecondition a b := (forall t, 
    (loves b a t) <-> (forall t', t' > t -> loves a b t')).
(* once you start loving me, I'll love you back. 
   But then I'll love you unconditionally! 

   Of course I won't just start loving you, you need to love me first.
*)

Require Import Coq.Arith.Lt Coq.Arith.Compare_dec.

(* once I start loving you, you'll love me back. 
   But then you started loving me, so I'll love you back. *)
Lemma because_you_love_me_back_I_will_love_you A B : 
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      loves A B t ->
      forall t', t' > (S t) ->
        loves A B t'.
intros LAB LBA t lABt t' de.
apply LAB with (S t) ; auto. (* auto handles assumption *)
apply LBA with t ; auto. (* auto handles assumption, S t > t *)
Qed.

(* because you love me back unconditionally, 
   and you don't just start doing that without me loving you, 
   I have to love you as well. *)
Lemma I_still_love_you_tomorrow A B :
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      loves A B t ->
      loves A B (S t).
intros LAB LBA t lABt.
apply LBA. intros t' de. apply LAB.
intros t'' de''.
assert (t'' > S t) by now apply lt_trans with t'.
now apply because_you_love_me_back_I_will_love_you with t.
Qed.

(* But then if I ever love you, I'll love you forever! *)
Lemma I_will_love_you_forever A B :
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      loves A B (S t) ->
      forall t', t' > t ->
        loves A B t'.
intros LAB LBA t lABSt.
intros t' de'. induction de'.
  assumption.
  
  now apply I_still_love_you_tomorrow.
Qed.

(* But of course you have to love me first. *)
Lemma you_loved_me_first A B :
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      loves A B (S t) ->
      loves B A t.
intros LAB LBA t lABSt.
apply LAB. now apply I_will_love_you_forever.
Qed.

(* But I have to love you first as well, so if I don't love you first,
   you will not love me,
   and then I'll not love you back tomorrow either. *)
Lemma I_will_not_love_you_tomorrow A B :
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      ~ loves A B t ->
      ~ loves A B (S t).
intros LAB LBA t nlABt lABSt.
apply nlABt. 
apply you_loved_me_first ; try assumption. (* you were first! *)
apply you_loved_me_first ; try assumption. (* no, you were first! *)
apply I_still_love_you_tomorrow ; assumption.
Qed.

(* But if I can't start loving you within one day,
   I will never be able to. *)
Lemma I_will_never_love_you A B :
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      ~ loves A B t ->
      forall t', t' >= t ->
        ~ loves A B t'.
intros LAB LBA t nlABt t' de'.
induction de'.
  assumption.
  
  now apply I_will_not_love_you_tomorrow.
Qed.

(* Also I never really loved you. *)
Lemma I_never_loved_you A B :
    lovecondition A B -> 
    lovecondition B A -> 
    forall t, 
      ~ loves A B t ->
      forall t', t' <= t ->
        ~ loves A B t'.
intros LAB LBA t nlABt t' de'.
induction de'.
  assumption.
  
  apply IHde'.
  intros lABm. apply nlABt.
  now apply I_still_love_you_tomorrow.
Qed.

(* So if there is a point in time where I don't love you,
   I never have
   and never will. *)
Lemma love_does_not_exist A B :
    lovecondition A B -> 
    lovecondition B A -> 
    (exists t, ~ loves A B t) ->
    forall t, ~ loves A B t.
intros LAB LBA [t nlABt] t'.
destruct (le_gt_dec t' t). (* t' <= t or t' > t *)
  now apply I_never_loved_you with t.
  
  assert (t' >= t) by auto with arith.
  now apply I_will_never_love_you with t.
Qed.