proposition: Lemma compute_red_is_correct : (forall l r, In (l,r) rule_list -> forall v, In v (var_list r) -> In v (var_list l)) -> forall R, (forall l r, R r l <-> In (l,r) rule_list) -> forall t s, (In s (compute_red t) <-> one_step R s t).
proof: Proof. intros Reg R Equiv t; pattern t; apply term_rec3; clear t. intros v s; split; intro H. rewrite compute_red_unfold in H; simpl in H. apply at_top; rewrite <- (compute_head_red_is_correct rule_list Reg R Equiv); trivial. inversion H; subst. rewrite compute_red_unfold; simpl. rewrite (compute_head_red_is_correct rule_list Reg R Equiv); trivial. intros f l IHl; split; intro H. rewrite compute_red_unfold in H; simpl in H. destruct (in_app_or _ _ _ H) as [H1 | H2]; clear H. apply at_top; rewrite <- (compute_head_red_is_correct rule_list Reg R Equiv); trivial. rewrite in_map_iff in H2. destruct H2 as [k [H2 H3]]. subst s; apply in_context. generalize IHl k H3; clear IHl k H3; induction l as [ | a l]; intros IHll k H3; rewrite mapii_dep_unfold in H3; simpl in H3; trivial. contradiction. destruct (in_app_or _ _ _ H3) as [H4 | H5]; clear H3. rewrite in_map_iff in H4. destruct H4 as [b [H4 H5]]; subst. apply head_step. rewrite <- (IHll a); trivial. left; trivial. rewrite in_map_iff in H5. destruct H5 as [l' [H5 H6]]; subst. apply tail_step. apply IHl; trivial. intros t t_in_l; apply IHll; right; trivial. inversion H; clear H; subst. rewrite compute_red_unfold; simpl. apply in_or_app; left; rewrite (compute_head_red_is_correct rule_list Reg R Equiv); trivial. rewrite compute_red_unfold; simpl. apply in_or_app; right. rewrite in_map_iff; exists l1; split; trivial. generalize IHl; clear IHl; induction H2; intros IHl. rewrite mapii_dep_unfold; simpl. apply in_or_app; left. rewrite in_map_iff; exists t1; split; trivial. rewrite (IHl _ (or_introl _ (eq_refl _)) t1); trivial. rewrite mapii_dep_unfold; simpl. apply in_or_app; right. rewrite in_map_iff. exists l1; split; trivial. apply IHone_step_list; trivial. intros u u_in_l2; apply IHl; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)