proposition: Lemma ty_subst_extend : forall ty1 n ty2 val, let interp_ty2 := {| comp_term := interp_term ty2 val; comp_val := interp_val ty2 val |} in no_capture ty1 ty2 -> (forall ectx t, interp_term (ty_subst n ty1 ty2) val ectx t <-> interp_term ty1 (extend val n interp_ty2) ectx t) /\ (forall v, interp_val (ty_subst n ty1 ty2) val v <-> interp_val ty1 (extend val n interp_ty2) v) .
proof: Proof. induction ty1; unfold extend in *; simpl; intros m; intros. - simpl; destruct (n =? m); now auto. - split; split; intros h. + destruct h as [t' [ectx' [eval_t comp_t]]]. exists t', ectx'; split; auto; intros v0. intros. apply IHty1_2; eauto. apply comp_t. apply IHty1_1; eauto. + destruct h as [t' [ectx' [eval_t comp_t]]]. exists t', ectx'; split; auto. intros; apply IHty1_2; eauto. apply comp_t. apply IHty1_1; eauto. + destruct v; intros v comp_v. apply IHty1_2; eauto. apply h. apply IHty1_1; eauto. + destruct v; intros v comp_v. apply IHty1_2; eauto. apply h. apply IHty1_1; eauto. - simpl; unfold extend. case_eq (m =? n); intros eq_n_m; try rewrite eq_n_m; simpl; [assert (m = n) by (apply beq_nat_true; eauto) | assert (m <> n) by (apply beq_nat_false; eauto)]; [subst; unfold extend; split; intros; split; intros; assert (val_ext : forall n m, equiv_comp_pair ((fun var : name => if var =? n then P else val var) m) ((fun var : name => if var =? n then P else if var =? n then {| comp_term := interp_term ty2 val; comp_val := interp_val ty2 val |} else val var) m) ) by (intros k1 k2; destruct (k2 =? k1); eauto); eapply ty_subst_ext; eauto; try apply val_ext; intros; try (apply equiv_comp_pair_sym; apply val_ext) |]. split; split; intros; assert (IH := IHty1 m ty2 (extend val n P)); clear IHty1; unfold extend in *. + apply (ty_subst_ext ty1 ( fun var : name => if var =? m then {| comp_term := interp_term ty2 (fun var0 : name => if var0 =? n then P else val var0); comp_val := interp_val ty2 (fun var0 : name => if var0 =? n then P else val var0) |} else if var =? n then P else val var ) _); [| apply IH; eauto]. intros. assert (at_most_one : ((n0 =? m) = false) \/ ((n0 =? n) = false)) by (case_eq (n0 =? m); case_eq (n0 =? n); repeat rewrite Nat.eqb_neq; repeat rewrite Nat.eqb_eq; intros; try congruence; auto). split; intros; destruct (n0 =? m); destruct (n0 =? n); simpl; try reflexivity; destruct at_most_one; try congruence. -- symmetry; eapply is_not_free_extend; eauto. -- symmetry; eapply is_not_free_extend; eauto. + apply IH; [ now eauto |]. apply (ty_subst_ext ty1 ( fun var : name => if var =? n then P else if var =? m then {| comp_term := interp_term ty2 val; comp_val := interp_val ty2 val |} else val var ) _); [ | now auto]. intros n0; assert (at_most_one : ((n0 =? m) = false) \/ ((n0 =? n) = false)) by (case_eq (n0 =? m); case_eq (n0 =? n); repeat rewrite Nat.eqb_neq; repeat rewrite Nat.eqb_eq; intros; try congruence; auto). split; intros; destruct (n0 =? m); destruct (n0 =? n); simpl; try reflexivity; destruct at_most_one; try congruence. -- eapply is_not_free_extend; eauto. -- eapply is_not_free_extend; eauto. + apply (ty_subst_ext ty1 ( fun var : name => if var =? m then {| comp_term := interp_term ty2 (fun var0 : name => if var0 =? n then P else val var0); comp_val := interp_val ty2 (fun var0 : name => if var0 =? n then P else val var0) |} else if var =? n then P else val var ) _); [| apply IH; eauto]. intros. assert (at_most_one : ((n0 =? m) = false) \/ ((n0 =? n) = false)) by (case_eq (n0 =? m); case_eq (n0 =? n); repeat rewrite Nat.eqb_neq; repeat rewrite Nat.eqb_eq; intros; try congruence; auto). split; intros; destruct (n0 =? m); destruct (n0 =? n); simpl; try reflexivity; destruct at_most_one; try congruence. -- symmetry; eapply is_not_free_extend; eauto. -- symmetry; eapply is_not_free_extend; eauto. + apply IH; [now eauto |]. apply (ty_subst_ext ty1 ( fun var : name => if var =? n then P else if var =? m then {| comp_term := interp_term ty2 val; comp_val := interp_val ty2 val |} else val var ) _); [| now eauto]. intros; assert (at_most_one : ((n0 =? m) = false) \/ ((n0 =? n) = false)) by (case_eq (n0 =? m); case_eq (n0 =? n); repeat rewrite Nat.eqb_neq; repeat rewrite Nat.eqb_eq; intros; try congruence; auto). split; intros; destruct (n0 =? m); destruct (n0 =? n); simpl; try reflexivity; destruct at_most_one; try congruence; eapply is_not_free_extend; eauto. Qed.
imports: List Arith Bool