proposition: Lemma matching_unfold2 : forall pb, matching pb = match pb with | nil => Some nil | (patt, subj) :: pb => match patt with | Var x => match matching pb with | Some subst => merge eq_var_bool eq_bool ((x,subj) :: nil) subst | None => None end | Term f l => match subj with | Var _ => None | Term g m => if eq_symb_bool f g then match l with | nil => match m with | nil => matching pb | sub1 :: lsub => None end | pat1 :: lpat => match m with | nil => None | sub1 :: lsub => match (matching ((pat1, sub1) :: nil)) with | Some subst1 => match (matching ((Term f lpat, Term g lsub) :: pb)) with | Some subst => merge eq_var_bool eq_bool subst1 subst | None => None end | None => None end end end else None end end end.
proof: Proof. intros pb; rewrite matching_unfold; unfold F_matching; simpl. destruct pb as [ | [patt subj] pb]; trivial. destruct patt as [ x | f l]; trivial. destruct subj as [x | g m]; trivial. case (eq_symb_bool f g); trivial. destruct l as [ | pat1 lpat]; destruct m as [ | sub1 lsub]; trivial. destruct (matching pb); trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)