Library Proofs_Progress

Proof of the Progress Property


Require Import Calculus.
Require Import List.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Proofs_AdmissibilityOfTransitivity.
Module My_Proofs_AdmissibilityOfTransitivity := Proofs_AdmissibilityOfTransitivity.SetProgram(My_Program).

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.

Lemma lemmaA29_aux_1:
  forall (f: FieldSym) (fvs: FieldValueList),
    (In f (fields_of_fieldValueList fvs)) ->
    exists v: Value,
      (FieldValueList_contains fvs f v)
.

Definition params_evaluated (xts: ParamTermList): Prop :=
  exists xvs: (list (ParamSym * Value)),
    (paramValueList_to_ParamTermList xvs) = xts
.

Definition fields_evaluated (fts: FieldTermList): Prop :=
  exists fvs: FieldValueList,
    (fieldValueList_to_fieldTermList fvs) = fts
.

Definition lemmaA29_aux_2_prop1 (t: Term): Prop :=
    (term_evaluated t) \/ ~(term_evaluated t)
.

Definition lemmaA29_aux_2_prop2 (fts: FieldTermList): Prop :=
    (fields_evaluated fts) \/ ~(fields_evaluated fts)
.

Definition lemmaA29_aux_2_prop3 (xts: ParamTermList): Prop :=
    (params_evaluated xts) \/ ~(params_evaluated xts)
.

Lemma lemmaA29_aux_2:
  forall (t: Term),
    (term_evaluated t) \/ ~(term_evaluated t)
.

Lemma lemmaA29_aux_3:
  forall (xts: ParamTermList),
    (params_evaluated xts) \/ ~(params_evaluated xts)
.

Definition lemmaA29_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
  G = rootEnv ->
  ~(term_evaluated t) ->
  exists u: Term, (Red_term t u)
.

Definition lemmaA29_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList) (H: (ParamTermListTyping G p m xts)): Prop :=
  G = rootEnv ->
  ~(params_evaluated xts) ->
  exists xts': ParamTermList, (Red_paramTermList xts xts')
.

Definition lemmaA29_prop3 (G: Env) (C: ClassSym) (fts: FieldTermList) (H: (FieldTermListTyping G C fts)): Prop :=
  G = rootEnv ->
  ~(fields_evaluated fts) ->
  exists fts': FieldTermList, (Red_fieldTermList fts fts')
.

Progress
Lemma lemmaA29:
  forall (t: Term) (T: type),
    (Typing rootEnv t T) ->
    ~(term_evaluated t) ->
    exists u: Term, (Red_term t u)
.

End SetProgram.

Index
This page has been generated by coqdoc