Last active
June 27, 2020 23:13
-
-
Save Gurkenglas/37174a002777ea302d9bdbef73c07326 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment