Skip to content

Instantly share code, notes, and snippets.

@jaykru jaykru/theft.v Secret
Last active Sep 22, 2019

Embed
What would you like to do?
Definition time := nat.
Section Theft.
Context (Person Object: Set).
(* In this meme we model monopolistic ownership of objects as follows:
A person owns /with monopoly/ an object at time t if
they were consensually given the object by someone who owned the object at time t-1.
Retainment of an object over time is modeled as reflexive giving. *)
(* A receipt is some proof of consent to transfer of ownership that
we leave abstract here. The details aren't necessary for our proof. *)
Context (receipt: Person -> Object -> Person -> time -> Set).
Inductive own: time -> Person -> Object -> Prop :=
| Give (person1 person2: Person) (ob: Object) (t: time):
own t person1 ob ->
receipt person1 ob person2 t ->
own (S t) person2 ob.
(* In the above described and formalized model, no one can legitimately
own anything at any time. *)
Theorem theft: forall o p t, not (own t p o).
intros ? ? ? H;
induction H;
auto.
Qed.
(* God, regarded as a generator of free receipts, allows for legitimate
monopolistic ownership over objects. *)
Axiom (god: Person).
Inductive own': time -> Person -> Object -> Prop :=
| Give' (person1 person2: Person) (ob: Object) (t: time):
own t person1 ob ->
receipt person1 ob person2 t ->
own' (S t) person2 ob
| Godgiven person ob:
receipt god ob person 0 ->
own' 0 person ob.
Theorem refute_theft: forall person o, receipt god o person 0 ->
~ (forall o p t, not (own' t p o)).
intros ??? H0;
eapply (H0 _ _ 0);
econstructor;
exact H.
Qed.
End Theft.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.