theft.v

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.