

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

Require Export Main.
Require Export SortV6.

Section CoqV6.

  (* Definition des composantes du calcul *)

  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_delta_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))).

  Hint 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 :
   forall (e : env_v6) (t : trm_v6),
   v6_sn e t ->
   {u : trm_v6 | red _ (beta_delta _) e t u & 
   head_normal _ (beta_delta _) e u}.
Proof beta_delta_whnf srt_v6.


  Lemma bd_conv_hnf :
   forall (e : env_v6) (x y : trm_v6),
   v6_sn e x -> v6_sn e y -> decide (conv_hn_inv _ (beta_delta_rule _) e x y).
Proof
  CR_WHNF_convert_hn srt_v6 v6_sort_dec (beta_delta_rule srt_v6)
    (church_rosser_beta_delta srt_v6) whnf.


  Theorem v6_is_subtype_dec : subtype_dec_CTS _ v6.
(* Goal: subtype_dec_CTS srt_v6 v6 *)
apply Build_subtype_dec_CTS.
(* Goal: church_rosser srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) *)
(* Goal: forall (e : env srt_v6) (s : srt_v6), head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e (Srt srt_v6 s) *)
(* Goal: forall (e : env srt_v6) (A B : term srt_v6), head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e (Prod srt_v6 A B) *)
(* Goal: forall (e : env srt_v6) (t : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e t), @sig2 (term srt_v6) (fun u : term srt_v6 => red srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e t u) (fun u : term srt_v6 => head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e u) *)
(* Goal: forall (e : env srt_v6) (x y : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e x) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e y), decide (conv_hn_inv srt_v6 (head_reduct srt_v6 v6) e x y) *)
(* Goal: forall s s' : srt_v6, decide (clos_refl_trans srt_v6 (universes srt_v6 v6) s s') *)
exact (church_rosser_beta_delta srt_v6).

(* Goal: forall (e : env srt_v6) (s : srt_v6), head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e (Srt srt_v6 s) *)
(* Goal: forall (e : env srt_v6) (A B : term srt_v6), head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e (Prod srt_v6 A B) *)
(* Goal: forall (e : env srt_v6) (t : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e t), @sig2 (term srt_v6) (fun u : term srt_v6 => red srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e t u) (fun u : term srt_v6 => head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e u) *)
(* Goal: forall (e : env srt_v6) (x y : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e x) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e y), decide (conv_hn_inv srt_v6 (head_reduct srt_v6 v6) e x y) *)
(* Goal: forall s s' : srt_v6, decide (clos_refl_trans srt_v6 (universes srt_v6 v6) s s') *)
exact (bd_hn_sort srt_v6).

(* Goal: forall (e : env srt_v6) (A B : term srt_v6), head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e (Prod srt_v6 A B) *)
(* Goal: forall (e : env srt_v6) (t : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e t), @sig2 (term srt_v6) (fun u : term srt_v6 => red srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e t u) (fun u : term srt_v6 => head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e u) *)
(* Goal: forall (e : env srt_v6) (x y : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e x) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e y), decide (conv_hn_inv srt_v6 (head_reduct srt_v6 v6) e x y) *)
(* Goal: forall s s' : srt_v6, decide (clos_refl_trans srt_v6 (universes srt_v6 v6) s s') *)
exact (bd_hn_prod srt_v6).

(* Goal: forall (e : env srt_v6) (t : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e t), @sig2 (term srt_v6) (fun u : term srt_v6 => red srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e t u) (fun u : term srt_v6 => head_normal srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6)) e u) *)
(* Goal: forall (e : env srt_v6) (x y : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e x) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e y), decide (conv_hn_inv srt_v6 (head_reduct srt_v6 v6) e x y) *)
(* Goal: forall s s' : srt_v6, decide (clos_refl_trans srt_v6 (universes srt_v6 v6) s s') *)
exact whnf.

(* Goal: forall (e : env srt_v6) (x y : term srt_v6) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e x) (_ : sn srt_v6 (ctxt srt_v6 (Rule srt_v6 (head_reduct srt_v6 v6))) e y), decide (conv_hn_inv srt_v6 (head_reduct srt_v6 v6) e x y) *)
(* Goal: forall s s' : srt_v6, decide (clos_refl_trans srt_v6 (universes srt_v6 v6) s s') *)
exact bd_conv_hnf.

(* Goal: forall s s' : srt_v6, decide (clos_refl_trans srt_v6 (universes srt_v6 v6) s s') *)
exact univ_v6_dec.
Qed.




  (* Subject-Reduction *)

  Lemma sound_v6_bd : rule_sound _ v6_pts (beta_delta _).
(* Goal: rule_sound srt_v6 v6_pts (beta_delta srt_v6) *)
unfold beta_delta in |- *.
(* Goal: product_inversion srt_v6 (Rule srt_v6 (Le_type srt_v6 (pts_le_type srt_v6 v6_pts))) *)
(* Goal: rule_sound srt_v6 v6_pts (delta srt_v6) *)
simpl in |- *.
(* Goal: rule_sound srt_v6 v6_pts (reunion srt_v6 (beta srt_v6) (delta srt_v6)) *)
apply union_sound.
(* Goal: rule_sound srt_v6 v6_pts (beta srt_v6) *)
(* Goal: rule_sound srt_v6 v6_pts (delta srt_v6) *)
apply beta_sound; auto with arith pts.
(* Goal: product_inversion srt_v6 (Rule srt_v6 (Le_type srt_v6 (pts_le_type srt_v6 v6_pts))) *)
(* Goal: rule_sound srt_v6 v6_pts (delta srt_v6) *)
simpl in |- *.
(* Goal: product_inversion srt_v6 (R_rt srt_v6 (cumul srt_v6 v6)) *)
(* Goal: rule_sound srt_v6 v6_pts (delta srt_v6) *)
apply cumul_inv_prod.
(* Goal: subtype_dec_CTS srt_v6 v6 *)
(* Goal: rule_sound srt_v6 v6_pts (delta srt_v6) *)
exact v6_is_subtype_dec.

