# Library Icharate.Kernel.natDed

Set Implicit Arguments.
Require Export basics.

Section Main.
Variables
I
J
A
W
: Set.

Variables (eqdecI :eqdec I)
(eqdecJ :eqdec J).

Variable R : extension I J.

Inductive natded : context I J A W -> Form I J A -> Set :=
| Wd : forall r F, natded (res r F) F
| SlashI :
forall (Gamma:context I J A W) (F G:Form I J A) (i:I) n,
natded (Comma i Gamma (res (hyp n) G)) F ->
natded Gamma (Slash i F G)
| BackI :
forall (Gamma:context I J A W) (F G:Form I J A) (i:I) n,
natded (Comma i (res (hyp n) G) Gamma) F ->
natded Gamma (Backslash i G F)
| DotI :
forall (Gamma Delta:context I J A W) (F G:Form I J A) (i:I),
natded Gamma F ->
natded Delta G ->
natded (Comma i Gamma Delta) (Dot i F G)
| DiamI :
forall (Gamma:context I J A W) (F:Form I J A) (j:J),
natded Gamma F ->
natded (TDiamond j Gamma) (Diamond j F)
| BoxI :
forall (Gamma:context I J A W) (F:Form I J A) (i:J),
natded (TDiamond i Gamma) F ->
natded Gamma (Box i F)
| SlashE :
forall (Gamma Delta:context I J A W) (F G:Form I J A) (i:I),
natded Gamma (Slash i F G) ->
natded Delta G ->
natded (Comma i Gamma Delta) F
| BackE :
forall (Gamma Delta:context I J A W) (F G:Form I J A) (i:I),
natded Gamma G ->
natded Delta (Backslash i G F) ->
natded (Comma i Gamma Delta) F
| DotE :
forall (Gamma Gamma': context I J A W)(Delta:context I J A W)
(F G H:Form I J A) (i:I) n p,
replace
(Comma i (res (hyp n) F) (res (hyp p) G)) Delta Gamma Gamma' ->
natded Delta (Dot i F G) ->
natded Gamma H -> natded Gamma' H
| DiamE :
forall (Gamma Gamma' Delta:context I J A W) (F G:Form I J A) (j:J) n,
replace (TDiamond j (res (hyp n) F)) Delta Gamma Gamma' ->
natded Delta (Diamond j F) ->
natded Gamma G -> natded Gamma' G
| BoxE :
forall (Gamma:context I J A W) (F:Form I J A) (j:J),
natded Gamma (Box j F) ->
natded (TDiamond j Gamma) F
| StructRule :
forall (Gamma Gamma' T1 T2:context I J A W) (F:Form I J A) Ru,
in_extension Ru R ->
struct_replace eqdecI eqdecJ Ru T1 T2 Gamma Gamma' ->
natded Gamma' F -> natded Gamma F.

Definition XStructRule : forall (Gamma Gamma' T1 T2:context I J A W) (F:Form I J A) Ru,
struct_replace eqdecI eqdecJ Ru T1 T2 Gamma Gamma' ->
in_extension Ru R ->
natded Gamma' F ->
natded Gamma F.
intros; eapply StructRule;eauto.
Defined.

Definition Structrule' :
forall (ZGamma : zcontext I J A W)(T1 T2:context I J A W) (F:Form I J A) Ru,
in_extension Ru R ->
apply_rule Ru eqdecI eqdecJ T2 = Some T1 ->
natded (zfill ZGamma T1) F ->
natded (zfill ZGamma T2) F.
intros.
eapply StructRule.
eexact H.
eapply struct_replace_as_zfill.
eexact H0.
trivial.
Defined.

Definition XStructrule' :
forall (ZGamma : zcontext I J A W)(T1 T2:context I J A W) (F:Form I J A) Ru,
apply_rule Ru eqdecI eqdecJ T2 = Some T1 ->
in_extension Ru R ->
natded (zfill ZGamma T1) F ->
natded (zfill ZGamma T2) F.
intros;eapply Structrule';eauto.
Defined.

Definition DotE' : forall (ZGamma : zcontext I J A W)(Delta:context I J A W)
(F G H:Form I J A) (i:I) n p,
natded Delta (Dot i F G) ->
natded (zfill ZGamma (Comma i (res (hyp n) F) (res (hyp p) G))) H ->
natded (zfill ZGamma Delta) H.
intros.
eapply DotE;eauto with ctl_db.
Defined.

Definition DiamondE' :
forall (ZGamma : zcontext I J A W)(Delta:context I J A W) (F G:Form I J A) (j:J) n,
natded Delta (Diamond j F) ->
natded (zfill ZGamma (TDiamond j (res (hyp n) F))) G ->
natded (zfill ZGamma Delta) G.
intros; eapply DiamE;eauto with ctl_db.
Defined.

End Main.

Definition natded0 (I J A:Set) decI decJ e (bGamma:bcontext I J A )(F:Form I J A) :=
forall W Gamma, matches (W:=W) bGamma Gamma -> natded decI decJ e Gamma F.

Hint Resolve in_extension_rule in_extension_right.
Hint Resolve form_matches comma_matches diam_matches.

Notation "Gamma '{' eqdecI eqdecJ ext '}' '|--' F" :=(natded eqdecI eqdecJ ext Gamma F) (at level 30):mmg_scope.