Matching-related equivalences #446
Conversation
TODO: prettify
| (* Proof for Γ ⊢ (θ -> (l = ti)) <-> (l /\ θ = ti /\ θ) *) | ||
|
|
||
| (* Helper lemma for predicate patterns. *) | ||
| Lemma predicate_iff φ₁ φ₂ : |
There was a problem hiding this comment.
Please move this to FOEqualityProofSystem.v.
| (* Proof for Γ ⊢ (∃. (l = ti)) <-> (ti ∈ ∃. l) *) | ||
|
|
||
| (* Single exists version. *) | ||
| Goal forall l ti, |
There was a problem hiding this comment.
Give this lemma a name, please.
|
|
||
| (* Definitions for multiple exists version. *) | ||
|
|
||
| Fixpoint functional_when_applied (n : nat) (φ : Pattern) := |
There was a problem hiding this comment.
Describe these definitions in comments a bit. For example, the result of many_ex n \phi is
There was a problem hiding this comment.
Additional remarks:
- This function is essentially opening n times, and checking whether the result is functional.
many_exis essentially quantifying n times.- Check whether these functions are just instances of Coq's/stdpp's n-times application (such as
PeanoNat.Nat.iter). functional_when_appliedshould be renamed to include opening instead of "apply" (since the pattern is opened and not applied).
| mlReflexivity. | ||
| Defined. | ||
|
|
||
| Lemma fwa_drop_one : forall n m l y, |
There was a problem hiding this comment.
This name is misleading, it should include "opening".
| apply le_lt_eq_dec in Hle as [Hle%Arith_prebase.lt_n_Sm_le | ->]. | ||
|
|
||
| (* Multiple exists version. *) | ||
| Goal forall l ti n m, |
There was a problem hiding this comment.
Give this theorem a name, please.
| all: try solve [(eapply extract_wfp + eapply extract_wfq); eauto]; mlApplyMeta IHn in "0"; mlAssumption. | ||
| Qed. | ||
|
|
||
| (* Proof for Γ ⊢ (⌈l /\ ti⌉) -> (ti ∈ ∃. l) *) |
There was a problem hiding this comment.
These comments would be nice for the previous Goals too.
|
|
||
| (* Definitions for multiple exists version. *) | ||
|
|
||
| Fixpoint fully_apply (n : nat) (p : Pattern) := |
There was a problem hiding this comment.
Rename it to many_open to match many_ex. Can this also be phrased with iter?
| Defined. | ||
|
|
||
| (* Multiple exists version. *) | ||
| Goal forall n m l ti, |
There was a problem hiding this comment.
Give this lemma a name, please.
| set_solver. | ||
| Defined. | ||
|
|
||
| Goal forall (sy : symbols) (a : evar), exists ti s M, forall ρ, |
There was a problem hiding this comment.
Explain this proposition in a comment, and if it is purely unification-specific, move it into Unification.v.
Equivalences relating to the matching algorithm.