(* Goal: rule_sound srt_v6 v6_pts (delta srt_v6) *)
apply delta_sound.
Qed.


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

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



  Lemma v6_is_norm_sound : norm_sound_CTS _ v6.
Proof.
(* Goal: norm_sound_CTS srt_v6 v6 *)
refine (Build_norm_sound_CTS srt_v6 v6 sound_v6_bd v6_normalise _ _ _).
(* Goal: forall s : srt_v6, @ppal_dec srt_v6 (cts_axiom srt_v6 v6 s) (clos_refl_trans srt_v6 (universes srt_v6 v6)) *)
(* Goal: forall x1 x2 : srt_v6, @sig2 srt_v6 (fun x3 : srt_v6 => cts_rules srt_v6 v6 x1 x2 x3) (fun x3 : srt_v6 => forall (s1 s2 s3 : srt_v6) (_ : cts_rules srt_v6 v6 s1 s2 s3) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) x1 s1) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) x2 s2), clos_refl_trans srt_v6 (universes srt_v6 v6) x3 s3) *)
(* Goal: forall (s1 s2 : srt_v6) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) s1 s2) (_ : typed_sort srt_v6 (cts_axiom srt_v6 v6) s2), typed_sort srt_v6 (cts_axiom srt_v6 v6) s1 *)
left.
(* Goal: @sig srt_v6 (fun x : srt_v6 => @ppal srt_v6 (cts_axiom srt_v6 v6 s) (clos_refl_trans srt_v6 (universes srt_v6 v6)) x) *)
(* Goal: forall x1 x2 : srt_v6, @sig2 srt_v6 (fun x3 : srt_v6 => cts_rules srt_v6 v6 x1 x2 x3) (fun x3 : srt_v6 => forall (s1 s2 s3 : srt_v6) (_ : cts_rules srt_v6 v6 s1 s2 s3) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) x1 s1) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) x2 s2), clos_refl_trans srt_v6 (universes srt_v6 v6) x3 s3) *)
(* Goal: forall (s1 s2 : srt_v6) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) s1 s2) (_ : typed_sort srt_v6 (cts_axiom srt_v6 v6) s2), typed_sort srt_v6 (cts_axiom srt_v6 v6) s1 *)
apply v6_inf_axiom.

(* Goal: forall x1 x2 : srt_v6, @sig2 srt_v6 (fun x3 : srt_v6 => cts_rules srt_v6 v6 x1 x2 x3) (fun x3 : srt_v6 => forall (s1 s2 s3 : srt_v6) (_ : cts_rules srt_v6 v6 s1 s2 s3) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) x1 s1) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) x2 s2), clos_refl_trans srt_v6 (universes srt_v6 v6) x3 s3) *)
(* Goal: forall (s1 s2 : srt_v6) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) s1 s2) (_ : typed_sort srt_v6 (cts_axiom srt_v6 v6) s2), typed_sort srt_v6 (cts_axiom srt_v6 v6) s1 *)
exact v6_inf_rule.

(* Goal: forall (s1 s2 : srt_v6) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) s1 s2) (_ : typed_sort srt_v6 (cts_axiom srt_v6 v6) s2), typed_sort srt_v6 (cts_axiom srt_v6 v6) s1 *)
intros.
(* Goal: forall (s1 s2 : srt_v6) (_ : clos_refl_trans srt_v6 (universes srt_v6 v6) s1 s2) (_ : typed_sort srt_v6 (cts_axiom srt_v6 v6) s2), typed_sort srt_v6 (cts_axiom srt_v6 v6) s1 *)
elim v6_inf_axiom with s1; intros.
(* Goal: typed_sort srt_v6 (cts_axiom srt_v6 v6) s1 *)
split with x.
(* Goal: cts_axiom srt_v6 v6 s1 x *)
apply (pp_ok p).
Qed.


  (* Construction du type-checker *)

  Theorem v6_algorithms : PTS_TC _ v6_pts.
  Proof full_cts_type_checker srt_v6 v6 v6_is_subtype_dec v6_is_norm_sound.


  (* open the type-checker *)

  Lemma infer_type :
   forall (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 :
   forall (e : env_v6) (t : trm_v6), wf_v6 e -> wft_dec _ v6_pts e t.
Proof ptc_chk_wft _ _ v6_algorithms.


  Lemma check_type :
   forall (e : env_v6) (t T : trm_v6), wf_v6 e -> check_dec _ v6_pts e t T.
Proof ptc_chk_typ _ _ v6_algorithms.


  Lemma add_type :
   forall (e : env_v6) (t : trm_v6), wf_v6 e -> decl_dec _ v6_pts e (Ax _ t).
Proof ptc_add_typ _ _ v6_algorithms.


  Lemma add_def :
   forall (e : env_v6) (t T : trm_v6),
   wf_v6 e -> decl_dec _ v6_pts e (Def _ t T).
Proof ptc_add_def _ _ v6_algorithms.

End CoqV6.