Definitions and proofs for simplified constraint-based auction

AGT-FOL.v

Require Import PeanoNat.

Inductive Atom {T: Type} : Type :=
| avar: nat -> Atom
| aconst: T -> Atom
.

Inductive prop {T: Type} : Type :=
| Eq : @Atom T -> @Atom T -> prop
| Lt : @Atom nat -> @Atom nat -> prop
| Not : prop -> prop
| Imp : prop -> prop -> prop
| Iff : prop -> prop -> prop
| And : prop -> prop -> prop
.

Definition interpret (T: Type) : Type := @Atom T -> T.

Fixpoint sem {T: Type} (pval: interpret T) (nval: interpret nat) (p: prop) : Prop :=
  match p with
  | Eq v1 v2 => pval v1 = pval v2
  | Lt v1 v2 => nval v1 < nval v2
  | Not p => ~ sem pval nval p
  | Imp p1 p2 => sem pval nval p1 -> sem pval nval p2
  | Iff p1 p2 => sem pval nval p1 <-> sem pval nval p2
  | And p1 p2 => sem pval nval p1 /\ sem pval nval p2
  end
.

Inductive player :=
  | player_a
  | player_b
.

Lemma player_eq_dec: forall (p q: player), {p = q}+{p <> q}.
Proof.
  intros.
  destruct p, q; try (left; reflexivity); right; intro; discriminate.
Qed.

Definition other (p: player) :=
  match p with player_a => player_b | _ => player_a end.

Lemma other_eq_irrefl: forall p, other p <> p.
Proof. destruct p; discriminate. Qed.

Record Outcome : Set := mkOutcome
  { winner: player
  ; pays_winner: nat
  }.


Definition Winner := @avar player 0.
Definition PaysWinner := @avar nat 0.

Definition interpret_player_outcome (outcome: Outcome) c :=
  match c with
  | avar 0 => winner outcome
  | avar _ => player_a
  | aconst x => x
  end.

Definition interpret_payment_outcome (outcome: Outcome) c :=
  match c with
  | avar 0 => pays_winner outcome
  | avar _ => 0
  | aconst x => x
  end.

Definition sem_aug outcome := sem (interpret_player_outcome outcome) (interpret_payment_outcome outcome).

Definition simple_participation_constraints (me: player) (bid: nat) : prop :=
  Iff (Eq Winner (aconst me)) (Lt PaysWinner (aconst bid))
.

Lemma higher_bid_wins: forall outcome (x y: player) j k,
  x <> y ->
  sem_aug outcome (simple_participation_constraints x j) ->
  sem_aug outcome (simple_participation_constraints y k) ->
  j < k ->
  winner outcome = y.
Proof.
  intros outcome x y j k.
  intros diff_xy [A1 _] [_ B2] j_lt_k.
  simpl in A1, B2.
  destruct (player_eq_dec (winner outcome) y).
  * exact e.
  * apply B2.
    apply Nat.lt_trans with (m:=j); try exact j_lt_k.
    destruct x, y, (winner outcome); try intuition.
Qed.

Lemma winner_pays_more: forall outcome loser j k,
  sem_aug outcome (simple_participation_constraints loser j) ->
  sem_aug outcome (simple_participation_constraints (winner outcome) k) ->
  k < j ->
  (winner outcome) = loser.
Proof.
  intros outcome loser j k.
  intros [_ A] [B _] k_lt_j.
  simpl in A, B.
  apply A.
  apply Nat.lt_trans with (m:=k); try exact k_lt_j.
  apply B.
  reflexivity.
Qed.

Definition game {T: Type} := player -> @prop T.

Definition simple_game j k p := 
  match p with
  | player_a => simple_participation_constraints player_a j
  | player_b => simple_participation_constraints player_b k
  end.

Definition game_sem outcome (g: game) :=
  sem_aug outcome (g player_a) /\ sem_aug outcome (g player_b).

