Unification #431
Unification #431
Conversation
Well-formedness is good now Still needs some uniqueness on subs
There was a problem hiding this comment.
In general, the code is good this way, I only made some suggestions where to move the general lemmas. The anti-unification developments could be phrased as a separate PR. Also, if there are unnecessary comments (e.g., failed proof attempts), any Search, Print, About, and Check commands, these should be removed.
| (* https://github.com/harp-project/AML-Formalization/blob/09f24d95119769ce578c8c15eceba5a3a00c45d4/matching-logic/src/Theories/Nat_ProofSystem.v#L392 *) | ||
| Section predicate_stuff. | ||
|
|
||
| Axiom predicate_equiv : |
There was a problem hiding this comment.
You can copy the proof for these, since the branch mentioned above won't be merged into main in the short term future.
|
|
||
| (* These [are from/should be part of] that branch. *) | ||
| (* https://github.com/harp-project/AML-Formalization/blob/09f24d95119769ce578c8c15eceba5a3a00c45d4/matching-logic/src/Theories/Nat_ProofSystem.v#L392 *) | ||
| Section predicate_stuff. |
There was a problem hiding this comment.
If nothing is against it, you could move these theorems into Definedness_ProofSystem.v.
|
|
||
| Section helpers. | ||
|
|
||
| Lemma functional_pattern_defined : |
There was a problem hiding this comment.
This lemma should be moved to FOEquality_ProofSystem.v.
| * mlExact "H0". | ||
| Defined. | ||
|
|
||
| Lemma membership_equal_equal : |
There was a problem hiding this comment.
This lemma should be moved to FOEquality_ProofSystem.v.
| mlExactMeta Func2. | ||
| Defined. | ||
|
|
||
| Lemma free_evar_subst_id : |
There was a problem hiding this comment.
This lemma should be moved to Substitution.v.
| Γ ⊢ φ and φ' =ml φ' ---> φ | ||
| . | ||
| (* foldr_ind_set is more general *) | ||
| Lemma foldr_preserves_function_set {A : Type} (t : A -> Pattern) (P : Pattern -> Set) (f : A -> Pattern -> Pattern) x xs : |
There was a problem hiding this comment.
This could go into stpp_ext.v.
| Defined. | ||
|
|
||
| End corollaries. | ||
|
|
There was a problem hiding this comment.
Here (or at the beginning of the file), could you make a comment on the sources where the names come from (i.e., cite the two papers on unification).
There was a problem hiding this comment.
By "names", I meant "Lemma_3", "Prop_3_left" etc.
|
|
||
| Theorem wf_unify_pattern : | ||
| forall u, wf_unification u -> well_formed (unification_to_pattern u). | ||
| Class UP (T : Type) := { |
There was a problem hiding this comment.
A short textual description could help here on what the fields of this class represent.
|
|
||
| Section stdpp_but_for_set. | ||
|
|
||
| Lemma set_choose_or_empty' `{FinSet A C} (X : C) : (sig (.∈ X)) + (X ≡ ∅). |
There was a problem hiding this comment.
From the following (unadmitted) lemmas, those which are independent of the unification could go into stdpp_ext.v.
| | (patt_free_evar x, p2)::xs => | ||
| | (p1, p2)::xs => unify_step3 xs | ||
| end. *) | ||
| Section antiunification. |
There was a problem hiding this comment.
The anti-unification developments can go into a separate file in the same folder (which could depend on this module if needed).
No description provided.