Commit a195aa7d authored by François Thiré's avatar François Thiré

Stuck to an easy inversion proof

parent 420ba9fc
......@@ -40,37 +40,130 @@ Inductive context : Set :=
Notation "Γ ',' x ':' A" := (CVar x A Γ) (at level 40, x at level 40).
Notation "[ ]" := CEmpty (at level 80).
Notation "Γ ';' t '≡' u" := (CRel t u Γ) (at level 40).
Notation "Γ ';' t '≡' u" := (CRel t u Γ) (at level 40, t at level 55).
Reserved Notation "x ':' A '∈' Γ" (at level 60).
Reserved Notation "t '≡' u '∈' Γ" (at level 70).
Inductive InCtx : context -> Var -> term -> Prop :=
| Now : forall Γ x A, x : A (Γ , x : A)
| After : forall Γ A x y B, x : A Γ -> x : A (Γ, y : B)
| INow : forall Γ x A, x : A (Γ , x : A)
| IAfterV : forall Γ A x y B, x : A Γ -> x : A (Γ, y : B)
| IAfterR : forall Γ A x t u, x : A Γ -> x : A (Γ ; t u)
where "x ':' A ∈ Γ" := (InCtx Γ x A).
Inductive InRelCtx : context -> term -> term -> Prop :=
| IRNow : forall Γ t u, t u (Γ ; t u)
| IRAfterV : forall Γ t u y B, t u Γ -> t u (Γ, y : B)
| IRAfterR : forall Γ t u v w, t u Γ -> t u (Γ ; v w)
where "t '≡' u ∈ Γ" := (InRelCtx Γ t u).
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).
Inductive Beta : term -> term -> Prop := .
Inductive Conv (Γ: context) : term -> term -> Prop := .
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 t u, Beta t u -> Conv Γ t u
| CVRel : forall t u, t u Γ -> Conv Γ t u
| CVCtx : forall t u f, Conv Γ t u -> Conv Γ (f t) (f u).
Definition substk (t u : term) (k : nat) : term := t. (* TODO *)
Notation "t '[' k '<-' u ']'" := (substk t u k) (at level 40, u at level 20).
Notation "Γ ⊧ t '≡' u" := (Conv Γ t u) (at level 50).
Notation "Γ ⊧ t '≡' u" := (Conv Γ t u).
Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ -> x : A Γ -> Γ (# x) : A
| TyType : forall Γ, Γ type : kind
| TyType : forall Γ, Γ -> Γ type : kind
| TyPi : forall Γ A B s x, Γ A : type -> Γ, x : A B : s -> Γ Π A ~ B : s
| TyAbs : forall Γ x A B t s, Γ A : type -> Γ, x : A B : s ->
Γ, x : A t : B -> Γ λ A ~ t : Π A ~ B
| TyAbs : forall Γ x A B t s, Γ A : type -> Γ, x : A B : s -> Γ, x : A t : B -> Γ λ A ~ t : Π A ~ B
| 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 t u, Γ A : type -> Γ t : A -> Γ u : A -> Γ -> Γ ; t u
| 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.
remember kind as x.
induction H ; try inversion Heqx.
apply IHtyping1.
easy.
Qed.
Lemma inversion_typing : forall Γ t A, Γ t : A -> Γ .
Proof.
intros.
induction H ; try easy.
Qed.
Lemma inversion_rel : forall Γ t u, Γ -> t u Γ -> exists s A Δ, Δ t : A /\ Δ u : A /\ Δ A : s.
Proof.
intros.
induction Γ.
- inversion H0.
- inversion H ; subst.
inversion H0 ; subst.
pose proof (IHΓ H5 H8).
destruct H1 as [s [A [Δ]]].
exists s,A,Δ.
apply H1.
- inversion H ; subst.
inversion H0 ; subst.
+ exists s,A,Γ.
now split.
+pose proof (IHΓ H7 H10).
destruct H1 as [s0 [A0 [Δ0]]].
exists s0,A0,Δ0.
apply H1.
Qed.
Lemma empty_conv : forall t u, ([ ]) t u -> t = u.
Proof.
intros.
induction H ; subst ; try easy.
Qed.
Lemma context_var_conv : forall Γ x A t u, Γ, x : A t u -> Γ t u.
Proof.
intros ; induction H.
- apply CVRefl.
- eapply CVTrans ; eassumption.
- now apply CVSym.
- now eapply CVBeta.
- apply CVRel.
inversion H ; now subst.
- now apply CVCtx.
Qed.
Lemma inverse_kind : forall Γ t, Γ -> Γ kind t -> t = kind.
Proof.
intros Γ.
induction Γ ; intros.
- inversion H0 ; subst ; try apply empty_conv in H0 ; try easy. rewrite H1,H0 ; easy.
- apply IHΓ.
+ now inversion H.
+ eapply context_var_conv ; eassumption.
- (* TODO: harder than expected *)
Lemma type_kind : forall Γ A, Γ type : A -> A = kind.
Proof.
intros.
remember type as x.
induction H ; try inversion Heqx.
- easy.
- apply IHtyping1 in H2.
pose proof (inversion_typing Γ t A H).
subst.
now apply (inverse_kind Γ B H3 H1).
Qed.
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