Commit 78ab7ede authored by Gaspard Ferey's avatar Gaspard Ferey

Split dev into modules.

parent f9d960cc
......@@ -160,217 +160,3 @@ with well_formed : context -> Prop :=
| 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 Γ).
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.
exact (IHΓ H5 H8).
- inversion H. subst.
inversion H0 ; subst.
+ exists s,A,Γ.
split. apply H5.
split. apply H6. apply H4.
+exact (IHΓ H7 H10).
Qed.
Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A t →β u -> Γ t →β u.
Proof.
intros.
induction H; econstructor.
Qed.
Lemma context_var_conv_Γ2 : forall Γ x A t u, Γ, x : A t →Γ u -> Γ t →Γ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H.
destruct H ; inversion HeqΓ0.
- subst. econstructor. easy.
Qed.
Lemma context_var_conv_β : forall Γ x A t u, Γ, x : A t ↪β u -> Γ t ↪β u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H; rewrite HeqΓ0 in H.
- econstructor. induction H. econstructor.
- apply CCApp1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCApp2. apply (context_var_conv_β2 Γ x A). easy.
- apply CCAbs1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCAbs2. apply (context_var_conv_β2 Γ x A). easy.
- apply CCPi1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCPi2. apply (context_var_conv_β2 Γ x A). easy.
Qed.
Lemma context_var_conv_Γ : forall Γ x A t u, Γ, x : A t ↪Γ u -> Γ t ↪Γ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H; rewrite HeqΓ0 in H.
- econstructor. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCApp1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCApp2. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCAbs1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCAbs2. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCPi1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCPi2. apply (context_var_conv_Γ2 Γ x A). easy.
Qed.
Lemma context_var_conv_βΓ : forall Γ x A t u, Γ, x : A t ↪βΓ u -> Γ t ↪βΓ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
destruct H.
- left ; eapply context_var_conv_β ; now rewrite <- HeqΓ0.
- right ; eapply context_var_conv_Γ ; now rewrite <- HeqΓ0.
Qed.
Lemma context_var_conv : forall Γ x A t u, Γ, x : A t u -> Γ t u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H.
- econstructor.
- eapply CVSym ; now eapply IHRSTClosure.
- eapply CVTrans ; [eapply IHRSTClosure1 | eapply IHRSTClosure2] ; easy.
- eapply CVRule ; eapply context_var_conv_βΓ ; now rewrite <- HeqΓ0.
Qed.
Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False.
Proof.
induction Γ ; intros.
- inversion H0.
- inversion H0 ; subst.
+ inversion H ; subst. inversion H3 ; subst. eapply no_type_kind ; eassumption.
+ inversion H ; subst ; eapply IHΓ ; eassumption.
- inversion H0 ; subst ; inversion H ; subst ; eapply IHΓ ; eassumption.
Qed.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ, kind t -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma not_rel_kind_gamma_right : forall Γ t, Γ, t kind -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma rel_kind_in_left : forall Γ t, Γ -> kind t Γ -> False.
Proof.
intros Γ.
induction Γ ; intros u Γwf H.
- inversion H.
- eapply IHΓ ; inversion H ; subst.
+ now inversion Γwf.
+ eassumption.
- inversion H ; subst.
+ eapply not_rel_kind_gamma_left ; eassumption.
+ eapply IHΓ.
* now inversion Γwf.
* eassumption.
Qed.
Lemma rel_kind_in_right : forall Γ t, Γ -> t kind Γ -> False.
Proof.
intros Γ.
induction Γ ; intros u Γwf H.
- inversion H.
- eapply IHΓ ; inversion H ; subst.
+ now inversion Γwf.
+ eassumption.
- inversion H ; subst.
+ eapply not_rel_kind_gamma_right ; eassumption.
+ eapply IHΓ.
* now inversion Γwf.
* eassumption.
Qed.
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 inhabit_kind : forall Γ t, Γ -> Γ t : kind -> of_typed_kind t.
Proof.
intros.
remember kind as x.
induction H0 ; subst.
- exfalso ; eapply not_var_kind_gamma ; eassumption.
- constructor.
- assert (Γ, x : A ).
constructor ; eassumption.
pose proof (IHtyping2 H0 eq_refl).
now constructor.
- inversion Heqx.
-
Lemma inverse_kind : forall Γ t, Γ -> forall u, Γ u t -> u = kind <-> t = kind.
Proof.
intros.
induction H0.
- easy.
- split ; intro.
apply IHConv2 ; now apply IHConv1.
apply IHConv1 ; now apply IHConv2.
- split ; intro ; now apply IHConv.
- split ; intro.
+ inversion H0.
+ (* FALSE because t and u might not be typable *) admit.
- inversion H0 ; split ; intro ; subst.
+ exfalso ; eapply not_rel_kind_gamma_left ; eassumption.
+ exfalso ; eapply not_rel_kind_gamma_right ; eassumption.
+ exfalso ; eapply rel_kind_in_left.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_right.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_left.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_right.
* inversion H ; subst ; eassumption.
* eassumption.
- split. admit. (* a better definition of context is needed here *)
Admitted.
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.
pose proof (inverse_kind Γ B H3 kind H1).
now apply H2.
Qed.
*)
\ No newline at end of file
Require Import LPTerm.
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 ; 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.
exact (IHΓ H5 H8).
- inversion H. subst.
inversion H0 ; subst.
+ exists s,A,Γ.
split. apply H5.
split. apply H6. apply H4.
+exact (IHΓ H7 H10).
Qed.
Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A t →β u -> Γ t →β u.
Proof.
intros. induction H; econstructor.
Qed.
Lemma context_var_conv_Γ2 : forall Γ x A t u, Γ, x : A t →Γ u -> Γ t →Γ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H. rewrite HeqΓ0 in H.
inversion H. subst. econstructor. easy.
Qed.
Lemma context_var_conv_β : forall Γ x A t u, Γ, x : A t ↪β u -> Γ t ↪β u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H; rewrite HeqΓ0 in H.
- econstructor. induction H. econstructor.
- apply CCApp1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCApp2. apply (context_var_conv_β2 Γ x A). easy.
- apply CCAbs1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCAbs2. apply (context_var_conv_β2 Γ x A). easy.
- apply CCPi1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCPi2. apply (context_var_conv_β2 Γ x A). easy.
Qed.
Lemma context_var_conv_Γ : forall Γ x A t u, Γ, x : A t ↪Γ u -> Γ t ↪Γ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H; rewrite HeqΓ0 in H.
- econstructor. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCApp1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCApp2. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCAbs1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCAbs2. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCPi1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCPi2. apply (context_var_conv_Γ2 Γ x A). easy.
Qed.
Lemma context_var_conv_βΓ : forall Γ x A t u, Γ, x : A t ↪βΓ u -> Γ t ↪βΓ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
destruct H.
- left ; eapply context_var_conv_β ; now rewrite <- HeqΓ0.
- right ; eapply context_var_conv_Γ ; now rewrite <- HeqΓ0.
Qed.
Lemma context_var_conv : forall Γ x A t u, Γ, x : A t u -> Γ t u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H.
- econstructor.
- eapply CVSym ; now eapply IHRSTClosure.
- eapply CVTrans ; [eapply IHRSTClosure1 | eapply IHRSTClosure2] ; easy.
- eapply CVRule ; eapply context_var_conv_βΓ ; now rewrite <- HeqΓ0.
Qed.
Require Import LPTerm.
Require Import conversion.
Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False.
Proof.
induction Γ ; intros.
- inversion H0.
- inversion H0 ; subst.
+ inversion H ; subst. inversion H3 ; subst. eapply no_type_kind ; eassumption.
+ inversion H ; subst ; eapply IHΓ ; eassumption.
- inversion H0 ; subst ; inversion H ; subst ; eapply IHΓ ; eassumption.
Qed.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ, kind t -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma not_rel_kind_gamma_right : forall Γ t, Γ, t kind -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma rel_kind_in_left : forall Γ t, Γ -> kind t Γ -> False.
Proof.
intros Γ.
induction Γ ; intros u Γwf H.
- inversion H.
- eapply IHΓ ; inversion H ; subst.
+ now inversion Γwf.
+ eassumption.
- inversion H ; subst.
+ eapply not_rel_kind_gamma_left ; eassumption.
+ eapply IHΓ.
* now inversion Γwf.
* eassumption.
Qed.
Lemma rel_kind_in_right : forall Γ t, Γ -> t kind Γ -> False.
Proof.
intros Γ.
induction Γ ; intros u Γwf H.
- inversion H.
- eapply IHΓ ; inversion H ; subst.
+ now inversion Γwf.
+ eassumption.
- inversion H ; subst.
+ eapply not_rel_kind_gamma_right ; eassumption.
+ eapply IHΓ.
* now inversion Γwf.
* eassumption.
Qed.
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 inhabit_kind : forall Γ t, Γ -> Γ t : kind -> of_typed_kind t.
Proof.
intros.
remember kind as x.
induction H0 ; subst.
- exfalso ; eapply not_var_kind_gamma ; eassumption.
- constructor.
- assert (Γ, x : A ).
constructor ; eassumption.
pose proof (IHtyping2 H0 eq_refl).
now constructor.
- inversion Heqx.
-
Lemma inverse_kind : forall Γ t, Γ -> forall u, Γ u t -> u = kind <-> t = kind.
Proof.
intros.
induction H0.
- easy.
- split ; intro.
apply IHConv2 ; now apply IHConv1.
apply IHConv1 ; now apply IHConv2.
- split ; intro ; now apply IHConv.
- split ; intro.
+ inversion H0.
+ (* FALSE because t and u might not be typable *) admit.
- inversion H0 ; split ; intro ; subst.
+ exfalso ; eapply not_rel_kind_gamma_left ; eassumption.
+ exfalso ; eapply not_rel_kind_gamma_right ; eassumption.
+ exfalso ; eapply rel_kind_in_left.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_right.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_left.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_right.
* inversion H ; subst ; eassumption.
* eassumption.
- split. admit. (* a better definition of context is needed here *)
Admitted.
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.
pose proof (inverse_kind Γ B H3 kind H1).
now apply H2.
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