File Unification
From MatchingLogic.Theories Require Export FOEquality_ProofSystem.
Import MatchingLogic.Logic.Notations.
Import MatchingLogic.Theories.Definedness_Syntax.Notations.
Close Scope equations_scope. (* Because of ! *)
Section unification.
Context {Σ : Signature} {syntax : Syntax}.
Section helpers.
Definition get_fresh_evar (φ : Pattern) : sig (.∉ free_evars φ).
End helpers.
Import MatchingLogic.Logic.Notations.
Import MatchingLogic.Theories.Definedness_Syntax.Notations.
Close Scope equations_scope. (* Because of ! *)
Section unification.
Context {Σ : Signature} {syntax : Syntax}.
Section helpers.
Definition get_fresh_evar (φ : Pattern) : sig (.∉ free_evars φ).
End helpers.
The naming of the following lemmas matches this article:
Unification in Matching Logic - Extended Version
Andrei Arusoaie, Dorel Lucanu
https://arxiv.org/abs/1811.02835v3
Lemma Prop₃_left: ∀ Γ φ φ',
theory ⊆ Γ →
well_formed φ → well_formed φ' →
Γ ⊢ (φ and (φ' =ml φ)) ---> (φ and φ').
Lemma Prop₃_right : ∀ Γ φ φ',
theory ⊆ Γ →
well_formed φ → well_formed φ' → mu_free φ' →
Γ ⊢ (ex , (φ =ml b0)) →
Γ ⊢ (ex , (φ' =ml b0)) →
Γ ⊢ (φ and φ') ---> (φ and (φ =ml φ')) .
Definition substitute_list (σ : list (evar × Pattern)) (t : Pattern) : Pattern := fold_left (fun φ '(x, φ') ⇒ φ^[[evar: x ↦ φ']]) σ t.
Lemma wf_substitute_list : ∀ σ t, wf (map snd σ) → well_formed t → well_formed (substitute_list σ t).
Definition predicate_list (σ : list (evar × Pattern)) : Pattern := fold_right (fun '(x, φ') φ ⇒ patt_free_evar x =ml φ' and φ) patt_top σ.
Lemma wf_predicate_list : ∀ σ, wf (map snd σ) → well_formed (predicate_list σ).
Lemma Lemma₁ : ∀ Γ φ t x, theory ⊆ Γ →
well_formed φ →
mu_free φ →
well_formed t →
Γ ⊢ (patt_free_evar x) =ml t ---> φ^[[evar:x↦t]] =ml φ.
Lemma Lemma₂ : ∀ Γ φ σ (i : ProofInfo),
theory ⊆ Γ → mu_free φ → well_formed φ →
forallb mu_free (map snd σ) → wf (map snd σ) →
Γ ⊢i substitute_list σ φ and predicate_list σ <--->
φ and predicate_list σ using i.
Definition is_unifier_of (σ : list (evar × Pattern)) t₁ t₂ := substitute_list σ t₁ =ml substitute_list σ t₂.
Lemma wf_is_unifier_of : ∀ σ t₁ t₂, wf (map snd σ) → well_formed t₁ → well_formed t₂ → well_formed (is_unifier_of σ t₁ t₂).
Lemma predicate_list_predicate Γ σ : theory ⊆ Γ → wf (map snd σ) → Γ ⊢ is_predicate_pattern (predicate_list σ).
(* Similar proof as in Definedness_ProofSystem but object level. *)
Lemma def_of_pred_impl_pred_obj Γ ψ :
theory ⊆ Γ →
well_formed ψ →
Γ ⊢ is_predicate_pattern ψ ---> ⌈ ψ ⌉ ---> ψ.
Lemma extend_total_to_imp Γ p f :
theory ⊆ Γ →
well_formed p →
well_formed f →
Γ ⊢ is_predicate_pattern p ---> (p ---> ⌊ f ⌋) ---> ⌊ p ---> f ⌋.
Tactic Notation "mlDeductHypo" constr(name) :=
match goal with
| [ |- context[ mkNH _ name (⌊ ?p ⌋) ] ] ⇒
match goal with
| [ |- context[ mkMLGoal _ ?t _ _ _ ] ] ⇒
mlDeduct name;
let i := fresh "i" in remember (ExGen := _, SVSubst := _, KT:= _, AKT := _) as i;
let H := fresh "H" in opose proof (hypothesis (t ∪ {[p]}) p _ ltac:(set_solver)) as H;
last first;
[use i in H |]
end
end.
Lemma extract_common_from_equality_r_2 Γ a b p :
theory ⊆ Γ →
well_formed a →
well_formed b →
well_formed p →
Γ ⊢ is_predicate_pattern p --->
(p ---> a =ml b) <---> (a and p) =ml (b and p).
Lemma Lemma₅ : ∀ (σ : list (evar × Pattern)) t₁ t₂ Γ,
theory ⊆ Γ →
well_formed t₁ → well_formed t₂ →
mu_free t₁ → mu_free t₂ →
wf (map snd σ) → forallb mu_free (map snd σ) →
Γ ⊢ is_unifier_of σ t₁ t₂ ---> predicate_list σ ---> (t₁ =ml t₂).
Lemma R₅' : ∀ x Γ, theory ⊆ Γ → Γ ⊢ (ex , patt_free_evar x =ml b0).
Definition WFPattern := sig well_formed.
Definition mkWFWrapper (f : Pattern → Pattern → Pattern) (wfp : ∀ a b, well_formed a → well_formed b → well_formed (f a b)) : WFPattern → WFPattern → WFPattern.
Definition WFPatt_imp := mkWFWrapper patt_imp well_formed_imp.
Notation "a wf---> b" := (WFPatt_imp a b) (at level 75, right associativity) : ml_scope.
Definition WFPatt_and := mkWFWrapper patt_and well_formed_and.
Notation "a 'wfand' b" := (WFPatt_and a b) (at level 72, left associativity) : ml_scope.
Definition WFPatt_iff := mkWFWrapper patt_iff well_formed_iff.
Notation "a wf<---> b" := (WFPatt_iff a b) (at level 74, no associativity) : ml_scope.
Definition WFPatt_equal := mkWFWrapper patt_equal well_formed_equal.
Notation "p wf=ml q" := (WFPatt_equal p q) (at level 67) : ml_scope.
Definition WFFree_evar_subst (x : evar) := mkWFWrapper (flip free_evar_subst x) (fun a b ⇒ well_formed_free_evar_subst x b a).
Notation "e ^wf[[ 'evar:' x ↦ e' ]]" := (WFFree_evar_subst x e' e) (at level 2, e' at level 200, left associativity, format "e ^wf[[ 'evar:' x ↦ e' ]]" ) : ml_scope.
Definition WFDerives (Γ : Theory) (p : WFPattern) : Set := derives Γ (proj1_sig p).
Notation "Γ ⊢wf ϕ" := (WFDerives Γ ϕ) (at level 95, no associativity).
Definition WFPatt_app := mkWFWrapper patt_app well_formed_app.
Notation "a wf⋅ b" := (WFPatt_app a b) (at level 66, left associativity) : ml_scope.
Lemma well_formed_free_evar : ∀ e, well_formed (patt_free_evar e).
This typeclass represents (in an abstract way) the unification problems of
Unification in Matching Logic - Extended Version
Andrei Arusoaie, Dorel Lucanu
https://arxiv.org/abs/1811.02835v3
In the following description, we highlight the connection to this paper.
Class UP (T : Type) := {
Insertion operation:
insertUP P (t, u) ~ P ∪ {t ≐ u}
insertUP : T → (WFPattern × WFPattern) → T;
Failed unification problem
bottomUP ~ ⊥
bottomUP : T;
Conversion to predicate. Expected to be conjunction of equalities.
toPredicateUP P ~ ϕᴾ
toPredicateUP : T → WFPattern;
Substitution of a variable to a pattern in every pattern of
a unification problem
substituteAllUP x t P ~ P{x ↦ t}
substituteAllUP : evar → WFPattern → T → T;
Creation of a singleton problem
singletonUP t u ~ {t ≐ u}
singletonUP : WFPattern → WFPattern → T;
Converting a unification problem maps insertion to conjunction.
toPredicateInsertUP : ∀ Γ t x y, Γ ⊢wf toPredicateUP (insertUP t (x, y)) wf<---> ((x wf=ml y) wfand (toPredicateUP t));
Converting a unification problem maps substitution of unification problems
to substitution of patterns.
toPredicateSubstituteAllUP : ∀ Γ t e p, Γ ⊢wf toPredicateUP (substituteAllUP e p t) wf<---> (toPredicateUP t)^wf[[evar:e↦p]];
Inserting into a non-⊥ unification problem cannot result ⊥.
insertNotBottomUP : ∀ t x, t ≠ bottomUP → insertUP t x ≠ bottomUP;
Converting a singleton problem to a predicate pattern gives us an equality.
toPredicateSingletonUP : ∀ Γ t1 t2, Γ ⊢wf toPredicateUP (singletonUP t1 t2) wf<---> (t1 wf=ml t2)
}.
Lemma lift_derives : ∀ Γ p, derives Γ (proj1_sig p) → WFDerives Γ p.
Lemma unwrap_wfwrapper : ∀ f wff a b, proj1_sig (mkWFWrapper f wff a b) = f (`a) (`b).
Lemma wfWFPattern : ∀ (p : WFPattern), well_formed (proj1_sig p).
Tactic Notation "mlDestructBotDocVer" := match goal with [ |- context [mkNH _ ?x patt_bott] ] ⇒ mlDestructBot x end.
Tactic Notation "refine_wf" := repeat first [
apply well_formed_imp |
apply well_formed_and |
apply well_formed_equal |
apply well_formed_free_evar_subst |
apply well_formed_top |
apply well_formed_free_evar
].
Tactic Notation "mlDecomposeAll" := do !
match goal with
| [ |- context[(mkMLGoal _ _ _ (patt_imp _ _) _)] ] ⇒ mlIntro
| [ |- context[mkNH _ ?x (patt_and _ _)] ] ⇒ mlDestructAnd x
end.
Lemma set_fold_disj_union_strong_equiv `{FinSet A C} Γ (f : A → WFPattern → WFPattern) (b : WFPattern) (X Y : C) :
(∀ x1 x2 b',
x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
Γ ⊢wf (f x1 (f x2 b')) wf<---> (f x2 (f x1 b'))) →
X ## Y →
Γ ⊢wf (set_fold f b (X ∪ Y)) wf<---> (set_fold f (set_fold f b X) Y).
(* Proof. *)
(* intros Hf Hdisj. unfold set_fold; simpl. *)
(* rewrite <- foldr_app. *)
(* epose proof foldr_permutation. *)
(* apply (foldr_permutation R f b). *)
(* - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf. *)
(* + apply elem_of_list_lookup_2 in Hj1. set_solver. *)
(* + apply elem_of_list_lookup_2 in Hj2. set_solver. *)
(* + intros →. pose proof (NoDup_elements (X ∪ Y)). *)
(* by eapply Hj, NoDup_lookup. *)
(* - by rewrite elements_disj_union, (comm (++)). *)
(* Qed. *)
Lemma in_set_implies_in_predicate `{FinSet A C} `{!LeibnizEquiv C} : ∀ Γ f b x (X : C), x ∈ X → Γ ⊢wf set_fold (WFPatt_and ∘ f) b X wf---> f x.
Lemma WFPattern_eq_dec : EqDecision (WFPattern × WFPattern).
#[refine] Instance optionSetUP `{H : ElemOf (WFPattern × WFPattern) T, H0 : Empty T, H1 : Singleton (WFPattern × WFPattern) T, H2 : Union T, H3 : Intersection T, H4 : Difference T, H5 : Elements (WFPattern × WFPattern) T, @FinSet (WFPattern × WFPattern) T H H0 H1 H2 H3 H4 H5 WFPattern_eq_dec, !LeibnizEquiv T} : UP (option T) := {
insertUP t x := option_map ({[x]} ∪.) t;
bottomUP := None;
toPredicateUP := from_option (set_fold (WFPatt_and ∘ (fun '(x, y) ⇒ x wf=ml y)) (Top ↾ well_formed_top)) (patt_bott ↾ well_formed_bott);
substituteAllUP e p := option_map (set_map (fun '(x, y) ⇒ (x^wf[[evar:e↦p]], y^wf[[evar:e↦p]])));
singletonUP t1 t2 := Some {[(t1, t2)]}
}.
Reserved Notation "P ===> P'" (at level 80).
Inductive unification_step {T : Set} {UPT : UP T} : T → T → Set :=
| deleteUS : ∀ P t,
P ≠ bottomUP →
insertUP P (t, t) ===> P
| decompositionUS : ∀ P f t g u,
P ≠ bottomUP →
insertUP P (f wf⋅ t, g wf⋅ u) ===> insertUP (insertUP P (f, g)) (t, u)
| symbol_clash_lUS : ∀ P f t,
P ≠ bottomUP →
patt_sym f ≠ `t →
(∀ x, `t ≠ patt_free_evar x) →
insertUP P (patt_sym f ↾ well_formed_sym f, t) ===> bottomUP
| symbol_clash_rUS : ∀ P f t,
P ≠ bottomUP →
patt_sym f ≠ `t →
(∀ x, `t ≠ patt_free_evar x) →
insertUP P (t, patt_sym f ↾ well_formed_sym f) ===> bottomUP
| orientUS : ∀ P x y,
P ≠ bottomUP →
insertUP P (x, patt_free_evar y ↾ well_formed_free_evar y) ===> insertUP P (patt_free_evar y ↾ well_formed_free_evar y, x)
| occours_checkUS : ∀ P x t,
P ≠ bottomUP →
x ∈ free_evars (`t) →
insertUP P (patt_free_evar x ↾ well_formed_free_evar x, t) ===> bottomUP
| eliminationUS : ∀ P x t,
P ≠ bottomUP →
x ∉ free_evars (`t) →
mu_free (`t) →
insertUP P (patt_free_evar x ↾ well_formed_free_evar x, t) ===> insertUP (substituteAllUP x t P) (patt_free_evar x ↾ well_formed_free_evar x, t)
where "P ===> P'" := (unification_step P P').
}.
Lemma lift_derives : ∀ Γ p, derives Γ (proj1_sig p) → WFDerives Γ p.
Lemma unwrap_wfwrapper : ∀ f wff a b, proj1_sig (mkWFWrapper f wff a b) = f (`a) (`b).
Lemma wfWFPattern : ∀ (p : WFPattern), well_formed (proj1_sig p).
Tactic Notation "mlDestructBotDocVer" := match goal with [ |- context [mkNH _ ?x patt_bott] ] ⇒ mlDestructBot x end.
Tactic Notation "refine_wf" := repeat first [
apply well_formed_imp |
apply well_formed_and |
apply well_formed_equal |
apply well_formed_free_evar_subst |
apply well_formed_top |
apply well_formed_free_evar
].
Tactic Notation "mlDecomposeAll" := do !
match goal with
| [ |- context[(mkMLGoal _ _ _ (patt_imp _ _) _)] ] ⇒ mlIntro
| [ |- context[mkNH _ ?x (patt_and _ _)] ] ⇒ mlDestructAnd x
end.
Lemma set_fold_disj_union_strong_equiv `{FinSet A C} Γ (f : A → WFPattern → WFPattern) (b : WFPattern) (X Y : C) :
(∀ x1 x2 b',
x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
Γ ⊢wf (f x1 (f x2 b')) wf<---> (f x2 (f x1 b'))) →
X ## Y →
Γ ⊢wf (set_fold f b (X ∪ Y)) wf<---> (set_fold f (set_fold f b X) Y).
(* Proof. *)
(* intros Hf Hdisj. unfold set_fold; simpl. *)
(* rewrite <- foldr_app. *)
(* epose proof foldr_permutation. *)
(* apply (foldr_permutation R f b). *)
(* - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf. *)
(* + apply elem_of_list_lookup_2 in Hj1. set_solver. *)
(* + apply elem_of_list_lookup_2 in Hj2. set_solver. *)
(* + intros →. pose proof (NoDup_elements (X ∪ Y)). *)
(* by eapply Hj, NoDup_lookup. *)
(* - by rewrite elements_disj_union, (comm (++)). *)
(* Qed. *)
Lemma in_set_implies_in_predicate `{FinSet A C} `{!LeibnizEquiv C} : ∀ Γ f b x (X : C), x ∈ X → Γ ⊢wf set_fold (WFPatt_and ∘ f) b X wf---> f x.
Lemma WFPattern_eq_dec : EqDecision (WFPattern × WFPattern).
#[refine] Instance optionSetUP `{H : ElemOf (WFPattern × WFPattern) T, H0 : Empty T, H1 : Singleton (WFPattern × WFPattern) T, H2 : Union T, H3 : Intersection T, H4 : Difference T, H5 : Elements (WFPattern × WFPattern) T, @FinSet (WFPattern × WFPattern) T H H0 H1 H2 H3 H4 H5 WFPattern_eq_dec, !LeibnizEquiv T} : UP (option T) := {
insertUP t x := option_map ({[x]} ∪.) t;
bottomUP := None;
toPredicateUP := from_option (set_fold (WFPatt_and ∘ (fun '(x, y) ⇒ x wf=ml y)) (Top ↾ well_formed_top)) (patt_bott ↾ well_formed_bott);
substituteAllUP e p := option_map (set_map (fun '(x, y) ⇒ (x^wf[[evar:e↦p]], y^wf[[evar:e↦p]])));
singletonUP t1 t2 := Some {[(t1, t2)]}
}.
Reserved Notation "P ===> P'" (at level 80).
Inductive unification_step {T : Set} {UPT : UP T} : T → T → Set :=
| deleteUS : ∀ P t,
P ≠ bottomUP →
insertUP P (t, t) ===> P
| decompositionUS : ∀ P f t g u,
P ≠ bottomUP →
insertUP P (f wf⋅ t, g wf⋅ u) ===> insertUP (insertUP P (f, g)) (t, u)
| symbol_clash_lUS : ∀ P f t,
P ≠ bottomUP →
patt_sym f ≠ `t →
(∀ x, `t ≠ patt_free_evar x) →
insertUP P (patt_sym f ↾ well_formed_sym f, t) ===> bottomUP
| symbol_clash_rUS : ∀ P f t,
P ≠ bottomUP →
patt_sym f ≠ `t →
(∀ x, `t ≠ patt_free_evar x) →
insertUP P (t, patt_sym f ↾ well_formed_sym f) ===> bottomUP
| orientUS : ∀ P x y,
P ≠ bottomUP →
insertUP P (x, patt_free_evar y ↾ well_formed_free_evar y) ===> insertUP P (patt_free_evar y ↾ well_formed_free_evar y, x)
| occours_checkUS : ∀ P x t,
P ≠ bottomUP →
x ∈ free_evars (`t) →
insertUP P (patt_free_evar x ↾ well_formed_free_evar x, t) ===> bottomUP
| eliminationUS : ∀ P x t,
P ≠ bottomUP →
x ∉ free_evars (`t) →
mu_free (`t) →
insertUP P (patt_free_evar x ↾ well_formed_free_evar x, t) ===> insertUP (substituteAllUP x t P) (patt_free_evar x ↾ well_formed_free_evar x, t)
where "P ===> P'" := (unification_step P P').
TODO: this axiom should be placed into Γ later, and we have to use `hypothesis`
to obtain it. For this, we have to create a spec. for unification/term
algebras.
Axiom injectivity : ∀ Γ f t g u, Γ ⊢ (f ⋅ t) =ml (g ⋅ u) ---> (f =ml g) and (t =ml u).
Tactic Notation "inside" tactic(inside) "outside" tactic(outside) :=
match goal with
| [ |- of_MLGoal _ ] ⇒ inside
| _ ⇒ outside
end.
Lemma Lemma₃ {T : Set} {UPT : UP T} Γ P P' : theory ⊆ Γ → P ===> P' → P' ≠ bottomUP → Γ ⊢wf toPredicateUP P wf---> toPredicateUP P'.
Definition compose_substitution (σ η : list (evar × Pattern)) : list (evar × Pattern) := map (fun '(e, p) ⇒ (e, substitute_list η p)) σ.
Definition more_general_substitution (σ η : list (evar × Pattern)) : Prop := ∃ (θ : list (evar × Pattern)), compose_substitution σ θ = η.
Definition is_most_general_unifier_of (σ : list (evar × Pattern)) (t₁ t₂ : Pattern) : Type := (∀ Γ, Γ ⊢ is_unifier_of σ t₁ t₂) × (∀ η, more_general_substitution σ η).
(* NOTE Could I make US a Prop and use stdpp's rtc for this? *)
Inductive USrtc {T : Set} {UPT : UP T} : T → T → Set :=
| USrtc_last : ∀ a, USrtc a a
| USrtc_step : ∀ a b c, a ===> b → USrtc b c → USrtc a c
.
Tactic Notation "inside" tactic(inside) "outside" tactic(outside) :=
match goal with
| [ |- of_MLGoal _ ] ⇒ inside
| _ ⇒ outside
end.
Lemma Lemma₃ {T : Set} {UPT : UP T} Γ P P' : theory ⊆ Γ → P ===> P' → P' ≠ bottomUP → Γ ⊢wf toPredicateUP P wf---> toPredicateUP P'.
Definition compose_substitution (σ η : list (evar × Pattern)) : list (evar × Pattern) := map (fun '(e, p) ⇒ (e, substitute_list η p)) σ.
Definition more_general_substitution (σ η : list (evar × Pattern)) : Prop := ∃ (θ : list (evar × Pattern)), compose_substitution σ θ = η.
Definition is_most_general_unifier_of (σ : list (evar × Pattern)) (t₁ t₂ : Pattern) : Type := (∀ Γ, Γ ⊢ is_unifier_of σ t₁ t₂) × (∀ η, more_general_substitution σ η).
(* NOTE Could I make US a Prop and use stdpp's rtc for this? *)
Inductive USrtc {T : Set} {UPT : UP T} : T → T → Set :=
| USrtc_last : ∀ a, USrtc a a
| USrtc_step : ∀ a b c, a ===> b → USrtc b c → USrtc a c
.
The formalized unification algorithm gives us an MGU.
Axiom convenient : ∀ {T : Set} {UPT : UP T} σ t1 t2, is_most_general_unifier_of σ (`t1) (`t2) → {P : T & (USrtc (singletonUP t1 t2) P × (P ≠ bottomUP) × ∀ Γ, Γ ⊢ projT1 (toPredicateUP P) <---> predicate_list σ)%type}.
Lemma Lemma₄_helper : ∀ {T : Set} {UPT : UP T} Γ P P',
theory ⊆ Γ →
USrtc P P' →
P' ≠ bottomUP →
Γ ⊢wf toPredicateUP P wf---> toPredicateUP P'.
From stdpp Require Import gmap.
Definition wf := Pattern.wf.
Lemma Lemma₄ : ∀ Γ (σ : list (evar × Pattern)) (t1 t2 : WFPattern),
theory ⊆ Γ → wf (map snd σ) →
is_most_general_unifier_of σ (`t1) (`t2) → Γ ⊢ `t1 =ml `t2 ---> predicate_list σ.
Lemma Lemma₆ : ∀ Γ (σ : list (evar × Pattern)) (t1 t2 : WFPattern),
theory ⊆ Γ →
wf (map snd σ) →
mu_free (`t1) → mu_free (`t2) →
forallb mu_free (map snd σ) →
is_most_general_unifier_of σ (`t1) (`t2) →
Γ ⊢ (`t1 =ml `t2) <---> predicate_list σ.
Lemma Prop3_full : ∀ Γ t1 t2,
theory ⊆ Γ → well_formed t1 → well_formed t2 → mu_free t2 →
Γ ⊢ is_functional t1 → Γ ⊢ is_functional t2 →
Γ ⊢ t1 and t2 <---> t1 and t1 =ml t2.
Lemma Theorem₁ : ∀ Γ σ t1 t2,
theory ⊆ Γ →
well_formed t1 → well_formed t2 →
wf (map snd σ) →
mu_free t1 → mu_free t2 →
forallb mu_free (map snd σ) →
Γ ⊢ is_functional t1 → Γ ⊢ is_functional t2 →
is_most_general_unifier_of σ t1 t2 →
(Γ ⊢ (t1 and t2) =ml (t1 and predicate_list σ)) × (Γ ⊢ (t1 and t2) =ml (t2 and predicate_list σ)).
Tactic Notation "mlConjFast" constr(a) constr(b) "as" constr(c) "wfby" tactic(d) := match goal with | [ |- context[mkNH _ a ?x] ] ⇒ match goal with | [ |- context[mkNH _ b ?y] ] ⇒ mlAssert (c : (x and y)); [d | mlSplitAnd; [mlExact a | mlExact b] |] end end.
Tactic Notation "mlConjFast" constr(a) constr(b) "as" constr(c) := mlConjFast a b as c wfby idtac.
Goal ∀ Γ (f' g' one' : symbols) (x' y' z' : evar) (*one : WFPattern*),
x' ≠ z' → y' ≠ z' →
theory ⊆ Γ →
let f := (patt_sym f' ↾ well_formed_sym f') in
let g := (patt_sym g' ↾ well_formed_sym g') in
let one := (patt_sym one' ↾ well_formed_sym one') in
let x := (patt_free_evar x' ↾ well_formed_free_evar x') in
let y := (patt_free_evar y' ↾ well_formed_free_evar y') in
let z := (patt_free_evar z' ↾ well_formed_free_evar z') in
let t1 := f wf⋅ x wf⋅ (g wf⋅ one) wf⋅ (g wf⋅ z) in
let t2 := f wf⋅ (g wf⋅ y) wf⋅ (g wf⋅ y) wf⋅ (g wf⋅ (g wf⋅ x)) in
Lemma Lemma₄_helper : ∀ {T : Set} {UPT : UP T} Γ P P',
theory ⊆ Γ →
USrtc P P' →
P' ≠ bottomUP →
Γ ⊢wf toPredicateUP P wf---> toPredicateUP P'.
From stdpp Require Import gmap.
Definition wf := Pattern.wf.
Lemma Lemma₄ : ∀ Γ (σ : list (evar × Pattern)) (t1 t2 : WFPattern),
theory ⊆ Γ → wf (map snd σ) →
is_most_general_unifier_of σ (`t1) (`t2) → Γ ⊢ `t1 =ml `t2 ---> predicate_list σ.
Lemma Lemma₆ : ∀ Γ (σ : list (evar × Pattern)) (t1 t2 : WFPattern),
theory ⊆ Γ →
wf (map snd σ) →
mu_free (`t1) → mu_free (`t2) →
forallb mu_free (map snd σ) →
is_most_general_unifier_of σ (`t1) (`t2) →
Γ ⊢ (`t1 =ml `t2) <---> predicate_list σ.
Lemma Prop3_full : ∀ Γ t1 t2,
theory ⊆ Γ → well_formed t1 → well_formed t2 → mu_free t2 →
Γ ⊢ is_functional t1 → Γ ⊢ is_functional t2 →
Γ ⊢ t1 and t2 <---> t1 and t1 =ml t2.
Lemma Theorem₁ : ∀ Γ σ t1 t2,
theory ⊆ Γ →
well_formed t1 → well_formed t2 →
wf (map snd σ) →
mu_free t1 → mu_free t2 →
forallb mu_free (map snd σ) →
Γ ⊢ is_functional t1 → Γ ⊢ is_functional t2 →
is_most_general_unifier_of σ t1 t2 →
(Γ ⊢ (t1 and t2) =ml (t1 and predicate_list σ)) × (Γ ⊢ (t1 and t2) =ml (t2 and predicate_list σ)).
Tactic Notation "mlConjFast" constr(a) constr(b) "as" constr(c) "wfby" tactic(d) := match goal with | [ |- context[mkNH _ a ?x] ] ⇒ match goal with | [ |- context[mkNH _ b ?y] ] ⇒ mlAssert (c : (x and y)); [d | mlSplitAnd; [mlExact a | mlExact b] |] end end.
Tactic Notation "mlConjFast" constr(a) constr(b) "as" constr(c) := mlConjFast a b as c wfby idtac.
Goal ∀ Γ (f' g' one' : symbols) (x' y' z' : evar) (*one : WFPattern*),
x' ≠ z' → y' ≠ z' →
theory ⊆ Γ →
let f := (patt_sym f' ↾ well_formed_sym f') in
let g := (patt_sym g' ↾ well_formed_sym g') in
let one := (patt_sym one' ↾ well_formed_sym one') in
let x := (patt_free_evar x' ↾ well_formed_free_evar x') in
let y := (patt_free_evar y' ↾ well_formed_free_evar y') in
let z := (patt_free_evar z' ↾ well_formed_free_evar z') in
let t1 := f wf⋅ x wf⋅ (g wf⋅ one) wf⋅ (g wf⋅ z) in
let t2 := f wf⋅ (g wf⋅ y) wf⋅ (g wf⋅ y) wf⋅ (g wf⋅ (g wf⋅ x)) in
f is a functional symbol
(all, all, all, ex, (patt_sym f') ⋅ b3 ⋅ b2 ⋅ b1 =ml b0) ∈ Γ →
g is a functional symbol
(all, ex, (patt_sym g') ⋅ b1 =ml b0) ∈ Γ →
one is a functional symbol
(ex, patt_sym one' =ml b0) ∈ Γ →
(*
TODO: after defining term algebra spec. these functional axioms should be
in the theory of the spec.
*)
{σ & Γ ⊢ `t1 and `t2 <---> `t1 and predicate_list σ}.
End unification.
Close Scope ml_scope.
Close Scope string_scope.
Close Scope list_scope.
(*
TODO: after defining term algebra spec. these functional axioms should be
in the theory of the spec.
*)
{σ & Γ ⊢ `t1 and `t2 <---> `t1 and predicate_list σ}.
End unification.
Close Scope ml_scope.
Close Scope string_scope.
Close Scope list_scope.
This page has been generated by coqdoc