proposition: Lemma matching_complete : forall pb sigma, (forall p s, In (p,s) pb -> apply_subst sigma p = s) -> match matching pb with | Some tau => forall v p s, In v (var_list p) -> In (p,s) pb -> apply_subst tau (Var v) = apply_subst sigma (Var v) | None => False end.
proof: Proof. assert (Rt : reflexive _ (@eq term)). intro a; reflexivity. intro pb; pattern pb; apply (well_founded_ind wf_size); clear pb. intros [ | [patt subj] pb] IH sigma H; rewrite matching_unfold2. intros; contradiction. assert (tailH : forall p s : term, In (p, s) pb -> apply_subst sigma p = s). intros; apply H; right; assumption. assert (Hsigma := IH _ (matching_call1 _ _ _) sigma tailH). destruct patt as [ x | f l]. case_eq (matching pb). intros subst matching_pb_eq_subst; rewrite matching_pb_eq_subst in Hsigma. destruct (matching_correct_aux pb matching_pb_eq_subst) as [C1 [C2 [C4 C3]]]. assert (H'' := merge_correct _ X.eq_bool_ok _ eq_bool_ok EX.eq_proof Rt ((x,subj) :: nil) subst). case_eq (merge eq_var_bool eq_bool ((x, subj) :: nil) subst). intros tau matching_pb_eq_tau; rewrite matching_pb_eq_tau in H''. destruct H'' as [H1 [H2 H3]]. intros v p s v_in_p [ps_eq_xsubj | ps_in_pb]. injection ps_eq_xsubj; clear ps_eq_xsubj; intros; subst. destruct v_in_p as [v_eq_x | v_in_nil]; [idtac | contradiction]. subst v; rewrite (H (Var x) s (or_introl _ (eq_refl _))). simpl; rewrite (H1 x s); trivial. simpl; rewrite eq_var_bool_refl; reflexivity. rewrite <- (Hsigma v p s v_in_p ps_in_pb). simpl; assert (K2 := C2 v p s v_in_p ps_in_pb). case_eq (find eq_var_bool v subst). intros v_subst H''; destruct (H2 _ _ H'') as [b [K3 K4]]; rewrite K3; trivial. symmetry; generalize (eq_bool_ok v_subst b); rewrite K4; intro K5; exact K5. intros H''; rewrite H'' in K2; absurd (@None term = None); trivial. intro matching_pb_eq_none; rewrite matching_pb_eq_none in H''. destruct H'' as [v [v' [t1 [t2 [H1 [H2 [v_eq_v' t1_diff_t2]]]]]]]. generalize (X.eq_bool_ok v v'); rewrite v_eq_v'; intro v_eq_v''; subst v'. generalize (eq_bool_ok t2 t1); rewrite t1_diff_t2; clear t1_diff_t2; intro t1_diff_t2. rewrite C1 in H1; rewrite C1 in H2. case H1; clear H1; intro H1. destruct (C4 v) as [p [s [ps_in_pb v_in_p]]]. rewrite H2; discriminate. simpl in H1; generalize (X.eq_bool_ok v x); destruct (eq_var_bool v x); [intros v_eq_x | intros v_diff_x; discriminate]. subst v; injection H1; clear H1; intros; subst subj. assert (Hv := Hsigma x p s v_in_p ps_in_pb). assert (Hv' := H (Var x) t1 (or_introl _ (eq_refl _))). rewrite Hv' in Hv; simpl in Hv; rewrite H2 in Hv; absurd (t2 = t1); assumption. rewrite H1 in H2; apply t1_diff_t2; symmetry; injection H2; intro H3; exact H3. intro matching_pb_eq_none; rewrite matching_pb_eq_none in Hsigma. elim Hsigma. destruct subj as [x | g m]. assert (H' := H (Term f l) (Var x) (or_introl _ (eq_refl _))); simpl in H'. discriminate. case_eq (eq_symb_bool f g); [intro f_eq_g | intro f_diff_g]. destruct l as [ | pat1 lpat]; destruct m as [ | sub1 lsub]. destruct (matching pb) as [tau | ]. intros v p s v_in_p [ps_eq_ff | ps_in_pb]. injection ps_eq_ff; intros; subst; simpl in v_in_p; contradiction. apply Hsigma with p s; trivial. contradiction. assert (H' := H (Term f nil) (Term g (sub1 :: lsub)) (or_introl _ (eq_refl _))); simpl in H'. discriminate. assert (H' := H (Term f (pat1 :: lpat)) (Term g nil) (or_introl _ (eq_refl _))); simpl in H'. discriminate. assert (H' := IH _ (matching_call2 pat1 sub1 f lpat g lsub pb)). assert (Correct := matching_correct_aux ((pat1,sub1) :: nil)). case_eq (matching ((pat1,sub1) :: nil)). intros subst1 matching_pat1sub1_eq_subst1. destruct (Correct _ matching_pat1sub1_eq_subst1) as [C1 [C2 [C4 C3]]]; clear Correct. assert (H'' := IH _ (matching_call3 pat1 sub1 f lpat g lsub pb)). assert (Correct' := matching_correct_aux ((Term f lpat, Term g lsub) :: pb)). case_eq (matching ((Term f lpat, Term g lsub) :: pb)). intros subst matching_pb_eq_subst. destruct (Correct' _ matching_pb_eq_subst) as [C1' [C2' [C4' C3']]]; clear Correct'. assert (H''' := merge_correct _ X.eq_bool_ok _ eq_bool_ok EX.eq_proof Rt subst1 subst). assert (headH : forall p s, In (p,s) ((pat1,sub1) :: nil) -> apply_subst sigma p = s). intros p s [ps_eq_pat1sub1 | ps_in_nil]; [idtac | contradiction]. injection ps_eq_pat1sub1; clear ps_eq_pat1sub1; intros; subst p s. assert (K := H _ _ (or_introl _ (eq_refl _))). simpl in K; injection K; intros; subst; trivial. assert (Hsigma1 := IH _ (matching_call2 pat1 sub1 f lpat g lsub pb) sigma headH). rewrite matching_pat1sub1_eq_subst1 in Hsigma1. clear tailH; assert (tailH : forall p s, In (p,s) ((Term f lpat, Term g lsub) :: pb) -> apply_subst sigma p = s). intros p s [ps_eq_patsub | ps_in_pb]. injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s. assert (K := H _ _ (or_introl _ (eq_refl _))). simpl in K; injection K; intros; subst; trivial. apply H; right; trivial. clear Hsigma; assert (Hsigma := IH _ (matching_call3 pat1 sub1 f lpat g lsub pb) sigma tailH). rewrite matching_pb_eq_subst in Hsigma. case_eq (merge eq_var_bool eq_bool subst1 subst). intros tau matching_pb_eq_tau; rewrite matching_pb_eq_tau in H'''. destruct H''' as [H1 [H2 H3]]. intros v p s v_in_p [ps_eq_pat_sub | ps_in_pb]. injection ps_eq_pat_sub; clear ps_eq_pat_sub; intros; subst p s. rewrite var_list_unfold in v_in_p; simpl in v_in_p. destruct (in_app_or _ _ _ v_in_p) as [v_in_pat1 | v_in_lpat]; clear v_in_p. rewrite <- (Hsigma1 v _ _ v_in_pat1 (or_introl _ (eq_refl _))). simpl; assert (K2 := C2 v _ _ v_in_pat1 (or_introl _ (eq_refl _))). case_eq (find eq_var_bool v subst1). intros v_subst1 H'''; rewrite (H1 _ _ H'''); trivial. intros H'''; rewrite H''' in K2; absurd (@None term = None); trivial. assert (K := Hsigma v (Term f lpat) (Term g lsub)). simpl in K; generalize (K v_in_lpat (or_introl _ (eq_refl _))); clear K; intro K. simpl; assert (K2 := C2' v (Term f lpat) (Term g lsub)). simpl in K2; generalize (K2 v_in_lpat (or_introl _ (eq_refl _))); clear K2; intro K2. case_eq (find eq_var_bool v subst); [idtac | intro H'''; rewrite H''' in K2; apply False_rect; apply K2; reflexivity]. intros v_subst H'''; destruct (H2 _ _ H''') as [b [K3 K4]]. generalize (eq_bool_ok v_subst b); rewrite K4; clear K4; intro K4; subst b. rewrite H''' in K; rewrite K3; assumption. assert (K := Hsigma v p s v_in_p (or_intror _ ps_in_pb)). simpl; assert (K2 := C2' v p s v_in_p (or_intror _ ps_in_pb)). simpl in K; case_eq (find eq_var_bool v subst). intros v_subst H'''; destruct (H2 _ _ H''') as [b [K3 K4]]. generalize (eq_bool_ok v_subst b); rewrite K4; clear K4; intro K4; subst b. rewrite H''' in K; rewrite K3; assumption. intros H'''; rewrite H''' in K2; absurd (@None term = None); trivial. intro matching_pb_eq_none; rewrite matching_pb_eq_none in H'''. destruct H''' as [v [v' [t1 [t2 [H1 [H2 [v_eq_v' t1_diff_t2]]]]]]]. generalize (X.eq_bool_ok v v'); rewrite v_eq_v'; intro v_eq_v''; subst v'. generalize (eq_bool_ok t2 t1); rewrite t1_diff_t2; clear t1_diff_t2; intro t1_diff_t2. case H1; clear H1; intro H1. destruct (C4 v) as [p [s [ps_in_pb v_in_p]]]. rewrite H1; discriminate. assert (H1v := Hsigma1 v p s v_in_p ps_in_pb); simpl in H1v. rewrite H1 in H1v. destruct (C4' v) as [p' [s' [ps'_in_pb v_in_p']]]. rewrite C1' in H2; rewrite H2; discriminate. assert (H2v := Hsigma v p' s' v_in_p' ps'_in_pb); simpl in H2v. rewrite <- H2v in H1v. rewrite C1' in H2; rewrite H2 in H1v; apply t1_diff_t2; symmetry; assumption. apply t1_diff_t2; symmetry; rewrite C1' in H1; rewrite C1' in H2; rewrite H1 in H2; injection H2; intro H3; exact H3. intro matching_pb_eq_none; rewrite matching_pb_eq_none in H''. apply (H'' sigma). intros p s [ps_eq_patsub | ps_in_pb]. injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s. assert (K := H _ _ (or_introl _ (eq_refl _))). simpl in K; injection K; intros; subst; trivial. apply H; right; trivial. intro matching_pb_eq_none; rewrite matching_pb_eq_none in H'. apply (H' sigma). intros p s [ps_eq_patsub | ps_in_pb]. injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s. assert (K := H _ _ (or_introl _ (eq_refl _))). simpl in K; injection K; intros; subst; trivial. contradiction. absurd (f=g). generalize (F.Symb.eq_bool_ok f g); rewrite f_diff_g; intro H3; exact H3. assert (K := H _ _ (or_introl _ (eq_refl _))). simpl in K; injection K; intros; subst; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)