Paweł Wieczorek avatar Paweł Wieczorek committed 8c3b955

quick fix

Comments (0)

Files changed (3)

 Nbe/Model/LogRelTm_ClosedUnderPer.v
 Nbe/Model/LogRelTm_Lift.v
 Nbe/Model/LogRelTm_Back.v
+Nbe/Model/LogRelTm.v
 Nbe/Model/LogRelSb_Def.v
 Nbe/Model/LogRelSb_BasicFacts.v
+Nbe/Model/LogRelSb_Fundamental_Helpers.v
 Nbe/Model/LogRelSb_Fundamental.v
 Nbe/Model/LogRelSb_Id.v
 Nbe/Model/LogRelSb.v
   Nbe/Model/LogRelTm_ClosedUnderPer.v\
   Nbe/Model/LogRelTm_Lift.v\
   Nbe/Model/LogRelTm_Back.v\
+  Nbe/Model/LogRelTm.v\
   Nbe/Model/LogRelSb_Def.v\
   Nbe/Model/LogRelSb_BasicFacts.v\
+  Nbe/Model/LogRelSb_Fundamental_Helpers.v\
   Nbe/Model/LogRelSb_Fundamental.v\
   Nbe/Model/LogRelSb_Id.v\
   Nbe/Model/LogRelSb.v\

Nbe/Model/LogRelSb_Def.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.
+
+(*****************************************************************************)
+(*****************************************************************************)
+(*****************************************************************************)
+(******************************************************************************
+ * Relations for substitutions
+ *)
+
+Reserved Notation "Gamma ||- [ s ] : Delta #aeq# env"
+ (no associativity, at level 75, A, X, t, d at next level).
+
+
+Inductive RelSb : Cxt -> Sb -> Cxt -> DEnv -> Prop :=
+  | RelSb_Sid: forall Gamma sb,
+    Gamma |-- [ sb ] : nil ->
+    Gamma ||- [ sb ] : nil #aeq# Did
+
+ |  RelSb_Sext: forall Gamma Delta A M SB sb denv dM DX DX' (HDX : DX === DX' #in# PerType) PX,
+   Gamma ||- [ sb ] : Delta #aeq# denv ->
+   Gamma ||- TmSb A sb #in# HDX ->
+   Gamma ||- M : TmSb A sb #aeq# dM #in# HDX ->
+   Gamma |-- [ SB ] === [Sext sb M ] : Delta,,A ->
+   [denv] === [denv] #in# Delta ->
+   EvalTm A denv DX ->
+   Interp DX PX ->
+   dM === dM #in# PX ->
+   Gamma ||- [ SB ] : Delta,,A #aeq# Dext denv dM
+    
+where "Gamma ||- [ s ] : Delta #aeq# denv" := (RelSb Gamma s Delta denv)
+.
+Hint Constructors RelSb.
+
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.