God.v

Module Type GAxioms.
    Axiom U : Set.
    Axiom causes : U -> U -> Prop.
    Axiom isPartOf : U -> U -> Prop.

    Definition S (r : U) : Prop := causes r r.
    Definition C (r : U) : Prop := exists s, causes r s.
    Definition O (q : U) : Prop := forall t, causes q t.

    Axiom A1 : forall r, exists v, causes v r.
    Axiom A2 : forall r s t, causes r s -> causes s t -> causes r t.
    Axiom A3 : forall r s, causes r s -> causes s r -> r = s.
    Axiom A4 : forall r s, causes r s -> forall u, isPartOf u s -> causes r u.
    Axiom A5 : exists r, forall z, C z -> isPartOf z r.
End GAxioms.

Module ExampleModel : GAxioms.
    Definition U := unit.

    Definition causes (_ : U) (_ : U) := True.
    Definition isPartOf (_ : U) (_ : U) := True.

    Definition S (r : U) : Prop := causes r r.
    Definition C (r : U) : Prop := exists s, causes r s.
    Definition O (q : U) : Prop := forall t, causes q t.

    Ltac solve_it :=
        cbv; repeat (auto; intros; eexists).

    Theorem A1: forall r, exists v, causes v r.
        solve_it.
    Qed.

    Theorem A2: forall r s t, causes r s -> causes s t -> causes r t.
        solve_it.
    Qed.

    Theorem A3: forall r s, causes r s -> causes s r -> r = s.
        induction r, s. solve_it.
    Qed.

    Theorem A4: forall r s, causes r s -> forall u, isPartOf u s -> causes r u.
        solve_it.
    Qed.

    Theorem A5: exists r, forall z, C z -> isPartOf z r.
        solve_it.
    Qed.
End ExampleModel.

Module GodExists (G : GAxioms).
    Import G.

    Hint Resolve A1 A2 A3 A4 A5.
    Hint Unfold S C O.

    Theorem T1: exists x, O x.
    Proof.
        destruct A5 as [h H0].
        unfold O, C in *.
        destruct (A1 h) as [a H1].
        exists a.
        intros t.
        destruct (A1 t) as [b H2].
        specialize (H0 b).
        set (H3 := A4 a h H1 b).
        set (H4 := A2 a b t).
        eauto.
    Qed.

    Theorem T2: exists y, S y /\ O y.
    Proof.
        destruct T1 as [x H].
        exists x.
        auto.
    Qed.

    Theorem T3:
        exists! x, S x /\ O x.
    Proof.
        destruct T1 as [x H].
        exists x. split. auto.
        intros x' [? ?].
        eauto.
    Qed.
End GodExists.