Library ModelZF
Require Import Models GenModelSyntax.
Require Import ZF ZFcoc.
Import IZF.
Module CCM <: CC_Model.
Definition X := set.
Definition inX : X -> X -> Prop := in_set.
Definition eqX : X -> X -> Prop := eq_set.
Definition eqX_equiv : Equivalence eqX := eq_set_equiv.
Notation "x \in y" := (inX x y) (at level 60).
Notation "x == y" := (eqX x y) (at level 70).
Lemma in_ext:
forall x1 x2 : X, x1 == x2 ->
forall x3 x4 : X, x3 == x4 ->
(x1 \in x3 <-> x2 \in x4).
Definition props : X := props.
Definition app : X -> X -> X := cc_app.
Definition lam : X -> (X -> X) -> X := cc_lam.
Definition prod : X -> (X -> X) -> X := cc_prod.
Definition eq_fun (x:X) (f1 f2:X->X) :=
forall y1 y2, y1 \in x -> y1 == y2 -> f1 y1 == f2 y2.
Lemma lam_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_fun x1 f1 f2 ->
lam x1 f1 == lam x2 f2.
Lemma app_ext:
forall x1 x2 : X, x1 == x2 ->
forall x3 x4 : X, x3 == x4 ->
app x1 x3 == app x2 x4.
Lemma prod_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_fun x1 f1 f2 ->
prod x1 f1 == prod x2 f2.
Lemma prod_intro : forall dom f F,
eq_fun dom f f ->
eq_fun dom F F ->
(forall x, x \in dom -> f x \in F x) ->
lam dom f \in prod dom F.
Lemma prod_elim : forall dom f x F,
eq_fun dom F F ->
f \in prod dom F ->
x \in dom ->
app f x \in F x.
Lemma impredicative_prod : forall dom F,
eq_fun dom F F ->
(forall x, x \in dom -> F x \in props) ->
prod dom F \in props.
Lemma beta_eq:
forall dom F x,
eq_fun dom F F ->
x \in dom ->
app (lam dom F) x == F x.
End CCM.
Module BuildModel := MakeModel(CCM).
Require Import Term Env.
Require Import TypeJudge.
Load "template/Library.v".
Lemma cc_consistency : forall M M', ~ eq_typ nil M M' FALSE.
Require Import ZF ZFcoc.
Import IZF.
Module CCM <: CC_Model.
Definition X := set.
Definition inX : X -> X -> Prop := in_set.
Definition eqX : X -> X -> Prop := eq_set.
Definition eqX_equiv : Equivalence eqX := eq_set_equiv.
Notation "x \in y" := (inX x y) (at level 60).
Notation "x == y" := (eqX x y) (at level 70).
Lemma in_ext:
forall x1 x2 : X, x1 == x2 ->
forall x3 x4 : X, x3 == x4 ->
(x1 \in x3 <-> x2 \in x4).
Definition props : X := props.
Definition app : X -> X -> X := cc_app.
Definition lam : X -> (X -> X) -> X := cc_lam.
Definition prod : X -> (X -> X) -> X := cc_prod.
Definition eq_fun (x:X) (f1 f2:X->X) :=
forall y1 y2, y1 \in x -> y1 == y2 -> f1 y1 == f2 y2.
Lemma lam_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_fun x1 f1 f2 ->
lam x1 f1 == lam x2 f2.
Lemma app_ext:
forall x1 x2 : X, x1 == x2 ->
forall x3 x4 : X, x3 == x4 ->
app x1 x3 == app x2 x4.
Lemma prod_ext :
forall x1 x2 f1 f2,
x1 == x2 ->
eq_fun x1 f1 f2 ->
prod x1 f1 == prod x2 f2.
Lemma prod_intro : forall dom f F,
eq_fun dom f f ->
eq_fun dom F F ->
(forall x, x \in dom -> f x \in F x) ->
lam dom f \in prod dom F.
Lemma prod_elim : forall dom f x F,
eq_fun dom F F ->
f \in prod dom F ->
x \in dom ->
app f x \in F x.
Lemma impredicative_prod : forall dom F,
eq_fun dom F F ->
(forall x, x \in dom -> F x \in props) ->
prod dom F \in props.
Lemma beta_eq:
forall dom F x,
eq_fun dom F F ->
x \in dom ->
app (lam dom F) x == F x.
End CCM.
Module BuildModel := MakeModel(CCM).
Require Import Term Env.
Require Import TypeJudge.
Load "template/Library.v".
Lemma cc_consistency : forall M M', ~ eq_typ nil M M' FALSE.