Commit 68be8091 authored by Gaspard Ferey's avatar Gaspard Ferey

Added notations.

parent 5c323e66
...@@ -125,6 +125,10 @@ where "t '≡' u ∈ Γ" := (InRelCtx Γ t u). ...@@ -125,6 +125,10 @@ where "t '≡' u ∈ Γ" := (InRelCtx Γ t u).
Definition Defined_var Γ v := exists T, v : T Γ. Definition Defined_var Γ v := exists T, v : T Γ.
Definition Fresh_var Γ v := ~ (Defined_var Γ v). Definition Fresh_var Γ v := ~ (Defined_var Γ v).
Notation "x '∈' Γ" := (Defined_var Γ x) (at level 90).
Notation "x '∉' Γ" := (Fresh_var Γ x) (at level 90).
(* ************ Locally nameless representation ************ *) (* ************ Locally nameless representation ************ *)
Fixpoint open_k (t u : term) (k : nat) := Fixpoint open_k (t u : term) (k : nat) :=
...@@ -287,8 +291,8 @@ Inductive typing : context -> term -> term -> Prop := ...@@ -287,8 +291,8 @@ Inductive typing : context -> term -> term -> Prop :=
where "Γ '⊢' t ':' A" := (typing Γ t A) where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop := with well_formed : context -> Prop :=
| WFEmpty : [ ] | WFEmpty : [ ]
| WFVarT : forall Γ x A, Fresh_var Γ x -> Γ A : type -> Γ, x : A | WFVarT : forall Γ x A, x Γ -> Γ A : type -> Γ, x : A
| WFVarK : forall Γ x A, Fresh_var Γ x -> Γ A : kind -> Γ, x : A | WFVarK : forall Γ x A, x Γ -> Γ A : kind -> Γ, x : A
| WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u | WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u
where "Γ ✓" := (well_formed Γ). where "Γ ✓" := (well_formed Γ).
...@@ -22,16 +22,17 @@ Proof. ...@@ -22,16 +22,17 @@ Proof.
Qed. Qed.
Reserved Notation "Γ '⊂' Γ'" (at level 80).
Inductive weaker : context -> context -> Prop := Inductive weaker : context -> context -> Prop :=
| WeakRefl : forall Γ , weaker Γ Γ | WeakRefl : forall Γ , Γ Γ
| WeakVarDecl : forall Γ x A, weaker Γ (Γ, x : A) | WeakVarDecl : forall Γ x A, Γ Γ, x : A
| WeakRulDecl : forall Γ t u, weaker Γ (Γ, t u) | WeakRulDecl : forall Γ t u, Γ Γ, t u
| WeakNextVarDecl : forall Γ Γ' x A, weaker Γ Γ' -> weaker (Γ, x : A) (Γ', x : A) | WeakNextVarDecl : forall Γ Γ' x A, Γ Γ' -> Γ, x : A Γ', x : A
| WeakNextRulDecl : forall Γ Γ' t u, weaker Γ Γ' -> weaker (Γ, t u) (Γ', t u). | WeakNextRulDecl : forall Γ Γ' t u, Γ Γ' -> Γ, t u Γ', t u
where "Γ '⊂' Γ'" := (weaker Γ Γ').
Theorem subset_var_decl : forall Γ Γ' x A, weaker Γ Γ' -> x : A Γ -> x : A Γ'. Theorem subset_var_decl : forall Γ Γ' x A, Γ Γ' -> x : A Γ -> x : A Γ'.
Proof. Proof.
intros. intros.
induction H. induction H.
...@@ -46,7 +47,7 @@ Proof. ...@@ -46,7 +47,7 @@ Proof.
subst. apply IAfterR. apply IHweaker. easy. subst. apply IAfterR. apply IHweaker. easy.
Qed. Qed.
Theorem subset_rul_decl : forall Γ Γ' t u, weaker Γ Γ' -> t u Γ -> t u Γ'. Theorem subset_rul_decl : forall Γ Γ' t u, Γ Γ' -> t u Γ -> t u Γ'.
Proof. Proof.
intros. intros.
induction H. induction H.
...@@ -62,13 +63,13 @@ Proof. ...@@ -62,13 +63,13 @@ Proof.
+ inversion HeqΓ2. subst. apply IRAfterR. apply IHweaker. easy. + inversion HeqΓ2. subst. apply IRAfterR. apply IHweaker. easy.
Qed. Qed.
Theorem fresh_vars_weaker : forall Γ Γ' x, weaker Γ Γ' -> Fresh_var Γ' x -> Fresh_var Γ x. Theorem fresh_vars_weaker : forall Γ Γ' x, Γ Γ' -> x Γ' -> x Γ.
Proof. Proof.
intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy. intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy.
Qed. Qed.
Theorem weak : forall Γ Γ' t u, Γ t : u -> weaker Γ Γ' -> Γ' -> Γ' t : u. Theorem weak : forall Γ Γ' t u, Γ t : u -> Γ Γ' -> Γ' -> Γ' t : u.
Proof. Proof.
intros. intros.
generalize dependent Γ'. generalize dependent Γ'.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment