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)

.

Soundness


Lemma lemmaA42:

  forall (t: Term),

    (Red_term_star main t) ->

    (term_evaluated t) \/ (exists u: Term, (Red_term t u))

.




End SetProgram.

Index

This page has been generated by coqdoc