proposition: Lemma defined_subterms_unfold_gen : forall is_def s lhs acc1 acc2 acc1' acc2', (forall t, In t acc1 <-> In t acc1') -> (forall t, In t acc2 <-> In t acc2') -> forall t, In t (defined_subterms is_def lhs (acc1 ++ acc2) s) <-> (In t (defined_subterms is_def lhs acc1' s) \/ In t acc2').
proof: Proof. intros is_def s; pattern s; apply term_rec3; clear s. intros v lhs acc1 acc2 acc1' acc2' I1 I2 t; simpl; split. rewrite <- I1; rewrite <- I2; apply in_app_or. rewrite <- I1; rewrite <- I2; apply in_or_app. intros f l IH lhs acc1 acc2 acc1' acc2' I1 I2 t; simpl. set (fl := Term f l) in *. set (flacc1 := (if is_def f then if eq_bool lhs fl then fl :: acc1 else if is_subterm fl lhs then acc1 else fl :: acc1 else acc1)) in *. replace (if is_def f then if eq_bool lhs fl then fl :: acc1 ++ acc2 else if is_subterm fl lhs then acc1 ++ acc2 else fl :: acc1 ++ acc2 else acc1 ++ acc2) with (flacc1 ++ acc2). set (flacc1' := (if is_def f then if eq_bool lhs fl then fl :: acc1' else if is_subterm fl lhs then acc1' else fl :: acc1' else acc1')) in *. assert (flI1 : forall t : term, In t flacc1 <-> In t flacc1'). intros s; unfold flacc1, flacc1'; case (is_def f). case (eq_bool lhs fl). simpl; rewrite I1; split; exact (fun H => H). case (is_subterm fl lhs). rewrite I1; split; exact (fun H => H). simpl; rewrite I1; split; exact (fun H => H). rewrite I1; split; exact (fun H => H). clearbody flacc1; clearbody flacc1'; clear acc1 acc1' I1. revert flacc1 acc2 flacc1' acc2' flI1 I2; induction l as [ | s l]; simpl; intros acc1 acc2 acc1' acc2' I1 I2. split. rewrite <- I1; rewrite <- I2; apply in_app_or. rewrite <- I1; rewrite <- I2; apply in_or_app. replace (defined_subterms is_def lhs (acc1 ++ acc2) s) with (nil ++ defined_subterms is_def lhs (acc1 ++ acc2) s); [ | apply eq_refl]. rewrite (IHl (tail_prop _ IH) nil (defined_subterms is_def lhs (acc1 ++ acc2) s) nil ((defined_subterms is_def lhs acc1' s) ++ acc2')). replace (defined_subterms is_def lhs acc1' s) with (nil ++ defined_subterms is_def lhs acc1' s); [ | apply eq_refl]. rewrite (IHl (tail_prop _ IH) nil (defined_subterms is_def lhs acc1' s) nil (defined_subterms is_def lhs acc1' s)). split. intros [H1 | H2]. do 2 left; assumption. simpl in H2; destruct (in_app_or _ _ _ H2) as [H3 | H3]. left; right; assumption. right; assumption. intros [[H1 | H2] | H3]. left; assumption. right; simpl; apply in_or_app; left; assumption. right; simpl; apply in_or_app; right; assumption. intro; split; exact (fun H => H). intro; split; exact (fun H => H). intro; split; exact (fun H => H). intro u; rewrite (IH _ (or_introl _ (eq_refl _)) lhs acc1 acc2 acc1' acc2'). split. apply in_or_app. apply in_app_or. assumption. assumption. unfold flacc1; case (is_def f); [ | apply eq_refl]. case (eq_bool lhs fl). apply eq_refl. case (is_subterm fl lhs); apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)