#StackBounty: #coq Prisoner's dilemma with Provability Logic

Bounty: 100

I am hoping to look at all the possible bots to submit to a noniterated prisoner’s dilemma where both bots can reason about each other’s behavior. Can I hide unsafeNecessitation within the definition of prove and/or open a fresh context for prove? Can I construct Coops such that fixedpoint2 is true? How can my proofs be shortened? What should I write differently? In particular the asserts to duplicate hypotheses seem clumsy. How should I automate the application of unfix? How should I automate the search of what theorems to prove?

Require Setoid.

Parameter Provable : Prop -> Prop.
Axiom Pmodus : forall {a b:Prop}, Provable (a -> b) -> Provable a -> Provable b.
Axiom loeb : forall {a:Prop}, Provable (Provable a -> a) -> Provable a.
Axiom unsafeNecessitation: forall {a:Prop}, a -> Provable a. (* WRONG *)
Ltac prove := repeat match goal with 
  | [ H : Provable _ |- _ ] => refine (Pmodus _ H); clear H
end; clear; apply unsafeNecessitation; intuition. (* sometimes doesnt clear *)

Parameter Fixedpoint2 : (Prop -> Prop -> Prop) -> (Prop -> Prop -> Prop) -> Prop. (* SHOULD BE REDUNDANT *)
Notation "A <3 B" := (Fixedpoint2 A B) (at level 70).
Axiom fixedpoint2 : forall {a b}, a <3 b = a (a <3 b) (b <3 a).
Ltac unfix := rewrite fixedpoint2.

Definition Prudent (self other:Prop) := Provable (self <-> other).
Definition Fair    (self other:Prop) := Provable other.
Definition Coop    (self other:Prop) := True.
Definition Defect  (self other:Prop) := False.

Theorem prudentbotcoops : Prudent <3 Prudent. unfix. prove. Qed.

Theorem fairbotcoops : Fair <3 Fair. unfix. apply loeb. prove. unfix. prove. Qed.

Theorem p2pp : forall {a : Prop}, Provable a -> Provable (Provable a).
Proof.
  intros a pa.
  refine (Pmodus _ (@loeb (a / Provable a) _)).
  prove. prove. prove.
Qed.

Theorem prudentfaircoops : Prudent <3 Fair.
Proof.
  unfix.
  apply loeb.
  prove.
  unfix. apply p2pp in H. prove. unfix. assumption.
  unfix. exact H.
Qed.

Definition PA_1 (a:Prop) := (forall {a:Prop}, Provable a -> a) -> a.

Theorem npnp : forall x, PA_1 (~Provable (~Provable x)).
Proof.
  intros x trust pnp.
  apply trust.
  apply loeb.
  prove.
  contradict H.
  prove.
Qed.

Theorem fairdbotdefect : PA_1 (~Fair <3 Defect).
Proof.
  intros trust cooperates.
  rewrite fixedpoint2 in cooperates.
  apply trust in cooperates.
  rewrite fixedpoint2 in cooperates.
  exact cooperates.
Qed.

(* Take the action for which you can prove the best lower bound. *)
Definition UDT (self other:Prop) := Provable (self -> other) / ~Provable (~self -> other).

Theorem theyneverknowUDTcoops : forall b, PA_1(~Provable (UDT <3 b)).
Proof. intros b trust pub. assert (pub' := pub). apply trust in pub. rewrite fixedpoint2 in pub. firstorder.
  clear H. contradict H0. prove.
Qed.

Notation "'UC'" := (UDT <3 UDT).
Lemma UDTdoesntgetexploitedbyUDT : UC <-> ~Provable (~UC -> UC).
Proof. split.
  intro. rewrite fixedpoint2 in H. firstorder.
  intro. unfix. firstorder. prove.
Qed.

Lemma modus_tollens: forall {p q: Prop}, (p->q) -> ~q -> ~p. auto. Qed.

Theorem udtcoops : PA_1 UC.
Proof.
  intros trust.
  rewrite UDTdoesntgetexploitedbyUDT.
  refine (modus_tollens (Pmodus _) (theyneverknowUDTcoops UDT trust)).
  prove.
  rewrite UDTdoesntgetexploitedbyUDT.
  rewrite UDTdoesntgetexploitedbyUDT in H.
  firstorder.
Qed.

Theorem prudentunexploitable : forall b, PA_1 (Prudent <3 b -> b <3 Prudent).
Proof. intros b trust pb. assert (eq := pb). rewrite fixedpoint2 in eq. apply trust in eq.
  firstorder.
Qed.

Theorem UDTunexploitable : forall b, PA_1 (UDT <3 b -> b <3 UDT).
Proof. intros b trust ub. assert (ub' := ub). rewrite fixedpoint2 in ub. destruct ub as [notexp _].
  apply trust in notexp. firstorder.
Qed.

Theorem whenPBcoopstheyknow : forall b, Prudent <3 b -> Provable (Prudent <3 b).
  intro b. unfix. intro pb. apply p2pp. firstorder.
Qed.

Theorem prudentudtdefect : PA_1 (~Prudent <3 UDT).
Proof.
  intros trust pu.
  absurd (Provable (UDT <3 Prudent)).
  exact (theyneverknowUDTcoops _ trust).
  assert (pu' := pu).
  rewrite fixedpoint2 in pu'.
  refine (Pmodus _ pu').
  refine (Pmodus _ (whenPBcoopstheyknow _ pu)).
  prove.
Qed.


Get this bounty!!!

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.