Commit 89a5c94f authored by François Thiré's avatar François Thiré

Add LN stuff

parent 6f0828e8
......@@ -5,6 +5,8 @@
- Try a localy nameless representation, but not implemented
*)
Require Import PeanoNat.
Parameter Var : Set.
Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.
......@@ -61,17 +63,59 @@ Reserved Notation "Γ '⊢' t ':' A" (at level 45, t at level 55, A at level 55)
Reserved Notation "Γ ✓" (at level 100).
Reserved Notation "Γ ⊧ t '≡' u" (at level 50, t at level 45).
Definition substk (t u : term) (k : nat) : term := t. (* TODO *)
Fixpoint open_k (t u : term) (k : nat) :=
match t with
| TBound i =>
if Nat.eq_dec k i then
u
else
t
| TFree n => t
| TSort _ => t
| TApp l r => TApp (open_k l u k) (open_k r u k)
| TAbs ty te => TAbs (open_k ty u k) (open_k te u (S k))
| TPi ty te => TPi (open_k ty u k) (open_k te u (S k))
end.
Definition open (t u : term) := open_k t u 0.
Fixpoint subst_k (t u : term) (z : Var) : term :=
match t with
| TBound i => t
| TFree x =>
if var_dec x z then
u
else
t
| TSort _ => t
| TApp l r => TApp (subst_k l u z) (subst_k r u z)
| TAbs ty te => TAbs (subst_k ty u z) (subst_k ty u z)
| TPi ty te => TPi (subst_k ty u z) (subst_k ty u z)
end.
Fixpoint close_k (t : term) (k : nat) (z : Var) : term :=
match t with
| TBound i => t
| TFree x =>
if var_dec x z then
TBound k
else
t
| TSort _ => t
| TApp l r => TApp (close_k l k z) (close_k r k z)
| TAbs ty te => TAbs (close_k ty k z) (close_k ty (S k) z)
| TPi ty te => TAbs (close_k ty k z) (close_k ty (S k) z)
end.
Inductive Conv (Γ: context) : term -> term -> Prop :=
| CVRefl : forall t, Conv Γ t t
| CVTrans : forall t u v, Conv Γ t u -> Conv Γ u v -> Conv Γ t v
| CVSym : forall t u, Conv Γ t u -> Conv Γ u t
| CVBeta : forall A t u, Conv Γ ((λ A ~ t) @ u) (substk t u 0)
| CVBeta : forall A t u, Conv Γ ((λ A ~ t) @ u) (open_k t u 0)
| CVRel : forall t u, t u Γ -> Conv Γ t u
| CVCtx : forall t u f, Conv Γ t u -> Conv Γ (f t) (f u).
Notation "t '[' k '<-' u ']'" := (substk t u k) (at level 40, u at level 20).
Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 40, u at level 20).
Notation "Γ ⊧ t '≡' u" := (Conv Γ t u).
......@@ -89,6 +133,8 @@ with well_formed : context -> Prop :=
| WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ ; t u
where "Γ ✓" := (well_formed Γ).
Lemma no_type_kind : forall Γ A, Γ kind : A -> False.
Proof.
intros.
......@@ -191,34 +237,6 @@ Inductive of_typed_kind : term -> Prop :=
| IKType : of_typed_kind type
| IKPiType : forall A B, of_typed_kind B -> of_typed_kind (Π A ~ B).
(*
Lemma exchange : forall Γ x A y B t C, Γ, x : A -> Γ, y : B -> Γ, x : A, y : B t : C -> Γ, y : B, x : A t : C.
Proof.
intros.
induction H1.
- constructor.
+ constructor.
Lemma weakening : forall Γ x A t B, Γ, x : A -> Γ t : B -> Γ, x : A t : B.
Proof.
intros.
induction H0.
- constructor.
+ easy.
+ now constructor.
- now constructor.
- econstructor.
apply IHtyping1.
apply H.
*)
Lemma pi_is_sort : forall Γ A B t, Γ -> Γ t : Π A ~ B -> exists s, Γ Π A ~ B : s.
Proof.
intros.
induction H0.
- exists type.
inversion H1 ; subst.
inversion H ; subst.
Lemma inhabit_kind : forall Γ t, Γ -> Γ t : kind -> of_typed_kind t.
......@@ -248,7 +266,7 @@ Proof.
- split ; intro ; now apply IHConv.
- split ; intro.
+ inversion H0.
+ (* STUCK! Not provable... *)
+ (* STUCK! Not provable... *) admit.
- inversion H0 ; split ; intro ; subst.
+ exfalso ; eapply not_rel_kind_gamma_left ; eassumption.
+ exfalso ; eapply not_rel_kind_gamma_right ; eassumption.
......
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