Library IZF.IZF_logic


Universes

In what follows, we will work with explicit universes rather than with Coq-style implicit universes.
For that, we define two universes Typ1 and Typ2 as shorthands for the generic universe Type by enforcing the constraint Typ1 : Typ2 so that Coq knows that the implicit index associated to Typ1 is smaller than the implicit index associated to Typ2.

Definition Typ2 := Type.
Definition Typ1 : Typ2 := Type.
Intuitively:
  • Typ1 is the universe of small types, which contains the type Prop of propositions, and is closed under dependent product.
  • Typ2 is the top-universe of large types, which contains the universe Typ1, and is closed under dependent product again.
In the following, small types (i.e. the inhabitants of Typ1) will be used as the carriers of pointed graphs (for representing sets).
The type of binary relations:

Definition Rel (X : Typ1) : Typ1 := X → X → Prop.

Logical connectives

To avoid the use of Coq-style inductive definitions, we redefine all the logical connectives from their second-order encoding and give their introduction rules. Except in a few cases, it is not necessary to give the corresponding elimination rules whose behaviour is mimicked by using the tactic Apply H (instead of Elim H) in the subsequent proof-scripts.

Truth and falsity


Definition top : Prop := ∀ E : Prop, E → E.

Lemma top_intro : top.
Proof fun E e ⇒ e.

Definition bot : Prop := ∀ E : Prop, E.

Conjunction


Definition and (A B : Prop) : Prop := ∀ E : Prop, (A → B → E) → E.

Lemma and_intro : ∀ A B : Prop, A → B → and A B.
Proof fun A B a b E f ⇒ f a b.

Lemma and_fst : ∀ A B : Prop, and A B → A.
Proof fun A B p ⇒ p A (fun a _ ⇒ a).

Lemma and_snd : ∀ A B : Prop, and A B → B.
Proof fun A B p ⇒ p B (fun _ b ⇒ b).

Disjunction


Definition or (A B : Prop) : Prop :=
  ∀ E : Prop, (A → E) → (B → E) → E.

Lemma or_inl : ∀ A B : Prop, A → or A B.
Proof fun A B a E f g ⇒ f a.

Lemma or_inr : ∀ A B : Prop, B → or A B.
Proof fun A B b E f g ⇒ g b.

Logical equivalence


Definition iff (A B : Prop) : Prop := and (A → B) (B → A).

Existential quantifiers and Leibniz equality

Existential quantification in a given small type


Definition ex (X : Typ1) (P : X → Prop) : Prop :=
  ∀ E : Prop, (∀ x : X, P x → E) → E.

Lemma ex_intro : ∀ (X : Typ1) (P : X → Prop) (x : X), P x → ex X P.
Proof fun X P x p E f ⇒ f x p.

We define a variant of the former existential quantification in order to express the existence of an object that fulfills the conjunction of two predicates P and Q.

Definition ex2 (X : Typ1) (P Q : X → Prop) : Prop :=
  ∀ E : Prop, (∀ x : X, P x → Q x → E) → E.

Lemma ex2_intro :
 ∀ (X : Typ1) (P Q : X → Prop) (x : X), P x → Q x → ex2 X P Q.
Proof fun X P Q x p q E f ⇒ f x p q.

Existential quantification over all small types


Definition exT (P : Typ1 → Prop) : Prop :=
  ∀ E : Prop, (∀ X : Typ1, P X → E) → E.

Lemma exT_intro : ∀ (P : Typ1 → Prop) (X : Typ1), P X → exT P.
Proof fun P X p E f ⇒ f X p.

Existential quantification over all pointed graphs


Definition exG (P : ∀ X : Typ1, Rel X → X → Prop) : Prop :=
  ∀ E : Prop, (∀ (X : Typ1) (A : Rel X) (a : X), P X A a → E) → E.

Lemma exG_intro :
 ∀ (P : ∀ X : Typ1, Rel X → X → Prop) (X : Typ1)
   (A : Rel X) (a : X), P X A a → exG P.

Proof fun P X A a p E f ⇒ f X A a p.

Leibniz equality


Definition eq (X : Typ1) (x y : X) : Prop := ∀ P : X → Prop, P x → P y.

Lemma eq_refl : ∀ (X : Typ1) (x : X), eq X x x.
Proof fun X x P p ⇒ p.

Lemma eq_sym : ∀ (X : Typ1) (x y : X), eq X x y → eq X y x.
Proof fun X x y e ⇒ e (fun z ⇒ eq X z x) (eq_refl X x).

Lemma eq_trans :
 ∀ (X : Typ1) (x y z : X), eq X x y → eq X y z → eq X x z.
Proof fun X x y z e1 e2 P p ⇒ e2 P (e1 P p).

Some data structures

Option type

The option type (opt X) : Typ1 (parametrized by X : Typ1) that would be inductively defined in Coq by
Inductive opt X:Typ1 : Typ1 := | some : X->(opt X) | none : (opt X).
is mimicked by the following definitions:

