ECC.v

Require Bool.
Require Arith.
Require Compare_dec.
Require Peano_dec.
Require General.
Require MyList.
Require MyRelations.

Require Export Main.
Require Export SortECC.

Section ECC.

  Definition trm_ecc := (term srt_ecc).
  Definition env_ecc := (env srt_ecc).

  (* Construction du CTS *)

  Definition ecc: (CTS_spec srt_ecc) :=
    (Build_CTS_spec ? axiom_ecc rules_ecc univ_ecc (beta_delta_rule ?)).

  (* Construction du PTS issu du CTS *)

  Definition ecc_pts: (PTS_sub_spec srt_ecc) := (cts_pts_functor ? ecc).
  Definition le_type: (red_rule srt_ecc) :=
                        (Rule ? (Le_type ? (pts_le_type ? ecc_pts))).

  Definition typ_ecc: env_ecc -> trm_ecc -> trm_ecc -> Prop := (typ ? ecc_pts).
  Definition wft_ecc: env_ecc -> trm_ecc -> Prop := (wf_type ? ecc_pts).
  Definition wf_ecc: env_ecc -> Prop := (wf ? ecc_pts).
  Definition ecc_sn := (sn srt_ecc (ctxt ? (Rule ? (head_reduct ? ecc)))).

  Hints Unfold le_type typ_ecc wft_ecc wf_ecc ecc_sn : pts.

  (* Algorithme de mise en forme normale de tete      Decidabilite du sous-typage pour les types bien formes *)

  Lemma whnf: (e:env_ecc)(t:trm_ecc)(ecc_sn e t)
                 ->{u:trm_ecc | (red ? (beta_delta ?) e t u)
                               & (head_normal ? (beta_delta ?) e u)}.
Proof (beta_delta_whnf srt_ecc).

  Lemma bd_conv_hnf: (e:env_ecc)(x,y:trm_ecc)(ecc_sn e x)->(ecc_sn e y)
         ->(decide (conv_hn_inv ? (beta_delta_rule ?) e x y)).
Proof (CR_WHNF_convert_hn srt_ecc ecc_sort_dec (beta_delta_rule srt_ecc)
         (church_rosser_beta_delta srt_ecc) whnf).

  Theorem ecc_is_subtype_dec: (subtype_dec_CTS ? ecc).
Apply Build_subtype_dec_CTS.
Exact (church_rosser_beta_delta srt_ecc).

Exact (bd_hn_sort srt_ecc).

Exact (bd_hn_prod srt_ecc).

Exact whnf.

Exact bd_conv_hnf.

Exact univ_ecc_dec.
Save.

  (* L'axiome:  ECC est fortement normalisant *)

  Axiom ecc_normalise: (e:env_ecc)(t,T:trm_ecc)(typ_ecc e t T)->(ecc_sn e t).

  (* Subject-Reduction *)

  Lemma sound_ecc_bd: (rule_sound ? ecc_pts (beta_delta ?)).
Unfold beta_delta .
Simpl.
Unfold union .
Apply union_sound.
(Apply beta_sound; Auto with arith pts).
Simpl.
Apply cumul_inv_prod.
Exact ecc_is_subtype_dec.

Apply delta_sound.
Save.

  Theorem ecc_is_norm_sound: (norm_sound_CTS ? ecc).
Proof (Build_norm_sound_CTS srt_ecc ecc sound_ecc_bd ecc_normalise).

  (* Construction du type-checker *)

  Theorem ecc_algorithms: (PTS_TC ? ecc_pts).
Unfold ecc_pts.
Apply full_cts_type_checker.
Exact ecc_is_subtype_dec.

Exact ecc_is_norm_sound.

Left.
Apply ecc_inf_axiom.

Exact ecc_inf_rule.

Intros.
(Elim ecc_inf_axiom with s1; Intros).
Split with x.
Apply (pp_ok y).
Save.

  (* open the type-checker *)

  Lemma infer_type: (e:env_ecc)(t:trm_ecc)(wf_ecc e)
                               -> (infer_ppal_type ? ecc_pts e t).
Proof (ptc_inf_ppal_type ? ? ecc_algorithms).

  Lemma check_wf_type: (e:env_ecc)(t:trm_ecc)(wf_ecc e)
                              ->(decide (wft_ecc e t)).
Proof (ptc_chk_wft ? ? ecc_algorithms).

  Lemma check_type: (e:env_ecc)(t,T:trm_ecc)(wf_ecc e)
                                    ->(decide (typ_ecc e t T)).
Proof (ptc_chk_typ ? ? ecc_algorithms).

  Lemma add_type: (e:env_ecc)(t:trm_ecc)(wf_ecc e)
                          ->(decide (wf_ecc (cons (Ax ? t) e))).
Proof (ptc_add_typ ? ? ecc_algorithms).

  Lemma add_def: (e:env_ecc)(t,T:trm_ecc)(wf_ecc e)
                          ->(decide (wf_ecc (cons (Def ? t T) e))).
Proof (ptc_add_def ? ? ecc_algorithms).

End ECC.

23/12/98, 14:29