Approx.v

Require Import ZArith.
Open Scope Z_scope.

Notation "x '/<' y" := (x / y)
  (at level 40, left associativity).

Definition div_nearest_down (x y : Z) : Z := (1 + (2 * x - 1) /< y) /< 2.

Notation "x '/~<' y" := (div_nearest_down x y)
  (at level 40, left associativity).

Definition div_nearest_up (x y : Z) : Z := (1 + 2 * x /< y) /< 2.

Notation "x '/~>' y" := (div_nearest_up x y)
  (at level 40, left associativity).

Definition clamp (l u x : Z) : Z :=
  if x <? l then l else
  if x >? u then u else x.

Definition approx (l u m x : Z) : Z :=
  if x <? l then l else
  if x >? u then u else
  l + m * ((1 + (2 * (x - l) - 1) /< m) /< 2).

Definition approx_valid (l u m x : Z) : Prop :=
  l <= u /\ m > 0 /\ (u - l) mod m = 0.

Definition approx' (l u m x : Z) : Z :=
  l + m * ((clamp l u x - l) /~< m).

Import Z.

Theorem approx_lower_bound : forall l u m x : Z,
  approx_valid l u m x -> approx l u m x >= l.
Proof.
  unfold approx, approx_valid. intros l u m x [Hlelu [Hgtm0 Heq]].
  destruct (ltb_spec x l) as [Hltxl | Hlelx].
  - omega.
  - destruct (gtb_spec x u) as [Hltux | Hlexu].
    + omega.
    + apply le_ge. rewrite <- (add_0_r l) at 1. apply Zplus_le_compat_l.
      rewrite <- (mul_0_r m). apply mul_le_mono_nonneg_l.
      * omega.
      * apply div_pos.
          ++ destruct (eqb_spec l x) as [Heqlx | Feqlx].
            ** apply eq_le_incl. rewrite Heqlx. rewrite sub_diag.
              rewrite mul_0_r. rewrite sub_0_l.
              destruct (leb_spec m 1).
              --- replace m with 1 by omega. reflexivity.
              --- rewrite Z_div_nz_opp_full.
                +++ rewrite div_1_l by omega. reflexivity.
                +++ rewrite mod_1_l by omega. omega.
            ** assert (l < x) as Hltlx by omega.
              assert (exists y : Z, succ y = x - l).
              exists (pred (x - l)). apply succ_pred.
              induction H as [y H]. rewrite <- H. rewrite mul_succ_r.
              replace (2 * y + 2 - 1) with (2 * y + 1) by omega.
              rewrite <- (add_0_r 0). apply add_le_mono.
              --- omega.
              --- rewrite <- (div_0_l m) by omega. apply div_le_mono.
                +++ omega.
                +++ omega.
          ++ omega. Qed.

Theorem approx_upper_bound : forall l u m x : Z,
  approx_valid l u m x -> approx l u m x <= u.
Proof.
  unfold approx, approx_valid. intros l u m x [Hlelu [Hgtm0 Heq]].
  destruct (ltb_spec x l) as [Hltxl | Hlelx].
  - omega.
  - destruct (gtb_spec x u) as [Hltux | Hlexu].
    + omega.
    + (* by symmetry. *) Admitted.

Theorem approx_divisible_lower : forall l u m x : Z,
  approx_valid l u m x -> (approx l u m x - l) mod m = 0.
Proof.
  unfold approx, approx_valid. intros l u m x [Hlelu [Hgtm0 Heq]].
  destruct (ltb_spec x l) as [Hltxl | Hlelx].
  - rewrite sub_diag. rewrite mod_0_l by omega. reflexivity.
  - destruct (gtb_spec x u) as [Hltux | Hlexu].
    + apply Heq.
    + rewrite add_simpl_l. rewrite (mul_comm m). apply Z_mod_mult. Qed.

Theorem approx_divisible_upper : forall l u m x : Z,
  approx_valid l u m x -> (u - approx l u m x) mod m = 0.
Proof.
  unfold approx, approx_valid. intros l u m x [Hlelu [Hgtm0 Heq]].
  destruct (ltb_spec x l) as [Hltxl | Hlelx].
  - apply Heq.
  - destruct (gtb_spec x u) as [Hltux | Hlexu].
    + rewrite sub_diag. apply mod_0_l. omega.
    + rewrite sub_add_distr. rewrite Zminus_mod. rewrite Heq.
      rewrite sub_0_l. apply Z_mod_zero_opp.
      * omega.
      * rewrite Zmod_mod. rewrite (mul_comm m). apply Z_mod_mult. Defined.

gpt3coq.py

import sys, pexpect

coqtop = pexpect.spawn("coqtop -load-vernac-source " + sys.argv[1])

coqtop.expect("\n\w* < ")
if coqtop.before.find("Error".encode()) == -1:
  sys.stderr.write("module didn't compile")

with open (sys.argv[1], "r") as promptfile:
  prompt = promptfile.read()

import openai

while(True):
  line = openai.Completion.create(model="davinci", prompt=prompt, stop=".", temperature=0, max_tokens=300)
  coqtop.sendline(line)
  coqtop.expect("\n\w* < ")
  if coqtop.before.find("Error".encode()) == -1:
    print(line)
    prompt += line + "\n"
  else:
    sys.stderr.write("Tried: " + line)

modal.v

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 *)
Ltac loebprove := apply loeb; prove.

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. loebprove. unfix. prove. Qed.

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

Theorem prudentfaircoops : Prudent <3 Fair.
Proof.
  unfix.
  loebprove.
  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.
  loebprove.
  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).

Lemma composition : forall {a b c:Prop}, (b -> c) -> (a -> b) -> (a -> c). intuition. Qed.
Lemma modus_tollens: forall {p q: Prop}, (p->q) -> ~q -> ~p. auto. Qed.

Theorem theyneverknowUDTcoops : forall b, PA_1(~Provable (UDT <3 b)).
Proof.
  intros d trust.
  unfix.
  refine (_ (npnp trust)). intuition.
  contradict x.
  prove.
  destruct H as [_ u].
  contradict u.
  exact H0.
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.

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.