Universe inconsistency errors when using ZF model in Coq

Question

I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that each axiom holds in that context. The problem is, I'm getting stuck on the first of those steps.

My definition is as follows:

Inductive ZFSet : Type :=
  | sup : forall (A : Type), (A -> ZFSet) -> ZFSet.

Fixpoint ZFEq (S T : ZFSet) : Prop :=
  match S, T with
  | sup A f, sup B g =>
    (forall a, exists b, ZFEq (f a) (g b)) /\
    (forall b, exists a, ZFEq (f a) (g b))
  end.

Definition ZFIn E S : Prop :=
  match S with
  | sup A f => exists a, ZFEq E (f a)
  end.

Since the formal logic system needs to support predicates of arbitrary arity, I have defined:

Definition zf_in (a : Vector.t ZFSet 2) : Prop :=
  Vector.caseS' a (const Prop) (fun e a =>
  Vector.caseS' a (const Prop) (fun x a =>
  Vector.case0 (const Prop) (ZFIn e x) a))

so that ZFIn e x <-> zf_in [e; x]. I know that case0 is redundant, but it feels neater to me, and I doubt it will affect the core issue.

The trouble is, I need to prove that zf_in is compatible with ZFEq as an equivalence relation. In my system, that means proving:

Lemma zf_in_wd : forall (a b : Vector.t ZFSet 2),
  Vector.Forall2 ZFEq a b -> zf_in a -> zf_in b

I have already managed to prove:

Lemma ZFIn_wd : forall (e e' x x' : ZFSet), ZFEq e e' -> ZFEq x x' -> ZFIn e x -> ZFIn e' x'.

The problem is in closing the gap between these two Lemmas. I cannot figure out how to deconstruct the Vector.Forall2 ZFSet 2 object. Note that I can deconstruct the Vector ZFSet 2 objects into a fixed collection of variables just fine; it is only the Vector.Forall2 ZFSet 2 which is causing trouble.

I have tried the following tactics on a hypothesis named E, which generated the indicated errors:

• inversion E:

Illegal application: 
The term "sigT" of type "forall A : Type, (A -> Type) -> Type"
cannot be applied to the terms
"nat" : "Set"
"fun n : nat => Vector.t ZFSet n" : "nat -> Type"
The 2nd term has type "nat -> Type@{max(Set,ZFSet.u0+1)}" which should be coercible to
"nat -> Type@{sigT.u1}".

• dependent destruction E:

Illegal application: 
The term "JMeq" of type "forall A : Type, A -> forall B : Type, B -> Prop"
cannot be applied to the terms
"Vector.t ZFSet n" : "Type"
"gen_x" : "Vector.t ZFSet n"
"Vector.t ZFSet 2" : "Type"
"Vector.cons ZFSet ea 1 (Vector.cons ZFSet xa 0 (Vector.nil ZFSet))" : "Vector.t ZFSet 2"
The 1st term has type "Type@{max(Set,ZFSet.u0+1)}" which should be coercible to
"Type@{JMeq.u0}".

• dependent induction E: same as dependent destruction
• apply Vector.Forall2_nth_order in E:

Unable to apply lemma of type
"forall (A : Type) (P : A -> A -> Prop) (n : nat) (v1 v2 : VectorDef.t A n),
 VectorDef.Forall2 P v1 v2 <->
 (forall (i : nat) (Hi1 Hi2 : i < n),
  P (VectorDef.nth_order v1 Hi1) (VectorDef.nth_order v2 Hi2))"
on hypothesis of type
"Vector.Forall2 ZFEq (Vector.cons ZFSet ea 1 (Vector.cons ZFSet xa 0 (Vector.nil ZFSet)))
   (Vector.cons ZFSet eb 1 (Vector.cons ZFSet xb 0 (Vector.nil ZFSet)))".

• pose proof (proj1 (Vector.Forall2_nth_order ZFSet ZFEq 2 _ _) E):

In environment
ea, xa, eb, xb : ZFSet
E : Vector.Forall2 ZFEq (Vector.cons ZFSet ea 1 (Vector.cons ZFSet xa 0 (Vector.nil ZFSet)))
     (Vector.cons ZFSet eb 1 (Vector.cons ZFSet xb 0 (Vector.nil ZFSet)))
I : zf_set_interp 2 set_in_p
     (Vector.cons ZFSet ea 1 (Vector.cons ZFSet xa 0 (Vector.nil ZFSet)))
The term "ZFSet" has type "Type@{ZFSet.u0+1}" while it is expected to have type
"Type@{Vector.Forall2_nth_order.u0}" (universe inconsistency: Cannot enforce ZFSet.u0 <
Vector.Forall2_nth_order.u0 because Vector.Forall2_nth_order.u0 <= ZFSet.u0).

I believe that the last error message is most telling of the problem here. I'm not deeply familiar with the workings of the Coq universe, so I don't know where the constraint Vector.Forall2_nth_order.u0 <= ZFSet.u0 is coming from. If possible, I would like to know a solution that does not involve rewriting my formal logic system to use a custom, universe polymorphic copy of the Vector library. Thanks in advance!

Update

I've tracked down the source of the error by copy-pasting a minimal reproducible example. It worked fine directly under the definitions, but not down the file. The problem is in another definition:

Definition ZFUnion (x : ZFSet) : ZFSet.
Proof.
  destruct x as [A f].
  apply sup with (A := sigT A (fun a => match f a with sup B _ => B end)).
  intros [a b]. destruct (f a) as [B g]. exact (g b).
Defined.

which puts a constraint between sigT and ZFSet. This seems to be the root cause of all the problems. The neatest solution I can think of is making a duplicate of sigT for this one definition. This sort of issue seems to be the exact reason that Universe Polymorphism exists, but it's not applied to the standard library since it's still experimental.

Answer 1

Not sure exactly how your problem appears since you do not give the code up to the point where you get your failures so I cannot reproduce. But here is a self-contained example that should do the trick:

Require Import Vector RelationClasses Lia.

Import VectorNotations.

Inductive ZFSet : Type :=
  | sup : forall (A : Type), (A -> ZFSet) -> ZFSet.

Fixpoint ZFEq (S T : ZFSet) : Prop :=
  match S, T with
  | sup A f, sup B g =>
    (forall a, exists b, ZFEq (f a) (g b)) /\
    (forall b, exists a, ZFEq (f a) (g b))
  end.

Definition ZFIn E S : Prop :=
  match S with
  | sup A f => exists a, ZFEq E (f a)
  end.

Definition zf_in (a : Vector.t ZFSet 2) : Prop :=
  Vector.caseS' a (fun _ => Prop) (fun e a =>
  Vector.caseS' a (fun _ => Prop) (fun x a =>
  Vector.case0 (fun _ => Prop) (ZFIn e x) a)).

Instance ZFEq_trans : Transitive ZFEq.
Proof.
Admitted.

Instance ZFEq_sym : Symmetric ZFEq.
Proof.
Admitted.

Lemma ZFIn_wd : forall (e e' x x' : ZFSet), ZFEq e e' -> ZFEq x x' -> ZFIn e x -> ZFIn e' x'.
Proof.
Admitted.

Lemma zf_in_wd : forall (a b : Vector.t ZFSet 2),
  VectorDef.Forall2 ZFEq a b -> zf_in a -> zf_in b.
