Library ModelHF

Require Import Bool List.
Require Import HFcoc.
Require Import Models GenModelSyntax.

Module HF_Coc_Model <: CC_Model.

Definition X := hf.
Definition inX := In_hf.
Definition eqX := Eq_hf.
Definition eqX_equiv : Equivalence Eq_hf.
Qed.

Notation "x \in y" := (inX x y) (at level 60).
Notation "x == y" := (eqX x y) (at level 70).

Lemma in_ext: Proper (eqX ==> eqX ==> iff) inX.
Definition props := props.
Definition app := cc_app.
Definition lam := cc_lam.
Definition prod := 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: Proper (eqX ==> eqX ==> eqX) app.
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 HF_Coc_Model.

Module Soundness := GenModelSyntax.MakeModel(HF_Coc_Model).

Import Soundness.
Import T.

Fixpoint forall_int_env (e:Env.env) (f:(nat->hf)->bool) {struct e} : bool :=
  match e with
    nil => f (fun _ => empty)
  | T::e' => forall_int_env e'
      (fun i_f => forall_elt (fun x => f (V.cons x i_f)) (int (int_trm T) i_f))
  end.

Definition valid_context (e:Env.env) : bool :=
  negb (forall_int_env e (fun _ => false)).


Require Import Term TypeJudge.

Definition int_clos T := int (int_trm T) vnil.

  Lemma cc_consistency : forall M M', ~ eq_typ nil M M' FALSE.

Eval vm_compute in (int_clos FALSE).
Eval vm_compute in (int_clos TRUE).
Eval vm_compute in (int_clos INAT). Eval vm_compute in (int_clos EM). Eval vm_compute in (int_clos PI). Eval vm_compute in (int_clos (EXT prop prop)).