proposition: Lemma compute_head_red_is_correct : forall rule_list, (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_head_red t rule_list) <-> axiom R s t).
proof: Proof. intros rule_list; induction rule_list as [ | [l r] rule_list]; intros Reg R Equiv t s; split; intro H. contradiction. inversion H; subst. rewrite Equiv in H0; contradiction. simpl in H. case_eq (matching ((l,t) :: nil)). intros sigma mlt_eq_sigma. destruct (matching_correct mlt_eq_sigma) as [C1 [C2 C3]]. assert (H' := C3 _ _ (or_introl _ (eq_refl _))). rewrite mlt_eq_sigma in H. destruct H as [H | H]. subst; apply instance. rewrite Equiv; left; trivial. set (R' := fun r l => In (l,r) rule_list). apply axiom_incl with R'; trivial. intros l1 r1; unfold R'; rewrite Equiv; intro; right; trivial. rewrite <- IHrule_list; trivial. intros l1 r1 l1r1_in_rule_list; apply Reg; right; trivial. intros l1 r1; unfold R'; intuition. intro mlt_eq_none; rewrite mlt_eq_none in H. set (R' := fun r l => In (l,r) rule_list). apply axiom_incl with R'; trivial. intros l1 r1; unfold R'; rewrite Equiv; intro; right; trivial. rewrite <- IHrule_list; trivial. intros l1 r1 l1r1_in_rule_list; apply Reg; right; trivial. intros l1 r1; unfold R'; intuition. inversion H; subst. rewrite Equiv in H0. destruct H0 as [H0 | H0]. injection H0; clear H0; intros; subst t1 t2. simpl. assert (C := @matching_correct ((l, apply_subst sigma l) :: nil)). assert (C' := matching_complete ((l, apply_subst sigma l) :: nil) sigma). destruct (matching ((l, apply_subst sigma l) :: nil)) as [tau | ]. generalize (C _ (eq_refl _)); clear C; intros [C1 [C2 C3]]. left. assert (H' : forall v, In v (var_list r) -> apply_subst tau (Var v) = apply_subst sigma (Var v)). intros v v_in_r; assert (v_in_l : In v (var_list l)). apply Reg with r; trivial; left; trivial. apply C' with l (apply_subst sigma l); trivial. intros p s [ps_eq_llsigma | ps_in_nil]; [idtac | contradiction]. injection ps_eq_llsigma; intros; subst; trivial. left; trivial. generalize r H'; clear H'; intro t; pattern t; apply term_rec3; clear t. intros v IH; apply IH; left; trivial. intros f k IHl IH. simpl; apply (f_equal (fun ll => Term f ll)). apply map_eq; intros a a_in_k; apply IHl; trivial. destruct (In_split _ _ a_in_k) as [k1 [k2 K]]; subst. intros v v_in_a; apply IH. apply (@var_in_subterm v a (Term f (k1 ++ a :: k2)) (length k1 :: nil)); trivial. simpl; rewrite nth_error_at_pos; trivial. assert False. apply C'. intros p s [ps_eq_llsigma | ps_in_nil]; [idtac | contradiction]. injection ps_eq_llsigma; intros; subst; trivial. contradiction. simpl. assert (H' : forall l r : term, In (l, r) rule_list -> forall v : variable, In v (var_list r) -> In v (var_list l)). intros l1 r1 lr_in_rule_list; apply Reg; right; trivial. destruct (matching ((l, apply_subst sigma t2) :: nil)) as [tau | ]; [right | idtac]. set (R' := fun r l => In (l,r) rule_list). rewrite (IHrule_list H' R'); trivial. apply instance; unfold R'; trivial. intros l1 r1; unfold R'; split; trivial. set (R' := fun r l => In (l,r) rule_list). rewrite (IHrule_list H' R'); trivial. apply instance; unfold R'; trivial. intros l1 r1; unfold R'; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)