Proof.
  intros a b Heq Hin.
  set (x := hd a).
  set (x' := hd b).
  set (e := hd (tl a)).
  set (e' := hd (tl b)).
  assert (a = [x;e]).
  {
    etransitivity.
    1: apply Vector.eta.
    f_equal.
    unfold e.
    etransitivity.
    1: apply Vector.eta.
    f_equal.
    apply (case0 (fun v => v = [])).
    reflexivity.
  }
  assert (b = [x';e']).
  {
    etransitivity.
    1: apply Vector.eta.
    f_equal.
    unfold e.
    etransitivity.
    1: apply Vector.eta.
    f_equal.
    apply (case0 (fun v => v = [])).
    reflexivity.
  }
  clearbody x x' e e'.
  cbn in *.
  subst.
  (* Interesting bit from here *)
  assert (ZFEq x x').
  {
    unshelve eapply Vector.Forall2_nth_order in Heq.
    1: exact 0.
    1-2: lia.
    assumption.
  }
  assert (ZFEq e e').
  {
    unshelve eapply Vector.Forall2_nth_order in Heq.
    1: exact 1.
    1-2: lia.
    assumption.
  }
  eapply ZFIn_wd.
  all: eassumption.
Qed.

The interesting bit can be replaced by the maybe more compact

  pose proof Forall2_nth_order as [H _].
  specialize (H Heq).
  pose proof (H 0 ltac:(lia) ltac:(lia)) as H' ; cbn in H'.
  pose proof (H 1 ltac:(lia) ltac:(lia)) as H'' ; cbn in H''.

Not sure which one is best.

I am rather puzzled by the last error you encounter: I would really not have though this kind of things to throw universe level errors.

On the other hand, I second Andrej's advise to stay away from vectors in this kind of setting: the arity-based version is much cleaner if you want to statically enforce well-formed formulae. And even if you want to keep use vectors, I believe those from the standard library of Coq, that you are using, are advised against, as they have the tendency to lead to nasty dependency issues.

Answer 2

Here is how I would go about formalizing first-order logic and models, with a small fragment of ZF as an example. Note that we can still carry out Gödel coding by natural numbers, so long as the types appearing in the signature can be Gödel coded.

The same code is also available in this gist.

(*
   A formalization of first-order logic, theories and their models.
   As an example we formalize the language of ZF set theory and a a small fragment of ZF.
*)

(* A signature is given by function symbols, relation symbols, and their arities. *)
Structure Signature :=
  { funSym : Type (* names of function symbols *)
  ; funArity : funSym -> Type (* arities of function symbols *)
  ; relSym : Type (* names of relation symbols *)
  ; relArity : relSym -> Type (* arities of relation symbols *)
  }.

Arguments funArity {_} _.
Arguments relArity {_} _.

(* A context is just a type whose elements are the variables. *)
Definition Context := Type.

Inductive EmptyContext := .

(* Extension of a context by a fresh variable. The constructors are named S and Z
   for "successor" and "zero", because we use them later on to construct deBruijn indices. *)
Inductive Extend (Γ : Context) : Context :=
  | Z : Extend Γ
  | S : Γ -> Extend Γ
.

Arguments S {_} _.
Arguments Z {_}.

(* Terms in a context, where a context is simply a type whose elements are variables. *)
Inductive term (Σ : Signature) (Γ : Context) : Type :=
  | var : Γ -> term Σ Γ
  | tm : forall (f : funSym Σ), (funArity f -> term Σ Γ) -> term Σ Γ
.

Arguments var {_} {_} _.
Arguments tm {_} {_} _ _.

(* First-order formulas over a given signature and context. *)
Inductive formula (Σ : Signature) (Γ : Context) : Type :=
  | rel : forall (R: relSym Σ), (relArity R -> term Σ Γ) -> formula Σ Γ
  | equal : term Σ Γ -> term Σ Γ -> formula Σ Γ
  | true : formula Σ Γ
  | conj : formula Σ Γ -> formula Σ Γ -> formula Σ Γ
  | disj : formula Σ Γ -> formula Σ Γ -> formula Σ Γ
  | impl : formula Σ Γ -> formula Σ Γ -> formula Σ Γ
  | not : formula Σ Γ -> formula Σ Γ
  | all : formula Σ (Extend Γ) -> formula Σ Γ
  | some : formula Σ (Extend Γ) -> formula Σ Γ
.

Arguments rel {_} {_} _ _.
Arguments equal {_} {_} _ _.
Arguments true {_} {_}.
Arguments conj {_} {_} _ _.
Arguments disj {_} {_} _ _.
Arguments impl {_} {_} _ _.
Arguments not {_} {_} _.
Arguments all {_} {_} _.
Arguments some {_} {_} _.

Definition iff {Σ : Signature} {Γ : Context} (p q : formula Σ Γ) :=
  conj (impl p q) (impl q p).

Definition closedFormula Σ := formula Σ EmptyContext.

(* An interpretation of a signature Σ is given by a carrier
   and interpretations of the function and relation symbols of Σ. *)
Structure Interpretation (Σ : Signature) : Type :=
  { carrier :> Type
  ; interpRel : forall (R : relSym Σ), (relArity R -> carrier) -> Prop
  ; interpFun : forall (f : funSym Σ), (funArity f -> carrier) -> carrier
  }.

Arguments interpRel {_} {_} _ _.
Arguments interpFun {_} {_} _ _.

(* A valuation is a map from variables to the carrier of an interpretation. *)
Definition valuation {Σ} {I : Interpretation Σ} (Γ : Context) := Γ -> I.

Definition emptyValuation {Σ} {I : Interpretation Σ}: @valuation Σ I EmptyContext :=
  fun x => match x with end.

(* Extend a valuation η by one more value. *)
Definition extend {Σ} {I : Interpretation Σ} {Γ : Context} (η : valuation Γ) (v : I) (x : Extend Γ) : I :=
  match x with
  | S y => η y
  | Z => v
  end.

(* Extend an interpretation to terms. *)
Fixpoint interpTerm {Σ} {I : Interpretation Σ} {Γ : Context} (η : valuation Γ) (t : term Σ Γ) : I :=
  match t with
  | var x => η x
  | tm f ts => interpFun f (fun i => interpTerm η (ts i))
  end.

(* Extend an interpretation to formulas. *)
Fixpoint interpFormula {Σ} (I : Interpretation Σ) {Γ : Context} (η : valuation Γ) (F : formula Σ Γ) : Prop :=
  match F with
  | rel R ts => interpRel R (fun i => interpTerm η (ts i))
  | equal t u => interpTerm η t = interpTerm η u
  | true => True
  | conj F₁ F₂ => interpFormula I η F₁ /\ interpFormula I η F₂
  | disj F₁ F₂ => interpFormula I η F₁ \/ interpFormula I η F₂
  | impl F₁ F₂ => interpFormula I η F₁ -> interpFormula I η F₂
  | not F => ~ (interpFormula I η F)
  | all F => forall (v : I), interpFormula I (extend η v) F
  | some F => exists (v : I), interpFormula I (extend η v) F
  end.

(* A first-order theory over a signature Σ is given by a type of axiom names, and axiom statements. *)
Structure Theory (Σ : Signature) :=
  { axiom_name :> Type (* names of axioms *)
  ; axiom : axiom_name -> closedFormula Σ (* axiom statements *)
  }.

Arguments axiom {_} {_}.

(* A model is given by an interpretation and validation of the axioms. *)
Structure Model {Σ : Signature} (T : Theory Σ) :=
  { theoryInterp : Interpretation Σ
  ; theoryValid : forall (ax : T), interpFormula theoryInterp emptyValuation (axiom ax)
  }.

Section ZF.
  (* Example:
     ZF is a small "proto" fragment of ZF whose axioms are just the empty set and union.
     Note that the model given here does not validate extensionality. We would have to
     extend interpretations so that they interpret equality as equivalence relation if
     we wanted to validate extensionality (because Coq does not have quotients).
  *)

  (* Binary arity *)
  Inductive binary := arg1 | arg2.

  (* There is one relation symbol, called "elementOf" *)
  Inductive ZF_relSymbol := elementOf.

  (* The ZF signature. *)
  Definition ZFΣ : Signature :=
    {| funSym := Empty_set
    ;  funArity := fun x => match x with end
    ;  relSym := ZF_relSymbol
    ;  relArity := fun elementOf => binary
    |}.

  Definition ZF_term (Γ : Context) := term ZFΣ Γ.
  Definition ZF_formula := formula ZFΣ.
  Definition ZF_closedFormula := closedFormula ZFΣ.

  (* Short-hand for writing down "u is element of v" *)
  Definition elem {Γ : Context} (u v : ZF_term Γ) :=
    @rel ZFΣ Γ elementOf (fun i => match i with arg1 => u | arg2 => v end).

  (* The axioms names. *)
  Inductive ZF_axiom_name :=
  | ZF_empty
  | ZF_union
  .

  (* Axiom statements. *)
  Definition ZF_axiom (ax : ZF_axiom_name) : ZF_closedFormula :=
    match ax with

    | ZF_empty =>
        (* ∃ sz ∀ z, ¬ (z ∈ sz) *)
        some (all (not (elem (var Z) (var (S Z)))))

    | ZF_union =>
        (* ∀ x ∃ y . ∀ z . (z ∈ y) ⇔ (∃ w . w ∈ x ∧ y ∈ w) *)
        all (some (all (
          iff
            (elem (var Z) (var (S Z)))
            (some (conj
                    (elem (var Z) (var (S (S (S Z)))))
                    (elem (var (S Z)) (var Z))
                  ))
        )))
    end.

  Definition ZF_Theory : Theory ZFΣ :=
    {| axiom_name := ZF_axiom_name
     ; axiom := ZF_axiom
    |}.

  (* We next construct a model V of ZF_Theory. *)

  Inductive ZFSet : Type :=
  | zf : forall (A : Type), (A -> ZFSet) -> ZFSet.

  (* The underlying index type of a ZF-set *)
  Definition index (x : ZFSet) : Type :=
    match x with
    | zf A _ => A
    end.

  (* The element of a ZF-set at a given index. *)
  Definition el (x : ZFSet) (i : index x) : ZFSet.
  Proof.
    destruct x as [I f].
    exact (f i).
  Defined.

  (* The interpretation of ∈. *)
  Definition ZFelem (u : binary -> ZFSet) : Prop :=
    match u arg2 with
    | zf _ s => exists i, u arg1 = s i
    end.

  (* The interpretation of ZFΣ in ZFSet. *)
  Definition ZFI : Interpretation ZFΣ :=
    {| carrier := ZFSet
     ; interpRel := fun (r : relSym ZFΣ) => match r with elementOf => ZFelem end
     ; interpFun := fun f => match f with end
    |}.

  Definition ZFempty : ZFSet :=
    zf Empty_set (fun x => match x with end).

  Definition ZFunion (x : ZFSet) : ZFSet.
  Proof.
    destruct x as [I x].
    apply (zf {i : I & index (x i)}).
    intros [i j].
    exact (el (x i) j).
  Defined.

  (* Auxliary lemma, it should exist in the standard library. *)
  Definition convert {A B : Type} (e : A = B) (x : A) : B :=
    match e in (_ = T) return T with
    | eq_refl => x
    end.

  (* Finally, we define the model. *)
  Definition V : Model ZF_Theory.
  Proof.
    exists ZFI.
    intros [|].
    - (* empty set axiom *)
      exists ZFempty.
      intros x [[] ?].
    - (* union *)
      intros [I x].
      exists (ZFunion (zf I x)).
      intros [J y].
      split.
      + intros [[i j] eq].
        exists (x i).
        split.
        * now exists i.
        * destruct (x i).
          now exists j.
      + intros [[K z] [[i H] [k G]]].
        pose (k' := convert (f_equal index H) k).
        exists (existT (fun (i : I) => index (x i)) i k').
        destruct H as [].
        now transitivity (z k).
  Defined.
End ZF.
```