Library Proofs_SubstitutionLemmas

Proofs about Substitution for the Current Instance


Require Import Calculus.
Require Import Arith.
Require Import MatchCompNat.
Require Import Util.
Require Import List.
Require Import ListSet.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Proofs_DeBruijnSIndices.
Module My_Proofs_DeBruijnSIndices := Proofs_DeBruijnSIndices.SetProgram(My_Program).

Import My_Proofs_DeBruijnSIndices.
Import My_Proofs_Progress.
Import My_Proofs_AdmissibilityOfTransitivity.
Import My_Proofs_Subclassing.
Import My_Proofs_TypeOrdering.
Import My_Proofs_Miscellaneous.
Import My_WellFormedness.
Import My_Semantics.
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.

Predicate: P is true for all elements of the list xs
Fixpoint list_forall (A: Set) (xs: (list A)) (P: A -> Prop) {struct xs}: Prop :=
  match xs with
    | nil => True
    | x :: xs' => (P x) /\ (list_forall A xs' P)
  end
.

Lemma listForall_is_forall:
  forall (A: Set) (xs: (list A)) (P: A -> Prop),
    (list_forall A xs P) -> (forall (x: A), (In x xs) -> (P x))
.

Lemma forall_is_listForall:
  forall (A: Set) (xs: (list A)) (P: A -> Prop),
    (forall (x: A), (In x xs) -> (P x)) -> (list_forall A xs P)
.

Predicate: for all i in 0,|Ts|-1, for all k in fv(Ts_i), k < i

Fixpoint local_types_well_formed_aux (Ts: TypeList) (i: nat) {struct Ts}: Prop :=
  match Ts with
    | nil => True
    | T :: Ts' =>
      (forall (k: VarSym), (var_in_type k T) -> (k < i)) /\
      (local_types_well_formed_aux Ts' (S i))
  end
.

Definition local_types_well_formed (Ts: TypeList): Prop :=
  (local_types_well_formed_aux Ts 0)
.

Well-formed contexts
Inductive context_is_well_formed: Env -> Prop :=

  | context_is_well_formed_intro:
    forall (O: Owner) (xTs: ParamTypeList) (Ts: TypeList),
    (list_forall _ xTs (fun xT => let (x, T) := xT in (fp_in_type T) = empty_paramset)) ->
    (local_types_well_formed Ts) ->
    (context_is_well_formed (Env_mk O xTs Ts))
.

Definition lemmaA40_aux_4_prop1 (v: Value): Prop :=
  forall (G: Env) (T: type),
    (Gen_PathTyping G (Path_value v) T) ->
    (Typing G (value_to_term v) T)
.

Definition lemmaA40_aux_4_prop2 (fvs: FieldValueList): Prop :=
  forall (G: Env) (C: ClassSym),
    (Gen_FieldValueListTyping G C fvs) ->
    (FieldTermListTyping G C (fieldValueList_to_fieldTermList fvs))
.

Lemma lemmaA40_aux_4:
  forall (G: Env) (v: Value) (T: type),
    (Gen_PathTyping G (Path_value v) T) ->
    (Typing G (value_to_term v) T)
.
rewrite temp_lemma. trivial.
apply H. trivial.
rewrite temp_lemma. trivial. trivial.
red. intros. simpl.
apply FieldTermListTyping_nil.
red. intros. simpl.
rename f0 into fvs.
inversion_clear H1.
eapply FieldTermListTyping_cons.
apply H. apply H2. trivial. apply H4. trivial.
apply H0. trivial.
Qed.

Definition lemmaA40_aux_8_prop1 (v: Value): Prop :=
  forall (G: Env) (T: type),
    (Typing G (value_to_term v) T) ->
    (Gen_PathTyping G (Path_value v) T)
.

Definition lemmaA40_aux_8_prop2 (fvs: FieldValueList): Prop :=
  forall (G: Env) (C: ClassSym),
    (FieldTermListTyping G C (fieldValueList_to_fieldTermList fvs)) ->
    (Gen_FieldValueListTyping G C fvs)
.

Lemma lemmaA40_aux_8:
  forall (G: Env) (v: Value) (T: type),
    (Typing G (value_to_term v) T) ->
    (Gen_PathTyping G (Path_value v) T)
.
rewrite temp_lemma1 in H1. trivial.
apply H. trivial.
rewrite temp_lemma1 in H3. trivial. trivial.
red. intros. simpl.
apply Gen_FieldValueListTyping_nil.
red. intros. simpl.
rename f0 into fvs.
inversion_clear H1.
eapply Gen_FieldValueListTyping_cons.
apply H. apply H2. trivial. apply H4. trivial.
apply H0. trivial.
Qed.

Lemma lemmaA40_aux_9:
  forall (G: Env) (p: Path) (T: type),
    (Gen_PathTyping G p T) ->
    (Typing G (path_to_term p) T)
.

Lemma lemmaA40_aux_10:
  forall (G: Env) (p: Path) (T: type),
    (Typing G (path_to_term p) T) ->
    (Gen_PathTyping G p T)
.

Definition lemmaA38_0_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
  forall (xTs: ParamTypeList) (Ts Us: TypeList),
    G = (Env_mk Owner_root nil Ts) ->
    (Gen_PathTyping (Env_mk Owner_root xTs (app Us Ts)) p T)
.

Definition lemmaA38_0_prop2 (G: Env) (C: ClassSym) (fvs: FieldValueList) (H: (Gen_FieldValueListTyping G C fvs)): Prop :=
  forall (xTs: ParamTypeList) (Ts Us: TypeList),
    G = (Env_mk Owner_root nil Ts) ->
    (Gen_FieldValueListTyping (Env_mk Owner_root xTs (app Us Ts)) C fvs)
.

Definition lemmaA38_0_prop3 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
  forall (xTs: ParamTypeList) (Ts Us: TypeList),
    G = (Env_mk Owner_root nil Ts) ->
    (Gen_Subtyping (Env_mk Owner_root xTs (app Us Ts)) T U)
.

Lemma lemmaA38_0:
  forall (xTs: ParamTypeList) (Ts Us: TypeList) (p: Path) (T: type),
    (Gen_PathTyping (Env_mk Owner_root nil Ts) p T) ->
    (Gen_PathTyping (Env_mk Owner_root xTs (app Us Ts)) p T)
.

Lemma lemmaA38_2:
  forall (xTs: ParamTypeList) (Ts Us: TypeList) (T U: type),
    (Gen_Subtyping (Env_mk Owner_root nil Ts) T U) ->
    (Gen_Subtyping (Env_mk Owner_root xTs (app Us Ts)) T U)
.

Lemma lemmaA38_0_corollary:
  forall (xTs: ParamTypeList) (Ts: TypeList) (p: Path) (T: type),
    (Gen_PathTyping rootEnv p T) ->
    (Gen_PathTyping (Env_mk Owner_root xTs Ts) p T)
.

Substitution for this in a list of types
Definition thisSubst_in_typeList (Ts: TypeList) (p: Path): TypeList :=
  (map (fun T => (thisSubst_in_type T p)) Ts)
.

Substitution for this in a list of bindings (Param * Type)
Definition thisSubst_in_paramTypeList (xTs: ParamTypeList) (p: Path): ParamTypeList :=
  (map (fun xT => match xT with (x, T) => (x, (thisSubst_in_type T p)) end) xTs)
.
Lemma lemmaA1_for_paths:
  forall (G: Env) (p: Path) (T U: type),
    (Gen_PathTyping G p T) ->
    (Gen_Subtyping G T U) ->
    (Gen_PathTyping G p U)
.

Definition lemmaA39_this_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
    G = (Env_mk (Owner_class C) xTs Us) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Gen_PathTyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_path p (Path_value v)) (thisSubst_in_type T (Path_value v))
      )