Definition opt (X : Typ1) : Typ1 := (X → Prop) → Prop.
Definition some (X : Typ1) (x : X) : opt X := fun f ⇒ f x.
Definition none (X : Typ1) : opt X := fun _ ⇒ bot.

These definitions fulfill the expected properties of injectivity and non-confusion:

Lemma eq_some_some :
 ∀ (X : Typ1) (x1 x2 : X),
 eq (opt X) (some X x1) (some X x2) → eq X x1 x2.

Proof fun X x1 x2 e ⇒ e (fun z ⇒ z (fun x ⇒ eq X x1 x)) (eq_refl X x1).

Lemma eq_some_none :
 ∀ (X : Typ1) (x : X), eq (opt X) (some X x) (none X) → bot.

Proof fun X x e ⇒ e (fun z ⇒ z (fun _ ⇒ top)) top_intro.

Lemma eq_none_some :
 ∀ (X : Typ1) (x : X), eq (opt X) (none X) (some X x) → bot.

Proof
  fun X x e ⇒ e (fun z ⇒ z (fun _ ⇒ top) → bot) (fun p ⇒ p) top_intro.

On the other hand, the corresponding elimination scheme does not hold, due to the existence of inhabitants of the type (opt X) that are neither of the form (some X x) nor of the form (none X), such as the term f:X→Proptop : (opt X) for instance.
In practice, the existence of such parasitic elements will not pose a problem. When defining edge relations on data-types such as (opt X), we will simply ignore these extra elements so that they will become invisible up to a bisimulation.

Extended sum type

The (extended) sum type (sum X Y) : Typ1 (parametrized by the types X,Y : Typ1) that would be inductively defined in Coq by
Inductive sum X,Y:Typ1 : Typ1 := | inl : X->(sum X Y) (left injection) | inr : Y->(sum X Y) (right injection) | out : (sum X Y). (extra element)
is mimicked by the following definitions:

Definition sum (X Y : Typ1) : Typ1 := (X → Prop) → (Y → Prop) → Prop.
Definition inl (X Y : Typ1) (x : X) : sum X Y := fun f _ ⇒ f x.
Definition inr (X Y : Typ1) (y : Y) : sum X Y := fun _ g ⇒ g y.
Definition out (X Y : Typ1) : sum X Y := fun _ _ ⇒ bot.

Again, these definitions fulfill the expected properties of injectivity and non-confusion:

Lemma eq_inl_inl :
 ∀ (X Y : Typ1) (x1 x2 : X),
 eq (sum X Y) (inl X Y x1) (inl X Y x2) → eq X x1 x2.

Proof
  fun X Y x1 x2 e ⇒
  e (fun z ⇒ z (fun x ⇒ eq X x1 x) (fun _ ⇒ bot)) (eq_refl X x1).

Lemma eq_inr_inr :
 ∀ (X Y : Typ1) (y1 y2 : Y),
 eq (sum X Y) (inr X Y y1) (inr X Y y2) → eq Y y1 y2.

Proof
  fun X Y y1 y2 e ⇒
  e (fun z ⇒ z (fun _ ⇒ bot) (fun y ⇒ eq Y y1 y)) (eq_refl Y y1).

Lemma eq_inl_inr :
 ∀ (X Y : Typ1) (x : X) (y : Y),
 eq (sum X Y) (inl X Y x) (inr X Y y) → bot.

Proof fun X Y x y e ⇒ e (fun z ⇒ z (fun _ ⇒ top) (fun _ ⇒ bot)) top_intro.

Lemma eq_inr_inl :
 ∀ (X Y : Typ1) (x : X) (y : Y),
 eq (sum X Y) (inr X Y y) (inl X Y x) → bot.

Proof fun X Y x y e ⇒ e (fun z ⇒ z (fun _ ⇒ bot) (fun _ ⇒ top)) top_intro.

Lemma eq_inl_out :
 ∀ (X Y : Typ1) (x : X), eq (sum X Y) (inl X Y x) (out X Y) → bot.

Proof fun X Y x e ⇒ e (fun z ⇒ z (fun _ ⇒ top) (fun _ ⇒ top)) top_intro.

Lemma eq_out_inl :
 ∀ (X Y : Typ1) (x : X), eq (sum X Y) (out X Y) (inl X Y x) → bot.

Proof
  fun X Y x e ⇒
  e (fun z ⇒ z (fun _ ⇒ top) (fun _ ⇒ top) → bot) (fun p ⇒ p) top_intro.

Lemma eq_inr_out :
 ∀ (X Y : Typ1) (y : Y), eq (sum X Y) (inr X Y y) (out X Y) → bot.

Proof fun X Y y e ⇒ e (fun z ⇒ z (fun _ ⇒ top) (fun _ ⇒ top)) top_intro.

Lemma eq_out_inr :
 ∀ (X Y : Typ1) (y : Y), eq (sum X Y) (out X Y) (inr X Y y) → bot.

Proof
  fun X Y y e ⇒
  e (fun z ⇒ z (fun _ ⇒ top) (fun _ ⇒ top) → bot) (fun p ⇒ p) top_intro.

The corresponding elimination scheme does not hold here, for the same reason as for the option type (see above).