proposition: Lemma defined_subterms_is_sound: forall is_def lhs, forall r g k, In (Term g k) (defined_subterms is_def lhs nil r) -> ((is_def g = true) /\ (exists p, subterm_at_pos r p = Some (Term g k)) /\ (forall i q, subterm_at_pos lhs (i :: q) <> Some (Term g k))).
proof: Proof. intros is_def lhs r. induction r using term_rec3; intros g k gk_in_d. contradiction. simpl in gk_in_d. rewrite fold_left_defined_subterms_unfold in gk_in_d. destruct gk_in_d as [gk_in_d | gk_in_d]. assert (K : is_def g = true /\ (exists i, exists p : list nat, subterm_at_pos (Term f l) (i :: p) = Some (Term g k)) /\ (forall (i : nat) (q : list nat), subterm_at_pos lhs (i :: q) <> Some (Term g k))). simpl subterm_at_pos at 1. induction l as [ | t l]. contradiction. simpl in gk_in_d. rewrite fold_left_defined_subterms_unfold in gk_in_d. destruct gk_in_d as [gk_in_d | gk_in_d]. destruct (IHl (tail_prop _ H) gk_in_d) as [Dg [[i [p K1]] K2]]. split. assumption. split. exists (S i); exists p; simpl; assumption. assumption. destruct (H _ (or_introl _ (eq_refl _)) _ _ gk_in_d) as [Dg [[p K1] K2]]. split. assumption. split. exists 0; exists p; simpl; assumption. assumption. destruct K as [Dg [[i [p K1]] K2]]. split. assumption. split. exists (i :: p); assumption. assumption. revert gk_in_d. case_eq (is_def f). case_eq (eq_bool lhs (Term f l)). intros lhs_eq_fl Df [gk_eq_fl | gk_in_nil]; [ | contradiction]. injection gk_eq_fl; clear gk_eq_fl; intros; subst; split. assumption. split. exists nil; apply eq_refl. generalize (eq_bool_ok lhs (Term g k)); rewrite lhs_eq_fl; clear lhs_eq_fl; intro lhs_eq_gk; rewrite <- lhs_eq_gk. intros i q Sub. generalize (size_subterm_at_pos lhs i q); rewrite Sub. apply Nat.lt_irrefl. case_eq (is_subterm (Term f l) lhs). contradiction. intros nSub lhs_diff_fl Df [gk_eq_fl | gk_in_nil]; [ | contradiction]. injection gk_eq_fl; clear gk_eq_fl; intros; subst; split. assumption. split. exists nil; apply eq_refl. intros i q; apply is_subterm_ok_false; assumption. contradiction. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)