proposition: Lemma matching_correct_aux : forall pb sigma, matching pb = Some sigma -> ((forall v t1, In (v,t1) sigma <-> find eq_var_bool v sigma = Some t1) /\ (forall v p s, In v (var_list p) -> In (p,s) pb -> find eq_var_bool v sigma <> None) /\ (forall v, find eq_var_bool v sigma <> None -> exists p, exists s, In (p,s) pb /\ In v (var_list p)) /\ (forall p s, In (p,s) pb -> apply_subst sigma p = s)).
proof: Proof. assert (Rt : reflexive _ (@eq term)). intro a; reflexivity. assert (change_hyp : forall sigma, (forall v t1, In (v,t1) sigma <-> find eq_var_bool v sigma = Some t1) -> (forall a1 a1' b1 c1, In (a1,b1) sigma -> In (a1',c1) sigma -> eq_var_bool a1 a1' = true -> eq_bool b1 c1 =true)). intros sigma H v v' t1 t2 H1 H2; generalize (X.eq_bool_ok v v') (eq_bool_ok t1 t2). case (eq_var_bool v v'). case (eq_bool t1 t2). intros _ _ _; reflexivity. intros v_eq_v' t1_diff_t2; apply False_rect; apply t1_diff_t2. subst v'; rewrite H in H1; rewrite H in H2; rewrite H1 in H2; injection H2; intro H3; exact H3. intros _ _ Abs; discriminate. intro pb; pattern pb; apply (well_founded_ind wf_size); clear pb. intros [ | [patt subj] pb] IH sigma H; rewrite matching_unfold2 in H. injection H; clear H; intros; subst; repeat split; trivial; intros; try contradiction. simpl in H; discriminate. destruct patt as [ x | f l]. assert (H' := IH _ (matching_call1 _ _ _)). destruct (matching pb) as [subst | ]. generalize (H' _ (eq_refl _)) ; clear H'; intros [IH1 [IH2 [IH4 IH3]]]. assert (H' := merge_correct _ X.eq_bool_ok _ eq_bool_ok EX.eq_proof Rt ((x,subj) :: nil) subst). rewrite H in H'; destruct H' as [H1 [H2 H3]]. split. intros v t1; split; intro Ht1. assert (H'' := merge_inv _ X.eq_bool_ok _ eq_bool_ok EX.eq_proof Rt ((x,subj) :: nil) subst). rewrite H in H''. generalize (find_not_found eq_var_bool v v t1 sigma). case_eq (find eq_var_bool v sigma). intros t2 F _; apply f_equal; symmetry. assert (t1_eq_t2 : eq_bool t1 t2 = true). apply H'' with v v; trivial. intros w w' u1 u2 [wu1_eq_xs | wu1_in_nil] [wu2_eq_xs | wu2_in_nil]; try contradiction. injection wu1_eq_xs; intros; subst; injection wu2_eq_xs; intros; subst; trivial. generalize (eq_bool_ok u2 u2); case (eq_bool u2 u2). intros _; reflexivity. intro u2_diff_u2; apply False_rect; apply u2_diff_u2; reflexivity. apply change_hyp; assumption. destruct (find_mem _ _ X.eq_bool_ok _ _ F) as [v' [l1 [l2 [K1 K2]]]]; subst; apply in_or_app; right; left; reflexivity. apply eq_var_bool_refl. generalize (eq_bool_ok t1 t2); rewrite t1_eq_t2; intro Eq; exact Eq. intros _ Abs; apply False_rect; apply (Abs (eq_refl _) (eq_var_bool_refl v) Ht1). destruct (find_mem _ _ X.eq_bool_ok _ _ Ht1) as [v' [l1 [l2 [K1 K2]]]]; subst; apply in_or_app; right; left; reflexivity. split. intros v p s v_in_p [ps_eq_xsubj | ps_in_pb]. injection ps_eq_xsubj; clear ps_eq_xsubj; intros; subst; simpl. destruct v_in_p as [v_eq_x | v_in_nil]; [subst v | contradiction]. rewrite (H1 x s). discriminate. simpl; rewrite eq_var_bool_refl; reflexivity. assert (K2 := IH2 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' [H'' _]]; rewrite H''; discriminate. intros H'; rewrite H' in K2; absurd (@None term = None); trivial. split. intros v H'; assert (H3v := H3 v). destruct (find eq_var_bool v sigma) as [v_sigma | ]. destruct (H3v v_sigma (eq_refl _)) as [case1 | case2]. simpl in case1; revert case1; generalize (X.eq_bool_ok v x); case (eq_var_bool v x); [intro v_eq_x | intro v_diff_x]. subst v; exists (Var x); exists subj; split; left; trivial. intro; discriminate. destruct (IH4 v) as [p [s [ps_in_pb v_in_p]]]. rewrite (proj2 case2); discriminate. exists p; exists s; split; trivial; right; trivial. absurd (@None term = None); trivial. intros p s [ps_eq_xsubj | ps_in_pb]. assert (K1 := H1 x subj). injection ps_eq_xsubj; clear ps_eq_xsubj; intros; subst; simpl. rewrite K1; trivial. simpl; rewrite eq_var_bool_refl; reflexivity. assert (K2 : forall v, In v (var_list p) -> find eq_var_bool v subst <> None). intros v v_in_p; apply IH2 with p s; trivial. assert (KK2 : forall v, In v (var_list p) -> apply_subst subst (Var v) = apply_subst sigma (Var v)). intros v v_in_p; generalize (K2 v v_in_p) (H2 v); simpl. destruct (find eq_var_bool v subst) as [v_subst | ]. clear K2; intros _ K2; destruct (K2 _ (eq_refl _)) as [b [K3 K4]]. rewrite K3. generalize (eq_bool_ok v_subst b); rewrite K4; intro K5; exact K5. intro; absurd (@None term = None); trivial. rewrite <- (IH3 _ _ ps_in_pb). symmetry. generalize KK2; clear s ps_in_pb K2 KK2; pattern p; apply term_rec3; clear p. intros v KK2; apply KK2; left; trivial. intros f l IHl KK2. assert (IHl' : forall t, In t l -> apply_subst subst t = apply_subst sigma t). intros t t_in_l; apply IHl; trivial. intros v v_in_t; apply KK2. destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst l. apply (@var_in_subterm v t (Term f (l1 ++ t :: l2)) (length l1 :: nil)); trivial. simpl; rewrite nth_error_at_pos; trivial. simpl; apply (f_equal (fun l => Term f l)). apply map_eq; trivial. discriminate. destruct subj as [x | g m]. discriminate. generalize (F.Symb.eq_bool_ok f g); revert H; case (eq_symb_bool f g); [intros H f_eq_g | intros H f_diff_g]. destruct l as [ | pat1 lpat]; destruct m as [ | sub1 lsub]. destruct (IH _ (matching_call1 _ _ _) sigma H) as [H1 [H2 [H4 H3]]]. split; trivial. split. intros v p s v_in_p [ps_eq_ff | ps_in_pb]. injection ps_eq_ff; intros; subst. contradiction. apply H2 with p s; trivial. split. intros v H'; destruct (H4 _ H') as [p [s [ps_in_pb v_in_p]]]. exists p; exists s; split; trivial; right; trivial. intros p s [ps_eq_ff | ps_in_pb]. injection ps_eq_ff; intros; subst; simpl; trivial. apply H3; trivial. discriminate. discriminate. assert (H' := IH _ (matching_call2 pat1 sub1 f lpat g lsub pb)). destruct (matching ((pat1,sub1) :: nil)) as [subst1 | ]. generalize (H' _ (eq_refl _)); clear H'; intros [IH1 [IH2 [IH4 IH3]]]. assert (H' := IH _ (matching_call3 pat1 sub1 f lpat g lsub pb)). destruct (matching ((Term f lpat, Term g lsub) :: pb)) as [subst | ]. generalize (H' _ (eq_refl _)); clear H'; intros [IH1' [IH2' [IH4' IH3']]]. assert (H' := merge_correct _ X.eq_bool_ok _ eq_bool_ok EX.eq_proof Rt subst1 subst). rewrite H in H'; destruct H' as [H1 [H2 H3]]. split. intros v t1; split; intro Ht1. assert (H'' := merge_inv _ X.eq_bool_ok _ eq_bool_ok EX.eq_proof Rt subst1 subst). rewrite H in H''. generalize (find_not_found eq_var_bool v v t1 sigma). case_eq (find eq_var_bool v sigma). intros t2 F _; apply f_equal; symmetry. assert (t1_eq_t2 : eq_bool t1 t2 = true). apply H'' with v v; trivial. apply change_hyp; assumption. apply change_hyp; assumption. destruct (find_mem _ _ X.eq_bool_ok _ _ F) as [v' [l1 [l2 [K1 K2]]]]; subst; apply in_or_app; right; left; reflexivity. apply eq_var_bool_refl. generalize (eq_bool_ok t1 t2); rewrite t1_eq_t2; intro Eq; exact Eq. intros _ Abs; apply False_rect; apply (Abs (eq_refl _) (eq_var_bool_refl v) Ht1). destruct (find_mem _ _ X.eq_bool_ok _ _ Ht1) as [v' [l1 [l2 [K1 K2]]]]; subst; apply in_or_app; right; left; reflexivity. split. intros v p s v_in_p [ps_eq_patsub | ps_in_pb]. injection ps_eq_patsub; clear ps_eq_patsub; intros; subst; simpl. simpl in v_in_p; destruct (in_app_or _ _ _ v_in_p) as [v_in_pat1 | v_in_lpat]. assert (K2 := IH2 v pat1 sub1 v_in_pat1 (or_introl _ (eq_refl _))). case_eq (find eq_var_bool v subst1). intros v_subst H'. rewrite (H1 _ _ H'); discriminate. intros H'; rewrite H' in K2; absurd (@None term = None); trivial. assert (K2 := IH2' v (Term g lpat) (Term g lsub) v_in_lpat (or_introl _ (eq_refl _))). case_eq (find eq_var_bool v subst). intros v_subst H'. destruct (H2 _ _ H') as [b [K3 _]]; rewrite K3; discriminate. intros H'; rewrite H' in K2; absurd (@None term = None); trivial. assert (K2 := IH2' v p s v_in_p (or_intror _ ps_in_pb)). case_eq (find eq_var_bool v subst). intros v_subst H'. destruct (H2 _ _ H') as [b [K3 _]]; rewrite K3; discriminate. intros H'; rewrite H' in K2; absurd (@None term = None); trivial. split. intros v H'; assert (H3v := H3 v). destruct (find eq_var_bool v sigma) as [v_sigma | ]. destruct (H3v v_sigma (eq_refl _)) as [case1 | case2]. destruct (IH4 v) as [p [s [ps_in_pb v_in_p]]]. rewrite case1; discriminate. exists (Term f (pat1 :: lpat)); exists (Term g (sub1 :: lsub)); split. left; trivial. destruct ps_in_pb as [ps_eq_pat1sub1 | ps_in_nil]. injection ps_eq_pat1sub1; clear ps_eq_pat1sub1; intros; subst p s. simpl; apply in_or_app; left; trivial. contradiction. destruct (IH4' v) as [p [s [ps_in_pb v_in_p]]]. rewrite (proj2 case2); discriminate. destruct ps_in_pb as [ps_eq_patsub | ps_in_pb]. exists (Term f (pat1 :: lpat)); exists (Term g (sub1 :: lsub)); split. left; trivial. injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s. simpl; apply in_or_app; right; trivial. exists p; exists s; split; trivial; right; trivial. absurd (@None term = None); trivial. intros p s [ps_eq_patsub | ps_in_pb]. injection ps_eq_patsub; clear ps_eq_patsub; intros; subst; simpl. replace (apply_subst sigma pat1) with sub1. apply (f_equal (fun l => Term g (sub1 :: l))). assert (K := IH3' _ _ (or_introl _ (eq_refl _))). simpl in K; injection K; clear K; intro K. rewrite <- K; symmetry; apply map_eq. intros p p_in_lpat. rewrite <- subst_eq_vars. assert (K2 : forall v, In v (var_list p) -> find eq_var_bool v subst <> None). intros v v_in_p; apply IH2' with (Term g lpat) (Term g lsub); trivial. destruct (In_split _ _ p_in_lpat) as [lpat1 [lpat2 H']]; subst lpat. apply (@var_in_subterm v p (Term g (lpat1 ++ p :: lpat2)) (length lpat1 :: nil)); trivial. simpl; rewrite nth_error_at_pos; trivial. left; trivial. intros v v_in_p; generalize (K2 v v_in_p) (H2 v); simpl. destruct (find eq_var_bool v subst) as [v_subst | ]. clear K2; intros _ K2. destruct (K2 _ (eq_refl _)) as [b [K3 K4]]; rewrite K3; trivial. generalize (eq_bool_ok v_subst b); rewrite K4; intro K5; exact K5. intro; absurd (@None term = None); trivial. assert (K := IH3 _ _ (or_introl _ (eq_refl _))). rewrite <- K; symmetry. rewrite <- subst_eq_vars. assert (K2 : forall v, In v (var_list pat1) -> find eq_var_bool v subst1 <> None). intros v v_in_pat1; apply IH2 with pat1 sub1; trivial. left; trivial. intros v v_in_pat1; generalize (K2 v v_in_pat1) (H1 v); simpl. destruct (find eq_var_bool v subst1) as [v_subst1 | ]. clear K2; intros _ K2; rewrite (K2 _ (eq_refl _)); trivial. intro; absurd (@None term = None); trivial. rewrite <- (IH3' _ _ (or_intror _ ps_in_pb)). symmetry; rewrite <- subst_eq_vars. assert (K2 : forall v, In v (var_list p) -> find eq_var_bool v subst <> None). intros v v_in_p; apply IH2' with p s; trivial; right; trivial. intros v v_in_p; generalize (K2 v v_in_p) (H2 v); simpl. destruct (find eq_var_bool v subst) as [v_subst | ]. clear K2; intros _ K2; destruct (K2 _ (eq_refl _)) as [b [K3 K4]]; rewrite K3. generalize (eq_bool_ok v_subst b); rewrite K4; intro K5; exact K5. intro; absurd (@None term = None); trivial. discriminate. discriminate. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)