CoqV6Beta.v

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

Require Export Main.
Require Export SortV6.

Section CoqV6Beta.

  Definition trm_v6 := (term srt_v6).
  Definition env_v6 := (env srt_v6).

  (* Construction du CTS *)

  Definition v6: (CTS_spec srt_v6) :=
    (Build_CTS_spec ? axiom_v6 rules_v6 univ_v6 (beta_rule ?)).

  (* Construction du PTS issu du CTS *)

  Definition v6_pts: (PTS_sub_spec srt_v6) := (cts_pts_functor ? v6).
  Definition le_type: (red_rule srt_v6) :=
                        (Rule ? (Le_type ? (pts_le_type ? v6_pts))).

  Definition typ_v6: env_v6 -> trm_v6 -> trm_v6 -> Prop := (typ ? v6_pts).
  Definition wft_v6: env_v6 -> trm_v6 -> Prop := (wf_type ? v6_pts).
  Definition wf_v6: env_v6 -> Prop := (wf ? v6_pts).
  Definition v6_sn := (sn srt_v6 (ctxt ? (Rule ? (head_reduct ? v6)))).

  Hints Unfold le_type typ_v6 wft_v6 wf_v6 v6_sn : pts.

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

  Lemma whnf: (e:env_v6)(t:trm_v6)(v6_sn e t)
                 ->{u:trm_v6 | (red ? (beta ?) e t u)
                               & (head_normal ? (beta ?) e u)}.
Proof (beta_whnf srt_v6).

  Lemma beta_conv_hnf: (e:env_v6)(x,y:trm_v6)(v6_sn e x)->(v6_sn e y)
         ->(decide (conv_hn_inv ? (beta_rule ?) e x y)).
Proof (CR_WHNF_convert_hn srt_v6 v6_sort_dec (beta_rule srt_v6)
         (church_rosser_red srt_v6) whnf).

  Theorem v6_is_subtype_dec: (subtype_dec_CTS ? v6).
Apply Build_subtype_dec_CTS.
Exact (church_rosser_red srt_v6).

Exact (beta_hn_sort srt_v6).

Exact (beta_hn_prod srt_v6).

Exact whnf.

Exact beta_conv_hnf.

Exact univ_v6_dec.
Save.

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

  Axiom v6_normalise: (e:env_v6)(t,T:trm_v6)(typ_v6 e t T)->(v6_sn e t).

  (* Subject-Reduction *)

  Lemma sound_v6_beta: (rule_sound ? v6_pts (beta ?)).
Unfold beta.
Simpl.
(Apply beta_sound; Auto with arith pts).
Simpl.
Apply cumul_inv_prod.
Exact v6_is_subtype_dec.
Save.

  Theorem v6_is_norm_sound: (norm_sound_CTS ? v6).
Proof (Build_norm_sound_CTS srt_v6 v6 sound_v6_beta v6_normalise).

  (* Construction du type-checker *)

  Theorem v6_algorithms: (PTS_TC ? v6_pts).
Unfold v6_pts.
Apply full_cts_type_checker;Simpl.
Exact v6_is_subtype_dec.

Exact v6_is_norm_sound.

Left.
Apply v6_inf_axiom.

Exact v6_inf_rule.

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

  (* open the type-checker *)

  Lemma infer_type: (e:env_v6)(t:trm_v6)(wf_v6 e)
                               -> (infer_ppal_type ? v6_pts e t).
Proof (ptc_inf_ppal_type ? ? v6_algorithms).

  Lemma check_wf_type: (e:env_v6)(t:trm_v6)(wf_v6 e)
                              ->(decide (wft_v6 e t)).
Proof (ptc_chk_wft ? ? v6_algorithms).

  Lemma check_type: (e:env_v6)(t,T:trm_v6)(wf_v6 e)
                                    ->(decide (typ_v6 e t T)).
Proof (ptc_chk_typ ? ? v6_algorithms).

  Lemma add_type: (e:env_v6)(t:trm_v6)(wf_v6 e)
                          ->(decide (wf_v6 (cons (Ax ? t) e))).
Proof (ptc_add_typ ? ? v6_algorithms).

  Lemma add_def: (e:env_v6)(t,T:trm_v6)(wf_v6 e)
                          ->(decide (wf_v6 (cons (Def ? t T) e))).
Proof (ptc_add_def ? ? v6_algorithms).

End CoqV6Beta.

23/12/98, 14:29