Commit ab487d8b authored by Gaspard Ferey's avatar Gaspard Ferey

CHanged a little bit the conversion type.

parent 7d61aa26
......@@ -107,17 +107,8 @@ Fixpoint close_k (t : term) (k : nat) (z : Var) : term :=
| 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) (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 ']'" := (open_k t u k) (at level 40, u at level 20).
Notation "Γ ⊧ t '≡' u" := (Conv Γ t u).
Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ -> x : A Γ -> Γ (# x) : A
......@@ -132,12 +123,22 @@ Inductive typing : context -> term -> term -> Prop :=
| TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ t @ u : B [0 <- u]
| TyConv : forall Γ t A B s, Γ t : A -> Γ B : s -> Γ A B -> Γ t : B
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
| WFEmpty : [ ]
| WFVar : forall Γ x A, Γ A : type -> Γ -> Γ , x : A
| WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ ; t u
where "Γ ✓" := (well_formed Γ).
where "Γ ✓" := (well_formed Γ)
with 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 T s, Γ (λ A ~ t) @ u : T -> Γ T : s -> 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)
(* CVCtx should be split into all different cases of term constructors. *)
where "Γ ⊧ t '≡' u" := (Conv Γ t u).
Lemma no_type_kind : forall Γ A, Γ kind : A -> False.
......
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