Lemma monotone: forall outcome1 outcome2 j bid1 bid2,
   game_sem outcome1 (simple_game j bid1) ->
   game_sem outcome2 (simple_game j bid2) ->
   bid1 < bid2 ->
   (winner outcome1 = player_b \/ winner outcome2 = player_a) ->
   winner outcome2 = winner outcome1
.
Proof.
   unfold simple_game.
   unfold game_sem.
   unfold sem_aug.
   simpl.
   intros [w1 p1] [w2 p2] j bid1 bid2 [[G1x G1y] [G1m G1n]] [[G2x G2y] [G2m G2n]] PM ?.
   simpl in *.
   intuition; [subst w1; destruct w2|subst w2; destruct w1]; try reflexivity; intuition;
   apply G2n;
   apply Nat.lt_trans with (m := j); try assumption;
   apply Nat.lt_trans with (m := bid1); try assumption;
   apply Nat.le_lt_trans with (m := p1); try assumption;
   apply Nat.nlt_ge;
   intuition;
   discriminate.
Qed.

Lemma simple_game_symm : forall j k p q,
  game_sem (mkOutcome p q) (simple_game j k) <-> game_sem (mkOutcome (other p) q) (simple_game k j).
Proof.
   unfold game_sem.
   unfold sem_aug.
   intros j k p q.
   destruct p; simpl in *; intuition.
Qed.