.

Definition lemmaA39_this_prop2 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
    G = (Env_mk (Owner_class C) xTs Us) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Gen_Subtyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))
      )
.

Definition lemmaA39_this_prop3 (G: Env) (A: ClassSym) (fvs: FieldValueList) (H: (Gen_FieldValueListTyping G A fvs)): Prop :=
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
    G = (Env_mk (Owner_class C) xTs Us) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Gen_FieldValueListTyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        A fvs
      )
.

Lemma lemmaA39_this_main:
  forall (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)),
    (lemmaA39_this_prop1 G p T H)
.

Subtitution lemmas -- path
Lemma lemmaA39_this_0:
    forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList) (p: Path) (T: type),
    (Gen_PathTyping (Env_mk (Owner_class C) xTs Us) p T) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Gen_PathTyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_path p (Path_value v)) (thisSubst_in_type T (Path_value v))
      )
.

Subtitution lemmas -- type
Lemma lemmaA39_this_2:
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList) (T U: type),
    (Gen_Subtyping (Env_mk (Owner_class C) xTs Us) T U) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Gen_Subtyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))
      )
.

Definition lemmaA39_this1_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
    G = (Env_mk (Owner_class C) xTs Us) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Typing
        (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v))
        (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_term t (Path_value v)) (thisSubst_in_type T (Path_value v))
      )
.

Definition lemmaA39_this1_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList)
  (H: (ParamTermListTyping G p m xts)): Prop :=
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
    G = (Env_mk (Owner_class C) xTs Us) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (ParamTermListTyping
        (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_path p (Path_value v))
        m
        (thisSubst_in_paramTermList xts (Path_value v))
      )
.

Definition lemmaA39_this1_prop3 (G: Env) (A: ClassSym) (fts: FieldTermList)
  (H: (FieldTermListTyping G A fts)): Prop :=
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
    G = (Env_mk (Owner_class C) xTs Us) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (FieldTermListTyping
        (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        A
        (thisSubst_in_fieldTermList fts (Path_value v))
      )
.

Lemma lemmaA39_this1_aux_1:
  forall (xts: ParamTermList) (p: Path),
    (params_of_paramTermList (thisSubst_in_paramTermList xts p)) =
    (params_of_paramTermList xts)
.

Lemma lemmaA39_this1_aux_2:
  forall (fts: FieldTermList) (p: Path),
    (fields_of_fieldTermList (thisSubst_in_fieldTermList fts p)) =
    (fields_of_fieldTermList fts)
.

Subtitution lemmas -- term
Lemma lemmaA39_this_1:
  forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList) (t: Term) (T: type),
    (Typing (Env_mk (Owner_class C) xTs Us) t T) ->
    forall (v: Value),
      (Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
      (Typing
        (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
        (thisSubst_in_term t (Path_value v))
        (thisSubst_in_type T (Path_value v))
      )
.

End SetProgram.

Index
This page has been generated by coqdoc