Commit 02d12cca authored by François Thiré's avatar François Thiré

WIP: Inversion lemma for Pi

parent 4c1f59b0
......@@ -34,35 +34,60 @@ Proof.
+ right. now apply IHt2.
Qed.
Theorem left_arr_type : forall Γ t u AB, Γ t ~> u : AB -> exists A, Γ t : A.
Proof.
intros.
remember (t ~> u) as w.
induction H ; try inversion Heqw.
- subst. exists type ; easy.
- subst. clear H2.
pose proof (IHtyping1 (eq_refl _)).
assumption.
Qed.
Theorem right_arr_type : forall Γ t u AB, Γ t ~> u : AB ->
exists A L, forall x, ~In x L -> Γ, x : A close u x : type \/ u = type .
Proof.
Admitted.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> Defined_var Γ v.
Proof.
intros. induction t; try inversion H0.
intros Γ t ; revert Γ ; induction t; intros ; try inversion H0.
- subst. induction H.
+ inversion H0. subst. exists A ; easy. inversion H2.
+ inversion H0.
+ destruct (in_app_or (FV A) (FV B) v H0).
+ destruct (in_app_or (FV A) (FV B) v0 H0).
* apply IHtyping. easy.
* destruct (var_inf (v :: L)). assert (Defined_var (Γ, x : A) v).
* destruct (var_inf (v0 :: L)). assert (Defined_var (Γ, x : A) v0).
-- apply H2. intro. apply H4. simpl. right. easy.
assert (x <> v) by (apply (not_in_not_eq _ _ _ H4)).
assert (x <> v0) by (apply (not_in_not_eq _ _ _ H4)).
apply FV_close ; [assumption | now apply not_eq_sym].
-- induction H5. inversion H5 ; subst.
++ contradict H4. simpl. auto.
++ econstructor. apply H11.
+ destruct (in_app_or (FV A) (FV t) v H0).
+ destruct (in_app_or (FV A) (FV t) v0 H0).
* apply IHtyping. easy.
* destruct (var_inf (v :: L)). assert (Defined_var (Γ, x : A) v).
-- apply H4. intro. apply H6. simpl. right. easy. easy.
* destruct (var_inf (v0 :: L)). assert (Defined_var (Γ, x : A) v0).
-- apply H4. intro. apply H6. simpl. right. easy.
assert (x <> v0) by (apply (not_in_not_eq _ _ _ H6)).
apply FV_close ; [assumption | now apply not_eq_sym].
-- induction H7. inversion H7; subst.
++ contradict H6. simpl. auto.
++ econstructor.apply H13.
+ destruct (in_app_or (FV t) (FV u) v H0).
++ econstructor. apply H13.
+ destruct (in_app_or (FV t) (FV u) v0 H0).
* apply IHtyping1. easy.
* apply IHtyping2. easy.
+ apply IHtyping1. easy.
- contradict H1.
- destruct (in_app_or (FV t1) (FV t2) v H0).
+ apply IHt1.
- simpl in H0.
pose proof (left_arr_type Γ t1 t2 u H).
destruct H1.
apply in_app_or in H0 ; destruct H0.
+ eapply IHt1 ; eassumption.
+ admit.
- admit.
- admit.
Qed.
Theorem FV_decl1 : forall Γ x A t u, Γ, x : A -> ~ In x (FV t) -> ~ In x (FV u) -> Γ t : u -> Γ, x: A t : u.
......
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