Definition valid (P P': Outcome -> Prop) := forall t,
  (exists outcome, P' outcome /\ t = pays_winner outcome) ->
  (exists outcome, P' outcome /\ P outcome /\ t <= pays_winner outcome)
.

Definition simple_participation (me: player) (bid: nat) (outcome: Outcome) : Prop :=
     winner outcome = me <-> pays_winner outcome < bid
.

Lemma join_only_different : forall j p1 p2 outcome,
  simple_participation p1 j outcome
  -> simple_participation p2 j outcome
  -> p1 = p2.
Proof.
  intros j p1 p2 outcome [A J] [B K].
  destruct (winner outcome), p1, p2; intuition.
Qed.

Lemma join_valid : forall j k t pj pk,
  k <> j ->
  (exists outcome, simple_participation pj j outcome
                /\ winner outcome = pj
                /\ t = pays_winner outcome) ->
  (exists outcome, simple_participation pj j outcome
                /\ simple_participation pk k outcome
                /\ t <= pays_winner outcome).
Proof.
  unfold simple_participation.
  intros j k t pj pk k_ne_j [outcome [[A _] [E Q]]].
  rewrite -> E in *. clear E.
  rewrite <- Q in *. clear Q.
  assert (E: t < j) by (apply A; reflexivity).
  clear A.

  destruct (player_eq_dec pk pj) as [<- | P_NE].
  ++
    clear k_ne_j.
    exists (mkOutcome (other pk) (max j k)).
    simpl.
    repeat split;
    try (intro Q; apply other_eq_irrefl in Q; contradiction);
    try (intro Q; apply Nat.max_lub_lt_iff in Q; inversion Q as [Q1 Q2]; exfalso).
    - contradict Q1. apply Nat.lt_irrefl.
    - contradict Q2. apply Nat.lt_irrefl.
    - apply Nat.lt_le_incl in E. 
      apply (Nat.le_trans _ _ _ E), Nat.le_max_l.
  ++
    destruct (Nat.lt_decidable j k) as [J_LT_K | NOT_J_LT_K].
    *
      exists (mkOutcome pk j).
      simpl.
      split.
      + split; intro Q; contradict Q; [exact P_NE | apply Nat.lt_irrefl].
      + split.
        - split; intro; [exact J_LT_K | reflexivity].
        - apply Nat.lt_le_incl, E.
    *
      apply Nat.nlt_ge in NOT_J_LT_K.
      exists (mkOutcome pj (max t k)).
      simpl.
      split.
      + split.
        -- apply Nat.max_case.
           - intuition.
           - rewrite -> Nat.le_neq.
             intuition.
        -- reflexivity.
      + split.
        - split; intro H.
           ** symmetry in H.
              intuition.
           ** exfalso.
              rewrite -> Nat.max_lub_lt_iff in H.
              inversion H as [_ H2].
              apply (Nat.lt_irrefl _ H2).
        - apply Nat.le_max_l.
Qed.

Definition strategy (p: prop) (f: prop -> Outcome) :=
   sem_aug (f p) p.


Definition strategy_2 (p1 p2: prop) (f: prop -> prop -> Outcome) :=
   sem_aug (f p1 p2) p1 /\ sem_aug (f p1 p2) p2.


Definition first_price (p: prop) : Outcome := 
  match p with
  | Iff (Eq (avar 0) (aconst pk)) (Lt (avar 0) (aconst (S k))) => mkOutcome pk k
  | _ => mkOutcome player_a 0
  end.

Lemma first_price_is_strategy: forall p pk,
  strategy (simple_participation_constraints p (S pk)) first_price.
Proof.
  intros.
  unfold simple_participation_constraints.
  unfold strategy.
  unfold sem_aug.
  simpl.
  split; intro.
  - apply Nat.lt_succ_diag_r.
  - reflexivity.
Qed.


Definition second_price (p1 p2: prop) : Outcome := 
  match p1, p2 with
  | Iff (Eq (avar 0) (aconst pk)) (Lt (avar 0) (aconst (S k))),
    Iff (Eq (avar 0) (aconst pj)) (Lt (avar 0) (aconst (S j))) => if k <? j then mkOutcome pj (S k)
                                                                  else mkOutcome pk (S j)
  | _, _ => mkOutcome player_a 0
  end.


Lemma second_price_is_strategy: forall pj pk j k,
  pj <> pk
  -> j <> k
  -> strategy_2 (simple_participation_constraints pk (S k))
                (simple_participation_constraints pj (S j)) second_price.
Proof.
  intros.
  unfold simple_participation_constraints.
  unfold strategy_2.
  unfold sem_aug.
  simpl.
  destruct (k <? j) eqn:Q; simpl; split; split; try intro; try reflexivity; try (exfalso; apply (Nat.lt_irrefl _ H1)).
    
    - exfalso. apply H, H1. 
    - rewrite -> Nat.ltb_lt in Q.
      rewrite <- Nat.succ_lt_mono.
      assumption.
    - rewrite -> Nat.ltb_ge in Q.
      assert (j <= k /\ j <> k) by (split; assumption).
      apply Nat.le_neq in H2.
      rewrite <- Nat.succ_lt_mono.
      assumption.
    - exfalso. symmetry in H1. apply H, H1.
Qed.

Lemma second_price_independent: forall pj pk j k l w1 w2,
  pj <> pk
  -> mkOutcome pj w1 = second_price (simple_participation_constraints pk (S k)) (simple_participation_constraints pj (S j))
  -> mkOutcome pj w2 = second_price (simple_participation_constraints pk (S k)) (simple_participation_constraints pj (S l))
  -> w1 = w2.
Proof.
  simpl.
  intros.
  destruct (k <? j), (k <? l); inversion H0; inversion H1; intuition.
Qed.

Lemma second_price_independent': forall pj pk j k l p w1 w2,
  pk <> pj
  -> mkOutcome p w1 = second_price (simple_participation_constraints pk (S k)) (simple_participation_constraints pj (S j))
  -> mkOutcome p w2 = second_price (simple_participation_constraints pk (S k)) (simple_participation_constraints pj (S l))
  -> w1 <> w2
  -> p <> pj.
Proof.
  simpl.
  intros.
  destruct (k <? j), (k <? l); inversion H0; inversion H1; clear H0 H1; intro; try (subst w1 w2 p pj; intuition).
  subst w1 w2 p. apply H2. reflexivity.
Qed.