Library Proofs_Soundness

Proof of Type Safety

Require Import Calculus.
Require Import Arith.
Require Import MatchCompNat.
Require Import List.
Require Import Relations.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Proofs_SubjectReduction.
Module My_Proofs_SubjectReduction := Proofs_SubjectReduction.SetProgram(My_Program).

Import My_Proofs_SubjectReduction.
Import My_Proofs_SubstitutionLemmas3.
Import My_Proofs_SubstitutionLemmas2.
Import My_Proofs_SubstitutionLemmas.
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.

Reflexive transitive closure of the reduction relation
Definition Red_term_star :=
  (clos_refl_trans _ Red_term)

Multi-step subject reduction
Lemma lemmaA41:
  forall (T: type) (t u: Term),
    (Typing rootEnv t T) ->
    (Red_term_star t u) ->
    (Typing rootEnv u T)

Lemma lemmaA42:
  forall (t: Term),
    (Red_term_star main t) ->
    (term_evaluated t) \/ (exists u: Term, (Red_term t u))

End SetProgram.

This page has been generated by coqdoc