Library SN_CC_Real

Require Import Sat.
Require Import ZF ZFcoc ZFlambda.
Require GenRealSN.

Proving the SN model requirements

Module CCSN.

Types are coded by a carrier set X and a realizability relation R assigning a reducibility candidate to each element of the domain. This means that even non-computable functions have "realizers", but no closed ones (it is the set of neutral terms).

Definition mkTY X R := couple X (cc_lam X (fun x => iSAT (R x))).

Lemma mkTY_ext : ∀ X Y R R',
  X == Y ->
  (∀ x x', x ∈ X -> x == x' -> eqSAT (R x) (R' x')) ->
  mkTY X R == mkTY Y R'.

Definition El T := fst T.

Definition Real T x := sSAT (cc_app (snd T) x) .

Instance El_morph : morph1 El.

Instance Real_morph : Proper (eq_set ==>eq_set ==>eqSAT) Real.
Qed.

Lemma El_def : ∀ X R, El (mkTY X R) == X.

Lemma Real_def : ∀ x X R,
  (∀ x x', x ∈ X -> x == x' -> eqSAT (R x) (R x')) ->
  x ∈ X ->
  eqSAT (Real (mkTY X R) x) (R x).

The realizability relation of a dependent product of domain type A and co-domain family of types F for a function f: it is the intersection of all reducibility candidates {x}A -> {f(x)}F(x) when x ranges A. Note: {x}A -> {f(x)}F(x) is the set of that map any realizer of x (in A) to a realizer of f(x) (in F(x)). So the intersection of these sets when x ranges El(A) is the set of terms that realize f (in forall x:A. F(x)).

Definition piSAT A (F:set->set) (f:set->set) :=
  interSAT (fun p:{x|x ∈ El A } =>
    prodSAT (Real A (proj1_sig p)) (Real (F (proj1_sig p)) (f (proj1_sig p)))).

Lemma piSAT_morph : ∀ A B F F' f f',
  A == B ->
  eq_fun (El A) F F' ->
  eq_fun (El A) f f' ->
  eqSAT (piSAT A F f) (piSAT B F' f').

Definition prod A F :=
  mkTY (cc_prod (El A) (fun x => El (F x))) (fun f => piSAT A F (cc_app f)).

Lemma Real_prod : ∀ dom f F,
    eq_fun (El dom) F F ->
    f ∈ El (prod dom F) ->
    eqSAT (Real (prod dom F) f) (piSAT dom F (cc_app f)).

Definition lam A F := cc_lam (El A) F.

Definition app := cc_app.

Lemma prod_intro : ∀ dom f F,
  ext_fun (El dom) f ->
  ext_fun (El dom) F ->
  (∀ x, x ∈ El dom -> f x ∈ El (F x)) ->
  lam dom f ∈ El (prod dom F).

Lemma prod_elim : ∀ dom f x F,
  eq_fun (El dom) F F ->
  f ∈ El (prod dom F) ->
  x ∈ El dom ->
  cc_app f x ∈ El (F x).

The type of propositions:

propositions are types and do not interact with their surrounding context (they are neutral), so the set of realizers of any proposition is SN;
all propositions are non-empty (and have the same values as True), but their set of realizers must depend on the syntax of the propositions, because proofs compute. The realizer sets can be any reducibility candidate.

Remark: we cannot have that all propositions are equal (they can differ on the set of realizers). Otherwise True=(True->True) wold allow non normalizing terms (e.g. Y).

Injecting reducibility candidates into propositions

Definition mkProp S := mkTY (singl empty) (fun _ => S).

Instance mkProp_morph : Proper (eqSAT ==> eq_set) mkProp.
Qed.

Lemma El_mkProp : ∀ S, El (mkProp S) == singl empty.

Lemma Real_mkProp S x : x == empty -> eqSAT (Real (mkProp S) x) S.

The sort of propositions

Definition props :=
  mkTY

    (replSAT (fun S:SAT => mkProp S))

    (fun _ => snSAT).

Lemma El_props_def P :
  P ∈ El props <-> exists S, P == mkProp S.

  Lemma Real_sort : ∀ x, x ∈ El props -> eqSAT (Real props x) snSAT.

Lemma cc_impredicative_prod_non_empty : ∀ dom F,
  ext_fun dom F ->
  (∀ x, x ∈ dom -> F x == singl prf_trm) ->
  cc_prod dom F == singl prf_trm.

Lemma impredicative_prod : ∀ dom F,
  ext_fun (El dom) F ->
  (∀ x, x ∈ El dom -> F x ∈ El props) ->
  prod dom F ∈ El props.

  Definition daimon := prf_trm.
  Lemma daimon_false : prf_trm ∈ El (prod props (fun P => P)).

Definition X:=set.
Definition eqX := eq_set.
Definition eqX_equiv := eq_set_equiv.
Definition inX x y := x ∈ El y.
Instance in_ext : Proper (eq_set ==>eq_set ==>iff) inX.
Qed.

Definition eq_fun (x:X) (f1 f2:X->X) :=
  ∀ y1 y2, y1 ∈ El x -> y1 == y2 -> f1 y1 == f2 y2.

Lemma lam_ext :
  ∀ 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 :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  prod x1 f1 == prod x2 f2.

Lemma beta_eq:
  ∀ dom F x,
  eq_fun dom F F ->
  x ∈ El dom ->
  app (lam dom F) x == F x.

End CCSN.
Import CCSN.

Building the generic model

Module SN := GenRealSN.MakeModel CCSN CCSN.
Import SN.

Module Lc := Lambda.

Consistency out of the strong normalization model

If t belongs to all reducibility candidates, then it has a free variable

Lemma neutral_not_closed :
∀ t, (∀ S, inSAT t S) -> exists k, Lc.occur k t.

Another consistency proof.

What is original is that it is based on the strong normalization model which precisely inhabits all types and propositions. We get out of this by noticing that non provable propositions contain no closed realizers. So, by a substitutivity invariant (realizers of terms typed in the empty context cannot introduce free variables), we derive the impossibility to derive absurdity in the empty context.

The result is at the level of the model. See below for the proof that the actual syntax (libraries Term and TypeJudge) can be mapped to the model.

Theorem consistency : ∀ M, ~ typ List.nil M (Prod prop (Ref 0)).

Print Assumptions consistency.

Strong Normalization on actual syntax

Require TypeJudge.

Module Ty := TypeJudge.
Module Tm := Term.

Fixpoint int_trm t :=
  match t with
  | Tm.Srt Tm.prop => SN.prop
  | Tm.Srt Tm.kind => SN.kind
  | Tm.Ref n => SN.Ref n
  | Tm.App u v => SN.App (int_trm u) (int_trm v)
  | Tm.Abs T M => SN.Abs (int_trm T) (int_trm M)
  | Tm.Prod T U => SN.Prod (int_trm T) (int_trm U)
  end.
Definition interp t := int_trm (Ty.unmark_app t).
Definition int_env := List.map interp.

Section LiftAndSubstEquiv.

Import SN.

Lemma int_lift_rec : ∀ n t k,
  eq_trm (lift_rec n k (int_trm t)) (int_trm (Tm.lift_rec n t k)).

Lemma int_lift : ∀ n t,
  eq_trm (int_trm (Tm.lift n t)) (lift n (int_trm t)).

Lemma int_subst_rec : ∀ arg,
  int_trm arg <> kind ->
  ∀ t k,
  eq_trm (subst_rec (int_trm arg) k (int_trm t)) (int_trm (Tm.subst_rec arg t k)).

Lemma int_subst : ∀ u t,
  int_trm u <> kind ->
  eq_trm (int_trm (Tm.subst u t)) (subst (int_trm u) (int_trm t)).

Lemma int_not_kind : ∀ T, T <> Tm.Srt Tm.kind -> interp T <> kind.

End LiftAndSubstEquiv.

Hint Resolve int_not_kind Ty.eq_typ_not_kind.

Proof that beta-reduction at the Lc level simulates beta-reduction at the Tm level. One beta at the Tm level may require several (but not zero) steps at the Lc level, because of the encoding of type-carrying lambda abstractions.

Lemma red1_sound : ∀ x y,
  Tm.red1 x y -> ~ Tm.mem_sort Tm.kind x ->
  SN.red_term (int_trm x) (int_trm y).

Import Wellfounded.

Lemma sn_sound : ∀ M,
  Acc (transp _ red_term) (interp M) ->
  ~ Tm.mem_sort Tm.kind (Ty.unmark_app M) ->
  Tm.sn (Ty.unmark_app M).

Soundness of the typing rules

Lemma int_sound : ∀ e M M' T,
  Ty.eq_typ e M M' T ->
  SN.typ (int_env e) (interp M) (interp T) /\
  SN.eq_typ (int_env e) (interp M) (interp M').

  Lemma interp_wf : ∀ e, Ty.wf e -> SN.wf (int_env e).

Lemma interp_sound : ∀ e M M' T,
  Ty.eq_typ e M M' T ->
  SN.wf (int_env e) /\ SN.typ (int_env e) (interp M) (interp T).

The main theorem: strong normalization

Theorem strong_normalization : ∀ e M M' T,
Ty.eq_typ e M M' T ->
Tm.sn (Ty.unmark_app M).

Print the assumptions made to derive strong normalization of CC: the axioms of ZF. (In fact we don't need full replacement, only the functional version, so we should be able to have the SN theorem without assumption.)

Print Assumptions strong_normalization.