proposition: Lemma term_build_conv : forall M Q E, (forall x y A B, envSub Q x y -> activeEnv M |= x := A -> E |= y := B -> A = B) -> exists Q', Q' |=> Q /\ exists M', M ~(Q') M' /\ env M' [<->] E /\ envMinimal M' /\ (forall x y, envSub Q' x y -> envSub Q x y \/ E |= y :!).
proof: Proof. destruct M as [E Pt T M]; induction M; intros. destruct (envSubst_dec x Q) as [[y xy] | ny]. exists Q; split. apply envSubst_extends_refl. set (v' := buildVar A y). exists (buildT v'); split. constructor. simpl; constructor; trivial. apply conv_env_var with x y; trivial. split; simpl. apply env_comp_single. destruct (isVarDecl_dec E0 y) as [[B E0y] | E0yn]. rewrite (H x y A B xy); trivial. right; trivial. apply activeEnv_var_decl; trivial. left; trivial. split. unfold v'; apply buildVar_minimal. intros. left; trivial. destruct (envSubst_extend x Q E0 ny) as [Q' [QQ' [j [Q'xj [E0j Q'Q_ext]]]]]. exists Q'; split; trivial. set (v' := buildVar A j). exists (buildT v'); split. constructor. simpl; constructor; trivial. apply conv_env_var with x j; trivial. split; simpl. apply env_comp_single. left; trivial. split; simpl. unfold v'; apply buildVar_minimal. intros. destruct (eq_nat_dec x0 x); destruct (eq_nat_dec y j); solve [ right; rewrite e0; trivial | left; apply Q'Q_ext; auto ]. exists Q; split. apply envSubst_extends_refl. exists (buildT (TFun EmptyEnv f)); split. split. simpl; constructor. intros x y xy A. rewrite activeEnv_funS; simpl; trivial. split; intro X; destruct x; destruct y; try_solve. split. simpl. apply env_comp_empty_r. split. unfold envMinimal; trivial. fo. destruct (IHM (envSubst_lift1 Q) (Some A :: E0)) as [Q' [Q'Q [M'b [MM' [M'E0 [M'min Q'ext]]]]]]. intros. destruct x; destruct y. rewrite (@activeEnv_abs0 (buildT (TAbs M)) I A0); trivial. inversion H2; trivial. absurd (0 = S y). lia. apply envSub_Lok with (envSubst_lift1 Q) 0; destruct Q; simpl; trivial. absurd (0 = S x). lia. apply envSub_Rok with (envSubst_lift1 Q) 0; destruct Q; simpl; trivial. apply (H x y). destruct Q; simpl; trivial. rewrite (@activeEnv_abs (buildT (TAbs M)) I). change (absBody (M:=buildT (TAbs M)) I) with (buildT M). destruct (activeEnv (buildT M)); try_solve. try_solve. exists (envSubst_lower Q'); split; trivial. intros i j Qij. destruct Q; destruct Q'. exact (Q'Q (S i) (S j) Qij). assert (Q'00: envSub Q' 0 0). apply Q'Q; destruct Q; try_solve. assert (M''b_t: A [#] tail (env M'b) |- term M'b := type M'b). replace (A [#] tail (env M'b)) with ((Some A::EmptyEnv) [+] env M'b). apply typing_ext_env_l; exact (typing M'b). destruct (env M'b); simpl; trivial. destruct o; destruct e; trivial; solve [rewrite (M'E0 0 s A); trivial; constructor]. set (M''b := buildT M''b_t). assert (M''0: env M''b |= 0 := A). constructor. set (M''cond := Build_absCond M''b M''0). set (M'' := buildAbs M''cond). exists M''; unfold M''; split. apply abs_conv with I (buildAbs_isAbs M''cond). rewrite buildAbs_absType; trivial. rewrite buildAbs_absBody; simpl. rewrite (envSubst_lift_lower Q' Q'00); trivial. apply terms_conv_diff_env with M'b; trivial. apply equiv_term_activeEnv; trivial. simpl; intros w C D LC RD. destruct w. inversion LC. sym; apply (M'E0 0); trivial. inversion LC; inversion RD; destruct (env M'b); try_solve. split. rewrite buildAbs_env; simpl. clear M''cond M''. destruct (env M'b); simpl. apply env_comp_empty_r. apply env_comp_tail with o (Some A); trivial. split. apply envMinimal_abs with M'b (buildAbs_isAbs M''cond); trivial. destruct (env M'b); try destruct o. compute. auto. right; simpl. rewrite (M'E0 0 s A); unfold VarD; simpl; trivial. left; right; trivial. intros x y Q'xy. destruct (Q'ext (S x) (S y)). destruct Q'; try_solve. left; destruct Q; try_solve. right; try_solve. destruct (IHM1 Q E0) as [Q' [Q'Q [M'L0 [MM'L [M'Lenv [M'Lmin Q'ext]]]]]]. intros. apply H with x y; trivial. rewrite (activeEnv_app (buildT (TApp M1 M2)) I). apply env_sum_ly; trivial. apply activeEnv_app_comp. destruct (IHM2 Q' (E0 [+] env M'L0)) as [Q'' [Q''Q' [M'R0 [MM'R [M'Renv [M'Rmin Q''ext]]]]]]. intros. destruct (env_sum_varDecl E0 (env M'L0) H2) as [[E0y _] | M'L0y]. apply H with x y; trivial. destruct (Q'ext x y); trivial. inversion E0y; inversion H3; try_solve. rewrite (activeEnv_app (buildT (TApp M1 M2)) I). apply env_sum_ry; trivial. rewrite M'Lmin in M'L0y. sym. apply ((activeEnv_app_comp (buildT (TApp M1 M2)) I) x); trivial. set (MM'comp := proj2 MM'L x y H0 B0). apply (proj2 MM'comp); trivial. exists Q''; split. apply envSubst_extends_trans with Q'; trivial. assert (M'L_typ: env M'L0 [+] env M'R0 |- term M'L0 := type M'L0). apply typing_ext_env_r. apply env_comp_sym; trivial. apply env_comp_sum_comp_right with E0; trivial. exact (typing M'L0). set (M'L := buildT M'L_typ). assert (M'R_typ: env M'L0 [+] env M'R0 |- term M'R0 := type M'R0). apply typing_ext_env_l. exact (typing M'R0). set (M'R := buildT M'R_typ). assert (envOk: env M'L = env M'R). trivial. assert (Larr: isArrowType (type M'L)). simpl; rewrite <- (terms_conv_eq_type (conv_by MM'L)); try_solve. assert (typeOk: type_left (type M'L) = type M'R). simpl. rewrite <- (terms_conv_eq_type (conv_by MM'L)). rewrite <- (terms_conv_eq_type (conv_by MM'R)). trivial. set (M'cond := Build_appCond M'L M'R envOk Larr typeOk). set (M' := buildApp M'cond). exists M'; split. assert (Conv_term: conv_term (PtL @@ PtR) (term M') Q''). unfold M'; rewrite buildApp_preterm; simpl. constructor. apply conv_term_ext with Q'; trivial. destruct MM'L; trivial. destruct MM'R; trivial. constructor; trivial. apply conv_env_app with I (buildApp_isApp M'cond). simpl; unfold M'; trivial. rewrite buildApp_Lok; simpl. apply conv_env_ext with Q'; trivial. destruct MM'L; trivial. unfold conv_env, activeEnv_compSubst_on. rewrite (equiv_term_activeEnv M'L M'L0); trivial. destruct MM'L; trivial. simpl; apply env_comp_sym; apply env_comp_sum. apply env_comp_refl. apply env_comp_sym; apply env_comp_sum_comp_right with E0; trivial. rewrite buildApp_Rok; simpl. unfold conv_env, activeEnv_compSubst_on. rewrite (equiv_term_activeEnv M'R M'R0); trivial. destruct MM'R; trivial. simpl; apply env_comp_ext_l. split. unfold M'; rewrite buildApp_env_l; simpl. apply env_comp_sym. apply env_comp_sum; apply env_comp_sym; trivial. apply env_comp_sum_comp_right with (env M'L0); trivial. rewrite env_comp_sum_comm; trivial. split. apply envMinimal_app with M'L0 M'R0; unfold M'; trivial. apply buildApp_isApp. apply env_comp_sym. apply env_comp_sum_comp_right with E0; trivial. rewrite buildApp_env_l; trivial. rewrite buildApp_preterm; trivial. intros x y Q''xy. destruct (Q''ext x y); trivial. destruct (Q'ext x y); trivial. left; trivial. right; trivial. right; apply env_sumn_ln with (env M'L0); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)